src/Pure/proofterm.ML
changeset 32726 a900d3cd47cc
parent 32711 e24acd21e60e
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/proofterm.ML	Mon Sep 28 12:09:55 2009 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Mon Sep 28 20:52:05 2009 +0200
     1.3 @@ -40,7 +40,8 @@
     1.4    val proof_of: proof_body -> proof
     1.5    val join_proof: proof_body future -> proof
     1.6    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     1.7 -  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
     1.8 +  val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
     1.9 +    proof_body list -> 'a -> 'a
    1.10    val join_bodies: proof_body list -> unit
    1.11    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    1.12  
    1.13 @@ -109,7 +110,7 @@
    1.14    val axm_proof: string -> term -> proof
    1.15    val oracle_proof: string -> term -> oracle * proof
    1.16    val promise_proof: theory -> serial -> term -> proof
    1.17 -  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    1.18 +  val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
    1.19    val thm_proof: theory -> string -> term list -> term ->
    1.20      (serial * proof_body future) list -> proof_body -> pthm * proof
    1.21    val get_name: term list -> term -> proof -> string
    1.22 @@ -173,19 +174,16 @@
    1.23  
    1.24  fun fold_body_thms f =
    1.25    let
    1.26 -    fun app path (PBody {thms, ...}) =
    1.27 +    fun app (PBody {thms, ...}) =
    1.28       (Future.join_results (map (#3 o #2) thms);
    1.29        thms |> fold (fn (i, (name, prop, body)) => fn (x, seen) =>
    1.30 -        if Inttab.defined path i then
    1.31 -          error ("Cyclic reference to theorem " ^ quote name)
    1.32 -        else if Inttab.defined seen i then (x, seen)
    1.33 +        if Inttab.defined seen i then (x, seen)
    1.34          else
    1.35            let
    1.36              val body' = Future.join body;
    1.37 -            val path' = Inttab.update (i, ()) path;
    1.38 -            val (x', seen') = app path' body' (x, Inttab.update (i, ()) seen);
    1.39 -          in (f (name, prop, body') x', seen') end));
    1.40 -  in fn bodies => fn x => #1 (fold (app Inttab.empty) bodies (x, Inttab.empty)) end;
    1.41 +            val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    1.42 +          in (f (i, (name, prop, body')) x', seen') end));
    1.43 +  in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    1.44  
    1.45  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    1.46  
    1.47 @@ -1281,12 +1279,16 @@
    1.48          | _ => false));
    1.49    in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
    1.50  
    1.51 -fun fulfill_proof _ [] body0 = body0
    1.52 -  | fulfill_proof thy ps body0 =
    1.53 +fun fulfill_proof _ _ [] body0 = body0
    1.54 +  | fulfill_proof thy id ps body0 =
    1.55        let
    1.56          val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
    1.57 -        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
    1.58 -        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
    1.59 +        val bodies = map snd ps;
    1.60 +        val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
    1.61 +          if i = id then error ("Cyclic reference to theorem " ^ quote name)
    1.62 +          else ()) bodies ();
    1.63 +        val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
    1.64 +        val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
    1.65          val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
    1.66  
    1.67          fun fill (Promise (i, prop, Ts)) =
    1.68 @@ -1298,10 +1300,10 @@
    1.69          val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
    1.70        in PBody {oracles = oracles, thms = thms, proof = proof} end;
    1.71  
    1.72 -fun fulfill_proof_future _ [] body = Future.value body
    1.73 -  | fulfill_proof_future thy promises body =
    1.74 +fun fulfill_proof_future _ _ [] body = Future.value body
    1.75 +  | fulfill_proof_future thy id promises body =
    1.76        Future.fork_deps (map snd promises) (fn () =>
    1.77 -        fulfill_proof thy (map (apsnd Future.join) promises) body);
    1.78 +        fulfill_proof thy id (map (apsnd Future.join) promises) body);
    1.79  
    1.80  
    1.81  (***** theorems *****)
    1.82 @@ -1321,7 +1323,9 @@
    1.83        else MinProof;
    1.84      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    1.85  
    1.86 -    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
    1.87 +    fun new_prf () =
    1.88 +      let val id = serial ()
    1.89 +      in (id, name, prop, fulfill_proof_future thy id promises body0) end;
    1.90      val (i, name, prop, body') =
    1.91        (case strip_combt (fst (strip_combP prf)) of
    1.92          (PThm (i, ((old_name, prop', NONE), body')), args') =>