Merge pull request #487 from LPCIC/fix-parsing-quotations

[quotations] check end of input (fix #468)
LPCIC · Jul 27, 2023 · df29085 · df29085
2 parents a25c989 + f7db0f5
commit df29085
Show file tree

Hide file tree

Showing 5 changed files with 11 additions and 5 deletions.
diff --git a/Changelog.md b/Changelog.md
@@ -34,6 +34,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
@@ -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/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
@@ -3437,7 +3437,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 ->

diff --git 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)