keep/transaction: unified execution model (with debugging etc.);
authorwenzelm
Fri Jul 14 14:19:48 2006 +0200 (2006-07-14)
changeset 201288f0e07d7cf92
parent 20127 4ddbf46ef9bd
child 20129 95e84d2c9f2c
keep/transaction: unified execution model (with debugging etc.);
tuned;
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Fri Jul 14 13:51:30 2006 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Jul 14 14:19:48 2006 +0200
     1.3 @@ -44,6 +44,8 @@
     1.4    val skip_proofs: bool ref
     1.5    exception TERMINATE
     1.6    exception RESTART
     1.7 +  val exn_message: exn -> string
     1.8 +  val program: (unit -> 'a) -> 'a
     1.9    val checkpoint: state -> state
    1.10    val copy: state -> state
    1.11    type transition
    1.12 @@ -64,9 +66,9 @@
    1.13    val init: (bool -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition
    1.14    val exit: transition -> transition
    1.15    val kill: transition -> transition
    1.16 +  val history: (node History.T -> node History.T) -> transition -> transition
    1.17    val keep: (state -> unit) -> transition -> transition
    1.18    val keep': (bool -> state -> unit) -> transition -> transition
    1.19 -  val history: (node History.T -> node History.T) -> transition -> transition
    1.20    val imperative: (unit -> unit) -> transition -> transition
    1.21    val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit)
    1.22      -> transition -> transition
    1.23 @@ -93,11 +95,9 @@
    1.24    val unknown_theory: transition -> transition
    1.25    val unknown_proof: transition -> transition
    1.26    val unknown_context: transition -> transition
    1.27 -  val exn_message: exn -> string
    1.28    val apply: bool -> transition -> state -> (state * (exn * string) option) option
    1.29    val present_excursion: (transition * (state -> state -> 'a -> 'a)) list -> 'a -> 'a
    1.30    val excursion: transition list -> unit
    1.31 -  val program: (unit -> 'a) -> 'a
    1.32    val set_state: state -> unit
    1.33    val get_state: unit -> state
    1.34    val exn: unit -> (exn * string) option
    1.35 @@ -247,12 +247,91 @@
    1.36  exception EXCURSION_FAIL of exn * string;
    1.37  exception FAILURE of state * exn;
    1.38  
    1.39 +
    1.40 +(* print exceptions *)
    1.41 +
    1.42 +local
    1.43 +
    1.44 +fun with_context f xs =
    1.45 +  (case Context.get_context () of NONE => []
    1.46 +  | SOME thy => map (f thy) xs);
    1.47 +
    1.48 +fun raised name [] = "exception " ^ name ^ " raised"
    1.49 +  | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
    1.50 +  | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
    1.51 +
    1.52 +fun exn_msg _ TERMINATE = "Exit."
    1.53 +  | exn_msg _ RESTART = "Restart."
    1.54 +  | exn_msg _ Interrupt = "Interrupt."
    1.55 +  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
    1.56 +  | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
    1.57 +  | exn_msg _ (ERROR msg) = msg
    1.58 +  | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
    1.59 +  | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
    1.60 +  | exn_msg false (THEORY (msg, _)) = msg
    1.61 +  | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
    1.62 +  | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
    1.63 +      fail_msg detailed "simproc" ((name, Position.none), exn)
    1.64 +  | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
    1.65 +  | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
    1.66 +  | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
    1.67 +  | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
    1.68 +  | exn_msg true (Syntax.AST (msg, asts)) =
    1.69 +      raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
    1.70 +  | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
    1.71 +  | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
    1.72 +        with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
    1.73 +  | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
    1.74 +  | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
    1.75 +  | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
    1.76 +  | exn_msg true (THM (msg, i, thms)) =
    1.77 +      raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
    1.78 +  | exn_msg _ Option.Option = raised "Option" []
    1.79 +  | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" []
    1.80 +  | exn_msg _ Empty = raised "Empty" []
    1.81 +  | exn_msg _ Subscript = raised "Subscript" []
    1.82 +  | exn_msg _ (Fail msg) = raised "Fail" [msg]
    1.83 +  | exn_msg _ exn = General.exnMessage exn
    1.84 +and fail_msg detailed kind ((name, pos), exn) =
    1.85 +  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
    1.86 +
    1.87 +in
    1.88 +
    1.89 +fun exn_message exn = exn_msg (! debug) exn;
    1.90 +
    1.91 +fun print_exn NONE = ()
    1.92 +  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
    1.93 +
    1.94 +end;
    1.95 +
    1.96 +
    1.97 +(* controlled execution *)
    1.98 +
    1.99 +local
   1.100 +
   1.101  fun debugging f x =
   1.102    if ! debug then
   1.103      setmp Library.do_transform_failure false
   1.104        exception_trace (fn () => f x)
   1.105    else f x;
   1.106  
   1.107 +fun interruptible f x =
   1.108 +  let val y = ref x
   1.109 +  in raise_interrupt (fn () => y := f x) (); ! y end;
   1.110 +
   1.111 +in
   1.112 +
   1.113 +fun controlled_execution f =
   1.114 +  f
   1.115 +  |> debugging
   1.116 +  |> interruptible
   1.117 +  |> setmp Output.do_toplevel_errors false;
   1.118 +
   1.119 +fun program f =
   1.120 +  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
   1.121 +
   1.122 +end;
   1.123 +
   1.124  
   1.125  (* node transactions and recovery from stale theories *)
   1.126  
   1.127 @@ -273,35 +352,28 @@
   1.128  fun return (result, NONE) = result
   1.129    | return (result, SOME exn) = raise FAILURE (result, exn);
   1.130  
   1.131 -fun interruptible f x =
   1.132 -  let val y = ref x
   1.133 -  in raise_interrupt (fn () => y := f x) (); ! y end;
   1.134 -
   1.135  in
   1.136  
   1.137 -fun transaction _ _ (State NONE) = raise UNDEF
   1.138 -  | transaction hist f (State (SOME (node, term))) =
   1.139 -      let
   1.140 -        val cont_node = History.map checkpoint_node node;
   1.141 -        val back_node = History.map copy_node cont_node;
   1.142 -        fun state nd = State (SOME (nd, term));
   1.143 -        fun normal_state nd = (state nd, NONE);
   1.144 -        fun error_state nd exn = (state nd, SOME exn);
   1.145 +fun transaction hist f (node, term) =
   1.146 +  let
   1.147 +    val cont_node = History.map checkpoint_node node;
   1.148 +    val back_node = History.map copy_node cont_node;
   1.149 +    fun state nd = State (SOME (nd, term));
   1.150 +    fun normal_state nd = (state nd, NONE);
   1.151 +    fun error_state nd exn = (state nd, SOME exn);
   1.152  
   1.153 -        val (result, err) =
   1.154 -          cont_node
   1.155 -          |> (f
   1.156 -              |> (if hist then History.apply_copy copy_node else History.map)
   1.157 -              |> debugging
   1.158 -              |> interruptible
   1.159 -              |> setmp Output.do_toplevel_errors false)
   1.160 -          |> normal_state
   1.161 -          handle exn => error_state cont_node exn;
   1.162 -      in
   1.163 -        if is_stale result
   1.164 -        then return (error_state back_node (the_default stale_theory err))
   1.165 -        else return (result, err)
   1.166 -      end;
   1.167 +    val (result, err) =
   1.168 +      cont_node
   1.169 +      |> (f
   1.170 +          |> (if hist then History.apply_copy copy_node else History.map)
   1.171 +          |> controlled_execution)
   1.172 +      |> normal_state
   1.173 +      handle exn => error_state cont_node exn;
   1.174 +  in
   1.175 +    if is_stale result
   1.176 +    then return (error_state back_node (the_default stale_theory err))
   1.177 +    else return (result, err)
   1.178 +  end;
   1.179  
   1.180  fun mapping f (State (SOME (node, term))) = State (SOME (History.map f node, term))
   1.181    | mapping _ state = state;
   1.182 @@ -325,8 +397,8 @@
   1.183                                                          (*init node; with exit/kill operation*)
   1.184    Exit |                                                (*conclude node*)
   1.185    Kill |                                                (*abort node*)
   1.186 +  History of node History.T -> node History.T |         (*history operation (undo etc.)*)
   1.187    Keep of bool -> state -> unit |                       (*peek at state*)
   1.188 -  History of node History.T -> node History.T |         (*history operation (undo etc.)*)
   1.189    Transaction of bool * (bool -> node -> node);         (*node transaction*)
   1.190  
   1.191  fun undo_limit int = if int then NONE else SOME 0;
   1.192 @@ -343,11 +415,13 @@
   1.193    | apply_tr _ Kill (State NONE) = raise UNDEF
   1.194    | apply_tr _ Kill (State (SOME (node, (_, kill)))) =
   1.195        (kill (History.current node); State NONE)
   1.196 -  | apply_tr int (Keep f) state =
   1.197 -      (setmp Output.do_toplevel_errors false (raise_interrupt (f int)) state; state)
   1.198    | apply_tr _ (History _) (State NONE) = raise UNDEF
   1.199    | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term))
   1.200 -  | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state;
   1.201 +  | apply_tr int (Keep f) state =
   1.202 +      controlled_execution (fn x => tap (f int) x) state
   1.203 +  | apply_tr _ (Transaction _) (State NONE) = raise UNDEF
   1.204 +  | apply_tr int (Transaction (hist, f)) (State (SOME state)) =
   1.205 +      transaction hist (fn x => f int x) state;
   1.206  
   1.207  fun apply_union _ [] state = raise FAILURE (state, UNDEF)
   1.208    | apply_union int (tr :: trs) state =
   1.209 @@ -435,8 +509,8 @@
   1.210  fun init f exit kill = add_trans (Init (f, (exit, kill)));
   1.211  val exit = add_trans Exit;
   1.212  val kill = add_trans Kill;
   1.213 +val history = add_trans o History;
   1.214  val keep' = add_trans o Keep;
   1.215 -val history = add_trans o History;
   1.216  fun map_current f = add_trans (Transaction (false, f));
   1.217  fun app_current f = add_trans (Transaction (true, f));
   1.218  
   1.219 @@ -527,63 +601,6 @@
   1.220  
   1.221  (** toplevel transactions **)
   1.222  
   1.223 -(* print exceptions *)
   1.224 -
   1.225 -local
   1.226 -
   1.227 -fun with_context f xs =
   1.228 -  (case Context.get_context () of NONE => []
   1.229 -  | SOME thy => map (f thy) xs);
   1.230 -
   1.231 -fun raised name [] = "exception " ^ name ^ " raised"
   1.232 -  | raised name [msg] = "exception " ^ name ^ " raised: " ^ msg
   1.233 -  | raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs);
   1.234 -
   1.235 -fun exn_msg _ TERMINATE = "Exit."
   1.236 -  | exn_msg _ RESTART = "Restart."
   1.237 -  | exn_msg _ Interrupt = "Interrupt."
   1.238 -  | exn_msg _ Output.TOPLEVEL_ERROR = "Error."
   1.239 -  | exn_msg _ (SYS_ERROR msg) = "## SYSTEM ERROR ##\n" ^ msg
   1.240 -  | exn_msg _ (ERROR msg) = msg
   1.241 -  | exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   1.242 -  | exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg]
   1.243 -  | exn_msg false (THEORY (msg, _)) = msg
   1.244 -  | exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys)
   1.245 -  | exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) =
   1.246 -      fail_msg detailed "simproc" ((name, Position.none), exn)
   1.247 -  | exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info
   1.248 -  | exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info
   1.249 -  | exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info
   1.250 -  | exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg]
   1.251 -  | exn_msg true (Syntax.AST (msg, asts)) =
   1.252 -      raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
   1.253 -  | exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
   1.254 -  | exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
   1.255 -        with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts)
   1.256 -  | exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
   1.257 -  | exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts)
   1.258 -  | exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
   1.259 -  | exn_msg true (THM (msg, i, thms)) =
   1.260 -      raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms)
   1.261 -  | exn_msg _ Option.Option = raised "Option" []
   1.262 -  | exn_msg _ Library.UnequalLengths = raised "UnequalLengths" []
   1.263 -  | exn_msg _ Empty = raised "Empty" []
   1.264 -  | exn_msg _ Subscript = raised "Subscript" []
   1.265 -  | exn_msg _ (Fail msg) = raised "Fail" [msg]
   1.266 -  | exn_msg _ exn = General.exnMessage exn
   1.267 -and fail_msg detailed kind ((name, pos), exn) =
   1.268 -  "Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn;
   1.269 -
   1.270 -in
   1.271 -
   1.272 -fun exn_message exn = exn_msg (! debug) exn;
   1.273 -
   1.274 -fun print_exn NONE = ()
   1.275 -  | print_exn (SOME (exn, s)) = Output.error_msg (cat_lines [exn_message exn, s]);
   1.276 -
   1.277 -end;
   1.278 -
   1.279 -
   1.280  (* apply transitions *)
   1.281  
   1.282  local
   1.283 @@ -646,12 +663,6 @@
   1.284  end;
   1.285  
   1.286  
   1.287 -(* toplevel program: independent of state *)
   1.288 -
   1.289 -fun program f =
   1.290 -  Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) ();
   1.291 -
   1.292 -
   1.293  
   1.294  (** interactive transformations **)
   1.295