src/Pure/System/isar.ML
changeset 30173 eabece26b89b
parent 29417 779ff1187327
child 30175 62ba490670e8
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/System/isar.ML	Sat Feb 28 18:00:20 2009 +0100
     1.3 @@ -0,0 +1,415 @@
     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 +
   1.357 +(** command syntax **)
   1.358 +
   1.359 +local
   1.360 +
   1.361 +structure P = OuterParse and K = OuterKeyword;
   1.362 +val op >> = Scan.>>;
   1.363 +
   1.364 +in
   1.365 +
   1.366 +(* global history *)
   1.367 +
   1.368 +val _ =
   1.369 +  OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
   1.370 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
   1.371 +
   1.372 +val _ =
   1.373 +  OuterSyntax.improper_command "linear_undo" "undo commands" K.control
   1.374 +    (Scan.optional P.nat 1 >>
   1.375 +      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
   1.376 +
   1.377 +val _ =
   1.378 +  OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
   1.379 +    (Scan.optional P.nat 1 >>
   1.380 +      (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
   1.381 +
   1.382 +val _ =
   1.383 +  OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
   1.384 +    (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
   1.385 +      Toplevel.keep (fn state =>
   1.386 +        if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
   1.387 +
   1.388 +val _ =
   1.389 +  OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
   1.390 +    (P.name >>
   1.391 +      (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
   1.392 +        | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   1.393 +
   1.394 +val _ =
   1.395 +  OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   1.396 +    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   1.397 +
   1.398 +
   1.399 +(* editor model *)
   1.400 +
   1.401 +val _ =
   1.402 +  OuterSyntax.internal_command "Isar.command"
   1.403 +    (P.string -- P.string >> (fn (id, text) =>
   1.404 +      Toplevel.imperative (fn () =>
   1.405 +        ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
   1.406 +
   1.407 +val _ =
   1.408 +  OuterSyntax.internal_command "Isar.insert"
   1.409 +    (P.string -- P.string >> (fn (prev, id) =>
   1.410 +      Toplevel.imperative (fn () => insert_command prev id)));
   1.411 +
   1.412 +val _ =
   1.413 +  OuterSyntax.internal_command "Isar.remove"
   1.414 +    (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
   1.415 +
   1.416 +end;
   1.417 +
   1.418 +end;