# HG changeset patch # User wenzelm # Date 1216050703 -7200 # Node ID 7afff36043e662120062d38ad484b6fc17f1fc14 # Parent e540ad3fb50a46777a674b511eb914aacc06807d eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning; diff -r e540ad3fb50a -r 7afff36043e6 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Jul 14 17:51:42 2008 +0200 +++ b/src/Pure/Isar/toplevel.ML Mon Jul 14 17:51:43 2008 +0200 @@ -20,7 +20,7 @@ val is_theory: state -> bool val is_proof: state -> bool val level: state -> int - val node_history_of: state -> node History.T + val previous_node_of: state -> node option val node_of: state -> node val node_case: (generic_theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a val context_of: state -> Proof.context @@ -38,13 +38,11 @@ val profiling: int ref val skip_proofs: bool ref exception TERMINATE - exception RESTART exception CONTEXT of Proof.context * exn exception TOPLEVEL_ERROR val exn_message: exn -> string val program: (unit -> 'a) -> 'a type transition - val undo_limit: bool -> int option val empty: transition val init_of: transition -> string option val name_of: transition -> string @@ -54,13 +52,9 @@ val interactive: bool -> transition -> transition val print: transition -> transition val no_timing: transition -> transition - val init_theory: string -> (bool -> theory) -> (theory -> unit) -> (theory -> unit) -> - transition -> transition - val init_empty: (state -> bool) -> (unit -> unit) -> transition -> transition + val init_theory: string -> (bool -> theory) -> (theory -> unit) -> transition -> transition val exit: transition -> transition - val undo_exit: transition -> transition - val kill: transition -> transition - val history: (node History.T -> node History.T) -> transition -> transition + val commit_exit: transition val keep: (state -> unit) -> transition -> transition val keep': (bool -> state -> unit) -> transition -> transition val imperative: (unit -> unit) -> transition -> transition @@ -100,7 +94,6 @@ structure Toplevel: TOPLEVEL = struct - (** toplevel state **) exception UNDEF; @@ -126,9 +119,10 @@ (* datatype node *) datatype node = - Theory of generic_theory * Proof.context option | (*theory with presentation context*) - Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory) | - (*proof node, finish, original theory*) + Theory of generic_theory * Proof.context option + (*theory with presentation context*) | + Proof of ProofNode.T * ((Proof.context -> generic_theory) * generic_theory) + (*proof node, finish, original theory*) | SkipProof of int * (generic_theory * generic_theory); (*proof depth, resulting theory, original theory*) @@ -152,39 +146,33 @@ (* datatype state *) -type state_info = node History.T * ((theory -> unit) * (theory -> unit)); +datatype state = State of + (node * (theory -> unit)) option * (*current node with exit operation*) + node option; (*previous node*) -datatype state = - Toplevel of state_info option | (*outer toplevel, leftover end state*) - State of state_info; +val toplevel = State (NONE, NONE); -val toplevel = Toplevel NONE; - -fun is_toplevel (Toplevel _) = true +fun is_toplevel (State (NONE, _)) = true | is_toplevel _ = false; -fun level (Toplevel _) = 0 - | level (State (node, _)) = - (case History.current node of - Theory _ => 0 - | Proof (prf, _) => Proof.level (ProofNode.current prf) - | SkipProof (d, _) => d + 1); (*different notion of proof depth!*) +fun level (State (NONE, _)) = 0 + | level (State (SOME (Theory _, _), _)) = 0 + | level (State (SOME (Proof (prf, _), _), _)) = Proof.level (ProofNode.current prf) + | level (State (SOME (SkipProof (d, _), _), _)) = d + 1; (*different notion of proof depth!*) -fun str_of_state (Toplevel _) = "at top level" - | str_of_state (State (node, _)) = - (case History.current node of - Theory (Context.Theory _, _) => "in theory mode" - | Theory (Context.Proof _, _) => "in local theory mode" - | Proof _ => "in proof mode" - | SkipProof _ => "in skipped proof mode"); +fun str_of_state (State (NONE, _)) = "at top level" + | str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode" + | str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode" + | str_of_state (State (SOME (Proof _, _), _)) = "in proof mode" + | str_of_state (State (SOME (SkipProof _, _), _)) = "in skipped proof mode"; -(* top node *) +(* current node *) -fun node_history_of (Toplevel _) = raise UNDEF - | node_history_of (State (node, _)) = node; +fun previous_node_of (State (_, prev_node)) = prev_node; -val node_of = History.current o node_history_of; +fun node_of (State (NONE, _)) = raise UNDEF + | node_of (State (SOME (node, _), _)) = node; fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); @@ -237,7 +225,6 @@ val skip_proofs = ref false; exception TERMINATE; -exception RESTART; exception EXCURSION_FAIL of exn * string; exception FAILURE of state * exn; exception TOPLEVEL_ERROR; @@ -271,7 +258,6 @@ | exn_msg ctxt (EXCURSION_FAIL (exn, loc)) = exn_msg ctxt exn ^ Markup.markup Markup.location ("\n" ^ loc) | exn_msg _ TERMINATE = "Exit." - | exn_msg _ RESTART = "Restart." | exn_msg _ Interrupt = "Interrupt." | exn_msg _ TimeLimit.TimeOut = "Timeout." | exn_msg _ TOPLEVEL_ERROR = "Error." @@ -339,25 +325,22 @@ fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") | stale_error some = some; -fun map_theory f = History.map_current - (fn Theory (gthy, ctxt) => Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt) - | node => node); +fun map_theory f (Theory (gthy, ctxt)) = + Theory (Context.mapping f (LocalTheory.raw_theory f) gthy, ctxt) + | map_theory _ node = node; in -fun transaction hist pos f (node, term) = +fun transaction pos f (node, exit) = let - val _ = is_draft_theory (History.current node) andalso - error "Illegal draft theory in toplevel state"; - val cont_node = node |> History.map_current reset_presentation; - val back_node = cont_node |> map_theory Theory.copy |> map_theory Theory.checkpoint; - fun state_error e nd = (State (nd, term), e); + val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state"; + val cont_node = reset_presentation node; + val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; + fun state_error e nd = (State (SOME (nd, exit), SOME node), e); val (result, err) = cont_node - |> (f - |> (if hist then History.apply' (History.current back_node) else History.map_current) - |> controlled_execution) + |> controlled_execution f |> map_theory Theory.checkpoint |> state_error NONE handle exn => state_error (SOME exn) cont_node; @@ -382,43 +365,24 @@ Transaction.*) datatype trans = - Init of string * (bool -> theory) * ((theory -> unit) * (theory -> unit)) | - (*name; init node; with exit/kill operation*) - InitEmpty of (state -> bool) * (unit -> unit) | (*init empty toplevel*) - Exit | (*conclude node -- deferred until init*) - UndoExit | (*continue after conclusion*) - Kill | (*abort node*) - History of node History.T -> node History.T | (*history operation (undo etc.)*) - Keep of bool -> state -> unit | (*peek at state*) - Transaction of bool * (bool -> node -> node); (*node transaction*) - -fun undo_limit int = if int then NONE else SOME 0; - -fun safe_exit (Toplevel (SOME (node, (exit, _)))) = - (case try the_global_theory (History.current node) of - SOME thy => controlled_execution exit thy - | NONE => ()) - | safe_exit _ = (); + Init of string * (bool -> theory) * (theory -> unit) | (*theory name, init, exit*) + Exit | (*formal exit of theory -- without committing*) + CommitExit | (*exit and commit final theory*) + Keep of bool -> state -> unit | (*peek at state*) + Transaction of bool -> node -> node; (*node transaction*) local -fun keep_state int f = controlled_execution (fn x => tap (f int) x); - -fun apply_tr int _ (Init (_, f, term)) (state as Toplevel _) = - let val node = Theory (Context.Theory (Theory.checkpoint (f int)), NONE) - in safe_exit state; State (History.init (undo_limit int) node, term) end - | apply_tr int _ (InitEmpty (check, f)) (state as Toplevel _) = - if check state then (safe_exit state; keep_state int (fn _ => fn _ => f ()) toplevel) - else raise UNDEF - | apply_tr _ _ Exit (State (node, term)) = - (the_global_theory (History.current node); Toplevel (SOME (node, term))) - | apply_tr _ _ UndoExit (Toplevel (SOME state_info)) = State state_info - | apply_tr _ _ Kill (State (node, (_, kill))) = - (kill (the_global_theory (History.current node)); toplevel) - | apply_tr _ _ (History f) (State (node, term)) = State (f node, term) - | apply_tr int _ (Keep f) state = keep_state int f state - | apply_tr int pos (Transaction (hist, f)) (State state) = - transaction hist pos (fn x => f int x) state +fun apply_tr int _ (Init (_, f, exit)) (State (NONE, _)) = + State (SOME (Theory (Context.Theory (Theory.checkpoint (f int)), NONE), exit), NONE) + | apply_tr _ _ Exit (State (SOME (node as Theory (Context.Theory _, _), _), _)) = + State (NONE, SOME node) + | apply_tr _ _ CommitExit (State (SOME (Theory (Context.Theory thy, _), exit), _)) = + (controlled_execution exit thy; toplevel) + | apply_tr int _ (Keep f) state = + controlled_execution (fn x => tap (f int) x) state + | apply_tr int pos (Transaction f) (State (SOME state, _)) = + transaction pos (fn x => f int x) state | apply_tr _ _ _ _ = raise UNDEF; fun apply_union _ _ [] state = raise FAILURE (state, UNDEF) @@ -495,15 +459,11 @@ (* basic transitions *) -fun init_theory name f exit kill = add_trans (Init (name, f, (exit, kill))); -fun init_empty check f = add_trans (InitEmpty (check, f)); +fun init_theory name f exit = add_trans (Init (name, f, exit)); val exit = add_trans Exit; -val undo_exit = add_trans UndoExit; -val kill = add_trans Kill; -val history = add_trans o History; +val commit_exit = add_trans CommitExit (name "end" empty); val keep' = add_trans o Keep; -fun map_current f = add_trans (Transaction (false, f)); -fun app_current f = add_trans (Transaction (true, f)); +fun app_current f = add_trans (Transaction f); fun keep f = add_trans (Keep (fn _ => f)); fun imperative f = keep (fn _ => f ()); @@ -557,7 +517,7 @@ (* proof transitions *) -fun end_proof f = map_current (fn int => +fun end_proof f = app_current (fn int => (fn Proof (prf, (finish, _)) => let val state = ProofNode.current prf in if can (Proof.assert_bottom true) state then @@ -601,17 +561,17 @@ end; -val forget_proof = map_current (fn _ => +val forget_proof = app_current (fn _ => (fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) | SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) | _ => raise UNDEF)); -fun present_proof f = map_current (fn int => +fun present_proof f = app_current (fn int => (fn Proof (prf, x) => Proof (ProofNode.apply I prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF) #> tap (f int)); -fun proofs' f = map_current (fn int => +fun proofs' f = app_current (fn int => (fn Proof (prf, x) => Proof (ProofNode.applys (f int) prf, x) | skip as SkipProof _ => skip | _ => raise UNDEF)); @@ -620,15 +580,15 @@ val proofs = proofs' o K; val proof = proof' o K; -fun actual_proof f = map_current (fn _ => +fun actual_proof f = app_current (fn _ => (fn Proof (prf, x) => Proof (f prf, x) | _ => raise UNDEF)); -fun skip_proof f = map_current (fn _ => +fun skip_proof f = app_current (fn _ => (fn SkipProof (h, x) => SkipProof (f h, x) | _ => raise UNDEF)); -fun skip_proof_to_theory pred = map_current (fn _ => +fun skip_proof_to_theory pred = app_current (fn _ => (fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF | _ => raise UNDEF)); @@ -677,7 +637,6 @@ let val ctxt = try context_of st in (case app int tr st of (_, SOME TERMINATE) => NONE - | (_, SOME RESTART) => SOME (toplevel, NONE) | (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) | (state', SOME exn) => SOME (state', SOME (exn_context ctxt exn, at_command tr)) | (state', NONE) => SOME (state', NONE)) @@ -690,24 +649,25 @@ local -fun excur [] x = x - | excur ((tr, pr) :: trs) (st, res) = - (case transition (! interact) tr st of - SOME (st', NONE) => - excur trs (st', setmp_thread_position tr (fn () => pr st st' res) () handle exn => - raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) - | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info - | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); +fun no_pr _ _ _ = (); -fun no_pr _ _ _ = (); +fun excur (tr, pr) st res = + (case transition (! interact) tr st of + SOME (st', NONE) => + (st, st', setmp_thread_position tr (fn () => pr st st' res) () handle exn => + raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) + | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info + | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); + +fun excurs (tr :: trs) (_, st, res) = excurs trs (excur tr st res) + | excurs [] (st, st', res') = + if is_toplevel st' then (excur (commit_exit, no_pr) st (); res') + else error "Unfinished development at end of input"; in fun present_excursion trs res = - (case excur trs (toplevel, res) of - (state as Toplevel _, res') => (safe_exit state; res') - | _ => error "Unfinished development at end of input") - handle exn => error (exn_message exn); + excurs trs (toplevel, toplevel, res) handle exn => error (exn_message exn); fun excursion trs = present_excursion (map (rpair no_pr) trs) ();