port to elpi 3.0

.gitignore

@@ -58,3 +58,4 @@ _minted-*
 *.vtc
 
 *.dot
+config.stamp

HB/about.elpi

@@ -3,14 +3,14 @@
 
 namespace about {
 
-pred main i:string.
+func main string ->.
 main S :-
   coq.locate-all S All,
-  std.filter All (x\sigma gr a\x = loc-gref gr ; x = loc-abbreviation a) L,
+  std.filter All (x\sigma gr a\ std.once (x = loc-gref gr ; x = loc-abbreviation a)) L,
   if (L = []) (coq.error "HB: unable to locate" S) true,
   std.forall L (about.main-located S).
 
-pred main-located i:string, i:located.
+func main-located string, located ->.
 main-located S (loc-gref GR) :- class-def (class Class GR MLwP), !,
   private.main-structure S Class GR MLwP.
 
@@ -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 _,
@@ -61,23 +61,23 @@ main-located S (loc-abbreviation _) :- coq.error "HB: unknown abbreviation" S.
 
 shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }.
 
-pred bulletize1 i:(A -> coq.pp -> prop), i:A, o:coq.pp.
+func bulletize1 (func A -> coq.pp), A -> coq.pp.
 bulletize1 F X (glue [str "- ", M]) :- F X M.
 
-pred bulletize i:list A, i:(A -> coq.pp -> prop), o:coq.pp.
-bulletize [] _ empty.
+func bulletize list A, (func A -> coq.pp) -> coq.pp.
+bulletize [] _ empty :- !.
 bulletize L F (glue [brk 0 0 | PLB]) :-
   std.map L (bulletize1 F) PL,
   std.intersperse (brk 0 0) PL PLB.
 
 % Print shortest qualified identifier of the module containing a gref
-pred pp-module i:gref, o:coq.pp.
+func pp-module gref -> coq.pp.
 pp-module GR (str ID) :- gref->modname_short GR "." ID.
 
-pred unif-hint? i:cs-instance.
+func unif-hint? cs-instance -> .
 unif-hint? (cs-instance _ (cs-gref GR) _) :- coq.CS.db-for GR _ [_|_].
 
-pred not1 i:(A -> prop), i:A.
+func not1 (pred i:A), A.
 not1 P X :- not (P X).
 
 
