1.1 --- a/src/Pure/Isar/isar.ML Wed Mar 04 11:05:02 2009 +0100
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,379 +0,0 @@
1.4 -(* Title: Pure/Isar/isar.ML
1.5 - Author: Makarius
1.6 -
1.7 -The global Isabelle/Isar state and main read-eval-print loop.
1.8 -*)
1.9 -
1.10 -signature ISAR =
1.11 -sig
1.12 - val init: unit -> unit
1.13 - val exn: unit -> (exn * string) option
1.14 - val state: unit -> Toplevel.state
1.15 - val context: unit -> Proof.context
1.16 - val goal: unit -> thm
1.17 - val print: unit -> unit
1.18 - val >> : Toplevel.transition -> bool
1.19 - val >>> : Toplevel.transition list -> unit
1.20 - val linear_undo: int -> unit
1.21 - val undo: int -> unit
1.22 - val kill: unit -> unit
1.23 - val kill_proof: unit -> unit
1.24 - val crashes: exn list ref
1.25 - val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
1.26 - val loop: unit -> unit
1.27 - val main: unit -> unit
1.28 -
1.29 - type id = string
1.30 - val no_id: id
1.31 - val create_command: Toplevel.transition -> id
1.32 - val insert_command: id -> id -> unit
1.33 - val remove_command: id -> unit
1.34 -end;
1.35 -
1.36 -structure Isar: ISAR =
1.37 -struct
1.38 -
1.39 -
1.40 -(** TTY model -- SINGLE-THREADED! **)
1.41 -
1.42 -(* the global state *)
1.43 -
1.44 -type history = (Toplevel.state * Toplevel.transition) list;
1.45 - (*previous state, state transition -- regular commands only*)
1.46 -
1.47 -local
1.48 - val global_history = ref ([]: history);
1.49 - val global_state = ref Toplevel.toplevel;
1.50 - val global_exn = ref (NONE: (exn * string) option);
1.51 -in
1.52 -
1.53 -fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
1.54 - let
1.55 - fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
1.56 - | edit n (st, hist) = edit (n - 1) (f st hist);
1.57 - in edit count (! global_state, ! global_history) end);
1.58 -
1.59 -fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
1.60 -fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
1.61 -
1.62 -fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
1.63 -fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
1.64 -
1.65 -end;
1.66 -
1.67 -
1.68 -fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
1.69 -
1.70 -fun context () = Toplevel.context_of (state ())
1.71 - handle Toplevel.UNDEF => error "Unknown context";
1.72 -
1.73 -fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
1.74 - handle Toplevel.UNDEF => error "No goal present";
1.75 -
1.76 -fun print () = Toplevel.print_state false (state ());
1.77 -
1.78 -
1.79 -(* history navigation *)
1.80 -
1.81 -local
1.82 -
1.83 -fun find_and_undo _ [] = error "Undo history exhausted"
1.84 - | find_and_undo which ((prev, tr) :: hist) =
1.85 - ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
1.86 - if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
1.87 -
1.88 -in
1.89 -
1.90 -fun linear_undo n = edit_history n (K (find_and_undo (K true)));
1.91 -
1.92 -fun undo n = edit_history n (fn st => fn hist =>
1.93 - find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
1.94 -
1.95 -fun kill () = edit_history 1 (fn st => fn hist =>
1.96 - find_and_undo
1.97 - (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
1.98 -
1.99 -fun kill_proof () = edit_history 1 (fn st => fn hist =>
1.100 - if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
1.101 - else raise Toplevel.UNDEF);
1.102 -
1.103 -end;
1.104 -
1.105 -
1.106 -(* interactive state transformations *)
1.107 -
1.108 -fun op >> tr =
1.109 - (case Toplevel.transition true tr (state ()) of
1.110 - NONE => false
1.111 - | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
1.112 - | SOME (st', NONE) =>
1.113 - let
1.114 - val name = Toplevel.name_of tr;
1.115 - val _ = if OuterKeyword.is_theory_begin name then init () else ();
1.116 - val _ =
1.117 - if OuterKeyword.is_regular name
1.118 - then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
1.119 - in true end);
1.120 -
1.121 -fun op >>> [] = ()
1.122 - | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
1.123 -
1.124 -
1.125 -(* toplevel loop *)
1.126 -
1.127 -val crashes = ref ([]: exn list);
1.128 -
1.129 -local
1.130 -
1.131 -fun raw_loop secure src =
1.132 - let
1.133 - fun check_secure () =
1.134 - (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
1.135 - in
1.136 - (case Source.get_single (Source.set_prompt Source.default_prompt src) of
1.137 - NONE => if secure then quit () else ()
1.138 - | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
1.139 - handle exn =>
1.140 - (Output.error_msg (Toplevel.exn_message exn)
1.141 - handle crash =>
1.142 - (CRITICAL (fn () => change crashes (cons crash));
1.143 - warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
1.144 - raw_loop secure src)
1.145 - end;
1.146 -
1.147 -in
1.148 -
1.149 -fun toplevel_loop {init = do_init, welcome, sync, secure} =
1.150 - (Context.set_thread_data NONE;
1.151 - if do_init then init () else (); (* FIXME init editor model *)
1.152 - if welcome then writeln (Session.welcome ()) else ();
1.153 - uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
1.154 -
1.155 -end;
1.156 -
1.157 -fun loop () =
1.158 - toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
1.159 -
1.160 -fun main () =
1.161 - toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
1.162 -
1.163 -
1.164 -
1.165 -(** individual toplevel commands **)
1.166 -
1.167 -(* unique identification *)
1.168 -
1.169 -type id = string;
1.170 -val no_id : id = "";
1.171 -
1.172 -
1.173 -(* command category *)
1.174 -
1.175 -datatype category = Empty | Theory | Proof | Diag | Control;
1.176 -
1.177 -fun category_of tr =
1.178 - let val name = Toplevel.name_of tr in
1.179 - if name = "" then Empty
1.180 - else if OuterKeyword.is_theory name then Theory
1.181 - else if OuterKeyword.is_proof name then Proof
1.182 - else if OuterKeyword.is_diag name then Diag
1.183 - else Control
1.184 - end;
1.185 -
1.186 -val is_theory = fn Theory => true | _ => false;
1.187 -val is_proper = fn Theory => true | Proof => true | _ => false;
1.188 -val is_regular = fn Control => false | _ => true;
1.189 -
1.190 -
1.191 -(* command status *)
1.192 -
1.193 -datatype status =
1.194 - Unprocessed |
1.195 - Running |
1.196 - Failed of exn * string |
1.197 - Finished of Toplevel.state;
1.198 -
1.199 -fun status_markup Unprocessed = Markup.unprocessed
1.200 - | status_markup Running = (Markup.runningN, [])
1.201 - | status_markup (Failed _) = Markup.failed
1.202 - | status_markup (Finished _) = Markup.finished;
1.203 -
1.204 -fun run int tr state =
1.205 - (case Toplevel.transition int tr state of
1.206 - NONE => NONE
1.207 - | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
1.208 - | SOME (state', NONE) => SOME (Finished state'));
1.209 -
1.210 -
1.211 -(* datatype command *)
1.212 -
1.213 -datatype command = Command of
1.214 - {category: category,
1.215 - transition: Toplevel.transition,
1.216 - status: status};
1.217 -
1.218 -fun make_command (category, transition, status) =
1.219 - Command {category = category, transition = transition, status = status};
1.220 -
1.221 -val empty_command =
1.222 - make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
1.223 -
1.224 -fun map_command f (Command {category, transition, status}) =
1.225 - make_command (f (category, transition, status));
1.226 -
1.227 -fun map_status f = map_command (fn (category, transition, status) =>
1.228 - (category, transition, f status));
1.229 -
1.230 -
1.231 -(* global collection of identified commands *)
1.232 -
1.233 -fun err_dup id = sys_error ("Duplicate command " ^ quote id);
1.234 -fun err_undef id = sys_error ("Unknown command " ^ quote id);
1.235 -
1.236 -local val global_commands = ref (Graph.empty: command Graph.T) in
1.237 -
1.238 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
1.239 - handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
1.240 -
1.241 -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
1.242 -
1.243 -end;
1.244 -
1.245 -fun add_edge (id1, id2) =
1.246 - if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
1.247 -
1.248 -
1.249 -fun init_commands () = change_commands (K Graph.empty);
1.250 -
1.251 -fun the_command id =
1.252 - let val Command cmd =
1.253 - if id = no_id then empty_command
1.254 - else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
1.255 - in cmd end;
1.256 -
1.257 -fun prev_command id =
1.258 - if id = no_id then no_id
1.259 - else
1.260 - (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
1.261 - [] => no_id
1.262 - | [prev] => prev
1.263 - | _ => sys_error ("Non-linear command dependency " ^ quote id));
1.264 -
1.265 -fun next_commands id =
1.266 - if id = no_id then []
1.267 - else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
1.268 -
1.269 -fun descendant_commands ids =
1.270 - Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
1.271 - handle Graph.UNDEF bad => err_undef bad;
1.272 -
1.273 -
1.274 -(* maintain status *)
1.275 -
1.276 -fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
1.277 -
1.278 -fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
1.279 -
1.280 -fun report_update_status status id =
1.281 - change_commands (Graph.map_node id (map_status (fn old_status =>
1.282 - let val markup = status_markup status
1.283 - in if markup <> status_markup old_status then report_status markup id else (); status end)));
1.284 -
1.285 -
1.286 -(* create and dispose commands *)
1.287 -
1.288 -fun create_command raw_tr =
1.289 - let
1.290 - val (id, tr) =
1.291 - (case Toplevel.get_id raw_tr of
1.292 - SOME id => (id, raw_tr)
1.293 - | NONE =>
1.294 - let val id =
1.295 - if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
1.296 - else "isabelle:" ^ serial_string ()
1.297 - in (id, Toplevel.put_id id raw_tr) end);
1.298 -
1.299 - val cmd = make_command (category_of tr, tr, Unprocessed);
1.300 - val _ = change_commands (Graph.new_node (id, cmd));
1.301 - in id end;
1.302 -
1.303 -fun dispose_commands ids =
1.304 - let
1.305 - val desc = descendant_commands ids;
1.306 - val _ = List.app (report_status Markup.disposed) desc;
1.307 - val _ = change_commands (Graph.del_nodes desc);
1.308 - in () end;
1.309 -
1.310 -
1.311 -(* final state *)
1.312 -
1.313 -fun the_state id =
1.314 - (case the_command id of
1.315 - {status = Finished state, ...} => state
1.316 - | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
1.317 -
1.318 -
1.319 -
1.320 -(** editor model **)
1.321 -
1.322 -(* run commands *)
1.323 -
1.324 -fun try_run id =
1.325 - (case try the_state (prev_command id) of
1.326 - NONE => ()
1.327 - | SOME state =>
1.328 - (case run true (#transition (the_command id)) state of
1.329 - NONE => ()
1.330 - | SOME status => report_update_status status id));
1.331 -
1.332 -fun rerun_commands ids =
1.333 - (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
1.334 -
1.335 -
1.336 -(* modify document *)
1.337 -
1.338 -fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
1.339 - let
1.340 - val nexts = next_commands prev;
1.341 - val _ = change_commands
1.342 - (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
1.343 - fold (fn next => Graph.add_edge (id, next)) nexts);
1.344 - in descendant_commands [id] end) |> rerun_commands;
1.345 -
1.346 -fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
1.347 - let
1.348 - val prev = prev_command id;
1.349 - val nexts = next_commands id;
1.350 - val _ = change_commands
1.351 - (fold (fn next => Graph.del_edge (id, next)) nexts #>
1.352 - fold (fn next => add_edge (prev, next)) nexts);
1.353 - in descendant_commands nexts end) |> rerun_commands;
1.354 -
1.355 -
1.356 -(* concrete syntax *)
1.357 -
1.358 -local
1.359 -
1.360 -structure P = OuterParse;
1.361 -val op >> = Scan.>>;
1.362 -
1.363 -in
1.364 -
1.365 -val _ =
1.366 - OuterSyntax.internal_command "Isar.command"
1.367 - (P.string -- P.string >> (fn (id, text) =>
1.368 - Toplevel.imperative (fn () =>
1.369 - ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
1.370 -
1.371 -val _ =
1.372 - OuterSyntax.internal_command "Isar.insert"
1.373 - (P.string -- P.string >> (fn (prev, id) =>
1.374 - Toplevel.imperative (fn () => insert_command prev id)));
1.375 -
1.376 -val _ =
1.377 - OuterSyntax.internal_command "Isar.remove"
1.378 - (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
1.379 -
1.380 -end;
1.381 -
1.382 -end;