API coq.CS.db-for for fast CS lookup

Changelog.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## UNRELEASED
+
+### API
+- New `coq.CS.db-for` to filter the CS db given a projection or a canonical
+  value, or both.
+
 ## [1.9.4] - 17-03-2021
 
 Requires Elpi 1.13 and Coq 8.13.

coq-builtin.elpi

@@ -712,6 +712,10 @@ external pred coq.CS.declare-instance i:gref.
 % [coq.CS.db Db] reads all instances
 external pred coq.CS.db o:list cs-instance.
 
+% [coq.CS.db-for Proj Value Db] reads all instances for a given Projection
+% or canonical Value, or both
+external pred coq.CS.db-for i:gref, i:cs-pattern, o:list cs-instance.
+
 % [coq.CS.canonical-projections StructureName Projections] given a record
 % StructureName lists all projections
 external pred coq.CS.canonical-projections i:inductive, 

src/coq_elpi_builtins.ml

@@ -1526,6 +1526,31 @@ Supported attributes:
      !: (Recordops.canonical_projections ()))),
   DocAbove);
 
+  MLCode(Pred("coq.CS.db-for",
+    In(unspec gref, "Proj",
+    In(unspec cs_pattern, "Value",
+    COut(!>> list cs_instance, "Db",
+    Read(global,"reads all instances for a given Projection or canonical Value, or both")))),
+  (fun proj value _ ~depth _ _ state ->
+    let env = get_global_env state in
+    (* This comes from recordops, it should be exported *)
+    let eq_cs_pattern env p1 p2 = let open Recordops in match p1, p2 with
+      | Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+      | Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
+      | Prod_cs, Prod_cs -> true
+      | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
+      | Default_cs, Default_cs -> true
+      | _ -> false in
+     match proj, value with
+     | Unspec, Unspec -> !: (Recordops.canonical_projections ())
+     | Given p, Unspec ->
+         (* This could be made more efficient by exposing the find methof of the CS db in Recordops *)
+         !: (Recordops.canonical_projections () |> List.filter (fun ((p1,_),_) -> Names.GlobRef.equal p p1))
+     | Unspec, Given v ->
+         !: (Recordops.canonical_projections () |> List.filter (fun ((_,v1),_) -> eq_cs_pattern env v v1))
+     | Given p, Given v -> !: (try [(p,v),snd @@ Recordops.lookup_canonical_conversion env (p,v)] with Not_found -> []))),
+  DocAbove);
+
     MLCode(Pred("coq.CS.canonical-projections",
     In(inductive, "StructureName",
     Out(list (option constant), "Projections",

tests/test_API.v

@@ -596,7 +596,18 @@ Definition myc1 : eq := mk_eq W1 Z1 3.
 
 Section CStest.
 Elpi Query lp:{{ coq.locate "myc1" GR, @local! => coq.CS.declare-instance GR. }}.
+
 Check (eq_op _ t1 t1).
+
+Elpi Query lp:{{ coq.locate "eq_op" P, coq.CS.db-for P _ [_,_] }}.
+
+Elpi Query lp:{{ coq.locate "W" W, coq.CS.db-for _ (cs-gref W) [_] }}.
+
+Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "Z1" W, coq.CS.db-for P (cs-gref W) L, coq.say L, L = [cs-instance P (cs-gref W) {{myc1}}] }}.
+
+Elpi Query lp:{{ coq.locate "eq_op" P, coq.locate "nat" W, coq.CS.db-for P (cs-gref W) [] }}.
+
+
 End CStest.
 
 Fail Check (eq_op _ t1 t1).