author | wenzelm |
Thu, 04 Jul 2013 16:04:53 +0200 | |
changeset 52526 | d234cb6b60e3 |
parent 52516 | b5b3c888df9f |
child 52527 | dbac84eab3bc |
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 |
|
52509 | 9 |
type span = Token.T list |
10 |
val range: span -> Position.range |
|
11 |
val proper_range: span -> Position.range |
|
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
12 |
type 'a memo |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
13 |
val memo: (unit -> 'a) -> 'a memo |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
14 |
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
|
15 |
val memo_eval: 'a memo -> 'a |
52526 | 16 |
val memo_fork: Future.params -> 'a memo -> unit |
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
17 |
val memo_result: 'a memo -> 'a |
52526 | 18 |
val memo_stable: 'a memo -> bool |
52510 | 19 |
val read: span -> Toplevel.transition |
52526 | 20 |
type eval_state = |
21 |
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state} |
|
22 |
type eval = eval_state memo |
|
23 |
val no_eval: eval |
|
24 |
val eval: span -> Toplevel.transition -> eval_state -> eval_state |
|
25 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit |
|
26 |
type print = {name: string, pri: int, print: unit memo} |
|
27 |
val print: string -> eval -> print list |
|
28 |
val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit |
|
47336 | 29 |
end; |
30 |
||
31 |
structure Command: COMMAND = |
|
32 |
struct |
|
33 |
||
52509 | 34 |
(* source *) |
35 |
||
36 |
type span = Token.T list; |
|
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
|
37 |
|
49866 | 38 |
val range = Token.position_range_of; |
51266
3007d0bc9cb1
unified Command.is_proper in ML with Scala (see also 123be08eed88);
wenzelm
parents:
50914
diff
changeset
|
39 |
val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper; |
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
|
40 |
|
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
|
41 |
|
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
42 |
(* memo results *) |
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 |
datatype 'a expr = |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
45 |
Expr of unit -> 'a | |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
46 |
Result of 'a Exn.result; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
47 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
48 |
abstype 'a memo = Memo of 'a expr Synchronized.var |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
49 |
with |
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 |
fun memo e = Memo (Synchronized.var "Command.memo" (Expr e)); |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
52 |
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
|
53 |
|
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
54 |
fun memo_eval (Memo v) = |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
55 |
(case Synchronized.value v of |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
56 |
Result res => res |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
57 |
| _ => |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
58 |
Synchronized.guarded_access v |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
59 |
(fn Result res => SOME (res, Result res) |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
60 |
| Expr e => |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
61 |
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
|
62 |
in SOME (res, Result res) end)) |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
63 |
|> Exn.release; |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
64 |
|
52526 | 65 |
fun memo_fork params (Memo v) = |
66 |
(case Synchronized.value v of |
|
67 |
Result _ => () |
|
68 |
| _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v)))); |
|
69 |
||
47342
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
70 |
fun memo_result (Memo v) = |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
71 |
(case Synchronized.value v of |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
72 |
Result res => Exn.release res |
7828c7b3c143
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
wenzelm
parents:
47341
diff
changeset
|
73 |
| _ => raise Fail "Unfinished memo result"); |
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
74 |
|
52526 | 75 |
fun memo_stable (Memo v) = |
76 |
(case Synchronized.value v of |
|
77 |
Expr _ => true |
|
78 |
| Result res => not (Exn.is_interrupt_exn res)); |
|
79 |
||
47341
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
80 |
end; |
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
81 |
|
00f6279bb67a
Command.memo including physical interrupts (unlike Lazy.lazy);
wenzelm
parents:
47336
diff
changeset
|
82 |
|
52510 | 83 |
(* read *) |
52509 | 84 |
|
52510 | 85 |
fun read span = |
86 |
let |
|
87 |
val outer_syntax = #2 (Outer_Syntax.get_syntax ()); |
|
88 |
val command_reports = Outer_Syntax.command_reports outer_syntax; |
|
52509 | 89 |
|
52510 | 90 |
val proper_range = Position.set_range (proper_range span); |
91 |
val pos = |
|
92 |
(case find_first Token.is_command span of |
|
93 |
SOME tok => Token.position_of tok |
|
94 |
| NONE => proper_range); |
|
52509 | 95 |
|
52510 | 96 |
val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span; |
97 |
val _ = Position.reports_text (token_reports @ maps command_reports span); |
|
98 |
in |
|
99 |
if is_malformed then Toplevel.malformed pos "Malformed command syntax" |
|
100 |
else |
|
101 |
(case Outer_Syntax.read_spans outer_syntax span of |
|
102 |
[tr] => |
|
103 |
if Keyword.is_control (Toplevel.name_of tr) then |
|
104 |
Toplevel.malformed pos "Illegal control command" |
|
105 |
else tr |
|
106 |
| [] => Toplevel.ignored (Position.set_range (range span)) |
|
107 |
| _ => Toplevel.malformed proper_range "Exactly one command expected") |
|
108 |
handle ERROR msg => Toplevel.malformed proper_range msg |
|
109 |
end; |
|
52509 | 110 |
|
111 |
||
112 |
(* eval *) |
|
47336 | 113 |
|
52526 | 114 |
type eval_state = |
115 |
{failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}; |
|
116 |
val no_eval_state: eval_state = |
|
117 |
{failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel}; |
|
118 |
||
119 |
type eval = eval_state memo; |
|
120 |
val no_eval = memo_value no_eval_state; |
|
121 |
||
47336 | 122 |
local |
123 |
||
124 |
fun run int tr st = |
|
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
125 |
if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then |
51605
eca8acb42e4a
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents:
51603
diff
changeset
|
126 |
(Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} |
eca8acb42e4a
more explicit Goal.fork_params -- avoid implicit arguments via thread data;
wenzelm
parents:
51603
diff
changeset
|
127 |
(fn () => Toplevel.command_exception int tr st); ([], SOME st)) |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51266
diff
changeset
|
128 |
else Toplevel.command_errors int tr st; |
47336 | 129 |
|
52510 | 130 |
fun check_cmts span tr st' = |
131 |
Toplevel.setmp_thread_position tr |
|
132 |
(fn () => |
|
133 |
Outer_Syntax.side_comments span |> maps (fn cmt => |
|
134 |
(Thy_Output.check_text (Token.source_position_of cmt) st'; []) |
|
135 |
handle exn => ML_Compiler.exn_messages_ids exn)) (); |
|
136 |
||
47336 | 137 |
fun proof_status tr st = |
138 |
(case try Toplevel.proof_of st of |
|
139 |
SOME prf => Toplevel.status tr (Proof.status_markup prf) |
|
140 |
| NONE => ()); |
|
141 |
||
142 |
in |
|
143 |
||
52526 | 144 |
fun eval span tr ({malformed, state = st, ...}: eval_state) = |
52509 | 145 |
if malformed then |
52526 | 146 |
{failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel} |
48772 | 147 |
else |
148 |
let |
|
149 |
val malformed' = Toplevel.is_malformed tr; |
|
150 |
val is_init = Toplevel.is_init tr; |
|
151 |
val is_proof = Keyword.is_proof (Toplevel.name_of tr); |
|
47336 | 152 |
|
48772 | 153 |
val _ = Multithreading.interrupted (); |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
154 |
val _ = Toplevel.status tr Markup.running; |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48772
diff
changeset
|
155 |
val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st; |
52509 | 156 |
val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st'); |
48918
6e5fd4585512
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
wenzelm
parents:
48772
diff
changeset
|
157 |
val errs = errs1 @ errs2; |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
158 |
val _ = Toplevel.status tr Markup.finished; |
50914
fe4714886d92
identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
wenzelm
parents:
50911
diff
changeset
|
159 |
val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs; |
48772 | 160 |
in |
161 |
(case result of |
|
162 |
NONE => |
|
163 |
let |
|
164 |
val _ = if null errs then Exn.interrupt () else (); |
|
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49866
diff
changeset
|
165 |
val _ = Toplevel.status tr Markup.failed; |
52526 | 166 |
in {failed = true, malformed = malformed', command = tr, state = st} end |
48772 | 167 |
| SOME st' => |
168 |
let |
|
169 |
val _ = proof_status tr st'; |
|
52526 | 170 |
in {failed = false, malformed = malformed', command = tr, state = st'} end) |
48772 | 171 |
end; |
47336 | 172 |
|
173 |
end; |
|
174 |
||
52509 | 175 |
|
176 |
(* print *) |
|
177 |
||
52526 | 178 |
type print = {name: string, pri: int, print: unit memo}; |
179 |
type print_fn = Toplevel.transition -> Toplevel.state -> unit; |
|
52515 | 180 |
|
52511 | 181 |
local |
182 |
||
52526 | 183 |
type print_function = string * (int * (string -> print_fn option)); |
184 |
val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list); |
|
52511 | 185 |
|
52516
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
186 |
fun output_error tr exn = |
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
187 |
List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn); |
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
188 |
|
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
189 |
fun print_error tr f x = |
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
190 |
(Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x |
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
191 |
handle exn => output_error tr exn; |
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
192 |
|
52511 | 193 |
in |
52509 | 194 |
|
52526 | 195 |
fun print command_name eval = |
196 |
rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) => |
|
197 |
(case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of |
|
52516
b5b3c888df9f
more exception handling -- make print functions total;
wenzelm
parents:
52515
diff
changeset
|
198 |
Exn.Res NONE => NONE |
52526 | 199 |
| Exn.Res (SOME print_fn) => |
200 |
SOME {name = name, pri = pri, |
|
201 |
print = memo (fn () => |
|
202 |
let val {failed, command = tr, state = st', ...} = memo_result eval |
|
203 |
in if failed then () else print_error tr (fn () => print_fn tr st') () end)} |
|
204 |
| Exn.Exn exn => |
|
205 |
SOME {name = name, pri = pri, |
|
206 |
print = memo (fn () => output_error (#command (memo_result eval)) exn)})); |
|
52511 | 207 |
|
52526 | 208 |
fun print_function {name, pri} f = |
52511 | 209 |
Synchronized.change print_functions (fn funs => |
210 |
(if not (AList.defined (op =) funs name) then () |
|
211 |
else warning ("Redefining command print function: " ^ quote name); |
|
52515 | 212 |
AList.update (op =) (name, (pri, f)) funs)); |
52511 | 213 |
|
214 |
end; |
|
215 |
||
52526 | 216 |
val _ = |
217 |
print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' => |
|
218 |
let |
|
219 |
val is_init = Keyword.is_theory_begin command_name; |
|
220 |
val is_proof = Keyword.is_proof command_name; |
|
221 |
val do_print = |
|
222 |
not is_init andalso |
|
223 |
(Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st')); |
|
224 |
in if do_print then Toplevel.print_state false st' else () end)); |
|
52509 | 225 |
|
47336 | 226 |
end; |
227 |