From fe059721ddfd710ae3fceb20194376d66097cf88 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Jul 2023 14:12:32 +0200 Subject: [PATCH 1/2] [quotations] check end of input (fix #468) Before {{ foo.x }} was just discarding ".x" --- Changelog.md | 3 +++ apps/derive/elpi/eqbcorrect.elpi | 4 ++-- src/coq_elpi_glob_quotation.ml | 4 +++- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/Changelog.md b/Changelog.md index 2f1d75bba..eafa11537 100644 --- a/Changelog.md +++ b/Changelog.md @@ -33,6 +33,9 @@ - Change propagate type constraints in `Prop` inward (Coq 8.17 only). Eg. `Check (T -> _) : Prop` fails in 8.17 since `_` is assumed to be in `Type`. We propagate the constraint ourselves across `->`, `/\`, `\/` and `~`. +- Quotations `{{ ... }}` are now parsed by Coq ensuring the end of input is + reached. Spurious text results in a parse error. For example `{{ f ) }}` + is no more accepted, as well as `{{ _.x }}` ### Vernacular - New `Elpi Print` also print the program in `.txt` format diff --git a/apps/derive/elpi/eqbcorrect.elpi b/apps/derive/elpi/eqbcorrect.elpi index d2c529305..dfa4d8360 100644 --- a/apps/derive/elpi/eqbcorrect.elpi +++ b/apps/derive/elpi/eqbcorrect.elpi @@ -307,10 +307,10 @@ args (stop TY) K As Hs Bs 0 {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- % no tri eqb-fields T T EqbFields, std.assert! (common-body Common) "anomaly, no let for common body proof", coq.mk-app Common [K,{{ fun (x : lp:Fields_t (lp:Tag lp:K)) => lp:(Proof x) }}] B, - @pi-decl `x` {{ lp:Fields_t (lp:Tag lp:K)) }} x\ + @pi-decl `x` {{ lp:Fields_t (lp:Tag lp:K) }} x\ HYP = (x\ {{ @eq bool (lp:EqbFields (lp:Tag lp:K) (lp:Fields lp:K) lp:x) true }}), GOAL = (x\ {{ @eq (option lp:T) (@Some lp:T lp:K) (lp:Construct (lp:Tag lp:K) lp:x) }}), - correct-proof x {{ lp:Fields_t (lp:Tag lp:K)) }} HYP GOAL As Bs Hs (Proof x) + correct-proof x {{ lp:Fields_t (lp:Tag lp:K) }} HYP GOAL As Bs Hs (Proof x) ]. args (stop TY) K _As _Hs _Bs _ {{ lp:B : lp:Pred_on lp:T lp:Cmp lp:K }} :- config {{ @eqb_correct }} Pred_on _Pred_body Solver _Db, !, std.do! [ diff --git a/src/coq_elpi_glob_quotation.ml b/src/coq_elpi_glob_quotation.ml index 60ad5cdce..0f65f4ce3 100644 --- a/src/coq_elpi_glob_quotation.ml +++ b/src/coq_elpi_glob_quotation.ml @@ -377,10 +377,12 @@ let rec gterm2lp ~depth state x = | GArray _ -> nYI "(glob)HOAS persistent arrays" ;; +let lconstr_eoi = Pcoq.eoi_entry Pcoq.Constr.lconstr + let coq_quotation ~depth state loc src = let ce = try - Pcoq.parse_string ~loc:(to_coq_loc loc) Pcoq.Constr.lconstr src + Pcoq.parse_string ~loc:(to_coq_loc loc) lconstr_eoi src with e -> CErrors.user_err Pp.(str(API.Ast.Loc.show loc) ++ spc() ++ CErrors.print_no_report e) From f7db0f56a7aa3b30b614b49c4cd9f3888f2dfb74 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 27 Jul 2023 16:08:16 +0200 Subject: [PATCH 2/2] fix cbv doc --- coq-builtin.elpi | 3 ++- src/coq_elpi_builtins.ml | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/coq-builtin.elpi b/coq-builtin.elpi index 89b3ca746..2ad5fe7d1 100644 --- a/coq-builtin.elpi +++ b/coq-builtin.elpi @@ -1462,7 +1462,8 @@ external pred coq.reduction.lazy.norm i:term, o:term. % beta and iota redexes external pred coq.reduction.lazy.bi-norm i:term, o:term. -% [coq.reduction.cbv.norm T Tred] Puts T in weak head normal form. +% [coq.reduction.cbv.norm T Tred] Puts T in normal form using the call by +% value strategy. % Supported attributes: % - @redflags! (default coq.redflags.all) external pred coq.reduction.cbv.norm i:term, o:term. diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index c1b4c76b6..d00b7eab3 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -3386,7 +3386,7 @@ Supported attributes: MLCode(Pred("coq.reduction.cbv.norm", CIn(term,"T", COut(term,"Tred", - Read(proof_context, {|Puts T in weak head normal form. + Read(proof_context, {|Puts T in normal form using the call by value strategy. Supported attributes: - @redflags! (default coq.redflags.all)|}))), (fun t _ ~depth proof_context constraints state ->