author  wenzelm 
Wed, 04 Jan 2006 00:52:45 +0100  
changeset 18563  1df7022eac6f 
parent 17904  21c6894b5998 
child 18564  2b8ac8bc9719 
permissions  rwrr 
5828  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 

16815  10 
datatype node = 
17076  11 
Theory of theory * Proof.context option  
18563  12 
Proof of ProofHistory.T * theory  
13 
SkipProof of (int History.T * theory) * theory 

5828  14 
type state 
15 
val toplevel: state 

7732  16 
val is_toplevel: state > bool 
17076  17 
val level: state > int 
6689  18 
exception UNDEF 
17266  19 
val assert: bool > unit 
6689  20 
val node_history_of: state > node History.T 
5828  21 
val node_of: state > node 
6664  22 
val node_case: (theory > 'a) > (Proof.state > 'a) > state > 'a 
5828  23 
val theory_of: state > theory 
16452  24 
val sign_of: state > theory (*obsolete*) 
17076  25 
val body_context_of: state > Proof.context 
17208  26 
val no_body_context: state > state 
5828  27 
val proof_of: state > Proof.state 
17076  28 
val is_proof: state > bool 
9453  29 
val enter_forward_proof: state > Proof.state 
16815  30 
val prompt_state_default: state > string 
31 
val prompt_state_fn: (state > string) ref 

32 
val print_state_context: state > unit 

33 
val print_state_default: bool > state > unit 

34 
val print_state_hook: (bool > state > unit) > unit 

35 
val print_state_fn: (bool > state > unit) ref 

36 
val print_state: bool > state > unit 

37 
val pretty_state: bool > state > Pretty.T list 

16682  38 
val quiet: bool ref 
39 
val debug: bool ref 

17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

40 
val interact: bool ref 
16682  41 
val timing: bool ref 
42 
val profiling: int ref 

16815  43 
val skip_proofs: bool ref 
5828  44 
exception TERMINATE 
5990  45 
exception RESTART 
16682  46 
type transition 
6689  47 
val undo_limit: bool > int option 
5828  48 
val empty: transition 
14923  49 
val name_of: transition > string 
50 
val source_of: transition > OuterLex.token list option 

5828  51 
val name: string > transition > transition 
52 
val position: Position.T > transition > transition 

14923  53 
val source: OuterLex.token list > transition > transition 
5828  54 
val interactive: bool > transition > transition 
55 
val print: transition > transition 

16607  56 
val print': string > transition > transition 
17363  57 
val three_buffersN: string 
58 
val print3: transition > transition 

9010  59 
val no_timing: transition > transition 
5828  60 
val reset: transition > transition 
8465  61 
val init: (bool > node) > (node > unit) > (node > unit) > transition > transition 
6689  62 
val exit: transition > transition 
63 
val kill: transition > transition 

5828  64 
val keep: (state > unit) > transition > transition 
7612  65 
val keep': (bool > state > unit) > transition > transition 
6689  66 
val history: (node History.T > node History.T) > transition > transition 
5828  67 
val imperative: (unit > unit) > transition > transition 
7105  68 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) 
6689  69 
> transition > transition 
5828  70 
val theory: (theory > theory) > transition > transition 
7612  71 
val theory': (bool > theory > theory) > transition > transition 
17076  72 
val theory_context: (theory > theory * Proof.context) > transition > transition 
17363  73 
val theory_to_proof: (theory > Proof.state) > transition > transition 
18563  74 
val theory_theory_to_proof: (theory > Proof.state) > transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

