port to elpi 2.0

HB/about.elpi

@@ -276,7 +276,7 @@ compute-arg-type.fields [C|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :- exported-op
   coq.env.typeof (const OP) Ty,
   coq.gref->id (const OP) ID,
   coq.subst-prod Args Ty TyArgs,
-  @pplevel! 200 => coq.term->pp TyArgs PPTy,
+  (@pplevel! 200 => coq.term->pp TyArgs PPTy),
   compute-arg-type.fields Cs NDeps Args Xs FN.
 compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
   % factories don't get exported ops, so we hack their types :-/
@@ -288,7 +288,7 @@ compute-arg-type.fields [OP|Cs] NDeps Args [pr ID PPTy|Xs] [ID|FN] :-
   coq.subst-prod Deps TyArgs TyArgsDeps,
   coq.subst-prod [_] TyArgsDeps TyArgsDepsRecord,
   ToDrop is NDeps + 2,
-  @pplevel! 200 => coq.term->pp TyArgsDepsRecord PPTy,
+  (@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) =>

HB/builders.elpi

@@ -76,7 +76,7 @@ namespace builders.private {
 % declares all the new builders F to M via B.
 % From holds the (from F Mi Bi) new clauses during folding.
 pred declare-1-builder i:builder, i:list prop, o:list prop.
-declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- FromClauses => from SrcFactory TgtMixin _, !,
+declare-1-builder (builder _ SrcFactory TgtMixin _) FromClauses FromClauses :- (FromClauses => from SrcFactory TgtMixin _), !,
   if-verbose (coq.say {header} "skipping duplicate builder from"
     {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}).
 declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin B|FromClauses] :-

HB/common/database.elpi

@@ -167,10 +167,10 @@ toposort-mixins In Out :- std.do! [
   toposort-proj triple_1 ES In Out,
 ].
 
-pred toposort-proj i:(A -> B -> prop), i:list (pair B B), i:list A, o:list A.
+pred toposort-proj i:(A -> gref -> prop), i:list (pair gref gref), i:list A, o:list A.
 toposort-proj Proj ES In Out :- !, toposort-proj.acc Proj ES [] In Out.
 pred topo-find i:B, o:A.
-pred toposort-proj.acc i:(A -> B -> prop), i:list (pair B B), i:list B, i:list A, o:list A.
+pred toposort-proj.acc i:(A -> gref -> prop), i:list (pair gref gref), i:list gref, i:list A, o:list A.
 toposort-proj.acc _ ES Acc [] Out :- !,
   std.map {std.gref.toposort ES Acc} topo-find Out.
 toposort-proj.acc Proj ES Acc [A|In] Out :- std.do![

HB/common/log.elpi

@@ -265,15 +265,15 @@ with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.l
   std.string.concat "\n" ["","HIERARCHY BUILDER PATCH v1",LocStr,""] PATCH1,
   output OC1 PATCH1,
   close_out OC1,
-  log.private.logger L NICE => P,
+  (log.private.logger L NICE => P),
   log.private.logger-close L,
   std.intersperse coq.pp.spc L PP,
   coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S,
   open_append FILENAME OC2,
   output OC2 S,
   close_out OC2.
 with-logging P :- (get-option "log" tt, NICE = tt ; get-option "log.raw" tt, NICE = ff), !,
-  log.private.logger L NICE => P,
+  (log.private.logger L NICE => P),
   log.private.logger-close L,
   std.intersperse coq.pp.spc L PP,
   coq.pp->string (coq.pp.box (coq.pp.v 0) PP) S,
@@ -371,7 +371,7 @@ coq.vernac->pp1 (vernac.implicit Local Name [L]) (box h [Locality, str "Argument
 coq.vernac->pp1 (comment A) (box (hov 2) [str"(*", str S, str"*)"]) :-
   std.any->string A S.
 coq.vernac->pp1 (check T Fail) (box (hov 2) [Failure, str"Check", spc, PPT, str"."]) :-
-  @holes! => coq.term->pp T PPT,
+  (@holes! => coq.term->pp T PPT),
   fail->failure Fail Failure.
 coq.vernac->pp1 (strategy L opaque) (box (hov 2) [str"Strategy opaque [", glue PPL , str"]."]) :-
   std.map L (c\r\sigma id\coq.gref->id (const c) id, r = str id) LID, std.intersperse spc LID PPL.

HB/common/stdpp.elpi

@@ -5,17 +5,19 @@
 % This file contains additions to elpi or coq-elpi standard library
 
 
-kind triple type -> type -> type -> type.
-type triple A -> B -> C -> triple A B C.
+% elpi:if version < 2.0.0
+  kind triple type -> type -> type -> type.
+  type triple A -> B -> C -> triple A B C.
 
-pred triple_1 i:triple A B C, o:A.
-triple_1 (triple A _ _) A.
+  pred triple_1 i:triple A B C, o:A.
+  triple_1 (triple A _ _) A.
 
-pred triple_2 i:triple A B C, o:B.
-triple_2 (triple _ B _) B.
+  pred triple_2 i:triple A B C, o:B.
+  triple_2 (triple _ B _) B.
 
-pred triple_3 i:triple A B C, o:C.
-triple_3 (triple _ _ C) C.
+  pred triple_3 i:triple A B C, o:C.
+  triple_3 (triple _ _ C) C.
+% elpi:endif
 
 namespace std {
 
@@ -42,7 +44,7 @@ partition [] _ [] [].
 partition [X|XS] P [X|YS] ZS :- P X, !, partition XS P YS ZS.
 partition [X|XS] P YS [X|ZS] :- partition XS P YS ZS.
 
-pred under.do! i:((A -> Prop) -> A -> prop), i:list prop.
+pred under.do! i:((A -> prop) -> A -> prop), i:list prop.
 under.do! Then LP :- Then (_\ std.do! LP) _.
 
 pred map-triple i:(A -> A1 -> prop), i:(B -> B1 -> prop), i:(C -> C1 -> prop), i:triple A B C, o:triple A1 B1 C1.
@@ -286,6 +288,10 @@ term->cs-pattern (sort U) (cs-sort U).
 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
+type gref->modname-label gref -> int -> string -> string -> prop.
+
 pred cs-pattern->name i:cs-pattern, o:string.
 cs-pattern->name cs-prod "prod".
 cs-pattern->name (cs-sort _) "sort".

HB/common/utils.elpi

@@ -124,11 +124,11 @@ pred mk0 i:A, o:A.
 mk0 F R :- constant R F [].
 pred mk1 i:(A -> B), i:A, o:B.
 mk1 F X1 R :- constant R F [X1].
-pred mk2 i:(A -> B -> C), i:A, i:B, o:C.
+pred mk2 i:(A -> A -> C), i:A, i:A, o:C.
 mk2 F X1 X2 R :- constant R F [X1, X2].
-pred mk3 i:(A -> B -> C -> D), i:A, i:B, i:C, o:D.
+pred mk3 i:(A -> A -> A -> D), i:A, i:A, i:A, o:D.
 mk3 F X1 X2 X3 R :- constant R F [X1, X2, X3].
-pred mk4 i:(A -> B -> C -> D -> E), i:A, i:B, i:C, i:D, o:E.
+pred mk4 i:(A -> A -> A -> A -> E), i:A, i:A, i:A, i:A, o:E.
 mk4 F X1 X2 X3 X4 R :- constant R F [X1, X2, X3,X4].
 
 pred mk-fun i:name, i:term, i:(term -> term), o:term.
@@ -233,6 +233,7 @@ list-w-params.append (w-params.cons N Ty ML1) (w-params.cons N Ty ML2) (w-params
 
 pred list-w-params.rcons i:list-w-params A, i:(list term -> term -> w-args A -> prop), o:list-w-params A.
 list-w-params.rcons LwP F R :- list-w-params.rcons.aux LwP F [] R.
+pred list-w-params.rcons.aux i:list-w-params A, i:(list term -> term -> w-args A -> prop), i:list term, o:list-w-params A.
 list-w-params.rcons.aux (w-params.nil N T ML1) F Acc (w-params.nil N T ML2) :-
   pi x\ sigma Last\ F {std.rev Acc} x Last, std.append (ML1 x) [Last] (ML2 x).
 list-w-params.rcons.aux (w-params.cons N Ty ML1) F Acc (w-params.cons N Ty ML2) :-

HB/factory.elpi

@@ -263,8 +263,8 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
   if-verbose (coq.say {header} "declare notation axioms"),
 
   if (D = asset-mixin)
-     (GRDepsClauses => mk-factory-abbrev "axioms" (indt R) FRClauses FactAbbrev,
-      GRDepsClauses => FRClauses => declare-id-builder (indt R) IdBuilderClause,
+     ((GRDepsClauses => mk-factory-abbrev "axioms" (indt R) FRClauses FactAbbrev),
+      (GRDepsClauses => FRClauses => declare-id-builder (indt R) IdBuilderClause),
       Clauses = [IdBuilderClause|FRClauses])
      (GRDepsClauses => mk-factory-abbrev "axioms" (indt R) Clauses FactAbbrev),
 
@@ -404,7 +404,7 @@ mk-factory-sort MLwP GR (const FactorySortCst) Coe :-
   log.coq.env.add-const-noimplicits "sort" FactorySort FactorySortTy ff FactorySortCst,
   synthesis.mixins-w-params.length MLwP MLwPLength,
   std.nlist {calc (MLwPLength + 1)} implicit MLwPImplicits,
-  @global! => log.coq.arguments.set-implicit (const FactorySortCst) [MLwPImplicits],
+  (@global! => log.coq.arguments.set-implicit (const FactorySortCst) [MLwPImplicits]),
   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.

HB/instance.elpi

@@ -201,6 +201,8 @@ declare-factory-sort-factory GR :- std.do! [
   std.forall CSL (x\ sigma CS\ x = pr _ CS, log.coq.CS.declare-instance CS)
 ].
 
+pred context.declare i:factories, o:mixins, o:list term, o:term, o:list prop, o:list constant.
+
 pred mk-factory-sort-deps i:gref, o:list (pair id constant).
 mk-factory-sort-deps AliasGR CSL :- std.do! [
   factory-alias->gref AliasGR GR,

HB/structure.elpi

@@ -6,7 +6,6 @@ namespace structure {
 % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }
 %  cons p1\ cons p2\ nil t\ [triple f1 [p1] t,triple f2 [p1, {{p1 * p2}}] t]
 pred declare i:string, i:term, i:sort.
-pred declare i:string, i:term, i:universe.
 declare Module BSkel Sort :- std.do! [
   disable-id-phant BSkel BSkelNoId,
   std.assert-ok! (coq.elaborate-skeleton BSkelNoId _ BNoId) "illtyped structure definition",
@@ -442,7 +441,6 @@ synthesize-fields.body _Params T ML (record "axioms_" {{ Type }} "Class" FS) :-
   synthesize-fields T ML FS.
 
 pred mk-record+sort-field i:sort, i:name, i:term, i:(term -> record-decl), o:indt-decl.
-pred mk-record+sort-field i:universe, i:name, i:term, i:(term -> record-decl), o:indt-decl.
 mk-record+sort-field Sort _ T F (record "type" (sort Sort) "Pack" (field _ "sort" T F)).
 
 pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl.
@@ -451,7 +449,6 @@ mk-class-field ClassName Params T _ (field [canonical ff] "class" (app [global C
 
 % Builds the axioms record and the factories from this class to each mixin
 pred declare-class+structure i:mixins, i:sort, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
-pred declare-class+structure i:mixins, i:universe, o:factoryname, o:structure, o:term, o:term, o:list prop, o:prop.
 declare-class+structure MLwP Sort
     (indt ClassInd) (indt StructureInd) SortProjection ClassProjection AllFactories
     (structure-key SortP ClassP (indt StructureInd)):- std.do! [

HB/structures.v

@@ -66,7 +66,7 @@ typeabbrev structure   gref.
 
 typeabbrev (w-args A) (triple A (list term) term).
 
-kind w-params type -> type -> type.
+kind w-params type -> type.
 type w-params.cons id -> term -> (term -> w-params A) -> w-params A.
 type w-params.nil id -> term -> (term -> A) -> w-params A.
 
@@ -292,10 +292,10 @@ Elpi Export HB.locate.
 #[arguments(raw)] Elpi Command HB.about.
 Elpi Accumulate Db hb.db.
 Elpi Accumulate File "HB/common/stdpp.elpi".
+Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
 #[only="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_816.elpi".
-Elpi Accumulate File "HB/common/utils.elpi".
 Elpi Accumulate File "HB/common/log.elpi".
 Elpi Accumulate File "HB/about.elpi".
 Elpi Accumulate lp:{{

Makefile.test-suite.coq.local

@@ -12,6 +12,7 @@ DIFF=\
 	$(COQTOP) $(COQFLAGS) $(COQLIBS) -topfile $(1) \
 	  < $(1) 2>/dev/null \
 	  | grep -v -e "Skipping rcfile" -e "is declared" -e "is defined" -e "Loading ML file" -e "Welcome to Coq" \
+	  | sed 's/characters \([0-9]\+\)-[0-9]\+/character \1/' \
 	  > $(1).out.aux;\
 	diff -u --strip-trailing-cr $(call output_for,$(1)) $(1).out.aux;\
 	fi

_CoqProject

@@ -1,6 +1,7 @@
 HB/structures.v
 -arg -w -arg -elpi.accumulate-syntax
 -arg -w -arg +elpi.typecheck
+-arg -w -arg -elpi.typecheck-syntax
 -Q HB HB
 
 -R tests HB.tests