Notation: a new annotation "compat 8.x" extending "only parsing"

 Suppose we declare : Notation foo := bar (compat "8.3").
 Then each time foo is used in a script :

 - By default nothing particular happens (for the moment)

 - But we could get a warning explaining that
   "foo is bar since coq > 8.3".
   For that, either use the command-line option -verb-compat-notations
   or the interactive command "Set Verbose Compat Notations".

 - There is also a strict mode, where foo is forbidden : the previous
   warning is now an error.
   For that, either use the command-line option -no-compat-notations
   or the interactive command "Unset Compat Notations".

 When Coq is launched in compatibility mode (via -compat 8.x),
 using a notation tagged "8.x" will never trigger a warning or error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15514 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 37 insertions, 14 deletions

diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 08cbe0640..652d0f7c6 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -136,3 +136,11 @@ let init_ocaml_path () =
 	[ "pretyping" ]; [ "interp" ]; [ "parsing" ]; [ "proofs" ];
 	[ "tactics" ]; [ "toplevel" ]; [ "printing" ]; [ "intf" ];
         [ "grammar" ]; [ "ide" ] ]
+
+let get_compat_version = function
+  | "8.3" -> Flags.V8_3
+  | "8.2" -> Flags.V8_2
+  | ("8.1" | "8.0") as s ->
+    msg_warning (strbrk ("Compatibility with version "^s^" not supported."));
+    Flags.V8_2
+  | s -> Errors.error ("Unknown compatibility version \""^s^"\".")
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 43b1556d5..4461f721d 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -22,3 +22,5 @@ val init_load_path : unit -> unit
 val init_library_roots : unit -> unit
 
 val init_ocaml_path : unit -> unit
+
+val get_compat_version : string -> Flags.compat_version
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6e5019adb..1a6867a51 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -125,13 +125,6 @@ let compile_files () =
 	   Vernac.compile v f)
       (List.rev !compile_list)
 
-let set_compat_version = function
-  | "8.3" -> compat_version := Some V8_3
-  | "8.2" -> compat_version := Some V8_2
-  | "8.1" -> msg_warning (strbrk "Compatibility with version 8.1 not supported.")
-  | "8.0" -> msg_warning (strbrk "Compatibility with version 8.0 not supported.")
-  | s -> error ("Unknown compatibility version \""^s^"\".")
-
 (*s options for the virtual machine *)
 
 let boxed_val = ref false
@@ -158,6 +151,9 @@ let warning s = msg_warning (strbrk s)
 let ide_slave = ref false
 let filter_opts = ref false
 
+let verb_compat_ntn = ref false
+let no_compat_ntn = ref false
+
 let parse_args arglist =
   let glob_opt = ref false in
   let rec parse = function
@@ -249,9 +245,13 @@ let parse_args arglist =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
-    | "-compat" :: v :: rem -> set_compat_version v; parse rem
+    | "-compat" :: v :: rem ->
+        Flags.compat_version := get_compat_version v; parse rem
     | "-compat" :: []       -> usage ()
 
+    | "-verb-compat-notations" :: rem -> verb_compat_ntn := true; parse rem
+    | "-no-compat-notations" :: rem -> no_compat_ntn := true; parse rem
+
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem ->
 	Flags.print_emacs := true; Pp.make_pp_emacs();
@@ -342,6 +342,9 @@ let init arglist =
       Mltop.init_known_plugins ();
       set_vm_opt ();
       engage ();
+      (* Be careful to set these variables after the inputstate *)
+      Syntax_def.set_verbose_compat_notations !verb_compat_ntn;
+      Syntax_def.set_compat_notations (not !no_compat_ntn);
       if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
         Option.iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index fee4fef18..52722c9f5 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -770,7 +770,7 @@ let interp_modifiers modl =
     | SetAssoc a :: l ->
 	if assoc <> None then error"An associativity is given more than once.";
 	interp (Some a) level etyps format l
-    | SetOnlyParsing :: l ->
+    | SetOnlyParsing _ :: l ->
 	onlyparsing := true;
 	interp assoc level etyps format l
     | SetFormat s :: l ->
@@ -783,8 +783,13 @@ let check_infix_modifiers modifiers =
   if t <> [] then
     error "Explicit entry level or type unexpected in infix notation."
 
-let no_syntax_modifiers modifiers =
-  modifiers = [] or modifiers = [SetOnlyParsing]
+let no_syntax_modifiers = function
+  | [] | [SetOnlyParsing _] -> true
+  | _ -> false
+
+let is_only_parsing = function
+  | [SetOnlyParsing _] -> true
+  | _ -> false
 
 (* Compute precedences from modifiers (or find default ones) *)
 
@@ -1131,7 +1136,7 @@ let add_notation local c ((loc,df),modifiers) sc =
   let df' =
    if no_syntax_modifiers modifiers then
     (* No syntax data: try to rely on a previously declared rule *)
-    let onlyparse = modifiers=[SetOnlyParsing] in
+    let onlyparse = is_only_parsing modifiers in
     try add_notation_interpretation_core local df c sc onlyparse
     with NoSyntaxRule ->
       (* Try to determine a default syntax rule *)
@@ -1209,6 +1214,9 @@ let add_syntactic_definition ident (vars,c) local onlyparse =
       let vars,pat = interp_notation_constr i_vars [] c in
       List.map (fun (id,(sc,kind)) -> (id,sc)) vars, pat
   in
-  let onlyparse = onlyparse or is_not_printable pat in
+  let onlyparse = match onlyparse with
+    | None when (is_not_printable pat) -> Some Flags.Current
+    | p -> p
+  in
   Syntax_def.declare_syntactic_definition local ident onlyparse (vars,pat)
 
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f34b0ccae..22b16be23 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -52,7 +52,7 @@ val add_syntax_extension :
 (** Add a syntactic definition (as in "Notation f := ...") *)
 
 val add_syntactic_definition : identifier -> identifier list * constr_expr ->
-  bool -> bool -> unit
+  bool -> Flags.compat_version option -> unit
 
 (** Print the Camlp4 state of a grammar *)
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index dcf11354b..e1b70b52e 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -32,6 +32,8 @@ let print_usage_channel co command =
 \n  -nois                  start with an empty state\
 \n  -outputstate f         write state in file f.coq\
 \n  -compat X.Y            provides compatibility support for Coq version X.Y\
+\n  -verb-compat-notations be warned when using compatibility notations\
+\n  -no-compat-notations   get an error when using compatibility notations\
 \n\
 \n  -load-ml-object f      load ML object file f\
 \n  -load-ml-source f      load ML file f\