75 
val proof: (Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

76 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

77 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

78 
val proofs': (bool > Proof.state > Proof.state Seq.seq) > transition > transition 
16815  79 
val actual_proof: (ProofHistory.T > ProofHistory.T) > transition > transition 
80 
val skip_proof: (int History.T > int History.T) > transition > transition 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

81 
val proof_to_theory: (Proof.state > theory) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

82 
val proof_to_theory': (bool > Proof.state > theory) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

83 
val proof_to_theory_context: (bool > Proof.state > theory * Proof.context) 
17076  84 
> transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

85 
val skip_proof_to_theory: (int > bool) > transition > transition 
18563  86 
val forget_proof: transition > transition 
9512  87 
val unknown_theory: transition > transition 
88 
val unknown_proof: transition > transition 

89 
val unknown_context: transition > transition 

5922  90 
val exn_message: exn > string 
5828  91 
val apply: bool > transition > state > (state * (exn * string) option) option 
17266  92 
val command: transition > state > state 
17076  93 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  94 
val excursion: transition list > unit 
95 
val set_state: state > unit 

96 
val get_state: unit > state 

97 
val exn: unit > (exn * string) option 

98 
val >> : transition > bool 

14985  99 
val >>> : transition list > unit 
14091  100 
type 'a isar 
101 
val loop: 'a isar > unit 

5828  102 
end; 
103 

6965  104 
structure Toplevel: TOPLEVEL = 
5828  105 
struct 
106 

107 

108 
(** toplevel state **) 

109 

16815  110 
(* datatype state *) 
5828  111 

112 
datatype node = 

18563  113 
Theory of theory * Proof.context option  (*theory with optional body context*) 
114 
Proof of ProofHistory.T * theory  (*history of proof states, original theory*) 

115 
SkipProof of (int History.T * theory) * theory; 

116 
(*history of proof depths, resulting theory, original theory*) 

5828  117 

8465  118 
datatype state = State of (node History.T * ((node > unit) * (node > unit))) option; 
5828  119 

15531  120 
val toplevel = State NONE; 
5828  121 

15531  122 
fun is_toplevel (State NONE) = true 
7732  123 
 is_toplevel _ = false; 
124 

17076  125 
fun level (State NONE) = 0 
126 
 level (State (SOME (node, _))) = 

127 
(case History.current node of 

128 
Theory _ => 0 

18563  129 
 Proof (prf, _) => Proof.level (ProofHistory.current prf) 
130 
 SkipProof ((h, _), _) => History.current h + 1); (*different notion of proof depth!*) 

17076  131 

15531  132 
fun str_of_state (State NONE) = "at top level" 
16815  133 
 str_of_state (State (SOME (node, _))) = 
134 
(case History.current node of 

135 
Theory _ => "in theory mode" 

136 
 Proof _ => "in proof mode" 

137 
 SkipProof _ => "in skipped proof mode"); 

5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

138 

a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

139 

5828  140 
(* top node *) 
141 

6689  142 
exception UNDEF; 
143 

17266  144 
fun assert true = () 
145 
 assert false = raise UNDEF; 

146 

15531  147 
fun node_history_of (State NONE) = raise UNDEF 
148 
 node_history_of (State (SOME (node, _))) = node; 

6689  149 

150 
val node_of = History.current o node_history_of; 

5828  151 

6664  152 
fun node_case f g state = 
5828  153 
(case node_of state of 
17076  154 
Theory (thy, _) => f thy 
18563  155 
 Proof (prf, _) => g (ProofHistory.current prf) 
156 
 SkipProof ((_, thy), _) => f thy); 

5828  157 

6664  158 
val theory_of = node_case I Proof.theory_of; 
16452  159 
val sign_of = theory_of; 
17076  160 

161 
fun body_context_of state = 

162 
(case node_of state of 

163 
Theory (_, SOME ctxt) => ctxt 

164 
 _ => node_case ProofContext.init Proof.context_of state); 

165 

17208  166 
fun no_body_context (State NONE) = State NONE 
167 
 no_body_context (State (SOME (node, x))) = 

168 
State (SOME (History.apply (fn Theory (thy, _) => Theory (thy, NONE)  nd => nd) node, x)); 

169 

6664  170 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17076  171 
val is_proof = can proof_of; 
6664  172 

17363  173 
val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward; 
5828  174 

175 

16815  176 
(* prompt state *) 
177 

178 
fun prompt_state_default (State _) = Source.default_prompt; 

179 

180 
val prompt_state_fn = ref prompt_state_default; 

181 
fun prompt_state state = ! prompt_state_fn state; 

182 

183 

184 
(* print state *) 

185 

186 
fun pretty_context thy = [Pretty.block 

187 
[Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), 

188 
Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]; 

189 

190 
fun pretty_state_context state = 

191 
(case try theory_of state of NONE => [] 

192 
 SOME thy => pretty_context thy); 

193 

17076  194 
fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy 
18563  195 
 pretty_node _ (Proof (prf, _)) = 
16815  196 
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) 
18563  197 
 pretty_node _ (SkipProof ((h, _), _)) = 
