[WIP] 🐕‍🦺 Cooltt Server v2.0

src/basis/SegmentTree.ml

@@ -9,8 +9,12 @@ end
 module type S = functor (Pos: POSITION) ->
 sig
   type !+'a t
-  val of_list : (Pos.range * 'a) list -> '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) ->
@@ -32,9 +36,13 @@ struct
     | 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 l, stack with
+      match stack, l with
       | _, [] -> SegTree.add_list tree stack
       | [], x :: l -> loop tree [x] l
       | ((xk, xv) as x) :: stack, ((yk, _) as y :: l) ->
@@ -58,4 +66,8 @@ struct
 
   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

@@ -9,8 +9,12 @@ end
 module type S = functor (Pos: POSITION) ->
 sig
   type !+'a t
-  val of_list : ((Pos.t * Pos.t) * 'a) list -> '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/core/RefineMonad.ml

@@ -174,14 +174,14 @@ let emit_tp loc tp =
   | Some loc ->
     let* env = read in
     let* qtp = quote_tp tp in
-    modify (St.add_metadata (Metadata.TypeAt (loc, Env.pp_env env, qtp)))
+    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 = Metadata.Hole { ctx; tp } in
-    modify (St.add_metadata (Metadata.HoleAt (loc, Env.pp_env env, hole)))
+    let hole = St.Metadata.Hole { ctx; tp } in
+    modify (St.add_hole loc hole)
   | None -> ret ()

src/core/RefineState.ml

@@ -3,22 +3,40 @@ open CodeUnit
 
 module IDMap = Map.Make (CodeUnitID)
 module D = Domain
-module Metadata = RefineMetadata
+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;
-           (** A message queue for emitting events that occured during refinement. *)
-           metadata : Metadata.t list
+           metadata : Metadata.t
          }
 
 let init =
   { code_units = IDMap.empty;
     namespaces = IDMap.empty;
     import_namespaces = IDMap.empty;
-    metadata = []
+    metadata = Metadata.init
   }
 
 let get_unit id st =
@@ -74,8 +92,11 @@ let get_import path st =
 let is_imported path st =
   IDMap.mem path st.code_units
 
-let add_metadata data st =
-  { st with metadata = data :: st.metadata }
+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,6 +1,7 @@
 open Basis
 open CodeUnit
 module D = Domain
+module S = Syntax
 
 type t
 
@@ -25,6 +26,16 @@ val is_imported : id -> t -> bool
 (** Create and add a new code unit. *)
 val init_unit : id -> t -> t
 
-val add_metadata : RefineMetadata.t -> t -> t
 
-val get_metadata  : t -> RefineMetadata.t list
+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

src/server/Actions.ml

