author | wenzelm |
Sat, 11 Aug 2012 19:34:36 +0200 | |
changeset 48772 | e46cd0d26481 |
parent 48771 | 2ea997196d04 |
child 48918 | 6e5fd4585512 |
permissions | -rw-r--r-- |
47336 | 1 |
(* Title: Pure/PIDE/command.ML |
2 |
Author: Makarius |
|
3 |
||
4 |
Prover command execution. |
|
5 |
*) |
|
6 |
||
7 |
signature COMMAND = |
|
8 |
sig |
|
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
9 |
val range: Token.T list -> Position.range |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
10 |
val proper_range: Token.T list -> Position.range |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
11 |
type 'a memo |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
12 |
val memo: (unit -> 'a) -> 'a memo |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
13 |
val memo_value: 'a -> 'a memo |
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
14 |
val memo_eval: 'a memo -> 'a |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
15 |
val memo_result: 'a memo -> 'a |
48772 | 16 |
val run_command: Toplevel.transition -> |
17 |
Toplevel.state * bool -> (Toplevel.state * bool) * unit lazy |
|
47336 | 18 |
end; |
19 |
||
20 |
structure Command: COMMAND = |
|
21 |
struct |
|
22 |
||
48771
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
23 |
(* span range *) |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
24 |
|
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
25 |
fun range [] = (Position.none, Position.none) |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
26 |
| range toks = |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
27 |
let |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
28 |
val start_pos = Token.position_of (hd toks); |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
29 |
val end_pos = Token.end_position_of (List.last toks); |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
30 |
in (start_pos, end_pos) end; |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
31 |
|
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
32 |
val proper_range = range o #1 o take_suffix Token.is_space; |
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
33 |
|
2ea997196d04
clarified Command.range vs. Command.proper_range according to Scala version, which is potentially relevant for command status markup;
wenzelm
parents:
47395
diff
changeset
|
34 |
|
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
35 |
(* memo results *) |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
36 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
37 |
datatype 'a expr = |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
38 |
Expr of unit -> 'a | |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
39 |
Result of 'a Exn.result; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
40 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
41 |
abstype 'a memo = Memo of 'a expr Synchronized.var |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
42 |
with |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
43 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
44 |
fun memo e = Memo (Synchronized.var "Command.memo" (Expr e)); |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
45 |
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a))); |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
46 |
|
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
47 |
fun memo_eval (Memo v) = |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
48 |
(case Synchronized.value v of |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
49 |
Result res => res |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
50 |
| _ => |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
51 |
Synchronized.guarded_access v |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
52 |
(fn Result res => SOME (res, Result res) |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
53 |
| Expr e => |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
54 |
let val res = Exn.capture e (); (*memoing of physical interrupts!*) |
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
55 |
in SOME (res, Result res) end)) |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
56 |
|> Exn.release; |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
57 |
|
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
58 |
fun memo_result (Memo v) = |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
59 |
(case Synchronized.value v of |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
60 |
Result res => Exn.release res |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
61 |
| _ => raise Fail "Unfinished memo result"); |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
62 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
63 |
end; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
64 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
65 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
66 |
(* run command *) |
47336 | 67 |
|
68 |
local |
|
69 |
||
70 |
fun run int tr st = |
|
71 |
(case Toplevel.transition int tr st of |
|
72 |
SOME (st', NONE) => ([], SOME st') |
|
73 |
| SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages exn, NONE) |
|
74 |
| NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); |
|
75 |
||
76 |
fun timing tr t = |
|
77 |
if Timing.is_relevant t then Toplevel.status tr (Isabelle_Markup.timing t) else (); |
|
78 |
||
79 |
fun proof_status tr st = |
|
80 |
(case try Toplevel.proof_of st of |
|
81 |
SOME prf => Toplevel.status tr (Proof.status_markup prf) |
|
82 |
| NONE => ()); |
|
83 |
||
84 |
val no_print = Lazy.value (); |
|
85 |
||
86 |
fun print_state tr st = |
|
87 |
(Lazy.lazy o Toplevel.setmp_thread_position tr) |
|
88 |
(fn () => Toplevel.print_state false st); |
|
89 |
||
90 |
in |
|
91 |
||
48772 | 92 |
fun run_command tr (st, malformed) = |
93 |
if malformed then ((Toplevel.toplevel, malformed), no_print) |
|
94 |
else |
|
95 |
let |
|
96 |
val malformed' = Toplevel.is_malformed tr; |
|
97 |
val is_init = Toplevel.is_init tr; |
|
98 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
|
47336 | 99 |
|
48772 | 100 |
val _ = Multithreading.interrupted (); |
101 |
val _ = Toplevel.status tr Isabelle_Markup.forked; |
|
102 |
val start = Timing.start (); |
|
103 |
val (errs, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
|
104 |
val _ = timing tr (Timing.result start); |
|
105 |
val _ = Toplevel.status tr Isabelle_Markup.joined; |
|
106 |
val _ = List.app (Toplevel.error_msg tr) errs; |
|
107 |
in |
|
108 |
(case result of |
|
109 |
NONE => |
|
110 |
let |
|
111 |
val _ = if null errs then Exn.interrupt () else (); |
|
112 |
val _ = Toplevel.status tr Isabelle_Markup.failed; |
|
113 |
in ((st, malformed'), no_print) end |
|
114 |
| SOME st' => |
|
115 |
let |
|
116 |
val _ = Toplevel.status tr Isabelle_Markup.finished; |
|
117 |
val _ = proof_status tr st'; |
|
118 |
val do_print = |
|
119 |
not is_init andalso |
|
120 |
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); |
|
121 |
in ((st', malformed'), if do_print then print_state tr st' else no_print) end) |
|
122 |
end; |
|
47336 | 123 |
|
124 |
end; |
|
125 |
||
126 |
end; |
|
127 |