more Command.memo operations;
authorwenzelm
Thu Jul 04 16:04:53 2013 +0200 (2013-07-04)
changeset 52526d234cb6b60e3
parent 52524 bc6e0144726a
child 52527 dbac84eab3bc
more Command.memo operations;
more explicit types Command.eval vs. Command.print vs. Document.exec;
clarified print function parameters;
src/Pure/PIDE/command.ML
src/Pure/PIDE/document.ML
     1.1 --- a/src/Pure/PIDE/command.ML	Thu Jul 04 12:02:11 2013 +0200
     1.2 +++ b/src/Pure/PIDE/command.ML	Thu Jul 04 16:04:53 2013 +0200
     1.3 @@ -13,16 +13,19 @@
     1.4    val memo: (unit -> 'a) -> 'a memo
     1.5    val memo_value: 'a -> 'a memo
     1.6    val memo_eval: 'a memo -> 'a
     1.7 +  val memo_fork: Future.params -> 'a memo -> unit
     1.8    val memo_result: 'a memo -> 'a
     1.9 +  val memo_stable: 'a memo -> bool
    1.10    val read: span -> Toplevel.transition
    1.11 -  val eval: span -> Toplevel.transition ->
    1.12 -    Toplevel.state * {malformed: bool} -> {failed: bool} * (Toplevel.state * {malformed: bool})
    1.13 -  type print = {name: string, pri: int, pr: unit lazy}
    1.14 -  val print: Toplevel.state -> Toplevel.transition -> Toplevel.state -> print list
    1.15 -  type print_function =
    1.16 -    {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
    1.17 -      (unit -> unit) option
    1.18 -  val print_function: string -> int -> print_function -> unit
    1.19 +  type eval_state =
    1.20 +    {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state}
    1.21 +  type eval = eval_state memo
    1.22 +  val no_eval: eval
    1.23 +  val eval: span -> Toplevel.transition -> eval_state -> eval_state
    1.24 +  type print_fn = Toplevel.transition -> Toplevel.state -> unit
    1.25 +  type print = {name: string, pri: int, print: unit memo}
    1.26 +  val print: string -> eval -> print list
    1.27 +  val print_function: {name: string, pri: int} -> (string -> print_fn option) -> unit
    1.28  end;
    1.29  
    1.30  structure Command: COMMAND =
    1.31 @@ -59,11 +62,21 @@
    1.32                in SOME (res, Result res) end))
    1.33    |> Exn.release;
    1.34  
    1.35 +fun memo_fork params (Memo v) =
    1.36 +  (case Synchronized.value v of
    1.37 +    Result _ => ()
    1.38 +  | _ => ignore ((singleton o Future.forks) params (fn () => memo_eval (Memo v))));
    1.39 +
    1.40  fun memo_result (Memo v) =
    1.41    (case Synchronized.value v of
    1.42      Result res => Exn.release res
    1.43    | _ => raise Fail "Unfinished memo result");
    1.44  
    1.45 +fun memo_stable (Memo v) =
    1.46 +  (case Synchronized.value v of
    1.47 +    Expr _ => true
    1.48 +  | Result res => not (Exn.is_interrupt_exn res));
    1.49 +
    1.50  end;
    1.51  
    1.52  
    1.53 @@ -98,6 +111,14 @@
    1.54  
    1.55  (* eval *)
    1.56  
    1.57 +type eval_state =
    1.58 +  {failed: bool, malformed: bool, command: Toplevel.transition, state: Toplevel.state};
    1.59 +val no_eval_state: eval_state =
    1.60 +  {failed = false, malformed = false, command = Toplevel.empty, state = Toplevel.toplevel};
    1.61 +
    1.62 +type eval = eval_state memo;
    1.63 +val no_eval = memo_value no_eval_state;
    1.64 +
    1.65  local
    1.66  
    1.67  fun run int tr st =
    1.68 @@ -120,9 +141,9 @@
    1.69  
    1.70  in
    1.71  
    1.72 -fun eval span tr (st, {malformed}) =
    1.73 +fun eval span tr ({malformed, state = st, ...}: eval_state) =
    1.74    if malformed then
    1.75 -    ({failed = true}, (Toplevel.toplevel, {malformed = malformed}))
    1.76 +    {failed = true, malformed = malformed, command = tr, state = Toplevel.toplevel}
    1.77    else
    1.78      let
    1.79        val malformed' = Toplevel.is_malformed tr;
    1.80 @@ -142,11 +163,11 @@
    1.81            let
    1.82              val _ = if null errs then Exn.interrupt () else ();
    1.83              val _ = Toplevel.status tr Markup.failed;
    1.84 -          in ({failed = true}, (st, {malformed = malformed'})) end
    1.85 +          in {failed = true, malformed = malformed', command = tr, state = st} end
    1.86        | SOME st' =>
    1.87            let
    1.88              val _ = proof_status tr st';
    1.89 -          in ({failed = false}, (st', {malformed = malformed'})) end)
    1.90 +          in {failed = false, malformed = malformed', command = tr, state = st'} end)
    1.91      end;
    1.92  
    1.93  end;
    1.94 @@ -154,16 +175,13 @@
    1.95  
    1.96  (* print *)
    1.97  
    1.98 -type print_function =
    1.99 -  {old_state: Toplevel.state, tr: Toplevel.transition, state: Toplevel.state} ->
   1.100 -    (unit -> unit) option;
   1.101 -
   1.102 -type print = {name: string, pri: int, pr: unit lazy};
   1.103 +type print = {name: string, pri: int, print: unit memo};
   1.104 +type print_fn = Toplevel.transition -> Toplevel.state -> unit;
   1.105  
   1.106  local
   1.107  
   1.108 -val print_functions =
   1.109 -  Synchronized.var "Command.print_functions" ([]: (string * (int * print_function)) list);
   1.110 +type print_function = string * (int * (string -> print_fn option));
   1.111 +val print_functions = Synchronized.var "Command.print_functions" ([]: print_function list);
   1.112  
   1.113  fun output_error tr exn =
   1.114    List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   1.115 @@ -174,14 +192,20 @@
   1.116  
   1.117  in
   1.118  
   1.119 -fun print st tr st' =
   1.120 -  rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, f)) =>
   1.121 -    (case Exn.capture (Runtime.controlled_execution f) {old_state = st, tr = tr, state = st'} of
   1.122 +fun print command_name eval =
   1.123 +  rev (Synchronized.value print_functions) |> map_filter (fn (name, (pri, get_print_fn)) =>
   1.124 +    (case Exn.capture (Runtime.controlled_execution get_print_fn) command_name of
   1.125        Exn.Res NONE => NONE
   1.126 -    | Exn.Res (SOME pr) => SOME {name = name, pri = pri, pr = (Lazy.lazy o print_error tr) pr}
   1.127 -    | Exn.Exn exn => SOME {name = name, pri = pri, pr = Lazy.lazy (fn () => output_error tr exn)}));
   1.128 +    | Exn.Res (SOME print_fn) =>
   1.129 +        SOME {name = name, pri = pri,
   1.130 +          print = memo (fn () =>
   1.131 +            let val {failed, command = tr, state = st', ...} = memo_result eval
   1.132 +            in if failed then () else print_error tr (fn () => print_fn tr st') () end)}
   1.133 +    | Exn.Exn exn =>
   1.134 +        SOME {name = name, pri = pri,
   1.135 +          print = memo (fn () => output_error (#command (memo_result eval)) exn)}));
   1.136  
   1.137 -fun print_function name pri f =
   1.138 +fun print_function {name, pri} f =
   1.139    Synchronized.change print_functions (fn funs =>
   1.140     (if not (AList.defined (op =) funs name) then ()
   1.141      else warning ("Redefining command print function: " ^ quote name);
   1.142 @@ -189,14 +213,15 @@
   1.143  
   1.144  end;
   1.145  
   1.146 -val _ = print_function "print_state" 0 (fn {tr, state, ...} =>
   1.147 -  let
   1.148 -    val is_init = Toplevel.is_init tr;
   1.149 -    val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   1.150 -    val do_print =
   1.151 -      not is_init andalso
   1.152 -        (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof state));
   1.153 -  in if do_print then SOME (fn () => Toplevel.print_state false state) else NONE end);
   1.154 +val _ =
   1.155 +  print_function {name = "print_state", pri = 0} (fn command_name => SOME (fn tr => fn st' =>
   1.156 +    let
   1.157 +      val is_init = Keyword.is_theory_begin command_name;
   1.158 +      val is_proof = Keyword.is_proof command_name;
   1.159 +      val do_print =
   1.160 +        not is_init andalso
   1.161 +          (Toplevel.print_of tr orelse (is_proof andalso Toplevel.is_proof st'));
   1.162 +    in if do_print then Toplevel.print_state false st' else () end));
   1.163  
   1.164  end;
   1.165  
     2.1 --- a/src/Pure/PIDE/document.ML	Thu Jul 04 12:02:11 2013 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Thu Jul 04 16:04:53 2013 +0200
     2.3 @@ -56,23 +56,31 @@
     2.4  fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
     2.5  
     2.6  
     2.7 +(* command execution *)
     2.8 +
     2.9 +type exec = exec_id * (Command.eval * Command.print list);  (*eval/print process*)
    2.10 +val no_exec: exec = (no_id, (Command.no_eval, []));
    2.11 +
    2.12 +fun exec_result ((_, (eval, _)): exec) = Command.memo_result eval;
    2.13 +
    2.14 +fun exec_run ((_, (eval, prints)): exec) =
    2.15 + (Command.memo_eval eval;
    2.16 +  prints |> List.app (fn {name, pri, print} =>
    2.17 +    Command.memo_fork {name = name, group = NONE, deps = [], pri = pri, interrupts = true} print));
    2.18 +
    2.19 +
    2.20  
    2.21  (** document structure **)
    2.22  
    2.23  type node_header = string * Thy_Header.header * string list;
    2.24 -type perspective = (command_id -> bool) * command_id option;
    2.25 +type perspective = Inttab.set * command_id option;
    2.26  structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    2.27  
    2.28 -type exec = ((Toplevel.state * {malformed: bool}) * Command.print list) Command.memo;
    2.29 -  (*eval/print process*)
    2.30 -val no_exec =
    2.31 -  Command.memo_value ((Toplevel.toplevel, {malformed = false}), []: Command.print list);
    2.32 -
    2.33  abstype node = Node of
    2.34   {header: node_header,  (*master directory, theory header, errors*)
    2.35    perspective: perspective,  (*visible commands, last visible command*)
    2.36 -  entries: (exec_id * exec) option Entries.T * bool,  (*command entries with excecutions, stable*)
    2.37 -  result: exec option}  (*result of last execution*)
    2.38 +  entries: exec option Entries.T * bool,  (*command entries with excecutions, stable*)
    2.39 +  result: Command.eval option}  (*result of last execution*)
    2.40  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    2.41  with
    2.42  
    2.43 @@ -83,7 +91,7 @@
    2.44    make_node (f (header, perspective, entries, result));
    2.45  
    2.46  fun make_perspective command_ids : perspective =
    2.47 -  (Inttab.defined (Inttab.make (map (rpair ()) command_ids)), try List.last command_ids);
    2.48 +  (Inttab.make_set command_ids, try List.last command_ids);
    2.49  
    2.50  val no_header = ("", Thy_Header.make ("", Position.none) [] [], ["Bad theory header"]);
    2.51  val no_perspective = make_perspective [];
    2.52 @@ -112,7 +120,8 @@
    2.53  fun set_perspective ids =
    2.54    map_node (fn (header, _, entries, result) => (header, make_perspective ids, entries, result));
    2.55  
    2.56 -val visible_command = #1 o get_perspective;
    2.57 +val visible_commands = #1 o get_perspective;
    2.58 +val visible_command = Inttab.defined o visible_commands;
    2.59  val visible_last = #2 o get_perspective;
    2.60  val visible_node = is_some o visible_last
    2.61  
    2.62 @@ -164,8 +173,8 @@
    2.63      NONE => err_undef "command entry" id
    2.64    | SOME (exec, _) => exec);
    2.65  
    2.66 -fun the_default_entry node (SOME id) = (id, the_default (no_id, no_exec) (the_entry node id))
    2.67 -  | the_default_entry _ NONE = (no_id, (no_id, no_exec));
    2.68 +fun the_default_entry node (SOME id) = (id, the_default no_exec (the_entry node id))
    2.69 +  | the_default_entry _ NONE = (no_id, no_exec);
    2.70  
    2.71  fun update_entry id exec =
    2.72    map_entries (Entries.update (id, exec));
    2.73 @@ -304,15 +313,14 @@
    2.74  
    2.75  (* consolidated states *)
    2.76  
    2.77 -fun stable_command (exec_id, exec) =
    2.78 +fun stable_command ((exec_id, (eval, prints)): exec) =
    2.79    not (Par_Exn.is_interrupted (Future.join_results (Goal.peek_futures exec_id))) andalso
    2.80 -    (case Exn.capture Command.memo_result exec of
    2.81 -      Exn.Exn exn => not (Exn.is_interrupt exn)
    2.82 -    | Exn.Res _ => true);
    2.83 +  Command.memo_stable eval andalso
    2.84 +  forall (Command.memo_stable o #print) prints;
    2.85  
    2.86  fun finished_theory node =
    2.87    (case Exn.capture (Command.memo_result o the) (get_result node) of
    2.88 -    Exn.Res ((st, _), _) => can (Toplevel.end_theory Position.none) st
    2.89 +    Exn.Res {state = st, ...} => can (Toplevel.end_theory Position.none) st
    2.90    | _ => false);
    2.91  
    2.92  
    2.93 @@ -325,15 +333,7 @@
    2.94  
    2.95  fun start_execution state =
    2.96    let
    2.97 -    fun execute exec =
    2.98 -      Command.memo_eval exec
    2.99 -      |> (fn (_, print) =>
   2.100 -        print |> List.app (fn {name, pri, pr} =>
   2.101 -          Lazy.future {name = name, group = NONE, deps = [], pri = pri, interrupts = true} pr
   2.102 -          |> ignore));
   2.103 -
   2.104      val (version_id, group, running) = execution_of state;
   2.105 -
   2.106      val _ =
   2.107        (singleton o Future.forks)
   2.108          {name = "Document.execution", group = SOME group, deps = [], pri = ~2, interrupts = true}
   2.109 @@ -350,7 +350,7 @@
   2.110                    (fn () =>
   2.111                      iterate_entries (fn (_, opt_exec) => fn () =>
   2.112                        (case opt_exec of
   2.113 -                        SOME (_, exec) => if ! running then SOME (execute exec) else NONE
   2.114 +                        SOME exec => if ! running then SOME (exec_run exec) else NONE
   2.115                        | NONE => NONE)) node ()))));
   2.116    in () end;
   2.117  
   2.118 @@ -391,10 +391,10 @@
   2.119            SOME thy => thy
   2.120          | NONE =>
   2.121              Toplevel.end_theory (Position.file_only import)
   2.122 -              (fst (fst
   2.123 +              (#state
   2.124                  (Command.memo_result
   2.125 -                  (the_default no_exec
   2.126 -                    (get_result (snd (the (AList.lookup (op =) deps import))))))))));
   2.127 +                  (the_default Command.no_eval
   2.128 +                    (get_result (snd (the (AList.lookup (op =) deps import)))))))));
   2.129      val _ = Position.reports (map #2 imports ~~ map Theory.get_markup parents);
   2.130    in Thy_Load.begin_theory master_dir header parents end;
   2.131  
   2.132 @@ -439,28 +439,28 @@
   2.133    else
   2.134      let
   2.135        val (name, span) = the_command state command_id' ||> Lazy.force;
   2.136 +
   2.137        fun illegal_init _ = error "Illegal theory header after end of theory";
   2.138        val (modify_init, init') =
   2.139          if Keyword.is_theory_begin name then
   2.140            (Toplevel.modify_init (fn () => the_default illegal_init init span), NONE)
   2.141          else (I, init);
   2.142 +
   2.143        val exec_id' = new_id ();
   2.144 -      val exec_id'_string = print_id exec_id';
   2.145 -      val read =
   2.146 -        Position.setmp_thread_data (Position.id_only exec_id'_string)
   2.147 -          (fn () =>
   2.148 -            Command.read span
   2.149 -            |> modify_init
   2.150 -            |> Toplevel.put_id exec_id'_string);
   2.151 -      val exec' =
   2.152 +      val eval' =
   2.153          Command.memo (fn () =>
   2.154            let
   2.155 -            val ((st, malformed), _) = Command.memo_result (snd (snd command_exec));
   2.156 -            val tr = read ();
   2.157 -            val ({failed}, (st', malformed')) = Command.eval span tr (st, malformed);
   2.158 -            val print = if failed orelse not command_visible then [] else Command.print st tr st';
   2.159 -          in ((st', malformed'), print) end);
   2.160 -      val command_exec' = (command_id', (exec_id', exec'));
   2.161 +            val eval_state = exec_result (snd command_exec);
   2.162 +            val tr =
   2.163 +              Position.setmp_thread_data (Position.id_only (print_id exec_id'))
   2.164 +                (fn () =>
   2.165 +                  Command.read span
   2.166 +                  |> modify_init
   2.167 +                  |> Toplevel.put_id (print_id exec_id')) ();
   2.168 +          in Command.eval span tr eval_state end);
   2.169 +      val prints' = if command_visible then Command.print name eval' else [];
   2.170 +
   2.171 +      val command_exec' = (command_id', (exec_id', (eval', prints')));
   2.172      in SOME (command_exec' :: execs, command_exec', init') end;
   2.173  
   2.174  in
   2.175 @@ -502,7 +502,7 @@
   2.176                        else last_common state last_visible node0 node;
   2.177                      val common_command_exec = the_default_entry node common;
   2.178  
   2.179 -                    val (new_execs, (command_id', (_, exec')), _) =
   2.180 +                    val (new_execs, (command_id', (_, (eval', _))), _) =
   2.181                        ([], common_command_exec, if initial then SOME init else NONE) |>
   2.182                        (still_visible orelse node_required) ?
   2.183                          iterate_entries_after common
   2.184 @@ -514,13 +514,14 @@
   2.185                        iterate_entries_after common
   2.186                          (fn ((_, id0), exec0) => fn res =>
   2.187                            if is_none exec0 then NONE
   2.188 -                          else if exists (fn (_, (id, _)) => id0 = id) new_execs then SOME res
   2.189 +                          else if exists (fn (_, (id, _)) => id0 = id) new_execs
   2.190 +                          then SOME res
   2.191                            else SOME (id0 :: res)) node0 [];
   2.192  
   2.193                      val last_exec = if command_id' = no_id then NONE else SOME command_id';
   2.194                      val result =
   2.195                        if is_some (after_entry node last_exec) then NONE
   2.196 -                      else SOME exec';
   2.197 +                      else SOME eval';
   2.198  
   2.199                      val node' = node
   2.200                        |> fold reset_entry no_execs