Merge pull request #644 from FissoreD/add-proj-API

Add API for projections

Changelog.md

@@ -19,6 +19,7 @@ Requires Elpi 1.19.2 and Coq 8.19 or Coq 8.20.
 - New `coq.*.set.min`, `coq.*.set.max`, `coq.*.set.choose`, `coq.*.set.fold`,
   `coq.*.set.partition`
 - New `coq.*.map.fold`
+- New `coq.env.projection?` and `coq-env.primitive-projection?`
 
 ### HOAS
 - New `primitive (pstring S)` in Coq 8.20

builtin-doc/coq-builtin.elpi

@@ -910,11 +910,19 @@ external pred coq.env.end-section .
 % StructureName lists all projections
 external pred coq.env.projections i:inductive, o:list (option constant).
 
+% [coq.env.projection? Constant Number of parameters] if the constant is a
+% projection, returns the number of parameters of its record.
+external pred coq.env.projection? i:constant, o:int.
+
 % [coq.env.primitive-projections StructureName Projections] given a record
 % StructureName lists all primitive projections
 external pred coq.env.primitive-projections i:inductive, 
                                             o:list (option (pair projection int)).
 
+% [coq.env.primitive-projection? Projection Compatibility constant] relates
+% a projection to its compatibility constant.
+external pred coq.env.primitive-projection? i:projection, o:constant.
+
 % -- Sorts (and their universe level, if applicable) ----------------
 
 % Warning: universe polymorphism has to be considered experimental *E* as

src/coq_elpi_builtins.ml

@@ -2275,6 +2275,16 @@ denote the same x as before.|};
       CList.map (Option.map (fun x -> Constant x))))),
   DocAbove);
 
+  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-projections",
     In(inductive, "StructureName",
     Out(list (option (pair projection int)), "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! [