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