diff --git a/.github/workflows/doc.yml b/.github/workflows/doc.yml index fdc51f7f8..958a3fd30 100644 --- a/.github/workflows/doc.yml +++ b/.github/workflows/doc.yml @@ -25,7 +25,7 @@ jobs: - name: setup ocaml uses: avsm/setup-ocaml@v1 with: - ocaml-version: 4.10.1 + ocaml-version: 4.14.2 - name: install deps run: | @@ -34,7 +34,7 @@ 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 ./coq-elpi.opam coq-core.8.19.1 + opam install coq-serapi.8.20.0+0.20.0 ./coq-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 diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 3da11c123..609b027bf 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -31,15 +31,17 @@ jobs: strategy: fail-fast: false matrix: - coq_version: [ '8.19.2' , '8.20+rc1' , 'dev' ] + coq_version: [ '8.20+rc1' , 'dev' ] ocaml_version: - '4.14.x' - '5.2.x' steps: - uses: actions/checkout@v2 - - uses: avsm/setup-ocaml@v2 + - uses: avsm/setup-ocaml@v3 with: ocaml-compiler: ${{ matrix.ocaml_version }} + opam-pin: false + opam-local-packages: - run: opam repo add coq-dev https://coq.inria.fr/opam/core-dev - run: opam install coq-core.${{ matrix.coq_version }} - run: opam install coq-stdlib.${{ matrix.coq_version }} diff --git a/.github/workflows/nix-action-coq-8.19.yml b/.github/workflows/nix-action-coq-8.19.yml deleted file mode 100644 index d5721afa2..000000000 --- a/.github/workflows/nix-action-coq-8.19.yml +++ /dev/null @@ -1,1643 +0,0 @@ -jobs: - QuickChick: - needs: - - coq - - mathcomp-ssreflect - 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@v27 - 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: stepCheck - name: Checking presence of CI target QuickChick - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-ext-lib' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "coq-ext-lib" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: simple-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "simple-io" - - 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.19" - --argstr job "QuickChick" - async-test: - needs: - - coq - - QuickChick - 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@v27 - 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: stepCheck - name: Checking presence of CI target async-test - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"async-test\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: itree-io' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "itree-io" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: json' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "json" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "QuickChick" - - 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.19" - --argstr job "async-test" - coq: - needs: [] - 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@v27 - 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: stepCheck - name: Checking presence of CI target coq - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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.19" - --argstr job "coq" - coq-elpi: - 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@v27 - 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: stepCheck - name: Checking presence of CI target coq-elpi - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --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-8.19" - --argstr job "coq-elpi" - coqeal: - needs: - - coq - - mathcomp-algebra - - multinomials - - mathcomp-real-closed - 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@v27 - 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: stepCheck - name: Checking presence of CI target coqeal - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: paramcoq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "paramcoq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: multinomials' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "multinomials" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-real-closed" - - 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.19" - --argstr job "coqeal" - coquelicot: - needs: - - coq - - mathcomp-ssreflect - 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@v27 - 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: stepCheck - name: Checking presence of CI target coquelicot - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\ - \ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\ - \ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - 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.19" - --argstr job "coquelicot" - hierarchy-builder: - needs: - - coq - - coq-elpi - 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@v27 - 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: stepCheck - name: Checking presence of CI target hierarchy-builder - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"hierarchy-builder\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coq-elpi' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "coq-elpi" - - 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.19" - --argstr job "hierarchy-builder" - http: - needs: - - coq - - QuickChick - - async-test - 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@v27 - 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: stepCheck - name: Checking presence of CI target http - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"http\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: QuickChick' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "QuickChick" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: async-test' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "async-test" - - 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.19" - --argstr job "http" - interval: - needs: - - coq - - coquelicot - - mathcomp-ssreflect - - mathcomp-fingroup - 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@v27 - 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: stepCheck - name: Checking presence of CI target interval - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "bignums" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: coquelicot' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "coquelicot" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "flocq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - 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.19" - --argstr job "interval" - mathcomp: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp-character - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp" - mathcomp-algebra: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-algebra - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-algebra\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-algebra" - mathcomp-analysis: - needs: - - coq - - mathcomp-classical - - mathcomp-field - - mathcomp-bigenough - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-analysis - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-classical' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-classical" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-bigenough" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-analysis" - mathcomp-bigenough: - needs: - - coq - - mathcomp-ssreflect - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-bigenough - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - 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.19" - --argstr job "mathcomp-bigenough" - mathcomp-character: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-character - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-character\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-character" - mathcomp-classical: - needs: - - coq - - mathcomp-algebra - - mathcomp-finmap - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-classical - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-classical" - mathcomp-field: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-field - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-field\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-field" - mathcomp-fingroup: - needs: - - coq - - mathcomp-ssreflect - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-fingroup - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-fingroup\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-fingroup" - mathcomp-finmap: - needs: - - coq - - mathcomp-ssreflect - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-finmap - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - 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.19" - --argstr job "mathcomp-finmap" - mathcomp-real-closed: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra - - mathcomp-field - - mathcomp-fingroup - - mathcomp-solvable - - mathcomp-bigenough - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-real-closed - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-real-closed\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-bigenough" - - 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.19" - --argstr job "mathcomp-real-closed" - mathcomp-solvable: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-solvable - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-solvable\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-solvable" - mathcomp-ssreflect: - needs: - - coq - - hierarchy-builder - 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@v27 - 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: stepCheck - name: Checking presence of CI target mathcomp-ssreflect - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "hierarchy-builder" - - 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.19" - --argstr job "mathcomp-ssreflect" - multinomials: - needs: - - coq - - mathcomp-ssreflect - - mathcomp-algebra - - mathcomp-finmap - - mathcomp-fingroup - - mathcomp-bigenough - 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@v27 - 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: stepCheck - name: Checking presence of CI target multinomials - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"multinomials\" \\\n --dry-run 2>&1\ - \ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\ - built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-finmap" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-bigenough' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-bigenough" - - 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.19" - --argstr job "multinomials" - odd-order: - needs: - - coq - - mathcomp-character - - mathcomp-ssreflect - - mathcomp-fingroup - - mathcomp-algebra - - mathcomp-solvable - - mathcomp-field - - mathcomp - 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@v27 - 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: stepCheck - name: Checking presence of CI target odd-order - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-character' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-character" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-ssreflect' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-ssreflect" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-fingroup' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-fingroup" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-algebra' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-algebra" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-solvable' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-solvable" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp-field" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "mathcomp" - - 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.19" - --argstr job "odd-order" - vcfloat: - needs: - - coq - - interval - 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@v27 - 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: stepCheck - name: Checking presence of CI target vcfloat - run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.19\" --argstr job \"vcfloat\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\ - s/.*/built/\") >> $GITHUB_OUTPUT\n" - - 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-8.19" - --argstr job "coq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: interval' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "interval" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: compcert' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "compcert" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: flocq' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "flocq" - - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: bignums' - run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.19" - --argstr job "bignums" - - 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.19" - --argstr job "vcfloat" -name: Nix CI for bundle coq-8.19 -'on': - pull_request: - paths: - - .github/workflows/nix-action-coq-8.19.yml - pull_request_target: - paths-ignore: - - .github/workflows/nix-action-coq-8.19.yml - types: - - opened - - synchronize - - reopened - push: - branches: - - master diff --git a/.nix/config.nix b/.nix/config.nix index d39bce63f..c77e3a2e1 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -27,15 +27,6 @@ let master = [ default-bundle = "coq-8.20"; bundles = { - "coq-8.19" = { - coqPackages = common-bundles // { - coq.override.version = "8.19"; - }; - ocamlPackages = { - elpi.override.version = "v1.19.5"; - }; - }; - "coq-8.20" = { coqPackages = common-bundles // { coq.override.version = "8.20"; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index 94d28ec69..9b872206b 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"a9f1e055901cba59260d03d64f523089bf63169c" +"24e96b4870378d5e87fd2d0dd46405b471c286ab" diff --git a/apps/coercion/src/coq_elpi_coercion_hook.mlg b/apps/coercion/src/coq_elpi_coercion_hook.mlg index 02b24f932..dd0aecca0 100644 --- a/apps/coercion/src/coq_elpi_coercion_hook.mlg +++ b/apps/coercion/src/coq_elpi_coercion_hook.mlg @@ -7,14 +7,6 @@ open Elpi_plugin open Coq_elpi_arg_syntax open Coq_elpi_vernacular -[%%if coq = "8.19" ] -let relevant = Sorts.Relevant -let anonR = Context.anonR -let nameR = Context.nameR -let annotR = Context.annotR -let build_expected_type env sigma expected = sigma, expected, false -let return s g _ = Some (s,g) -[%%else] let relevant = EConstr.ERelevance.relevant let anonR = Context.make_annot Names.Name.Anonymous EConstr.ERelevance.irrelevant let nameR x = Context.make_annot (Names.Name.Name x) EConstr.ERelevance.irrelevant @@ -30,7 +22,6 @@ let build_expected_type env sigma expected = sigma, EConstr.mkProd (annotR (Names.Name (Namegen.default_type_ident)), source, target), true | Coercion.Sort -> let (sigma, t) = Evarutil.new_Type sigma in sigma, t, true let return s g t = Some (s,g,t) -[%%endif] let elpi_coercion_hook program env sigma ~flags v ~inferred ~expected = let loc = API.Ast.Loc.initial "(unknown)" in diff --git a/apps/cs/src/coq_elpi_cs_hook.mlg b/apps/cs/src/coq_elpi_cs_hook.mlg index c94e63dcc..668a348dd 100644 --- a/apps/cs/src/coq_elpi_cs_hook.mlg +++ b/apps/cs/src/coq_elpi_cs_hook.mlg @@ -2,2074 +2,6 @@ DECLARE PLUGIN "coq-elpi.cs" { -[%%if coq = "8.19"] -module Evarconv_hacked = struct -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * Copyright INRIA, CNRS and contributors *) -(* - env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result - -let default_transparent_state env = TransparentState.full -(* Conv_oracle.get_transp_state (Environ.oracle env) *) - -let default_flags_of ?(subterm_ts=TransparentState.empty) ts = - { modulo_betaiota = true; - open_ts = ts; closed_ts = ts; subterm_ts; - allowed_evars = AllowedEvars.all; with_cs = true; - } - -let default_flags env = - let ts = default_transparent_state env in - default_flags_of ts - -let debug_unification = CDebug.create ~name:"elpi-unification" () - -let debug_ho_unification = CDebug.create ~name:"elpi-ho-unification" () - -(*******************************************) -(* Functions to deal with impossible cases *) -(*******************************************) - -(* In case the constants id/ID are not defined *) -let unit_judge_fallback = - let na1 = make_annot (Name (Id.of_string "A")) Sorts.Relevant in - let na2 = make_annot (Name (Id.of_string "H")) Sorts.Relevant in - make_judge - (mkLambda (na1,mkProp,mkLambda(na2,mkRel 1,mkRel 1))) - (mkProd (na1,mkProp,mkArrow (mkRel 1) Sorts.Relevant (mkRel 2))) - -let coq_unit_judge env sigma = - match Coqlib.lib_ref_opt "core.IDProp.idProp" with - | Some c -> - let sigma, c = Evd.fresh_global env sigma c in - let t = Retyping.get_type_of env sigma c in - sigma, make_judge c t - | None -> sigma, unit_judge_fallback - -let unfold_projection env evd ts p r c = - let cst = Projection.constant p in - if TransparentState.is_transparent_constant ts cst then - Some (mkProj (Projection.unfold p, r, c)) - else None - -let eval_flexible_term ts env evd c = - match EConstr.kind evd c with - | Const (c, u) -> - if TransparentState.is_transparent_constant ts c - then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u)) - else None - | Rel n -> - (try match lookup_rel n env with - | RelDecl.LocalAssum _ -> None - | RelDecl.LocalDef (_,v,_) -> Some (lift n v) - with Not_found -> None) - | Var id -> - (try - if TransparentState.is_transparent_variable ts id then - env |> lookup_named id |> NamedDecl.get_value - else None - with Not_found -> None) - | LetIn (_,b,_,c) -> Some (subst1 b c) - | Lambda _ -> Some c - | Proj (p, r, c) -> - if Projection.unfolded p then assert false - else unfold_projection env evd ts p r c - | _ -> assert false - -type flex_kind_of_term = - | Rigid - | MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *) - | Flexible of EConstr.existential - -let has_arg s = Option.has_some (Stack.strip_n_app 0 s) - -let flex_kind_of_term flags env evd c sk = - match EConstr.kind evd c with - | LetIn _ | Rel _ | Const _ | Var _ | Proj _ -> - Option.cata (fun x -> MaybeFlexible x) Rigid (eval_flexible_term flags.open_ts env evd c) - | Lambda _ when has_arg sk -> - if flags.modulo_betaiota then MaybeFlexible c - else Rigid - | Evar ev -> - if is_evar_allowed flags (fst ev) then Flexible ev else Rigid - | Lambda _ | Prod _ | Sort _ | Ind _ | Int _ | Float _ | Array _ -> Rigid - | Construct _ | CoFix _ (* Incorrect: should check only app in sk *) -> Rigid - | Meta _ -> Rigid - | Fix _ -> Rigid (* happens when the fixpoint is partially applied (should check it?) *) - | Cast _ | App _ | Case _ -> assert false - -let apprec_nohdbeta flags env evd c = - let (t,sk as appr) = Reductionops.whd_nored_state env evd (c, []) in - if flags.modulo_betaiota && Stack.not_purely_applicative sk - then Stack.zip evd (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env evd appr) - else c - -let position_problem l2r = function - | CONV -> None - | CUMUL -> Some l2r - -(* [occur_rigidly ev evd t] tests if the evar ev occurs in a rigid - context in t. Precondition: t has a rigid head and is not reducible. - - That function is an under approximation of occur-check, it can return - false even if the occur-check would succeed on the normal form. This - means we might postpone unsolvable constraints which will ultimately - result in an occur-check after reductions. If it returns true, we - know that the occur-check would also return true on the normal form. - - [t] is assumed to have a rigid head, which can - appear under a elimination context (e.g. application, match or projection). - - In the inner recursive function, the result indicates if the term is - rigid (irreducible), normal (succession of constructors) or - potentially reducible. For applications, this means than an - occurrence of the evar in arguments should be looked at to find an - occur-check if the head is rigid or normal. For inductive - eliminations, only an occurrence in a rigid context of the - discriminee counts as a rigid occurrence overall, not a normal - occurrence which might disappear after reduction. *) - -type result = Rigid of bool | Normal of bool | Reducible - -let rigid_normal_occ = function Rigid b -> b | Normal b -> b | _ -> false - -let occur_rigidly flags env evd (evk,_) t = - let rec aux t = - match EConstr.kind evd t with - | App (f, c) -> - (match aux f with - | Rigid b -> Rigid (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) - | Normal b -> Normal (b || Array.exists (fun x -> rigid_normal_occ (aux x)) c) - | Reducible -> Reducible) - | Construct _ -> Normal false - | Ind _ | Sort _ -> Rigid false - | Proj (p, _, c) -> - let cst = Projection.constant p in - let rigid = not (TransparentState.is_transparent_constant flags.open_ts cst) in - if rigid then aux c - else (* if the evar appears rigidly in c then this elimination - cannot reduce and we have a rigid occurrence, otherwise - we don't know. *) - (match aux c with - | Rigid _ as res -> res - | Normal b -> Reducible - | Reducible -> Reducible) - | Evar (evk',l) -> - if Evar.equal evk evk' then Rigid true - else if is_evar_allowed flags evk' then - Reducible - else Rigid (SList.Skip.exists (fun x -> rigid_normal_occ (aux x)) l) - | Cast (p, _, _) -> aux p - | Lambda (na, t, b) -> aux b - | LetIn (na, _, _, b) -> aux b - | Const (c,_) -> - if TransparentState.is_transparent_constant flags.open_ts c then Reducible - else Rigid false - | Prod (_, b, t) -> - let b' = aux b and t' = aux t in - if rigid_normal_occ b' || rigid_normal_occ t' then Rigid true - else Reducible - | Rel _ | Var _ -> Reducible - | Case (_,_,_,_,_,c,_) -> - (match aux c with - | Rigid b -> Rigid b - | _ -> Reducible) - | Meta _ | Fix _ | CoFix _ | Int _ | Float _ | Array _ -> Reducible - in - match aux t with - | Rigid b -> b - | Normal b -> b - | Reducible -> false - -(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose - the problem (t1 stack1) = (t2 stack2) into a problem - - stack1 = params1@[c1]@extra_args1 - stack2 = us2@extra_args2 - t1 params1 c1 = proji params (c xs) - t2 us2 = head us - extra_args1 = extra_args2 - - by finding a record R and an object c := [xs:bs](Build_R params v1..vn) - with vi = (head us), for which we know that the i-th projection proji - satisfies - - proji params (c xs) = head us - - Rem: such objects, usable for conversion, are defined in the objdef - table; practically, it amounts to "canonically" equip t2 into a - object c in structure R (since, if c1 were not an evar, the - projection would have been reduced) *) - -let check_conv_record env sigma (t1,sk1) (t2,sk2) = - let open ValuePattern in - let (proji, u), arg = Termops.global_app_of_constr sigma t1 in - let t2, sk2' = decompose_app sigma (shrink_eta sigma t2) in - let sk2 = Stack.append_app sk2' sk2 in - let (sigma, solution), sk2_effective = - let t2 = - let rec remove_lambda t2 = - match EConstr.kind sigma t2 with - | Lambda (_,_,t2) -> remove_lambda t2 - | Cast (t2,_,_) -> remove_lambda t2 - | App (t2,_) -> t2 - | _ -> t2 in - if Stack.is_empty sk2 then remove_lambda t2 else t2 in - try - match EConstr.kind sigma t2 with - Prod (_,_,_) -> (* assert (l2=[]); *) - CanonicalSolution.find env sigma (proji, Prod_cs), - (Stack.append_app [|t2|] Stack.empty) - | Sort s -> - let s = ESorts.kind sigma s in - CanonicalSolution.find env sigma - (proji, Sort_cs (Sorts.family s)),[] - | Proj (p, _, c) -> - CanonicalSolution.find env sigma(proji, Proj_cs (Names.Projection.repr p)), Stack.append_app [|c|] sk2 - | _ -> - let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in - CanonicalSolution.find env sigma (proji, Const_cs c2),sk2 - with Not_found -> - CanonicalSolution.find env sigma (proji,Default_cs), [] - in - let open CanonicalSolution in - let params1, c1, extra_args1 = - match arg with - | Some c -> (* A primitive projection applied to c *) - let ty = Retyping.get_type_of ~lax:true env sigma c in - let (i,u), ind_args = - (* Are we sure that ty is not an evar? *) - Inductiveops.find_mrectype env sigma ty - in ind_args, c, sk1 - | None -> - match Stack.strip_n_app solution.nparams sk1 with - | Some (params1, c1, extra_args1) -> (Option.get @@ Stack.list_of_app_stack params1), c1, extra_args1 - | _ -> raise Not_found in - let us2,extra_args2 = - let l_us = List.length solution.cvalue_arguments in - if Int.equal l_us 0 then [], sk2_effective - else match (Stack.strip_n_app (l_us-1) sk2_effective) with - | None -> raise Not_found - | Some (l',el,s') -> ((Option.get @@ Stack.list_of_app_stack l') @ [el],s') in - let h, _ = decompose_app sigma solution.body in - let t2 = Stack.zip sigma (t2,sk2) in - let h2, _ = decompose_app sigma t2 in - sigma,(h, h2),solution.constant,solution.abstractions_ty,(solution.params,params1), - (solution.cvalue_arguments,us2),(extra_args1,extra_args2),c1, - (solution.cvalue_abstraction, t2) - -(* Precondition: one of the terms of the pb is an uninstantiated evar, - * possibly applied to arguments. *) - -let join_failures evd1 evd2 e1 e2 = - match e1, e2 with - | _, CannotSolveConstraint (_,ProblemBeyondCapabilities) -> (evd1,e1) - | _ -> (evd2,e2) - -let rec ise_try evd = function - [] -> assert false - | [f] -> f evd - | f1::l -> - match f1 evd with - | Success _ as x -> x - | UnifFailure (evd1,e1) -> - match ise_try evd l with - | Success _ as x -> x - | UnifFailure (evd2,e2) -> - let evd,e = join_failures evd1 evd2 e1 e2 in - UnifFailure (evd,e) - -let ise_and evd l = - let rec ise_and i = function - [] -> assert false - | [f] -> f i - | f1::l -> - match f1 i with - | Success i' -> ise_and i' l - | UnifFailure _ as x -> x in - ise_and evd l - -let ise_list2 evd f l1 l2 = - let rec allrec k l1 l2 = match l1, l2 with - | [], [] -> k evd - | x1 :: l1, x2 :: l2 -> - let k evd = match k evd with - | Success evd -> f evd x1 x2 - | UnifFailure _ as x -> x - in - allrec k l1 l2 - | ([], _ :: _) | (_ :: _, []) -> UnifFailure (evd, NotSameArgSize) - in - allrec (fun i -> Success i) l1 l2 - -let ise_array2 evd f v1 v2 = - let rec allrec i = function - | -1 -> Success i - | n -> - match f i v1.(n) v2.(n) with - | Success i' -> allrec i' (n-1) - | UnifFailure _ as x -> x in - let lv1 = Array.length v1 in - if Int.equal lv1 (Array.length v2) then allrec evd (pred lv1) - else UnifFailure (evd,NotSameArgSize) - -let rec ise_inst2 evd f l1 l2 = match l1, l2 with -| [], [] -> Success evd -| [], (_ :: _) | (_ :: _), [] -> assert false -| c1 :: l1, c2 :: l2 -> - match ise_inst2 evd f l1 l2 with - | Success evd' -> f evd' c1 c2 - | UnifFailure _ as x -> x - -(* Applicative node of stack are read from the outermost to the innermost - but are unified the other way. *) -let rec ise_app_rev_stack2 env f evd revsk1 revsk2 = - match Stack.decomp_rev revsk1, Stack.decomp_rev revsk2 with - | Some (t1,revsk1), Some (t2,revsk2) -> - begin - match ise_app_rev_stack2 env f evd revsk1 revsk2 with - | (_, UnifFailure _) as x -> x - | x, Success i' -> x, f env i' CONV t1 t2 - end - | _, _ -> (revsk1,revsk2), Success evd - -(* Add equality constraints for covariant/invariant positions. For - irrelevant positions, unify universes when flexible. *) -let compare_cumulative_instances pbty evd variances u u' = - match Evarutil.compare_cumulative_instances pbty variances u u' evd with - | Inl evd -> - Success evd - | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) - -let compare_constructor_instances evd u u' = - match Evarutil.compare_constructor_instances evd u u' with - | Inl evd -> - Success evd - | Inr p -> UnifFailure (evd, UnifUnivInconsistency p) - -type application = FullyApplied | NumArgs of int - -let is_applied o n = match o with FullyApplied -> true | NumArgs m -> Int.equal m n - -let compare_heads pbty env evd ~nargs term term' = - let check_strict evd u u' = - let cstrs = UVars.enforce_eq_instances u u' Sorts.QUConstraints.empty in - try Success (Evd.add_quconstraints evd cstrs) - with UGraph.UniverseInconsistency p -> UnifFailure (evd, UnifUnivInconsistency p) - in - match EConstr.kind evd term, EConstr.kind evd term' with - | Const (c, u), Const (c', u') when QConstant.equal env c c' -> - if is_applied nargs 1 && Environ.is_array_type env c - then - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - compare_cumulative_instances pbty evd [|UVars.Variance.Irrelevant|] u u' - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - check_strict evd u u' - | Const _, Const _ -> UnifFailure (evd, NotSameHead) - | Ind ((mi,i) as ind , u), Ind (ind', u') when QInd.equal env ind ind' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let needed = Conversion.inductive_cumulativity_arguments (mind,i) in - if not (is_applied nargs needed) - then check_strict evd u u' - else - compare_cumulative_instances pbty evd variances u u' - end - | Ind _, Ind _ -> UnifFailure (evd, NotSameHead) - | Construct (((mi,ind),ctor as cons), u), Construct (cons', u') - when QConstruct.equal env cons cons' -> - if EInstance.is_empty u && EInstance.is_empty u' then Success evd - else - let u = EInstance.kind evd u and u' = EInstance.kind evd u' in - let mind = Environ.lookup_mind mi env in - let open Declarations in - begin match mind.mind_variance with - | None -> check_strict evd u u' - | Some variances -> - let needed = Conversion.constructor_cumulativity_arguments (mind,ind,ctor) in - if not (is_applied nargs needed) - then check_strict evd u u' - else compare_constructor_instances evd u u' - end - | Construct _, Construct _ -> UnifFailure (evd, NotSameHead) - | _, _ -> anomaly (Pp.str "") - -(* This function tries to unify 2 stacks element by element. It works - from the end to the beginning. If it unifies a non empty suffix of - stacks but not the entire stacks, the first part of the answer is - Some(the remaining prefixes to tackle) - If [no_app] is set, situations like [match head u1 u2 with ... end] - will not try to match [u1] and [u2] (why?); but situations like - [match head u1 u2 with ... end v] will try to match [v] (??) *) -(* Input: E1[] =? E2[] where the E1, E2 are concatenations of - n-ary-app/case/fix/proj elimination rules - Output: - - either None if E1 = E2 is solved, - - or Some (E1'',E2'') such that there is a decomposition of - E1[] = E1'[E1''[]] and E2[] = E2'[E2''[]] s.t. E1' = E2' and - E1'' cannot be unified with E2'' - - UnifFailure if no such non-empty E1' = E2' exists *) -let rec ise_stack2 no_app env evd f sk1 sk2 = - let rec ise_rev_stack2 deep i revsk1 revsk2 = - let fail x = if deep then Some (List.rev revsk1, List.rev revsk2), Success i - else None, x in - match revsk1, revsk2 with - | [], [] -> None, Success i - | Stack.Case cse1 :: q1, Stack.Case cse2 :: q2 -> - let (ci1, u1, pms1, (t1,_), br1) = Stack.expand_case env evd cse1 in - let (ci2, u2, pms2, (t2,_), br2) = Stack.expand_case env evd cse2 in - let hd1 = mkIndU (ci1.ci_ind, u1) in - let hd2 = mkIndU (ci2.ci_ind, u2) in - let fctx i (ctx1, t1) (_ctx2, t2) = f (push_rel_context ctx1 env) i CONV t1 t2 in - begin - match ise_and i [ - (fun i -> compare_heads CONV env i ~nargs:FullyApplied hd1 hd2); - (fun i -> ise_array2 i (fun ii -> f env ii CONV) pms1 pms2); - (fun i -> fctx i t1 t2); - (fun i -> ise_array2 i fctx br1 br2); - ] - with - | Success i' -> ise_rev_stack2 true i' q1 q2 - | UnifFailure _ as x -> fail x - end - | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> - if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_rev_stack2 true i q1 q2 - else fail (UnifFailure (i, NotSameHead)) - | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, - Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> - if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then - match ise_and i [ - (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); - (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> snd (ise_stack2 no_app env i f a1 a2))] with - | Success i' -> ise_rev_stack2 true i' q1 q2 - | UnifFailure _ as x -> fail x - else fail (UnifFailure (i,NotSameHead)) - | Stack.App _ :: _, Stack.App _ :: _ -> - if no_app && deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else - begin match ise_app_rev_stack2 env f i revsk1 revsk2 with - |_,(UnifFailure _ as x) -> fail x - |(l1, l2), Success i' -> ise_rev_stack2 true i' l1 l2 - end - |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead)) - in ise_rev_stack2 false evd (List.rev sk1) (List.rev sk2) - -type hook = Environ.env -> Evd.evar_map -> (EConstr.t * Reductionops.Stack.t) -> (EConstr.t * Reductionops.Stack.t) -> (Evd.evar_map * (EConstr.t * EConstr.t) * EConstr.t * EConstr.t list * -(EConstr.t list * EConstr.t list) * (EConstr.t list * EConstr.t list) * -(Reductionops.Stack.t * Reductionops.Stack.t) * EConstr.constr * -(int option * EConstr.constr)) option - -let all_hooks = ref (CString.Map.empty : hook CString.Map.t) - -let register_hook ~name ?(override=false) h = - if not override && CString.Map.mem name !all_hooks then - CErrors.anomaly ~label:"CanonicalSolution.register_hook" - Pp.(str "Hook already registered: \"" ++ str name ++ str "\"."); - all_hooks := CString.Map.add name h !all_hooks - -let active_hooks = Summary.ref ~name:"canonical_solution_hooks" ([] : string list) - -let deactivate_hook ~name = - active_hooks := List.filter (fun s -> not (String.equal s name)) !active_hooks - -let activate_hook ~name = - assert (CString.Map.mem name !all_hooks); - deactivate_hook ~name; - active_hooks := name :: !active_hooks - -let apply_hooks env sigma proj pat = - List.find_map (fun name -> CString.Map.get name !all_hooks env sigma proj pat) !active_hooks - -(* Make sure that the matching suffix is the all stack *) -let rec exact_ise_stack2 env evd f sk1 sk2 = - let rec ise_rev_stack2 i revsk1 revsk2 = - match revsk1, revsk2 with - | [], [] -> Success i - | Stack.Case cse1 :: q1, Stack.Case cse2 :: q2 -> - let (ci1, u1, pms1, (t1,_), br1) = Stack.expand_case env evd cse1 in - let (ci2, u2, pms2, (t2,_), br2) = Stack.expand_case env evd cse2 in - let hd1 = mkIndU (ci1.ci_ind, u1) in - let hd2 = mkIndU (ci2.ci_ind, u2) in - let fctx i (ctx1, t1) (_ctx2, t2) = f (push_rel_context ctx1 env) i CONV t1 t2 in - ise_and i [ - (fun i -> ise_rev_stack2 i q1 q2); - (fun i -> compare_heads CONV env i ~nargs:FullyApplied hd1 hd2); - (fun i -> ise_array2 i (fun ii -> f env ii CONV) pms1 pms2); - (fun i -> fctx i t1 t2); - (fun i -> ise_array2 i fctx br1 br2); - ] - | Stack.Fix (((li1, i1),(_,tys1,bds1 as recdef1)),a1)::q1, - Stack.Fix (((li2, i2),(_,tys2,bds2)),a2)::q2 -> - if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then - ise_and i [ - (fun i -> ise_rev_stack2 i q1 q2); - (fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2); - (fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2); - (fun i -> exact_ise_stack2 env i f a1 a2)] - else UnifFailure (i,NotSameHead) - | Stack.Proj (p1,_)::q1, Stack.Proj (p2,_)::q2 -> - if QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) - then ise_rev_stack2 i q1 q2 - else (UnifFailure (i, NotSameHead)) - | Stack.App _ :: _, Stack.App _ :: _ -> - begin match ise_app_rev_stack2 env f i revsk1 revsk2 with - |_,(UnifFailure _ as x) -> x - |(l1, l2), Success i' -> ise_rev_stack2 i' l1 l2 - end - |_, _ -> UnifFailure (i,(* Maybe improve: *) NotSameHead) - in - if Reductionops.Stack.compare_shape sk1 sk2 then - ise_rev_stack2 evd (List.rev sk1) (List.rev sk2) - else UnifFailure (evd, (* Dummy *) NotSameHead) - -let compare_heads pbty env evd ~nargs term term' = - compare_heads pbty env evd ~nargs:(NumArgs nargs) term term' - -let conv_fun f flags on_types = - let typefn env evd pbty term1 term2 = - let flags = { (default_flags env) with - with_cs = flags.with_cs; - allowed_evars = flags.allowed_evars } - in f flags env evd pbty term1 term2 - in - let termfn env evd pbty term1 term2 = - f flags env evd pbty term1 term2 - in - match on_types with - | TypeUnification -> typefn - | TermUnification -> termfn - -let infer_conv_noticing_evars ~pb ~ts env sigma t1 t2 = - let has_evar = ref false in - let evar_expand ev = - let v = existential_expand_value0 sigma ev in - let () = match v with - | CClosure.EvarUndefined _ -> has_evar := true - | CClosure.EvarDefined _ -> () - in - v - in - let evar_handler = { (Evd.evar_handler sigma) with evar_expand } in - let conv pb ~l2r sigma = Conversion.generic_conv pb ~l2r ~evars:evar_handler in - match infer_conv_gen conv ~catch_incon:false ~pb ~ts env sigma t1 t2 with - | Some sigma -> Some (Success sigma) - | None -> - if !has_evar then None - else Some (UnifFailure (sigma, ConversionFailed (env,t1,t2))) - | exception UGraph.UniverseInconsistency e -> - if !has_evar then None - else Some (UnifFailure (sigma, UnifUnivInconsistency e)) - -let pr_econstr = ref (fun _ _ _ -> Pp.str "unable to print econstr") - -(* TODO: move to a proper place *) -let rec split_at n acc l = - if n = 0 then (List.rev acc, l) - else match l with - | [] -> (List.rev acc, l) - | h :: t -> split_at (n-1) (h :: acc) t -let split_at n l = split_at n [] l - -let try_simplify_proj_construct flags env evd v k sk = - match k with (* try unfolding an applied projection on the rhs *) - | Proj (p, _, c) -> begin - let c = whd_all env evd c in (* reduce argument *) - try let (hd, args) = destApp evd c in - if isConstruct evd hd then Some (whd_nored_state env evd (args.(Projection.npars p + Projection.arg p), sk)) - else None - with _ -> None - end - | Const (cn, _) when Structures.Structure.is_projection cn -> begin - match split_at (Structures.Structure.projection_nparams cn) (Option.default [] (Stack.list_of_app_stack sk)) with - | (_, []) -> None - | (_, c :: _) -> begin - let c = whd_all env evd c in - try let (hd, _) = destApp evd c in - if isConstruct evd hd then - Some (whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (v,sk)) - else None - with _ -> None - end end - | _ -> None - -let rec evar_conv_x flags env evd pbty term1 term2 = - let term1 = whd_head_evar evd term1 in - let term2 = whd_head_evar evd term2 in - (* Maybe convertible but since reducing can erase evars which [evar_apprec] - could have found, we do it only if the terms are free of evar. - Note: incomplete heuristic... *) - let ground_test = - if is_ground_term evd term1 && is_ground_term evd term2 then - infer_conv_noticing_evars ~pb:pbty ~ts:flags.closed_ts env evd term1 term2 - else None - in - match ground_test with - | Some result -> result - | None -> - (* Until pattern-unification is used consistently, use nohdbeta to not - destroy beta-redexes that can be used for 1st-order unification *) - let term1 = apprec_nohdbeta flags env evd term1 in - let term2 = apprec_nohdbeta flags env evd term2 in - let default () = - match - evar_eqappr_x flags env evd pbty - (whd_nored_state env evd (term1,Stack.empty)) - (whd_nored_state env evd (term2,Stack.empty)) - with - | UnifFailure _ as x -> - if Retyping.relevance_of_term env evd term1 == Sorts.Irrelevant || - Retyping.relevance_of_term env evd term2 == Sorts.Irrelevant - then Success evd - else x - | Success _ as x -> x - in - begin match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> - (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem true pbty,ev,term2) with - | UnifFailure (_,(OccurCheck _ | NotClean _)) -> - (* Eta-expansion might apply *) - (* OccurCheck: eta-expansion could solve - ?X = {| foo := ?X.(foo) |} - NotClean: pruning in solve_simple_eqn is incomplete wrt - Miller patterns *) - default () - | x -> x) - | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) -> - (match solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem false pbty,ev,term1) with - | UnifFailure (_, (OccurCheck _ | NotClean _)) -> - (* OccurCheck: eta-expansion could solve - ?X = {| foo := ?X.(foo) |} - NotClean: pruning in solve_simple_eqn is incomplete wrt - Miller patterns *) - default () - | x -> x) - | _ -> default () - end - -and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty - (term1, sk1 as appr1) (term2, sk2 as appr2) = - let quick_fail i = (* not costly, loses info *) - UnifFailure (i, NotSameHead) - in - let miller_pfenning l2r fallback ev lF tM evd = - match is_unification_pattern_evar env evd ev lF tM with - | None -> fallback () - | Some l1' -> (* Miller-Pfenning's patterns unification *) - let t2 = tM in - let t2 = solve_pattern_eqn env evd l1' t2 in - solve_simple_eqn (conv_fun evar_conv_x) flags env evd - (position_problem l2r pbty,ev,t2) - in - let consume_stack l2r (termF,skF) (termO,skO) evd = - let switch f a b = if l2r then f a b else f b a in - let not_only_app = Stack.not_purely_applicative skO in - match switch (ise_stack2 not_only_app env evd (evar_conv_x flags)) skF skO with - | Some (l,r), Success i' when l2r && (not_only_app || List.is_empty l) -> - (* E[?n]=E'[redex] reduces to either l[?n]=r[redex] with - case/fix/proj in E' (why?) or ?n=r[redex] *) - switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - | Some (r,l), Success i' when not l2r && (not_only_app || List.is_empty l) -> - (* E'[redex]=E[?n] reduces to either r[redex]=l[?n] with - case/fix/proj in E' (why?) or r[redex]=?n *) - switch (evar_conv_x flags env i' pbty) (Stack.zip evd (termF,l)) (Stack.zip evd (termO,r)) - | None, Success i' -> switch (evar_conv_x flags env i' pbty) termF termO - | _, (UnifFailure _ as x) -> x - | Some _, _ -> UnifFailure (evd,NotSameArgSize) in - let eta_lambda env evd onleft term (term',sk') = - (* Reduces an equation [env |- <(fun na:c1 => c'1)|empty> = ] to - [env, na:c1 |- c'1 = sk'[term'] (with some additional reduction) *) - let (na,c1,c'1) = destLambda evd term in - let env' = push_rel (RelDecl.LocalAssum (na,c1)) env in - let out1 = whd_betaiota_deltazeta_for_iota_state - flags.open_ts env' evd (c'1, Stack.empty) in - let out2 = whd_nored_state env' evd - (lift 1 (Stack.zip evd (term', sk')), Stack.append_app [|EConstr.mkRel 1|] Stack.empty) in - if onleft then evar_eqappr_x flags env' evd CONV out1 out2 - else evar_eqappr_x flags env' evd CONV out2 out1 - in - let rigids env evd sk term sk' term' = - let nargs = Stack.args_size sk in - let nargs' = Stack.args_size sk' in - if not (Int.equal nargs nargs') then UnifFailure (evd, NotSameArgSize) - else - ise_and evd [(fun i -> - try compare_heads pbty env i ~nargs term term' - with UGraph.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk sk')] - in - let consume l2r (_, skF as apprF) (_,skM as apprM) i = - if not (Stack.is_empty skF && Stack.is_empty skM) then - consume_stack l2r apprF apprM i - else quick_fail i - in - let miller l2r ev (termF,skF as apprF) (termM, skM as apprM) i = - let switch f a b = if l2r then f a b else f b a in - let not_only_app = Stack.not_purely_applicative skM in - match Stack.list_of_app_stack skF with - | None -> quick_fail evd - | Some lF -> - let tM = Stack.zip evd apprM in - miller_pfenning l2r - (fun () -> if not_only_app then (* Postpone the use of an heuristic *) - switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) (Stack.zip evd apprF) tM - else quick_fail i) - ev lF tM i - in - let flex_maybeflex l2r ev (termF,skF as apprF) (termM, skM as apprM) vM = - (* Problem: E[?n[inst]] = E'[redex] - Strategy, as far as I understand: - 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[redex] is a Miller pattern: solve it now - 2a. if E'=E'1[E'2] and E=E'1 unifiable, recursively solve ?n[inst] = E'2[redex] - 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, - recursively solve E2[?n[inst]] = E'2[redex] - 3. reduce the redex into M and recursively solve E[?n[inst]] =? E'[M] *) - let switch f a b = if l2r then f a b else f b a in - let delta i = - switch (evar_eqappr_x flags env i pbty) apprF - (whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (vM,skM)) - in - let default i = ise_try i [miller l2r ev apprF apprM; - consume l2r apprF apprM; - delta] - in - match EConstr.kind evd termM with - | Proj (p, _, c) when not (Stack.is_empty skF) -> - (* Might be ?X args = p.c args', and we have to eta-expand the - primitive projection if |args| >= |args'|+1. *) - let nargsF = Stack.args_size skF and nargsM = Stack.args_size skM in - begin - (* ?X argsF' ~= (p.c ..) argsM' -> ?X ~= (p.c ..), no need to expand *) - if nargsF <= nargsM then default evd - else - let f = - try - let termM' = Retyping.expand_projection env evd p c [] in - let apprM' = - whd_betaiota_deltazeta_for_iota_state flags.open_ts env evd (termM',skM) - in - let delta' i = - switch (evar_eqappr_x flags env i pbty) apprF apprM' - in - fun i -> ise_try i [miller l2r ev apprF apprM'; - consume l2r apprF apprM'; delta'] - with Retyping.RetypeError _ -> - (* Happens thanks to w_unify building ill-typed terms *) - default - in f evd - end - | _ -> default evd - in - let flex_rigid l2r ev (termF, skF as apprF) (termR, skR as apprR) = - (* Problem: E[?n[inst]] = E'[M] with M blocking computation (in theory) - Strategy, as far as I understand: - 1. if E[]=[]u1..un and ?n[inst] u1..un = E'[M] is a Miller pattern: solve it now - 2a. if E'=E'1[E'2] and E=E'1 unifiable and E' contient app/fix/proj, - recursively solve ?n[inst] = E'2[M] - 2b. if E'=E'1[E'2] and E=E1[E2] and E=E'1 unifiable and E' contient app/fix/proj, - recursively solve E2[?n[inst]] = E'2[M] - 3a. if M a lambda or a constructor: eta-expand and recursively solve - 3b. if M a constructor C ..ui..: eta-expand and recursively solve proji[E[?n[inst]]]=ui - 4. fail if E purely applicative and ?n occurs rigidly in E'[M] - 5. absorb arguments if purely applicative and postpone *) - let switch f a b = if l2r then f a b else f b a in - let eta evd = - match EConstr.kind evd termR with - | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> - eta_lambda env evd false termR apprF - | Construct u -> eta_constructor flags env evd u skR apprF - | _ -> UnifFailure (evd,NotSameHead) - in - match Stack.list_of_app_stack skF with - | None -> - ise_try evd [consume_stack l2r apprF apprR; eta] - | Some lF -> - let tR = Stack.zip evd apprR in - miller_pfenning l2r - (fun () -> - ise_try evd - [eta;(* Postpone the use of an heuristic *) - (fun i -> - if not (occur_rigidly flags env i ev tR) then - let i,tF = - if isRel i tR || isVar i tR then - (* Optimization so as to generate candidates *) - let i,ev = evar_absorb_arguments env i ev lF in - i,mkEvar ev - else - i,Stack.zip evd apprF in - switch (fun x y -> Success (Evarutil.add_unification_pb (pbty,env,x,y) i)) - tF tR - else - UnifFailure (evd,OccurCheck (fst ev,tR)))]) - ev lF tR evd - in - let first_order env i t1 t2 sk1 sk2 = - (* Try first-order unification *) - match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with - | None, Success i' -> - (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *) - (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *) - let ev1' = whd_evar i' t1 in - if isEvar i' ev1' then - solve_simple_eqn (conv_fun evar_conv_x) flags env i' - (position_problem true pbty,destEvar i' ev1',term2) - else - (* HH: Why not to drop sk1 and sk2 since they unified *) - evar_eqappr_x flags env evd pbty - (ev1', sk1) (term2, sk2) - | Some (r,[]), Success i' -> - (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *) - (* we now unify r[?ev1] and ?ev2 *) - let ev2' = whd_evar i' t2 in - if isEvar i' ev2' then - solve_simple_eqn (conv_fun evar_conv_x) flags env i' - (position_problem false pbty,destEvar i' ev2',Stack.zip i' (term1,r)) - else - evar_eqappr_x flags env evd pbty - (ev2', sk1) (term2, sk2) - | Some ([],r), Success i' -> - (* Symmetrically *) - (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *) - (* we now unify ?ev1 and r[?ev2] *) - let ev1' = whd_evar i' t1 in - if isEvar i' ev1' then - solve_simple_eqn (conv_fun evar_conv_x) flags env i' - (position_problem true pbty,destEvar i' ev1',Stack.zip i' (term2,r)) - else - (* HH: Why not to drop sk1 and sk2 since they unified *) - evar_eqappr_x flags env evd pbty - (ev1', sk1) (term2, sk2) - | None, (UnifFailure _ as x) -> - (* sk1 and sk2 have no common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true (destEvar evd t1) appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false (destEvar evd t2) appr2 appr1 - else - (* We could instead try Miller unification, then - postpone to see if other equations help, as in: - [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *) - x - | Some _, Success _ -> - (* sk1 and sk2 have a common outer part *) - if Stack.not_purely_applicative sk2 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid true (destEvar evd t1) appr1 appr2 - else - if Stack.not_purely_applicative sk1 then - (* Ad hoc compatibility with 8.4 which treated non-app as rigid *) - flex_rigid false (destEvar evd t2) appr2 appr1 - else - (* We could instead try Miller unification, then - postpone to see if other equations help, as in: - [Check fun a b c : unit => (eq_refl : _ a b = _ c a b)] *) - UnifFailure (i,NotSameArgSize) - | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.") - in - let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in - (* Evar must be undefined since we have flushed evars *) - let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in - match (flex_kind_of_term flags env evd term1 sk1, - flex_kind_of_term flags env evd term2 sk2) with - | Flexible (sp1,al1), Flexible (sp2,al2) -> - (* Notations: - - "sk" is a stack (or, more abstractly, an evaluation context, written E) - - "ev" is an evar "?ev", more precisely an evar ?n with an instance inst - - "al" is an evar instance - Problem: E₁[?n₁[inst₁]] = E₂[?n₂[inst₂]] (i.e. sk1[?ev1] =? sk2[?ev2] - Strategy is first-order unification - 1a. if E₁=E₂ unifiable, solve ?n₁[inst₁] = ?n₂[inst₂] - 1b. if E₂=E₂'[E₂''] and E₁=E₂' unifiable, recursively solve ?n₁[inst₁] = E₂''[?n₂[inst₂]] - 1b'. if E₁=E₁'[E₁''] and E₁'=E₂ unifiable, recursively solve E₁''[?n₁[inst₁]] = ?n₂[inst₂] - recursively solve E2[?n[inst]] = E'2[redex] - 2. fails if neither E₁ nor E₂ is a prefix of the other *) - let f1 i = first_order env i term1 term2 sk1 sk2 - and f2 i = - if Evar.equal sp1 sp2 then - match ise_stack2 false env i (evar_conv_x flags) sk1 sk2 with - |None, Success i' -> - Success (solve_refl (fun flags p env i pbty a1 a2 -> - let flags = - match p with - | TypeUnification -> default_flags env - | TermUnification -> flags - in - is_success (evar_conv_x flags env i pbty a1 a2)) flags - env i' (position_problem true pbty) sp1 al1 al2) - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (i,NotSameArgSize) - else UnifFailure (i,NotSameHead) - and f3 i = miller true (sp1,al1) appr1 appr2 i - and f4 i = miller false (sp2,al2) appr2 appr1 i - and f5 i = - (* We ensure failure of consuming the stacks does not - propagate an error about unification of the stacks while - the heads themselves cannot be unified, so we return - NotSameHead. *) - match consume true appr1 appr2 i with - | Success _ as x -> x - | UnifFailure _ -> quick_fail i - in - ise_try evd [f1; f2; f3; f4; f5] - - | Flexible ev1, MaybeFlexible v2 -> - flex_maybeflex true ev1 appr1 appr2 v2 - - | MaybeFlexible v1, Flexible ev2 -> - flex_maybeflex false ev2 appr2 appr1 v1 - - | MaybeFlexible v1, MaybeFlexible v2 -> begin - let k1 = EConstr.kind evd term1 in - let k2 = EConstr.kind evd term2 in - begin - match k1, k2 with - | LetIn (na1,b1,t1,c'1), LetIn (na2,b2,t2,c'2) -> - let f1 i = (* FO *) - ise_and i - [(fun i -> ise_try i - [(fun i -> evar_conv_x flags env i CUMUL t1 t2); - (fun i -> evar_conv_x flags env i CUMUL t2 t1)]); - (fun i -> evar_conv_x flags env i CONV b1 b2); - (fun i -> - let b = nf_evar i b1 in - let t = nf_evar i t1 in - let na = Nameops.Name.pick_annot na1 na2 in - evar_conv_x flags (push_rel (RelDecl.LocalDef (na,b,t)) env) i pbty c'1 c'2); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2) - in evar_eqappr_x flags env i pbty out1 out2 - in - ise_try evd [f1; f2] - - | Proj (p, _, c), Proj (p', _, c') when QProjection.Repr.equal env (Projection.repr p) (Projection.repr p') -> - let f1 i = - ise_and i - [(fun i -> evar_conv_x flags env i CONV c c'); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - and f2 i = - let out1 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v1,sk1) - and out2 = whd_betaiota_deltazeta_for_iota_state flags.open_ts env i (v2,sk2) - in evar_eqappr_x flags env i pbty out1 out2 - in - ise_try evd [f1; f2] - - (* Catch the p.c ~= p c' cases *) - | Proj (p,_,c), Const (p',u) when QConstant.equal env (Projection.constant p) p' -> - let res = - try Some (destApp evd (Retyping.expand_projection env evd p c [])) - with Retyping.RetypeError _ -> None - in - (match res with - | Some (f1,args1) -> - evar_eqappr_x flags env evd pbty (f1,Stack.append_app args1 sk1) - appr2 - | None -> UnifFailure (evd,NotSameHead)) - - | Const (p,u), Proj (p',_,c') when QConstant.equal env p (Projection.constant p') -> - let res = - try Some (destApp evd (Retyping.expand_projection env evd p' c' [])) - with Retyping.RetypeError _ -> None - in - (match res with - | Some (f2,args2) -> - evar_eqappr_x flags env evd pbty appr1 (f2,Stack.append_app args2 sk2) - | None -> UnifFailure (evd,NotSameHead)) - - | _, _ -> - let f1 i = - (* Gather the universe constraints that would make term1 and term2 equal. - If these only involve unifications of flexible universes to other universes, - allow this identification (first-order unification of universes). Otherwise - fallback to unfolding. - *) - let univs = EConstr.eq_constr_universes env evd term1 term2 in - match univs with - | Some univs -> - ise_and i [(fun i -> - try Success (Evd.add_universe_constraints i univs) - with UniversesDiffer -> UnifFailure (i,NotSameHead) - | UGraph.UniverseInconsistency p -> UnifFailure (i, UnifUnivInconsistency p)); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - | None -> - UnifFailure (i,NotSameHead) - and f2 i = - (match try_simplify_proj_construct flags env evd v1 k1 sk1, try_simplify_proj_construct flags env evd v2 k2 sk2 with - | Some x1, Some x2 -> UnifFailure (i,NoCanonicalStructure) - | Some x1, None -> UnifFailure (i,NoCanonicalStructure) - | None, Some x2 -> UnifFailure (i,NoCanonicalStructure) - | _, _ -> (try - if not flags.with_cs then raise Not_found - else conv_record flags env - (try check_conv_record env i appr1 appr2 - with Not_found -> begin match (apply_hooks env i appr1 appr2) with - | Some r -> r - | None -> begin try check_conv_record env i appr2 appr1 - with Not_found -> begin match (apply_hooks env i appr2 appr1) with - | Some r -> r - | None -> raise Not_found - end end end) - with Not_found -> UnifFailure (i,NoCanonicalStructure))) - and f3 i = - (* heuristic: unfold second argument first, exception made - if the first argument is a beta-redex (expand a constant - only if necessary) or the second argument is potentially - usable as a canonical projection or canonical value *) - let rec is_unnamed (hd, args) = match EConstr.kind i hd with - | (Var _|Construct _|Ind _|Const _|Prod _|Sort _|Int _ |Float _|Array _) -> - Stack.not_purely_applicative args - | (CoFix _|Meta _|Rel _)-> true - | Evar _ -> Stack.not_purely_applicative args - (* false (* immediate solution without Canon Struct *)*) - | Lambda _ -> assert (match args with [] -> true | _ -> false); true - | LetIn (_,b,_,c) -> is_unnamed - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i (subst1 b c, args)) - | Fix _ -> true (* Partially applied fix can be the result of a whd call *) - | Proj (p, _, _) -> Projection.unfolded p || Stack.not_purely_applicative args - | Case _ | App _| Cast _ -> assert false in - let rhs_is_stuck_and_unnamed () = - let applicative_stack = fst (Stack.strip_app sk2) in - is_unnamed - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i (v2, applicative_stack)) in - let rhs_is_already_stuck = - rhs_is_already_stuck || rhs_is_stuck_and_unnamed () in - - if (EConstr.isLambda i term1 || rhs_is_already_stuck) - && (not (Stack.not_purely_applicative sk1)) then - evar_eqappr_x ~rhs_is_already_stuck flags env i pbty - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i(v1,sk1)) - appr2 - else - evar_eqappr_x flags env i pbty appr1 - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i (v2,sk2)) - in - ise_try evd [f1; f2; f3] - end end - - | Rigid, Rigid when EConstr.isLambda evd term1 && EConstr.isLambda evd term2 -> - let (na1,c1,c'1) = EConstr.destLambda evd term1 in - let (na2,c2,c'2) = EConstr.destLambda evd term2 in - ise_and evd - [(fun i -> evar_conv_x flags env i CONV c1 c2); - (fun i -> - let c = nf_evar i c1 in - let na = Nameops.Name.pick_annot na1 na2 in - evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i CONV c'1 c'2); - (* When in modulo_betaiota = false case, lambda's are not reduced *) - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - - | Flexible ev1, Rigid -> flex_rigid true ev1 appr1 appr2 - | Rigid, Flexible ev2 -> flex_rigid false ev2 appr2 appr1 - - | MaybeFlexible v1, Rigid -> - let k1 = EConstr.kind evd term1 in begin - let () = debug_unification (fun () -> Pp.(v 0 (str "v1 maybeflexible against rigid" ++ !pr_econstr env evd v1 ++ cut ()))) in - match try_simplify_proj_construct flags env evd v1 k1 sk1 with - | Some x1 -> evar_eqappr_x flags env evd pbty x1 appr2 - | None -> - let f3 i = - (try - if not flags.with_cs then raise Not_found - else conv_record flags env ( - try check_conv_record env i appr1 appr2 with - | Not_found -> begin match apply_hooks env i appr1 appr2 with - | Some r -> r - | None -> raise Not_found - end) - with Not_found -> UnifFailure (i,NoCanonicalStructure)) - - and f4 i = - evar_eqappr_x flags env i pbty - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i (v1,sk1)) - appr2 - in - ise_try evd [f3; f4] - end - - | Rigid, MaybeFlexible v2 -> - let k2 = EConstr.kind evd term2 in begin - let () = debug_unification (fun () -> Pp.(v 0 (str "rigid against v2 maybeflexible" ++ !pr_econstr env evd v2 ++ cut ()))) in - match try_simplify_proj_construct flags env evd v2 k2 sk2 with - | Some x2 -> let () = debug_unification (fun () -> Pp.(v 0 (str "reduced to" ++ !pr_econstr env evd (let (x, _) = x2 in x)))) in evar_eqappr_x flags env evd pbty appr1 x2 - | None -> - let f3 i = - (try - if not flags.with_cs then raise Not_found - else conv_record flags env ( - try check_conv_record env i appr2 appr1 with - | Not_found -> begin let () = debug_unification (fun () -> Pp.(v 0 (str "ask cs hook"))) in match apply_hooks env i appr2 appr1 with - | Some r -> r - | None -> raise Not_found - end - | e -> let () = Feedback.msg_info Pp.(str "cs hook crashed") in failwith "argh") - with Not_found -> UnifFailure (i,NoCanonicalStructure)) - and f4 i = - evar_eqappr_x flags env i pbty appr1 - (whd_betaiota_deltazeta_for_iota_state - flags.open_ts env i (v2,sk2)) - in - ise_try evd [f3; f4] - end - - (* Eta-expansion *) - | Rigid, _ when isLambda evd term1 && (* if ever ill-typed: *) List.is_empty sk1 -> - eta_lambda env evd true term1 (term2,sk2) - - | _, Rigid when isLambda evd term2 && (* if ever ill-typed: *) List.is_empty sk2 -> - eta_lambda env evd false term2 (term1,sk1) - - | Rigid, Rigid -> begin - match EConstr.kind evd term1, EConstr.kind evd term2 with - - | Sort s1, Sort s2 when app_empty -> - (try - let evd' = - if pbty == CONV - then Evd.set_eq_sort env evd s1 s2 - else Evd.set_leq_sort env evd s1 s2 - in Success evd' - with UGraph.UniverseInconsistency p -> - UnifFailure (evd,UnifUnivInconsistency p) - | e when CErrors.noncritical e -> UnifFailure (evd,NotSameHead)) - - | Prod (n1,c1,c'1), Prod (n2,c2,c'2) when app_empty -> - ise_and evd - [(fun i -> evar_conv_x flags env i CONV c1 c2); - (fun i -> - let c = nf_evar i c1 in - let na = Nameops.Name.pick_annot n1 n2 in - evar_conv_x flags (push_rel (RelDecl.LocalAssum (na,c)) env) i pbty c'1 c'2)] - - | Rel x1, Rel x2 -> - if Int.equal x1 x2 then - exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 - else UnifFailure (evd,NotSameHead) - - | Var var1, Var var2 -> - if Id.equal var1 var2 then - exact_ise_stack2 env evd (evar_conv_x flags) sk1 sk2 - else UnifFailure (evd,NotSameHead) - - | Const _, Const _ - | Ind _, Ind _ - | Construct _, Construct _ - | Int _, Int _ - | Float _, Float _ - | Array _, Array _ -> - rigids env evd sk1 term1 sk2 term2 - - | Evar (sp1,al1), Evar (sp2,al2) -> (* Frozen evars *) - if Evar.equal sp1 sp2 then - match ise_stack2 false env evd (evar_conv_x flags) sk1 sk2 with - |None, Success i' -> - let al1 = Evd.expand_existential i' (sp1, al1) in - let al2 = Evd.expand_existential i' (sp2, al2) in - ise_inst2 i' (fun i' -> evar_conv_x flags env i' CONV) al1 al2 - |_, (UnifFailure _ as x) -> x - |Some _, _ -> UnifFailure (evd,NotSameArgSize) - else UnifFailure (evd,NotSameHead) - - | Construct u, _ -> - eta_constructor flags env evd u sk1 (term2,sk2) - - | _, Construct u -> - eta_constructor flags env evd u sk2 (term1,sk1) - - | Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *) - if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then - ise_and evd [ - (fun i -> ise_array2 i (fun i' -> evar_conv_x flags env i' CONV) tys1 tys2); - (fun i -> ise_array2 i (fun i' -> evar_conv_x flags (push_rec_types recdef1 env) i' CONV) bds1 bds2); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2)] - else UnifFailure (evd, NotSameHead) - - | CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) -> - if Int.equal i1 i2 then - ise_and evd - [(fun i -> ise_array2 i - (fun i -> evar_conv_x flags env i CONV) tys1 tys2); - (fun i -> ise_array2 i - (fun i -> evar_conv_x flags (push_rec_types recdef1 env) i CONV) - bds1 bds2); - (fun i -> exact_ise_stack2 env i - (evar_conv_x flags) sk1 sk2)] - else UnifFailure (evd,NotSameHead) - - | (Meta _, _) | (_, Meta _) -> - begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with - |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x flags env i' CONV term1 term2 - |Some (sk1',sk2'), Success i' -> evar_conv_x flags env i' CONV (Stack.zip i' (term1,sk1')) (Stack.zip i' (term2,sk2')) - end - - | Proj (p1,_,c1), Proj(p2,_,c2) when QProjection.Repr.equal env (Projection.repr p1) (Projection.repr p2) -> - begin match ise_stack2 true env evd (evar_conv_x flags) sk1 sk2 with - |_, (UnifFailure _ as x) -> x - |None, Success i' -> evar_conv_x flags env i' CONV c1 c2 - |Some _, Success _ -> UnifFailure (evd,NotSameHead) - end - - (* Catch the c.(p) ~= p c' cases *) - | Proj (p1,_,c1), Const (p2,_) when QConstant.equal env (Projection.constant p1) p2 -> - let c1 = - try Some (destApp evd (Retyping.expand_projection env evd p1 c1 [])) - with Retyping.RetypeError _ -> None - in - begin match c1 with - | Some (c1,new_args) -> - rigids env evd (Stack.append_app new_args sk1) c1 sk2 term2 - | None -> UnifFailure (evd,NotSameHead) - end - - | Const (p1,_), Proj (p2,_,c2) when QConstant.equal env p1 (Projection.constant p2) -> - let c2 = - try Some (destApp evd (Retyping.expand_projection env evd p2 c2 [])) - with Retyping.RetypeError _ -> None - in - begin match c2 with - | Some (c2,new_args) -> - rigids env evd sk1 term1 (Stack.append_app new_args sk2) c2 - | None -> UnifFailure (evd,NotSameHead) - end - - | (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Float _ | Array _ | Evar _ | Lambda _), _ -> - UnifFailure (evd,NotSameHead) - | _, (Ind _ | Sort _ | Prod _ | CoFix _ | Fix _ | Rel _ | Var _ | Const _ | Int _ | Array _ | Evar _ | Lambda _) -> - UnifFailure (evd,NotSameHead) - | Case _, _ -> UnifFailure (evd,NotSameHead) - | Proj _, _ -> UnifFailure (evd,NotSameHead) - | (App _ | Cast _), _ -> assert false - | LetIn _, _ -> assert false - end - -and conv_record flags env (evd,(h,h2),c,bs,(params,params1),(us,us2),(sk1,sk2),c1,(n,t2)) = - (* Tries to unify the states - - (proji params1 c1 | sk1) = (proji params2 (c (?xs:bs)) | sk2) - - and the terms - - h us = h2 us2 - - where - - c = the constant for the canonical structure (i.e. some term of the form - fun (xs:bs) => Build_R params v1 .. vi-1 (h us) vi+1 .. vn) - bs = the types of the parameters of the canonical structure - c1 = the main argument of the canonical projection - sk1, sk2 = the surrounding stacks of the conversion problem - params1, params2 = the params of the projection (empty if a primitive proj) - - knowing that - - (proji params1 c1 | sk1) = (h2 us2 | sk2) - - had to be initially resolved - *) - if Reductionops.Stack.compare_shape sk1 sk2 then - let (evd',ks,_,test) = - List.fold_left - (fun (i,ks,m,test) b -> - if match n with Some n -> Int.equal m n | None -> false then - let ty = Retyping.get_type_of env i t2 in - let test i = evar_conv_x flags env i CUMUL ty (substl ks b) in - (i,t2::ks, m-1, test) - else - let dloc = Loc.tag Evar_kinds.InternalHole in - let (i', ev) = Evarutil.new_evar env i ~src:dloc (substl ks b) in - (i', ev :: ks, m - 1,test)) - (evd,[],List.length bs,fun i -> Success i) bs - in - let app = mkApp (c, Array.rev_of_list ks) in - ise_and evd' - [(fun i -> - ise_list2 i - (fun i' x1 x -> evar_conv_x flags env i' CONV x1 (substl ks x)) - params1 params); - (fun i -> - ise_list2 i - (fun i' u1 u -> evar_conv_x flags env i' CONV u1 (substl ks u)) - us2 us); - (fun i -> evar_conv_x flags env i CONV c1 app); - (fun i -> exact_ise_stack2 env i (evar_conv_x flags) sk1 sk2); - test; - (fun i -> evar_conv_x flags env i CONV h2 (fst (decompose_app i (substl ks h))))] - else UnifFailure(evd,(*dummy*)NotSameHead) - -and eta_constructor flags env evd ((ind, i), u) sk1 (term2,sk2) = - (* reduces an equation == to the - equations [arg_i = Proj_i (sk2[term2])] where [sk1] is [params args] *) - let open Declarations in - let mib = lookup_mind (fst ind) env in - match get_projections env ind with - | Some projs when mib.mind_finite == BiFinite -> - let pars = mib.mind_nparams in - begin match Stack.list_of_app_stack sk1 with - | None -> UnifFailure (evd,NotSameHead) - | Some l1 -> - (try - let l1' = List.skipn pars l1 in - let l2' = - let term = Stack.zip evd (term2,sk2) in - List.map (fun (p,r) -> - let r = UVars.subst_instance_relevance (Unsafe.to_instance u) r in - EConstr.mkProj (Projection.make p false, r, term)) - (Array.to_list projs) - in - let f i t1 t2 = evar_conv_x { flags with with_cs = false } env i CONV t1 t2 in - ise_list2 evd f l1' l2' - with - | Failure _ -> - (* List.skipn: partially applied constructor *) - UnifFailure(evd,NotSameHead)) - end - | _ -> UnifFailure (evd,NotSameHead) - -let evar_conv_x flags = evar_conv_x flags - -let evar_unify = conv_fun evar_conv_x - -let evar_conv_hook = ref evar_conv_x - -let evar_conv_x flags = !evar_conv_hook flags - -let set_evar_conv f = evar_conv_hook := f - - -(* We assume here |l1| <= |l2| *) - -let first_order_unification flags env evd (ev1,l1) (term2,l2) = - let (deb2,rest2) = Array.chop (Array.length l2-Array.length l1) l2 in - ise_and evd - (* First compare extra args for better failure message *) - [(fun i -> ise_array2 i (fun i -> evar_conv_x flags env i CONV) rest2 l1); - (fun i -> - (* Then instantiate evar unless already done by unifying args *) - let t2 = mkApp(term2,deb2) in - if is_defined i (fst ev1) then - evar_conv_x flags env i CONV t2 (mkEvar ev1) - else - solve_simple_eqn ~choose:true ~imitate_defs:false - evar_unify flags env i (None,ev1,t2))] - -let choose_less_dependent_instance evd term (evk, args) = - let evi = Evd.find_undefined evd evk in - let rec get_subst accu decls args = match decls, SList.view args with - | [], Some _ | _ :: _, None -> assert false - | [], None -> accu - | decl :: decls, Some (arg, args) -> - let accu = get_subst accu decls args in - let arg = match arg with None -> mkVar (NamedDecl.get_id decl) | Some a -> a in - if EConstr.eq_constr evd arg term then NamedDecl.get_id decl :: accu - else accu - in - let subst = get_subst [] (evar_filtered_context evi) args in - match subst with - | [] -> None - | id :: _ -> Some (Evd.define evk (mkVar id) evd) - -type occurrence_match_test = - env -> evar_map -> constr -> constr -> bool * evar_map - -type occurrence_selection = - | AtOccurrences of Locus.occurrences - | Unspecified of Abstraction.abstraction - -type occurrences_selection = - occurrence_match_test * occurrence_selection list - -let default_occurrence_selection = Unspecified Abstraction.Imitate - -let default_occurrence_test ~allowed_evars ts env sigma c pat = - let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in - match evar_conv_x flags env sigma CONV c pat with - | Success sigma -> true, sigma - | UnifFailure _ -> false, sigma - -let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n = - (default_occurrence_test ~allowed_evars ts, - List.init n (fun _ -> default_occurrence_selection)) - -let occur_evars sigma evs c = - if Evar.Set.is_empty evs then false - else - let rec occur_rec c = match EConstr.kind sigma c with - | Evar (sp, args) -> - if Evar.Set.mem sp evs then raise Occur - else SList.Skip.iter occur_rec args - | _ -> EConstr.iter sigma occur_rec c - in - try occur_rec c; false with Occur -> true - -let apply_on_subterm env evd fixed f test c t = - let prc env evd = Termops.Internal.print_constr_env env evd in - let evdref = ref evd in - let fixedref = ref fixed in - let rec applyrec (env,(k,c) as acc) t = - if occur_evars !evdref !fixedref t then - match EConstr.kind !evdref t with - | Evar (evk, args) -> - if Evar.Set.mem evk !fixedref then t - else - let args = Evd.expand_existential !evdref (evk, args) in - let args = List.Smart.map (applyrec acc) args in - EConstr.mkLEvar !evdref (evk, args) - | _ -> map_constr_with_binders_left_to_right env !evdref - (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc t - else - (debug_ho_unification (fun () -> - Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t)); - let b, evd = - try test env !evdref c t - with e when CErrors.noncritical e -> assert false in - if b then (debug_ho_unification (fun () -> Pp.str "succeeded"); - let evd', fixed, t' = f !evdref !fixedref k t in - fixedref := fixed; - evdref := evd'; t') - else ( - debug_ho_unification (fun () -> Pp.str "failed"); - map_constr_with_binders_left_to_right env !evdref - (fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c))) - applyrec acc t)) - in - let t' = applyrec (env,(0,c)) t in - !evdref, !fixedref, t' - -let filter_possible_projections evd c ty ctxt args = - (* Since args in the types will be replaced by holes, we count the - fv of args to have a well-typed filter; don't know how necessary - it is however to have a well-typed filter here *) - let args = Array.of_list args in - let fv1 = free_rels evd (mkApp (c,args)) (* Hack: locally untyped *) in - let fv2 = collect_vars evd (mkApp (c,args)) in - let len = Array.length args in - let tyvars = collect_vars evd ty in - List.map_i (fun i decl -> - let () = assert (i < len) in - let a = Array.unsafe_get args i in - (match decl with - | NamedDecl.LocalAssum _ -> false - | NamedDecl.LocalDef (_,c,_) -> not (isRel evd c || isVar evd c)) || - a == c || - (* Here we make an approximation, for instance, we could also be *) - (* interested in finding a term u convertible to c such that a occurs *) - (* in u *) - isRel evd a && Int.Set.mem (destRel evd a) fv1 || - isVar evd a && Id.Set.mem (destVar evd a) fv2 || - Id.Set.mem (NamedDecl.get_id decl) tyvars) - 0 ctxt - -let solve_evars = ref (fun _ -> failwith "solve_evars not installed") -let set_solve_evars f = solve_evars := f - -(* We solve the problem env_rhs |- ?e[u1..un] = rhs knowing - * x1:T1 .. xn:Tn |- ev : ty - * by looking for a maximal well-typed abtraction over u1..un in rhs - * - * We first build C[e11..e1p1,..,en1..enpn] obtained from rhs by replacing - * all occurrences of u1..un by evars eij of type Ti' where itself Ti' has - * been obtained from the type of ui by also replacing all occurrences of - * u1..ui-1 by evars. - * - * Then, we use typing to infer the relations between the different - * occurrences. If some occurrence is still unconstrained after typing, - * we instantiate successively the unresolved occurrences of un by xn, - * of un-1 by xn-1, etc [the idea comes from Chung-Kil Hur, that he - * used for his Heq plugin; extensions to several arguments based on a - * proposition from Dan Grayson] - *) - -let check_selected_occs env sigma c occ occs = - let notfound = - match occs with - | AtOccurrences occs -> - (match occs with - | Locus.AtLeastOneOccurrence -> occ == 1 - | Locus.AllOccurrences -> false - | Locus.AllOccurrencesBut l -> List.last l > occ - | Locus.OnlyOccurrences l -> List.last l > occ - | Locus.NoOccurrences -> false) - | Unspecified abstract -> false - in if notfound then - raise (PretypeError (env,sigma,NoOccurrenceFound (c,None))) - else () - -(* Error local to the module *) -exception TypingFailed of evar_map - -let set_of_evctx l = - List.fold_left (fun s decl -> Id.Set.add (NamedDecl.get_id decl) s) Id.Set.empty l - -(** Weaken the existentials so that they can be typed in sign and raise - an error if the term otherwise mentions variables not bound in sign. *) -let thin_evars env sigma sign c = - let sigma = ref sigma in - let ctx = set_of_evctx sign in - let rec applyrec (env,acc) t = - match kind !sigma t with - | Evar (ev, args) -> - let evi = Evd.find_undefined !sigma ev in - let args = Evd.expand_existential !sigma (ev, args) in - let filter = List.map (fun c -> Id.Set.subset (collect_vars !sigma c) ctx) args in - let filter = Filter.make filter in - let candidates = evar_candidates evi in - let evd, ev = restrict_evar !sigma ev filter candidates in - sigma := evd; whd_evar !sigma t - | Var id -> - if not (Id.Set.mem id ctx) then raise (TypingFailed !sigma) - else t - | _ -> - map_constr_with_binders_left_to_right env !sigma - (fun d (env,acc) -> (push_rel d env, acc+1)) - applyrec (env,acc) t - in - let c' = applyrec (env,0) c in - (!sigma, c') - -let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs = - try - let evi = Evd.find_undefined evd evk in - let evi = nf_evar_info evd evi in - let env_evar_unf = evar_env env_rhs evi in - let env_evar = evar_filtered_env env_rhs evi in - let sign = named_context_val env_evar in - let ctxt = evar_filtered_context evi in - debug_ho_unification (fun () -> - Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++ - str"env evars: " ++ Termops.Internal.print_env env_evar)); - let args = Evd.expand_existential evd (evk, args) in - let args = List.map (nf_evar evd) args in - let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in - let rhs = nf_evar evd rhs in - if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd); - (* Ensure that any progress made by Typing.e_solve_evars will not contradict - the solution we are trying to build here by adding the problem as a constraint. *) - let evd = Evarutil.add_unification_pb (CONV,env_rhs,mkLEvar evd (evk, args),rhs) evd in - let prc env evd c = Termops.Internal.print_constr_env env evd c in - let rec make_subst = function - | decl'::ctxt', c::l, occs::occsl when isVarId evd (NamedDecl.get_id decl') c -> - begin match occs with - | AtOccurrences loc when not (Locusops.is_all_occurrences loc) -> - user_err Pp.(str "Cannot force abstraction on identity instance.") - | _ -> - make_subst (ctxt',l,occsl) - end - | decl'::ctxt', c::l, occs::occsl -> - let id = NamedDecl.get_annot decl' in - let t = NamedDecl.get_type decl' in - let evs = ref [] in - let c = nf_evar evd c in - (* ty is in env_rhs now *) - let ty = replace_vars evd argsubst t in - let filter' = filter_possible_projections evd c (nf_evar evd ty) ctxt args in - (id,t,c,ty,evs,Filter.make filter',occs) :: make_subst (ctxt',l,occsl) - | _, _, [] -> [] - | _ -> anomaly (Pp.str "Signature or instance are shorter than the occurrences list.") - in - let rec set_holes env_rhs evd fixed rhs = function - | (id,idty,c,cty,evsref,filter,occs)::subst -> - let c = nf_evar evd c in - debug_ho_unification (fun () -> - Pp.(str"set holes for: " ++ - prc env_rhs evd (mkVar id.binder_name) ++ spc () ++ - prc env_rhs evd c ++ str" in " ++ - prc env_rhs evd rhs)); - let occ = ref 1 in - let set_var evd fixed k inst = - let oc = !occ in - debug_ho_unification (fun () -> - Pp.(str"Found one occurrence" ++ fnl () ++ - str"cty: " ++ prc env_rhs evd c)); - incr occ; - match occs with - | AtOccurrences occs -> - if Locusops.is_selected oc occs then evd, fixed, mkVar id.binder_name - else evd, fixed, inst - | Unspecified prefer_abstraction -> - let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in - let evty = nf_evar evd evty in - debug_ho_unification (fun () -> - Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++ - str" of type: " ++ prc env_evar evd evty ++ - str " for " ++ prc env_rhs evd c)); - (* Allow any type lower than the variable's type as the - abstracted subterm might have a smaller type, which could be - crucial to make the surrounding context typecheck. *) - let evd, evty = - if isArity evd evty then - refresh_universes ~status:Evd.univ_flexible (Some true) - env_evar_unf evd evty - else evd, evty in - let (evd, evk) = new_pure_evar sign evd evty ~filter in - let EvarInfo evi = Evd.find evd evk in - let instance = Evd.evar_identity_subst evi in - let fixed = Evar.Set.add evk fixed in - evsref := (evk,evty,inst,prefer_abstraction)::!evsref; - evd, fixed, mkEvar (evk, instance) - in - let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in - debug_ho_unification (fun () -> - Pp.(str"abstracted: " ++ prc env_rhs evd rhs')); - let () = check_selected_occs env_rhs evd c !occ occs in - let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in - set_holes env_rhs' evd fixed rhs' subst - | [] -> evd, fixed, rhs in - - let subst = make_subst (ctxt,args,argoccs) in - - let evd, _, rhs' = set_holes env_rhs evd Evar.Set.empty rhs subst in - let rhs' = nf_evar evd rhs' in - (* Thin evars making the term typable in env_evar *) - let evd, rhs' = thin_evars env_evar evd ctxt rhs' in - (* We instantiate the evars of which the value is forced by typing *) - debug_ho_unification (fun () -> - Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++ - str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); - let evd,rhs' = - try !solve_evars env_evar evd rhs' - with e when Pretype_errors.precatchable_exception e -> - (* Could not revert all subterms *) - raise (TypingFailed evd) in - let rhs' = nf_evar evd rhs' in - (* We instantiate the evars of which the value is forced by typing *) - debug_ho_unification (fun () -> - Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++ - str"evars: " ++ pr_evar_map (Some 0) env_evar evd)); - - let rec abstract_free_holes evd = function - | (id,idty,c,cty,evsref,_,_)::l -> - let id = id.binder_name in - let c = nf_evar evd c in - debug_ho_unification (fun () -> - Pp.(str"abstracting: " ++ - prc env_rhs evd (mkVar id) ++ spc () ++ - prc env_rhs evd c)); - let rec force_instantiation evd = function - | (evk,evty,inst,abstract)::evs -> - let evk = Option.default evk (Evarutil.advance evd evk) in - let evd = - if is_undefined evd evk then - (* We try abstraction or concretisation for *) - (* this unconstrained occurrence *) - (* and we use typing to propagate this instantiation *) - (* We avoid making an arbitrary choice by leaving candidates *) - (* if both can work *) - let evi = Evd.find_undefined evd evk in - let vid = mkVar id in - let candidates = [inst; vid] in - try - let evd, ev = Evarutil.restrict_evar evd evk (Evd.evar_filter evi) (Some candidates) in - let evi = Evd.find_undefined evd ev in - (match evar_candidates evi with - | Some [t] -> - if not (noccur_evar env_rhs evd ev t) then - raise (TypingFailed evd); - instantiate_evar evar_unify flags env_rhs evd ev t - | Some l when abstract = Abstraction.Abstract && - List.exists (fun c -> isVarId evd id c) l -> - instantiate_evar evar_unify flags env_rhs evd ev vid - | _ -> evd) - with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ -> - user_err (Pp.str "Cannot find an instance.") - else - ((debug_ho_unification (fun () -> - let EvarInfo evi = Evd.find evd evk in - let env = Evd.evar_env env_rhs evi in - Pp.(str"evar is defined: " ++ - int (Evar.repr evk) ++ spc () ++ - prc env evd (match evar_body evi with Evar_defined c -> c - | Evar_empty -> assert false))); - evd)) - in force_instantiation evd evs - | [] -> abstract_free_holes evd l - in force_instantiation evd !evsref - | [] -> - if Evd.is_defined evd evk then - (* Can happen due to dependencies: instantiating evars in the arguments of evk might - instantiate evk itself. *) - (debug_ho_unification (fun () -> - begin - let EvarInfo evi = Evd.find evd evk in - let evenv = evar_env env_rhs evi in - let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in - Pp.(str"evar was defined already as: " ++ prc evenv evd body) - end); - evd) - else - try - let evi = Evd.find_undefined evd evk in - let evenv = evar_env env_rhs evi in - let rhs' = nf_evar evd rhs' in - debug_ho_unification (fun () -> - Pp.(str"abstracted type before second solve_evars: " ++ - prc evenv evd rhs')); - (* solve_evars is not commuting with nf_evar, because restricting - an evar might provide a more specific type. *) - let evd, _ = !solve_evars evenv evd rhs' in - debug_ho_unification (fun () -> - Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'))); - let flags = default_flags_of TransparentState.full in - Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs' - with IllTypedInstance _ -> raise (TypingFailed evd) - in - let evd = abstract_free_holes evd subst in - evd, true - with TypingFailed evd -> evd, false - -let default_evar_selection flags evd (ev,args) = - let evi = Evd.find_undefined evd ev in - let args = Evd.expand_existential evd (ev, args) in - let rec aux args abs = - match args, abs with - | _ :: args, a :: abs -> - let spec = Unspecified a in - spec :: aux args abs - | l, [] -> List.map (fun _ -> default_occurrence_selection) l - | [], _ :: _ -> assert false - in aux args (Evd.evar_abstract_arguments evi) - -let second_order_matching_with_args flags env evd with_ho pbty ev l t = - if with_ho then - let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in - let argoccs = default_evar_selection flags evd ev in - let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in - let evd, b = - try second_order_matching flags env evd ev (test,argoccs) t - with PretypeError (_, _, NoOccurrenceFound _) -> evd, false - in - if b then Success evd - else - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) - else - let pb = (pbty,env,mkApp(mkEvar ev,l),t) in - UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) - -let is_beyond_capabilities = function - | CannotSolveConstraint (pb,ProblemBeyondCapabilities) -> true - | _ -> false - -let is_constant_instance sigma (evk, args) alias = - let args = Evd.expand_existential sigma (evk, args) in - List.for_all (fun a -> EConstr.eq_constr sigma a alias || isEvar sigma a) - (remove_instance_local_defs sigma evk args) - -let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 = - let t1 = apprec_nohdbeta flags env evd (whd_head_evar evd t1) in - let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in - let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in - let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in - let () = debug_unification (fun () -> - Pp.(v 0 (str "Heuristic:" ++ spc () ++ - Termops.Internal.print_constr_env env evd t1 ++ cut () ++ - Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in - let app_empty = Array.is_empty l1 && Array.is_empty l2 in - match EConstr.kind evd term1, EConstr.kind evd term2 with - | Evar (evk1,args1), (Rel _|Var _) when app_empty - && is_evar_allowed flags evk1 - && is_constant_instance evd (evk1, args1) term2 -> - (* The typical kind of constraint coming from pattern-matching return - type inference *) - (match choose_less_dependent_instance evd term2 (evk1, args1) with - | Some evd -> Success evd - | None -> - let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | (Rel _|Var _), Evar (evk2,args2) when app_empty - && is_evar_allowed flags evk2 - && is_constant_instance evd (evk2, args2) term1 -> - (* The typical kind of constraint coming from pattern-matching return - type inference *) - (match choose_less_dependent_instance evd term1 (evk2, args2) with - | Some evd -> Success evd - | None -> - let reason = ProblemBeyondCapabilities in - UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) - | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> - let f flags ontype env evd pbty x y = - let reds = - match ontype with - | TypeUnification -> TransparentState.full - | TermUnification -> flags.open_ts - in is_fconv ~reds pbty env evd x y - in - Success (solve_refl ~can_drop:true f flags env evd - (position_problem true pbty) evk1 args1 args2) - | Evar (evk1,_ as ev1), Evar ev2 when app_empty -> - (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *) - (try - Success (solve_evar_evar ~force:true - (evar_define evar_unify flags ~choose:true) - evar_unify flags env evd - (position_problem true pbty) ev1 ev2) - with IllTypedInstance (env,evd,t,u) -> - UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))) - | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 -> - (* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *) - (* and otherwise second-order matching *) - ise_try evd - [(fun evd -> first_order_unification flags env evd (ev1,l1) appr2); - (fun evd -> - second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)] - | _,Evar ev2 when is_evar_allowed flags (fst ev2) && Array.length l2 <= Array.length l1 -> - (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) - (* and otherwise second-order matching *) - ise_try evd - [(fun evd -> first_order_unification flags env evd (ev2,l2) appr1); - (fun evd -> - second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)] - | Evar ev1,_ when is_evar_allowed flags (fst ev1) -> - (* Try second-order pattern-matching *) - second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2 - | _,Evar ev2 when is_evar_allowed flags (fst ev2) -> - (* Try second-order pattern-matching *) - second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1 - | _ -> - (* Some head evar have been instantiated, or unknown kind of problem *) - evar_conv_x flags env evd pbty t1 t2 - -let error_cannot_unify env evd pb ?reason t1 t2 = - Pretype_errors.error_cannot_unify - ?loc:(loc_of_conv_pb evd pb) env - evd ?reason (t1, t2) - -let check_problems_are_solved env evd = - match snd (extract_all_conv_pbs evd) with - | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2 - | _ -> () - -let rec solve_unconstrained_evars_with_candidates flags env evd = - (* max_undefined is supposed to return the most recent, hence - possibly most dependent evar *) - match Evd.max_undefined_with_candidates evd with - | None -> evd - | Some evk -> - let ev_info = Evd.find_undefined evd evk in - let l = match evar_candidates ev_info with - | None -> assert false - | Some l -> l - in - let rec aux = function - | [] -> user_err Pp.(str "Unsolvable existential variables.") - | a::l -> - (* In case of variables, most recent ones come first *) - try - let evd = instantiate_evar evar_unify flags env evd evk a in - match reconsider_unif_constraints evar_unify flags evd with - | Success evd -> solve_unconstrained_evars_with_candidates flags env evd - | UnifFailure _ -> aux l - with - | IllTypedInstance _ -> aux l - | e when Pretype_errors.precatchable_exception e -> aux l in - (* Expected invariant: most dependent solutions come first *) - (* so as to favor progress when used with the refine tactics *) - let evd = aux l in - solve_unconstrained_evars_with_candidates flags env evd - -let solve_unconstrained_impossible_cases env evd = - Evar.Set.fold (fun evk evd' -> - let evd', j = coq_unit_judge env evd' in - let ty = j_type j in - let flags = default_flags env in - instantiate_evar evar_unify flags env evd' evk ty (* should we protect from raising IllTypedInstance? *) - ) - (Evd.get_impossible_case_evars evd) - evd - -let solve_unif_constraints_with_heuristics env - ?(flags=default_flags env) ?(with_ho=false) evd = - let evd = solve_unconstrained_evars_with_candidates flags env evd in - let rec aux evd pbs progress stuck = - match pbs with - | (pbty,env,t1,t2 as pb) :: pbs -> - (match apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 with - | Success evd' -> - let evd' = solve_unconstrained_evars_with_candidates flags env evd' in - let (evd', rest) = extract_all_conv_pbs evd' in - begin match rest with - | [] -> aux evd' pbs true stuck - | l -> - (* Unification got actually stuck, postpone *) - let reason = CannotSolveConstraint (pb,ProblemBeyondCapabilities) in - aux evd pbs progress ((pb, reason):: stuck) - end - | UnifFailure (evd,reason) -> - if is_beyond_capabilities reason then - aux evd pbs progress ((pb,reason) :: stuck) - else aux evd [] false ((pb,reason) :: stuck)) - | _ -> - if progress then aux evd (List.map fst stuck) false [] - else - match stuck with - | [] -> (* We're finished *) evd - | ((pbty,env,t1,t2 as pb), reason) :: _ -> - (* There remains stuck problems *) - Pretype_errors.error_cannot_unify ?loc:(loc_of_conv_pb evd pb) - env evd ~reason (t1, t2) - in - let (evd,pbs) = extract_all_conv_pbs evd in - let heuristic_solved_evd = aux evd pbs false [] in - check_problems_are_solved env heuristic_solved_evd; - solve_unconstrained_impossible_cases env heuristic_solved_evd - -(* Main entry points *) - -exception UnableToUnify of evar_map * unification_error - -let evar_conv_x flags env evd pb x1 x2 : unification_result = - NewProfile.profile "unification" (fun () -> - evar_conv_x flags env evd pb x1 x2) - () - -let unify_delay ?flags env evd t1 t2 = - let flags = - match flags with - | None -> default_flags_of (default_transparent_state env) - | Some flags -> flags - in - match evar_conv_x flags env evd CONV t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) - -let unify_leq_delay ?flags env evd t1 t2 = - let flags = - match flags with - | None -> default_flags_of (default_transparent_state env) - | Some flags -> flags - in - match evar_conv_x flags env evd CUMUL t1 t2 with - | Success evd' -> evd' - | UnifFailure (evd',e) -> raise (UnableToUnify (evd',e)) - -let unify ?flags ?(with_ho=true) env evd cv_pb ty1 ty2 = - let flags = - match flags with - | None -> default_flags_of (default_transparent_state env) - | Some flags -> flags - in - let res = evar_conv_x flags env evd cv_pb ty1 ty2 in - match res with - | Success evd -> - solve_unif_constraints_with_heuristics ~flags ~with_ho env evd - | UnifFailure (evd, reason) -> - raise (PretypeError (env, evd, CannotUnify (ty1, ty2, Some reason))) - -let compare_heads = compare_heads CONV -end -let () = Evarconv.set_evar_conv Evarconv_hacked.evar_conv_x -module Evarconv = Evarconv_hacked -open Elpi -open Elpi_plugin -open Coq_elpi_arg_syntax -open Coq_elpi_vernacular - -let elpi_cs_hook program env sigma (t1, sk1) (t2, sk2) = - let loc = API.Ast.Loc.initial "(unknown)" in - let atts = [] in - let (proji, u), arg = - match Termops.global_app_of_constr sigma t1 with - | (Names.GlobRef.ConstRef proji, u), arg -> (proji, u), arg - | (proji, _), _ -> raise Not_found in - let structure = Structures.Structure.find_from_projection proji in - let params1, c1, extra_args1 = - match arg with - | Some c -> (* A primitive projection applied to c *) - let ty = Retyping.get_type_of ~lax:true env sigma c in - let (i,u), ind_args = - (* Are we sure that ty is not an evar? *) - Inductiveops.find_mrectype env sigma ty - in ind_args, c, sk1 - | None -> - match Reductionops.Stack.strip_n_app structure.nparams sk1 with - | Some (params1, c1, extra_args1) -> (Option.get @@ Reductionops.Stack.list_of_app_stack params1), c1, extra_args1 - | _ -> raise Not_found in - let sk2, extra_args2 = - if Reductionops.Stack.args_size sk2 = Reductionops.Stack.args_size extra_args1 then [], sk2 - else match Reductionops.Stack.strip_n_app (Reductionops.Stack.args_size sk2 - Reductionops.Stack.args_size extra_args1 - 1) sk2 with - | None -> raise Not_found - | Some (l',el,s') -> ((Option.get @@ Reductionops.Stack.list_of_app_stack l') @ [el],s') in - let rhs = Reductionops.Stack.zip sigma (t2, Reductionops.Stack.append_app_list sk2 Reductionops.Stack.empty) in - let sigma, goal = Evarutil.new_evar env sigma (Retyping.get_type_of env sigma c1) in - let goal_evar, _ = EConstr.destEvar sigma goal in - let query ~depth state = - let state, (loc, q), gls = - Coq_elpi_HOAS.goals2query sigma [goal_evar] loc ~main:(Coq_elpi_HOAS.Solve [EConstr.mkApp (EConstr.mkConstU (proji, EConstr.EInstance.empty), Array.of_list params1); rhs]) - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac_econstr ~depth 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 - state, (loc, qatts), gls in - match Interp.get_and_compile program with - | None -> None - | Some (cprogram, _) -> - begin try match Interp.run ~static_check:false 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 - if Evd.is_defined sigma goal_evar then - let lhs = Reductionops.Stack.zip sigma (EConstr.mkConstU (proji, EConstr.EInstance.empty), Reductionops.Stack.append_app_list (params1 @ [goal]) Reductionops.Stack.empty) in - let lhs = Reductionops.whd_const proji env sigma lhs in - let lhs = Reductionops.whd_betaiotazeta env sigma lhs in - let hh, sk1 = EConstr.decompose_app sigma lhs in - let h2, sk2 = EConstr.decompose_app sigma rhs in - let _, params = EConstr.decompose_app sigma (Retyping.get_type_of env sigma goal) in - Some (sigma, (hh, h2), goal, [], (Array.to_list params, params1), (Array.to_list sk1, Array.to_list sk2), (extra_args1, extra_args2), c1, (None, rhs)) - else None - | API.Execute.NoMoreSteps - | API.Execute.Failure -> None - with e -> raise e end - | exception e -> raise e -[%%else] open Elpi open Elpi_plugin open Coq_elpi_arg_syntax @@ -2121,7 +53,6 @@ let elpi_cs_hook program env sigma ((proji, u), params1, c1) (t2, args2) = | API.Execute.NoMoreSteps | API.Execute.Failure -> None end -[%%endif] open Elpi open Elpi_plugin diff --git a/apps/tc/src/coq_elpi_class_tactics_takeover.ml b/apps/tc/src/coq_elpi_class_tactics_takeover.ml index d1ac9a911..cdbcd6f58 100644 --- a/apps/tc/src/coq_elpi_class_tactics_takeover.ml +++ b/apps/tc/src/coq_elpi_class_tactics_takeover.ml @@ -4,1544 +4,6 @@ type aaction = ARm | AAdd | ASet | ANone | AAll -[%%if coq = "8.19"] -open Util -open Names -open Typeclasses - -open Elpi - -module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) - -open Elpi_plugin -open Coq_elpi_utils - -type override = - | AllButFor of Names.GlobRef.Set.t - | Only of Names.GlobRef.Set.t - -type action = - | Set of Coq_elpi_utils.qualified_name * override - | Add of GlobRef.t list - | Rm of GlobRef.t list - -let elpi_solver = Summary.ref ~name:"tc_takeover" None - -let takeover action = - let open Names.GlobRef in - match !elpi_solver, action with - | _, Set(solver,mode) -> - elpi_solver := Some (mode,solver) - | None, (Add _ | Rm _) -> - CErrors.user_err Pp.(str "Set the override program first") - | Some(AllButFor s,solver), Add grl -> - let s' = List.fold_right Set.add grl Set.empty in - elpi_solver := Some (AllButFor (Set.diff s s'),solver) - | Some(AllButFor s,solver), Rm grl -> - let s' = List.fold_right Set.add grl Set.empty in - elpi_solver := Some (AllButFor (Set.union s s'),solver) - | Some(Only s,solver), Add grl -> - let s' = List.fold_right Set.add grl Set.empty in - elpi_solver := Some (Only (Set.union s s'),solver) - | Some(Only s,solver), Rm grl -> - let s' = List.fold_right Set.add grl Set.empty in - elpi_solver := Some (Only (Set.diff s s'),solver) - -let inTakeover = - let cache x = takeover x in - Libobject.(declare_object (superglobal_object_nodischarge "TC_HACK_OVERRIDE" ~cache ~subst:None)) - -let takeover isNone l solver = - let open Names.GlobRef in - let l = List.map Coq_elpi_utils.locate_simple_qualid l in - let s = List.fold_right Set.add l Set.empty in - let mode = if isNone then Only Set.empty else if Set.is_empty s then AllButFor s else Only s in - Lib.add_leaf (inTakeover (Set(solver,mode))) - -let takeover_add l = - let l = List.map Coq_elpi_utils.locate_simple_qualid l in - Lib.add_leaf (inTakeover (Add l)) - -let takeover_rm l = - let l = List.map Coq_elpi_utils.locate_simple_qualid l in - Lib.add_leaf (inTakeover (Rm l)) - -let path2str = List.fold_left (fun acc e -> Printf.sprintf "%s/%s" acc e) "" -let debug_covered_gref = CDebug.create ~name:"tc_current_gref" () - -let covered1 env sigma classes i default= - let ei = Evd.find_undefined sigma i in - let ty = Evd.evar_concl ei in - match Typeclasses.class_of_constr env sigma ty with - | Some (_,(((cl: typeclass),_),_)) -> - let cl_impl = cl.Typeclasses.cl_impl in - debug_covered_gref (fun () -> Pp.(str "The current gref is: " ++ - Printer.pr_global cl_impl ++ str ", with path: " ++ str (path2str (gr2path cl_impl)))); - Names.GlobRef.Set.mem cl_impl classes - | None -> default - -let covered env sigma omode s = - match omode with - | AllButFor blacklist -> - Evar.Set.for_all (fun x -> not (covered1 env sigma blacklist x false)) s - | Only whitelist -> - Evar.Set.for_all (fun x -> covered1 env sigma whitelist x true) s - -let debug_handle_takeover = CDebug.create ~name:"handle_takeover" () - -let elpi_fails program_name = - let open Pp in - let kind = "tactic/command" in - let name = show_qualified_name program_name in - CErrors.user_err (strbrk (String.concat " " [ - "The elpi"; kind; name ; "failed without giving a specific error message."; - "Please report this inconvenience to the authors of the program." - ])) -let solve_TC program env sigma depth unique ~best_effort filter = - let atts = [] in - let glss, _ = Evar.Set.partition (filter sigma) (Evd.get_typeclass_evars sigma) in - let gls = Evar.Set.elements glss in - let xx = - match gls with - | [] -> None - | g::_ -> Evd.evar_source @@ Evd.find_undefined sigma g |> fst in - let loc = Option.cata Coq_elpi_utils.of_coq_loc (API.Ast.Loc.initial "(unknown)") xx in - (* TODO: activate following row to compute new gls - this row to make goal sort in msolve *) - (* let evar_deps = List.map (fun e -> - let evar_info = Evd.find_undefined sigma e in - let evar_deps = Evarutil.filtered_undefined_evars_of_evar_info sigma evar_info in - e, Evar.Set.elements evar_deps - ) gls in *) - (* let g = Graph.build_graph evar_deps in *) - (* let gls = List.map (fun (e: 'a Graph.node) -> e.name ) (Graph.topo_sort g) in *) - let query ~depth state = - let state, (loc, q), gls = - Coq_elpi_HOAS.goals2query sigma gls loc ~main:(Coq_elpi_HOAS.Solve []) - ~in_elpi_tac_arg:Coq_elpi_arg_HOAS.in_elpi_tac ~depth 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 - state, (loc, qatts), gls - in - match Coq_elpi_vernacular.Interp.get_and_compile program with - | None -> assert false - | Some (cprogram,_) -> - match Coq_elpi_vernacular.Interp.run ~static_check:false cprogram (`Fun query) with - | API.Execute.Success solution -> - let sigma, sub_goals, to_shelve = Coq_elpi_HOAS.solution2evd ~eta_contract_solution:true sigma solution glss in - let sigma = Evd.shelve sigma sub_goals in - Some (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)) -> Some(false, sigma) - -let handle_takeover coq_solver env sigma (cl: Intpart.set) = - let t = Unix.gettimeofday () in - let is_elpi, res = - match !elpi_solver with - | Some(omode,solver) when covered env sigma omode cl -> - true, solve_TC solver - | _ -> false, coq_solver in - let is_elpi_text = if is_elpi then "Elpi" else "Coq" in - debug_handle_takeover (fun () -> - let len = (Evar.Set.cardinal cl) in Pp.str @@ - Printf.sprintf "handle_takeover for %s - Class : %d - Time : %f" - is_elpi_text len (Unix.gettimeofday () -. t)); - res, cl - -let assert_same_generated_TC = Goptions.declare_bool_option_and_ref - ~depr:(Deprecation.make ()) ~key:["assert_same_generated_TC"] ~value:false - -(* let same_solution evd1 evd2 i = - let print_discrepancy a b = - CErrors.anomaly Pp.(str - "Discrepancy in same solution: \n" ++ - str"Expected : " ++ a ++ str"\n" ++ - str"Found : " ++ b) - in - let get_types evd t = EConstr.to_constr ~abort_on_undefined_evars:false evd t in - try ( - let t1 = Evd.find evd1 i in - let t2 = Evd.find evd2 i |> Evd.evar_body in - match t1, t2 with - | Evd.Evar_defined t1, Evd.Evar_defined t2 -> - let t1, t2 = get_types evd1 t1, get_types evd2 t2 in - let b = try Constr.eq_constr_nounivs t1 t2 with Not_found -> - CErrors.anomaly Pp.(str "Discrepancy in same solution: problem with universes") in - if (not b) then - print_discrepancy (Printer.pr_constr_env (Global.env ()) evd1 t1) (Printer.pr_constr_env (Global.env ()) evd2 t2) - else - b - | Evd.Evar_empty, Evd.Evar_empty -> true - | Evd.Evar_defined t1, Evar_empty -> - let t1 = get_types evd1 t1 in - print_discrepancy (Printer.pr_constr_env (Global.env ()) evd1 t1) (Pp.str "Nothing") - | Evd.Evar_empty, Evd.Evar_defined t2 -> - let t2 = get_types evd2 t2 in - print_discrepancy (Pp.str "Nothing") (Printer.pr_constr_env (Global.env ()) evd2 t2) - ) with Not_found -> - CErrors.anomaly Pp.(str "Discrepancy in same solution: Not found All") *) - - -(* let same_solution comp evd1 evd2 = - Evar.Set.for_all (same_solution evd1 evd2) comp *) - -let set_solver_mode = function - | ARm -> fun _ l -> takeover_rm l - | AAdd -> fun _ l -> takeover_add l - | ASet -> fun x l -> takeover false l x - | ANone -> fun x l -> takeover true l x - | AAll -> fun x l -> takeover false l x -let solver_register x = takeover false [] x -let solver_activate s = set_solver_mode AAll s [] -let solver_deactivate s = set_solver_mode ANone s [] - - - -module Coq_elpi_class_tactics_hacked = struct - (************************************************************************) - (* * The Coq Proof Assistant / The Coq Development Team *) - (* v * Copyright INRIA, CNRS and contributors *) - (* x - | _ -> assert false - - let get_option_bool s () = - match Option.get (Goptions.get_option_value s) () with - | BoolValue x -> x - | _ -> assert false - - let typeclasses_depth_opt_name = ["Typeclasses";"Depth"] - let get_typeclasses_depth = - get_option_int typeclasses_depth_opt_name - - let set_typeclasses_depth = - Goptions.set_int_option_value typeclasses_depth_opt_name - - (** When this flag is enabled, the resolution of type classes tries to avoid - useless introductions. This is no longer useful since we have eta, but is - here for compatibility purposes. Another compatibility issues is that the - cost (in terms of search depth) can differ. *) - let get_typeclasses_limit_intros = - get_option_bool ["Typeclasses";"Limit";"Intros"] - - let get_typeclasses_dependency_order = - get_option_bool ["Typeclasses";"Dependency";"Order"] - - let iterative_deepening_opt_name = ["Typeclasses";"Iterative";"Deepening"] - let get_typeclasses_iterative_deepening = - get_option_bool iterative_deepening_opt_name - - module Debug : sig - val ppdebug : int -> (unit -> Pp.t) -> unit - - val get_debug : unit -> int - - val set_typeclasses_debug : bool -> unit - end = struct - let typeclasses_debug = ref 0 - - let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) - let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false - - let set_typeclasses_verbose = function - | None -> typeclasses_debug := 0 - | Some n -> typeclasses_debug := n - let get_typeclasses_verbose () = - if !typeclasses_debug = 0 then None else Some !typeclasses_debug - - let () = - let open Goptions in - declare_bool_option - { optstage = Summary.Stage.Interp; - optdepr = None; - optkey = ["Elpi"; "Typeclasses";"Debug"]; - optread = get_typeclasses_debug; - optwrite = set_typeclasses_debug; } - - let () = - let open Goptions in - declare_int_option - { optstage = Summary.Stage.Interp; - optdepr = None; - optkey = ["Elpi"; "Typeclasses";"Debug";"Verbosity"]; - optread = get_typeclasses_verbose; - optwrite = set_typeclasses_verbose; } - - let ppdebug lvl pp = - if !typeclasses_debug > lvl then Feedback.msg_debug (pp()) - - let get_debug () = !typeclasses_debug - end - open Debug - let set_typeclasses_debug = set_typeclasses_debug - - type search_strategy = Dfs | Bfs - - let set_typeclasses_strategy = function - | Dfs -> Goptions.set_bool_option_value iterative_deepening_opt_name false - | Bfs -> Goptions.set_bool_option_value iterative_deepening_opt_name true - - let pr_ev evs ev = - let evi = Evd.find_undefined evs ev in - let env = Evd.evar_filtered_env (Global.env ()) evi in - Printer.pr_econstr_env env evs (Evd.evar_concl evi) - - let pr_ev_with_id evs ev = - Evar.print ev ++ str " : " ++ pr_ev evs ev - - (** Typeclasses instance search tactic / eauto *) - - open Auto - open Unification - - let auto_core_unif_flags st allowed_evars = { - modulo_conv_on_closed_terms = Some st; - use_metas_eagerly_in_conv_on_closed_terms = true; - use_evars_eagerly_in_conv_on_closed_terms = false; - modulo_delta = st; - modulo_delta_types = st; - check_applied_meta_types = false; - use_pattern_unification = true; - use_meta_bound_pattern_unification = true; - allowed_evars; - restrict_conv_on_strict_subterms = false; (* ? *) - modulo_betaiota = true; - modulo_eta = false; - } - - let auto_unif_flags ?(allowed_evars = Evarsolve.AllowedEvars.all) st = - let fl = auto_core_unif_flags st allowed_evars in - { core_unify_flags = fl; - merge_unify_flags = fl; - subterm_unify_flags = fl; - allow_K_in_toplevel_higher_order_unification = false; - resolve_evars = false - } - - let e_give_exact flags h = - let open Tacmach in - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = project gl in - let sigma, c = Hints.fresh_hint env sigma h in - let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in - Proofview.Unsafe.tclEVARS sigma <*> - Clenv.unify ~flags ~cv_pb:CUMUL t1 <*> exact_no_check c - end - - let unify_resolve ~with_evars flags h diff = match diff with - | None -> - Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h - | Some (diff, ty) -> - let () = assert (Option.is_empty (fst @@ hint_as_term @@ h)) in - Proofview.Goal.enter begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.project gl in - let sigma, c = Hints.fresh_hint env sigma h in - let clenv = Clenv.mk_clenv_from_n env sigma diff (c, ty) in - Clenv.res_pf ~with_evars ~with_classes:false ~flags clenv - end - - (** Dealing with goals of the form A -> B and hints of the form - C -> A -> B. - *) - let with_prods nprods h f = - if get_typeclasses_limit_intros () then - Proofview.Goal.enter begin fun gl -> - if Option.has_some (fst @@ hint_as_term h) || Int.equal nprods 0 then f None - else - let sigma = Tacmach.project gl in - let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma (snd @@ hint_as_term h) in - let diff = nb_prod sigma ty - nprods in - if (>=) diff 0 then f (Some (diff, ty)) - else Tacticals.tclZEROMSG (str"Not enough premisses") - end - else Proofview.Goal.enter - begin fun gl -> - if Int.equal nprods 0 then f None - else Tacticals.tclZEROMSG (str"Not enough premisses") end - - (** Semantics of type class resolution lemma application: - - - Use unification to find a well-typed substitution. There might - be evars in the goal and the lemma. Evars in the goal can get refined. - - Independent evars are turned into goals, whatever their kind is. - - Dependent evars of the lemma corresponding to arguments which appear - in independent goals or the conclusion are turned into subgoals iff - they are of typeclass kind. - - The remaining dependent evars not of typeclass type are shelved, - and resolution must fill them for it to succeed, otherwise we - backtrack. - *) - - let pr_gls sigma gls = - prlist_with_sep spc - (fun ev -> int (Evar.repr ev) ++ spc () ++ pr_ev sigma ev) gls - - (** Ensure the dependent subgoals are shelved after an apply/eapply. *) - let shelve_dependencies gls = - let open Proofview in - if CList.is_empty gls then tclUNIT () - else - tclEVARMAP >>= fun sigma -> - ppdebug 1 (fun () -> str" shelving dependent subgoals: " ++ pr_gls sigma gls); - shelve_goals gls - - let hintmap_of env sigma hdc secvars concl = - match hdc with - | None -> fun db -> ModeMatch (NoMode, Hint_db.map_none ~secvars db) - | Some hdc -> - fun db -> Hint_db.map_eauto env sigma ~secvars hdc concl db - - (** Hack to properly solve dependent evars that are typeclasses *) - let rec e_trivial_fail_db only_classes db_list local_db secvars = - let open Tacticals in - let open Tacmach in - let trivial_fail = - Proofview.Goal.enter - begin fun gl -> - let env = Proofview.Goal.env gl in - let sigma = Tacmach.project gl in - let d = NamedDecl.get_id @@ pf_last_hyp gl in - let hints = push_resolve_hyp env sigma d local_db in - e_trivial_fail_db only_classes db_list hints secvars - end - in - let trivial_resolve = - Proofview.Goal.enter - begin fun gl -> - let tacs = e_trivial_resolve db_list local_db secvars only_classes - (pf_env gl) (project gl) (pf_concl gl) in - tclFIRST (List.map (fun (x,_,_,_,_) -> x) tacs) - end - in - let tacl = - Eauto.e_assumption :: - (tclTHEN Tactics.intro trivial_fail :: [trivial_resolve]) - in - tclSOLVE tacl - - and e_my_find_search db_list local_db secvars hdc complete only_classes env sigma concl0 = - let prods, concl = EConstr.decompose_prod_decls sigma concl0 in - let nprods = List.length prods in - let allowed_evars = - let all = Evarsolve.AllowedEvars.all in - match hdc with - | Some (hd,_) when only_classes -> - begin match Typeclasses.class_info hd with - | Some cl -> - if cl.cl_strict then - let undefined = lazy (Evarutil.undefined_evars_of_term sigma concl) in - let allowed evk = not (Evar.Set.mem evk (Lazy.force undefined)) in - Evarsolve.AllowedEvars.from_pred allowed - else all - | None -> all - end - | _ -> all - in - let tac_of_hint = - fun (flags, h) -> - let name = FullHint.name h in - let tac = function - | Res_pf h -> - let tac = - with_prods nprods h (unify_resolve ~with_evars:false flags h) in - Proofview.tclBIND (Proofview.with_shelf tac) - (fun (gls, ()) -> shelve_dependencies gls) - | ERes_pf h -> - let tac = - with_prods nprods h (unify_resolve ~with_evars:true flags h) in - Proofview.tclBIND (Proofview.with_shelf tac) - (fun (gls, ()) -> shelve_dependencies gls) - | Give_exact h -> - e_give_exact flags h - | Res_pf_THEN_trivial_fail h -> - let fst = with_prods nprods h (unify_resolve ~with_evars:true flags h) in - let snd = if complete then Tacticals.tclIDTAC - else e_trivial_fail_db only_classes db_list local_db secvars in - Tacticals.tclTHEN fst snd - | Unfold_nth c -> - Proofview.tclPROGRESS (unfold_in_concl [AllOccurrences,c]) - | Extern (p, tacast) -> conclPattern concl0 p tacast - in - let tac = FullHint.run h tac in - let tac = if complete then Tacticals.tclCOMPLETE tac else tac in - let extern = match FullHint.repr h with - | Extern _ -> true - | _ -> false - in - (tac, FullHint.priority h, extern, name, lazy (FullHint.print env sigma h)) - in - let hint_of_db = hintmap_of env sigma hdc secvars concl in - let hintl = List.map_filter (fun db -> match hint_of_db db with - | ModeMatch (m, l) -> Some (db, m, l) - | ModeMismatch -> None) - (local_db :: db_list) - in - (* In case there is a mode mismatch in all the databases we get stuck. - Otherwise we consider the hints that match. - Recall the local database uses the union of all the modes in the other databases. *) - if List.is_empty hintl then None - else - let hintl = - CList.map - (fun (db, m, tacs) -> - let flags = auto_unif_flags ~allowed_evars (Hint_db.transparent_state db) in - m, List.map (fun x -> tac_of_hint (flags, x)) tacs) - hintl - in - let modes, hintl = List.split hintl in - let all_mode_match = List.for_all (fun m -> m != NoMode) modes in - let hintl = match hintl with - (* Optim: only sort if multiple hint sources were involved *) - | [hintl] -> hintl - | _ -> - let hintl = List.flatten hintl in - let hintl = List.stable_sort - (fun (_, pri1, _, _, _) (_, pri2, _, _, _) -> Int.compare pri1 pri2) - hintl - in - hintl - in - Some (all_mode_match, hintl) - - and e_trivial_resolve db_list local_db secvars only_classes env sigma concl = - let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in - try - (match e_my_find_search db_list local_db secvars hd true only_classes env sigma concl with - | Some (_,l) -> l - | None -> []) - with Not_found -> [] - - let e_possible_resolve db_list local_db secvars only_classes env sigma concl = - let hd = try Some (decompose_app_bound sigma concl) with Bound -> None in - try - e_my_find_search db_list local_db secvars hd false only_classes env sigma concl - with Not_found -> Some (true, []) - - let cut_of_hints h = - List.fold_left (fun cut db -> PathOr (Hint_db.cut db, cut)) PathEmpty h - - let pr_depth l = - let rec fmt elts = - match elts with - | [] -> [] - | [n] -> [string_of_int n] - | n1::n2::rest -> - (string_of_int n1 ^ "." ^ string_of_int n2) :: fmt rest - in - prlist_with_sep (fun () -> str "-") str (fmt (List.rev l)) - - let is_Prop env sigma concl = - let ty = Retyping.get_type_of env sigma concl in - match EConstr.kind sigma ty with - | Sort s -> - begin match ESorts.kind sigma s with - | Prop -> true - | _ -> false - end - | _ -> false - - let is_unique env sigma concl = - try - let (cl,u), args = dest_class_app env sigma concl in - cl.cl_unique - with e when CErrors.noncritical e -> false - - (** Sort the undefined variables from the least-dependent to most dependent. *) - let top_sort evm undefs = - let l' = ref [] in - let tosee = ref undefs in - let cache = Evarutil.create_undefined_evars_cache () in - let rec visit ev evi = - let evs = Evarutil.filtered_undefined_evars_of_evar_info ~cache evm evi in - tosee := Evar.Set.remove ev !tosee; - Evar.Set.iter (fun ev -> - if Evar.Set.mem ev !tosee then - visit ev (Evd.find_undefined evm ev)) evs; - l' := ev :: !l'; - in - while not (Evar.Set.is_empty !tosee) do - let ev = Evar.Set.choose !tosee in - visit ev (Evd.find_undefined evm ev) - done; - List.rev !l' - - (** We transform the evars that are concerned by this resolution - (according to predicate p) into goals. - Invariant: function p only manipulates and returns undefined evars - *) - - let evars_to_goals p evm = - let goals, nongoals = Evar.Set.partition (p evm) (Evd.get_typeclass_evars evm) in - if Evar.Set.is_empty goals then None - else Some (goals, nongoals) - - (** Making local hints *) - let make_resolve_hyp env sigma st only_classes decl db = - let id = NamedDecl.get_id decl in - let cty = Evarutil.nf_evar sigma (NamedDecl.get_type decl) in - let iscl env ty = - let ctx, ar = decompose_prod_decls sigma ty in - match EConstr.kind sigma (fst (decompose_app sigma ar)) with - | Const (c,_) -> is_class (GlobRef.ConstRef c) - | Ind (i,_) -> is_class (GlobRef.IndRef i) - | _ -> false - in - let is_class = iscl env cty in - let keep = not only_classes || is_class in - if keep then - let id = GlobRef.VarRef id in - push_resolves env sigma id db - else db - - let make_hints env sigma (modes,st) only_classes sign = - let db = Hint_db.add_modes modes @@ Hint_db.empty st true in - List.fold_right - (fun hyp hints -> - let consider = - not only_classes || - try let t = hyp |> NamedDecl.get_id |> Global.lookup_named |> NamedDecl.get_type in - (* Section variable, reindex only if the type changed *) - not (EConstr.eq_constr sigma (EConstr.of_constr t) (NamedDecl.get_type hyp)) - with Not_found -> true - in - if consider then - make_resolve_hyp env sigma st only_classes hyp hints - else hints) - sign db - - module Search = struct - type autoinfo = - { search_depth : int list; - last_tac : Pp.t Lazy.t; - search_dep : bool; - search_only_classes : bool; - search_cut : hints_path; - search_hints : hint_db; - search_best_effort : bool; - } - - (** Local hints *) - let autogoal_cache = Summary.ref ~name:"autogoal_cachee" - (DirPath.empty, true, Context.Named.empty, GlobRef.Map.empty, - Hint_db.empty TransparentState.full true) - - let make_autogoal_hints only_classes (modes,st as mst) gl = - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let sign = EConstr.named_context env in - let (dir, onlyc, sign', cached_modes, cached_hints) = !autogoal_cache in - let cwd = Lib.cwd () in - let eq c1 c2 = EConstr.eq_constr sigma c1 c2 in - if DirPath.equal cwd dir && - (onlyc == only_classes) && - Context.Named.equal eq sign sign' && - cached_modes == modes - then cached_hints - else - let hints = make_hints env sigma mst only_classes sign in - autogoal_cache := (cwd, only_classes, sign, modes, hints); hints - - let make_autogoal mst only_classes dep cut best_effort i g = - let hints = make_autogoal_hints only_classes mst g in - { search_hints = hints; - search_depth = [i]; last_tac = lazy (str"none"); - search_dep = dep; - search_only_classes = only_classes; - search_cut = cut; - search_best_effort = best_effort } - - (** In the proof engine failures are represented as exceptions *) - exception ReachedLimit - exception NoApplicableHint - exception StuckGoal - - (** ReachedLimit has priority over NoApplicableHint to handle - iterative deepening: it should fail when no hints are applicable, - but go to a deeper depth otherwise. *) - let merge_exceptions e e' = - match fst e, fst e' with - | ReachedLimit, _ -> e - | _, ReachedLimit -> e' - | _, _ -> e - - (** Determine if backtracking is needed for this goal. - We generally backtrack except in the following (possibly - overlapping) cases: - - [unique_instances] is [true]. - This is the case when the goal's class has [Unique Instances]. - - [indep] is [true] and the current goal has no evars. - [indep] is generally [true] and only gets set to [false] if the - current goal's evar is mentioned in other goals. - ([indep] is the negation of [search_dep].) - - The current goal is a [Prop] and has no evars. *) - let needs_backtrack env evd ~unique_instances ~indep concl = - if unique_instances then false else - if indep || is_Prop env evd concl then - occur_existential evd concl - else true - - exception NonStuckFailure - (* exception Backtrack *) - - let pr_goals s = - let open Proofview in - if get_debug() > 1 then - tclEVARMAP >>= fun sigma -> - Unsafe.tclGETGOALS >>= fun gls -> - let gls = CList.map Proofview.drop_state gls in - let j = List.length gls in - let pr_goal gl = pr_ev_with_id sigma gl in - Feedback.msg_debug - (s ++ int j ++ str" goals:" ++ spc () ++ - prlist_with_sep Pp.fnl pr_goal gls); - tclUNIT () - else - tclUNIT () - - let pr_internal_exception ie = - match fst ie with - | ReachedLimit -> str "Proof-search reached its limit." - | NoApplicableHint -> str "Proof-search failed." - | StuckGoal | NonStuckFailure -> str "Proof-search got stuck." - | e -> CErrors.iprint ie - - (* XXX Is this handler needed for something? *) - let () = CErrors.register_handler begin function - | NonStuckFailure -> Some (str "NonStuckFailure") - | NoApplicableHint -> Some (str "NoApplicableHint") - | _ -> None - end - - (** - For each success of tac1 try tac2. - If tac2 raises NonStuckFailure, try the next success of tac1 until depleted. - If tac1 finally fails, returns the result of the first tac1 success, if any. - *) - - type goal_status = - | IsInitial - | IsStuckGoal - | IsNonStuckFailure - - let pr_goal_status = function - | IsInitial -> str "initial" - | IsStuckGoal -> str "stuck" - | IsNonStuckFailure -> str "stuck failure" - - - let pr_search_goal sigma (glid, ev, status, _) = - str"Goal " ++ int glid ++ str" evar: " ++ Evar.print ev ++ str " status: " ++ pr_goal_status status - - let pr_search_goals sigma = - prlist_with_sep fnl (pr_search_goal sigma) - - let search_fixpoint ~best_effort ~allow_out_of_order tacs = - let open Pp in - let open Proofview in - let open Proofview.Notations in - let rec fixpoint progress tacs stuck fk = - let next (glid, ev, status, tac) tacs stuck = - let () = ppdebug 1 (fun () -> - str "considering goal " ++ int glid ++ - str " of status " ++ pr_goal_status status) - in - let rec kont = function - | Fail ((NonStuckFailure | StuckGoal as exn), info) when allow_out_of_order -> - let () = ppdebug 1 (fun () -> - str "Goal " ++ int glid ++ - str" is stuck or failed without being stuck, trying other tactics.") - in - let status = - match exn with - | NonStuckFailure -> IsNonStuckFailure - | StuckGoal -> IsStuckGoal - | _ -> assert false - in - cycle 1 (* Puts the first goal last *) <*> - fixpoint progress tacs ((glid, ev, status, tac) :: stuck) fk (* Launches the search on the rest of the goals *) - | Fail ie -> - let () = ppdebug 1 (fun () -> - str "Goal " ++ int glid ++ str" has no more solutions, returning exception: " - ++ pr_internal_exception ie) - in - fk ie - | Next (res, fk') -> - let () = ppdebug 1 (fun () -> - str "Goal " ++ int glid ++ str" has a success, continuing resolution") - in - (* We try to solve the rest of the constraints, and if that fails - we backtrack to the next result of tac, etc.... Ultimately if none of the solutions - for tac work, we will come back to the failure continuation fk in one of - the above cases *) - fixpoint true tacs stuck (fun e -> tclCASE (fk' e) >>= kont) - in tclCASE tac >>= kont - in - tclEVARMAP >>= fun sigma -> - let () = ppdebug 1 (fun () -> - let stuck, failed = List.partition (fun (_, _, status, _) -> status = IsStuckGoal) stuck in - str"Calling fixpoint on : " ++ - int (List.length tacs) ++ str" initial goals" ++ - str", " ++ int (List.length stuck) ++ str" stuck goals" ++ - str" and " ++ int (List.length failed) ++ str" non-stuck failures kept" ++ - str" with " ++ str(if progress then "" else "no ") ++ - str"progress made in this run." ++ fnl () ++ - str "Stuck: " ++ pr_search_goals sigma stuck ++ fnl () ++ - str "Failed: " ++ pr_search_goals sigma failed ++ fnl () ++ - str "Initial: " ++ pr_search_goals sigma tacs) - in - tclCHECKINTERRUPT <*> - match tacs with - | tac :: tacs -> next tac tacs stuck - | [] -> (* All remaining goals are stuck *) - match stuck with - | [] -> - (* We found a solution! Great, but in case it's not good for the rest of the proof search, - we might have other solutions available through fk. *) - tclOR (tclUNIT ()) fk - | stuck -> - if progress then fixpoint false stuck [] fk - else (* No progress can be made on the stuck goals arising from this resolution, - try a different solution on the non-stuck goals, if any. *) - begin - tclORELSE (fk (NoApplicableHint, Exninfo.null)) - (fun (e, info) -> - let () = ppdebug 1 (fun () -> int (List.length stuck) ++ str " remaining goals left, no progress, calling continuation failed") - in - (* We keep the stuck goals to display to the user *) - if best_effort then - let stuckgls, failedgls = List.partition (fun (_, _, status, _) -> - match status with - | IsStuckGoal -> true - | IsNonStuckFailure -> false - (* There should remain no initial goals at this point *) - | IsInitial -> assert false) - stuck - in - pr_goals (str "best_effort is on and remaining goals are: ") <*> - (* We shelve the stuck goals but we keep the non-stuck failures in the goal list. - This is for compat with Coq 8.12 but might not be the wisest choice in the long run. - *) - let to_shelve = List.map (fun (glid, ev, _, _) -> ev) stuckgls in - let () = ppdebug 1 (fun () -> - str "Shelving subgoals: " ++ - prlist_with_sep spc Evar.print to_shelve) - in - Unsafe.tclNEWSHELVED to_shelve - else tclZERO ~info e) - end - in - pr_goals (str"Launching resolution fixpoint on ") <*> - Unsafe.tclGETGOALS >>= fun gls -> - (* We wrap all goals with their associated tactic. - It might happen that an initial goal is solved during the resolution of another goal, - hence the `tclUNIT` in case there is no goal for the tactic to apply anymore. *) - let tacs = List.map2_i - (fun i gls tac -> (succ i, Proofview.drop_state gls, IsInitial, tclFOCUS ~nosuchgoal:(tclUNIT ()) 1 1 tac)) - 0 gls tacs - in - fixpoint false tacs [] (fun (e, info) -> tclZERO ~info e) <*> - pr_goals (str "Result goals after fixpoint: ") - - - (** The general hint application tactic. - tac1 + tac2 .... The choice of OR or ORELSE is determined - depending on the dependencies of the goal and the unique/Prop - status *) - let hints_tac_gl hints info kont gl : unit Proofview.tactic = - let open Proofview in - let open Proofview.Notations in - let env = Goal.env gl in - let concl = Goal.concl gl in - let sigma = Goal.sigma gl in - let unique_instances = is_unique env sigma concl in - let indep = not info.search_dep in - let backtrack = needs_backtrack env sigma ~unique_instances ~indep concl in - let () = ppdebug 0 (fun () -> - pr_depth info.search_depth ++ str": looking for " ++ - Printer.pr_econstr_env (Goal.env gl) sigma concl ++ - (if backtrack then str" with backtracking" - else str" without backtracking")) - in - let secvars = compute_secvars gl in - match e_possible_resolve hints info.search_hints secvars - info.search_only_classes env sigma concl with - | None -> - Proofview.tclZERO StuckGoal - | Some (all_mode_match, poss) -> - (* If no goal depends on the solution of this one or the - instances are irrelevant/assumed to be unique, then - we don't need to backtrack, as long as no evar appears in the goal - This is an overapproximation. Evars could appear in this goal only - and not any other *) - let ortac = if backtrack then Proofview.tclOR else Proofview.tclORELSE in - let idx = ref 1 in - let foundone = ref false in - let rec onetac e (tac, pat, b, name, pp) tl = - let path = match name with - | None -> PathAny - | Some gr -> PathHints [gr] - in - let derivs = path_derivate info.search_cut path in - let pr_error ie = - ppdebug 1 (fun () -> - let idx = if fst ie == NoApplicableHint then pred !idx else !idx in - let header = - pr_depth (idx :: info.search_depth) ++ str": " ++ - Lazy.force pp ++ - (if !foundone != true then - str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) - else mt ()) - in - (header ++ str " failed with: " ++ pr_internal_exception ie)) - in - let tac_of gls i j = Goal.enter begin fun gl' -> - let sigma' = Goal.sigma gl' in - let () = ppdebug 0 (fun () -> - pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev sigma' (Proofview.Goal.goal gl')) - in - let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in - let hints' = - if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) - then - let st = Hint_db.transparent_state info.search_hints in - let modes = Hint_db.modes info.search_hints in - make_autogoal_hints info.search_only_classes (modes,st) gl' - else info.search_hints - in - let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in - let info' = - { search_depth = succ j :: i :: info.search_depth; - last_tac = pp; - search_dep = dep'; - search_only_classes = info.search_only_classes; - search_hints = hints'; - search_cut = derivs; - search_best_effort = info.search_best_effort } - in kont info' end - in - let rec result (shelf, ()) i k = - foundone := true; - Proofview.Unsafe.tclGETGOALS >>= fun gls -> - let gls = CList.map Proofview.drop_state gls in - let j = List.length gls in - let () = ppdebug 0 (fun () -> - pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) - ++ str", " ++ int j ++ str" subgoal(s)" ++ - (Option.cata (fun k -> str " in addition to the first " ++ int k) - (mt()) k)) - in - let res = - if j = 0 then tclUNIT () - else search_fixpoint ~best_effort:false ~allow_out_of_order:false - (List.init j (fun j' -> (tac_of gls i (Option.default 0 k + j')))) - in - let finish nestedshelf sigma = - let filter ev = - try - let evi = Evd.find_undefined sigma ev in - if info.search_only_classes then - Some (ev, not (is_class_evar sigma evi)) - else Some (ev, true) - with Not_found -> None - in - let remaining = CList.map_filter filter shelf in - let () = ppdebug 1 (fun () -> - let prunsolved (ev, _) = int (Evar.repr ev) ++ spc () ++ pr_ev sigma ev in - let unsolved = prlist_with_sep spc prunsolved remaining in - pr_depth (i :: info.search_depth) ++ - str": after " ++ Lazy.force pp ++ str" finished, " ++ - int (List.length remaining) ++ - str " goals are shelved and unsolved ( " ++ - unsolved ++ str")") - in - begin - (* Some existentials produced by the original tactic were not solved - in the subgoals, turn them into subgoals now. *) - let shelved, goals = List.partition (fun (ev, s) -> s) remaining in - let shelved = List.map fst shelved @ nestedshelf and goals = List.map fst goals in - let () = if not (List.is_empty shelved && List.is_empty goals) then - ppdebug 1 (fun () -> - str"Adding shelved subgoals to the search: " ++ - prlist_with_sep spc (pr_ev sigma) goals ++ - str" while shelving " ++ - prlist_with_sep spc (pr_ev sigma) shelved) - in - shelve_goals shelved <*> - if List.is_empty goals then tclUNIT () - else - let make_unresolvables = tclEVARMAP >>= fun sigma -> - let sigma = make_unresolvables (fun x -> List.mem_f Evar.equal x goals) sigma in - Unsafe.tclEVARS sigma - in - let goals = CList.map Proofview.with_empty_state goals in - with_shelf (make_unresolvables <*> Unsafe.tclNEWGOALS goals) >>= fun s -> - result s i (Some (Option.default 0 k + j)) - end - in - with_shelf res >>= fun (sh, ()) -> - tclEVARMAP >>= finish sh - in - if path_matches derivs [] then aux e tl - else - ortac - (with_shelf tac >>= fun s -> - let i = !idx in incr idx; result s i None) - (fun e' -> - (pr_error e'; aux (merge_exceptions e e') tl)) - and aux e = function - | tac :: tacs -> onetac e tac tacs - | [] -> - let () = if !foundone == false then - ppdebug 0 (fun () -> - pr_depth info.search_depth ++ str": no match for " ++ - Printer.pr_econstr_env (Goal.env gl) sigma concl ++ - str ", " ++ int (List.length poss) ++ - str" possibilities") - in - match e with - | (ReachedLimit,ie) -> Proofview.tclZERO ~info:ie ReachedLimit - | (StuckGoal,ie) -> Proofview.tclZERO ~info:ie StuckGoal - | (NoApplicableHint,ie) -> - (* If the constraint abides by the (non-trivial) modes but no - solution could be found, we consider it a failed goal, and let - proof search proceed on the rest of the - constraints, thus giving a more precise error message. *) - if all_mode_match && - info.search_best_effort then - Proofview.tclZERO ~info:ie NonStuckFailure - else Proofview.tclZERO ~info:ie NoApplicableHint - | (_,ie) -> Proofview.tclZERO ~info:ie NoApplicableHint - in - if backtrack then aux (NoApplicableHint,Exninfo.null) poss - else tclONCE (aux (NoApplicableHint,Exninfo.null) poss) - - let hints_tac hints info kont : unit Proofview.tactic = - Proofview.Goal.enter - (fun gl -> hints_tac_gl hints info kont gl) - - let intro_tac info kont gl = - let open Proofview in - let env = Goal.env gl in - let sigma = Goal.sigma gl in - let decl = Tacmach.pf_last_hyp gl in - let ldb = - make_resolve_hyp env sigma (Hint_db.transparent_state info.search_hints) - info.search_only_classes decl info.search_hints in - let info' = - { info with search_hints = ldb; last_tac = lazy (str"intro"); - search_depth = 1 :: 1 :: info.search_depth } - in kont info' - - let intro info kont = - Proofview.tclBIND Tactics.intro - (fun _ -> Proofview.Goal.enter (fun gl -> intro_tac info kont gl)) - - let rec search_tac hints limit depth = - let kont info = - Proofview.numgoals >>= fun i -> - let () = ppdebug 1 (fun () -> - str "calling eauto recursively at depth " ++ int (succ depth) ++ - str " on " ++ int i ++ str " subgoals") - in - search_tac hints limit (succ depth) info - in - fun info -> - if Int.equal depth (succ limit) then - let info = Exninfo.reify () in - Proofview.tclZERO ~info ReachedLimit - else - Proofview.tclOR (hints_tac hints info kont) - (fun e -> Proofview.tclOR (intro info kont) - (fun e' -> let (e, info) = merge_exceptions e e' in - Proofview.tclZERO ~info e)) - - let search_tac_gl mst only_classes dep hints best_effort depth i sigma gls gl : - unit Proofview.tactic = - let open Proofview in - let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in - let info = make_autogoal mst only_classes dep (cut_of_hints hints) - best_effort i gl in - search_tac hints depth 1 info - - let search_tac mst only_classes best_effort dep hints depth = - let open Proofview in - let tac sigma gls i = - Goal.enter - begin fun gl -> - search_tac_gl mst only_classes dep hints best_effort depth (succ i) sigma gls gl end - in - Proofview.Unsafe.tclGETGOALS >>= fun gls -> - let gls = CList.map Proofview.drop_state gls in - Proofview.tclEVARMAP >>= fun sigma -> - let j = List.length gls in - search_fixpoint ~best_effort ~allow_out_of_order:true (List.init j (fun i -> tac sigma gls i)) - - let fix_iterative t = - let rec aux depth = - Proofview.tclOR - (t depth) - (function - | (ReachedLimit,_) -> aux (succ depth) - | (e,ie) -> Proofview.tclZERO ~info:ie e) - in aux 1 - - let fix_iterative_limit limit t = - let open Proofview in - let rec aux depth = - if Int.equal depth (succ limit) - then - let info = Exninfo.reify () in - tclZERO ~info ReachedLimit - else tclOR (t depth) (function - | (ReachedLimit, _) -> aux (succ depth) - | (e,ie) -> Proofview.tclZERO ~info:ie e) - in aux 1 - - let eauto_tac_stuck mst ?(unique=false) - ~only_classes - ~best_effort - ?strategy ~depth ~dep hints = - let open Proofview in - let tac = - let search = search_tac mst only_classes best_effort dep hints in - let dfs = - match strategy with - | None -> not (get_typeclasses_iterative_deepening ()) - | Some Dfs -> true - | Some Bfs -> false - in - if dfs then - let depth = match depth with None -> -1 | Some d -> d in - search depth - else - match depth with - | None -> fix_iterative search - | Some l -> fix_iterative_limit l search - in - let error (e, info) = - match e with - | ReachedLimit -> - Tacticals.tclFAIL ~info (str"Proof search reached its limit") - | NoApplicableHint -> - Tacticals.tclFAIL ~info (str"Proof search failed" ++ - (if Option.is_empty depth then mt() - else str" without reaching its limit")) - | Proofview.MoreThanOneSuccess -> - Tacticals.tclFAIL ~info (str"Proof search failed: " ++ - str"more than one success found") - | e -> Proofview.tclZERO ~info e - in - let tac = Proofview.tclOR tac error in - let tac = - if unique then - Proofview.tclEXACTLY_ONCE Proofview.MoreThanOneSuccess tac - else tac - in - with_shelf numgoals >>= fun (initshelf, i) -> - let () = ppdebug 1 (fun () -> - str"Starting resolution with " ++ int i ++ - str" goal(s) under focus and " ++ - int (List.length initshelf) ++ str " shelved goal(s)" ++ - (if only_classes then str " in only_classes mode" else str " in regular mode") ++ - match depth with - | None -> str ", unbounded" - | Some i -> str ", with depth limit " ++ int i) - in - tac <*> pr_goals (str "after eauto_tac_stuck: ") - - let eauto_tac mst ?unique ~only_classes ~best_effort ?strategy ~depth ~dep hints = - Hints.wrap_hint_warning @@ - (eauto_tac_stuck mst ?unique ~only_classes - ~best_effort ?strategy ~depth ~dep hints) - - let run_on_goals env evm p tac goals nongoals = - let goalsl = - if get_typeclasses_dependency_order () then - top_sort evm goals - else Evar.Set.elements goals - in - let goalsl = List.map Proofview.with_empty_state goalsl in - let tac = Proofview.Unsafe.tclNEWGOALS goalsl <*> tac in - let evm = Evd.set_typeclass_evars evm Evar.Set.empty in - let evm = Evd.push_future_goals evm in - let _, pv = Proofview.init evm [] in - (* Instance may try to call this before a proof is set up! - Thus, give_me_the_proof will fail. Beware! *) - let name, poly = - (* try - * let Proof.{ name; poly } = Proof.data Proof_global.(give_me_the_proof ()) in - * name, poly - * with | Proof_global.NoCurrentProof -> *) - Id.of_string "instance", false - in - let tac = - if get_debug () > 1 then Proofview.Trace.record_info_trace tac - else tac - in - let (), pv', unsafe, info = - try Proofview.apply ~name ~poly env tac pv - with Logic_monad.TacticFailure _ -> raise Not_found - in - let () = - ppdebug 1 (fun () -> - str"The tactic trace is: " ++ hov 0 (Proofview.Trace.pr_info env evm ~lvl:1 info)) - in - let finished = Proofview.finished pv' in - let evm' = Proofview.return pv' in - let _, evm' = Evd.pop_future_goals evm' in - let () = ppdebug 1 (fun () -> - str"Finished resolution with " ++ str(if finished then "a complete" else "an incomplete") ++ - str" solution." ++ fnl() ++ - str"Old typeclass evars not concerned by this resolution = " ++ - hov 0 (prlist_with_sep spc (pr_ev_with_id evm') - (Evar.Set.elements (Evd.get_typeclass_evars evm'))) ++ fnl() ++ - str"Shelf = " ++ - hov 0 (prlist_with_sep spc (pr_ev_with_id evm') - (Evar.Set.elements (Evd.get_typeclass_evars evm')))) - in - let nongoals' = - Evar.Set.fold (fun ev acc -> match Evarutil.advance evm' ev with - | Some ev -> Evar.Set.add ev acc - | None -> acc) (Evar.Set.union goals nongoals) (Evd.get_typeclass_evars evm') - in - (* FIXME: the need to merge metas seems to come from this being called - internally from Unification. It should be handled there instead. *) - let evm' = Evd.meta_merge (Evd.meta_list evm) (Evd.clear_metas evm') in - let evm' = Evd.set_typeclass_evars evm' nongoals' in - let () = ppdebug 1 (fun () -> - str"New typeclass evars are: " ++ - hov 0 (prlist_with_sep spc (pr_ev_with_id evm') (Evar.Set.elements nongoals'))) - in - Some (finished, evm') - - let run_on_evars env evm p tac = - match evars_to_goals p evm with - | None -> None (* This happens only because there's no evar having p *) - | Some (goals, nongoals) -> - run_on_goals env evm p tac goals nongoals - let evars_eauto env evd depth only_classes ~best_effort unique dep mst hints p = - let eauto_tac = eauto_tac_stuck mst ~unique ~only_classes - ~best_effort - ~depth ~dep:(unique || dep) hints in - run_on_evars env evd p eauto_tac - - (** Typeclasses eauto is an eauto which tries to resolve only - goals of typeclass type, and assumes that the initially selected - evars in evd are independent of the rest of the evars *) - let typeclasses_eauto env evd ?depth unique ~best_effort st hints p = - NewProfile.profile "typeclass search" (fun () -> - evars_eauto env evd depth true ~best_effort unique false st hints p) - () - - let typeclasses_resolve env evd depth unique ~best_effort p = - let db = searchtable_map typeclasses_db in - let st = Hint_db.transparent_state db in - let modes = Hint_db.modes db in - typeclasses_eauto env evd ?depth ~best_effort unique (modes,st) [db] p - end - - let typeclasses_eauto ?(only_classes=false) - ?(best_effort=false) - ?(st=TransparentState.full) - ?strategy ~depth dbs = - let dbs = List.map_filter - (fun db -> try Some (searchtable_map db) - with e when CErrors.noncritical e -> None) - dbs - in - let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in - let modes = List.map Hint_db.modes dbs in - let modes = List.fold_left (GlobRef.Map.union (fun _ m1 m2 -> Some (m1@m2))) GlobRef.Map.empty modes in - let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in - Proofview.tclIGNORE - (Search.eauto_tac (modes,st) ~only_classes ?strategy - ~best_effort ~depth ~dep:true dbs) - (* Stuck goals can remain here, we could shelve them, but this way - the user can use `solve [typeclasses eauto]` to check there are - no stuck goals remaining, or use [typeclasses eauto; shelve] himself. *) - - (** We compute dependencies via a union-find algorithm. - Beware of the imperative effects on the partition structure, - it should not be shared, but only used locally. *) - - module Intpart = Unionfind.Make(Evar.Set)(Evar.Map) - - let deps_of_constraints cstrs evm p = - List.iter (fun (_, _, x, y) -> - let evx = Evarutil.undefined_evars_of_term evm x in - let evy = Evarutil.undefined_evars_of_term evm y in - Intpart.union_set (Evar.Set.union evx evy) p) - cstrs - - let evar_dependencies pred evm p = - let cache = Evarutil.create_undefined_evars_cache () in - Evd.fold_undefined - (fun ev evi _ -> - if Evd.is_typeclass_evar evm ev && pred evm ev evi then - let evars = Evar.Set.add ev (Evarutil.filtered_undefined_evars_of_evar_info ~cache evm evi) - in Intpart.union_set evars p - else ()) - evm () - - (** [split_evars] returns groups of undefined evars according to dependencies *) - - let split_evars pred evm = - let p = Intpart.create () in - evar_dependencies pred evm p; - deps_of_constraints (snd (extract_all_conv_pbs evm)) evm p; - Intpart.partition p - - let is_inference_forced p evd ev = - try - if Evar.Set.mem ev (Evd.get_typeclass_evars evd) && p ev - then - let (loc, k) = evar_source (Evd.find_undefined evd ev) in - match k with - | Evar_kinds.ImplicitArg (_, _, b) -> b - | Evar_kinds.QuestionMark _ -> false - | _ -> true - else true - with Not_found -> assert false - - let is_mandatory p comp evd = - Evar.Set.exists (is_inference_forced p evd) comp - - (** Check if an evar is concerned by the current resolution attempt, - (and in particular is in the current component). - Invariant : this should only be applied to undefined evars. *) - - let select_and_update_evars p oevd in_comp evd ev = - try - if Evd.is_typeclass_evar oevd ev then - (in_comp ev && p evd ev (Evd.find_undefined evd ev)) - else false - with Not_found -> false - - (** Do we still have unresolved evars that should be resolved ? *) - - let has_undefined p oevd evd = - let check ev evi = p oevd ev in - Evar.Map.exists check (Evd.undefined_map evd) - let find_undefined p oevd evd = - let check ev evi = p oevd ev in - Evar.Map.domain (Evar.Map.filter check (Evd.undefined_map evd)) - - exception Unresolved of evar_map - - type solver_type = Environ.env -> evar_map -> - metavariable option -> prefix_of_inductive_support_flag -> - best_effort:prefix_of_inductive_support_flag -> - (evar_map -> Evar.t -> prefix_of_inductive_support_flag) -> - (prefix_of_inductive_support_flag * evar_map) option - - (** If [do_split] is [true], we try to separate the problem in - several components and then solve them separately *) - let resolve_all_evars depth unique env p oevd fail = - let () = - ppdebug 0 (fun () -> - str"Calling typeclass resolution with flags: "++ - str"depth = " ++ (match depth with None -> str "∞" | Some d -> int d) ++ str"," ++ - str"unique = " ++ bool unique ++ str"," ++ - str"fail = " ++ bool fail); - ppdebug 2 (fun () -> - str"Initial evar map: " ++ - Termops.pr_evar_map ~with_univs:!Detyping.print_universes None env oevd) - in - let split = split_evars p oevd in - let split_solver = List.map (handle_takeover Search.typeclasses_resolve env oevd) split in - let in_comp comp ev = Evar.Set.mem ev comp in - let rec docomp evd = function - | [] -> - let () = ppdebug 2 (fun () -> - str"Final evar map: " ++ - Termops.pr_evar_map ~with_univs:!Detyping.print_universes None env evd) - in - evd - | ((solver: solver_type), comp) :: comps -> - let p = select_and_update_evars p oevd (in_comp comp) in - try - (try - let res = solver env evd depth - ~best_effort:true unique p in - match res with - | Some (finished, evd') -> - if has_undefined p oevd evd' then - let () = if finished then ppdebug 1 (fun () -> - str"Proof is finished but there remain undefined evars: " ++ - prlist_with_sep spc (pr_ev evd') - (Evar.Set.elements (find_undefined p oevd evd'))) - in - raise (Unresolved evd') - else docomp evd' comps - | None -> docomp evd comps (* No typeclass evars left in this component *) - with Not_found -> - (* Typeclass resolution failed *) - raise (Unresolved evd)) - with Unresolved evd' -> - if fail && is_mandatory (p evd') comp evd' - then (* Unable to satisfy the constraints. *) - error_unresolvable env evd' comp - else (* Best effort: use the best found solution on this component *) - docomp evd' comps - in docomp oevd split_solver - - let initial_select_evars filter = - fun evd ev evi -> - filter ev (Lazy.from_val (snd (Evd.evar_source evi))) && - (* Typeclass evars can contain evars whose conclusion is not - yet determined to be a class or not. *) - Typeclasses.is_class_evar evd evi - - - let classes_transparent_state () = - try Hint_db.transparent_state (searchtable_map typeclasses_db) - with Not_found -> TransparentState.empty - - let resolve_typeclass_evars depth unique env evd filter fail = - let evd = - try Evarconv.solve_unif_constraints_with_heuristics - ~flags:(Evarconv.default_flags_of (classes_transparent_state())) env evd - with e when CErrors.noncritical e -> evd - in - resolve_all_evars depth unique env - (initial_select_evars filter) evd fail - - let solve_inst env evd filter unique fail = - let ((), sigma) = Hints.wrap_hint_warning_fun env evd begin fun evd -> - (), resolve_typeclass_evars - (get_typeclasses_depth ()) - unique env evd filter fail - end in - sigma - - let () = - Typeclasses.set_solve_all_instances solve_inst - - let resolve_one_typeclass env ?(sigma=Evd.from_env env) concl unique = - let (term, sigma) = Hints.wrap_hint_warning_fun env sigma begin fun sigma -> - let hints = searchtable_map typeclasses_db in - let st = Hint_db.transparent_state hints in - let modes = Hint_db.modes hints in - let depth = get_typeclasses_depth () in - let tac = Tacticals.tclCOMPLETE (Search.eauto_tac (modes,st) - ~only_classes:true ~best_effort:false - ~depth [hints] ~dep:true) - in - let entry, pv = Proofview.init sigma [env, concl] in - let pv = - let name = Names.Id.of_string "legacy_pe" in - match Proofview.apply ~name ~poly:false (Global.env ()) tac pv with - | (_, final, _, _) -> final - | exception (Logic_monad.TacticFailure (Tacticals.FailError _)) -> - raise Not_found - in - let evd = Proofview.return pv in - let term = match Proofview.partial_proof entry pv with [t] -> t | _ -> assert false in - term, evd - end in - (sigma, term) - - let () = - Typeclasses.set_solve_one_instance - (fun x y z w -> resolve_one_typeclass x ~sigma:y z w) - - (** Take the head of the arity of a constr. - Used in the partial application tactic. *) - - let rec head_of_constr sigma t = - let t = strip_outer_cast sigma t in - match EConstr.kind sigma t with - | Prod (_,_,c2) -> head_of_constr sigma c2 - | LetIn (_,_,_,c2) -> head_of_constr sigma c2 - | App (f,args) -> head_of_constr sigma f - | _ -> t - - let head_of_constr h c = - Proofview.tclEVARMAP >>= fun sigma -> - let c = head_of_constr sigma c in - letin_tac None (Name h) c None Locusops.allHyps - - let not_evar c = - Proofview.tclEVARMAP >>= fun sigma -> - match EConstr.kind sigma c with - | Evar _ -> Tacticals.tclFAIL (str"Evar") - | _ -> Proofview.tclUNIT () - - let is_ground c = - let open Tacticals in - Proofview.tclEVARMAP >>= fun sigma -> - if Evarutil.is_ground_term sigma c then tclIDTAC - else tclFAIL (str"Not ground") - - let autoapply c i = - let open Proofview.Notations in - Hints.wrap_hint_warning @@ - Proofview.Goal.enter begin fun gl -> - let hintdb = try Hints.searchtable_map i with Not_found -> - CErrors.user_err (Pp.str ("Unknown hint database " ^ i ^ ".")) - in - let flags = auto_unif_flags - (Hints.Hint_db.transparent_state hintdb) in - let cty = Tacmach.pf_get_type_of gl c in - let env = Proofview.Goal.env gl in - let sigma = Proofview.Goal.sigma gl in - let ce = Clenv.mk_clenv_from env sigma (c,cty) in - Clenv.res_pf ~with_evars:true ~with_classes:false ~flags ce <*> - Proofview.tclEVARMAP >>= (fun sigma -> - let sigma = Typeclasses.make_unresolvables - (fun ev -> Typeclasses.all_goals ev (Lazy.from_val (snd (Evd.evar_source (Evd.find_undefined sigma ev))))) sigma in - Proofview.Unsafe.tclEVARS sigma) end - - let resolve_tc c = - let open Proofview.Notations in - Proofview.tclENV >>= fun env -> - Proofview.tclEVARMAP >>= fun sigma -> - let depth = get_typeclasses_depth () in - let unique = get_typeclasses_unique_solutions () in - let evars = Evarutil.undefined_evars_of_term sigma c in - let filter = (fun ev _ -> Evar.Set.mem ev evars) in - let fail = true in - let sigma = resolve_all_evars depth unique env (initial_select_evars filter) sigma fail in - Proofview.Unsafe.tclEVARS sigma - - end - - -[%%else] module Coq_elpi_lib_obj = struct let add_obj_no_discharge name cache = @@ -1713,4 +175,3 @@ let solver_register l = let solver_activate l = Lib.add_leaf (Solver.cache_solver (l, Activate)) let solver_deactivate l = Lib.add_leaf (Solver.cache_solver (l, Deactivate)) -[%%endif] diff --git a/coq-elpi.opam b/coq-elpi.opam index ea641c395..b14ef6f82 100644 --- a/coq-elpi.opam +++ b/coq-elpi.opam @@ -19,7 +19,7 @@ depends: [ "ocaml" {>= "4.10.0"} "stdlib-shims" "elpi" {>= "1.18.2" & < "1.20.0~"} - "coq" {>= "8.19" & < "8.21"} + "coq" {>= "8.20" & < "8.21"} "ppx_optcomp" "ocaml-lsp-server" {with-dev-setup} "odoc" {with-doc} diff --git a/dune-project b/dune-project index 031adaecd..c80dbac4b 100644 --- a/dune-project +++ b/dune-project @@ -32,7 +32,7 @@ (ocaml (>= 4.10.0)) stdlib-shims (elpi (and (>= 1.18.2) (< 1.20.0~))) - (coq (and (>= 8.19) (< 8.21))) + (coq (and (>= 8.20+rc1) (< 8.21~))) ppx_optcomp (ocaml-lsp-server :with-dev-setup))) diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 472cf8222..d9296a08c 100644 --- a/src/coq_elpi_HOAS.ml +++ b/src/coq_elpi_HOAS.ml @@ -330,52 +330,6 @@ type universe_decl_option = | NotUniversePolymorphic | Cumulative of universe_decl_cumul | NonCumulative of universe_decl -[%%if coq = "8.19"] -type options = { - hoas_holes : hole_mapping option; - local : bool option; - deprecation : Deprecation.t option; - primitive : bool option; - failsafe : bool; (* readback is resilient to illformed terms *) - ppwidth : int; - pp : ppoption; - pplevel : Constrexpr.entry_relative_level; - using : string option; - inline : Declaremods.inline; - uinstance : uinstanceoption; - universe_decl : universe_decl_option; - reversible : bool option; - keepunivs : bool option; - redflags : RedFlags.reds option; - no_tc: bool option; -} -let default_options () = { - hoas_holes = Some Verbatim; - local = None; - deprecation = None; - primitive = None; - failsafe = false; - ppwidth = Option.default 80 (Topfmt.get_margin ()); - pp = Normal; - pplevel = Constrexpr.LevelSome; - using = None; - inline = Declaremods.NoInline; - uinstance = NoInstance; - universe_decl = NotUniversePolymorphic; - reversible = None; - keepunivs = None; - redflags = None; - no_tc = None; -} -let make_options ~hoas_holes ~local ~warn:_ ~depr ~primitive ~failsafe ~ppwidth - ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs - ~redflags ~no_tc = - { hoas_holes; local; deprecation = depr; primitive; failsafe; ppwidth; pp; - pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs; - redflags; no_tc; } -let make_warn ~note ?cats () = () - -[%%else] type options = { hoas_holes : hole_mapping option; local : bool option; @@ -420,7 +374,6 @@ let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs; redflags; no_tc; } let make_warn = UserWarn.make_warn -[%%endif] type 'a coq_context = { section : Names.Id.t list; @@ -463,17 +416,10 @@ fun ~depth dbl name ~names -> | Name.Name id when Id.Set.mem id names -> Name.Name (mk_fresh dbl) | Name.Name id as x -> x -[%%if coq = "8.19" ] -let relevant = Sorts.Relevant -let anonR = Context.anonR -let nameR = Context.nameR -let annotR = Context.annotR -[%%else] let relevant = EConstr.ERelevance.relevant let anonR = Context.make_annot Names.Name.Anonymous EConstr.ERelevance.irrelevant let nameR x = Context.make_annot (Names.Name.Name x) EConstr.ERelevance.irrelevant let annotR x = Context.make_annot x EConstr.ERelevance.irrelevant -[%%endif] let in_coq_annot ~depth t = Context.make_annot (in_coq_name ~depth t) relevant @@ -790,15 +736,11 @@ let in_elpi_fix name rno ty bo = let primitivec = E.Constants.declare_global_symbol "primitive" -[%%if coq = "8.19"] -type pstring = string -let pp_pstring _ = "primitive strings not supported in Coq 8.19" -let eC_mkString _ = assert false -[%%else] + type pstring = Pstring.t let pp_pstring = Pstring.to_string let eC_mkString = EC.mkString -[%%endif] + type primitive_value = | Uint63 of Uint63.t | Float64 of Float64.t @@ -835,20 +777,13 @@ let in_elpi_primitive ~depth state i = let state, i, _ = primitive_value.API.Conversion.embed ~depth state i in state, E.mkApp primitivec i [] -[%%if coq = "8.19"] -let in_elpi_primitive_value ~depth state = function - | C.Int i -> in_elpi_primitive ~depth state (Uint63 i) - | C.Float f -> in_elpi_primitive ~depth state (Float64 f) - | C.Array _ -> nYI "HOAS for persistent arrays" - | (C.Fix _ | C.CoFix _ | C.Lambda _ | C.App _ | C.Prod _ | C.Case _ | C.Cast _ | C.Construct _ | C.LetIn _ | C.Ind _ | C.Meta _ | C.Rel _ | C.Var _ | C.Proj _ | C.Evar _ | C.Sort _ | C.Const _) -> assert false -[%%else] + let in_elpi_primitive_value ~depth state = function | C.Int i -> in_elpi_primitive ~depth state (Uint63 i) | C.Float f -> in_elpi_primitive ~depth state (Float64 f) | C.String s -> in_elpi_primitive ~depth state (Pstring s) | C.Array _ -> nYI "HOAS for persistent arrays" | (C.Fix _ | C.CoFix _ | C.Lambda _ | C.App _ | C.Prod _ | C.Case _ | C.Cast _ | C.Construct _ | C.LetIn _ | C.Ind _ | C.Meta _ | C.Rel _ | C.Var _ | C.Proj _ | C.Evar _ | C.Sort _ | C.Const _) -> assert false -[%%endif] (* ********************************* }}} ********************************** *) @@ -883,7 +818,7 @@ let show_coq_engine ?with_univs e = Format.asprintf "%a" (pp_coq_engine ?with_un let from_env env = from_env_sigma env (Evd.from_env env) -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let demote uctx sigma0 env = let uctx = UState.update_sigma_univs (Evd.evar_universe_context sigma0) (Environ.universes env) in UState.demote_global_univs env uctx @@ -2910,15 +2845,7 @@ let name_universe_level state l = { e with sigma }, id ) -[%%if coq = "8.19"] -let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = - let open UState in - { univdecl_qualities = []; - univdecl_extensible_instance; - univdecl_extensible_constraints; - univdecl_constraints; - univdecl_instance} -[%%else] + let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance = let open UState in { univdecl_qualities = []; @@ -2927,7 +2854,6 @@ let mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraint univdecl_extensible_constraints; univdecl_constraints; univdecl_instance} -[%%endif] let poly_cumul_udecl_variance_of_options state options = match options.universe_decl with @@ -2944,14 +2870,7 @@ let poly_cumul_udecl_variance_of_options state options = mk_universe_decl univdecl_extensible_instance univdecl_extensible_constraints univdecl_constraints univdecl_instance, Array.of_list variance -[%%if coq = "8.19"] -let comInductive_interp_mutual_inductive_constr env_ar_params sigma arity ~cumulative ~poly ~template ~finite = - let arityconcl = - match Reductionops.sort_of_arity env_ar_params sigma arity with - | exception Reduction.NotArity -> None - | s -> Some s in - ComInductive.interp_mutual_inductive_constr ~arityconcl:[arityconcl] ~cumulative ~poly ~template ~finite -[%%elif coq = "8.20"] +[%%if coq = "8.20"] let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~template ~finite = ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~cumulative ~poly ~template ~finite [%%else] @@ -2968,11 +2887,8 @@ let comInductive_interp_mutual_inductive_constr _ _ _ ~cumulative ~poly ~templat ComInductive.interp_mutual_inductive_constr ~arities_explicit:[true] ~template_syntax:[SyntaxAllowsTemplatePoly] ~flags [%%endif] -[%%if coq = "8.19"] -let comInductive_interp_mutual_inductive_constr_post (a,b,c) = [],a,b,c -[%%else] + let comInductive_interp_mutual_inductive_constr_post x = x -[%%endif] let lp2inductive_entry ~depth coq_ctx constraints state t = @@ -3686,56 +3602,6 @@ type module_item = | Functor of Names.ModPath.t * Names.ModPath.t list | FunctorType of Names.ModPath.t * Names.ModPath.t list -[%%if coq = "8.19"] -let rec in_elpi_module_item ~depth path state (name, item) = - let open Declarations in - match item with - | SFBconst _ -> - [Gref (GlobRef.ConstRef (Constant.make2 path name))] - | SFBmind { mind_packets } -> - CList.init (Array.length mind_packets) (fun i -> Gref (GlobRef.IndRef (MutInd.make2 path name,i))) - | SFBmodule ({ mod_mp; mod_type = NoFunctor _ } as b) -> [Module (mod_mp,in_elpi_module ~depth state b) ] - | SFBmodule { mod_mp; mod_type = MoreFunctor _ as l } -> [Functor(mod_mp,functor_params l)] - | SFBmodtype { mod_mp; mod_type = NoFunctor _ } -> [ModuleType mod_mp] - | SFBmodtype { mod_mp; mod_type = MoreFunctor _ as l } -> [FunctorType (mod_mp,functor_params l)] - -and functor_params x = - let open Declarations in - match x with - | MoreFunctor(_,{ mod_type_alg = Some (MENoFunctor (MEident mod_mp)) },rest) -> mod_mp :: functor_params rest - | _ -> [] (* XXX non trivial functors, eg P : X with type a = nat, are badly described (no params) *) - -and in_elpi_module : 'a. depth:int -> API.Data.state -> 'a Declarations.generic_module_body -> module_item list = - fun ~depth state { Declarations. - mod_mp; (* Names.module_path *) - mod_expr; (* Declarations.module_implementation *) - mod_type; (* Declarations.module_signature *) - mod_type_alg; (* Declarations.module_expression option *) - mod_delta; (* Mod_subst.delta_resolver *) - mod_retroknowledge; (* Retroknowledge.action list *) -} -> - match mod_type with - | Declarations.MoreFunctor _ -> nYI "functors" - | Declarations.NoFunctor contents -> - let l = - CList.map (in_elpi_module_item ~depth mod_mp state) contents in - CList.flatten l - -let rec in_elpi_modty_item (name, item) = match item with - | Declarations.SFBconst _ -> - [ Label.to_string name ] - | Declarations.SFBmind _ -> - [ Label.to_string name ] - | Declarations.SFBmodule mb -> in_elpi_modty mb - | Declarations.SFBmodtype _ -> [] - -and in_elpi_modty : 'a.'a Declarations.generic_module_body -> string list = - fun { Declarations.mod_type; (* Declarations.modty_signature *) } -> - match mod_type with - | Declarations.MoreFunctor _ -> nYI "functors" - | Declarations.NoFunctor contents -> - CList.flatten (CList.map in_elpi_modty_item contents) -[%%else] let rec in_elpi_module_item ~depth path state (name, item) = let open Declarations in match item with @@ -3786,7 +3652,6 @@ and in_elpi_modty : 'a.'a Declarations.generic_module_body -> string list = | Declarations.MoreFunctor _ -> nYI "functors" | Declarations.NoFunctor contents -> CList.flatten (CList.map in_elpi_modty_item contents) -[%%endif] let in_elpi_module ~depth s (x : Declarations.module_body) = in_elpi_module ~depth s x diff --git a/src/coq_elpi_HOAS.mli b/src/coq_elpi_HOAS.mli index aa94e1f48..6e5866a35 100644 --- a/src/coq_elpi_HOAS.mli +++ b/src/coq_elpi_HOAS.mli @@ -31,26 +31,6 @@ type universe_decl_option = | Cumulative of universe_decl_cumul | NonCumulative of universe_decl -[%%if coq = "8.19"] -type options = { - hoas_holes : hole_mapping option; - local : bool option; - deprecation : Deprecation.t option; - primitive : bool option; - failsafe : bool; (* readback is resilient to illformed terms *) - ppwidth : int; - pp : ppoption; - pplevel : Constrexpr.entry_relative_level; - using : string option; - inline : Declaremods.inline; - uinstance : uinstanceoption; - universe_decl : universe_decl_option; - reversible : bool option; - keepunivs : bool option; - redflags : RedFlags.reds option; - no_tc: bool option; -} -[%%else] type options = { hoas_holes : hole_mapping option; local : bool option; @@ -69,7 +49,6 @@ type options = { redflags : RedFlags.reds option; no_tc: bool option; } -[%%endif] type 'a coq_context = { (* Elpi representation of the context *) @@ -131,15 +110,9 @@ val lp2skeleton : type coercion_status = Regular | Off | Reversible type record_field_spec = { name : Name.t; is_coercion : coercion_status; is_canonical : bool } -[%%if coq = "8.19"] -val lp2inductive_entry : - depth:int -> empty coq_context -> constraints -> State.t -> term -> - State.t * ('a list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals -[%%else] val lp2inductive_entry : depth:int -> empty coq_context -> constraints -> State.t -> term -> State.t * (DeclareInd.default_dep_elim list * Entries.mutual_inductive_entry * Univ.ContextSet.t * UnivNames.universe_binders * (bool * record_field_spec list) option * DeclareInd.one_inductive_impls list) * Conversion.extra_goals -[%%endif] val inductive_decl2lp : depth:int -> empty coq_context -> constraints -> State.t -> (Names.MutInd.t * UVars.Instance.t * (Declarations.mutual_inductive_body * Declarations.one_inductive_body) * (Glob_term.binding_kind list * Glob_term.binding_kind list list)) -> @@ -205,11 +178,7 @@ val global_constant_of_globref : Names.GlobRef.t -> global_constant val abbreviation : Globnames.abbreviation Conversion.t val implicit_kind : Glob_term.binding_kind Conversion.t val collect_term_variables : depth:int -> term -> Names.Id.t list -[%%if coq = "8.19"] -type pstring = string -[%%else] type pstring = Pstring.t -[%%endif] type primitive_value = | Uint63 of Uint63.t | Float64 of Float64.t diff --git a/src/coq_elpi_arg_HOAS.ml b/src/coq_elpi_arg_HOAS.ml index 4476d771c..8a3cfff41 100644 --- a/src/coq_elpi_arg_HOAS.ml +++ b/src/coq_elpi_arg_HOAS.ml @@ -18,11 +18,7 @@ let push_name x = function { x with Genintern.genv = Environ.push_named decl x.Genintern.genv } | _ -> x -[%%if coq = "8.19"] -let push_gdecl (name,_,_,_) x = push_name x name -[%%else] let push_gdecl (name,_,_,_,_) x = push_name x name -[%%endif] let push_glob_ctx glob_ctx x = List.fold_right push_gdecl glob_ctx x @@ -47,16 +43,6 @@ let intern_global_constr_ty { Ltac_plugin.Tacintern.genv = env } ~intern_env ?(e let intern_global_context { Ltac_plugin.Tacintern.genv = env } ~intern_env ctx = Constrintern.intern_context env ~bound_univs:UnivNames.empty_binders intern_env ctx -[%%if coq = "8.19"] -let intern_one h = - let open Constrexpr in - match h with - | CLocalAssum(nl,Default bk,_) -> nl |> List.map (fun n -> n.CAst.v,bk,None,mkGHole) - | CLocalAssum(nl,Generalized(bk,_),_) -> nl |> List.map (fun n -> n.CAst.v,bk,None,mkGHole) - | CLocalDef (n,_,None) -> [n.CAst.v,Glob_term.Explicit,None,mkGHole] - | CLocalDef (n,_,Some _) -> [n.CAst.v,Glob_term.Explicit,Some mkGHole,mkGHole] - | CLocalPattern _ -> nYI "irrefutable pattern in synterp" -[%%else] let intern_one h = let open Constrexpr in match h with @@ -65,13 +51,7 @@ let intern_one h = | CLocalDef (n,_,_,None) -> [n.CAst.v,None,Glob_term.Explicit,None,mkGHole] | CLocalDef (n,_,_,Some _) -> [n.CAst.v,None,Glob_term.Explicit,Some mkGHole,mkGHole] | CLocalPattern _ -> nYI "irrefutable pattern in synterp" -[%%endif] - -[%%if coq = "8.19"] -let drop_relevance x = x -[%%else] let drop_relevance (a,_,c,d,e) = (a,c,d,e) -[%%endif] let intern_global_context_synterp (ctx : Constrexpr.local_binder_expr list) : Glob_term.glob_decl list = CList.concat_map intern_one ctx |> List.rev @@ -231,7 +211,7 @@ let univpoly_of ~poly ~cumulative = | true, false -> Poly | false, _ -> Mono -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let of_coq_inductive_definition id = let open Vernacentries.Preprocessed_Mind_decl in let { flags; typing_flags; private_ind; uniform; inductives } = id in @@ -283,7 +263,7 @@ let of_coq_inductive_definition id = } [%%endif] -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let of_coq_record_definition id = let open Vernacentries.Preprocessed_Mind_decl in let { flags; primitive_proj; kind; records; } : record = id in @@ -334,13 +314,8 @@ let of_coq_record_definition id = [%%endif] let intern_record_decl glob_sign (it : raw_record_decl) = glob_sign, it -[%%if coq = "8.19"] -let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,y,z) -let dest_entry (_,_,_,x) = x -[%%else] let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z) let dest_entry (_,_,_,_,x) = x -[%%endif] let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi = let name, space = sep_last_qualid name in @@ -363,11 +338,7 @@ let raw_record_decl_to_glob_synterp ({ name; sort; parameters; constructor; fiel [] fields in { name = (space, Names.Id.of_string name); arity; params; constructorname = constructor; fields = List.rev fields; univpoly } -[%%if coq = "8.19"] -let expr_Type_sort = Glob_term.UAnonymous {rigid=UState.univ_rigid} -[%%else] let expr_Type_sort = Constrexpr_ops.expr_Type_sort -[%%endif] let raw_record_decl_to_glob glob_sign ({ name; sort; parameters; constructor; fields; univpoly } : raw_record_decl_elpi) : glob_record_decl_elpi = let name, space = sep_last_qualid name in @@ -453,11 +424,7 @@ let raw_decl_name_to_glob name = let name, space = sep_last_qualid name in (space, Names.Id.of_string name) -[%%if coq = "8.19"] -let interp_red_expr = Ltac_plugin.Tacinterp.interp_redexp -[%%else] let interp_red_expr = Redexpr.interp_redexp_no_ltac -[%%endif] let raw_constant_decl_to_constr ~depth coq_ctx state { name; typ = (bl,typ); body; red; udecl; atts } = let env = coq_ctx.env in @@ -848,18 +815,6 @@ let cdecl2lp ~depth state { Cmd.name; params; typ; body; udecl } = let ctxitemc = E.Constants.declare_global_symbol "context-item" let ctxendc = E.Constants.declare_global_symbol "context-end" -[%%if coq = "8.19"] -let rec do_context_glob_synterp fields ~depth state = - match fields with - | [] -> state, E.mkGlobal ctxendc - | (name,bk,bo,ty) :: fields -> - let ty = E.mkDiscard in - let bo = Option.map (fun _ -> E.mkDiscard) bo in - let state, fields = do_context_glob_synterp 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] -[%%else] let rec do_context_glob_synterp fields ~depth state = match fields with | [] -> state, E.mkGlobal ctxendc @@ -870,21 +825,7 @@ let rec do_context_glob_synterp fields ~depth state = 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] -[%%endif] -[%%if coq = "8.19"] -let rec do_context_glob fields ~depth state = - match fields with - | [] -> state, E.mkGlobal ctxendc - | (name,bk,bo,ty) :: fields -> - let open Coq_elpi_glob_quotation in - let state, ty = gterm2lp ~depth state ty in - let state, bo = option_map_acc (gterm2lp ~depth) state bo in - let state, fields, () = under_ctx name ty bo (nogls (do_context_glob 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] -[%%else] let rec do_context_glob fields ~depth state = match fields with | [] -> state, E.mkGlobal ctxendc @@ -896,7 +837,6 @@ let rec do_context_glob fields ~depth state = 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] -[%%endif] let rec do_context_constr coq_ctx csts fields ~depth state = let map s x = constr2lp coq_ctx csts ~depth s (EConstr.of_constr x) in match fields with @@ -1049,7 +989,7 @@ let handle_template_polymorphism = function | Some false -> Some false | Some true -> err Pp.(str "#[universes(template)] is not supported") -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let handle_template_polymorphism flags = let open Vernacentries.Preprocessed_Mind_decl in { flags with template = handle_template_polymorphism flags.template } @@ -1083,7 +1023,7 @@ let in_elpi_cmd_synterp ~depth ?calldepth state (x : Cmd.raw) = | Term raw_term -> state, E.mkApp trmc E.mkDiscard [], [] -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let dest_rdecl raw_rdecl = let open Vernacentries.Preprocessed_Mind_decl in let { flags = ({ template; poly; cumulative; udecl; finite } as flags); primitive_proj; kind; records } = raw_rdecl in @@ -1101,7 +1041,7 @@ let interp_structure ~flags udecl kind ~primitive_proj x = Record.interp_structure ~flags udecl kind ~primitive_proj x [%%endif] -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let dest_idecl raw_indt = let open Vernacentries.Preprocessed_Mind_decl in let { flags = ({ udecl } as flags); typing_flags; uniform; private_ind; inductives } = raw_indt in diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg index 4e805675a..6028ce747 100644 --- a/src/coq_elpi_arg_syntax.mlg +++ b/src/coq_elpi_arg_syntax.mlg @@ -222,7 +222,7 @@ END { -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let mkAttributesFlagQualid q = Attributes.FlagIdent (Names.Id.to_string (Libnames.qualid_basename q)) [%%else] let mkAttributesFlagQualid q = Attributes.FlagQualid q diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index 1162d041b..dff9ba2e9 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -427,7 +427,7 @@ let tc_instance = let open Conv in let open API.AlgebraicData in declare { M (fun ~ok ~ko { implementation; priority } -> ok implementation priority)); ]} |> CConv.(!<) -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let clenv_missing sigma ce cty = let rec nb_hyp sigma c = match EConstr.kind sigma c with | Prod(_,_,c2) -> if EConstr.Vars.noccurn sigma 1 c2 then 1+(nb_hyp sigma c2) else nb_hyp sigma c2 @@ -523,7 +523,7 @@ let set_accumulate_to_db_interp, get_accumulate_to_db_interp = (fun x -> f := x), (fun () -> !f) -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let is_global_level env u = try let set = Univ.Level.Set.singleton u in @@ -892,34 +892,6 @@ let warn_deprecated_add_axiom = "section variables is deprecated. Use coq.env.add-axiom or " ^ "coq.env.add-section-variable instead")) -[%%if coq = "8.19"] -let comAssumption_declare_variable id coe ~kind ty ~univs:uentry ~impargs ex ~name = - ComAssumption.declare_variable coe ~kind ty uentry impargs ex name; - GlobRef.VarRef id, UVars.Instance.empty -let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name ~id:_ ty = - ComAssumption.declare_axiom coe ~local ~kind ty univs impargs inline name -let declare_mutual_inductive_with_eliminations ~primitive_expected ~default_dep_elim:_ x y z = - DeclareInd.declare_mutual_inductive_with_eliminations ~primitive_expected x y z - -let cinfo_make state types using = - let using = Option.map Proof_using.(fun s -> - let sigma = get_sigma state in - let types = Option.List.cons types [] in - let using = using_from_string s in - definition_using (get_global_env state) sigma ~fixnames:[] ~using ~terms:types) - using in - Declare.CInfo.make ?using -let eval_of_constant c = - match c with - | Variable v -> Tacred.EvalVarRef v - | Constant c -> Tacred.EvalConstRef c -let eval_to_oeval = function -| Tacred.EvalVarRef v -> Names.VarKey v -| Tacred.EvalConstRef c -> Names.ConstKey c -let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,y,z) -let pattern_of_glob_constr _ g = Patternops.pattern_of_glob_constr g -let warns_of_options options = options.deprecation -[%%else] let comAssumption_declare_variable id coe ~kind ty ~univs ~impargs impl ~name:_ = ComAssumption.declare_variable ~coe ~kind ty ~univs ~impargs ~impl ~name:id let comAssumption_declare_axiom coe ~local ~kind ~univs ~impargs ~inline ~name:_ ~id ty = @@ -939,13 +911,8 @@ let eval_of_constant c = let eval_to_oeval = Evaluable.to_kevaluable let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z) let pattern_of_glob_constr env g = Patternops.pattern_of_glob_constr env g -[%%endif] -[%%if coq = "8.19"] -let declare_definition hack _using ~cinfo ~info ~opaque ~body sigma = - let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body sigma in - gr, Option.get !hack -[%%elif coq = "8.20"] +[%%if coq = "8.20"] let declare_definition hack using ~cinfo ~info ~opaque ~body sigma = let using = Option.map Proof_using.using_from_string using in let gr = Declare.declare_definition ~cinfo ~info ~opaque ~body ?using sigma in @@ -959,7 +926,7 @@ let declare_definition _ using ~cinfo ~info ~opaque ~body sigma = [%%if coq = "8.20"] let warns_of_options options = options.user_warns -[%%elif coq <> "8.19"] +[%%else] let warns_of_options options = options.user_warns |> Option.map UserWarn.with_empty_qf [%%endif] let add_axiom_or_variable api id ty local options state = @@ -1348,7 +1315,7 @@ let coq_header_builtins = |}; ] -[%%if coq = "8.19" || coq = "8.20" ] +[%%if coq = "8.20" ] let compat_reduction_behavior_set ~local gref strategy = Reductionops.ReductionBehaviour.set ~local gref strategy [%%else] @@ -1356,7 +1323,7 @@ let compat_reduction_behavior_set ~local gref strategy = Reductionops.ReductionBehaviour.set ~local gref (Some strategy) [%%endif] -[%%if coq = "8.19" || coq = "8.20" ] +[%%if coq = "8.20" ] let compat_reset_simplification = [] [%%else] let compat_reset_simplification = diff --git a/src/coq_elpi_builtins_synterp.ml b/src/coq_elpi_builtins_synterp.ml index 28b54fc8d..ecbf203e9 100644 --- a/src/coq_elpi_builtins_synterp.ml +++ b/src/coq_elpi_builtins_synterp.ml @@ -567,7 +567,7 @@ module SynterpAction = struct type 'a replay = 'a -> State.t -> State.t * ModPath.t option - [%%if coq = "8.19" || coq = "8.20"] + [%%if coq = "8.20"] let interp_close_section = Lib.Interp.close_section [%%else] let interp_close_section = Declaremods.Interp.close_section @@ -938,7 +938,7 @@ let attribute_value = let open API.AlgebraicData in let open CConv in declare { let attribute = attribute attribute_value -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let synterp_close_section = Lib.Synterp.close_section [%%else] let synterp_close_section = Declaremods.Synterp.close_section diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index e3c981f4a..1f560a2df 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -35,15 +35,6 @@ let get_ctx, set_ctx, _update_ctx = let set_coq_ctx_hyps s (x,h) = set_ctx s (Some (upcast @@ x, h)) -[%%if coq = "8.19"] -let glob_intros ctx bo = - List.fold_right (fun (name,_,ov,ty) bo -> - DAst.make - (match ov with - | None -> GLambda(name,Explicit,ty,bo) - | Some v -> GLetIn(name,v,Some ty,bo))) - ctx bo -[%%else] let glob_intros ctx bo = List.fold_right (fun (name,r,_,ov,ty) bo -> DAst.make @@ -51,17 +42,7 @@ let glob_intros ctx bo = | None -> GLambda(name,r,Explicit,ty,bo) | Some v -> GLetIn(name,r,v,Some ty,bo))) ctx bo -[%%endif] -[%%if coq = "8.19"] -let glob_intros_prod ctx bo = - List.fold_right (fun (name,_,ov,ty) bo -> - DAst.make - (match ov with - | None -> GProd(name,Explicit,ty,bo) - | Some v -> GLetIn(name,v,Some ty,bo))) - ctx bo -[%%else] let glob_intros_prod ctx bo = List.fold_right (fun (name,r,_,ov,ty) bo -> DAst.make @@ -69,7 +50,6 @@ let glob_intros_prod ctx bo = | None -> GProd(name,r,Explicit,ty,bo) | Some v -> GLetIn(name,r,v,Some ty,bo))) ctx bo -[%%endif] (* HACK: names not visible by evars *) @@ -162,15 +142,6 @@ let glob_level loc state = function let nogls f ~depth state x = let state, x = f ~depth state x in state, x, () let noglsk f ~depth state = let state, x = f ~depth state in state, x, () -[%%if coq = "8.19"] -let rigid_anon_type = function GSort(UAnonymous {rigid=UnivRigid}) -> true | _ -> false -let named_type = function GSort(UNamed _) -> true | _ -> false -let name_of_type = function GSort(UNamed u) -> snd u | _ -> assert false -let dest_GProd = function GProd(n,_,s,t) -> n,s,t | _ -> assert false -let dest_GLambda = function GLambda(n,_,s,t) -> n,s,t | _ -> assert false -let dest_GLetIn = function GLetIn(n,bo,s,t) -> n,bo,s,t | _ -> assert false -let mkGLambda (n,b,s,t) = GLambda(n,b,s,t) -[%%else] let rigid_anon_type = function GSort(None, UAnonymous {rigid=UnivRigid}) -> true | _ -> false let named_type = function GSort(None, UNamed _) -> true | _ -> false let name_of_type = function GSort(None, UNamed u) -> u | _ -> assert false @@ -178,7 +149,6 @@ let dest_GProd = function GProd(n,_,_,s,t) -> n,s,t | _ -> assert false let dest_GLambda = function GLambda(n,_,_,s,t) -> n,s,t | _ -> assert false let dest_GLetIn = function GLetIn(n,_,bo,s,t) -> n,bo,s,t | _ -> assert false let mkGLambda (n,b,s,t) = GLambda(n,None,b,s,t) -[%%endif] let rec gterm2lp ~depth state x = debug Pp.(fun () -> @@ -424,7 +394,7 @@ let rec gterm2lp ~depth state x = | GRec _ -> nYI "(glob)HOAS mutual/non-struct fix" | GInt i -> in_elpi_primitive ~depth state (Uint63 i) | GFloat f -> in_elpi_primitive ~depth state (Float64 f) - | GString s [@if coq <> "8.19"] -> in_elpi_primitive ~depth state (Pstring s) + | GString s -> in_elpi_primitive ~depth state (Pstring s) | GArray _ -> nYI "HOAS for persistent arrays" ;; @@ -474,11 +444,7 @@ let rec do_params params kont ~depth state = let state, imp = in_elpi_imp ~depth state imp in state, in_elpi_parameter name ~imp src tgt -[%%if coq = "8.19"] -let drop_relevance x = x -[%%else] let drop_relevance (a,_,c,d,e) = (a,c,d,e) -[%%endif] let do_params params k ~depth s = do_params (List.map drop_relevance params) k ~depth s diff --git a/src/coq_elpi_utils.ml b/src/coq_elpi_utils.ml index 0560dba47..7f7022377 100644 --- a/src/coq_elpi_utils.ml +++ b/src/coq_elpi_utils.ml @@ -87,17 +87,6 @@ let string_split_on_char c s = in aux 0 0 -[%%if coq = "8.19"] -let rec mk_gforall ty = function - | (name, bk, None, t) :: ps -> DAst.make @@ Glob_term.GProd (name, bk, t, mk_gforall ty ps) - | (name, _, Some bo, t) :: ps -> DAst.make @@ Glob_term.GLetIn (name, bo, Some t, mk_gforall ty ps) - | [] -> ty - -let rec mk_gfun ty = function - | (name, bk, None, t) :: ps -> DAst.make @@ Glob_term.GLambda (name, bk, t, mk_gfun ty ps) - | (name, _, Some bo, t) :: ps -> DAst.make @@ Glob_term.GLetIn (name, bo, Some t, mk_gfun ty ps) - | [] -> ty -[%%else] let rec mk_gforall ty = function | (name, r, bk, None, t) :: ps -> DAst.make @@ Glob_term.GProd (name, r, bk, t, mk_gforall ty ps) | (name, r, _, Some bo, t) :: ps -> DAst.make @@ Glob_term.GLetIn (name, r, bo, Some t, mk_gforall ty ps) @@ -108,8 +97,6 @@ let rec mk_gfun ty = function | (name, r, _, Some bo, t) :: ps -> DAst.make @@ Glob_term.GLetIn (name, r, bo, Some t, mk_gfun ty ps) | [] -> ty -[%%endif] - let manual_implicit_of_binding_kind name = function | Glob_term.NonMaxImplicit -> CAst.make (Some (name, false)) | Glob_term.MaxImplicit -> CAst.make (Some (name, true)) @@ -121,11 +108,7 @@ let binding_kind_of_manual_implicit x = | Some (_, true) -> Glob_term.MaxImplicit | None -> Glob_term.Explicit -[%%if coq = "8.19"] -let manual_implicit_of_gdecl (name, bk, _, _) = manual_implicit_of_binding_kind name bk -[%%else] let manual_implicit_of_gdecl (name, _, bk, _, _) = manual_implicit_of_binding_kind name bk -[%%endif] let lookup_inductive env i = let mind, indbo = Inductive.lookup_mind_specif env i in @@ -188,22 +171,6 @@ let float64 : Float64.t Elpi.API.Conversion.t = constants = []; } -[%%if coq = "8.19"] -let pstring : string Elpi.API.Conversion.t = - let open Elpi.API.OpaqueData in - declare { - name = "pstring"; - doc = ""; - pp = (fun fmt _ -> Format.fprintf fmt "%S" "primitive strings not supported in Coq 8.19" ); - compare = (fun _ _ -> 0); - hash = (fun _ -> 0); - hconsed = false; - constants = []; - } - -let pstring_of_string x = Some x -let string_of_pstring x = x -[%%else] let pstring : Pstring.t Elpi.API.Conversion.t = let open Elpi.API.OpaqueData in declare { @@ -217,7 +184,6 @@ let pstring : Pstring.t Elpi.API.Conversion.t = } let pstring_of_string = Pstring.of_string let string_of_pstring = Pstring.to_string -[%%endif] let debug = CDebug.create ~name:"elpi" () @@ -286,20 +252,6 @@ let detype_level sigma l = let open Glob_term in UNamed (detype_level_name sigma l) -[%%if coq = "8.19"] -let detype_universe sigma u = List.map (Util.on_fst (detype_level_name sigma)) (Univ.Universe.repr u) - -let detype_sort ku sigma x = - let open Sorts in - let open Glob_term in - match x with - | Prop -> UNamed (None, [ (GProp, 0) ]) - | SProp -> UNamed (None, [ (GSProp, 0) ]) - | Set -> UNamed (None, [ (GSet, 0) ]) - | Type u when ku -> UNamed (None, detype_universe sigma u) - | QSort (q, u) when ku -> UNamed (Some (detype_qvar sigma q), detype_universe sigma u) - | _ -> UAnonymous { rigid = UState.UnivRigid } -[%%else] let detype_universe sigma u = Glob_term.UNamed (List.map (Util.on_fst (detype_level_name sigma)) (Univ.Universe.repr u)) let detype_sort ku sigma x = @@ -313,7 +265,6 @@ let detype_sort ku sigma x = | Type u when ku -> None, detype_universe sigma u | QSort (q, u) when ku -> Some (detype_qvar sigma q), detype_universe sigma u | _ -> glob_Type_sort -[%%endif] (* let detype_relevance_info sigma na = @@ -335,21 +286,6 @@ let detype_instance ku sigma l = let us = List.map (detype_level sigma) (Array.to_list us) in Some (qs, us) -[%%if coq = "8.19"] -let it_destRLambda_or_LetIn_names l c = - let open Glob_term in - let rec aux l nal c = - match (DAst.get c, l) with - | _, [] -> (List.rev nal, c) - | GLambda (na, _, _, c), false :: l -> aux l (na :: nal) c - | GLetIn (na, _, _, c), true :: l -> aux l (na :: nal) c - | _ -> nYI "detype eta" - in - aux l [] c -let rec decompose accu c = match DAst.get c with -| Glob_term.GLambda (na, _, _, c) -> decompose (na :: accu) c -| _ -> List.rev accu, c -[%%else] let it_destRLambda_or_LetIn_names l c = let open Glob_term in let rec aux l nal c = @@ -364,94 +300,6 @@ let rec decompose accu c = match DAst.get c with | Glob_term.GLambda (na, _, _, _, c) -> decompose (na :: accu) c | _ -> List.rev accu, c -[%%endif] - -[%%if coq = "8.19"] - -(** Reimplementation of kernel case expansion functions in more lenient way *) -module RobustExpand : sig - val return_clause : - Environ.env -> - Evd.evar_map -> - Names.Ind.t -> - EConstr.EInstance.t -> - EConstr.t array -> - EConstr.case_return -> - EConstr.rel_context * EConstr.t - - val branch : - Environ.env -> - Evd.evar_map -> - Names.Construct.t -> - EConstr.EInstance.t -> - EConstr.t array -> - EConstr.case_branch -> - EConstr.rel_context * EConstr.t -end = struct - open Context.Rel.Declaration - open Declarations - open UVars - open Constr - open Vars - - let instantiate_context u subst nas ctx = - let rec instantiate i ctx = - match ctx with - | [] -> [] - | LocalAssum (_, ty) :: ctx -> - let ctx = instantiate (pred i) ctx in - let ty = substnl subst i (subst_instance_constr u ty) in - LocalAssum (nas.(i), ty) :: ctx - | LocalDef (_, ty, bdy) :: ctx -> - let ctx = instantiate (pred i) ctx in - let ty = substnl subst i (subst_instance_constr u ty) in - let bdy = substnl subst i (subst_instance_constr u bdy) in - LocalDef (nas.(i), ty, bdy) :: ctx - in - let () = if not (Int.equal (Array.length nas) (List.length ctx)) then raise_notrace Exit in - instantiate (Array.length nas - 1) ctx - - let return_clause env sigma ind u params ((nas, p), _) = - try - let u = EConstr.Unsafe.to_instance u in - let params = EConstr.Unsafe.to_constr_array params in - let () = if not @@ Environ.mem_mind (fst ind) env then raise_notrace Exit in - let mib = Environ.lookup_mind (fst ind) env in - let mip = mib.mind_packets.(snd ind) in - let paramdecl = subst_instance_context u mib.mind_params_ctxt in - let paramsubst = subst_of_rel_context_instance paramdecl params in - let realdecls, _ = CList.chop mip.mind_nrealdecls mip.mind_arity_ctxt in - let self = - let args = Context.Rel.instance mkRel 0 mip.mind_arity_ctxt in - let inst = Instance.(abstract_instance (length u)) in - mkApp (mkIndU (ind, inst), args) - in - let realdecls = LocalAssum (Context.anonR, self) :: realdecls in - let realdecls = instantiate_context u paramsubst nas realdecls in - (List.map EConstr.of_rel_decl realdecls, p) - with e when CErrors.noncritical e -> - let dummy na = LocalAssum (na, EConstr.mkProp) in - (List.rev (CArray.map_to_list dummy nas), p) - - let branch env sigma (ind, i) u params (nas, br) = - try - let u = EConstr.Unsafe.to_instance u in - let params = EConstr.Unsafe.to_constr_array params in - let () = if not @@ Environ.mem_mind (fst ind) env then raise_notrace Exit in - let mib = Environ.lookup_mind (fst ind) env in - let mip = mib.mind_packets.(snd ind) in - let paramdecl = subst_instance_context u mib.mind_params_ctxt in - let paramsubst = subst_of_rel_context_instance paramdecl params in - let ctx, _ = mip.mind_nf_lc.(i - 1) in - let ctx, _ = CList.chop mip.mind_consnrealdecls.(i - 1) ctx in - let ctx = instantiate_context u paramsubst nas ctx in - (List.map EConstr.of_rel_decl ctx, br) - with e when CErrors.noncritical e -> - let dummy na = LocalAssum (na, EConstr.mkProp) in - (List.rev (CArray.map_to_list dummy nas), br) -end - -[%%else] module RobustExpand : sig @@ -536,21 +384,6 @@ let branch env sigma (ind, i) u params (nas, br) = end -[%%endif] - -[%%if coq = "8.19"] -let mk_glob_decl_g _ na x y z = Context.binder_name na, x, y, z -let mkGProd _ na x y z = Glob_term.GProd(Context.binder_name na, x, y, z) -let mkGLambda _ na x y z = Glob_term.GLambda(Context.binder_name na, x, y, z) -let mkGLetIn _ na x y z = Glob_term.GLetIn(Context.binder_name na, x, y, z) -let get_ind_tags _ ci _ = ci.Constr.ci_pp_info.ind_tags -let get_cstr_tags _ ci _ = ci.Constr.ci_pp_info.cstr_tags -let get_GLambda_name_tgt typ = - match DAst.get typ with - | Glob_term.GLambda (x, _, t, c) -> (x, c) - | _ -> (Anonymous, typ) -let detype_primitive_string _ = assert false -[%%else] let detype_relevance_info sigma na = match EConstr.ERelevance.kind sigma na with | Relevant -> Some Glob_term.GRelevant @@ -587,7 +420,6 @@ let get_GLambda_name_tgt typ = let detype_primitive_string = function | Constr.String s -> DAst.make @@ Glob_term.GString s | _ -> assert false -[%%endif] [%%if coq = "8.19" || coq = "8.20" ] let fresh (names, e) sigma name ty = diff --git a/src/coq_elpi_utils.mli b/src/coq_elpi_utils.mli index 3ba93702c..6b543bba0 100644 --- a/src/coq_elpi_utils.mli +++ b/src/coq_elpi_utils.mli @@ -20,13 +20,8 @@ val err : ?loc:Elpi.API.Ast.Loc.t -> Pp.t -> 'a exception LtacFail of int * Pp.t val ltac_fail_err : ?loc:Elpi.API.Ast.Loc.t -> int -> Pp.t -> 'a val nYI : string -> 'a -[%%if coq = "8.19"] -val safe_destApp : Evd.evar_map -> - EConstr.t -> (EConstr.t,EConstr.types,EConstr.ESorts.t, EConstr.EInstance.t) Constr.kind_of_term * EConstr.t array -[%%else] val safe_destApp : Evd.evar_map -> EConstr.t -> (EConstr.t,EConstr.types,EConstr.ESorts.t, EConstr.EInstance.t, EConstr.ERelevance.t) Constr.kind_of_term * EConstr.t array -[%%endif] val mkGHole : Glob_term.glob_constr val pp2string : (Format.formatter -> 'a -> unit) -> 'a -> string val mkApp : depth:int -> Elpi.API.RawData.term -> Elpi.API.RawData.term list -> Elpi.API.RawData.term @@ -50,15 +45,9 @@ val fold_elpi_term : val uint63 : Uint63.t Elpi.API.Conversion.t val float64 : Float64.t Elpi.API.Conversion.t val projection : Names.Projection.t Elpi.API.Conversion.t -[%%if coq = "8.19"] -val pstring : string Elpi.API.Conversion.t -val pstring_of_string : string -> string option -val string_of_pstring : string -> string -[%%else] val pstring : Pstring.t Elpi.API.Conversion.t val pstring_of_string : string -> Pstring.t option val string_of_pstring : Pstring.t -> string -[%%endif] val debug : CDebug.t val elpitime : CDebug.t diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml index f18d76286..8d7f5c14c 100644 --- a/src/coq_elpi_vernacular.ml +++ b/src/coq_elpi_vernacular.ml @@ -33,8 +33,8 @@ let atts2impl loc phase ~depth state atts q = and convert_att att = convert_att_r att.CAst.v and convert_atts l = List.map convert_att l and convert_att_value = function - | Attributes.FlagIdent s [@if coq = "8.19" || coq = "8.20"] -> AttributeString s - | Attributes.FlagQualid q [@if coq <> "8.19" && coq <> "8.20"] -> AttributeString (Libnames.string_of_qualid q) + | Attributes.FlagIdent s [@if coq = "8.20"] -> AttributeString s + | Attributes.FlagQualid q [@if coq <> "8.20"] -> AttributeString (Libnames.string_of_qualid q) | Attributes.FlagString s -> AttributeString s in let phase = match phase with Summary.Stage.Interp -> "interp" | Summary.Stage.Synterp -> "synterp" in @@ -194,7 +194,7 @@ let get_and_compile ?even_if_empty name : (EC.program * bool) option = Coq_elpi_utils.elpitime (fun _ -> Pp.(str(Printf.sprintf "Elpi: get_and_compile %1.4f" (Unix.gettimeofday () -. t)))); res -[%%if coq = "8.19" || coq = "8.20"] +[%%if coq = "8.20"] let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,CErrors.iprint ei))) [%%else] let feedback_error loc ei = Feedback.(feedback (Message(Error,loc,[],CErrors.iprint ei))) diff --git a/theories/elpi.v.in b/theories/elpi.v.in index 4379d648d..a975056e6 100644 --- a/theories/elpi.v.in +++ b/theories/elpi.v.in @@ -50,10 +50,8 @@ Register Coq.Bool.Bool.ReflectF as elpi.ReflectF. Register Coq.Bool.Bool.ReflectT as elpi.ReflectT. From Coq Require PrimFloat PrimInt63. -#[skip="8.19"] From Coq Require PrimString. -#[only="8.19"] From Coq Require String. +From Coq Require PrimString. Register Coq.Floats.PrimFloat.float as elpi.float64. Register Coq.Numbers.Cyclic.Int63.PrimInt63.int as elpi.uint63. -#[skip="8.19"] Register Coq.Strings.PrimString.string as elpi.pstring. -#[only="8.19"] Register Coq.Strings.String.string as elpi.pstring. +Register Coq.Strings.PrimString.string as elpi.pstring.