30 val name: string -> transition -> transition |
30 val name: string -> transition -> transition |
31 val position: Position.T -> transition -> transition |
31 val position: Position.T -> transition -> transition |
32 val interactive: bool -> transition -> transition |
32 val interactive: bool -> transition -> transition |
33 val print: transition -> transition |
33 val print: transition -> transition |
34 val reset: transition -> transition |
34 val reset: transition -> transition |
35 val init: (state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition |
35 val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition |
36 val exit: transition -> transition |
36 val exit: transition -> transition |
37 val kill: transition -> transition |
37 val kill: transition -> transition |
38 val keep: (state -> unit) -> transition -> transition |
38 val keep: (state -> unit) -> transition -> transition |
39 val history: (node History.T -> node History.T) -> transition -> transition |
39 val history: (node History.T -> node History.T) -> transition -> transition |
40 val imperative: (unit -> unit) -> transition -> transition |
40 val imperative: (unit -> unit) -> transition -> transition |
41 val init_theory: (unit -> theory) -> (theory -> unit) -> (theory -> unit) |
41 val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) |
42 -> transition -> transition |
42 -> transition -> transition |
43 val theory: (theory -> theory) -> transition -> transition |
43 val theory: (theory -> theory) -> transition -> transition |
44 val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition |
44 val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition |
45 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
45 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
46 val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition |
46 val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition |
203 Also note that interrupts are enabled for Keep, MapCurrent, and |
203 Also note that interrupts are enabled for Keep, MapCurrent, and |
204 AppCurrent only.*) |
204 AppCurrent only.*) |
205 |
205 |
206 datatype trans = |
206 datatype trans = |
207 Reset | (*empty toplevel*) |
207 Reset | (*empty toplevel*) |
208 Init of (state -> node) * ((node -> unit) * (node -> unit)) | |
208 Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) | |
209 (*push node; provide exit/kill operation*) |
209 (*push node; provide exit/kill operation*) |
210 Exit | (*pop node*) |
210 Exit | (*pop node*) |
211 Kill | (*abort node*) |
211 Kill | (*abort node*) |
212 Keep of state -> unit | (*peek at state*) |
212 Keep of state -> unit | (*peek at state*) |
213 History of node History.T -> node History.T | (*history operation (undo etc.)*) |
213 History of node History.T -> node History.T | (*history operation (undo etc.)*) |
218 |
218 |
219 local |
219 local |
220 |
220 |
221 fun apply_tr _ Reset _ = toplevel |
221 fun apply_tr _ Reset _ = toplevel |
222 | apply_tr int (Init (f, term)) (state as State nodes) = |
222 | apply_tr int (Init (f, term)) (state as State nodes) = |
223 State ((History.init (undo_limit int) (f state), term) :: nodes) |
223 State ((History.init (undo_limit int) (f int state), term) :: nodes) |
224 | apply_tr _ Exit (State []) = raise UNDEF |
224 | apply_tr _ Exit (State []) = raise UNDEF |
225 | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) = |
225 | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) = |
226 (exit (History.current node); State nodes) |
226 (exit (History.current node); State nodes) |
227 | apply_tr _ Kill (State []) = raise UNDEF |
227 | apply_tr _ Kill (State []) = raise UNDEF |
228 | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) = |
228 | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) = |
308 val app_current = add_trans o AppCurrent; |
308 val app_current = add_trans o AppCurrent; |
309 |
309 |
310 fun imperative f = keep (fn _ => f ()); |
310 fun imperative f = keep (fn _ => f ()); |
311 |
311 |
312 fun init_theory f exit kill = |
312 fun init_theory f exit kill = |
313 init (fn _ => Theory (f ())) |
313 init (fn int => fn _ => Theory (f int)) |
314 (fn Theory thy => exit thy | _ => raise UNDEF) |
314 (fn Theory thy => exit thy | _ => raise UNDEF) |
315 (fn Theory thy => kill thy | _ => raise UNDEF); |
315 (fn Theory thy => kill thy | _ => raise UNDEF); |
316 |
316 |
317 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF)); |
317 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF)); |
318 fun theory_to_proof f = |
318 fun theory_to_proof f = |