From 664e1d8b93c2c931ba6b03ebe9b9ec70e92a4c3f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 12 Feb 2021 17:49:48 +0100 Subject: [PATCH 1/4] fix elaboration of parameters in HB.structure --- hb.elpi | 4 ++++ structures.v | 3 ++- 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/hb.elpi b/hb.elpi index 0fbae1b73..eb651956c 100644 --- a/hb.elpi +++ b/hb.elpi @@ -116,6 +116,10 @@ located->gref S [loc-modpath _|_] _ :- coq.error S "should be a factory, but is located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but is a module type". located->gref S [] _ :- coq.error "Could not locate name" S. +pred purge-id i:term, o:term. +purge-id T T1 :- + (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1. + % TODO: generalize/rename when we support parameters pred argument->gref i:argument, o:gref. argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR. diff --git a/structures.v b/structures.v index 11048da25..1f92c4b7d 100644 --- a/structures.v +++ b/structures.v @@ -290,7 +290,8 @@ sigT->list-w-params {{ lib:@hb.sigT _ lp:{{ fun N Ty B }} }} L C :- product->triples (B t) (Rest t) C. main [const-decl Module (some B) _] :- !, std.do! [ - sigT->list-w-params B GRFS ClosureCheck, !, + purge-id B B1, std.assert-ok! (coq.elaborate-skeleton B1 _ B2) "illtyped structure definition", + sigT->list-w-params B2 GRFS ClosureCheck, !, with-attributes (main-declare-structure Module GRFS ClosureCheck), ]. main _ :- coq.error "Usage: HB.structure Definition := { A of A & … & A }". From 142fb083cbe35a5813d14005dd4917d6e3704aa9 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 12 Feb 2021 18:43:06 +0100 Subject: [PATCH 2/4] smart elaboration of contexts We elaborate the last item by purging id_phant so that the term can type check even if the requirements of the factory were not postulated --- hb.elpi | 38 +++++++++++++++++++++++--------------- 1 file changed, 23 insertions(+), 15 deletions(-) diff --git a/hb.elpi b/hb.elpi index eb651956c..59f67b0a4 100644 --- a/hb.elpi +++ b/hb.elpi @@ -1857,31 +1857,39 @@ declare-old-constant (some C) :- std.forall {coq.locate-all Id} (declare-old-located Id). declare-old-constant _ :- true. -pred context->factory i:context-decl, o:factoryname. -context->factory (context-item IDT _ TTySkel none t\ context-item _ _ (TF t) none _\ context-end) GRF :- !, - coq.id->name IDT NameT, - std.assert-ok! (coq.elaborate-ty-skeleton TTySkel _ TTy) "context entry illtyped", - @pi-decl NameT TTy t\ - std.assert! (factory? (TF t) (triple GRF _Params t)) - "the last argument must be a factory applied to the type variable". -context->factory (context-item ID _ TSkel none Factories) GRF :- !, - coq.id->name ID Name, - std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "context entry illtyped", - @pi-decl Name T x\ context->factory (Factories x) GRF. -context->factory (context-item ID _ _ (some _) _) _ :- +pred elaborate-context-skel->factory i:context-decl, o:context-decl, o:factoryname, o:diagnostic. +elaborate-context-skel->factory + (context-item IDT IT TTySkel none t\ context-item IDF IF (TFSkel t) none _\ context-end) + (context-item IDT IT TTy none t\ context-item IDF IF (TFSkel t) none _\ context-end) GRF Diag +:- !, std.do-ok! Diag [ + coq.elaborate-ty-skeleton TTySkel _ TTy, + (d\ coq.id->name IDT NameT), + (d\ @pi-decl NameT TTy t\ purge-id (TFSkel t) (TFSkel1 t), coq.elaborate-ty-skeleton (TFSkel1 t) _ (TF1 t) d), + (d\ @pi-decl NameT TTy t\ std.assert! (factory? (TF1 t) (triple GRF _Params t)) "the last argument must be a factory applied to the type variable"), +]. +elaborate-context-skel->factory (context-item ID I TSkel none C) (context-item ID I T none C1) GRF Diag :- !, std.do-ok! Diag [ + coq.elaborate-ty-skeleton TSkel _ T, + (d\ coq.id->name ID Name), + (d\ @pi-decl Name T x\ elaborate-context-skel->factory (C x) (C1 x) GRF d), +]. +elaborate-context-skel->factory (context-item ID _ _ (some _) _) _ _ _ :- coq.error "context item cannot be given a body:" ID. +pred purge-id i:term, o:term. +purge-id T T1 :- + (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1. + pred main-begin-declare-builders i:context-decl. main-begin-declare-builders CtxSkel :- std.do! [ Name is "Builders_" ^ {term_to_string {new_int}}, % TODO? - context->factory CtxSkel GRF, + std.assert-ok! (elaborate-context-skel->factory CtxSkel Ctx GRF) "Context illtyped", coq.env.begin-module Name none, if (GRF = indt FRecord) (std.do! [ coq.env.begin-module "Super" none, std.forall {coq.CS.canonical-projections FRecord} declare-old-constant, coq.env.end-module _]) (true), coq.env.begin-section Name, - builders-postulate-factories CtxSkel, + builders-postulate-factories Ctx, ]. pred postulate-factory-abbrev i:term, i:list term, i:id, i:factoryname, o:term. @@ -1940,7 +1948,7 @@ builders-postulate-factories (context-item IDT _ TySkel none t\ context-item IDF builders-postulate-factories (context-item ID _ TSkel none Factories) :- std.do! [ if-verbose (coq.say "HB: postulating" ID), - std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factorie: illtyped context", + std.assert-ok! (coq.elaborate-ty-skeleton TSkel _ T) "builders-postulate-factories: illtyped context", if (var T) (coq.fresh-type T) true, @local! => hb-add-const ID _ T @opaque! P, % no body, local -> a variable TheParam = global (const P), From d0e8e0dbb4597076fb9c2670c2f38ecfdb0ae1ad Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 13 Feb 2021 17:23:24 +0100 Subject: [PATCH 3/4] type inference is a sharp weapon it "infers" indexes (in the wrong place) --- tests/subtype.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/subtype.v b/tests/subtype.v index 1a8e8aa86..097b038e4 100644 --- a/tests/subtype.v +++ b/tests/subtype.v @@ -22,7 +22,7 @@ SubK : forall x Px, val (@Sub x Px) = x HB.structure Definition SUB (T : Type) (P : pred T) := { S of is_SUB T P S }. -HB.structure Definition SubInhab T P := { sT of is_inhab T & is_SUB T P sT }. +HB.structure Definition SubInhab (T : Type) P := { sT of is_inhab T & is_SUB T P sT }. HB.structure Definition SubNontrivial T P := { sT of is_nontrivial sT & is_SUB T P sT }. From d9164306c6ad13a041ba149a684fe95d00c0bd53 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 13 Feb 2021 17:23:57 +0100 Subject: [PATCH 4/4] little optimization --- hb.elpi | 8 +------- structures.v | 5 +++++ 2 files changed, 6 insertions(+), 7 deletions(-) diff --git a/hb.elpi b/hb.elpi index 59f67b0a4..dc687dfd9 100644 --- a/hb.elpi +++ b/hb.elpi @@ -104,8 +104,6 @@ if-MC-compat P :- get-option "mathcomp.axiom" S, !, P (some GR). if-MC-compat _. - - % TODO: Should this only be used for gref that are factories? (and check in the first/second branch so?) % Should we make this an HO predicate, eg "located->gref S L is-factory? GR" pred located->gref i:string, i:list located, o:gref. @@ -116,10 +114,6 @@ located->gref S [loc-modpath _|_] _ :- coq.error S "should be a factory, but is located->gref S [loc-modtypath _|_] _ :- coq.error S "should be a factory, but is a module type". located->gref S [] _ :- coq.error "Could not locate name" S. -pred purge-id i:term, o:term. -purge-id T T1 :- - (pi fresh t v\ copy {{lib:@hb.id lp:t lp:v}} fresh :- !) => copy T T1. - % TODO: generalize/rename when we support parameters pred argument->gref i:argument, o:gref. argument->gref (str S) GR :- located->gref S {coq.locate-all S} GR. @@ -700,7 +694,7 @@ phant-fun-struct T Name S Params PF Out :- std.do! [ mk-app (global S) Params SParams, mk-app SortProj Params SortProjParams, % Msg = {{lib:hb.nomsg}}, - Msg = {{lib:hb.some (lib:hb.pair "is not canonically a"%string lp:SParams)}}, + Msg = {{lib:hb.some (lib:hb.pair lib:hb.not_a_msg lp:SParams)}}, (@pi-decl Name SParams s\ phant-fun-unify Msg T {mk-app SortProjParams [s]} (PF s) (UnifSI s)), phant-fun-implicit Name SParams UnifSI Out ]. diff --git a/structures.v b/structures.v index 1f92c4b7d..c7fa67d85 100644 --- a/structures.v +++ b/structures.v @@ -7,11 +7,13 @@ Definition unify T1 T2 (t1 : T1) (t2 : T2) (s : option (string * Type)) := phantom T1 t1 -> phantom T2 t2. Definition id_phant {T} {t : T} (x : phantom T t) := x. Definition nomsg : option (string * Type) := None. +Definition is_not_canonically_a : string := "is not canonically a". Register unify as hb.unify. Register id_phant as hb.id. Register Coq.Init.Datatypes.None as hb.none. Register nomsg as hb.nomsg. +Register is_not_canonically_a as hb.not_a_msg. Register Coq.Init.Datatypes.Some as hb.some. Register Coq.Init.Datatypes.pair as hb.pair. Register Coq.Init.Datatypes.prod as hb.prod. @@ -508,6 +510,9 @@ Elpi Typecheck. Notation "`Error_cannot_unify: t1 'with' t2" := (unify t1 t2 None) (at level 0, format "`Error_cannot_unify: t1 'with' t2", only printing) : form_scope. + Notation "`Error: t `is_not_canonically_a T" := (unify t _ (Some (is_not_canonically_a, T))) + (at level 0, T at level 0, format "`Error: t `is_not_canonically_a T", only printing) : + form_scope. Notation "`Error: t msg T" := (unify t _ (Some (msg%string, T))) (at level 0, msg, T at level 0, format "`Error: t msg T", only printing) : form_scope.