use -> for functions and remove once

Author: gares

HB/about.elpi

@@ -20,10 +20,10 @@ main-located _ (loc-gref Class) :- class-def (class Class GR MLwP), !,
   S is M ^ "." ^ St,
   private.main-structure S Class GR MLwP.
 
-main-located S (loc-gref (indt I)) :- factory-constructor (indt I) _, !,
+main-located S (loc-gref (indt I)) :- factory->constructor (indt I) _, !,
   private.main-factory S I.
 
-main-located S (loc-gref (const C)) :- factory-constructor (const C) _, !,
+main-located S (loc-gref (const C)) :- factory->constructor (const C) _, !,
   private.main-factory-alias S C.
 
 main-located S (loc-gref (const C)) :- exported-op M _ C, !,
@@ -32,8 +32,8 @@ main-located S (loc-gref (const C)) :- exported-op M _ C, !,
 main-located S (loc-gref GR) :- factory-alias->gref GR F ok, not (F = GR), !,
   main-located S (loc-gref F).
 
-main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory-constructor (indt F) GR, !,
-  private.main-factory-constructor S F PhB GR.
+main-located S (loc-abbreviation A) :- phant-abbrev GR PhB A, factory->constructor (indt F) GR, !,
+  private.main-factory->constructor S F PhB GR.
 
 main-located S (loc-abbreviation A) :-
   coq.notation.abbreviation-body A NArgs _,
@@ -170,7 +170,7 @@ main-coercion S [coercion GR _ Src Tgt|_] :-
 func main-operation string, mixinname, constant -> .
 main-operation S MixinSource _ :-
   % fetch
