STM: invalid states are first class citizens

A state in the cache (document node) is now one of "Empty | Error | Valid".
This paves the way to commands/blocks-of-commands resilient-to/confining
errors: one can catch and "ignore" the exception obtained by reaching the
previous state and do something sensible, like running anyway the command
or skipping until the end of an error-confining block is reached.

Invalid states carry an enriched exception with the safe_id attached, so
that if one edits_at or observe them gets a safe place to land (CoqIDE
needs such piece of info).

Little API change in Stm.state_of_id now returning a `Error variant for
the new kind of state.

2 files changed, 78 insertions, 59 deletions

diff --git a/stm/stm.ml b/stm/stm.ml
index e2acb1029..1dd089a26 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -187,20 +187,24 @@ let summary_pstate = [ Evarutil.meta_counter_summary_name;
                        Evd.evar_counter_summary_name;
                        "program-tcc-table" ]
 type state = {
-  system : States.state;
-  proof : Proof_global.state;
-  shallow : bool
+  system : States.state;       (* summary + libstack *)
+  proof : Proof_global.state;  (* proof state *)
+  shallow : bool               (* is the state trimmed down (libstack) *)
 }
+type cached_state =
+  | Empty
+  | Error of Exninfo.iexn
+  | Valid of state
 type branch = Vcs_.Branch.t * branch_type Vcs_.branch_info
 type backup = { mine : branch; others : branch list }
-type 'vcs state_info = { (* Make private *)
-  mutable n_reached : int;
-  mutable n_goals : int;
-  mutable state : state option;
+type 'vcs state_info = { (* TODO: Make this record private to VCS *)
+  mutable n_reached : int;      (* debug cache: how many times was computed *)
+  mutable n_goals : int;        (* open goals: indentation *)
+  mutable state : cached_state; (* state value *)
   mutable vcs_backup : 'vcs option * backup option;
 }
 let default_info () =
-  { n_reached = 0; n_goals = 0; state = None; vcs_backup = None,None }
+  { n_reached = 0; n_goals = 0; state = Empty; vcs_backup = None,None }
 
 (* Functions that work on a Vcs with a specific branch type *)
 module Vcs_aux : sig
@@ -296,10 +300,10 @@ module VCS : sig
   val cur_tip : unit -> id
 
   val get_info : id -> vcs state_info
-  val reached : id -> bool -> unit
+  val reached : id -> unit
   val goals : id -> int -> unit
-  val set_state : id -> state -> unit
-  val get_state : id -> state option
+  val set_state : id -> cached_state -> unit
+  val get_state : id -> cached_state
 
   (* cuts from start -> stop, raising Expired if some nodes are not there *)
   val slice : start:id -> stop:id -> vcs
@@ -345,11 +349,11 @@ end = struct (* {{{ *)
       | Qed { qast } -> string_of_ppcmds (pr_ast qast) in
     let is_green id = 
       match get_info vcs id with
-      | Some { state = Some _ } -> true
+      | Some { state = Valid _ } -> true
       | _ -> false in
     let is_red id =
       match get_info vcs id with
-      | Some s -> Int.equal s.n_reached ~-1
+      | Some { state = Error _ } -> true
       | _ -> false in
     let head = current_branch vcs in
     let heads =
@@ -452,13 +456,12 @@ end = struct (* {{{ *)
     | Some x -> x
     | None -> raise Vcs_aux.Expired
   let set_state id s =
-    (get_info id).state <- Some s;
+    (get_info id).state <- s;
     if Flags.async_proofs_is_master () then Hooks.(call state_ready id)
   let get_state id = (get_info id).state
-  let reached id b =
+  let reached id =
     let info = get_info id in
-    if b then info.n_reached <- info.n_reached + 1
-    else info.n_reached <- -1
+    info.n_reached <- info.n_reached + 1
   let goals id n = (get_info id).n_goals <- n
   let cur_tip () = get_branch_pos (current_branch ())
 
@@ -508,7 +511,7 @@ end = struct (* {{{ *)
     let l = nodes_in_slice ~start ~stop in
     let copy_info v id =
       Vcs_.set_info v id
-        { (get_info id) with state = None; vcs_backup = None,None } in
+        { (get_info id) with state = Empty; vcs_backup = None,None } in
     let copy_info_w_state v id =
       Vcs_.set_info v id { (get_info id) with vcs_backup = None,None } in
     let v = Vcs_.empty start in
@@ -518,11 +521,12 @@ end = struct (* {{{ *)
       let v = copy_info v id in
       v) l v in
     (* Stm should have reached the beginning of proof *)
-    assert (not (Option.is_empty (get_info start).state));
+    assert (match (get_info start).state with Valid _ -> true | _ -> false);
     (* We put in the new dag the most recent state known to master *)
     let rec fill id =
-      if (get_info id).state = None then fill (Vcs_aux.visit v id).next
-      else copy_info_w_state v id in
+      match (get_info id).state with
+      | Empty | Error _ -> fill (Vcs_aux.visit v id).next
+      | Valid _ -> copy_info_w_state v id in
     let v = fill stop in
     (* We put in the new dag the first state (since Qed shall run on it,
      * see check_task_aux) *)
@@ -596,7 +600,10 @@ end = struct (* {{{ *)
 end (* }}} *)
 
 let state_of_id id =
-  try `Valid (VCS.get_info id).state
+  try match (VCS.get_info id).state with
+    | Valid s -> `Valid (Some s)
+    | Error (e,_) -> `Error e
+    | Empty -> `Valid None
   with VCS.Expired -> `Expired
 
 
