Merge pull request #373 from math-comp/fix-spill-next-coq-elpi

Do not spill predicates defined in files accumulated after the spilling

Author: gares

HB/common/database.elpi

@@ -233,9 +233,10 @@ assert-building-bottom-up CurrentClass C3n C1n C2n :-
   CurrentClass = class CC _ _,
   if (not (sub-class? CurrentClass (class C3n X Y)))
      (gref->modname CC 1 "." Before, gref->modname_short C3n "." After,
+      gref->modname_short C1n "." C1nS, gref->modname_short C2n "." C2nS,
       Msg1 is "- declare structure " ^ Before ^ " before structure " ^ After ^ " if " ^ After ^ " inherits from it;",
       Msg2 is "- declare an additional structure that inherits from both "
-        ^ {gref->modname_short C1n "."} ^ " and " ^ {gref->modname_short C2n "."}
+        ^ C1nS ^ " and " ^ C2nS
         ^ " and from which " ^ Before ^ " and/or " ^ After ^ " inherit.",
       coq.error "You must declare the hierarchy bottom-up or addd a missing join."
        "There are two ways out:"

HB/factory.elpi

@@ -166,7 +166,8 @@ cdecl->w-mixins.mixins (context-item ID _ TySkel none Rest) Out :- !,
 % The identity builder
 pred declare-id-builder i:factoryname, o:prop.
 declare-id-builder GR (from GR GR (const C)) :- std.do! [
-  synthesis.mixins-w-params.fun {gref-deps GR} (declare-id-builder.aux GR) IDBodySkel,
+  gref-deps GR GRD,
+  synthesis.mixins-w-params.fun GRD (declare-id-builder.aux GR) IDBodySkel,
   std.assert-ok! (coq.elaborate-skeleton IDBodySkel IDType IDBody) "identity builder illtyped",
   log.coq.env.add-const-noimplicits "identity_builder" IDBody IDType @transparent! C,
 ].
@@ -281,7 +282,9 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   ]] NewClauses,
   acc-clauses current NewClauses,
 
-  std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits,
+  list-w-params_list MLwP MLwoP,
+  std.map MLwoP (_\ r\ r = maximal) Implicits,
+  /* std.map {list-w-params_list MLwP} (_\ r\ r = maximal) Implicits, */
   @global! => log.coq.arguments.set-implicit GRK [[maximal|Implicits]],
   % @global! => log.coq.coercion.declare FactorySortCoe,
 

HB/howto.elpi

@@ -100,7 +100,8 @@ pred list_factories o:list factory_deps_prov.
 list_factories FL :-
   std.map-filter {std.findall (factory-constructor _ _)} list_factories.aux FL.
 list_factories.aux (factory-constructor F _) (fdp F DML PML) :-
-  list-w-params_list {gref-deps F} DML,
+  gref-deps F FD,
+  list-w-params_list FD DML,
   list-w-params_list {factory-provides F} PML.
 
 % [paths-from-for-step MLSrc ML K R] returns in [R] a list of sequences

HB/structure.elpi

@@ -275,7 +275,8 @@ export-1-operation M Struct Psort Pclass MwP (some Poperation) EXI EXO :- !, std
 
   w-params.nparams MwP NP,
   NImplicits is NP + 1,
-  std.map {std.iota NImplicits} (_\r\ r = maximal) Implicits,
+  std.iota NImplicits INI,
+  std.map INI (_\r\ r = maximal) Implicits,
   @global! => log.coq.arguments.set-implicit (const C) [Implicits],
 
   EXO = [exported-op M Poperation C|EXI]
@@ -315,8 +316,9 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [
   std.map TML (from FC) Builders,
   std.map Builders (x\r\mk-app (global x) Params r) BuildersP,
 
+  factory-nparams TC TCNP,
   mk-app (global {get-constructor TC})
-    {coq.mk-n-holes {factory-nparams TC}} KCHoles,
+    {coq.mk-n-holes TCNP} KCHoles,
 
   (pi c\ sigma Mixes\
     std.map BuildersP (builder\r\ r = app[builder, T, c]) Mixes,
@@ -343,8 +345,9 @@ mk-coe-structure-body StructureF StructureT TC Coercion SortProjection ClassProj
   mk-app     ClassProjection Params ClassP,
   mk-app     Coercion        Params CoercionP,
 
+  factory-nparams TC TCNP,
   mk-app (global {get-constructor StructureT})
-    {coq.mk-n-holes {factory-nparams TC}} PackPH,
+    {coq.mk-n-holes TCNP} PackPH,
 
   SCoeBody = {{ fun s : lp:StructureP =>
      (* let T := lp:SortP s in*)
@@ -582,7 +585,8 @@ mc-compat-structure ModuleName _Module NewMixins CNParams ClassProjection GRPack
 
   if (NewMixins = [NewMixin]) (std.do! [
     if-verbose (coq.say "mc-compat-structure: declaring notations 'axioms', 'mixin_of' and 'Mixin'"),
-    MArgs is {factory-nparams NewMixin} + 1,
+    factory-nparams NewMixin NewMixinNP,
+    MArgs is NewMixinNP + 1,
     mk-eta MArgs {coq.env.typeof NewMixin} (global NewMixin) EtaNewMixin,
     @global! => log.coq.notation.add-abbreviation "axioms" MArgs EtaNewMixin ff _,
     @deprecated! "mathcomp 2.0.0" "use the factory instead" =>