SSL debugger.ML Sprache: SML

(*  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_ML
        (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;

quality93%

¤ Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.