From dfa99b152114271cf9fac4cab9d8663ac6ec078c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 May 2018 14:57:00 +0200 Subject: Fixes part 1 of #7462 (only-printing not to override existing interp rule). --- interp/notation.ml | 32 +++++++++++++++----------------- 1 file changed, 15 insertions(+), 17 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 4a6d2a154..76d0efb72 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -49,7 +49,6 @@ type notation_location = (DirPath.t * DirPath.t) * string type notation_data = { not_interp : interpretation; not_location : notation_location; - not_onlyprinting : bool; } type scope = { @@ -449,20 +448,21 @@ let warn_notation_overridden = let declare_notation_interpretation ntn scopt pat df ~onlyprint = let scope = match scopt with Some s -> s | None -> default_scope in let sc = find_scope scope in - let () = - if String.Map.mem ntn sc.notations then - let which_scope = match scopt with - | None -> mt () - | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in - warn_notation_overridden (ntn,which_scope) - in - let notdata = { - not_interp = pat; - not_location = df; - not_onlyprinting = onlyprint; - } in - let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in - let () = scope_map := String.Map.add scope sc !scope_map in + if not onlyprint then begin + let () = + if String.Map.mem ntn sc.notations then + let which_scope = match scopt with + | None -> mt () + | Some _ -> spc () ++ strbrk "in scope" ++ spc () ++ str scope in + warn_notation_overridden (ntn,which_scope) + in + let notdata = { + not_interp = pat; + not_location = df; + } in + let sc = { sc with notations = String.Map.add ntn notdata sc.notations } in + scope_map := String.Map.add scope sc !scope_map + end; begin match scopt with | None -> scope_stack := SingleNotation ntn :: !scope_stack | Some _ -> () @@ -487,7 +487,6 @@ let rec find_interpretation ntn find = function let find_notation ntn sc = let n = String.Map.find ntn (find_scope sc).notations in - let () = if n.not_onlyprinting then raise Not_found in (n.not_interp, n.not_location) let notation_of_prim_token = function @@ -631,7 +630,6 @@ let exists_notation_in_scope scopt ntn onlyprint r = try let sc = String.Map.find scope !scope_map in let n = String.Map.find ntn sc.notations in - onlyprint = n.not_onlyprinting && interpretation_eq n.not_interp r with Not_found -> false -- cgit v1.2.3 From 0acaa906367c02c57a6d70dd5d19eaea884b7568 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 May 2018 15:04:13 +0200 Subject: Fixes #7462, part 2 (only-printing not make believe parsing rule is declared). --- interp/notation.ml | 10 ++++++---- interp/notation.mli | 4 ++-- test-suite/bugs/closed/7462.v | 7 +++++++ vernac/metasyntax.ml | 6 +++--- 4 files changed, 18 insertions(+), 9 deletions(-) (limited to 'interp') diff --git a/interp/notation.ml b/interp/notation.ml index 76d0efb72..20e46bfe3 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -429,13 +429,15 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function (* Uninterpreted notation levels *) -let declare_notation_level ntn level = +let declare_notation_level ?(onlyprint=false) ntn level = if String.Map.mem ntn !notation_level_map then anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level."); - notation_level_map := String.Map.add ntn level !notation_level_map + notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map -let level_of_notation ntn = - String.Map.find ntn !notation_level_map +let level_of_notation ?(onlyprint=false) ntn = + let (level,onlyprint') = String.Map.find ntn !notation_level_map in + if onlyprint' && not onlyprint then raise Not_found; + level (* The mapping between notations and their interpretation *) diff --git a/interp/notation.mli b/interp/notation.mli index eac87414f..ccc67fe49 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -137,8 +137,8 @@ val availability_of_notation : scope_name option * notation -> local_scopes -> (** {6 Declare and test the level of a (possibly uninterpreted) notation } *) -val declare_notation_level : notation -> level -> unit -val level_of_notation : notation -> level (** raise [Not_found] if no level *) +val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit +val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *) (** {6 Miscellaneous} *) diff --git a/test-suite/bugs/closed/7462.v b/test-suite/bugs/closed/7462.v index 37af64caa..40ca39e38 100644 --- a/test-suite/bugs/closed/7462.v +++ b/test-suite/bugs/closed/7462.v @@ -4,3 +4,10 @@ Notation "$ x" := (@id nat x) (only parsing, at level 0). Notation "$ x" := (@id bool x) (only printing, at level 0). Check $1. (* Was: Error: Unknown interpretation for notation "$ _". *) + +(* Adding an only-printing notation should not let believe + that a parsing rule has been given *) + +Notation "$ x" := (@id bool x) (only printing, at level 0). +Notation "$ x" := (@id nat x) (only parsing, at level 0). +Check $1. (* Was: Error: Syntax Error: Lexer: Undefined token *) diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index feeca6075..76958b05f 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -738,12 +738,12 @@ let cache_one_syntax_extension se = let prec = se.synext_level in let onlyprint = se.synext_notgram.notgram_onlyprinting in try - let oldprec = Notation.level_of_notation ntn in + let oldprec = Notation.level_of_notation ~onlyprint ntn in if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec; with Not_found -> if is_active_compat se.synext_compat then begin (* Reserve the notation level *) - Notation.declare_notation_level ntn prec; + Notation.declare_notation_level ntn prec ~onlyprint; (* Declare the parsing rule *) if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules; (* Declare the notation rule *) @@ -1274,7 +1274,7 @@ exception NoSyntaxRule let recover_notation_syntax ntn = try - let prec = Notation.level_of_notation ntn in + let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in let pp_rule,_ = Notation.find_notation_printing_rule ntn in let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in let pa_rule = Notation.find_notation_parsing_rules ntn in -- cgit v1.2.3