From 7149fef354d55f4b5012eac7efa15b4e7bac3d38 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 19 Dec 2019 12:45:28 +0100 Subject: Fix handling of recursive notations with custom entries Fixes #9532 Fixes #9490 --- .../03-notations/11311-custom-entries-recursive.rst | 5 +++++ parsing/extend.ml | 2 +- vernac/egramcoq.ml | 12 ++++++------ vernac/metasyntax.ml | 2 +- 4 files changed, 13 insertions(+), 8 deletions(-) create mode 100644 doc/changelog/03-notations/11311-custom-entries-recursive.rst diff --git a/doc/changelog/03-notations/11311-custom-entries-recursive.rst b/doc/changelog/03-notations/11311-custom-entries-recursive.rst new file mode 100644 index 0000000000..ae9888512d --- /dev/null +++ b/doc/changelog/03-notations/11311-custom-entries-recursive.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Recursive notations with custom entries were incorrectly parsing `constr` + instead of custom grammars (`#11311 `_ + by Maxime Dénès, fixes `#9532 `_, + `#9490 `_). diff --git a/parsing/extend.ml b/parsing/extend.ml index ed6ebe5aed..dcdaa25c33 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -54,7 +54,7 @@ type constr_prod_entry_key = | ETProdBigint (* Parsed as an (unbounded) integer *) | ETProdConstr of Constrexpr.notation_entry * (production_level * production_position) (* Parsed as constr or pattern, or a subentry of those *) | ETProdPattern of int (* Parsed as pattern as a binder (as subpart of a constr) *) - | ETProdConstrList of (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr *) + | ETProdConstrList of Constrexpr.notation_entry * (production_level * production_position) * string Tok.p list (* Parsed as non-empty list of constr, or subentries of those *) | ETProdBinderList of binder_entry_kind (* Parsed as non-empty list of local binders *) (** {5 AST for user-provided entries} *) diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml index e02f94629c..b65a126f55 100644 --- a/vernac/egramcoq.ml +++ b/vernac/egramcoq.ml @@ -247,7 +247,7 @@ type (_, _) entry = | TTReference : ('self, qualid) entry | TTBigint : ('self, string) entry | TTConstr : notation_entry * prod_info * 'r target -> ('r, 'r) entry -| TTConstrList : prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry +| TTConstrList : notation_entry * prod_info * string Tok.p list * 'r target -> ('r, 'r list) entry | TTPattern : int -> ('self, cases_pattern_expr) entry | TTOpenBinderList : ('self, local_binder_expr list) entry | TTClosedBinderList : string Tok.p list -> ('self, local_binder_expr list list) entry @@ -347,12 +347,12 @@ let symbol_of_target : type s. _ -> _ -> _ -> _ -> s target -> (s, s) mayrec_sym let symbol_of_entry : type s r. _ -> _ -> (s, r) entry -> (s, r) mayrec_symbol = fun assoc from typ -> match typ with | TTConstr (s, p, forpat) -> symbol_of_target s p assoc from forpat -| TTConstrList (typ', [], forpat) -> - begin match symbol_of_target InConstrEntry typ' assoc from forpat with +| TTConstrList (s, typ', [], forpat) -> + begin match symbol_of_target s typ' assoc from forpat with | MayRecNo s -> MayRecNo (Alist1 s) | MayRecMay s -> MayRecMay (Alist1 s) end -| TTConstrList (typ', tkl, forpat) -> - begin match symbol_of_target InConstrEntry typ' assoc from forpat with +| TTConstrList (s, typ', tkl, forpat) -> + begin match symbol_of_target s typ' assoc from forpat with | MayRecNo s -> MayRecNo (Alist1sep (s, make_sep_rules tkl)) | MayRecMay s -> MayRecMay (Alist1sep (s, make_sep_rules tkl)) end | TTPattern p -> MayRecNo (Aentryl (Constr.pattern, string_of_int p)) @@ -369,7 +369,7 @@ let interp_entry forpat e = match e with | ETProdBigint -> TTAny TTBigint | ETProdConstr (s,p) -> TTAny (TTConstr (s, p, forpat)) | ETProdPattern p -> TTAny (TTPattern p) -| ETProdConstrList (p, tkl) -> TTAny (TTConstrList (p, tkl, forpat)) +| ETProdConstrList (s, p, tkl) -> TTAny (TTConstrList (s, p, tkl, forpat)) | ETProdBinderList ETBinderOpen -> TTAny TTOpenBinderList | ETProdBinderList (ETBinderClosed tkl) -> TTAny (TTClosedBinderList tkl) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index e23522da9e..35681aed13 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -611,7 +611,7 @@ let expand_list_rule s typ tkl x n p ll = else if Int.equal i (p+n) then let hds = GramConstrListMark (p+n,true,p) :: hds - @ [GramConstrNonTerminal (ETProdConstrList (typ,tkl), Some x)] in + @ [GramConstrNonTerminal (ETProdConstrList (s, typ,tkl), Some x)] in distribute hds ll else distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @ -- cgit v1.2.3 From 515bdf52963c42f007178b608d8dc0707b340360 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 19 Dec 2019 12:50:15 +0100 Subject: Add test cases for #9490 and #9532 --- test-suite/bugs/bug_9490.v | 9 +++++++++ test-suite/bugs/bug_9532.v | 12 ++++++++++++ 2 files changed, 21 insertions(+) create mode 100644 test-suite/bugs/bug_9490.v create mode 100644 test-suite/bugs/bug_9532.v diff --git a/test-suite/bugs/bug_9490.v b/test-suite/bugs/bug_9490.v new file mode 100644 index 0000000000..a5def40c49 --- /dev/null +++ b/test-suite/bugs/bug_9490.v @@ -0,0 +1,9 @@ +Declare Custom Entry with_pattern. +Declare Custom Entry M_branch. +Notation "'with' | p1 | .. | pn 'end'" := + (cons p1 (.. (cons pn nil) ..)) + (in custom with_pattern at level 91, p1 custom M_branch at level 202, pn custom M_branch at level 202). +Notation "'bla'" := I (in custom M_branch at level 202). +Notation "'[use_with' l ]" := (l) (at level 0, l custom with_pattern at level 91). +Check [use_with with | bla end]. +Check [use_with with | bla | bla end]. diff --git a/test-suite/bugs/bug_9532.v b/test-suite/bugs/bug_9532.v new file mode 100644 index 0000000000..d198d45f2f --- /dev/null +++ b/test-suite/bugs/bug_9532.v @@ -0,0 +1,12 @@ +Declare Custom Entry atom. +Notation "1" := tt (in custom atom). +Notation "atom:( s )" := s (s custom atom). + +Declare Custom Entry expr. +Notation "expr:( s )" := s (s custom expr). +Notation "( x , y , .. , z )" := (@cons unit x (@cons unit y .. (@cons unit z (@nil unit)) ..)) + (in custom expr at level 0, x custom atom, y custom atom, z custom atom). + +Check atom:(1). +Check expr:((1,1)). +Check expr:((1,1,1)). -- cgit v1.2.3