equal
deleted
inserted
replaced
148 val freezeT: thm -> thm |
148 val freezeT: thm -> thm |
149 val join_futures: theory -> unit |
149 val join_futures: theory -> unit |
150 val future: (unit -> thm) -> cterm -> thm |
150 val future: (unit -> thm) -> cterm -> thm |
151 val proof_body_of: thm -> proof_body |
151 val proof_body_of: thm -> proof_body |
152 val proof_of: thm -> proof |
152 val proof_of: thm -> proof |
|
153 val force_proof: thm -> unit |
153 val extern_oracles: theory -> xstring list |
154 val extern_oracles: theory -> xstring list |
154 val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory |
155 val add_oracle: bstring * ('a -> cterm) -> theory -> (string * ('a -> thm)) * theory |
155 end; |
156 end; |
156 |
157 |
157 structure Thm:> THM = |
158 structure Thm:> THM = |
1592 |
1593 |
1593 structure Futures = TheoryDataFun |
1594 structure Futures = TheoryDataFun |
1594 ( |
1595 ( |
1595 type T = thm Future.T list ref; |
1596 type T = thm Future.T list ref; |
1596 val empty : T = ref []; |
1597 val empty : T = ref []; |
1597 val copy = I; (*shared ref within whole theory body*) |
1598 val copy = I; (*shared ref within all versions of whole theory body*) |
1598 fun extend _ : T = ref []; |
1599 fun extend _ : T = ref []; |
1599 fun merge _ _ : T = ref []; |
1600 fun merge _ _ : T = ref []; |
1600 ); |
1601 ); |
1601 |
1602 |
1602 val _ = Context.>> (Context.map_theory Futures.init); |
1603 val _ = Context.>> (Context.map_theory Futures.init); |
1611 CRITICAL (fn () => |
1612 CRITICAL (fn () => |
1612 let |
1613 let |
1613 val (finished, unfinished) = List.partition Future.is_finished (! futures); |
1614 val (finished, unfinished) = List.partition Future.is_finished (! futures); |
1614 val _ = futures := unfinished; |
1615 val _ = futures := unfinished; |
1615 in finished end) |
1616 in finished end) |
1616 |> Future.join_results |> Exn.release_all |> null); |
1617 |> Future.join_results |> null); |
1617 in while not (joined ()) do () end; |
1618 in while not (joined ()) do () end; |
1618 |
1619 |
1619 |
1620 |
1620 (* future rule *) |
1621 (* future rule *) |
1621 |
1622 |
1665 val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises)); |
1666 val _ = Exn.release_all (map (Future.join_result o #2) (rev all_promises)); |
1666 val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises; |
1667 val ps = map (apsnd (Lazy.value o raw_proof_of o Future.join)) promises; |
1667 in Pt.fulfill_proof (Theory.deref thy_ref) ps body end; |
1668 in Pt.fulfill_proof (Theory.deref thy_ref) ps body end; |
1668 |
1669 |
1669 val proof_of = Proofterm.proof_of o proof_body_of; |
1670 val proof_of = Proofterm.proof_of o proof_body_of; |
|
1671 val force_proof = ignore o proof_body_of; |
1670 |
1672 |
1671 |
1673 |
1672 (* closed derivations with official name *) |
1674 (* closed derivations with official name *) |
1673 |
1675 |
1674 fun get_name thm = |
1676 fun get_name thm = |