rewriting the function to remove duplicates and the test for it

HB/common/database.elpi

@@ -139,30 +139,25 @@ factories-provide FLwP MLwP :- std.do! [
   w-params.map UnsortedMLwP (p\t\ toposort-mixins) MLwP,
 ].
 
-% pred gref-set-undup i:list gref, i:coq.gref.set, o:coq.gref.set.
-%   gref-set-undup (Gr::LN) S US :-
-%       if (coq.gref.set.mem Gr S) 
-%           (gref-set-undup LN S US) 
-%           (std.do! [gref-set-undup LN S US1, coq.gref.set.add Gr (gref-set-undup LN S US1) US]).
-%   gref-set-undup [] E E1 :- E = E1.
-% pred undup-terms  i:list term, o:list term.
-% undup-terms [T|TL] UTL :-
-% filter TL (x\ coq.gref.list->set) UTL
-
-pred undup-gref  i:list gref, o:list gref.
-undup-gref [] [].
-undup-gref  [Te | Tl] Utl :- 
-  (coq.gref.list->set Tl TS), (coq.gref.set.mem Te TS), !, std.append [Te] Utl Utl.
-  undup-gref  [_ | TL] UTL :-  (undup-gref TL UTL).
-% % finds all unique types for which an instance was created
+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,
+].
 
+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,
+].
+
+% % finds all unique types for which an instance was created
 pred findall-cs-types o:list term.
 findall-cs-types TypeList :- std.do![
   std.findall (has-db-instance _) Clauses,
   std.map Clauses has-db-instance_type TypeListDup,
-  std.map TypeListDup coq.term->gref TGref,
-  undup-gref TGref UTgref,
-  std.map UTgref (coq.env.global ) TypeList,
+  undup-terms TypeListDup TypeList,
 ].
 
 

tests/findall_cs_type.v

@@ -3,29 +3,28 @@ From elpi Require Import elpi.
 
 HB.mixin Record m1 T := { default1 : T }.
 HB.mixin Record m2 T := { default1 : T }.
-
+HB.mixin Record m3 T := { default2 : T }.
+HB.mixin Record m4 T := { default3 : T }.
+HB.mixin Record m5 T := { default4 : T }.
 (* no types yet*)
 Elpi Query HB.instance lp:{{std.assert! (findall-cs-types []) "a type was found"}}.
 
-HB.instance Definition _ : m1 nat := m1.Build nat 1.
-HB.instance Definition _ : m2 nat := m2.Build nat 2.
 
-HB.instance Definition _ : m1 bool := m1.Build bool true.
 
-HB.instance Definition _ : m1 bool := m1.Build bool true.
 HB.instance Definition _ : m1 nat := m1.Build nat 1.
 HB.instance Definition _ : m2 nat := m2.Build nat 2.
-
 (*no duplicates *)
 Elpi Query HB.instance lp:{{
-    undup-gref [m1,m2] L,
-    std.assert! (std.last L m2) "no type",
-
+    std.assert! (findall-cs-types [X]) "no type",
+    std.assert! (X = {{nat}}) "wrong type".
 }}.
 
-HB.instance Definition _ : m1 bool := m1.Build bool true.
-
+HB.instance Definition _ : m4 bool := m4.Build bool true.
+HB.instance Definition _ : m5 nat := m5.Build nat 5.
+HB.instance Definition _ : m3 bool := m3.Build bool false.
 Elpi Query HB.instance lp:{{
-    std.assert! (findall-cs-types [X,Y]) "no type",
-    std.assert! (Y = {{bool}}) "wrong type".
+    findall-cs-types Clauses,
+    std.assert! (std.length Clauses 2) "wrong number of clauses",
+    std.assert! (X = {{bool}}) "wrong type",
+    std.assert! (Y = {{nat}}) "wrong type".
 }}.