Separate vernac controls and regular commands.

Virtually all classifications of vernacular commands (the STM
classifier, "filtered commands", "navigation commands", etc.) were
broken in presence of control vernaculars like Time, Timeout, Fail.

Funny examples of bugs include Time Abort All in coqtop or Time Set Ltac
Debug in CoqIDE.

This change introduces a type separation between vernacular controls and
vernacular commands, together with an "under_control" combinator.

5 files changed, 67 insertions, 48 deletions

diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 6c3dfec7d1..1bb9e0da19 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -80,8 +80,8 @@ let pr_grammar = function
   | "pattern" ->
       pr_entry Pcoq.Constr.pattern
   | "vernac" ->
-      str "Entry vernac is" ++ fnl () ++
-      pr_entry Pcoq.Vernac_.vernac ++
+      str "Entry vernac_control is" ++ fnl () ++
+      pr_entry Pcoq.Vernac_.vernac_control ++
       str "Entry command is" ++ fnl () ++
       pr_entry Pcoq.Vernac_.command ++
       str "Entry syntax is" ++ fnl () ++
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index a581043ac1..aa6121c39a 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1380,11 +1380,13 @@ let _ =
       optread  = (fun () -> !Flags.program_mode);
       optwrite = (fun b -> Flags.program_mode:=b) }
 
+let universe_polymorphism_option_name = ["Universe"; "Polymorphism"]
+
 let _ =
   declare_bool_option
     { optdepr  = false;
       optname  = "universe polymorphism";
-      optkey   = ["Universe"; "Polymorphism"];
+      optkey   = universe_polymorphism_option_name;
       optread  = Flags.is_universe_polymorphism;
       optwrite = Flags.make_universe_polymorphism }
 
@@ -1933,19 +1935,11 @@ let vernac_load interp fname =
  * loc is the Loc.t of the vernacular command being interpreted. *)
 let interp ?proof ~atts ~st c =
   let open Vernacinterp in
-  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac c);
+  vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
-  (* The below vernac are candidates for removal from the main type
-     and to be put into a new doc_command datatype: *)
 
   | VernacLoad _ -> assert false
 
-  (* Done later in this file *)
-  | VernacFail _ -> assert false
-  | VernacTime _ -> assert false
-  | VernacRedirect _ -> assert false
-  | VernacTimeout _ -> assert false
-
   (* The STM should handle that, but LOAD bypasses the STM... *)
   | VernacAbortAll    -> CErrors.user_err  (str "AbortAll cannot be used through the Load command")
   | VernacRestart     -> CErrors.user_err  (str "Restart cannot be used through the Load command")
@@ -2209,7 +2203,20 @@ let with_fail st b f =
 
 let interp ?(verbosely=true) ?proof ~st (loc,c) =
   let orig_program_mode = Flags.is_program_mode () in
-  let rec aux ?polymorphism ~atts isprogcmd = function
+  let rec control = function
+  | VernacExpr v ->
+      let atts = { loc; locality = None; polymorphic = false; } in
+      aux ~atts orig_program_mode v
+  | VernacFail v -> with_fail st true (fun () -> control v)
+  | VernacTimeout (n,v) ->
+      current_timeout := Some n;
+      control v
+  | VernacRedirect (s, (_,v)) ->
+       Topfmt.with_output_to_file s control v
+  | VernacTime (_,v) ->
+      System.with_time !Flags.time control v;
+
+  and aux ?polymorphism ~atts isprogcmd = function
 
     | VernacProgram c when not isprogcmd ->
       aux ?polymorphism ~atts true c
@@ -2229,20 +2236,7 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
     | VernacLocal _ ->
       user_err Pp.(str "Locality specified twice")
 
-    | VernacFail v ->
-      with_fail st true (fun () -> aux ?polymorphism ~atts isprogcmd v)
-
-    | VernacTimeout (n,v) ->
-      current_timeout := Some n;
-      aux ?polymorphism ~atts isprogcmd v
-
-    | VernacRedirect (s, (_,v)) ->
-      Topfmt.with_output_to_file s (aux ?polymorphism ~atts isprogcmd) v
-
-    | VernacTime (_,v) ->
-      System.with_time !Flags.time (aux ?polymorphism ~atts isprogcmd) v;
-
-    | VernacLoad (_,fname) -> vernac_load (aux ?polymorphism ~atts false) fname
+    | VernacLoad (_,fname) -> vernac_load control fname
 
     | c ->
       check_vernac_supports_locality c atts.locality;
