From f22f3bbec5881f68e07fe95baa14a0bdc73e490c Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Wed, 6 Mar 2024 15:45:23 +0100
Subject: [PATCH] HB.saturate: take a cs pattern as a filter

---
 HB/common/database.elpi |  6 +++---
 HB/instance.elpi        |  7 ++++---
 _CoqProject.test-suite  |  2 ++
 structures.v            | 15 +++++++++------
 tests/saturate_on.v     | 19 +++++++++++++++++++
 5 files changed, 37 insertions(+), 12 deletions(-)
 create mode 100644 tests/saturate_on.v

diff --git a/HB/common/database.elpi b/HB/common/database.elpi
index d583b4c3..f8870473 100644
--- a/HB/common/database.elpi
+++ b/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.
diff --git a/HB/instance.elpi b/HB/instance.elpi
index 2eec1d08..2426f14b 100644
--- a/HB/instance.elpi
+++ b/HB/instance.elpi
@@ -226,9 +226,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,
diff --git a/_CoqProject.test-suite b/_CoqProject.test-suite
index d60c9bb6..f59e999a 100644
--- a/_CoqProject.test-suite
+++ b/_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
 
diff --git a/structures.v b/structures.v
index 027c1442..5a8a81e0 100644
--- a/structures.v
+++ b/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.
diff --git a/tests/saturate_on.v b/tests/saturate_on.v
new file mode 100644
index 00000000..f39798df
--- /dev/null
+++ b/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.
+
+