Introduce abstract debugger

GillianCore/command_line/command_line.ml

@@ -35,8 +35,12 @@ struct
   module Verification = Verifier.Make (SState) (SPState) (PC) (External)
   module Lifter = Lifter (Verification)
   module Abductor = Abductor.Make (SPState) (PC) (External)
-  module Debugger = Debugger.Make (ID) (PC) (Verification) (Lifter)
-  module Debug_adapter = Debug_adapter.Make (Debugger)
+
+  module Symb_debugger =
+    Debugger.Symbolic_debugger.Make (ID) (PC) (Verification) (Lifter)
+
+  module Verif_debugger =
+    Debugger.Verification_debugger.Make (ID) (PC) (Verification) (Lifter)
 
   let main () =
     Memtrace.trace_if_requested ();
@@ -60,7 +64,12 @@ struct
                   (Gil_parsing));
         (module Verification_console.Make (ID) (PC) (Verification) (Gil_parsing));
         (module Act_console.Make (ID) (PC) (Abductor) (Gil_parsing));
-        (module Debug_verification_console.Make (PC) (Debug_adapter));
+        (module Debug_verification_console.Make
+                  (PC)
+                  (Debug_adapter.Make (Verif_debugger)));
+        (module Debug_wpst_console.Make
+                  (PC)
+                  (Debug_adapter.Make (Symb_debugger)));
         (module Bulk_console.Make (PC) (Runners));
       ]
     in

GillianCore/command_line/debug_verification_console.ml

@@ -21,6 +21,7 @@ module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) :
     Cmd.info "debugverify" ~doc ~man
 
   let start_debug_adapter manual () =
+    Config.current_exec_mode := Utils.Exec_mode.Verification;
     Config.manual_proof := manual;
     Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout)
 

GillianCore/command_line/debug_wpst_console.ml

@@ -0,0 +1,28 @@
+open Cmdliner
+
+module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) :
+  Console.S = struct
+  module Common_args = Common_args.Make (PC)
+
+  let debug_wpst_info =
+    let doc =
+      "Starts Gillian in debugging mode for whole-program symbolic testing"
+    in
+    let man =
+      [
+        `S Manpage.s_description;
+        `P
+          "Starts Gillian in debugging mode for whole-program symbolic \
+           testing, which communicates via the Debug Adapter Protocol";
+      ]
+    in
+    Cmd.info "debugwpst" ~doc ~man
+
+  let start_debug_adapter () =
+    Config.current_exec_mode := Utils.Exec_mode.Symbolic;
+    Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout)
+
+  let debug_wpst_t = Common_args.use Term.(const start_debug_adapter)
+  let debug_wpst_cmd = Cmd.v debug_wpst_info debug_wpst_t
+  let cmds = [ debug_wpst_cmd ]
+end

GillianCore/debugging/adapter/inspect.ml

@@ -73,8 +73,8 @@ module Make (Debugger : Debugger.S) = struct
     DL.set_rpc_command_handler rpc ~name:"Unification"
       (module Unification_command)
       (fun { id } ->
-        let unify_id, unify_map = dbg |> Debugger.Inspect.get_unification id in
-        let result = Unification_command.Result.make ~unify_id ~unify_map in
+        let unify_map = dbg |> Debugger.Inspect.get_unify_map id in
+        let result = Unification_command.Result.make ~unify_id:id ~unify_map in
         Lwt.return result);
     Lwt.return ()
 end