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, 143 insertions, 56 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 33a4b55e87..fd31d782a5 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -23,6 +23,10 @@ open Environ
 open Entries
 open Typeops
 
+let debug = false
+let prerr_endline =
+  if debug then prerr_endline else fun _ -> ()
+
 let constrain_type env j cst1 = function
   | None ->
       make_polymorphic_if_constant_for_ind env j, cst1
@@ -33,19 +37,6 @@ let constrain_type env j cst1 = function
       let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
       NonPolymorphicType t, cstrs
 
-let local_constrain_type env j cst1 = function
-  | None ->
-      j.uj_type, cst1
-  | Some t ->
-      let (tj,cst2) = infer_type env t in
-      let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-      assert (eq_constr t tj.utj_val);
-      t, union_constraints (union_constraints cst1 cst2) cst3
-
-let translate_local_def env de =
-  let (j,cst) = infer env de.const_entry_body in
-  let (typ,cst) = local_constrain_type env j cst de.const_entry_type in
-    (j.uj_val,typ,cst)
 
 let translate_local_assum env t =
   let (j,cst) = infer env t in
@@ -55,23 +46,89 @@ let translate_local_assum env t =
 
 (* Insertion of constants and parameters in environment. *)
 
-let infer_declaration env = function
+let handle_side_effects env body side_eff =
+  let handle_sideff t (NewConstant (c,cb)) =
+    let cname = 
+      let name = string_of_con c in
+      for i = 0 to String.length name - 1 do
+        if name.[i] = '.' || name.[i] = '#' then name.[i] <- '_' done;
+      Name (id_of_string name) in
+    let rec sub i x = match kind_of_term x with
+      | Const c' when eq_constant c c' -> mkRel i
+      | _ -> map_constr_with_binders ((+) 1) sub i x in
+    match cb.const_body with
+    | Undef _ -> assert false
+    | Def b ->
+        let b = Lazyconstr.force b in
+        let b_ty = Typeops.type_of_constant_type env cb.const_type in
+        let t = sub 1 (Vars.lift 1 t) in
+        mkLetIn (cname, b, b_ty, t)
+    | OpaqueDef b -> 
+        let b = Lazyconstr.force_opaque (Future.force b) in
+        let b_ty = Typeops.type_of_constant_type env cb.const_type in
+        let t = sub 1 (Vars.lift 1 t) in
+        mkApp (mkLambda (cname, b_ty, t), [|b|])
+  in
+  (* CAVEAT: we assure a proper order *)
+  Declareops.fold_side_effects handle_sideff body
+    (Declareops.uniquize_side_effects side_eff)
+
+(* what is used for debugging only *)
+let infer_declaration ?(what="UNKNOWN") env dcl =
+  match dcl with
   | DefinitionEntry c ->
-      let (j,cst) = infer env c.const_entry_body in
-      let j =
-        {uj_val = hcons_constr j.uj_val;
-         uj_type = hcons_constr j.uj_type} in
-      let (typ,cst) = constrain_type env j cst c.const_entry_type in
-      let def =
-	if c.const_entry_opaque
-	then OpaqueDef (Lazyconstr.opaque_from_val j.uj_val)
-	else Def (Lazyconstr.from_val j.uj_val)
-      in
-      def, typ, cst, c.const_entry_inline_code, c.const_entry_secctx
+      let ctx, entry_body = c.const_entry_secctx, c.const_entry_body in
+      if c.const_entry_opaque && c.const_entry_type <> None then
+        let _ = prerr_endline ("deferring typing of "^what) in
+        let body_cst = Future.chain ~id:("infer_declaration " ^ what)
+            entry_body (fun entry_body ->
+          let _ = prerr_endline ("forcing deferred typing of "^what) in
+          let body, side_eff = entry_body in
+          let _ = prerr_endline ("... got proof of "^what) in
+          let body = if side_eff = Declareops.no_seff then body else
+            let _ = prerr_endline ("    Handling the following side eff:") in
+            Declareops.iter_side_effects (fun e -> 
+              prerr_endline("     " ^ Declareops.string_of_side_effect e)) 
+              side_eff;
+            handle_side_effects env body side_eff in
+          let (j,cst) = infer env body in
+          let _ = prerr_endline ("... typed proof of "^what) in
+          let j =
+            {uj_val = hcons_constr j.uj_val;
+             uj_type = hcons_constr j.uj_type} in
+          let (_typ,cst) = constrain_type env j cst c.const_entry_type in
+          Lazyconstr.opaque_from_val j.uj_val, cst) in
+        let body, cst = Future.split2 body_cst in
+        let def = OpaqueDef body in
+        let typ = match c.const_entry_type with
+        | None -> assert false
+        | Some typ -> NonPolymorphicType typ in
+        (def, typ, cst, c.const_entry_inline_code, ctx)
+      else
+        let _ = prerr_endline ("typing now "^what) in
+        let body, side_eff = Future.force entry_body in
+        let body = if side_eff = Declareops.no_seff then body else
+          let _ = prerr_endline ("    Handling the following side eff:") in
+          Declareops.iter_side_effects (fun e -> 
+            prerr_endline("     " ^ Declareops.string_of_side_effect e))
+            side_eff;
+          handle_side_effects env body side_eff in
+        let (j,cst) =
+          try infer env body 
+          with Not_found as e -> 
+            prerr_endline ("infer not found " ^ what);
+            raise e in
+        let j =
+          {uj_val = hcons_constr j.uj_val;
+           uj_type = hcons_constr j.uj_type} in
+        let (typ,cst) = constrain_type env j cst c.const_entry_type in
+        let _ = prerr_endline ("...typed "^what) in
+        let def = Def (Lazyconstr.from_val j.uj_val) in
+        (def, typ, Future.from_val cst, c.const_entry_inline_code, ctx)
   | ParameterEntry (ctx,t,nl) ->
       let (j,cst) = infer env t in
       let t = hcons_constr (Typeops.assumption_of_judgment env j) in
