1(* Title: Pure/PIDE/command.ML 2 Author: Makarius 3 4Prover command execution: read -- eval -- print. 5*) 6 7signature COMMAND = 8sig 9 type blob = (string * (SHA1.digest * string list) option) Exn.result 10 val read_file: Path.T -> Position.T -> Path.T -> Token.file 11 val read_thy: Toplevel.state -> theory 12 val read: Keyword.keywords -> theory -> Path.T-> (unit -> theory) -> 13 blob list * int -> Token.T list -> Toplevel.transition 14 type eval 15 val eval_command_id: eval -> Document_ID.command 16 val eval_exec_id: eval -> Document_ID.exec 17 val eval_eq: eval * eval -> bool 18 val eval_running: eval -> bool 19 val eval_finished: eval -> bool 20 val eval_result_command: eval -> Toplevel.transition 21 val eval_result_state: eval -> Toplevel.state 22 val eval: Keyword.keywords -> Path.T -> (unit -> theory) -> 23 blob list * int -> Document_ID.command -> Token.T list -> eval -> eval 24 type print 25 type print_fn = Toplevel.transition -> Toplevel.state -> unit 26 val print0: {pri: int, print_fn: print_fn} -> eval -> print 27 val print: bool -> (string * string list) list -> Keyword.keywords -> string -> 28 eval -> print list -> print list option 29 val parallel_print: print -> bool 30 type print_function = 31 {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> 32 {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option 33 val print_function: string -> print_function -> unit 34 val no_print_function: string -> unit 35 type exec = eval * print list 36 val init_exec: theory option -> exec 37 val no_exec: exec 38 val exec_ids: exec option -> Document_ID.exec list 39 val exec: Document_ID.execution -> exec -> unit 40 val exec_parallel_prints: Document_ID.execution -> Future.task list -> exec -> exec option 41end; 42 43structure Command: COMMAND = 44struct 45 46(** main phases of execution **) 47 48fun task_context group f = 49 f 50 |> Future.interruptible_task 51 |> Future.task_context "Command.run_process" group; 52 53 54(* read *) 55 56type blob = 57 (string * (SHA1.digest * string list) option) Exn.result; (*file node name, digest, lines*) 58 59fun read_file_node file_node master_dir pos src_path = 60 let 61 val _ = Position.report pos Markup.language_path; 62 val _ = 63 (case try Url.explode file_node of 64 NONE => () 65 | SOME (Url.File _) => () 66 | _ => 67 error ("Prover cannot load remote file " ^ 68 Markup.markup (Markup.path file_node) (quote file_node))); 69 val full_path = File.check_file (File.full_path master_dir src_path); 70 val text = File.read full_path; 71 val lines = split_lines text; 72 val digest = SHA1.digest text; 73 val file_pos = Position.copy_id pos (Path.position full_path); 74 in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end 75 handle ERROR msg => error (msg ^ Position.here pos); 76 77val read_file = read_file_node ""; 78 79local 80 81fun blob_file src_path lines digest file_node = 82 let 83 val file_pos = 84 Position.file file_node |> 85 (case Position.get_id (Position.thread_data ()) of 86 NONE => I 87 | SOME exec_id => Position.put_id exec_id); 88 in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end 89 90fun resolve_files keywords master_dir (blobs, blobs_index) toks = 91 (case Outer_Syntax.parse_spans toks of 92 [Command_Span.Span (Command_Span.Command_Span (cmd, _), _)] => 93 (case try (nth toks) blobs_index of 94 SOME tok => 95 let 96 val pos = Token.pos_of tok; 97 val path = Path.explode (Token.content_of tok) 98 handle ERROR msg => error (msg ^ Position.here pos); 99 fun make_file src_path (Exn.Res (file_node, NONE)) = 100 Exn.interruptible_capture (fn () => 101 read_file_node file_node master_dir pos src_path) () 102 | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) = 103 (Position.report pos Markup.language_path; 104 Exn.Res (blob_file src_path lines digest file_node)) 105 | make_file _ (Exn.Exn e) = Exn.Exn e; 106 val src_paths = Keyword.command_files keywords cmd path; 107 val files = 108 if null blobs then 109 map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths) 110 else if length src_paths = length blobs then 111 map2 make_file src_paths blobs 112 else error ("Misalignment of inlined files" ^ Position.here pos); 113 in 114 toks |> map_index (fn (i, tok) => 115 if i = blobs_index then Token.put_files files tok else tok) 116 end 117 | NONE => toks) 118 | _ => toks); 119 120fun reports_of_token keywords tok = 121 let 122 val malformed_symbols = 123 Input.source_explode (Token.input_of tok) 124 |> map_filter (fn (sym, pos) => 125 if Symbol.is_malformed sym 126 then SOME ((pos, Markup.bad ()), "Malformed symbolic character") else NONE); 127 val is_malformed = Token.is_error tok orelse not (null malformed_symbols); 128 val reports = Token.reports keywords tok @ Token.completion_report tok @ malformed_symbols; 129 in (is_malformed, reports) end; 130 131in 132 133fun read_thy st = Toplevel.theory_of st 134 handle Toplevel.UNDEF => Pure_Syn.bootstrap_thy; 135 136fun read keywords thy master_dir init blobs_info span = 137 let 138 val command_reports = Outer_Syntax.command_reports thy; 139 140 val core_range = Token.range_of (drop_suffix Token.is_ignored span); 141 val pos = 142 (case find_first Token.is_command span of 143 SOME tok => Token.pos_of tok 144 | NONE => #1 core_range); 145 146 val token_reports = map (reports_of_token keywords) span; 147 val _ = Position.reports_text (maps #2 token_reports @ maps command_reports span); 148 149 val verbatim = 150 span |> map_filter (fn tok => 151 if Token.kind_of tok = Token.Verbatim then SOME (Token.pos_of tok) else NONE); 152 val _ = 153 if null verbatim then () 154 else legacy_feature ("Old-style {* verbatim *} token -- use \<open>cartouche\<close> instead" ^ 155 Position.here_list verbatim); 156 in 157 if exists #1 token_reports then Toplevel.malformed pos "Malformed command syntax" 158 else Outer_Syntax.parse_span thy init (resolve_files keywords master_dir blobs_info span) 159 end; 160 161end; 162 163 164(* eval *) 165 166type eval_state = {failed: bool, command: Toplevel.transition, state: Toplevel.state}; 167 168fun init_eval_state opt_thy = 169 {failed = false, 170 command = Toplevel.empty, 171 state = 172 (case opt_thy of 173 NONE => Toplevel.init_toplevel () 174 | SOME thy => Toplevel.theory_toplevel thy)}; 175 176datatype eval = 177 Eval of 178 {command_id: Document_ID.command, exec_id: Document_ID.exec, eval_process: eval_state lazy}; 179 180fun eval_command_id (Eval {command_id, ...}) = command_id; 181 182fun eval_exec_id (Eval {exec_id, ...}) = exec_id; 183val eval_eq = op = o apply2 eval_exec_id; 184 185val eval_running = Execution.is_running_exec o eval_exec_id; 186fun eval_finished (Eval {eval_process, ...}) = Lazy.is_finished eval_process; 187 188fun eval_result (Eval {eval_process, ...}) = 189 Exn.release (Lazy.finished_result eval_process); 190 191val eval_result_command = #command o eval_result; 192val eval_result_state = #state o eval_result; 193 194local 195 196fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () => 197 let 198 val name = Toplevel.name_of tr; 199 val res = 200 if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0 201 else if Keyword.is_proof keywords name then Toplevel.reset_proof st0 202 else if Keyword.is_theory_end keywords name then 203 (case Toplevel.reset_notepad st0 of 204 NONE => Toplevel.reset_theory st0 205 | some => some) 206 else NONE; 207 in 208 (case res of 209 NONE => st0 210 | SOME st => (Output.error_message (Toplevel.type_error tr ^ " -- using reset state"); st)) 211 end) (); 212 213fun run keywords int tr st = 214 if Future.proofs_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then 215 let 216 val (tr1, tr2) = Toplevel.fork_presentation tr; 217 val _ = 218 Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1} 219 (fn () => Toplevel.command_exception int tr1 st); 220 in Toplevel.command_errors int tr2 st end 221 else Toplevel.command_errors int tr st; 222 223fun check_token_comments ctxt tok = 224 (Thy_Output.check_comments ctxt (Input.source_explode (Token.input_of tok)); []) 225 handle exn => 226 if Exn.is_interrupt exn then Exn.reraise exn 227 else Runtime.exn_messages exn; 228 229fun check_span_comments ctxt span tr = 230 Toplevel.setmp_thread_position tr (fn () => maps (check_token_comments ctxt) span) (); 231 232fun report tr m = 233 Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) (); 234 235fun status tr m = 236 Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) (); 237 238fun command_indent tr st = 239 (case try Toplevel.proof_of st of 240 SOME prf => 241 let val keywords = Thy_Header.get_keywords (Proof.theory_of prf) in 242 if Keyword.command_kind keywords (Toplevel.name_of tr) = SOME Keyword.prf_script then 243 (case try Proof.goal prf of 244 SOME {goal, ...} => 245 let val n = Thm.nprems_of goal 246 in if n > 1 then report tr (Markup.command_indent (n - 1)) else () end 247 | NONE => ()) 248 else () 249 end 250 | NONE => ()); 251 252 253fun eval_state keywords span tr ({state, ...}: eval_state) = 254 let 255 val _ = Thread_Attributes.expose_interrupt (); 256 257 val st = reset_state keywords tr state; 258 259 val _ = command_indent tr st; 260 val _ = status tr Markup.running; 261 val (errs1, result) = run keywords true tr st; 262 val errs2 = 263 (case result of 264 NONE => [] 265 | SOME st' => check_span_comments (Toplevel.presentation_context st') span tr); 266 val errs = errs1 @ errs2; 267 val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs; 268 in 269 (case result of 270 NONE => 271 let 272 val _ = status tr Markup.failed; 273 val _ = status tr Markup.finished; 274 val _ = if null errs then (status tr Markup.canceled; Exn.interrupt ()) else (); 275 in {failed = true, command = tr, state = st} end 276 | SOME st' => 277 let 278 val _ = 279 if Keyword.is_theory_end keywords (Toplevel.name_of tr) andalso 280 can (Toplevel.end_theory Position.none) st' 281 then status tr Markup.finalized else (); 282 val _ = status tr Markup.finished; 283 in {failed = false, command = tr, state = st'} end) 284 end; 285 286in 287 288fun eval keywords master_dir init blobs_info command_id span eval0 = 289 let 290 val exec_id = Document_ID.make (); 291 fun process () = 292 let 293 val eval_state0 = eval_result eval0; 294 val thy = read_thy (#state eval_state0); 295 val tr = 296 Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id)) 297 (fn () => 298 read keywords thy master_dir init blobs_info span |> Toplevel.exec_id exec_id) (); 299 in eval_state keywords span tr eval_state0 end; 300 in 301 Eval {command_id = command_id, exec_id = exec_id, 302 eval_process = Lazy.lazy_name "Command.eval" process} 303 end; 304 305end; 306 307 308(* print *) 309 310datatype print = Print of 311 {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool, 312 exec_id: Document_ID.exec, print_process: unit lazy}; 313 314fun print_exec_id (Print {exec_id, ...}) = exec_id; 315val print_eq = op = o apply2 print_exec_id; 316 317type print_fn = Toplevel.transition -> Toplevel.state -> unit; 318 319type print_function = 320 {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} -> 321 {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option; 322 323local 324 325val print_functions = 326 Synchronized.var "Command.print_functions" ([]: (string * print_function) list); 327 328fun print_error tr opt_context e = 329 (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e () 330 handle exn => 331 if Exn.is_interrupt exn then Exn.reraise exn 332 else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages exn); 333 334fun print_finished (Print {print_process, ...}) = Lazy.is_finished print_process; 335 336fun print_persistent (Print {persistent, ...}) = persistent; 337 338val overlay_ord = prod_ord string_ord (list_ord string_ord); 339 340fun make_print (name, args) {delay, pri, persistent, strict, print_fn} eval = 341 let 342 val exec_id = Document_ID.make (); 343 fun process () = 344 let 345 val {failed, command, state = st', ...} = eval_result eval; 346 val tr = Toplevel.exec_id exec_id command; 347 val opt_context = try Toplevel.generic_theory_of st'; 348 in 349 if failed andalso strict then () 350 else print_error tr opt_context (fn () => print_fn tr st') 351 end; 352 in 353 Print { 354 name = name, args = args, delay = delay, pri = pri, persistent = persistent, 355 exec_id = exec_id, print_process = Lazy.lazy_name "Command.print" process} 356 end; 357 358fun bad_print name_args exn = 359 make_print name_args {delay = NONE, pri = 0, persistent = false, 360 strict = false, print_fn = fn _ => fn _ => Exn.reraise exn}; 361 362in 363 364fun print0 {pri, print_fn} = 365 make_print ("", [serial_string ()]) 366 {delay = NONE, pri = pri, persistent = true, strict = true, print_fn = print_fn}; 367 368fun print command_visible command_overlays keywords command_name eval old_prints = 369 let 370 val print_functions = Synchronized.value print_functions; 371 372 fun new_print (name, args) get_pr = 373 let 374 val params = 375 {keywords = keywords, 376 command_name = command_name, 377 args = args, 378 exec_id = eval_exec_id eval}; 379 in 380 (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of 381 Exn.Res NONE => NONE 382 | Exn.Res (SOME pr) => SOME (make_print (name, args) pr eval) 383 | Exn.Exn exn => SOME (bad_print (name, args) exn eval)) 384 end; 385 386 fun get_print (name, args) = 387 (case find_first (fn Print print => (#name print, #args print) = (name, args)) old_prints of 388 NONE => 389 (case AList.lookup (op =) print_functions name of 390 NONE => 391 SOME (bad_print (name, args) (ERROR ("Missing print function " ^ quote name)) eval) 392 | SOME get_pr => new_print (name, args) get_pr) 393 | some => some); 394 395 val retained_prints = 396 filter (fn print => print_finished print andalso print_persistent print) old_prints; 397 val visible_prints = 398 if command_visible then 399 fold (fn (name, _) => cons (name, [])) print_functions command_overlays 400 |> sort_distinct overlay_ord 401 |> map_filter get_print 402 else []; 403 val new_prints = visible_prints @ retained_prints; 404 in 405 if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints 406 end; 407 408fun parallel_print (Print {pri, ...}) = 409 pri <= 0 orelse (Future.enabled () andalso Options.default_bool "parallel_print"); 410 411fun print_function name f = 412 Synchronized.change print_functions (fn funs => 413 (if name = "" then error "Unnamed print function" else (); 414 if not (AList.defined (op =) funs name) then () 415 else warning ("Redefining command print function: " ^ quote name); 416 AList.update (op =) (name, f) funs)); 417 418fun no_print_function name = 419 Synchronized.change print_functions (filter_out (equal name o #1)); 420 421end; 422 423val _ = 424 print_function "Execution.print" 425 (fn {args, exec_id, ...} => 426 if null args then 427 SOME {delay = NONE, pri = Task_Queue.urgent_pri + 2, persistent = false, strict = false, 428 print_fn = fn _ => fn _ => Execution.fork_prints exec_id} 429 else NONE); 430 431val _ = 432 print_function "print_state" 433 (fn {keywords, command_name, ...} => 434 if Options.default_bool "editor_output_state" andalso Keyword.is_printed keywords command_name 435 then 436 SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false, 437 print_fn = fn _ => fn st => 438 if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st) 439 else ()} 440 else NONE); 441 442 443(* combined execution *) 444 445type exec = eval * print list; 446 447fun init_exec opt_thy : exec = 448 (Eval 449 {command_id = Document_ID.none, exec_id = Document_ID.none, 450 eval_process = Lazy.value (init_eval_state opt_thy)}, []); 451 452val no_exec = init_exec NONE; 453 454fun exec_ids NONE = [] 455 | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints; 456 457local 458 459fun run_process execution_id exec_id process = 460 let val group = Future.worker_subgroup () in 461 if Execution.running execution_id exec_id [group] then 462 ignore (task_context group (fn () => Lazy.force_result {strict = true} process) ()) 463 else () 464 end; 465 466fun ignore_process process = 467 Lazy.is_running process orelse Lazy.is_finished process; 468 469fun run_eval execution_id (Eval {exec_id, eval_process, ...}) = 470 if Lazy.is_finished eval_process then () 471 else run_process execution_id exec_id eval_process; 472 473fun fork_print execution_id deps (Print {name, delay, pri, exec_id, print_process, ...}) = 474 let 475 val group = Future.worker_subgroup (); 476 fun fork () = 477 ignore ((singleton o Future.forks) 478 {name = name, group = SOME group, deps = deps, pri = pri, interrupts = true} 479 (fn () => 480 if ignore_process print_process then () 481 else run_process execution_id exec_id print_process)); 482 in 483 (case delay of 484 NONE => fork () 485 | SOME d => ignore (Event_Timer.request {physical = true} (Time.now () + d) fork)) 486 end; 487 488fun run_print execution_id (print as Print {exec_id, print_process, ...}) = 489 if ignore_process print_process then () 490 else if parallel_print print then fork_print execution_id [] print 491 else run_process execution_id exec_id print_process; 492 493in 494 495fun exec execution_id (eval, prints) = 496 (run_eval execution_id eval; List.app (run_print execution_id) prints); 497 498fun exec_parallel_prints execution_id deps (exec as (Eval {eval_process, ...}, prints)) = 499 if Lazy.is_finished eval_process 500 then (List.app (fork_print execution_id deps) prints; NONE) 501 else SOME exec; 502 503end; 504 505end; 506