src/Pure/PIDE/command.ML
author wenzelm
Fri Jul 05 22:58:24 2013 +0200 (2013-07-05 ago)
changeset 52536 3a35ce87a55c
parent 52535 b7badd371e4d
child 52559 ddaf277e0d8c
permissions -rw-r--r--
tuned signature;
tuned comments;
     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 eval_process
    10   type eval = {exec_id: Document_ID.exec, eval_process: eval_process}
    11   val eval_result_state: eval -> Toplevel.state
    12   type print_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 no_exec: exec
    16   val exec_ids: exec -> Document_ID.exec list
    17   val read: (unit -> theory) -> Token.T list -> Toplevel.transition
    18   val eval: (unit -> theory) -> Token.T list -> 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
    22   val execute: exec -> unit
    23   val stable_eval: eval -> bool
    24   val stable_print: print -> bool
    25 end;
    26 
    27 structure Command: COMMAND =
    28 struct
    29 
    30 (** memo results -- including physical interrupts! **)
    31 
    32 datatype 'a expr =
    33   Expr of unit -> 'a |
    34   Result of 'a Exn.result;
    35 
    36 abstype 'a memo = Memo of 'a expr Synchronized.var
    37 with
    38 
    39 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    40 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    41 
    42 fun memo_eval (Memo v) =
    43   (case Synchronized.value v of
    44     Result res => res
    45   | _ =>
    46       Synchronized.guarded_access v
    47         (fn Result res => SOME (res, Result res)
    48           | Expr e =>
    49               let val res = Exn.capture e ();  (*sic!*)
    50               in SOME (res, Result res) end))
    51   |> Exn.release;
    52 
    53 fun memo_fork params (Memo v) =
    54   (case Synchronized.value v of
    55     Result _ => ()
    56   | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
    57 
    58 fun memo_result (Memo v) =
    59   (case Synchronized.value v of
    60     Result res => Exn.release res
    61   | _ => raise Fail "Unfinished memo result");
    62 
    63 fun memo_stable (Memo v) =
    64   (case Synchronized.value v of
    65     Expr _ => true
    66   | Result res => not (Exn.is_interrupt_exn res));
    67 
    68 end;
    69 
    70 
    71 
    72 (** main phases of execution **)
    73 
    74 (* basic type definitions *)
    75 
    76 type eval_state =
    77   {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    78 val init_eval_state =
    79   {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    80 
    81 type eval_process = eval_state memo;
    82 type eval = {exec_id: Document_ID.exec, eval_process: eval_process};
    83 
    84 fun eval_result ({eval_process, ...}: eval) = memo_result eval_process;
    85 val eval_result_state = #state o eval_result;
    86 
    87 type print_process = unit memo;
    88 type print = {name: string, pri: int, exec_id: Document_ID.exec, print_process: print_process};
    89 
    90 type exec = eval * print list;
    91 val no_exec: exec = ({exec_id = Document_ID.none, eval_process = memo_value init_eval_state}, []);
    92 
    93 fun exec_ids (({exec_id, ...}, prints): exec) = exec_id :: map #exec_id prints;
    94 
    95 
    96 (* read *)
    97 
    98 fun read init span =
    99   let
   100     val outer_syntax = #2 (Outer_Syntax.get_syntax ());
   101     val command_reports = Outer_Syntax.command_reports outer_syntax;
   102 
   103     val proper_range =
   104       Position.set_range (Token.position_range_of (#1 (take_suffix Token.is_improper span)));
   105     val pos =
   106       (case find_first Token.is_command span of
   107         SOME tok => Token.position_of tok
   108       | NONE => proper_range);
   109 
   110     val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens span;
   111     val _ = Position.reports_text (token_reports @ maps command_reports span);
   112   in
   113     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
   114     else
   115       (case Outer_Syntax.read_spans outer_syntax span of
   116         [tr] =>
   117           if Keyword.is_control (Toplevel.name_of tr) then
   118             Toplevel.malformed pos "Illegal control command"
   119           else Toplevel.modify_init init tr
   120       | [] => Toplevel.ignored (Position.set_range (Token.position_range_of span))
   121       | _ => Toplevel.malformed proper_range "Exactly one command expected")
   122       handle ERROR msg => Toplevel.malformed proper_range msg
   123   end;
   124 
   125 
   126 (* eval *)
   127 
   128 local
   129 
   130 fun run int tr st =
   131   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
   132     (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   133       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   134   else Toplevel.command_errors int tr st;
   135 
   136 fun check_cmts span tr st' =
   137   Toplevel.setmp_thread_position tr
   138     (fn () =>
   139       Outer_Syntax.side_comments span |> maps (fn cmt =>
   140         (Thy_Output.check_text (Token.source_position_of cmt) st'; [])
   141           handle exn => ML_Compiler.exn_messages_ids exn)) ();
   142 
   143 fun proof_status tr st =
   144   (case try Toplevel.proof_of st of
   145     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   146   | NONE => ());
   147 
   148 fun eval_state span tr ({malformed, state = st, ...}: eval_state) =
   149   if malformed then
   150     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   151   else
   152     let
   153       val malformed' = Toplevel.is_malformed tr;
   154       val is_init = Toplevel.is_init tr;
   155       val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   156 
   157       val _ = Multithreading.interrupted ();
   158       val _ = Toplevel.status tr Markup.running;
   159       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   160       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   161       val errs = errs1 @ errs2;
   162       val _ = Toplevel.status tr Markup.finished;
   163       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   164     in
   165       (case result of
   166         NONE =>
   167           let
   168             val _ = if null errs then Exn.interrupt () else ();
   169             val _ = Toplevel.status tr Markup.failed;
   170           in {failed = true, malformed = malformed', command = tr, state = st} end
   171       | SOME st' =>
   172           let
   173             val _ = proof_status tr st';
   174           in {failed = false, malformed = malformed', command = tr, state = st'} end)
   175     end;
   176 
   177 in
   178 
   179 fun eval init span eval0 =
   180   let
   181     val exec_id = Document_ID.make ();
   182     fun process () =
   183       let
   184         val tr =
   185           Position.setmp_thread_data (Position.id_only (Document_ID.print exec_id))
   186             (fn () => read init span |> Toplevel.exec_id exec_id) ();
   187       in eval_state span tr (eval_result eval0) end;
   188   in {exec_id = exec_id, eval_process = memo process} end;
   189 
   190 end;
   191 
   192 
   193 (* print *)
   194 
   195 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   196 
   197 local
   198 
   199 type print_function = string * (int * (string -> print_fn option));
   200 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
   201 
   202 fun output_error tr exn =
   203   List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   204 
   205 fun print_error tr f x =
   206   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
   207     handle exn => output_error tr exn;
   208 
   209 in
   210 
   211 fun print command_name eval =
   212   rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
   213     (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
   214       Exn.Res NONE => NONE
   215     | Exn.Res (SOME print_fn) =>
   216         let
   217           val exec_id = Document_ID.make ();
   218           fun process () =
   219             let
   220               val {failed, command, state = st', ...} = eval_result eval;
   221               val tr = Toplevel.exec_id exec_id command;
   222             in if failed then () else print_error tr (fn () => print_fn tr st') () end;
   223         in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end
   224     | Exn.Exn exn =>
   225         let
   226           val exec_id = Document_ID.make ();
   227           fun process () =
   228             let
   229               val {command, ...} = eval_result eval;
   230               val tr = Toplevel.exec_id exec_id command;
   231             in output_error tr exn end;
   232         in SOME {name = name, pri = pri, exec_id = exec_id, print_process = memo process} end));
   233 
   234 fun print_function {name, pri} f =
   235   Synchronized.change print_functions (fn funs =>
   236    (if not (AList.defined (op =) funs name) then ()
   237     else warning ("Redefining command print function: " ^ quote name);
   238     AList.update (op =) (name, (pri, f)) funs));
   239 
   240 end;
   241 
   242 val _ =
   243   print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
   244     let
   245       val is_init = Keyword.is_theory_begin command_name;
   246       val is_proof = Keyword.is_proof command_name;
   247       val do_print =
   248         not is_init andalso
   249           (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   250     in if do_print then Toplevel.print_state false st' else () end));
   251 
   252 
   253 (* overall execution process *)
   254 
   255 fun execute (({eval_process, ...}, prints): exec) =
   256  (memo_eval eval_process;
   257   prints |> List.app (fn {name, pri, print_process, ...} =>
   258     memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print_process));
   259 
   260 fun stable_goals exec_id =
   261   not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id)));
   262 
   263 fun stable_eval ({exec_id, eval_process}: eval) =
   264   stable_goals exec_id andalso memo_stable eval_process;
   265 
   266 fun stable_print ({exec_id, print_process, ...}: print) =
   267   stable_goals exec_id andalso memo_stable print_process;
   268 
   269 end;
   270