From 54bdd706d3b2843bd20f47478f7400652c38f1d9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 20 Nov 2024 15:58:54 +0100 Subject: [PATCH] port to elpi 2.0 --- HB/about.elpi | 4 ++-- HB/builders.elpi | 2 +- HB/common/database.elpi | 4 ++-- HB/common/log.elpi | 6 +++--- HB/common/stdpp.elpi | 24 +++++++++++++++--------- HB/common/utils.elpi | 7 ++++--- HB/factory.elpi | 6 +++--- HB/instance.elpi | 2 ++ HB/structure.elpi | 3 --- HB/structures.v | 4 ++-- Makefile.test-suite.coq.local | 1 + _CoqProject | 1 + 12 files changed, 36 insertions(+), 28 deletions(-) diff --git a/HB/about.elpi b/HB/about.elpi index d39dc4585..971b99967 100644 --- a/HB/about.elpi +++ b/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) => diff --git a/HB/builders.elpi b/HB/builders.elpi index 37493db36..81aad47ac 100644 --- a/HB/builders.elpi +++ b/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] :- diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 2b0268daa..39fd0274c 100644 --- 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/log.elpi b/HB/common/log.elpi index 5e86d403b..358e48367 100644 --- a/HB/common/log.elpi +++ b/HB/common/log.elpi @@ -265,7 +265,7 @@ 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, @@ -273,7 +273,7 @@ with-logging P :- (get-option "elpi.hb.log" _, NICE = tt ; get-option "elpi.hb.l 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. diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 50655adfd..a094435f8 100644 --- a/HB/common/stdpp.elpi +++ b/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". diff --git a/HB/common/utils.elpi b/HB/common/utils.elpi index 137edc393..ae4216b66 100644 --- 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/factory.elpi b/HB/factory.elpi index 8ff726654..690adc4ea 100644 --- a/HB/factory.elpi +++ b/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. diff --git a/HB/instance.elpi b/HB/instance.elpi index 1410106b1..4dd1ccc1f 100644 --- 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 index be549496a..097cd6e36 100644 --- 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 index 8b2bf7b5e..5eca9d8d4 100644 --- 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. @@ -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:{{ diff --git a/Makefile.test-suite.coq.local b/Makefile.test-suite.coq.local index 2b1a6ac59..b69480aa0 100644 --- 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 diff --git a/_CoqProject b/_CoqProject index b2e67cab3..89887ca11 100644 --- a/_CoqProject +++ b/_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