Relax lookahead test for ltac2 { foo with ... } to allow qualids

SkySkimmer · Sep 28, 2023 · 41c59ab · 41c59ab
1 parent 045c362
commit 41c59ab
Show file tree

Hide file tree

Showing 7 changed files with 23 additions and 8 deletions.
diff --git a/doc/tools/docgram/common.edit_mlg b/doc/tools/docgram/common.edit_mlg
@@ -161,7 +161,7 @@ DELETE: [
 | test_array_opening
 | test_array_closing
 | test_variance_ident
-| test_ident_with_or_lpar_or_rbrac
+| test_qualid_with_or_lpar_or_rbrac
 | test_leftsquarebracket_equal
 
 (* unused *)

diff --git a/doc/tools/docgram/fullGrammar b/doc/tools/docgram/fullGrammar
@@ -2705,7 +2705,7 @@ ltac2_expr0: [
 | "(" ")"      (* ltac2 plugin *)
 | array_literal      (* ltac2 plugin *)
 | list_literal      (* ltac2 plugin *)
-| "{" test_ident_with_or_lpar_or_rbrac ltac2_expr0 "with" tac2rec_fieldexprs "}"      (* ltac2 plugin *)
+| "{" test_qualid_with_or_lpar_or_rbrac ltac2_expr0 "with" tac2rec_fieldexprs "}"      (* ltac2 plugin *)
 | "{" tac2rec_fieldexprs "}"      (* ltac2 plugin *)
 | G_LTAC2_tactic_atom      (* ltac2 plugin *)
 ]

diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml
@@ -105,6 +105,12 @@ struct
 
   let lk_ident_list = lk_list lk_ident
 
+  let lk_field n kwstate strm = match LStream.peek_nth kwstate n strm with
+    | Tok.FIELD _ -> Some (n+1)
+    | _ -> None
+
+  let lk_qualid = lk_ident >> lk_list lk_field
+
 end
 
 (** Grammar extensions *)

diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
@@ -36,6 +36,7 @@ module Lookahead : sig
   val lk_nat : t
   val lk_ident : t
   val lk_name : t
+  val lk_qualid : t
   val lk_ident_except : string list -> t
   val lk_ident_list : t
 end

diff --git a/plugins/ltac2/g_ltac2.mlg b/plugins/ltac2/g_ltac2.mlg
@@ -77,10 +77,10 @@ let test_ltac1_env =
     lk_ident_list >> lk_kw "|-"
   end
 
-let test_ident_with_or_lpar_or_rbrac =
+let test_qualid_with_or_lpar_or_rbrac =
   let open Pcoq.Lookahead in
-  to_entry "test_ident_with_or_lpar_or_rbrac" begin
-    (lk_ident >> lk_kw "with") <+> lk_kw "(" <+> lk_kw "{"
+  to_entry "test_qualid_with_or_lpar_or_rbrac" begin
+    (lk_qualid >> lk_kw "with") <+> lk_kw "(" <+> lk_kw "{"
   end
 
 let test_array_opening =
@@ -226,7 +226,7 @@ GRAMMAR EXTEND Gram
         { CAst.make ~loc @@ CTacCst (AbsKn (Tuple 0)) }
       | a = array_literal -> { a }
       | a = list_literal -> { a }
-      | "{"; test_ident_with_or_lpar_or_rbrac; e = ltac2_expr LEVEL "0"; "with"; a = tac2rec_fieldexprs; "}" ->
+      | "{"; test_qualid_with_or_lpar_or_rbrac; e = ltac2_expr LEVEL "0"; "with"; a = tac2rec_fieldexprs; "}" ->
         { CAst.make ~loc @@ CTacRec (Some e, a) }
       | "{"; a = tac2rec_fieldexprs; "}" ->
         { CAst.make ~loc @@ CTacRec (None, a) }

diff --git a/plugins/ltac2/g_ltac2.mli b/plugins/ltac2/g_ltac2.mli
@@ -22,8 +22,6 @@ val test_dollar_ident : unit Pcoq.Entry.t
 
 val test_ltac1_env : unit Pcoq.Entry.t
 
-val test_ident_with_or_lpar_or_rbrac : unit Pcoq.Entry.t
-
 val test_array_opening : unit Pcoq.Entry.t
 
 val test_array_closing : unit Pcoq.Entry.t

diff --git a/test-suite/ltac2/default_record.v b/test-suite/ltac2/default_record.v
@@ -16,3 +16,13 @@ Fail Ltac2 foobar () := { { a := (); b := () } with aa := () }.
 
 Ltac2 varvar v := { v with aa := () }.
 Print varvar.
+
+(* From #17764 *)
+Module Point.
+  Ltac2 Type t := { x : int ; y : int }.
+
+  Ltac2 origin : t := { x := 0; y := 0; }.
+
+End Point.
+
+Ltac2 Eval { Point.origin with Point.y := 1; }.