saturate: honor #[export]

.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

HB/structures.v

@@ -1,5 +1,5 @@
 (* Support constants, to be kept in sync with shim/structures.v *)
-From Corelib Require Import ssreflect ssrfun.
+From Coq Require Import ssreflect ssrfun.
 
 Variant error_msg := NoMsg | IsNotCanonicallyA (x : Type).
 Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : error_msg) :=
@@ -21,17 +21,17 @@
 Register id_phant_disabled as hb.id_disabled.
 Register ignore as hb.ignore.
 Register ignore_disabled as hb.ignore_disabled.
 Register Coq.Init.Datatypes.None as hb.none.
 Register nomsg as hb.nomsg.
 Register is_not_canonically_a as hb.not_a_msg.
 Register Coq.Init.Datatypes.Some as hb.some.
 Register Coq.Init.Datatypes.pair as hb.pair.
 Register Coq.Init.Datatypes.prod as hb.prod.
 Register Coq.Init.Specif.sigT as hb.sigT.
 Register Coq.ssr.ssreflect.phant as hb.phant.
 Register Coq.ssr.ssreflect.Phant as hb.Phant.
 Register Coq.ssr.ssreflect.phantom as hb.phantom.
 Register Coq.ssr.ssreflect.Phantom as hb.Phantom.
 Register Coq.Init.Logic.eq as hb.eq.
 Register Coq.Init.Logic.eq_refl as hb.erefl.
 Register new as hb.new.

_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).