Skip to content
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

do not crash if the key has no name #195

Open
wants to merge 1 commit into
base: master
Choose a base branch
from
Open

do not crash if the key has no name #195

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
10 changes: 7 additions & 3 deletions HB/common/database.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -256,12 +256,16 @@ get-cs-structure (cs-instance _ _ (global Inst)) Struct :- std.do! [
coq.prod-tgt->gref InstTy Struct
].

pred has-cs-instance i:gref, i:cs-instance.
has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).
pred has-cs-instance i:term, i:cs-instance.
has-cs-instance (global GR) (cs-instance _ (cs-gref GR) _) :- !.
has-cs-instance (app[global GR|_]) (cs-instance _ (cs-gref GR) _) :- !.
has-cs-instance (prod _ _ _) (cs-instance _ cs-prod _) :- !.
has-cs-instance (sort U) (cs-instance _ (cs-sort U) _) :- !.
Copy link
Member Author

@gares gares Mar 31, 2021 •
edited
Loading

Choose a reason for hiding this comment

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

Suggested change
has-cs-instance (sort U) (cs-instance _ (cs-sort U) _) :- !.
has-cs-instance (sort U) (cs-instance _ (cs-sort U) _) :- !.
has-cs-instance (fun _ _ _) _ :- coq.version _ _ N _, N < 14, coq.error "Coq cannot handle canonical values which are anonymous functions".
has-cs-instance (fun _ _ _) _ :- coq.version _ _ N _, N >= 14, coq.error "NYI: canonical values which are anonymous functions".

Copy link
Member Author

Choose a reason for hiding this comment

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

@CohenCyril is this what you want? It is unclear what to do when we move to Coq 8.14 (assuming it gets support for cs-fun canonical value)

has-cs-instance _ (cs-instance _ cs-default _) :- !.

pred get-local-structures i:term, o:list structure.
get-local-structures TyTrm StructL :- std.do! [
std.filter {coq.CS.db} (has-cs-instance {term->gref TyTrm}) DBGTyL,
std.filter {coq.CS.db} (has-cs-instance TyTrm) DBGTyL,
std.map DBGTyL get-cs-structure RecL,
std.filter RecL is-structure StructL
].
Expand Down
15 changes: 9 additions & 6 deletions HB/common/synthesis.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -46,29 +46,32 @@ assert!-infer-mixin T M B :-
% Given TheType it looks all canonical structure instances on it and makes
% all their mixins available for inference
pred under-local-canonical-mixins-of.do! i:term, i:list prop.
under-local-canonical-mixins-of.do! T P :-
under-local-canonical-mixins-of.do! T P :- std.do! [
get-local-structures T CS,
std.map CS (private.structure-instance->mixin-srcs T) MSLL,
std.flatten MSLL MSL,
MSL => std.do! P.
MSL => std.do! P,
].

% Given TheType and a factory instance (on it), makes all the mixins provided by
% the factory available for inference.
pred under-mixin-src-from-factory.do! i:term, i:term, i:list prop.
under-mixin-src-from-factory.do! TheType TheFactory LP :-
under-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [
private.factory-instance->new-mixins [] TheFactory ML,
std.map ML (m\c\ c = mixin-src TheType m TheFactory) MLClauses,
MLClauses => std.do! LP.
MLClauses => std.do! LP,
].

% Given TheType and a factory instance (on it), builds all the *new* mixins
% provided by the factory available for and passes them to the given
% continuation
pred under-new-mixin-src-from-factory.do! i:term, i:term, i:(list mixinname -> prop).
under-new-mixin-src-from-factory.do! TheType TheFactory LP :-
under-new-mixin-src-from-factory.do! TheType TheFactory LP :- std.do! [
findall-mixin-src TheType OldMixins,
private.factory-instance->new-mixins OldMixins TheFactory NewML,
std.map NewML (m\c\ c = mixin-src TheType m TheFactory) NewMLClauses,
NewMLClauses => std.do! [ LP NewML ].
NewMLClauses => std.do! [ LP NewML ],
].

% [under-mixins.then MLwP Pred F] states that F has shape
% fun p_1 .. p_k T,
Expand Down
29 changes: 20 additions & 9 deletions HB/instance.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -85,13 +85,7 @@ declare-all T [class Class Struct MLwP|Rest] [pr Name CS|L] :-
fail,

!,
coq.term->gref T TGR,
coq.gref->path TGR TPath,
std.rev TPath [TMod|_],
coq.gref->id TGR TID,
if (TMod = TID)
(Name is TID ^ "_canonical_" ^ {gref->modname Struct})
(Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}),
private.craft-instance-name T Struct Name,

if-verbose (coq.say "HB: declare canonical structure instance" Name),

Expand Down Expand Up @@ -122,10 +116,26 @@ declare-instance T F Clauses :-
(std.map CS (x\r\ sigma i c\ x = pr i c, r = instance-to-export i c) Clauses)
(Clauses = []).

pred craft-instance-name i:term, i:structure, o:id.
craft-instance-name (global TGR) Struct Name :- craft-instance-name.of-gref TGR Struct Name.
craft-instance-name (app[global TGR|_]) Struct Name :- craft-instance-name.of-gref TGR Struct Name.
craft-instance-name (fun _ _ _) Struct Name :-
Name is "Fun" ^ {std.any->string {new_int}} ^ "_canonical_" ^ {gref->modname Struct}.

pred craft-instance-name.of-gref i:gref, i:structure, o:id.
craft-instance-name.of-gref TGR Struct Name :-
coq.gref->path TGR TPath,
std.rev TPath [TMod|_],
coq.gref->id TGR TID,
if (TMod = TID)
(Name is TID ^ "_canonical_" ^ {gref->modname Struct})
(Name is TMod ^ "_" ^ TID ^ "_canonical_" ^ {gref->modname Struct}).


% [add-mixin T F _ M Cl] adds a constant begin the mixin instance for M on type
% T built from factory F
pred add-mixin i:term, i:factoryname, i:bool, i:mixinname, o:list prop.
add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :-
add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :- std.do! [
synthesis.assert!-infer-mixin T MissinMixin Bo,
MixinSrcCl = mixin-src T MixinName (global (const C)),
BuiderDeclCl = builder-decl (builder N FGR MixinName (const C)),
Expand All @@ -146,7 +156,8 @@ add-mixin T FGR MakeCanon MissinMixin [MixinSrcCl, BuiderDeclCl] :-
if (MakeCanon = tt, whd (global (const C)) [] (global (indc _)) _)
(if-verbose (coq.say "HB: declare canonical mixin instance" C),
with-locality (log.coq.CS.declare-instance C))
true.
true,
].

pred add-all-mixins i:term, i:factoryname, i:list mixinname, i:bool, o:list prop.
add-all-mixins T FGR ML MakeCanon Clauses :- std.do! [
Expand Down
1 change: 1 addition & 0 deletions _CoqProject.test-suite
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -56,6 +56,7 @@ tests/log_impargs_record.v
tests/compress_coe.v
tests/funclass.v
tests/local_instance.v
tests/alias_f_instance.v

-R tests HB.tests
-R examples HB.examples
Expand Down
8 changes: 8 additions & 0 deletions tests/alias_f_instance.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
From HB Require Import structures.

HB.mixin Record IsPred (R : Type) (S : R -> bool) := {}.
HB.structure Definition Pred R := {S of IsPred R S}.

Definition bool_pred := IsPred.Build bool (fun x => true).

HB.instance Definition _ := bool_pred.