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