src/Pure/Isar/toplevel.ML
author wenzelm
Wed Sep 29 13:49:07 1999 +0200 (1999-09-29)
changeset 7632 25a0d2ba3a87
parent 7612 ba11b5db431a
child 7732 d62523296573
permissions -rw-r--r--
removed extra shyps error;
     1 (*  Title:      Pure/Isar/toplevel.ML
     2     ID:         $Id$
     3     Author:     Markus Wenzel, TU Muenchen
     4 
     5 The Isabelle/Isar toplevel.
     6 *)
     7 
     8 signature TOPLEVEL =
     9 sig
    10   datatype node = Theory of theory | Proof of ProofHistory.T
    11   type state
    12   val toplevel: state
    13   val prompt_state_default: state -> string
    14   val prompt_state_fn: (state -> string) ref
    15   val print_state_context: state -> unit
    16   val print_state_default: state -> unit
    17   val print_state_fn: (state -> unit) ref
    18   val print_state: state -> unit
    19   exception UNDEF
    20   val node_history_of: state -> node History.T
    21   val node_of: state -> node
    22   val node_case: (theory -> 'a) -> (Proof.state -> 'a) -> state -> 'a
    23   val theory_of: state -> theory
    24   val sign_of: state -> Sign.sg
    25   val context_of: state -> Proof.context
    26   val proof_of: state -> Proof.state
    27   type transition
    28   exception TERMINATE
    29   exception RESTART
    30   val undo_limit: bool -> int option
    31   val empty: transition
    32   val name: string -> transition -> transition
    33   val position: Position.T -> transition -> transition
    34   val interactive: bool -> transition -> transition
    35   val print: transition -> transition
    36   val reset: transition -> transition
    37   val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    38   val exit: transition -> transition
    39   val kill: transition -> transition
    40   val keep: (state -> unit) -> transition -> transition
    41   val keep': (bool -> state -> unit) -> transition -> transition
    42   val history: (node History.T -> node History.T) -> transition -> transition
    43   val imperative: (unit -> unit) -> transition -> transition
    44   val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    45     -> transition -> transition
    46   val theory: (theory -> theory) -> transition -> transition
    47   val theory': (bool -> theory -> theory) -> transition -> transition
    48   val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition
    49   val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition
    50   val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition
    51   val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition
    52   val quiet: bool ref
    53   val trace: bool ref
    54   val exn_message: exn -> string
    55   val apply: bool -> transition -> state -> (state * (exn * string) option) option
    56   val excursion: transition list -> unit
    57   val excursion_error: transition list -> unit
    58   val set_state: state -> unit
    59   val get_state: unit -> state
    60   val exn: unit -> (exn * string) option
    61   val >> : transition -> bool
    62   type isar
    63   val loop: isar -> unit
    64 end;
    65 
    66 structure Toplevel: TOPLEVEL =
    67 struct
    68 
    69 
    70 (** toplevel state **)
    71 
    72 (* datatype node *)
    73 
    74 datatype node =
    75   Theory of theory |
    76   Proof of ProofHistory.T;
    77 
    78 fun str_of_node (Theory _) = "in theory mode"
    79   | str_of_node (Proof _) = "in proof mode";
    80 
    81 fun print_ctxt thy = Pretty.writeln (Pretty.block
    82   [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
    83     Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
    84 
    85 fun print_node_ctxt (Theory thy) = print_ctxt thy
    86   | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf));
    87 
    88 fun print_node (Theory thy) = print_ctxt thy
    89   | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf)
    90       (ProofHistory.current prf);
    91 
    92 
    93 (* datatype state *)
    94 
    95 datatype state = State of (node History.T * ((node -> unit) * (node -> unit))) list;
    96 
    97 val toplevel = State [];
    98 
    99 fun str_of_state (State []) = "at top level"
   100   | str_of_state (State ((node, _) :: _)) = str_of_node (History.current node);
   101 
   102 
   103 (* prompt_state hook *)
   104 
   105 fun prompt_state_default (State nodes) =
   106   let val len = length nodes
   107   in (if len < 2 then "" else string_of_int len) ^ Source.default_prompt end;
   108 
   109 val prompt_state_fn = ref prompt_state_default;
   110 fun prompt_state state = ! prompt_state_fn state;
   111 
   112 
   113 (* print state *)
   114 
   115 fun print_topnode _ (State []) = ()
   116   | print_topnode prt (State ((node, _) :: _)) = prt (History.current node);
   117 
   118 val print_state_context = print_topnode print_node_ctxt;
   119 
   120 fun print_state_default state =
   121   let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
   122     if begin_state = "" then () else writeln begin_state;
   123     print_topnode print_node state;
   124     if end_state = "" then () else writeln end_state
   125   end;
   126 
   127 val print_state_fn = ref print_state_default;
   128 fun print_state state = ! print_state_fn state;
   129 
   130 
   131 (* top node *)
   132 
   133 exception UNDEF;
   134 
   135 fun node_history_of (State []) = raise UNDEF
   136   | node_history_of (State ((node, _) :: _)) = node;
   137 
   138 val node_of = History.current o node_history_of;
   139 
   140 fun node_case f g state =
   141   (case node_of state of
   142     Theory thy => f thy
   143   | Proof prf => g (ProofHistory.current prf));
   144 
   145 val theory_of = node_case I Proof.theory_of;
   146 val context_of = node_case ProofContext.init Proof.context_of;
   147 val sign_of = Theory.sign_of o theory_of;
   148 val proof_of = node_case (fn _ => raise UNDEF) I;
   149 
   150 
   151 
   152 (** toplevel transitions **)
   153 
   154 exception TERMINATE;
   155 exception RESTART;
   156 exception EXCURSION_FAIL of exn * string;
   157 exception FAILURE of state * exn;
   158 
   159 
   160 (* recovery from stale signatures *)
   161 
   162 (*note: proof commands should be non-destructive!*)
   163 
   164 local
   165 
   166 fun is_stale state = Sign.is_stale (sign_of state) handle UNDEF => false;
   167 
   168 fun checkpoint_node true (Theory thy) = Theory (PureThy.checkpoint thy)
   169   | checkpoint_node _ node = node;
   170 
   171 fun copy_node true (Theory thy) = Theory (Theory.copy thy)
   172   | copy_node _ node = node;
   173 
   174 fun interruptible f x =
   175   let val y = ref (None: node History.T option);
   176   in exhibit_interrupt (fn () => y := Some (f x)) (); the (! y) end;
   177 
   178 val rollback = ERROR_MESSAGE "Stale signature encountered after succesful execution!";
   179 
   180 fun return (result, None) = result
   181   | return (result, Some exn) = raise FAILURE (result, exn);
   182 
   183 in
   184 
   185 fun node_trans _ _ _ (State []) = raise UNDEF
   186   | node_trans int hist f (State ((node, term) :: nodes)) =
   187       let
   188         fun mk_state nd = State ((nd, term) :: nodes);
   189 
   190         val cont_node = History.map (checkpoint_node int) node;
   191         val back_node = History.map (copy_node int) cont_node;
   192 
   193         val trans = if hist then History.apply_copy (copy_node int) else History.map;
   194         val (result, opt_exn) =
   195           (mk_state (transform_error (interruptible (trans (f int))) cont_node), None)
   196             handle exn => (mk_state cont_node, Some exn);
   197       in
   198         if is_stale result then return (mk_state back_node, Some (if_none opt_exn rollback))
   199         else return (result, opt_exn)
   200       end;
   201 
   202 fun check_stale state =
   203   if not (is_stale state) then ()
   204   else warning "Stale signature encountered!  Should restart current theory.";
   205 
   206 end;
   207 
   208 
   209 (* primitive transitions *)
   210 
   211 (*Important note: recovery from stale signatures is provided only for
   212   theory-level operations via MapCurrent and AppCurrent.  Other node
   213   or state operations should not touch signatures at all.
   214 
   215   Also note that interrupts are enabled for Keep, MapCurrent, and
   216   AppCurrent only.*)
   217 
   218 datatype trans =
   219   Reset |                                       (*empty toplevel*)
   220   Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) |
   221     (*push node; provide exit/kill operation*)
   222   Exit |                                        (*pop node*)
   223   Kill |                                        (*abort node*)
   224   Keep of bool -> state -> unit |               (*peek at state*)
   225   History of node History.T -> node History.T | (*history operation (undo etc.)*)
   226   MapCurrent of bool -> node -> node |          (*change node, bypassing history*)
   227   AppCurrent of bool -> node -> node;           (*change node, recording history*)
   228 
   229 fun undo_limit int = if int then None else Some 0;
   230 
   231 local
   232 
   233 fun apply_tr _ Reset _ = toplevel
   234   | apply_tr int (Init (f, term)) (state as State nodes) =
   235       State ((History.init (undo_limit int) (f int state), term) :: nodes)
   236   | apply_tr _ Exit (State []) = raise UNDEF
   237   | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) =
   238       (exit (History.current node); State nodes)
   239   | apply_tr _ Kill (State []) = raise UNDEF
   240   | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) =
   241       (kill (History.current node); State nodes)
   242   | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state)
   243   | apply_tr _ (History _) (State []) = raise UNDEF
   244   | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes)
   245   | apply_tr int (MapCurrent f) state = node_trans int false f state
   246   | apply_tr int (AppCurrent f) state = node_trans int true f state;
   247 
   248 fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   249   | apply_union int (tr :: trs) state =
   250       transform_error (apply_tr int tr) state
   251         handle UNDEF => apply_union int trs state
   252           | FAILURE (alt_state, UNDEF) => apply_union int trs alt_state
   253           | exn as FAILURE _ => raise exn
   254           | exn => raise FAILURE (state, exn);
   255 
   256 in
   257 
   258 fun apply_trans int trs state = (apply_union int trs state, None)
   259   handle FAILURE (alt_state, exn) => (alt_state, Some exn) | exn => (state, Some exn);
   260 
   261 end;
   262 
   263 
   264 (* datatype transition *)
   265 
   266 datatype transition = Transition of
   267  {name: string,
   268   pos: Position.T,
   269   int_only: bool,
   270   print: bool,
   271   trans: trans list};
   272 
   273 fun make_transition (name, pos, int_only, print, trans) =
   274   Transition {name = name, pos = pos, int_only = int_only, print = print, trans = trans};
   275 
   276 fun map_transition f (Transition {name, pos, int_only, print, trans}) =
   277   make_transition (f (name, pos, int_only, print, trans));
   278 
   279 val empty = make_transition ("<unknown>", Position.none, false, false, []);
   280 
   281 
   282 (* diagnostics *)
   283 
   284 fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos;
   285 
   286 fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr;
   287 fun at_command tr = command_msg "At " tr ^ ".";
   288 
   289 fun type_error tr state =
   290   ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state);
   291 
   292 
   293 (* modify transitions *)
   294 
   295 fun name nm = map_transition
   296   (fn (_, pos, int_only, print, trans) => (nm, pos, int_only, print, trans));
   297 
   298 fun position pos = map_transition
   299   (fn (name, _, int_only, print, trans) => (name, pos, int_only, print, trans));
   300 
   301 fun interactive int_only = map_transition
   302   (fn (name, pos, _, print, trans) => (name, pos, int_only, print, trans));
   303 
   304 val print = map_transition
   305   (fn (name, pos, int_only, _, trans) => (name, pos, int_only, true, trans));
   306 
   307 fun add_trans tr = map_transition
   308   (fn (name, pos, int_only, print, trans) => (name, pos, int_only, print, trans @ [tr]));
   309 
   310 
   311 (* build transitions *)
   312 
   313 val reset = add_trans Reset;
   314 fun init f exit kill = add_trans (Init (f, (exit, kill)));
   315 val exit = add_trans Exit;
   316 val kill = add_trans Kill;
   317 val keep' = add_trans o Keep;
   318 val history = add_trans o History;
   319 val map_current = add_trans o MapCurrent;
   320 val app_current = add_trans o AppCurrent;
   321 
   322 fun keep f = add_trans (Keep (fn _ => f));
   323 fun imperative f = keep (fn _ => f ());
   324 
   325 fun init_theory f exit kill =
   326   init (fn int => fn _ => Theory (f int))
   327     (fn Theory thy => exit thy | _ => raise UNDEF)
   328     (fn Theory thy => kill thy | _ => raise UNDEF);
   329 
   330 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF));
   331 fun theory' f = app_current (fn int => (fn Theory thy => Theory (f int thy) | _ => raise UNDEF));
   332 fun theory_to_proof f =
   333   app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF));
   334 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF));
   335 val proof = proof' o K;
   336 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF));
   337 
   338 
   339 
   340 (** toplevel transactions **)
   341 
   342 val quiet = ref false;
   343 val trace = ref false;
   344 
   345 
   346 (* print exceptions *)
   347 
   348 fun raised name = "exception " ^ name ^ " raised";
   349 fun raised_msg name msg = raised name ^ ": " ^ msg;
   350 
   351 fun exn_message TERMINATE = "Exit."
   352   | exn_message RESTART = "Restart."
   353   | exn_message (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_message exn, msg]
   354   | exn_message Interrupt = "Interrupt."
   355   | exn_message ERROR = "ERROR."
   356   | exn_message (ERROR_MESSAGE msg) = msg
   357   | exn_message (THEORY (msg, _)) = msg
   358   | exn_message (ProofContext.CONTEXT (msg, _)) = msg
   359   | exn_message (Proof.STATE (msg, _)) = msg
   360   | exn_message (ProofHistory.FAIL msg) = msg
   361   | exn_message (Attrib.ATTRIB_FAIL info) = fail_message "attribute" info
   362   | exn_message (Method.METHOD_FAIL info) = fail_message "method" info
   363   | exn_message (Syntax.AST (msg, _)) = raised_msg "AST" msg
   364   | exn_message (TYPE (msg, _, _)) = raised_msg "TYPE" msg
   365   | exn_message (TERM (msg, _)) = raised_msg "TERM" msg
   366   | exn_message (THM (msg, _, _)) = raised_msg "THM" msg
   367   | exn_message Library.OPTION = raised "Library.OPTION"
   368   | exn_message (Library.LIST msg) = raised_msg "Library.LIST" msg
   369   | exn_message exn = General.exnMessage exn
   370 and fail_message kind ((name, pos), exn) =
   371   "Error in " ^ kind ^ " " ^ name ^ Position.str_of pos ^ ":\n" ^ exn_message exn;
   372 
   373 fun print_exn None = ()
   374   | print_exn (Some (exn, s)) = error_msg (cat_lines [exn_message exn, s]);
   375 
   376 
   377 (* apply transitions *)
   378 
   379 local
   380 
   381 fun app int (tr as Transition {trans, int_only, print, ...}) state =
   382   let
   383     val _ =
   384       if int orelse not int_only then ()
   385       else warning (command_msg "Executing interactive-only " tr);
   386     val (result, opt_exn) =
   387       (if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
   388     val _ = if int andalso print andalso not (! quiet) then print_state result else ();
   389   in (result, apsome (fn UNDEF => type_error tr state | exn => exn) opt_exn) end;
   390 
   391 in
   392 
   393 fun apply int tr st =
   394   (case app int tr st of
   395     (_, Some TERMINATE) => None
   396   | (_, Some RESTART) => Some (toplevel, None)
   397   | (state', Some (EXCURSION_FAIL exn_info)) => Some (state', Some exn_info)
   398   | (state', Some exn) => Some (state', Some (exn, at_command tr))
   399   | (state', None) => Some (state', None));
   400 
   401 end;
   402 
   403 
   404 (* excursion: toplevel -- apply transformers -- toplevel *)
   405 
   406 local
   407 
   408 fun excur [] x = x
   409   | excur (tr :: trs) x =
   410       (case apply false tr x of
   411         Some (x', None) => excur trs x'
   412       | Some (x', Some exn_info) => raise EXCURSION_FAIL exn_info
   413       | None => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   414 
   415 in
   416 
   417 fun excursion trs =
   418   (case excur trs (State []) of
   419     State [] => ()
   420   | _ => raise ERROR_MESSAGE "Open block(s) pending at end of input");
   421 
   422 fun excursion_error trs =
   423   excursion trs handle exn => error (exn_message exn);
   424 
   425 end;
   426 
   427 
   428 
   429 (** interactive transformations **)
   430 
   431 (* the global state reference *)
   432 
   433 val global_state = ref (toplevel, None: (exn * string) option);
   434 
   435 fun set_state state = global_state := (state, None);
   436 fun get_state () = fst (! global_state);
   437 fun exn () = snd (! global_state);
   438 
   439 
   440 (* the Isar source of transitions *)
   441 
   442 type isar =
   443   (transition, (transition option,
   444     (OuterLex.token, (OuterLex.token,
   445       Position.T * (Symbol.symbol, (string, unit) Source.source) Source.source)
   446           Source.source) Source.source) Source.source) Source.source;
   447 
   448 
   449 (* apply transformers to global state *)
   450 
   451 nonfix >>;
   452 
   453 fun >> tr =
   454   (case apply true tr (get_state ()) of
   455     None => false
   456   | Some (state', exn_info) =>
   457       (global_state := (state', exn_info);
   458         check_stale state'; print_exn exn_info;
   459         true));
   460 
   461 (*Note: this is for Poly/ML only, we really do not intend to exhibit
   462   interrupts here*)
   463 fun get_interrupt src = Some (Source.get_single src) handle Interrupt => None;
   464 
   465 fun raw_loop src =
   466   (case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of
   467     None => (writeln "\nInterrupt."; raw_loop src)
   468   | Some None => ()
   469   | Some (Some (tr, src')) => if >> tr then raw_loop src' else ());
   470 
   471 
   472 fun loop src = mask_interrupt raw_loop src;
   473 
   474 
   475 end;