16815  198 
[Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]; 
199 

200 
fun pretty_state prf_only state = 

201 
let val ref (begin_state, end_state, _) = Display.current_goals_markers in 

202 
(case try node_of state of NONE => [] 

203 
 SOME node => 

204 
(if begin_state = "" then [] else [Pretty.str begin_state]) @ 

205 
pretty_node prf_only node @ 

206 
(if end_state = "" then [] else [Pretty.str end_state])) 

207 
end; 

208 

209 
val print_state_context = Pretty.writelns o pretty_state_context; 

210 
fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state); 

211 

212 
val print_state_hooks = ref ([]: (bool > state > unit) list); 

213 
fun print_state_hook f = change print_state_hooks (cons f); 

214 
val print_state_fn = ref print_state_default; 

215 

216 
fun print_state prf_only state = 

217 
(List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks); 

218 
! print_state_fn prf_only state); 

219 

220 

15668  221 

5828  222 
(** toplevel transitions **) 
223 

16682  224 
val quiet = ref false; 
225 
val debug = ref false; 

17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

226 
val interact = ref false; 
16682  227 
val timing = Output.timing; 
228 
val profiling = ref 0; 

16815  229 
val skip_proofs = ref false; 
16682  230 

5828  231 
exception TERMINATE; 
5990  232 
exception RESTART; 
7022  233 
exception EXCURSION_FAIL of exn * string; 
6689  234 
exception FAILURE of state * exn; 
5828  235 

236 

16815  237 
(* node transactions and recovery from stale theories *) 
6689  238 

16815  239 
(*NB: proof commands should be nondestructive!*) 
7022  240 

6689  241 
local 
242 

16452  243 
fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false; 
6689  244 

16815  245 
val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!"; 
246 

17076  247 
fun checkpoint_node true (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt) 
6689  248 
 checkpoint_node _ node = node; 
249 

17076  250 
fun copy_node true (Theory (thy, ctxt)) = Theory (Theory.copy thy, ctxt) 
6689  251 
 copy_node _ node = node; 
252 

15531  253 
fun return (result, NONE) = result 
254 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  255 

16729  256 
fun debug_trans f x = 
257 
if ! debug then 

16815  258 
setmp Output.transform_exceptions false 
259 
exception_trace (fn () => f x) 

16729  260 
else f x; 
261 

262 
fun interruptible f x = 

263 
let val y = ref x 

264 
in raise_interrupt (fn () => y := f x) (); ! y end; 

265 

6689  266 
in 
267 

16815  268 
fun transaction _ _ _ (State NONE) = raise UNDEF 
18563  269 
 transaction save hist f (State (SOME (node, term))) = 
6689  270 
let 
18563  271 
val cont_node = History.map (checkpoint_node save) node; 
272 
val back_node = History.map (copy_node save) cont_node; 

16729  273 
fun state nd = State (SOME (nd, term)); 
274 
fun normal_state nd = (state nd, NONE); 

275 
fun error_state nd exn = (state nd, SOME exn); 

6689  276 

16729  277 
val (result, err) = 
278 
cont_node 

18563  279 
> (f 
280 
> (if hist then History.apply_copy (copy_node save) else History.map) 

16729  281 
> debug_trans 
282 
> interruptible 

283 
> transform_error) 

284 
> normal_state 

285 
handle exn => error_state cont_node exn; 

6689  286 
in 
16729  287 
if is_stale result 
288 
then return (error_state back_node (if_none err stale_theory)) 

289 
else return (result, err) 

6689  290 
end; 
291 

