State Transaction Machine

The process_transaction function adds a new edge to the Dag without
executing the transaction (when possible).

The observe id function runs the transactions necessary to reach to the
state id.  Transaction being on a merged branch are not executed but
stored into a future.

The finish function calls observe on the tip of the current branch.

Imperative modifications to the environment made by some tactics are
now explicitly declared by the tactic and modeled as let-in/beta-redexes
at the root of the proof term. An example is the abstract tactic.

This is the work described in the Coq Workshop 2012 paper.

Coq is compile with thread support from now on.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16674 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 49 insertions, 26 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 45b7c084d7..8a2c7617c6 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -26,7 +26,8 @@ open Util
 type proofview = {
      initial : (Term.constr * Term.types) list;
      solution : Evd.evar_map;
-     comb : Goal.goal list
+     comb : Goal.goal list;
+     side_effects : Declareops.side_effects
      }
 
 let proofview p =
@@ -38,7 +39,8 @@ let init =
   let rec aux = function
   | [] ->  { initial = [] ; 
 	     solution = Evd.empty ;
-	     comb = []
+             comb = [];
+             side_effects = Declareops.no_seff
 	   }
   | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } =
                            aux l
@@ -50,12 +52,15 @@ let init =
 			 let gl = Goal.build e in
 			 { initial = (econstr,typ)::ret;
 			   solution = new_defs ;
-			   comb = gl::comb }
+                           comb = gl::comb;
+                           side_effects = Declareops.no_seff }
   in
   fun l -> let v = aux l in
     (* Marks all the goal unresolvable for typeclasses. *)
     { v with solution = Typeclasses.mark_unresolvables v.solution }
 
+let initial_goals { initial } = initial
+
 (* Returns whether this proofview is finished or not. That is,
    if it has empty subgoals in the comb. There could still be unsolved
    subgoaled, but they would then be out of the view, focused out. *)
@@ -64,8 +69,13 @@ let finished = function
   | _  -> false
 
 (* Returns the current value of the proofview partial proofs. *)
-let return { initial=init; solution=defs }  =
-  List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init
+let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff
+
+let partial_proof pv =
+  List.map fst (List.map (return pv) (List.map fst (initial_goals pv)))
+
+let emit_side_effects eff x =
+  { x with side_effects = Declareops.union_side_effects eff x.side_effects }
 
 (* spiwack: this function should probably go in the Util section,
     but I'd rather have Util (or a separate module for lists)
@@ -356,8 +366,8 @@ let rec catchable_exception = function
    [s] to each goal successively and applying [k] to each result. *)
 let list_of_sensitive s k env step =
   Goal.list_map begin fun defs g ->
-    let (a,defs) = Goal.eval s env defs g in
-    (k a) , defs
+    let (a,defs,effs) = Goal.eval s env defs g in
+    (k a) , defs, effs
   end step.comb step.solution
 (* In form of a tactic *)
 let list_of_sensitive s k env =
@@ -366,8 +376,10 @@ let list_of_sensitive s k env =
   let (>>) = Inner.seq in
   Inner.get >>= fun step ->
   try 
-    let (tacs,defs) = list_of_sensitive s k env step in
-    Inner.set { step with solution = defs } >>
+    let (tacs,defs,effs) = list_of_sensitive s k env step in
+    Inner.set { step with solution = defs;
+      side_effects = Declareops.union_side_effects step.side_effects 
+        (Declareops.flatten_side_effects effs) } >>
     Inner.return tacs
   with e when catchable_exception e ->
     tclZERO e env
@@ -388,19 +400,22 @@ let tclGOALBINDU s k =
 (* No backtracking can happen here, hence, as opposed to the dispatch tacticals,
     everything is done in one step. *)
 let sensitive_on_proofview s env step =
-  let wrap g ((defs, partial_list) as partial_res) = 
+  let wrap g ((defs, partial_list, partial_eff) as partial_res) = 
     match Goal.advance defs g with
-    | None ->partial_res
+    | None -> partial_res
     | Some g ->
-      let {Goal.subgoals = sg } , d' = Goal.eval s env defs g in
-      (d',sg::partial_list)
+      let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in
+      (d', sg::partial_list, eff::partial_eff)
   in
-  let ( new_defs , combed_subgoals ) = 
-    List.fold_right wrap step.comb (step.solution,[])
+  let ( new_defs , combed_subgoals, side_effects ) = 
+    List.fold_right wrap step.comb (step.solution,[],[])
   in
   { step with
      solution = new_defs;
-     comb = List.flatten combed_subgoals }
+     comb = List.flatten combed_subgoals;
+     side_effects =
+       Declareops.union_side_effects
+         (Declareops.flatten_side_effects side_effects) step.side_effects }
 let tclSENSITIVE s env =
   (* spiwack: convenience notations, waiting for ocaml 3.12 *)
   let (>>=) = Inner.bind in
@@ -440,18 +455,26 @@ module V82 = struct
     Inner.get >>= fun ps ->
     try
       let tac evd gl = 
-        let glsigma  = tac { Evd.it = gl ; Evd.sigma = evd }  in
+        let glsigma  =
+          tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff }  in
         let sigma = glsigma.Evd.sigma in
         let g = glsigma.Evd.it in
-        ( g , sigma )
+        ( g, sigma, glsigma.Evd.eff )
       in
     (* Old style tactics expect the goals normalized with respect to evars. *)
-      let (initgoals,initevd) = 
-        Goal.list_map Goal.V82.nf_evar ps.comb ps.solution
+      let no_side_eff f x y =
+        let a, b = f x y in a, b, Declareops.no_seff in
+      let (initgoals,initevd, eff1) = 
+        Goal.list_map (no_side_eff Goal.V82.nf_evar) ps.comb ps.solution
       in
-      let (goalss,evd) = Goal.list_map tac initgoals initevd in
+      let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in
       let sgs = List.flatten goalss in
-      Inner.set { ps with solution=evd ; comb=sgs }
+      Inner.set { ps with solution=evd ; comb=sgs; 
+        side_effects =
+          Declareops.union_side_effects ps.side_effects 
+            (Declareops.union_side_effects 
+              (Declareops.flatten_side_effects eff1)
+              (Declareops.flatten_side_effects eff2)) }
     with e when catchable_exception e ->
       tclZERO e env
 
@@ -471,12 +494,12 @@ module V82 = struct
 
   (* Returns the open goals of the proofview together with the evar_map to 
      interprete them. *)
-  let goals { comb = comb ; solution = solution } = 
-    { Evd.it = comb ; sigma = solution}
+  let goals { comb = comb ; solution = solution; side_effects=eff } =
+   { Evd.it = comb ; sigma = solution; eff=eff}
 
-  let top_goals { initial=initial ; solution=solution } = 
+  let top_goals { initial=initial ; solution=solution; side_effects=eff } =
     let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
-    { Evd.it = goals ; sigma=solution }
+    { Evd.it = goals ; sigma=solution; eff=eff }
 
   let top_evars { initial=initial } =
     let evars_of_initial (c,_) =