Merge pull request #414 from math-comp/saturate-filter

HB.saturate: take a cs pattern as a filter

HB/common/database.elpi

@@ -224,9 +224,9 @@ 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-has-mixin-instance i:cs-pattern,  o:list prop.
+findall-has-mixin-instance P CL :-
+   std.findall (has-mixin-instance P _ _) CL.
 
 pred has-mixin-instance_key i:prop, o:cs-pattern.
 has-mixin-instance_key (has-mixin-instance P _ _) P.

HB/instance.elpi

@@ -241,9 +241,10 @@ mk-factory-sort-factory AliasGR CSL :- std.do! [
 ].
 
 % create instances for all possible combinations of types and structure compatible 
-pred saturate-instances.
-saturate-instances :- std.do! [
-  findall-has-mixin-instance ClausesHas,
+pred saturate-instances i:cs-pattern.
+saturate-instances Filter :- std.do! [
+
+  findall-has-mixin-instance Filter ClausesHas,
 
   std.map ClausesHas has-mixin-instance_key KL,
   undup-cs-patterns KL UKL,

_CoqProject.test-suite

@@ -95,6 +95,8 @@ tests/unit/close_hole_term.v
 tests/unit/struct.v
 tests/factory_when_notation.v
 
+tests/saturate_on.v
+
 -R tests HB.tests
 -R examples HB.examples
 

structures.v

@@ -193,9 +193,8 @@ pred mixin-class o:mixinname, o:classname.
 % Coq's CS database (which is just for structures).
 pred mixin-src o:term, o:mixinname, o:term.
 
-% [has-mixin-instance P M G] states that G is a reference to an instance
-% which can be used to reconstruct an instance 
-% of the form [M P …] with eventually some parameters for P.
+% [has-mixin-instance K M G] states that G is a reference to an instance
+% of mixin M for subject K
 pred has-mixin-instance o:cs-pattern, o:mixinname, o:gref.
 
 %% database for HB.builders %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -690,7 +689,8 @@ Elpi Export HB.structure.
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 (* %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% *)
 
-(* [HB.saturate] saturates all instances w.r.t. the current hierarchy.
+(* [HB.saturate [key]] saturates all instances (of all known keys, if key is not
+   given) w.r.t. the current hierarchy.
 
    When two (unrelated) files are imported it might be that the instances
    declared in one file are sufficient to instantiate structures declared
@@ -715,8 +715,11 @@ Elpi Accumulate File "HB/instance.elpi".
 Elpi Accumulate File "HB/context.elpi".
 Elpi Accumulate File "HB/factory.elpi".
 Elpi Accumulate lp:{{
-main [] :- !, with-attributes (with-logging (instance.saturate-instances)).
-main _ :- coq.error "Usage: HB.saturate".
+main [] :- !, with-attributes (with-logging (instance.saturate-instances _)).
+main [str "Type"] :- !, with-attributes (with-logging (instance.saturate-instances (cs-sort _))).
+main [str K] :- !, coq.locate K GR, with-attributes (with-logging (instance.saturate-instances (cs-gref GR))).
+main [trm T] :- !, term->cs-pattern T P, with-attributes (with-logging (instance.saturate-instances P)).
+main _ :- coq.error "Usage: HB.saturate [key]".
 }}.
 Elpi Typecheck.
 Elpi Export HB.saturate.

tests/saturate_on.v

@@ -0,0 +1,19 @@
+From HB Require Import structures.
+
+HB.mixin Record HasPoint T := { default : T }.
+
+HB.instance Definition _ : HasPoint nat := HasPoint.Build nat 0.
+HB.instance Definition _ : HasPoint bool := HasPoint.Build bool false.
+HB.instance Definition _ A : HasPoint (list A) := HasPoint.Build (list A) nil.
+HB.instance Definition _ A : HasPoint Type := HasPoint.Build Type nat.
+
+HB.structure Definition Pointed  := { T of HasPoint T }.
+
+HB.saturate (list _).
+
+Fail Check nat : Pointed.type.
+Fail Check bool : Pointed.type.
+Check (list unit : Pointed.type).
+Fail Check Type : Pointed.type.
+
+