WIP

GillianCore/command_line/dune

@@ -12,7 +12,9 @@
   debugger_lifter
   incrementalAnalysis
   debug_adapter
-  memtrace)
+  memtrace
+  linol
+  linol-lwt)
  (flags
   :standard
   -open

GillianCore/command_line/verification_console.ml

@@ -66,43 +66,44 @@ module Make
       in
       (e_prog, init_data, None)
 
-  let process_files files already_compiled outfile_opt no_unfold incremental =
-    Verification.start_time := Sys.time ();
-    Fmt.pr "Parsing and compiling...\n@?";
-    let* e_prog, init_data, source_files_opt =
-      parse_eprog files already_compiled
-    in
-    let () =
-      let pp_annot fmt annot =
-        Fmt.pf fmt "%a"
-          (Yojson.Safe.pretty_print ?std:None)
-          (PC.Annot.to_yojson annot)
+  let verify files already_compiled outfile_opt no_unfold incremental =
+    Gillian_result.try_ @@ fun () ->
+      Verification.start_time := Sys.time ();
+      Fmt.pr "Parsing and compiling...\n@?";
+      let* e_prog, init_data, source_files_opt =
+        parse_eprog files already_compiled
       in
-      burn_gil
-        ~pp_prog:(Prog.pp_labeled ~pp_annot)
-        ~init_data:(ID.to_yojson init_data) e_prog outfile_opt
-    in
-    (* Prog.perform_syntax_checks e_prog; *)
-    Fmt.pr "Preprocessing...\n@?";
-    let+ prog =
-      Gil_parsing.eprog_to_prog ~other_imports:PC.other_imports e_prog
-    in
-    let () =
-      L.verbose (fun m ->
-          m "@\nProgram as parsed:@\n%a@\n"
-            (Prog.pp_indexed ?pp_annot:None)
-            prog)
-    in
-    let prog = LogicPreprocessing.preprocess prog (not no_unfold) in
-    let () =
-      L.verbose (fun m ->
-          m "@\nProgram after logic preprocessing:@\n%a@\n"
-            (Prog.pp_indexed ?pp_annot:None)
-            prog)
-    in
-    Verification.verify_prog ~init_data prog incremental source_files_opt
+      let () =
+        let pp_annot fmt annot =
+          Fmt.pf fmt "%a"
+            (Yojson.Safe.pretty_print ?std:None)
+            (PC.Annot.to_yojson annot)
+        in
+        burn_gil
+          ~pp_prog:(Prog.pp_labeled ~pp_annot)
+          ~init_data:(ID.to_yojson init_data) e_prog outfile_opt
+      in
+      (* Prog.perform_syntax_checks e_prog; *)
+      Fmt.pr "Preprocessing...\n@?";
+      let+ prog =
+        Gil_parsing.eprog_to_prog ~other_imports:PC.other_imports e_prog
+      in
+      let () =
+        L.verbose (fun m ->
+            m "@\nProgram as parsed:@\n%a@\n"
+              (Prog.pp_indexed ?pp_annot:None)
+              prog)
+      in
+      let prog = LogicPreprocessing.preprocess prog (not no_unfold) in
+      let () =
+        L.verbose (fun m ->
+            m "@\nProgram after logic preprocessing:@\n%a@\n"
+              (Prog.pp_indexed ?pp_annot:None)
+              prog)
+      in
+      Verification.verify_prog ~init_data prog incremental source_files_opt
 
-  let verify
+  let verify_once
       files
       already_compiled
       outfile_opt
@@ -124,17 +125,14 @@ module Make
     let () = Config.manual_proof := manual in
     let () = Config.Verification.set_procs_to_verify procs_to_verify in
     let () = Config.Verification.set_lemmas_to_verify lemmas_to_verify in
-    let r =
-      Gillian_result.try_ @@ fun () ->
-      process_files files already_compiled outfile_opt no_unfold incremental
-    in
+    let r = verify files already_compiled outfile_opt no_unfold incremental in
     let () = if stats then Statistics.print_statistics () in
     let () = Common_args.exit_on_error r in
     exit 0
 
   let verify_t =
     Term.(
-      const verify $ files $ already_compiled $ output_gil $ no_unfold $ stats
+      const verify_once $ files $ already_compiled $ output_gil $ no_unfold $ stats
       $ no_lemma_proof $ manual $ incremental $ proc_arg $ lemma_arg)
 
   let verify_info =
@@ -171,9 +169,90 @@ module Make
     let debug_verify_cmd = Cmd.v debug_verify_info debug_verify_t
   end
 
+  module Lsp = struct
+    class lsp_server =
+      object (self)
+        inherit Linol_lwt.Jsonrpc2.server
+
+        (* one env per document *)
+        val buffers : (Lsp.Types.DocumentUri.t, unit) Hashtbl.t =
+          Hashtbl.create 32
+
+        method spawn_query_handler f = Linol_lwt.spawn f
+
+        (* We define here a helper method that will:
+           - process a document
+           - store the state resulting from the processing
+           - return the diagnostics from the new state
+        *)
+        method private _on_doc
+            ~(notify_back : Linol_lwt.Jsonrpc2.notify_back)
+            (uri : Lsp.Types.DocumentUri.t)
+            (contents : string) =
+          let files = [ "" ] in  (* TODO *)
+          let r = verify files false None false false in
+
+
+        (* We now override the [on_notify_doc_did_open] method that will be called
+           by the server each time a new document is opened. *)
+        method on_notif_doc_did_open ~notify_back d ~content : unit Linol_lwt.t
+            =
+          self#_on_doc ~notify_back d.uri content
+
+        (* Similarly, we also override the [on_notify_doc_did_change] method that will be called
+           by the server each time a new document is opened. *)
+        method on_notif_doc_did_change
+            ~notify_back
+            d
+            _c
+            ~old_content:_old
+            ~new_content =
+          self#_on_doc ~notify_back d.uri new_content
+
+        (* On document closes, we remove the state associated to the file from the global
+           hashtable state, to avoid leaking memory. *)
+        method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t =
+          Hashtbl.remove buffers d.uri;
+          Linol_lwt.return ()
+      end
+
+    let debug_verify_info =
+      let doc = "Starts Gillian in language server mode for verification" in
+      let man =
+        [
+          `S Manpage.s_description;
+          `P
+            "Starts Gillian in language server mode for verification, which \
+             communicates via the Language Server Protocol";
+        ]
+      in
+      Cmd.info "debug" ~doc ~man
+
+    let start_language_server manual () =
+      Config.current_exec_mode := Utils.Exec_mode.Verification;
+      Config.manual_proof := manual;
+      let s = new lsp_server in
+      let server = Linol_lwt.Jsonrpc2.create_stdio ~env:() s in
+      let task =
+        let shutdown () = s#get_status = `ReceivedExit in
+        Linol_lwt.Jsonrpc2.run ~shutdown server
+      in
+      match Linol_lwt.run task with
+      | () -> ()
+      | exception e ->
+          let e = Printexc.to_string e in
+          Printf.eprintf "error: %s\n%!" e;
+          exit 1
+
+    let lsp_verify_t =
+      Common_args.use Term.(const start_language_server $ manual)
+
+    let lsp_verify_cmd = Cmd.v debug_verify_info lsp_verify_t
+  end
+
   let verify_cmd =
     Cmd.group ~default:(Common_args.use verify_t) verify_info
-      [ Debug.debug_verify_cmd ]
+      [ Debug.debug_verify_cmd; Lsp.lsp_verify_cmd ]
 
   let cmds = [ verify_cmd ]
 end