From f0e45eed77aebb5ee5fa727ec6528e1cd505c78f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 18 Jun 2024 16:12:57 +0200 Subject: [PATCH] use primproj for class->mixin builders --- HB/about.elpi | 2 +- HB/builders.elpi | 2 +- HB/common/database.elpi | 16 +++++++++++----- HB/common/stdpp.elpi | 5 +++++ HB/common/synthesis.elpi | 6 ++++-- HB/factory.elpi | 2 +- HB/instance.elpi | 2 +- HB/status.elpi | 6 +++++- HB/structure.elpi | 13 +++++++++---- HB/structures.v | 16 +++++++++++----- 10 files changed, 49 insertions(+), 21 deletions(-) diff --git a/HB/about.elpi b/HB/about.elpi index 57c4e7036..9eade5154 100644 --- a/HB/about.elpi +++ b/HB/about.elpi @@ -41,7 +41,7 @@ main-located S (loc-abbreviation A) :- coq.safe-dest-app T (global GR) _, !, main-located S (loc-gref GR). -main-located S (loc-gref GR) :- from Factory Mixin GR, !, +main-located S (loc-gref GR) :- from Factory Mixin (gref GR), !, private.main-builder S Factory Mixin. main-located S (loc-gref GR) :- diff --git a/HB/builders.elpi b/HB/builders.elpi index 81aad47ac..b4556f31d 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -79,7 +79,7 @@ pred declare-1-builder i:builder, i:list prop, o:list prop. 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] :- +declare-1-builder (builder _ SrcFactory TgtMixin B) FromClauses [from SrcFactory TgtMixin (gref B)|FromClauses] :- if-verbose (coq.say {header} "declare builder from" {nice-gref->string SrcFactory} "to" {nice-gref->string TgtMixin}). diff --git a/HB/common/database.elpi b/HB/common/database.elpi index 39fd0274c..a2711b2ca 100644 --- a/HB/common/database.elpi +++ b/HB/common/database.elpi @@ -11,8 +11,8 @@ from_factory (from X _ _) X. pred from_mixin i:prop, o:mixinname. from_mixin (from _ X _) X. -pred from_builder i:prop, o:term. -from_builder (from _ _ X) (global X). +pred from_builder i:prop, o:gref-or-primitive. +from_builder (from _ _ X) X. pred mixin-src_mixin i:prop, o:mixinname. mixin-src_mixin (mixin-src _ M _) M. @@ -97,12 +97,18 @@ factory-provides.base Factory Params T _RMLwP MLwP :- std.do! [ std.map2 BL ML (factory-provides.one Params T) MLwP, ]. -pred factory-provides.one i:list term, i:term, i:term, i:mixinname, o:w-args mixinname. -factory-provides.one Params T B M (triple M PL T) :- std.do! [ - std.assert-ok! (coq.typecheck B Ty) "Builder illtyped", +pred factory-provides.one i:list term, i:term, i:gref-or-primitive, i:mixinname, o:w-args mixinname. +factory-provides.one Params T (gref B) M (triple M PL T) :- std.do! [ + coq.env.typeof B Ty, subst-prod [T] {subst-prod Params Ty} TyParams, std.assert! (extract-conclusion-params T TyParams PL) "The conclusion of a builder is a mixin whose parameters depend on other mixins", ]. +factory-provides.one Params T (primitive (pr P N)) M (triple M PL T) :- std.do! [ + coq.mk-app {coq.mk-app (global M) Params} [T] TyM, % fine since M is the class hence no extra arg needed + std.assert-ok! (d\@pi-decl `m` TyM m\coq.typecheck (app[primitive(proj P N),m]) (TyParams m) d) "Builder illtyped", + @pi-decl `m` TyM m\ + std.assert! (extract-conclusion-params T (TyParams m) PL) "The conclusion of a primitive projection is a mixin whose parameters depend on other mixins" +]. pred extract-conclusion-params i:term, i:term, o:list term. extract-conclusion-params TheType (prod _ S T) R :- !, diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index 71e17f8fc..deb236aab 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -302,6 +302,11 @@ coq.term->gref (app [primitive (proj N J),T|_]) GR :- !, std.do! [ std.map2-filter Ps PPs (x\y\gr\sigma c\x = some c, y = some (pr N J), gr = const c) [GR], ]. +%hack/ fixup API +:before "subst-fun:fail" +coq.subst-fun L (primitive (proj _ _) as F) (app[F|L]). + + 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/synthesis.elpi b/HB/common/synthesis.elpi index c596fc5c4..39359c93c 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -223,13 +223,15 @@ mixin-for_mixin-builder (mixin-for _ _ B) B. % and fills in all the mixins required by the builder using mixin-src, obtaining % a function (MF = Builder Params TheType InferredStuff : Src -> Tgt) 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, +builder->term Ps T Src Tgt B :- from Src Tgt (gref FGR), !, std.do! [ F = global FGR, gref-deps Src MLwP, list-w-params_list MLwP ML, infer-all-these-mixin-args Ps T ML F B, ]. +builder->term _ _ Src Tgt (primitive (proj P N)) :- + % no deps, Src is a class + from Src Tgt (primitive (pr P N)). % [instantiate-all-these-mixin-args T F M_i TFX] where mixin-for T M_i X_i states that % if F ~ fun xs (m_0 : M_0 T) .. (m_n : M_n T ..) ys diff --git a/HB/factory.elpi b/HB/factory.elpi index 0f8837233..b4eaf0cbb 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -165,7 +165,7 @@ 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! [ +declare-id-builder GR (from GR GR (gref (const C))) :- std.do! [ 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", diff --git a/HB/instance.elpi b/HB/instance.elpi index 4dd1ccc1f..4a8c2d8b1 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -424,7 +424,7 @@ optimize-class-body _ _ (app L) (app L) []. pred declare-mixin-name i:term, o:term, o:list prop. declare-mixin-name (global _ as T) T []. declare-mixin-name T (global GR) [] :- mixin-mem T GR. -declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ GR), not (get-option "hnf" tt). +declare-mixin-name T T [] :- coq.safe-dest-app T (global GR) _, not (from _ _ (gref GR)), not (get-option "hnf" tt). declare-mixin-name T (global (const C)) [mixin-mem T (const C)] :- std.do! [ Name is "HB_unnamed_mixin_" ^ {std.any->string {new_int}}, if-verbose (coq.say {header} "Giving name" Name "to mixin instance" {coq.term->string T}), diff --git a/HB/status.elpi b/HB/status.elpi index e6bf3684e..5699194f6 100644 --- a/HB/status.elpi +++ b/HB/status.elpi @@ -43,10 +43,14 @@ print-hierarchy :- std.do! [ namespace private { pred pp-from i:prop. -pp-from (from F M T) :- +pp-from (from F M (gref T)) :- coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)}, coq.say " " {coq.term->string (global T)}, coq.say "". +pp-from (from F M (primitive (pr P N))) :- + coq.say "From" {coq.term->string (global F)} "to" {coq.term->string (global M)}, + coq.say " " P " (" N "th field)", + coq.say "". pred pp-list-w-params i:mixins, i:term. pred pp-list-w-params.list-triple i:list (w-args mixinname), i:term. diff --git a/HB/structure.elpi b/HB/structure.elpi index ef90c694a..26de63686 100644 --- a/HB/structure.elpi +++ b/HB/structure.elpi @@ -308,6 +308,11 @@ export-operations Structure ProjSort ProjClass MLwP EX1 EX2 MLToExport :- std.do std.map LMwPToExport w-params_1 MLToExport, ]. +pred mk-app-builder i:list term, i:term, i:gref-or-primitive, o:term. +mk-app-builder Params TheType (gref B) T :- + coq.mk-app {coq.env.global B} {std.append Params [TheType]} T. +mk-app-builder _ _ (primitive (pr P N)) (primitive(proj P N)). + pred mk-coe-class-body i:factoryname, % From class i:factoryname, % To class @@ -320,14 +325,14 @@ mk-coe-class-body FC TC TMLwP Params T _ CoeBody :- std.do! [ list-w-params_list TMLwP TML, std.map TML (from FC) Builders, - std.map Builders (x\r\mk-app (global x) Params r) BuildersP, + std.map Builders (mk-app-builder Params T) BuildersP, factory-nparams TC TCNP, mk-app (global {get-constructor TC}) {coq.mk-n-holes TCNP} KCHoles, (pi c\ sigma Mixes\ - std.map BuildersP (builder\r\ r = app[builder, T, c]) Mixes, + std.map BuildersP (builder\r\ r = app[builder, c]) Mixes, mk-app KCHoles [T | Mixes] (ClassCoercion c)), CoeBody = {{ fun (c : lp:Class) => lp:(ClassCoercion c) }} @@ -494,12 +499,12 @@ declare-class+structure MLwP Sort std.assert-ok! (coq.typecheck-indt-decl ClassDeclaration) "declare-class: illtyped", (@primitive! => log.coq.env.add-indt ClassDeclaration ClassInd), - coq.env.projections ClassInd Projs, + coq.env.primitive-projections ClassInd Projs, % TODO: put this code in a named clause w-params.nparams MLwP NParams, std.map2 {list-w-params_list MLwP} Projs (m\ p\ r\ sigma P\ std.assert! (p = some P) "BUG: we build a class with an anonymous field", - r = from (indt ClassInd) m (const P)) Factories, + r = from (indt ClassInd) m (primitive P)) Factories, AllFactories = [factory-nparams (indt ClassInd) NParams | Factories], if-verbose (coq.say {header} "declare type record"), diff --git a/HB/structures.v b/HB/structures.v index 07e942ee5..c33fa1eaf 100644 --- a/HB/structures.v +++ b/HB/structures.v @@ -109,13 +109,19 @@ pred class-def o:class. %%%%% Builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% [from FN MN F] invariant: -% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where -% - LMN1 and LMN2 are sub lists of LMN -% - c1 .. cm are terms built using p1 .. pn and T +% [from FN MN B] invariant: +% - B = gref F +% "F : forall p1 .. pn T LMN, FN p1 .. pn T LMN1 -> MN c1 .. cm T LMN2" where +% - LMN1 and LMN2 are sub lists of LMN +% - c1 .. cm are terms built using p1 .. pn and T +% - B = primitive (pr P N) +% - as above but no parameters % - [factory-requires FN LMN] % [from _ M _] tests whether M is a declared mixin. -pred from o:factoryname, o:mixinname, o:gref. +kind gref-or-primitive type. +type gref gref -> gref-or-primitive. +type primitive pair projection int -> gref-or-primitive. +pred from o:factoryname, o:mixinname, o:gref-or-primitive. %%%%% Abbreviations %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%