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, 69 insertions, 22 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 753b97a0c4..13368aab97 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -99,6 +99,7 @@ type safe_environment =
       objlabels : Label.Set.t;
       revstruct : structure_body;
       univ : Univ.constraints;
+      future_cst : Univ.constraints Future.computation list;
       engagement : engagement option;
       imports : library_info list;
       loads : (module_path * module_body) list;
@@ -107,6 +108,36 @@ type safe_environment =
 let exists_modlabel l senv = Label.Set.mem l senv.modlabels
 let exists_objlabel l senv = Label.Set.mem l senv.objlabels
 
+(* type to be maintained isomorphic to Entries.side_effects *)
+(* XXX ideally this function obtains a valid side effect that 
+ * can be pushed into another (safe) environment without re-typechecking *)
+type side_effect = NewConstant of constant * constant_body
+let sideff_of_con env c = 
+  Obj.magic (NewConstant (c, Environ.lookup_constant c env.env))
+
+let env_of_safe_env senv = senv.env
+let env_of_senv = env_of_safe_env
+
+type constraints_addition =
+  Now of Univ.constraints | Later of Univ.constraints Future.computation
+
+let add_constraints cst senv =
+  match cst with
+  | Later fc -> {senv with future_cst = fc :: senv.future_cst}
+  | Now cst ->
+  { senv with
+    env = Environ.add_constraints cst senv.env;
+    univ = Univ.union_constraints cst senv.univ }
+
+let is_curmod_library senv = 
+  match senv.modinfo.variant with LIBRARY _ -> true | _ -> false
+
+let rec join_safe_environment e =
+  join_structure_body e.revstruct;
+  List.fold_left 
+    (fun e fc -> add_constraints (Now (Future.join fc)) e)
+    {e with future_cst = []} e.future_cst
+
 let check_modlabel l senv =
   if exists_modlabel l senv then error_existing_label l
 let check_objlabel l senv =
@@ -141,25 +172,21 @@ let rec empty_environment =
     modlabels = Label.Set.empty;
     objlabels = Label.Set.empty;
     revstruct = [];
+    future_cst = [];
     univ = Univ.empty_constraint;
     engagement = None;
     imports = [];
     loads = [];
     local_retroknowledge = [] }
 
-let env_of_safe_env senv = senv.env
-let env_of_senv = env_of_safe_env
-
-let add_constraints cst senv =
-  { senv with
-    env = Environ.add_constraints cst senv.env;
-    univ = Univ.union_constraints cst senv.univ }
-
 let constraints_of_sfb = function
-  | SFBconst cb -> cb.const_constraints
-  | SFBmind mib -> mib.mind_constraints
-  | SFBmodtype mtb -> mtb.typ_constraints
-  | SFBmodule mb -> mb.mod_constraints
+  | SFBmind mib -> Now mib.mind_constraints
+  | SFBmodtype mtb -> Now mtb.typ_constraints
+  | SFBmodule mb -> Now mb.mod_constraints
+  | SFBconst cb -> 
+      match Future.peek_val cb.const_constraints with
+      | Some c -> Now c
+      | None -> Later cb.const_constraints
 
 (* A generic function for adding a new field in a same environment.
    It also performs the corresponding [add_constraints]. *)
@@ -246,14 +273,20 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 let push_named_def (id,de) senv =
-  let (c,typ,cst) = Term_typing.translate_local_def senv.env de in
-  let senv' = add_constraints cst senv in
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env id de in
+  (* XXX for now we force *)
+  let c = match c with
+    | Def c -> Lazyconstr.force c
+    | OpaqueDef c -> Lazyconstr.force_opaque (Future.join c)
+    | _ -> assert false in
+  let cst = Future.join cst in
+  let senv' = add_constraints (Now cst) senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
 
 let push_named_assum (id,t) senv =
   let (t,cst) = Term_typing.translate_local_assum senv.env t in