-      Undef nl, NonPolymorphicType t, cst, false, ctx
+      Undef nl, NonPolymorphicType t, Future.from_val cst, false, ctx
 
 let global_vars_set_constant_type env = function
   | NonPolymorphicType t -> global_vars_set env t
@@ -81,48 +138,78 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let check_declared_variables declared inferred =
-  let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
-  let undeclared_set = Id.Set.diff (mk_set inferred) (mk_set declared) in
-  if not (Id.Set.is_empty undeclared_set) then
-    error ("The following section variables are used but not declared:\n"^
-              (String.concat ", "
-                 (List.map Id.to_string (Id.Set.elements undeclared_set))))
-
-let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
-  let hyps =
-    let inferred =
-      let ids_typ = global_vars_set_constant_type env typ in
-      let ids_def = match def with
-        | Undef _ -> Id.Set.empty
-        | Def cs -> global_vars_set env (Lazyconstr.force cs)
-        | OpaqueDef lc -> global_vars_set env (Lazyconstr.force_opaque lc)
-      in
-      keep_hyps env (Id.Set.union ids_typ ids_def)
-    in
+let build_constant_declaration kn env (def,typ,cst,inline_code,ctx) =
+  let check declared inferred =
+    let mk_set l = List.fold_right Id.Set.add (List.map pi1 l) Id.Set.empty in
+    let inferred_set, declared_set = mk_set inferred, mk_set declared in
+    if not (Id.Set.subset inferred_set declared_set) then
+      error ("The following section variable are used but not declared:\n"^
+        (String.concat ", " (List.map Id.to_string
+          (Id.Set.elements (Idset.diff inferred_set declared_set))))) in
+  (* We try to postpone the computation of used section variables *)
+  let hyps, def = 
     match ctx with
-      | None -> inferred
-      | Some declared ->
-        check_declared_variables declared inferred;
-        declared
-  in
-  let tps = Cemitcodes.from_val (compile_constant_body env def) in
+    | None when named_context env <> [] -> 
+        (* No declared section vars, and non-empty section context:
+           we must look at the body NOW, if any *)
+        let ids_typ = global_vars_set_constant_type env typ in
+        let ids_def = match def with
+        | Undef _ -> Idset.empty
+        | Def cs -> global_vars_set env (Lazyconstr.force cs)
+        | OpaqueDef lc -> 
+            (* we force so that cst are added to the env immediately after *)
+            ignore(Future.join cst);
+            global_vars_set env (Lazyconstr.force_opaque (Future.force lc)) in
+        keep_hyps env (Idset.union ids_typ ids_def), def
+    | None -> [], def (* Empty section context: no need to check *)
+    | Some declared ->
+        (* We use the declared set and chain a check of correctness *)
+        declared,
+        match def with
+        | Undef _ as x -> x (* nothing to check *)
+        | Def cs as x ->
+            let ids_typ = global_vars_set_constant_type env typ in
+            let ids_def = global_vars_set env (Lazyconstr.force cs) in
+            let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+            check declared inferred;
+            x
+        | OpaqueDef lc -> (* In this case we can postpone the check *)
+            OpaqueDef (Future.chain ~id:(string_of_con kn) lc (fun lc ->
+              let ids_typ = global_vars_set_constant_type env typ in
+              let ids_def =
+                global_vars_set env (Lazyconstr.force_opaque lc) in
+              let inferred = keep_hyps env (Idset.union ids_typ ids_def) in
+              check declared inferred; lc)) in
   { const_hyps = hyps;
     const_body = def;
     const_type = typ;
-    const_body_code = tps;
+    const_body_code = Cemitcodes.from_val (compile_constant_body env def);
     const_constraints = cst;
     const_native_name = ref NotLinked;
     const_inline_code = inline_code }
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env ce =
-  build_constant_declaration env (infer_declaration env ce)
+let translate_constant env kn ce =
+  build_constant_declaration kn env 
+    (infer_declaration ~what:(string_of_con kn) env ce)
+
+let translate_recipe env kn r =
+  let def,typ,cst,inline_code,hyps = Cooking.cook_constant env r in
+  build_constant_declaration kn env (def,typ,cst,inline_code,hyps)
 
-let translate_recipe env r =
-  build_constant_declaration env (Cooking.cook_constant env r)
+let translate_local_def env id centry =
+  let def,typ,cst,inline_code,ctx =
+    infer_declaration ~what:(string_of_id id) env (DefinitionEntry centry) in
+  let typ = type_of_constant_type env typ in
+  def, typ, cst
 
 (* Insertion of inductive types. *)
 
 let translate_mind env kn mie = Indtypes.check_inductive env kn mie
+
+let handle_side_effects env ce = { ce with
+  const_entry_body = Future.chain ~id:"handle_side_effects" 
+    ce.const_entry_body (fun (body, side_eff) ->
+    handle_side_effects env body side_eff, Declareops.no_seff);
+}