HB.saturate: saturating instances on new structure declaration

When a new structure `S` is created it may be the case that
some type which is already equipped with some mixins
is an instance of `S`, but was not declared as such since `S`
was not declared yet.

Similarly, mixin instances which have parameters may not
be available on a single type until there is a structure for the parameter
which is rich enough.

We store in the predicate `has-mixin-instance` the list of types which
have mixin instances, so that we can reconsider them later.

Out of these we craft `mixin-src` clauses (used by `HB/common/inference.elpi`)
which have premises using Coq's unifyer (which in turn can compute the
smallest structure having all requirements thanks to the hints we declare
on joins).

Example:

When such an instance is declared:
```coq
HB.instance Definition I1 (X:t1) : mixin1 (list X) := ... .
```
a clause of this form is generated:
```coq
has-mixin-instance (cs-gref (indt «list»)) (indt «mixin1.axioms_») (const «I1»)
```
When `HB.saturate` is called, we generate conditional `mixin-src` clauses with
conditions on parameters (via the function `has-mixin-instance->mixin-src`).

Then for each type constructor mentioned in a `has-mixin-src` clause
we try to declare new instances with the new clauses via
`declare-all-on-type-constructor`.

Unresolved parameters are abstracted out. Their type is the smallest structure
which can satisfy all the constraints coming from single mixins.

.gitignore

@@ -58,3 +58,4 @@ _minted-*
 *.vtc
 
 *.dot
+*.json

HB/common/database.elpi

@@ -1,7 +1,7 @@
 /*        Hierarchy Builder: algebraic hierarchies made easy
     This software is released under the terms of the MIT license              */
 
