Merge pull request #521 from LPCIC/fix-HOAS-primproj

API to fold/unfold primproj

Author: gares

Changelog.md

@@ -14,6 +14,9 @@
 - New `coq.begin-synterp-group` and `coq.end-synterp-group` primitives
 - New `coq.replay-synterp-action-group` primitive (replaces `coq.replay-all-missing-synterp-actions` in conjunction with a group)
 - New `coq.replay-next-synterp-actions` to replay all synterp actions until the next beginning/end of a synterp group
+- 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.
 
 ## [2.0.2] - 01/02/2024
 

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, []])

apps/derive/tests/test_lens.v

@@ -29,5 +29,32 @@ match goal with
 end.
 Abort.
 
+#[projections(primitive=yes)]
+Record R := MkR {
+  proj : nat;
+}.
 
+Elpi derive.lens R "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.
+  simpl.
+  intros Hpr.
+  rewrite Hpr.
+  Fail reflexivity.
+  unfold proj.
+  rewrite Hpr.
+  reflexivity.
+Qed.

coq-builtin.elpi

@@ -1102,6 +1102,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_builtins.ml

@@ -2557,6 +2557,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