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, 34 insertions, 5 deletions

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 64496033a..e597ea9a9 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -19,7 +19,7 @@ open Util
 let body_of_constant cb = match cb.const_body with
   | Undef _ -> None
   | Def c -> Some (Lazyconstr.force c)
-  | OpaqueDef lc -> Some (Lazyconstr.force_opaque lc)
+  | OpaqueDef lc -> Some (Lazyconstr.force_opaque (Future.force lc))
 
 let constant_has_body cb = match cb.const_body with
   | Undef _ -> false
@@ -50,7 +50,8 @@ let subst_const_type sub arity =
 let subst_const_def sub = function
   | Undef inl -> Undef inl
   | Def c -> Def (subst_constr_subst sub c)
-  | OpaqueDef lc -> OpaqueDef (subst_lazy_constr sub lc)
+  | OpaqueDef lc ->
+      OpaqueDef (Future.chain ~pure:true lc (subst_lazy_constr sub))
 
 let subst_const_body sub cb = {
   const_hyps = (match cb.const_hyps with [] -> [] | _ -> assert false);
@@ -84,14 +85,24 @@ let hcons_const_type = function
 
 let hcons_const_def = function
   | Undef inl -> Undef inl
-  | Def cs -> Def (from_val (Term.hcons_constr (Lazyconstr.force cs)))
-  | OpaqueDef lc -> OpaqueDef (Lazyconstr.hcons_lazy_constr lc)
+  | Def l_constr ->
+    let constr = force l_constr in
+    Def (from_val (Term.hcons_constr constr))
+  | OpaqueDef lc ->
+    if Future.is_val lc then
+      let constr = force_opaque (Future.force lc) in
+      OpaqueDef (Future.from_val (opaque_from_val (Term.hcons_constr constr)))
+    else OpaqueDef lc
 
 let hcons_const_body cb =
   { cb with
     const_body = hcons_const_def cb.const_body;
     const_type = hcons_const_type cb.const_type;
-    const_constraints = Univ.hcons_constraints cb.const_constraints }
+    const_constraints =
+      if Future.is_val cb.const_constraints then
+        Future.from_val
+          (Univ.hcons_constraints (Future.force cb.const_constraints))
+      else cb.const_constraints }
 
 (** Inductive types *)
 
@@ -193,3 +204,21 @@ let hcons_mind mib =
     mind_packets = Array.smartmap hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
     mind_constraints = Univ.hcons_constraints mib.mind_constraints }
+
+let join_constant_body cb =
+  ignore(Future.join cb.const_constraints);
+  match cb.const_body with
+  | OpaqueDef d -> ignore(Future.join d)
+  | _ -> ()
+
+let string_of_side_effect = function
+  | NewConstant (c,_) -> Names.string_of_con c
+type side_effects = side_effect list
+let no_seff = ([] : side_effects)
+let iter_side_effects f l = List.iter f l
+let fold_side_effects f a l = List.fold_left f a l
+let uniquize_side_effects l = List.uniquize l
+let union_side_effects l1 l2 = l1 @ l2
+let flatten_side_effects l = List.flatten l
+let side_effects_of_list l = l
+let cons_side_effects x l = x :: l