make primitive-projection? bidirectional and adds canonical-projection?

Author: Tragicus

src/rocq_elpi_builtins.ml

@@ -2361,10 +2361,27 @@ denote the same x as before.|};
   DocAbove);
 
   MLCode(Pred("coq.env.primitive-projection?",
-    In(projection, "Projection",
-    Out(constant, "Compatibility constant",
-    Easy "relates a primitive projection to its compatibility constant.")),
-    (fun p _ ~depth -> !: (Constant (Projection.constant p)))),
+    InOut(B.ioarg projection, "Projection",
+    InOut(B.ioarg constant, "Compatibility constant",
+    Read(global, "Relates a primitive projection to its compatibility constant."))),
+    (fun p c ~depth coq_context _ _ ->
+      match p, c with
+      | _, Data (Variable c) -> raise No_clause
+      | Data p, Data (Constant c) ->
+          if Constant.equal (Projection.constant p) c then ?: None +? None else raise No_clause
+      | NoData, NoData -> U.type_error "coq.env.primitive-projection?: got no input data"
+      | Data p, NoData -> ?: None +! (Constant (Projection.constant p))
+      | NoData, Data (Constant c) ->
+          (match Environ.constant_opt_value_in coq_context.env (UVars.in_punivs c) with
+          | None -> raise No_clause
+          | Some p ->
+            let rec get_proj c =
+              match Constr.kind c with
+              | Lambda (_, _, t) -> get_proj t
+              | App (hd, _) -> get_proj hd
+              | Proj (p, _, _) -> p
+              | _ -> raise No_clause
+            in !: (get_proj p) +? None))),
   DocAbove);
 
   LPDoc "-- Sorts (and their universe level, if applicable) ----------------";
@@ -2760,6 +2777,17 @@ Supported attributes:
          with Not_found -> !: [])),
   DocAbove);
 
+  MLCode(Pred("coq.CS.canonical-projection?",
+    In(constant, "Projection",
+    Easy "Tells if the projection can be used for CS inference."),
+    (fun c ~depth ->
+      match c with
+      | Variable _ -> raise No_clause
+      | Constant c ->
+        try ignore (Structures.Structure.find_from_projection c)
+        with Not_found -> raise No_clause)),
+  DocAbove);
+
   MLCode(Pred("coq.TC.declare-class",
     In(gref, "GR",
     Full(global, {|Declare GR as a type class|})),