@@ -2272,10 +2266,9 @@ let interp ?(verbosely=true) ?proof ~st (loc,c) =
 	    ignore (Flags.use_polymorphic_flag ());
             iraise e
   in
-  let atts = { loc; locality = None; polymorphic = false; } in
   if verbosely
-  then Flags.verbosely (aux ~atts orig_program_mode) c
-  else aux ~atts orig_program_mode c
+  then Flags.verbosely control c
+  else control  c
 
 (* XXX: There is a bug here in case of an exception, see @gares
    comments on the PR *)
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index a559912a09..e99a62fe6c 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -18,7 +18,7 @@ val vernac_require :
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-  st:Vernacstate.t -> Vernacexpr.vernac_expr Loc.located -> Vernacstate.t
+  st:Vernacstate.t -> Vernacexpr.vernac_control Loc.located -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
@@ -36,3 +36,5 @@ val command_focus : unit Proof.focus_kind
 
 val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr ->
   Evd.evar_map * Redexpr.red_expr) Hook.t
+
+val universe_polymorphism_option_name : string list
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 3cff1f14c0..4a01ef2efa 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -11,32 +11,49 @@
 
 open Vernacexpr
 
+let rec under_control = function
+  | VernacExpr c -> c
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+
+let rec has_Fail = function
+  | VernacExpr c -> false
+  | VernacRedirect (_,(_,c))
+  | VernacTime (_,c)
+  | VernacTimeout (_,c) -> has_Fail c
+  | VernacFail _ -> true
+
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let rec is_navigation_vernac = function
+let is_navigation_vernac_expr = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBacktrack _
   | VernacBackTo _
   | VernacBack _ -> true
-  | VernacRedirect (_, (_,c))
-  | VernacTime (_,c) ->
-      is_navigation_vernac c (* Time Back* is harmless *)
-  | c -> is_deep_navigation_vernac c
+  | _ -> false
 
-and is_deep_navigation_vernac = function
+let is_navigation_vernac c =
+  is_navigation_vernac_expr (under_control c)
+
+let rec is_deep_navigation_vernac = function
+  | VernacTime (_,c) -> is_deep_navigation_vernac c
+  | VernacRedirect (_, (_,c))
   | VernacTimeout (_,c) | VernacFail c -> is_navigation_vernac c
-  | _ -> false
+  | VernacExpr _ -> false
 
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
 let is_reset = function
-  | VernacResetInitial | VernacResetName _ -> true
+  | VernacExpr VernacResetInitial
+  | VernacExpr (VernacResetName _) -> true
   | _ -> false
 
-let is_debug cmd = match cmd with
+let is_debug cmd = match under_control cmd with
   | VernacSetOption (["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_query cmd = match cmd with
+let is_query cmd = match under_control cmd with
   | VernacChdir None
   | VernacMemOption _
   | VernacPrintOption _
@@ -47,6 +64,6 @@ let is_query cmd = match cmd with
   | VernacLocate _ -> true
   | _ -> false
 
-let is_undo cmd = match cmd with
+let is_undo cmd = match under_control cmd with
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index fbdba6bacb..eb7c7055ac 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -11,9 +11,16 @@
 
 open Vernacexpr
 
-val is_navigation_vernac : vernac_expr -> bool
-val is_deep_navigation_vernac : vernac_expr -> bool
-val is_reset : vernac_expr -> bool
-val is_query : vernac_expr -> bool
-val is_debug : vernac_expr -> bool
-val is_undo : vernac_expr -> bool
+(* Return the vernacular command below control (Time, Timeout, Redirect, Fail).
+   Beware that Fail can change many properties of the underlying command, since
+   a success of Fail means the command was backtracked over. *)
+val under_control : vernac_control -> vernac_expr
+
+val has_Fail : vernac_control -> bool
+
+val is_navigation_vernac : vernac_control -> bool
+val is_deep_navigation_vernac : vernac_control -> bool
+val is_reset : vernac_control -> bool
+val is_query : vernac_control -> bool
+val is_debug : vernac_control -> bool
+val is_undo : vernac_control -> bool