@@ -616,6 +623,7 @@ module State : sig
 
   val install_cached : Stateid.t -> unit
   val is_cached : ?cache:Summary.marshallable -> Stateid.t -> bool
+  val is_cached_and_valid : ?cache:Summary.marshallable -> Stateid.t -> bool
 
 
   val exn_on : Stateid.t -> ?valid:Stateid.t -> iexn -> iexn
@@ -661,51 +669,60 @@ end = struct (* {{{ *)
     proof,
     Summary.project_summary (States.summary_of_state system) summary_pstate
 
-  let freeze marshallable id = VCS.set_state id (freeze_global_state marshallable)
+  let freeze marshallable id =
+    VCS.set_state id (Valid (freeze_global_state marshallable))
+  let freeze_invalid id iexn = VCS.set_state id (Error iexn)
 
-  let is_cached ?(cache=`No) id =
+  let is_cached ?(cache=`No) id only_valid =
     if Stateid.equal id !cur_id then
       try match VCS.get_info id with
-        | { state = None } when cache = `Yes -> freeze `No id; true
-        | { state = None } when cache = `Shallow -> freeze `Shallow id; true
+        | { state = Empty } when cache = `Yes -> freeze `No id; true
+        | { state = Empty } when cache = `Shallow -> freeze `Shallow id; true
         | _ -> true
       with VCS.Expired -> false
     else
       try match VCS.get_info id with
-        | { state = Some _ } -> true
-        | _ -> false 
+        | { state = Empty } -> false
+        | { state = Valid _ } -> true
+        | { state = Error _ } -> not only_valid
       with VCS.Expired -> false
 
+  let is_cached_and_valid ?cache id = is_cached ?cache id true
+  let is_cached ?cache id = is_cached ?cache id false
+
   let install_cached id =
-    if Stateid.equal id !cur_id then () else (* optimization *)
-    let s =
-      match VCS.get_info id with
-      | { state = Some s } -> s
-      | _ -> anomaly (str "unfreezing a non existing state") in
-    unfreeze_global_state s; cur_id := id
+    match VCS.get_info id with
+    | { state = Valid s } ->
+         if Stateid.equal id !cur_id then () (* optimization *)
+         else begin unfreeze_global_state s; cur_id := id end
+    | { state = Error ie } -> cur_id := id; Exninfo.iraise ie 
+    | _ ->
+        (* coqc has a 1 slot cache and only for valid states *)
+        if interactive () = `No && Stateid.equal id !cur_id then ()
+        else anomaly (str "installing a non cached state")
 
   let get_cached id =
     try match VCS.get_info id with
-    | { state = Some s } -> s
+    | { state = Valid s } -> s
     | _ -> anomaly (str "not a cached state")
     with VCS.Expired -> anomaly (str "not a cached state (expired)")
 
   let assign id what =
-    if VCS.get_state id <> None then () else
+    if VCS.get_state id <> Empty then () else
     try match what with
     | `Full s ->
          let s =
            try
             let prev = (VCS.visit id).next in
-            if is_cached prev
+            if is_cached_and_valid prev
             then { s with proof = 
               Proof_global.copy_terminators
                 ~src:(get_cached prev).proof ~tgt:s.proof }
             else s
            with VCS.Expired -> s in
-         VCS.set_state id s
+         VCS.set_state id (Valid s)
     | `Proof(ontop,(pstate,counters)) ->
-         if is_cached ontop then
+         if is_cached_and_valid ontop then
            let s = get_cached ontop in
            let s = { s with proof =
              Proof_global.copy_terminators ~src:s.proof ~tgt:pstate } in
@@ -714,7 +731,7 @@ end = struct (* {{{ *)
                (Summary.surgery_summary
                  (States.summary_of_state s.system)
                counters) } in
-           VCS.set_state id s
+           VCS.set_state id (Valid s)
     with VCS.Expired -> ()
 
   let exn_on id ?valid (e, info) =
@@ -753,20 +770,22 @@ end = struct (* {{{ *)
       cur_id := id;
       if feedback_processed then
         Hooks.(call state_computed id ~in_cache:false);
-      VCS.reached id true;
+      VCS.reached id;
       if Proof_global.there_are_pending_proofs () then
         VCS.goals id (Proof_global.get_open_goals ())
     with e ->
       let (e, info) = Errors.push e in
       let good_id = !cur_id in
-      cur_id := Stateid.dummy;
-      VCS.reached id false;
-      Hooks.(call unreachable_state id (e, info));
-      match Stateid.get info, safe_id with
-      | None, None -> iraise (exn_on id ~valid:good_id (e, info))
-      | None, Some good_id -> iraise (exn_on id ~valid:good_id (e, info))
-      | Some _, None -> iraise (e, info)
-      | Some (_,at), Some id -> iraise (e, Stateid.add info ~valid:id at)
+      VCS.reached id;
+      let ie =
+        match Stateid.get info, safe_id with
+        | None, None -> (exn_on id ~valid:good_id (e, info))
+        | None, Some good_id -> (exn_on id ~valid:good_id (e, info))
+        | Some _, None -> (e, info)
+        | Some (_,at), Some id -> (e, Stateid.add info ~valid:id at) in
+      if cache = `Yes || cache = `Shallow then freeze_invalid id ie;
+      Hooks.(call unreachable_state id ie);
+      Exninfo.iraise ie
 
 end (* }}} *)
 
@@ -842,7 +861,7 @@ end = struct (* {{{ *)
   let back_safe () =
     let id =
       fold_until (fun n (id,_,_,_,_) ->
-        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+        if n >= 0 && State.is_cached_and_valid id then `Stop id else `Cont (succ n))
         0 (VCS.get_branch_pos (VCS.current_branch ())) in
     backto id
 
@@ -1133,7 +1152,7 @@ end = struct (* {{{ *)
         let e_msg = iprint (e, info) in
         prerr_endline (fun () -> "failed with the following exception:");
         prerr_endline (fun () -> string_of_ppcmds e_msg);
-        let e_safe_states = List.filter State.is_cached my_states in
+        let e_safe_states = List.filter State.is_cached_and_valid my_states in
         RespError { e_error_at; e_safe_id; e_msg; e_safe_states }
   
   let perform_states query =
@@ -1151,12 +1170,12 @@ end = struct (* {{{ *)
       let prev =
         try
           let { next = prev; step } = VCS.visit id in
-          if State.is_cached prev && List.mem prev seen
+          if State.is_cached_and_valid prev && List.mem prev seen
           then Some (prev, State.get_cached prev, step)
           else None
         with VCS.Expired -> None in
       let this = 
-        if State.is_cached id then Some (State.get_cached id) else None in
+        if State.is_cached_and_valid id then Some (State.get_cached id) else None in
       match prev, this with
       | _, None -> None
       | Some (prev, o, `Cmd { cast = { expr }}), Some n
@@ -1724,7 +1743,7 @@ let collect_proof keep cur hd brkind id =
         let name = name ids in
         `ASync (parent last,proof_using_ast last,accn,name,delegate name)
     | `Fork((_, hd', GuaranteesOpacity, ids), _) when
-       has_proof_no_using last && not (State.is_cached (parent last)) &&
+       has_proof_no_using last && not (State.is_cached_and_valid (parent last)) &&
        !Flags.compilation_mode = Flags.BuildVio ->
         assert (VCS.Branch.equal hd hd'||VCS.Branch.equal hd VCS.edit_branch);
         (try
@@ -1760,7 +1779,7 @@ let collect_proof keep cur hd brkind id =
        let rc = collect (Some cur) [] id in
        if is_empty rc then make_sync `AlreadyEvaluated rc
        else if (keep == VtKeep || keep == VtKeepAsAxiom) &&
-          (not(State.is_cached id) || !Flags.async_proofs_full)
+          (not(State.is_cached_and_valid id) || !Flags.async_proofs_full)
        then check_policy rc
        else make_sync `AlreadyEvaluated rc
 
@@ -1808,9 +1827,9 @@ let known_state ?(redefine_qed=false) ~cache id =
   and reach ?(redefine_qed=false) ?(cache=cache) id =
     prerr_endline (fun () -> "reaching: " ^ Stateid.to_string id);
     if not redefine_qed && State.is_cached ~cache id then begin
-      State.install_cached id;
       Hooks.(call state_computed id ~in_cache:true);
-      prerr_endline (fun () -> "reached (cache)")
+      prerr_endline (fun () -> "reached (cache)");
+      State.install_cached id
     end else
     let step, cache_step, feedback_processed =
       let view = VCS.visit id in
@@ -1842,7 +1861,7 @@ let known_state ?(redefine_qed=false) ~cache id =
             reach view.next; vernac_interp id x;
             wall_clock_last_fork := Unix.gettimeofday ()
           ), `Yes, true
-      | `Fork ((x,_,_,_), Some prev) -> (fun () ->
+      | `Fork ((x,_,_,_), Some prev) -> (fun () -> (* nested proof *)
             reach ~cache:`Shallow prev;
             reach view.next;
             (try vernac_interp id x;
diff --git a/stm/stm.mli b/stm/stm.mli
index 6ffe0beb4..d825ff33e 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -122,7 +122,7 @@ type state = {
   proof : Proof_global.state;
   shallow : bool
 }
-val state_of_id : Stateid.t -> [ `Valid of state option | `Expired ]
+val state_of_id : Stateid.t -> [ `Valid of state option | `Expired | `Error of exn ]
 
 (** read-eval-print loop compatible interface ****************************** **)