-  let senv' = add_constraints cst senv in
+  let senv' = add_constraints (Now cst) senv in
   let env'' = safe_push_named (id,None,t) senv'.env in
   (cst, {senv' with env=env''})
 
@@ -267,16 +300,17 @@ type global_declaration =
 let add_constant dir l decl senv =
   let kn = make_con senv.modinfo.modpath dir l in
   let cb = match decl with
-    | ConstantEntry ce -> Term_typing.translate_constant senv.env ce
+    | ConstantEntry ce -> Term_typing.translate_constant senv.env kn ce
     | GlobalRecipe r ->
-      let cb = Term_typing.translate_recipe senv.env r in
+      let cb = Term_typing.translate_recipe senv.env kn r in 
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
   let cb = match cb.const_body with
     | OpaqueDef lc when DirPath.is_empty dir ->
       (* In coqc, opaque constants outside sections will be stored
          indirectly in a specific table *)
-      { cb with const_body = OpaqueDef (Lazyconstr.turn_indirect lc) }
+      { cb with const_body =
+           OpaqueDef (Future.chain lc Lazyconstr.turn_indirect) }
     | _ -> cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -317,7 +351,7 @@ let add_modtype l mte inl senv =
 
 (* full_add_module adds module with universes and constraints *)
 let full_add_module mb senv =
-  let senv = add_constraints mb.mod_constraints senv in
+  let senv = add_constraints (Now mb.mod_constraints) senv in
   { senv with env = Modops.add_module mb senv.env }
 
 (* Insertion of modules *)
@@ -350,6 +384,7 @@ let start_module l senv =
 	 objlabels = Label.Set.empty;
 	 revstruct = [];
          univ = Univ.empty_constraint;
+         future_cst = [];
          engagement = None;
 	 imports = senv.imports;
 	 loads = [];
@@ -435,6 +470,7 @@ let end_module l restype senv =
 		  objlabels = oldsenv.objlabels;
 		  revstruct = (l,SFBmodule mb)::oldsenv.revstruct;
 		  univ = Univ.union_constraints senv'.univ oldsenv.univ;
+                  future_cst = senv'.future_cst @ oldsenv.future_cst;
 		  (* engagement is propagated to the upper level *)
 		  engagement = senv'.engagement;
 		  imports = senv'.imports;
@@ -457,14 +493,14 @@ let end_module l restype senv =
 	   senv.modinfo.modpath inl me in
        mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
-   let senv = add_constraints cst senv in
+   let senv = add_constraints (Now cst) senv in
    let mp_sup = senv.modinfo.modpath in
      (* Include Self support  *)
    let rec compute_sign sign mb resolver senv = 
      match sign with
      | SEBfunctor(mbid,mtb,str) ->
 	 let cst_sub = check_subtypes senv.env mb mtb in
-	 let senv = add_constraints cst_sub senv in
+	 let senv = add_constraints (Now cst_sub) senv in
 	 let mpsup_delta =
 	   inline_delta_resolver senv.env inl mp_sup mbid mtb mb.typ_delta
 	 in
@@ -533,6 +569,7 @@ let add_module_parameter mbid mte inl senv =
 		     objlabels = senv.objlabels;
 		     revstruct = [];
 		     univ = senv.univ;
+                     future_cst = senv.future_cst;
 		     engagement = senv.engagement;
 		     imports = senv.imports;
 		     loads = [];
@@ -557,6 +594,7 @@ let start_modtype l senv =
 	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
+        future_cst = [];
         engagement = None;
 	imports = senv.imports;
 	loads = [] ;
@@ -609,6 +647,7 @@ let end_modtype l senv =
 	  objlabels = oldsenv.objlabels;
 	  revstruct = (l,SFBmodtype mtb)::oldsenv.revstruct;
           univ = Univ.union_constraints senv.univ oldsenv.univ;
+          future_cst = senv.future_cst @ oldsenv.future_cst;
           engagement = senv.engagement;
 	  imports = senv.imports;
 	  loads = senv.loads@oldsenv.loads;
@@ -644,6 +683,8 @@ type compiled_library = {
 
 type native_library = Nativecode.global list
 
+let join_compiled_library l = join_module_body l.comp_mod
+
 (* We check that only initial state Require's were performed before
    [start_library] was called *)
 
@@ -674,12 +715,16 @@ let start_library dir senv =
 	objlabels = Label.Set.empty;
 	revstruct = [];
         univ = Univ.empty_constraint;
+        future_cst = [];
         engagement = None;
 	imports = senv.imports;
 	loads = [];
         local_retroknowledge = [] }
 
 let export senv dir =
+  let senv = 
+    try join_safe_environment senv
+    with e -> Errors.errorlabstrm "future" (Errors.print e) in
   let modinfo = senv.modinfo in
   begin
     match modinfo.variant with
@@ -763,7 +808,6 @@ let import lib digest senv =
   in
   mp, senv, lib.comp_natsymbs
 
-
 type judgment = unsafe_judgment
 
 let j_val j = j.uj_val
@@ -787,3 +831,6 @@ let register_inline kn senv =
   let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in
   let env = { env with Pre_env.env_globals = new_globals } in
   { senv with env = env_of_pre_env env }
+
+let add_constraints c = add_constraints (Now c)
+