@@ -89,12 +89,12 @@ namespace private {
 
 shorten coq.pp.{ v , h, hv, hov , spc , str , box , glue , brk , empty }.
 
-pred docstring-for-file i:string, o:prop.
+func docstring-for-file string -> prop.
 docstring-for-file Rex (docstring Loc Doc) :- docstring Loc Doc,
   loc.fields Loc File _ _ _ _,
-  rex.match {calc(".*" ^ Rex)} File.
+  rex.match {calc(".*" ^ Rex)} File, !.
 
-pred main-canonical-value i:string, i:list cs-instance.
+func main-canonical-value string, list cs-instance ->.
 main-canonical-value S CanonicalValues :-
   group-by-loc CanonicalValues CanonicalValuesL,
   %format
@@ -105,29 +105,29 @@ main-canonical-value S CanonicalValues :-
   coq.say {coq.pp->string PpCanonicalValues},
   coq.say.
 
-pred group-by-loc i:list cs-instance, o:list (pair (option loc) (list cs-instance)).
+func group-by-loc list cs-instance -> list (pair (option loc) (list cs-instance)).
 group-by-loc [] [].
 group-by-loc [cs-instance P V GR|L] [pr (some Loc) [cs-instance P V GR|SameLoc]|Rest1] :- decl-location GR Loc, !,
   std.partition L (x\ sigma GR1\ x = cs-instance _ _ GR1, decl-location GR1 Loc) SameLoc Rest,
   group-by-loc Rest Rest1.
 group-by-loc [I|Rest] [pr none [I]|Rest1] :- group-by-loc Rest Rest1.
 
-pred pp-canonical-solution-list i:pair (option loc) (list cs-instance), o:coq.pp.
+func pp-canonical-solution-list pair (option loc) (list cs-instance) -> coq.pp.
 pp-canonical-solution-list (pr none [CS]) Pp :-
   pp-canonical-solution CS Pp.
 pp-canonical-solution-list (pr (some Loc) L) Pp :-
   Pp = box (v 0)
     { std.append {std.intersperse spc {std.map L pp-canonical-solution}}
                  [ spc, {pp-loc Loc} ] }.
 
-pred pp-canonical-solution i:cs-instance, o:coq.pp.
+func pp-canonical-solution cs-instance -> coq.pp.
 pp-canonical-solution (cs-instance _Proj _Pat GR) Pp :-
   coq.env.typeof GR T,
   coq.prod-tgt->gref T F,
   if (class-def (class _ F _)) (gref->modname_short F "." ID) (coq.gref->string F ID),
   Pp = box (hov 0) [ str ID ].
 
-pred main-canonical-projection i:string, i:gref, i:list cs-instance.
+func main-canonical-projection string, gref, list cs-instance.
 main-canonical-projection S Proj CanonicalProjectionValues :-
   %format
   PpCanonicalProjectionOrigin = box (hov 4) [
@@ -141,12 +141,12 @@ main-canonical-projection S Proj CanonicalProjectionValues :-
   coq.say {coq.pp->string PpCanonicalProjectionValues},
   coq.say.
 
-pred pp-canonical-value i:cs-instance, o:coq.pp.
+func pp-canonical-value cs-instance -> coq.pp.
 pp-canonical-value (cs-instance _Proj (cs-gref GR) _Sol) Pp :-
   coq.term->pp (global GR) V,
   Pp = box (hov 2) [ V , spc, {pp-loc-of GR} ].
 
-pred main-coercion i:string, i:list coercion.
+func main-coercion string, list coercion.
 main-coercion S [coercion GR _ Src Tgt|_] :-
   % format
   if (class-def (class _ Src _) ; class-def (class Src _ _))
@@ -166,11 +166,11 @@ main-coercion S [coercion GR _ Src Tgt|_] :-
   coq.say {coq.pp->string PpCoercionOrigin},
   coq.say.
 
-pred main-operation i:string, i:mixinname, i:constant.
+func main-operation string, mixinname, constant -> .
 main-operation S MixinSource _ :-
   % fetch
-  mixin-first-class MixinSource Class,
-  class-def (class Class Structure _),
+  mixin->first-class MixinSource Class,
+  class-def (class Class Structure _), !,
   % format
   PpOriginStructure = box (hov 4) [
     str "HB:", spc, str S, spc, str "is an operation of structure", spc,
@@ -183,12 +183,12 @@ main-operation S MixinSource _ :-
   coq.say {coq.pp->string PpOriginMixin},
   coq.say.
 
-pred main-structure i:string, i:classname, i:structure, i:mixins.
+func main-structure string, classname, structure, mixins.
 main-structure S Class Structure MLwP :-
   % fetch
   list-w-params_list MLwP ML,
   std.map-filter ML (m\r\ sigma P O OPS\
-    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,
@@ -206,7 +206,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) [
@@ -224,10 +224,10 @@ main-structure S Class Structure MLwP :-
   print-docstring Structure,
   coq.say.
 
-pred main-factory-constructor i:string, i:inductive, i:gref, i:gref.
-main-factory-constructor S F PhBuild Build :-
+func main-factory->constructor string, inductive, gref, gref.
+main-factory->constructor S F PhBuild Build :-
   % fetch
-  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,
@@ -263,14 +263,16 @@ main-factory-constructor S F PhBuild Build :-
   print-docstring Build,
   coq.say.
 
-pred compute-arg-type i:list-w-params mixinname, i:list constant, i:list term, o:list id, o:id, o:list id, o:list (pair id coq.pp).
+func compute-arg-type list-w-params mixinname, list constant, list term -> list id, id, list id, list (pair id coq.pp).
 compute-arg-type (w-params.cons ID Ty Rest) F Acc [ID|PN] TN FN [pr ID PPTy |Xs] :-
   coq.term->pp Ty PPTy,
   @pi-parameter ID Ty x\ compute-arg-type (Rest x) F [x|Acc] PN TN FN Xs.
 compute-arg-type (w-params.nil ID Ty Rest) F Acc [] ID FN [pr ID PPTy|Xs] :-
   coq.term->pp Ty PPTy,
   @pi-parameter ID Ty x\ compute-arg-type.fields F {std.length (Rest x)} {std.rev [x|Acc]} Xs FN.
-pred compute-arg-type.fields i:list constant, i:int, i:list term, o:list (pair id coq.pp), o:list id.
+
+:index(1)
+func compute-arg-type.fields list constant, int, list term -> list (pair id coq.pp), list id.
 compute-arg-type.fields [] _ _ [] [].
 compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op _ C OP, !,
   coq.env.typeof (const OP) Ty,
@@ -291,15 +293,15 @@ compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
   (@pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy),
   @pi-parameter ID TyArgsDepsRecord op\
   (pi L L1 X\
-    copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X) =>
+    copy (app[global(const OP)|L]) X :- std.drop ToDrop L L1, coq.mk-app op L1 X, !) =>
     compute-arg-type.fields Cs NDeps Args Xs FN.
 
-pred main-factory i:string, i:inductive.
+func main-factory string, inductive.
 main-factory S Factory :-
   % fetch
   coq.env.projections Factory Ps,
   std.map-filter Ps (x\r\ x = some r) Fields,
-  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,
@@ -324,16 +326,16 @@ main-factory S Factory :-
   print-docstring (indt Factory),
   coq.say.
 
-pred main-factory-alias i:string, i:constant.
+func main-factory-alias string, constant.
 main-factory-alias S _Const :-
   coq.say "HB: todo HB.about for factory alias" S.
 
-pred main-builder i:string, i:factoryname, i:mixinname.
+func main-builder string, factoryname, mixinname.
 main-builder _S From To :-
   coq.say "HB: todo HB.about for builder from"
     {gref->modname_short From "."} "to" {gref->modname_short To "."}.
 
-pred compute-field-info.aux i:list id, i:list implicit_kind, o:list coq.pp.
+func compute-field-info.aux list id, list implicit_kind -> list coq.pp.
 compute-field-info.aux [] _ [].
 compute-field-info.aux [Name|NS] [explicit|IS] [str Name|PS] :-
   compute-field-info.aux NS IS PS.
@@ -343,48 +345,50 @@ compute-field-info.aux [Name|NS] [maximal|IS] [glue[str"{",str Name,str"}"]|PS]
   compute-field-info.aux NS IS PS.
 compute-field-info.aux [Name|NS] [] [str Name|PS] :-
   compute-field-info.aux NS [] PS.
-pred compute-field-info i:list id, i:list implicit_kind, o:list coq.pp.
+
+func compute-field-info list id, list implicit_kind -> list coq.pp.
 compute-field-info Names Impls O :-
   compute-field-info.aux {std.rev Names} {std.rev Impls} Pp,
   std.intersperse spc {std.rev Pp} O.
 
-pred pp-const i:constant, o:coq.pp.
+func pp-const constant -> coq.pp.
 pp-const F (str ID) :- coq.gref->id (const F) ID.
 
-pred pp-arg-type i:pair id coq.pp, o:coq.pp.
+func pp-arg-type pair id coq.pp -> coq.pp.
 pp-arg-type (pr ID PPTy) (box (hov 2) [str ID, str" :", spc, PPTy]).
 
-pred pp-if-verbose o:coq.pp, i:(coq.pp -> prop).
+:functional
+pred pp-if-verbose o:coq.pp, i:(func -> coq.pp).
 pp-if-verbose V P :- get-option "verbose" tt, !, P V.
 pp-if-verbose empty _.
 
-pred pp-loc-of i:gref, o:coq.pp.
+func pp-loc-of gref -> coq.pp.
 pp-loc-of GR PP :- decl-location GR Loc, !, pp-loc Loc PP.
 pp-loc-of _ coq.pp.empty.
 
-pred pp-loc i:loc, o:coq.pp.
+func pp-loc loc -> coq.pp.
 pp-loc Loc (coq.pp.glue PP) :-
   loc.fields Loc File _ _ Line _,
   QFile is "\"" ^ File ^ "\", line " ^ {std.any->string Line},
   PP = [str "(from ", str QFile, str")"].
 
-pred docstring->pp i:string, o:coq.pp.
+func docstring->pp string -> coq.pp.
 docstring->pp Txt (glue Doc) :-
   rex.replace "\n" " " Txt PlainTxt,
   rex.split " " PlainTxt Words,
   std.filter Words (w\not (w = "")) NEWords,
   std.map NEWords (w\r\ r = str w) PpWords,
   std.intersperse spc PpWords Doc.
 
-pred docstring-of i:gref, o:option coq.pp.
+func docstring-of gref -> option coq.pp.
 docstring-of GR (some Doc) :- decl-location GR Loc, docstring Loc Txt, !, docstring->pp Txt Doc.
 docstring-of _ none.
 
-pred pp-docstring-of i:gref, o:coq.pp.
+func pp-docstring-of gref -> coq.pp.
 pp-docstring-of GR D :- docstring-of GR (some D), !.
 pp-docstring-of _ coq.pp.empty.
 
-pred print-docstring i:gref.
+func print-docstring gref ->.
 print-docstring GR :-
   if (docstring-of GR (some Doc))
      (coq.say {coq.pp->string (box (hov 5) [str"Doc: ",Doc])})