port to elpi 2.0

math-comp · Nov 20, 2024 · 9b19687 · 9b19687
1 parent cbc149f
commit 9b19687
Show file tree

Hide file tree

Showing 7 changed files with 19 additions and 36 deletions.
diff --git a/HB/common/database.elpi b/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![

diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi
@@ -5,17 +5,17 @@
 % 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.
+% 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.
 
 namespace std {
 
@@ -42,7 +42,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.

diff --git a/HB/common/utils.elpi b/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) :-

diff --git a/HB/instance.elpi b/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,

diff --git a/HB/structure.elpi b/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! [

diff --git a/HB/structures.v b/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.
 
@@ -272,7 +272,6 @@ main [str S] :- !,
 
 main _ :- coq.error "Usage: HB.locate <name>.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.locate.
 
 
@@ -305,7 +304,6 @@ main [str S] :- !, with-attributes (with-logging (about.main S)).
 
 main _ :- coq.error "Usage: HB.about <name>.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.about.
 
 
@@ -353,7 +351,6 @@ main _ :-
   coq.error
     "Usage: HB.howto [(<type>)|<structure>] <structure> [<search depth>].".
 }}.
-Elpi Typecheck.
 Elpi Export HB.howto.
 
 
@@ -380,7 +377,6 @@ main [] :- !, status.print-hierarchy.
 
 main _ :- coq.error "Usage: HB.status.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.status.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -410,7 +406,6 @@ main [str File] :- with-attributes (with-logging (graph.to-file File)).
 main _ :- coq.error "Usage: HB.graph <filename>.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.graph.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -486,7 +481,6 @@ main [indt-decl D] :- record-decl->id D N, with-attributes (actions N).
 main _ :-
   coq.error "Usage: HB.mixin Record <MixinName> T of F A & … := { … }.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.mixin.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -545,7 +539,6 @@ solve (goal _ _ S _ [trm Ty | Args] as G) GLS :- with-attributes (with-logging (
 ])).
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.pack_for.
 
 Elpi Tactic HB.pack.
@@ -568,7 +561,6 @@ solve (goal _ _ Ty _ Args as G) GLS :- with-attributes (with-logging (std.do! [
 ])).
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.pack.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -689,7 +681,6 @@ main [const-decl N _ _] :- !, with-attributes (actions N).
 
 main _ :- coq.error "Usage: HB.structure Definition <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
 }}.
-Elpi Typecheck.
 Elpi Export HB.structure.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -728,7 +719,6 @@ main [str K] :- !, coq.locate K GR, with-attributes (with-logging (instance.satu
 main [trm T] :- !, term->cs-pattern T P, with-attributes (with-logging (instance.saturate-instances P)).
 main _ :- coq.error "Usage: HB.saturate [key]".
 }}.
-Elpi Typecheck.
 Elpi Export HB.saturate.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -790,7 +780,6 @@ main [_, _] :- !.
 
 main _ :- coq.error "Usage: HB.instance Definition <Name> := <Builder> T ...".
 }}.
-Elpi Typecheck.
 Elpi Export HB.instance.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -843,7 +832,6 @@ main [const-decl N _ _] :- with-attributes (actions N).
 main _ :-
   coq.error "Usage: HB.factory Record <FactoryName> T of F A & … := { … }.\nUsage: HB.factory Definition <FactoryName> T of F A := t.".
 }}.
-Elpi Typecheck.
 Elpi Export HB.factory.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -919,7 +907,6 @@ main [ctx-decl _] :- !, with-attributes (actions {calc ("Builders_" ^ {std.any->
 
 main _ :- coq.error "Usage: HB.builders Context A (f : F1 A).".
 }}.
-Elpi Typecheck.
 Elpi Export HB.builders.
 
 
@@ -962,7 +949,6 @@ main [] :- !, with-attributes actions.
 main _ :- coq.error "Usage: HB.end.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.end.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1030,7 +1016,6 @@ main [str M] :- !, with-attributes (actions {coq.locate-all M}).
 main _ :- coq.error "Usage: HB.export M.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.export.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1084,7 +1069,6 @@ main [str M] :- !, with-attributes (actions (some M)).
 main _ :- coq.error "Usage: HB.reexport.".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.reexport.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1151,7 +1135,6 @@ main [Ctx] :- Ctx = ctx-decl _, !,
 main _ :- coq.error "Usage: HB.declare Context <Parameters> <Key> <Factories>".
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.declare.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
@@ -1191,7 +1174,6 @@ check-or-not Skel :-
              (coq.say "HB.check:" {coq.term->string T} ":" {coq.term->string Ty}))).
 
 }}.
-Elpi Typecheck.
 Elpi Export HB.check.
 
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)

diff --git a/Makefile.test-suite.coq.local b/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