API to fold/unfold primproj

Changelog.md

@@ -3,8 +3,10 @@
 ## UNRELEASED
 
 
-### HOAS:
-- Fix primitive projects are always folded
+### API:
+- New `coq.primitive.projection-unfolded` to fold/unfold a primitive projection.
+  Note that unfolded primitive projections are still compact terms, but they
+  are displayed as `match` expressions and some Ltac code can see that.
 
 ## [1.19.3] - 12/10/2023
 

apps/derive/elpi/lens.elpi

@@ -68,7 +68,8 @@ declare-lens Prefix I FieldName RawBody (lens-db I FieldName C):-
   % In order to support primitive records we call the elaborator, which
   % eventually compiles the match into primitive projections
   std.assert-ok! (coq.elaborate-skeleton RawBody Ty Body) "derive.lens generates illtyped term",
-  coq.env.add-const Name Body Ty @transparent! C,
+  (pi P P1 N\ copy (primitive (proj P N)) (primitive (proj P1 N)) :- coq.primitive.projection-unfolded P1 P) => copy Body Body1,
+  coq.env.add-const Name Body1 Ty @transparent! C,
   std.map {std.iota Nparams} (_\r\ r = maximal) Implicits,
   if (Nparams > 0)
     (@global! => coq.arguments.set-implicit (const C) [Implicits, []])

coq-builtin.elpi

@@ -1091,6 +1091,12 @@ external pred coq.float64->float i:float64, o:float.
 % on 64 bits. Currently, it should not fail.
 external pred coq.float->float64 i:float, o:float64.
 
+% [coq.primitive.projection-unfolded P PU] Relates a primitive projection P
+% to its unfolded version PU. PU is still a primitive projection, but it is
+% displayed as a match and some Ltac code can see that.
+external pred coq.primitive.projection-unfolded o:projection, 
+                                                o:projection.
+
 
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects

src/coq_elpi_HOAS.ml

@@ -722,8 +722,6 @@ type primitive_value =
   | Float64 of Float64.t
   | Projection of Projection.t
 
-let fold_projection p = Names.Projection.(make (repr p) false)
-
 let primitive_value : primitive_value API.Conversion.t =
   let module B = Coq_elpi_utils in
   let open API.AlgebraicData in  declare {
@@ -741,8 +739,8 @@ let primitive_value : primitive_value API.Conversion.t =
       B (fun x -> Float64 x),
       M (fun ~ok ~ko -> function Float64 x -> ok x | _ -> ko ()));
     K("proj","primitive projection",A(B.projection,A(API.BuiltInData.int,N)),
-      B (fun p n -> Projection (fold_projection p)),
-      M (fun ~ok ~ko -> function Projection p -> ok (fold_projection p) Names.Projection.(arg p + npars p) | _ -> ko ()));
+      B (fun p n -> Projection p),
+      M (fun ~ok ~ko -> function Projection p -> ok p Names.Projection.(arg p + npars p) | _ -> ko ()));
   ]
 } |> API.ContextualConversion.(!<)
 

src/coq_elpi_builtins.ml

@@ -2630,6 +2630,24 @@ declared as cumulative.|};
        !: (Float64.of_float f))),
   DocAbove);
 
+  MLCode(Pred("coq.primitive.projection-unfolded",
+    InOut(B.ioarg projection,"P",
+    InOut(B.ioarg projection,"PU",
+    Read(global, "Relates a primitive projection P to its unfolded version PU. PU is still a primitive projection, but it is displayed as a match and some Ltac code can see that."))),
+    (fun p q ~depth:_ coq_context _ _ ->
+      let test_folded = function Data x -> if Projection.unfolded x then raise No_clause | _ -> () in
+      let test_unfolded = function Data x -> if not (Projection.unfolded x) then raise No_clause | _ -> () in
+      test_folded p;
+      test_unfolded q;
+      match p, q with
+      | Data p, Data q ->
+          if Environ.QProjection.Repr.equal coq_context.env (Projection.repr p) (Projection.repr q) then ?: None +? None else raise No_clause
+      | NoData, NoData -> U.type_error "coq.projection.unfolded: got no input data"
+      | Data p, NoData -> ?: None +! Projection.(make (repr p) true)
+      | NoData, Data q -> !: Projection.(make (repr q) false) +? None
+      )),
+    DocAbove);
+
   LPCode {|
 % %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % API for extra logical objects