Merge pull request #147 from math-comp/exports

Managing Exports

Author: CohenCyril

_CoqProject

@@ -52,5 +52,6 @@ tests/duplicate_structure.v
 tests/instance_params_no_type.v
 tests/test_CS_db_filtering.v
 tests/subtype.v
+tests/exports.v
 
 -R . HB

hb.elpi

@@ -1241,13 +1241,20 @@ main-declare-builder (builder _ SrcFactory TgtMixin B) FromClauses MoreFromClaus
   ].
 
 % [export Module] exports a Module now adds it to the collection of
-% modules to export in the end
+% modules to export in the end of the current enclosing module,
+% by the command HB.Exports
+
 pred to-export o:modpath.
 pred export i:modpath.
 export Module :- !,
   coq.env.export-module Module,
   acc current (clause _ _ (to-export Module)).
 
+pred main-reexport.
+main-reexport :- !,
+  std.findall (to-export Module_) Mods,
+  std.forall Mods (x\ sigma y\ to-export y = x, coq.env.export-module y).
+
 pred mk-mixin-fun i:list-w-params mixinname, i:term, o:term.
 mk-mixin-fun ML X MLX :- mk-mixin-fun.then ML (p\ t\ body\ body = X) MLX.
 
@@ -1673,11 +1680,6 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
 
   coq.env.begin-module "Exports" none,
   declare-sort-coercion Structure SortProjection,
-  if-verbose (coq.say "HB: exporting operations"),
-  ClassAlias => ClassRequires => Factories =>
-    export-operations Structure SortProjection ClassProjection MLwP [] EX MLToExport,
-  % TODO: issue an Arguments op T : rename, where T is the name written by
-  %   the user in Definition foo := { T of ... }
 
   if-verbose (coq.say "HB: exporting unification hints"),
   ClassAlias => ClassRequires => Factories =>
@@ -1693,10 +1695,8 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
     (coq.say "declare-structure:" ClassName "should be an inductive", fail),
 
   if-verbose (coq.say "HB: accumulating various props"),
-  std.map MLToExport (m\r\ r = mixin-first-class m ClassName) MixinFirstClass,
   std.flatten [
-      MixinFirstClass, EX, Factories,
-      [ClassRequires], [ClassAlias], [is-structure Structure],
+      Factories, [ClassRequires], [ClassAlias], [is-structure Structure],
       NewJoins, [class-def CurrentClass]
     ]
     NewClauses,
@@ -1711,6 +1711,20 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [
 
   export Exports,
 
+  if-verbose (coq.say "HB: exporting operations"),
+    ClassAlias => ClassRequires => Factories =>
+      export-operations Structure SortProjection ClassProjection MLwP [] EX   MLToExport,
+    % TODO: issue an Arguments op T : rename, where T is the name written by
+    %   the user in Definition foo := { T of ... }
+
+  if-verbose (coq.say "HB: start operations meta-data module ElpiOperations"),
+  ElpiOperationModName is "ElpiOperations" ^ {std.any->string {new_int}},
+  coq.env.begin-module ElpiOperationModName none,
+    std.map MLToExport (m\r\ r = mixin-first-class m ClassName) MixinFirstClass,
+    std.forall {std.append EX MixinFirstClass} (c\ acc current (clause _ _ c)),
+  coq.env.end-module ElpiOperations,
+  export ElpiOperations,
+
   declare-factory-abbrev Module (factory-by-classname ClassName),
 
   NewClauses => if-MC-compat (mc-compat-structure Module ModulePath MLToExport {w-params.nparams MLwP} ClassName ClassProjection),

structures.v

@@ -454,6 +454,51 @@ main _ :- coq.error "Usage: HB.end.".
 Elpi Typecheck.
 Elpi Export HB.end.
 
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+(** [HB.export Modname] does the work of [Export Modname] but also schedules [Modname]
+   to be exported later on, when [HB.reexport] is called.
+   Note that the list of modules to be exported is stored in the current module,
+   hence the recommended way to do is
+   <<<
+   Module Algebra.
+     HB.mixin .... HB.structure ...
+     Module MoreExports. ... End MoreExports. HB.export MoreExports.
+     ...
+     Module Export. HB.reexport. End Exports.
+   End Algebra.
+   Export Algebra.Exports.
+   >>> *)
+
+Elpi Command HB.export.
+Elpi Accumulate File "hb.elpi".
+Elpi Accumulate Db hb.db.
+Elpi Accumulate lp:{{
+main [str M] :- !, with-attributes (export {coq.locate-module M}).
+main _ :- coq.error "Usage: HB.export M.".
+}}.
+Elpi Typecheck.
+Elpi Export HB.export.
+
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+(* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
+
+(** [HB.reexport] Exports all modules that were previously exported via [HB.export].
+   It is useful to create one big module with all exports at the end of a file. *)
+
+Elpi Command HB.reexport.
+Elpi Accumulate File "hb.elpi".
+Elpi Accumulate Db hb.db.
+Elpi Accumulate lp:{{
+main [] :- !, with-attributes (main-reexport).
+main _ :- coq.error "Usage: HB.reexport.".
+}}.
+Elpi Typecheck.
+Elpi Export HB.reexport.
+
 (*
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)

tests/exports.v

@@ -0,0 +1,75 @@
+From Coq Require Import ssreflect ssrfun.
+From HB Require Import structures.
+
+Module Enclosing.
+(**************************************************************************)
+(* Stage 0: +Ring+                                                        *)
+(**************************************************************************)
+
+HB.mixin Record Ring_of_TYPE 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;
+}.
+HB.structure Definition Ring := { A of Ring_of_TYPE A }.
+
+(* Notations *)
+
+Module RingExports.
+Declare Scope hb_scope.
+Delimit Scope hb_scope with G.
+Local Open Scope hb_scope.
+Notation "0" := zero : hb_scope.
+Notation "1" := one : hb_scope.
+Infix "+" := (@add _) : hb_scope.
+Notation "- x" := (@opp _ x) : hb_scope.
+Infix "*" := (@mul _) : hb_scope.
+Notation "x - y" := (x + - y) : hb_scope.
+End RingExports.
+HB.export RingExports.
+
+(* Theory *)
+
+Section Theory.
+Local Open Scope hb_scope.
+Variable R : Ring.type.
+Implicit Type (x : R).
+
+Lemma addr0 : right_id (@zero R) add.
+Proof. by move=> x; rewrite addrC add0r. Qed.
+
+Lemma addrN : right_inverse (@zero R) opp add.
+Proof. by move=> x; rewrite addrC addNr. Qed.
+
+Lemma subrr x : x - x = 0.
+Proof. by rewrite addrN. Qed.
+
+Lemma addrNK x y : x + y - y = x.
+Proof. by rewrite -addrA subrr addr0. Qed.
+
+End Theory.
+
+Module Exports.
+HB.reexport.
+End Exports.
+End Enclosing.
+
+(* We miss the coercions, canonical and elpi metadata *)
+Fail Check forall (R : Enclosing.Ring.type) (x : R), x = x.
+Fail Check 0%G.
+
+Export Enclosing.Exports.
+
+Check forall (R : Enclosing.Ring.type) (x : R), x = x.
+Check 0%G.