src/Pure/thm.ML
changeset 28378 60cc0359363d
parent 28364 0012c6e5347e
child 28381 0b8237df37bd
     1.1 --- a/src/Pure/thm.ML	Sat Sep 27 15:20:36 2008 +0200
     1.2 +++ b/src/Pure/thm.ML	Sat Sep 27 15:20:37 2008 +0200
     1.3 @@ -126,10 +126,10 @@
     1.4    val adjust_maxidx_cterm: int -> cterm -> cterm
     1.5    val capply: cterm -> cterm -> cterm
     1.6    val cabs: cterm -> cterm -> cterm
     1.7 -  val dest_deriv: thm ->
     1.8 +  val rep_deriv: thm ->
     1.9     {oracle: bool,
    1.10      proof: Proofterm.proof,
    1.11 -    promises: (serial * (thm Future.T * theory * sort OrdList.T * term)) OrdList.T}
    1.12 +    promises: (serial * thm Future.T) OrdList.T}
    1.13    val oracle_of: thm -> bool
    1.14    val major_prem_of: thm -> term
    1.15    val no_prems: thm -> bool
    1.16 @@ -340,20 +340,18 @@
    1.17  (*** Derivations and Theorems ***)
    1.18  
    1.19  datatype thm = Thm of
    1.20 - deriv *                                  (*derivation*)
    1.21 - {thy_ref: theory_ref,                    (*dynamic reference to theory*)
    1.22 -  tags: Properties.T,                     (*additional annotations/comments*)
    1.23 -  maxidx: int,                            (*maximum index of any Var or TVar*)
    1.24 -  shyps: sort OrdList.T,                  (*sort hypotheses*)
    1.25 -  hyps: term OrdList.T,                   (*hypotheses*)
    1.26 -  tpairs: (term * term) list,             (*flex-flex pairs*)
    1.27 -  prop: term}                             (*conclusion*)
    1.28 -and deriv = Deriv of
    1.29 - {oracle: bool,                           (*oracle occurrence flag*)
    1.30 -  proof: Pt.proof,                        (*proof term*)
    1.31 -  promises: (serial * promise) OrdList.T} (*promised derivations*)
    1.32 -and promise = Promise of
    1.33 -  thm Future.T * theory * sort OrdList.T * term;
    1.34 + deriv *                                        (*derivation*)
    1.35 + {thy_ref: theory_ref,                          (*dynamic reference to theory*)
    1.36 +  tags: Properties.T,                           (*additional annotations/comments*)
    1.37 +  maxidx: int,                                  (*maximum index of any Var or TVar*)
    1.38 +  shyps: sort OrdList.T,                        (*sort hypotheses*)
    1.39 +  hyps: term OrdList.T,                         (*hypotheses*)
    1.40 +  tpairs: (term * term) list,                   (*flex-flex pairs*)
    1.41 +  prop: term}                                   (*conclusion*)
    1.42 +and deriv = Deriv of                     
    1.43 + {oracle: bool,                                 (*oracle occurrence flag*)
    1.44 +  proof: Pt.proof,                              (*proof term*)
    1.45 +  promises: (serial * thm Future.T) OrdList.T}; (*promised derivations*)
    1.46  
    1.47  type conv = cterm -> thm;
    1.48  
    1.49 @@ -400,10 +398,8 @@
    1.50  
    1.51  (* basic components *)
    1.52  
    1.53 -fun dest_deriv (Thm (Deriv {oracle, proof, promises}, _)) =
    1.54 -  {oracle = oracle, proof = proof, promises = map (fn (i, Promise args) => (i, args)) promises};
    1.55 -
    1.56 -fun oracle_of (Thm (Deriv {oracle, ...}, _)) = oracle;
    1.57 +fun rep_deriv (Thm (Deriv args, _)) = args;
    1.58 +val oracle_of = #oracle o rep_deriv;
    1.59  
    1.60  val theory_of_thm = Theory.deref o #thy_ref o rep_thm;
    1.61  val maxidx_of = #maxidx o rep_thm;
    1.62 @@ -508,7 +504,7 @@
    1.63  
    1.64  (* inference rules *)
    1.65  
    1.66 -fun promise_ord ((i, Promise _), (j, Promise _)) = int_ord (j, i);
    1.67 +fun promise_ord ((i, _), (j, _)) = int_ord (j, i);
    1.68  
    1.69  fun deriv_rule2 f
    1.70      (Deriv {oracle = ora1, promises = ps1, proof = prf1})
    1.71 @@ -1605,7 +1601,7 @@
    1.72  (
    1.73    type T = thm Future.T list ref;
    1.74    val empty : T = ref [];
    1.75 -  fun copy (ref futures) : T = ref futures;
    1.76 +  val copy = I;  (*shared ref within whole theory body*)
    1.77    fun extend _ : T = ref [];
    1.78    fun merge _ _ : T = ref [];
    1.79  );
    1.80 @@ -1626,16 +1622,31 @@
    1.81  
    1.82  (* promise *)
    1.83  
    1.84 +fun promise_result orig_thy orig_shyps orig_prop raw_thm =
    1.85 +  let
    1.86 +    val _ = Theory.check_thy orig_thy;
    1.87 +    val thm = strip_shyps (transfer orig_thy raw_thm);
    1.88 +    val _ = Theory.check_thy orig_thy;
    1.89 +    fun err msg = raise THM ("promise_result: " ^ msg, 0, [thm]);
    1.90 +
    1.91 +    val Thm (_, {shyps, hyps, tpairs, prop, ...}) = thm;
    1.92 +    val _ = prop aconv orig_prop orelse err "bad prop";
    1.93 +    val _ = null tpairs orelse err "bad tpairs";
    1.94 +    val _ = null hyps orelse err "bad hyps";
    1.95 +    val _ = Sorts.subset (shyps, orig_shyps) orelse err "bad shyps";
    1.96 +  in thm end;
    1.97 +
    1.98  fun promise make_result ct =
    1.99    let
   1.100      val {thy_ref = thy_ref, t = prop, T, maxidx, sorts} = rep_cterm ct;
   1.101      val thy = Context.reject_draft (Theory.deref thy_ref);
   1.102      val _ = T <> propT andalso raise CTERM ("promise: prop expected", [ct]);
   1.103 -    val future = Future.fork_irrelevant make_result;
   1.104 +
   1.105 +    val future = Future.fork_irrelevant (promise_result thy sorts prop o make_result);
   1.106      val _ = add_future thy future;
   1.107      val i = serial ();
   1.108    in
   1.109 -    Thm (make_deriv false [(i, Promise (future, thy, sorts, prop))] (Pt.promise_proof i prop),
   1.110 +    Thm (make_deriv false [(i, future)] (Pt.promise_proof i prop),
   1.111       {thy_ref = thy_ref,
   1.112        tags = [],
   1.113        maxidx = maxidx,
   1.114 @@ -1645,32 +1656,17 @@
   1.115        prop = prop})
   1.116    end;
   1.117  
   1.118 -fun check_promise (i, Promise (future, thy1, shyps1, prop1)) =
   1.119 -  let
   1.120 -    val thm = transfer thy1 (Future.join future);
   1.121 -    val _ = Theory.check_thy thy1;
   1.122 -    fun err msg = raise THM ("check_promise: " ^ msg, 0, [thm]);
   1.123 -
   1.124 -    val Thm (Deriv {oracle, proof, promises}, {shyps, hyps, tpairs, prop, ...}) = thm;
   1.125 -    val _ = null promises orelse err "illegal nested promises";
   1.126 -    val _ = shyps = shyps1 orelse err "bad shyps";
   1.127 -    val _ = null hyps orelse err "bad hyps";
   1.128 -    val _ = null tpairs orelse err "bad tpairs";
   1.129 -    val _ = prop aconv prop1 orelse err "bad prop";
   1.130 -  in (oracle, (i, proof)) end;
   1.131 -
   1.132  
   1.133  (* fulfill *)
   1.134  
   1.135  fun fulfill (thm as Thm (Deriv {oracle, proof, promises}, args)) =
   1.136    let
   1.137 -    val _ = Future.join_results (map (fn (_, Promise (future, _, _, _)) => future) promises)
   1.138 -      |> ParList.release_results;
   1.139 -    val results = map check_promise promises;
   1.140 -
   1.141 -    val ora = oracle orelse exists #1 results;
   1.142 -    val prf = Pt.fulfill (fold (Inttab.update o #2) results Inttab.empty) proof;
   1.143 -  in Thm (make_deriv ora [] prf, args) end;
   1.144 +    val _ = ParList.release_results (Future.join_results (map #2 promises));
   1.145 +    val results = map (apsnd Future.join) promises;
   1.146 +    val proofs = fold (fn (i, Thm (Deriv {proof = prf, ...}, _)) => Inttab.update (i, prf))
   1.147 +      results Inttab.empty;
   1.148 +    val ora = oracle orelse exists (oracle_of o #2) results;
   1.149 +  in Thm (make_deriv ora [] (Pt.fulfill proofs proof), args) end;
   1.150  
   1.151  val proof_of = fulfill #> (fn Thm (Deriv {proof, ...}, _) => proof);
   1.152