@@ -0,0 +1,118 @@
+open Basis
+open Bwd
+open Frontend
+open Core
+open CodeUnit
+open Cubical
+
+module S = Syntax
+module D = Domain
+
+open Lsp.Types
+module Json = Lsp.Import.Json
+
+module LwtIO = Lwt_io
+
+open LspLwt.Notation
+
+(* FIXME: This should live elsewhere, we use this a lot. *)
+let ppenv_bind env ident =
+  Pp.Env.bind env @@ Ident.to_string_opt ident
+
+module Visualize = struct
+  let command_name = "cooltt.visualize"
+  let action_kind = CodeActionKind.Other "cooltt.visualize.hole"
+
+  let serialize_label (str : string) (pos : (string * float) list) : Json.t =
+    `Assoc [
+      "position", `Assoc (List.map (fun (nm, d) -> (nm, `Float d)) pos);
+      "txt", `String str
+    ]
+
+  let dim_tm : S.t -> float =
+    function
+    | S.Dim0 -> -. 1.0
+    | S.Dim1 -> 1.0
+    | _ -> failwith "dim_tm: bad dim"
+
+  let rec dim_from_cof (dims : (string option) bwd) (cof : S.t) : (string * float) list list =
+    match cof with
+    | S.Cof (Cof.Eq (S.Var v, r)) ->
+      let axis = Option.get @@ Bwd.nth dims v in
+      let d = dim_tm r in
+      [[(axis, d)]]
+    | S.Cof (Cof.Join cofs) -> List.concat_map (dim_from_cof dims) cofs
+    | S.Cof (Cof.Meet cofs) -> [List.concat @@ List.concat_map (dim_from_cof dims) cofs]
+    | _ -> failwith "dim_from_cof: bad cof"
+
+  let boundary_labels dims env bdry =
+    let rec go env dims (bdry, cons) =
+      match cons with
+      | S.CofSplit branches ->
+        let (_x, envx) = ppenv_bind env `Anon in
+        List.concat_map (go envx (Snoc (dims, None))) branches
+      | _ ->
+        let (_x, envx) = ppenv_bind env `Anon in
+        let lbl = Format.asprintf "%a" (S.pp envx) cons in
+        List.map (serialize_label lbl) @@ dim_from_cof (Snoc (dims, None)) bdry
+    in
+    match bdry with
+    | S.CofSplit branches ->
+      let (_x, envx) = ppenv_bind env `Anon in
+      List.concat_map (go envx dims) branches
+    | _ -> []
+
+  let serialize_boundary ctx goal : Json.t option =
+    let rec go dims env =
+      function
+      | [] ->
+        begin
+          match goal with
+          | S.Sub (_, _, bdry) ->
+            let dim_names = Bwd.to_list @@ Bwd.filter_map (Option.map (fun name -> `String name)) dims in
+            let labels = boundary_labels dims env bdry in
+            let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in
+            let msg = `Assoc [
+                ("dims", `List dim_names);
+                ("labels", `List labels);
+                ("context", `String context)
+              ]
+            in Some (`Assoc ["DisplayGoal", msg])
+          | _ -> None
+        end
+      | (var, var_tp) :: ctx ->
+        let (dim_name, envx) = ppenv_bind env var in
+        match var_tp with
+        | S.TpDim -> go (Snoc (dims, Some dim_name)) envx ctx
+        | _ -> go (Snoc (dims, None)) envx ctx
+    in go Emp Pp.Env.emp ctx
+
+  let create ctx goal =
+    serialize_boundary ctx goal |> Option.map @@ fun json ->
+    let command = Command.create
+        ~title:"visualize"
+        ~command:command_name
+        ~arguments:[json]
+        ()
+    in CodeAction.create
+      ~title:"visualize hole"
+      ~kind:action_kind
+      ~command
+      ()
+
+  let execute arguments =
+    match arguments with
+    | Some [arg] ->
+      (* FIXME: Handle the visualizer socket better *)
+      let host = Unix.gethostbyname "localhost" in
+      let host_entry = Array.get host.h_addr_list 0 in
+      let addr = Unix.ADDR_INET (host_entry, 3001) in
+      let* (ic, oc) = LwtIO.open_connection addr in
+      let* _ = LwtIO.write oc (Json.to_string arg) in
+      let* _ = LwtIO.flush oc in
+      let* _ = LwtIO.close ic in
+      LwtIO.close oc
+    | _ ->
+      (* FIXME: Handle this better *)
+      Lwt.return ()
+end

src/server/Actions.mli

@@ -0,0 +1,11 @@
+open Basis
+open Core
+open CodeUnit
+
+module Json = Lsp.Import.Json
+
+module Visualize : sig
+  val command_name : string
+  val create : (Ident.t * Syntax.tp) list -> Syntax.tp -> Lsp.Types.CodeAction.t option
+  val execute : Json.t list option -> unit Lwt.t
+end

src/server/Executor.ml

@@ -96,7 +96,7 @@ let elab_decl (st : state) (decl : CS.decl) =
     print_ident st ident
   | _ -> Lwt.return st
 
-let elaborate_file (lib : Bantorra.Manager.library) (path : string) : (Diagnostic.t list * Metadata.t list) Lwt.t =
+let elaborate_file (lib : Bantorra.Manager.library) (path : string) : (Diagnostic.t list * ST.Metadata.t) Lwt.t =
   let open LspLwt.Notation in
   let* sign = parse_file path in
   let unit_id = CodeUnitID.file path in

src/server/Executor.mli

@@ -1,4 +1,4 @@
 open Basis
 open Core
 
-val elaborate_file : Bantorra.Manager.library -> string -> (Lsp.Types.Diagnostic.t list * RefineMetadata.t list) Lwt.t
+val elaborate_file : Bantorra.Manager.library -> string -> (Lsp.Types.Diagnostic.t list * RefineState.Metadata.t) Lwt.t