Merge PR #9926: [vernac] [ast] Make location info an attribute of vernaculars.

Ack-by: SkySkimmer
Ack-by: ejgallego
Reviewed-by: ppedrot

10 files changed, 42 insertions, 43 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3f491d1dd4..d97fb523f7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -77,11 +77,11 @@ let parse_compat_version = let open Flags in function
 GRAMMAR EXTEND Gram
   GLOBAL: vernac_control gallina_ext noedit_mode subprf;
   vernac_control: FIRST
-    [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) }
-      | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
-      | IDENT "Timeout"; n = natural; v = located_vernac -> { VernacTimeout(n,v) }
-      | IDENT "Fail"; v = located_vernac -> { VernacFail v }
-      | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+    [ [ 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) } ]
     ]
   ;
   decorated_vernac:
@@ -147,9 +147,6 @@ GRAMMAR EXTEND Gram
     ] ]
   ;
 
-  located_vernac:
-    [ [ v = vernac_control -> { CAst.make ~loc v } ] ]
-  ;
 END
 
 {
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 4e4d431e89..327efcda2b 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1262,15 +1262,15 @@ let pr_vernac_attributes =
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
-    match v with
+    match v.v with
     | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
-    | VernacTime (_,{v}) ->
+    | VernacTime (_,v) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
-    | VernacRedirect (s, {v}) ->
+    | VernacRedirect (s, v) ->
       return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v)
-    | VernacTimeout(n,{v}) ->
+    | VernacTimeout(n,v) ->
       return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v)
-    | VernacFail {v} ->
+    | VernacFail v->
       return (keyword "Fail" ++ spc() ++ pr_vernac_control v)
 
     let pr_vernac v =
diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml
index d474ef8637..4d9157089c 100644
--- a/vernac/pvernac.ml
+++ b/vernac/pvernac.ml
@@ -52,7 +52,7 @@ module Vernac_ =
 
     let () =
       let open Extend in
-      let act_vernac v loc = Some CAst.(make ~loc v) in
+      let act_vernac v loc = Some v in
       let act_eoi _ loc = None in
       let rule = [
         Rule (Next (Stop, Atoken Tok.PEOI), act_eoi);
diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli
index 4bf7c9f7bd..41a2e7fd6f 100644
--- a/vernac/pvernac.mli
+++ b/vernac/pvernac.mli
@@ -26,7 +26,7 @@ module Vernac_ :
     val rec_definition : (fixpoint_expr * decl_notation list) Entry.t
     val noedit_mode : vernac_expr Entry.t
     val command_entry : vernac_expr Entry.t
-    val main_entry : vernac_control CAst.t option Entry.t
+    val main_entry : vernac_control option Entry.t
     val red_expr : raw_red_expr Entry.t
     val hint_info : Hints.hint_info_expr Entry.t
   end
@@ -40,7 +40,7 @@ module Unsafe : sig
 end
 
 (** The main entry: reads an optional vernac command *)
-val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t
+val main_entry : proof_mode option -> vernac_control option Entry.t
 
 (** Grammar entry for tactics: proof mode(s).
   By default Coq's grammar has an empty entry (non-terminal) for
diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml
index 7bc3264968..118c126970 100644
--- a/vernac/topfmt.ml
+++ b/vernac/topfmt.ml
@@ -425,7 +425,7 @@ let with_output_to_file fname func input =
 (* For coqtop -time, we display the position in the file,
    and a glimpse of the executed command *)
 
-let pr_cmd_header {CAst.loc;v=com} =
+let pr_cmd_header com =
   let shorten s =
     if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s
   in
@@ -435,7 +435,7 @@ let pr_cmd_header {CAst.loc;v=com} =
         | x -> x
       ) s
   in
-  let (start,stop) = Option.cata Loc.unloc (0,0) loc in
+  let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in
   let safe_pr_vernac x =
     try Ppvernac.pr_vernac x
     with e -> str (Printexc.to_string e) in
diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli
index a1e289cd5a..3d522a9e0f 100644
--- a/vernac/topfmt.mli
+++ b/vernac/topfmt.mli
@@ -73,4 +73,4 @@ val print_err_exn : exn -> unit
     redirected to a file [file] *)
 val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b
 
-val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t
+val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index fa170e4104..0f6374c506 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2599,7 +2599,7 @@ and vernac_load ?proof ~verbosely ~st fname =
     CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs.");
   pstate
 
-and interp_control ?proof ~st = function
+and interp_control ?proof ~st v = match v with
   | { v=VernacExpr (atts, cmd) } ->
     interp_expr ?proof ~atts ~st cmd
   | { v=VernacFail v } ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 71cc29b6e1..12451370c8 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -23,7 +23,7 @@ val vernac_require :
 val interp :
   ?verbosely:bool ->
   ?proof:Proof_global.closed_proof ->
-  st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t
+  st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t
 
 (** Prepare a "match" template for a given inductive type.
     For each branch of the match, we list the constructor name
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index d0dae1aa53..99b457effe 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -398,11 +398,12 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type vernac_control =
+type vernac_control_r =
   | VernacExpr of Attributes.vernac_flags * vernac_expr
   (* 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 CAst.t
-  | VernacRedirect of string * vernac_control CAst.t
-  | VernacTimeout of int * vernac_control CAst.t
-  | VernacFail of vernac_control CAst.t
+  | VernacTime of bool * vernac_control
+  | VernacRedirect of string * vernac_control
+  | VernacTimeout of int * vernac_control
+  | VernacFail of vernac_control
+and vernac_control = vernac_control_r CAst.t
diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml
index 704c5b2170..b3490c7dc6 100644
--- a/vernac/vernacprop.ml
+++ b/vernac/vernacprop.ml
@@ -13,19 +13,20 @@
 
 open Vernacexpr
 
-let rec under_control = function
+let rec under_control v = v |> CAst.with_val (function
   | VernacExpr (_, c) -> c
-  | VernacRedirect (_,{CAst.v=c})
-  | VernacTime (_,{CAst.v=c})
-  | VernacFail {CAst.v=c}
-  | VernacTimeout (_,{CAst.v=c}) -> under_control c
+  | VernacRedirect (_,c)
+  | VernacTime (_,c)
+  | VernacFail c
+  | VernacTimeout (_,c) -> under_control c
+  )
 
-let rec has_Fail = function
+let rec has_Fail v = v |> CAst.with_val (function
   | VernacExpr _ -> false
-  | VernacRedirect (_,{CAst.v=c})
-  | VernacTime (_,{CAst.v=c})
-  | VernacTimeout (_,{CAst.v=c}) -> has_Fail c
-  | VernacFail _ -> true
+  | 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 is_navigation_vernac_expr = function
@@ -38,17 +39,17 @@ let is_navigation_vernac_expr = function
 let is_navigation_vernac c =
   is_navigation_vernac_expr (under_control c)
 
-let rec is_deep_navigation_vernac = function
-  | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c
-  | VernacRedirect (_, {CAst.v=c})
-  | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c
-  | VernacExpr _ -> false
+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 = function
+let is_reset = CAst.with_val (function
   | VernacExpr ( _, VernacResetInitial)
   | VernacExpr (_, VernacResetName _) -> true
-  | _ -> false
+  | _ -> false)
 
 let is_debug cmd = match under_control cmd with
   | VernacSetOption (_, ["Ltac";"Debug"], _) -> true