src/Pure/Tools/debugger.ML
author wenzelm
Tue Nov 07 16:50:26 2017 +0100 (20 months ago)
changeset 67026 687c822ee5e3
parent 65222 fb8253564483
child 67381 146757999c8d
permissions -rw-r--r--
tuned signature;
wenzelm@60749
     1
(*  Title:      Pure/Tools/debugger.ML
wenzelm@60749
     2
    Author:     Makarius
wenzelm@60749
     3
wenzelm@60749
     4
Interactive debugger for Isabelle/ML.
wenzelm@60749
     5
*)
wenzelm@60749
     6
wenzelm@60830
     7
signature DEBUGGER =
wenzelm@60830
     8
sig
wenzelm@60834
     9
  val writeln_message: string -> unit
wenzelm@60834
    10
  val warning_message: string -> unit
wenzelm@60834
    11
  val error_message: string -> unit
wenzelm@60830
    12
end;
wenzelm@60830
    13
wenzelm@60830
    14
structure Debugger: DEBUGGER =
wenzelm@60765
    15
struct
wenzelm@60765
    16
wenzelm@60869
    17
(** global state **)
wenzelm@60869
    18
wenzelm@60869
    19
(* output messages *)
wenzelm@60830
    20
wenzelm@60834
    21
fun output_message kind msg =
wenzelm@60864
    22
  if msg = "" then ()
wenzelm@60864
    23
  else
wenzelm@60864
    24
    Output.protocol_message
wenzelm@61556
    25
      (Markup.debugger_output (Standard_Thread.the_name ()))
wenzelm@60864
    26
      [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
wenzelm@60834
    27
wenzelm@60834
    28
val writeln_message = output_message Markup.writelnN;
wenzelm@60834
    29
val warning_message = output_message Markup.warningN;
wenzelm@60834
    30
val error_message = output_message Markup.errorN;
wenzelm@60830
    31
wenzelm@60856
    32
fun error_wrapper e = e ()
wenzelm@60856
    33
  handle exn =>
wenzelm@62505
    34
    if Exn.is_interrupt exn then Exn.reraise exn
wenzelm@60856
    35
    else error_message (Runtime.exn_message exn);
wenzelm@60856
    36
wenzelm@60830
    37
wenzelm@60888
    38
(* thread input *)
wenzelm@60765
    39
wenzelm@60888
    40
val thread_input =
wenzelm@60891
    41
  Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);
wenzelm@60891
    42
wenzelm@60891
    43
fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
wenzelm@60891
    44
fun exit_input () = Synchronized.change thread_input (K NONE);
wenzelm@60765
    45
wenzelm@60842
    46
fun input thread_name msg =
wenzelm@60891
    47
  if null msg then error "Empty input"
wenzelm@60891
    48
  else
wenzelm@60891
    49
    Synchronized.change thread_input
wenzelm@60891
    50
      (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));
wenzelm@60887
    51
wenzelm@60842
    52
fun get_input thread_name =
wenzelm@60891
    53
  Synchronized.guarded_access thread_input