-  mixin-first-class MixinSource Class,
+  mixin->first-class MixinSource Class,
   class-def (class Class Structure _), !,
   % format
   PpOriginStructure = box (hov 4) [
@@ -189,7 +189,7 @@ main-structure S Class Structure MLwP :-
   % fetch
   list-w-params_list MLwP ML,
   std.map-filter ML (m\r\ sigma P O OPS\
-    std.once (mixin-first-class m Class),
+    mixin->first-class m Class,
     std.findall (exported-op m P O) OPS,
     std.map OPS (c\out\ sigma p\ c = exported-op m p out) r) OPLL,
   std.flatten OPLL Operations,
@@ -207,7 +207,7 @@ main-structure S Class Structure MLwP :-
   PpClass = box (v 4) [
     str "HB: ", {pp-module Class}, str " is a factory for the following mixins:",
     {bulletize ML (m\r\ sigma tmp\
-      if (mixin-first-class m Class)
+      if (mixin->first-class m Class)
          (pp-module m tmp, r = glue [tmp, str " (* new, not from inheritance *)"])
          (pp-module m r))}],
   PpSubClasses = box (v 4) [
@@ -225,10 +225,10 @@ main-structure S Class Structure MLwP :-
   print-docstring Structure,
   coq.say.
 
-func main-factory-constructor string, inductive, gref, gref.
-main-factory-constructor S F PhBuild Build :-
+func main-factory->constructor string, inductive, gref, gref.
+main-factory->constructor S F PhBuild Build :-
   % fetch
-  std.once(gref-deps Build DMLwP),
+  gref->deps Build DMLwP,
   list-w-params_list DMLwP DML,
   factory-provides (indt F) PMLwP,
   list-w-params_list PMLwP PML,
@@ -302,7 +302,7 @@ main-factory S Factory :-
   % fetch
   coq.env.projections Factory Ps,
   std.map-filter Ps (x\r\ x = some r) Fields,
-  std.once (gref-deps (indt Factory) DMLwP),
+  gref->deps (indt Factory) DMLwP,
   list-w-params_list DMLwP DML,
   factory-provides (indt Factory) PMLwP,
   list-w-params_list PMLwP PML,

HB/builders.elpi

@@ -143,7 +143,7 @@ postulate-factories ModName IDF CDecl :-
   context.declare.params-key FLwP ParamsSection FKey FLwA,
   std.assert! (FLwA = [triple GRF _ _])
     "HB: cannot declare builders for more than one factory at a time",
-  std.once(gref-deps GRF DepswPRaw),
+  gref->deps GRF DepswPRaw,
   context.declare.mixins FKey ParamsSection DepswPRaw _ _ _,
   std.map ParamsSection triple_2 FParams,
   postulate-factory-abbrev FKey FParams IDF GRF TheFactory,

HB/common/database.elpi

@@ -81,7 +81,7 @@ sub-class? (class C1 _ ML1P) (class C2 _ ML2P) :-
 func factory-provides factoryname -> mixins.
 factory-provides FactoryAlias MLwP :- std.do! [
   std.assert-ok! (factory-alias->gref FactoryAlias Factory) "HB",
-  gref-deps Factory RMLwP,
+  gref->deps Factory RMLwP,
   w-params.map RMLwP (factory-provides.base Factory) MLwP
 ].
 
@@ -112,7 +112,7 @@ extract-conclusion-params TheType (prod _ S T) R :- !,
   @pi-decl _ S x\ extract-conclusion-params TheType (T x) R.
 extract-conclusion-params TheType (app [global GR|Args]) R :- !, std.do! [
   std.assert-ok! (factory-alias->gref GR Factory) "HB",
-  factory-nparams Factory NP,
+  factory->nparams Factory NP,
   std.map Args (copy-pack-holes TheType TheType) NewArgs,
   std.take NP NewArgs R].
 extract-conclusion-params TheType T R :- whd1 T T1, !, extract-conclusion-params TheType T1 R.
@@ -165,7 +165,7 @@ undup-cs-patterns L R :- std.do! [
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
 toposort-mixins In Out :- std.do! [
   std.map In triple_1 ML,
-  std.map ML (m\r\sigma D D1\ gref-deps m D1, list-w-params_list D1 D, std.map D (d\r\r = pr d m) r) ES2,
+  std.map ML (m\r\sigma D D1\ gref->deps m D1, list-w-params_list D1 D, std.map D (d\r\r = pr d m) r) ES2,
   std.flatten ES2 ES,
   toposort-proj triple_1 ES In Out,
 ].
@@ -231,14 +231,14 @@ pred findall-mixin-src i:term, o:list mixinname.
 findall-mixin-src T ML :-
   std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.
 
-func findall-factory-constructor -> list prop.
-findall-factory-constructor L :-
-  std.map {std.findall (findall-factory-constructor.aux _)} findall-factory-constructor.make L.
-pred findall-factory-constructor.aux o:prop.
-findall-factory-constructor.aux (factory-constructor F C) :-
-  is-factory F, factory-constructor F C.
-func findall-factory-constructor.make prop -> prop.
-findall-factory-constructor.make (findall-factory-constructor.aux P) P.
+func findall-factory->constructor -> list prop.
+findall-factory->constructor L :-
+  std.map {std.findall (findall-factory->constructor.aux _)} findall-factory->constructor.make L.
+pred findall-factory->constructor.aux o:prop.
+findall-factory->constructor.aux (factory->constructor F C) :-
+  is-factory F, factory->constructor F C.
+func findall-factory->constructor.make prop -> prop.
+findall-factory->constructor.make (findall-factory->constructor.aux P) P.
 
 pred findall-local-canonical o:list constant.
 findall-local-canonical CL :-
@@ -441,14 +441,14 @@ has-CS-instance? TyTerm (indt Struct) :- std.do! [
 pred structure-nparams i:structure, o:int.
 structure-nparams Structure NParams :-
   class-def (class Class Structure _),
-  factory-nparams Class NParams.
+  factory->nparams Class NParams.
 
 pred factory? i:term, o:w-args factoryname.
 factory? S (triple F Params T) :-
   not (var S), !,
   safe-dest-app S (global GR) Args,
   factory-alias->gref GR F ok,
-  factory-nparams F NP, !,
+  factory->nparams F NP, !,
   std.split-at NP Args Params [T|_].
 
 % [find-max-classes Mixins Classes] states that Classes is a list of classes
@@ -460,7 +460,7 @@ factory? S (triple F Params T) :-
 pred find-max-classes i:list mixinname, o:list classname.
 find-max-classes [] [].
 find-max-classes [M|Mixins] [C|Classes] :-
-  mixin-first-class M C,
+  mixin->first-class M C,
   std.do! [
     class-def (class C _ MLwP),
     list-w-params_list MLwP ML,

HB/common/phant-abbreviation.elpi

@@ -37,7 +37,7 @@ add-abbreviation N (private.phant-term AL T1) C Abbrev :- std.do! [
 % and before the source keu to replace the target key by a user chosen one.
 pred of-gref i:bool, i:gref, i:list mixinname, o:phant-term.
 of-gref WithCopy GRF RealMixinArgs PhBody:- !, std.do! [
-  std.assert! (gref-deps GRF MLwP) "mk-phant-term: unknown gref",
+  std.assert! (gref->deps GRF MLwP) "mk-phant-term: unknown gref",
   std.assert! (coq.env.typeof GRF FTy) "mk-phant-term: F illtyped",
   coq.mk-eta (-1) FTy (global GRF) EtaF,
   % toposort-mixins ML MLSorted,
@@ -258,7 +258,7 @@ mk-phant-term.mixins Target Src CN PF Params N Ty MLwA Out :- std.do! [
 
 mk-phant-term.mixins.aux T Params C CN PF X :- std.do![
   get-constructor CN KC,
-  synthesis.infer-all-gref-deps Params T KC KCM,
+  synthesis.infer-all-gref->deps Params T KC KCM,
   fun-unify none KCM C PF X,
 ].
 

HB/common/stdpp.elpi

@@ -285,15 +285,6 @@ term->cs-pattern T (cs-gref GR) :- coq.term->gref T GR.
 term->cs-pattern T _ :- coq.error T "HB database: is not a valid canonical key".
 
 
-% this one is in utils, maybe cs-pattern->name is not stdpp material
-pred gref->modname-label i:gref, i:int, i:string, o:string.
-
-pred cs-pattern->name i:cs-pattern, o:string.
-cs-pattern->name cs-prod "prod".
-cs-pattern->name (cs-sort _) "sort".
-cs-pattern->name cs-default "default".
-cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
-
 % ---------------------------------------------------------------------
 % kit for closing a term by abstracting evars with lambdas
 % we use constraints to attach to holes a number

HB/common/synthesis.elpi

@@ -23,11 +23,11 @@ infer-all-these-mixin-args Ps T ML F SFX :- std.do! [
   private.instantiate-all-these-mixin-args FT T ML SFX,
 ].
 
-% [infer-all-gref-deps Ps T GR X] fills in all the arguments of GR
-% which are misxins in gref-deps GR, other arguments are abstracted
-pred infer-all-gref-deps i:list term, i:term, i:gref, o:term.
-infer-all-gref-deps Ps T GR X :- std.do! [
-  std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail",
+% [infer-all-gref->deps Ps T GR X] fills in all the arguments of GR
+% which are misxins in gref->deps GR, other arguments are abstracted
+pred infer-all-gref->deps i:list term, i:term, i:gref, o:term.
+infer-all-gref->deps Ps T GR X :- std.do! [
+  std.assert! (gref->deps GR MLwP) "BUG: gref->deps should never fail",
   list-w-params_list MLwP ML,
   coq.env.typeof GR Ty,
   coq.mk-eta (-1) Ty (global GR) EtaF,
@@ -52,7 +52,7 @@ infer-holes-depending-on-pack T (app [global GR | Args]) S :-
   ((coq.gref->id GR GRS, rex.match "phant.*" GRS /*TODO: phant-clone? GR N*/);
     pack? GR _),
   coq.env.typeof GR Ty, class-of-phant Ty KC SC C,
-  factory-nparams C N,
+  factory->nparams C N,
   std.take N Args Params, !,
   std.do! [
     infer-all-args-let Params T KC ClassInstance ok,
@@ -134,7 +134,7 @@ pred under-mixins.then i:list (w-args mixinname),
     i:(A -> prop), o:A.
 under-mixins.then [] _ Pred Body :- !, Pred Body.
 under-mixins.then [triple M Args T|ML] MkFun Pred Out :- std.do! [
-  infer-all-gref-deps Args T M MTy,
+  infer-all-gref->deps Args T M MTy,
   (@pi-decl `m` MTy m\ mixin-src T M m =>
     under-mixins.then ML MkFun Pred (Body m)),
   MkFun `m` MTy Body Out,
@@ -235,7 +235,7 @@ pred builder->term i:list term, i:term, i:factoryname, i:mixinname, o:term.
 builder->term Ps T Src Tgt B :- !, std.do! [
   from Src Tgt FGR,
   F = global FGR,
-  gref-deps Src MLwP,
+  gref->deps Src MLwP,
   list-w-params_list MLwP ML,
   infer-all-these-mixin-args Ps T ML F B,
 ].

HB/common/utils.elpi

@@ -69,15 +69,15 @@ nice-gref->string X Mod :-
 nice-gref->string X S :-
   coq.term->string (global X) S.
 
-pred gref->modname i:gref, i:int, i:string, o:string.
+func gref->modname gref, int, string -> string.
 gref->modname GR NComp Sep ModName :-
   coq.gref->path GR Path,
   std.rev Path Mods,
   std.length Path Len,
   if (Len >= NComp) true (coq.error "Not enough enclosing modules for" {coq.gref->string GR}),
   std.take NComp Mods L,
   std.string.concat Sep {std.rev L} ModName.
-pred gref->modname-label i:gref, i:int, i:string, o:string.
+func gref->modname-label gref, int, string -> string.
 gref->modname-label GR NComp Sep ModName :-
   coq.gref->path GR Path,
   std.rev Path PathRev,
@@ -86,15 +86,22 @@ gref->modname-label GR NComp Sep ModName :-
   std.take N PathRev L,
   std.string.concat Sep {std.rev [{coq.gref->id GR}|L]} ModName.
 
+pred cs-pattern->name i:cs-pattern, o:string.
+cs-pattern->name cs-prod "prod".
+cs-pattern->name (cs-sort _) "sort".
+cs-pattern->name cs-default "default".
+cs-pattern->name (cs-gref GR) Name :- gref->modname-label GR 1 "_" Name.
+
+
 func string->modpath string -> modpath.
 string->modpath S MP :-
   std.filter {coq.locate-all S} (l\l = loc-modpath _) L,
   L = [loc-modpath MP].
 
-pred gref->modname_short1 i:modpath, i:string, i:list string, o:string.
-gref->modname_short1 _ S [] S.
-gref->modname_short1 MP "" [X|L] L' :- gref->modname_short1 MP X L L'.
-gref->modname_short1 MP S _ S :- string->modpath S MP.
+func gref->modname_short1 modpath, string, list string -> string.
+gref->modname_short1 _ S [] S :- !.
+gref->modname_short1 MP "" [X|L] L' :- !, gref->modname_short1 MP X L L'.
+gref->modname_short1 MP S _ S :- !, string->modpath S MP.
 gref->modname_short1 MP S [X|L] S' :-
   gref->modname_short1 MP {std.string.concat "." [X,S]} L S'.
 

HB/context.elpi

@@ -63,7 +63,7 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
 
   if-verbose (coq.say "HB: postulate" Name "on" {coq.term->string T}),
 
-  synthesis.infer-all-gref-deps Ps T M TySkel,
+  synthesis.infer-all-gref->deps Ps T M TySkel,
   % was synthesis.infer-all-mixin-args Ps T M TySkel,
   % if-verbose (coq.say "HB: postulate-mixin checking" TySkel),
   % std.assert-ok! (coq.typecheck Ty _) "postulate-mixin: Ty illtyped",

HB/factory.elpi

@@ -193,13 +193,13 @@ 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! [
-  gref-deps GR GRD,
+  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,
 ].
 declare-id-builder.aux GR Params TheType (fun `x` Ty x\x) :-
-  synthesis.infer-all-gref-deps Params TheType GR Ty.
+  synthesis.infer-all-gref->deps Params TheType GR Ty.
 
 % [mk-factory-abbrev Str GR CL FactAbbrev]
 % creates an abbreviation for GR names Str and creates a phant-abbrev clause in CL.
@@ -275,7 +275,7 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   factories-provide GRFSwP MLwP,
   w-params.nparams MLwP NParams,
   build-deps-for-projections R MLwP GRDepsClausesProjs,
-  GRDepsClauses = [gref-deps (indt R) MLwP, gref-deps (indc K) MLwP|GRDepsClausesProjs],
+  GRDepsClauses = [gref->deps (indt R) MLwP, gref->deps (indc K) MLwP|GRDepsClausesProjs],
 
   % GRDepsClauses => mk-factory-sort MLwP (indt R) _ FactorySortCoe,
   % FactorySortCoe = coercion GRFSort _ _ _,
@@ -300,11 +300,11 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   log.coq.env.begin-module "Exports" none,
   std.flatten [Clauses, GRDepsClauses, [
     is-factory (indt R),
-    factory-constructor (indt R) GRK,
-    factory-nparams (indt R) NParams,
+    factory->constructor (indt R) GRK,
+    factory->nparams (indt R) NParams,
     factory-builder-nparams BuildConst NParams,
     phant-abbrev GRK (const BuildConst) BuildAbbrev,
-    % gref-deps GRFSort MLwP,
+    % gref->deps GRFSort MLwP,
     % factory-sort FactorySortCoe,
   ]] NewClauses,
   acc-clauses current NewClauses,
@@ -339,9 +339,9 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
 
   std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory",
   std.assert-ok! (factory-alias->gref PhF F) "HB",
-  std.assert! (factory-constructor F FK) "BUG: Factory constructor missing",
+  std.assert! (factory->constructor F FK) "BUG: Factory constructor missing",
 
-  MixinSrcClauses => synthesis.infer-all-gref-deps TheParams TheType FK MFK,
+  MixinSrcClauses => synthesis.infer-all-gref->deps TheParams TheType FK MFK,
   std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed",
   (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) => copy MFKTy MFKTyC,
 
@@ -355,14 +355,14 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   @global! => log.coq.arguments.set-implicit GRK [[]],
 
   factories-provide GRFSwP MLwP,
-  GRDepsClauses = [gref-deps (const C) MLwP, gref-deps (const CK) MLwP],
+  GRDepsClauses = [gref->deps (const C) MLwP, gref->deps (const CK) MLwP],
 
   GRDepsClauses => phant.of-gref ff GRK [] PhGRK0,
 
   % GRDepsClauses => mk-factory-sort MLwP (const C) _ FactorySortCoe,
   % FactorySortCoe = coercion GRFSort _ _ _,
 
-  if (mixin-first-class F _) (PhGRK = PhGRK0)
+  if (mixin->first-class F _) (PhGRK = PhGRK0)
     (phant.append-fun-unify PhGRK0 PhGRK),
   GRDepsClauses => phant.add-abbreviation "Build" PhGRK BuildConst _,
 
@@ -375,10 +375,10 @@ declare-factory-alias MixinSrcClauses SectionCanonicalInstance
   w-params.nparams MLwP NParams,
   std.flatten [ Clauses, GRDepsClauses,
       [ is-factory (const C),
-        factory-nparams (const C) NParams,
-        factory-constructor (const C) GRK,
+        factory->nparams (const C) NParams,
+        factory->constructor (const C) GRK,
         factory-builder-nparams BuildConst NParams,
-        % gref-deps GRFSort MLwP,
+        % gref->deps GRFSort MLwP,
         % factory-sort FactorySortCoe
       ]
     ] NewClauses,
@@ -403,7 +403,7 @@ pred build-deps-for-projections i:inductive, i:mixins, o:list prop.
 build-deps-for-projections R MLwP CL :- std.do! [
   compat.map-filter {coq.env.projections R} (x\y\x = some y) MixinOps,
   list-w-params.rcons MLwP (pl\t\r\ r = triple (indt R) pl t) MLRwP,
-  std.map MixinOps (gr\r\ r = gref-deps (const gr) MLRwP) CL,
+  std.map MixinOps (gr\r\ r = gref->deps (const gr) MLRwP) CL,
 ].
 
 % Section handling in Coq is smart, in the sense it it only abstracts over
@@ -433,7 +433,7 @@ mk-factory-sort MLwP GR (const FactorySortCst) Coe :-
   synthesis.infer-coercion-tgt MLwP CoeClass,
   Coe = coercion (const FactorySortCst) MLwPLength GR CoeClass.
 pred mk-factory-sort.term i:gref, i:list term, i:term, o:term.
-mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref-deps P T GR Ty.
+mk-factory-sort.term GR P T (fun `_` Ty _\ T) :- synthesis.infer-all-gref->deps P T GR Ty.