1 (* Title: Pure/PIDE/command.ML
4 Prover command execution: read -- eval -- print.
11 type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
13 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process}
14 type exec = eval * print list
15 val read: (unit -> theory) -> span -> Toplevel.transition
17 val eval_result_state: eval -> Toplevel.state
18 val eval: (unit -> theory) -> span -> eval -> eval
19 val print: string -> eval -> print list
20 type print_fn = Toplevel.transition -> Toplevel.state -> unit
21 val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
23 val exec_ids: exec -> Document_ID.exec list
24 val exec_run: exec -> unit
25 val stable_eval: eval -> bool
26 val stable_print: print -> bool
29 structure Command: COMMAND =
32 (** memo results -- including physical interrupts! **)
36 Result of 'a Exn.result;
38 abstype 'a memo = Memo of 'a expr Synchronized.var
41 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
42 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
44 fun memo_eval (Memo v) =
45 (case Synchronized.value v of
48 Synchronized.guarded_access v
49 (fn Result res => SOME (res, Result res)
51 let val res = Exn.capture e (); (*sic!*)
52 in SOME (res, Result res) end))
55 fun memo_fork params (Memo v) =
56 (case Synchronized.value v of
58 | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
60 fun memo_result (Memo v) =
61 (case Synchronized.value v of
62 Result res => Exn.release res
63 | _ => raise Fail "Unfinished memo result");
65 fun memo_stable (Memo v) =
66 (case Synchronized.value v of
68 | Result res => not (Exn.is_interrupt_exn res));
76 type span = Token.T list
79 {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
80 type eval_process = eval_state memo;
81 type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
83 type print_process = unit memo;
84 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
91 val outer_syntax = #2 (Outer_Syntax.get_syntax ());
92 val command_reports = Outer_Syntax.command_reports outer_syntax;
95 Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
97 (case find_first Token.is_command span of
98 SOME tok => Token.position_of tok
99 | NONE => proper_range);
101 val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
102 val _ = Position.reports_text (token_reports @ maps command_reports span);
104 if is_malformed then Toplevel.malformed pos "Malformed command syntax"
106 (case Outer_Syntax.read_spans outer_syntax span of
108 if Keyword.is_control (Toplevel.name_of tr) then
109 Toplevel.malformed pos "Illegal control command"
110 else Toplevel.modify_init init tr
111 | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
112 | _ => Toplevel.malformed proper_range "Exactly one command expected")
113 handle ERROR msg => Toplevel.malformed proper_range msg
119 val no_eval_state: eval_state =
120 {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
122 val no_eval: eval = {exec_id = Document_ID.none, eval_process = memo_value no_eval_state};
124 fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
125 val eval_result_state = #state o eval_result;
130 if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
131 (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
132 (fn () => Toplevel.command_exception int tr st); ([], SOME st))
133 else Toplevel.command_errors int tr st;
135 fun check_cmts span tr st' =
136 Toplevel.setmp_thread_position tr
138 Outer_Syntax.side_comments span |> maps (fn cmt =>
139 (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
140 handle exn => ML_Compiler.exn_messages_ids exn)) ();
142 fun proof_status tr st =
143 (case try Toplevel.proof_of st of
144 SOME prf => Toplevel.status tr (Proof.status_markup prf)
147 fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
149 {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
152 val malformed' = Toplevel.is_malformed tr;
153 val is_init = Toplevel.is_init tr;
154 val is_proof = Keyword.is_proof (Toplevel.name_of tr);
156 val _ = Multithreading.interrupted ();
157 val _ = Toplevel.status tr Markup.running;
158 val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
159 val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
160 val errs = errs1 @ errs2;
161 val _ = Toplevel.status tr Markup.finished;
162 val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
167 val _ = if null errs then Exn.interrupt () else ();
168 val _ = Toplevel.status tr Markup.failed;
169 in {failed = true, malformed = malformed', command = tr, state = st} end
172 val _ = proof_status tr st';
173 in {failed = false, malformed = malformed', command = tr, state = st'} end)
178 fun eval init span eval0 =
180 val exec_id = Document_ID.make ();
184 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
185 (fn () => read init span |> Toplevel.put_id exec_id) ();
186 in eval_state span tr (eval_result eval0) end;
187 in {exec_id = exec_id, eval_process = memo process} end;
194 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
198 type print_function = string * (int * (string -> print_fn option));
199 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
201 fun output_error tr exn =
202 List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
204 fun print_error tr f x =
205 (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
206 handle exn => output_error tr exn;
210 fun print command_name eval =
211 rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
212 (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
214 | Exn.Res (SOME print_fn) =>
216 val exec_id = Document_ID.make ();
219 val {failed, command, state = st', ...} = eval_result eval;
220 val tr = Toplevel.put_id exec_id command;
221 in if failed then () else print_error tr (fn () => print_fn tr st') () end;
222 in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
225 val exec_id = Document_ID.make ();
228 val {command, ...} = eval_result eval;
229 val tr = Toplevel.put_id exec_id command;
230 in output_error tr exn end;
231 in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
233 fun print_function {name, pri} f =
234 Synchronized.change print_functions (fn funs =>
235 (if not (AList.defined (op =) funs name) then ()
236 else warning ("Redefining command print function: " ^ quote name);
237 AList.update (op =) (name, (pri, f)) funs));
242 print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
244 val is_init = Keyword.is_theory_begin command_name;
245 val is_proof = Keyword.is_proof command_name;
248 (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
249 in if do_print then Toplevel.print_state false st' else () end));
253 (** managed evaluation **)
257 type exec = eval * print list;
258 val no_exec: exec = (no_eval, []);
260 fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
262 fun exec_run (({eval_process, ...}, prints): exec) =
263 (memo_eval eval_process;
264 prints |> List.app (fn {name, pri, print_process, ...} =>
265 memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
268 (* stable situations after cancellation *)
270 fun stable_goals exec_id =
271 not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
273 fun stable_eval ({exec_id, eval_process}: eval) =
274 stable_goals exec_id andalso memo_stable eval_process;
276 fun stable_print ({exec_id, print_process, ...}: print) =
277 stable_goals exec_id andalso memo_stable print_process;