minor cleanup: extract known keys from has-mixin-instance

HB/common/database.elpi

@@ -14,13 +14,6 @@ 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.
 
@@ -146,16 +139,31 @@ undup-grefs  L UL :- std.do! [
   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,
+pred undup-sorts i:list sort, o:list sort.
+undup-sorts L R :- std.do! [
+
+  if (std.mem L prop) (R1 = [prop]) (R1 = []),
+  if (std.mem L sprop) (R2 = [sprop]) (R2 = []),
+  if (std.mem L (typ _)) (R3 = [typ _]) (R3 = []),
+
+  std.flatten [R1, R2, R3] R,
 ].
 
+% remove duplicates from a list of terms, but all the terms have to be global references
+pred undup-cs-patterns  i:list cs-pattern, o:list cs-pattern.
+undup-cs-patterns L R :- std.do! [
+  std.map-filter L (x\r\ x = cs-gref r) LGR,
+  undup-grefs LGR ULGR,
+  std.map ULGR (x\r\ r = cs-gref x) R1,
+
+  std.map-filter L (x\r\ x = cs-sort r) LS,
+  undup-sorts LS ULS,
+  std.map ULS (x\r\ r = cs-sort x) R2,
 
+  if (std.mem L cs-prod) (R3 = [cs-prod]) (R3 = []),
 
+  std.flatten [R1, R2, R3] R,
+].
 
 % Mixins can be topologically sorted according to their dependencies
 pred toposort-mixins i:list (w-args mixinname), o:list (w-args mixinname).
@@ -220,6 +228,9 @@ pred findall-has-mixin-instance o:list prop.
 findall-has-mixin-instance CL :-
    std.findall (has-mixin-instance  _ _ _) CL.
 
+pred has-mixin-instance_key i:prop, o:cs-pattern.
+has-mixin-instance_key (has-mixin-instance P _ _) P.
+
 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.

HB/common/utils.elpi

@@ -375,3 +375,10 @@ 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.
+
+pred cs-pattern->term i:cs-pattern, o:term.
+cs-pattern->term (cs-gref GR) T :- coq.env.global GR T.
+cs-pattern->term (cs-sort prop) (sort prop).
+cs-pattern->term (cs-sort sprop) (sort sprop).
+cs-pattern->term (cs-sort _) T :- coq.elaborate-skeleton {{ Type }} _ T ok.
+cs-pattern->term cs-prod T :- coq.elaborate-skeleton (prod `x` Ty_ x\ Bo_ x) _ T ok.

HB/instance.elpi

@@ -260,14 +260,21 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
 pred saturate-instances.
 saturate-instances :- std.do! [
   findall-has-mixin-instance ClausesHas,
+
+  std.map ClausesHas has-mixin-instance_key KL,
+  undup-cs-patterns KL UKL,
+  std.map UKL cs-pattern->term TL,
+
+  findall-classes AllClasses,
+  std.filter AllClasses (no-instance-for UKL) Classes,
+
   std.map ClausesHas mk-src-map Clauses,
-  std.map-filter Clauses mixin-src-w-cond_type TLD,
-  undup-terms TLD TL,
-  findall-classes Classes,
+
   Clauses => std.forall TL (t\ (declare-all-generic-type t Classes _)),
 ].
 
-
+pred no-instance-for i:list cs-pattern, i:class.
+no-instance-for _ _.
 
 /* ------------------------------------------------------------------------- */
 /* ----------------------------- private code ------------------------------ */