From c3593bcc411516b445effe97984cb79ff4dd01f4 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 11 Feb 2025 10:02:40 +0100 Subject: [PATCH 1/3] [CI] Update setup-ocaml action --- .github/workflows/doc.yml | 2 +- .github/workflows/release.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index d29ca187f..316c28b6a 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -23,7 +23,7 @@ jobs: uses: actions/checkout@v3 - name: setup ocaml - uses: avsm/setup-ocaml@v3 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: 4.14.2 diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index afd7e4994..d237c44bc 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -63,7 +63,7 @@ jobs: fetch-tags: 'true' - name: Use OCaml 4.14.x - uses: avsm/setup-ocaml@v3 + uses: ocaml/setup-ocaml@v3 with: ocaml-compiler: 4.14.x opam-local-packages: | From f6df88c5fe8695aebfe30ba726801129f2ba406e Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 7 Feb 2025 11:03:44 +0100 Subject: [PATCH 2/3] Enable compilation without the coq shim on Rocq 9.0 --- .github/workflows/ci.yml | 2 +- .github/workflows/doc.yml | 6 +- .github/workflows/nix-action-coq-8.20.yml | 5 - .github/workflows/nix-action-coq-master.yml | 63 ----- .github/workflows/nix-action-rocq-9.0.yml | 63 ----- .gitignore | 21 +- .nix/config.nix | 2 - .../coq-elpi-no-stdlib/default.nix | 11 - .../coq-elpi-tests-stdlib/default.nix | 3 + .nix/coq-overlays/coq-elpi-tests/default.nix | 4 - .nix/coq-overlays/coq-elpi/default.nix | 123 +++++++++ .../hierarchy-builder/default.nix | 51 ++++ .vscode/settings.json | 6 +- Makefile | 63 +++-- README.md | 6 +- apps/NES/elpi/dune | 6 +- apps/NES/tests/dune | 3 +- apps/NES/theories/dune | 2 +- apps/coercion/src/META.coq-elpi-coercion | 10 - apps/coercion/src/{dune => dune.in} | 6 +- apps/coercion/src/elpi_coercion_plugin.mlpack | 2 +- ...n_hook.mlg => rocq_elpi_coercion_hook.mlg} | 18 +- apps/coercion/tests/dune | 2 +- apps/coercion/theories/coercion.v | 2 +- apps/coercion/theories/dune | 4 +- apps/cs/src/META.coq-elpi-cs | 10 - apps/cs/src/{dune => dune.in} | 6 +- apps/cs/src/elpi_cs_plugin.mlpack | 2 +- ...elpi_cs_hook.mlg => rocq_elpi_cs_hook.mlg} | 16 +- apps/cs/tests/dune | 2 +- apps/cs/theories/cs.v | 2 +- apps/cs/theories/dune | 4 +- apps/derive/elpi/dune | 6 +- apps/derive/elpi/paramX_lib.elpi | 2 +- apps/derive/tests-stdlib/dune | 2 +- apps/derive/tests/dune | 2 +- apps/derive/theories/dune | 2 +- apps/eltac/tests-stdlib/dune | 2 +- apps/eltac/tests/dune | 2 +- apps/eltac/theories/dune | 2 +- apps/locker/elpi/dune | 6 +- apps/locker/tests/dune | 2 +- apps/locker/theories/dune | 2 +- apps/tc/README.md | 4 +- apps/tc/elpi/dune | 6 +- apps/tc/src/META.coq-elpi-tc | 10 - apps/tc/src/{dune => dune.in} | 6 +- apps/tc/src/elpi_tc_plugin.mlpack | 8 +- ...ml => rocq_elpi_class_tactics_takeover.ml} | 32 +-- ...i => rocq_elpi_class_tactics_takeover.mli} | 8 +- ...elpi_tc_hook.mlg => rocq_elpi_tc_hook.mlg} | 8 +- ...c_register.ml => rocq_elpi_tc_register.ml} | 18 +- ...q_elpi_tc_time.ml => rocq_elpi_tc_time.ml} | 4 +- apps/tc/tests-stdlib/dune | 2 +- apps/tc/tests/dune | 2 +- apps/tc/tests/test_backtrack_several_goals.v | 4 +- apps/tc/theories/dune | 4 +- apps/tc/theories/tc.v | 4 +- apps/tc/theories/wip.v | 4 +- builtin-doc/coq-builtin-synterp.elpi | 2 +- builtin-doc/coq-builtin.elpi | 6 +- builtin-doc/dune | 2 +- builtin-doc/gen_doc.ml | 2 +- coq-elpi-tests.opam | 29 -- coq-elpi.opam | 29 +- dune-project | 20 +- elpi/coq-arg-HOAS.elpi | 2 +- elpi/coq-elpi-checker.elpi | 2 +- elpi/coq-lib-common.elpi | 2 +- elpi/coq-lib.elpi | 2 +- elpi/dune | 6 +- etc/dune | 12 +- etc/tools/dune | 2 + etc/tools/hash.ml | 2 + etc/tools/hash.mli | 0 etc/with-rocq-wrap.sh | 59 +++++ examples-stdlib/dune | 4 +- examples/dune | 4 +- examples/tutorial_coq_elpi_HOAS.v | 6 +- examples/tutorial_coq_elpi_tactic.v | 2 +- rocq-elpi.opam | 44 ++++ src/META.coq-elpi | 10 - src/README.md | 4 +- src/{dune => dune.in} | 20 +- src/elpi_plugin.mlpack | 30 +-- src/{coq_elpi_HOAS.ml => rocq_elpi_HOAS.ml} | 20 +- src/{coq_elpi_HOAS.mli => rocq_elpi_HOAS.mli} | 2 +- ...elpi_arg_HOAS.ml => rocq_elpi_arg_HOAS.ml} | 102 +++---- ...pi_arg_HOAS.mli => rocq_elpi_arg_HOAS.mli} | 16 +- ...rg_syntax.mlg => rocq_elpi_arg_syntax.mlg} | 24 +- ...elpi_builtins.ml => rocq_elpi_builtins.ml} | 248 +++++++++--------- ...pi_builtins.mli => rocq_elpi_builtins.mli} | 10 +- ...nterp.ml => rocq_elpi_builtins_synterp.ml} | 34 +-- ...erp.mli => rocq_elpi_builtins_synterp.mli} | 14 +- ...otation.ml => rocq_elpi_glob_quotation.ml} | 18 +- ...ation.mli => rocq_elpi_glob_quotation.mli} | 6 +- src/{coq_elpi_graph.ml => rocq_elpi_graph.ml} | 0 ...coq_elpi_graph.mli => rocq_elpi_graph.mli} | 0 ...otation.ml => rocq_elpi_name_quotation.ml} | 4 +- ...elpi_programs.ml => rocq_elpi_programs.ml} | 48 ++-- ...pi_programs.mli => rocq_elpi_programs.mli} | 4 +- src/{coq_elpi_utils.ml => rocq_elpi_utils.ml} | 2 +- ...coq_elpi_utils.mli => rocq_elpi_utils.mli} | 2 +- ..._vernacular.ml => rocq_elpi_vernacular.ml} | 110 ++++---- ...ernacular.mli => rocq_elpi_vernacular.mli} | 16 +- ...ax.mlg => rocq_elpi_vernacular_syntax.mlg} | 26 +- tests-stdlib/dune | 4 +- tests-stdlib/test_open_terms.v | 2 +- tests/dune | 2 +- tests/test_API.v | 2 +- theories-stdlib/Program/dune | 4 +- theories-stdlib/dune.in | 24 +- theories/core/dune | 24 +- theories/dune | 6 +- theories/elpi.v.in | 2 +- 115 files changed, 916 insertions(+), 843 deletions(-) delete mode 100644 .nix/coq-overlays/coq-elpi-no-stdlib/default.nix create mode 100644 .nix/coq-overlays/coq-elpi/default.nix create mode 100644 .nix/coq-overlays/hierarchy-builder/default.nix delete mode 100644 apps/coercion/src/META.coq-elpi-coercion rename apps/coercion/src/{dune => dune.in} (56%) rename apps/coercion/src/{coq_elpi_coercion_hook.mlg => rocq_elpi_coercion_hook.mlg} (82%) delete mode 100644 apps/cs/src/META.coq-elpi-cs rename apps/cs/src/{dune => dune.in} (57%) rename apps/cs/src/{coq_elpi_cs_hook.mlg => rocq_elpi_cs_hook.mlg} (85%) delete mode 100644 apps/tc/src/META.coq-elpi-tc rename apps/tc/src/{dune => dune.in} (57%) rename apps/tc/src/{coq_elpi_class_tactics_takeover.ml => rocq_elpi_class_tactics_takeover.ml} (79%) rename apps/tc/src/{coq_elpi_class_tactics_takeover.mli => rocq_elpi_class_tactics_takeover.mli} (51%) rename apps/tc/src/{coq_elpi_tc_hook.mlg => rocq_elpi_tc_hook.mlg} (94%) rename apps/tc/src/{coq_elpi_tc_register.ml => rocq_elpi_tc_register.ml} (88%) rename apps/tc/src/{coq_elpi_tc_time.ml => rocq_elpi_tc_time.ml} (83%) delete mode 100644 coq-elpi-tests.opam create mode 100644 etc/tools/dune create mode 100644 etc/tools/hash.ml create mode 100644 etc/tools/hash.mli create mode 100755 etc/with-rocq-wrap.sh create mode 100644 rocq-elpi.opam delete mode 100644 src/META.coq-elpi rename src/{dune => dune.in} (69%) rename src/{coq_elpi_HOAS.ml => rocq_elpi_HOAS.ml} (99%) rename src/{coq_elpi_HOAS.mli => rocq_elpi_HOAS.mli} (99%) rename src/{coq_elpi_arg_HOAS.ml => rocq_elpi_arg_HOAS.ml} (92%) rename src/{coq_elpi_arg_HOAS.mli => rocq_elpi_arg_HOAS.mli} (93%) rename src/{coq_elpi_arg_syntax.mlg => rocq_elpi_arg_syntax.mlg} (96%) rename src/{coq_elpi_builtins.ml => rocq_elpi_builtins.ml} (95%) rename src/{coq_elpi_builtins.mli => rocq_elpi_builtins.mli} (74%) rename src/{coq_elpi_builtins_synterp.ml => rocq_elpi_builtins_synterp.ml} (97%) rename src/{coq_elpi_builtins_synterp.mli => rocq_elpi_builtins_synterp.mli} (89%) rename src/{coq_elpi_glob_quotation.ml => rocq_elpi_glob_quotation.ml} (98%) rename src/{coq_elpi_glob_quotation.mli => rocq_elpi_glob_quotation.mli} (86%) rename src/{coq_elpi_graph.ml => rocq_elpi_graph.ml} (100%) rename src/{coq_elpi_graph.mli => rocq_elpi_graph.mli} (100%) rename src/{coq_elpi_name_quotation.ml => rocq_elpi_name_quotation.ml} (96%) rename src/{coq_elpi_programs.ml => rocq_elpi_programs.ml} (96%) rename src/{coq_elpi_programs.mli => rocq_elpi_programs.mli} (98%) rename src/{coq_elpi_utils.ml => rocq_elpi_utils.ml} (99%) rename src/{coq_elpi_utils.mli => rocq_elpi_utils.mli} (98%) rename src/{coq_elpi_vernacular.ml => rocq_elpi_vernacular.ml} (86%) rename src/{coq_elpi_vernacular.mli => rocq_elpi_vernacular.mli} (87%) rename src/{coq_elpi_vernacular_syntax.mlg => rocq_elpi_vernacular_syntax.mlg} (96%) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4cd4fb5a3..af8131ba2 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -25,7 +25,7 @@ jobs: - uses: actions/checkout@v3 - uses: coq-community/docker-coq-action@v1 with: - opam_file: 'coq-elpi.opam' + opam_file: 'rocq-elpi.opam' custom_image: ${{ matrix.image }} export: 'OPAMWITHTEST OPAMIGNORECONSTRAINTS OPAMVERBOSE' # space-separated list of variables env: diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index 316c28b6a..e80a9b629 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -34,13 +34,15 @@ jobs: opam repo add coq-dev https://coq.inria.fr/opam/core-dev opam repo add extra-dev https://coq.inria.fr/opam/extra-dev opam update - opam install coq-serapi.8.20.0+0.20.0 ./coq-elpi.opam coq-core.8.20.0 + opam install coq-serapi.8.20.0+0.20.0 ./rocq-elpi.opam coq-core.8.20.0 sudo apt-get update sudo apt-get install python3-pip -y pip3 install git+https://github.com/cpitclaudel/alectryon.git@c8ab1ec - name: build doc - run: opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1 + run: | + opam exec -- make dune-files + opam exec -- make doc COQ_ELPI_ALREADY_INSTALLED=1 - name: Save artifact uses: actions/upload-artifact@v4 diff --git a/.github/workflows/nix-action-coq-8.20.yml b/.github/workflows/nix-action-coq-8.20.yml index 30c0c0421..a7dd61e26 100644 --- a/.github/workflows/nix-action-coq-8.20.yml +++ b/.github/workflows/nix-action-coq-8.20.yml @@ -189,7 +189,6 @@ jobs: coq-elpi: needs: - coq - - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -241,10 +240,6 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20" diff --git a/.github/workflows/nix-action-coq-master.yml b/.github/workflows/nix-action-coq-master.yml index 36dd607d1..6fe5ad316 100644 --- a/.github/workflows/nix-action-coq-master.yml +++ b/.github/workflows/nix-action-coq-master.yml @@ -118,7 +118,6 @@ jobs: coq-elpi: needs: - coq - - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -170,72 +169,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" --argstr job "coq-elpi" - coq-elpi-no-stdlib: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepGetDerivation - name: Getting derivation for current job (coq-elpi-no-stdlib) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"coq-master\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err - > out || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master" - --argstr job "coq-elpi-no-stdlib" coq-elpi-tests: needs: - coq diff --git a/.github/workflows/nix-action-rocq-9.0.yml b/.github/workflows/nix-action-rocq-9.0.yml index d3a25c9c8..b097485af 100644 --- a/.github/workflows/nix-action-rocq-9.0.yml +++ b/.github/workflows/nix-action-rocq-9.0.yml @@ -189,7 +189,6 @@ jobs: coq-elpi: needs: - coq - - stdlib runs-on: ubuntu-latest steps: - name: Determine which commit to initially checkout @@ -241,72 +240,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: stdlib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "stdlib" - if: steps.stepCheck.outputs.status == 'built' name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" --argstr job "coq-elpi" - coq-elpi-no-stdlib: - needs: - - coq - runs-on: ubuntu-latest - steps: - - name: Determine which commit to initially checkout - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.target_commit }} - - name: Determine which commit to test - run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{ - github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url - }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git - merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null - 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\ - \ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha - }}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\ - \ fi\nfi\n" - - name: Git checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - ref: ${{ env.tested_commit }} - - name: Cachix install - uses: cachix/install-nix-action@v30 - with: - nix_path: nixpkgs=channel:nixpkgs-unstable - - name: Cachix setup coq-elpi - uses: cachix/cachix-action@v15 - with: - authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} - extraPullNames: coq, coq-community, math-comp - name: coq-elpi - - id: stepGetDerivation - name: Getting derivation for current job (coq-elpi-no-stdlib) - run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle - \"rocq-9.0\" --argstr job \"coq-elpi-no-stdlib\" \\\n --dry-run 2> err > - out || (touch fail; true)\n" - - name: Error reporting - run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n" - - name: Failure check - run: if [ -e fail ]; then exit 1; else exit 0; fi; - - id: stepCheck - name: Checking presence of CI target for current job - run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: Building/fetching current CI target - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0" - --argstr job "coq-elpi-no-stdlib" coq-elpi-tests: needs: - coq diff --git a/.gitignore b/.gitignore index 29784562d..1a1d6e358 100644 --- a/.gitignore +++ b/.gitignore @@ -27,10 +27,10 @@ etc/__pycache__/ /.deps.elpi -src/coq_elpi_config.ml -src/coq_elpi_vernacular_syntax.ml -src/coq_elpi_arg_syntax.ml -src/coq_elpi_builtins_HOAS.ml +src/rocq_elpi_config.ml +src/rocq_elpi_vernacular_syntax.ml +src/rocq_elpi_arg_syntax.ml +src/rocq_elpi_builtins_HOAS.ml doc/ Makefile.coq @@ -45,16 +45,17 @@ META *.cache -apps/coercion/src/coq_elpi_coercion_hook.ml +apps/coercion/src/rocq_elpi_coercion_hook.ml .filestoinstall -apps/tc/src/coq_elpi_tc_hook.ml -apps/cs/src/coq_elpi_cs_hook.ml +apps/tc/src/rocq_elpi_tc_hook.ml +apps/cs/src/rocq_elpi_cs_hook.ml *.timing _build tmp.out -coq-elpi-tests.opam -coq-elpi-tests.install +rocq-elpi-tests.opam +rocq-elpi-tests.install +rocq-elpi.install coq-elpi.install -theories-stdlib/dune \ No newline at end of file +theories-stdlib/dune diff --git a/.nix/config.nix b/.nix/config.nix index a4dbcc43e..616056962 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -14,7 +14,6 @@ let master = [ common-bundles = listToAttrs (forEach master (p: { name = p; value.override.version = "master"; })) // { - coq-elpi-no-stdlib.job = true; coq-elpi-tests.job = true; stdlib.job = true; coq-elpi-tests-stdlib.job = true; @@ -35,7 +34,6 @@ let master = [ "coq-8.20".coqPackages = common-bundles // { coq.override.version = "8.20"; coq-elpi.override.elpi-version = "2.0.7"; - coq-elpi-no-stdlib.job = false; coq-elpi-tests-stdlib.job = false; }; diff --git a/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix b/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix deleted file mode 100644 index 001239b6b..000000000 --- a/.nix/coq-overlays/coq-elpi-no-stdlib/default.nix +++ /dev/null @@ -1,11 +0,0 @@ -{ lib, coq-elpi, coqPackages }: - -coqPackages.lib.overrideCoqDerivation { - - pname = "coq-elpi-no-stdlib"; - opam-name = "coq-elpi"; - - propagatedBuildInputs = - lib.filter (d: d?pname && d.pname != "stdlib") - coq-elpi.propagatedBuildInputs; -} coq-elpi diff --git a/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix b/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix index c23648568..677473a81 100644 --- a/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix +++ b/.nix/coq-overlays/coq-elpi-tests-stdlib/default.nix @@ -4,6 +4,9 @@ coqPackages.lib.overrideCoqDerivation { pname = "coq-elpi-tests-stdlib"; + propagatedBuildInputs = coq-elpi.propagatedBuildInputs + ++ [ coqPackages.stdlib ]; + buildPhase = '' make test-stdlib make examples-stdlib diff --git a/.nix/coq-overlays/coq-elpi-tests/default.nix b/.nix/coq-overlays/coq-elpi-tests/default.nix index b261deb07..68e42c0ab 100644 --- a/.nix/coq-overlays/coq-elpi-tests/default.nix +++ b/.nix/coq-overlays/coq-elpi-tests/default.nix @@ -4,10 +4,6 @@ coqPackages.lib.overrideCoqDerivation { pname = "coq-elpi-tests"; - propagatedBuildInputs = - lib.filter (d: d?pname && d.pname != "stdlib") - coq-elpi.propagatedBuildInputs; - buildPhase = '' make test-core make examples diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix new file mode 100644 index 000000000..85c5e89e8 --- /dev/null +++ b/.nix/coq-overlays/coq-elpi/default.nix @@ -0,0 +1,123 @@ +{ + lib, + mkCoqDerivation, + which, + coq, + version ? null, + elpi-version ? null, +}: + +let +default-elpi-version = if elpi-version != null then elpi-version else ( + lib.switch coq.coq-version [ + { case = "8.11"; out = "1.11.4"; } + { case = "8.12"; out = "1.12.0"; } + { case = "8.13"; out = "1.13.7"; } + { case = "8.14"; out = "1.13.7"; } + { case = "8.15"; out = "1.15.0"; } + { case = "8.16"; out = "1.17.0"; } + { case = "8.17"; out = "1.17.0"; } + { case = "8.18"; out = "1.18.1"; } + { case = "8.19"; out = "1.18.1"; } + { case = "8.20"; out = "1.19.2"; } + { case = "9.0"; out = "2.0.7"; } + ] { } +); +elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; }; +propagatedBuildInputs_wo_elpi = [ + coq.ocamlPackages.findlib +]; +derivation = mkCoqDerivation { + pname = "elpi"; + repo = "coq-elpi"; + owner = "LPCIC"; + opam-name = "rocq-elpi"; + inherit version; + defaultVersion = lib.switch coq.coq-version [ + { case = "9.0"; out = "2.4.0"; } + { case = "8.20"; out = "2.2.0"; } + { case = "8.19"; out = "2.0.1"; } + { case = "8.18"; out = "2.0.0"; } + { case = "8.17"; out = "1.18.0"; } + { case = "8.16"; out = "1.15.6"; } + { case = "8.15"; out = "1.14.0"; } + { case = "8.14"; out = "1.11.2"; } + { case = "8.13"; out = "1.11.1"; } + { case = "8.12"; out = "1.8.3_8.12"; } + { case = "8.11"; out = "1.6.3_8.11"; } + ] null; + release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc="; + release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I="; + release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc="; + release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM="; + release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ="; + release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y="; + release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM="; + release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno="; + release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg="; + release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"; + release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; + release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; + release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; + release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; + release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; + release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; + release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; + release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; + release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; + release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; + release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; + release."1.8.3_8.12".version = "1.8.3"; + release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; + release."1.8.2_8.12".version = "1.8.2"; + release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; + release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; + release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; + release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; + release."1.6.3_8.11".version = "1.6.3"; + release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; + release."1.6.2_8.11".version = "1.6.2"; + release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; + release."1.6.1_8.11".version = "1.6.1"; + release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; + release."1.6.0_8.11".version = "1.6.0"; + release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; + releaseRev = v: "v${v}"; + + buildFlags = [ "OCAMLWARN=" ]; + + mlPlugin = true; + useDuneifVersion = v: lib.versions.isGe "2.2.0" v || v == "dev"; + + propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ]; + + preConfigure = '' + make elpi/dune || true + make dune-files || true + ''; + + meta = { + description = "Coq plugin embedding ELPI"; + maintainers = [ lib.maintainers.cohencyril ]; + license = lib.licenses.lgpl21Plus; + }; +}; +patched-derivation1 = derivation.overrideAttrs + ( + o: + lib.optionalAttrs (o ? elpi-version) + { + propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ + (coq.ocamlPackages.elpi.override { version = o.elpi-version; }) + ]; + } + ); +patched-derivation2 = patched-derivation1.overrideAttrs + ( + o: + lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version)) + { + propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ]; + } + ); +in patched-derivation2 diff --git a/.nix/coq-overlays/hierarchy-builder/default.nix b/.nix/coq-overlays/hierarchy-builder/default.nix new file mode 100644 index 000000000..084cc9f7f --- /dev/null +++ b/.nix/coq-overlays/hierarchy-builder/default.nix @@ -0,0 +1,51 @@ +{ lib, mkCoqDerivation, coq, coq-elpi, stdlib, version ? null }: + +let hb = mkCoqDerivation { + pname = "hierarchy-builder"; + owner = "math-comp"; + inherit version; + defaultVersion = with lib.versions; lib.switch coq.coq-version [ + { case = range "9.0" "9.0"; out = "1.8.1"; } + { case = range "8.19" "8.20"; out = "1.8.0"; } + { case = range "8.18" "8.20"; out = "1.7.1"; } + { case = range "8.16" "8.18"; out = "1.6.0"; } + { case = range "8.15" "8.18"; out = "1.5.0"; } + { case = range "8.15" "8.17"; out = "1.4.0"; } + { case = range "8.13" "8.14"; out = "1.2.0"; } + { case = range "8.12" "8.13"; out = "1.1.0"; } + { case = isEq "8.11"; out = "0.10.0"; } + ] null; + release."1.8.1".sha256 = "sha256-Z0WAHDyycqgL+Le/zNfEAoLWzFb7WIL+3G3vEBExlb4="; + release."1.8.0".sha256 = "sha256-4s/4ZZKj5tiTtSHGIM8Op/Pak4Vp52WVOpd4l9m19fY="; + release."1.7.1".sha256 = "sha256-MCmOzMh/SBTFAoPbbIQ7aqd3hMcSMpAKpiZI7dbRaGs="; + release."1.7.0".sha256 = "sha256-WqSeuJhmqicJgXw/xGjGvbRzfyOK7rmkVRb6tPDTAZg="; + release."1.6.0".sha256 = "sha256-E8s20veOuK96knVQ7rEDSt8VmbtYfPgItD0dTY/mckg="; + release."1.5.0".sha256 = "sha256-Lia3o156Pbe8rDHOA1IniGYsG5/qzZkzDKdHecfmS+c="; + release."1.4.0".sha256 = "sha256-tOed9UU3kMw6KWHJ5LVLUFEmzHx1ImutXQvZ0ldW9rw="; + release."1.3.0".sha256 = "17k7rlxdx43qda6i1yafpgc64na8br285cb0mbxy5wryafcdrkrc"; + release."1.2.1".sha256 = "sha256-pQYZJ34YzvdlRSGLwsrYgPdz3p/l5f+KhJjkYT08Mj0="; + release."1.2.0".sha256 = "0sk01rvvk652d86aibc8rik2m8iz7jn6mw9hh6xkbxlsvh50719d"; + release."1.1.0".sha256 = "sha256-spno5ty4kU4WWiOfzoqbXF8lWlNSlySWcRReR3zE/4Q="; + release."1.0.0".sha256 = "0yykygs0z6fby6vkiaiv3azy1i9yx4rqg8xdlgkwnf2284hffzpp"; + release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h"; + releaseRev = v: "v${v}"; + + propagatedBuildInputs = [ coq-elpi stdlib ]; + + mlPlugin = true; + + meta = with lib; { + description = "High level commands to declare a hierarchy based on packed classes"; + maintainers = with maintainers; [ cohencyril siraben ]; + license = licenses.mit; + }; +}; in +hb.overrideAttrs (o: + lib.optionalAttrs (lib.versions.isGe "1.2.0" o.version || o.version == "dev") + { buildPhase = "make build"; } + // + (if lib.versions.isGe "1.1.0" o.version || o.version == "dev" then + { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; } + else + { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; }) +) diff --git a/.vscode/settings.json b/.vscode/settings.json index 8427b3d80..6c15288e5 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -23,8 +23,8 @@ "**/*.crashcoqide": true, "**/\\#*\\#": true, ".deps.elpi": true, - "src/coq_elpi_config.ml": true, - "src/coq_elpi_vernacular_syntax.ml": true, + "src/rocq_elpi_config.ml": true, + "src/rocq_elpi_vernacular_syntax.ml": true, "**/Makefile.coq": true, "**/Makefile.coq.conf": true, "**/.merlin": true @@ -33,4 +33,4 @@ "ocaml.server.args": [ "--fallback-read-dot-merlin" ], -} \ No newline at end of file +} diff --git a/Makefile b/Makefile index 04ef7c430..5f9a8bdbf 100644 --- a/Makefile +++ b/Makefile @@ -1,48 +1,75 @@ -dune = dune $(1) $(DUNE_$(1)_FLAGS) --stop-on-first-error +dune_wrap = $(shell command -v coqc > /dev/null || echo "etc/with-rocq-wrap.sh") +dune = $(dune_wrap) dune $(1) $(DUNE_$(1)_FLAGS --stop-on-first-error +DUNE_IN_FILES = $(shell find . -name "dune.in" | sed -e 's/.in$$//') -all: theories-stdlib/dune +all: $(DUNE_IN_FILES) $(call dune,build) $(call dune,build) builtin-doc .PHONY: all -build-core: theories-stdlib/dune +# simplify this and get rid of the dune.in files once we require Rocq >= 9.0 +%dune: %dune.in + @rm -f $@ + @echo "; generated by make, do not edit\n" > $@ + @if test -e .coq-dune-files || \ + (command -v coqc > /dev/null && (coqc --version | grep -q '8.19\|8.20')) ; then \ + sed -e 's/@@STDLIB_THEORY@@//' $< | \ + sed -e 's/@@STDLIB@@//' | \ + sed -e 's/@@ROCQ_RUNTIME@@/coq-core/g' >> $@ ; \ + else \ + sed -e 's/@@STDLIB_THEORY@@/(theories Stdlib)/' $< | \ + sed -e 's/@@STDLIB@@/Stdlib/' | \ + sed -e 's/@@ROCQ_RUNTIME@@/rocq-runtime/g' >> $@ ; \ + fi + @chmod a-w $@ + +dune-files: $(DUNE_IN_FILES) +.PHONE: dune-files + +coq-dune-files: + touch .coq-dune-files + $(MAKE) dune-files + $(RM) .coq-dune-files +.PHONE: coq-dune-files + +build-core: $(DUNE_IN_FILES) $(call dune,build) theories $(call dune,build) builtin-doc .PHONY: build-core -build-apps: theories-stdlib/dune +build-apps: $(DUNE_IN_FILES) $(call dune,build) $$(find apps -type d -name theories) .PHONY: build-apps -build: theories-stdlib/dune - $(call dune,build) -p coq-elpi @install +build: $(DUNE_IN_FILES) + $(call dune,build) -p rocq-elpi @install $(call dune,build) builtin-doc .PHONY: build all-tests: test-core test-stdlib test-apps test-apps-stdlib .PHONY: all-tests -test-core: theories-stdlib/dune +test-core: $(DUNE_IN_FILES) $(call dune,runtest) tests $(call dune,build) tests .PHONY: test-core -test-apps: theories-stdlib/dune +test-apps: $(DUNE_IN_FILES) $(call dune,build) $$(find apps -type d -name tests) .PHONY: test-apps -test-apps-stdlib: theories-stdlib/dune +test-apps-stdlib: $(DUNE_IN_FILES) $(call dune,build) $$(find apps -type d -name tests-stdlib) .PHONY: test-apps-stdlib -test-stdlib: theories-stdlib/dune +test-stdlib: $(DUNE_IN_FILES) $(call dune,build) tests-stdlib .PHONY: test-stdlib all-examples: examples examples-stdlib .PHONY: all-examples -examples: theories-stdlib/dune +examples: $(DUNE_IN_FILES) $(call dune,build) examples .PHONY: examples @@ -50,16 +77,6 @@ examples-stdlib: theories-stdlib/dune $(call dune,build) examples-stdlib .PHONY: examples-stdlib -theories-stdlib/dune: theories-stdlib/dune.in - @rm -f $@ - @echo "; generated by make, do not edit" > $@ - @if $$(coqc --version | grep -q "8.19\|8.20") ; then \ - sed -e 's/@@STDLIB@@//' $< >> $@ ; \ - else \ - sed -e 's/@@STDLIB@@/Stdlib/' $< >> $@ ; \ - fi - @chmod a-w $@ - doc: build @echo "########################## generating doc ##########################" @mkdir -p doc @@ -78,8 +95,8 @@ clean: $(call dune,clean) .PHONY: clean -install: - $(call dune,install) coq-elpi +install: $(DUNE_IN_FILES) + $(call dune,install) rocq-elpi .PHONY: install nix: diff --git a/README.md b/README.md index 2f97cd6ca..2eb695277 100644 --- a/README.md +++ b/README.md @@ -39,7 +39,7 @@ inference, and to provide an alternative elaborator for Coq. The simplest way is to use [OPAM](http://opam.ocaml.org/) and type ``` opam repo add coq-released https://coq.inria.fr/opam/released -opam install coq-elpi +opam install rocq-elpi ``` ### Editor Setup @@ -72,10 +72,10 @@ highlighting and handles quotations. To install the development version one can type ``` -opam pin add coq-elpi https://github.com/LPCIC/coq-elpi.git +opam pin add rocq-elpi https://github.com/LPCIC/coq-elpi.git ``` One can also clone this repository and type `make`, but check you have -all the dependencies installed first (see [coq-elpi.opam](coq-elpi.opam)). +all the dependencies installed first (see [rocq-elpi.opam](rocq-elpi.opam)). We recommend to look at the [CI setup](.github/workflows) for ocaml versions being tested. Also, we recommend to install `dot-merlin-reader` diff --git a/apps/NES/elpi/dune b/apps/NES/elpi/dune index d5b54bc98..096a65a85 100644 --- a/apps/NES/elpi/dune +++ b/apps/NES/elpi/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.NES.elpi) - (package coq-elpi) + (package rocq-elpi) (theories elpi)) (rule @@ -10,10 +10,10 @@ (action (with-stdout-to %{target} (progn - (run coq_elpi_shafile %{deps}))))) + (run rocq_elpi_shafile %{deps}))))) (install (files (glob_files (*.elpi with_prefix coq/user-contrib/elpi/apps/NES/elpi/))) (section lib_root) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/apps/NES/tests/dune b/apps/NES/tests/dune index 80a1d465d..d2ab3b5bd 100644 --- a/apps/NES/tests/dune +++ b/apps/NES/tests/dune @@ -1,6 +1,7 @@ (coq.theory (name elpi.apps.NES.tests) - (package coq-elpi-tests) + (package rocq-elpi-tests) (theories elpi elpi.apps.NES)) (include_subdirs qualified) + diff --git a/apps/NES/theories/dune b/apps/NES/theories/dune index 87e94c86a..33950b493 100644 --- a/apps/NES/theories/dune +++ b/apps/NES/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.NES) - (package coq-elpi) + (package rocq-elpi) (theories elpi elpi.apps.NES.elpi)) (include_subdirs qualified) diff --git a/apps/coercion/src/META.coq-elpi-coercion b/apps/coercion/src/META.coq-elpi-coercion deleted file mode 100644 index 507e9af0e..000000000 --- a/apps/coercion/src/META.coq-elpi-coercion +++ /dev/null @@ -1,10 +0,0 @@ - -package "plugin" ( - directory = "." - requires = "coq-core.plugins.ltac coq-elpi.elpi" - archive(byte) = "elpi_coercion_plugin.cma" - archive(native) = "elpi_coercion_plugin.cmxa" - plugin(byte) = "elpi_coercion_plugin.cma" - plugin(native) = "elpi_coercion_plugin.cmxs" -) -directory = "." diff --git a/apps/coercion/src/dune b/apps/coercion/src/dune.in similarity index 56% rename from apps/coercion/src/dune rename to apps/coercion/src/dune.in index 72926590a..0a13ebfb3 100644 --- a/apps/coercion/src/dune +++ b/apps/coercion/src/dune.in @@ -1,9 +1,9 @@ (library (name elpi_coercion_plugin) - (public_name coq-elpi.coercion) + (public_name rocq-elpi.coercion) (flags :standard -w -27) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) - (libraries coq-core.plugins.ltac coq-core.vernac coq-elpi.elpi)) + (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi)) (coq.pp - (modules coq_elpi_coercion_hook)) + (modules rocq_elpi_coercion_hook)) diff --git a/apps/coercion/src/elpi_coercion_plugin.mlpack b/apps/coercion/src/elpi_coercion_plugin.mlpack index 0e41afce5..613d239cb 100644 --- a/apps/coercion/src/elpi_coercion_plugin.mlpack +++ b/apps/coercion/src/elpi_coercion_plugin.mlpack @@ -1 +1 @@ -Coq_elpi_coercion_hook \ No newline at end of file +Rocq_elpi_coercion_hook diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/rocq_elpi_coercion_hook.mlg similarity index 82% rename from apps/coercion/src/coq_elpi_coercion_hook.mlg rename to apps/coercion/src/rocq_elpi_coercion_hook.mlg index ec3440bac..4fa00bf39 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/rocq_elpi_coercion_hook.mlg @@ -1,11 +1,11 @@ -DECLARE PLUGIN "coq-elpi.coercion" +DECLARE PLUGIN "rocq-elpi.coercion" { open Elpi open Elpi_plugin -open Coq_elpi_arg_syntax -open Coq_elpi_vernacular +open Rocq_elpi_arg_syntax +open Rocq_elpi_vernacular let relevant = EConstr.ERelevance.relevant let anonR = Context.make_annot Names.Name.Anonymous EConstr.ERelevance.irrelevant @@ -29,13 +29,13 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = let sigma, goal = Evarutil.new_evar env sigma expected in let goal_evar, _ = EConstr.destEvar sigma goal in let query state = - let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in + let loc = Elpi.API.State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let depth = 0 in let state, q, gls = - Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[v; inferred] - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth ~base:() state in + Rocq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[v; inferred] + ~in_elpi_tac_arg:Rocq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth ~base:() state in let state, qatts = atts2impl loc Summary.Stage.Interp ~depth state atts q in - let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + let state = API.State.set Rocq_elpi_builtins.tactic_mode state true in state, qatts, gls in let loc = Loc.initial Loc.ToplevelInput in @@ -45,7 +45,7 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = match Interp.run ~loc cprogram (Fun (query)) with | API.Execute.Success solution -> let gls = Evar.Set.singleton goal_evar in - let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in + let sigma, _, _ = Rocq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in if Evd.is_defined sigma goal_evar then let t = if retype then Retyping.get_type_of env sigma goal else expected in return sigma goal t @@ -53,7 +53,7 @@ let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = None | API.Execute.NoMoreSteps | API.Execute.Failure -> None - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> None + | exception (Rocq_elpi_utils.LtacFail (level, msg)) -> None let add_coercion_hook = let coercion_hook_program = Summary.ref ~name:"elpi-coercion" None in diff --git a/apps/coercion/tests/dune b/apps/coercion/tests/dune index 5d0075e46..5d9965570 100644 --- a/apps/coercion/tests/dune +++ b/apps/coercion/tests/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.coercion.tests) - (package coq-elpi-tests) + (package rocq-elpi-tests) (theories elpi elpi.apps.coercion)) (include_subdirs qualified) diff --git a/apps/coercion/theories/coercion.v b/apps/coercion/theories/coercion.v index e51706f03..26a964cd8 100644 --- a/apps/coercion/theories/coercion.v +++ b/apps/coercion/theories/coercion.v @@ -1,4 +1,4 @@ -Declare ML Module "coq-elpi.coercion". +Declare ML Module "rocq-elpi.coercion". From elpi Require Import elpi. Elpi Db coercion.db lp:{{ diff --git a/apps/coercion/theories/dune b/apps/coercion/theories/dune index 90f81f0f0..a4cb29733 100644 --- a/apps/coercion/theories/dune +++ b/apps/coercion/theories/dune @@ -1,7 +1,7 @@ (coq.theory (name elpi.apps.coercion) - (package coq-elpi) + (package rocq-elpi) (theories elpi) - (plugins coq-elpi.coercion)) + (plugins rocq-elpi.coercion)) (include_subdirs qualified) diff --git a/apps/cs/src/META.coq-elpi-cs b/apps/cs/src/META.coq-elpi-cs deleted file mode 100644 index e3937f070..000000000 --- a/apps/cs/src/META.coq-elpi-cs +++ /dev/null @@ -1,10 +0,0 @@ - -package "plugin" ( - directory = "." - requires = "coq-core.plugins.ltac coq-elpi.elpi" - archive(byte) = "elpi_cs_plugin.cma" - archive(native) = "elpi_cs_plugin.cmxa" - plugin(byte) = "elpi_cs_plugin.cma" - plugin(native) = "elpi_cs_plugin.cmxs" -) -directory = "." diff --git a/apps/cs/src/dune b/apps/cs/src/dune.in similarity index 57% rename from apps/cs/src/dune rename to apps/cs/src/dune.in index 03ce1c4a6..9ed675452 100644 --- a/apps/cs/src/dune +++ b/apps/cs/src/dune.in @@ -1,9 +1,9 @@ (library (name elpi_cs_plugin) - (public_name coq-elpi.cs) + (public_name rocq-elpi.cs) (flags :standard -w -27) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) - (libraries coq-core.plugins.ltac coq-core.vernac coq-elpi.elpi)) + (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi)) (coq.pp - (modules coq_elpi_cs_hook)) + (modules rocq_elpi_cs_hook)) diff --git a/apps/cs/src/elpi_cs_plugin.mlpack b/apps/cs/src/elpi_cs_plugin.mlpack index a159a0f41..4e61310d5 100644 --- a/apps/cs/src/elpi_cs_plugin.mlpack +++ b/apps/cs/src/elpi_cs_plugin.mlpack @@ -1 +1 @@ -Coq_elpi_cs_hook +Rocq_elpi_cs_hook diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/rocq_elpi_cs_hook.mlg similarity index 85% rename from apps/cs/src/coq_elpi_cs_hook.mlg rename to apps/cs/src/rocq_elpi_cs_hook.mlg index 88700c914..8149683d8 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/rocq_elpi_cs_hook.mlg @@ -1,11 +1,11 @@ -DECLARE PLUGIN "coq-elpi.cs" +DECLARE PLUGIN "rocq-elpi.cs" { open Elpi open Elpi_plugin -open Coq_elpi_arg_syntax -open Coq_elpi_vernacular +open Rocq_elpi_arg_syntax +open Rocq_elpi_vernacular let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) = let atts = [] in @@ -15,15 +15,15 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) = let goal_evar, _ = EConstr.destEvar sigma goal in let nparams = Structures.Structure.projection_nparams proji in let query state = - let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in + let loc = Elpi.API.State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let state, q, gls = let lhs = match params1 with | Some params1 -> EConstr.mkApp (EConstr.mkConstU (proji, u), Array.of_list params1) | None -> EConstr.mkConstU (proji, u) in - Coq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[lhs; rhs] - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth:0 ~base:() state in + Rocq_elpi_HOAS.solvegoals2query sigma [goal_evar] loc ~main:[lhs; rhs] + ~in_elpi_tac_arg:Rocq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth:0 ~base:() state in let state, qatts = atts2impl loc Summary.Stage.Interp ~depth:0 state atts q in - let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + let state = API.State.set Rocq_elpi_builtins.tactic_mode state true in state, qatts, gls in let loc = Loc.initial Loc.ToplevelInput in @@ -33,7 +33,7 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) = begin match Interp.run ~loc cprogram (Fun query) with | API.Execute.Success solution -> let gls = Evar.Set.singleton goal_evar in - let sigma, _, _ = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in + let sigma, _, _ = Rocq_elpi_HOAS.solution2evd ~eta_contract_solution:false sigma solution gls in if Evd.is_defined sigma goal_evar then let constant = EConstr.to_constr sigma goal in let args_goal, t = Reduction.whd_decompose_lambda env constant in diff --git a/apps/cs/tests/dune b/apps/cs/tests/dune index c49811c04..511463202 100644 --- a/apps/cs/tests/dune +++ b/apps/cs/tests/dune @@ -3,5 +3,5 @@ (deps %{bin:coqc} %{bin:coqdep} - (package coq-elpi) + (package rocq-elpi) setup-project.sh)) diff --git a/apps/cs/theories/cs.v b/apps/cs/theories/cs.v index e16a6196b..28814c08b 100644 --- a/apps/cs/theories/cs.v +++ b/apps/cs/theories/cs.v @@ -1,4 +1,4 @@ -Declare ML Module "coq-elpi.cs". +Declare ML Module "rocq-elpi.cs". From elpi Require Import elpi. Elpi Db cs.db lp:{{ diff --git a/apps/cs/theories/dune b/apps/cs/theories/dune index ebc2a3419..608660970 100644 --- a/apps/cs/theories/dune +++ b/apps/cs/theories/dune @@ -1,7 +1,7 @@ (coq.theory (name elpi.apps.cs) - (package coq-elpi) + (package rocq-elpi) (theories elpi) - (plugins coq-elpi.cs)) + (plugins rocq-elpi.cs)) (include_subdirs qualified) diff --git a/apps/derive/elpi/dune b/apps/derive/elpi/dune index 02f0525dd..6db189007 100644 --- a/apps/derive/elpi/dune +++ b/apps/derive/elpi/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.derive.elpi) - (package coq-elpi) + (package rocq-elpi) (theories elpi)) (rule @@ -10,10 +10,10 @@ (action (with-stdout-to %{target} (progn - (run coq_elpi_shafile %{deps}))))) + (run rocq_elpi_shafile %{deps}))))) (install (files (glob_files (*.elpi with_prefix coq/user-contrib/elpi/apps/derive/elpi/))) (section lib_root) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/apps/derive/elpi/paramX_lib.elpi b/apps/derive/elpi/paramX_lib.elpi index ac1e74428..343e88a5b 100644 --- a/apps/derive/elpi/paramX_lib.elpi +++ b/apps/derive/elpi/paramX_lib.elpi @@ -1,4 +1,4 @@ -/* coq-elpi: Coq terms as the object language of elpi */ +/* rocq-elpi: Coq terms as the object language of elpi */ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ diff --git a/apps/derive/tests-stdlib/dune b/apps/derive/tests-stdlib/dune index 2411d4773..d11bed5d1 100644 --- a/apps/derive/tests-stdlib/dune +++ b/apps/derive/tests-stdlib/dune @@ -1,5 +1,5 @@ (coq.theory - (package coq-elpi-tests-stdlib) + (package rocq-elpi-tests-stdlib) (name elpi_apps_derive_tests_stdlib) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive elpi.apps.derive.tests elpi_stdlib)) diff --git a/apps/derive/tests/dune b/apps/derive/tests/dune index a5ff4e02d..a06ce33d5 100644 --- a/apps/derive/tests/dune +++ b/apps/derive/tests/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.derive.tests) - (package coq-elpi-tests) + (package rocq-elpi-tests) (flags :standard -w -default-output-directory) (theories elpi elpi.apps.derive)) diff --git a/apps/derive/theories/dune b/apps/derive/theories/dune index 2f66ea4ab..eb7cd2d6b 100644 --- a/apps/derive/theories/dune +++ b/apps/derive/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.derive) - (package coq-elpi) + (package rocq-elpi) (theories elpi elpi.apps.derive.elpi)) (include_subdirs qualified) diff --git a/apps/eltac/tests-stdlib/dune b/apps/eltac/tests-stdlib/dune index 8c31d8a88..da48ee9b9 100644 --- a/apps/eltac/tests-stdlib/dune +++ b/apps/eltac/tests-stdlib/dune @@ -1,5 +1,5 @@ (coq.theory - (package coq-elpi-tests-stdlib) + (package rocq-elpi-tests-stdlib) (name elpi_apps_eltac_tests_stdlib) (theories elpi elpi.apps.eltac elpi_stdlib)) diff --git a/apps/eltac/tests/dune b/apps/eltac/tests/dune index 273e01345..dde8292cc 100644 --- a/apps/eltac/tests/dune +++ b/apps/eltac/tests/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.eltac.tests) - (package coq-elpi-tests) + (package rocq-elpi-tests) (theories elpi elpi.apps.eltac)) (include_subdirs qualified) diff --git a/apps/eltac/theories/dune b/apps/eltac/theories/dune index 11d5b4899..0a91ec7b6 100644 --- a/apps/eltac/theories/dune +++ b/apps/eltac/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.eltac) - (package coq-elpi) + (package rocq-elpi) (theories elpi elpi.apps.derive)) (include_subdirs qualified) diff --git a/apps/locker/elpi/dune b/apps/locker/elpi/dune index 989469a31..000dc366f 100644 --- a/apps/locker/elpi/dune +++ b/apps/locker/elpi/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.locker.elpi) - (package coq-elpi) + (package rocq-elpi) (theories elpi)) (rule @@ -10,10 +10,10 @@ (action (with-stdout-to %{target} (progn - (run coq_elpi_shafile %{deps}))))) + (run rocq_elpi_shafile %{deps}))))) (install (files (glob_files (*.elpi with_prefix coq/user-contrib/elpi/apps/locker/elpi/))) (section lib_root) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/apps/locker/tests/dune b/apps/locker/tests/dune index 6b5b68868..cadbe6376 100644 --- a/apps/locker/tests/dune +++ b/apps/locker/tests/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.locker.tests) - (package coq-elpi-tests) + (package rocq-elpi-tests) (theories elpi elpi.apps.locker)) (include_subdirs qualified) diff --git a/apps/locker/theories/dune b/apps/locker/theories/dune index 71c54f4e0..35024b5a8 100644 --- a/apps/locker/theories/dune +++ b/apps/locker/theories/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.locker) - (package coq-elpi) + (package rocq-elpi) (theories elpi elpi.apps.locker.elpi)) (include_subdirs qualified) diff --git a/apps/tc/README.md b/apps/tc/README.md index 571aa29d5..ef1c26d2e 100644 --- a/apps/tc/README.md +++ b/apps/tc/README.md @@ -377,12 +377,12 @@ which allows to set a solver to be called on type class goals. We have taken the file [`classes.ml`] from [here](https://github.com/coq/coq/blob/f022d5d194cb42c2321ea91cecbcce703a9bcad3/vernac/classes.ml#L1) and slightly modified the function -[`resolve_all_evars`](https://github.com/FissoreD/coq-elpi/blob/17d1f20d3d4f37abfeee7edcf31f3757fd515ff3/apps/tc/src/coq_elpi_class_tactics_hacked.ml#L1165). +[`resolve_all_evars`](https://github.com/FissoreD/coq-elpi/blob/17d1f20d3d4f37abfeee7edcf31f3757fd515ff3/apps/tc/src/rocq_elpi_class_tactics_hacked.ml#L1165). Now that function, before solving a goal verifies if the current goal contains only type classes overriden by the user and if so, it uses the elpi solver for its resolution, otherwise, it calls the default coq solver. Note that the choice of using elpi or coq solver is done -[here](src/coq_elpi_class_tactics_takeover.ml). Moreover, we provide different +[here](src/rocq_elpi_class_tactics_takeover.ml). Moreover, we provide different commands to 1. Override all type class goals and solve them by the solver of elpi, that diff --git a/apps/tc/elpi/dune b/apps/tc/elpi/dune index b975a85b4..834876548 100644 --- a/apps/tc/elpi/dune +++ b/apps/tc/elpi/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.apps.tc.elpi) - (package coq-elpi) + (package rocq-elpi) (theories elpi)) (rule @@ -10,10 +10,10 @@ (action (with-stdout-to %{target} (progn - (run coq_elpi_shafile %{deps}))))) + (run rocq_elpi_shafile %{deps}))))) (install (files (glob_files (*.elpi with_prefix coq/user-contrib/elpi/apps/tc/elpi/))) (section lib_root) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/apps/tc/src/META.coq-elpi-tc b/apps/tc/src/META.coq-elpi-tc deleted file mode 100644 index 5c3045ab8..000000000 --- a/apps/tc/src/META.coq-elpi-tc +++ /dev/null @@ -1,10 +0,0 @@ - -package "plugin" ( - directory = "." - requires = "coq-core.plugins.ltac coq-elpi.elpi" - archive(byte) = "elpi_tc_plugin.cma" - archive(native) = "elpi_tc_plugin.cmxa" - plugin(byte) = "elpi_tc_plugin.cma" - plugin(native) = "elpi_tc_plugin.cmxs" -) -directory = "." diff --git a/apps/tc/src/dune b/apps/tc/src/dune.in similarity index 57% rename from apps/tc/src/dune rename to apps/tc/src/dune.in index 701249a11..c8a0e13c6 100644 --- a/apps/tc/src/dune +++ b/apps/tc/src/dune.in @@ -1,9 +1,9 @@ (library (name elpi_tc_plugin) - (public_name coq-elpi.tc) + (public_name rocq-elpi.tc) (flags :standard -w -27) (preprocess (pps ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) - (libraries coq-core.plugins.ltac coq-core.vernac coq-elpi.elpi)) + (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac rocq-elpi.elpi)) (coq.pp - (modules coq_elpi_tc_hook)) + (modules rocq_elpi_tc_hook)) diff --git a/apps/tc/src/elpi_tc_plugin.mlpack b/apps/tc/src/elpi_tc_plugin.mlpack index dd84965e0..14f5384e9 100644 --- a/apps/tc/src/elpi_tc_plugin.mlpack +++ b/apps/tc/src/elpi_tc_plugin.mlpack @@ -1,4 +1,4 @@ -Coq_elpi_tc_time -Coq_elpi_tc_register -Coq_elpi_class_tactics_takeover -Coq_elpi_tc_hook \ No newline at end of file +Rocq_elpi_tc_time +Rocq_elpi_tc_register +Rocq_elpi_class_tactics_takeover +Rocq_elpi_tc_hook diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml similarity index 79% rename from apps/tc/src/coq_elpi_class_tactics_takeover.ml rename to apps/tc/src/rocq_elpi_class_tactics_takeover.ml index 9d1d31299..e611531e0 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.ml @@ -1,11 +1,11 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) type aaction = ARm | AAdd | ASet | ANone | AAll -module Coq_elpi_lib_obj = struct +module Rocq_elpi_lib_obj = struct let add_obj_no_discharge name cache = Libobject.(declare_object (global_object_nodischarge name ~cache ~subst:None)) @@ -19,13 +19,13 @@ open Util open Typeclasses open Elpi open Elpi_plugin -open Coq_elpi_utils +open Rocq_elpi_utils module GRSet = Names.GlobRef.Set module CSMap = CString.Map let qname2str observer = String.concat "." observer -let str2gr = Coq_elpi_utils.locate_simple_qualid +let str2gr = Rocq_elpi_utils.locate_simple_qualid let elpi_fails program_name = let open Pp in @@ -63,7 +63,7 @@ module OSet : M = struct let gr2elt (x: Names.GlobRef.t) : elt = x let of_qualid_list (x: Libnames.qualid list) : t = - let add s x = add (Coq_elpi_utils.locate_simple_qualid x) s in + let add s x = add (Rocq_elpi_utils.locate_simple_qualid x) s in List.fold_left add empty x end @@ -98,7 +98,7 @@ module Modes = struct in omodes := CSMap.set name new_mode !omodes - let cache_solver_mode = Coq_elpi_lib_obj.add_superobj_no_discharge "TC_Solver_omode" takeover + let cache_solver_mode = Rocq_elpi_lib_obj.add_superobj_no_discharge "TC_Solver_omode" takeover end module Solver = struct @@ -106,27 +106,27 @@ module Solver = struct let atts = [] in let gls = goals in let query ~base state = - let loc = Elpi.API.State.get Coq_elpi_builtins_synterp.invocation_site_loc state in + let loc = Elpi.API.State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let depth = 0 in let state, q, gls = - Coq_elpi_HOAS.solvegoals2query sigma gls loc ~main:[] - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.(in_elpi_tac ~loc:(to_coq_loc loc)) ~depth ~base state in - let state, qatts = Coq_elpi_vernacular.atts2impl loc Summary.Stage.Interp ~depth state atts q in - let state = API.State.set Coq_elpi_builtins.tactic_mode state true in + Rocq_elpi_HOAS.solvegoals2query sigma gls loc ~main:[] + ~in_elpi_tac_arg:Rocq_elpi_arg_HOAS.(in_elpi_tac ~loc:(to_coq_loc loc)) ~depth ~base state in + let state, qatts = Rocq_elpi_vernacular.atts2impl loc Summary.Stage.Interp ~depth state atts q in + let state = API.State.set Rocq_elpi_builtins.tactic_mode state true in state, qatts, gls in let loc = Loc.initial Loc.ToplevelInput in - match Coq_elpi_vernacular.Interp.get_and_compile ~loc program with + match Rocq_elpi_vernacular.Interp.get_and_compile ~loc program with | None -> assert false | Some (base,_) -> - match Coq_elpi_vernacular.Interp.run ~loc base (Fun (query ~base)) with + match Rocq_elpi_vernacular.Interp.run ~loc base (Fun (query ~base)) with | API.Execute.Success solution -> - let sigma, sub_goals, to_shelve = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:true sigma solution (Evar.Set.of_list goals) in + let sigma, sub_goals, to_shelve = Rocq_elpi_HOAS.solution2evd ~eta_contract_solution:true sigma solution (Evar.Set.of_list goals) in let sigma = Evd.shelve sigma sub_goals in sub_goals = [], sigma | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> elpi_fails program - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> raise Not_found + | exception (Rocq_elpi_utils.LtacFail (level, msg)) -> raise Not_found } type action = @@ -156,7 +156,7 @@ module Solver = struct | Activate -> Class_tactics.activate_solver ~name | Deactivate -> Class_tactics.deactivate_solver ~name - let cache_solver = Coq_elpi_lib_obj.add_superobj_no_discharge "TC_Solver" action_manager + let cache_solver = Rocq_elpi_lib_obj.add_superobj_no_discharge "TC_Solver" action_manager end diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.mli b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli similarity index 51% rename from apps/tc/src/coq_elpi_class_tactics_takeover.mli rename to apps/tc/src/rocq_elpi_class_tactics_takeover.mli index 245cc6c71..49ecce52c 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.mli +++ b/apps/tc/src/rocq_elpi_class_tactics_takeover.mli @@ -1,10 +1,10 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) type aaction = ARm | AAdd | ASet | ANone | AAll val set_solver_mode : aaction -> string list -> Libnames.qualid list -> unit -val solver_register : Elpi_plugin.Coq_elpi_utils.qualified_name -> unit -val solver_activate : Elpi_plugin.Coq_elpi_utils.qualified_name -> unit -val solver_deactivate : Elpi_plugin.Coq_elpi_utils.qualified_name -> unit +val solver_register : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit +val solver_activate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit +val solver_deactivate : Elpi_plugin.Rocq_elpi_utils.qualified_name -> unit diff --git a/apps/tc/src/coq_elpi_tc_hook.mlg b/apps/tc/src/rocq_elpi_tc_hook.mlg similarity index 94% rename from apps/tc/src/coq_elpi_tc_hook.mlg rename to apps/tc/src/rocq_elpi_tc_hook.mlg index 0ee471768..8c84d8855 100644 --- a/apps/tc/src/coq_elpi_tc_hook.mlg +++ b/apps/tc/src/rocq_elpi_tc_hook.mlg @@ -1,14 +1,14 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -DECLARE PLUGIN "coq-elpi.tc" +DECLARE PLUGIN "rocq-elpi.tc" { open Stdarg open Elpi_plugin -open Coq_elpi_arg_syntax -open Coq_elpi_tc_register -open Coq_elpi_class_tactics_takeover +open Rocq_elpi_arg_syntax +open Rocq_elpi_tc_register +open Rocq_elpi_class_tactics_takeover } VERNAC COMMAND EXTEND ElpiTypeclasses CLASSIFIED AS SIDEFF diff --git a/apps/tc/src/coq_elpi_tc_register.ml b/apps/tc/src/rocq_elpi_tc_register.ml similarity index 88% rename from apps/tc/src/coq_elpi_tc_register.ml rename to apps/tc/src/rocq_elpi_tc_register.ml index 6fc4a2e24..a952b9416 100644 --- a/apps/tc/src/coq_elpi_tc_register.ml +++ b/apps/tc/src/rocq_elpi_tc_register.ml @@ -3,10 +3,10 @@ open Elpi_plugin open Classes -open Coq_elpi_arg_HOAS +open Rocq_elpi_arg_HOAS open Names -type qualified_name = Coq_elpi_utils.qualified_name +type qualified_name = Rocq_elpi_utils.qualified_name type loc_name_atts = (Loc.t * qualified_name * Attributes.vernac_flags) @@ -20,13 +20,13 @@ let gref2elpi_term (gref: GlobRef.t) : Cmd.raw = Libnames.qualid_of_string @@ gref_2_string gref,None)) *) (* Returns the elpi term representing the type class received in argument *) -let observer_class (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = +let observer_class (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = [Cmd.String "new_class"; gref2elpi_term x.cl_impl] -let observer_default_instance (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = +let observer_default_instance (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = [Cmd.String "default_instance";gref2elpi_term x.cl_impl] -let observer_coercion add (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.raw list = +let observer_coercion add (x : Typeclasses.typeclass) : Rocq_elpi_arg_HOAS.Cmd.raw list = let name2str x = Cmd.String (Names.Name.print x |> Pp.string_of_ppcmds) in let proj = x.cl_projs |> List.map (fun (x: Typeclasses.class_method) -> x.meth_name) in let mode = if add then "add_coercions" else "remove_coercions" in @@ -42,7 +42,7 @@ let observer_coercion add (x : Typeclasses.typeclass) : Coq_elpi_arg_HOAS.Cmd.ra | -1 if the instance has no user-defined priority | N if the instance has the user-defined priority N *) -let observer_instance ({locality; instance; info; class_name} : instance) : Coq_elpi_arg_HOAS.Cmd.raw list = +let observer_instance ({locality; instance; info; class_name} : instance) : Rocq_elpi_arg_HOAS.Cmd.raw list = let locality2elpi_string loc = let hint2string = function | Hints.Local -> "Local" @@ -80,7 +80,7 @@ let inObservation1 = ~discharge:(fun (_,inst as x) -> if inst.locality = Local then None else Some x) let observer_evt ((loc, name, atts) : loc_name_atts) (x : Event.t) = - let open Coq_elpi_vernacular in + let open Rocq_elpi_vernacular in let run_program e = Interp.run_program ~loc name ~syndata:None ~atts e in match x with | Event.NewClass cl -> Lib.add_leaf (inObservation (run_program,cl)) @@ -113,7 +113,7 @@ let action_manager x = Feedback.msg_warning Pp.(str (Printf.sprintf "%s already registered" name)) end; let t2 = Sys.time () in - if Coq_elpi_tc_time.get_time_tc_bench () then Feedback.msg_debug Pp.(str @@ Printf.sprintf "[TC] register.ml time is %.5f" (t1 -. t2)) + if Rocq_elpi_tc_time.get_time_tc_bench () then Feedback.msg_debug Pp.(str @@ Printf.sprintf "[TC] register.ml time is %.5f" (t1 -. t2)) | Activate observer -> Classes.activate_observer (StringMap.find (build_observer_name observer) !observers) | Deactivate observer -> @@ -135,4 +135,4 @@ let activate_observer (observer : qualified_name) = Lib.add_leaf (inTakeover (Activate observer)) let deactivate_observer (observer : qualified_name) = - Lib.add_leaf (inTakeover (Deactivate observer)) \ No newline at end of file + Lib.add_leaf (inTakeover (Deactivate observer)) diff --git a/apps/tc/src/coq_elpi_tc_time.ml b/apps/tc/src/rocq_elpi_tc_time.ml similarity index 83% rename from apps/tc/src/coq_elpi_tc_time.ml rename to apps/tc/src/rocq_elpi_tc_time.ml index a30632d0e..a20f059ea 100644 --- a/apps/tc/src/coq_elpi_tc_time.ml +++ b/apps/tc/src/rocq_elpi_tc_time.ml @@ -12,5 +12,5 @@ let () = Goptions.declare_bool_option { optstage = Summary.Stage.Interp; optwrite = set_time_tc_bench; } let time_all b = - CDebug.set_flag Coq_elpi_utils.elpitime_flag b; - set_time_tc_bench b \ No newline at end of file + CDebug.set_flag Rocq_elpi_utils.elpitime_flag b; + set_time_tc_bench b diff --git a/apps/tc/tests-stdlib/dune b/apps/tc/tests-stdlib/dune index 91824cb3d..8bae8722d 100644 --- a/apps/tc/tests-stdlib/dune +++ b/apps/tc/tests-stdlib/dune @@ -1,5 +1,5 @@ (coq.theory - (package coq-elpi-tests-stdlib) + (package rocq-elpi-tests-stdlib) (name elpi_apps_tc_tests_stdlib) (flags :standard -async-proofs-cache force) (theories elpi elpi.apps.tc elpi.apps.tc.tests elpi_stdlib)) diff --git a/apps/tc/tests/dune b/apps/tc/tests/dune index 98696f732..aa17dd497 100644 --- a/apps/tc/tests/dune +++ b/apps/tc/tests/dune @@ -1,7 +1,7 @@ (coq.theory (name elpi.apps.tc.tests) (flags :standard -async-proofs-cache force) - (package coq-elpi-tests) + (package rocq-elpi-tests) (theories elpi elpi.apps.tc)) (include_subdirs qualified) diff --git a/apps/tc/tests/test_backtrack_several_goals.v b/apps/tc/tests/test_backtrack_several_goals.v index 953ee89cc..06e5280f9 100644 --- a/apps/tc/tests/test_backtrack_several_goals.v +++ b/apps/tc/tests/test_backtrack_several_goals.v @@ -44,7 +44,7 @@ Module M1. Qed. End M1. -(* Here similar problems using the coq-elpi solver *) +(* Here similar problems using the rocq-elpi solver *) From elpi Require Import elpi tc. Module ElpiBt. @@ -93,4 +93,4 @@ Module M_in_elpi. eexists. apply m. Qed. -End M_in_elpi. \ No newline at end of file +End M_in_elpi. diff --git a/apps/tc/theories/dune b/apps/tc/theories/dune index 1561dd7b9..6e7a83821 100644 --- a/apps/tc/theories/dune +++ b/apps/tc/theories/dune @@ -1,8 +1,8 @@ (coq.theory (name elpi.apps.tc) - (package coq-elpi) + (package rocq-elpi) (theories elpi elpi.apps.tc.elpi) (flags -w -all -w -elpi) - (plugins coq-elpi.tc)) + (plugins rocq-elpi.tc)) (include_subdirs qualified) diff --git a/apps/tc/theories/tc.v b/apps/tc/theories/tc.v index 9882939f7..a9cd831b8 100644 --- a/apps/tc/theories/tc.v +++ b/apps/tc/theories/tc.v @@ -1,7 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -Declare ML Module "coq-elpi.tc". +Declare ML Module "rocq-elpi.tc". From elpi.apps.tc.elpi Extra Dependency "tc_aux.elpi" as tc_aux. (* From elpi.apps.tc.elpi Extra Dependency "compiler.elpi" as compiler. *) @@ -199,4 +199,4 @@ Elpi Export TC.Unfold. Set Warnings "elpi". Elpi TC.AddAllClasses. -Elpi TC.AddAllInstances. \ No newline at end of file +Elpi TC.AddAllInstances. diff --git a/apps/tc/theories/wip.v b/apps/tc/theories/wip.v index cfcac589a..d7060d727 100644 --- a/apps/tc/theories/wip.v +++ b/apps/tc/theories/wip.v @@ -1,7 +1,7 @@ (* license: GNU Lesser General Public License Version 2.1 or later *) (* --------------------------------------------------------------------------*) -Declare ML Module "coq-elpi.tc". +Declare ML Module "rocq-elpi.tc". From elpi Require Import elpi. From elpi.apps.tc.elpi Extra Dependency "modes.elpi" as modes. @@ -54,4 +54,4 @@ Elpi Accumulate lp:{{ main [trm New, trm Old] :- add-tc-db _ _ (alias New Old). }}. - *) \ No newline at end of file + *) diff --git a/builtin-doc/coq-builtin-synterp.elpi b/builtin-doc/coq-builtin-synterp.elpi index 8fb8a19e6..5714c4942 100644 --- a/builtin-doc/coq-builtin-synterp.elpi +++ b/builtin-doc/coq-builtin-synterp.elpi @@ -162,7 +162,7 @@ type end-record record-decl. % % Note: when and inductive type declaration is passed as an argument to an % Elpi command non uniform parameters must be separated from the uniform ones -% with a | (a syntax introduced in Coq 8.12 and accepted by coq-elpi since +% with a | (a syntax introduced in Coq 8.12 and accepted by rocq-elpi since % version 1.4, in Coq this separator is optional, but not in Elpi). % Context declaration (used as an argument to Elpi commands) diff --git a/builtin-doc/coq-builtin.elpi b/builtin-doc/coq-builtin.elpi index 4d62b1f8b..7f1af9eb9 100644 --- a/builtin-doc/coq-builtin.elpi +++ b/builtin-doc/coq-builtin.elpi @@ -6,7 +6,7 @@ % This file is automatically generated from % - coq-HOAS.elpi -% - coq_elpi_builtin.ml +% - rocq_elpi_builtin.ml % and contains the description of the data type of Coq terms and the % API to access Coq. @@ -135,7 +135,7 @@ type end-record record-decl. % % Note: when and inductive type declaration is passed as an argument to an % Elpi command non uniform parameters must be separated from the uniform ones -% with a | (a syntax introduced in Coq 8.12 and accepted by coq-elpi since +% with a | (a syntax introduced in Coq 8.12 and accepted by rocq-elpi since % version 1.4, in Coq this separator is optional, but not in Elpi). % Context declaration (used as an argument to Elpi commands) @@ -963,7 +963,7 @@ external pred coq.env.primitive-projection? i:projection, o:constant. % which is able to craft a universe variable which is roughly % equivalent to an algebraic universe, e.g. k such that j+1 = k. % -% Coq-Elpi systematically purges algebraic universes from terms (and +% Rocq-Elpi systematically purges algebraic universes from terms (and % types and sorts) when one reads them from the environment. This % makes the embedding of terms less precise than what it could be. % The different data types stay, since Coq will eventually become diff --git a/builtin-doc/dune b/builtin-doc/dune index 15e577fa9..601934208 100644 --- a/builtin-doc/dune +++ b/builtin-doc/dune @@ -17,4 +17,4 @@ coq-builtin-synterp.elpi elpi-builtin.elpi) (section doc) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/builtin-doc/gen_doc.ml b/builtin-doc/gen_doc.ml index cf77d30f5..82b252182 100644 --- a/builtin-doc/gen_doc.ml +++ b/builtin-doc/gen_doc.ml @@ -1,2 +1,2 @@ let _ = - Elpi_plugin.Coq_elpi_programs.document_builtins () + Elpi_plugin.Rocq_elpi_programs.document_builtins () diff --git a/coq-elpi-tests.opam b/coq-elpi-tests.opam deleted file mode 100644 index 95260bf1c..000000000 --- a/coq-elpi-tests.opam +++ /dev/null @@ -1,29 +0,0 @@ -# This file is generated by dune, edit dune-project instead -opam-version: "2.0" -synopsis: "Technical package to run tests" -description: "Do not install" -maintainer: ["Enrico Tassi "] -authors: ["Enrico Tassi "] -license: "LGPL-2.1-or-later" -homepage: "https://github.com/LPCIC/coq-elpi" -bug-reports: "https://github.com/LPCIC/coq-elpi/issues" -depends: [ - "dune" {>= "3.13"} - "coq-elpi" - "odoc" {with-doc} -] -build: [ - ["dune" "subst"] {dev} - [ - "dune" - "build" - "-p" - name - "-j" - jobs - "@install" - "@runtest" {with-test} - "@doc" {with-doc} - ] -] -dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" diff --git a/coq-elpi.opam b/coq-elpi.opam index 1fa94daa1..c80409da4 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -1,8 +1,6 @@ # This file is generated by dune, edit dune-project instead opam-version: "2.0" -synopsis: "Elpi extension language for Coq" -description: - "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics." +synopsis: "Compatibility metapackage for Elpi extension language after the Rocq renaming" maintainer: ["Enrico Tassi "] authors: ["Enrico Tassi "] license: "LGPL-2.1-or-later" @@ -15,28 +13,7 @@ tags: [ homepage: "https://github.com/LPCIC/coq-elpi" bug-reports: "https://github.com/LPCIC/coq-elpi/issues" depends: [ - "dune" {>= "3.13"} - "ocaml" {>= "4.10.0"} - "elpi" {>= "2.0.7" & < "2.1.0~"} - ("coq-core" {>= "8.20+rc1" & < "8.21~" } & "coq-stdlib" - | "rocq-core" {>= "9.0+rc1" & < "9.1~" | = "dev" } & "coq-core") - "ppx_optcomp" - "ocaml-lsp-server" {with-dev-setup} - "odoc" {with-doc} - "coq-stdlib" {with-doc} -] -build: [ - ["dune" "subst"] {dev} - [ - "dune" - "build" - "-p" - name - "-j" - jobs - "@install" - "@runtest" {with-test} - "@doc" {with-doc} - ] + "coq-core" + "rocq-elpi" {= version} ] dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" diff --git a/dune-project b/dune-project index f615477be..bdecff756 100644 --- a/dune-project +++ b/dune-project @@ -1,6 +1,6 @@ (lang dune 3.13) (using coq 0.8) -(name coq-elpi) +(name rocq-elpi) ;(generate_opam_files) (source (github LPCIC/coq-elpi)) @@ -9,7 +9,7 @@ (maintainers "Enrico Tassi ") (package - (name coq-elpi) + (name rocq-elpi) (synopsis "Elpi extension language for Coq") (description "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides \ @@ -36,13 +36,21 @@ (ocaml-lsp-server :with-dev-setup))) (package - (name coq-elpi-tests) + (name rocq-elpi-tests) (synopsis "Technical package to run tests") (description "Do not install") - (depends coq-elpi)) + (depends rocq-elpi)) (package - (name coq-elpi-tests-stdlib) + (name rocq-elpi-tests-stdlib) (synopsis "Technical package to run tests depending on Stdlib") (description "Do not install") - (depends coq-elpi coq-stdlib)) + (depends rocq-elpi rocq-stdlib)) + +(package + (name coq-elpi) + (allow_empty) + (depends + coq-core + (rocq-elpi (= :version))) + (synopsis "Compatibility metapackage for Elpi extension language after the Rocq renaming")) diff --git a/elpi/coq-arg-HOAS.elpi b/elpi/coq-arg-HOAS.elpi index a07977a6e..517337f08 100644 --- a/elpi/coq-arg-HOAS.elpi +++ b/elpi/coq-arg-HOAS.elpi @@ -120,7 +120,7 @@ type end-record record-decl. % % Note: when and inductive type declaration is passed as an argument to an % Elpi command non uniform parameters must be separated from the uniform ones -% with a | (a syntax introduced in Coq 8.12 and accepted by coq-elpi since +% with a | (a syntax introduced in Coq 8.12 and accepted by rocq-elpi since % version 1.4, in Coq this separator is optional, but not in Elpi). % Context declaration (used as an argument to Elpi commands) diff --git a/elpi/coq-elpi-checker.elpi b/elpi/coq-elpi-checker.elpi index fa10533fe..26d5fc6cd 100644 --- a/elpi/coq-elpi-checker.elpi +++ b/elpi/coq-elpi-checker.elpi @@ -1,4 +1,4 @@ -/* coq-elpi: Coq terms as the object language of elpi */ +/* rocq-elpi: Coq terms as the object language of elpi */ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ diff --git a/elpi/coq-lib-common.elpi b/elpi/coq-lib-common.elpi index 6042339d7..7ce15e1e9 100644 --- a/elpi/coq-lib-common.elpi +++ b/elpi/coq-lib-common.elpi @@ -1,4 +1,4 @@ -/* coq-elpi: Helpers common to synterp and interp */ +/* rocq-elpi: Helpers common to synterp and interp */ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ diff --git a/elpi/coq-lib.elpi b/elpi/coq-lib.elpi index abe409132..fb834b161 100644 --- a/elpi/coq-lib.elpi +++ b/elpi/coq-lib.elpi @@ -1,4 +1,4 @@ -/* coq-elpi: Coq terms as the object language of elpi */ +/* rocq-elpi: Coq terms as the object language of elpi */ /* license: GNU Lesser General Public License Version 2.1 or later */ /* ------------------------------------------------------------------------- */ diff --git a/elpi/dune b/elpi/dune index fb14a6ddd..cf2ad65a6 100644 --- a/elpi/dune +++ b/elpi/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi_elpi) ; FIXME - (package coq-elpi)) + (package rocq-elpi)) (rule (target dummy.v) @@ -9,10 +9,10 @@ (action (with-stdout-to %{target} (progn - (run coq_elpi_shafile %{deps}))))) + (run rocq_elpi_shafile %{deps}))))) (install (files (glob_files (*.elpi with_prefix coq/user-contrib/elpi_elpi/))) (section lib_root) - (package coq-elpi)) + (package rocq-elpi)) diff --git a/etc/dune b/etc/dune index 1630cb67b..da77b295a 100644 --- a/etc/dune +++ b/etc/dune @@ -1,19 +1,19 @@ (executable (name shafile) - (public_name coq_elpi_shafile) + (public_name rocq_elpi_shafile) (modules shafile) - (package coq-elpi)) + (package rocq-elpi)) (executable (name optcomp) - (public_name coq_elpi_optcomp) + (public_name rocq_elpi_optcomp) (modules optcomp) (libraries str) - (package coq-elpi)) + (package rocq-elpi)) (executable (name version_parser) - (public_name coq_elpi_version_parser) + (public_name rocq_elpi_version_parser) (modules version_parser) (libraries str elpi) - (package coq-elpi)) \ No newline at end of file + (package rocq-elpi)) diff --git a/etc/tools/dune b/etc/tools/dune new file mode 100644 index 000000000..0ee2e772b --- /dev/null +++ b/etc/tools/dune @@ -0,0 +1,2 @@ +(executable + (name hash)) diff --git a/etc/tools/hash.ml b/etc/tools/hash.ml new file mode 100644 index 000000000..f2d9348db --- /dev/null +++ b/etc/tools/hash.ml @@ -0,0 +1,2 @@ +let () = + Printf.printf "%s\n%!" Digest.(to_hex (input stdin)) diff --git a/etc/tools/hash.mli b/etc/tools/hash.mli new file mode 100644 index 000000000..e69de29bb diff --git a/etc/with-rocq-wrap.sh b/etc/with-rocq-wrap.sh new file mode 100755 index 000000000..0dd7db9da --- /dev/null +++ b/etc/with-rocq-wrap.sh @@ -0,0 +1,59 @@ +#!/usr/bin/env bash + +set -ex + +rocq=$(command -v rocq) +# NB on cygwin "$rocq" is a cygwin path (/foo/bar) +# but reading files from hash.exe needs windows paths (C:/cygwin/foo/bar) +# we avoid the problem by going through stdin +rocqhash=$(dune exec --root "$(dirname "$0")"/.. -- etc/tools/hash.exe < "$rocq") + +rm -rf .wrappers +mkdir .wrappers + +cat > .wrappers/coqc < .wrappers/coqdep < .wrappers/coqdoc < .wrappers/coqpp < .wrappers/META.coq-core < X1*} +.. mquote:: .s(Elpi).msg{Rocq-Elpi mapping:*[?]X11 <-> X1*} :language: text Note that Coq's evar identifiers are of the form `?X`, while the Elpi ones @@ -631,7 +631,7 @@ conclusion (the suspended goal). The mapping between Coq and Elpi is: -.. mquote:: .s(Elpi).msg{Coq-Elpi mapping:*[?]X13 <-> X1*} +.. mquote:: .s(Elpi).msg{Rocq-Elpi mapping:*[?]X13 <-> X1*} :language: text where `?X13` can be found in Coq's sigma: diff --git a/examples/tutorial_coq_elpi_tactic.v b/examples/tutorial_coq_elpi_tactic.v index a070cd55e..269135ff4 100644 --- a/examples/tutorial_coq_elpi_tactic.v +++ b/examples/tutorial_coq_elpi_tactic.v @@ -689,7 +689,7 @@ represent the proof state in Coq. It is printed just afterwards: .. mquote:: .s(elpi show_more).msg{EVARS:*[?]X57*x + 1 = 0*} :language: text -.. mquote:: .s(elpi show_more).msg{Coq-Elpi mapping:*RAW:*[?]X57 <-> *X1*ELAB:*[?]X57 <-> *X0*} +.. mquote:: .s(elpi show_more).msg{Rocq-Elpi mapping:*RAW:*[?]X57 <-> *X1*ELAB:*[?]X57 <-> *X0*} :language: text Here `?X57` is a Coq evar linked with Elpi's :e:`X0` and :e:`X1`. diff --git a/rocq-elpi.opam b/rocq-elpi.opam new file mode 100644 index 000000000..53c7bd8b5 --- /dev/null +++ b/rocq-elpi.opam @@ -0,0 +1,44 @@ +# This file is generated by dune, edit dune-project instead +opam-version: "2.0" +synopsis: "Elpi extension language for Coq" +description: + "Coq-elpi provides a Coq plugin that embeds ELPI. It also provides a way to embed Coq's terms into λProlog using the Higher-Order Abstract Syntax approach and a way to read terms back. In addition to that it exports to ELPI a set of Coq's primitives, e.g. printing a message, accessing the environment of theorems and data types, defining a new constant and so on. For convenience it also provides a quotation and anti-quotation for Coq's syntax in λProlog. E.g., `{{nat}}` is expanded to the type name of natural numbers, or `{{A -> B}}` to the representation of a product by unfolding the `->` notation. Finally it provides a way to define new vernacular commands and new tactics." +maintainer: ["Enrico Tassi "] +authors: ["Enrico Tassi "] +license: "LGPL-2.1-or-later" +tags: [ + "category:Miscellaneous/Coq Extensions" + "keyword:λProlog" + "keyword:higher order abstract syntax" + "logpath:elpi" +] +homepage: "https://github.com/LPCIC/coq-elpi" +bug-reports: "https://github.com/LPCIC/coq-elpi/issues" +depends: [ + "dune" {>= "3.13"} + "ocaml" {>= "4.10.0"} + "elpi" {>= "2.0.7" & < "2.1.0~"} + ("coq" {>= "8.20+rc1" & < "8.21~"} + | "rocq-core" {>= "9.0+rc1" & < "9.1~"}) + "ppx_optcomp" + "ocaml-lsp-server" {with-dev-setup} + "odoc" {with-doc} + "rocq-stdlib" {with-doc} +] +build: [ + ["dune" "subst"] {dev} + [make "dune-files"] + [ + "etc/with-rocq-wrap.sh" {!coq-core:installed} + "dune" + "build" + "-p" + name + "-j" + jobs + "@install" + "@runtest" {with-test} + "@doc" {with-doc} + ] +] +dev-repo: "git+https://github.com/LPCIC/coq-elpi.git" diff --git a/src/META.coq-elpi b/src/META.coq-elpi deleted file mode 100644 index b1aa861ed..000000000 --- a/src/META.coq-elpi +++ /dev/null @@ -1,10 +0,0 @@ -package "elpi" ( - directory = "." - description = "Coq Elpi" - requires = "coq-core.plugins.ltac stdlib-shims elpi" - archive(byte) = "elpi_plugin.cma" - archive(native) = "elpi_plugin.cmxa" - plugin(byte) = "elpi_plugin.cma" - plugin(native) = "elpi_plugin.cmxs" -) -directory = "." diff --git a/src/README.md b/src/README.md index d47388ec0..9b1da9cbc 100644 --- a/src/README.md +++ b/src/README.md @@ -2,8 +2,8 @@ This directory contains the OCaml code bridging Elpi and Coq. -The most interesting file is [coq_elpi_HOAS.ml](coq_elpi_HOAS.ml) where +The most interesting file is [rocq_elpi_HOAS.ml](rocq_elpi_HOAS.ml) where conversions for term, context and evar_map are provided. -The exposed Coq API is in [coq_elpi_builtins.ml](coq_elpi_builtins.ml). +The exposed Coq API is in [rocq_elpi_builtins.ml](rocq_elpi_builtins.ml). diff --git a/src/dune b/src/dune.in similarity index 69% rename from src/dune rename to src/dune.in index 180a03a1b..5333dfa3a 100644 --- a/src/dune +++ b/src/dune.in @@ -1,15 +1,15 @@ (library (name elpi_plugin) - (public_name coq-elpi.elpi) + (public_name rocq-elpi.elpi) (synopsis "Elpi") (flags :standard -w -27) - (preprocessor_deps coq_elpi_config.mlh) + (preprocessor_deps rocq_elpi_config.mlh) (preprocess (pps ppx_deriving.std ppx_optcomp -- -cookie "ppx_optcomp.env=env ~coq:(Defined \"%{coq:version.major}.%{coq:version.minor}\")")) - (libraries coq-core.plugins.ltac coq-core.vernac elpi)) + (libraries @@ROCQ_RUNTIME@@.plugins.ltac @@ROCQ_RUNTIME@@.vernac elpi)) (rule - (target coq_elpi_builtins_arg_HOAS.ml) + (target rocq_elpi_builtins_arg_HOAS.ml) (deps ../elpi/coq-arg-HOAS.elpi (package elpi)) (action (with-stdout-to %{target} (progn @@ -19,7 +19,7 @@ (echo "|}\n"))))) (rule - (target coq_elpi_builtins_HOAS.ml) + (target rocq_elpi_builtins_HOAS.ml) (deps ../elpi/coq-HOAS.elpi) (action (with-stdout-to %{target} (progn @@ -29,22 +29,22 @@ (echo "|}\n"))))) (rule - (target coq_elpi_config.ml) + (target rocq_elpi_config.ml) (action (with-stdout-to %{target} (progn (echo "(* Automatically generated, don't edit *)\n") - (echo "[%%import \"coq_elpi_config.mlh\"]\n") + (echo "[%%import \"rocq_elpi_config.mlh\"]\n") (echo "let elpi_version = \"%{version:elpi}\"\n"))))) (rule - (target coq_elpi_config.mlh) + (target rocq_elpi_config.mlh) (action (with-stdout-to %{target} (progn (echo "(* Automatically generated, don't edit *)\n") (echo "[%%define elpi ") - (run coq_elpi_version_parser %{version:elpi}) + (run rocq_elpi_version_parser %{version:elpi}) (echo "]\n"))))) (coq.pp - (modules coq_elpi_vernacular_syntax coq_elpi_arg_syntax)) + (modules rocq_elpi_vernacular_syntax rocq_elpi_arg_syntax)) diff --git a/src/elpi_plugin.mlpack b/src/elpi_plugin.mlpack index 6c47f092c..42af1885a 100644 --- a/src/elpi_plugin.mlpack +++ b/src/elpi_plugin.mlpack @@ -1,15 +1,15 @@ -Coq_elpi_config -Coq_elpi_utils -Coq_elpi_graph -Coq_elpi_HOAS -Coq_elpi_glob_quotation -Coq_elpi_name_quotation -Coq_elpi_arg_HOAS -Coq_elpi_arg_syntax -Coq_elpi_builtins_arg_HOAS -Coq_elpi_builtins_HOAS -Coq_elpi_builtins_synterp -Coq_elpi_builtins -Coq_elpi_programs -Coq_elpi_vernacular -Coq_elpi_vernacular_syntax +Rocq_elpi_config +Rocq_elpi_utils +Rocq_elpi_graph +Rocq_elpi_HOAS +Rocq_elpi_glob_quotation +Rocq_elpi_name_quotation +Rocq_elpi_arg_HOAS +Rocq_elpi_arg_syntax +Rocq_elpi_builtins_arg_HOAS +Rocq_elpi_builtins_HOAS +Rocq_elpi_builtins_synterp +Rocq_elpi_builtins +Rocq_elpi_programs +Rocq_elpi_vernacular +Rocq_elpi_vernacular_syntax diff --git a/src/coq_elpi_HOAS.ml b/src/rocq_elpi_HOAS.ml similarity index 99% rename from src/coq_elpi_HOAS.ml rename to src/rocq_elpi_HOAS.ml index a6cf116b7..d0109479f 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/rocq_elpi_HOAS.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -15,7 +15,7 @@ module C = Constr module EC = EConstr open Names module G = GlobRef -open Coq_elpi_utils +open Rocq_elpi_utils (* ************************************************************************ *) (* ****************** HOAS of Coq terms and goals ************************* *) @@ -96,7 +96,7 @@ module UM = F.Map(struct let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (Univ.Universe.pr UnivNames.pr_level_with_global_universes x) end) -let um = S.declare_component ~name:"coq-elpi:evar-univ-map" ~descriptor:interp_state +let um = S.declare_component ~name:"rocq-elpi:evar-univ-map" ~descriptor:interp_state ~pp:UM.pp ~init:(fun () -> UM.empty) ~start:(fun x -> x) () @@ -827,7 +827,7 @@ let projectionina ~loc p = let pstringina ~loc x = A.mkAppGlobal ~loc primitivec (A.mkAppGlobal ~loc pstrc (A.mkOpaque ~loc (pstringc.cino x)) []) [] let primitive_value : primitive_value API.Conversion.t = - let module B = Coq_elpi_utils in + let module B = Rocq_elpi_utils in let open API.AlgebraicData in declare { ty = API.Conversion.TyName "primitive-value"; doc = "Primitive values"; @@ -925,7 +925,7 @@ let from_env_keep_univ_of_sigma ~uctx ~env0 ~env sigma0 = from_env (Global.env ()) let engine : coq_engine S.component = - S.declare_component ~name:"coq-elpi:evmap-constraint-type" ~descriptor:interp_state + S.declare_component ~name:"rocq-elpi:evmap-constraint-type" ~descriptor:interp_state ~pp:pp_coq_engine ~init ~start:(fun _ -> init()) () end @@ -1826,7 +1826,7 @@ module UIM = F.Map(struct let pp fmt x = Format.fprintf fmt "%a" Pp.pp_with (UVars.Instance.pr Sorts.QVar.raw_pr UnivNames.pr_level_with_global_universes x) end) -let uim = S.declare_component ~name:"coq-elpi:evar-univ-instance-map" ~descriptor:interp_state +let uim = S.declare_component ~name:"rocq-elpi:evar-univ-instance-map" ~descriptor:interp_state ~pp:UIM.pp ~init:(fun () -> UIM.empty) ~start:(fun x -> x) () let in_coq_poly_gref ~depth ~origin ~failsafe s t i = @@ -2424,7 +2424,7 @@ let eat_n_lambdas ~depth t upto state = | UnifVar(r,a) -> aux (n+1) (mkUnifVar r ~args:(a@[mkConst n]) state) | Const c -> aux (n+1) (mkApp c (mkConst n) []) | App (c, x, xs) -> aux (n+1) (mkApp c x (xs@[mkConst n])) - | _ -> CErrors.anomaly Pp.(str "Coq-elpi eat_n_lambdas : " ++ + | _ -> CErrors.anomaly Pp.(str "rocq-elpi eat_n_lambdas : " ++ str(pp2string (P.term depth) t)) in @@ -2474,7 +2474,7 @@ let show_coq_engine ?with_univs state = show_coq_engine ?with_univs (S.get engine state) let show_coq_elpi_engine_mapping state = - "Coq-Elpi mapping:\n" ^ UVMap.show state + "Rocq-Elpi mapping:\n" ^ UVMap.show state let show_all_engine state = show_coq_engine ~with_univs:true state ^ "\n" ^ show_coq_elpi_engine_mapping state @@ -2905,7 +2905,7 @@ let readback_arity ~depth coq_ctx constraints state t = let inference_nonuniform_params_off = CWarnings.create ~name:"elpi.unsupported-nonuniform-parameters-inference" - ~category:Coq_elpi_utils.elpi_cat Pp.(fun () -> + ~category:Rocq_elpi_utils.elpi_cat Pp.(fun () -> strbrk"Inference of non-uniform parameters is not available in Elpi, please use the explicit | mark in the inductive declaration or Set Uniform Inductive Parameters") let restricted_sigma_of s state = @@ -3742,7 +3742,7 @@ let lp2skeleton ~depth coq_ctx constraints state t = let coq_ctx = { coq_ctx with options = { coq_ctx.options with hoas_holes = Some Implicit }} in let state, t, gls = lp2constr coq_ctx constraints ~depth state t in let sigma = get_sigma state in - let gt = Coq_elpi_utils.detype ?keepunivs:coq_ctx.options.keepunivs coq_ctx.env sigma t in + let gt = Rocq_elpi_utils.detype ?keepunivs:coq_ctx.options.keepunivs coq_ctx.env sigma t in let gt = let is_GRef_hole x = match DAst.get x with diff --git a/src/coq_elpi_HOAS.mli b/src/rocq_elpi_HOAS.mli similarity index 99% rename from src/coq_elpi_HOAS.mli rename to src/rocq_elpi_HOAS.mli index 6bae0d63d..70f2d7e7b 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/rocq_elpi_HOAS.mli @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) diff --git a/src/coq_elpi_arg_HOAS.ml b/src/rocq_elpi_arg_HOAS.ml similarity index 92% rename from src/coq_elpi_arg_HOAS.ml rename to src/rocq_elpi_arg_HOAS.ml index 3974bfb3d..daf1d0dcf 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/rocq_elpi_arg_HOAS.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -6,8 +6,8 @@ module API = Elpi.API module E = API.RawData module CD = API.RawOpaqueData -open Coq_elpi_utils -open Coq_elpi_HOAS +open Rocq_elpi_utils +open Rocq_elpi_HOAS open Names type phase = Interp | Synterp | Both @@ -26,7 +26,7 @@ let push_glob_ctx glob_ctx x = let push_inductive_in_intern_env intern_env name params arity user_impls = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, ty = Pretyping.understand_tcc env sigma ~expected_type:Pretyping.IsType (Coq_elpi_utils.mk_gforall arity params) in + let sigma, ty = Pretyping.understand_tcc env sigma ~expected_type:Pretyping.IsType (Rocq_elpi_utils.mk_gforall arity params) in ty, Constrintern.compute_internalization_env env sigma ~impls:intern_env Constrintern.Inductive [name] [ty] [user_impls] @@ -86,7 +86,7 @@ type glob_record_decl_elpi = { constructorname : Names.Id.t option; params : Glob_term.glob_decl list; arity : Glob_term.glob_constr; - fields : (Glob_term.glob_constr * Coq_elpi_HOAS.record_field_spec) list; + fields : (Glob_term.glob_constr * Rocq_elpi_HOAS.record_field_spec) list; univpoly : univpoly; } @@ -325,16 +325,16 @@ let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fiel let fields = List.fold_left (fun acc -> function | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,bl,x), { Vernacexpr.rf_coercion = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } -> - if nots <> [] then Coq_elpi_utils.nYI "notation in record fields"; - if pr <> None then Coq_elpi_utils.nYI "priority in record fields"; - let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = if inst = Vernacexpr.AddCoercion then Reversible else Off; name } in + if nots <> [] then Rocq_elpi_utils.nYI "notation in record fields"; + if pr <> None then Rocq_elpi_utils.nYI "priority in record fields"; + let atts = { Rocq_elpi_HOAS.is_canonical = canon; is_coercion = if inst = Vernacexpr.AddCoercion then Reversible else Off; name } in let x = if bl = [] then x else Constrexpr_ops.mkCProdN bl x in let entry = intern_global_context_synterp [mkCLocalAssum [fn] (Constrexpr.Default Glob_term.Explicit) x] in let x = match entry with | [x] -> dest_entry x | _ -> assert false in (x, atts) :: acc - | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr") + | Vernacexpr.DefExpr _, _ -> Rocq_elpi_utils.nYI "DefExpr") [] fields in { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly } @@ -352,9 +352,9 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi let _, _, fields = List.fold_left (fun (gs,intern_env,acc) -> function | Vernacexpr.AssumExpr ({ CAst.v = name } as fn,bl,x), { Vernacexpr.rf_coercion = inst; rf_priority = pr; rf_notation = nots; rf_canonical = canon } -> - if nots <> [] then Coq_elpi_utils.nYI "notation in record fields"; - if pr <> None then Coq_elpi_utils.nYI "priority in record fields"; - let atts = { Coq_elpi_HOAS.is_canonical = canon; is_coercion = if inst = Vernacexpr.AddCoercion then Reversible else Off; name } in + if nots <> [] then Rocq_elpi_utils.nYI "notation in record fields"; + if pr <> None then Rocq_elpi_utils.nYI "priority in record fields"; + let atts = { Rocq_elpi_HOAS.is_canonical = canon; is_coercion = if inst = Vernacexpr.AddCoercion then Reversible else Off; name } in let x = if bl = [] then x else Constrexpr_ops.mkCProdN bl x in let intern_env, entry = intern_global_context ~intern_env gs [mkCLocalAssum [fn] (Constrexpr.Default Glob_term.Explicit) x] in let x = match entry with @@ -362,7 +362,7 @@ let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fi | _ -> assert false in let gs = push_glob_ctx entry gs in gs, intern_env, (x, atts) :: acc - | Vernacexpr.DefExpr _, _ -> Coq_elpi_utils.nYI "DefExpr") + | Vernacexpr.DefExpr _, _ -> Rocq_elpi_utils.nYI "DefExpr") (glob_sign_params,intern_env,[]) fields in { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly } @@ -397,8 +397,8 @@ let raw_indt_decl_to_glob glob_sign ({ finiteness; name; parameters; non_uniform let nuparams = List.rev nuparams in let allparams = params @ nuparams in let user_impls : Impargs.manual_implicits = - if nuparams_given then List.map Coq_elpi_utils.manual_implicit_of_gdecl nuparams - else List.map Coq_elpi_utils.manual_implicit_of_gdecl allparams in + if nuparams_given then List.map Rocq_elpi_utils.manual_implicit_of_gdecl nuparams + else List.map Rocq_elpi_utils.manual_implicit_of_gdecl allparams in let glob_sign_params = push_glob_ctx allparams glob_sign in let arity = intern_global_constr_ty ~intern_env glob_sign_params indexes in let glob_sign_params_self = push_name glob_sign_params (Names.Name name) in @@ -439,7 +439,7 @@ let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); bod | Some udecl, true -> let open UState in let sigma, { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} = - Constrintern.interp_univ_decl_opt (Coq_elpi_HOAS.get_global_env state) (Some udecl) in + Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in let ustate = Evd.evar_universe_context sigma in let state = merge_universe_context state ustate in state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in @@ -495,7 +495,7 @@ let raw_constant_decl_to_glob glob_sign ({ name; atts; udecl; typ = (params,typ) | Some udecl, true -> let open UState in let sigma, { univdecl_extensible_instance; univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} = - Constrintern.interp_univ_decl_opt (Coq_elpi_HOAS.get_global_env state) (Some udecl) in + Constrintern.interp_univ_decl_opt (Rocq_elpi_HOAS.get_global_env state) (Some udecl) in let ustate = Evd.evar_universe_context sigma in let state = merge_universe_context state ustate in state, NonCumulative ((univdecl_instance,univdecl_extensible_instance),(univdecl_constraints,univdecl_extensible_constraints)) in @@ -665,7 +665,7 @@ let rec gparams2lp_synterp ~depth params k state = match params with | [] -> k state | (name,imp,ob,src) :: params -> - if ob <> None then Coq_elpi_utils.nYI "defined parameters in a record/inductive declaration"; + if ob <> None then Rocq_elpi_utils.nYI "defined parameters in a record/inductive declaration"; let src = E.mkDiscard in let state, tgt = gparams2lp_synterp ~depth params k state in let state, imp = in_elpi_imp ~depth state imp in @@ -696,19 +696,19 @@ let grecord2lp_synterp ~depth state { Cmd.name; arity; params; constructorname; mk_indt_decl state univpoly r let grecord2lp ~loc ~base ~depth state { Cmd.name; arity; params; constructorname; fields; univpoly } = - let open Coq_elpi_glob_quotation in + let open Rocq_elpi_glob_quotation in let state, r = gparams2lp ~loc ~base params ~k:(grecord2lp ~loc ~base ~name ~constructorname arity fields) ~depth state in mk_indt_decl state univpoly r let contract_params env sigma name params nuparams_given t = if nuparams_given then t else let open Glob_term in - let loc = Option.map Coq_elpi_utils.of_coq_loc t.CAst.loc in + let loc = Option.map Rocq_elpi_utils.of_coq_loc t.CAst.loc in let rec contract params args = match params, args with | [], rest -> rest | _ :: _, [] -> - Coq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++ + Rocq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++ str" is not applied to enough parameters. Missing: " ++ prlist_with_sep spc Names.Name.print (List.map (fun (x,_,_,_) -> x) params)) | (Name.Anonymous,_,_,_) :: ps , _ :: rest -> contract ps rest @@ -716,7 +716,7 @@ let contract_params env sigma name params nuparams_given t = begin match DAst.get arg with | GVar v when Names.Id.equal pname v -> contract ps rest | GHole _ -> contract ps rest - | _ -> Coq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++ + | _ -> Rocq_elpi_utils.err ?loc Pp.(str "Inductive type "++ Names.Id.print name ++ str" is not applied to parameter " ++ Names.Id.print pname ++ str" but rather " ++ Printer.pr_glob_constr_env env sigma arg) end @@ -751,14 +751,14 @@ let ginductive2lp_synterp ~depth state { Cmd.finiteness; name; arity; params; nu let do_inductive_synterp ~depth state = let qindt_name = Id.of_string_soft @@ String.concat "." (space @ [Id.to_string indt_name]) in let state, arity = gparams2lp_synterp nuparams (fun state -> state, in_elpi_arity E.mkDiscard) ~depth state in - let state, constructors = Coq_elpi_utils.list_map_acc (do_constructor ~depth ) state constructors in + let state, constructors = Rocq_elpi_utils.list_map_acc (do_constructor ~depth ) state constructors in state, in_elpi_indtdecl_inductive state finiteness (Name.Name qindt_name) arity constructors in let state, r = gparams2lp_synterp params (do_inductive_synterp ~depth) ~depth state in mk_indt_decl state univpoly r let ginductive2lp ~loc ~depth ~base state { Cmd.finiteness; name; arity; params; nuparams; nuparams_given; constructors; univpoly } = - let open Coq_elpi_glob_quotation in + let open Rocq_elpi_glob_quotation in let space, indt_name = name in let contract state x = let params = List.map drop_relevance params in @@ -770,10 +770,10 @@ let ginductive2lp ~loc ~depth ~base state { Cmd.finiteness; name; arity; params; let do_inductive ~depth state = let short_name = Name.Name indt_name in let qindt_name = Id.of_string_soft @@ String.concat "." (space @ [Id.to_string indt_name]) in - let state, term_arity = gterm2lp ~loc ~depth ~base (Coq_elpi_utils.mk_gforall arity nuparams) state in + let state, term_arity = gterm2lp ~loc ~depth ~base (Rocq_elpi_utils.mk_gforall arity nuparams) state in let state, arity = gparams2lp ~loc ~base nuparams ~k:(garity2lp ~loc ~base arity) ~depth state in under_ctx short_name term_arity None ~k:(fun ~depth state -> - let state, constructors = Coq_elpi_utils.list_map_acc (do_constructor ~depth ) state constructors in + let state, constructors = Rocq_elpi_utils.list_map_acc (do_constructor ~depth ) state constructors in state, in_elpi_indtdecl_inductive state finiteness (Name.Name qindt_name) arity constructors, ()) ~depth state in @@ -805,9 +805,9 @@ let gdecl2lp_synterp ~depth state { Cmd.name; params; typ : _; body; udecl } = state, E.mkApp ucdeclc name [body;typ;ud], gls @ gls1 let cdecl2lp ~loc ~depth ~base state { Cmd.name; params; typ; body; udecl } = - let open Coq_elpi_glob_quotation in + let open Rocq_elpi_glob_quotation in let state, typ = gparams2lp ~loc ~base params ~k:(garity2lp ~loc ~base typ) ~depth state in - let state, body = option_map_acc (fun state bo -> gterm2lp ~loc ~depth ~base (Coq_elpi_utils.mk_gfun bo params) state) state body in + let state, body = option_map_acc (fun state bo -> gterm2lp ~loc ~depth ~base (Rocq_elpi_utils.mk_gfun bo params) state) state body in let name = decl_name2lp name in let state, body, gls = in_option ~depth state body in match udecl with @@ -835,10 +835,10 @@ let rec do_context_glob ~loc fields ~depth ~base state = match fields with | [] -> state, E.mkGlobal ctxendc | (name,_,bk,bo,ty) :: fields -> - let open Coq_elpi_glob_quotation in + let open Rocq_elpi_glob_quotation in let state, ty = gterm2lp ~loc ~depth ~base ty state in let state, bo = option_map_acc (fun state bo -> gterm2lp ~loc ~depth ~base bo state) state bo in - let state, fields, () = Coq_elpi_glob_quotation.under_ctx name ty bo ~k:(nogls (do_context_glob ~loc ~base fields)) ~depth state in + let state, fields, () = Rocq_elpi_glob_quotation.under_ctx name ty bo ~k:(nogls (do_context_glob ~loc ~base fields)) ~depth state in let state, bo, _ = in_option ~depth state bo in let state, imp = in_elpi_imp ~depth state bk in state, E.mkApp ctxitemc (in_elpi_id name) [imp;ty;bo;E.mkLam fields] @@ -853,7 +853,7 @@ let rec do_context_constr coq_ctx csts fields ~depth state = | None -> state, None, [] | Some bo -> let state, bo, gl = map state bo in state, Some bo, gl in (* TODO GLS *) - let state, fields, gl2 = Coq_elpi_glob_quotation.under_ctx name ty bo ~k:(do_context_constr coq_ctx csts fields) ~depth state in + let state, fields, gl2 = Rocq_elpi_glob_quotation.under_ctx name ty bo ~k:(do_context_constr coq_ctx csts fields) ~depth state in let state, bo, gl3 = in_option ~depth state bo in let state, imp = in_elpi_imp ~depth state bk in state, E.mkApp ctxitemc (in_elpi_id name) [imp;ty;bo;E.mkLam fields], gl0 @ gl1 @ gl2 @ gl3 @@ -887,7 +887,7 @@ let best_effort_recover_arity ~depth state glob_sign typ bl = let rec aux ~depth state typ gbl = match gbl with | (name,ik,_,_) :: gbl -> - begin match Coq_elpi_HOAS.is_prod ~depth typ with + begin match Rocq_elpi_HOAS.is_prod ~depth typ with | None -> state, in_elpi_arity typ | Some(ty,bo) -> let state, imp = in_elpi_imp ~depth state ik in @@ -935,22 +935,22 @@ let close_glob coq_ctx term = let in_elpi_term_arg ~loc ~base ~depth state coq_ctx hyps sigma ist glob_or_expr = let closure = Ltac_plugin.Tacinterp.interp_glob_closure ist coq_ctx.env sigma glob_or_expr in - let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in - let state, t = Coq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in + let g = Rocq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state, t = Rocq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in state, E.mkApp trmc t [], [] let in_elpi_open_term_arg ~loc ~base ~depth state coq_ctx hyps sigma ist glob_or_expr = let closure = Ltac_plugin.Tacinterp.interp_glob_closure ist coq_ctx.env sigma glob_or_expr in - let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in + let g = Rocq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in let (n, g) = close_glob coq_ctx g in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in - let state, t = Coq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state, t = Rocq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in state, E.mkApp open_trmc (CD.of_int n) [t], [] let in_elpi_tac_econstr ~base:() ~depth ?calldepth coq_ctx hyps sigma state x = let state, gls0 = set_current_sigma ~depth state sigma in - let state, t, gls1 = Coq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state x in + let state, t, gls1 = Rocq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state x in state, [E.mkApp trmc t []], gls0 @ gls1 let in_elpi_elab_term_arg ~depth ?calldepth state coq_ctx hyps sigma ist glob_or_expr = @@ -972,7 +972,7 @@ let rec in_elpi_ltac_arg ~loc ~depth ~base ?calldepth coq_ctx hyps sigma state t raise (Taccoerce.CannotCoerceTo (s ^ " list")) in match (ty : ltac_ty) with | List (List _) -> - Coq_elpi_utils.err Pp.(str"ltac__list_list is not implemented") + Rocq_elpi_utils.err Pp.(str"ltac__list_list is not implemented") | List ty -> let l = to_list v in self_list ty state l @@ -988,23 +988,23 @@ let rec in_elpi_ltac_arg ~loc ~depth ~base ?calldepth coq_ctx hyps sigma state t state, [E.mkApp trmc t []], gls with CErrors.UserError _ -> try let closure = Taccoerce.coerce_to_uconstr v in - let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in - let state, t = Coq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in + let g = Rocq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state, t = Rocq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in state, [E.mkApp trmc t []], [] with Taccoerce.CannotCoerceTo _ -> try let id = Taccoerce.coerce_to_hyp coq_ctx.env sigma v in - let state, t, gls = Coq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state (EConstr.mkVar id) in + let state, t, gls = Rocq_elpi_HOAS.constr2lp ~depth ?calldepth coq_ctx E.no_constraints state (EConstr.mkVar id) in state, [E.mkApp trmc t []], gls with Taccoerce.CannotCoerceTo _ -> raise (Taccoerce.CannotCoerceTo "a term") end | OpenTerm -> let closure = Taccoerce.coerce_to_uconstr v in - let g = Coq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in + let g = Rocq_elpi_utils.detype_closed_glob coq_ctx.env sigma closure in let n, g = close_glob coq_ctx g in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in - let state, t = Coq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state, t = Rocq_elpi_glob_quotation.gterm2lp ~loc ~depth ~base g state in state, [E.mkApp open_trmc (CD.of_int n) [t]], [] let { CD.cin = of_ltac_tactic; isc = is_ltac_tactic; cout = to_ltac_tactic }, tac = CD.declare { @@ -1119,7 +1119,7 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = | RecordDecl (_ist,(glob_sign,raw_rdecl)) when raw -> let raw_rdecl = of_coq_record_definition raw_rdecl in let glob_rdecl = raw_record_decl_to_glob glob_sign raw_rdecl in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = grecord2lp ~loc ~base ~depth state glob_rdecl in state, t, [] | RecordDecl (_ist,(glob_sign,raw_rdecl)) -> @@ -1132,7 +1132,7 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = | IndtDecl (_ist,(glob_sign,raw_indt)) when raw -> let raw_indt = of_coq_inductive_definition raw_indt in let glob_indt = raw_indt_decl_to_glob glob_sign raw_indt in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = ginductive2lp ~loc ~depth ~base state glob_indt in state, t, [] | IndtDecl (_ist,(glob_sign,raw_indt)) -> @@ -1147,7 +1147,7 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = inductive_entry2lp ~depth coq_ctx E.no_constraints state ~loose_udecl:(udecl = None) e | ConstantDecl (_ist,(glob_sign,raw_cdecl)) when raw -> let state, glob_cdecl = raw_constant_decl_to_glob glob_sign raw_cdecl state in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in cdecl2lp ~loc ~depth ~base state glob_cdecl | ConstantDecl (_ist,(glob_sign,({ name; typ = (bl,_) } as raw_cdecl))) -> let state, udecl, typ, body, gls0 = @@ -1167,7 +1167,7 @@ let in_elpi_cmd ~loc ~depth ~base ?calldepth coq_ctx state ~raw (x : Cmd.top) = end | Context (_ist,(glob_sign,raw_ctx)) when raw -> let glob_ctx = raw_context_decl_to_glob glob_sign raw_ctx in - let state = Coq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in + let state = Rocq_elpi_glob_quotation.set_coq_ctx_hyps state (coq_ctx,hyps) in let state, t = do_context_glob ~loc glob_ctx ~depth ~base state in state, E.mkApp ctxc t [], [] | Context (_ist,(glob_sign,raw_ctx)) -> diff --git a/src/coq_elpi_arg_HOAS.mli b/src/rocq_elpi_arg_HOAS.mli similarity index 93% rename from src/coq_elpi_arg_HOAS.mli rename to src/rocq_elpi_arg_HOAS.mli index a72b263ed..7efa812e1 100644 --- a/src/coq_elpi_arg_HOAS.mli +++ b/src/rocq_elpi_arg_HOAS.mli @@ -1,9 +1,9 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) open Elpi.API.RawData -open Coq_elpi_utils +open Rocq_elpi_utils type phase = Interp | Synterp | Both @@ -103,8 +103,8 @@ val in_elpi_tac : base: Elpi.API.Compile.program -> depth:int -> ?calldepth:int -> - Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context -> - Coq_elpi_HOAS.hyp list -> + Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context -> + Rocq_elpi_HOAS.hyp list -> Evd.evar_map -> Elpi.API.State.t -> Tac.top -> @@ -114,8 +114,8 @@ val in_elpi_tac : val in_elpi_tac_econstr : base:unit -> depth:int -> ?calldepth:int -> - Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context -> - Coq_elpi_HOAS.hyp list -> + Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context -> + Rocq_elpi_HOAS.hyp list -> Evd.evar_map -> Elpi.API.State.t -> EConstr.t -> @@ -127,7 +127,7 @@ val in_elpi_cmd : depth:int -> base:Elpi.API.Compile.program -> ?calldepth:int -> - Coq_elpi_HOAS.empty Coq_elpi_HOAS.coq_context -> + Rocq_elpi_HOAS.empty Rocq_elpi_HOAS.coq_context -> Elpi.API.State.t -> raw:bool -> Cmd.top -> @@ -142,7 +142,7 @@ type coq_arg = Cint of int | Cstr of string | Ctrm of EConstr.t | CLtac1 of Geni val in_coq_arg : depth:int -> - Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context -> + Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context -> Elpi.API.Data.constraints -> Elpi.API.State.t -> term -> diff --git a/src/coq_elpi_arg_syntax.mlg b/src/rocq_elpi_arg_syntax.mlg similarity index 96% rename from src/coq_elpi_arg_syntax.mlg rename to src/rocq_elpi_arg_syntax.mlg index 1467ddff2..a0d226179 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/rocq_elpi_arg_syntax.mlg @@ -1,8 +1,8 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -DECLARE PLUGIN "coq-elpi.elpi" +DECLARE PLUGIN "rocq-elpi.elpi" { @@ -14,8 +14,8 @@ open Pcoq.Prim open Pvernac.Vernac_ open Pltac -module EA = Coq_elpi_arg_HOAS -module U = Coq_elpi_utils +module EA = Rocq_elpi_arg_HOAS +module U = Rocq_elpi_utils (* Arguments ************************************************************* *) let pr_elpi_string _ _ _ (s : Elpi.API.Ast.Loc.t * string) = Pp.str (snd s) @@ -28,17 +28,17 @@ let idents_of loc s = let s = String.sub s 1 (String.length s - 2) in let l = Str.(split (regexp "[\t \n]+") s) in List.iter (fun x -> if not (CLexer.is_ident x) then raise Stream.Failure) l; - Coq_elpi_utils.of_coq_loc (trim_loc loc), l + Rocq_elpi_utils.of_coq_loc (trim_loc loc), l let rec strip_curly loc s = if s.[0] = '\123' then strip_curly (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s + else Rocq_elpi_utils.of_coq_loc loc, s let rec strip_round loc s = if s.[0] = '(' then strip_round (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s + else Rocq_elpi_utils.of_coq_loc loc, s let rec strip_square loc s = if s.[0] = '[' then strip_square (trim_loc loc) String.(sub s 1 (length s - 2)) - else Coq_elpi_utils.of_coq_loc loc, s + else Rocq_elpi_utils.of_coq_loc loc, s } @@ -51,10 +51,10 @@ elpi_string : FIRST [ if s.[0] = '\123' then strip_curly loc s else if s.[0] = '(' then strip_round loc s else if s.[0] = '[' then strip_square loc s - else Coq_elpi_utils.of_coq_loc loc, s + else Rocq_elpi_utils.of_coq_loc loc, s } | s = STRING -> { - Coq_elpi_utils.of_coq_loc loc, s + Rocq_elpi_utils.of_coq_loc loc, s } ]]; END @@ -112,9 +112,9 @@ let any_attribute : Attributes.vernac_flags Attributes.attribute = let ignore_unknown_attributes extra = CWarnings.with_warn "unsupported-attributes" Attributes.unsupported_attributes extra -let scope_attribute : Coq_elpi_utils.clause_scope Attributes.attribute = +let scope_attribute : Rocq_elpi_utils.clause_scope Attributes.attribute = let open Attributes.Notations in - let open Coq_elpi_utils in + let open Rocq_elpi_utils in Attributes.attribute_of_list ["local", (fun ?loc old -> function diff --git a/src/coq_elpi_builtins.ml b/src/rocq_elpi_builtins.ml similarity index 95% rename from src/coq_elpi_builtins.ml rename to src/rocq_elpi_builtins.ml index d4e1ce2ab..398428698 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/rocq_elpi_builtins.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -25,8 +25,8 @@ module CNotation = Notation open Names -open Coq_elpi_utils -open Coq_elpi_HOAS +open Rocq_elpi_utils +open Rocq_elpi_HOAS let string_of_ppcmds options pp = let b = Buffer.create 512 in @@ -112,47 +112,47 @@ let pr_econstr_env options env sigma t = if options.hoas_holes = Some Heuristic then aux () expr else expr in Ppconstr.pr_constr_expr_n env sigma options.pplevel expr) -let tactic_mode : bool State.component = State.declare_component ~name:"coq-elpi:tactic-mode" ~descriptor:interp_state +let tactic_mode : bool State.component = State.declare_component ~name:"rocq-elpi:tactic-mode" ~descriptor:interp_state ~pp:(fun fmt x -> Format.fprintf fmt "%b" x) ~init:(fun () -> false) ~start:(fun x -> x) () let base = - API.State.declare_component ~name:"coq-elpi:base" ~descriptor:interp_state + API.State.declare_component ~name:"rocq-elpi:base" ~descriptor:interp_state ~init:(fun () -> None) ~pp:(fun fmt -> function Some _ -> () | None -> ()) ~start:(fun x -> x) () let abstract__grab_global_env_keep_sigma api thunk = (); (fun state -> let uctx, state, result, gls = thunk state in - Coq_elpi_HOAS.grab_global_env ~uctx state, result, gls) + Rocq_elpi_HOAS.grab_global_env ~uctx state, result, gls) let grab_global_env__drop_sigma_univs_if_option_is_set options api thunk = (); (fun state -> if State.get tactic_mode state then - Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); + Rocq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); let uctx, state, result, gls = thunk state in match options with - | { keepunivs = Some false } -> Coq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls - | _ -> Coq_elpi_HOAS.grab_global_env ~uctx state, result, gls) + | { keepunivs = Some false } -> Rocq_elpi_HOAS.grab_global_env_drop_univs_and_sigma state, result, gls + | _ -> Rocq_elpi_HOAS.grab_global_env ~uctx state, result, gls) let grab_global_env api thunk = (); (fun state -> if State.get tactic_mode state then - Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); + Rocq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); let uctx, state, result, gls = thunk state in - Coq_elpi_HOAS.grab_global_env ~uctx state, result, gls) + Rocq_elpi_HOAS.grab_global_env ~uctx state, result, gls) (* This is for stuff that is not monotonic in the env, eg section closing *) let grab_global_env_drop_sigma api thunk = (); (fun state -> if State.get tactic_mode state then - Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); + Rocq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); let state, result, gls = thunk state in - Coq_elpi_HOAS.grab_global_env_drop_sigma state, result, gls) + Rocq_elpi_HOAS.grab_global_env_drop_sigma state, result, gls) let grab_global_env_drop_sigma_keep_univs api thunk = (); (fun state -> if State.get tactic_mode state then - Coq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); + Rocq_elpi_utils.err Pp.(strbrk ("API " ^ api ^ " cannot be used in tactics")); let uctx, state, result, gls = thunk state in - Coq_elpi_HOAS.grab_global_env_drop_sigma_keep_univs ~uctx state, result, gls) + Rocq_elpi_HOAS.grab_global_env_drop_sigma_keep_univs ~uctx state, result, gls) let bool = B.bool let int = B.int @@ -192,14 +192,14 @@ let constr2lp_closed_ground ~depth hyps constraints state t = constr2lp_closed_ground ~depth hyps constraints state t let clauses_for_later_interp : _ State.component = - State.declare_component ~name:"coq-elpi:clauses_for_later" ~descriptor:interp_state + State.declare_component ~name:"rocq-elpi:clauses_for_later" ~descriptor:interp_state ~init:(fun () -> []) ~start:(fun x -> x) ~pp:(fun fmt l -> List.iter (fun (dbname, code,vars,scope) -> Format.fprintf fmt "db:%s code:%a scope:%a\n" (String.concat "." dbname) - Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l) () + Elpi.API.Pp.Ast.program code Rocq_elpi_utils.pp_scope scope) l) () let term = { CConv.ty = Conv.TyName "term"; @@ -260,26 +260,26 @@ let sealed_goal = { readback = (fun ~depth _ _ -> assert false); } -let goal : ( (Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context * Evar.t * Coq_elpi_arg_HOAS.coq_arg list) , API.Data.hyps, API.Data.constraints) CConv.t = { +let goal : ( (Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context * Evar.t * Rocq_elpi_arg_HOAS.coq_arg list) , API.Data.hyps, API.Data.constraints) CConv.t = { CConv.ty = Conv.TyName "goal"; pp_doc = (fun fmt () -> ()); pp = (fun fmt _ -> Format.fprintf fmt "TODO"); embed = (fun ~depth _ _ _ _ -> assert false); readback = (fun ~depth hyps csts state g -> - let state, ctx, k, raw_args, gls1 = Coq_elpi_HOAS.lp2goal ~depth hyps csts state g in - let state, args, gls2 = U.map_acc (Coq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in + let state, ctx, k, raw_args, gls1 = Rocq_elpi_HOAS.lp2goal ~depth hyps csts state g in + let state, args, gls2 = U.map_acc (Rocq_elpi_arg_HOAS.in_coq_arg ~depth ctx csts) state raw_args in state, (ctx,k,args), gls1 @ gls2); } -let tactic_arg : (Coq_elpi_arg_HOAS.coq_arg, Coq_elpi_HOAS.full Coq_elpi_HOAS.coq_context, API.Data.constraints) CConv.t = { +let tactic_arg : (Rocq_elpi_arg_HOAS.coq_arg, Rocq_elpi_HOAS.full Rocq_elpi_HOAS.coq_context, API.Data.constraints) CConv.t = { CConv.ty = Conv.TyName "argument"; pp_doc = (fun fmt () -> ()); pp = (fun fmt _ -> Format.fprintf fmt "TODO"); embed = (fun ~depth _ _ _ _ -> assert false); - readback = Coq_elpi_arg_HOAS.in_coq_arg; + readback = Rocq_elpi_arg_HOAS.in_coq_arg; } -let id = Coq_elpi_builtins_synterp.id +let id = Rocq_elpi_builtins_synterp.id let flag name = { (B.unspec bool) with Conv.ty = Conv.TyName name } @@ -524,7 +524,7 @@ let err_if_contains_alg_univ ~depth t = Univ.Universe.pr UnivNames.pr_level_with_global_universes u) | _ -> Univ.Universe.Set.add u acc end - | x -> Coq_elpi_utils.fold_elpi_term aux acc ~depth x + | x -> Rocq_elpi_utils.fold_elpi_term aux acc ~depth x in let univs = aux ~depth Univ.Universe.Set.empty t in univs @@ -913,7 +913,7 @@ let add_axiom_or_variable api id ty local_bkind options state = let univs = UState.check_univ_decl (Evd.evar_universe_context sigma) udecl ~poly in let kind = Decls.Logical in let impargs = [] in - let loc = to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in let id = Id.of_string id in let name = CAst.(make ~loc id) in if not (is_ground sigma ty) then @@ -937,7 +937,7 @@ let add_axiom_or_variable api id ty local_bkind options state = type tac_abbrev = { abbrev_name : qualified_name; tac_name : qualified_name; - tac_fixed_args : Coq_elpi_arg_HOAS.Tac.glob list; + tac_fixed_args : Rocq_elpi_arg_HOAS.Tac.glob list; } type ('a,'d) gbpmp = Gbpmp : ('d, _, 'b, Loc.t -> 'd) Pcoq.Rule.t * ('a -> 'b) -> ('a,'d) gbpmp @@ -955,25 +955,25 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let tac = let open Tacexpr in let elpi_tac = { - mltac_plugin = "coq-elpi.elpi"; + mltac_plugin = "rocq-elpi.elpi"; mltac_tactic = "elpi_tac"; } in let elpi_tac_entry = { mltac_name = elpi_tac; mltac_index = 0; } in let more_args = more_args |> List.map (function - | Coq_elpi_arg_HOAS.Tac.Int _ as t -> t - | Coq_elpi_arg_HOAS.Tac.String _ as t -> t - | Coq_elpi_arg_HOAS.Tac.Term (t,_) -> + | Rocq_elpi_arg_HOAS.Tac.Int _ as t -> t + | Rocq_elpi_arg_HOAS.Tac.String _ as t -> t + | Rocq_elpi_arg_HOAS.Tac.Term (t,_) -> let expr = Constrextern.extern_glob_constr Constrextern.empty_extern_env t in let rec aux () ({ CAst.v } as orig) = match v with | Constrexpr.CEvar _ -> CAst.make @@ Constrexpr.CHole(None) | _ -> Constrexpr_ops.map_constr_expr_with_binders (fun _ () -> ()) aux () orig in - Coq_elpi_arg_HOAS.Tac.Term (aux () expr) + Rocq_elpi_arg_HOAS.Tac.Term (aux () expr) | _ -> assert false) in let tacname = loc, tacname in - let tacname = Genarg.in_gen (Genarg.rawwit Coq_elpi_arg_syntax.wit_qualified_name) tacname in - let args = args |> List.map (fun (arg,_) -> Coq_elpi_arg_HOAS.Tac.Term(arg)) in - let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Coq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in + let tacname = Genarg.in_gen (Genarg.rawwit Rocq_elpi_arg_syntax.wit_qualified_name) tacname in + let args = args |> List.map (fun (arg,_) -> Rocq_elpi_arg_HOAS.Tac.Term(arg)) in + let args = Genarg.in_gen (Genarg.rawwit (Genarg.wit_list Rocq_elpi_arg_syntax.wit_elpi_tactic_arg)) (more_args @ args) in (TacML (elpi_tac_entry, [TacGeneric(None, tacname); TacGeneric(None, args)])) in CAst.make @@ Constrexpr.CGenarg (Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) (CAst.make tac)) in let Gbpmp (rule, action) = gbpmp action (List.rev abbrev_name) in @@ -987,7 +987,7 @@ let cache_abbrev_for_tac { abbrev_name; tac_name = tacname; tac_fixed_args = mor let subst_abbrev_for_tac (subst, { abbrev_name; tac_name; tac_fixed_args }) = { abbrev_name; tac_name; - tac_fixed_args = List.map (Coq_elpi_arg_HOAS.Tac.subst subst) tac_fixed_args + tac_fixed_args = List.map (Rocq_elpi_arg_HOAS.Tac.subst subst) tac_fixed_args } let inAbbreviationForTactic : tac_abbrev -> Libobject.obj = @@ -1278,15 +1278,15 @@ let coq_header_builtins = % This file is automatically generated from % - coq-HOAS.elpi -% - coq_elpi_builtin.ml +% - rocq_elpi_builtin.ml % and contains the description of the data type of Coq terms and the % API to access Coq. |}; - LPCode Coq_elpi_builtins_arg_HOAS.code; - LPCode Coq_elpi_builtins_HOAS.code; - MLData Coq_elpi_HOAS.record_field_att; - MLData Coq_elpi_HOAS.coercion_status; + LPCode Rocq_elpi_builtins_arg_HOAS.code; + LPCode Rocq_elpi_builtins_HOAS.code; + MLData Rocq_elpi_HOAS.record_field_att; + MLData Rocq_elpi_HOAS.coercion_status; LPCode {| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -1384,7 +1384,7 @@ let coq_misc_builtins = let x, args = List.hd args, List.tl args in match E.look ~depth x with | E.CData loc when API.RawOpaqueData.is_loc loc -> - Some (Coq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args + Some (Rocq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args | _ -> None, x :: args in warning ?loc (pp2string (P.list ~boxed:true pp " ") args); @@ -1418,7 +1418,7 @@ line option|}))), let x, args = List.hd args, List.tl args in match E.look ~depth x with | E.CData loc when API.RawOpaqueData.is_loc loc -> - Some (Coq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args + Some (Rocq_elpi_utils.to_coq_loc (API.RawOpaqueData.to_loc loc)), args | _ -> None, x :: args in let txt = pp2string (P.list ~boxed:true pp " ") args in @@ -1475,11 +1475,11 @@ Note: [ctype "bla"] is an opaque data type and by convention it is written [@bla MLData id; MLData modpath; MLData modtypath; - MLData Coq_elpi_builtins_synterp.located; + MLData Rocq_elpi_builtins_synterp.located; MLCode(Pred("coq.locate-all", In(id, "Name", - Out(B.list Coq_elpi_builtins_synterp.located, "Located", + Out(B.list Rocq_elpi_builtins_synterp.located, "Located", Easy {|finds all possible meanings of a string. Does not fail.|})), (fun s _ ~depth -> let qualid = Libnames.qualid_of_string s in @@ -1487,16 +1487,16 @@ Note: [ctype "bla"] is an opaque data type and by convention it is written [@bla let add x = l := !l @ [x] in begin match locate_qualid qualid with - | Some (`Gref gr) -> add @@ Coq_elpi_builtins_synterp.LocGref gr - | Some (`Abbrev sd) -> add @@ Coq_elpi_builtins_synterp.LocAbbreviation sd + | Some (`Gref gr) -> add @@ Rocq_elpi_builtins_synterp.LocGref gr + | Some (`Abbrev sd) -> add @@ Rocq_elpi_builtins_synterp.LocAbbreviation sd | None -> () end; begin - try add @@ Coq_elpi_builtins_synterp.LocModule (Nametab.locate_module qualid) + try add @@ Rocq_elpi_builtins_synterp.LocModule (Nametab.locate_module qualid) with Not_found -> () end; begin - try add @@ Coq_elpi_builtins_synterp.LocModuleType (Nametab.locate_modtype qualid) + try add @@ Rocq_elpi_builtins_synterp.LocModuleType (Nametab.locate_modtype qualid) with Not_found -> () end; !: !l)), @@ -1864,8 +1864,8 @@ Supported attributes: | Variable v -> raise No_clause)), DocAbove); - Coq_elpi_builtins_synterp.locate_module; - Coq_elpi_builtins_synterp.locate_module_type; + Rocq_elpi_builtins_synterp.locate_module; + Rocq_elpi_builtins_synterp.locate_module_type; MLData module_item; @@ -1944,7 +1944,7 @@ Supported attributes: (fun _ ~depth _ _ state -> !: (mp2path (Global.current_modpath ())))), DocAbove); - Coq_elpi_builtins_synterp.current_section_path; + Rocq_elpi_builtins_synterp.current_section_path; LPCode {|% Deprecated, use coq.env.opaque? pred coq.env.const-opaque? i:constant. @@ -2044,7 +2044,7 @@ Supported attributes: let gr, uctx = declare_definition uctx options.using ~cinfo ~info ~opaque ~body sigma in let () = - let lid = CAst.make ~loc:(to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in + let lid = CAst.make ~loc:(to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state) (Id.of_string id) in match scope with | Locality.Discharge -> Dumpglob.dump_definition lid true "var" | Locality.Global _ -> Dumpglob.dump_definition lid false "def" @@ -2123,7 +2123,7 @@ Supported attributes: | [ { Entries.mind_entry_typename = id; mind_entry_consnames = cids }] -> id, cids | _ -> assert false in - let lid_of id = CAst.make ~loc:(to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state) id in + let lid_of id = CAst.make ~loc:(to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state) id in begin match record_info with | None -> (* regular inductive *) Dumpglob.dump_definition (lid_of id) false "ind"; @@ -2188,9 +2188,9 @@ with a number, starting from 1. In(id, "The name of the functor", In(B.unspec (option modtypath), "Its module type (optional)", In(B.unspec (list (pair id modtypath)), "Parameters of the functor (optional)", - Full(unit_ctx, "Starts a functor" ^ Coq_elpi_builtins_synterp.synterp_api_doc)))), + Full(unit_ctx, "Starts a functor" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)))), (fun name mp params ~depth _ _ -> grab_global_env "coq.env.begin-module-functor" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_BeginModule (name,mp,params) state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginModule (name,mp,params) state in Univ.ContextSet.empty, state, (), []))), DocNext); @@ -2202,9 +2202,9 @@ coq.env.begin-module Name MP :- coq.env.begin-module-functor Name MP []. (* XXX When Coq's API allows it, call vernacentries directly *) MLCode(Pred("coq.env.end-module", Out(modpath, "ModPath", - Full(unit_ctx, "end the current module that becomes known as ModPath *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc)), + Full(unit_ctx, "end the current module that becomes known as ModPath *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)), (fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module" (fun state -> - let state, mp = Coq_elpi_builtins_synterp.SynterpAction.pop_EndModule () state in + let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_EndModule () state in state, ?: mp, []))), DocAbove); @@ -2212,9 +2212,9 @@ coq.env.begin-module Name MP :- coq.env.begin-module-functor Name MP []. MLCode(Pred("coq.env.begin-module-type-functor", In(id, "The name of the functor", In(B.unspec (list (pair id modtypath)), "The parameters of the functor (optional)", - Full(unit_ctx,"Starts a module type functor *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc))), + Full(unit_ctx,"Starts a module type functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun id params ~depth _ _ -> grab_global_env "coq.env.begin-module-type-functor" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_BeginModuleType (id,params) state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginModuleType (id,params) state in Univ.ContextSet.empty, state, (), []))), DocNext); @@ -2227,9 +2227,9 @@ coq.env.begin-module-type Name :- (* XXX When Coq's API allows it, call vernacentries directly *) MLCode(Pred("coq.env.end-module-type", Out(modtypath, "ModTyPath", - Full(unit_ctx, "end the current module type that becomes known as ModPath *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc)), + Full(unit_ctx, "end the current module type that becomes known as ModPath *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)), (fun _ ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-module-type" (fun state -> - let state, mp = Coq_elpi_builtins_synterp.SynterpAction.pop_EndModuleType () state in + let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_EndModuleType () state in state, ?: mp, []))), DocAbove); @@ -2240,9 +2240,9 @@ coq.env.begin-module-type Name :- In(B.unspec (list modpath), "Its arguments (optional)", In(B.unspec module_inline_default, "Arguments inlining (optional)", Out(modpath, "The modpath of the new module", - Full(unit_ctx, "Applies a functor *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc))))))), + Full(unit_ctx, "Applies a functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))))))), (fun name mp f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-functor" (fun state -> - let state, mp = Coq_elpi_builtins_synterp.SynterpAction.pop_ApplyModule (name,mp,f,arguments,inline) state in + let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_ApplyModule (name,mp,f,arguments,inline) state in Univ.ContextSet.empty, state, ?: mp, []))), DocNext); @@ -2252,9 +2252,9 @@ coq.env.begin-module-type Name :- In(B.unspec (list modpath), "Its arguments (optional)", In(B.unspec module_inline_default, "Arguments inlining (optional)", Out(modtypath, "The modtypath of the new module type", - Full(unit_ctx, "Applies a type functor *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc)))))), + Full(unit_ctx, "Applies a type functor *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc)))))), (fun name f arguments inline _ ~depth _ _ -> grab_global_env "coq.env.apply-module-type-functor" (fun state -> - let state, mp = Coq_elpi_builtins_synterp.SynterpAction.pop_ApplyModuleType (name,f,arguments,inline) state in + let state, mp = Rocq_elpi_builtins_synterp.SynterpAction.pop_ApplyModuleType (name,f,arguments,inline) state in Univ.ContextSet.empty, state, ?: mp, []))), DocNext); @@ -2262,9 +2262,9 @@ coq.env.begin-module-type Name :- MLCode(Pred("coq.env.include-module", In(modpath, "ModPath", In(B.unspec module_inline_default, "Inline (optional)", - Full(unit_ctx, "is like the vernacular Include, Inline can be omitted *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc))), + Full(unit_ctx, "is like the vernacular Include, Inline can be omitted *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun mp i ~depth _ _ -> grab_global_env "coq.env.include-module" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_IncludeModule (mp,i) state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_IncludeModule (mp,i) state in Univ.ContextSet.empty, state, (), []))), DocAbove); @@ -2272,9 +2272,9 @@ coq.env.begin-module-type Name :- MLCode(Pred("coq.env.include-module-type", In(modtypath, "ModTyPath", In(B.unspec module_inline_default, "Inline (optional)", - Full(unit_ctx, "is like the vernacular Include Type, Inline can be omitted *E*" ^ Coq_elpi_builtins_synterp.synterp_api_doc))), + Full(unit_ctx, "is like the vernacular Include Type, Inline can be omitted *E*" ^ Rocq_elpi_builtins_synterp.synterp_api_doc))), (fun mp i ~depth _ _ -> grab_global_env "coq.env.include-module-type" (fun state -> - let state,_ = Coq_elpi_builtins_synterp.SynterpAction.pop_IncludeModuleType (mp,i) state in + let state,_ = Rocq_elpi_builtins_synterp.SynterpAction.pop_IncludeModuleType (mp,i) state in Univ.ContextSet.empty, state, (), []))), DocAbove); @@ -2282,7 +2282,7 @@ coq.env.begin-module-type Name :- In(modpath, "ModPath", Full(unit_ctx, "is like the vernacular Import *E*")), (fun mp ~depth _ _ -> grab_global_env "coq.env.import-module" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_ImportModule mp state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_ImportModule mp state in Univ.ContextSet.empty, state, (), []))), DocAbove); @@ -2290,7 +2290,7 @@ coq.env.begin-module-type Name :- In(modpath, "ModPath", Full(unit_ctx, "is like the vernacular Export *E*")), (fun mp ~depth _ _ -> grab_global_env "coq.env.export-module" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_ExportModule mp state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_ExportModule mp state in Univ.ContextSet.empty, state, (), []))), DocAbove); @@ -2314,14 +2314,14 @@ denote the same x as before.|}; In(id, "Name", Full(unit_ctx, "starts a section named Name *E*")), (fun id ~depth _ _ -> grab_global_env "coq.env.begin-section" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_BeginSection id state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_BeginSection id state in Univ.ContextSet.empty, state, (), []))), DocAbove); MLCode(Pred("coq.env.end-section", Full(unit_ctx, "end the current section *E*"), (fun ~depth _ _ -> grab_global_env_drop_sigma "coq.env.end-section" (fun state -> - let state, _ = Coq_elpi_builtins_synterp.SynterpAction.pop_EndSection () state in + let state, _ = Rocq_elpi_builtins_synterp.SynterpAction.pop_EndSection () state in state, (), []))), DocAbove); @@ -2391,7 +2391,7 @@ accept universe variables, we provide the coq.univ.variable API which is able to craft a universe variable which is roughly equivalent to an algebraic universe, e.g. k such that j+1 = k. -Coq-Elpi systematically purges algebraic universes from terms (and +Rocq-Elpi systematically purges algebraic universes from terms (and types and sorts) when one reads them from the environment. This makes the embedding of terms less precise than what it could be. The different data types stay, since Coq will eventually become @@ -2633,14 +2633,14 @@ declared as cumulative.|}; LPDoc "-- Primitive --------------------------------------------------------"; - MLData Coq_elpi_utils.uint63; - MLData Coq_elpi_utils.float64; - MLData Coq_elpi_utils.pstring; - MLData Coq_elpi_utils.projection; + MLData Rocq_elpi_utils.uint63; + MLData Rocq_elpi_utils.float64; + MLData Rocq_elpi_utils.pstring; + MLData Rocq_elpi_utils.projection; MLData primitive_value; MLCode(Pred("coq.uint63->int", - In(Coq_elpi_utils.uint63,"U", + In(Rocq_elpi_utils.uint63,"U", Out(B.int,"I", Easy "Transforms a primitive unsigned integer U into an elpi integer I. Fails if it does not fit.")), (fun u _ ~depth:_ -> @@ -2652,14 +2652,14 @@ declared as cumulative.|}; MLCode(Pred("coq.int->uint63", In(B.int,"I", - Out(Coq_elpi_utils.uint63,"U", + Out(Rocq_elpi_utils.uint63,"U", Easy "Transforms an elpi integer I into a primitive unsigned integer U. Fails if I is negative.")), (fun i _ ~depth:_ -> if i >= 0 then !: (Uint63.of_int i) else raise No_clause)), DocAbove); MLCode(Pred("coq.float64->float", - In(Coq_elpi_utils.float64,"F64", + In(Rocq_elpi_utils.float64,"F64", Out(B.float,"F", Easy "Transforms a primitive float on 64 bits to an elpi one. Currently, it should not fail.")), (fun f _ ~depth:_ -> @@ -2670,7 +2670,7 @@ declared as cumulative.|}; MLCode(Pred("coq.float->float64", In(B.float,"F", - Out(Coq_elpi_utils.float64,"F64", + Out(Rocq_elpi_utils.float64,"F64", Easy "Transforms an elpi float F to a primitive float on 64 bits. Currently, it should not fail.")), (fun f _ ~depth:_ -> !: (Float64.of_float f))), @@ -2695,7 +2695,7 @@ declared as cumulative.|}; DocAbove); MLCode(Pred("coq.pstring->string", - In(Coq_elpi_utils.pstring,"PS", + In(Rocq_elpi_utils.pstring,"PS", Out(B.string,"S", Easy "Transforms a Coq primitive string to an elpi string. It does not fail.")), (fun s _ ~depth:_ -> !: (string_of_pstring s))), @@ -2703,7 +2703,7 @@ declared as cumulative.|}; MLCode(Pred("coq.string->pstring", In(B.string,"S", - Out(Coq_elpi_utils.pstring,"PS", + Out(Rocq_elpi_utils.pstring,"PS", Easy "Transforms an elpi string into a Coq primitive string. It fails if the lenght of S is greater than the maximal primitive string length.")), (fun s _ ~depth:_ -> match pstring_of_string s with @@ -2775,9 +2775,9 @@ Supported attributes: Out(B.list (B.poly "A"), "Nodes in toposort order", Read(global,"takes a graph and returns the nodes in topological order"))), (fun graph _ ~depth { options } _ _ -> - let graph = Coq_elpi_graph.Graph.build graph in - let topo_sort = Coq_elpi_graph.Graph.topo_sort graph in - (* Coq_elpi_graph.Graph.print string_of_int graph; *) + let graph = Rocq_elpi_graph.Graph.build graph in + let topo_sort = Rocq_elpi_graph.Graph.topo_sort graph in + (* Rocq_elpi_graph.Graph.print string_of_int graph; *) !: topo_sort)), DocAbove); @@ -2981,7 +2981,7 @@ Supported attributes:|} ^ hint_locality_doc))))), let hint_priority = unspec2opt priority in let sigma = get_sigma state in let hint_pattern = unspec2opt pattern |> Option.map (fun x -> x |> - Coq_elpi_utils.detype env sigma |> + Rocq_elpi_utils.detype env sigma |> pattern_of_glob_constr env) in let info = { Typeclasses.hint_priority; hint_pattern } in Hints.add_hints ~locality [db] Hints.(Hints.HintsResolveEntry[info, true, hint_globref gr]); @@ -3186,7 +3186,7 @@ Supported attributes: let onlyparsing = (onlyparsing = B.Given true) in let name = Id.of_string name in let vars, nenv, env, body = strip_n_lambas nargs env term in - let gbody = Coq_elpi_utils.detype env sigma body in + let gbody = Rocq_elpi_utils.detype env sigma body in let pat, _ = Notation_ops.notation_constr_of_glob_constr nenv gbody in let warns = warns_of_options options in Abbreviation.declare_abbreviation ~local ~onlyparsing warns name (vars,pat); @@ -3211,7 +3211,7 @@ Supported attributes: int nargs ++ str " arguments but was given " ++ int argno); let open Constrexpr in let binders, vars = List.split (CList.init nargs (fun i -> - let name = Coq_elpi_glob_quotation.mk_restricted_name i in + let name = Rocq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in mkCLocalAssum [lname] (Default Glob_term.Explicit) (CAst.make @@ CHole(None)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in @@ -3219,12 +3219,12 @@ Supported attributes: let sigma = get_sigma state in let geta = Constrintern.intern_constr env sigma eta in let base = Option.get @@ State.get base state in - let loc = to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state in - let teta = Coq_elpi_glob_quotation.runtime_gterm2lp ~loc ~base ~depth geta state in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let teta = Rocq_elpi_glob_quotation.runtime_gterm2lp ~loc ~base ~depth geta state in let t = let rec aux ~depth n t = if n = 0 then t - else match Coq_elpi_HOAS.is_lam ~depth t with + else match Rocq_elpi_HOAS.is_lam ~depth t with | Some(_,bo) -> E.mkLam (aux ~depth:(depth+1) (n-1) bo) | None -> CErrors.anomaly Pp.(str"coq.notation.abbreviation") in @@ -3243,7 +3243,7 @@ Supported attributes: let nargs = List.length args in let open Constrexpr in let binders, vars = List.split (CList.init nargs (fun i -> - let name = Coq_elpi_glob_quotation.mk_restricted_name i in + let name = Rocq_elpi_glob_quotation.mk_restricted_name i in let lname = CAst.make @@ Name.Name (Id.of_string name) in mkCLocalAssum [lname] (Default Glob_term.Explicit) (CAst.make @@ CHole(None)), (CAst.make @@ CRef(Libnames.qualid_of_string name,None), None))) in @@ -3251,8 +3251,8 @@ Supported attributes: let sigma = get_sigma state in let geta = Constrintern.intern_constr env sigma eta in let base = Option.get @@ State.get base state in - let loc = to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state in - let teta = Coq_elpi_glob_quotation.runtime_gterm2lp ~loc ~base ~depth geta state in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in + let teta = Rocq_elpi_glob_quotation.runtime_gterm2lp ~loc ~base ~depth geta state in state, !: nargs +! teta, [] )), DocAbove); @@ -3276,18 +3276,18 @@ is equivalent to Elpi Export TacName.|})))), let sigma = get_sigma state in let env = get_global_env state in let tac_fixed_args = more_args |> List.map (function - | Coq_elpi_arg_HOAS.Cint n -> Coq_elpi_arg_HOAS.Tac.Int n - | Coq_elpi_arg_HOAS.Cstr s -> Coq_elpi_arg_HOAS.Tac.String s - | Coq_elpi_arg_HOAS.Ctrm t -> Coq_elpi_arg_HOAS.Tac.Term (Coq_elpi_utils.detype env sigma t,None) - | Coq_elpi_arg_HOAS.CLtac1 _ -> nYI "tactic notation with LTac1 argument") in - let abbrev_name = Coq_elpi_utils.string_split_on_char '.' name in - let tac_name = Coq_elpi_utils.string_split_on_char '.' tacname in + | Rocq_elpi_arg_HOAS.Cint n -> Rocq_elpi_arg_HOAS.Tac.Int n + | Rocq_elpi_arg_HOAS.Cstr s -> Rocq_elpi_arg_HOAS.Tac.String s + | Rocq_elpi_arg_HOAS.Ctrm t -> Rocq_elpi_arg_HOAS.Tac.Term (Rocq_elpi_utils.detype env sigma t,None) + | Rocq_elpi_arg_HOAS.CLtac1 _ -> nYI "tactic notation with LTac1 argument") in + let abbrev_name = Rocq_elpi_utils.string_split_on_char '.' name in + let tac_name = Rocq_elpi_utils.string_split_on_char '.' tacname in Lib.add_leaf @@ inAbbreviationForTactic { abbrev_name; tac_name; tac_fixed_args}; Univ.ContextSet.empty, state, (), []))), DocAbove); - MLData Coq_elpi_builtins_synterp.attribute_value; - MLData Coq_elpi_builtins_synterp.attribute; + MLData Rocq_elpi_builtins_synterp.attribute_value; + MLData Rocq_elpi_builtins_synterp.attribute; LPDoc "-- Coq's pretyper ---------------------------------------------------"; @@ -3664,7 +3664,7 @@ coq.reduction.lazy.whd_all X Y :- LPDoc "-- Coq's tactics --------------------------------------------"; - MLData Coq_elpi_arg_HOAS.tac; + MLData Rocq_elpi_arg_HOAS.tac; MLCode(Pred("coq.ltac.fail", In(B.unspec B.int,"Level", @@ -3749,10 +3749,10 @@ Supported attributes: let sigma = get_sigma state in let tac_args = tac_args |> List.map (function - | Coq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t - | Coq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s - | Coq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i - | Coq_elpi_arg_HOAS.CLtac1 x -> x) in + | Rocq_elpi_arg_HOAS.Ctrm t -> Tacinterp.Value.of_constr t + | Rocq_elpi_arg_HOAS.Cstr s -> Geninterp.(Val.inject (val_tag (Genarg.topwit Stdarg.wit_string))) s + | Rocq_elpi_arg_HOAS.Cint i -> Tacinterp.Value.of_int i + | Rocq_elpi_arg_HOAS.CLtac1 x -> x) in let tactic = let tac = match E.look ~depth tac with @@ -3769,8 +3769,8 @@ Supported attributes: let tacref = Locus.ArgArg (Loc.tag @@ tac_name) in let tacexpr = Tacexpr.(CAst.make @@ TacArg (TacCall (CAst.make @@ (tacref, [])))) in Tacinterp.Value.of_closure (Tacinterp.default_ist ()) tacexpr - | E.CData t when Coq_elpi_arg_HOAS.is_ltac_tactic t -> - Coq_elpi_arg_HOAS.to_ltac_tactic t + | E.CData t when Rocq_elpi_arg_HOAS.is_ltac_tactic t -> + Rocq_elpi_arg_HOAS.to_ltac_tactic t | _ -> U.type_error ("coq.ltac.call-ltac1: string or ltac1-tactic are expected as the tactic to call") in Tacinterp.Value.apply tac tac_args in @@ -3954,10 +3954,10 @@ coq.id->name S N :- coq.string->name S N. (fun gr _ ~depth h c state -> !: (gr2path gr))), DocAbove); - Coq_elpi_builtins_synterp.modpath_to_path; - Coq_elpi_builtins_synterp.modtypath_to_path; - Coq_elpi_builtins_synterp.modpath_to_library; - Coq_elpi_builtins_synterp.modtypath_to_library; + Rocq_elpi_builtins_synterp.modpath_to_path; + Rocq_elpi_builtins_synterp.modtypath_to_path; + Rocq_elpi_builtins_synterp.modpath_to_library; + Rocq_elpi_builtins_synterp.modtypath_to_library; MLCode(Pred("coq.term->string", CIn(failsafe_term,"T", @@ -4028,9 +4028,9 @@ Supported attributes: LPDoc "-- Access to Elpi's data --------------------------------------------"; (* Self modification *) - MLData Coq_elpi_builtins_synterp.clause; - MLData Coq_elpi_builtins_synterp.grafting; - MLData Coq_elpi_builtins_synterp.scope; + MLData Rocq_elpi_builtins_synterp.clause; + MLData Rocq_elpi_builtins_synterp.grafting; + MLData Rocq_elpi_builtins_synterp.scope; LPCode {| % see coq.elpi.accumulate-clauses @@ -4039,9 +4039,9 @@ coq.elpi.accumulate S N C :- coq.elpi.accumulate-clauses S N [C]. |}; MLCode(Pred("coq.elpi.accumulate-clauses", - In(B.unspec Coq_elpi_builtins_synterp.scope, "Scope", + In(B.unspec Rocq_elpi_builtins_synterp.scope, "Scope", In(id, "DbName", - In(B.list Coq_elpi_builtins_synterp.clause, "Clauses", + In(B.list Rocq_elpi_builtins_synterp.clause, "Clauses", Full (global, {| Declare that, once the program is over, the given clauses has to be added to the given db (see Elpi Db). @@ -4060,7 +4060,7 @@ Supported attributes: - @local! (default: false, discard at the end of section or module) - @global! (default: false, always active, only if Scope is execution-site, discouraged)|} )))), (fun scope dbname clauses ~depth {options} _ state -> - Coq_elpi_builtins_synterp.accumulate_clauses + Rocq_elpi_builtins_synterp.accumulate_clauses ~clauses_for_later:clauses_for_later_interp ~accumulate_to_db:(get_accumulate_to_db_interp()) ~preprocess_clause ~scope ~dbname clauses ~depth ~options state)), @@ -4081,7 +4081,7 @@ Supported attributes: - @local! (default: false, discard at the end of section or module) - @global! (default: false, always active|}))))), (fun dbname indexing predname spec ~depth ctx _ state -> - let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in + let dbname = Rocq_elpi_utils.string_split_on_char '.' dbname in let f = get_accumulate_text_to_db_interp () in let local = ctx.options.local = Some true in let super_global = ctx.options.local = Some false in @@ -4099,7 +4099,7 @@ Supported attributes: let spec = String.concat ", " spec in let text = indexing ^ "pred " ^ predname ^ " " ^ spec ^ "." in let scope = if local then Local else if super_global then SuperGlobal else Regular in - let loc = to_coq_loc @@ State.get Coq_elpi_builtins_synterp.invocation_site_loc state in + let loc = to_coq_loc @@ State.get Rocq_elpi_builtins_synterp.invocation_site_loc state in f ~loc dbname text scope; state, (), [] )), @@ -4121,7 +4121,7 @@ Supported attributes: DocAbove); - ] @ Coq_elpi_builtins_synterp.SynterpAction.builtins_interp @ [ + ] @ Rocq_elpi_builtins_synterp.SynterpAction.builtins_interp @ [ LPDoc "-- Utils ------------------------------------------------------------"; ] @ diff --git a/src/coq_elpi_builtins.mli b/src/rocq_elpi_builtins.mli similarity index 74% rename from src/coq_elpi_builtins.mli rename to src/rocq_elpi_builtins.mli index 93675e1f6..3a8da84ef 100644 --- a/src/coq_elpi_builtins.mli +++ b/src/rocq_elpi_builtins.mli @@ -1,9 +1,9 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) open Elpi.API -open Coq_elpi_utils +open Rocq_elpi_utils val coq_header_builtins : BuiltIn.declaration list val coq_misc_builtins : BuiltIn.declaration list @@ -12,10 +12,10 @@ val coq_rest_builtins : BuiltIn.declaration list (* Clauses to be added to elpi programs when the execution is over *) -val clauses_for_later_interp : (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list State.component +val clauses_for_later_interp : (qualified_name * Ast.program * Names.Id.t list * Rocq_elpi_utils.clause_scope) list State.component -val set_accumulate_to_db_interp : (loc:Loc.t -> (qualified_name * Ast.program * Names.Id.t list * Coq_elpi_utils.clause_scope) list -> unit) -> unit -val set_accumulate_text_to_db_interp : (loc:Loc.t -> (string list -> string -> Coq_elpi_utils.clause_scope -> unit)) -> unit +val set_accumulate_to_db_interp : (loc:Loc.t -> (qualified_name * Ast.program * Names.Id.t list * Rocq_elpi_utils.clause_scope) list -> unit) -> unit +val set_accumulate_text_to_db_interp : (loc:Loc.t -> (string list -> string -> Rocq_elpi_utils.clause_scope -> unit)) -> unit (* In tactic mode some APIs are disabled *) val tactic_mode : bool State.component diff --git a/src/coq_elpi_builtins_synterp.ml b/src/rocq_elpi_builtins_synterp.ml similarity index 97% rename from src/coq_elpi_builtins_synterp.ml rename to src/rocq_elpi_builtins_synterp.ml index a5089c672..3a65643f3 100644 --- a/src/coq_elpi_builtins_synterp.ml +++ b/src/rocq_elpi_builtins_synterp.ml @@ -1,8 +1,8 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -[%%import "coq_elpi_config.mlh"] +[%%import "rocq_elpi_config.mlh"] module API = Elpi.API module State = API.State @@ -17,8 +17,8 @@ module U = API.Utils open Names -open Coq_elpi_utils -open Coq_elpi_HOAS +open Rocq_elpi_utils +open Rocq_elpi_HOAS let prop = { B.any with Conv.ty = Conv.TyName "prop" } @@ -100,14 +100,14 @@ let set_accumulate_to_db_synterp, get_accumulate_to_db_synterp = (fun () -> !f) let clauses_for_later_synterp : _ State.component = - State.declare_component ~name:"coq-elpi:clauses_for_later" ~descriptor:synterp_state + State.declare_component ~name:"rocq-elpi:clauses_for_later" ~descriptor:synterp_state ~init:(fun () -> []) ~start:(fun x -> x) ~pp:(fun fmt l -> List.iter (fun (dbname, code,vars,scope) -> Format.fprintf fmt "db:%s code:%a scope:%a\n" (String.concat "." dbname) - Elpi.API.Pp.Ast.program code Coq_elpi_utils.pp_scope scope) l) () + Elpi.API.Pp.Ast.program code Rocq_elpi_utils.pp_scope scope) l) () type located = @@ -142,12 +142,12 @@ let pair = B.pair let option = B.option let invocation_site_loc : API.Ast.Loc.t State.component = - State.declare_component ~name:"coq-elpi:invocation-site-loc" ~descriptor:interp_state + State.declare_component ~name:"rocq-elpi:invocation-site-loc" ~descriptor:interp_state ~pp:(fun fmt x -> Format.fprintf fmt "%a" API.Ast.Loc.pp x) ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)") ~start:(fun x -> x) () let invocation_site_loc_synterp : API.Ast.Loc.t State.component = - State.declare_component ~name:"coq-elpi:invocation-site-loc" ~descriptor:synterp_state + State.declare_component ~name:"rocq-elpi:invocation-site-loc" ~descriptor:synterp_state ~pp:(fun fmt x -> Format.fprintf fmt "%a" API.Ast.Loc.pp x) ~init:(fun () -> API.Ast.Loc.initial "(should-not-happen)") ~start:(fun x -> x) () @@ -158,11 +158,11 @@ let compat_graft x = x let compat_graft = Option.map (function `Remove, _ -> nYI "clause removal" | ((`Replace | `Before | `After), _) as x -> x) [%%endif] -type accumulation_item = qualified_name * API.Ast.program * Id.t list * Coq_elpi_utils.clause_scope +type accumulation_item = qualified_name * API.Ast.program * Id.t list * Rocq_elpi_utils.clause_scope let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~scope ~dbname clauses ~depth ~options state = let invocation_loc = State.get invocation_site_loc_synterp state in let loc = invocation_loc in - let dbname = Coq_elpi_utils.string_split_on_char '.' dbname in + let dbname = Rocq_elpi_utils.string_split_on_char '.' dbname in let clauses scope = clauses |> CList.rev_map (fun (name,graft,clause) -> let vars, clause = preprocess_clause ~depth clause in @@ -179,7 +179,7 @@ let accumulate_clauses ~clauses_for_later ~accumulate_to_db ~preprocess_clause ~ | B.Given Library -> if local then CErrors.user_err Pp.(str "coq.elpi.accumulate: library scope is incompatible with @local!"); State.update clauses_for_later state (fun l -> - clauses Coq_elpi_utils.Global @ l), (), [] + clauses Rocq_elpi_utils.Global @ l), (), [] | B.Given CurrentModule -> let scope = if local then Local else Regular in let f = accumulate_to_db in @@ -507,7 +507,7 @@ module SynterpAction = struct } |> CConv.(!<) let log : WZipper.zipper State.component = - State.declare_component ~name:"coq-elpi:synterp-action-write" ~descriptor:synterp_state + State.declare_component ~name:"rocq-elpi:synterp-action-write" ~descriptor:synterp_state ~pp:(fun fmt x -> Format.fprintf fmt "") ~init:(fun () -> WZipper.empty) ~start:(fun x -> x) () @@ -557,7 +557,7 @@ module SynterpAction = struct ] let read : RZipper.zipper State.component = - State.declare_component ~name:"coq-elpi:synterp-action-read" ~descriptor:interp_state + State.declare_component ~name:"rocq-elpi:synterp-action-read" ~descriptor:interp_state ~pp:(fun fmt x -> Format.fprintf fmt "") ~init:(fun () -> RZipper.empty) ~start:(fun x -> x) () @@ -606,11 +606,11 @@ module SynterpAction = struct | EndModule mp -> let mp1 = Declaremods.Interp.end_module () in assert(ModPath.equal mp mp1); - (Coq_elpi_HOAS.grab_global_env_drop_sigma state, Some mp) + (Rocq_elpi_HOAS.grab_global_env_drop_sigma state, Some mp) | EndModuleType mp -> let mp1 = Declaremods.Interp.end_modtype () in assert(ModPath.equal mp mp1); - (Coq_elpi_HOAS.grab_global_env_drop_sigma state, Some mp) + (Rocq_elpi_HOAS.grab_global_env_drop_sigma state, Some mp) | BeginSection name -> let id = Id.of_string name in let lid = CAst.make ~loc:(to_coq_loc @@ State.get invocation_site_loc state) id in @@ -622,7 +622,7 @@ module SynterpAction = struct Dumpglob.dump_reference ~loc (DirPath.to_string (Lib.current_dirpath true)) "<>" "sec"; interp_close_section (); - (Coq_elpi_HOAS.grab_global_env_drop_sigma state, None) + (Rocq_elpi_HOAS.grab_global_env_drop_sigma state, None) | ImportModule mp -> Declaremods.import_module ~export:Lib.Import Libobject.unfiltered mp; (state, None) @@ -962,7 +962,7 @@ let coq_synterp_builtins = let open Notation in let open CConv in [ - LPCode Coq_elpi_builtins_arg_HOAS.code; + LPCode Rocq_elpi_builtins_arg_HOAS.code; LPDoc "Coq terms are not visible at synterp time, they are always holes"; LPCode "kind term type."; LPDoc "-- Parsing time APIs ----------------------------------------------------"; diff --git a/src/coq_elpi_builtins_synterp.mli b/src/rocq_elpi_builtins_synterp.mli similarity index 89% rename from src/coq_elpi_builtins_synterp.mli rename to src/rocq_elpi_builtins_synterp.mli index 26aa2b94d..e585009e2 100644 --- a/src/coq_elpi_builtins_synterp.mli +++ b/src/rocq_elpi_builtins_synterp.mli @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -75,14 +75,14 @@ module SynterpAction : sig end open Elpi.API -open Coq_elpi_utils +open Rocq_elpi_utils open Names val clauses_for_later_synterp : - (qualified_name * Ast.program * Id.t list * Coq_elpi_utils.clause_scope) list State.component + (qualified_name * Ast.program * Id.t list * Rocq_elpi_utils.clause_scope) list State.component val set_accumulate_to_db_synterp : - (loc:Loc.t -> (qualified_name * Ast.program * Id.t list * Coq_elpi_utils.clause_scope) list -> unit) -> unit + (loc:Loc.t -> (qualified_name * Ast.program * Id.t list * Rocq_elpi_utils.clause_scope) list -> unit) -> unit val prop : Data.term Conversion.t val id : string Conversion.t @@ -95,7 +95,7 @@ type scope = ExecutionSite | CurrentModule | Library val scope : scope Conversion.t val grafting : ([ `After | `Before | `Remove | `Replace ] * string) Conversion.t -val options : (Coq_elpi_HOAS.options, Data.constraints) ContextualConversion.ctx_readback +val options : (Rocq_elpi_HOAS.options, Data.constraints) ContextualConversion.ctx_readback val locate_module : BuiltIn.declaration val locate_module_type : BuiltIn.declaration val current_path : BuiltIn.declaration @@ -126,7 +126,7 @@ type attribute_value = val attribute_value : attribute_value Conversion.t val attribute : (string * attribute_value) Conversion.t -type accumulation_item = qualified_name * Ast.program * Id.t list * Coq_elpi_utils.clause_scope +type accumulation_item = qualified_name * Ast.program * Id.t list * Rocq_elpi_utils.clause_scope val accumulate_clauses : clauses_for_later:accumulation_item list State.component -> @@ -136,7 +136,7 @@ val accumulate_clauses : dbname:string -> clause list -> depth:int -> - options:Coq_elpi_HOAS.options -> + options:Rocq_elpi_HOAS.options -> State.t -> State.t * unit * Conversion.extra_goals diff --git a/src/coq_elpi_glob_quotation.ml b/src/rocq_elpi_glob_quotation.ml similarity index 98% rename from src/coq_elpi_glob_quotation.ml rename to src/rocq_elpi_glob_quotation.ml index 4236beeec..6a275cde5 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/rocq_elpi_glob_quotation.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -10,10 +10,10 @@ module Q = API.Quotation module F = API.FlexibleData module A = API.Ast -open Coq_elpi_HOAS +open Rocq_elpi_HOAS open Names -open Coq_elpi_utils +open Rocq_elpi_utils (* ***************** {{ quotation }} for Glob_terms ********************** *) @@ -45,7 +45,7 @@ let empty_glob_ctx env : glob_ctx = { env; bound = Names.Id.Set.empty; bound_list = []; taken = section_ids env; section = section_ids env; hyps = [] } let glob_ctx : glob_ctx option S.component = - S.declare_component ~name:"coq-elpi:glob-environment" ~descriptor:interp_state + S.declare_component ~name:"rocq-elpi:glob-environment" ~descriptor:interp_state ~pp:(fun _ _ -> ()) ~init:(fun () -> None) ~start:(fun _ -> Some (empty_glob_ctx (Global.env ()))) () @@ -173,7 +173,7 @@ let under_glob_ctx name ~tyast ~k t state = (* Set by the parser that declares an ARGUMENT EXTEND to Coq *) let get_ctx, set_ctx, _update_ctx = let bound_vars = - S.declare_component ~name:"coq-elpi:glob-quotation-bound-vars" ~descriptor:interp_state + S.declare_component ~name:"rocq-elpi:glob-quotation-bound-vars" ~descriptor:interp_state ~init:(fun () -> None) ~pp:(fun fmt -> function Some (x,_) -> () | None -> ()) ~start:(fun x -> x) () @@ -331,7 +331,7 @@ let gterm2lpast ~pattern ~language state glob = debug Pp.(fun () -> str"gterm2lp:" ++ str " term=" ++Printer.pr_glob_constr_env (get_glob_env state).env (get_sigma state) x); let coqloc = Option.default dummy_loc loc in - let loc = Coq_elpi_utils.of_coq_loc coqloc in + let loc = Rocq_elpi_utils.of_coq_loc coqloc in match (DAst.get_thunk v) (*.CAst.v*) with | GRef(GlobRef.ConstRef p,_ul) when Structures.PrimitiveProjections.mem p -> let p = Option.get @@ Structures.PrimitiveProjections.find_opt p in @@ -579,7 +579,7 @@ let coq_quotation ~language state loc src = gterm2lpast ~language state glob let coq = Q.register_named_quotation ~name:"coq" (coq_quotation ~pattern:false) ~descriptor:interp_quotations -let () = Coq_elpi_HOAS.set_coq coq +let () = Rocq_elpi_HOAS.set_coq coq let _coqpat = Q.register_named_quotation ~name:"pat" (coq_quotation ~pattern:true) ~descriptor:interp_quotations @@ -616,7 +616,7 @@ let rec gparams2lp ~loc ~base params (kont : depth:int -> S.t -> S.t * _) ~depth match params with | [] -> kont ~depth state | (name,imp,ob,src) :: params -> - if ob <> None then Coq_elpi_utils.nYI "defined parameters in a record/inductive declaration"; + if ob <> None then Rocq_elpi_utils.nYI "defined parameters in a record/inductive declaration"; let state, src = gterm2lp ~loc ~depth ~base src state in let k = nogls (gparams2lp ~loc ~base params kont) in let state, tgt, () = under_ctx name src None ~k ~depth state in @@ -651,4 +651,4 @@ let grecord2lp ~loc ~base ~name ~constructorname arity fields ~depth state = state, in_elpi_indtdecl_record (Name.Name qrecord_name) arity constructor fields - let gterm2lpast = gterm2lpast ~language:coq \ No newline at end of file + let gterm2lpast = gterm2lpast ~language:coq diff --git a/src/coq_elpi_glob_quotation.mli b/src/rocq_elpi_glob_quotation.mli similarity index 86% rename from src/coq_elpi_glob_quotation.mli rename to src/rocq_elpi_glob_quotation.mli index f0acea2ed..0bea180a0 100644 --- a/src/coq_elpi_glob_quotation.mli +++ b/src/rocq_elpi_glob_quotation.mli @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -9,7 +9,7 @@ open RawData val coq : Ast.Scope.language (* The context used to interpret Var("x") nodes in all the APIs below *) -val set_coq_ctx_hyps : State.t -> [> `Options ] Coq_elpi_HOAS.coq_context * Coq_elpi_HOAS.hyp list -> State.t +val set_coq_ctx_hyps : State.t -> [> `Options ] Rocq_elpi_HOAS.coq_context * Rocq_elpi_HOAS.hyp list -> State.t val under_ctx : Names.Name.t -> term -> term option -> @@ -38,7 +38,7 @@ val grecord2lp : name:string list * Names.Id.t -> constructorname:Names.Id.t option -> Glob_term.glob_constr -> - (Glob_term.glob_constr * Coq_elpi_HOAS.record_field_spec) list -> + (Glob_term.glob_constr * Rocq_elpi_HOAS.record_field_spec) list -> depth:int -> State.t -> State.t * term val runtime_gterm2lp : diff --git a/src/coq_elpi_graph.ml b/src/rocq_elpi_graph.ml similarity index 100% rename from src/coq_elpi_graph.ml rename to src/rocq_elpi_graph.ml diff --git a/src/coq_elpi_graph.mli b/src/rocq_elpi_graph.mli similarity index 100% rename from src/coq_elpi_graph.mli rename to src/rocq_elpi_graph.mli diff --git a/src/coq_elpi_name_quotation.ml b/src/rocq_elpi_name_quotation.ml similarity index 96% rename from src/coq_elpi_name_quotation.ml rename to src/rocq_elpi_name_quotation.ml index f7269f4d4..7af32fb27 100644 --- a/src/coq_elpi_name_quotation.ml +++ b/src/rocq_elpi_name_quotation.ml @@ -3,8 +3,8 @@ (* ------------------------------------------------------------------------- *) module API = Elpi.API -open Coq_elpi_utils -open Coq_elpi_HOAS +open Rocq_elpi_utils +open Rocq_elpi_HOAS open Names let to_name ~loc src = diff --git a/src/coq_elpi_programs.ml b/src/rocq_elpi_programs.ml similarity index 96% rename from src/coq_elpi_programs.ml rename to src/rocq_elpi_programs.ml index 0bf4731b0..ad13697c4 100644 --- a/src/coq_elpi_programs.ml +++ b/src/rocq_elpi_programs.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -6,7 +6,7 @@ module API = Elpi.API module EC = API.Compile module EP = API.Parse -open Coq_elpi_utils +open Rocq_elpi_utils type program_name = Loc.t * qualified_name type cunit = Full of Names.KerName.t * EC.compilation_unit | Signature of EC.compilation_unit_signature @@ -168,7 +168,7 @@ type from = Initialization | User type snippet = { program : qualified_name; code :cunit list; - scope : Coq_elpi_utils.clause_scope; + scope : Rocq_elpi_utils.clause_scope; vars : Names.Id.t list; } @@ -215,7 +215,7 @@ module type Programs = sig val accumulate : qualified_name -> src list -> unit - val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit + val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Rocq_elpi_utils.clause_scope -> unit val load_command : loc:Loc.t -> string -> unit val load_tactic : loc:Loc.t -> string -> unit @@ -548,23 +548,23 @@ let get ?(fail_if_not_exists=false) p = db_name_src := SLMap.add name (append_to_db name kn p) !db_name_src in let load i ((_,kn),s as o) = if Int.equal i 1 || - (s.scope = Coq_elpi_utils.Global && is_inside_current_library kn) || - s.scope = Coq_elpi_utils.SuperGlobal then cache o in + (s.scope = Rocq_elpi_utils.Global && is_inside_current_library kn) || + s.scope = Rocq_elpi_utils.SuperGlobal then cache o in let import i (_,s as o) = if Int.equal i 1 then cache o in declare_named_object @@ { (default_object "ELPI-DB") with classify_function = (fun { scope; program; _ } -> match scope with - | Coq_elpi_utils.Local -> Dispose - | Coq_elpi_utils.Regular -> Substitute - | Coq_elpi_utils.Global -> Keep - | Coq_elpi_utils.SuperGlobal -> Keep); + | Rocq_elpi_utils.Local -> Dispose + | Rocq_elpi_utils.Regular -> Substitute + | Rocq_elpi_utils.Global -> Keep + | Rocq_elpi_utils.SuperGlobal -> Keep); load_function = load; cache_function = cache; subst_function = (fun (_,o) -> o); open_function = simple_open import; discharge_function = (fun (({ scope; program; vars; } as o)) -> - if scope = Coq_elpi_utils.Local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None + if scope = Rocq_elpi_utils.Local || (List.exists (fun x -> Lib.is_in_section (Names.GlobRef.VarRef x)) vars) then None else Some o); } @@ -636,8 +636,8 @@ let get ?(fail_if_not_exists=false) p = let base_sig, base = db_init_base ~loc in let elpi = ensure_initialized () in let unit = unit_from_string ~elpi ~base ~loc sloc s in - add_to_db qualid [base_sig;unit] [] Coq_elpi_utils.SuperGlobal - (* add_to_db qualid [base_sig] [] Coq_elpi_utils.SuperGlobal *) + add_to_db qualid [base_sig;unit] [] Rocq_elpi_utils.SuperGlobal + (* add_to_db qualid [base_sig] [] Rocq_elpi_utils.SuperGlobal *) let lp_tactic_ast = Summary.ref ~name:("elpi-lp-tactic") None let in_lp_tactic_ast : src -> Libobject.obj = @@ -728,7 +728,7 @@ let find_with_stats k t = let () = at_exit (fun () -> let { lookups; hits } = !cache_stats in - Coq_elpi_utils.debug Pp.(fun () -> + Rocq_elpi_utils.debug Pp.(fun () -> str(Format.asprintf "Compiler cache: lookups=%d, hits=%d\n" lookups hits)) ) @@ -813,7 +813,7 @@ let get_and_compile ~loc ?even_if_empty name : (EC.program * bool) option = | Program { raw_args } -> raw_args | Tactic -> true in (prog, raw_args)) in - Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t)))); + Rocq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t)))); res let rec compile_db ~loc src = @@ -859,10 +859,10 @@ let coq_interp_builtins = API.BuiltIn.declare ~file_name:"coq-builtin.elpi" begin - Coq_elpi_builtins.coq_header_builtins @ - Coq_elpi_builtins.coq_misc_builtins @ - Coq_elpi_builtins.coq_locate_builtins @ - Coq_elpi_builtins.coq_rest_builtins + Rocq_elpi_builtins.coq_header_builtins @ + Rocq_elpi_builtins.coq_misc_builtins @ + Rocq_elpi_builtins.coq_locate_builtins @ + Rocq_elpi_builtins.coq_rest_builtins end let coq_synterp_builtins = @@ -878,8 +878,8 @@ kind upoly-decl-cumul type. |} ] @ - Coq_elpi_builtins.coq_misc_builtins @ - Coq_elpi_builtins_synterp.coq_synterp_builtins + Rocq_elpi_builtins.coq_misc_builtins @ + Rocq_elpi_builtins_synterp.coq_synterp_builtins end let resolve_file_path ~must_exist ~allow_absolute ~only_elpi file = @@ -978,7 +978,7 @@ module Synterp : Programs = struct end include SourcesStorage(S) - let () = Coq_elpi_builtins_synterp.set_accumulate_to_db_synterp (fun ~loc clauses_to_add -> + let () = Rocq_elpi_builtins_synterp.set_accumulate_to_db_synterp (fun ~loc clauses_to_add -> let elpi = ensure_initialized () in let clauses_to_add = clauses_to_add |> group_clauses |> List.map (fun (dbname,asts,vs,scope) -> @@ -1000,7 +1000,7 @@ module Interp : Programs = struct ~quotations:interp_quotations ~builtins:[elpi_builtins;coq_interp_builtins] ~file_resolver () end) -let () = Coq_elpi_builtins.set_accumulate_to_db_interp (fun ~loc clauses_to_add -> +let () = Rocq_elpi_builtins.set_accumulate_to_db_interp (fun ~loc clauses_to_add -> let elpi = ensure_initialized () in let clauses_to_add = clauses_to_add |> group_clauses |> List.map (fun (dbname,asts,vs,scope) -> @@ -1010,7 +1010,7 @@ let () = Coq_elpi_builtins.set_accumulate_to_db_interp (fun ~loc clauses_to_add clauses_to_add |> List.iter (fun (dbname,units,vs,scope) -> accumulate_to_db dbname units vs ~scope)) -let () = Coq_elpi_builtins.set_accumulate_text_to_db_interp (fun ~loc n txt scope -> +let () = Rocq_elpi_builtins.set_accumulate_text_to_db_interp (fun ~loc n txt scope -> let elpi = ensure_initialized () in let base = get_and_compile_existing_db ~loc n in let u = unit_from_string ~elpi ~base ~loc (of_coq_loc loc) txt in diff --git a/src/coq_elpi_programs.mli b/src/rocq_elpi_programs.mli similarity index 98% rename from src/coq_elpi_programs.mli rename to src/rocq_elpi_programs.mli index 59c3dd863..cc3fcc1b3 100644 --- a/src/coq_elpi_programs.mli +++ b/src/rocq_elpi_programs.mli @@ -3,7 +3,7 @@ (* ------------------------------------------------------------------------- *) open Elpi.API -open Coq_elpi_utils +open Rocq_elpi_utils type cunit = Full of Names.KerName.t * Compile.compilation_unit | Signature of Compile.compilation_unit_signature type program_name = Loc.t * qualified_name @@ -103,7 +103,7 @@ module type Programs = sig val ast_of_file : qualified_name -> Digest.t * Compile.scoped_program val accumulate : qualified_name -> src list -> unit - val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Coq_elpi_utils.clause_scope -> unit + val accumulate_to_db : qualified_name -> cunit list -> Names.Id.t list -> scope:Rocq_elpi_utils.clause_scope -> unit val load_command : loc:Loc.t -> string -> unit val load_tactic : loc:Loc.t -> string -> unit diff --git a/src/coq_elpi_utils.ml b/src/rocq_elpi_utils.ml similarity index 99% rename from src/coq_elpi_utils.ml rename to src/rocq_elpi_utils.ml index c0e3d1458..611ddde79 100644 --- a/src/coq_elpi_utils.ml +++ b/src/rocq_elpi_utils.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) diff --git a/src/coq_elpi_utils.mli b/src/rocq_elpi_utils.mli similarity index 98% rename from src/coq_elpi_utils.mli rename to src/rocq_elpi_utils.mli index f9228548a..af07dadb0 100644 --- a/src/coq_elpi_utils.mli +++ b/src/rocq_elpi_utils.mli @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) diff --git a/src/coq_elpi_vernacular.ml b/src/rocq_elpi_vernacular.ml similarity index 86% rename from src/coq_elpi_vernacular.ml rename to src/rocq_elpi_vernacular.ml index 3db446852..424cc6f98 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/rocq_elpi_vernacular.ml @@ -1,4 +1,4 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) @@ -8,9 +8,9 @@ module EPP = API.Pp module EU = API.Utils module ET = API.RawData -open Coq_elpi_utils -open Coq_elpi_arg_HOAS -module Programs = Coq_elpi_programs +open Rocq_elpi_utils +open Rocq_elpi_arg_HOAS +module Programs = Rocq_elpi_programs (* ******************** Vernacular commands ******************************* *) @@ -26,7 +26,7 @@ let attributesc = ET.Constants.declare_global_symbol "attributes" let atts2impl ~depth loc phase state atts q = - let open Coq_elpi_builtins_synterp in + let open Rocq_elpi_builtins_synterp in let rec convert_att_r = function | (name,Attributes.VernacFlagEmpty) -> name, AttributeEmpty | (name,Attributes.VernacFlagList l) -> name, AttributeList (convert_atts l) @@ -52,7 +52,7 @@ let atts2impl ~depth loc phase | Some { Vernacexpr.attrs ; _ } -> List.map (fun {CAst.v=(name,v)} -> convert_att_r ("elpi."^name,v)) attrs @ atts | exception Gramlib.Grammar.Error msg -> CErrors.user_err Pp.(str"Environment variable COQ_ELPI_ATTRIBUTES contains ill formed value:" ++ spc () ++ str txt ++ cut () ++ str msg) in - let state, atts, _ = EU.map_acc (Coq_elpi_builtins_synterp.attribute.API.Conversion.embed ~depth) state atts in + let state, atts, _ = EU.map_acc (Rocq_elpi_builtins_synterp.attribute.API.Conversion.embed ~depth) state atts in let atts = ET.mkApp attributesc (EU.list_to_lp_list atts) [] in state, ET.mkApp ET.Constants.implc atts [q] @@ -138,8 +138,8 @@ let run ~loc program query = let t5 = Unix.gettimeofday () in let txt = Printf.sprintf "Elpi: query-compilation:%1.4f static-check:%1.4f optimization:%1.4f runtime:%1.4f %s\n" (t2 -. t1) (t3 -. t2) (t4 -. t3) (t5 -. t4) (if with_error then "(with error)" else "(with success)") in - Coq_elpi_utils.debug Pp.(fun () -> str txt); - Coq_elpi_utils.elpitime Pp.(fun () -> str txt) + Rocq_elpi_utils.debug Pp.(fun () -> str txt); + Rocq_elpi_utils.elpitime Pp.(fun () -> str txt) in try let rc = API.Execute.once ~max_steps:!max_steps exe in @@ -161,8 +161,8 @@ let elpi_fails program_name = "Please report this inconvenience to the authors of the program." ])) -let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper = - let open API.Data in let open Coq_elpi_utils in +let run_and_print ~print ~loc program_name program_ast query_ast : _ * Rocq_elpi_builtins_synterp.SynterpAction.RZipper.zipper = + let open API.Data in let open Rocq_elpi_utils in match run ~loc program_ast query_ast with | API.Execute.Failure -> elpi_fails program_name @@ -185,7 +185,7 @@ let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_ if scst <> "" then Feedback.msg_notice Pp.(str"Syntactic constraints:" ++ spc()++str scst); if P.stage = Summary.Stage.Interp then begin - let sigma = Coq_elpi_HOAS.get_sigma state in + let sigma = Rocq_elpi_HOAS.get_sigma state in let ccst = Evd.evar_universe_context sigma in if not (UState.is_empty ccst) then Feedback.msg_notice Pp.(str"Universe constraints:" ++ spc() ++ @@ -196,8 +196,8 @@ let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_ let clauses_to_add = API.State.get (match P.stage with - | Summary.Stage.Synterp -> Coq_elpi_builtins_synterp.clauses_for_later_synterp - | Summary.Stage.Interp -> Coq_elpi_builtins.clauses_for_later_interp) + | Summary.Stage.Synterp -> Rocq_elpi_builtins_synterp.clauses_for_later_synterp + | Summary.Stage.Interp -> Rocq_elpi_builtins.clauses_for_later_interp) state in (* TODO: this code is duplicate, see set_accumulate_to_db_* *) @@ -212,8 +212,8 @@ let run_and_print ~print ~loc program_name program_ast query_ast : _ * Coq_elpi_ P.accumulate_to_db dbname units vs ~scope); relocate_assignment_to_runtime, if P.stage = Summary.Stage.Synterp then - API.State.get Coq_elpi_builtins_synterp.SynterpAction.log state |> Coq_elpi_builtins_synterp.SynterpAction.RZipper.of_w - else API.State.get Coq_elpi_builtins_synterp.SynterpAction.read state + API.State.get Rocq_elpi_builtins_synterp.SynterpAction.log state |> Rocq_elpi_builtins_synterp.SynterpAction.RZipper.of_w + else API.State.get Rocq_elpi_builtins_synterp.SynterpAction.read state let current_program = Summary.ref ~name:"elpi-cur-program-name" None let set_current_program n = @@ -374,7 +374,7 @@ let run_in_program ~loc ?(program = current_program ()) ?(st_setup=fun _ x -> x) Option.map fst @@ P.get_and_compile ~loc name in program |> Option.iter @@ fun program -> let fname = - Coq_elpi_programs.resolve_file_path + Rocq_elpi_programs.resolve_file_path ~must_exist:false ~allow_absolute:false ~only_elpi:false output in let fname_txt = fname ^ ".txt" in @@ -470,7 +470,7 @@ module type Common = sig end module Synterp = struct - include Compiler(Coq_elpi_programs.Synterp) + include Compiler(Rocq_elpi_programs.Synterp) let main_syterp args syndata = ET.mkApp API.RawData.Constants.orc @@ -481,24 +481,24 @@ module Synterp = struct get_and_compile ~loc name |> Option.map (fun (program, raw_args) -> let initial_synterp_state = Vernacstate.Synterp.freeze () in let query state = - let loc = Coq_elpi_utils.of_coq_loc loc in + let loc = Rocq_elpi_utils.of_coq_loc loc in let depth = 0 in let state, args, gls = EU.map_acc - (Coq_elpi_arg_HOAS.in_elpi_cmd_synterp ~depth) + (Rocq_elpi_arg_HOAS.in_elpi_cmd_synterp ~depth) state args in let state, ek = API.FlexibleData.Elpi.make ~name:"NewData" state in let data = ET.mkUnifVar ek ~args:[] state in let state, q = atts2impl loc Summary.Stage.Synterp ~depth state atts (main_syterp args data) in - let state = API.State.set Coq_elpi_builtins_synterp.invocation_site_loc_synterp state loc in + let state = API.State.set Rocq_elpi_builtins_synterp.invocation_site_loc_synterp state loc in state, q, gls in try let relocate, synterplog = run_and_print ~loc ~print:false name program (Fun query) in initial_synterp_state, relocate "NewData", synterplog - with Coq_elpi_builtins_synterp.SynterpAction.Error x -> err x) + with Rocq_elpi_builtins_synterp.SynterpAction.Error x -> err x) let run_in_program ~loc ?program query = try run_in_program ~loc ?program query |> Option.map (fun (_,x) -> x) - with Coq_elpi_builtins_synterp.SynterpAction.Error x -> err x + with Rocq_elpi_builtins_synterp.SynterpAction.Error x -> err x end @@ -506,7 +506,7 @@ let document_builtins = document_builtins module Interp = struct - include Compiler(Coq_elpi_programs.Interp) + include Compiler(Rocq_elpi_programs.Interp) let main_interp args syndata = ET.mkApp API.RawData.Constants.orc @@ -522,50 +522,50 @@ module Interp = struct let env = Global.env () in let sigma = Evd.from_env env in let args = args - |> List.map (Coq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign ~strict:true env)) - |> List.map (Coq_elpi_arg_HOAS.Cmd.interp (Ltac_plugin.Tacinterp.default_ist ()) env sigma) + |> List.map (Rocq_elpi_arg_HOAS.Cmd.glob (Genintern.empty_glob_sign ~strict:true env)) + |> List.map (Rocq_elpi_arg_HOAS.Cmd.interp (Ltac_plugin.Tacinterp.default_ist ()) env sigma) in let initial_synterp_state, synterplog, synterm = match syndata with | None -> let initial_synterp_state = Vernacstate.Synterp.freeze () in initial_synterp_state, - Coq_elpi_builtins_synterp.SynterpAction.RZipper.empty, + Rocq_elpi_builtins_synterp.SynterpAction.RZipper.empty, fun ~target:_ ~depth -> Stdlib.Result.Ok ET.mkDiscard | Some (initial_synterp_state,relocate_term,log) -> initial_synterp_state, log, relocate_term in let query state = let depth = 0 in let state, args, gls = EU.map_acc - (Coq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args Coq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state)) + (Rocq_elpi_arg_HOAS.in_elpi_cmd ~loc ~depth ~base:program ~raw:raw_args Rocq_elpi_HOAS.(mk_coq_context ~options:(default_options ()) state)) state args in - let loc = Coq_elpi_utils.of_coq_loc loc in + let loc = Rocq_elpi_utils.of_coq_loc loc in let synterm = match synterm ~target:program ~depth with | Stdlib.Result.Ok x -> x | Stdlib.Result.Error s -> err Pp.(str"Data returned by the synterp phase cannot be passed to the interp phase due to unknown symbol: " ++ str s) in let state, q = atts2impl loc Summary.Stage.Interp ~depth state atts (main_interp args synterm) in - let state = API.State.set Coq_elpi_builtins.base state (Some program) in - let state = API.State.set Coq_elpi_builtins.tactic_mode state false in - let state = API.State.set Coq_elpi_builtins_synterp.invocation_site_loc state loc in - let state = API.State.set Coq_elpi_builtins_synterp.SynterpAction.read state synterplog in + let state = API.State.set Rocq_elpi_builtins.base state (Some program) in + let state = API.State.set Rocq_elpi_builtins.tactic_mode state false in + let state = API.State.set Rocq_elpi_builtins_synterp.invocation_site_loc state loc in + let state = API.State.set Rocq_elpi_builtins_synterp.SynterpAction.read state synterplog in state, q, gls in let final_synterp_state = Vernacstate.Synterp.freeze () in Vernacstate.Synterp.unfreeze initial_synterp_state; try begin try let _, synterp_left = run_and_print ~loc ~print:false name program (Fun query) in - match Coq_elpi_builtins_synterp.SynterpAction.RZipper.is_empty synterp_left with + match Rocq_elpi_builtins_synterp.SynterpAction.RZipper.is_empty synterp_left with | `Empty -> Vernacstate.Synterp.unfreeze final_synterp_state | `Group g -> - let g = Coq_elpi_builtins_synterp.SynterpAction.Tree.group_name g in + let g = Rocq_elpi_builtins_synterp.SynterpAction.Tree.group_name g in err Pp.(strbrk"The execution phase did not consume all the parse time actions. Next in the queue is group " ++ str g) | `Action a -> - err Pp.(strbrk"The execution phase did not consume all the parse time actions. Next in the queue is action " ++ Coq_elpi_builtins_synterp.SynterpAction.pp a) + err Pp.(strbrk"The execution phase did not consume all the parse time actions. Next in the queue is action " ++ Rocq_elpi_builtins_synterp.SynterpAction.pp a) with - | Coq_elpi_builtins_synterp.SynterpAction.Error x when syndata = None -> + | Rocq_elpi_builtins_synterp.SynterpAction.Error x when syndata = None -> err Pp.(x ++ missing_synterp) - | Coq_elpi_builtins_synterp.SynterpAction.Error x -> + | Rocq_elpi_builtins_synterp.SynterpAction.Error x -> err x end with e -> let e = Exninfo.capture e in @@ -577,13 +577,13 @@ module Interp = struct let run_in_program ~loc ?program ~syndata query = let st_setup base state = - let syndata = Option.default (Coq_elpi_builtins_synterp.SynterpAction.RZipper.empty) syndata in - let state = API.State.set Coq_elpi_builtins.base state (Some base) in - API.State.set Coq_elpi_builtins_synterp.SynterpAction.read state syndata in + let syndata = Option.default (Rocq_elpi_builtins_synterp.SynterpAction.RZipper.empty) syndata in + let state = API.State.set Rocq_elpi_builtins.base state (Some base) in + API.State.set Rocq_elpi_builtins_synterp.SynterpAction.read state syndata in try ignore @@ run_in_program ~loc ?program ~st_setup query with - | Coq_elpi_builtins_synterp.SynterpAction.Error x when syndata = None -> err Pp.(x ++ missing_synterp) - | Coq_elpi_builtins_synterp.SynterpAction.Error x -> err x + | Rocq_elpi_builtins_synterp.SynterpAction.Error x when syndata = None -> err Pp.(x ++ missing_synterp) + | Rocq_elpi_builtins_synterp.SynterpAction.Error x -> err x end @@ -602,28 +602,28 @@ let run_tactic_common ~loc program ~main ?(atts=[]) () = let depth = 0 in let state, main_query, gls = main ~base sigma gls state in let state, main_query = atts2impl ~depth loc Summary.Stage.Interp state atts main_query in - let state = API.State.set Coq_elpi_builtins.tactic_mode state true in - let state = API.State.set Coq_elpi_builtins_synterp.invocation_site_loc state loc in + let state = API.State.set Rocq_elpi_builtins.tactic_mode state true in + let state = API.State.set Rocq_elpi_builtins_synterp.invocation_site_loc state loc in state, main_query, gls in get_and_compile ~loc program |> Option.cata (fun (cprogram, _) -> match run ~loc cprogram (Fun (query ~base:cprogram)) with - | API.Execute.Success solution -> Coq_elpi_HOAS.tclSOLUTION2EVD ~eta_contract_solution:false sigma solution + | API.Execute.Success solution -> Rocq_elpi_HOAS.tclSOLUTION2EVD ~eta_contract_solution:false sigma solution | API.Execute.NoMoreSteps -> CErrors.user_err Pp.(str "elpi run out of steps") | API.Execute.Failure -> elpi_fails program - | exception (Coq_elpi_utils.LtacFail (level, msg)) -> tclFAILn level msg + | exception (Rocq_elpi_utils.LtacFail (level, msg)) -> tclFAILn level msg | exception (CErrors.UserError _ as e) -> let e = Exninfo.capture e in Exninfo.iraise e | exception e when CErrors.noncritical e -> let e = Exninfo.capture e in (Feedback.msg_debug Pp.(str "elpi lets escape exception: " ++ CErrors.iprint e); Exninfo.iraise e)) tclIDTAC let run_tactic ~loc program ~atts _ist args = run_tactic_common ~loc program ~atts ~main:(fun ~base sigma gls state -> - Coq_elpi_HOAS.solvegoals2query sigma gls (Coq_elpi_utils.of_coq_loc loc) ~main:args ~base - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.(in_elpi_tac ~loc) ~depth:0 state) () + Rocq_elpi_HOAS.solvegoals2query sigma gls (Rocq_elpi_utils.of_coq_loc loc) ~main:args ~base + ~in_elpi_tac_arg:Rocq_elpi_arg_HOAS.(in_elpi_tac ~loc) ~depth:0 state) () let run_in_tactic ~loc ?(program = Interp.current_program ()) (qloc,query) _ist = run_tactic_common ~loc program ~main:(fun ~base sigma gls state -> - Coq_elpi_HOAS.txtgoals2query sigma gls qloc ~main:query ~base ~depth:0 state) + Rocq_elpi_HOAS.txtgoals2query sigma gls qloc ~main:query ~base ~depth:0 state) () let loc_merge l1 l2 = @@ -635,7 +635,7 @@ let cache_program (nature,p,q) = match nature with | Command _ -> let command = Vernacexpr.{ - ext_plugin = "coq-elpi.elpi"; + ext_plugin = "rocq-elpi.elpi"; ext_entry = "Elpi" ^ p_str; ext_index = 0; } in @@ -649,14 +649,14 @@ let cache_program (nature,p,q) = (Vernacextend.TyNonTerminal (Extend.TUentry - (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + (Genarg.get_arg_tag Rocq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyTerminal (p_str, Vernacextend.TyNonTerminal (Extend.TUlist0 - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_cmd_arg)) + (Extend.TUentry (Genarg.get_arg_tag Rocq_elpi_arg_syntax.wit_elpi_cmd_arg)) ,Vernacextend.TyNonTerminal - (Extend.TUentry (Genarg.get_arg_tag Coq_elpi_arg_syntax.wit_elpi_loc), + (Extend.TUentry (Genarg.get_arg_tag Rocq_elpi_arg_syntax.wit_elpi_loc), Vernacextend.TyNil))))) (fun loc0 args loc1 ?loc ~atts () -> @@ -668,7 +668,7 @@ let cache_program (nature,p,q) = Egramml.extend_vernac_command_grammar ~undoable:true ext | Tactic -> - Coq_elpi_builtins.cache_tac_abbrev ~code:p ~name:q + Rocq_elpi_builtins.cache_tac_abbrev ~code:p ~name:q | Program _ -> CErrors.user_err Pp.(str "elpi: Only commands and tactics can be exported") @@ -688,6 +688,6 @@ let export_command ?as_ p = match as_ with | None -> p | Some x -> x in - let nature = Coq_elpi_programs.Synterp.get_nature p in + let nature = Rocq_elpi_programs.Synterp.get_nature p in Lib.add_leaf (in_exported_program (nature,p,q)) diff --git a/src/coq_elpi_vernacular.mli b/src/rocq_elpi_vernacular.mli similarity index 87% rename from src/coq_elpi_vernacular.mli rename to src/rocq_elpi_vernacular.mli index 3de53f3f0..013d14091 100644 --- a/src/coq_elpi_vernacular.mli +++ b/src/rocq_elpi_vernacular.mli @@ -1,10 +1,10 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -open Coq_elpi_utils -open Coq_elpi_programs -open Coq_elpi_arg_HOAS +open Rocq_elpi_utils +open Rocq_elpi_programs +open Rocq_elpi_arg_HOAS val atts2impl : depth:int -> Elpi.API.Ast.Loc.t -> Summary.Stage.t -> Elpi.API.State.t -> Attributes.vernac_flags -> @@ -51,13 +51,13 @@ module type Common = sig end module Synterp : sig include Common -val run_program : loc:Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Cmd.raw list -> (Vernacstate.Synterp.t * (target:Elpi.API.Compile.program -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option -val run_in_program : loc:Loc.t -> ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option +val run_program : loc:Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> Cmd.raw list -> (Vernacstate.Synterp.t * (target:Elpi.API.Compile.program -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Rocq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option +val run_in_program : loc:Loc.t -> ?program:qualified_name -> Elpi.API.Ast.Loc.t * string -> Rocq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option end module Interp : sig include Common -val run_program : loc:Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> syndata:(Vernacstate.Synterp.t * (target:Elpi.API.Compile.program -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option -> Cmd.raw list -> unit -val run_in_program : loc:Loc.t -> ?program:qualified_name -> syndata:Coq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option -> Elpi.API.Ast.Loc.t * string -> unit +val run_program : loc:Loc.t -> qualified_name -> atts:Attributes.vernac_flags -> syndata:(Vernacstate.Synterp.t * (target:Elpi.API.Compile.program -> depth:int -> (Elpi.API.Data.term,string) Stdlib.Result.t) * Rocq_elpi_builtins_synterp.SynterpAction.RZipper.zipper) option -> Cmd.raw list -> unit +val run_in_program : loc:Loc.t -> ?program:qualified_name -> syndata:Rocq_elpi_builtins_synterp.SynterpAction.RZipper.zipper option -> Elpi.API.Ast.Loc.t * string -> unit end val document_builtins : unit -> unit diff --git a/src/coq_elpi_vernacular_syntax.mlg b/src/rocq_elpi_vernacular_syntax.mlg similarity index 96% rename from src/coq_elpi_vernacular_syntax.mlg rename to src/rocq_elpi_vernacular_syntax.mlg index c0853b4c7..742bc47ac 100644 --- a/src/coq_elpi_vernacular_syntax.mlg +++ b/src/rocq_elpi_vernacular_syntax.mlg @@ -1,8 +1,8 @@ -(* coq-elpi: Coq terms as the object language of elpi *) +(* rocq-elpi: Coq terms as the object language of elpi *) (* license: GNU Lesser General Public License Version 2.1 or later *) (* ------------------------------------------------------------------------- *) -DECLARE PLUGIN "coq-elpi.elpi" +DECLARE PLUGIN "rocq-elpi.elpi" { @@ -11,10 +11,10 @@ open Ltac_plugin open Pcoq.Constr -open Coq_elpi_arg_syntax -module EV = Coq_elpi_vernacular -module EA = Coq_elpi_arg_HOAS -module U = Coq_elpi_utils +open Rocq_elpi_arg_syntax +module EV = Rocq_elpi_vernacular +module EA = Rocq_elpi_arg_HOAS +module U = Rocq_elpi_utils } @@ -28,9 +28,9 @@ ARGUMENT EXTEND elpi_code PRINTED BY { pr_elpi_code } END { -let () = Coq_elpi_glob_quotation.is_elpi_code := +let () = Rocq_elpi_glob_quotation.is_elpi_code := (fun x -> Genarg.(has_type x (glbwit wit_elpi_code))) -let () = Coq_elpi_glob_quotation.get_elpi_code := +let () = Rocq_elpi_glob_quotation.get_elpi_code := (fun x -> Genarg.(out_gen (glbwit wit_elpi_code) x)) let pr_elpi_code_appArg _ _ _ (s : Elpi.API.Ast.Loc.t * string list) = Pp.prlist Pp.str (snd s) @@ -47,9 +47,9 @@ ARGUMENT EXTEND elpi_code_appArg END { -let () = Coq_elpi_glob_quotation.is_elpi_code_appArg := +let () = Rocq_elpi_glob_quotation.is_elpi_code_appArg := (fun x -> Genarg.(has_type x (glbwit wit_elpi_code_appArg ))) -let () = Coq_elpi_glob_quotation.get_elpi_code_appArg := +let () = Rocq_elpi_glob_quotation.get_elpi_code_appArg := (fun x -> Genarg.(out_gen (glbwit wit_elpi_code_appArg ) x)) let rec inlogpath q = function @@ -57,11 +57,11 @@ let rec inlogpath q = function | x :: xs -> (Libnames.string_of_qualid q ^ "/" ^ x) :: inlogpath q xs let warning_legacy_typecheck = - CWarnings.create ~name:"elpi.typecheck-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun () -> + CWarnings.create ~name:"elpi.typecheck-syntax" ~category:Rocq_elpi_utils.elpi_depr_cat (fun () -> Pp.strbrk "The command 'Elpi Typecheck' is deprecated (and does nothing) since type checking is now performed by 'Elpi Accumulate'.") let warning_legacy_accumulate_gen = - CWarnings.create ~default:CWarnings.AsError ~name:"elpi.accumulate-syntax" ~category:Coq_elpi_utils.elpi_depr_cat (fun has_from -> + CWarnings.create ~default:CWarnings.AsError ~name:"elpi.accumulate-syntax" ~category:Rocq_elpi_utils.elpi_depr_cat (fun has_from -> if has_from then Pp.strbrk "The syntax 'Elpi Accumulate File \"path\"' is deprecated, use 'Elpi Accumulate File \"path\" From logpath'" else Pp.strbrk "The syntax 'Elpi Accumulate File \"path\" From logpath' is deprecated, use 'From logpath Extra Dependency \"path\" as name. Elpi Accumulate File name.'") @@ -91,7 +91,7 @@ GRAMMAR EXTEND Gram then Genarg.in_gen (Genarg.rawwit wit_elpi_code_appArg) (idents_of loc s) else if s.[0] = '\123' then Genarg.in_gen (Genarg.rawwit wit_elpi_code) (strip_curly loc s) - else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Coq_elpi_utils.of_coq_loc loc,s) in + else Genarg.in_gen (Genarg.rawwit wit_elpi_code) (Rocq_elpi_utils.of_coq_loc loc,s) in CAst.make ~loc (Constrexpr.CGenarg arg) } ] ] diff --git a/tests-stdlib/dune b/tests-stdlib/dune index 3793ba99d..aa422179f 100644 --- a/tests-stdlib/dune +++ b/tests-stdlib/dune @@ -1,7 +1,7 @@ (coq.theory - (package coq-elpi-tests-stdlib) + (package rocq-elpi-tests-stdlib) (name elpi_tests_stdlib) - (plugins coq-elpi.elpi) + (plugins rocq-elpi.elpi) (theories elpi elpi_stdlib)) ; (include_subdirs qualified) diff --git a/tests-stdlib/test_open_terms.v b/tests-stdlib/test_open_terms.v index 3600951e1..ef975f385 100644 --- a/tests-stdlib/test_open_terms.v +++ b/tests-stdlib/test_open_terms.v @@ -120,7 +120,7 @@ pred instantiate i:name, i:term, i:term, i:argument, o:argument. pred remove_one_unknown i:name, i:term, i:term, i:term, o:term. -% TODO : needs a fix in a coq-elpi to detect if renaming has happened in +% TODO : needs a fix in a rocq-elpi to detect if renaming has happened in % in the current context. remove_one_unknown N _T C (fun N1 _T1 F) Res :- {coq.name->id N} = {coq.name->id N1},!, diff --git a/tests/dune b/tests/dune index 7c9f90aac..3b824fa10 100644 --- a/tests/dune +++ b/tests/dune @@ -1,6 +1,6 @@ (coq.theory (name elpi.tests) - (plugins coq-elpi.elpi) + (plugins rocq-elpi.elpi) (theories elpi)) (include_subdirs qualified) diff --git a/tests/test_API.v b/tests/test_API.v index fea48ee13..c96febb70 100644 --- a/tests/test_API.v +++ b/tests/test_API.v @@ -13,7 +13,7 @@ Elpi Query lp:{{ Elpi Command version. Elpi Accumulate lp:{{ -% elpi:if version coq-elpi < 2.0.0 +% elpi:if version rocq-elpi < 2.0.0 main _ :- coq.error "bad". % elpi:endif diff --git a/theories-stdlib/Program/dune b/theories-stdlib/Program/dune index 5d2f6304e..651703434 100644 --- a/theories-stdlib/Program/dune +++ b/theories-stdlib/Program/dune @@ -4,7 +4,7 @@ (glob_files Basics.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Syntax.v) @@ -12,4 +12,4 @@ (glob_files Syntax.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) \ No newline at end of file + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) \ No newline at end of file diff --git a/theories-stdlib/dune.in b/theories-stdlib/dune.in index e9406839c..0c71157c2 100644 --- a/theories-stdlib/dune.in +++ b/theories-stdlib/dune.in @@ -1,7 +1,7 @@ (coq.theory (name elpi_stdlib) - (plugins coq-elpi.elpi) - (package coq-elpi-tests-stdlib) + (plugins rocq-elpi.elpi) + (package rocq-elpi-tests-stdlib) (theories elpi_elpi elpi @@STDLIB@@)) (rule @@ -10,7 +10,7 @@ (glob_files Bool.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Vector.v) @@ -18,7 +18,7 @@ (glob_files Vector.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Arith.v) @@ -26,7 +26,7 @@ (glob_files Arith.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target ZArith.v) @@ -34,7 +34,7 @@ (glob_files ZArith.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target FunctionalExtensionality.v) @@ -42,7 +42,7 @@ (glob_files FunctionalExtensionality.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target List.v) @@ -50,7 +50,7 @@ (glob_files List.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Ranalysis5.v) @@ -58,7 +58,7 @@ (glob_files Ranalysis5.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Utf8.v) @@ -66,7 +66,7 @@ (glob_files Utf8.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Peano.v) @@ -74,7 +74,7 @@ (glob_files Peano.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Permutation.v) @@ -82,6 +82,6 @@ (glob_files Permutation.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (include_subdirs qualified) \ No newline at end of file diff --git a/theories/core/dune b/theories/core/dune index 7f82b0a5e..2f8ad19b4 100644 --- a/theories/core/dune +++ b/theories/core/dune @@ -7,7 +7,7 @@ (glob_files Bool.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target ListDef.v) @@ -15,7 +15,7 @@ (glob_files ListDef.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Morphisms.v) @@ -23,7 +23,7 @@ (glob_files Morphisms.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target PosDef.v) @@ -31,7 +31,7 @@ (glob_files PosDef.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target PrimInt63.v) @@ -39,7 +39,7 @@ (glob_files PrimInt63.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target PrimFloat.v) @@ -47,7 +47,7 @@ (glob_files PrimFloat.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target RelationClasses.v) @@ -55,7 +55,7 @@ (glob_files RelationClasses.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Setoid.v) @@ -63,7 +63,7 @@ (glob_files Setoid.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target Uint63Axioms.v) @@ -71,7 +71,7 @@ (glob_files Uint63Axioms.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target ssreflect.v) @@ -79,7 +79,7 @@ (glob_files ssreflect.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target ssrfun.v) @@ -87,7 +87,7 @@ (glob_files ssrfun.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (rule (target ssrbool.v) @@ -95,4 +95,4 @@ (glob_files ssrbool.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) diff --git a/theories/dune b/theories/dune index d72cbd288..7a1e22cfe 100644 --- a/theories/dune +++ b/theories/dune @@ -1,7 +1,7 @@ (coq.theory (name elpi) - (package coq-elpi) - (plugins coq-elpi.elpi) + (package rocq-elpi) + (plugins rocq-elpi.elpi) (theories elpi_elpi)) (rule @@ -10,6 +10,6 @@ (glob_files elpi.v.in)) (action (with-stdout-to %{target} - (run coq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) + (run rocq_elpi_optcomp "%{coq:version.major}.%{coq:version.minor}" %{deps})))) (include_subdirs qualified) diff --git a/theories/elpi.v.in b/theories/elpi.v.in index cb3bef5d1..ece31feff 100644 --- a/theories/elpi.v.in +++ b/theories/elpi.v.in @@ -1,6 +1,6 @@ (*From Coq Require Ltac.*) From elpi_elpi Require Import dummy. -Declare ML Module "coq-elpi.elpi". +Declare ML Module "rocq-elpi.elpi". (* Generate coq-bultins.elpi *) Elpi Document Builtins. From 27b5c88f2a5b97d6026ae42474db391fdf344bd0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 11 Feb 2025 16:27:22 +0100 Subject: [PATCH 3/3] Update release.yml --- .github/workflows/release.yml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index d237c44bc..bc45a4d6a 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -41,16 +41,16 @@ jobs: - name: Create archive run: | VERSION="${GITHUB_REF_NAME_SLUG#v}" - git archive -o coq-elpi-$VERSION.tar.gz --prefix=coq-elpi-$VERSION/ $GITHUB_SHA . + git archive -o rocq-elpi-$VERSION.tar.gz --prefix=rocq-elpi-$VERSION/ $GITHUB_SHA . - name: Release uses: softprops/action-gh-release@v1 with: - files: coq-elpi-*.tar.gz + files: rocq-elpi-*.tar.gz fail_on_unmatched_files: true prerelease: true generate_release_notes: true - name: Coq-Elpi ${{ github.ref }} for Coq XXX + name: Rocq-Elpi ${{ github.ref }} for Rocq XXX opam: runs-on: ubuntu-latest @@ -68,6 +68,7 @@ jobs: ocaml-compiler: 4.14.x opam-local-packages: | !coq-elpi.opam + !rocq-elpi.opam - name: Write PAT env: @@ -93,4 +94,4 @@ jobs: git tag TAG=`git tag --sort=-v:refname|head -1` echo selected tag: $TAG - opam-publish --no-confirmation --tag=$TAG --packages-directory=${OPAM_SUITE:-released}/packages --repo=coq/opam --no-browser -v ${TAG##v} coq-elpi.opam https://github.com/LPCIC/coq-elpi/releases/download/$TAG/coq-elpi-${TAG##v}.tar.gz + opam-publish --no-confirmation --tag=$TAG --packages-directory=${OPAM_SUITE:-released}/packages --repo=coq/opam --no-browser -v ${TAG##v} rocq-elpi.opam coq-elpi.opam https://github.com/LPCIC/coq-elpi/releases/download/$TAG/rocq-elpi-${TAG##v}.tar.gz