[vernac] Refactor Vernacular Control Attributes into a list

We place control attributes on their own, datatype, similarly to
regular attributes.

This is a step towards fixing #10452 , as we can now decouple control
attributes from the vernac AST itself, allowing to pass them
independently.

6 files changed, 75 insertions, 82 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index dcd1979a85..54ce527ea2 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -72,16 +72,29 @@ let parse_compat_version = let open Flags in function
     CErrors.user_err ~hdr:"get_compat_version"
       Pp.(str "Unknown compatibility version \"" ++ str s ++ str "\".")
 
+(* For now we just keep the top-level location of the whole
+   vernacular, that is to say, including attributes and control flags;
+   this is not very convenient for advanced clients tho, so in the
+   future it'd be cool to actually locate the attributes and control
+   flags individually too. *)
+let add_control_flag ~loc ~flag { CAst.v = cmd } =
+  CAst.make ~loc { cmd with control = flag :: cmd.control }
+
 }
 
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf;
   vernac_control: FIRST
-    [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) }
-      | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) }
-      | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) }
-      | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v }
-      | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ]
+    [ [ IDENT "Time"; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlTime false) c }
+      | IDENT "Redirect"; s = ne_string; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlRedirect s) c }
+      | IDENT "Timeout"; n = natural; c = vernac_control ->
+        { add_control_flag ~loc ~flag:(ControlTimeout n) c }
+      | IDENT "Fail"; c = vernac_control ->
+        { add_control_flag ~loc ~flag:ControlFail c }
+      | v = decorated_vernac ->
+        { let (attrs, expr) = v in CAst.make ~loc { control = []; attrs; expr = expr } } ]
     ]
   ;
   decorated_vernac:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 0eb0b1b6f6..bd6f8f01d8 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1266,6 +1266,16 @@ let string_of_definition_object_kind = let open Decls in function
       | VernacEndSubproof ->
         return (str "}")
 
+let pr_control_flag (p : control_flag) =
+  let w = match p with
+    | ControlTime _ -> keyword "Time"
+    | ControlRedirect s -> keyword "Redirect" ++ spc() ++ qs s
+    | ControlTimeout n -> keyword "Timeout " ++ int n
+    | ControlFail -> keyword "Fail" in
+  w ++ spc ()
+
+let pr_vernac_control flags = Pp.prlist pr_control_flag flags
+
 let rec pr_vernac_flag (k, v) =
   let k = keyword k in
   let open Attributes in
@@ -1281,19 +1291,11 @@ let pr_vernac_attributes =
   | [] -> mt ()
   | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
-  let rec pr_vernac_control v =
-    let return = tag_vernac v in
-    match v.v with
-    | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
-    | VernacTime (_,v) ->
-      return (keyword "Time" ++ spc() ++ pr_vernac_control v)
-    | VernacRedirect (s, v) ->
-      return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
-    | VernacTimeout(n,v) ->
-      return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
-    | VernacFail v->
-      return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
-
-    let pr_vernac v =
-      try pr_vernac_control v
-      with e -> CErrors.print e
+let pr_vernac ({v = {control; attrs; expr}} as v) =
+  try
+    tag_vernac v
+      (pr_vernac_control control ++
+       pr_vernac_attributes attrs ++
+       pr_vernac_expr expr ++
+       sep_end expr)
+  with e -> CErrors.print e
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index bc51dd46f3..2c55f73a88 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2610,7 +2610,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
  * loc is the Loc.t of the vernacular command being interpreted. *)
-and interp_expr ?proof ~atts ~st c =
+and interp_expr ~atts ~st c =
   let stack = st.Vernacstate.lemmas in
   vernac_pperr_endline (fun () -> str "interpreting: " ++ Ppvernac.pr_vernac_expr c);
   match c with
@@ -2660,7 +2660,7 @@ and vernac_load ~verbosely fname =
     try
       let proof_mode = Option.map (fun _ -> get_default_proof_mode ()) stack in
       let stack =
-        v_mod (interp_control ?proof:None ~st:{ st with Vernacstate.lemmas = stack })
+        v_mod (interp_control ~st:{ st with Vernacstate.lemmas = stack })
           (parse_sentence proof_mode input) in
       load_loop ~stack
     with
@@ -2673,22 +2673,23 @@ and vernac_load ~verbosely fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   ()
 
-and interp_control ?proof ~st v = match v with
-  | { v=VernacExpr (atts, cmd) } ->
+and pop_control cl = CAst.map (fun cmd -> { cmd with control = cl })
+and interp_control ~st ({ v = cmd } as vernac) = match cmd.control with
+  | [] ->
     let before_univs = Global.universes () in
