src/Pure/PIDE/command.ML
author wenzelm
Wed Dec 03 14:04:38 2014 +0100 (2014-12-03 ago)
changeset 59083 88b0b1f28adc
parent 59058 a78612c67ec0
child 59123 e68e44836d04
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/PIDE/command.ML
     2     Author:     Makarius
     3 
     4 Prover command execution: read -- eval -- print.
     5 *)
     6 
     7 signature COMMAND =
     8 sig
     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 -> Token.T list -> Toplevel.transition
    14   type eval
    15   val eval_eq: eval * eval -> bool
    16   val eval_running: eval -> bool
    17   val eval_finished: eval -> bool
    18   val eval_result_state: eval -> Toplevel.state
    19   val eval: Keyword.keywords -> Path.T -> (unit -> theory) ->
    20     blob list -> Token.T list -> eval -> eval
    21   type print
    22   val print: bool -> (string * string list) list -> Keyword.keywords -> string ->
    23     eval -> print list -> print list option
    24   type print_fn = Toplevel.transition -> Toplevel.state -> unit
    25   type print_function =
    26     {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
    27       {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option
    28   val print_function: string -> print_function -> unit
    29   val no_print_function: string -> unit
    30   type exec = eval * print list
    31   val no_exec: exec
    32   val exec_ids: exec option -> Document_ID.exec list
    33   val exec: Document_ID.execution -> exec -> unit
    34 end;
    35 
    36 structure Command: COMMAND =
    37 struct
    38 
    39 (** memo results **)
    40 
    41 datatype 'a expr =
    42   Expr of Document_ID.exec * (unit -> 'a) |
    43   Result of 'a Exn.result;
    44 
    45 abstype 'a memo = Memo of 'a expr Synchronized.var
    46 with
    47 
    48 fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
    49 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    50 
    51 fun memo_result (Memo v) =
    52   (case Synchronized.value v of
    53     Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
    54   | Result res => Exn.release res);
    55 
    56 fun memo_finished (Memo v) =
    57   (case Synchronized.value v of Expr _ => false | Result _ => true);
    58 
    59 fun memo_exec execution_id (Memo v) =
    60   Synchronized.timed_access v (K (SOME Time.zeroTime))
    61     (fn expr =>
    62       (case expr of
    63         Expr (exec_id, body) =>
    64           uninterruptible (fn restore_attributes => fn () =>
    65             let val group = Future.worker_subgroup () in
    66               if Execution.running execution_id exec_id [group] then
    67                 let
    68                   val res =
    69                     (body
    70                       |> restore_attributes
    71                       |> Future.task_context "Command.memo_exec" group
    72                       |> Exn.interruptible_capture) ();
    73                 in SOME ((), Result res) end
    74               else SOME ((), expr)
    75             end) ()
    76       | Result _ => SOME ((), expr)))
    77   |> (fn NONE => error "Conflicting command execution" | _ => ());
    78 
    79 fun memo_fork params execution_id (Memo v) =
    80   (case Synchronized.value v of
    81     Result _ => ()
    82   | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));
    83 
    84 end;
    85 
    86 
    87 
    88 (** main phases of execution **)
    89 
    90 (* read *)
    91 
    92 type blob =
    93   (string * (SHA1.digest * string list) option) Exn.result;  (*file node name, digest, lines*)
    94 
    95 fun read_file_node file_node master_dir pos src_path =
    96   let
    97     val _ = Position.report pos Markup.language_path;
    98     val _ =
    99       (case try Url.explode file_node of
   100         NONE => ()
   101       | SOME (Url.File _) => ()
   102       | _ =>
   103          (Position.report pos (Markup.path file_node);
   104           error ("Prover cannot load remote file " ^
   105             Markup.markup (Markup.path file_node) (quote file_node) ^ Position.here pos)));
   106     val full_path = File.check_file (File.full_path master_dir src_path);
   107     val _ = Position.report pos (Markup.path (Path.implode full_path));
   108     val text = File.read full_path;
   109     val lines = split_lines text;
   110     val digest = SHA1.digest text;
   111   in {src_path = src_path, lines = lines, digest = digest, pos = Path.position full_path} end;
   112 
   113 val read_file = read_file_node "";
   114 
   115 local
   116 
   117 fun blob_file src_path lines digest file_node =
   118   let
   119     val file_pos =
   120       Position.file file_node |>
   121       (case Position.get_id (Position.thread_data ()) of
   122         NONE => I
   123       | SOME exec_id => Position.put_id exec_id);
   124   in {src_path = src_path, lines = lines, digest = digest, pos = file_pos} end
   125 
   126 fun resolve_files keywords master_dir blobs toks =
   127   (case Outer_Syntax.parse_spans toks of
   128     [span] => span
   129       |> Command_Span.resolve_files keywords (fn cmd => fn (path, pos) =>
   130         let
   131           fun make_file src_path (Exn.Res (file_node, NONE)) =
   132                 Exn.interruptible_capture (fn () =>
   133                   read_file_node file_node master_dir pos src_path) ()
   134             | make_file src_path (Exn.Res (file_node, SOME (digest, lines))) =
   135                (Position.reports [(pos, Markup.language_path), (pos, Markup.path file_node)];
   136                 Exn.Res (blob_file src_path lines digest file_node))
   137             | make_file _ (Exn.Exn e) = Exn.Exn e;
   138           val src_paths = Keyword.command_files keywords cmd path;
   139         in
   140           if null blobs then
   141             map2 make_file src_paths (map (K (Exn.Res ("", NONE))) src_paths)
   142           else if length src_paths = length blobs then
   143             map2 make_file src_paths blobs
   144           else error ("Misalignment of inlined files" ^ Position.here pos)
   145         end)
   146       |> Command_Span.content
   147   | _ => toks);
   148 
   149 val bootstrap_thy = ML_Context.the_global_context ();
   150 
   151 in
   152 
   153 fun read_thy st = Toplevel.theory_of st handle Toplevel.UNDEF => bootstrap_thy;
   154 
   155 fun read keywords thy master_dir init blobs span =
   156   let
   157     val command_reports = Outer_Syntax.command_reports thy;
   158 
   159     val proper_range = Token.range_of (#1 (take_suffix Token.is_improper span));
   160     val pos =
   161       (case find_first Token.is_command span of
   162         SOME tok => Token.pos_of tok
   163       | NONE => #1 proper_range);
   164 
   165     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
   166     val _ = Position.reports_text (token_reports @ maps command_reports span);
   167   in
   168     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
   169     else
   170       (case Outer_Syntax.parse_tokens thy (resolve_files keywords master_dir blobs span) of
   171         [tr] => Toplevel.modify_init init tr
   172       | [] => Toplevel.ignored (#1 (Token.range_of span))
   173       | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
   174       handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
   175   end;
   176 
   177 end;
   178 
   179 
   180 (* eval *)
   181 
   182 type eval_state =
   183   {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
   184 val init_eval_state =
   185   {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
   186 
   187 datatype eval = Eval of {exec_id: Document_ID.exec, eval_process: eval_state memo};
   188 
   189 fun eval_exec_id (Eval {exec_id, ...}) = exec_id;
   190 val eval_eq = op = o apply2 eval_exec_id;
   191 
   192 val eval_running = Execution.is_running_exec o eval_exec_id;
   193 fun eval_finished (Eval {eval_process, ...}) = memo_finished eval_process;
   194 
   195 fun eval_result (Eval {eval_process, ...}) = memo_result eval_process;
   196 val eval_result_state = #state o eval_result;
   197 
   198 local
   199 
   200 fun reset_state keywords tr st0 = Toplevel.setmp_thread_position tr (fn () =>
   201   let
   202     val name = Toplevel.name_of tr;
   203     val res =
   204       if Keyword.is_theory_body keywords name then Toplevel.reset_theory st0
   205       else if Keyword.is_proof keywords name then Toplevel.reset_proof st0
   206       else NONE;
   207   in
   208     (case res of
   209       NONE => st0
   210     | SOME st => (Output.error_message (Toplevel.type_error tr st0 ^ " -- using reset state"); st))
   211   end) ();
   212 
   213 fun run keywords int tr st =
   214   if Goal.future_enabled 1 andalso Keyword.is_diag keywords (Toplevel.name_of tr) then
   215     (Execution.fork {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   216       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   217   else Toplevel.command_errors int tr st;
   218 
   219 fun check_cmts span tr st' =
   220   Toplevel.setmp_thread_position tr
   221     (fn () =>
   222       Outer_Syntax.side_comments span |> maps (fn cmt =>
   223         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
   224           handle exn =>
   225             if Exn.is_interrupt exn then reraise exn
   226             else Runtime.exn_messages_ids exn)) ();
   227 
   228 fun report tr m =
   229   Toplevel.setmp_thread_position tr (fn () => Output.report [Markup.markup_only m]) ();
   230 
   231 fun status tr m =
   232   Toplevel.setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) ();
   233 
   234 fun proof_status tr st =
   235   (case try Toplevel.proof_of st of
   236     SOME prf => status tr (Proof.status_markup prf)
   237   | NONE => ());
   238 
   239 fun eval_state keywords span tr ({malformed, state, ...}: eval_state) =
   240   if malformed then
   241     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   242   else
   243     let
   244       val _ = Multithreading.interrupted ();
   245 
   246       val malformed' = Toplevel.is_malformed tr;
   247       val st = reset_state keywords tr state;
   248 
   249       val _ = status tr Markup.running;
   250       val (errs1, result) = run keywords true tr st;
   251       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   252       val errs = errs1 @ errs2;
   253       val _ = List.app (Future.error_message (Toplevel.pos_of tr)) errs;
   254     in
   255       (case result of
   256         NONE =>
   257           let
   258             val _ = status tr Markup.failed;
   259             val _ = status tr Markup.finished;
   260             val _ = if null errs then (report tr Markup.bad; Exn.interrupt ()) else ();
   261           in {failed = true, malformed = malformed', command = tr, state = st} end
   262       | SOME st' =>
   263           let
   264             val _ = proof_status tr st';
   265             val _ = status tr Markup.finished;
   266           in {failed = false, malformed = malformed', command = tr, state = st'} end)
   267     end;
   268 
   269 in
   270 
   271 fun eval keywords master_dir init blobs span eval0 =
   272   let
   273     val exec_id = Document_ID.make ();
   274     fun process () =
   275       let
   276         val eval_state0 = eval_result eval0;
   277         val thy = read_thy (#state eval_state0);
   278         val tr =
   279           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   280             (fn () => read keywords thy master_dir init blobs span |> Toplevel.exec_id exec_id) ();
   281       in eval_state keywords span tr eval_state0 end;
   282   in Eval {exec_id = exec_id, eval_process = memo exec_id process} end;
   283 
   284 end;
   285 
   286 
   287 (* print *)
   288 
   289 datatype print = Print of
   290  {name: string, args: string list, delay: Time.time option, pri: int, persistent: bool,
   291   exec_id: Document_ID.exec, print_process: unit memo};
   292 
   293 fun print_exec_id (Print {exec_id, ...}) = exec_id;
   294 val print_eq = op = o apply2 print_exec_id;
   295 
   296 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   297 
   298 type print_function =
   299   {keywords: Keyword.keywords, command_name: string, args: string list, exec_id: Document_ID.exec} ->
   300     {delay: Time.time option, pri: int, persistent: bool, strict: bool, print_fn: print_fn} option;
   301 
   302 local
   303 
   304 val print_functions =
   305   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
   306 
   307 fun print_error tr opt_context e =
   308   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution opt_context) e ()
   309     handle exn =>
   310       if Exn.is_interrupt exn then reraise exn
   311       else List.app (Future.error_message (Toplevel.pos_of tr)) (Runtime.exn_messages_ids exn);
   312 
   313 fun print_finished (Print {print_process, ...}) = memo_finished print_process;
   314 
   315 fun print_persistent (Print {persistent, ...}) = persistent;
   316 
   317 val overlay_ord = prod_ord string_ord (list_ord string_ord);
   318 
   319 in
   320 
   321 fun print command_visible command_overlays keywords command_name eval old_prints =
   322   let
   323     val print_functions = Synchronized.value print_functions;
   324 
   325     fun make_print name args {delay, pri, persistent, strict, print_fn} =
   326       let
   327         val exec_id = Document_ID.make ();
   328         fun process () =
   329           let
   330             val {failed, command, state = st', ...} = eval_result eval;
   331             val tr = Toplevel.exec_id exec_id command;
   332             val opt_context = try Toplevel.generic_theory_of st';
   333           in
   334             if failed andalso strict then ()
   335             else print_error tr opt_context (fn () => print_fn tr st')
   336           end;
   337       in
   338         Print {
   339           name = name, args = args, delay = delay, pri = pri, persistent = persistent,
   340           exec_id = exec_id, print_process = memo exec_id process}
   341       end;
   342 
   343     fun bad_print name args exn =
   344       make_print name args {delay = NONE, pri = 0, persistent = false,
   345         strict = false, print_fn = fn _ => fn _ => reraise exn};
   346 
   347     fun new_print name args get_pr =
   348       let
   349         val params =
   350          {keywords = keywords,
   351           command_name = command_name,
   352           args = args,
   353           exec_id = eval_exec_id eval};
   354       in
   355         (case Exn.capture (Runtime.controlled_execution NONE get_pr) params of
   356           Exn.Res NONE => NONE
   357         | Exn.Res (SOME pr) => SOME (make_print name args pr)
   358         | Exn.Exn exn => SOME (bad_print name args exn))
   359       end;
   360 
   361     fun get_print (a, b) =
   362       (case find_first (fn Print {name, args, ...} => name = a andalso args = b) old_prints of
   363         NONE =>
   364           (case AList.lookup (op =) print_functions a of
   365             NONE => SOME (bad_print a b (ERROR ("Missing print function " ^ quote a)))
   366           | SOME get_pr => new_print a b get_pr)
   367       | some => some);
   368 
   369     val new_prints =
   370       if command_visible then
   371         fold (fn (a, _) => cons (a, [])) print_functions command_overlays
   372         |> sort_distinct overlay_ord
   373         |> map_filter get_print
   374       else filter (fn print => print_finished print andalso print_persistent print) old_prints;
   375   in
   376     if eq_list print_eq (old_prints, new_prints) then NONE else SOME new_prints
   377   end;
   378 
   379 fun print_function name f =
   380   Synchronized.change print_functions (fn funs =>
   381    (if not (AList.defined (op =) funs name) then ()
   382     else warning ("Redefining command print function: " ^ quote name);
   383     AList.update (op =) (name, f) funs));
   384 
   385 fun no_print_function name =
   386   Synchronized.change print_functions (filter_out (equal name o #1));
   387 
   388 end;
   389 
   390 val _ =
   391   print_function "Execution.print"
   392     (fn {args, exec_id, ...} =>
   393       if null args then
   394         SOME {delay = NONE, pri = 1, persistent = false, strict = false,
   395           print_fn = fn _ => fn _ => Execution.fork_prints exec_id}
   396       else NONE);
   397 
   398 val _ =
   399   print_function "print_state"
   400     (fn {keywords, command_name, ...} =>
   401       if Keyword.is_printed keywords command_name then
   402         SOME {delay = NONE, pri = 1, persistent = false, strict = true,
   403           print_fn = fn _ => fn st => if Toplevel.is_proof st then Toplevel.print_state st else ()}
   404       else NONE);
   405 
   406 
   407 (* combined execution *)
   408 
   409 type exec = eval * print list;
   410 val no_exec: exec =
   411   (Eval {exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
   412 
   413 fun exec_ids NONE = []
   414   | exec_ids (SOME (eval, prints)) = eval_exec_id eval :: map print_exec_id prints;
   415 
   416 local
   417 
   418 fun run_print execution_id (Print {name, delay, pri, print_process, ...}) =
   419   if pri <= 0 orelse (Multithreading.enabled () andalso Options.default_bool "parallel_print")
   420   then
   421     let
   422       val group = Future.worker_subgroup ();
   423       fun fork () =
   424         memo_fork {name = name, group = SOME group, deps = [], pri = pri, interrupts = true}
   425           execution_id print_process;
   426     in
   427       (case delay of
   428         NONE => fork ()
   429       | SOME d => ignore (Event_Timer.request (Time.+ (Time.now (), d)) fork))
   430     end
   431   else memo_exec execution_id print_process;
   432 
   433 in
   434 
   435 fun exec execution_id (Eval {eval_process, ...}, prints) =
   436   (memo_exec execution_id eval_process; List.app (run_print execution_id) prints);
   437 
   438 end;
   439 
   440 end;
   441