292 
end; 

293 

294 

295 
(* primitive transitions *) 

296 

18563  297 
(*Note: Recovery from stale theories is provided only for theorylevel 
298 
operations via Transaction. Other node or state operations should 

299 
not touch theories at all. Interrupts are enabled only for Keep and 

300 
Transaction.*) 

5828  301 

302 
datatype trans = 

18563  303 
Reset  (*empty toplevel*) 
8465  304 
Init of (bool > node) * ((node > unit) * (node > unit))  
18563  305 
(*init node; with exit/kill operation*) 
306 
Exit  (*conclude node*) 

307 
Kill  (*abort node*) 

308 
Keep of bool > state > unit  (*peek at state*) 

309 
History of node History.T > node History.T  (*history operation (undo etc.)*) 

310 
Transaction of bool * bool * (bool > node > node); (*node transaction*) 

6689  311 

15531  312 
fun undo_limit int = if int then NONE else SOME 0; 
6689  313 

314 
local 

5828  315 

6689  316 
fun apply_tr _ Reset _ = toplevel 
15531  317 
 apply_tr int (Init (f, term)) (State NONE) = 
318 
State (SOME (History.init (undo_limit int) (f int), term)) 

319 
 apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF 

320 
 apply_tr _ Exit (State NONE) = raise UNDEF 

321 
 apply_tr _ Exit (State (SOME (node, (exit, _)))) = 

322 
(exit (History.current node); State NONE) 

323 
 apply_tr _ Kill (State NONE) = raise UNDEF 

324 
 apply_tr _ Kill (State (SOME (node, (_, kill)))) = 

325 
(kill (History.current node); State NONE) 

12987  326 
 apply_tr int (Keep f) state = (raise_interrupt (f int) state; state) 
15531  327 
 apply_tr _ (History _) (State NONE) = raise UNDEF 
328 
 apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) 

18563  329 
 apply_tr int (Transaction (save, hist, f)) state = 
330 
transaction (int orelse save) hist (fn x => f int x) state; 

5828  331 

6689  332 
fun apply_union _ [] state = raise FAILURE (state, UNDEF) 
333 
 apply_union int (tr :: trs) state = 

334 
transform_error (apply_tr int tr) state 

335 
handle UNDEF => apply_union int trs state 

336 
 FAILURE (alt_state, UNDEF) => apply_union int trs alt_state 

337 
 exn as FAILURE _ => raise exn 

338 
 exn => raise FAILURE (state, exn); 

339 

340 
in 

341 

15531  342 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
343 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 

6689  344 

345 
end; 

5828  346 

347 

348 
(* datatype transition *) 

349 

350 
datatype transition = Transition of 

16815  351 
{name: string, (*command name*) 
352 
pos: Position.T, (*source position*) 

353 
source: OuterLex.token list option, (*source text*) 

354 
int_only: bool, (*interactiveonly*) 

355 
print: string list, (*print modes (union)*) 

356 
no_timing: bool, (*suppress timing*) 

357 
trans: trans list}; (*primitive transitions (union)*) 

5828  358 

14923  359 
fun make_transition (name, pos, source, int_only, print, no_timing, trans) = 
360 
Transition {name = name, pos = pos, source = source, 

361 
int_only = int_only, print = print, no_timing = no_timing, trans = trans}; 

5828  362 

14923  363 
fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) = 
364 
make_transition (f (name, pos, source, int_only, print, no_timing, trans)); 

5828  365 

16607  366 
val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []); 
14923  367 

368 
fun name_of (Transition {name, ...}) = name; 

369 
fun source_of (Transition {source, ...}) = source; 

5828  370 

371 

372 
(* diagnostics *) 

373 

374 
fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; 

375 

376 
fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr; 

377 
fun at_command tr = command_msg "At " tr ^ "."; 

378 

379 
fun type_error tr state = 

6689  380 
ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  381 

382 

383 
(* modify transitions *) 

384 

14923  385 
fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) => 
386 
(nm, pos, source, int_only, print, no_timing, trans)); 

5828  387 

