[stm] Rename Side-Effect type.

As suggested by @gares, now the meaning becomes way clearer.

1 files changed, 28 insertions, 28 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index ac4dc0e9e..b98cb312e 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -127,7 +127,7 @@ type qed_t = {
   brname : Vcs_.Branch.t;
   brinfo : branch_type Vcs_.branch_info
 }
-type seff_t = Ast of aast | Virtual
+type seff_t = ReplayCommand of aast | CherryPickEnv
 type alias_t = Stateid.t * aast
 
 type transaction =
@@ -240,11 +240,11 @@ end = struct (* {{{ *)
       | [p, Noop; n, Fork x] -> { step = `Fork (x,Some p); next = n }
       | [n, Qed x; p, Noop]
       | [p, Noop; n, Qed x] -> { step = `Qed (x,p); next = n }
-      | [n, Sideff Virtual; p, Noop]
-      | [p, Noop; n, Sideff Virtual]-> { step = `Sideff (Virtual, p); next = n }
-      | [n, Sideff (Ast x); p, Noop]
-      | [p, Noop; n, Sideff (Ast x)]-> { step = `Sideff(Ast x,p); next = n }
-      | [n, Sideff (Ast x)]-> {step = `Sideff(Ast x, Stateid.dummy); next=n}
+      | [n, Sideff CherryPickEnv; p, Noop]
+      | [p, Noop; n, Sideff CherryPickEnv]-> { step = `Sideff (CherryPickEnv, p); next = n }
+      | [n, Sideff (ReplayCommand x); p, Noop]
+      | [p, Noop; n, Sideff (ReplayCommand x)]-> { step = `Sideff(ReplayCommand x,p); next = n }
+      | [n, Sideff (ReplayCommand x)]-> {step = `Sideff(ReplayCommand x, Stateid.dummy); next=n}
       | _ -> anomaly (Pp.str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
@@ -306,7 +306,7 @@ module VCS : sig
 
   val proof_nesting : unit -> int
   val checkout_shallowest_proof_branch : unit -> unit
-  val propagate_sideff : replay:seff_t -> unit
+  val propagate_sideff : action:seff_t -> unit
 
   val gc : unit -> unit
 
@@ -339,10 +339,10 @@ end = struct (* {{{ *)
     let string_of_transaction = function
       | Cmd { cast = t } | Fork (t, _,_,_) ->
           (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
-      | Sideff (Ast t) ->
+      | Sideff (ReplayCommand t) ->
           sprintf "Sideff(%s)"
             (try Pp.string_of_ppcmds (pr_ast t) with _ -> "ERR")
-      | Sideff Virtual -> "EnvChange"
+      | Sideff CherryPickEnv -> "EnvChange"
       | Noop -> " "
       | Alias (id,_) -> sprintf "Alias(%s)" (Stateid.to_string id)
       | Qed { qast } -> Pp.string_of_ppcmds (pr_ast qast) in
@@ -515,11 +515,11 @@ end = struct (* {{{ *)
         Proof_global.disactivate_current_proof_mode ()
 
   (* copies the transaction on every open branch *)
-  let propagate_sideff ~replay:t =
+  let propagate_sideff ~action =
     List.iter (fun b ->
       checkout b;
       let id = new_node () in
-      merge id ~ours:(Sideff t) ~into:b Branch.master)
+      merge id ~ours:(Sideff action) ~into:b Branch.master)
     (List.filter (fun b -> not (Branch.equal b Branch.master)) (branches ()))
   
   let visit id = Vcs_aux.visit !vcs id
@@ -530,8 +530,8 @@ end = struct (* {{{ *)
       match visit id with
       | { next = n; step = `Cmd x } -> (id,Cmd x) :: aux n
       | { next = n; step = `Alias x } -> (id,Alias x) :: aux n
-      | { next = n; step = `Sideff (Ast x,_) } ->
-           (id,Sideff (Ast x)) :: aux n
+      | { next = n; step = `Sideff (ReplayCommand x,_) } ->
+           (id,Sideff (ReplayCommand x)) :: aux n
       | _ -> anomaly Pp.(str("Cannot slice from "^ Stateid.to_string block_start ^
                          " to "^Stateid.to_string block_stop))
     in aux block_stop
@@ -914,9 +914,9 @@ let get_script prf =
     match view.step with
     | `Fork((_,_,_,ns), _) when test ns -> acc
     | `Qed (qed, proof) -> find [qed.qast.expr, (VCS.get_info id).n_goals] proof
-    | `Sideff (Ast x,_) ->
+    | `Sideff (ReplayCommand x,_) ->
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next
-    | `Sideff (Virtual, id)  -> find acc id
+    | `Sideff (CherryPickEnv, id)  -> find acc id
     | `Cmd {cast = x; ctac} when ctac -> (* skip non-tactics *)
          find ((x.expr, (VCS.get_info id).n_goals)::acc) view.next 
     | `Cmd _ -> find acc view.next
@@ -1172,7 +1172,7 @@ let register_proof_block_delimiter name static dynamic =
 let mk_doc_node id = function
   | { step = `Cmd { ctac; cast = { indentation; expr }}; next } when ctac ->
        Some { indentation; ast = expr; id }
-  | { step = `Sideff (Ast { indentation; expr }, _); next } ->
+  | { step = `Sideff (ReplayCommand { indentation; expr }, _); next } ->
        Some { indentation; ast = expr; id }
   | _ -> None
 let prev_node { id } =
@@ -1538,7 +1538,7 @@ end = struct (* {{{ *)
           | { step = `Cmd { cast = { loc } } }
           | { step = `Fork (( { loc }, _, _, _), _) } 
           | { step = `Qed ( { qast = { loc } }, _) } 
-          | { step = `Sideff (Ast { loc }, _) } ->
+          | { step = `Sideff (ReplayCommand { loc }, _) } ->
               let start, stop = Option.cata Loc.unloc (0,0) loc in
               msg_error Pp.(
                 str"File " ++ str name ++ str ": proof of " ++ str r_name ++
@@ -2004,10 +2004,10 @@ let collect_proof keep cur hd brkind id =
  let rec collect last accn id =
     let view = VCS.visit id in
     match view.step with
-    | (`Sideff (Ast x,_) | `Cmd { cast = x })
+    | (`Sideff (ReplayCommand x,_) | `Cmd { cast = x })
       when too_complex_to_delegate x -> `Sync(no_name,None,`Print)
     | `Cmd { cast = x } -> collect (Some (id,x)) (id::accn) view.next
-    | `Sideff (Ast x,_) -> collect (Some (id,x)) (id::accn) view.next
+    | `Sideff (ReplayCommand x,_) -> collect (Some (id,x)) (id::accn) view.next
     (* An Alias could jump everywhere... we hope we can ignore it*)
     | `Alias _ -> `Sync (no_name,None,`Alias)
     | `Fork((_,_,_,_::_::_), _) ->
@@ -2306,10 +2306,10 @@ let known_state ?(redefine_qed=false) ~cache id =
               ), (if redefine_qed then `No else `Yes), true
           in
           aux (collect_proof keep (view.next, x) brname brinfo eop)
-      | `Sideff (Ast x,_) -> (fun () ->
+      | `Sideff (ReplayCommand x,_) -> (fun () ->
             reach view.next; stm_vernac_interp id x; update_global_env ()
           ), cache, true
-      | `Sideff (Virtual, origin) -> (fun () ->
+      | `Sideff (CherryPickEnv, origin) -> (fun () ->
             reach view.next;
             inject_non_pstate (pure_cherry_pick_non_pstate view.next origin);
           ), cache, true
@@ -2430,7 +2430,7 @@ let merge_proof_branch ~valid ?id qast keep brname =
       let id = VCS.new_node ?id () in
       VCS.merge id ~ours:(Qed (qed None)) brname;
       VCS.delete_branch brname;
-      VCS.propagate_sideff ~replay:Virtual;
+      VCS.propagate_sideff ~action:CherryPickEnv;
       `Ok
   | { VCS.kind = `Edit (mode, qed_id, master_id, _,_) } ->
       let ofp =
@@ -2601,10 +2601,10 @@ let process_transaction ?(newtip=Stateid.fresh ())
           VCS.commit id (mkTransCmd x l in_proof `MainQueue);
           (* We can't replay a Definition since universes may be differently
            * inferred.  This holds in Coq >= 8.5 *)
-	  let replay = match x.expr with
-	    | VernacDefinition(_, _, DefineBody _) -> Virtual
-	    | _ -> Ast x in
-	  VCS.propagate_sideff ~replay;
+	  let action = match x.expr with
+	    | VernacDefinition(_, _, DefineBody _) -> CherryPickEnv
+	    | _ -> ReplayCommand x in
+	  VCS.propagate_sideff ~action;
           VCS.checkout_shallowest_proof_branch ();
           Backtrack.record (); if w == VtNow then finish (); `Ok
 
@@ -2635,7 +2635,7 @@ let process_transaction ?(newtip=Stateid.fresh ())
             end else begin
               VCS.commit id (mkTransCmd x [] in_proof `MainQueue);
               (* We hope it can be replayed, but we can't really know *)
-              VCS.propagate_sideff ~replay:(Ast x);
+              VCS.propagate_sideff ~action:(ReplayCommand x);
               VCS.checkout_shallowest_proof_branch ();
             end in
           State.define ~safe_id:head_id ~cache:`Yes step id;
@@ -2812,7 +2812,7 @@ let edit_at id =
       if Stateid.equal tip Stateid.initial then tip else
       match VCS.visit tip with
       | { step = (`Fork _ | `Qed _) } -> tip
-      | { step = `Sideff (Ast _,id) } -> id
+      | { step = `Sideff (ReplayCommand _,id) } -> id
       | { step = `Sideff _ } -> tip
       | { next } -> master_for_br root next in
   let reopen_branch start at_id mode qed_id tip old_branch =