From 4ab668100be546bb80ed4219ca304cd2c74ce6f5 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Oct 2023 14:50:23 +0200 Subject: [PATCH 1/2] primproj are folded --- Changelog.md | 6 ++++++ apps/derive/tests/test_lens.v | 27 +++++++++++++++++++++++++++ src/coq_elpi_HOAS.ml | 6 ++++-- 3 files changed, 37 insertions(+), 2 deletions(-) diff --git a/Changelog.md b/Changelog.md index 39ce8a438..ae645f7d6 100644 --- a/Changelog.md +++ b/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. diff --git a/apps/derive/tests/test_lens.v b/apps/derive/tests/test_lens.v index 4a8d59553..87ddcabca 100644 --- a/apps/derive/tests/test_lens.v +++ b/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. diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index 8c65bd859..bdd185732 100644 --- a/src/coq_elpi_HOAS.ml +++ b/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.(!<) From ed68f5474493ddef5086726b63dc0162d4b165ae Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Oct 2023 21:39:03 +0200 Subject: [PATCH 2/2] API to fold/unfold primproj --- Changelog.md | 6 ++++-- apps/derive/elpi/lens.elpi | 3 ++- coq-builtin.elpi | 6 ++++++ src/coq_elpi_HOAS.ml | 6 ++---- src/coq_elpi_builtins.ml | 18 ++++++++++++++++++ 5 files changed, 32 insertions(+), 7 deletions(-) diff --git a/Changelog.md b/Changelog.md index ae645f7d6..a5c6285bd 100644 --- a/Changelog.md +++ b/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 diff --git a/apps/derive/elpi/lens.elpi b/apps/derive/elpi/lens.elpi index 62ddb222a..371615f12 100644 --- a/apps/derive/elpi/lens.elpi +++ b/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, []]) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index fa4f798d4..1ea634521 100644 --- a/coq-builtin.elpi +++ b/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 diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml index bdd185732..8c65bd859 100644 --- a/src/coq_elpi_HOAS.ml +++ b/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.(!<) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index ebb75198c..a048819d5 100644 --- a/src/coq_elpi_builtins.ml +++ b/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