STM: code refactoring

This is mainly shuffling code around and removing internal
refs that are not needed anymore.

7 files changed, 338 insertions, 297 deletions

diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 22e7c0243..fa7aa9584 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -251,7 +251,7 @@ module Make(T : Task) = struct
   let slave_ic = ref stdin
   let slave_oc = ref stdout
 
-  let slave_init_stdout () =
+  let init_stdout () =
     let ic, oc = Spawned.get_channels () in
     slave_oc := oc; slave_ic := ic
 
@@ -264,7 +264,7 @@ module Make(T : Task) = struct
 
   let slave_handshake () = WorkersPool.worker_handshake !slave_ic !slave_oc
 
-  let slave_main_loop reset =
+  let main_loop () =
     let feedback_queue = ref [] in
     let slave_feeder oc fb =
       match fb.Feedback.content with
@@ -293,7 +293,7 @@ module Make(T : Task) = struct
         flush_feeder !slave_oc;
         report_status "Idle";
         marshal_response !slave_oc response;
-        reset ()
+        Ephemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
@@ -328,3 +328,6 @@ module Make(T : Task) = struct
   let n_workers = WorkersPool.n_workers
 
 end
+
+module MakeQueue(T : Task) = struct include Make(T) end
+module MakeWorker(T : Task) = struct include Make(T) end
diff --git a/stm/asyncTaskQueue.mli b/stm/asyncTaskQueue.mli
index cd91ba129..96239d145 100644
--- a/stm/asyncTaskQueue.mli
+++ b/stm/asyncTaskQueue.mli
@@ -36,7 +36,7 @@ end
 
 type cancel_switch = bool ref
 
-module Make(T : Task) : sig
+module MakeQueue(T : Task) : sig
 
   (* Number of workers, 0 = lazy local *)
   val init : int -> unit
@@ -53,10 +53,6 @@ module Make(T : Task) : sig
   val join : unit -> unit
   val cancel_all : unit -> unit
 
-  (* slave process main loop *)
-  val slave_main_loop : (unit -> unit) -> unit
-  val slave_init_stdout : unit -> unit
-  
   val cancel_worker : string -> unit
 
   val set_order : (T.task -> T.task -> int) -> unit
@@ -69,3 +65,10 @@ module Make(T : Task) : sig
   val clear : unit -> unit
 
 end
+
+module MakeWorker(T : Task) : sig
+
+  val main_loop : unit -> unit
+  val init_stdout : unit -> unit
+  
+end
diff --git a/stm/proofworkertop.ml b/stm/proofworkertop.ml
index 0d1b44e49..c19f8bdd2 100644
--- a/stm/proofworkertop.ml
+++ b/stm/proofworkertop.ml
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module W = AsyncTaskQueue.MakeWorker(Stm.ProofTask)
+
 let () = Coqtop.toploop_init := (fun args ->
         Flags.make_silent true;
-        Stm.slave_init_stdout ();
+        W.init_stdout ();
         CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
         args)
 
-let () = Coqtop.toploop_run := Stm.slave_main_loop
+let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/queryworkertop.ml b/stm/queryworkertop.ml
index dbc188d51..8170f8cc6 100644
--- a/stm/queryworkertop.ml
+++ b/stm/queryworkertop.ml
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module W = AsyncTaskQueue.MakeWorker(Stm.QueryTask)
+
 let () = Coqtop.toploop_init := (fun args ->
         Flags.make_silent true;
-        Stm.queryslave_init_stdout ();
+        W.init_stdout ();
         CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
         args)
 
-let () = Coqtop.toploop_run := Stm.queryslave_main_loop
+let () = Coqtop.toploop_run := W.main_loop
 
