Merge pull request #296 from math-comp/fun_instances

Adding missing feature: instances on function spaces

Author: CohenCyril

.github/workflows/main.yml

@@ -17,11 +17,9 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.13'
-          - '8.14'
-          - '8.15'
+          - '8.16'
         ocaml_version:
-          - '4.07-flambda'
+          - '4.09-flambda'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1
@@ -40,8 +38,8 @@ jobs:
     - uses: coq-community/docker-coq-action@v1
       with:
         opam_file: './coq-hierarchy-builder.opam'
-        coq_version: '8.14'
-        ocaml_version: '4.07-flambda'
+        coq_version: '8.16'
+        ocaml_version: '4.09-flambda'
         script: |
           mkdir /home/coq/workspace
           cp -ra . /home/coq/workspace

.github/workflows/nix-action-coq-mcHB-8.16.yml

@@ -366,6 +366,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-algebra"
+  mathcomp-analysis:
+    needs:
+    - coq
+    - mathcomp-ssreflect
+    - mathcomp-field
+    - 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-analysis
+      run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n   --argstr\
+        \ bundle \"coq-mcHB-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"
+    - 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-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'
+      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-analysis"
   mathcomp-character:
     needs:
     - coq

.nix/config.nix

@@ -13,13 +13,12 @@
       graph-theory.job = false;
       fourcolor.override.version = "master";
       odd-order.override.version = "hirarchy-builder";
