Merge pull request LPCIC#791 from Tragicus/primgref

Give constant to every primitive projection

Author: gares

elpi/coq-lib.elpi

@@ -510,7 +510,7 @@ coq.term->gref (global GR) GR :- !.
 coq.term->gref (pglobal GR _) GR :- !.
 coq.term->gref (app [Hd|_]) GR :- !, coq.term->gref Hd GR.
 coq.term->gref (let _ _ T x\x) GR :- !, coq.term->gref T GR.
-coq.term->gref (primitive (proj Proj _)) (const C) :- coq.env.primitive-projection? Proj C, !.
+coq.term->gref (primitive (proj Proj _)) (const C) :- coq.env.primitive-projection? Proj C _, !.
 :name "term->gref:fail"
 coq.term->gref Term _ :-
   fatal-error-w-data "term->gref: input has no global reference" Term.

src/rocq_elpi_builtins.ml

@@ -2361,13 +2361,30 @@ denote the same x as before.|};
   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)),
+    InOut(B.ioarg projection, "Projection",
+    InOut(B.ioarg constant, "Compatibility constant",
+    Out(int, "Index",
+    Read(global, "Relates a primitive projection to its compatibility constant. Index is set to the constructor argument extracted by the projection (starting from 0).")))),
+    (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 +! Names.Projection.(arg p + npars p) 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)) +! Names.Projection.(arg p + npars 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
+            let p = get_proj p in
+            !: p +? None +! Names.Projection.(arg p + npars p)))),
   DocAbove);
 
   LPDoc "-- Sorts (and their universe level, if applicable) ----------------";
@@ -2763,6 +2780,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|})),

tests/test_HOAS.v

@@ -221,7 +221,7 @@ Module P''.
 
   Elpi Query  lp:{{
     app[primitive (proj P _) | _] = {{X.(proj1 _)}},
-    coq.env.primitive-projection? P C,
+    coq.env.primitive-projection? P C _,
     global (const C) = {{proj1}}.
   }}.