LSP

Author: strub

dune-project

@@ -19,6 +19,10 @@
   dune
   dune-build-info
   dune-site
+  fmt
+  logs
+  lsp
+  lwt
   markdown
   (pcre2 (>= 8))
   (why3 (and (>= 1.8.0) (< 1.9)))

easycrypt.opam

@@ -7,6 +7,9 @@ depends: [
   "dune" {>= "3.13"}
   "dune-build-info"
   "dune-site"
+  "logs"
+  "lsp"
+  "lwt"
   "markdown"
   "pcre2" {>= "8"}
   "why3" {>= "1.8.0" & < "1.9"}

src/dune

@@ -16,15 +16,16 @@
  (public_name easycrypt.ecLib)
  (foreign_stubs (language c) (names eunix))
  (modules :standard \ ec)
- (libraries batteries camlp-streams dune-build-info dune-site inifiles markdown markdown.html pcre2 tyxml why3 yojson zarith)
+ (libraries batteries camlp-streams dune-build-info dune-site inifiles logs logs.fmt lsp lwt lwt.unix markdown markdown.html pcre2 tyxml why3 yojson zarith)
 )
 
 (executable
  (public_name easycrypt)
  (name ec)
  (modules ec)
  (promote (until-clean))
- (libraries batteries camlp-streams dune-build-info dune-site inifiles pcre2 why3 yojson zarith ecLib))
+ (libraries batteries ecLib)
+)
 
 (ocamllex ecLexer)
 

src/ec.ml

@@ -214,6 +214,9 @@ let main () =
   (* Execution of eager commands *)
   begin
     match options.o_command with
+    | `Lsp ->
+        EcLsp.run ();
+        exit 0
     | `Runtest input -> begin
         let root =
           match EcRelocate.sourceroot with
@@ -535,6 +538,9 @@ let main () =
     | `Runtest _ ->
         (* Eagerly executed *)
         assert false
+    | `Lsp ->
+        (* Eagerly executed *)
+        assert false
 
     | `DocGen docopts -> begin
         let name = docopts.doco_input in

src/ecIo.ml

@@ -96,14 +96,15 @@ let from_string data =
 let finalize (ecreader : ecreader) =
   Disposable.dispose ecreader
 
+(* -------------------------------------------------------------------- *)
+let isfinal_token = function
+  | EcParser.FINAL _ -> true
+  | _ -> false
+
 (* -------------------------------------------------------------------- *)
 let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
   let lexbuf = ecreader.ecr_lexbuf in
 
-  let isfinal = function
-    | EcParser.FINAL _ -> true
-    | _ -> false in
-
   if ecreader.ecr_atstart then
     ecreader.ecr_trim <- ecreader.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum;
 
@@ -134,7 +135,7 @@ let lexer ?(checkpoint : _ I.checkpoint option) (ecreader : ecreader_r) =
 
   ecreader.ecr_tokens  <- prequeue @ queue;
 
-  if isfinal token then
+  if isfinal_token token then
     ecreader.ecr_atstart <- true
   else
     ecreader.ecr_atstart <- ecreader.ecr_atstart && (
@@ -177,6 +178,42 @@ let parse (ecreader : ecreader) : EcParsetree.prog =
 
   in parse (EcParser.Incremental.prog ecreader.ecr_lexbuf.lex_curr_p)
 
+(* -------------------------------------------------------------------- *)
+let next_sentence_from (text : string) (start : int) : (string * int * int) option =
+  let len = String.length text in
+  if start < 0 || start >= len then
+    None
+  else
+    let sub = String.sub text start (len - start) in
+    let reader = from_string sub in
+    let ecr = Disposable.get reader in
+
+    let exception EOF in
+
+    Fun.protect
+      ~finally:(fun () -> finalize reader)
+      (fun () ->
+        try
+          begin
+            let exception Done in
+
+            try
+              while true do
+                match proj3_1 (lexer ecr) with
+                | EcParser.FINAL _ -> raise Done
+                | EcParser.EOF -> raise EOF
+                | _ -> ()
+              done
+            with Done -> ()
+          end;
+
+          let p = ecr.ecr_lexbuf.Lexing.lex_curr_p.pos_cnum - 1 in
+          let s = String.sub sub 0 p in
+
+          Some (s, start, start + p)
+        with
+        | EcLexer.LexicalError _ | EOF -> None)
+
 (* -------------------------------------------------------------------- *)
 let xparse (ecreader : ecreader) : string * EcParsetree.prog =
   let ecr = Disposable.get ecreader in

src/ecIo.mli

@@ -13,6 +13,7 @@ val parse    : ecreader -> EcParsetree.prog
 val parseall : ecreader -> EcParsetree.global list
 val drain    : ecreader -> unit
 val lexbuf   : ecreader -> Lexing.lexbuf
+val next_sentence_from : string -> int -> (string * int * int) option
 
 (* -------------------------------------------------------------------- *)
 val lex_single_token : string -> EcParser.token option