Skip to content

Commit

Permalink
starting to work on math-comp#347
Browse files Browse the repository at this point in the history
  • Loading branch information
ThomasPortet committed Mar 15, 2023
1 parent d2a8a5f commit d79445b
Show file tree
Hide file tree
Showing 4 changed files with 64 additions and 21 deletions.
51 changes: 32 additions & 19 deletions HB/common/database.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ pred from_builder i:prop, o:term.
from_builder (from _ _ X) (global X).

pred has-mixin-instance_cspat i:prop, o:cs-pattern.
has-mixin-instance_cspat (has-mixin-instance P _ _) P.
has-mixin-instance_cspat (has-mixin-instance P _ _ _) P.

pred mixin-src_type i:prop, o:term.
mixin-src_type (mixin-src T _ _ ) T.
Expand Down Expand Up @@ -225,11 +225,11 @@ findall-builders LFIL :-

pred findall-has-mixin-instance o:list prop.
findall-has-mixin-instance CL :-
std.findall (has-mixin-instance _ _ _) CL.
std.findall (has-mixin-instance _ _ _ _) CL.

pred findall-type-src o:list cs-pattern.
findall-type-src TL :-
std.map {std.findall (has-mixin-instance T_ M_ S_)} has-mixin-instance_cspat TL.
std.map {std.findall (has-mixin-instance T_ M_ S_ L_)} has-mixin-instance_cspat TL.

pred findall-mixin-src i:term, o:list mixinname.
findall-mixin-src T ML :-
Expand Down Expand Up @@ -349,60 +349,73 @@ get-cs-instance (cs-instance _ _ (const Inst)) Inst.
pred has-cs-instance i:gref, i:cs-instance.
has-cs-instance GTy (cs-instance _ (cs-gref GTy) _).

pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref.

pred arg-is-instance i:term, i:term, o:bool.
arg-is-instance _ _ tt.

pred args-is-instance i:term, o:list bool.
args-is-instance (app [_|[A|Args]] as T) [B|L] :-
arg-is-instance T A B, args-is-instance (app [_|Args]) L.
args-is-instance (sort _U) [].
args-is-instance (prod _N _S _F) [].

pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref, o:list bool.

% change order of cases
% if I isn't gref ?
pred mixin-src->has-mixin-instance o:prop, o:prop.

mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd) :-
term->gref T G, term->gref I IHd.
mixin-src->has-mixin-instance (mixin-src T M I) (has-mixin-instance (cs-gref G) M IHd A) :-
term->gref T G, term->gref I IHd, args-is-instance I A.

mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd):-
term->gref I IHd.
mixin-src->has-mixin-instance (mixin-src (prod _ _ _) M I) (has-mixin-instance cs-prod M IHd A):-
term->gref I IHd, args-is-instance I A.

mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
term->gref I IHd.
mixin-src->has-mixin-instance (mixin-src (sort U) M I) (has-mixin-instance (cs-sort U) M IHd A):-
term->gref I IHd, args-is-instance I A.

pred find-instance i:term, i:term, o:term.

pred mk-src
i:term, % type of the instance Ty
i:mixinname, % name of mixin
i:term, % instance body I of type Ty
i:list bool, % list of bool for each param, true if they're instance parameters
i:list prop, % todo list
o:prop.

% mk-src (global _ as T) M I TODO (mixin-src T M I :- TODO). % impossible

mk-src (app [_|Args]) M I TODO (mixin-src T M I :- TODO) :-
std.last Args T',
.
mk-src (app [_|Args]) M I _L TODO (mixin-src T M I :- TODO) :-
std.last Args T.
% std.last Args T',

% coq.mk-app ---- avoids ----> app[ app[ I, a ], b]
% invariant: mk-src Ty _ I _ _ ---> I : Ty

