[WIP] 🐕‍🦺 Cooltt Server v2.0

cooltt.opam

@@ -18,6 +18,7 @@ depends: [
   "menhir" {>= "20180703"}
   "uuseg" {>= "12.0.0"}
   "uutf" {>= "1.0.2"}
+  "lsp" {>= "1.8.3"}
   "odoc" {with-doc}
   "bantorra"
   "yuujinchou"

emacs/cooltt-lsp.el

@@ -0,0 +1,19 @@
+;;; cooltt-lsp ---  -*- lexical-binding: t; -*-
+
+;;; Commentary:
+(require 'cooltt)
+(require 'lsp-mode)
+
+(lsp-register-client
+ (make-lsp-client
+  :new-connection (lsp-stdio-connection (list cooltt-command "--mode" "server"))
+  :major-modes '(cooltt-mode)
+  :server-id 'cooltt))
+
+(lsp-consistency-check cooltt-lsp)
+(add-to-list 'lsp-language-id-configuration '(cooltt-mode . "cooltt"))
+
+;;; Code:
+
+(provide 'cooltt-lsp)
+;;; cooltt-lsp.el ends here

emacs/cooltt.el

@@ -120,7 +120,7 @@
   "Declaration keywords.")
 
 (defconst cooltt-command-keywords
-  '("#fail" "#normalize" "#print" "#quit")
+  '("#fail" "#normalize" "#print" "#quit" "#viz")
   "Command keywords.")
 
 (defconst cooltt-expression-keywords
@@ -186,7 +186,7 @@ See `compilation-error-regexp-alist' for semantics.")
 
 (defun cooltt-compile-options ()
   "Compute the options to provide to cooltt."
-  (let (opts cooltt-options)
+  (let ((opts cooltt-options))
     (when cooltt-debug
       (push "--debug" opts))
     opts))

src/basis/SegmentTree.ml

@@ -0,0 +1,73 @@
+module type POSITION =
+sig
+  include Map.OrderedType
+  type range = { start : t; stop: t }
+  val cut_range_after : t -> range -> range
+  val cut_range_before : t -> range -> range
+end
+
+module type S = functor (Pos: POSITION) ->
+sig
+  type !+'a t
+  val lookup : Pos.t -> 'a t -> 'a option
+  val containing : Pos.t -> 'a t -> 'a list
+  val of_list : (Pos.range * 'a) list -> 'a t
+  val empty : 'a t
+
+  val pp : (Format.formatter -> Pos.range -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+end
+
+module Make : S = functor (Pos : POSITION) ->
+struct
+
+  module Range = struct
+    type t = Pos.range
+    let compare (x : t) (y : t) =
+      CCOrd.(Pos.compare x.start y.start <?> (opp Pos.compare, x.stop, y.stop))
+  end
+
+  module SegTree = CCMap.Make(Range)
+
+  type !+'a t = 'a SegTree.t
+
+  let lookup pos t =
+    match SegTree.find_last_opt (fun k -> Range.compare k {start = pos; stop = pos} <= 0) t with
+    | None -> None
+    | Some (r, v) ->
+      if Pos.compare r.stop pos >= 0 then Some v else None
+
+  let containing pos t =
+    (* FIXME: This is suboptimal *)
+    CCList.of_iter @@ SegTree.values @@ SegTree.filter (fun range _ -> range.start <= pos && pos <= range.stop) t
+
+  let of_sorted_list l =
+    let rec loop tree stack l =
+      match stack, l with
+      | _, [] -> SegTree.add_list tree stack
+      | [], x :: l -> loop tree [x] l
+      | ((xk, xv) as x) :: stack, ((yk, _) as y :: l) ->
+        if Pos.compare yk.stop xk.start < 0 then
+          loop tree (y :: x :: stack) l
+        else if Pos.compare xk.stop yk.start < 0 then
+          loop (SegTree.add xk xv tree) stack (y :: l)
+        else
+          let tree =
+            if Pos.compare xk.start yk.start < 0 then
+              SegTree.add (Pos.cut_range_after yk.start xk) xv tree
+            else
+              tree
+          in
+          if Pos.compare xk.stop yk.stop > 0 then
+            loop tree (y :: (Pos.cut_range_before yk.stop xk, xv) :: stack) l
+          else
+            loop tree stack (y :: l)
+    in
+    loop SegTree.empty [] l
+
+  let of_list l =
+    of_sorted_list (CCList.sort (CCOrd.(>|=) Range.compare fst) l)
+
+  let empty = SegTree.empty
+
+  let pp pp_range pp_elem : Format.formatter -> 'a t -> unit = SegTree.pp pp_range pp_elem
+end

src/basis/SegmentTree.mli

@@ -0,0 +1,20 @@
+module type POSITION =
+sig
+  include Map.OrderedType
+  type range = { start : t; stop: t }
+  val cut_range_after : t -> range -> range
+  val cut_range_before : t -> range -> range
+end
+
+module type S = functor (Pos: POSITION) ->
+sig
+  type !+'a t
+  val lookup : Pos.t -> 'a t -> 'a option
+  val containing : Pos.t -> 'a t -> 'a list
+  val of_list : (Pos.range * 'a) list -> 'a t
+  val empty : 'a t
+
+  val pp : (Format.formatter -> Pos.range -> unit) -> (Format.formatter -> 'a -> unit) -> Format.formatter -> 'a t -> unit
+end
+
+module Make : S

src/bin/dune

@@ -2,7 +2,7 @@
 
 (executables
  (names main)
- (libraries cooltt.frontend cmdliner))
+ (libraries cooltt.frontend cooltt.server cmdliner))
 
 (install
  (section bin)

src/bin/main.ml

@@ -1,22 +1,34 @@
+open Server
 open Frontend
 open Cmdliner
 
 let _ =
   Printexc.record_backtrace false;
   ()
 
+type mode =
+  [ `Interactive
+  | `Scripting of [`Stdin | `File of string]
+  | `Server
+  ]
+
 type options =
-  { mode : [`Interactive | `Scripting of [`Stdin | `File of string]];
+  { mode : mode;
     as_file : string option;
     width : int;
-    debug_mode : bool }
+    debug_mode : bool;
+  }
+
+let options mode as_file width debug_mode =
+  { mode; as_file; width; debug_mode }
 
-let main {mode; as_file; width; debug_mode} =
+let main {mode; as_file; width; debug_mode; _} =
   Format.set_margin width;
   match
     match mode with
-    | `Interactive -> Driver.do_repl ~as_file ~debug_mode
-    | `Scripting input -> Driver.load_file ~as_file ~debug_mode input
+    | `Interactive -> Driver.do_repl {as_file; debug_mode}
+    | `Scripting input -> Driver.load_file {as_file; debug_mode;} input
+    | `Server -> LanguageServer.run ()
   with
   | Ok () -> `Ok ()
   | Error () -> `Error (false, "encountered one or more errors")
@@ -25,7 +37,7 @@ let opt_mode =
   let doc =
     "Set the interaction mode. "^
     "The value $(docv) must be one of "^
-    "$(b,scripting) (default) or $(b,interactive)." in
+    "$(b,scripting) (default), $(b,interactive), or $(b,server)." in
   Arg.(value & opt (some string) None & info ["m"; "mode"] ~doc ~docv:"MODE")
 
 let opt_interactive =
@@ -63,28 +75,34 @@ let parse_mode =
   function
   | "interactive" -> `Interactive
   | "scripting" -> `Scripting
+  | "server" -> `Server
   | s -> `Nonexistent s
 
 let quote s = "`" ^ s ^ "'"
 
-let consolidate_options mode interactive width input_file as_file debug_mode : options Term.ret =
-  match Option.map parse_mode mode, interactive, width, input_file with
-  | (Some `Scripting | None), false, width, Some input_file ->
-    `Ok {mode = `Scripting input_file; as_file; width; debug_mode}
-  | (Some `Scripting | None), false, _, None ->
-    `Error (true, "scripting mode expects an input file")
-  | Some `Interactive, _, width, None | None, true, width, None ->
-    `Ok {mode = `Interactive; as_file; width; debug_mode}
-  | Some `Interactive, _, _, Some _ | None, true, _, _ ->
-    `Error (true, "interactive mode expects no input files")
-  | Some `Scripting, true, _, _ ->
-    `Error (true, "inconsistent mode assignment")
-  | Some (`Nonexistent s), _, _, _ ->
-    `Error (true, "no mode named " ^ quote s)
+let consolidate_input_options mode interactive input_file : (mode, [`Msg of string]) result  =
+  match Option.map parse_mode mode, interactive, input_file with
+  | (Some `Scripting | None), false, Some input_file ->
+    Ok (`Scripting input_file)
+  | (Some `Scripting | None), false, None ->
+    Error (`Msg "scripting mode expects an input file")
+  | Some `Interactive, _, None | None, true, None ->
+    Ok `Interactive
+  | Some `Server, false, None ->
+    Ok `Server
+  | Some `Interactive, _, Some _ | None, true, _ ->
+    Error (`Msg "interactive mode expects no input files")
+  | Some `Server, _, Some _ ->
+    Error (`Msg "server mode expects no input files")
+  | Some `Scripting, true, _ ->
+    Error (`Msg "inconsistent mode assignment")
+  | Some `Server, true, _ ->
+    Error (`Msg "inconsistent mode assignment")
+  | Some (`Nonexistent s), _, _ ->
+    Error (`Msg ("no mode named " ^ quote s))
 
 let () =
-  let options : options Term.t =
-    Term.(ret (const consolidate_options $ opt_mode $ opt_interactive $ opt_width $ opt_input_file $ opt_as_file $ opt_debug))
-  in
+  let opts_input = Term.(term_result ~usage:true (const consolidate_input_options $ opt_mode $ opt_interactive $ opt_input_file))  in
+  let options : options Term.t = Term.(const options $ opts_input $ opt_as_file $ opt_width $ opt_debug) in
   let t = Term.ret @@ Term.(const main $ options) in
   Term.exit @@ Term.eval ~catch:true ~err:Format.std_formatter (t, myinfo)

src/core/RefineMonad.ml

@@ -5,6 +5,7 @@ module S = Syntax
 module St = RefineState
 module Env = RefineEnv
 module Err = RefineError
+module Metadata = RefineMetadata
 module Qu = Quote
 module Conv = Conversion
 
@@ -167,3 +168,20 @@ let push_problem lbl =
 
 let update_span loc =
   scope @@ Env.set_location loc
+
+let emit_tp loc tp =
+  match loc with
+  | Some loc ->
+    let* env = read in
+    let* qtp = quote_tp tp in
+    modify (St.add_type_at loc (Env.pp_env env) qtp)
+  | None ->
+    ret ()
+
+let emit_hole ctx tp =
+  let* env = read in
+  match Env.location env with
+  | Some loc -> 
+    let hole = St.Metadata.Hole { ctx; tp } in
+    modify (St.add_hole loc hole)
+  | None -> ret ()

src/core/RefineMonad.mli

@@ -44,3 +44,6 @@ val with_pp : (Pp.env -> 'a m) -> 'a m
 val expected_connective : RefineError.connective -> D.tp -> 'a m
 val expected_field : D.sign -> S.t -> string list -> 'a m
 val field_names_mismatch : expected:string list list -> actual:string list list -> 'a m
+
+val emit_tp : LexingUtil.span option -> D.tp -> unit m
+val emit_hole : (Ident.t * S.tp) list -> S.tp -> unit m

src/core/RefineState.ml

@@ -1,18 +1,43 @@
+open Basis
 open CodeUnit
 
 module IDMap = Map.Make (CodeUnitID)
 module D = Domain
+module S = Syntax
+
+module Metadata = struct
+  type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp }
+
+  type t = { holes : (LexingUtil.span * hole) list;
+             type_spans : (LexingUtil.span * Pp.env * S.tp) list
+           }
+
+  let init : t = { holes = []; type_spans = [] }
+
+  let holes metadata = metadata.holes
+
+  let type_spans metadata = metadata.type_spans
+
+  let add_hole span hole t = { t with holes = (span, hole) :: t.holes }
+
+  let add_type_at span env tp t = { t with type_spans = (span, env, tp) :: t.type_spans }
+end
+
 
 type t = { code_units : CodeUnit.t IDMap.t;
            (** The binding namespace for each code unit. *)
            namespaces : (Global.t Namespace.t) IDMap.t;
            (** The import namespace for each code unit. *)
-           import_namespaces : (Global.t Namespace.t) IDMap.t }
+           import_namespaces : (Global.t Namespace.t) IDMap.t;
+           metadata : Metadata.t
+         }
 
 let init =
   { code_units = IDMap.empty;
     namespaces = IDMap.empty;
-    import_namespaces = IDMap.empty }
+    import_namespaces = IDMap.empty;
+    metadata = Metadata.init
+  }
 
 let get_unit id st =
   IDMap.find id st.code_units
@@ -57,10 +82,21 @@ let add_import id modifier import_id st =
 let init_unit id st =
   { code_units = IDMap.add id (CodeUnit.create id) st.code_units;
     namespaces = IDMap.add id Namespace.empty st.namespaces;
-    import_namespaces = IDMap.add id Namespace.empty st.import_namespaces }
+    import_namespaces = IDMap.add id Namespace.empty st.import_namespaces;
+    metadata = st.metadata
+  }
 
 let get_import path st =
   IDMap.find_opt path st.code_units
 
 let is_imported path st =
   IDMap.mem path st.code_units
+
+let add_hole span hole st =
+  { st with metadata = Metadata.add_hole span hole st.metadata }
+
+let add_type_at span env tp st =
+  { st with metadata = Metadata.add_type_at span env tp st.metadata }
+
+let get_metadata st =
+  st.metadata

src/core/RefineState.mli

@@ -1,5 +1,7 @@
+open Basis
 open CodeUnit
 module D = Domain
+module S = Syntax
 
 type t
 
@@ -23,3 +25,17 @@ val is_imported : id -> t -> bool
 
 (** Create and add a new code unit. *)
 val init_unit : id -> t -> t
+
+
+module Metadata : sig
+  type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp }
+
+  type t
+
+  val holes : t -> (LexingUtil.span * hole) list
+  val type_spans : t -> (LexingUtil.span * Pp.env * S.tp) list
+end
+
+val add_hole : LexingUtil.span -> Metadata.hole -> t -> t
+val add_type_at : LexingUtil.span -> Pp.env -> S.tp -> t -> t
+val get_metadata  : t -> Metadata.t