primproj are folded

Changelog.md

@@ -1,5 +1,11 @@
 # Changelog
 
+## UNRELEASED
+
+
+### HOAS:
+- Fix primitive projects are always folded
+
 ## [1.19.3] - 12/10/2023
 
 Requires Elpi 1.16.5 and Coq 8.18.

apps/derive/tests/test_lens.v

@@ -29,5 +29,32 @@ match goal with
 end.
 Abort.
 
+#[projections(primitive=yes)]
+Record R := MkR {
+  proj : nat;
+}.
+#[only(lens)] derive R.
 
+Lemma failing r :
+  r.(proj) = 0 ->
+  view R__proj r = r.(proj).
+Proof.
+  simpl.
+  intros Hpr.
+  rewrite Hpr.
+  reflexivity.
+Abort.
 
+Lemma working r :
+  match r with MkR r_proj => r_proj end = 0 ->
+  view R__proj r = match r with MkR r_proj => r_proj end.
+Proof.
+  elpi show.
+  simpl.
+  intros Hpr.
+  rewrite Hpr.
+  Fail reflexivity.
+  unfold proj.
+  rewrite Hpr.
+  reflexivity.
+Qed.

src/coq_elpi_HOAS.ml

@@ -722,6 +722,8 @@ 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 {
@@ -739,8 +741,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 p),
-      M (fun ~ok ~ko -> function Projection p -> ok p Names.Projection.(arg p + npars p) | _ -> ko ()));
+      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 ()));
   ]
 } |> API.ContextualConversion.(!<)