back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
authorwenzelm
Thu Oct 01 14:27:50 2009 +0200 (2009-10-01 ago)
changeset 32810f3466a5645fa
parent 32809 e72347dd3e64
child 32811 a692298ecbe0
back to simple fold_body_thms and fulfill_proof/thm_proof (reverting a900d3cd47cc) -- the cycle check is implicit in the future computation of join_proofs;
src/Pure/Thy/thm_deps.ML
src/Pure/proofterm.ML
src/Pure/thm.ML
     1.1 --- a/src/Pure/Thy/thm_deps.ML	Thu Oct 01 14:11:28 2009 +0200
     1.2 +++ b/src/Pure/Thy/thm_deps.ML	Thu Oct 01 14:27:50 2009 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4                 path = "",
     1.5                 parents = parents};
     1.6            in cons entry end;
     1.7 -    val deps = Proofterm.fold_body_thms (add_dep o #2) (map Thm.proof_body_of thms) [];
     1.8 +    val deps = Proofterm.fold_body_thms add_dep (map Thm.proof_body_of thms) [];
     1.9    in Present.display_graph (sort_wrt #ID deps) end;
    1.10  
    1.11  
    1.12 @@ -55,9 +55,10 @@
    1.13        fold (Facts.fold_static add_fact o PureThy.facts_of) thys []
    1.14        |> sort_distinct (string_ord o pairself #1);
    1.15  
    1.16 -    val tab = Proofterm.fold_body_thms
    1.17 -      (fn (_, (name, prop, _)) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    1.18 -      (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
    1.19 +    val tab =
    1.20 +      Proofterm.fold_body_thms
    1.21 +        (fn (name, prop, _) => name <> "" ? Symtab.insert_list (op =) (name, prop))
    1.22 +        (map (Proofterm.strip_thm o Thm.proof_body_of o snd) thms) Symtab.empty;
    1.23      fun is_unused (name, th) =
    1.24        not (member (op aconv) (Symtab.lookup_list tab name) (Thm.prop_of th));
    1.25  
     2.1 --- a/src/Pure/proofterm.ML	Thu Oct 01 14:11:28 2009 +0200
     2.2 +++ b/src/Pure/proofterm.ML	Thu Oct 01 14:27:50 2009 +0200
     2.3 @@ -40,8 +40,7 @@
     2.4    val proof_of: proof_body -> proof
     2.5    val join_proof: proof_body future -> proof
     2.6    val fold_proof_atoms: bool -> (proof -> 'a -> 'a) -> proof list -> 'a -> 'a
     2.7 -  val fold_body_thms: (serial * (string * term * proof_body) -> 'a -> 'a) ->
     2.8 -    proof_body list -> 'a -> 'a
     2.9 +  val fold_body_thms: (string * term * proof_body -> 'a -> 'a) -> proof_body list -> 'a -> 'a
    2.10    val join_bodies: proof_body list -> unit
    2.11    val status_of: proof_body list -> {failed: bool, oracle: bool, unfinished: bool}
    2.12  
    2.13 @@ -110,7 +109,7 @@
    2.14    val axm_proof: string -> term -> proof
    2.15    val oracle_proof: string -> term -> oracle * proof
    2.16    val promise_proof: theory -> serial -> term -> proof
    2.17 -  val fulfill_proof: theory -> serial -> (serial * proof_body) list -> proof_body -> proof_body
    2.18 +  val fulfill_proof: theory -> (serial * proof_body) list -> proof_body -> proof_body
    2.19    val thm_proof: theory -> string -> term list -> term ->
    2.20      (serial * proof_body future) list -> proof_body -> pthm * proof
    2.21    val get_name: term list -> term -> proof -> string
    2.22 @@ -182,7 +181,7 @@
    2.23            let
    2.24              val body' = Future.join body;
    2.25              val (x', seen') = app body' (x, Inttab.update (i, ()) seen);
    2.26 -          in (f (i, (name, prop, body')) x', seen') end));
    2.27 +          in (f (name, prop, body') x', seen') end));
    2.28    in fn bodies => fn x => #1 (fold app bodies (x, Inttab.empty)) end;
    2.29  
    2.30  fun join_bodies bodies = fold_body_thms (fn _ => fn () => ()) bodies ();
    2.31 @@ -1279,16 +1278,12 @@
    2.32          | _ => false));
    2.33    in Promise (i, prop, map TVar (Term.add_tvars prop [])) end;
    2.34  
    2.35 -fun fulfill_proof _ _ [] body0 = body0
    2.36 -  | fulfill_proof thy id ps body0 =
    2.37 +fun fulfill_proof _ [] body0 = body0
    2.38 +  | fulfill_proof thy ps body0 =
    2.39        let
    2.40          val PBody {oracles = oracles0, thms = thms0, proof = proof0} = body0;
    2.41 -        val bodies = map snd ps;
    2.42 -        val _ = fold_body_thms (fn (i, (name, _, _)) => fn () =>
    2.43 -          if i = id then error ("Cyclic reference to theorem " ^ quote name)
    2.44 -          else ()) bodies ();
    2.45 -        val oracles = fold (fn PBody {oracles, ...} => merge_oracles oracles) bodies oracles0;
    2.46 -        val thms = fold (fn PBody {thms, ...} => merge_thms thms) bodies thms0;
    2.47 +        val oracles = fold (fn (_, PBody {oracles, ...}) => merge_oracles oracles) ps oracles0;
    2.48 +        val thms = fold (fn (_, PBody {thms, ...}) => merge_thms thms) ps thms0;
    2.49          val proofs = fold (fn (i, PBody {proof, ...}) => Inttab.update (i, proof)) ps Inttab.empty;
    2.50  
    2.51          fun fill (Promise (i, prop, Ts)) =
    2.52 @@ -1300,18 +1295,18 @@
    2.53          val proof = rewrite_prf fst (rules, K fill :: procs) proof0;
    2.54        in PBody {oracles = oracles, thms = thms, proof = proof} end;
    2.55  
    2.56 -fun fulfill_proof_future _ _ [] body = Future.value body
    2.57 -  | fulfill_proof_future thy id promises body =
    2.58 +fun fulfill_proof_future _ [] body = Future.value body
    2.59 +  | fulfill_proof_future thy promises body =
    2.60        Future.fork_deps (map snd promises) (fn () =>
    2.61 -        fulfill_proof thy id (map (apsnd Future.join) promises) body);
    2.62 +        fulfill_proof thy (map (apsnd Future.join) promises) body);
    2.63  
    2.64  
    2.65  (***** theorems *****)
    2.66  
    2.67 -fun thm_proof thy name hyps prop promises body =
    2.68 +fun thm_proof thy name hyps concl promises body =
    2.69    let
    2.70      val PBody {oracles = oracles0, thms = thms0, proof = prf} = body;
    2.71 -    val prop = Logic.list_implies (hyps, prop);
    2.72 +    val prop = Logic.list_implies (hyps, concl);
    2.73      val nvs = needed_vars prop;
    2.74      val args = map (fn (v as Var (ixn, _)) =>
    2.75          if member (op =) nvs ixn then SOME v else NONE) (vars_of prop) @
    2.76 @@ -1323,9 +1318,7 @@
    2.77        else MinProof;
    2.78      val body0 = PBody {oracles = oracles0, thms = thms0, proof = proof0};
    2.79  
    2.80 -    fun new_prf () =
    2.81 -      let val id = serial ()
    2.82 -      in (id, name, prop, fulfill_proof_future thy id promises body0) end;
    2.83 +    fun new_prf () = (serial (), name, prop, fulfill_proof_future thy promises body0);
    2.84      val (i, name, prop, body') =
    2.85        (case strip_combt (fst (strip_combP prf)) of
    2.86          (PThm (i, ((old_name, prop', NONE), body')), args') =>
     3.1 --- a/src/Pure/thm.ML	Thu Oct 01 14:11:28 2009 +0200
     3.2 +++ b/src/Pure/thm.ML	Thu Oct 01 14:27:50 2009 +0200
     3.3 @@ -540,7 +540,7 @@
     3.4  fun raw_body (Thm (Deriv {body, ...}, _)) = body;
     3.5  
     3.6  fun fulfill_body (Thm (Deriv {promises, body}, {thy_ref, ...})) =
     3.7 -  Pt.fulfill_proof (Theory.deref thy_ref) ~1
     3.8 +  Pt.fulfill_proof (Theory.deref thy_ref)
     3.9      (map #1 promises ~~ fulfill_bodies (map #2 promises)) body
    3.10  and fulfill_bodies futures = map fulfill_body (Exn.release_all (Future.join_results futures));
    3.11