src/Pure/System/isar.ML
author wenzelm
Thu Jun 04 22:52:53 2009 +0200 (2009-06-04)
changeset 31443 c23663825e23
parent 30175 62ba490670e8
child 31478 5e412e4c6546
permissions -rw-r--r--
uniform (short) ids on both sides;
     1 (*  Title:      Pure/System/isar.ML
     2     Author:     Makarius
     3 
     4 The global Isabelle/Isar state and main read-eval-print loop.
     5 *)
     6 
     7 signature ISAR =
     8 sig
     9   val init: unit -> unit
    10   val exn: unit -> (exn * string) option
    11   val state: unit -> Toplevel.state
    12   val context: unit -> Proof.context
    13   val goal: unit -> thm
    14   val print: unit -> unit
    15   val >> : Toplevel.transition -> bool
    16   val >>> : Toplevel.transition list -> unit
    17   val linear_undo: int -> unit
    18   val undo: int -> unit
    19   val kill: unit -> unit
    20   val kill_proof: unit -> unit
    21   val crashes: exn list ref
    22   val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
    23   val loop: unit -> unit
    24   val main: unit -> unit
    25 
    26   type id = string
    27   val no_id: id
    28   val create_command: Toplevel.transition -> id
    29   val insert_command: id -> id -> unit
    30   val remove_command: id -> unit
    31 end;
    32 
    33 structure Isar: ISAR =
    34 struct
    35 
    36 
    37 (** TTY model -- SINGLE-THREADED! **)
    38 
    39 (* the global state *)
    40 
    41 type history = (Toplevel.state * Toplevel.transition) list;
    42   (*previous state, state transition -- regular commands only*)
    43 
    44 local
    45   val global_history = ref ([]: history);
    46   val global_state = ref Toplevel.toplevel;
    47   val global_exn = ref (NONE: (exn * string) option);
    48 in
    49 
    50 fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
    51   let
    52     fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
    53       | edit n (st, hist) = edit (n - 1) (f st hist);
    54   in edit count (! global_state, ! global_history) end);
    55 
    56 fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
    57 fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
    58 
    59 fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
    60 fun set_exn exn =  NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
    61 
    62 end;
    63 
    64 
    65 fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
    66 
    67 fun context () = Toplevel.context_of (state ())
    68   handle Toplevel.UNDEF => error "Unknown context";
    69 
    70 fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
    71   handle Toplevel.UNDEF => error "No goal present";
    72 
    73 fun print () = Toplevel.print_state false (state ());
    74 
    75 
    76 (* history navigation *)
    77 
    78 local
    79 
    80 fun find_and_undo _ [] = error "Undo history exhausted"
    81   | find_and_undo which ((prev, tr) :: hist) =
    82       ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
    83         if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
    84 
    85 in
    86 
    87 fun linear_undo n = edit_history n (K (find_and_undo (K true)));
    88 
    89 fun undo n = edit_history n (fn st => fn hist =>
    90   find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
    91 
    92 fun kill () = edit_history 1 (fn st => fn hist =>
    93   find_and_undo
    94     (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
    95 
    96 fun kill_proof () = edit_history 1 (fn st => fn hist =>
    97   if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
    98   else raise Toplevel.UNDEF);
    99 
   100 end;
   101 
   102 
   103 (* interactive state transformations *)
   104 
   105 fun op >> tr =
   106   (case Toplevel.transition true tr (state ()) of
   107     NONE => false
   108   | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
   109   | SOME (st', NONE) =>
   110       let
   111         val name = Toplevel.name_of tr;
   112         val _ = if OuterKeyword.is_theory_begin name then init () else ();
   113         val _ =
   114           if OuterKeyword.is_regular name
   115           then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
   116       in true end);
   117 
   118 fun op >>> [] = ()
   119   | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
   120 
   121 
   122 (* toplevel loop *)
   123 
   124 val crashes = ref ([]: exn list);
   125 
   126 local
   127 
   128 fun raw_loop secure src =
   129   let
   130     fun check_secure () =
   131       (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
   132   in
   133     (case Source.get_single (Source.set_prompt Source.default_prompt src) of
   134       NONE => if secure then quit () else ()
   135     | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
   136     handle exn =>
   137       (Output.error_msg (Toplevel.exn_message exn)
   138         handle crash =>
   139           (CRITICAL (fn () => change crashes (cons crash));
   140             warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
   141           raw_loop secure src)
   142   end;
   143 
   144 in
   145 
   146 fun toplevel_loop {init = do_init, welcome, sync, secure} =
   147  (Context.set_thread_data NONE;
   148   if do_init then init () else ();  (* FIXME init editor model *)
   149   if welcome then writeln (Session.welcome ()) else ();
   150   uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
   151 
   152 end;
   153 
   154 fun loop () =
   155   toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
   156 
   157 fun main () =
   158   toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
   159 
   160 
   161 
   162 (** individual toplevel commands **)
   163 
   164 (* unique identification *)
   165 
   166 type id = string;
   167 val no_id : id = "";
   168 
   169 
   170 (* command category *)
   171 
   172 datatype category = Empty | Theory | Proof | Diag | Control;
   173 
   174 fun category_of tr =
   175   let val name = Toplevel.name_of tr in
   176     if name = "" then Empty
   177     else if OuterKeyword.is_theory name then Theory
   178     else if OuterKeyword.is_proof name then Proof
   179     else if OuterKeyword.is_diag name then Diag
   180     else Control
   181   end;
   182 
   183 val is_theory = fn Theory => true | _ => false;
   184 val is_proper = fn Theory => true | Proof => true | _ => false;
   185 val is_regular = fn Control => false | _ => true;
   186 
   187 
   188 (* command status *)
   189 
   190 datatype status =
   191   Unprocessed |
   192   Running |
   193   Failed of exn * string |
   194   Finished of Toplevel.state;
   195 
   196 fun status_markup Unprocessed = Markup.unprocessed
   197   | status_markup Running = (Markup.runningN, [])
   198   | status_markup (Failed _) = Markup.failed
   199   | status_markup (Finished _) = Markup.finished;
   200 
   201 fun run int tr state =
   202   (case Toplevel.transition int tr state of
   203     NONE => NONE
   204   | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
   205   | SOME (state', NONE) => SOME (Finished state'));
   206 
   207 
   208 (* datatype command *)
   209 
   210 datatype command = Command of
   211  {category: category,
   212   transition: Toplevel.transition,
   213   status: status};
   214 
   215 fun make_command (category, transition, status) =
   216   Command {category = category, transition = transition, status = status};
   217 
   218 val empty_command =
   219   make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
   220 
   221 fun map_command f (Command {category, transition, status}) =
   222   make_command (f (category, transition, status));
   223 
   224 fun map_status f = map_command (fn (category, transition, status) =>
   225   (category, transition, f status));
   226 
   227 
   228 (* global collection of identified commands *)
   229 
   230 fun err_dup id = sys_error ("Duplicate command " ^ quote id);
   231 fun err_undef id = sys_error ("Unknown command " ^ quote id);
   232 
   233 local val global_commands = ref (Graph.empty: command Graph.T) in
   234 
   235 fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
   236   handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
   237 
   238 fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
   239 
   240 end;
   241 
   242 fun add_edge (id1, id2) =
   243   if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
   244 
   245 
   246 fun init_commands () = change_commands (K Graph.empty);
   247 
   248 fun the_command id =
   249   let val Command cmd =
   250     if id = no_id then empty_command
   251     else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
   252   in cmd end;
   253 
   254 fun prev_command id =
   255   if id = no_id then no_id
   256   else
   257     (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
   258       [] => no_id
   259     | [prev] => prev
   260     | _ => sys_error ("Non-linear command dependency " ^ quote id));
   261 
   262 fun next_commands id =
   263   if id = no_id then []
   264   else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
   265 
   266 fun descendant_commands ids =
   267   Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
   268     handle Graph.UNDEF bad => err_undef bad;
   269 
   270 
   271 (* maintain status *)
   272 
   273 fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
   274 
   275 fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
   276 
   277 fun report_update_status status id =
   278   change_commands (Graph.map_node id (map_status (fn old_status =>
   279     let val markup = status_markup status
   280     in if markup <> status_markup old_status then report_status markup id else (); status end)));
   281 
   282 
   283 (* create and dispose commands *)
   284 
   285 fun create_command raw_tr =
   286   let
   287     val (id, tr) =
   288       (case Toplevel.get_id raw_tr of
   289         SOME id => (id, raw_tr)
   290       | NONE =>
   291           let val id =
   292             if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
   293             else "i" ^ serial_string ()
   294           in (id, Toplevel.put_id id raw_tr) end);
   295 
   296     val cmd = make_command (category_of tr, tr, Unprocessed);
   297     val _ = change_commands (Graph.new_node (id, cmd));
   298   in id end;
   299 
   300 fun dispose_commands ids =
   301   let
   302     val desc = descendant_commands ids;
   303     val _ = List.app (report_status Markup.disposed) desc;
   304     val _ = change_commands (Graph.del_nodes desc);
   305   in () end;
   306 
   307 
   308 (* final state *)
   309 
   310 fun the_state id =
   311   (case the_command id of
   312     {status = Finished state, ...} => state
   313   | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
   314 
   315 
   316 
   317 (** editor model **)
   318 
   319 (* run commands *)
   320 
   321 fun try_run id =
   322   (case try the_state (prev_command id) of
   323     NONE => ()
   324   | SOME state =>
   325       (case run true (#transition (the_command id)) state of
   326         NONE => ()
   327       | SOME status => report_update_status status id));
   328 
   329 fun rerun_commands ids =
   330   (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
   331 
   332 
   333 (* modify document *)
   334 
   335 fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
   336   let
   337     val nexts = next_commands prev;
   338     val _ = change_commands
   339      (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
   340       fold (fn next => Graph.add_edge (id, next)) nexts);
   341   in descendant_commands [id] end) |> rerun_commands;
   342 
   343 fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
   344   let
   345     val prev = prev_command id;
   346     val nexts = next_commands id;
   347     val _ = change_commands
   348      (fold (fn next => Graph.del_edge (id, next)) nexts #>
   349       fold (fn next => add_edge (prev, next)) nexts);
   350   in descendant_commands nexts end) |> rerun_commands;
   351 
   352 
   353 
   354 (** command syntax **)
   355 
   356 local
   357 
   358 structure P = OuterParse and K = OuterKeyword;
   359 val op >> = Scan.>>;
   360 
   361 in
   362 
   363 (* global history *)
   364 
   365 val _ =
   366   OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
   367     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
   368 
   369 val _ =
   370   OuterSyntax.improper_command "linear_undo" "undo commands" K.control
   371     (Scan.optional P.nat 1 >>
   372       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
   373 
   374 val _ =
   375   OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
   376     (Scan.optional P.nat 1 >>
   377       (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
   378 
   379 val _ =
   380   OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
   381     (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
   382       Toplevel.keep (fn state =>
   383         if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
   384 
   385 val _ =
   386   OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
   387     (P.name >>
   388       (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
   389         | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
   390 
   391 val _ =
   392   OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   393     (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   394 
   395 
   396 (* editor model *)
   397 
   398 val _ =
   399   OuterSyntax.internal_command "Isar.command"
   400     (P.string -- P.string >> (fn (id, text) =>
   401       Toplevel.imperative (fn () =>
   402         ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
   403 
   404 val _ =
   405   OuterSyntax.internal_command "Isar.insert"
   406     (P.string -- P.string >> (fn (prev, id) =>
   407       Toplevel.imperative (fn () => insert_command prev id)));
   408 
   409 val _ =
   410   OuterSyntax.internal_command "Isar.remove"
   411     (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
   412 
   413 end;
   414 
   415 end;