Skip to content

Elaboration of parameters in HB.structure and HB.builders #135

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Feb 14, 2021
Merged

Elaboration of parameters in HB.structure and HB.builders #135

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
664e1d8
fix elaboration of parameters in HB.structure
gares Feb 12, 2021
142fb08
smart elaboration of contexts
gares Feb 12, 2021
d0e8e0d
type inference is a sharp weapon
gares Feb 13, 2021
d916430
little optimization
gares Feb 13, 2021
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
42 changes: 24 additions & 18 deletions hb.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -696,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
].
Expand Down Expand Up @@ -1853,31 +1851,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.
Expand Down Expand Up @@ -1936,7 +1942,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),
Expand Down
8 changes: 7 additions & 1 deletion structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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".
Copy link
Member

@CohenCyril CohenCyril Feb 13, 2021

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Amazing!


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.
Expand Down Expand Up @@ -290,7 +292,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 <ModuleName> := { A of <Factory1> A & … & <FactoryN> A }".
Expand Down Expand Up @@ -507,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.
Expand Down
2 changes: 1 addition & 1 deletion tests/subtype.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 }.

Expand Down