wenzelm@60891
    54
    (fn NONE => SOME ([], NONE)
wenzelm@60891
    55
      | SOME input =>
wenzelm@60891
    56
          (case Symtab.lookup input thread_name of
wenzelm@60891
    57
            NONE => NONE
wenzelm@60891
    58
          | SOME queue =>
wenzelm@60891
    59
              let
wenzelm@60891
    60
                val (msg, queue') = Queue.dequeue queue;
wenzelm@60891
    61
                val input' =
wenzelm@60891
    62
                  if Queue.is_empty queue' then Symtab.delete_safe thread_name input
wenzelm@60891
    63
                  else Symtab.update (thread_name, queue') input;
wenzelm@60891
    64
              in SOME (msg, SOME input') end));
wenzelm@60765
    65
wenzelm@60765
    66
wenzelm@60932
    67
(* global break *)
wenzelm@60932
    68
wenzelm@60932
    69
local
wenzelm@60932
    70
  val break = Synchronized.var "Debugger.break" false;
wenzelm@60932
    71
in
wenzelm@60932
    72
wenzelm@60932
    73
fun is_break () = Synchronized.value break;
wenzelm@60932
    74
fun set_break b = Synchronized.change break (K b);
wenzelm@60932
    75
wenzelm@60932
    76
end;
wenzelm@60932
    77
wenzelm@60932
    78
wenzelm@60869
    79
wenzelm@60869
    80
(** thread state **)
wenzelm@60869
    81
wenzelm@60869
    82
(* stack frame during debugging *)
wenzelm@60856
    83
wenzelm@62937
    84
val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var;
wenzelm@60765
    85
wenzelm@62889
    86
fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
wenzelm@60856
    87
val is_debugging = not o null o get_debugging;
wenzelm@60765
    88
wenzelm@60856
    89
fun with_debugging e =
wenzelm@62937
    90
  Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e ();
wenzelm@60749
    91
wenzelm@60858
    92
fun the_debug_state thread_name index =
wenzelm@60858
    93
  (case get_debugging () of
wenzelm@60858
    94
    [] => error ("Missing debugger information for thread " ^ quote thread_name)
wenzelm@60858
    95
  | states =>
wenzelm@60858
    96
      if index < 0 orelse index >= length states then
wenzelm@60858
    97
        error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
wenzelm@60858
    98
          quote thread_name)
wenzelm@60858
    99
      else nth states index);
wenzelm@60858
   100
wenzelm@60858
   101
wenzelm@60869
   102
(* flags for single-stepping *)
wenzelm@60765
   103
wenzelm@60869
   104
datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
wenzelm@60869
   105
wenzelm@62889
   106
val stepping_var = Thread_Data.var () : stepping Thread_Data.var;
wenzelm@60869
   107
wenzelm@62889
   108
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
wenzelm@62889
   109
fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));
wenzelm@60869
   110
wenzelm@60869
   111
fun is_stepping () =
wenzelm@60869
   112
  let
wenzelm@62937
   113
    val stack = PolyML.DebuggerInterface.debugState (Thread.self ());
wenzelm@60869
   114
    val Stepping (stepping, depth) = get_stepping ();
wenzelm@60869
   115
  in stepping andalso (depth < 0 orelse length stack <= depth) end;
wenzelm@60869
   116
wenzelm@60931
   117
fun continue () = put_stepping (false, ~1);
wenzelm@60931
   118
fun step () = put_stepping (true, ~1);
wenzelm@60931
   119
fun step_over () = put_stepping (true, length (get_debugging ()));
wenzelm@60931
   120
fun step_out () = put_stepping (true, length (get_debugging ()) - 1);
wenzelm@60869
   121
wenzelm@60869
   122
wenzelm@60935
   123
wenzelm@60869
   124
(** eval ML **)
wenzelm@60765
   125
wenzelm@60862
   126
local
wenzelm@60862
   127
wenzelm@60862
   128
val context_attempts =
wenzelm@60862
   129
  map ML_Lex.read
wenzelm@62889
   130
   ["Context.put_generic_context (SOME (Context.Theory ML_context))",
wenzelm@62889
   131
    "Context.put_generic_context (SOME (Context.Proof ML_context))",
wenzelm@62889
   132
    "Context.put_generic_context (SOME ML_context)"];
wenzelm@60862
   133
wenzelm@60862
   134
fun evaluate {SML, verbose} =
wenzelm@60862
   135
  ML_Context.eval
wenzelm@62902
   136
    {SML = SML, exchange = false, redirect = false, verbose = verbose,
wenzelm@60956
   137
      debug = SOME false, writeln = writeln_message, warning = warning_message}
wenzelm@60862
   138
    Position.none;
wenzelm@60862
   139
wenzelm@60935
   140
fun eval_setup thread_name index SML context =
wenzelm@60935
   141
  context
wenzelm@60935
   142
  |> Context_Position.set_visible_generic false
wenzelm@60935
   143
  |> ML_Env.add_name_space {SML = SML}
wenzelm@62937
   144
      (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
wenzelm@60935
   145
wenzelm@60897
   146
fun eval_context thread_name index SML toks =
wenzelm@60858
   147
  let
wenzelm@62876
   148
    val context = Context.the_generic_context ();
wenzelm@60897
   149
    val context1 =
wenzelm@60897
   150
      if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
wenzelm@60935
   151
      then context
wenzelm@60862
   152
      else
wenzelm@60862
   153
        let
wenzelm@60935
   154
          val context' = context
wenzelm@60935
   155
            |> eval_setup thread_name index SML
wenzelm@60897
   156
            |> ML_Context.exec (fn () =>
wenzelm@60897
   157
                evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
wenzelm@60862
   158
          fun try_exec toks =
wenzelm@60862
   159
            try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
wenzelm@60862
   160
        in
wenzelm@60862
   161
          (case get_first try_exec context_attempts of
wenzelm@60862
   162
            SOME context2 => context2
wenzelm@60862
   163
          | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
wenzelm@60862
   164
        end;
wenzelm@60935
   165
  in context1 |> eval_setup thread_name index SML end;
wenzelm@60897
   166
wenzelm@60897
   167
in
wenzelm@60897
   168
wenzelm@60897
   169
fun eval thread_name index SML txt1 txt2 =
wenzelm@60897
   170
  let
wenzelm@60897
   171
    val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
wenzelm@60897
   172
    val context = eval_context thread_name index SML toks1;
wenzelm@62889
   173
  in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
wenzelm@60897
   174
wenzelm@60897
   175
fun print_vals thread_name index SML txt =
wenzelm@60897
   176
  let
wenzelm@60935
   177
    val toks = ML_Lex.read_source SML (Input.string txt)
wenzelm@60935
   178
    val context = eval_context thread_name index SML toks;
wenzelm@62937
   179
    val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
wenzelm@60897
   180
wenzelm@60897
   181
    fun print x =
wenzelm@62663
   182
      Pretty.from_polyml
wenzelm@62934
   183
        (PolyML.NameSpace.Values.printWithType
wenzelm@62934
   184
          (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
wenzelm@60897
   185
    fun print_all () =
wenzelm@62937
   186
      #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) ()
wenzelm@60924
   187
      |> sort_by #1 |> map (Pretty.item o single o print o #2)
wenzelm@60897
   188
      |> Pretty.chunks |> Pretty.string_of |> writeln_message;
wenzelm@62889
   189
  in Context.setmp_generic_context (SOME context) print_all () end;
wenzelm@60862
   190
wenzelm@60862
   191
end;
wenzelm@60749
   192
wenzelm@60765
   193
wenzelm@60869
   194
wenzelm@60891
   195
(** debugger loop **)
wenzelm@60857
   196
wenzelm@60857
   197
local
wenzelm@60765
   198
wenzelm@60842
   199
fun debugger_state thread_name =
wenzelm@60842
   200
  Output.protocol_message (Markup.debugger_state thread_name)
wenzelm@60856
   201
   [get_debugging ()
wenzelm@60842
   202
    |> map (fn st =>
wenzelm@62821
   203
      (Position.properties_of
wenzelm@62937
   204
        (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
wenzelm@62937
   205
       PolyML.DebuggerInterface.debugFunction st))
wenzelm@60842
   206
    |> let open XML.Encode in list (pair properties string) end
wenzelm@60842
   207
    |> YXML.string_of_body];
wenzelm@60842
   208
wenzelm@60857
   209
fun debugger_command thread_name =
wenzelm@60857
   210
  (case get_input thread_name of
wenzelm@60931
   211
    [] => (continue (); false)
wenzelm@60931
   212
  | ["continue"] => (continue (); false)
wenzelm@60931
   213
  | ["step"] => (step (); false)
wenzelm@60931
   214
  | ["step_over"] => (step_over (); false)
wenzelm@60931
   215
  | ["step_out"] => (step_out (); false)
wenzelm@60857
   216
  | ["eval", index, SML, txt1, txt2] =>
wenzelm@60857
   217
     (error_wrapper (fn () =>
wenzelm@63806
   218
        eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
wenzelm@60897
   219
  | ["print_vals", index, SML, txt] =>
wenzelm@60897
   220
     (error_wrapper (fn () =>
wenzelm@63806
   221
        print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
wenzelm@60857
   222
  | bad =>
wenzelm@60857
   223
     (Output.system_message
wenzelm@60857
   224
        ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
wenzelm@60857
   225
wenzelm@60889
   226
in
wenzelm@60889
   227
wenzelm@60842
   228
fun debugger_loop thread_name =
wenzelm@62923
   229
  Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
wenzelm@60885
   230
    let
wenzelm@60885
   231
      fun loop () =
wenzelm@60885
   232
        (debugger_state thread_name; if debugger_command thread_name then loop () else ());
wenzelm@60885
   233
      val result = Exn.capture (restore_attributes with_debugging) loop;
wenzelm@60885
   234
      val _ = debugger_state thread_name;
wenzelm@60885
   235
    in Exn.release result end) ();
wenzelm@60765
   236
wenzelm@60857
   237
end;
wenzelm@60857
   238
wenzelm@60765
   239
wenzelm@60869
   240
wenzelm@60869
   241
(** protocol commands **)
wenzelm@60765
   242
wenzelm@60765
   243
val _ =
wenzelm@60765
   244
  Isabelle_Process.protocol_command "Debugger.init"
wenzelm@60889
   245
    (fn [] =>
wenzelm@60891
   246
     (init_input ();
wenzelm@62937
   247
      PolyML.DebuggerInterface.setOnBreakPoint
wenzelm@60889
   248
        (SOME (fn (_, break) =>
wenzelm@60932
   249
          if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
wenzelm@60932
   250
          then
wenzelm@61556
   251
            (case Standard_Thread.get_name () of
wenzelm@60889
   252
              SOME thread_name => debugger_loop thread_name
wenzelm@60889
   253
            | NONE => ())
wenzelm@60891
   254
          else ()))));
wenzelm@60889
   255
wenzelm@60889
   256
val _ =
wenzelm@60889
   257
  Isabelle_Process.protocol_command "Debugger.exit"
wenzelm@62937
   258
    (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
wenzelm@60765
   259
wenzelm@60765
   260
val _ =
wenzelm@60932
   261
  Isabelle_Process.protocol_command "Debugger.break"
wenzelm@63806
   262
    (fn [b] => set_break (Value.parse_bool b));
wenzelm@60932
   263
wenzelm@60932
   264
val _ =
wenzelm@60878
   265
  Isabelle_Process.protocol_command "Debugger.breakpoint"
wenzelm@60880
   266
    (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
wenzelm@60878
   267
      let
wenzelm@63806
   268
        val id = Value.parse_int id0;
wenzelm@63806
   269
        val breakpoint = Value.parse_int breakpoint0;
wenzelm@63806
   270
        val breakpoint_state = Value.parse_bool breakpoint_state0;
wenzelm@60880
   271
wenzelm@63806
   272
        fun err () = error ("Bad exec for command " ^ Value.print_int id);
wenzelm@60880
   273
      in
wenzelm@60880
   274
        (case Document.command_exec (Document.state ()) node_name id of
wenzelm@60880
   275
          SOME (eval, _) =>
wenzelm@60880
   276
            if Command.eval_finished eval then
wenzelm@60880
   277
              let
wenzelm@60880
   278
                val st = Command.eval_result_state eval;
wenzelm@60880
   279
                val ctxt = Toplevel.presentation_context_of st
wenzelm@60880
   280
                  handle Toplevel.UNDEF => err ();
wenzelm@60880
   281
              in
wenzelm@60880
   282
                (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
wenzelm@60880
   283
                  SOME (b, _) => b := breakpoint_state
wenzelm@60880
   284
                | NONE => err ())
wenzelm@60880
   285
              end
wenzelm@60880
   286
            else err ()
wenzelm@60880
   287
        | NONE => err ())
wenzelm@60880
   288
      end);
wenzelm@60878
   289
wenzelm@60878
   290
val _ =
wenzelm@60765
   291
  Isabelle_Process.protocol_command "Debugger.input"
wenzelm@60842
   292
    (fn thread_name :: msg => input thread_name msg);
wenzelm@60765
   293
wenzelm@60749
   294
end;