diff --git a/stm/stm.ml b/stm/stm.ml
index bb48a4f00..15637afab 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -142,7 +142,7 @@ module Vcs_aux : sig
   exception Expired
   val visit : (branch_type, transaction,'i) Vcs_.t -> Vcs_.Dag.node -> visit
 
-end = struct
+end = struct (* {{{ *)
 
   let proof_nesting vcs =
     List.fold_left max 0
@@ -185,9 +185,13 @@ end = struct
       | _ -> anomaly (str ("Malformed VCS at node "^Stateid.to_string id))
     with Not_found -> raise Expired
 
-end
+end (* }}} *)
 
-(* Imperative wrap around VCS to obtain _the_ VCS *)
+(*************************** THE DOCUMENT *************************************)
+(******************************************************************************)
+
+(* Imperative wrap around VCS to obtain _the_ VCS that is the
+ * representation of the document Coq is currently processing *)
 module VCS : sig
 
   exception Expired
@@ -247,7 +251,7 @@ module VCS : sig
   val backup : unit -> vcs
   val restore : vcs -> unit
 
-end = struct
+end = struct (* {{{ *)
 
   include Vcs_
   exception Expired = Vcs_aux.Expired
@@ -508,74 +512,9 @@ end = struct
   let backup () = !vcs
   let restore v = vcs := v
 
-end
-
-
-(* TODO: Might not be the right place for this *)
-(* TODO: Currently, this mimics the process_goal function of ide/ide_slave.ml, 
- * but we have the opportunity to provide more structure in the xml, here. *)
-let process_goal sigma g =
-  let env = Goal.V82.env sigma g in
-  let id = Goal.uid g in
-  let ccl =
-    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
-    let ccl_string = string_of_ppcmds (Printer.pr_goal_concl_style_env env sigma norm_constr) in
-    Xml_datatype.Element ("conclusion", [], [Xml_datatype.PCData ccl_string]) in
-  let process_hyp env h_env acc =
-    let hyp_string = (string_of_ppcmds (Printer.pr_var_decl env sigma h_env)) in
-    (Xml_datatype.Element ("hypothesis", [], [Xml_datatype.PCData hyp_string])) :: acc in
-  let hyps = Xml_datatype.Element ("hypotheses", [], 
-    (List.rev (Environ.fold_named_context process_hyp env ~init:[]))) in
-  Xml_datatype.Element ("goal", [("id", id)], [hyps; ccl])
-
-let print_goals_of_state, forward_feedback =
-  let already_printed = ref Stateid.Set.empty in
-  let add_to_already_printed =
-    let m = Mutex.create () in
-    fun id ->
-      Mutex.lock m;
-      already_printed := Stateid.Set.add id !already_printed;
-      Mutex.unlock m in
-  (fun id ->
-    if Stateid.Set.mem id !already_printed then ()
-    else begin
-      add_to_already_printed id;
-      try
-        Option.iter (fun { proof = pstate } ->
-          let pfts = Proof_global.proof_of_state pstate in
-          let structured_goals = Proof.map_structured_proof pfts process_goal in
-          let xml_bg_goal = fun (l, r) -> Xml_datatype.Element("bg_goal", [], 
-              [Xml_datatype.Element("left_bg_goals", [], l); 
-               Xml_datatype.Element("right_bg_goals", [], r)]) in
+end (* }}} *)
 
-          let xml_structured_goals = Xml_datatype.Element("goals", [],
-            [ Xml_datatype.Element("focussed_goals", [], 
-                structured_goals.Proof.fg_goals);
-              Xml_datatype.Element("bg_goals", [], 
-                List.map xml_bg_goal structured_goals.Proof.bg_goals);
-              Xml_datatype.Element("shelved_goals", [], 
-                structured_goals.Proof.shelved_goals);
-              Xml_datatype.Element("given_up_goals", [], 
-                structured_goals.Proof.given_up_goals)
-            ]
-          ) in
-          Pp.feedback ~state_id:id
-           (Feedback.StructuredGoals (Loc.ghost, xml_structured_goals));
-          Pp.feedback ~state_id:id
-            (Feedback.Goals
-              (Loc.ghost, Pp.string_of_ppcmds
-                (Printer.pr_open_subgoals
-                  ~proof:(Proof_global.proof_of_state pstate) ()))))
-            (VCS.get_info id).state
-      with Proof_global.NoCurrentProof -> ()
-  end),
-  fun id -> function
-    | Feedback.Goals _ as msg ->
-        add_to_already_printed id;
-        Pp.feedback ~state_id:id msg
-    | msg -> Pp.feedback ~state_id:id msg
-
-(* Fills in the nodes of the VCS *)
+(****** A cache: fills in the nodes of the VCS document with their value ******)
 module State : sig
   
   (** The function is from unit, so it uses the current state to define
@@ -598,7 +537,7 @@ module State : sig
   val get_cached : Stateid.t -> frozen_state
   val assign : Stateid.t -> frozen_state -> unit
 
-end = struct
+end = struct (* {{{ *)
 
   (* cur_id holds Stateid.dummy in case the last attempt to define a state
    * failed, so the global state may contain garbage *)
@@ -691,7 +630,208 @@ end = struct
       | Some _, None -> raise e
       | Some (_,at), Some id -> raise (Stateid.add e ~valid:id at)
 
-end
+end (* }}} *)
+
+
+(****************************** CRUFT *****************************************)
+(******************************************************************************)
+
+(* TODO: Currently, this mimics the process_goal function of ide/ide_slave.ml, 
+ * but we have the opportunity to provide more structure in the xml, here. *)
+let process_goal sigma g =
+  let env = Goal.V82.env sigma g in
+  let id = Goal.uid g in
+  let ccl =
+    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
+    let ccl_string = string_of_ppcmds (Printer.pr_goal_concl_style_env env sigma norm_constr) in
+    Xml_datatype.Element ("conclusion", [], [Xml_datatype.PCData ccl_string]) in
+  let process_hyp env h_env acc =
+    let hyp_string = (string_of_ppcmds (Printer.pr_var_decl env sigma h_env)) in
+    (Xml_datatype.Element ("hypothesis", [], [Xml_datatype.PCData hyp_string])) :: acc in
+  let hyps = Xml_datatype.Element ("hypotheses", [], 
+    (List.rev (Environ.fold_named_context process_hyp env ~init:[]))) in
+  Xml_datatype.Element ("goal", [("id", id)], [hyps; ccl])
+
+let print_goals_of_state, forward_feedback =
+  let already_printed = ref Stateid.Set.empty in
+  let add_to_already_printed =
+    let m = Mutex.create () in
+    fun id ->
+      Mutex.lock m;
+      already_printed := Stateid.Set.add id !already_printed;
+      Mutex.unlock m in
+  (fun id ->
+    if Stateid.Set.mem id !already_printed then ()
+    else begin
+      add_to_already_printed id;
+      try
+        Option.iter (fun { proof = pstate } ->
+          let pfts = Proof_global.proof_of_state pstate in
+          let structured_goals = Proof.map_structured_proof pfts process_goal in
+          let xml_bg_goal = fun (l, r) -> Xml_datatype.Element("bg_goal", [], 
+              [Xml_datatype.Element("left_bg_goals", [], l); 
+               Xml_datatype.Element("right_bg_goals", [], r)]) in
+
+          let xml_structured_goals = Xml_datatype.Element("goals", [],
+            [ Xml_datatype.Element("focussed_goals", [], 
+                structured_goals.Proof.fg_goals);
+              Xml_datatype.Element("bg_goals", [], 
+                List.map xml_bg_goal structured_goals.Proof.bg_goals);
+              Xml_datatype.Element("shelved_goals", [], 
+                structured_goals.Proof.shelved_goals);
+              Xml_datatype.Element("given_up_goals", [], 
+                structured_goals.Proof.given_up_goals)
+            ]
+          ) in
+          Pp.feedback ~state_id:id
+           (Feedback.StructuredGoals (Loc.ghost, xml_structured_goals));
+          Pp.feedback ~state_id:id
+            (Feedback.Goals
+              (Loc.ghost, Pp.string_of_ppcmds
+                (Printer.pr_open_subgoals
+                  ~proof:(Proof_global.proof_of_state pstate) ()))))
+            (VCS.get_info id).state
+      with Proof_global.NoCurrentProof -> ()
+  end),
+  fun id -> function
+    | Feedback.Goals _ as msg ->
+        add_to_already_printed id;
+        Pp.feedback ~state_id:id msg
+    | msg -> Pp.feedback ~state_id:id msg
+
+(* The backtrack module simulates the classic behavior of a linear document *)
+module Backtrack : sig
+
+  val record : unit -> unit
+  val backto : Stateid.t -> unit
+  val back_safe : unit -> unit
+
+  (* we could navigate the dag, but this ways easy *)
+  val branches_of : Stateid.t -> backup
+
+  (* To be installed during initialization *)
+  val undo_vernac_classifier : vernac_expr -> vernac_classification
+
+end = struct (* {{{ *)
+
+  let record () =
+    List.iter (fun current_branch ->
+      let mine = current_branch, VCS.get_branch current_branch in
+      let info = VCS.get_info (VCS.get_branch_pos current_branch) in
+      let others =
+        CList.map_filter (fun b ->
+          if Vcs_.Branch.equal b current_branch then None
+          else Some(b, VCS.get_branch b)) (VCS.branches ()) in
+      let backup = if fst info.vcs_backup <> None then fst info.vcs_backup
+        else Some (VCS.backup ()) in
+      let branches = if snd info.vcs_backup <> None then snd info.vcs_backup
+        else Some { mine; others } in
+      info.vcs_backup <- backup, branches)
+    [VCS.current_branch (); VCS.Branch.master]
+
+  let backto oid =
+    let info = VCS.get_info oid in
+    match info.vcs_backup with
+    | None, _ ->
+       anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
+               str": a state with no vcs_backup")
+    | Some vcs, _ -> VCS.restore vcs
+
+  let branches_of id =
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | _, None ->
+       anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
+               str": a state with no vcs_backup")
+    | _, Some x -> x
+
+  let rec fold_until f acc id =
+    let next acc =
+      if id = Stateid.initial then raise Not_found
+      else fold_until f acc (VCS.visit id).next in
+    let info = VCS.get_info id in
+    match info.vcs_backup with
+    | None, _ -> next acc
+    | Some vcs, _ ->
+        let ids =
+          if id = Stateid.initial || id = Stateid.dummy then [] else
+          match VCS.visit id with
+          | { step = `Fork ((_,_,_,l),_) } -> l
+          | { step = `Cmd { cids = l } } -> l
+          | _ -> [] in
+        match f acc (id, vcs, ids) with
+        | `Stop x -> x
+        | `Cont acc -> next acc
+ 
+  let back_safe () =
+    let id =
+      fold_until (fun n (id,_,_) ->
+        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
+        0 (VCS.get_branch_pos (VCS.current_branch ())) in
+    backto id
+
+  let undo_vernac_classifier v =
+    try
+      match v with
+      | VernacResetInitial ->
+          VtStm (VtBack Stateid.initial, true), VtNow
+      | VernacResetName (_,name) ->
+          msg_warning
+            (str"Reset not implemented for automatically generated constants");
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          (try
+            let oid =
+              fold_until (fun b (id,_,label) ->
+                if b then `Stop id else `Cont (List.mem name label))
+              false id in
+            VtStm (VtBack oid, true), VtNow
+          with Not_found ->
+            VtStm (VtBack id, true), VtNow)
+      | VernacBack n ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
+          VtStm (VtBack oid, true), VtNow
+      | VernacUndo n ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
+          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
+             not !Flags.print_emacs then
+           VtStm (VtBack oid, false), VtNow
+          else VtStm (VtBack oid, true), VtLater
+      | VernacUndoTo _
+      | VernacRestart as e ->
+          let m = match e with VernacUndoTo m -> m | _ -> 0 in
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let vcs =
+            match (VCS.get_info id).vcs_backup with 
+            | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
+            | Some vcs, _ -> vcs in
+          let cb, _ =
+            Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
+          let n = fold_until (fun n (_,vcs,_) ->
+            if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
+            0 id in
+          let oid = fold_until (fun n (id,_,_) ->
+            if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
+          VtStm (VtBack oid, true), VtLater
+      | VernacAbortAll ->
+          let id = VCS.get_branch_pos (VCS.current_branch ()) in
+          let oid = fold_until (fun () (id,vcs,_) ->
+            match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
+            () id in
+          VtStm (VtBack oid, true), VtLater
+      | VernacBacktrack (id,_,_)
+      | VernacBackTo id ->
+          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
+      | _ -> VtUnknown, VtNow
+    with
+    | Not_found ->
+       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
+       VtStm (VtBack Stateid.initial, true), VtNow
+
+end (* }}} *)
 
 let hints = ref Aux_file.empty_aux_file
 let set_compilation_hints file =
@@ -719,10 +859,29 @@ let _ = Errors.register_handler (function
   | RemoteException ppcmd -> ppcmd
   | _ -> raise Unhandled)
 
-module Task = struct
+(****************************** THE SCHEDULER *********************************)
+(******************************************************************************)
 
-  let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
-  let set_reach_known_state f = reach_known_state := f
+module rec ProofTask : sig
+ 
+  type task = {
+    t_exn_info : Stateid.t * Stateid.t;
+    t_start    : Stateid.t;
+    t_stop     : Stateid.t;
+    t_assign   : Proof_global.closed_proof_output Future.assignement -> unit;
+    t_loc      : Loc.t;
+    t_uuid     : Future.UUID.t;
+    t_name     : string }   
+
+  include AsyncTaskQueue.Task with type task := task
+
+  val build_proof_here :
+    Stateid.t * Stateid.t -> Loc.t -> Stateid.t ->
+      Proof_global.closed_proof_output Future.computation
+  val build_proof_here_core :
+    Loc.t -> Stateid.t -> unit -> Proof_global.closed_proof_output
+   
+end = struct (* {{{ *)
 
   let forward_feedback = forward_feedback
 
@@ -792,8 +951,8 @@ module Task = struct
 
   let build_proof_here_core loc eop () =
     let wall_clock1 = Unix.gettimeofday () in
-    if !Flags.batch_mode then !reach_known_state ~cache:`No eop
-    else !reach_known_state ~cache:`Shallow eop;
+    if !Flags.batch_mode then Reach.known_state ~cache:`No eop
+    else Reach.known_state ~cache:`Shallow eop;
     let wall_clock2 = Unix.gettimeofday () in
     Aux_file.record_in_aux_at loc "proof_build_time"
       (Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
@@ -862,10 +1021,10 @@ module Task = struct
       flush_all (); exit 1
     end
 
-end
+end (* }}} *)
 
 (* Slave processes (if initialized, otherwise local lazy evaluation) *)
-module Slaves : sig
+and Slaves : sig
 
   (* (eventually) remote calls *)
   val build_proof : loc:Loc.t ->
@@ -878,10 +1037,6 @@ module Slaves : sig
   (* initialize the whole machinery (optional) *)
   val init : unit -> unit
 
-  (* slave process main loop *)
-  val slave_main_loop : (unit -> unit) -> unit
-  val slave_init_stdout : unit -> unit
-
   type 'a tasks = ('a,VCS.vcs) Stateid.request list
   val dump_snapshot : unit -> Future.UUID.t tasks
   val check_task : string -> int tasks -> int -> bool
@@ -897,9 +1052,9 @@ module Slaves : sig
 
   val set_perspective : Stateid.t list -> unit
 
-end = struct
+end = struct (* {{{ *)
 
-  module TaskQueue = AsyncTaskQueue.Make(Task)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(ProofTask)
 
   let check_task_aux extra name l i =
     let { Stateid.stop; document; loc; name = r_name } = List.nth l i in
@@ -907,7 +1062,7 @@ end = struct
       str(Printf.sprintf "Checking task %d (%s%s) of %s" i r_name extra name));
     VCS.restore document;
     try
-      !Task.reach_known_state ~cache:`No stop;
+      Reach.known_state ~cache:`No stop;
       (* The original terminator, a hook, has not been saved in the .vi*)
       Proof_global.set_terminator
         (Lemmas.standard_proof_terminator []
@@ -991,8 +1146,8 @@ end = struct
     let open Stateid in
     let p = List.fold_right Set.add idl Set.empty in
     TaskQueue.set_order (fun task1 task2 ->
-      let { Task.t_start = a1; Task.t_stop = b1 } = task1 in
-      let { Task.t_start = a2; Task.t_stop = b2 } = task2 in
+      let { ProofTask.t_start = a1; t_stop = b1 } = task1 in
+      let { ProofTask.t_start = a2; t_stop = b2 } = task2 in
       match Set.mem a1 p || Set.mem b1 p, Set.mem a2 p || Set.mem b2 p with
       | true, true | false, false -> 0
       | true, false -> -1
@@ -1003,28 +1158,26 @@ end = struct
     if TaskQueue.n_workers () = 0 then
       if !Flags.compilation_mode = Flags.BuildVi then begin
         let force () : Proof_global.closed_proof_output Future.assignement =
-          try `Val (Task.build_proof_here_core loc stop ())
+          try `Val (ProofTask.build_proof_here_core loc stop ())
           with e -> let e = Errors.push e in `Exn e in
         let f,assign = Future.create_delegate ~force (State.exn_on id ~valid) in
         let t_uuid = Future.uuid f in
         TaskQueue.enqueue_task {
-          Task.t_exn_info; t_start = start; t_stop = stop; t_assign = assign;
-          t_loc = loc; t_uuid; t_name = name } cancel_switch;
+          ProofTask.t_exn_info; t_start = start; t_stop = stop;
+          t_assign = assign; t_loc = loc; t_uuid; t_name = name } cancel_switch;
         f, cancel_switch
       end else
-        Task.build_proof_here t_exn_info loc stop, cancel_switch
+        ProofTask.build_proof_here t_exn_info loc stop, cancel_switch
     else 
       let f, t_assign = Future.create_delegate (State.exn_on id ~valid) in
       let t_uuid = Future.uuid f in
       Pp.feedback (Feedback.InProgress 1);
       TaskQueue.enqueue_task {
-        Task.t_exn_info; t_start = start; t_stop = stop; t_assign; t_loc = loc;
-        t_uuid; t_name = name } cancel_switch;
+        ProofTask.t_exn_info; t_start = start; t_stop = stop; t_assign;
+        t_loc = loc; t_uuid; t_name = name } cancel_switch;
       f, cancel_switch
 
   let init () = TaskQueue.init !Flags.async_proofs_n_workers
-  let slave_main_loop = TaskQueue.slave_main_loop
-  let slave_init_stdout = TaskQueue.slave_init_stdout
   let wait_all_done = TaskQueue.join
 
   let cancel_worker = TaskQueue.cancel_worker
@@ -1034,16 +1187,27 @@ end = struct
   let dump_snapshot () =
     let tasks = TaskQueue.snapshot () in
     prerr_endline (Printf.sprintf "dumping %d tasks\n" (List.length tasks));
-    CList.map_filter (Task.request_of_task `Fresh) tasks
+    CList.map_filter (ProofTask.request_of_task `Fresh) tasks
 
   let reset_task_queue () = TaskQueue.clear ()
 
-end
+end (* }}} *)
 
-module SubTask = struct
+and TacTask : sig
 
-  let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
-  let set_reach_known_state f = reach_known_state := f
+  type output = Constr.constr * Evd.evar_universe_context
+  type task = {
+    t_state    : Stateid.t;
+    t_state_fb : Stateid.t;
+    t_assign   : output Future.assignement -> unit;
+    t_ast      : ast;
+    t_goal     : Goal.goal;
+    t_kill     : unit -> unit;
+    t_name     : string }  
+
+  include AsyncTaskQueue.Task with type task := task
+
+end = struct (* {{{ *)
 
   type output = Constr.constr * Evd.evar_universe_context
   
@@ -1104,7 +1268,7 @@ module SubTask = struct
   let perform { r_state = id; r_state_fb; r_document = vcs; r_ast; r_goal } =
     Option.iter VCS.restore vcs;
     try
-      !reach_known_state ~cache:`No id;
+      Reach.known_state ~cache:`No id;
       let t, uc = Future.purify (fun () ->
         vernac_interp r_state_fb r_ast;
         let _,_,_,_,sigma = Proof.proof (Proof_global.give_me_the_proof ()) in
@@ -1122,15 +1286,21 @@ module SubTask = struct
   let name_of_task { t_name } = t_name
   let name_of_request { r_name } = r_name
   
-end
+end (* }}} *)
 
-module Partac = struct
+and Partac : sig
+
+  val vernac_interp :
+    cancel_switch -> int -> Stateid.t -> Stateid.t -> ast -> unit
+
+end = struct (* {{{ *)
     
-  module TaskQueue = AsyncTaskQueue.Make(SubTask)
+  module TaskQueue = AsyncTaskQueue.MakeQueue(TacTask)
 
   let vernac_interp cancel nworkers safe_id id { verbose; loc; expr = e } =
     let e, etac, time, fail =
-      let rec find time fail = function VernacSolve(_,_,re,b) -> re, b, time, fail
+      let rec find time fail = function
+        | VernacSolve(_,_,re,b) -> re, b, time, fail
         | VernacTime [_,e] -> find true fail e
         | VernacFail e -> find time true e
         | _ -> errorlabstrm "Stm" (str"unsupported") in find false false e in
@@ -1139,10 +1309,11 @@ module Partac = struct
     ignore(TaskQueue.with_n_workers nworkers (fun ~join ~cancel_all ->
     Proof_global.with_current_proof (fun _ p ->
       let goals, _, _, _, _ = Proof.proof p in
-      let open SubTask in
+      let open TacTask in
       let res = CList.map_i (fun i g ->
         let f,assign= Future.create_delegate (State.exn_on id ~valid:safe_id) in
-        let t_ast = { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
+        let t_ast =
+          { verbose;loc;expr = VernacSolve(SelectNth i,None,e,etac) } in
         let t_name = Goal.uid g in
         TaskQueue.enqueue_task
           { t_state = safe_id; t_state_fb = id;
@@ -1172,17 +1343,14 @@ module Partac = struct
             re_sig [g] sigma) in
       Proof.run_tactic (Global.env()) assign_tac p)))) ())
   
-  let slave_main_loop = TaskQueue.slave_main_loop
-  let slave_init_stdout = TaskQueue.slave_init_stdout
+end (* }}} *)
 
-end
+and QueryTask : sig
 
-let tacslave_main_loop () = Partac.slave_main_loop Ephemeron.clear
-let tacslave_init_stdout = Partac.slave_init_stdout
+  type task = { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
+  include AsyncTaskQueue.Task with type task := task
 
-module QueryTask = struct
-  let reach_known_state = ref (fun ?redefine_qed ~cache id -> ())
-  let set_reach_known_state f = reach_known_state := f
+end = struct (* {{{ *)
   
   type task =
     { t_where : Stateid.t; t_for : Stateid.t ; t_what : ast }
@@ -1216,7 +1384,7 @@ module QueryTask = struct
   let perform { r_where; r_doc; r_what; r_for } =
     VCS.restore r_doc;
     VCS.print ();
-    !reach_known_state ~cache:`No r_where;
+    Reach.known_state ~cache:`No r_where;
     try
       vernac_interp r_for { r_what with verbose = true };
       Pp.feedback ~state_id:r_for Feedback.Processed     
@@ -1227,33 +1395,34 @@ module QueryTask = struct
   let name_of_task { t_what } = string_of_ppcmds (pr_ast t_what)
   let name_of_request { r_what } = string_of_ppcmds (pr_ast r_what)
 
-end
+end (* }}} *)
 
-module Query = struct
+and Query : sig 
 
-  module TaskQueue = AsyncTaskQueue.Make(QueryTask)
+  val init : unit -> unit
+  val vernac_interp : cancel_switch -> Stateid.t ->  Stateid.t -> ast -> unit
+
+end = struct (* {{{ *)
+
+  module TaskQueue = AsyncTaskQueue.MakeQueue(QueryTask)
 
   let vernac_interp switch prev id q =
     assert(TaskQueue.n_workers () > 0);
     TaskQueue.enqueue_task
-      QueryTask.({ t_where = prev; t_for = id; t_what = q }) switch
+      QueryTask.({ QueryTask.t_where = prev; t_for = id; t_what = q }) switch
 
-  let slave_main_loop = TaskQueue.slave_main_loop
-  let slave_init_stdout = TaskQueue.slave_init_stdout
   let init () = TaskQueue.init 
     (if !Flags.async_queries_always_delegate then 1 else 0)
-end
 
-let queryslave_main_loop () = Query.slave_main_loop Ephemeron.clear
-let queryslave_init_stdout = Query.slave_init_stdout
+end (* }}} *)
 
 (* Runs all transactions needed to reach a state *)
-module Reach : sig
+and Reach : sig
 
   val known_state :
     ?redefine_qed:bool -> cache:Summary.marshallable -> Stateid.t -> unit
 
-end = struct
+end = struct (* {{{ *)
 
 let pstate = ["meta counter"; "evar counter"; "program-tcc-table"]
 
@@ -1496,145 +1665,10 @@ let known_state ?(redefine_qed=false) ~cache id =
     prerr_endline ("reached: "^ Stateid.to_string id) in
   reach ~redefine_qed id
 
-end
-
-let _ = Task.set_reach_known_state Reach.known_state
-let _ = SubTask.set_reach_known_state Reach.known_state
-let _ = QueryTask.set_reach_known_state Reach.known_state
+end (* }}} *)
 
-(* The backtrack module simulates the classic behavior of a linear document *)
-module Backtrack : sig
-
-  val record : unit -> unit
-  val backto : Stateid.t -> unit
-  val back_safe : unit -> unit
-
-  (* we could navigate the dag, but this ways easy *)
-  val branches_of : Stateid.t -> backup
-
-  (* To be installed during initialization *)
-  val undo_vernac_classifier : vernac_expr -> vernac_classification
-
-end = struct
-
-  let record () =
-    List.iter (fun current_branch ->
-      let mine = current_branch, VCS.get_branch current_branch in
-      let info = VCS.get_info (VCS.get_branch_pos current_branch) in
-      let others =
-        CList.map_filter (fun b ->
-          if Vcs_.Branch.equal b current_branch then None
-          else Some(b, VCS.get_branch b)) (VCS.branches ()) in
-      let backup = if fst info.vcs_backup <> None then fst info.vcs_backup
-        else Some (VCS.backup ()) in
-      let branches = if snd info.vcs_backup <> None then snd info.vcs_backup
-        else Some { mine; others } in
-      info.vcs_backup <- backup, branches)
-    [VCS.current_branch (); VCS.Branch.master]
-
-  let backto oid =
-    let info = VCS.get_info oid in
-    match info.vcs_backup with
-    | None, _ ->
-       anomaly(str"Backtrack.backto "++str(Stateid.to_string oid)++
-               str": a state with no vcs_backup")
-    | Some vcs, _ -> VCS.restore vcs
-
-  let branches_of id =
-    let info = VCS.get_info id in
-    match info.vcs_backup with
-    | _, None ->
-       anomaly(str"Backtrack.branches_of "++str(Stateid.to_string id)++
-               str": a state with no vcs_backup")
-    | _, Some x -> x
-
-  let rec fold_until f acc id =
-    let next acc =
-      if id = Stateid.initial then raise Not_found
-      else fold_until f acc (VCS.visit id).next in
-    let info = VCS.get_info id in
-    match info.vcs_backup with
-    | None, _ -> next acc
-    | Some vcs, _ ->
-        let ids =
-          if id = Stateid.initial || id = Stateid.dummy then [] else
-          match VCS.visit id with
-          | { step = `Fork ((_,_,_,l),_) } -> l
-          | { step = `Cmd { cids = l } } -> l
-          | _ -> [] in
-        match f acc (id, vcs, ids) with
-        | `Stop x -> x
-        | `Cont acc -> next acc
- 
-  let back_safe () =
-    let id =
-      fold_until (fun n (id,_,_) ->
-        if n >= 0 && State.is_cached id then `Stop id else `Cont (succ n))
-        0 (VCS.get_branch_pos (VCS.current_branch ())) in
-    backto id
-
-  let undo_vernac_classifier v =
-    try
-      match v with
-      | VernacResetInitial ->
-          VtStm (VtBack Stateid.initial, true), VtNow
-      | VernacResetName (_,name) ->
-          msg_warning
-            (str"Reset not implemented for automatically generated constants");
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          (try
-            let oid =
-              fold_until (fun b (id,_,label) ->
-                if b then `Stop id else `Cont (List.mem name label))
-              false id in
-            VtStm (VtBack oid, true), VtNow
-          with Not_found ->
-            VtStm (VtBack id, true), VtNow)
-      | VernacBack n ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          VtStm (VtBack oid, true), VtNow
-      | VernacUndo n ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then `Stop id else `Cont (n-1)) n id in
-          if n = 1 && !Flags.coqtop_ui && not !Flags.batch_mode &&
-             not !Flags.print_emacs then
-           VtStm (VtBack oid, false), VtNow
-          else VtStm (VtBack oid, true), VtLater
-      | VernacUndoTo _
-      | VernacRestart as e ->
-          let m = match e with VernacUndoTo m -> m | _ -> 0 in
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let vcs =
-            match (VCS.get_info id).vcs_backup with 
-            | None, _ -> anomaly(str"Backtrack: tip with no vcs_backup")
-            | Some vcs, _ -> vcs in
-          let cb, _ =
-            Vcs_aux.find_proof_at_depth vcs (Vcs_aux.proof_nesting vcs) in
-          let n = fold_until (fun n (_,vcs,_) ->
-            if List.mem cb (Vcs_.branches vcs) then `Cont (n+1) else `Stop n)
-            0 id in
-          let oid = fold_until (fun n (id,_,_) ->
-            if Int.equal n 0 then `Stop id else `Cont (n-1)) (n-m-1) id in
-          VtStm (VtBack oid, true), VtLater
-      | VernacAbortAll ->
-          let id = VCS.get_branch_pos (VCS.current_branch ()) in
-          let oid = fold_until (fun () (id,vcs,_) ->
-            match Vcs_.branches vcs with [_] -> `Stop id | _ -> `Cont ())
-            () id in
-          VtStm (VtBack oid, true), VtLater
-      | VernacBacktrack (id,_,_)
-      | VernacBackTo id ->
-          VtStm (VtBack (Stateid.of_int id), not !Flags.print_emacs), VtNow
-      | _ -> VtUnknown, VtNow
-    with
-    | Not_found ->
-       msg_warning(str"undo_vernac_classifier: going back to the initial state.");
-       VtStm (VtBack Stateid.initial, true), VtNow
-
-end
+(********************************* STM API ************************************)
+(******************************************************************************)
 
 let init () =
   VCS.init Stateid.initial;
@@ -1660,10 +1694,6 @@ let init () =
     with Not_found -> () end;
   end
 
-let slave_main_loop () = Slaves.slave_main_loop Ephemeron.clear
-
-let slave_init_stdout () = Slaves.slave_init_stdout ()
-
 let observe id =
   let vcs = VCS.backup () in
   try
@@ -1783,6 +1813,7 @@ let snapshot_vi ldir long_f_dot_v =
 
 let reset_task_queue = Slaves.reset_task_queue
 
+(* Document building *)
 let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
   let warn_if_pos a b =
     if b then msg_warning(pr_ast a ++ str" should not be part of a script") in
@@ -1963,8 +1994,6 @@ let process_transaction ?(newtip=Stateid.fresh ()) ~tty verbose c (loc, expr) =
     let e = Errors.push e in
     handle_failure e vcs tty
 
-(** STM interface ******************************************************* **)
-  
 let print_ast id =
   try
     match VCS.visit id with
@@ -1977,7 +2006,6 @@ let print_ast id =
         xml;
     | _ -> Xml_datatype.PCData "ERROR"
   with _ -> Xml_datatype.PCData "ERROR"
- 
 
 let stop_worker n = Slaves.cancel_worker n
 
@@ -2112,14 +2140,16 @@ let edit_at id =
     match Stateid.get e with
     | None ->
         VCS.print ();
-        anomaly (str ("edit_at "^Stateid.to_string id^": "^string_of_ppcmds (Errors.print_no_report e)))
+        anomaly (str ("edit_at "^Stateid.to_string id^": ") ++
+          Errors.print_no_report e)
     | Some (_, id) ->
         prerr_endline ("Failed at state " ^ Stateid.to_string id);
         VCS.restore vcs;
         VCS.print ();
         raise e
 
-(** Old tty interface *************************************************** **)
+(*********************** TTY API (PG, coqtop, coqc) ***************************)
+(******************************************************************************)
 
 let interp verb (_,e as lexpr) =
   let clas = classify_vernac e in
diff --git a/stm/stm.mli b/stm/stm.mli
index 2e133f1eb..48e1ca4e4 100644
--- a/stm/stm.mli
+++ b/stm/stm.mli
@@ -72,13 +72,6 @@ val get_current_state : unit -> Stateid.t
 
 (* Misc *)
 val init : unit -> unit
-val slave_main_loop : unit -> unit
-val slave_init_stdout : unit -> unit
-val tacslave_main_loop : unit -> unit
-val tacslave_init_stdout : unit -> unit
-val queryslave_main_loop : unit -> unit
-val queryslave_init_stdout : unit -> unit
-
 val print_ast : Stateid.t -> Xml_datatype.xml
 
 (* Filename *)
@@ -87,6 +80,12 @@ val set_compilation_hints : string -> unit
 (* Reorders the task queue putting forward what is in the perspective *)
 val set_perspective : Stateid.t list -> unit
 
+(** workers **************************************************************** **)
+
+module ProofTask : AsyncTaskQueue.Task
+module TacTask   : AsyncTaskQueue.Task
+module QueryTask : AsyncTaskQueue.Task
+
 (** read-eval-print loop compatible interface ****************************** **)
 
 (* Adds a new line to the document.  It replaces the core of Vernac.interp.
diff --git a/stm/tacworkertop.ml b/stm/tacworkertop.ml
index 5e3d90c75..1c1542a61 100644
--- a/stm/tacworkertop.ml
+++ b/stm/tacworkertop.ml
@@ -6,11 +6,13 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+module W = AsyncTaskQueue.MakeWorker(Stm.TacTask)
+
 let () = Coqtop.toploop_init := (fun args ->
         Flags.make_silent true;
-        Stm.tacslave_init_stdout ();
+        W.init_stdout ();
         CoqworkmgrApi.init !Flags.async_proofs_worker_priority;
         args)
 
-let () = Coqtop.toploop_run := Stm.tacslave_main_loop
+let () = Coqtop.toploop_run := W.main_loop