-      mathcomp-finmap.override.version = "#84";
+      mathcomp-finmap.override.version = "proux01:hierarchy-builder";
       mathcomp.analyis.override.version = "#694";
     };
   in {
     "coq-mcHB-8.16".coqPackages = {
       coq.override.version = "8.16";
-      coq-elpi.override.version = "master";
       mathcomp-analysis.override.version = "coq816";
     } // mcHBcommon;
 
@@ -29,7 +28,6 @@
 
     "coq-8.16".coqPackages = {
       coq.override.version = "8.16";
-      coq-elpi.override.version = "master";
       mathcomp.override.version = "mathcomp-1.15.0";
     };
     "coq-8.15".coqPackages = {

.nix/coq-overlays/coq-elpi/default.nix

@@ -15,13 +15,15 @@ in mkCoqDerivation {
   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.14.0".sha256     = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
+  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";

HB/common/compat_815.elpi

@@ -0,0 +1,2 @@
+pred compat.coercion.declare i:coercion.
+compat.coercion.declare C :- @global! => coq.coercion.declare C.

HB/common/compat_all.elpi

@@ -0,0 +1,2 @@
+pred compat.coercion.declare i:coercion.
+compat.coercion.declare C :- @global! => @reversible! => coq.coercion.declare C.

HB/common/database.elpi

@@ -309,33 +309,39 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst.
 pred has-cs-instance i:gref, i:cs-instance.
 has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
 
+pred term->cs-pattern i:term, o:cs-pattern.
+term->cs-pattern (prod _ _ _) cs-prod.
+term->cs-pattern (sort U) (cs-sort U).
+term->cs-pattern T (cs-gref GR) :- term->gref T GR.
+term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
+
+pred cs-pattern->name i:cs-pattern, o:string.
+cs-pattern->name cs-prod "prod".
+cs-pattern->name (cs-sort _) "sort".
+cs-pattern->name cs-default "default".
+cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
 pred get-canonical-structures i:term, o:list structure.
 get-canonical-structures TyTrm StructL :- std.do! [
-  term->gref TyTrm CanonValue,
-  if (coq.version _ _ N _, N > 12)
-     (coq.CS.db-for _ (cs-gref CanonValue) DBGTyL)
-     (std.filter {coq.CS.db} (has-cs-instance CanonValue) DBGTyL),
+  term->cs-pattern TyTrm Pat, !,
+  coq.CS.db-for _ Pat DBGTyL,
   std.map-filter DBGTyL get-cs-structure StructL,
 ].
 
 pred get-canonical-instances i:term, o:list constant.
-get-canonical-instances TyTrm CL :- std.do! [
-  term->gref TyTrm CanonValue,
-  if (coq.version _ _ N _, N > 12)
-     (coq.CS.db-for _ (cs-gref CanonValue) DBGTyL)
-     (std.filter {coq.CS.db} (has-cs-instance CanonValue) DBGTyL),
-  std.map-filter DBGTyL get-cs-instance CL,
+get-canonical-instances TyTrm StructL :- std.do! [
+  term->cs-pattern TyTrm Pat, !,
+  coq.CS.db-for _ Pat DBGTyL,
+  std.map-filter DBGTyL get-cs-instance StructL,
 ].
 
 pred has-CS-instance? i:term, i:structure.
-has-CS-instance? TyTerm (indt Struct) :- coq.version _ _ N _, N > 12, !,
-  term->gref TyTerm Value,
+has-CS-instance? TyTerm (indt Struct) :- std.do! [
+  term->cs-pattern TyTerm Pat,
   coq.env.projections Struct [some Proj, _],
-  coq.CS.db-for (const Proj) (cs-gref Value) L,
-  not(L = []).
-has-CS-instance? TyTerm Struct :-
-  get-canonical-structures TyTerm StructL,
-  std.mem! StructL Struct.
+  coq.CS.db-for (const Proj) Pat L,
+  not(L = [])
+].
 
 pred structure-nparams i:structure, o:int.
 structure-nparams Structure NParams :-

HB/common/log.elpi

@@ -159,7 +159,7 @@ env.import-module MPNice M :- std.do! [
 
 pred coercion.declare i:coercion.
 coercion.declare C :- std.do! [
-  @global! => coq.coercion.declare C,
+  compat.coercion.declare C,
   C = coercion GR _ SRCGR TGTCL,
   coq.gref->id GR Name,
   log.private.log-vernac (log.private.coq.vernac.coercion Name SRCGR TGTCL),

HB/instance.elpi

@@ -102,13 +102,15 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
      fail,
 
   !,
-  coq.term->gref T TGR,
-  Name is  {gref->modname-label TGR 1 "_"} ^ "__canonical__" ^ {gref->modname Struct 2 "_"},
+
+  Name is {cs-pattern->name {term->cs-pattern T}}
+    ^ "__canonical__" ^ {gref->modname Struct 2 "_" },
 
   if-verbose (coq.say {header} "declare canonical structure instance" Name),
 
   get-constructor Struct KS,
-  private.optimize-class-body TGR {std.length Params} KCApp KCAppNames Clauses,
+  coq.safe-dest-app T THD _,
+  private.optimize-class-body THD {std.length Params} KCApp KCAppNames Clauses,
   coq.mk-app (global KS) {std.append Params [T, KCAppNames]} S,
   if-verbose (coq.say {header} "structure instance for" Name "is" {coq.term->string S}),
   std.assert-ok! (coq.typecheck S STy) "declare-all: S illtyped",
@@ -329,12 +331,12 @@ pred hnf i:term, o:term.
 hnf X R :- get-option "hnf" tt, !, unwind {whd X []} R.
 hnf X X.
 
-pred optimize-class-body i:gref, i:int, i:term, o:term, o:list prop.
-optimize-class-body TGR NParams (let _ _ MBo R) R1 Clauses :- std.do! [
+pred optimize-class-body i:term, i:int, i:term, o:term, o:list prop.
+optimize-class-body T NParams (let _ _ MBo R) R1 Clauses :- std.do! [
   declare-mixin-name {hnf MBo} MC CL1,
-  if (TGR = indt _, MC = global (const C), not(coq.env.opaque? C))
+  if (T = global (indt _), MC = global (const C), not(coq.env.opaque? C))
      (log.coq.strategy.set [C] (level 1000)) true, % opaque stops simpl
-  optimize-class-body TGR NParams (R MC) R1 CL2,
+  optimize-class-body T NParams (R MC) R1 CL2,
   std.append CL1 CL2 Clauses,
 ].
 optimize-class-body _ _ (app L) (app L) [].

HB/structure.elpi

@@ -5,6 +5,7 @@ namespace structure {
 
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
 %  cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
+pred declare i:string, i:term, i:sort.
 pred declare i:string, i:term, i:universe.
 declare Module BSkel Sort :- std.do! [
   disable-id-phant BSkel BSkelNoId,
@@ -495,6 +496,7 @@ pred synthesize-fields.body i:list term, i:term, i:list (w-args mixinname), o:in
 synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :-
   synthesize-fields T ML FS.
 
+pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl.
 pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl.
 mk-record+sort-field Sort _ T F (record RecordName (sort Sort) "Pack" (field _ "sort" T F)) :- !, std.do! [
   if (get-option "infer" _) (RecordName = "type_") (RecordName = "type")
@@ -505,6 +507,7 @@ mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global C
   std.append Params [T] Args.
 
 % Builds the axioms record and the factories from this class to each mixin
+pred declare-class+structure i:mixins, i:sort, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
 pred declare-class+structure i:mixins, i:universe, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
 declare-class+structure MLwP Sort
     (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories