VernacExtend produces vernac_interp_phase ADT (old name functional_vernac)

+ hide interp_functional_vernac in vernacentries

6 files changed, 53 insertions, 64 deletions

diff --git a/coqpp/coqpp_main.ml b/coqpp/coqpp_main.ml
index 48f9ed30b0..d6ae0a7d6f 100644
--- a/coqpp/coqpp_main.ml
+++ b/coqpp/coqpp_main.ml
@@ -369,22 +369,19 @@ let understand_state = function
 let print_body_state state fmt r =
   let state = match r.vernac_state with Some _ as s -> s | None -> state in
   match state with
-  | None -> fprintf fmt "Vernacentries.VtDefault (fun () -> %a)" print_code r.vernac_body
+  | None -> fprintf fmt "Vernacextend.VtDefault (fun () -> %a)" print_code r.vernac_body
   | Some "CUSTOM" -> print_code fmt r.vernac_body
   | Some state ->
     let state, unit_wrap = understand_state state in
-    fprintf fmt "Vernacentries.%s (%s%a)" state (if unit_wrap then "fun () ->" else "")
+    fprintf fmt "Vernacextend.%s (%s%a)" state (if unit_wrap then "fun () ->" else "")
       print_code r.vernac_body
 
-let print_body_wrapper state fmt r =
-  fprintf fmt "Vernacentries.interp_functional_vernac (%a)" (print_body_state state) r
-
 let print_body_fun state fmt r =
   fprintf fmt "let coqpp_body %a%a = @[%a@] in "
-    print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_wrapper state) r
+    print_binders r.vernac_toks print_atts_left r.vernac_atts (print_body_state state) r
 
 let print_body state fmt r =
-  fprintf fmt "@[(%afun %a~atts@ ~pstate@ -> coqpp_body %a%a ~pstate)@]"
+  fprintf fmt "@[(%afun %a~atts@ -> coqpp_body %a%a)@]"
     (print_body_fun state) r print_binders r.vernac_toks
     print_binders r.vernac_toks print_atts_right r.vernac_atts
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index db444a9b78..4ce87faaa1 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -532,7 +532,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~pstate = in_current_context econstr_display c; pstate in
+  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context econstr_display c) in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintConstr" [cmd]
@@ -541,7 +541,7 @@ let _ =
   let open Vernacextend in
   let ty_constr = Extend.TUentry (get_arg_tag Stdarg.wit_constr) in
   let cmd_sig = TyTerminal("PrintPureConstr", TyNonTerminal(ty_constr, TyNil)) in
-  let cmd_fn c ~atts ~pstate = in_current_context print_pure_econstr c; pstate in
+  let cmd_fn c ~atts = VtDefault (fun () -> in_current_context print_pure_econstr c) in
   let cmd_class _ = VtQuery,VtNow in
   let cmd : ty_ml = TyML (false, cmd_sig, cmd_fn, Some cmd_class) in
   vernac_extend ~command:"PrintPureConstr" [cmd]
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 77e8a92cc1..949ddfc3ee 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2295,6 +2295,30 @@ let locate_if_not_already ?loc (e, info) =
 
 exception End_of_input
 
+let vernac_interp_phase c ~pstate =
+  let open Proof_global in
+  let open Vernacextend in
+  match c with
+  | VtDefault f -> f (); pstate
+  | VtCloseProof f ->
+    vernac_require_open_proof ~pstate (fun ~pstate ->
+        f ~pstate:(Proof_global.get_current_pstate pstate);
+        Proof_global.discard_current pstate)
+  | VtMaybeOpenProof f ->
+    let proof = f () in
+    let pstate = maybe_push ~ontop:pstate proof in
+    pstate
+  | VtOpenProof f ->
+    Some (push ~ontop:pstate (f ()))
+  | VtModifyProof f ->
+    modify_pstate f ~pstate
+  | VtReadProofOpt f ->
+    f ~pstate:(Option.map get_current_pstate pstate);
+    pstate
+  | VtReadProof f ->
+    with_pstate ~pstate f;
+    pstate
+
 (* "locality" is the prefix "Local" attribute, while the "local" component
  * is the outdated/deprecated "Local" attribute of some vernacular commands
  * still parsed as the obsolete_locality grammar entry for retrocompatibility.
@@ -2629,7 +2653,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.stack option =
 
   (* Extensions *)
   | VernacExtend (opn,args) ->
-    Vernacextend.call ~atts opn args ~pstate
+    vernac_interp_phase (Vernacextend.call ~atts opn args) ~pstate
 
 (* XXX: This won't properly set the proof mode, as of today, it is
    controlled by the STM. Thus, we would need access information from
@@ -2709,37 +2733,3 @@ let interp ?(verbosely=true) ?proof ~st cmd =
     let exn = locate_if_not_already ?loc:cmd.CAst.loc exn in
     Vernacstate.invalidate_cache ();
     iraise exn
-
-(* mlg helpers *)
-
-type functional_vernac =
-  | VtDefault of (unit -> unit)
-  | VtCloseProof of (pstate:Proof_global.t -> unit)
-  | VtMaybeOpenProof of (unit -> Proof_global.t option)
-  | VtOpenProof of (unit -> Proof_global.t)
-  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
-  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
-  | VtReadProof of (pstate:Proof_global.t -> unit)
-
-let interp_functional_vernac c ~pstate =
-  let open Proof_global in
-  match c with
-  | VtDefault f -> f (); pstate
-  | VtCloseProof f ->
-    vernac_require_open_proof ~pstate (fun ~pstate ->
-        f ~pstate:(Proof_global.get_current_pstate pstate);
-        Proof_global.discard_current pstate)
-  | VtMaybeOpenProof f ->
-    let proof = f () in
-    let pstate = maybe_push ~ontop:pstate proof in
-    pstate
-  | VtOpenProof f ->
-    Some (push ~ontop:pstate (f ()))
-  | VtModifyProof f ->
-    modify_pstate f ~pstate
-  | VtReadProofOpt f ->
-    f ~pstate:(Option.map get_current_pstate pstate);
-    pstate
-  | VtReadProof f ->
-    with_pstate ~pstate f;
-    pstate
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index ca3a962319..d94ddc1aaf 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -51,19 +51,3 @@ val modify_pstate : pstate:Proof_global.stack option -> (pstate:Proof_global.t -
 (* Flag set when the test-suite is called. Its only effect to display
    verbose information for `Fail` *)
 val test_mode : bool ref
-
-(** For mlg *)
-
-type functional_vernac =
-  | VtDefault of (unit -> unit)
-  | VtCloseProof of (pstate:Proof_global.t -> unit)
-  | VtMaybeOpenProof of (unit -> Proof_global.t option)
-  | VtOpenProof of (unit -> Proof_global.t)
-  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
-  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
-  | VtReadProof of (pstate:Proof_global.t -> unit)
-
-val interp_functional_vernac
-  : functional_vernac
-  -> pstate:Proof_global.stack option
-  -> Proof_global.stack option
diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml
index 644413cbb9..cf704206af 100644
--- a/vernac/vernacextend.ml
+++ b/vernac/vernacextend.ml
@@ -53,7 +53,16 @@ type vernac_when =
   | VtLater
 type vernac_classification = vernac_type * vernac_when
 
-type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.stack option -> Proof_global.stack option
+type vernac_interp_phase =
+  | VtDefault of (unit -> unit)
+  | VtCloseProof of (pstate:Proof_global.t -> unit)
+  | VtMaybeOpenProof of (unit -> Proof_global.t option)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
+
+type vernac_command = atts:Attributes.vernac_flags -> vernac_interp_phase
 
 type plugin_args = Genarg.raw_generic_argument list
 
@@ -83,7 +92,7 @@ let warn_deprecated_command =
 
 (* Interpretation of a vernac command *)
 
-let call opn converted_args ~atts ~pstate =
+let call opn converted_args ~atts =
   let phase = ref "Looking up command" in
   try
     let depr, callback = vinterp_map opn in
@@ -99,7 +108,7 @@ let call opn converted_args ~atts ~pstate =
     phase := "Checking arguments";
     let hunk = callback converted_args in
     phase := "Executing command";
-    hunk ~atts ~pstate
+    hunk ~atts
   with
     | reraise ->
         let reraise = CErrors.push reraise in
diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli
index 46cee30a1e..4d885a3afc 100644
--- a/vernac/vernacextend.mli
+++ b/vernac/vernacextend.mli
@@ -71,7 +71,16 @@ type vernac_classification = vernac_type * vernac_when
 
 (** Interpretation of extended vernac phrases. *)
 
-type vernac_command = atts:Attributes.vernac_flags -> pstate:Proof_global.stack option -> Proof_global.stack option
+type vernac_interp_phase =
+  | VtDefault of (unit -> unit)
+  | VtCloseProof of (pstate:Proof_global.t -> unit)
+  | VtMaybeOpenProof of (unit -> Proof_global.t option)
+  | VtOpenProof of (unit -> Proof_global.t)
+  | VtModifyProof of (pstate:Proof_global.t -> Proof_global.t)
+  | VtReadProofOpt of (pstate:Proof_global.t option -> unit)
+  | VtReadProof of (pstate:Proof_global.t -> unit)
+
+type vernac_command = atts:Attributes.vernac_flags -> vernac_interp_phase
 
 type plugin_args = Genarg.raw_generic_argument list