14923  388 
fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) => 
389 
(name, pos, source, int_only, print, no_timing, trans)); 

9010  390 

14923  391 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
15531  392 
(name, pos, SOME src, int_only, print, no_timing, trans)); 
5828  393 

14923  394 
fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) => 
395 
(name, pos, source, int_only, print, no_timing, trans)); 

396 

17363  397 
val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) => 
398 
(name, pos, source, int_only, print, true, trans)); 

399 

400 
fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 

401 
(name, pos, source, int_only, print, no_timing, trans @ [tr])); 

402 

16607  403 
fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 
404 
(name, pos, source, int_only, insert (op =) mode print, no_timing, trans)); 

405 

406 
val print = print' ""; 

5828  407 

17363  408 
val three_buffersN = "three_buffers"; 
409 
val print3 = print' three_buffersN; 

5828  410 

411 

412 
(* build transitions *) 

413 

414 
val reset = add_trans Reset; 

6689  415 
fun init f exit kill = add_trans (Init (f, (exit, kill))); 
416 
val exit = add_trans Exit; 

417 
val kill = add_trans Kill; 

7612  418 
val keep' = add_trans o Keep; 
6689  419 
val history = add_trans o History; 
18563  420 
fun map_current f = add_trans (Transaction (false, false, f)); 
421 
fun app_current save f = add_trans (Transaction (save, true, f)); 

5828  422 

7612  423 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  424 
fun imperative f = keep (fn _ => f ()); 
425 

6689  426 
fun init_theory f exit kill = 
17076  427 
init (fn int => Theory (f int, NONE)) 
428 
(fn Theory (thy, _) => exit thy  _ => raise UNDEF) 

429 
(fn Theory (thy, _) => kill thy  _ => raise UNDEF); 

5828  430 

15668  431 

432 
(* typed transitions *) 

433 

18563  434 
fun theory f = app_current false 
435 
(K (fn Theory (thy, _) => Theory (f thy, NONE)  _ => raise UNDEF)); 

436 

437 
fun theory' f = app_current false (fn int => 

17076  438 
(fn Theory (thy, _) => Theory (f int thy, NONE)  _ => raise UNDEF)); 
439 

18563  440 
fun theory_context f = app_current false 
441 
(K (fn Theory (thy, _) => Theory (apsnd SOME (f thy))  _ => raise UNDEF)); 

15668  442 

18563  443 
fun to_proof save f = app_current save (fn int => 
17076  444 
(fn Theory (thy, _) => 
17452
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

445 
let val st = f thy in 
18563  446 
if save orelse Theory.eq_thy (thy, Proof.theory_of st) then () 
17452
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

447 
else error "Theory changed at start of proof"; 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

448 
if ! skip_proofs then 
18563  449 
SkipProof ((History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st)), thy) 
450 
else Proof (ProofHistory.init (undo_limit int) st, thy) 

17452
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

451 
end 
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

452 
 _ => raise UNDEF)); 
15668  453 

18563  454 
val theory_to_proof = to_proof false; 
455 
val theory_theory_to_proof = to_proof true; 

456 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

457 
fun proofs' f = map_current (fn int => 
18563  458 
(fn Proof (prf, orig_thy) => Proof (ProofHistory.applys (f int) prf, orig_thy) 
459 
 SkipProof ((h, thy), orig_thy) => SkipProof ((History.apply I h, thy), orig_thy) 

16815  460 
 _ => raise UNDEF)); 
15668  461 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

462 
fun proof' f = proofs' (Seq.single oo f); 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

463 
val proofs = proofs' o K; 
6689  464 
val proof = proof' o K; 
16815  465 

466 
fun actual_proof f = map_current (fn _ => 

18563  467 
(fn Proof (prf, orig_thy) => Proof (f prf, orig_thy)  _ => raise UNDEF)); 
16815  468 

469 
fun skip_proof f = map_current (fn _ => 

18563  470 
(fn SkipProof ((h, thy), orig_thy) => SkipProof ((f h, thy), orig_thy)  _ => raise UNDEF)); 
15668  471 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

