36 val reset: transition -> transition |
36 val reset: transition -> transition |
37 val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition |
37 val init: (bool -> state -> node) -> (node -> unit) -> (node -> unit) -> transition -> transition |
38 val exit: transition -> transition |
38 val exit: transition -> transition |
39 val kill: transition -> transition |
39 val kill: transition -> transition |
40 val keep: (state -> unit) -> transition -> transition |
40 val keep: (state -> unit) -> transition -> transition |
|
41 val keep': (bool -> state -> unit) -> transition -> transition |
41 val history: (node History.T -> node History.T) -> transition -> transition |
42 val history: (node History.T -> node History.T) -> transition -> transition |
42 val imperative: (unit -> unit) -> transition -> transition |
43 val imperative: (unit -> unit) -> transition -> transition |
43 val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) |
44 val init_theory: (bool -> theory) -> (theory -> unit) -> (theory -> unit) |
44 -> transition -> transition |
45 -> transition -> transition |
45 val theory: (theory -> theory) -> transition -> transition |
46 val theory: (theory -> theory) -> transition -> transition |
|
47 val theory': (bool -> theory -> theory) -> transition -> transition |
46 val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition |
48 val theory_to_proof: (bool -> theory -> ProofHistory.T) -> transition -> transition |
47 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
49 val proof: (ProofHistory.T -> ProofHistory.T) -> transition -> transition |
48 val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition |
50 val proof': (bool -> ProofHistory.T -> ProofHistory.T) -> transition -> transition |
49 val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition |
51 val proof_to_theory: (ProofHistory.T -> theory) -> transition -> transition |
50 val quiet: bool ref |
52 val quiet: bool ref |
217 Reset | (*empty toplevel*) |
219 Reset | (*empty toplevel*) |
218 Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) | |
220 Init of (bool -> state -> node) * ((node -> unit) * (node -> unit)) | |
219 (*push node; provide exit/kill operation*) |
221 (*push node; provide exit/kill operation*) |
220 Exit | (*pop node*) |
222 Exit | (*pop node*) |
221 Kill | (*abort node*) |
223 Kill | (*abort node*) |
222 Keep of state -> unit | (*peek at state*) |
224 Keep of bool -> state -> unit | (*peek at state*) |
223 History of node History.T -> node History.T | (*history operation (undo etc.)*) |
225 History of node History.T -> node History.T | (*history operation (undo etc.)*) |
224 MapCurrent of bool -> node -> node | (*change node, bypassing history*) |
226 MapCurrent of bool -> node -> node | (*change node, bypassing history*) |
225 AppCurrent of bool -> node -> node; (*change node, recording history*) |
227 AppCurrent of bool -> node -> node; (*change node, recording history*) |
226 |
228 |
227 fun undo_limit int = if int then None else Some 0; |
229 fun undo_limit int = if int then None else Some 0; |
235 | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) = |
237 | apply_tr _ Exit (State ((node, (exit, _)):: nodes)) = |
236 (exit (History.current node); State nodes) |
238 (exit (History.current node); State nodes) |
237 | apply_tr _ Kill (State []) = raise UNDEF |
239 | apply_tr _ Kill (State []) = raise UNDEF |
238 | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) = |
240 | apply_tr _ Kill (State ((node, (_, kill)) :: nodes)) = |
239 (kill (History.current node); State nodes) |
241 (kill (History.current node); State nodes) |
240 | apply_tr _ (Keep f) state = (exhibit_interrupt f state; state) |
242 | apply_tr int (Keep f) state = (exhibit_interrupt (f int) state; state) |
241 | apply_tr _ (History _) (State []) = raise UNDEF |
243 | apply_tr _ (History _) (State []) = raise UNDEF |
242 | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes) |
244 | apply_tr _ (History f) (State ((node, term) :: nodes)) = State ((f node, term) :: nodes) |
243 | apply_tr int (MapCurrent f) state = node_trans int false f state |
245 | apply_tr int (MapCurrent f) state = node_trans int false f state |
244 | apply_tr int (AppCurrent f) state = node_trans int true f state; |
246 | apply_tr int (AppCurrent f) state = node_trans int true f state; |
245 |
247 |
310 |
312 |
311 val reset = add_trans Reset; |
313 val reset = add_trans Reset; |
312 fun init f exit kill = add_trans (Init (f, (exit, kill))); |
314 fun init f exit kill = add_trans (Init (f, (exit, kill))); |
313 val exit = add_trans Exit; |
315 val exit = add_trans Exit; |
314 val kill = add_trans Kill; |
316 val kill = add_trans Kill; |
315 val keep = add_trans o Keep; |
317 val keep' = add_trans o Keep; |
316 val history = add_trans o History; |
318 val history = add_trans o History; |
317 val map_current = add_trans o MapCurrent; |
319 val map_current = add_trans o MapCurrent; |
318 val app_current = add_trans o AppCurrent; |
320 val app_current = add_trans o AppCurrent; |
319 |
321 |
|
322 fun keep f = add_trans (Keep (fn _ => f)); |
320 fun imperative f = keep (fn _ => f ()); |
323 fun imperative f = keep (fn _ => f ()); |
321 |
324 |
322 fun init_theory f exit kill = |
325 fun init_theory f exit kill = |
323 init (fn int => fn _ => Theory (f int)) |
326 init (fn int => fn _ => Theory (f int)) |
324 (fn Theory thy => exit thy | _ => raise UNDEF) |
327 (fn Theory thy => exit thy | _ => raise UNDEF) |
325 (fn Theory thy => kill thy | _ => raise UNDEF); |
328 (fn Theory thy => kill thy | _ => raise UNDEF); |
326 |
329 |
327 fun theory f = app_current (fn _ => (fn Theory thy => Theory (f thy) | _ => raise UNDEF)); |
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)); |
328 fun theory_to_proof f = |
332 fun theory_to_proof f = |
329 app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF)); |
333 app_current (fn int => (fn Theory thy => Proof (f int thy) | _ => raise UNDEF)); |
330 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF)); |
334 fun proof' f = map_current (fn int => (fn Proof prf => Proof (f int prf) | _ => raise UNDEF)); |
331 val proof = proof' o K; |
335 val proof = proof' o K; |
332 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF)); |
336 fun proof_to_theory f = map_current (fn _ => (fn Proof prf => Theory (f prf) | _ => raise UNDEF)); |