From f1531b5deb0f2bbb5653bb6f02abf6a1896f399a Mon Sep 17 00:00:00 2001 From: Paul Steckler Date: Mon, 25 Sep 2017 13:03:36 -0400 Subject: BZ#5739, Allow level for leftmost nonterminal for printing-ony Notations --- CHANGES | 2 ++ test-suite/output/Notations3.out | 4 ++++ test-suite/output/Notations3.v | 7 +++++++ vernac/metasyntax.ml | 13 +++++++++---- 4 files changed, 22 insertions(+), 4 deletions(-) diff --git a/CHANGES b/CHANGES index ca5172d7b..84b847028 100644 --- a/CHANGES +++ b/CHANGES @@ -5,6 +5,8 @@ Notations - Recursive notations with the recursive pattern repeating on the right (e.g. "( x ; .. ; y ; z )") now supported. +- Notations with a specific level for the leftmost nonterminal, + when printing-only, are supported. Tactics diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index 65efe228a..6ef75dd13 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -124,3 +124,7 @@ return (1, 2, 3, 4) : nat !!! _ _ : nat, True : (nat -> Prop) * ((nat -> Prop) * Prop) +((*1).2).3 + : nat +*(1.2) + : nat diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index ea372ad1a..8c7bbe591 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -190,3 +190,10 @@ Check 1+1+1. (* Test presence of notation variables in the recursive parts (introduced in dfdaf4de) *) Notation "!!! x .. y , b" := ((fun x => b), .. ((fun y => b), True) ..) (at level 200, x binder). Check !!! (x y:nat), True. + +(* Allow level for leftmost nonterminal when printing-only, BZ#5739 *) + +Notation "* x" := (id x) (only printing, at level 15, format "* x"). +Notation "x . y" := (x + y) (only printing, at level 20, x at level 14, left associativity, format "x . y"). +Check (((id 1) + 2) + 3). +Check (id (1 + 2)). diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index c424b1d50..c17ba765e 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -984,7 +984,7 @@ let is_not_printable onlyparse nonreversible = function (warn_non_reversible_notation (); true) else onlyparse -let find_precedence lev etyps symbols = +let find_precedence lev etyps symbols onlyprint = let first_symbol = let rec aux = function | Break _ :: t -> aux t @@ -1002,8 +1002,13 @@ let find_precedence lev etyps symbols = | None -> [],0 | Some (NonTerminal x) -> (try match List.assoc x etyps with - | ETConstr _ -> - user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") + | ETConstr _ -> + if onlyprint then + if Option.is_empty lev then + user_err Pp.(str "Explicit level needed in only-printing mode when the level of the leftmost non-terminal is given.") + else [],Option.get lev + else + user_err Pp.(str "The level of the leftmost non-terminal cannot be changed.") | ETName | ETBigint | ETReference -> begin match lev with | None -> @@ -1127,7 +1132,7 @@ let compute_syntax_data df modifiers = let need_squash = not (List.equal Notation.symbol_eq symbols symbols_for_grammar) in let ntn_for_grammar = if need_squash then make_notation_key symbols_for_grammar else ntn_for_interp in if not onlyprint then check_rule_productivity symbols_for_grammar; - let msgs,n = find_precedence mods.level mods.etyps symbols in + let msgs,n = find_precedence mods.level mods.etyps symbols onlyprint in (* To globalize... *) let etyps = join_auxiliary_recursive_types recvars mods.etyps in let sy_typs, prec = -- cgit v1.2.3