472 
fun end_proof f = map_current (fn int => 
18563  473 
(fn Proof (prf, _) => Theory (f int (ProofHistory.current prf)) 
474 
 SkipProof ((h, thy), _) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF 

475 
 _ => raise UNDEF)); 

476 

477 
val forget_proof = map_current (fn _ => 

478 
(fn Proof (_, orig_thy) => Theory (orig_thy, NONE) 

479 
 SkipProof (_, orig_thy) => Theory (orig_thy, NONE) 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

480 
 _ => raise UNDEF)); 
15668  481 

17076  482 
fun proof_to_theory' f = end_proof (rpair NONE oo f); 
483 
fun proof_to_theory f = proof_to_theory' (K f); 

17115  484 
fun proof_to_theory_context f = end_proof (apsnd SOME oo f); 
15668  485 

16815  486 
fun skip_proof_to_theory p = map_current (fn _ => 
18563  487 
(fn SkipProof ((h, thy), _) => 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

488 
if p (History.current h) then Theory (thy, NONE) 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

489 
else raise UNDEF 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

490 
 _ => raise UNDEF)); 
5828  491 

9512  492 
val unknown_theory = imperative (fn () => warning "Unknown theory context"); 
493 
val unknown_proof = imperative (fn () => warning "Unknown proof context"); 

494 
val unknown_context = imperative (fn () => warning "Unknown context"); 

495 

5828  496 

497 

498 
(** toplevel transactions **) 

499 

500 
(* print exceptions *) 

501 

15668  502 
local 
503 

504 
fun with_context f xs = 

505 
(case Context.get_context () of NONE => [] 

16452  506 
 SOME thy => map (f thy) xs); 
15668  507 

508 
fun raised name [] = "exception " ^ name ^ " raised" 

509 
 raised name [msg] = "exception " ^ name ^ " raised: " ^ msg 

510 
 raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); 

5828  511 

15668  512 
fun exn_msg _ TERMINATE = "Exit." 
513 
 exn_msg _ RESTART = "Restart." 

514 
 exn_msg _ Interrupt = "Interrupt." 

515 
 exn_msg _ ERROR = "ERROR." 

516 
 exn_msg _ (ERROR_MESSAGE msg) = msg 

17363  517 
 exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
16452  518 
 exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
15668  519 
 exn_msg false (THEORY (msg, _)) = msg 
16452  520 
 exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys) 
15668  521 
 exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg 
522 
 exn_msg _ (Proof.STATE (msg, _)) = msg 

523 
 exn_msg _ (ProofHistory.FAIL msg) = msg 

524 
 exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) = 

525 
fail_msg detailed "simproc" ((name, Position.none), exn) 

526 
 exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info 

527 
 exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info 

528 
 exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info 

529 
 exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] 

530 
 exn_msg true (Syntax.AST (msg, asts)) = 

531 
raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts) 

532 
 exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg] 

533 
 exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: 

534 
with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts) 

535 
 exn_msg false (TERM (msg, _)) = raised "TERM" [msg] 

536 
 exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts) 

537 
 exn_msg false (THM (msg, _, _)) = raised "THM" [msg] 

538 
 exn_msg true (THM (msg, i, thms)) = 

539 
raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms) 

540 
 exn_msg _ Option = raised "Option" [] 

541 
 exn_msg _ UnequalLengths = raised "UnequalLengths" [] 

542 
 exn_msg _ Empty = raised "Empty" [] 

543 
 exn_msg _ Subscript = raised "Subscript" [] 

16197  544 
 exn_msg _ (Fail msg) = raised "Fail" [msg] 
15668  545 
 exn_msg _ exn = General.exnMessage exn 
546 
and fail_msg detailed kind ((name, pos), exn) = 

547 
"Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; 

15519  548 

15668  549 
in 
550 

551 
fun exn_message exn = exn_msg (! debug) exn; 

5828  552 

15531  553 
fun print_exn NONE = () 
554 
 print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]); 

5828  555 

