Add API for projections

src/coq_elpi_builtins.ml

@@ -2275,7 +2275,17 @@ denote the same x as before.|};
       CList.map (Option.map (fun x -> Constant x))))),
   DocAbove);
 
-  MLCode(Pred("coq.env.primitive-projections",
+  MLCode(Pred("coq.env.projection?",
+    In(constant, "Constant",
+    Out(B.int, "Number of parameters",
+    Easy "if the constant is a projection, returns the number of parameters of its record.")),
+    (fun c _ ~depth ->
+      let c = match c with Constant t -> t | _ -> raise No_clause in 
+      try !: ((Structures.Structure.find_from_projection c).nparams)
+      with Not_found -> raise No_clause)),
+  DocAbove);
+
+  MLCode(Pred("coq.env.primitive-projection",
     In(inductive, "StructureName",
     Out(list (option (pair projection int)), "Projections",
     Easy "given a record StructureName lists all primitive projections")),
@@ -2289,6 +2299,16 @@ denote the same x as before.|};
             Some (c, np + na))))))),
   DocAbove);
 
+  MLCode(Pred("coq.env.primitive-projection?",
+    In(projection, "Projection",
+    Out(constant, "Compatibility constant",
+    Easy "relates a projection to its compatibility constant.")),
+    (fun p _ ~depth ->
+      let c = Projection.constant p in 
+      try !: (ignore (Structures.Structure.find_from_projection c); Constant c)
+      with Not_found -> raise No_clause)),
+  DocAbove);
+
   LPDoc "-- Sorts (and their universe level, if applicable) ----------------";
   LPDoc {|Warning: universe polymorphism has to be considered experimental *E* as
 a feature, not just as a set of APIs. Unfortunately some of the

tests/test_HOAS.v

@@ -197,6 +197,38 @@ Definition x : foo := {| p1 := 3; p2 := false |}.
 Unset Primitive Projections.
 End P.
 
+
+Module P'.
+  Record s (T : Type) := {
+    proj1 : nat;
+    proj2 : nat
+  }.
+
+  Elpi Query  lp:{{
+    global (const C) = {{proj1}},
+    coq.env.projection? C 1.
+  }}.
+End P'.
+
+
+Module P''.
+  #[local] Set Primitive Projections.
+  Record s1 (T : Type) := {
+    proj1 : nat;
+    proj2 : nat
+  }.
+
+  Axiom (X : s1 nat).
+
+  Elpi Query  lp:{{
+    app[primitive (proj P _) | _] = {{X.(proj1 _)}},
+    coq.env.primitive-projection? P C,
+    global (const C) = {{proj1}}.
+  }}.
+
+End P''.
+
+
 Elpi Command primitive_proj.
 Elpi Accumulate lp:{{
   main [str Kind, trm (global (indt I)), trm T, int N, trm V] :- std.do! [