-    let pstack = interp_expr ?proof ~atts ~st cmd in
+    let pstack = interp_expr ~atts:cmd.attrs ~st cmd.expr in
     if before_univs == Global.universes () then pstack
     else Option.map (Vernacstate.LemmaStack.map_top_pstate ~f:Proof_global.update_global_env) pstack
-  | { v=VernacFail v } ->
-    with_fail ~st (fun () -> interp_control ?proof ~st v);
+  | ControlFail :: cl ->
+    with_fail ~st (fun () -> interp_control ~st (pop_control cl vernac));
     st.Vernacstate.lemmas
-  | { v=VernacTimeout (timeout,v) } ->
-    vernac_timeout ~timeout (interp_control ?proof ~st) v
-  | { v=VernacRedirect (s, v) } ->
-    Topfmt.with_output_to_file s (interp_control ?proof ~st) v
-  | { v=VernacTime (batch, cmd) }->
-    let header = if batch then Topfmt.pr_cmd_header cmd else Pp.mt () in
-    System.with_time ~batch ~header (interp_control ?proof ~st) cmd
+  | ControlTimeout timeout :: cl ->
+    vernac_timeout ~timeout (interp_control ~st) (pop_control cl vernac)
+  | ControlRedirect s :: cl ->
+    Topfmt.with_output_to_file s (interp_control ~st) (pop_control cl vernac)
+  | ControlTime batch :: cl ->
+    let header = if batch then Topfmt.pr_cmd_header vernac else Pp.mt () in
+    System.with_time ~batch ~header (interp_control ~st) (pop_control cl vernac)
 
 let () =
   declare_int_option
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 0968632c2d..84f437f640 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -414,12 +414,17 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_control_r =
-  | VernacExpr of Attributes.vernac_flags * vernac_expr
+type control_flag =
+  | ControlTime of bool
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control
-  | VernacRedirect of string * vernac_control
-  | VernacTimeout of int * vernac_control
-  | VernacFail of vernac_control
+  | ControlRedirect of string
+  | ControlTimeout of int
+  | ControlFail
+
+type vernac_control_r =
+  { control : control_flag list
+  ; attrs : Attributes.vernac_flags
+  ; expr : vernac_expr
+  }
 and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 747998c6cc..903a28e953 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,47 +13,26 @@
 
 open Vernacexpr
 
-let rec under_control v = v |> CAst.with_val (function
-  | VernacExpr (_, c) -> c
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacFail c
-  | VernacTimeout (_,c) -> under_control c
-  )
-
-let rec has_Fail v = v |> CAst.with_val (function
-  | VernacExpr _ -> false
-  | VernacRedirect (_,c)
-  | VernacTime (_,c)
-  | VernacTimeout (_,c) -> has_Fail c
-  | VernacFail _ -> true)
+(* Does this vernacular involve Fail? *)
+let has_Fail { CAst.v } = List.mem ControlFail v.control
 
 (* Navigation commands are allowed in a coqtop session but not in a .v file *)
-let is_navigation_vernac_expr = function
+let is_navigation_vernac = function
   | VernacResetInitial
   | VernacResetName _
   | VernacBack _ -> true
   | _ -> false
 
-let is_navigation_vernac c =
-  is_navigation_vernac_expr (under_control c)
-
-let rec is_deep_navigation_vernac v = v |> CAst.with_val (function
-  | VernacTime (_,c) -> is_deep_navigation_vernac c
-  | VernacRedirect (_, c)
-  | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c
-  | VernacExpr _ -> false)
-
 (* NB: Reset is now allowed again as asked by A. Chlipala *)
-let is_reset = CAst.with_val (function
-  | VernacExpr ( _, VernacResetInitial)
-  | VernacExpr (_, VernacResetName _) -> true
-  | _ -> false)
+let is_reset = function
+  | VernacResetInitial
+  | VernacResetName _ -> true
+  | _ -> false
 
-let is_debug cmd = match under_control cmd with
+let is_debug = function
   | VernacSetOption (_, ["Ltac";"Debug"], _) -> true
   | _ -> false
 
-let is_undo cmd = match under_control cmd with
+let is_undo = function
   | VernacUndo _ | VernacUndoTo _ -> true
   | _ -> false
diff --git a/vernac/vernacprop.mli b/vernac/vernacprop.mli
index 8875b86d94..320878e401 100644
--- a/vernac/vernacprop.mli
+++ b/vernac/vernacprop.mli
@@ -13,16 +13,9 @@
 
 open Vernacexpr
 
-(* 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_debug : vernac_control -> bool
-val is_undo : vernac_control -> bool
+val is_navigation_vernac : vernac_expr -> bool
+val is_reset : vernac_expr -> bool
+val is_debug : vernac_expr -> bool
+val is_undo : vernac_expr -> bool