15668  556 
end; 
557 

5828  558 

559 
(* apply transitions *) 

560 

6664  561 
local 
562 

9010  563 
fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = 
5828  564 
let 
16682  565 
val _ = conditional (not int andalso int_only) (fn () => 
566 
warning (command_msg "Interactiveonly " tr)); 

567 

568 
fun do_timing f x = (info (command_msg "" tr); timeap f x); 

569 
fun do_profiling f x = profile (! profiling) f x; 

570 

6689  571 
val (result, opt_exn) = 
16729  572 
state > (apply_trans int trans 
573 
> (if ! profiling > 0 then do_profiling else I) 

574 
> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); 

16607  575 
val _ = conditional (int andalso not (! quiet) andalso 
576 
exists (fn m => m mem_string print) ("" :: ! print_mode)) 

577 
(fn () => print_state false result); 

15570  578 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) opt_exn) end; 
6664  579 

580 
in 

5828  581 

6689  582 
fun apply int tr st = 
6965  583 
(case app int tr st of 
15531  584 
(_, SOME TERMINATE) => NONE 
585 
 (_, SOME RESTART) => SOME (toplevel, NONE) 

586 
 (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) 

587 
 (state', SOME exn) => SOME (state', SOME (exn, at_command tr)) 

588 
 (state', NONE) => SOME (state', NONE)); 

6664  589 

17266  590 
fun command tr st = 
591 
(case apply false tr st of 

592 
SOME (st', NONE) => st' 

593 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 

594 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

595 

6664  596 
end; 
5828  597 

598 

17076  599 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  600 

6664  601 
local 
602 

5828  603 
fun excur [] x = x 
17076  604 
 excur ((tr, pr) :: trs) (st, res) = 
17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

605 
(case apply (! interact) tr st of 
15531  606 
SOME (st', NONE) => 
17076  607 
excur trs (st', transform_error (fn () => pr st st' res) () handle exn => 
10324  608 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
15531  609 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
610 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

5828  611 

17076  612 
fun no_pr _ _ _ = (); 
613 

6664  614 
in 
615 

17076  616 
fun present_excursion trs res = 
15531  617 
(case excur trs (State NONE, res) of 
618 
(State NONE, res') => res' 

9134  619 
 _ => raise ERROR_MESSAGE "Unfinished development at end of input") 
620 
handle exn => error (exn_message exn); 

621 

17076  622 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  623 

6664  624 
end; 
625 

5828  626 

627 

628 
(** interactive transformations **) 

629 

630 
(* the global state reference *) 

631 

15531  632 
val global_state = ref (toplevel, NONE: (exn * string) option); 
5828  633 

15531  634 
fun set_state state = global_state := (state, NONE); 
5828  635 
fun get_state () = fst (! global_state); 
636 
fun exn () = snd (! global_state); 

637 

638 

6965  639 
(* the Isar source of transitions *) 
640 

14091  641 
type 'a isar = 
6965  642 
(transition, (transition option, 
12881  643 
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, 
14091  644 
Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) 
12881  645 
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; 
6965  646 

647 

5828  648 
(* apply transformers to global state *) 
649 

14985  650 
nonfix >> >>>; 
5828  651 

652 
fun >> tr = 

653 
(case apply true tr (get_state ()) of 

15531  654 
NONE => false 
655 
 SOME (state', exn_info) => 

5828  656 
(global_state := (state', exn_info); 
16729  657 
print_exn exn_info; 
5828  658 
true)); 
659 

14985  660 
fun >>> [] = () 
661 
 >>> (tr :: trs) = if >> tr then >>> trs else (); 

662 

17513
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

663 
(*Spurious interrupts ahead! Race condition?*) 
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

664 
fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; 
7602  665 

5828  666 
fun raw_loop src = 
7602  667 
(case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of 
15531  668 
NONE => (writeln "\nInterrupt."; raw_loop src) 
669 
 SOME NONE => () 

670 
 SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ()); 

5828  671 

12987  672 
fun loop src = ignore_interrupt raw_loop src; 
5828  673 

674 
end; 