% mk-src I : A -> B
% create a : A
% I a : B
mk-src (prod N_ (sort _) F) M I TODO (pi A \ C A) :- !,
mk-src (prod N_ (sort _) F) M I L TODO (pi A \ C A) :- !,
pi a\
sigma Ia\
coq.mk-app I [a] Ia, % Ia = app[I,a]
mk-src (F a) M Ia TODO (C a).
mk-src (F a) M Ia L TODO (C a).

mk-src (prod N_ S F) M I TODO (pi A pA \ C A pA) :-
mk-src (prod N_ S F) M I L TODO (pi A pA \ C A pA) :-
term->gref S SG, is-structure SG,
pi a\
sigma Ia\
pi pa \
coq.mk-app I [a] Ia,
mk-src (F a) M Ia [find-instance a S pa|TODO] (C a pa).
mk-src (F a) M Ia L [find-instance a S pa|TODO] (C a pa).

pred mk-src-map i:prop, o:prop.
mk-src-map (has-mixin-instance _ M IHd) C :-
mk-src-map (has-mixin-instance _ M IHd []) C :-
T = global IHd,
/*coq.env.typeof IHd Ty,*/
coq.typecheck T Ty ok,
std.spy(mk-src Ty M T [] C).
std.spy(mk-src Ty M T [] [] C).

pred term->cs-pattern i:term, o:cs-pattern.
term->cs-pattern (prod _ _ _) cs-prod.
Expand Down
1 change: 1 addition & 0 deletions HB/instance.elpi
Original file line number Diff line number Diff line change
Expand Up @@ -326,6 +326,7 @@ declare-canonical-instances-from-factory Factory T F ClausesHas CSL :- std.do! [
synthesis.under-local-canonical-mixins-of.do! T [
list-w-params_list {factory-provides Factory} ML,
add-all-mixins T Factory ML tt Clauses MCSL,
coq.say "clausesbef : " Clauses,
std.map-filter Clauses mixin-src->has-mixin-instance ClausesHas,

%std.map ClausesHas has-mixin-instance->mixin-src Clauses,
Expand Down
26 changes: 26 additions & 0 deletions tests/instance_merge_with_distinct_param.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,26 @@
From HB Require Import structures.

HB.mixin Record m1 T := { default1 : T }.

HB.mixin Record m2 T := { default2 : T }.

HB.structure Definition s1 := { T of m1 T }.
HB.structure Definition s2 := { T of m2 T }.

HB.instance Definition _ (X : s1.type) : m1 (list X) :=
m1.Build (list X) (cons default1 nil).
HB.instance Definition list_m2 (X : s2.type) : m2 (list X) :=
m2.Build (list X) (cons default2 nil).

HB.structure Definition s3 := { T of m1 T & m2 T }.

HB.about list. (* should have s3 *)

(* The s3 instance on list should be synthetized automatically, *)
(* this is nontrivial because the parameters are not the same *)
(* but there is a join in the hierarchy, so it can be defined. *)
(* Actually just recalling the list_m2 instance above suffices. *)
HB.instance Definition _ (X : s3.type) := list_m2 X.
HB.about list.


7 changes: 5 additions & 2 deletions tests/instance_params_no_type.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,12 +4,15 @@ HB.mixin Record is_foo P A := { op : P -> A -> A }.

HB.instance Definition nat_foo P := is_foo.Build P nat (fun _ x => x).
HB.instance Definition list_foo P := is_foo.Build P (list P) (fun _ x => x).
HB.instance Definition list_foo' P A:= is_foo.Build P (list A) (fun _ x => x).

About list_foo'.

HB.structure Definition foo P := { A of is_foo P A }.

Section try1.
Variable A : Type.
.... list A ....
(* .... list A ....
(fun A => {|
foo.sort := list..;
Expand All @@ -18,7 +21,7 @@ Variable A : Type.
|} ).
HB.about foo.
HB.about foo. *)

(* Elpi Trace Browser. *)
Check nat_foo.
Expand Down

0 comments on commit d79445b

Please sign in to comment.