src/Pure/Isar/isar.ML
author wenzelm
Thu Jul 10 20:02:55 2008 +0200 (2008-07-10 ago)
changeset 27530 df14c9cbd21d
parent 27529 6a5ccbb1bca0
child 27533 85bbd045ac3e
permissions -rw-r--r--
export init_point;
added kill, kill_proof;
misc tuning;
wenzelm@26605
     1
(*  Title:      Pure/Isar/isar.ML
wenzelm@26605
     2
    ID:         $Id$
wenzelm@26605
     3
    Author:     Makarius
wenzelm@26605
     4
wenzelm@26605
     5
The global Isabelle/Isar state and main read-eval-print loop.
wenzelm@26605
     6
*)
wenzelm@26605
     7
wenzelm@26605
     8
signature ISAR =
wenzelm@26605
     9
sig
wenzelm@27530
    10
  val init_point: unit -> unit
wenzelm@26605
    11
  val state: unit -> Toplevel.state
wenzelm@26605
    12
  val exn: unit -> (exn * string) option
wenzelm@26605
    13
  val context: unit -> Proof.context
wenzelm@26605
    14
  val goal: unit -> thm
wenzelm@26605
    15
  val >> : Toplevel.transition -> bool
wenzelm@26605
    16
  val >>> : Toplevel.transition list -> unit
wenzelm@27529
    17
  val linear_undo: int -> unit
wenzelm@27524
    18
  val undo: int -> unit
wenzelm@27530
    19
  val kill: unit -> unit
wenzelm@27530
    20
  val kill_proof: unit -> unit
wenzelm@26605
    21
  val crashes: exn list ref
wenzelm@26643
    22
  val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
wenzelm@26605
    23
  val loop: unit -> unit
wenzelm@26606
    24
  val main: unit -> unit
wenzelm@26605
    25
end;
wenzelm@26605
    26
wenzelm@26605
    27
structure Isar: ISAR =
wenzelm@26605
    28
struct
wenzelm@26605
    29
wenzelm@27432
    30
wenzelm@27428
    31
(** individual toplevel commands **)
wenzelm@27428
    32
wenzelm@27428
    33
(* unique identification *)
wenzelm@27428
    34
wenzelm@27428
    35
type id = string;
wenzelm@27428
    36
val no_id : id = "";
wenzelm@27428
    37
wenzelm@27428
    38
fun identify tr =
wenzelm@27428
    39
  (case Toplevel.get_id tr of
wenzelm@27428
    40
    SOME id => (id, tr)
wenzelm@27428
    41
  | NONE =>
wenzelm@27428
    42
      let val id = "isabelle:" ^ serial_string ()
wenzelm@27428
    43
      in (id, Toplevel.put_id id tr) end);
wenzelm@27428
    44
wenzelm@27428
    45
wenzelm@27438
    46
(* command category *)
wenzelm@27438
    47
wenzelm@27524
    48
datatype category = Empty | Theory | Proof | Diag | Control;
wenzelm@27428
    49
wenzelm@27438
    50
fun category_of tr =
wenzelm@27438
    51
  let val name = Toplevel.name_of tr in
wenzelm@27438
    52
    if name = "" then Empty
wenzelm@27524
    53
    else if OuterKeyword.is_theory name then Theory
wenzelm@27524
    54
    else if OuterKeyword.is_proof name then Proof
wenzelm@27524
    55
    else if OuterKeyword.is_diag name then Diag
wenzelm@27524
    56
    else Control
wenzelm@27438
    57
  end;
wenzelm@27428
    58
wenzelm@27524
    59
val is_theory = fn Theory => true | _ => false;
wenzelm@27524
    60
val is_proper = fn Theory => true | Proof => true | _ => false;
wenzelm@27524
    61
wenzelm@27428
    62
wenzelm@27428
    63
(* datatype command *)
wenzelm@27428
    64
wenzelm@27438
    65
datatype status =
wenzelm@27438
    66
  Initial |
wenzelm@27518
    67
  Result of Toplevel.state * (exn * string) option;
