From 448731391242249d2320ad6fde51fd33e1c6fcc7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 18:52:38 +0100 Subject: [PATCH 1/7] hack: backport from coq-elpi a new kind of attribute (map) in this way we can parse #[infer(P = "foo", Q = "bar")] --- hb.elpi | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/hb.elpi b/hb.elpi index f9e840327..06c80d62e 100644 --- a/hb.elpi +++ b/hb.elpi @@ -82,17 +82,31 @@ under.do! Then LP :- Then (_\ std.do! LP) _. %%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +% HACK: move to coq-elpi proper +type attmap attribute-type. + % runs P in a context where Coq #[attributes] are parsed pred with-attributes i:prop. with-attributes P :- attributes A, +% HACK: move to coq-elpi proper +(pi S L AS Prefix R R1 Map PS\ + parse-attributes.aux [attribute S (node L)|AS] Prefix R :- + if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !, + parse-attributes.aux AS Prefix R1, + (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map, + std.append R1 [get-option PS Map] R +) => coq.parse-attributes A [ att "verbose" bool, att "mathcomp" bool, att "mathcomp.axiom" string, + att "infer" attmap, ] Opts, !, Opts => P. + pred if-verbose i:prop. if-verbose P :- get-option "verbose" tt, !, P. if-verbose _. From 63a52839159c2c19cf1e06e2d000912f4ee63559 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 18:51:36 +0100 Subject: [PATCH 2/7] automatic inference of a structure on structure paramters --- _CoqProject | 1 + hb.elpi | 29 +++++++++++++++++++++++++++-- structures.v | 2 ++ tests/infer.v | 27 +++++++++++++++++++++++++++ 4 files changed, 57 insertions(+), 2 deletions(-) create mode 100644 tests/infer.v diff --git a/_CoqProject b/_CoqProject index b90e4da21..06f446fb7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -53,5 +53,6 @@ tests/instance_params_no_type.v tests/test_CS_db_filtering.v tests/subtype.v tests/exports.v +tests/infer.v -R . HB diff --git a/hb.elpi b/hb.elpi index 06c80d62e..ef60843c9 100644 --- a/hb.elpi +++ b/hb.elpi @@ -660,6 +660,7 @@ type mterm list term -> term -> list mixinname -> term -> mterm. % - [id] using [unify-arg] kind phant-arg type. type real-arg name -> phant-arg. +type infer-type name -> phant-arg. type implicit-arg phant-arg. type unify-arg phant-arg. @@ -934,6 +935,9 @@ mk-phant-abbrev.term K F [] K F. mk-phant-abbrev.term K F [real-arg N|AL] K'' (fun N _ AbbrevFx) :- !, pi x\ mk-phant-abbrev.term K {mk-app F [x]} AL K' (AbbrevFx x), K'' is K' + 1. +mk-phant-abbrev.term K F [infer-type N|AL] K'' (fun N _ AbbrevFx) :- !, + pi x\ mk-phant-abbrev.term K {mk-app F [{{ lib:hb.Phant lp:x }}]} AL K' (AbbrevFx x), + K'' is K' + 1. mk-phant-abbrev.term K F [implicit-arg|AL] K' FAbbrev :- !, mk-phant-abbrev.term K {mk-app F [_]} AL K' FAbbrev. mk-phant-abbrev.term K F [unify-arg|AL] K' FAbbrev :- !, @@ -1513,7 +1517,8 @@ synthesize-fields.body _Params T ML (record "axioms" {{ Type }} "Class" FS) :- synthesize-fields T ML FS. pred mk-record+sort-field i:name, i:term, i:(term -> record-decl), o:indt-decl. -mk-record+sort-field _ T F (record "type" {{ Type }} "Pack" (field _ "sort" T F)). +mk-record+sort-field _ T F (record RecordName {{ Type }} "Pack" (field _ "sort" T F)) :- + if (get-option "infer" _) (RecordName = "type_") (RecordName = "type"). pred mk-class-field i:classname, i:list term, i:term, i:list (w-args mixinname), o:record-decl. mk-class-field ClassName Params T _ (field _ "class" (app [global ClassName|Args]) _\end-record) :- @@ -1648,6 +1653,24 @@ pack-body ClassName PL T MLwA F :- std.do! [ under-mixins.then MLwA mk-fun (pack-body.mixins PL T BuildC PackS) F ]. +pred declare-auto-infer-params-abbrev i:structure, i:list-w-params mixinname. +declare-auto-infer-params-abbrev GR MLwP :- get-option "infer" Map, !, + Map => mk-infer (global GR) MLwP PHARGS TSK, + std.assert-ok! (coq.elaborate-skeleton TSK _ T) "infer illtyped", + mk-phant-abbrev "type" (phant-term PHARGS T) _ _. +declare-auto-infer-params-abbrev _ _. + +pred mk-infer i:term, i:list-w-params mixinname, o:list phant-arg, o:term. +mk-infer T (w-params.nil _ _ _) [] T. +mk-infer T (w-params.cons N Ty W) [implicit-arg, infer-type N|A] R1 :- coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !, + R1 = (fun N Ty n\ fun `ph` {{ lib:@hb.phant lp:n }} _\ R n), + @pi-decl N Ty n\ + mk-infer {mk-app T [n]} (W n) A (R n). +mk-infer T (w-params.cons N Ty W) [real-arg N|A] (fun N Ty R) :- coq.name->id N ID, not (get-option ID _), !, + @pi-decl N Ty x\ mk-infer {mk-app T [x]} (W x) A (R x). +mk-infer _ (w-params.cons N _ _) _ _ :- coq.name->id N ID, get-option ID Infer, + coq.error "Automatic inference of paramter" N "from" Infer "not supported". + % 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 main-declare-structure i:string, i:list-w-params gref, i:bool. @@ -1682,6 +1705,8 @@ main-declare-structure Module GRFSwP ClosureCheck :- std.do! [ ClassRequires = factory-requires (ClassName) NilwP, ClassAlias = (factory-alias->gref ClassName ClassName), CurrentClass = (class ClassName Structure MLwP), + + declare-auto-infer-params-abbrev Structure MLwP, if-verbose (coq.say "HB: declaring clone abbreviation"), @@ -2227,4 +2252,4 @@ declare-mixin-or-factory Sort1 Fields GRFSwP Module TheType D TheParams :- std.d export Exports, declare-factory-abbrev Module FactAbbrev, -]. \ No newline at end of file +]. diff --git a/structures.v b/structures.v index b6bcb3b1a..f5c6836e8 100644 --- a/structures.v +++ b/structures.v @@ -18,6 +18,8 @@ Register Coq.Init.Datatypes.Some as hb.some. Register Coq.Init.Datatypes.pair as hb.pair. Register Coq.Init.Datatypes.prod as hb.prod. Register Coq.Init.Specif.sigT as hb.sigT. +Register Coq.ssr.ssreflect.phant as hb.phant. +Register Coq.ssr.ssreflect.Phant as hb.Phant. Definition indexed {T} (x : T) := x. Bind Scope type_scope with indexed. Register indexed as hb.indexed. diff --git a/tests/infer.v b/tests/infer.v new file mode 100644 index 000000000..e1202e1be --- /dev/null +++ b/tests/infer.v @@ -0,0 +1,27 @@ +From HB Require Import structures. + +HB.mixin Record foom T := { + op : T -> T -> T +}. + +HB.structure Definition foo := { T of foom T }. + +HB.instance Definition _ := foom.Build nat plus. + +HB.mixin Record barm (P : foo.type) (T : indexed Type) := { + law : P -> T +}. + +#[infer(P)] +HB.structure Definition bar P := { T of barm P T }. + +Fail Check bar.type_ nat. +Print bar.phant_type. +Print bar.type. +Check bar.type nat. + +Fail #[infer(P = "whatever")] +HB.structure Definition bar1 P := { T of barm P T & foom T }. + +#[infer(P = "Type")] +HB.structure Definition bar1 P := { T of barm P T & foom T }. From f595e9af3ab77b0df092fd7507b8d9a56f7f25b7 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 19:01:17 +0100 Subject: [PATCH 3/7] CI is for free --- .github/workflows/main.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml index 728fb9db2..9dc3eccc2 100644 --- a/.github/workflows/main.yml +++ b/.github/workflows/main.yml @@ -27,6 +27,7 @@ jobs: opam: runs-on: ubuntu-latest strategy: + fail-fast: false matrix: coq_version: - '8.11' From 34f663a7ede43bcee667be9784ee3e8a3d8c897f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 19:08:11 +0100 Subject: [PATCH 4/7] fix CI on old coq-elpi --- tests/infer.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/infer.v b/tests/infer.v index e1202e1be..f0f73682f 100644 --- a/tests/infer.v +++ b/tests/infer.v @@ -6,7 +6,7 @@ HB.mixin Record foom T := { HB.structure Definition foo := { T of foom T }. -HB.instance Definition _ := foom.Build nat plus. +HB.instance Definition i := foom.Build nat plus. HB.mixin Record barm (P : foo.type) (T : indexed Type) := { law : P -> T From f88a2bc6997edaa802943cbb5c90ce986b476e0f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 19:16:04 +0100 Subject: [PATCH 5/7] better test --- tests/infer.v | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/tests/infer.v b/tests/infer.v index f0f73682f..1c875fa6a 100644 --- a/tests/infer.v +++ b/tests/infer.v @@ -8,20 +8,21 @@ HB.structure Definition foo := { T of foom T }. HB.instance Definition i := foom.Build nat plus. -HB.mixin Record barm (P : foo.type) (T : indexed Type) := { - law : P -> T +HB.mixin Record barm (A : Type) (P : foo.type) (B: Type) (T : indexed Type) := { + law : P -> T -> A -> B }. #[infer(P)] -HB.structure Definition bar P := { T of barm P T }. +HB.structure Definition bar A P B := { T of barm A P B T }. -Fail Check bar.type_ nat. +Fail Check bar.type_ bool nat bool. Print bar.phant_type. Print bar.type. -Check bar.type nat. +Check bar.type bool nat bool. Fail #[infer(P = "whatever")] -HB.structure Definition bar1 P := { T of barm P T & foom T }. +HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }. #[infer(P = "Type")] -HB.structure Definition bar1 P := { T of barm P T & foom T }. +HB.structure Definition bar1 P := { T of barm bool P bool T & foom T }. +Check bar1.type nat. From f6fd7eca7b77354a21b7784c3a437f2985486834 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 16 Feb 2021 19:24:08 +0100 Subject: [PATCH 6/7] note about attribute parsing hack --- hb.elpi | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/hb.elpi b/hb.elpi index ef60843c9..691d6fb66 100644 --- a/hb.elpi +++ b/hb.elpi @@ -83,14 +83,15 @@ under.do! Then LP :- Then (_\ std.do! LP) _. %%%%% HB Utils %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -% HACK: move to coq-elpi proper +% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2 type attmap attribute-type. % runs P in a context where Coq #[attributes] are parsed pred with-attributes i:prop. with-attributes P :- attributes A, -% HACK: move to coq-elpi proper + +% HACK: move to coq-elpi proper, remove when coq-elpi > 1.9.2 (pi S L AS Prefix R R1 Map PS\ parse-attributes.aux [attribute S (node L)|AS] Prefix R :- if (Prefix = "") (PS = S) (PS is Prefix ^ "." ^ S), supported-attribute (att PS attmap), !, @@ -98,6 +99,7 @@ with-attributes P :- (pi x\ supported-attribute (att x string) :- !) => parse-attributes.aux L "" Map, std.append R1 [get-option PS Map] R ) => + coq.parse-attributes A [ att "verbose" bool, att "mathcomp" bool, From 7c65a67b762b87a3cadb7910289cb70ea4906023 Mon Sep 17 00:00:00 2001 From: Cyril Cohen Date: Wed, 17 Feb 2021 17:42:10 +0100 Subject: [PATCH 7/7] changing mk-phant-abbrev to use skeletons --- hb.elpi | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/hb.elpi b/hb.elpi index 691d6fb66..fdaf1cbac 100644 --- a/hb.elpi +++ b/hb.elpi @@ -946,9 +946,9 @@ mk-phant-abbrev.term K F [unify-arg|AL] K' FAbbrev :- !, mk-phant-abbrev.term K {mk-app F [{{lib:@hb.id _ _}}]} AL K' FAbbrev. pred mk-phant-abbrev i:string, i:phant-term, o:constant, o:abbreviation. -mk-phant-abbrev N (phant-term AL T) C Abbrev :- std.do! [ +mk-phant-abbrev N (phant-term AL T1) C Abbrev :- std.do! [ NC is "phant_" ^ N, - std.assert-ok! (coq.typecheck T TTy) "mk-phant-abbrev: T illtyped", + std.assert-ok! (coq.elaborate-skeleton T1 TTy T) "mk-phant-abbrev: T illtyped", hb-add-const NC T TTy @transparent! C, mk-phant-abbrev.term 0 (global (const C)) AL NParams AbbrevT, @global! => coq.notation.add-abbreviation N NParams AbbrevT tt Abbrev, @@ -1657,20 +1657,21 @@ pack-body ClassName PL T MLwA F :- std.do! [ pred declare-auto-infer-params-abbrev i:structure, i:list-w-params mixinname. declare-auto-infer-params-abbrev GR MLwP :- get-option "infer" Map, !, - Map => mk-infer (global GR) MLwP PHARGS TSK, - std.assert-ok! (coq.elaborate-skeleton TSK _ T) "infer illtyped", - mk-phant-abbrev "type" (phant-term PHARGS T) _ _. + Map => mk-infer (global GR) MLwP PHT, + mk-phant-abbrev "type" PHT _ _. declare-auto-infer-params-abbrev _ _. -pred mk-infer i:term, i:list-w-params mixinname, o:list phant-arg, o:term. -mk-infer T (w-params.nil _ _ _) [] T. -mk-infer T (w-params.cons N Ty W) [implicit-arg, infer-type N|A] R1 :- coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !, +pred mk-infer i:term, i:list-w-params mixinname, o:phant-term. +mk-infer T (w-params.nil _ _ _) (phant-term [] T). +mk-infer T (w-params.cons N Ty W) (phant-term [implicit-arg, infer-type N|A] R1) :- + coq.name->id N ID, (get-option ID "Type" ; get-option ID ""), !, R1 = (fun N Ty n\ fun `ph` {{ lib:@hb.phant lp:n }} _\ R n), @pi-decl N Ty n\ - mk-infer {mk-app T [n]} (W n) A (R n). -mk-infer T (w-params.cons N Ty W) [real-arg N|A] (fun N Ty R) :- coq.name->id N ID, not (get-option ID _), !, - @pi-decl N Ty x\ mk-infer {mk-app T [x]} (W x) A (R x). -mk-infer _ (w-params.cons N _ _) _ _ :- coq.name->id N ID, get-option ID Infer, + mk-infer {mk-app T [n]} (W n) (phant-term A (R n)). +mk-infer T (w-params.cons N Ty W) (phant-term [real-arg N|A] (fun N Ty R)) :- + coq.name->id N ID, not (get-option ID _), !, + @pi-decl N Ty x\ mk-infer {mk-app T [x]} (W x) (phant-term A (R x)). +mk-infer _ (w-params.cons N _ _) _ :- coq.name->id N ID, get-option ID Infer, coq.error "Automatic inference of paramter" N "from" Infer "not supported". % HB.structure Definition S P1 P2 := { T of F1 P1 T & F2 P1 (P2*P2) T }