separate synterp phase

Author: gares

HB/builders.elpi

@@ -5,21 +5,21 @@ namespace builders {
 
 pred begin i:context-decl.
 begin CtxSkel :- std.do! [
-  Name is "Builders_" ^ {std.any->string {new_int}}, % TODO?
+  std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module",
   if-verbose (coq.say {header} "begin module for builders"),
   log.coq.env.begin-module Name none,
 
   builders.private.factory CtxSkel IDF GRF,
 
   % the Super module to access operations/axioms shadowed by the ones in the factory
+  if-verbose (coq.say {header} "begin module Super"),
+  log.coq.env.begin-module "Super" none,
   if (GRF = indt FRecord) (std.do! [
-    if-verbose (coq.say {header} "begin module Super"),
-    log.coq.env.begin-module "Super" none,
     std.forall {coq.env.projections FRecord}
       builders.private.declare-shadowed-constant,
-    log.coq.env.end-module-name "Super" _,
-    if-verbose (coq.say {header} "ended module Super")
-  ]) (true),
+  ]) true,
+  if-verbose (coq.say {header} "ended module Super"),
+  log.coq.env.end-module-name "Super" _,
 
   log.coq.env.begin-section Name,
   if-verbose (coq.say {header} "postulating factories"),
@@ -31,7 +31,7 @@ begin CtxSkel :- std.do! [
 % "end" is a keyword, be put it in the namespace by hand
 pred builders.end.
 builders.end :- std.do! [
-  current-mode (builder-from _ _ GR ModName),
+  current-mode (builder-from _ _ _ ModName),
 
   log.coq.env.end-section-name ModName,
 
@@ -48,8 +48,7 @@ builders.end :- std.do! [
   std.filter ExportClauses (export.private.abbrev-in-module CurModPath) ExportClausesFiltered,
 
   % TODO: Do we need this module?
-  gref->modname GR 1 "" M,
-  Name is M ^ "_Exports",
+  std.assert!(coq.next-synterp-action (begin-module Name)) "synterp code did not open module",
   log.coq.env.begin-module Name none,
 
   acc-clauses current Clauses,

HB/common/stdpp.elpi

@@ -118,11 +118,6 @@ constraint print-ctx mixin-src {
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
-% approximation, it should be logical path, not the file name
-pred coq.env.current-library o:string.
-coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
-coq.env.current-library "dummy.v".
-
 pred coq.term-is-gref? i:term, o:gref.
 coq.term-is-gref? (global GR) GR :- !.
 coq.term-is-gref? (pglobal GR _) GR :- !.

HB/common/utils-synterp.elpi

@@ -0,0 +1,73 @@
+/*        Hierarchy Builder: algebraic hierarchies made easy
+    This software is released under the terms of the MIT license              */
+
+% runs P in a context where Coq #[attributes] are parsed
+pred with-attributes i:prop.
+with-attributes P :-
+  attributes A,
+  coq.parse-attributes A [
+    att "verbose" bool,
+    att "mathcomp" bool,
+    att "mathcomp.axiom" string,
+    att "short.type" string,
+    att "short.pack" string,
+    att "key" string,
+    att "arg_sort" bool,
+    att "log" bool,
+    att "log.raw" bool,
+    att "compress_coercions" bool,
+    att "export" bool,
+    att "skip" string,
+    att "local" bool,
+    att "fail" bool,
+    att "doc" string,
+    att "primitive" bool,
+    att "non_forgetful_inheritance" bool,
+    att "hnf" bool,
+  ] Opts, !,
+  Opts => (save-docstring, P).
+
+pred if-verbose i:prop.
+if-verbose P :- get-option "verbose" tt, !, P.
+if-verbose _.
+
+% header of if-verbose messages
+pred header o:string.
+header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ".
+
+% approximation, it should be logical path, not the file name
+pred coq.env.current-library o:string.
+coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
+coq.env.current-library "dummy.v".
+
+% this is only declared in hb.db, this declaration is only to avoid a warning
+pred docstring o:loc, o:string.
+
+pred save-docstring.
+save-docstring :-
+  if (get-option "elpi.loc" Loc, get-option "elpi.phase" "interp", get-option "doc" Txt)
+     (coq.elpi.accumulate _ "hb.db" (clause _ _ (docstring Loc Txt)))
+     true.
+
+pred compute-filter i:option string, o:list string.
+compute-filter none [].
+compute-filter (some S) MFilter :- % S is a component of the current modpath
+  coq.env.current-path P,
+  rex_split "\\." S L,
+  compute-filter.aux P L MFilter, !.
+compute-filter (some S) MFilter :-
+  coq.locate-module S M,
+  coq.modpath->path M MFilter.
+compute-filter.aux [S|_] [S] [S] :- !.
+compute-filter.aux [S|XS] [S|SS] [S|YS] :- compute-filter.aux XS SS YS.
+compute-filter.aux [X|XS] L [X|YS] :- compute-filter.aux XS L YS.
+
+pred list-uniq i:list A, o:list A.
+pred list-uniq.seen i:A.
+list-uniq [] [].
+list-uniq [X|XS] YS :- list-uniq.seen X, !, list-uniq XS YS.
+list-uniq [X|XS] [X|YS] :- list-uniq.seen X => list-uniq XS YS.
+
+pred record-decl->id i:indt-decl, o:id.
+record-decl->id (parameter _ _ _ D) N :- pi p\ record-decl->id (D p) N.
+record-decl->id (record N _ _ _) N.

HB/common/utils.elpi

@@ -3,56 +3,10 @@
 
 
 % This file contains some HB specific utilities
+accumulate HB/common/utils-synterp.
 
 shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
-% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
-type attmap attribute-type.
-
-% runs P in a context where Coq #[attributes] are parsed
-pred with-attributes i:prop.
-with-attributes P :-
-  attributes A,
-
-% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2
-(pi S L AS Prefix R R1 Map PS\
-  parse-attributes.aux [attribute S (node L)|AS] Prefix R :-
-    if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !,
-    parse-attributes.aux AS Prefix R1,
-    (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map,
-    std.append R1 [get-option PS Map] R
-) =>
-
-  coq.parse-attributes A [
-    att "verbose" bool,
-    att "mathcomp" bool,
-    att "mathcomp.axiom" string,
-    att "short.type" string,
-    att "short.pack" string,
-    att "key" string,
-    att "arg_sort" bool,
-    att "log" bool,
-    att "log.raw" bool,
-    att "compress_coercions" bool,
-    att "export" bool,
-    att "skip" string,
-    att "local" bool,
-    att "fail" bool,
-    att "doc" string,
-    att "primitive" bool,
-    att "non_forgetful_inheritance" bool,
-    att "hnf" bool,
-  ] Opts, !,
-  Opts => (save-docstring, P).
-
-pred if-verbose i:prop.
-if-verbose P :- get-option "verbose" tt, !, P.
-if-verbose _.
-
-% header of if-verbose messages
-pred header o:string.
-header Msg :- Msg is "[" ^ {std.any->string {gettimeofday}} ^ "] HB: ".
-
 pred if-arg-sort i:prop.
 if-arg-sort P :- get-option "arg_sort" tt, !, P.
 if-arg-sort _.
@@ -78,12 +32,6 @@ pred acc-clauses i:scope, i:list prop.
 acc-clauses Scope CL :- coq.elpi.accumulate-clauses Scope "hb.db" {std.map CL (c\r\ r = clause _ _ c)}.
 */
 
-pred save-docstring.
-save-docstring :-
-  if (get-option "elpi.loc" Loc, get-option "doc" Txt)
-     (acc-clause _ (docstring Loc Txt))
-     true.
-
 % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?)
 % Should we make this an HO predicate, eg "located->gref S L is-factory? GR"
 % TODO: rename since this is HB specific and is expected to return a factory

HB/instance.elpi

@@ -35,7 +35,7 @@ declare-const Name BodySkel TyWPSkel CSL :- std.do! [
      if-verbose (coq.say  "HB: skipping section opening"),
      SectionBody = Body
    ) (
-    SectionName is "hb_instance_" ^ {std.any->string {new_int}},
+    std.assert! (coq.next-synterp-action (begin-section SectionName)) "synterp code did not open section",
     log.coq.env.begin-section SectionName,
     private.postulate-arity TyWP [] Body SectionBody SectionTy
   ),

HB/lock.elpi

@@ -170,7 +170,7 @@ declare Module BSkel Sort :- std.do! [
 
   if-verbose (coq.say {header} "operations meta-data module: ElpiOperations"),
 
-  ElpiOperationModName is "ElpiOperations" ^ {std.any->string {new_int}},
+  ElpiOperationModName is {calc (Module ^ "ElpiOperations")},
   log.coq.env.begin-module ElpiOperationModName none,
   acc-clauses current {std.append EX MixinFirstClass},
   log.coq.env.end-module-name ElpiOperationModName ElpiOperations,

HB/structure.elpi

@@ -269,7 +269,7 @@ rewrite new_concept.unlock.
 Time Fail reflexivity. (* takes 7s, the original body is restored *)
 Abort.
 
-Print Module Type new_conceptLocked.
+Print Module Type new_concept_Locked.
 Print Module new_concept.
 (*
    Module Type new_conceptLocked = Sig