Instance saturation with parameters

[CohenCyril]

TODO:

• Test file
• Actual fix

Fixes #339

CC @gares @ThomasPortet

[gares]

Some notes

[gares]

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.

[gares]

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

[gares]

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])).

[gares]

integrated in #334