src/Pure/Tools/debugger.ML

More tidying of Nominal proofs

(*  Title:      Pure/Tools/debugger.ML
    Author:     Makarius

Interactive debugger for Isabelle/ML.
*)

signature DEBUGGER =
sig
  val writeln_message: string -> unit
  val warning_message: string -> unit
  val error_message: string -> unit
end;

structure Debugger: DEBUGGER =
struct

(** global state **)

(* output messages *)

fun output_message kind msg =
  if msg = "" then ()
  else
    Output.protocol_message
      (Markup.debugger_output (Isabelle_Thread.print (Isabelle_Thread.self ())))
      [[XML.Text (Markup.markup (kind, Markup.serial_properties (serial ())) msg)]];

val writeln_message = output_message Markup.writelnN;
val warning_message = output_message Markup.warningN;
val error_message = output_message Markup.errorN;

fun error_wrapper e =
  (case Exn.result e () of
    Exn.Res res => res
  | Exn.Exn exn => error_message (Runtime.exn_message exn));


(* thread input *)

val thread_input =
  Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);

fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
fun exit_input () = Synchronized.change thread_input (K NONE);

fun input thread_name msg =
  if null msg then error "Empty input"
  else
    Synchronized.change thread_input
      (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));

fun get_input thread_name =
  Synchronized.guarded_access thread_input
    (fn NONE => SOME ([], NONE)
      | SOME input =>
          (case Symtab.lookup input thread_name of
            NONE => NONE
          | SOME queue =>
              let
                val (msg, queue') = Queue.dequeue queue;
                val input' =
                  if Queue.is_empty queue' then Symtab.delete_safe thread_name input
                  else Symtab.update (thread_name, queue') input;
              in SOME (msg, SOME input') end));


(* global break *)

local
  val break = Synchronized.var "Debugger.break" false;
in

fun is_break () = Synchronized.value break;
fun set_break b = Synchronized.change break (K b);

end;



(** thread state **)

(* stack frame during debugging *)

val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var;

fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
val is_debugging = not o null o get_debugging;

fun with_debugging e =
  Thread_Data.setmp debugging_var
    (SOME (PolyML.DebuggerInterface.debugState (Thread.Thread.self ()))) e ();

fun the_debug_state thread_name index =
  (case get_debugging () of
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
  | states =>
      if index < 0 orelse index >= length states then
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
          quote thread_name)
      else nth states index);


(* flags for single-stepping *)

datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)

val stepping_var = Thread_Data.var () : stepping Thread_Data.var;

fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));

fun is_stepping () =
  let
    val stack = PolyML.DebuggerInterface.debugState (Thread.Thread.self ());
    val Stepping (stepping, depth) = get_stepping ();
  in stepping andalso (depth < 0 orelse length stack <= depth) end;

fun continue () = put_stepping (false, ~1);
fun step () = put_stepping (true, ~1);
fun step_over () = put_stepping (true, length (get_debugging ()));
fun step_out () = put_stepping (true, length (get_debugging ()) - 1);



(** eval ML **)

local

val context_attempts =
  map ML_Lex.read
   ["Context.put_generic_context (SOME (Context.Theory ML_context))",
    "Context.put_generic_context (SOME (Context.Proof ML_context))",
    "Context.put_generic_context (SOME ML_context)"];

fun environment SML = if SML then ML_Env.SML else ML_Env.Isabelle;
fun operations SML = if SML then ML_Env.SML_operations else ML_Env.Isabelle_operations;

fun evaluate {SML, verbose} =
  ML_Context.eval
    {environment = environment SML, redirect = false, verbose = verbose, catch_all = SML,
      debug = SOME false, writeln = writeln_message, warning = warning_message}
    Position.none;

fun eval_setup thread_name index SML context =
  context
  |> Context_Position.set_visible_generic false
  |> ML_Env.add_name_space (environment SML)
      (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));

fun eval_context thread_name index SML toks =
  let
    val context = Context.the_generic_context ();
    val context1 =
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
      then context
      else
        let
          val context' = context
            |> eval_setup thread_name index SML
            |> ML_Context.exec (fn () =>
                evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
          fun try_exec toks =
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
        in
          (case get_first try_exec context_attempts of
            SOME context2 => context2
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
        end;
  in context1 |> eval_setup thread_name index SML end;

in

fun eval thread_name index SML txt1 txt2 =
  let
    val (toks1, toks2) = apply2 (#read_source (operations SML) o Input.string) (txt1, txt2);
    val context = eval_context thread_name index SML toks1;
  in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;

fun print_vals thread_name index SML txt =
  let
    val toks = #read_source (operations SML) (Input.string txt)
    val context = eval_context thread_name index SML toks;
    val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);

    fun print x =
      Pretty.from_polyml
        (PolyML.NameSpace.Values.printWithType
          (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
    fun print_all () =
      #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) ()
      |> sort_by #1 |> map (Pretty.item o single o print o #2)
      |> Pretty.chunks |> Pretty.string_of |> writeln_message;
  in Context.setmp_generic_context (SOME context) print_all () end;

end;



(** debugger loop **)

local

fun debugger_state thread_name =
  Output.protocol_message (Markup.debugger_state thread_name)
   [get_debugging ()
    |> map (fn st =>
      (Position.properties_of
        (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
       PolyML.DebuggerInterface.debugFunction st))
    |> let open XML.Encode in list (pair properties string) end];

fun debugger_command thread_name =
  (case get_input thread_name of
    [] => (continue (); false)
  | ["continue"] => (continue (); false)
  | ["step"] => (step (); false)
  | ["step_over"] => (step_over (); false)
  | ["step_out"] => (step_out (); false)
  | ["eval", index, SML, txt1, txt2] =>
     (error_wrapper (fn () =>
        eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
  | ["print_vals", index, SML, txt] =>
     (error_wrapper (fn () =>
        print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
  | bad =>
     (Output.system_message
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));

in

fun debugger_loop thread_name =
  Thread_Attributes.uninterruptible_body (fn run =>
    let
      fun loop () =
        (debugger_state thread_name; if debugger_command thread_name then loop () else ());
      val result = Exn.capture (run with_debugging) loop;
      val _ = debugger_state thread_name;
    in Exn.release result end);

end;



(** protocol commands **)

val _ =
  Protocol_Command.define "Debugger.init"
    (fn [] =>
     (init_input ();
      PolyML.DebuggerInterface.setOnBreakPoint
        (SOME (fn (_, break) =>
          if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
          then
            (case try (Isabelle_Thread.print o Isabelle_Thread.self) () of
              SOME thread_name => debugger_loop thread_name
            | NONE => ())
          else ()))));

val _ =
  Protocol_Command.define "Debugger.exit"
    (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));

val _ =
  Protocol_Command.define "Debugger.break"
    (fn [b] => set_break (Value.parse_bool b));

val _ =
  Protocol_Command.define "Debugger.breakpoint"
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
      let
        val id = Value.parse_int id0;
        val breakpoint = Value.parse_int breakpoint0;
        val breakpoint_state = Value.parse_bool breakpoint_state0;

        fun err () = error ("Bad exec for command " ^ Value.print_int id);
      in
        (case Document.command_exec (Document.state ()) node_name id of
          SOME (eval, _) =>
            if Command.eval_finished eval then
              let
                val st = Command.eval_result_state eval;
                val ctxt = Toplevel.presentation_context st;
              in
                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
                  SOME (b, _) => b := breakpoint_state
                | NONE => err ())
              end
            else err ()
        | NONE => err ())
      end);

val _ =
  Protocol_Command.define "Debugger.input"
    (fn thread_name :: msg => input thread_name msg);

end;