wenzelm@27438
    68
wenzelm@27428
    69
datatype command = Command of
wenzelm@27501
    70
 {category: category,
wenzelm@27438
    71
  transition: Toplevel.transition,
wenzelm@27428
    72
  status: status};
wenzelm@27428
    73
wenzelm@27501
    74
fun make_command (category, transition, status) =
wenzelm@27501
    75
  Command {category = category, transition = transition, status = status};
wenzelm@27438
    76
wenzelm@27438
    77
val empty_command =
wenzelm@27518
    78
  make_command (Empty, Toplevel.empty, Result (Toplevel.toplevel, NONE));
wenzelm@27428
    79
wenzelm@27501
    80
fun map_command f (Command {category, transition, status}) =
wenzelm@27501
    81
  make_command (f (category, transition, status));
wenzelm@27428
    82
wenzelm@27501
    83
fun map_status f = map_command (fn (category, transition, status) =>
wenzelm@27501
    84
  (category, transition, f status));
wenzelm@27428
    85
wenzelm@26605
    86
wenzelm@27501
    87
(* global collection of identified commands *)
wenzelm@27428
    88
wenzelm@27518
    89
fun err_dup id = sys_error ("Duplicate command " ^ quote id);
wenzelm@27518
    90
fun err_undef id = sys_error ("Unknown command " ^ quote id);
wenzelm@27518
    91
wenzelm@27428
    92
local
wenzelm@27428
    93
wenzelm@27501
    94
val empty_commands = Graph.empty: command Graph.T;
wenzelm@27428
    95
val global_commands = ref empty_commands;
wenzelm@27428
    96
wenzelm@27428
    97
in
wenzelm@27428
    98
wenzelm@27501
    99
fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
wenzelm@27518
   100
  handle Graph.DUP id => err_dup id | Graph.UNDEF id => err_undef id;
wenzelm@27501
   101
wenzelm@27428
   102
fun init_commands () = change_commands (K empty_commands);
wenzelm@27428
   103
wenzelm@27428
   104
fun the_command id =
wenzelm@27524
   105
  let val Command cmd =
wenzelm@27524
   106
    if id = no_id then empty_command
wenzelm@27524
   107
    else (Graph.get_node (! global_commands) id handle Graph.UNDEF _ => err_undef id)
wenzelm@27524
   108
  in cmd end;
wenzelm@27518
   109
wenzelm@27518
   110
fun prev_command id =
wenzelm@27518
   111
  if id = no_id then NONE
wenzelm@27518
   112
  else
wenzelm@27518
   113
    (case Graph.imm_preds (! global_commands) id handle Graph.UNDEF _ => err_undef id of
wenzelm@27518
   114
      [] => NONE
wenzelm@27518
   115
    | [prev] => SOME prev
wenzelm@27518
   116
    | _ => sys_error ("Non-linear command dependency " ^ quote id));
wenzelm@27501
   117
wenzelm@27501
   118
end;
wenzelm@27501
   119
wenzelm@26605
   120
wenzelm@27518
   121
