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

Instance saturation with parameters #343

Closed
wants to merge 1 commit into from
Closed

Instance saturation with parameters #343

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
26 changes: 26 additions & 0 deletions tests/instance_merge_with_distinct_param.v
View file
Open in desktop
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).
Copy link
Member

Choose a reason for hiding this comment

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

The code does

Section TMP.
Variable X : s1.type.
Definition unnamed_ : m1 (list X) := ...
(* generate clause c = mixin-src (list X) m1 "unname_"
    run inference for all known structures, namely s1 and s2 on (list X), loading on the
    fly (with Elpi's => operator) c (and other clauses of the same nature).
    If all the mixins of a structure have a mixin-src, then we declare a canonical instance.
    In this case find that (list X) is an s1. *)

Then, from c we generate a clause like this:

pi P\ has-mixin-instance (list P) m1 [ff] "unnamed_" :- find-structure P s1.

and adds it to the db.

Note that the new clause does not mention the term X hence it makes sense even outside the section TMP. The presence of find-structure part depends on the type of the section parameters, in this case
X has the s1 structure, so we record it in the premise of the clause.

HB.instance Definition list_m2 (X : s2.type) : m2 (list X) :=
m2.Build (list X) (cons default2 nil).
Copy link
Member

Choose a reason for hiding this comment

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

pi P\ has-mixin-instance (list P) m2 [ff] "list_m2" :- find-structure P s2.


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

Choose a reason for hiding this comment

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

We run the code to infer instances about all known types, since maybe we already have all the mixin instances we need. E.g. list is already both an m1 and m2, but when we did run instance inference before, s3 did not exist yet.

We know "list" is an interesting type since we have some has-mixin-src on it.

We run some code corresponding to the question "does (list ?T) have s3". This is a query run
by the already existing code for HB.instance.

mixin-src (list T) m1 P1,  mixin-src (list T) m2 P2

I guess we need one extra rule

mixin-src T M P :- has-mixin-instance T M P.

which in turn checks the premises on the parameter of list are satisfied.
There are two calls to find-structure:

find-structure T s1 V1,  find-structure T s2 V2

the implementation of find structure calls Coq's unification (structure-proj may be named differently, it is in HB/database.elpi)

find-structure T Struct V :- structure-proj Struct Proj, coq.unify T (app[Proj,V]).

Since Coe 8.16 can compute the "pullback" asking

s1.sort ?V1 = ?X,
s2.sort ?V2 = ?X

Coq will figure out something like V1 = s1_of_s3 ?V and V2 = s2_of_s3 ?V hence ?V is a Coq hole
of type s3 which is the join of the two structures.

To simulate in Coq

Check ((erefl _ : s1.sort _ = ?[x]) , (erefl _ : s2.sort _ = ?[x])).

The answer should be

Check ((erefl _ : s1.sort (s1_of_s3 ?[v] = ?[x]) , (erefl _ : s2.sort (s2_of_s3 ?[v]) = ?[x])).


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_s2 instance above suffices. *)
HB.instance Definition _ (X : s3.type) := list_m2 X.
HB.about list.


26 changes: 26 additions & 0 deletions tests/instance_merge_with_param.v
View file
Open in desktop
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 : s1.type) : m2 (list X) :=
m2.Build (list X) 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, *)
(* But since it's defined afterwards, it's not taken into account. *)
(* The subtelty now is that there is a parameter, but it's always the same *)
(* A simple recall suffices: *)
HB.instance Definition _ (X : s1.type) := list_m2 X.
HB.about list.