promise_result: enforce strictly sequential dependencies, via serial numbers;
authorwenzelm
Sun Sep 28 12:23:44 2008 +0200 (2008-09-28)
changeset 28389777bdc429ea3
parent 28388 0789bbedfc62
child 28390 0b9fb63b8e1d
promise_result: enforce strictly sequential dependencies, via serial numbers;
src/Pure/thm.ML
     1.1 --- a/src/Pure/thm.ML	Sun Sep 28 09:25:24 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Sun Sep 28 12:23:44 2008 +0200
     1.3 @@ -1622,18 +1622,19 @@
     1.4  
     1.5  (* promise *)
     1.6  
     1.7 -fun promise_result orig_thy orig_shyps orig_prop raw_thm =
     1.8 +fun promise_result i orig_thy orig_shyps orig_prop raw_thm =
     1.9    let
    1.10      val _ = Theory.check_thy orig_thy;
    1.11      val thm = strip_shyps (transfer orig_thy raw_thm);
    1.12      val _ = Theory.check_thy orig_thy;
    1.13      fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
    1.14  
    1.15 -    val Thm (_, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.16 +    val Thm (Deriv {promises, ...}, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.17      val _ = prop aconv orig_prop orelse err "bad prop";
    1.18      val _ = null tpairs orelse err "bad tpairs";
    1.19      val _ = null hyps orelse err "bad hyps";
    1.20      val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    1.21 +    val _ = forall (fn (j, _) => j < i) promises orelse err "bad dependencies";
    1.22    in thm end;
    1.23  
    1.24  fun promise make_result ct =
    1.25 @@ -1642,9 +1643,9 @@
    1.26      val thy = Context.reject_draft (Theory.deref thy_ref);
    1.27      val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
    1.28  
    1.29 -    val future = Future.fork_irrelevant (promise_result thy sorts prop o make_result);
    1.30 +    val i = serial ();
    1.31 +    val future = Future.fork_irrelevant (promise_result i thy sorts prop o make_result);
    1.32      val _ = add_future thy future;
    1.33 -    val i = serial ();
    1.34    in
    1.35      Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
    1.36       {thy_ref = thy_ref,