aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/texmacspp.ml3
-rw-r--r--intf/vernacexpr.mli3
-rw-r--r--lib/flags.ml27
-rw-r--r--lib/flags.mli1
-rw-r--r--parsing/g_vernac.ml45
-rw-r--r--printing/ppvernac.ml8
-rw-r--r--test-suite/bugs/closed/4798.v3
-rw-r--r--toplevel/metasyntax.ml75
8 files changed, 80 insertions, 45 deletions
diff --git a/ide/texmacspp.ml b/ide/texmacspp.ml
index 53a29008a..9de1df9f1 100644
--- a/ide/texmacspp.ml
+++ b/ide/texmacspp.ml
@@ -189,7 +189,8 @@ match sm with
end
| SetEntryType (s, _) -> ["entrytype", s]
| SetOnlyPrinting -> ["onlyprinting", ""]
- | SetOnlyParsing v -> ["compat", Flags.pr_version v]
+ | SetOnlyParsing -> ["onlyparsing", ""]
+ | SetCompatVersion v -> ["compat", Flags.pr_version v]
| SetFormat (system, (loc, s)) ->
let start, stop = unlock loc in
["format-"^system, s; "begin", start; "end", stop]
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 6df85f076..1063a74d9 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -211,8 +211,9 @@ type syntax_modifier =
| SetLevel of int
| SetAssoc of Extend.gram_assoc
| SetEntryType of string * Extend.simple_constr_prod_entry_key
- | SetOnlyParsing of Flags.compat_version
+ | SetOnlyParsing
| SetOnlyPrinting
+ | SetCompatVersion of Flags.compat_version
| SetFormat of string * string located
type proof_end =
diff --git a/lib/flags.ml b/lib/flags.ml
index d29064c97..af55e9e2b 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -112,17 +112,22 @@ type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
let compat_version = ref Current
-let version_strictly_greater v = match !compat_version, v with
-| V8_2, (V8_2 | V8_3 | V8_4 | V8_5 | Current) -> false
-| V8_3, (V8_3 | V8_4 | V8_5 | Current) -> false
-| V8_4, (V8_4 | V8_5 | Current) -> false
-| V8_5, (V8_5 | Current) -> false
-| Current, Current -> false
-| V8_3, V8_2 -> true
-| V8_4, (V8_2 | V8_3) -> true
-| V8_5, (V8_2 | V8_3 | V8_4) -> true
-| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> true
-
+let version_compare v1 v2 = match v1, v2 with
+| V8_2, V8_2 -> 0
+| V8_2, (V8_3 | V8_4 | V8_5 | Current) -> -1
+| V8_3, V8_2 -> 1
+| V8_3, V8_3 -> 0
+| V8_3, (V8_4 | V8_5 | Current) -> -1
+| V8_4, (V8_2 | V8_3) -> 1
+| V8_4, V8_4 -> 0
+| V8_4, (V8_5 | Current) -> -1
+| V8_5, (V8_2 | V8_3 | V8_4) -> 1
+| V8_5, V8_5 -> 0
+| V8_5, Current -> -1
+| Current, Current -> 0
+| Current, (V8_2 | V8_3 | V8_4 | V8_5) -> 1
+
+let version_strictly_greater v = version_compare !compat_version v > 0
let version_less_or_equal v = not (version_strictly_greater v)
let pr_version = function
diff --git a/lib/flags.mli b/lib/flags.mli
index 839c252cb..9dc0c9c04 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -64,6 +64,7 @@ val univ_print : bool ref
type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | Current
val compat_version : compat_version ref
+val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index b0b656acf..1a4012891 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -1115,10 +1115,9 @@ GEXTEND Gram
| IDENT "right"; IDENT "associativity" -> SetAssoc RightA
| IDENT "no"; IDENT "associativity" -> SetAssoc NonA
| IDENT "only"; IDENT "printing" -> SetOnlyPrinting
- | IDENT "only"; IDENT "parsing" ->
- SetOnlyParsing Flags.Current
+ | IDENT "only"; IDENT "parsing" -> SetOnlyParsing
| IDENT "compat"; s = STRING ->
- SetOnlyParsing (Coqinit.get_compat_version s)
+ SetCompatVersion (Coqinit.get_compat_version s)
| IDENT "format"; s1 = [s = STRING -> (!@loc,s)];
s2 = OPT [s = STRING -> (!@loc,s)] ->
begin match s1, s2 with
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 1d8dcabcc..503b29aaf 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -367,8 +367,8 @@ module Make
| SetAssoc NonA -> keyword "no associativity"
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
| SetOnlyPrinting -> keyword "only printing"
- | SetOnlyParsing Flags.Current -> keyword "only parsing"
- | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+ | SetOnlyParsing -> keyword "only parsing"
+ | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
| SetFormat("text",s) -> keyword "format " ++ pr_located qs s
| SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
@@ -1002,13 +1002,13 @@ module Make
)
| VernacHints (_, dbnames,h) ->
return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
+ | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
return (
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
pr_syntax_modifiers
- (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
+ (match compat with None -> [] | Some v -> [SetCompatVersion v]))
)
| VernacDeclareImplicits (q,[]) ->
return (
diff --git a/test-suite/bugs/closed/4798.v b/test-suite/bugs/closed/4798.v
new file mode 100644
index 000000000..dbc3d46fc
--- /dev/null
+++ b/test-suite/bugs/closed/4798.v
@@ -0,0 +1,3 @@
+Check match 2 with 0 => 0 | S n => n end.
+Notation "|" := 1 (compat "8.4").
+Check match 2 with 0 => 0 | S n => n end. (* fails *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index a1edb7139..ce8798c71 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -673,8 +673,13 @@ type syntax_extension = {
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
synext_extra : (string * string) list;
+ synext_compat : Flags.compat_version option;
}
+let is_active_compat = function
+| None -> true
+| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
+
type syntax_extension_obj = locality_flag * syntax_extension list
let cache_one_syntax_extension se =
@@ -685,13 +690,15 @@ let cache_one_syntax_extension se =
let oldprec = Notation.level_of_notation ntn in
if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
with Not_found ->
- (* Reserve the notation level *)
- Notation.declare_notation_level ntn prec;
- (* Declare the parsing rule *)
- if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
- (* Declare the notation rule *)
- Notation.declare_notation_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+ if is_active_compat se.synext_compat then begin
+ (* Reserve the notation level *)
+ Notation.declare_notation_level ntn prec;
+ (* Declare the parsing rule *)
+ if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
+ (* Declare the notation rule *)
+ Notation.declare_notation_rule ntn
+ ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+ end
let cache_syntax_extension (_, (_, sy)) =
List.iter cache_one_syntax_extension sy
@@ -725,9 +732,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
let interp_modifiers modl =
let onlyparsing = ref false in
let onlyprinting = ref false in
+ let compat = ref None in
let rec interp assoc level etyps format extra = function
| [] ->
- (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra)
+ (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra)
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
@@ -749,12 +757,15 @@ let interp_modifiers modl =
| SetAssoc a :: l ->
if not (Option.is_empty assoc) then error"An associativity is given more than once.";
interp (Some a) level etyps format extra l
- | SetOnlyParsing _ :: l ->
+ | SetOnlyParsing :: l ->
onlyparsing := true;
interp assoc level etyps format extra l
| SetOnlyPrinting :: l ->
onlyprinting := true;
interp assoc level etyps format extra l
+ | SetCompatVersion v :: l ->
+ compat := Some v;
+ interp assoc level etyps format extra l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty format) then error "A format is given more than once.";
interp assoc level etyps (Some s) extra l
@@ -763,7 +774,7 @@ let interp_modifiers modl =
in interp None None [] None [] modl
let check_infix_modifiers modifiers =
- let (_, _, t, _, _, _, _) = interp_modifiers modifiers in
+ let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in
if not (List.is_empty t) then
error "Explicit entry level or type unexpected in infix notation."
@@ -775,20 +786,25 @@ let check_useless_entry_types recvars mainvars etyps =
| _ -> ()
let not_a_syntax_modifier = function
-| SetOnlyParsing _ -> true
+| SetOnlyParsing -> true
| SetOnlyPrinting -> true
+| SetCompatVersion _ -> true
| _ -> false
let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
let is_only_parsing mods =
- let test = function SetOnlyParsing _ -> true | _ -> false in
+ let test = function SetOnlyParsing -> true | _ -> false in
List.exists test mods
let is_only_printing mods =
let test = function SetOnlyPrinting -> true | _ -> false in
List.exists test mods
+let get_compat_version mods =
+ let test = function SetCompatVersion v -> Some v | _ -> None in
+ try Some (List.find_map test mods) with Not_found -> None
+
(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type etyps (x,typ) =
@@ -966,7 +982,7 @@ let remove_curly_brackets l =
in aux true l
let compute_syntax_data df modifiers =
- let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in
+ let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in
let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
let toks = split_notation_string df in
let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -992,12 +1008,12 @@ let compute_syntax_data df modifiers =
let sy_data = (n,sy_typs,symbols',fmt) in
let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
- let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in
+ let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in
(* Return relevant data for interpretation and for parsing/printing *)
(msgs,i_data,i_typs,sy_fulldata,extra)
let compute_pure_syntax_data df mods =
- let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
+ let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
(Feedback.msg_warning ?loc:None,
@@ -1014,6 +1030,7 @@ type notation_obj = {
notobj_interp : interpretation;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
+ notobj_compat : Flags.compat_version option;
notobj_notation : notation * notation_location;
}
@@ -1024,7 +1041,9 @@ let open_notation i (_, nobj) =
let scope = nobj.notobj_scope in
let (ntn, df) = nobj.notobj_notation in
let pat = nobj.notobj_interp in
- if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
+ let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in
+ let active = is_active_compat nobj.notobj_compat in
+ if Int.equal i 1 && fresh && active then begin
(* Declare the interpretation *)
let onlyprint = nobj.notobj_onlyprint in
let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
@@ -1094,7 +1113,9 @@ let recover_syntax ntn =
synext_notation = ntn;
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
- synext_extra = pp_extra_rules }
+ synext_extra = pp_extra_rules;
+ synext_compat = None;
+ }
with Not_found ->
raise NoSyntaxRule
@@ -1128,7 +1149,7 @@ let make_pp_rule (n,typs,symbols,fmt) =
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
| Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
-let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint =
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat =
let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in
let pp_rule = make_pp_rule sy_data in
let sy = {
@@ -1137,6 +1158,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint =
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
synext_extra = extra;
+ synext_compat = compat;
} in
(* By construction, the rule for "{ _ }" is declared, but we need to
redeclare it because the file where it is declared needs not be open
@@ -1153,9 +1175,9 @@ let to_map l =
let add_notation_in_scope local df c mods scope =
let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
(* Prepare the interpretation *)
- let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in
+ let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in
(* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sy_data extra onlyprint in
+ let sy_rules = make_syntax_rules sy_data extra onlyprint compat in
let i_vars = make_internalization_vars recvars mainvars i_typs in
let nenv = {
ninterp_var_type = to_map i_vars;
@@ -1173,6 +1195,7 @@ let add_notation_in_scope local df c mods scope =
(** Order is important here! *)
notobj_onlyparse = onlyparse;
notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
(* Ready to change the global state *)
@@ -1181,7 +1204,7 @@ let add_notation_in_scope local df c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
df'
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint =
+let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
@@ -1212,6 +1235,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
(** Order is important here! *)
notobj_onlyparse = onlyparse;
notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
Lib.add_anonymous_leaf (inNotation notation);
@@ -1221,19 +1245,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
let add_syntax_extension local ((loc,df),mods) =
let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in
- let sy_rules = make_syntax_rules sy_data extra onlyprint in
+ let sy_rules = make_syntax_rules sy_data extra onlyprint None in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
let add_notation_interpretation ((loc,df),c,sc) =
- let df' = add_notation_interpretation_core false df c sc false false in
+ let df' = add_notation_interpretation_core false df c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
- (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ());
+ (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
error "Parsing rule for this notation has to be previously declared.");
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
@@ -1246,7 +1270,8 @@ let add_notation local c ((loc,df),modifiers) sc =
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
- try add_notation_interpretation_core local df c sc onlyparse onlyprint
+ let compat = get_compat_version modifiers in
+ try add_notation_interpretation_core local df c sc onlyparse onlyprint compat
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
add_notation_in_scope local df c modifiers sc
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-30 13:40:13 +0000