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