saturate: honor #[export]

Author: gares

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,
@@ -265,7 +265,11 @@ saturate-instances Filter :- std.do! [
 
   Clauses => std.forall2 TL UKL (t\k\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),
+
+  private.clauses-for-export CI 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) :=

_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
 

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