Merge pull request #564 from math-comp/saturate-export

saturate: honor #[export]

Author: gares

.github/workflows/main.yml

@@ -20,7 +20,7 @@ jobs:
         coq_version:
           - '8.20'
           - '9.0'
-          #- '9.1'
+          - '9.1'
     steps:
     - uses: actions/checkout@v2
     - uses: coq-community/docker-coq-action@v1

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"7af8a21e712b7665447bea5189ce3ff83fcfeac8"
+"f21be9b79484884fb23d06463c6f03cb2a266b8b"

HB/instance.elpi

@@ -250,7 +250,7 @@ mk-factory-sort-factory AliasGR CFL CSL :- std.do! [
 ].
 
 % create instances for all possible combinations of types and structure compatible 
-func saturate-instances cs-pattern ->.
+func saturate-instances cs-pattern -> .
 saturate-instances Filter :- std.do! [
 
   findall-has-mixin-instance Filter ClausesHas,
@@ -263,9 +263,13 @@ saturate-instances Filter :- std.do! [
 
   std.map ClausesHas has-mixin-instance->mixin-src Clauses,
 
-  Clauses => std.forall2 TL UKL (t\k\sigma Classes\
+  Clauses => std.map2 TL UKL (t\k\CI\sigma Classes\
     std.filter AllClasses (no-instance-for k) Classes,
-    declare-all-on-type-constructor t Classes _),
+    declare-all-on-type-constructor t Classes CI) CIL,
+
+  private.clauses-for-export {std.flatten CIL} ClausesExport,
+
+  acc-clauses current ClausesExport,
 ].
 
 func no-instance-for cs-pattern, hbclass ->.
@@ -293,11 +297,15 @@ declare-instance Factory T F Clauses CFL CSL :-
     T F TheFactory FGR Clauses CFL CSL.
 declare-instance Factory T F Clauses CFL CSL :-
   declare-canonical-instances-from-factory Factory T F Clauses1 CFL CSL,
-  if (get-option "export" tt)
+  clauses-for-export {std.append CFL CSL} Clauses2,
+  std.append Clauses1 Clauses2 Clauses.
+
+func clauses-for-export list (pair id constant) -> list prop.
+clauses-for-export CL ECL :-
+   if (get-option "export" tt)
      (coq.env.current-library File,
-      std.map {std.append CFL CSL} (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) Clauses2)
-     (Clauses2 = []),
-     std.append Clauses1 Clauses2 Clauses.
+      std.map CL (x\r\ sigma i c\ x = pr i c, r = instance-to-export File i c) ECL)
+     (ECL = []).
 
 % [add-mixin T F _ M Cl] adds a constant being the mixin instance for M on type
 % T built from factory F

_CoqProject.test-suite

@@ -60,6 +60,7 @@ tests/unit/struct.v
 tests/factory_when_notation.v
 
 tests/saturate_on.v
+tests/saturate_export.v
 tests/bug_435.v
 tests/bug_447.v
 

rocq-hierarchy-builder.opam

@@ -14,7 +14,7 @@ build: [ [ make "build"]
 install: [ make "install" ]
 depends: [
   ("coq" {>= "8.20" & < "8.21~"} & "coq-elpi" {>= "3" | = "dev"}
-  | "rocq-core" {(>= "9.0" & < "9.1~") | = "dev"} & "rocq-elpi" {>= "3" | = "dev"})
+  | "rocq-core" {(>= "9.0" & < "9.2~") | = "dev"} & "rocq-elpi" {>= "3" | = "dev"})
 ]
 conflicts: [
   "coq-hierarchy-builder" {< "1.9~"}

tests/saturate_export.v

@@ -0,0 +1,29 @@
+From HB Require Import structures.
+
+HB.mixin Record HasPoint T := { default : T }.
+
+HB.instance Definition _ : HasPoint nat := HasPoint.Build nat 0.
+HB.instance Definition _ : HasPoint bool := HasPoint.Build bool false.
+HB.instance Definition _ A : HasPoint (list A) := HasPoint.Build (list A) nil.
+HB.instance Definition _ A : HasPoint Type := HasPoint.Build Type nat.
+
+HB.structure Definition Pointed  := { T of HasPoint T }.
+
+Fail Check (list unit : Pointed.type).
+
+Module Foo.
+HB.saturate (list _).
+Module E. HB.reexport. End E.
+End Foo.
+
+Import Foo.E.
+Fail Check (list unit : Pointed.type).
+
+Module Bar.
+#[export]    
+HB.saturate (list _).
+Module E. HB.reexport. End E.
+End Bar.
+
+Import Bar.E.
+Check (list unit : Pointed.type).