<commit_before>(*  Title:      Pure/PIDE/command.ML
    Author:     Makarius

Prover command execution: read -- eval -- print.
*)

signature COMMAND =
sig
  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
  type eval
  val eval_eq: eval * eval -> bool
  val eval_result_state: eval -> Toplevel.state
  val eval_stable: eval -> bool
  val eval: (unit -> theory) -> Token.T list -> eval -> eval
  type print
  val print: bool -> string -> eval -> print list -> print list option
  type print_fn = Toplevel.transition -> Toplevel.state -> unit
  val print_function: {name: string, pri: int, persistent: bool} ->
    ({command_name: string} -> print_fn option) -> unit
  val no_print_function: string -> unit
  type exec = eval * print list
  val no_exec: exec
  val exec_ids: exec option -> Document_ID.exec list
  val exec: Document_ID.execution -> exec -> unit
end;

structure Command: COMMAND =
struct

(** memo results -- including physical interrupts! **)

datatype 'a expr =
  Expr of Document_ID.exec * (unit -> 'a) |
  Result of 'a Exn.result;

abstype 'a memo = Memo of 'a expr Synchronized.var
with

fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));

fun memo_result (Memo v) =
  (case Synchronized.value v of
    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
  | Result res => Exn.release res);

fun memo_stable (Memo v) =
  (case Synchronized.value v of
   Expr _ => true
 | Result res => not (Exn.is_interrupt_exn res));

fun memo_exec execution_id (Memo v) =
  (case Synchronized.value v of
    Result res => res
  | Expr _ =>
      Synchronized.timed_access v (fn _ => SOME Time.zeroTime)
        (fn Result res => SOME (res, Result res)
          | expr as Expr (exec_id, e) =>
              uninterruptible (fn restore_attributes => fn () =>
                if Execution.running execution_id exec_id then
                  let
                    val res = Exn.capture (restore_attributes e) ();
                    val _ = Execution.finished exec_id;
                  in SOME (res, Result res) end
                else SOME (Exn.interrupt_exn, expr)) ())
      |> (fn NONE => error "Concurrent execution attempt" | SOME res => res))
  |> Exn.release |> ignore;

fun memo_fork params execution_id (Memo v) =
  (case Synchronized.value v of
    Result _ => ()
  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));

end;
<commit_msg>clarified memo_exec: plain synchronized access without any special tricks;<commit_after>(*  Title:      Pure/PIDE/command.ML
    Author:     Makarius

Prover command execution: read -- eval -- print.
*)

signature COMMAND =
sig
  val read: (unit -> theory) -> Token.T list -> Toplevel.transition
  type eval
  val eval_eq: eval * eval -> bool
  val eval_result_state: eval -> Toplevel.state
  val eval_stable: eval -> bool
  val eval: (unit -> theory) -> Token.T list -> eval -> eval
  type print
  val print: bool -> string -> eval -> print list -> print list option
  type print_fn = Toplevel.transition -> Toplevel.state -> unit
  val print_function: {name: string, pri: int, persistent: bool} ->
    ({command_name: string} -> print_fn option) -> unit
  val no_print_function: string -> unit
  type exec = eval * print list
  val no_exec: exec
  val exec_ids: exec option -> Document_ID.exec list
  val exec: Document_ID.execution -> exec -> unit
end;

structure Command: COMMAND =
struct

(** memo results -- including physical interrupts! **)

datatype 'a expr =
  Expr of Document_ID.exec * (unit -> 'a) |
  Result of 'a Exn.result;

abstype 'a memo = Memo of 'a expr Synchronized.var
with

fun memo exec_id e = Memo (Synchronized.var "Command.memo" (Expr (exec_id, e)));
fun memo_value a = Memo (Synchronized.var "Command.memo" (Result (Exn.Res a)));

fun memo_result (Memo v) =
  (case Synchronized.value v of
    Expr (exec_id, _) => error ("Unfinished execution result: " ^ Document_ID.print exec_id)
  | Result res => Exn.release res);

fun memo_stable (Memo v) =
  (case Synchronized.value v of
   Expr _ => true
 | Result res => not (Exn.is_interrupt_exn res));

fun memo_exec execution_id (Memo v) =
  Synchronized.guarded_access v
    (fn expr =>
      (case expr of
        Result res => SOME (res, expr)
      | Expr (exec_id, e) =>
          uninterruptible (fn restore_attributes => fn () =>
            if Execution.running execution_id exec_id then
              let
                val res = Exn.capture (restore_attributes e) ();
                val _ = Execution.finished exec_id;
              in SOME (res, Result res) end
            else SOME (Exn.interrupt_exn, expr)) ()))
  |> Exn.release |> ignore;

fun memo_fork params execution_id (Memo v) =
  (case Synchronized.value v of
    Result _ => ()
  | _ => ignore ((singleton o Future.forks) params (fn () => memo_exec execution_id (Memo v))));

end;

{'fraction_non_alphanumeric': 0.11656318846384939, 'fraction_numerical': 0.0, 'mean_word_length': 2.8863813229571984, 'pattern_counts': {'":': 0, '<': 3, '<?xml version=': 0, '>': 84, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '1040848', 'n_tokens_mistral': 1620, 'n_tokens_neox': 1579, 'n_words': 535}