fun the_result id =
wenzelm@27524
   122
  (case the_command id of
wenzelm@27524
   123
    {status = Result res, ...} => res
wenzelm@27524
   124
  | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
wenzelm@27524
   125
wenzelm@27524
   126
val the_state = #1 o the_result;
wenzelm@27428
   127
wenzelm@27501
   128
fun new_command prev (id, cmd) =
wenzelm@27501
   129
  change_commands (Graph.new_node (id, cmd) #> prev <> no_id ? Graph.add_edge (prev, id));
wenzelm@27501
   130
wenzelm@27501
   131
fun dispose_command id = change_commands (Graph.del_nodes [id]);
wenzelm@27501
   132
wenzelm@27501
   133
fun change_command_status id f = change_commands (Graph.map_node id (map_status f));
wenzelm@27501
   134
wenzelm@27428
   135
wenzelm@27428
   136
wenzelm@27428
   137
(** TTY interaction **)
wenzelm@27428
   138
wenzelm@27428
   139
(* global point *)
wenzelm@27428
   140
wenzelm@27428
   141
local val global_point = ref no_id in
wenzelm@27428
   142
wenzelm@27428
   143
fun change_point f = NAMED_CRITICAL "Isar" (fn () => change global_point f);
wenzelm@27524
   144
fun point () = NAMED_CRITICAL "Isar" (fn () => ! global_point);
wenzelm@27428
   145
wenzelm@27501
   146
end;
wenzelm@27501
   147
wenzelm@27524
   148
fun set_point id = change_point (K id);
wenzelm@27530
   149
fun init_point () = set_point no_id;
wenzelm@27524
   150
wenzelm@27524
   151
fun point_result () = NAMED_CRITICAL "Isar" (fn () =>
wenzelm@27524
   152
  let val id = point () in (id, the_result id) end);
wenzelm@27501
   153
wenzelm@27518
   154
fun state () = #1 (#2 (point_result ()));
wenzelm@27518
   155
fun exn () = #2 (#2 (point_result ()));
wenzelm@26605
   156
wenzelm@26605
   157
fun context () =
wenzelm@26605
   158
  Toplevel.context_of (state ())
wenzelm@26605
   159
    handle Toplevel.UNDEF => error "Unknown context";
wenzelm@26605
   160
wenzelm@26605
   161
fun goal () =
wenzelm@26605
   162
  #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
wenzelm@26605
   163
    handle Toplevel.UNDEF => error "No goal present";
wenzelm@26605
   164
wenzelm@26605
   165
wenzelm@26605
   166
(* interactive state transformations --- NOT THREAD-SAFE! *)
wenzelm@26605
   167
wenzelm@26605
   168
nonfix >> >>>;
wenzelm@26605
   169
wenzelm@27428
   170
fun >> raw_tr =
wenzelm@27428
   171
  let
wenzelm@27428
   172
    val (id, tr) = identify raw_tr;
wenzelm@27518
   173
    val (prev, (prev_state, _)) = point_result ();
wenzelm@27524
   174
    val category = category_of tr;
wenzelm@27524
   175
    val _ = new_command prev (id, make_command (category, tr, Initial));
wenzelm@27428
   176
  in
wenzelm@27428
   177
    (case Toplevel.transition true tr prev_state of
wenzelm@27501
   178
      NONE => (dispose_command id; false)
wenzelm@27527
   179
    | SOME (result as (_, err)) =>
wenzelm@27527
   180
        (change_command_status id (K (Result result));
wenzelm@27527
   181
          Option.map (Toplevel.error_msg tr) err;
wenzelm@27527
   182
          if is_some err orelse category = Control then dispose_command id
wenzelm@27524
   183
          else set_point id;
wenzelm@27428
   184
          true))
wenzelm@27428
   185
  end;
wenzelm@26605
   186
wenzelm@26605
   187
fun >>> [] = ()
wenzelm@26605
   188
  | >>> (tr :: trs) = if >> tr then >>> trs else ();
wenzelm@26605
   189
wenzelm@26605
   190
wenzelm@27530
   191
(* implicit navigation wrt. proper commands *)
wenzelm@27524
   192
wenzelm@27524
   193
local
wenzelm@27524
   194
wenzelm@27524
   195
fun err_undo () = error "Undo history exhausted";
wenzelm@27524
   196
wenzelm@27524
   197
fun get_prev id = the_default no_id (prev_command id);
wenzelm@27524
   198
wenzelm@27530
   199
fun find_category which id =
wenzelm@27524
   200
  (case #category (the_command id) of
wenzelm@27524
   201
    Empty => err_undo ()
wenzelm@27530
   202
  | category => if which category then id else find_category which (get_prev id));
wenzelm@27530
   203
wenzelm@27530
   204
fun find_begin_theory id =
wenzelm@27530
   205
  if id = no_id then err_undo ()
wenzelm@27530
   206
  else if is_some (Toplevel.init_of (#transition (the_command id))) then id
wenzelm@27530
   207
  else find_begin_theory (get_prev id);
wenzelm@27524
   208
wenzelm@27529
   209
fun undo_command id =
wenzelm@27530
   210
  (case Toplevel.init_of (#transition (the_command id)) of
wenzelm@27530
   211
    SOME name => get_prev id before ThyInfo.kill_thy name
wenzelm@27530
   212
  | NONE => get_prev id);
wenzelm@27529
   213
wenzelm@27524
   214
in
wenzelm@27524
   215
wenzelm@27530
   216
fun linear_undo n = change_point (funpow n (fn id => undo_command (find_category is_proper id)));
wenzelm@27530
   217
wenzelm@27530
   218
fun undo n = change_point (funpow n (fn id => undo_command
wenzelm@27530
   219
  (find_category (if Toplevel.is_proof (the_state id) then is_proper else is_theory) id)));
wenzelm@27530
   220
wenzelm@27530
   221
fun kill () = change_point (fn id => undo_command
wenzelm@27530
   222
  (if Toplevel.is_proof (the_state id) then find_category is_theory id else find_begin_theory id));
wenzelm@27530
   223
wenzelm@27530
   224
fun kill_proof () = change_point (fn id =>
wenzelm@27530
   225
  if Toplevel.is_proof (the_state id) then undo_command (find_category is_theory id)
wenzelm@27530
   226
  else raise Toplevel.UNDEF);
wenzelm@27524
   227
wenzelm@27524
   228
end;
wenzelm@27524
   229
wenzelm@27524
   230
wenzelm@26606
   231
(* toplevel loop *)
wenzelm@26605
   232
wenzelm@26605
   233
val crashes = ref ([]: exn list);
wenzelm@26605
   234
wenzelm@26605
   235
local
wenzelm@26605
   236
wenzelm@26605
   237
fun raw_loop secure src =
wenzelm@26605
   238
  let
wenzelm@26605
   239
    fun check_secure () =
wenzelm@26605
   240
      (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
wenzelm@27524
   241
    val prev = point ();
wenzelm@27524
   242
    val prev_name = Toplevel.name_of (#transition (the_command prev));
wenzelm@27428
   243
    val prompt_markup =
wenzelm@27524
   244
      prev <> no_id ? Markup.markup
wenzelm@27524
   245
        (Markup.properties [(Markup.idN, prev), (Markup.nameN, prev_name)] Markup.prompt);
wenzelm@26605
   246
  in
wenzelm@27428
   247
    (case Source.get_single (Source.set_prompt (prompt_markup Source.default_prompt) src) of
wenzelm@26606
   248
      NONE => if secure then quit () else ()
wenzelm@26606
   249
    | SOME (tr, src') => if >> tr orelse check_secure () then raw_loop secure src' else ())
wenzelm@26605
   250
    handle exn => (Output.error_msg (Toplevel.exn_message exn) handle crash =>
wenzelm@26605
   251
      (CRITICAL (fn () => change crashes (cons crash));
wenzelm@26605
   252
        warning "Recovering after Isar toplevel crash -- see also Isar.crashes");
wenzelm@26605
   253
      raw_loop secure src)
wenzelm@26605
   254
  end;
wenzelm@26605
   255
wenzelm@26605
   256
in
wenzelm@26605
   257
wenzelm@27428
   258
fun toplevel_loop {init, welcome, sync, secure} =
wenzelm@26605
   259
 (Context.set_thread_data NONE;
wenzelm@27530
   260
  if init then (init_point (); init_commands ()) else ();
wenzelm@26643
   261
  if welcome then writeln (Session.welcome ()) else ();
wenzelm@26606
   262
  uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
wenzelm@26605
   263
wenzelm@26605
   264
end;
wenzelm@26605
   265
wenzelm@26643
   266
fun loop () =
wenzelm@26643
   267
  toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
wenzelm@27528
   268
wenzelm@26643
   269
fun main () =
wenzelm@26643
   270
  toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
wenzelm@26605
   271
wenzelm@26605
   272
end;
wenzelm@26605
   273