-shorten coq.{ term->gref, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
+shorten coq.{ term->gref, term-is-gref?, subst-fun, safe-dest-app, mk-app, mk-eta, subst-prod }.
 
 %%%%%%%%% HB database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
@@ -14,6 +14,13 @@ from_mixin (from _ X _) X.
 pred from_builder i:prop, o:term.
 from_builder (from _ _ X) (global X).
 
+% for a given clause mixin-src with eventually a condition, 
+% returns the type of the first argument
+pred mixin-src-w-cond_type i:prop, o:term.
+mixin-src-w-cond_type(mixin-src (global G) _ _ :- _) (global G).
+mixin-src-w-cond_type (mixin-src (app [T|_]) _ _ :- _) T.
+mixin-src-w-cond_type (pi x \ (C x)) T :- pi y \ mixin-src-w-cond_type (C y) T.
+
 pred mixin-src_mixin i:prop, o:mixinname.
 mixin-src_mixin (mixin-src _ M _) M.
 
@@ -133,6 +140,23 @@ factories-provide FLwP MLwP :- std.do! [
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
 ].
 
+pred undup-grefs  i:list gref, o:list gref.
+undup-grefs  L UL :- std.do! [
+  coq.gref.list->set L S, 
+  coq.gref.set.elements S UL,
+].
+
+% remove duplicates from a list of terms, but all the terms have to be global references
+pred undup-terms  i:list term, o:list term.
+undup-terms L UL :- std.do! [
+  std.map L coq.term->gref LG,
+  undup-grefs LG ULG,
+  std.map ULG (coq.env.global ) UL,
+].
+
+
+
+
 % Mixins can be topologically sorted according to their dependencies
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
 toposort-mixins In Out :- std.do! [
@@ -192,10 +216,14 @@ findall-builders LFIL :-
   std.map {std.findall (builder-decl B_)} extract-builder LFILunsorted,
   std.bubblesort LFILunsorted leq-builder LFIL.
 
+pred findall-has-mixin-instance o:list prop.
+findall-has-mixin-instance CL :-
+   std.findall (has-mixin-instance  _ _ _) CL.
+
 pred findall-mixin-src i:term, o:list mixinname.
 findall-mixin-src T ML :-
   std.map {std.findall (mixin-src T M_ V_)} mixin-src_mixin ML.
-
+  
 pred findall-local-canonical o:list constant.
 findall-local-canonical CL :-
   std.map {std.findall (local-canonical C_)} local-canonical-gref CL.
@@ -272,6 +300,7 @@ assert-good-coverage! MLSortedRev CNL :- std.do! [
      true
 ].
 
+
 %%%%% Coq Database %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 % [get-structure-coercion S1 S2 F] finds the coecion F from the structure S1 to S2
@@ -299,7 +328,7 @@ get-constructor (indt R) (indc K) :- !,
  if (coq.env.indt R _ _ _ _ [K] _) true (coq.error "Not a record" R).
 get-constructor I _ :- coq.error "get-constructor: not an inductive" I.
 
-%% finding for locally defined structures
+% finding for locally defined structures
 pred get-cs-structure i:cs-instance, o:structure.
 get-cs-structure (cs-instance _ _ (const Inst)) Struct :- std.do! [
   coq.env.typeof (const Inst) InstTy,
@@ -313,6 +342,78 @@ 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 mixin-src->has-mixin-instance i:prop, o:prop.
+mixin-src->has-mixin-instance  (mixin-src (global GR) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+
+mixin-src->has-mixin-instance (mixin-src (app [global GR|_] ) M I) (has-mixin-instance (cs-gref GR) M IHd) :-
+  term->gref I IHd.
+
+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 (sort U) M I) (has-mixin-instance (cs-sort U) M IHd):-
+  term->gref I IHd.
+
+% this auxiliary function iterates over the list of arguments of an application,
+% and create the necessary unify condition for each arguments 
+% and at the end returns the mixin-src clause with all the conditions
+pred mk-src-aux 
+  i:list term, % list of arguments
+  i:term, % head of the original application
+  i:mixinname, % name of mixin
+  i:term, % instance body
+  i:list prop, % Cond list
+  o:prop.
+mk-src-aux [] T M I Cond (mixin-src T M I :- Cond).
+mk-src-aux [A|Args] T M I Cond  (pi a \ C a) :-
+  pi a \
+  sigma Ta\
+    coq.mk-app T [a] Ta,
+    mk-src-aux Args Ta M I [coq.unify-eq A a ok|Cond] (C a).
+
+
+% transforms the has-mixin-instance clause arguments into a
+% mixin-src clause with eventuals conditions regarding its parameters
+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 prop, % Cond list
+  o:prop.
+
+mk-src (app [_|Args]) M I Cond C :-
+  std.last Args Last,
+  safe-dest-app Last Hd ArgsLast,
+  mk-src-aux ArgsLast Hd M I Cond C.
+
+mk-src (prod N_ _ F) M I Cond (pi a \ C a) :-
+  pi a\
+  sigma  Ia \
+  coq.mk-app I [a] Ia,
+    mk-src (F a) M Ia Cond (C a).
+
+
+% for a type T, create as many holes as there are foralls and returns that enriched type
+pred enrich-type i:term, o:term .
+enrich-type T ET :- 
+  coq.typecheck T TH ok,
+  coq.count-prods TH N,
+  if (N = 0) (ET = T) (coq.mk-app T {coq.mk-n-holes N} ET).
+
+% wrapper for mk-src so it can be called by a map on a list of clauses has-mixin-instance
+pred mk-src-map i:prop, o:prop.
+mk-src-map (has-mixin-instance _ M IHd) C :- std.do![
+  T = global IHd,
+  coq.env.typeof IHd Ty,
+  mk-src Ty M T [] C,
+  ].
+
+pred cs-pattern->term i:cs-pattern, o:term.
+cs-pattern->term (cs-gref GR) (global GR).
+cs-pattern->term (cs-sort U) (sort U).
+
 pred term->cs-pattern i:term, o:cs-pattern.
 term->cs-pattern (prod _ _ _) cs-prod.
 term->cs-pattern (sort U) (cs-sort U).

HB/common/stdpp.elpi

@@ -123,6 +123,12 @@ pred coq.env.current-library o:string.
 coq.env.current-library L :- loc.fields {get-option "elpi.loc"} L _ _ _ _.
 coq.env.current-library "dummy.v".
 
+pred coq.term-is-gref? i:term, o:gref.
+coq.term-is-gref? (global GR) GR :- !.
+coq.term-is-gref? (pglobal GR _) GR :- !.
+coq.term-is-gref? (app [Hd|_]) GR :- !, coq.term-is-gref? Hd GR.
+coq.term-is-gref? (let _ _ T x\x) GR :- !, coq.term-is-gref? T GR.
+
 pred coq.prod-tgt->gref i:term, o:gref.
 coq.prod-tgt->gref T GR :- whd1 T T1, !, coq.prod-tgt->gref T1 GR.
 coq.prod-tgt->gref (prod N Src Tgt) GR :- !, @pi-decl N Src x\ coq.prod-tgt->gref (Tgt x) GR.

HB/common/utils.elpi

@@ -374,4 +374,4 @@ prod-last X X :- !.
 
 pred prod-last-gref i:term, o:gref.
 prod-last-gref (prod N S X) GR :- !, @pi-decl N S x\ prod-last-gref (X x) GR.
-prod-last-gref X GR :- coq.term->gref X GR.
+prod-last-gref X GR :- coq.term->gref X GR.

HB/context.elpi

@@ -73,7 +73,7 @@ postulate-mixin TheType (triple M Ps T) (triple CL MSL MLwP) (triple OutCL [MC|M
 
   MC = mixin-src T M (global (const C)),
   MC => get-option "local" tt =>
-    instance.declare-all TheType {findall-classes-for [M]} NewCSL,
+    instance.declare-all-generic-type TheType {findall-classes-for [M]} NewCSL,
   std.map NewCSL snd NewCL,
   std.append CL NewCL OutCL
   ].

HB/factory.elpi

@@ -53,7 +53,7 @@ argument->w-mixins (ctx-decl Decl) (pr MLwP ArgwP) :- !, std.do! [
 pred argument-name i:argument, o:string.
 argument-name (const-decl Id _ _) Id :- !.
 argument-name (indt-decl (parameter _ _ _ R)) Id :- !,
-  argument-name (indt-decl (R (sort prop))) Id.
+argument-name (indt-decl (R (sort prop))) Id.
 argument-name (indt-decl (record Id _ _ _)) Id :- !.
 argument-name (indt-decl (inductive Id _ _ _)) Id :- !.
 argument-name (ctx-decl _) "_" :- !.
@@ -231,7 +231,6 @@ declare-mixin-or-factory MixinSrcClauses SectionCanonicalInstance
 
   abstract-over-section TheParams TheType MixinSrcClauses SectionCanonicalInstance coq.abstract-indt-decl RDecl RDeclClosed _,
 
-  % coq.say RDecl RDeclClosed,
 
   if (get-option "primitive" tt)
     (@primitive! => log.coq.env.add-indt RDeclClosed R)