src/Pure/PIDE/command.ML
author wenzelm
Thu Jul 04 23:51:47 2013 +0200 (2013-07-04 ago)
changeset 52527 dbac84eab3bc
parent 52526 d234cb6b60e3
child 52530 99dd8b4ef3fe
permissions -rw-r--r--
separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;
     1 (*  Title:      Pure/PIDE/command.ML
     2     Author:     Makarius
     3 
     4 Prover command execution.
     5 *)
     6 
     7 signature COMMAND =
     8 sig
     9   type span = Token.T list
    10   val range: span -> Position.range
    11   val proper_range: span -> Position.range
    12   type 'a memo
    13   val memo: (unit -> 'a) -> 'a memo
    14   val memo_value: 'a -> 'a memo
    15   val memo_eval: 'a memo -> 'a
    16   val memo_fork: Future.params -> 'a memo -> unit
    17   val memo_result: 'a memo -> 'a
    18   val memo_stable: 'a memo -> bool
    19   val read: span -> Toplevel.transition
    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, exec_id: int, print: unit memo}
    27   val print: (unit -> int) -> string -> eval -> print list
    28   val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    29 end;
    30 
    31 structure Command: COMMAND =
    32 struct
    33 
    34 (* source *)
    35 
    36 type span = Token.T list;
    37 
    38 val range = Token.position_range_of;
    39 val proper_range = Token.position_range_of o #1 o take_suffix Token.is_improper;
    40 
    41 
    42 (* memo results *)
    43 
    44 datatype 'a expr =
    45   Expr of unit -> 'a |
    46   Result of 'a Exn.result;
    47 
    48 abstype 'a memo = Memo of 'a expr Synchronized.var
    49 with
    50 
    51 fun memo e = Memo (Synchronized.var "Command.memo" (Expr e));
    52 fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));
    53 
    54 fun memo_eval (Memo v) =
    55   (case Synchronized.value v of
    56     Result res => res
    57   | _ =>
    58       Synchronized.guarded_access v
    59         (fn Result res => SOME (res, Result res)
    60           | Expr e =>
    61               let val res = Exn.capture e ();  (*memoing of physical interrupts!*)
    62               in SOME (res, Result res) end))
    63   |> Exn.release;
    64 
    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 
    70 fun memo_result (Memo v) =
    71   (case Synchronized.value v of
    72     Result res => Exn.release res
    73   | _ => raise Fail "Unfinished memo result");
    74 
    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 
    80 end;
    81 
    82 
    83 (* read *)
    84 
    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;
    89 
    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);
    95 
    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;
   110 
   111 
   112 (* eval *)
   113 
   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 
   122 local
   123 
   124 fun run int tr st =
   125   if Goal.future_enabled () andalso Keyword.is_diag (Toplevel.name_of tr) then
   126     (Goal.fork_params {name = "Toplevel.diag", pos = Toplevel.pos_of tr, pri = ~1}
   127       (fn () => Toplevel.command_exception int tr st); ([], SOME st))
   128   else Toplevel.command_errors int tr st;
   129 
   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 
   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 
   144 fun eval span tr ({malformed, state = st, ...}: eval_state) =
   145   if malformed then
   146     {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
   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);
   152 
   153       val _ = Multithreading.interrupted ();
   154       val _ = Toplevel.status tr Markup.running;
   155       val (errs1, result) = run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   156       val errs2 = (case result of NONE => [] | SOME st' => check_cmts span tr st');
   157       val errs = errs1 @ errs2;
   158       val _ = Toplevel.status tr Markup.finished;
   159       val _ = List.app (Future.error_msg (Toplevel.pos_of tr)) errs;
   160     in
   161       (case result of
   162         NONE =>
   163           let
   164             val _ = if null errs then Exn.interrupt () else ();
   165             val _ = Toplevel.status tr Markup.failed;
   166           in {failed = true, malformed = malformed', command = tr, state = st} end
   167       | SOME st' =>
   168           let
   169             val _ = proof_status tr st';
   170           in {failed = false, malformed = malformed', command = tr, state = st'} end)
   171     end;
   172 
   173 end;
   174 
   175 
   176 (* print *)
   177 
   178 type print = {name: string, pri: int, exec_id: int, print: unit memo};
   179 type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   180 
   181 local
   182 
   183 type print_function = string * (int * (string -> print_fn option));
   184 val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
   185 
   186 fun output_error tr exn =
   187   List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   188 
   189 fun print_error tr f x =
   190   (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) f x
   191     handle exn => output_error tr exn;
   192 
   193 in
   194 
   195 fun print new_id 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
   198       Exn.Res NONE => NONE
   199     | Exn.Res (SOME print_fn) =>
   200         let
   201           val exec_id = new_id ();
   202           fun body () =
   203             let
   204               val {failed, command, state = st', ...} = memo_result eval;
   205               val tr = Toplevel.put_id exec_id command;
   206             in if failed then () else print_error tr (fn () => print_fn tr st') () end;
   207         in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end
   208     | Exn.Exn exn =>
   209         let
   210           val exec_id = new_id ();
   211           fun body () =
   212             let
   213               val {command, ...} = memo_result eval;
   214               val tr = Toplevel.put_id exec_id command;
   215             in output_error tr exn end;
   216         in SOME {name = name, pri = pri, exec_id = exec_id, print = memo body} end));
   217 
   218 fun print_function {name, pri} f =
   219   Synchronized.change print_functions (fn funs =>
   220    (if not (AList.defined (op =) funs name) then ()
   221     else warning ("Redefining command print function: " ^ quote name);
   222     AList.update (op =) (name, (pri, f)) funs));
   223 
   224 end;
   225 
   226 val _ =
   227   print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
   228     let
   229       val is_init = Keyword.is_theory_begin command_name;
   230       val is_proof = Keyword.is_proof command_name;
   231       val do_print =
   232         not is_init andalso
   233           (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   234     in if do_print then Toplevel.print_state false st' else () end));
   235 
   236 end;
   237