diff --git a/.github/workflows/nix-action-coq-8.15.yml b/.github/workflows/nix-action-coq-8.15.yml index c02f572e4..af72e4639 100644 --- a/.github/workflows/nix-action-coq-8.15.yml +++ b/.github/workflows/nix-action-coq-8.15.yml @@ -141,6 +141,7 @@ jobs: mathcomp-analysis: needs: - coq + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -176,18 +177,10 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --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.15" - --argstr job "mathcomp-ssreflect" - 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.15" --argstr job "mathcomp-field" - - 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.15" - --argstr job "mathcomp-finmap" - 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.15" @@ -196,6 +189,10 @@ jobs: name: 'Building/fetching previous CI target: mathcomp-real-closed' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-real-closed" + - 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.15" + --argstr job "mathcomp-classical" - 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.15" @@ -204,6 +201,64 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15" --argstr job "mathcomp-analysis" + mathcomp-classical: + needs: + - coq + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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.15\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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.15" + --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.15" + --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.15" + --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.15" + --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.15" + --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.15" + --argstr job "mathcomp-classical" mathcomp-single: needs: - coq diff --git a/.github/workflows/nix-action-coq-8.16.yml b/.github/workflows/nix-action-coq-8.16.yml index a224c784c..8aadff070 100644 --- a/.github/workflows/nix-action-coq-8.16.yml +++ b/.github/workflows/nix-action-coq-8.16.yml @@ -35,9 +35,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "coq" - coq-elpi: + graph-theory: needs: - coq + - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,23 +64,34 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target graph-theory run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-8.16\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\ - echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ - \ \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.16\" --argstr job \"graph-theory\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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.16" --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.16" + --argstr job "mathcomp-algebra" + - 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.16" + --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.16" + --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.16" - --argstr job "coq-elpi" + --argstr job "graph-theory" hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -122,10 +134,9 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "hierarchy-builder" - mathcomp-analysis: + mathcomp: needs: - coq - - hierarchy-builder runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -151,11 +162,11 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target mathcomp-analysis + 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.16\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\ - \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ - \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n" + \ bundle \"coq-8.16\" --argstr job \"mathcomp\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\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.16" @@ -165,29 +176,32 @@ jobs: run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" --argstr job "mathcomp-ssreflect" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-field' + name: 'Building/fetching previous CI target: mathcomp-fingroup' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-field" + --argstr job "mathcomp-fingroup" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-algebra' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-algebra" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-real-closed' + name: 'Building/fetching previous CI target: mathcomp-solvable' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "mathcomp-real-closed" + --argstr job "mathcomp-solvable" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: hierarchy-builder' + name: 'Building/fetching previous CI target: mathcomp-field' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.16" - --argstr job "hierarchy-builder" + --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.16" + --argstr job "mathcomp-character" - 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.16" - --argstr job "mathcomp-analysis" + --argstr job "mathcomp" mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -238,7 +252,6 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: diff --git a/.github/workflows/nix-action-coq-mcHB-8.16.yml b/.github/workflows/nix-action-coq-mcHB-8.16.yml index bfeab5dd5..8ce64fc4e 100644 --- a/.github/workflows/nix-action-coq-mcHB-8.16.yml +++ b/.github/workflows/nix-action-coq-mcHB-8.16.yml @@ -1,4 +1,218 @@ jobs: + QuickChick: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-mcHB-8.16\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "QuickChick" + Verdi: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target Verdi + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"Verdi\" \\\n --dry-run 2>&1 >\ + \ /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --argstr job "coq" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: Cheerios' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "Cheerios" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: InfSeqExt' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" + --argstr job "InfSeqExt" + - 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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "Verdi" + addition-chains: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target addition-chains + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"addition-chains\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "mathcomp-algebra" + - 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-mcHB-8.16" + --argstr job "mathcomp-fingroup" + - 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-mcHB-8.16" + --argstr job "paramcoq" + - 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-mcHB-8.16" + --argstr job "addition-chains" + autosubst: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target autosubst + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"autosubst\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "autosubst" coq: needs: [] runs-on: ubuntu-latest @@ -35,9 +249,10 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "coq" - coq-elpi: + coq-bits: needs: - coq + - mathcomp-algebra runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -63,19 +278,115 @@ jobs: extraPullNames: coq, coq-community name: math-comp - id: stepCheck - name: Checking presence of CI target coq-elpi + name: Checking presence of CI target coq-bits run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ - \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"coq-bits\" \\\n --dry-run 2>&1\ \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" --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-mcHB-8.16" + --argstr job "mathcomp-algebra" - 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-mcHB-8.16" - --argstr job "coq-elpi" + --argstr job "coq-bits" + coquelicot: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-mcHB-8.16\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "coquelicot" + deriving: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target deriving + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"deriving\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "deriving" fourcolor: needs: - coq @@ -135,7 +446,6 @@ jobs: hierarchy-builder: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -181,7 +491,6 @@ jobs: hierarchy-builder-shim: needs: - coq - - coq-elpi runs-on: ubuntu-latest steps: - name: Determine which commit to test @@ -224,6 +533,70 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "hierarchy-builder-shim" + interval: + needs: + - coq + - coquelicot + - mathcomp-ssreflect + - mathcomp-fingroup + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-mcHB-8.16\" --argstr job \"interval\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "interval" mathcomp: needs: - coq @@ -233,7 +606,6 @@ jobs: - mathcomp-solvable - mathcomp-field - mathcomp-character - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -310,7 +682,6 @@ jobs: - coq - mathcomp-ssreflect - mathcomp-fingroup - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -369,9 +740,9 @@ jobs: mathcomp-analysis: needs: - coq - - mathcomp-ssreflect - mathcomp-field - - mathcomp-finmap + - mathcomp-bigenough + - mathcomp-classical - hierarchy-builder runs-on: ubuntu-latest steps: @@ -407,18 +778,18 @@ jobs: name: 'Building/fetching previous CI target: coq' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --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-mcHB-8.16" - --argstr job "mathcomp-ssreflect" - 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-mcHB-8.16" --argstr job "mathcomp-field" - if: steps.stepCheck.outputs.status == 'built' - name: 'Building/fetching previous CI target: mathcomp-finmap' + name: 'Building/fetching previous CI target: mathcomp-bigenough' run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" - --argstr job "mathcomp-finmap" + --argstr job "mathcomp-bigenough" + - 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-mcHB-8.16" + --argstr job "mathcomp-classical" - 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-mcHB-8.16" @@ -427,6 +798,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-analysis" + mathcomp-bigenough: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-mcHB-8.16\" --argstr job \"mathcomp-bigenough\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "mathcomp-bigenough" mathcomp-character: needs: - coq @@ -435,7 +852,6 @@ jobs: - mathcomp-algebra - mathcomp-solvable - mathcomp-field - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -503,6 +919,67 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "mathcomp-character" + mathcomp-classical: + needs: + - coq + - mathcomp-ssreflect + - mathcomp-algebra + - mathcomp-finmap + - hierarchy-builder + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - 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-mcHB-8.16\" --argstr job \"mathcomp-classical\" \\\n --dry-run\ + \ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\ + \ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "mathcomp-classical" mathcomp-field: needs: - coq @@ -510,7 +987,6 @@ jobs: - mathcomp-fingroup - mathcomp-algebra - mathcomp-solvable - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -578,7 +1054,6 @@ jobs: needs: - coq - mathcomp-ssreflect - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -679,9 +1154,7 @@ jobs: mathcomp-single: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -740,9 +1213,7 @@ jobs: mathcomp-single-planB: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder-shim runs-on: ubuntu-latest steps: @@ -801,9 +1272,7 @@ jobs: mathcomp-single-planB-src: needs: - coq - - coq-elpi - hierarchy-builder - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -865,7 +1334,6 @@ jobs: - mathcomp-ssreflect - mathcomp-fingroup - mathcomp-algebra - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -928,7 +1396,6 @@ jobs: mathcomp-ssreflect: needs: - coq - - coq-elpi - hierarchy-builder runs-on: ubuntu-latest steps: @@ -1052,6 +1519,52 @@ jobs: name: Building/fetching current CI target run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-mcHB-8.16" --argstr job "odd-order" + reglang: + needs: + - coq + - mathcomp-ssreflect + runs-on: ubuntu-latest + steps: + - 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 if [ -z \"$merge_commit\" ]; 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@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup math-comp + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: math-comp + - id: stepCheck + name: Checking presence of CI target reglang + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"coq-mcHB-8.16\" --argstr job \"reglang\" \\\n --dry-run 2>&1\ + \ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\ + \ | grep \"built:\" | sed \"s/.*/built/\")\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-mcHB-8.16" + --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-mcHB-8.16" + --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-mcHB-8.16" + --argstr job "reglang" name: Nix CI for bundle coq-mcHB-8.16 'on': pull_request: diff --git a/.nix/config.nix b/.nix/config.nix index bd392b3cb..693054c5a 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -1,7 +1,7 @@ { format = "1.0.0"; attribute = "hierarchy-builder"; - default-bundle = "coq-8.15"; + default-bundle = "coq-rev_coerce"; bundles = let mcHBcommon = { mathcomp.override.version = "hierarchy-builder"; @@ -33,6 +33,10 @@ "coq-8.15".coqPackages = { coq.override.version = "8.15"; }; + "coq-rev_coerce".coqPackages = { + coq.override.version = "proux01:rev_coerce"; + coq-elpi.override.version = "coq-master"; + }; }; cachix.coq = {}; cachix.coq-community = {}; diff --git a/.nix/coq-nix-toolbox.nix b/.nix/coq-nix-toolbox.nix index dd2bd938d..2e80cf19b 100644 --- a/.nix/coq-nix-toolbox.nix +++ b/.nix/coq-nix-toolbox.nix @@ -1 +1 @@ -"be976db262f1dc9f6e013153f263182e14372246" +"4f0eb194b37b6e0db28be2eb4643bd6924abf7ab" diff --git a/.nix/coq-overlays/coq-elpi/default.nix b/.nix/coq-overlays/coq-elpi/default.nix deleted file mode 100644 index 6c564594c..000000000 --- a/.nix/coq-overlays/coq-elpi/default.nix +++ /dev/null @@ -1,63 +0,0 @@ -{ lib, mkCoqDerivation, which, coq, version ? null }: - -with builtins; with lib; let - elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [ - { case = "8.11"; out = { version = "1.11.4"; };} - { case = "8.12"; out = { version = "1.12.0"; };} - { case = "8.13"; out = { version = "1.13.7"; };} - { case = "8.14"; out = { version = "1.13.7"; };} - { case = "8.15"; out = { version = "1.16.5"; };} - { case = "8.16"; out = { version = "1.16.5"; };} - ] {} ); -in mkCoqDerivation { - pname = "elpi"; - repo = "coq-elpi"; - owner = "LPCIC"; - inherit version; - defaultVersion = lib.switch coq.coq-version [ - { case = "8.16"; out = "1.15.3"; } - { case = "8.15"; out = "1.14.0"; } - { case = "8.14"; out = "1.11.2"; } - { case = "8.13"; out = "1.11.1"; } - { case = "8.12"; out = "1.8.3_8.12"; } - { case = "8.11"; out = "1.6.3_8.11"; } - ] null; - release."1.15.3".sha256 = "0vsgpflvfbbpbri3xfdhkz24bc36gy90f0mh0nr9ml6pqyp0ygji"; - release."1.14.0".sha256 = "1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp"; - release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n"; - release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY="; - release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4"; - release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc"; - release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk"; - release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1"; - release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6"; - release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq"; - release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z"; - release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07"; - release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557"; - release."1.8.3_8.12".version = "1.8.3"; - release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y"; - release."1.8.2_8.12".version = "1.8.2"; - release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r"; - release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1"; - release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8"; - release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp"; - release."1.6.3_8.11".version = "1.6.3"; - release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn"; - release."1.6.2_8.11".version = "1.6.2"; - release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53"; - release."1.6.1_8.11".version = "1.6.1"; - release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq"; - release."1.6.0_8.11".version = "1.6.0"; - release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b"; - releaseRev = v: "v${v}"; - - mlPlugin = true; - propagatedBuildInputs = [ elpi ]; - - meta = { - description = "Coq plugin embedding ELPI."; - maintainers = [ maintainers.cohencyril ]; - license = licenses.lgpl21Plus; - }; -} diff --git a/.nix/ocaml-overlays/elpi/default.nix b/.nix/ocaml-overlays/elpi/default.nix deleted file mode 100644 index bca9d8c90..000000000 --- a/.nix/ocaml-overlays/elpi/default.nix +++ /dev/null @@ -1,53 +0,0 @@ -{ lib -, buildDunePackage, camlp5 -, ocaml -, menhir, menhirLib -, stdlib-shims -, re, perl, ncurses -, ppxlib, ppx_deriving, atdgen -, coqPackages -, version ? if lib.versionAtLeast ocaml.version "4.07" then "1.16.2" else "1.14.1" -}: -with lib; -let fetched = coqPackages.metaFetch ({ - release."1.16.5".sha256 = "sha256:1l6grpglkvyyj0p01l0q5ih12lp4vizamgj7i63ig82gqpyzk9dl"; - release."1.16.2".sha256 = "sha256:0j4vbqbcz971pfhp8gxiaqpkzsjiisjgpybf6z1i65f1pavyfyss"; - release."1.15.2".sha256 = "sha256-XgopNP83POFbMNyl2D+gY1rmqGg03o++Ngv3zJfCn2s="; - release."1.15.0".sha256 = "sha256:1ngdc41sgyzyz3i3lkzjhnj66gza5h912virkh077dyv17ysb6ar"; - release."1.14.1".sha256 = "sha256-BZPVL8ymjrE9kVGyf6bpc+GA2spS5JBpkUtZi04nPis="; - release."1.13.7".sha256 = "10fnwz30bsvj7ii1vg4l1li5pd7n0qqmwj18snkdr5j9gk0apc1r"; - release."1.13.5".sha256 = "02a6r23mximrdvs6kgv6rp0r2dgk7zynbs99nn7lphw2c4189kka"; - release."1.13.1".sha256 = "12a9nbdvg9gybpw63lx3nw5wnxfznpraprb0wj3l68v1w43xq044"; - release."1.13.0".sha256 = "0dmzy058m1mkndv90byjaik6lzzfk3aaac7v84mpmkv6my23bygr"; - release."1.12.0".sha256 = "1agisdnaq9wrw3r73xz14yrq3wx742i6j8i5icjagqk0ypmly2is"; - release."1.11.4".sha256 = "1m0jk9swcs3jcrw5yyw5343v8mgax238cjb03s8gc4wipw1fn9f5"; - releaseRev = v: "v${v}"; - location = { domain = "github.com"; owner = "LPCIC"; repo = "elpi"; }; - }) version; -in -buildDunePackage rec { - pname = "elpi"; - inherit (fetched) version src; - - minimalOCamlVersion = "4.04"; - - buildInputs = [ perl ncurses ] - ++ optional (versionAtLeast version "1.15" || version == "dev") menhir; - - propagatedBuildInputs = [ re stdlib-shims ] - ++ (if versionAtLeast version "1.15" || version == "dev" - then [ menhirLib ] - else [ camlp5 ] ) - ++ [ ppxlib ppx_deriving atdgen ]; - - meta = { - description = "Embeddable λProlog Interpreter"; - license = licenses.lgpl21Plus; - maintainers = [ maintainers.vbgl ]; - homepage = "https://github.com/LPCIC/elpi"; - }; - - postPatch = '' - substituteInPlace elpi_REPL.ml --replace "tput cols" "${ncurses}/bin/tput cols" - ''; -} diff --git a/Changelog.md b/Changelog.md index 1ed500838..c69398bd5 100644 --- a/Changelog.md +++ b/Changelog.md @@ -1,5 +1,32 @@ # Changelog +## UNRELEASED + +## [1.4.0] - 2022-09-29 + +Compatible with +- Coq 8.15 with Coq-Elpi 1.14.x +- Coq 8.16 with Coq-Elpi 1.15.x and 1.16.x + +### General + +- **Fix** `HB.pack` works with structures about functions, and not just types. +- **Fix** `HB.about` and `HB.graph` now display shortest names. +- **New** Command `HB.howto` to find all possible ways to instanciate structures. +- **New** Structures now support keys which type's head is a global reference. + (Only keys corresponding to the coercion classes `Sortclass` and `Funclass` were accepted). + +## [1.3.0] - 2022-07-27 + +Compatible with +- Coq 8.15 with Coq-Elpi 1.14.x +- Coq 8.16 with Coq-Elpi 1.15.x + +### General + +- **Fix** Structures can be keyd on sorts (eg `Prop`) and products (eg `T -> U`) +- **New** Mixin parameters can depend on structure instances inferred using previous mixins (see [this test](tests/interleave_context.v)) + ## [1.2.1] - 2022-01-10 Compatible with diff --git a/HB/about.elpi b/HB/about.elpi index 9e512586f..5b90cfc1d 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -15,7 +15,7 @@ main-located S (loc-gref GR) :- class-def (class Class GR MLwP), !, private.main-structure S Class GR MLwP. main-located _ (loc-gref Class) :- class-def (class Class GR MLwP), !, - gref->modname GR 2 "." M, + gref->modname_short GR "." M, coq.gref->id GR St, S is M ^ "." ^ St, private.main-structure S Class GR MLwP. @@ -45,7 +45,7 @@ main-located S (loc-gref GR) :- from Factory Mixin GR, !, private.main-builder S Factory Mixin. main-located S (loc-gref GR) :- - std.filter {coq.CS.db-for _ (cs-gref GR)} (private.not1 private.unif-hint?) LV, + std.filter {coq.CS.db-for _ (cs-gref GR)} (not1 unif-hint?) LV, coq.CS.db-for GR _ LP, std.filter {coq.coercion.db} (c\c = coercion GR _ _ _) LC, if (LV = [], LP = [], LC = []) @@ -57,6 +57,29 @@ main-located S (loc-gref GR) :- main-located S (loc-abbreviation _) :- coq.error "HB: unknown abbreviation" S. +/* things also used in paths.elpi ------------------------------------------ */ + +shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }. + +pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp. +bulletize1 F X (glue [str "- ", M]) :- F X M. + +pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. +bulletize [] _ empty. +bulletize L F (glue [brk 0 0 | PLB]) :- + std.map L (bulletize1 F) PL, + std.intersperse (brk 0 0) PL PLB. + +% Print shortest qualified identifier of the module containing a gref +pred pp-module i:gref, o:coq.pp. +pp-module GR (str ID) :- gref->modname_short GR "." ID. + +pred unif-hint? i:cs-instance. +unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_]. + +pred not1 i:(A -> prop), i:A. +not1 P X :- not (P X). + /* ------------------------------------------------------------------------- */ /* ----------------------------- private code ------------------------------ */ @@ -76,7 +99,7 @@ main-canonical-value S CanonicalValues :- group-by-loc CanonicalValues CanonicalValuesL, %format PpCanonicalValues = box (v 4) [ - str "HB: ", str S, str " is canonically equipped with mixins:", + str "HB: ", str S, str " is canonically equipped with structures:", {bulletize CanonicalValuesL pp-canonical-solution-list}], % print coq.say {coq.pp->string PpCanonicalValues}, @@ -101,7 +124,7 @@ pred pp-canonical-solution i:cs-instance, o:coq.pp. pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :- coq.env.typeof GR T, coq.prod-tgt->gref T F, - if (class-def (class _ F _)) (gref->modname F 2 "." ID) (coq.gref->string F ID), + if (class-def (class _ F _)) (gref->modname_short F "." ID) (coq.gref->string F ID), Pp = box (hov 0) [ str ID ]. pred main-canonical-projection i:string, i:gref, i:list cs-instance. @@ -127,11 +150,11 @@ pred main-coercion i:string, i:list coercion. main-coercion S [coercion GR _ Src Tgt|_] :- % format if (class-def (class _ Src _) ; class-def (class Src _ _)) - (Source = str {gref->modname Src 2 "."}) + (Source = str {gref->modname_short Src "."}) (coq.term->pp (global Src) Source), if2 (Tgt = grefclass TGR) (if (class-def (class _ TGR _) ; class-def (class TGR _ _)) - (Target = str {gref->modname TGR 2 "."}) + (Target = str {gref->modname_short TGR "."}) (coq.term->pp (global TGR) Target)) (Tgt = sortclass) (Target = str "Sortclass") @@ -306,7 +329,7 @@ main-factory-alias S _Const :- pred main-builder i:string, i:factoryname, i:mixinname. main-builder _S From To :- coq.say "HB: todo HB.about for builder from" - {gref->modname From 2 "."} "to" {gref->modname To 2 "."}. + {gref->modname_short From "."} "to" {gref->modname_short To "."}. pred compute-field-info.aux i:list id, i:list implicit_kind, o:list coq.pp. compute-field-info.aux [] _ []. @@ -323,9 +346,6 @@ compute-field-info Names Impls O :- compute-field-info.aux {std.rev Names} {std.rev Impls} Pp, std.intersperse spc {std.rev Pp} O. -pred pp-module i:gref, o:coq.pp. -pp-module M (str ID) :- gref->modname M 2 "." ID. - pred pp-const i:constant, o:coq.pp. pp-const F (str ID) :- coq.gref->id (const F) ID. @@ -336,15 +356,6 @@ pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop). pp-if-verbose V P :- get-option "verbose" tt, !, P V. pp-if-verbose empty _. -pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp. -bulletize1 F X (glue [str "- ", M]) :- F X M. - -pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp. -bulletize [] _ empty. -bulletize L F (glue [brk 0 0 | PLB]) :- - std.map L (bulletize1 F) PL, - std.intersperse (brk 0 0) PL PLB. - pred pp-loc-of i:gref, o:coq.pp. pp-loc-of GR PP :- decl-location GR Loc, !, pp-loc Loc PP. pp-loc-of _ coq.pp.empty. @@ -377,10 +388,4 @@ print-docstring GR :- (coq.say {coq.pp->string (box (hov 5) [str"Doc: ",Doc])}) true. -pred unif-hint? i:cs-instance. -unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_]. - -pred not1 i:(A -> prop), i:A. -not1 P X :- not (P X). - }} diff --git a/HB/common/log.elpi b/HB/common/log.elpi index 2c3be8db9..2518b0db5 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -35,6 +35,7 @@ env.add-const-noimplicits Name Bo Ty Opaque C :- std.do! [ ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, avoid-name-collision Name Name1, + coq.typecheck Bo Ty _, coq.env.add-const Name1 Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), @@ -49,6 +50,7 @@ env.add-const Name Bo Ty Opaque C :- std.do! [ ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, avoid-name-collision Name Name1, + coq.typecheck Bo Ty _, coq.env.add-const Name1 Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), @@ -61,6 +63,7 @@ env.add-const-noimplicits-failondup Name Bo Ty Opaque C :- std.do! [ (coq.error "HB: cannot infer some information in" Name ":" {coq.term->string Ty} ":=" {coq.term->string Bo}) true, + coq.typecheck Bo Ty _, coq.env.add-const Name Bo Ty Opaque C, env.add-location (const C), if (var Ty) (Ty? = none) (Ty? = some Ty), @@ -266,8 +269,8 @@ pred log.private.log-tactic i:term. with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.log.raw" _, NICE = ff), !, get-option "elpi.loc" Loc, - loc.fields Loc FILE _ _ _ _, - std.any->string Loc LocStr, + loc.fields Loc FILE Start Stop _ _, + LocStr is "characters " ^ {std.any->string Start} ^ "-" ^ {std.any->string Stop}, FILENAME is FILE ^ ".hb", open_append FILENAME OC1, std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1, @@ -295,7 +298,7 @@ log.private.log-vernac _. log.private.log-tactic P :- log.private.logger L Nice, !, if (Nice = tt) (PPALL = []) (PPALL = [@ppall!]), - log.private.logger-extend L {PPALL => coq.term->pp P}. + log.private.logger-extend L {PPALL => @holes! => coq.term->pp P}. log.private.log-tactic _. % The main entry point to print vernacular commands is coq.vernac->pp @@ -361,7 +364,7 @@ coq.vernac->pp1 (abbreviation Name NParams Term) (box (hv 2) [box h [str "Notati coq.vernac->ppabbrterm NParams Term StrParams B. coq.vernac->pp1 (canonical Name Local) (box h [Locality, str "Canonical ", str Name, str "."]) :- local->locality Local Locality. -coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :- +coq.vernac->pp1 (coercion Name SRC TGT) (box h [str "#[reversible] Coercion ", str Name, str " : ", str S, str " >-> ", str T, str "."]) :- coq.gref->path SRC SP, std.string.concat "." {std.take-last 2 SP} S', S is S' ^ "." ^ {coq.gref->id SRC}, if2 (TGT = sortclass) (T = "Sortclass") (TGT = funclass) (T = "Funclass") @@ -446,8 +449,8 @@ coq.vernac->ppinductiveconstructor [constructor ID Arity|Ks] PP :- pred coq.vernac->ppinductiveparams i:list (pair implicit_kind term), o:list coq.pp. coq.vernac->ppinductiveparams [] []. coq.vernac->ppinductiveparams [pr Imp T|Rest] PP :- - PP = [box (hov 2) [str A,str ID,str " : ", TY,str B]|PPRest], - decl T Name Ty, coq.name->id Name ID, coq.term->pp Ty TY, + PP = [box (hov 2) [str A,ID,str " : ", TY,str B]|PPRest], + coq.term->pp T ID, decl T _ Ty, coq.term->pp Ty TY, if2 (Imp = explicit) (A = "(", B = ")") (Imp = maximal) (A = "{", B = "}") (A = "[", B = "]"), diff --git a/HB/common/phant-abbreviation.elpi b/HB/common/phant-abbreviation.elpi index b7f68148c..943c30c74 100644 --- a/HB/common/phant-abbreviation.elpi +++ b/HB/common/phant-abbreviation.elpi @@ -92,7 +92,10 @@ fun-infer-type funclass N Ty (t\private.phant-term AL (Bo t)) Out :- coq.name-suffix N "ph" PhN, fun-implicit N Ty (t\private.phant-term [private.infer-type N funclass|AL] (fun PhN {{ lib:@hb.phantom (_ -> _) lp:t }} _\ Bo t)) Out. -fun-infer-type C _ _ _ _ :- coq.error "HB: inference of parameters of call" C "not implemented yet". +fun-infer-type (grefclass Class) N Ty (t\private.phant-term AL (Bo t)) Out :- + coq.name-suffix N "ph" PhN, private.build-type-pattern Class Pat, + fun-implicit N Ty (t\private.phant-term [private.infer-type N (grefclass Class)|AL] + (fun PhN {{ lib:@hb.phantom lp:Pat lp:t }} _\ Bo t)) Out. % TODO: this looks like a hack to remove pred append-fun-unify i:phant-term, o:phant-term. @@ -180,12 +183,25 @@ build-abbreviation K F [infer-type N sortclass|AL] K'' (fun N _ AbbrevFx) :- !, build-abbreviation K F [infer-type N funclass|AL] K'' (fun N _ AbbrevFx) :- !, pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom (_ -> _) lp:x }}]} AL K' (AbbrevFx x), K'' is K' + 1. -build-abbreviation _ _ [infer-type _ (grefclass _)|_] _ _ :- coq.error "TODO". +build-abbreviation K F [infer-type N (grefclass Class)|AL] K'' (fun N _ AbbrevFx) :- !, + build-type-pattern Class Pat, + pi x\ build-abbreviation K {mk-app F [{{ lib:hb.Phantom lp:Pat lp:x }}]} AL K' (AbbrevFx x), + K'' is K' + 1. build-abbreviation K F [implicit|AL] K' FAbbrev :- !, build-abbreviation K {mk-app F [_]} AL K' FAbbrev. build-abbreviation K F [unify|AL] K' FAbbrev :- !, build-abbreviation K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev. +% [build-type-pattern GR Pat] cheks that GR : forall x_1 ... x_n, Type +% and returns Pat = GR _ ... _ (that is GR applied to n holes). +% Note that n can be 0 when GR : Type. +pred build-type-pattern i:gref, o:term. +build-type-pattern GR Pat :- build-type-pattern.aux GR {coq.env.typeof GR} Pat. +build-type-pattern.aux GR T {{ lp:Pat _ }} :- coq.unify-eq T (prod N S T') ok, !, + @pi-decl N S x\ build-type-pattern.aux GR (T' x) Pat. +build-type-pattern.aux GR T (global GR) :- coq.unify-eq T {{ Type }} ok, !. +build-type-pattern.aux _ _ _ :- coq.error "HB: wrong carrier type". + % [mk-phant-term F PF] states that % if F = fun p1 .. p_k T m_0 .. m_n => _ diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 9062241f9..cd1ffaa4d 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -48,6 +48,25 @@ under.do! Then LP :- Then (_\ std.do! LP) _. pred map-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1. map-triple F G H (triple X Y Z) (triple X1 Y1 Z1) :- F X X1, G Y Y1, H Z Z1. +pred sort.split i:list A, o:list A, o:list A. +sort.split [] [] [] :- !. +sort.split [X] [X] [] :- !. +sort.split [X,Y|TL] [X|L1] [Y|L2] :- sort.split TL L1 L2. + +pred sort.merge i:(A -> A -> prop), i:list A, i:list A, o:list A. +sort.merge _ [] L L :- !. +sort.merge _ L [] L :- !. +sort.merge Rel [X1|L1] [X2|L2] [X1|M] :- Rel X1 X2, !, + sort.merge Rel L1 [X2|L2] M. +sort.merge Rel [X1|L1] [X2|L2] [X2|M] :- + sort.merge Rel [X1|L1] L2 M. + +pred sort i:list A, i:(A -> A -> prop), o:list A. +sort [] _ [] :- !. +sort [X] _ [X] :- !. +sort L Rel M :- + sort.split L L1 L2, sort L1 Rel S1, sort L2 Rel S2, sort.merge Rel S1 S2 M. + pred bubblesort i:list A, i:(A -> A -> prop), o:list A. bubblesort [] _ [] :- !. bubblesort [X] _ [X] :- !. @@ -101,8 +120,7 @@ constraint print-ctx mixin-src { % approximation, it should be logical path, not the file name pred coq.env.current-library o:string. -coq.env.current-library L :- coq.version _ _ N _, N >= 13, !, - loc.fields {get-option "elpi.loc"} L _ _ _ _. +coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _. coq.env.current-library "dummy.v". pred coq.prod-tgt->gref i:term, o:gref. diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 1b98811cc..f194be009 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -154,8 +154,7 @@ infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :- @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass. infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass. infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass. -infer-coercion-tgt (w-params.nil _ _ _) _ :- - coq.error "HB: coercion not to Sortclass or Funclass not supported yet.". +infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR. pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop. w-args.check-key _PS _T [] true :- !. diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index f7c1e76fa..000826a2a 100644 --- a/HB/common/utils.elpi +++ b/HB/common/utils.elpi @@ -120,13 +120,6 @@ nice-gref->string X Mod :- nice-gref->string X S :- coq.term->string (global X) S. -pred compat.concat i:string, i:list string, o:string. -compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O. -compat.concat S L O :- compat.concat.aux L S O. -compat.concat.aux [] _ "". -compat.concat.aux [X] _ X :- !. -compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1. - pred gref->modname i:gref, i:int, i:string, o:string. gref->modname GR NComp Sep ModName :- coq.gref->path GR Path, @@ -134,7 +127,7 @@ gref->modname GR NComp Sep ModName :- std.length Path Len, if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), std.take NComp Mods L, - compat.concat Sep {std.rev L} ModName. + std.string.concat Sep {std.rev L} ModName. pred gref->modname-label i:gref, i:int, i:string, o:string. gref->modname-label GR NComp Sep ModName :- coq.gref->path GR Path, @@ -142,7 +135,28 @@ gref->modname-label GR NComp Sep ModName :- std.length PathRev Len, if (Len >= NComp) (N = NComp) (N = Len), std.take N PathRev L, - compat.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. + std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName. + +pred string->modpath i:string, o:modpath. +string->modpath S MP :- + std.filter {coq.locate-all S} (l\l = loc-modpath _) L, + L = [loc-modpath MP]. + +pred gref->modname_short1 i:modpath, i:string, i:list string, o:string. +gref->modname_short1 _ S [] S. +gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'. +gref->modname_short1 MP S _ S :- string->modpath S MP. +gref->modname_short1 MP S [X|L] S' :- + gref->modname_short1 MP {std.string.concat "." [X,S]} L S'. + +% Print shortest qualified identifier of the module containing a gref +% Sep is used as separator +pred gref->modname_short i:gref, i:string, o:string. +gref->modname_short GR Sep IDS :- + coq.gref->path GR Path, + string->modpath {std.string.concat "." Path} MP, + gref->modname_short1 MP "" {std.rev Path} ID, + rex.replace "[.]" Sep ID IDS. pred avoid-name-collision i:string, o:string. avoid-name-collision S S1 :- diff --git a/HB/graph.elpi b/HB/graph.elpi index 27c7495c3..b251c2f39 100644 --- a/HB/graph.elpi +++ b/HB/graph.elpi @@ -18,27 +18,11 @@ to-file File :- !, std.do! [ namespace private { -pred compat.concat i:string, i:list string, o:string. -compat.concat S L O :- coq.version _ _ N _, N > 12, !, std.string.concat S L O. -compat.concat S L O :- compat.concat.aux L S O. -compat.concat.aux [] _ "". -compat.concat.aux [X] _ X :- !. -compat.concat.aux [X|XS] Sep O :- compat.concat.aux XS Sep O1, O is X ^ Sep ^ O1. - -pred gref->modname i:gref, i:int, i:string, o:string. -gref->modname GR NComp Sep ModName :- - coq.gref->path GR Path, - std.rev Path Mods, - std.length Path Len, - if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}), - std.take NComp Mods L, - compat.concat Sep {std.rev L} ModName. - pred pp-coercion-dot i:out_stream, i:coercion. pp-coercion-dot OC (coercion _ _ Src (grefclass Tgt)) :- class-def (class Src _ _), class-def (class Tgt _ _), !, std.do! [ - output OC {gref->modname Tgt 2 "_"}, + output OC {gref->modname_short Tgt "_"}, output OC " -> ", - output OC {gref->modname Src 2 "_"}, + output OC {gref->modname_short Src "_"}, output OC ";\n", ]. pp-coercion-dot _ _. diff --git a/HB/howto.elpi b/HB/howto.elpi new file mode 100644 index 000000000..0d84be4b9 --- /dev/null +++ b/HB/howto.elpi @@ -0,0 +1,158 @@ +/* Hierarchy Builder: algebraic hierarchies made easy + This software is released under the terms of the MIT license */ + +namespace howto { + +pred main-trm i:term, i:string, i:option int. +main-trm T STgt Depth :- coq.term->gref T GR, main-gref GR STgt Depth. + +pred main-str i:string, i:string, i:option int. +main-str S STgt Depth :- coq.locate S GR, main-gref GR STgt Depth. + +pred main-gref i:gref, i:string, i:option int. +main-gref GR STgt Depth :- class-def (class _ GR _), !, + private.mixins-in-structures [GR] MLSrc, + main-from MLSrc STgt Depth. +main-gref GR STgt Depth :- + private.structures-on-gref GR SL, + private.mixins-in-structures SL MLSrc, + main-from MLSrc STgt Depth. + +pred main-from i:list mixinname, i:string, i:option int. +main-from MLSrc STgt Depth :- + private.mixins-in-structures [{coq.locate STgt}] MLTgt, + private.list-diff MLTgt MLSrc ML, + if (ML = []) (coq.say "HB: nothing to do.") (main-from.aux MLSrc ML Depth). +main-from.aux MLSrc ML (some Depth) :- main-increase-depth MLSrc ML Depth false. +main-from.aux MLSrc ML none :- main-increase-depth MLSrc ML 3 true. + +pred main-increase-depth i:list mixinname, i:list mixinname, i:int, i:prop. +main-increase-depth MLSrc ML Depth AutoIncrease :- + private.paths-from-for-step MLSrc ML Depth R, + if (not (R = [])) (private.pp-solutions R) + (if AutoIncrease + (Depth' is Depth + 1, + coq.say "HB: no solution found at depth" Depth "looking at depth" Depth', + main-increase-depth MLSrc ML Depth' true) + (coq.error "HB: no solution found, try to increase search depth.")). + + +/* ------------------------------------------------------------------------- */ +/* ----------------------------- private code ------------------------------ */ +/* ------------------------------------------------------------------------- */ + +namespace private { + +shorten coq.pp.{ v , hov , spc , str , box , glue }. + +% L1 \subseteq L2 +pred incl i:list A, i:list A. +incl L1 L2 :- std.forall L1 (std.mem L2). + +% R = L1 \ L2 +pred list-diff i:list A, i:list A, o:list A. +list-diff L1 L2 R :- std.filter L1 (about.not1 (std.mem L2)) R. + +% R = L1 U L2 +pred union i:list A, i:list A, o:list A. +union L1 L2 R :- + std.fold L2 L1 (x\l\l'\if (std.mem l x) (l' = l) (l' = [x|l])) R. + +pred insert-sorted i:(A -> A -> prop), i:A, i:list A, o:list A. +insert-sorted _ X [] [X] :- !. +insert-sorted Rel X [Y|T] [X,Y|T] :- Rel X Y, !. +insert-sorted Rel X [Y|T] [Y|T'] :- insert-sorted Rel X T T', !. + +pred lt-gref i:gref, i:gref. +lt-gref X Y :- + gref->modname_short X "." SX, gref->modname_short Y "." SY, !, SX s< SY. + +pred size-order i:(list A -> list A -> prop), i:list A, i:list A. +size-order Rel L1 L2 :- + std.length L1 S1, std.length L2 S2, !, (S1 i< S2; (S1 = S2, !, Rel L1 L2)). + +pred lexi-order i:list gref, i:list gref. +lexi-order [] []. +lexi-order [X1|_] [X2|_] :- lt-gref X1 X2. +lexi-order [X|T1] [X|T2] :- lexi-order T1 T2. + +% [structures-on-gref GR ML] list structures [GR] is equipped with +pred structures-on-gref i:gref, o:list structure. +structures-on-gref GR SL :- + std.filter {coq.CS.db-for _ (cs-gref GR)} (about.not1 about.unif-hint?) LV, + std.map LV structures-on-gref.aux SL. +structures-on-gref.aux (cs-instance _ _ GR) F :- + coq.prod-tgt->gref {coq.env.typeof GR} F, class-def (class _ F _). + +% [mixins-in-structures SL ML] list mixins in structures [SL] +pred mixins-in-structures i:list structure, o:list mixinname. +mixins-in-structures SL ML :- std.fold SL [] mixins-in-structures.aux ML. +mixins-in-structures.aux F L L' :- + class-def (class _ F MLWP), union L {list-w-params_list MLWP} L'. + +% a type to store a factory along with the mixins it depends on +% and the mixins it provides +kind factory_deps_prov type. +type fdp factoryname -> list mixinname -> list mixinname -> factory_deps_prov. + +% get all available factories in the above type +pred list_factories o:list factory_deps_prov. +list_factories FL :- + std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL. +list_factories.aux (factory-constructor F _) (fdp F DML PML) :- + list-w-params_list {gref-deps F} DML, + list-w-params_list {factory-provides F} PML. + +% [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences +% of at most [K] factories that could, starting from mixins [MLSrc], +% build exactly the mixins [ML] +pred paths-from-for-step i:list mixinname, i:list mixinname, i:int, + o:list (list factoryname). +paths-from-for-step MLSrc ML K R :- + std.filter {list_factories} (fd\sigma pml\fd = fdp _ _ pml, incl pml ML) FL, + paths-from-for-step-using MLSrc ML K [] [] FL _ R. + +% [paths-from-for-step-using MLSrc ML K Pre KnownPre FL KnownPre' R] +% same as [paths-from-for-step MLSrc ML K R] using only factories in [FL] +% [Pre] is a (sorted) prefix that is looked into the list of known (sorted) +% prefixes [KnownPre] to avoid generating identical solutions up to permutations +pred paths-from-for-step-using i:list mixinname, i:list mixinname, i:int, + i:list factoryname, i:list (list factoryname), i:list factory_deps_prov, + o:list (list factoryname), o:list (list factoryname). +paths-from-for-step-using _ _ K _ KnownPre _ KnownPre [] :- K i< 0. +paths-from-for-step-using _ _ _ Pre KnownPre _ KnownPre [] :- + std.mem KnownPre Pre, !. +paths-from-for-step-using _ [] _ Pre KnownPre _ [Pre|KnownPre] [[]] :- !. +paths-from-for-step-using MLSrc ML K Pre KnownPre FL [Pre|KnownPre'] R :- + K' is K - 1, + std.filter FL (p\sigma dml\p = fdp _ dml _, incl dml MLSrc) FLdep, + std.fold FLdep (pr KnownPre []) + (paths-from-for-step-using.aux MLSrc ML FL K' Pre) + (pr KnownPre' R). +paths-from-for-step-using.aux MLSrc ML FL' K' Pre (fdp F _ MLF) (pr KnPre L) + (pr KnPre' R) :- + std.append MLSrc MLF MLSrc', + list-diff ML MLF ML', + insert-sorted lt-gref F Pre Pre', + std.filter FL' (p\sigma pml\p = fdp _ _ pml, incl pml ML') FML', + paths-from-for-step-using MLSrc' ML' K' Pre' KnPre FML' KnPre' R', + std.map R' (l\r\r = [F|l]) R'', + std.append L R'' R. + +pred pp-solutions i:list (list factoryname). +pp-solutions LLF :- + std.sort LLF (size-order lexi-order) SLLF, + % format + PpSolutions = box (v 4) [ + str "HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F):", + {about.bulletize SLLF pp-solution}], + % print + coq.say {coq.pp->string PpSolutions}, + coq.say. + +pred pp-solution i:list factoryname o:coq.pp. +pp-solution L (box (hov 0) PLS) :- + std.map L about.pp-module PL, + std.intersperse (glue [str ";", spc]) PL PLS. + +}} \ No newline at end of file diff --git a/HB/instance.elpi b/HB/instance.elpi index 2d2bb073b..0b793248c 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -370,7 +370,7 @@ check-non-forgetful-inheritance T Factory :- std.do! [ "We strongly advise you encapsulate this instance inside a module," "in order to isolate it from the rest of the code, and to be able" "to import it on demand. See the above paper and the file" - "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non-forgetful-inheritance.v" + "https://github.com/math-comp/hierarchy-builder/blob/master/tests/non_forgetful_inheritance.v" "to witness devastating effects." ) true ]. diff --git a/HB/pack.elpi b/HB/pack.elpi index 3da251b1c..b957db382 100644 --- a/HB/pack.elpi +++ b/HB/pack.elpi @@ -14,7 +14,10 @@ main Ty Args Instance :- std.do! [ get-constructor Class KC, get-constructor Structure KS, - std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "HB.pack: not a type", + std.assert-ok! (d\ + (coq.elaborate-ty-skeleton TSkel _ T d, d = ok) ; + coq.elaborate-skeleton TSkel _ T d + ) "HB.pack: not a well typed key", private.elab-factories FactoriesSkel T Factories, diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index ec13e8b53..1bef12aaa 100644 --- a/Makefile.test-suite.coq.local +++ b/Makefile.test-suite.coq.local @@ -12,13 +12,15 @@ DIFF=\ $(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \ < $(1) 2>/dev/null \ | grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \ + | sed -E 's/characters? [0-9-]+://' \ > $(1).out.aux;\ - diff -u --strip-trailing-cr $(call output_for,$(1)) $(1).out.aux;\ + wdiff $(call output_for,$(1)) $(1).out.aux;\ fi post-all:: $(call DIFF, tests/compress_coe.v) $(call DIFF, tests/about.v) + $(call DIFF, tests/howto.v) $(call DIFF, tests/missing_join_error.v) $(call DIFF, tests/not_same_key.v) $(call DIFF, tests/hnf.v) \ No newline at end of file diff --git a/README.md b/README.md index 3c92c553b..7db7c8dd8 100644 --- a/README.md +++ b/README.md @@ -82,7 +82,8 @@ Proof. by rewrite example. Qed. This [paper](https://hal.inria.fr/hal-02478907) describes the language in details, and the corresponding talk [is available on youtube](https://www.youtube.com/watch?v=F6iRaTlQrlo). The [wiki](https://github.com/math-comp/hierarchy-builder/wiki) gathers some -tricks and FAQs. +tricks and FAQs. If you want to work on the implementation of HB, this +[recorded hacking session](https://www.youtube.com/watch?v=gmaJjCbzqO0) may be relevant to you. ### Installation & availability @@ -150,6 +151,7 @@ opam install coq-hierarchy-builder - `HB.locate` is similar to `Locate`, prints file name and line of any global constant synthesized by HB - `HB.graph` prints the structure hierarchy to a dot file + - `HB.howto` prints sequences of factories to equip a type with a given structure - HB debug commands: - `HB.status` dumps the contents of the hierarchy (debug purposes) diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite index b5ff7af61..88384982b 100644 --- a/_CoqProject.test-suite +++ b/_CoqProject.test-suite @@ -52,6 +52,8 @@ examples/Coq2020_material/CoqWS_abstract.v examples/Coq2020_material/CoqWS_expansion/withHB.v examples/Coq2020_material/CoqWS_expansion/withoutHB.v +examples/cat/cat.v + tests/type_of_exported_ops.v tests/duplicate_structure.v tests/instance_params_no_type.v @@ -63,12 +65,13 @@ tests/exports2.v tests/log_impargs_record.v tests/compress_coe.v tests/funclass.v +tests/grefclass.v tests/local_instance.v tests/lock.v tests/interleave_context.v tests/not_same_key.v #tests/factory_sort.v -tests/factory_sort_tac.v +tests/hb_pack.v tests/declare.v tests/short.v tests/primitive_records.v diff --git a/coq-hierarchy-builder-shim.opam b/coq-hierarchy-builder-shim.opam index 9a190e591..6f44b2a7f 100644 --- a/coq-hierarchy-builder-shim.opam +++ b/coq-hierarchy-builder-shim.opam @@ -11,7 +11,7 @@ dev-repo: "git+https://github.com/math-comp/hierarchy-builder" build: [ make "-C" "shim" "build" ] install: [ make "-C" "shim" "install" ] conflicts: [ "coq-hierarchy-builder" ] -depends: [ "coq" {>= "8.10"} ] +depends: [ "coq-elpi" { (>= "1.14" & < "1.17~") | = "dev" } ] synopsis: "Shim package for HB" description: """ This package provide the support constants one can use to compile files diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam index 70a22128b..694aac2af 100644 --- a/coq-hierarchy-builder.opam +++ b/coq-hierarchy-builder.opam @@ -12,7 +12,7 @@ build: [ [ make "build"] [ make "test-suite" ] {with-test} ] install: [ make "install" ] -depends: [ "coq-elpi" { (>= "1.15.1" & < "1.16~") | = "dev" } ] +depends: [ "coq-elpi" { (>= "1.15.1" & < "1.17~") | = "dev" } ] conflicts: [ "coq-hierarchy-builder-shim" ] synopsis: "High level commands to declare and evolve a hierarchy based on packed classes" description: """ diff --git a/examples/cat/cat.v b/examples/cat/cat.v index 1dd1f755d..b8601449e 100644 --- a/examples/cat/cat.v +++ b/examples/cat/cat.v @@ -6,6 +6,10 @@ Unset Strict Implicit. Unset Printing Implicit Defensive. Add Search Blacklist "__canonical__". +Declare Scope algebra_scope. +Delimit Scope algebra_scope with A. +Local Open Scope algebra_scope. + Declare Scope cat_scope. Delimit Scope cat_scope with cat. Local Open Scope cat_scope. @@ -18,18 +22,21 @@ Axiom Prop_irrelevance : forall (P : Prop) (x y : P), x = y. Definition U := Type. Identity Coercion U_to_type : U >-> Sortclass. -HB.mixin Record HasHom C := { hom : C -> C -> U }. +HB.mixin Record IsQuiver C := { hom : C -> C -> U }. Unset Universe Checking. -HB.structure Definition Hom : Set := { C of HasHom C }. +HB.structure Definition Quiver : Set := { C of IsQuiver C }. Set Universe Checking. -Notation homType := Hom.type. -Bind Scope cat_scope with Hom.type. +Notation quiver := Quiver.type. +Bind Scope cat_scope with Quiver.type. Bind Scope cat_scope with hom. Arguments hom {C} : rename. +Notation homs T := (hom (_ : T) (_ : T)). +Notation "C ~> D :> T" := (hom (C : T) (D : T)) + (at level 99, D, T at level 200, format "C ~> D :> T", only parsing) : cat_scope. Notation "a ~> b" := (hom a b) (at level 99, b at level 200, format "a ~> b") : cat_scope. -HB.mixin Record Hom_IsPreCat C of Hom C := { +HB.mixin Record Quiver_IsPreCat C of Quiver C := { idmap : forall (a : C), a ~> a; comp : forall (a b c : C), (a ~> b) -> (b ~> c) -> (a ~> c); }. @@ -40,8 +47,8 @@ HB.factory Record IsPreCat C := { comp : forall (a b c : C), hom a b -> hom b c -> hom a c; }. HB.builders Context C of IsPreCat C. - HB.instance Definition _ := HasHom.Build C hom. - HB.instance Definition _ := Hom_IsPreCat.Build C idmap comp. + HB.instance Definition _ := IsQuiver.Build C hom. + HB.instance Definition _ := Quiver_IsPreCat.Build C idmap comp. HB.end. Unset Universe Checking. @@ -53,6 +60,8 @@ Arguments idmap {C} {a} : rename. Arguments comp {C} {a b c} : rename. Notation "f \o g" := (comp g f) : cat_scope. +Notation "f \; g :> T" := (@comp T _ _ _ f g) + (at level 60, g, T at level 60, format "f \; g :> T", only parsing) : cat_scope. Notation "f \; g" := (comp f g) : cat_scope. Notation "\idmap_ a" := (@idmap _ a) (only parsing, at level 0) : cat_scope. @@ -95,30 +104,26 @@ Proof. by []. Qed. Lemma U1x (X : U) x : \idmap_X x = x. Proof. by []. Qed. -HB.mixin Record IsPreFunctor (C D : Hom.type) (F : C -> D) := { - Fhom_of : forall (a b : C), (a ~> b) -> (F a ~> F b) +HB.mixin Record IsPreFunctor (C D : Quiver.type) (F : C -> D) := { + Fhom : forall (a b : C), (a ~> b) -> (F a ~> F b) }. Unset Universe Checking. -HB.structure Definition PreFunctor (C D : Hom.type) : Set := +HB.structure Definition PreFunctor (C D : Quiver.type) : Set := { F of IsPreFunctor C D F }. Set Universe Checking. -HB.instance Definition _ := HasHom.Build Hom.type PreFunctor.type. -Arguments Fhom_of /. +HB.instance Definition _ := IsQuiver.Build Quiver.type PreFunctor.type. -Definition Fhom_phant (C D : Hom.type) (F : C ~> D) - of phantom (_ -> _) F := @Fhom_of C D F. -Notation "F ^$" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _) +Notation "F ^$" := (@Fhom _ _ F _ _) (at level 1, format "F ^$") : cat_scope. -Notation "F <$> f" := (@Fhom_phant _ _ _ (Phantom (_ -> _) F) _ _ f) +Notation "F <$> f" := (@Fhom _ _ F _ _ f) (at level 58, format "F <$> f", right associativity) : cat_scope. -Lemma prefunctorP (C D : homType) (F G : C ~> D) (eqFG : F =1 G) : +Lemma prefunctorP (C D : quiver) (F G : C ~> D) (eqFG : F =1 G) : let homF a b F := F a ~> F b in (forall a b f, eq_rect _ (homF a b) (F <$> f) _ (funext eqFG) = G <$> f) -> F = G. Proof. -rewrite !/Fhom_phant/=. move: F G => [F [[/= Fhom]]] [G [[/= Ghom]]] in eqFG *. case: _ / (funext eqFG) => /= in Ghom * => eqFGhom. congr PreFunctor.Pack; congr PreFunctor.Class; congr IsPreFunctor.Axioms_. @@ -135,8 +140,8 @@ Unset Universe Checking. HB.structure Definition Functor (C D : precat) : Set := { F of IsPreFunctor C D F & PreFunctor_IsFunctor C D F }. Set Universe Checking. -HB.instance Definition _ := HasHom.Build precat Functor.type. -HB.instance Definition _ := HasHom.Build cat Functor.type. +HB.instance Definition _ := IsQuiver.Build precat Functor.type. +HB.instance Definition _ := IsQuiver.Build cat Functor.type. Lemma functorP (C D : precat) (F G : C ~> D) (eqFG : F =1 G) : let homF a b F := F a ~> F b in @@ -158,11 +163,11 @@ HB.instance Definition _ (C : precat) := PreFunctor_IsFunctor.Build C C idfun (fun=> erefl) (fun _ _ _ _ _ => erefl). Section comp_prefunctor. -Context {C D E : homType} {F : C ~> D} {G : D ~> E}. +Context {C D E : quiver} {F : C ~> D} {G : D ~> E}. HB.instance Definition _ := IsPreFunctor.Build C E (G \o F)%FUN (fun a b f => G^$ (F^$ f)). -Lemma comp_Fun (a b : C) (f : a ~> b) : (G \o F)%FUN^$ f = G^$ (F^$ f). +Lemma comp_Fun (a b : C) (f : a ~> b) : (G \o F)%FUN <$> f = G <$> (F <$> f). Proof. by []. Qed. End comp_prefunctor. @@ -177,12 +182,10 @@ HB.instance Definition _ := PreFunctor_IsFunctor.Build C E (G \o F)%FUN comp_F1 comp_Fcomp. End comp_functor. -HB.instance Definition _ := Hom_IsPreCat.Build precat - (fun C => [the C ~> C of idfun]) - (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]). -HB.instance Definition _ := Hom_IsPreCat.Build cat - (fun C => [the C ~> C of idfun]) - (fun C D E (F : C ~> D) (G : D ~> E) => [the C ~> E of (G \o F)%FUN]). +HB.instance Definition _ := Quiver_IsPreCat.Build precat + (fun=> idfun) (fun C D E (F : C ~> D) (G : D ~> E) => (G \o F)%FUN). +HB.instance Definition _ := Quiver_IsPreCat.Build cat + (fun=> idfun) (fun C D E (F : C ~> D) (G : D ~> E) => (G \o F)%FUN). Lemma funext_frefl A B (f : A -> B) : funext (frefl f) = erefl. Proof. exact: Prop_irrelevance. Qed. @@ -200,60 +203,62 @@ by split=> [C D F|C D F|C D C' D' F G H]; Qed. HB.instance Definition _ := cat_cat. -HB.mixin Record Hom_IsPreConcrete T of Hom T := { +HB.mixin Record Quiver_IsPreConcrete T of Quiver T := { concrete : T -> U; concrete_fun : forall (a b : T), (a ~> b) -> (concrete a) -> (concrete b); + (* concrete_fun_inj : forall a b, injective (concrete_fun a b) *) }. Unset Universe Checking. -HB.structure Definition PreConcreteHom : Set := - { C of Hom_IsPreConcrete C & HasHom C }. +HB.structure Definition PreConcreteQuiver : Set := + { C of Quiver_IsPreConcrete C & IsQuiver C }. Set Universe Checking. -Coercion concrete : PreConcreteHom.sort >-> U. +Coercion concrete : PreConcreteQuiver.sort >-> U. -HB.mixin Record PreConcrete_IsConcrete T of PreConcreteHom T := { +HB.mixin Record PreConcrete_IsConcrete T of PreConcreteQuiver T := { concrete_fun_inj : forall (a b : T), injective (concrete_fun a b) }. Unset Universe Checking. -HB.structure Definition ConcreteHom : Set := - { C of PreConcreteHom C & PreConcrete_IsConcrete C }. +HB.structure Definition ConcreteQuiver : Set := + { C of PreConcreteQuiver C & PreConcrete_IsConcrete C }. Set Universe Checking. -HB.instance Definition _ (C : ConcreteHom.type) := +HB.instance Definition _ (C : ConcreteQuiver.type) := IsPreFunctor.Build _ _ (concrete : C -> U) concrete_fun. -HB.mixin Record PreCat_IsConcrete T of ConcreteHom T & PreCat T := { +HB.mixin Record PreCat_IsConcrete T of ConcreteQuiver T & PreCat T := { concrete1 : forall (a : T), concrete <$> \idmap_a = idfun; concrete_comp : forall (a b c : T) (f : a ~> b) (g : b ~> c), concrete <$> (f \; g) = ((concrete <$> g) \o (concrete <$> f))%FUN; }. Unset Universe Checking. HB.structure Definition ConcretePreCat : Set := - { C of PreCat C & ConcreteHom C & PreCat_IsConcrete C }. + { C of PreCat C & ConcreteQuiver C & PreCat_IsConcrete C }. HB.structure Definition ConcreteCat : Set := - { C of Cat C & ConcreteHom C & PreCat_IsConcrete C }. + { C of Cat C & ConcreteQuiver C & PreCat_IsConcrete C }. Set Universe Checking. +(* Anomaly *) HB.instance Definition _ (C : ConcretePreCat.type) := - PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _). + PreFunctor_IsFunctor.Build C U concrete (@concrete1 _) (@concrete_comp _). HB.instance Definition _ (C : ConcreteCat.type) := - PreFunctor_IsFunctor.Build _ _ (concrete : C -> U) (@concrete1 _) (@concrete_comp _). + PreFunctor_IsFunctor.Build C U concrete (@concrete1 _) (@concrete_comp _). -HB.instance Definition _ := Hom_IsPreConcrete.Build U (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build U (fun _ _ => id). HB.instance Definition _ := PreConcrete_IsConcrete.Build U (fun _ _ _ _ => id). HB.instance Definition _ := PreCat_IsConcrete.Build U (fun=> erefl) (fun _ _ _ _ _ => erefl). Unset Universe Checking. -HB.instance Definition _ := Hom_IsPreConcrete.Build homType (fun _ _ => id). -HB.instance Definition _ := Hom_IsPreConcrete.Build precat (fun _ _ => id). -HB.instance Definition _ := Hom_IsPreConcrete.Build cat (fun _ _ => id). -Lemma homType_concrete_subproof : PreConcrete_IsConcrete homType. +HB.instance Definition _ := Quiver_IsPreConcrete.Build quiver (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build precat (fun _ _ => id). +HB.instance Definition _ := Quiver_IsPreConcrete.Build cat (fun _ _ => id). +Lemma quiver_concrete_subproof : PreConcrete_IsConcrete quiver. Proof. constructor=> C D F G FG; apply: prefunctorP. by move=> x; congr (_ x); apply: FG. by move=> *; apply: Prop_irrelevance. Qed. -HB.instance Definition _ := homType_concrete_subproof. +HB.instance Definition _ := quiver_concrete_subproof. Lemma precat_concrete_subproof : PreConcrete_IsConcrete precat. Proof. @@ -276,7 +281,7 @@ HB.instance Definition _ := PreCat_IsConcrete.Build cat (fun=> erefl) (fun _ _ _ _ _ => erefl). Set Universe Checking. -Definition cst (C D : homType) (c : C) := fun of D => c. +Definition cst (C D : quiver) (c : C) := fun of D => c. Arguments cst {C} D c. HB.instance Definition _ {C D : precat} (c : C) := IsPreFunctor.Build D C (cst D c) (fun _ _ _ => idmap). @@ -285,14 +290,13 @@ HB.instance Definition _ {C D : cat} (c : C) := (fun _ _ _ _ _ => esym (compo1 idmap)). Definition catop (C : Type) : Type := C. -HB.instance Definition _ (C : homType) := HasHom.Build (catop C) (fun a b => hom b a). -HB.instance Definition _ (C : precat) := Hom_IsPreCat.Build (catop C) (fun=> idmap) +Notation "C ^op" := (catop C) (at level 10, format "C ^op") : cat_scope. +HB.instance Definition _ (C : quiver) := IsQuiver.Build (C^op) (fun a b => hom b a). +HB.instance Definition _ (C : precat) := Quiver_IsPreCat.Build (C^op) (fun=> idmap) (fun _ _ _ f g => g \; f). -HB.instance Definition _ (C : cat) := PreCat_IsCat.Build (catop C) +HB.instance Definition _ (C : cat) := PreCat_IsCat.Build (C^op) (fun _ _ _ => compo1 _) (fun _ _ _ => comp1o _) (fun _ _ _ _ _ _ _ => esym (compoA _ _ _)). -Notation "C ^op" := (catop C) (at level 10, format "C ^op") : cat_scope. - HB.instance Definition _ {C : precat} {c : C} := IsPreFunctor.Build C _ (hom c) (fun a b f g => g \; f). @@ -301,24 +305,19 @@ Lemma hom_Fhom_subproof (C : cat) (x : C) : Proof. by split=> *; apply/funext => h; [apply: compo1 | apply: compoA]. Qed. HB.instance Definition _ {C : cat} {c : C} := hom_Fhom_subproof c. -Lemma hom_op {C : homType} (c : C^op) : hom c = (@hom C)^~ c. +Lemma hom_op {C : quiver} (c : C^op) : hom c = (@hom C)^~ c. Proof. reflexivity. Qed. Lemma homFhomx {C : precat} (a b c : C) (f : a ~> b) (g : c ~> a) : (hom c <$> f) g = g \; f. Proof. by []. Qed. -Notation "C ~> D :> T" := ([the T of C] ~> [the T of D]) - (at level 99, D, T at level 200, format "C ~> D :> T"). -Notation "C :~>: D :> T" := ([the T of C : Type] ~> [the T of D : Type]) - (at level 99, D, T at level 200, format "C :~>: D :> T"). - Definition dprod {I : Type} (C : I -> Type) := forall i, C i. Section hom_dprod. -Context {I : Type} (C : I -> Hom.type). +Context {I : Type} (C : I -> Quiver.type). Definition dprod_hom_subdef (a b : dprod C) := forall i, a i ~> b i. -HB.instance Definition _ := HasHom.Build (dprod C) dprod_hom_subdef. +HB.instance Definition _ := IsQuiver.Build (dprod C) dprod_hom_subdef. End hom_dprod. Arguments dprod_hom_subdef /. @@ -345,14 +344,14 @@ HB.instance Definition _ := dprod_is_cat. End cat_dprod. Section hom_prod. -Context {C D : Hom.type}. +Context {C D : Quiver.type}. Definition prod_hom_subdef (a b : C * D) := ((a.1 ~> b.1) * (a.2 ~> b.2))%type. -HB.instance Definition _ := HasHom.Build (C * D)%type prod_hom_subdef. +HB.instance Definition _ := IsQuiver.Build (C * D)%type prod_hom_subdef. End hom_prod. Section precat_prod. Context {C D : precat}. -HB.instance Definition _ := IsPreCat.Build (C * D)%type (fun _ => (idmap, idmap)) +HB.instance Definition _ := IsPreCat.Build (C * D)%type (fun=> (idmap, idmap)) (fun a b c (f : a ~> b) (g : b ~> c) => (f.1 \; g.1, f.2 \; g.2)). End precat_prod. @@ -368,23 +367,22 @@ Qed. HB.instance Definition _ := prod_is_cat. End cat_prod. -HB.mixin Record IsNatural (C D : precat) (F G : C :~>: D :> homType) +HB.mixin Record IsNatural (C D : precat) (F G : C ~> D :> quiver) (n : forall c, F c ~> G c) := { natural : forall (a b : C) (f : a ~> b), F <$> f \; n b = n a \; G <$> f }. Unset Universe Checking. -HB.structure Definition Natural (C D : precat) - (F G : C :~>: D :> homType) : Set := +HB.structure Definition Natural (C D : precat) (F G : C ~> D :> quiver) : Set := { n of @IsNatural C D F G n }. Set Universe Checking. HB.instance Definition _ (C D : precat) := - HasHom.Build (PreFunctor.type C D) (@Natural.type C D). + IsQuiver.Build (C ~> D) (@Natural.type C D). HB.instance Definition _ (C D : precat) := - HasHom.Build (Functor.type C D) (@Natural.type C D). + IsQuiver.Build (C ~> D) (@Natural.type C D). Arguments natural {C D F G} n [a b] f : rename. Lemma naturalx (C : precat) (D : ConcretePreCat.type) - (F G : C :~>: D :> homType) (n : F ~> G) (a b : C) (f : a ~> b) g : + (F G : C ~> D :> quiver) (n : F ~> G) (a b : C) (f : a ~> b) g : (concrete <$> n b) ((concrete <$> F <$> f) g) = (concrete <$> G <$> f) ((concrete <$> n a) g). Proof. @@ -393,11 +391,11 @@ by rewrite !Fcomp. Qed. Arguments naturalx {C D F G} n [a b] f. -Lemma naturalU (C : precat) (F G : C :~>: U :> homType) (n : F ~> G) +Lemma naturalU (C : precat) (F G : C ~> U :> quiver) (n : F ~> G) (a b : C) (f : a ~> b) g : n b (F^$ f g) = G^$ f (n a g). Proof. exact: (naturalx n). Qed. -Lemma natP (C D : precat) (F G : C :~>: D :> homType) (n m : F ~> G) : +Lemma natP (C D : precat) (F G : C ~> D :> quiver) (n m : F ~> G) : Natural.sort n = Natural.sort m -> n = m. Proof. case: n m => [/= n nP] [/= m mP] enm. @@ -408,12 +406,116 @@ exact: Prop_irrelevance. Qed. Notation "F ~~> G" := - ((F : _ -> _) ~> (G : _ -> _) :> (_ :~>: _ :> homType)) + (F ~> G :> (homs quiver)) (at level 99, G at level 200, format "F ~~> G"). Notation "F ~~> G :> C ~> D" := - ((F : _ -> _) ~> (G : _ -> _) :> (C :~>: D :> homType)) + (F ~> G :> (C ~> D :> quiver)) (at level 99, G at level 200, C, D at level 0, format "F ~~> G :> C ~> D"). +Section nat_map_left. +Context {C D E : precat} {F G : C ~> D}. + +Definition nat_lmap (H : D ~> E :> quiver) (n : forall c, F c ~> G c) : + forall c, (H \o F)%FUN c ~> (H \o G)%FUN c := fun c => H <$> n c. +Lemma nat_lmap_is_natural (H : D ~> E) (n : F ~~> G) : + IsNatural C E (H \o F) (H \o G) (nat_lmap H n). +Proof. by constructor=> a b f; rewrite /nat_lmap/= -!Fcomp natural. Qed. +HB.instance Definition _ H n := nat_lmap_is_natural H n. +(* Definition nat_lmap_nat (H : D ~> E) (n : F ~~> G) : H \o F ~~> H \o G := nat_lmap H n. *) +End nat_map_left. + +Notation "F n" := (nat_lmap F n) + (at level 58, format "F n", right associativity) : cat_scope. + +Section nat_map_right. +Context {C D E : precat} {F G : C ~> D}. + +Definition nat_rmap (H : E -> C) (n : forall c, F c ~> G c) : + forall c, (F \o H)%FUN c ~> (G \o H)%FUN c := fun c => n (H c). +Lemma nat_rmap_is_natural (H : E ~> C :> quiver) (n : F ~~> G) : + IsNatural E D (F \o H)%FUN (G \o H)%FUN (nat_rmap H n). +Proof. by constructor=> a b f; rewrite /nat_lmap/= natural. Qed. +HB.instance Definition _ H n := nat_rmap_is_natural H n. + +End nat_map_right. + +Notation "F <$o> n" := (nat_rmap F n) + (at level 58, format "F <$o> n", right associativity) : cat_scope. + +HB.mixin Record IsMonad (C : precat) (M : C -> C) of @PreFunctor C C M := { + unit : idfun ~~> M; + join : (M \o M)%FUN ~~> M; + bind : forall (a b : C), (a ~> M b) -> (M a ~> M b); + bindE : forall a b (f : a ~> M b), bind a b f = M <$> f \; join b; + unit_join : forall a, (M <$> unit a) \; join _ = idmap; + join_unit : forall a, join _ \; (M <$> unit a) = idmap; + join_square : forall a, M <$> join a \; join _ = join _ \; join _ +}. + +HB.structure Definition PreMonad (C : precat) := + {M of @PreFunctor C C M & IsMonad C M}. +HB.structure Definition Monad (C : precat) := + {M of @Functor C C M & IsMonad C M}. + +HB.factory Record IsJoinMonad (C : precat) (M : C -> C) of @PreFunctor C C M := { + unit : idfun ~~> M; + join : (M \o M)%FUN ~~> M; + unit_join : forall a, (M <$> unit a) \; join _ = idmap; + join_unit : forall a, join _ \; (M <$> unit a) = idmap; + join_square : forall a, M <$> join a \; join _ = join _ \; join _ +}. +HB.builders Context C M of IsJoinMonad C M. + HB.instance Definition _ := IsMonad.Build C M + (fun a b f => erefl) unit_join join_unit join_square. +HB.end. + +HB.mixin Record IsCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := { + counit : M ~~> idfun; + cojoin : M ~~> (M \o M)%FUN; + cobind : forall (a b : C), (M a ~> b) -> (M a ~> M b); + cobindE : forall a b (f : M a ~> b), cobind a b f = cojoin _ \; M <$> f; + unit_cojoin : forall a, (M <$> counit a) \; cojoin _ = idmap; + join_counit : forall a, cojoin _ \; (M <$> counit a) = idmap; + cojoin_square : forall a, cojoin _ \; M <$> cojoin a = cojoin _ \; cojoin _ +}. +HB.structure Definition PreCoMonad (C : precat) := + {M of @PreFunctor C C M & IsCoMonad C M}. +HB.structure Definition CoMonad (C : precat) := + {M of @Functor C C M & IsCoMonad C M}. + +HB.factory Record IsJoinCoMonad (C : precat) (M : C -> C) of @IsPreFunctor C C M := { + counit : M ~~> idfun; + cojoin : M ~~> (M \o M)%FUN; + unit_cojoin : forall a, (M <$> counit a) \; cojoin _ = idmap; + join_counit : forall a, cojoin _ \; (M <$> counit a) = idmap; + cojoin_square : forall a, cojoin _ \; M <$> cojoin a = cojoin _ \; cojoin _ +}. +HB.builders Context C M of IsJoinCoMonad C M. + HB.instance Definition _ := IsCoMonad.Build C M + (fun a b f => erefl) unit_cojoin join_counit cojoin_square. +HB.end. + +HB.mixin Record IsRightAdjoint (D C : precat) (R : D -> C) + of @PreFunctor D C R := { + L_ : C ~> D; + phi : forall c d, (L_ c ~> d) -> (c ~> R d); + psy : forall c d, (c ~> R d) -> (L_ c ~> d); + phi_psy c d : (phi c d \o psy c d)%FUN = @id (c ~> R d); + psy_phi c d : (psy c d \o phi c d)%FUN = @id (L_ c ~> d) +}. +HB.structure Definition RightAdjoint (D C : precat) := + { R of @Functor D C R & IsRightAdjoint D C R }. +Arguments L_ {_ _}. +Arguments phi {D C s} {c d}. +Arguments psy {D C s} {c d}. + +Lemma idFmap (C : cat) (a b : C) (f : a ~> b) : idfun <$> f = f. +Proof. by []. Qed. + +Lemma compFmap (C D E : cat) (F : C ~> D) (G : D ~> E) (a b : C) (f : a ~> b) : + (G \o F) <$> f = G <$> F <$> f. +Proof. by []. Qed. + Section hom_repr. Context {C : cat} (F : C ~> U :> cat). @@ -421,20 +523,18 @@ Definition homF (c : C) : U := hom c ~~> F. Section nat. Context (x y : C) (xy : x ~> y) (n : hom x ~~> F). -Definition homFhom_subdef c : hom y c ~> F c := fun g => n _ (xy \; g). -Arguments homFhom_subdef / : clear implicits. +Definition homFhom c : hom y c ~> F c := fun g => n _ (xy \; g). -Lemma homFhom_natural_subdef : IsNatural _ _ _ _ homFhom_subdef. +Lemma homFhom_natural_subdef : IsNatural _ _ _ _ homFhom. Proof. -by split=> a b f /=; apply/funext => g /=; rewrite !Ucompx/= !naturalU/= Fcomp. +by split=> a b f /=; apply/funext => g /=; + rewrite /homFhom !Ucompx/= !naturalU/= Fcomp. Qed. HB.instance Definition _ := homFhom_natural_subdef. -Definition homFhom_subdef_nat : hom y ~~> F := [the _ ~~> _ of homFhom_subdef]. End nat. -Arguments homFhom_subdef / : clear implicits. - +Arguments homFhom / : clear implicits. -HB.instance Definition _ := IsPreFunctor.Build _ _ homF homFhom_subdef_nat. +HB.instance Definition _ := IsPreFunctor.Build _ _ homF homFhom. Lemma homF_functor_subproof : PreFunctor_IsFunctor _ _ homF. Proof. split=> [a|a b c f g]. @@ -452,22 +552,20 @@ Context (c : C). Definition hom_repr : homF c ~> F c := fun f => f _ idmap. Arguments hom_repr /. -Definition repr_hom (fc : F c) a : - [the C :~>: U :> homType of hom c] a ~> F a := fun f => F^$ f fc. +Definition repr_hom (fc : F c) a : hom c a ~> F a := fun f => F^$ f fc. Arguments repr_hom / : clear implicits. Lemma repr_hom_subdef (fc : F c) : IsNatural _ _ _ _ (repr_hom fc). Proof. by split=> a b f /=; apply/funext=> x; rewrite !Ucompx/= Fcomp. Qed. HB.instance Definition _ {fc : F c} := repr_hom_subdef fc. -Definition repr_hom_nat : F c ~> homF c := fun fc => - [the hom c ~~> F of repr_hom fc]. +Definition repr_hom_nat : F c ~> homF c := repr_hom. Lemma hom_reprK : cancel hom_repr repr_hom_nat. Proof. move=> f; apply/natP; apply/funext => a; apply/funext => g /=. by rewrite -naturalU/=; congr (f _ _); apply: comp1o. Qed. -Lemma repr_homK : cancel repr_hom_nat hom_repr. +Lemma repr_homK : cancel (repr_hom : F c ~> homF c) hom_repr. Proof. by move=> fc; rewrite /= F1. Qed. End pointed. Arguments hom_repr /. @@ -478,8 +576,8 @@ Proof. split=> a b f /=; apply/funext => n /=; rewrite !Ucompx/= compo1/=. by rewrite -naturalU/=; congr (n _ _); apply/esym/comp1o. Qed. - HB.instance Definition _ := hom_repr_natural_subproof. + Lemma hom_natural_repr_subproof : IsNatural _ _ _ _ repr_hom_nat. Proof. split=> a b f /=; apply: funext => fa /=; rewrite !Ucompx/=. @@ -488,8 +586,8 @@ by rewrite Fcomp Ucompx/=. Qed. HB.instance Definition _ := hom_natural_repr_subproof. -Definition hom_repr_nat := [the homF ~~> F of hom_repr]. -Definition repr_hom_nat_nat := [the F ~~> homF of repr_hom_nat]. +Definition hom_repr_nat : homF ~~> F := hom_repr. +Definition repr_hom_nat_nat : F ~~> homF := repr_hom_nat. End hom_repr. @@ -501,7 +599,7 @@ Definition type := { x : C * D & F x.1 ~> G x.2 }. Definition hom_subdef (a b : type) := { f : tag a ~> tag b & F^$ f.1 \; tagged b = tagged a \; G^$ f.2 }. -HB.instance Definition _ := HasHom.Build type hom_subdef. +HB.instance Definition _ := IsQuiver.Build type hom_subdef. End homcomma. Arguments hom_subdef /. Section comma. @@ -540,19 +638,19 @@ Notation "F `/ b" := (F `/` cst unit b) Notation "a / b" := (cst unit a `/ b) : cat_scope. HB.mixin Record PreCat_IsMonoidal C of PreCat C := { - one : C; + onec : C; prod : (C * C)%type ~> C :> precat ; }. HB.structure Definition PreMonoidal := { C of PreCat C & PreCat_IsMonoidal C }. Notation premonoidal := PreMonoidal.type. Arguments prod {C} : rename. Notation "a * b" := (prod (a, b)) : cat_scope. -Reserved Notation "f ** g" (at level 40, g at level 40, format "f ** g"). -Notation "f ** g" := (prod^$ (f, g)) (only printing) : cat_scope. -Notation "f ** g" := (prod^$ ((f, g) : (_, _) ~> (_, _))) (only parsing) : cat_scope. -Notation "1" := one. +Reserved Notation "f <*> g" (at level 40, g at level 40, format "f <*> g"). +Notation "f <*> g" := (prod^$ (f, g)) (only printing) : cat_scope. +Notation "f <*> g" := (prod^$ ((f, g) : (_, _) ~> (_, _))) (only parsing) : cat_scope. +Notation "1" := onec : cat_scope. -Definition hom_cast {C : homType} {a a' : C} (eqa : a = a') {b b' : C} (eqb : b = b') : +Definition hom_cast {C : quiver} {a a' : C} (eqa : a = a') {b b' : C} (eqb : b = b') : (a ~> b) -> (a' ~> b'). Proof. now elim: _ / eqa; elim: _ / eqb. Defined. @@ -560,57 +658,55 @@ Proof. now elim: _ / eqa; elim: _ / eqb. Defined. HB.mixin Record PreFunctor_IsMonoidal (C D : premonoidal) F of @PreFunctor C D F := { fun_one : F 1 = 1; fun_prod : forall (x y : C), F (x * y) = F x * F y; - (* fun_prodF : forall (x x' : C) (f : x ~> x') (y y' : C) (g : y ~> y'), *) - (* hom_cast (fun_prod _ _) (fun_prod _ _) (F^$ (f ** g)) = F^$ f ** F^$ g *) }. HB.structure Definition MonoidalPreFunctor C D := { F of @PreFunctor_IsMonoidal C D F }. Arguments fun_prod {C D F x y} : rename. (* Arguments fun_prodF {C D F x x'} f {y y'} g : rename. *) Unset Universe Checking. -HB.instance Definition _ := HasHom.Build premonoidal MonoidalPreFunctor.type. +HB.instance Definition _ := IsQuiver.Build premonoidal MonoidalPreFunctor.type. Set Universe Checking. (* Definition comma_is_premonoidal (C D E : premonoidal) *) (* (F : C ~> E) (G : D ~> E) := F. *) -HB.instance Definition _ (C : Hom.type) := - IsPreFunctor.Build [the homType of (C * C)%type] C fst +HB.instance Definition _ (C : Quiver.type) := + IsPreFunctor.Build (C * C)%type C fst (fun (a b : C * C) (f : a ~> b) => f.1). -HB.instance Definition _ (C : Hom.type) := - IsPreFunctor.Build [the homType of (C * C)%type] C snd +HB.instance Definition _ (C : Quiver.type) := + IsPreFunctor.Build (C * C)%type C snd (fun (a b : C * C) (f : a ~> b) => f.2). Definition prod3l {C : PreMonoidal.type} (x : C * C * C) : C := (x.1.1 * x.1.2) * x.2. HB.instance Definition _ {C : PreMonoidal.type} := IsPreFunctor.Build _ C prod3l - (fun a b (f : a ~> b) => (f.1.1 ** f.1.2) ** f.2). + (fun a b (f : a ~> b) => (f.1.1 <*> f.1.2) <*> f.2). Definition prod3r {C : PreMonoidal.type} (x : C * C * C) : C := x.1.1 * (x.1.2 * x.2). HB.instance Definition _ {C : PreMonoidal.type} := IsPreFunctor.Build _ C prod3r - (fun a b (f : a ~> b) => f.1.1 ** (f.1.2 ** f.2)). + (fun a b (f : a ~> b) => f.1.1 <*> (f.1.2 <*> f.2)). Definition prod1r {C : PreMonoidal.type} (x : C) : C := 1 * x. HB.instance Definition _ {C : PreMonoidal.type} := - IsPreFunctor.Build [the homType of C : Type] C prod1r - (fun (a b : C) (f : a ~> b) => \idmap_1 ** f). + IsPreFunctor.Build C C prod1r + (fun (a b : C) (f : a ~> b) => \idmap_1 <*> f). Definition prod1l {C : PreMonoidal.type} (x : C) : C := x * 1. HB.instance Definition _ {C : PreMonoidal.type} := - IsPreFunctor.Build [the homType of C : Type] C prod1l - (fun (a b : C) (f : a ~> b) => f ** \idmap_1). + IsPreFunctor.Build C C prod1l + (fun (a b : C) (f : a ~> b) => f <*> \idmap_1). HB.mixin Record PreMonoidal_IsMonoidal C of PreMonoidal C := { - prodA : prod3l ~~> prod3r :> _ ~> C; - prod1c : prod1r ~~> idfun :> C ~> C; - prodc1 : prod1l ~~> idfun :> C ~> C; + prodA : prod3l ~~> prod3r; + prod1c : prod1r ~~> idfun; + prodc1 : prod1l ~~> idfun; prodc1c : forall (x y : C), - prodA (x, 1, y) \; \idmap_x ** prod1c y = prodc1 x ** \idmap_y; + prodA (x, 1, y) \; \idmap_x <*> prod1c y = prodc1 x <*> \idmap_y; prodA4 : forall (w x y z : C), prodA (w * x, y, z) \; prodA (w, x, y * z) = - prodA (w, x, y) ** \idmap_z \; prodA (w, x * y, z) \; \idmap_w ** prodA (x, y, z); + prodA (w, x, y) <*> \idmap_z \; prodA (w, x * y, z) \; \idmap_w <*> prodA (x, y, z); }. Unset Universe Checking. @@ -618,4 +714,192 @@ HB.structure Definition Monoidal : Set := { C of PreMonoidal_IsMonoidal C & PreMonoidal C }. Set Universe Checking. +HB.mixin Record IsRing A := { + zero : A; + one : A; + add : A -> A -> A; + opp : A -> A; + mul : A -> A -> A; + addrA : associative add; + addrC : commutative add; + add0r : left_id zero add; + addNr : left_inverse zero opp add; + mulrA : associative mul; + mul1r : left_id one mul; + mulr1 : right_id one mul; + mulrDl : left_distributive mul add; + mulrDr : right_distributive mul add; +}. + +#[short(type="ringType")] +HB.structure Definition Ring := { A of IsRing A }. + +Bind Scope algebra_scope with Ring.sort. +Notation "0" := zero : algebra_scope. +Notation "1" := one : algebra_scope. +Infix "+" := (@add _) : algebra_scope. +Notation "- x" := (@opp _ x) : algebra_scope. +Infix "*" := (@mul _) : algebra_scope. +Notation "x - y" := (x + - y) : algebra_scope. + +Lemma addr0 (R : ringType) : right_id (@zero R) add. +Proof. by move=> x; rewrite addrC add0r. Qed. + +Lemma addrN (R : ringType) : right_inverse (@zero R) opp add. +Proof. by move=> x; rewrite addrC addNr. Qed. + +Lemma addKr (R : ringType) (x : R) : cancel (add x) (add (- x)). +Proof. by move=> y; rewrite addrA addNr add0r. Qed. + +Lemma addrI (R : ringType) (x : R) : injective (add x). +Proof. exact: can_inj (addKr _). Qed. + +Lemma opprK (R : ringType) : involutive (@opp R). +Proof. by move=> x; apply: (@addrI _ (- x)); rewrite addNr addrN. Qed. + +HB.mixin Record IsRingQuiver (A B : Ring.type) (f : A -> B) := { + hom1_subproof : f 1%A = 1%A; + homB_subproof : {morph f : x y / x - y}; + homM_subproof : {morph f : x y / (x * y)%A}; +}. + +HB.structure Definition RingQuiver A B := { f of IsRingQuiver A B f }. + +Lemma id_IsRingQuiver A : IsRingQuiver A A idfun. Proof. by []. Defined. +HB.instance Definition _ A := id_IsRingQuiver A. + +Lemma comp_IsRingQuiver (A B C : Ring.type) (f : RingQuiver.type A B) (g : RingQuiver.type B C) : + IsRingQuiver A C (f \; g :> U). +Proof. +by constructor => [|x y|x y]; +rewrite /comp/= ?hom1_subproof ?homB_subproof ?homM_subproof. +Qed. +HB.instance Definition _ A B C f g := @comp_IsRingQuiver A B C f g. + +HB.instance Definition _ := IsQuiver.Build Ring.type RingQuiver.type. +HB.instance Definition _ := + Quiver_IsPreCat.Build Ring.type (fun _ => idfun) (fun _ _ _ f g => f \; g :> U). +HB.instance Definition _ := Quiver_IsPreConcrete.Build Ring.type (fun _ _ => id). +Lemma ring_precat : PreConcrete_IsConcrete Ring.type. +Proof. +constructor => A B [f cf] [g cg]//=; rewrite -[_ = _]/(f = g) => fg. +case: _ / fg in cg *; congr {|RingQuiver.sort := _ ; RingQuiver.class := _|}. +case: cf cg => [[? ? ?]] [[? ? ?]]. +by congr RingQuiver.Class; congr IsRingQuiver.phant_Build => //=; apply: Prop_irrelevance. +Qed. +HB.instance Definition _ := ring_precat. + +Lemma ring_IsCat : PreCat_IsCat Ring.type. +Proof. +by constructor=> [A B f|A B f|A B C D f g h]; exact: concrete_fun_inj. +Qed. +HB.instance Definition _ := ring_IsCat. + +Lemma hom1 (R S : Ring.type) (f : R ~> S) : f 1%A = 1%A. +Proof. exact: hom1_subproof. Qed. +Lemma homB (R S : Ring.type) (f : R ~> S) : {morph f : x y / x - y}. +Proof. exact: homB_subproof. Qed. +Lemma homM (R S : Ring.type) (f : R ~> S) : {morph f : x y / (x * y)%A}. +Proof. exact: homM_subproof. Qed. +Lemma hom0 (R S : Ring.type) (f : R ~> S) : f 0%A = 0%A. +Proof. by rewrite -(addrN 1%A) homB addrN. Qed. +Lemma homN (R S : Ring.type) (f : R ~> S) : {morph f : x / - x}. +Proof. by move=> x; rewrite -[- x]add0r homB hom0 add0r. Qed. +Lemma homD (R S : Ring.type) (f : R ~> S) : {morph f : x y / x + y}. +Proof. by move=> x y; rewrite -[y]opprK !homB !homN. Qed. + +HB.mixin Record IsIdeal (R : ringType) (I : R -> Prop) := { + ideal0 : I 0; + idealD : forall x y, I x -> I y -> I (x + y); + idealM : forall x y, I y -> I (x * y)%A; +}. +HB.structure Definition Ideal (R : ringType) := { I of IsIdeal R I }. + +HB.mixin Record Ideal_IsPrime (R : ringType) (I : R -> Prop) of IsIdeal R I := { + ideal_prime : forall x y : R, I (x * y)%A -> I x \/ I y +}. +#[short(type="spec")] +HB.structure Definition PrimeIdeal (R : ringType) := + { I of Ideal_IsPrime R I & Ideal R I }. + +From HB Require Import classical. +Local Open Scope classical_set_scope. + +HB.mixin Record Topological T := { + open : (T -> Prop) -> Prop; + closed : (T -> Prop) -> Prop; + open_setT : open setT; + open_bigcup : forall {I} (D : set I) (F : I -> set T), + (forall i, D i -> open (F i)) -> open (\bigcup_(i in D) F i); + open_setI : forall X Y : set T, open X -> open Y -> open (setI X Y); + open_compl : forall X, open (~` X) = closed X +}. +HB.structure Definition TopologicalSpace := { A of Topological A }. + +#[export] Hint Extern 0 (open setT) => now apply: open_setT : core. + +HB.factory Record TopologicalBase T := { + open_base : set (set T); + open_base_covers : setT `<=` \bigcup_(X in open_base) X; + open_base_cup : forall X Y : set T, open_base X -> open_base Y -> + forall z, (X `&` Y) z -> exists2 Z, open_base Z & Z z /\ Z `<=` X `&` Y +}. + +HB.builders Context T (a : TopologicalBase T). + + Definition open_of := + [set A | exists2 D, D `<=` open_base & A = \bigcup_(X in D) X]. + + Definition closed_of := [set A | open_of (~` A)]. + + Lemma open_of_setT : open_of setT. + Proof. + exists open_base; rewrite // predeqE => x; split=> // _. + by apply: open_base_covers. + Qed. + + Lemma open_of_bigcup {I} (D : set I) (F : I -> set T) : + (forall i, D i -> open_of (F i)) -> open_of (\bigcup_(i in D) F i). + Proof. Admitted. + + Lemma open_of_cap X Y : open_of X -> open_of Y -> open_of (X `&` Y). + Proof. Admitted. + + HB.instance Definition to_Topological := + @Topological.Build T open_of closed_of open_of_setT + (@open_of_bigcup) open_of_cap (fun=> erefl). + +HB.end. + +HB.factory Record TopologicalClosedBase T := { + closed_base : set (set T); + closed_base_cap : setT `<=` \bigcup_(X in closed_base) X; + closed_base_cup : forall X Y : set T, closed_base X -> closed_base Y -> + forall z, (X `&` Y) z -> exists2 Z, closed_base Z & Z z /\ Z `<=` X `&` Y +}. + +HB.builders Context T (a : TopologicalClosedBase T). + + Definition open_of := + [set A | exists2 D, D `<=` [set ~` X | X in closed_base] & A = \bigcup_(X in D) ~` X]. + + Definition closed_of := [set A | open_of (~` A)]. + + Lemma open_of_setT : open_of setT. + Proof. + Admitted. + + Lemma open_of_bigcup {I} (D : set I) (F : I -> set T) : + (forall i, D i -> open_of (F i)) -> open_of (\bigcup_(i in D) F i). + Proof. Admitted. + + Lemma open_of_cap X Y : open_of X -> open_of Y -> open_of (X `&` Y). + Proof. Admitted. + + HB.instance + Definition to_Topological := + @Topological.Build T open_of closed_of + open_of_setT (@open_of_bigcup) open_of_cap (fun=> erefl). + +HB.end. diff --git a/examples/hulk.v b/examples/hulk.v index 60b68c530..60dc71109 100644 --- a/examples/hulk.v +++ b/examples/hulk.v @@ -258,6 +258,8 @@ Abort. End SlowFailure. +(* cf https://github.com/coq/coq/issues/17223 *) +Optimize Heap. Module FastFailure. diff --git a/structures.v b/structures.v index abae6db4b..30c9015f4 100644 --- a/structures.v +++ b/structures.v @@ -252,14 +252,12 @@ Elpi Accumulate Db hb.db. #[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". Elpi Accumulate lp:{{ -main _ :- coq.version _ _ N _, N < 13, !, - coq.say "HB: HB.locate requires Coq version 8.13 or above". main [str S] :- !, if (decl-location {coq.locate S} Loc) (coq.say "HB: synthesized in file" Loc) (coq.say "HB:" S "not synthesized by HB"). -main _ :- coq.error "Usage: HB.about .". +main _ :- coq.error "Usage: HB.locate .". }}. Elpi Typecheck. Elpi Export HB.locate. @@ -297,6 +295,53 @@ Elpi Typecheck. Elpi Export HB.about. +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) +(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) + +(** [HB.howto (T) Foo.type d] prints possible sequences of factories + to equip a type [T] with a structure [Foo.type], taking into account + structures already instantiated on [T]. The search depth [d] + is the maximum length of the sequences, 3 by default. + The first argument [T] is optional, when ommited [Foo.type] is built + from scratch. + Finally, the first argument can be another structure [Bar.type], + in which case [Foo.type] is built starting from [Bar.type]. +*) + +#[arguments(raw)] Elpi Command HB.howto. +#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi". +#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi". +Elpi Accumulate File "HB/common/stdpp.elpi". +Elpi Accumulate File "HB/common/database.elpi". +Elpi Accumulate File "HB/common/utils.elpi". +Elpi Accumulate File "HB/common/log.elpi". +Elpi Accumulate File "HB/about.elpi". +Elpi Accumulate File "HB/howto.elpi". +Elpi Accumulate Db hb.db. +Elpi Accumulate lp:{{ + +main [trm T, str STgt] :- !, + with-attributes (with-logging (howto.main-trm T STgt none)). +main [trm T, str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-trm T STgt (some Depth))). +main [str T, str STgt] :- !, + with-attributes (with-logging (howto.main-str T STgt none)). +main [str T, str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-str T STgt (some Depth))). +main [str STgt] :- !, + with-attributes (with-logging (howto.main-from [] STgt none)). +main [str STgt, int Depth] :- !, + with-attributes (with-logging (howto.main-from [] STgt (some Depth))). + +main _ :- + coq.error + "Usage: HB.howto [()|] [].". +}}. +Elpi Typecheck. +Elpi Export HB.howto. + + (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *) @@ -532,7 +577,7 @@ HB.structure Definition StructureName params := - [#[infer(variable)]], where [variable : pT] belongs to [params] and is a structure (e.g. from the hierarchy) with a coercion/canonical projection [pT >-> Sortclass]. It modifies the notation [StructureName.type] so as to accept [variable : Type] instead, - and will try to infer it's [pT] by unification (using canonical structure inference), + and will try to infer its [pT] by unification (using canonical structure inference), This is essential in [Lmodule.type R] where [R] should have type [Ring.type] but any [Type] which is canonically a [Ring.type] is accepted thanks to [#[infer(R)]]. If the carrier of the structure [S] is not a [Type] but rather a function, one has diff --git a/tests/about.v b/tests/about.v index 0baebc083..a8971ab2b 100644 --- a/tests/about.v +++ b/tests/about.v @@ -48,4 +48,11 @@ HB.about hierarchy_5_Ring__to__hierarchy_5_SemiRing. (* builder *) HB.about Builders_40.hierarchy_5_Ring_of_AddAG__to__hierarchy_5_BiNearRing_of_AddMonoid. -HB.locate BinNums_Z__canonical__hierarchy_5_AddAG. \ No newline at end of file +HB.locate BinNums_Z__canonical__hierarchy_5_AddAG. + +(* Test minimally qualified names *) +Module Import hierarchy_5. +Module AddComoid. +End AddComoid. +End hierarchy_5. +HB.about Z. diff --git a/tests/about.v.out b/tests/about.v.out index c56aaf2b1..3a56087fd 100644 --- a/tests/about.v.out +++ b/tests/about.v.out @@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are: - addr0 HB: AddMonoid_of_TYPE requires the following mixins: HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: AddMonoid_of_TYPE.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - S : Type - zero : AddMonoid.sort S @@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) HB: AddAG.type characterizing operations and axioms are: - addNr - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring -HB: hierarchy_5.AddMonoid.type is a structure +HB: AddMonoid.type is a structure (from "./examples/demo1/hierarchy_5.v", line 17) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: +HB: AddMonoid.type characterizing operations and axioms are: - addr0 - add0r - addrA - add - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring HB: Ring_of_AddAG is a factory (from "./examples/demo1/hierarchy_5.v", line 108) @@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are: - mulrDl - mulrDr HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and mul0r are derived from addrC and the other ring axioms, following a proof of Hankel (Gerhard Betsch. On the beginnings and development of near-ring @@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and HB: Ring_of_AddAG.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 108) HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - A : Type - one : A @@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, 1995). -HB: add is an operation of structure hierarchy_5.AddMonoid +HB: add is an operation of structure AddMonoid (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE +HB: add comes from mixin AddMonoid_of_TYPE (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddAG.sort is a canonical projection @@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values: - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - Z -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass +HB: AddAG.sort is a coercion from AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) -HB: Z is canonically equipped with mixins: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG +HB: Z is canonically equipped with structures: + - AddMonoid + AddComoid + AddAG (from "(stdin)", line 5) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring + - BiNearRing + SemiRing + Ring (from "(stdin)", line 10) HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid +HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid HB: synthesized in file File "(stdin)", line 5, column 0, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) + diff --git a/tests/about.v.out.13 b/tests/about.v.out.13 deleted file mode 100644 index 891babf10..000000000 --- a/tests/about.v.out.13 +++ /dev/null @@ -1,143 +0,0 @@ -HB: AddMonoid_of_TYPE is a factory - (from "./examples/demo1/hierarchy_5.v", line 2) -HB: AddMonoid_of_TYPE operations and axioms are: - - zero - - add - - addrA - - add0r - - addr0 -HB: AddMonoid_of_TYPE requires the following mixins: -HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - -HB: AddMonoid_of_TYPE.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 2) -HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: -HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE -HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - - S : Type - - zero : AddMonoid.sort S - - add : S -> S -> S - - addrA : associative add - - add0r : left_id 0%G add - - addr0 : right_id 0%G add - -HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 72) -HB: AddAG.type characterizing operations and axioms are: - - addNr - - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring - -HB: hierarchy_5.AddMonoid.type is a structure - (from "./examples/demo1/hierarchy_5.v", line 16) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: - - addr0 - - add0r - - addrA - - add - - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring - -HB: Ring_of_AddAG is a factory - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG operations and axioms are: - - one - - mul - - mulrA - - mulr1 - - mul1r - - mulrDl - - mulrDr -HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: Ring_of_AddAG.Build is a factory constructor - (from "./examples/demo1/hierarchy_5.v", line 108) -HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid -HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid -HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - - A : Type - - one : A - - mul : A -> A -> A - - mulrA : associative mul - - mulr1 : left_id one mul - - mul1r : right_id one mul - - mulrDl : left_distributive mul add - - mulrDr : right_distributive mul add -Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and - mul0r are derived from addrC and the other ring axioms, following a proof - of Hankel (Gerhard Betsch. On the beginnings and development of near-ring - theory. In Near-rings and near-fields. Proceedings of the conference held - in Fredericton, New Brunswick, July 18-24, 1993, pages 1–11. Mathematics - and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, - 1995). - -HB: add is an operation of structure hierarchy_5.AddMonoid - (from "./examples/demo1/hierarchy_5.v", line 16) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE - (from "./examples/demo1/hierarchy_5.v", line 2) - -HB: AddAG.sort is a canonical projection - (from "./examples/demo1/hierarchy_5.v", line 72) -HB: AddAG.sort has the following canonical values: - - Z - - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 194) - - @eta - -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass - (from "./examples/demo1/hierarchy_5.v", line 72) - -HB: Z is canonically equipped with mixins: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG - (from "(stdin)", line 3) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring - (from "(stdin)", line 8) - -HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 194) - -HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 194) - -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid -HB: synthesized in file -File "(stdin)", line 3, column 165, characters 125-249: diff --git a/tests/about.v.out.14 b/tests/about.v.out.15 similarity index 65% rename from tests/about.v.out.14 rename to tests/about.v.out.15 index a93916a7a..e8aa4b533 100644 --- a/tests/about.v.out.14 +++ b/tests/about.v.out.15 @@ -8,13 +8,13 @@ HB: AddMonoid_of_TYPE operations and axioms are: - addr0 HB: AddMonoid_of_TYPE requires the following mixins: HB: AddMonoid_of_TYPE provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: AddMonoid_of_TYPE.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddMonoid_of_TYPE.Build requires its subject to be already equipped with: HB: AddMonoid_of_TYPE.Build provides the following mixins: - - hierarchy_5.AddMonoid_of_TYPE + - AddMonoid_of_TYPE HB: arguments: AddMonoid_of_TYPE.Build S zero add addrA add0r addr0 - S : Type - zero : AddMonoid.sort S @@ -27,33 +27,33 @@ HB: AddAG.type is a structure (from "./examples/demo1/hierarchy_5.v", line 73) HB: AddAG.type characterizing operations and axioms are: - addNr - opp -HB: hierarchy_5.AddAG is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid (* new, not from inheritance *) -HB: hierarchy_5.AddAG inherits from: - - hierarchy_5.AddMonoid - - hierarchy_5.AddComoid -HB: hierarchy_5.AddAG is inherited by: - - hierarchy_5.Ring +HB: AddAG is a factory for the following mixins: + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid (* new, not from inheritance *) +HB: AddAG inherits from: + - AddMonoid + - AddComoid +HB: AddAG is inherited by: + - Ring -HB: hierarchy_5.AddMonoid.type is a structure +HB: AddMonoid.type is a structure (from "./examples/demo1/hierarchy_5.v", line 17) -HB: hierarchy_5.AddMonoid.type characterizing operations and axioms are: +HB: AddMonoid.type characterizing operations and axioms are: - addr0 - add0r - addrA - add - zero -HB: hierarchy_5.AddMonoid is a factory for the following mixins: - - hierarchy_5.AddMonoid_of_TYPE (* new, not from inheritance *) -HB: hierarchy_5.AddMonoid inherits from: -HB: hierarchy_5.AddMonoid is inherited by: - - hierarchy_5.AddComoid - - hierarchy_5.AddAG - - hierarchy_5.BiNearRing - - hierarchy_5.SemiRing - - hierarchy_5.Ring +HB: AddMonoid is a factory for the following mixins: + - AddMonoid_of_TYPE (* new, not from inheritance *) +HB: AddMonoid inherits from: +HB: AddMonoid is inherited by: + - AddComoid + - AddAG + - BiNearRing + - SemiRing + - Ring HB: Ring_of_AddAG is a factory (from "./examples/demo1/hierarchy_5.v", line 108) @@ -66,11 +66,11 @@ HB: Ring_of_AddAG operations and axioms are: - mulrDl - mulrDr HB: Ring_of_AddAG requires the following mixins: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and mul0r are derived from addrC and the other ring axioms, following a proof of Hankel (Gerhard Betsch. On the beginnings and development of near-ring @@ -82,11 +82,11 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and HB: Ring_of_AddAG.Build is a factory constructor (from "./examples/demo1/hierarchy_5.v", line 108) HB: Ring_of_AddAG.Build requires its subject to be already equipped with: - - hierarchy_5.AddMonoid_of_TYPE - - hierarchy_5.AddComoid_of_AddMonoid - - hierarchy_5.AddAG_of_AddComoid + - AddMonoid_of_TYPE + - AddComoid_of_AddMonoid + - AddAG_of_AddComoid HB: Ring_of_AddAG.Build provides the following mixins: - - hierarchy_5.BiNearRing_of_AddMonoid + - BiNearRing_of_AddMonoid HB: arguments: Ring_of_AddAG.Build A [one] [mul] mulrA mulr1 mul1r mulrDl mulrDr - A : Type - one : A @@ -104,9 +104,9 @@ Doc: Builds a Ring from an Abelian Group: the absorbing properties mul0r and and its Applications, 336. Kluwer Academic Publishers Group, Dordrecht, 1995). -HB: add is an operation of structure hierarchy_5.AddMonoid +HB: add is an operation of structure AddMonoid (from "./examples/demo1/hierarchy_5.v", line 17) -HB: add comes from mixin hierarchy_5.AddMonoid_of_TYPE +HB: add comes from mixin AddMonoid_of_TYPE (from "./examples/demo1/hierarchy_5.v", line 10) HB: AddAG.sort is a canonical projection @@ -116,27 +116,36 @@ HB: AddAG.sort has the following canonical values: - Ring.sort (from "./examples/demo1/hierarchy_5.v", line 196) - Z -HB: AddAG.sort is a coercion from hierarchy_5.AddAG to Sortclass +HB: AddAG.sort is a coercion from AddAG to Sortclass (from "./examples/demo1/hierarchy_5.v", line 73) -HB: Z is canonically equipped with mixins: - - hierarchy_5.AddMonoid - hierarchy_5.AddComoid - hierarchy_5.AddAG +HB: Z is canonically equipped with structures: + - AddMonoid + AddComoid + AddAG (from "(stdin)", line 5) - - hierarchy_5.BiNearRing - hierarchy_5.SemiRing - hierarchy_5.Ring + - BiNearRing + SemiRing + Ring (from "(stdin)", line 10) HB: hierarchy_5_Ring_class__to__hierarchy_5_SemiRing_class is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) HB: hierarchy_5_Ring__to__hierarchy_5_SemiRing is a coercion from - hierarchy_5.Ring to hierarchy_5.SemiRing - (from "./examples/demo1/hierarchy_5.v", line 196) + Ring to SemiRing (from "./examples/demo1/hierarchy_5.v", line 196) -HB: todo HB.about for builder from hierarchy_5.Ring_of_AddAG to -hierarchy_5.BiNearRing_of_AddMonoid +HB: todo HB.about for builder from Ring_of_AddAG to BiNearRing_of_AddMonoid HB: synthesized in file File "(stdin)", line 5, column 122, character 127: +Interactive Module hierarchy_5 started +Interactive Module AddComoid started +HB: Z is canonically equipped with structures: + - AddMonoid + demo1.hierarchy_5.AddComoid + AddAG + (from "(stdin)", line 5) + - BiNearRing + SemiRing + Ring + (from "(stdin)", line 10) + diff --git a/tests/compress_coe.v.out.13 b/tests/compress_coe.v.out.13 deleted file mode 100644 index 5a493ef33..000000000 --- a/tests/compress_coe.v.out.13 +++ /dev/null @@ -1,19 +0,0 @@ -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type diff --git a/tests/compress_coe.v.out.14 b/tests/compress_coe.v.out.14 deleted file mode 100644 index 5a493ef33..000000000 --- a/tests/compress_coe.v.out.14 +++ /dev/null @@ -1,19 +0,0 @@ -Datatypes_prod__canonical__compress_coe_D = -fun D D' : D.type => -{| - D.sort := D.sort D * D.sort D'; - D.class := - {| - D.compress_coe_hasA_mixin := - prodA (compress_coe_D__to__compress_coe_A D) - (compress_coe_D__to__compress_coe_A D'); - D.compress_coe_hasB_mixin := - prodB tt (compress_coe_D__to__compress_coe_B D) - (compress_coe_D__to__compress_coe_B D'); - D.compress_coe_hasC_mixin := - prodC tt tt (compress_coe_D__to__compress_coe_C D) - (compress_coe_D__to__compress_coe_C D'); - D.compress_coe_hasD_mixin := prodD D D' - |} -|} - : D.type -> D.type -> D.type diff --git a/tests/grefclass.v b/tests/grefclass.v new file mode 100644 index 000000000..c814aa584 --- /dev/null +++ b/tests/grefclass.v @@ -0,0 +1,12 @@ +From HB Require Import structures. + +Definition pred T := T -> bool. + +HB.mixin Record isPredNat (f : pred nat) := {}. + +HB.structure Definition PredNat := {f of isPredNat f}. + +Section TestSort. +Variable p : PredNat.type. +Check p : pred nat. +End TestSort. diff --git a/tests/factory_sort_tac.v b/tests/hb_pack.v similarity index 87% rename from tests/factory_sort_tac.v rename to tests/hb_pack.v index ccf6cb743..67b32cc0b 100644 --- a/tests/factory_sort_tac.v +++ b/tests/hb_pack.v @@ -25,7 +25,7 @@ About hasA'.type. Section test. Variables (G : Prop) (P : AB.type -> G). - +(* problem with planB Goal forall T (a b : T), G. Proof. move=> T a b. @@ -35,7 +35,7 @@ pose Tab := hasB.Build A (b,b). pose AB : AB.type := ltac:(elpi HB.pack (A) (Tab)). exact: P AB. Qed. - +*) Goal forall T (a b : T), G. Proof. move=> T a b. @@ -111,4 +111,15 @@ pose X := Foo.pack T (HasFoo.Build A P T H). Check X : Foo.type A P. Abort. -End test2. \ No newline at end of file +End test2. + +HB.mixin Record isID T (F : T -> T) := { p : forall x : T, F x = x }. +HB.structure Definition Fun T := { F of isID T F }. + +Goal forall f : nat -> nat, forall p : (forall x, f x = x ), True. +intros f p. +pose F := isID.Build nat f p. +pose T : Fun.type nat := HB.pack f F. +Check T : Fun.type nat. +Abort. + diff --git a/tests/howto.v b/tests/howto.v new file mode 100644 index 000000000..b7265d19b --- /dev/null +++ b/tests/howto.v @@ -0,0 +1,33 @@ +From Coq Require Import ZArith ssrfun ssreflect. +From HB Require Import structures. +From HB Require Import demo1.hierarchy_5. + +HB.howto Ring.type. + +HB.howto Ring.type 2. + +HB.howto Z Ring.type. + +HB.howto Z Ring.type 2. + +Fail HB.howto Z Ring.type 0. + +HB.howto AddComoid.type Ring.type. + +HB.instance + Definition _ := + AddAG_of_TYPE.Build Z 0%Z Z.add Z.opp + Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l. + +HB.howto Z Ring.type. + +HB.howto AddAG.type Ring.type. + +HB.instance + Definition _ := + Ring_of_TYPE.Build Z 0%Z 1%Z Z.add Z.opp Z.mul + Z.add_assoc Z.add_comm Z.add_0_l Z.add_opp_diag_l + Z.mul_assoc Z.mul_1_l Z.mul_1_r + Z.mul_add_distr_r Z.mul_add_distr_l. + +HB.howto Z Ring.type. diff --git a/tests/howto.v.out b/tests/howto.v.out new file mode 100644 index 000000000..a83cbce85 --- /dev/null +++ b/tests/howto.v.out @@ -0,0 +1,55 @@ +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddComoid_of_TYPE; AddAG_of_AddComoid; Ring_of_AddAG + - AddComoid_of_TYPE; AddAG_of_AddComoid; SemiRing_of_AddComoid + - AddMonoid_of_TYPE; AddComoid_of_AddMonoid; Ring_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_TYPE + - AddAG_of_TYPE; BiNearRing_of_AddMonoid + - AddAG_of_TYPE; Ring_of_AddAG + - AddAG_of_TYPE; SemiRing_of_AddComoid + - AddComoid_of_TYPE; Ring_of_AddComoid + +The command has indeed failed with message: +HB: no solution found, try to increase search depth. +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - Ring_of_AddComoid + - AddAG_of_AddComoid; BiNearRing_of_AddMonoid + - AddAG_of_AddComoid; Ring_of_AddAG + - AddAG_of_AddComoid; SemiRing_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid + +HB: solutions (use 'HB.about F.Build' to see the arguments of each factory F): + - BiNearRing_of_AddMonoid + - Ring_of_AddAG + - SemiRing_of_AddComoid + +HB: nothing to do. diff --git a/tests/infer.v b/tests/infer.v index a89d6104e..8f46f6229 100644 --- a/tests/infer.v +++ b/tests/infer.v @@ -17,7 +17,7 @@ HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : Type) := { HB.structure Definition bar A P B := { T of barm A P B T }. #[skip="8.1[0-5].*"] HB.check (bar.type_ bool nat bool). -#[skip="8.16.*", fail] HB.check (bar.type_ bool nat bool). +#[skip="8.1[6-9].*", fail] HB.check (bar.type_ bool nat bool). Print bar.phant_type. Print bar.type. Check bar.type bool nat bool. diff --git a/tests/interleave_context.v b/tests/interleave_context.v index dd055fcb3..8da42ed0a 100644 --- a/tests/interleave_context.v +++ b/tests/interleave_context.v @@ -7,9 +7,12 @@ HB.structure Definition A n := { T of HasA n T }. HB.mixin Record HasB (X : A.type 0) (T : Type) := { b : X -> T }. HB.structure Definition B (X : A.type 0) := { T of HasB X T }. -#[verbose] +(* Since `B` expects an argument of type `A.type 0` (and not just + just the naked type `T`) we pass `A.clone 0 T _` + (of type `A.type 0`) and inference uses the first + parameter `A` to elaborate it. *) HB.mixin Record IsSelfA T of A 0 T & B (A.clone 0 T _) T := {}. -#[verbose] + HB.structure Definition SelfA := { T of IsSelfA T }. HB.factory Record IsSelfA' T := { a : T ; b : T -> T}. @@ -19,5 +22,4 @@ HB.builders Context T of IsSelfA' T. HB.instance Definition _ := IsSelfA.Build T. HB.end. -#[verbose] - HB.instance Definition _ := IsSelfA'.Build nat 0 id. \ No newline at end of file +HB.instance Definition _ := IsSelfA'.Build nat 0 id. diff --git a/tests/rev_coerce.v b/tests/rev_coerce.v new file mode 100644 index 000000000..543bce5b2 --- /dev/null +++ b/tests/rev_coerce.v @@ -0,0 +1,24 @@ +From HB Require Import structures. + +HB.mixin Record isPointed V := { point : V }. +HB.structure Definition Pointed := {V of isPointed V}. + +Definition popt (U : Pointed.type) := option U. +HB.instance Definition _ U := isPointed.Build (popt U) None. + +HB.mixin Record hasTrue (U V : Pointed.type) (f : U -> V) := { + true_subproof : True +}. +HB.structure Definition HasTrue (U V : Pointed.type) := {f of hasTrue U V f}. + +Definition poptp (U : Pointed.type) (p : popt U) : U := point. + +Section Bug. +Variable U : Pointed.type. + +Check hasTrue.Build (popt U) U (@poptp U) I. +Set Printing Universes. +(* There used to be a universe issue at the line below: *) +HB.instance Definition _ := hasTrue.Build (popt U) U (@poptp U) I. + +End Bug.