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