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, 32 insertions, 25 deletions

diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index dfc9c0a63..06e35284d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -16,6 +16,7 @@ open Logic
 
 
 let sig_it x = x.it
+let sig_eff x = x.eff
 let project x = x.sigma
 
 (* Getting env *)
@@ -25,7 +26,7 @@ let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls)
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
-  {it=sgl; sigma = sigma'}
+  { it = sgl; sigma = sigma'; eff = goal_sigma.eff }
 
 let norm_evar_tac gl = refiner (Change_evars) gl
 
@@ -34,18 +35,19 @@ let norm_evar_tac gl = refiner (Change_evars) gl
 (*********************)
 
 
-let unpackage glsig = (ref (glsig.sigma)),glsig.it
+let unpackage glsig = (ref (glsig.sigma)), glsig.it, (ref (glsig.eff))
 
-let repackage r v = {it=v;sigma = !r}
+let repackage e r v = {it = v; sigma = !r; eff = !e}
 
-let apply_sig_tac r tac g =
+let apply_sig_tac eff r tac g =
   check_for_interrupt (); (* Breakpoint *)
-  let glsigma = tac (repackage r g) in
+  let glsigma = tac (repackage eff r g) in
   r := glsigma.sigma;
+  eff := glsigma.eff;
   glsigma.it
 
 (* [goal_goal_list : goal sigma -> goal list sigma] *)
-let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
+let goal_goal_list gls = {it=[gls.it]; sigma=gls.sigma; eff=gls.eff}
 
 (* forces propagation of evar constraints *)
 let tclNORMEVAR = norm_evar_tac
@@ -69,35 +71,39 @@ let tclFAIL lvl s g = raise (FailError (lvl,lazy s))
 let tclFAIL_lazy lvl s g = raise (FailError (lvl,s))
 
 let start_tac gls =
-  let (sigr,g) = unpackage gls in
-  (sigr,[g])
+  let sigr, g, eff = unpackage gls in
+  (sigr, [g], eff)
 
-let finish_tac (sigr,gl) = repackage sigr gl
+let finish_tac (sigr,gl,eff) = repackage eff sigr gl
 
 (* Apply [tacfi.(i)] on the first n subgoals, [tacli.(i)] on the last
    m subgoals, and [tac] on the others *)
-let thens3parts_tac tacfi tac tacli (sigr,gs) =
+let thens3parts_tac tacfi tac tacli (sigr,gs,eff) =
   let nf = Array.length tacfi in
   let nl = Array.length tacli in
   let ng = List.length gs in
   if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll =
       (List.map_i (fun i ->
-        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
+        apply_sig_tac eff sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
-    (sigr,List.flatten gll)
+    (sigr,List.flatten gll, eff)
 
 (* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
 let thensf_tac taci tac = thens3parts_tac taci tac [||]
 
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
-let thensi_tac tac (sigr,gs) =
+let thensi_tac tac (sigr,gs,eff) =
   let gll =
-    List.map_i (fun i -> apply_sig_tac sigr (tac i)) 1 gs in
-  (sigr, List.flatten gll)
+    List.map_i (fun i -> apply_sig_tac eff sigr (tac i)) 1 gs in
+  (sigr, List.flatten gll, eff)
 
 let then_tac tac = thensf_tac [||] tac
 
+let non_existent_goal n =
+  errorlabstrm ("No such goal: "^(string_of_int n))
+    (str"Trying to apply a tactic to a non existent goal")
+
 (* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
    applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
    the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
@@ -192,9 +198,9 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
   let oldhyps:Context.named_context = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
-  let {it=gls;sigma=sigma} = rslt in
+  let {it=gls;sigma=sigma;eff=eff} = rslt in
   let hyps:Context.named_context list =
-    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
+    List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; eff=eff}) gls in
   let newhyps =
     List.map (fun hypl -> List.subtract hypl oldhyps) hyps in
   let emacs_str s =
@@ -244,8 +250,8 @@ let tclORELSE_THEN t1 t2then t2else gls =
   with
     | None -> t2else gls
     | Some sgl ->
-        let (sigr,gl) = unpackage sgl in
-        finish_tac (then_tac t2then  (sigr,gl))
+        let sigr, gl, eff = unpackage sgl in
+        finish_tac (then_tac t2then  (sigr,gl,eff))
 
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
 let tclTRY f = (tclORELSE0 f tclIDTAC)
@@ -350,23 +356,24 @@ let tclIDTAC_list gls = gls
 (* first_goal : goal list sigma -> goal sigma *)
 
 let first_goal gls =
-  let gl = gls.it and sig_0 = gls.sigma in
+  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in
   if List.is_empty gl then error "first_goal";
-  { it = List.hd gl; sigma = sig_0 }
+  { it = List.hd gl; sigma = sig_0 ; eff = eff_0 }
 
 (* goal_goal_list : goal sigma -> goal list sigma *)
 
 let goal_goal_list gls =
-  let gl = gls.it and sig_0 = gls.sigma in { it = [gl]; sigma = sig_0 }
+  let gl = gls.it and sig_0 = gls.sigma and eff_0 = gls.eff in 
+  { it = [gl]; sigma = sig_0; eff = eff_0 }
 
 (* tactic -> tactic_list : Apply a tactic to the first goal in the list *)
 
 let apply_tac_list tac glls =
-  let (sigr,lg) = unpackage glls in
+  let (sigr,lg,eff) = unpackage glls in
   match lg with
   | (g1::rest) ->
-      let gl = apply_sig_tac sigr tac g1 in
-      repackage sigr (gl@rest)
+      let gl = apply_sig_tac eff sigr tac g1 in
+      repackage eff sigr (gl@rest)
   | _ -> error "apply_tac_list"
 
 let then_tactic_list tacl1 tacl2 glls =