From 816dbcb317667e3ba8ddf121fc1e0cf4228af9e6 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Fri, 5 Mar 2021 20:36:26 +0100 Subject: [PATCH 1/5] No section discharge for alias factories and builder instances --- HB/builders.elpi | 2 ++ HB/factory.elpi | 3 ++- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/HB/builders.elpi b/HB/builders.elpi index 82d48d920..baf6e2c1d 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -159,6 +159,8 @@ postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF postulate-factory-abbrev TheType Params IDF GRF TheFactory, define-factory-operations TheType Params TheFactory GRF, log.coq.env.accumulate current "hb.db" (clause _ _ (current-mode (builder-from TheFactory GRF ModName))), + if-verbose (coq.say "Adding clause @using!" IDF "to the context"), + log.coq.env.accumulate current "hb.db" (clause _ _ (@using! IDF)) ]. postulate-factories ModName (context-item ID _ TSkel none Factories) :- std.do! [ diff --git a/HB/factory.elpi b/HB/factory.elpi index f7f7f593f..7f90e8f2a 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -163,7 +163,8 @@ declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [ context.declare TheType TheParams GRFSwP Hyps _, std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory", - log.coq.env.add-const-noimplicits "axioms_" Ty1 _ @transparent! C, + @using! "All" => + log.coq.env.add-const-noimplicits "axioms_" Ty1 _ @transparent! C, std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory", std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing", From 6a971c5594dcbf33df79507cf9c25e590555836a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 25 Mar 2021 19:18:31 +0100 Subject: [PATCH 2/5] Update HB/builders.elpi --- HB/builders.elpi | 2 -- 1 file changed, 2 deletions(-) diff --git a/HB/builders.elpi b/HB/builders.elpi index baf6e2c1d..82d48d920 100644 --- a/HB/builders.elpi +++ b/HB/builders.elpi @@ -159,8 +159,6 @@ postulate-factories ModName (context-item IDT _ TySkel none t\ context-item IDF postulate-factory-abbrev TheType Params IDF GRF TheFactory, define-factory-operations TheType Params TheFactory GRF, log.coq.env.accumulate current "hb.db" (clause _ _ (current-mode (builder-from TheFactory GRF ModName))), - if-verbose (coq.say "Adding clause @using!" IDF "to the context"), - log.coq.env.accumulate current "hb.db" (clause _ _ (@using! IDF)) ]. postulate-factories ModName (context-item ID _ TSkel none Factories) :- std.do! [ From 2a72859060a54831809173ec498e90a8a7293a79 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Mar 2021 17:19:47 +0200 Subject: [PATCH 3/5] cleanup --- HB/common/stdpp.elpi | 15 ++++++++++++++- HB/common/synthesis.elpi | 6 +++--- HB/instance.elpi | 4 +++- tests/compress_coe.v | 2 +- tests/compress_coe.v.out | 2 +- 5 files changed, 22 insertions(+), 7 deletions(-) diff --git a/HB/common/stdpp.elpi b/HB/common/stdpp.elpi index dab100154..5674ea361 100644 --- a/HB/common/stdpp.elpi +++ b/HB/common/stdpp.elpi @@ -138,7 +138,7 @@ coq.gref.list->set L S :- std.fold L {coq.gref.set.empty} coq.gref.set.add S. % [coq.abstract-indt-decl Section I AbsI] abstracts I over the Section variables -% which becomes parameter nodes if the indt-decl type +% which becomes parameter nodes of the indt-decl type pred coq.abstract-indt-decl i:list constant, i:indt-decl, o:indt-decl. coq.abstract-indt-decl [] X X1 :- copy-indt-decl X X1. coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :- @@ -149,6 +149,19 @@ coq.abstract-indt-decl [C|CS] X (parameter ID explicit Ty1 X1) :- (copy (global (const C)) x :- !) => coq.abstract-indt-decl CS X (X1 x). +% [coq.abstract-const-decl Section I AbsI] abstracts I over the Section variables +% which becomes fun nodes +pred coq.abstract-const-decl i:list constant, i:pair term term, o:pair term term. +coq.abstract-const-decl [] (pr X Y) (pr X1 Y1) :- copy X X1, copy Y Y1. +coq.abstract-const-decl [C|CS] X (pr (fun Name Ty1 X1) (prod Name Ty1 X2)) :- + coq.gref->string (const C) ID, + coq.id->name ID Name, + coq.env.typeof (const C) Ty, + copy Ty Ty1, + @pi-parameter ID Ty x\ + (copy (global (const C)) x :- !) => + coq.abstract-const-decl CS X (pr (X1 x) (X2 x)). + % [coq.copy-clauses-for-unfold CS CL] generates clauses for the copy predicate % to unfold all constants in CS pred coq.copy-clauses-for-unfold i:list constant, o:list prop. diff --git a/HB/common/synthesis.elpi b/HB/common/synthesis.elpi index 4b1967c0f..02b7ac58d 100644 --- a/HB/common/synthesis.elpi +++ b/HB/common/synthesis.elpi @@ -31,7 +31,7 @@ pred infer-all-mixin-args i:list term, i:term, i:gref, o:term. infer-all-mixin-args Ps T GR X :- !, std.do! [ std.assert! (gref-deps GR MLwP) "BUG: gref-deps should never fail", list-w-params_list MLwP ML, - infer-mixin-args Ps T ML (global GR) X + infer-mixin-args Ps T ML (global GR) X, ]. % [assert!-infer-mixin TheType M Out] infers one mixin M on TheType and @@ -109,7 +109,7 @@ namespace private { % the databases [mixin-src] and [from] pred mixin-for i:term, i:mixinname, o:term. mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [ - if-verbose (coq.say "HB: Trying to infer mixin for" M), + %if-verbose (coq.say "HB: Trying to infer mixin for" M), std.assert-ok! (coq.typecheck Tm Ty) "mixin-for: Tm illtyped", factory? Ty (triple Factory Params _), @@ -119,7 +119,7 @@ mixin-for T M MICompressed :- mixin-src T M Tm, !, std.do! [ coq.subst-fun [Tm] B MI ), - if-verbose (coq.say "HB: Trying to compress mixin for" {coq.term->string MI}), + %if-verbose (coq.say "HB: Trying to compress mixin for" {coq.term->string MI}), compress-coercion-paths MI MICompressed, ]. diff --git a/HB/instance.elpi b/HB/instance.elpi index b784ef557..d50f888c3 100644 --- a/HB/instance.elpi +++ b/HB/instance.elpi @@ -89,7 +89,9 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :- coq.gref->path TGR TPath, std.rev TPath [TMod|_], coq.gref->id TGR TID, - Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}, + if (TMod = TID) + (Name is TID ^ "_canonical_" ^ {gref->modname Struct}) + (Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}), if-verbose (coq.say "HB: declare canonical structure instance" Name), diff --git a/tests/compress_coe.v b/tests/compress_coe.v index ccf2786d5..61e87ae2e 100644 --- a/tests/compress_coe.v +++ b/tests/compress_coe.v @@ -34,4 +34,4 @@ HB.instance Definition prodD (D D' : D.type) := hasD.Build (D * D')%type (d, d). Set Printing Coercions. -Print prod_prod_canonical_D. \ No newline at end of file +Print prod_canonical_D. \ No newline at end of file diff --git a/tests/compress_coe.v.out b/tests/compress_coe.v.out index 2535dfaea..1a68bd550 100644 --- a/tests/compress_coe.v.out +++ b/tests/compress_coe.v.out @@ -1,4 +1,4 @@ -prod_prod_canonical_D = +prod_canonical_D = fun D D' : D.type => {| D.sort := D.sort D * D.sort D'; From f37657450986f39889166ba38d80aced865514e9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 29 Mar 2021 17:20:02 +0200 Subject: [PATCH 4/5] abstract factory alias by hand --- HB/factory.elpi | 27 ++++++++++++++++----------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/HB/factory.elpi b/HB/factory.elpi index 7f90e8f2a..30d076222 100644 --- a/HB/factory.elpi +++ b/HB/factory.elpi @@ -157,23 +157,28 @@ process-asset-unnamed-parameters (asset-record _ Sort _ Fields) GRFS Module TheT pred declare-factory-alias i:term, i:list-w-params factoryname, i:id, i:term, i:list term. declare-factory-alias Ty1Skel GRFSwP Module TheType TheParams :- std.do! [ - % TODO maybe context.declare should just take GRFSwP and postulate % the parameters and the type - context.declare TheType TheParams GRFSwP Hyps _, + context.declare TheType TheParams GRFSwP MixinSrcClauses SectionCanonicalInstance, + + if-verbose (coq.say "HB: declare constant axioms_"), std.assert-ok! (coq.elaborate-ty-skeleton Ty1Skel _ Ty1) "Illtyped alias factory", - @using! "All" => - log.coq.env.add-const-noimplicits "axioms_" Ty1 _ @transparent! C, + + abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr Ty1 _) (pr Ty1Closed _) Section, + log.coq.env.add-const-noimplicits "axioms_" Ty1Closed _ @transparent! C, std.assert! (safe-dest-app Ty1 (global PhF) _Args) "Argument must be a factory", std.assert! (factory-alias->gref PhF F) "BUG: Factory alias declaration missing", std.assert! (factory-constructor F FK) "BUG: Factory constructor missing", - Hyps => synthesis.infer-all-mixin-args TheParams TheType FK MFK, + MixinSrcClauses => synthesis.infer-all-mixin-args TheParams TheType FK MFK, std.assert-ok! (coq.typecheck MFK MFKTy) "BUG: typecking of former factory constructor failed", - (pi Args\ copy (app [global F|Args]) (global (const C))) => copy MFKTy MFKTyC, - log.coq.env.add-const-noimplicits "Axioms_" MFK MFKTyC @transparent! CK, + (pi Args\ copy (app[global F|Args]) (app[global (const C)|Section])) => copy MFKTy MFKTyC, + + abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-const-decl (pr MFK MFKTyC) (pr MFKClosed MFKTyCClosed) _, + log.coq.env.add-const-noimplicits "Axioms_" MFKClosed MFKTyCClosed @transparent! CK, + GRK = const CK, log.coq.env.end-section-name Module, @@ -225,8 +230,8 @@ build-deps-for-projections R MLwP CL :- std.do! [ % variables that aoccur. We don't want that for mixin/factories, so we implement % our own discharging. Note that definitions (like canonical instance) have % to be abstracted too. -pred abstract-indt-decl-over-section i:list term, i:term, i:list prop, i:list constant, i:indt-decl, o:indt-decl. -abstract-indt-decl-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance RDecl RDeclClosed :- +pred abstract-over-section i:list term, i:term, i:list prop, i:list constant, i:(list constant -> A -> A -> prop), i:A, o:A, o:list term. +abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance F X X1 Section :- % compute section variables to be used for discharging std.map MixinSrcClauses mixin-src_src Mixins, std.append TheParams [TheType|{std.rev Mixins}] Section, @@ -234,7 +239,7 @@ abstract-indt-decl-over-section TheParams TheType MixinSrcClauses SectionCanonic % We discharge by hand the record declaration so that we can be sure all % parameters and mixins are abstracted (even if unused). coq.copy-clauses-for-unfold SectionCanonicalInstance CopyUnfold, - CopyUnfold => coq.abstract-indt-decl SectionVars RDecl RDeclClosed. + CopyUnfold => F SectionVars X X1. pred declare-mixin-or-factory i:term, i:record-decl, i:list-w-params factoryname, i:id, i:term, i:asset, i:list term. declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.do! [ @@ -246,7 +251,7 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d RDeclSkel = record "axioms_" Sort1 Kname Fields, std.assert-ok! (coq.elaborate-indt-decl-skeleton RDeclSkel RDecl) "record declaration illtyped", - abstract-indt-decl-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance RDecl RDeclClosed, + abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _, log.coq.env.add-indt RDeclClosed R, log.coq.env.end-section-name Module, % We need to anyway declare the record inside the section From 3e47afd19a1e555a6be3a6a50507a4fcaf95984f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 30 Mar 2021 15:01:21 +0200 Subject: [PATCH 5/5] test --- examples/demo1/hierarchy_5.v | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/examples/demo1/hierarchy_5.v b/examples/demo1/hierarchy_5.v index 1388cd0e2..64f01b375 100644 --- a/examples/demo1/hierarchy_5.v +++ b/examples/demo1/hierarchy_5.v @@ -223,4 +223,7 @@ Proof. by rewrite -addrA subrr addr0. Qed. End Theory. -HB.graph "hierarchy_5.dot". \ No newline at end of file +HB.graph "hierarchy_5.dot". + +(* we check the alias factory is abstracted over the whole section *) +HB.check (SemiRing_of_AddComoid.axioms_ : forall A, forall m : AddMonoid_of_TYPE.axioms_ A, AddComoid_of_AddMonoid.axioms_ A m -> Type). \ No newline at end of file