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

3 files changed, 22 insertions, 10 deletions

diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 2ba972b5dc..eae6d09d69 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -389,7 +389,6 @@ let pr_priority = function
 (* Pretty printer for vernac commands *)
 (**************************************)
 let make_pr_vernac pr_constr pr_lconstr =
-
 let pr_constrarg c = spc () ++ pr_constr c in
 let pr_lconstrarg c = spc () ++ pr_lconstr c in
 let pr_intarg n = spc () ++ int n in
@@ -477,6 +476,13 @@ let rec pr_vernac = function
   | VernacProgram v -> str"Program" ++ spc() ++ pr_vernac v
   | VernacLocal (local, v) -> pr_locality local ++ spc() ++ pr_vernac v
 
+  (* Stm *)
+  | VernacStm JoinDocument -> str"Stm JoinDocument"
+  | VernacStm Finish -> str"Stm Finish"
+  | VernacStm (Observe id) ->
+      str"Stm Observe " ++ str(Stateid.string_of_state_id id)
+  | VernacStm (Command v) -> str"Stm Command " ++ pr_vernac v
+
   (* Proof management *)
   | VernacAbortAll -> str "Abort All"
   | VernacRestart -> str"Restart"
@@ -614,7 +620,7 @@ let rec pr_vernac = function
       let n = List.length (List.flatten (List.map fst (List.map snd l))) in
       hov 2
         (pr_assumption_token (n > 1) stre ++ spc() ++
-	 pr_ne_params_list pr_lconstr_expr l)
+        pr_ne_params_list pr_lconstr_expr l)
   | VernacInductive (f,i,l) ->
 
       let pr_constructor (coe,(id,c)) =
@@ -975,3 +981,8 @@ in pr_vernac
 let pr_vernac_body v = make_pr_vernac pr_constr_expr pr_lconstr_expr v
 
 let pr_vernac v = make_pr_vernac pr_constr_expr pr_lconstr_expr v ++ sep_end v
+
+let pr_vernac x =
+  try pr_vernac x
+  with e -> Errors.print e
+
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 9a084adc48..0f6a5e8937 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -420,11 +420,11 @@ let print_constant with_values sep sp =
 	str"*** [ " ++
 	print_basename sp ++ str " : " ++ cut () ++ pr_ltype typ ++
 	str" ]" ++
-	Printer.pr_univ_cstr cb.const_constraints
+	Printer.pr_univ_cstr (Future.force cb.const_constraints)
     | _ ->
 	print_basename sp ++ str sep ++ cut () ++
 	(if with_values then print_typed_body (val_0,typ) else pr_ltype typ)++
-        Printer.pr_univ_cstr cb.const_constraints)
+        Printer.pr_univ_cstr (Future.force cb.const_constraints))
 
 let gallina_print_constant_with_infos sp =
   print_constant true " = " sp ++
@@ -566,7 +566,8 @@ let print_full_pure_context () =
 	      | OpaqueDef lc ->
 		str "Theorem " ++ print_basename con ++ cut () ++
 		str " : " ++ pr_ltype typ ++ str "." ++ fnl () ++
-		str "Proof " ++ pr_lconstr (Lazyconstr.force_opaque lc)
+		str "Proof " ++ pr_lconstr
+                  (Lazyconstr.force_opaque (Future.force lc))
 	      | Def c ->
 		str "Definition " ++ print_basename con ++ cut () ++
 		str "  : " ++ pr_ltype typ ++ cut () ++ str " := " ++
diff --git a/printing/printer.ml b/printing/printer.ml
index 696f25695b..cc9356cda7 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -387,7 +387,7 @@ let default_pr_subgoal n sigma =
     | [] -> error "No such goal."
     | g::rest ->
 	if Int.equal p 1 then
-          let pg = default_pr_goal { sigma=sigma ; it=g } in
+          let pg = default_pr_goal { sigma=sigma ; it=g; eff=Declareops.no_seff } in
           v 0 (str "subgoal " ++ int n ++ pr_goal_tag g
 	       ++ str " is:" ++ cut () ++ pg)
 	else
@@ -438,7 +438,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
   in
   let print_multiple_goals g l =
     if pr_first then
-      default_pr_goal { it = g ; sigma = sigma } ++
+      default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } ++
       pr_rec 2 l
     else 
       pr_rec 1 (g::l)
@@ -463,13 +463,13 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds stack goals =
                  str "You can use Grab Existential Variables.")
       end
   | [g],[] when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
       v 0 (
 	str "1 subgoal" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
       )
   | [g],a::l when not !Flags.print_emacs ->
-      let pg = default_pr_goal { it = g ; sigma = sigma } in
+      let pg = default_pr_goal { it = g ; sigma = sigma; eff=Declareops.no_seff } in
       v 0 (
 	str "1 focused subgoal (" ++ print_unfocused a l ++ str")" ++ pr_goal_tag g ++ cut () ++ pg
 	++ emacs_print_dependent_evars sigma seeds
@@ -555,7 +555,7 @@ let pr_goal_by_id id =
 	 ++ pr_goal gs)
   in
   try
-    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma})
+    Proof.in_proof p (fun sigma -> pr {it=g;sigma=sigma;eff=Declareops.no_seff})
   with Not_found -> error "Invalid goal identifier."
 
 (* Elementary tactics *)