diff -r 15178f4aa203 -r 1df7022eac6f src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Wed Jan 04 00:52:45 2006 +0100 +++ b/src/Pure/Isar/toplevel.ML Wed Jan 04 00:52:45 2006 +0100 @@ -9,8 +9,8 @@ sig datatype node = Theory of theory * Proof.context option | - Proof of ProofHistory.T | - SkipProof of int History.T * theory + Proof of ProofHistory.T * theory | + SkipProof of (int History.T * theory) * theory type state val toplevel: state val is_toplevel: state -> bool @@ -71,6 +71,7 @@ val theory': (bool -> theory -> theory) -> transition -> transition val theory_context: (theory -> theory * Proof.context) -> transition -> transition val theory_to_proof: (theory -> Proof.state) -> transition -> transition + val theory_theory_to_proof: (theory -> Proof.state) -> transition -> transition val proof: (Proof.state -> Proof.state) -> transition -> transition val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition @@ -82,6 +83,7 @@ val proof_to_theory_context: (bool -> Proof.state -> theory * Proof.context) -> transition -> transition val skip_proof_to_theory: (int -> bool) -> transition -> transition + val forget_proof: transition -> transition val unknown_theory: transition -> transition val unknown_proof: transition -> transition val unknown_context: transition -> transition @@ -108,9 +110,10 @@ (* datatype state *) datatype node = - Theory of theory * Proof.context option | (*theory with optional body context*) - Proof of ProofHistory.T | (*history of proof states*) - SkipProof of int History.T * theory; (*history of proof depths*) + Theory of theory * Proof.context option | (*theory with optional body context*) + Proof of ProofHistory.T * theory | (*history of proof states, original theory*) + SkipProof of (int History.T * theory) * theory; + (*history of proof depths, resulting theory, original theory*) datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) option; @@ -123,8 +126,8 @@ | level (State (SOME (node, _))) = (case History.current node of Theory _ => 0 - | Proof prf => Proof.level (ProofHistory.current prf) - | SkipProof (h, _) => History.current h + 1); (*different notion of proof depth!*) + | Proof (prf, _) => Proof.level (ProofHistory.current prf) + | SkipProof ((h, _), _) => History.current h + 1); (*different notion of proof depth!*) fun str_of_state (State NONE) = "at top level" | str_of_state (State (SOME (node, _))) = @@ -149,8 +152,8 @@ fun node_case f g state = (case node_of state of Theory (thy, _) => f thy - | Proof prf => g (ProofHistory.current prf) - | SkipProof (_, thy) => f thy); + | Proof (prf, _) => g (ProofHistory.current prf) + | SkipProof ((_, thy), _) => f thy); val theory_of = node_case I Proof.theory_of; val sign_of = theory_of; @@ -189,9 +192,9 @@ | SOME thy => pretty_context thy); fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy - | pretty_node _ (Proof prf) = + | pretty_node _ (Proof (prf, _)) = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) - | pretty_node _ (SkipProof (h, _)) = + | pretty_node _ (SkipProof ((h, _), _)) = [Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]; fun pretty_state prf_only state = @@ -263,18 +266,18 @@ in fun transaction _ _ _ (State NONE) = raise UNDEF - | transaction int hist f (State (SOME (node, term))) = + | transaction save hist f (State (SOME (node, term))) = let - val cont_node = History.map (checkpoint_node int) node; - val back_node = History.map (copy_node int) cont_node; + val cont_node = History.map (checkpoint_node save) node; + val back_node = History.map (copy_node save) cont_node; fun state nd = State (SOME (nd, term)); fun normal_state nd = (state nd, NONE); fun error_state nd exn = (state nd, SOME exn); val (result, err) = cont_node - |> ((fn nd => f int nd) - |> (if hist then History.apply_copy (copy_node int) else History.map) + |> (f + |> (if hist then History.apply_copy (copy_node save) else History.map) |> debug_trans |> interruptible |> transform_error) @@ -291,22 +294,20 @@ (* primitive transitions *) -(*NB: recovery from stale theories is provided only for theory-level - operations via MapCurrent and AppCurrent. Other node or state - operations should not touch theories at all. - - Interrupts are enabled only for Keep, MapCurrent, and AppCurrent.*) +(*Note: Recovery from stale theories is provided only for theory-level + operations via Transaction. Other node or state operations should + not touch theories at all. Interrupts are enabled only for Keep and + Transaction.*) datatype trans = - Reset | (*empty toplevel*) + Reset | (*empty toplevel*) Init of (bool -> node) * ((node -> unit) * (node -> unit)) | - (*init node; provide exit/kill operation*) - Exit | (*conclude node*) - Kill | (*abort node*) - Keep of bool -> state -> unit | (*peek at state*) - History of node History.T -> node History.T | (*history operation (undo etc.)*) - MapCurrent of bool -> node -> node | (*change node, bypassing history*) - AppCurrent of bool -> node -> node; (*change node, recording history*) + (*init node; with exit/kill operation*) + Exit | (*conclude node*) + Kill | (*abort node*) + Keep of bool -> state -> unit | (*peek at state*) + History of node History.T -> node History.T | (*history operation (undo etc.)*) + Transaction of bool * bool * (bool -> node -> node); (*node transaction*) fun undo_limit int = if int then NONE else SOME 0; @@ -325,8 +326,8 @@ | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state) | apply_tr _ (History _) (State NONE) = raise UNDEF | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) - | apply_tr int (MapCurrent f) state = transaction int false f state - | apply_tr int (AppCurrent f) state = transaction int true f state; + | apply_tr int (Transaction (save, hist, f)) state = + transaction (int orelse save) hist (fn x => f int x) state; fun apply_union _ [] state = raise FAILURE (state, UNDEF) | apply_union int (tr :: trs) state = @@ -416,8 +417,8 @@ val kill = add_trans Kill; val keep' = add_trans o Keep; val history = add_trans o History; -val map_current = add_trans o MapCurrent; -val app_current = add_trans o AppCurrent; +fun map_current f = add_trans (Transaction (false, false, f)); +fun app_current save f = add_trans (Transaction (save, true, f)); fun keep f = add_trans (Keep (fn _ => f)); fun imperative f = keep (fn _ => f ()); @@ -430,27 +431,32 @@ (* typed transitions *) -fun theory f = app_current (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF)); -fun theory' f = app_current (fn int => +fun theory f = app_current false + (K (fn Theory (thy, _) => Theory (f thy, NONE) | _ => raise UNDEF)); + +fun theory' f = app_current false (fn int => (fn Theory (thy, _) => Theory (f int thy, NONE) | _ => raise UNDEF)); -fun theory_context f = - app_current (K (fn Theory (thy, _) => Theory (apsnd SOME (f thy)) | _ => raise UNDEF)); +fun theory_context f = app_current false + (K (fn Theory (thy, _) => Theory (apsnd SOME (f thy)) | _ => raise UNDEF)); -fun theory_to_proof f = app_current (fn int => +fun to_proof save f = app_current save (fn int => (fn Theory (thy, _) => let val st = f thy in - if Theory.eq_thy (thy, Proof.theory_of st) then () + if save orelse Theory.eq_thy (thy, Proof.theory_of st) then () else error "Theory changed at start of proof"; if ! skip_proofs then - SkipProof (History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st)) - else Proof (ProofHistory.init (undo_limit int) st) + SkipProof ((History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st)), thy) + else Proof (ProofHistory.init (undo_limit int) st, thy) end | _ => raise UNDEF)); +val theory_to_proof = to_proof false; +val theory_theory_to_proof = to_proof true; + fun proofs' f = map_current (fn int => - (fn Proof prf => Proof (ProofHistory.applys (f int) prf) - | SkipProof (h, thy) => SkipProof (History.apply I h, thy) + (fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy) + | SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy) | _ => raise UNDEF)); fun proof' f = proofs' (Seq.single oo f); @@ -458,14 +464,19 @@ val proof = proof' o K; fun actual_proof f = map_current (fn _ => - (fn Proof prf => Proof (f prf) | _ => raise UNDEF)); + (fn Proof (prf, orig_thy) => Proof (f prf, orig_thy) | _ => raise UNDEF)); fun skip_proof f = map_current (fn _ => - (fn SkipProof (h, thy) => SkipProof (f h, thy) | _ => raise UNDEF)); + (fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy) | _ => raise UNDEF)); fun end_proof f = map_current (fn int => - (fn Proof prf => Theory (f int (ProofHistory.current prf)) - | SkipProof (h, thy) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF + (fn Proof (prf, _) => Theory (f int (ProofHistory.current prf)) + | SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF + | _ => raise UNDEF)); + +val forget_proof = map_current (fn _ => + (fn Proof (_, orig_thy) => Theory (orig_thy, NONE) + | SkipProof (_, orig_thy) => Theory (orig_thy, NONE) | _ => raise UNDEF)); fun proof_to_theory' f = end_proof (rpair NONE oo f); @@ -473,7 +484,7 @@ fun proof_to_theory_context f = end_proof (apsnd SOME oo f); fun skip_proof_to_theory p = map_current (fn _ => - (fn SkipProof (h, thy) => + (fn SkipProof ((h, thy), _) => if p (History.current h) then Theory (thy, NONE) else raise UNDEF | _ => raise UNDEF));