From 1bab8ffe96f9153334146e108a919fc1b8797ffb Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 12:51:47 -0700 Subject: [PATCH 01/38] Add socket communication code for a cooltt display server --- src/frontend/Server.ml | 31 +++++++++++++++++++++++++++++++ src/frontend/Server.mli | 9 +++++++++ src/frontend/dune | 2 +- 3 files changed, 41 insertions(+), 1 deletion(-) create mode 100644 src/frontend/Server.ml create mode 100644 src/frontend/Server.mli diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml new file mode 100644 index 000000000..d489e7928 --- /dev/null +++ b/src/frontend/Server.ml @@ -0,0 +1,31 @@ +open Core +open CodeUnit + +module S = Syntax + +module J = Ezjsonm + +type t = Unix.file_descr + +let init port = + try + Format.eprintf "Initializing cooltt server connection on port %n...@." port; + let socket = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in + let localhost = Unix.inet_addr_of_string "127.0.0.1" in + let () = Unix.connect socket (Unix.ADDR_INET (localhost, port)) in + Format.eprintf "Cooltt server connection initialized@."; + socket + with Unix.Unix_error (Unix.ECONNREFUSED,_,_) -> + Format.eprintf "Error: Could not initialize cooltt server connection.@."; + failwith "Cooltt server init failed." + +let close socket = + Unix.close socket + +let dispatch_goal socket ctx goal = + (* FIXME: Be smarter about the buffer sizes here. *) + let buf = Buffer.create 65536 in + J.to_buffer ~minify:true buf @@ Serialize.serialize_goal ctx goal; + let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in + Debug.print "Sent %n bytes to Server.@." nbytes; + () diff --git a/src/frontend/Server.mli b/src/frontend/Server.mli new file mode 100644 index 000000000..b16774e8a --- /dev/null +++ b/src/frontend/Server.mli @@ -0,0 +1,9 @@ +open Core +open CodeUnit + +type t + +val init : int -> t +val close : t -> unit + +val dispatch_goal : t -> (Ident.t * Syntax.tp) list -> Syntax.tp -> unit diff --git a/src/frontend/dune b/src/frontend/dune index a13d5edc8..8d5b22b9f 100644 --- a/src/frontend/dune +++ b/src/frontend/dune @@ -6,7 +6,7 @@ (library (name Frontend) - (libraries bantorra cooltt.basis cooltt.cubical cooltt.core menhirLib) + (libraries bantorra cooltt.basis cooltt.cubical cooltt.core ezjsonm menhirLib) (preprocess (pps ppx_deriving.std)) (flags From 856f19b9e56ce18016dec7c2a5cf8eeada7047bc Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 12:52:33 -0700 Subject: [PATCH 02/38] Add syntax for "Probe Holes" --- src/frontend/ConcreteSyntaxData.ml | 1 + src/frontend/Grammar.mly | 3 +++ src/frontend/Lex.mll | 2 ++ 3 files changed, 6 insertions(+) diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index e51de7194..b52dc6cef 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -45,6 +45,7 @@ and con_ = | Type | Hole of string option * con option | BoundaryHole of con option + | ProbeHole | Underscore | Unfold of Ident.t list * con | Generalize of Ident.t * con diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index 4a7f023ba..6ec8a7f99 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -33,6 +33,7 @@ %token NUMERAL %token ATOM %token HOLE_NAME +%token PROBE_HOLE %token LOCKED UNLOCK %token BANG COLON COLON_EQUALS PIPE COMMA DOT DOT_EQUALS SEMI RIGHT_ARROW RRIGHT_ARROW UNDERSCORE DIM COF BOUNDARY %token LPR RPR LBR RBR LSQ RSQ LBANG RBANG @@ -236,6 +237,8 @@ plain_atomic_term_except_name: { Type } | name = HOLE_NAME { Hole (name, None) } + | PROBE_HOLE + { ProbeHole } | DIM { Dim } | COF diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index d2a22f115..59f5e9431 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -170,6 +170,8 @@ and real_token = parse { HOLE_NAME None } | "!" { BANG } + | "!?" + { PROBE_HOLE } | "∂" (* XXX what to do with "∂i"? *) { BOUNDARY } | "#t" From bc5b903beab29df587762ecbd24cb820da1ae74e Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 13:22:41 -0700 Subject: [PATCH 03/38] Use a 'ref' to hold the cooltt server handle --- src/frontend/Server.ml | 44 ++++++++++++++++++++++++++++------------- src/frontend/Server.mli | 8 +++----- 2 files changed, 33 insertions(+), 19 deletions(-) diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index d489e7928..ab615598b 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -5,7 +5,11 @@ module S = Syntax module J = Ezjsonm -type t = Unix.file_descr +(* [NOTE: Cooltt Server] + We use a 'ref' here to prevent having to thread down a server handle + deep into the guts of the elaborator. *) +let server : Unix.file_descr option ref = + ref None let init port = try @@ -14,18 +18,30 @@ let init port = let localhost = Unix.inet_addr_of_string "127.0.0.1" in let () = Unix.connect socket (Unix.ADDR_INET (localhost, port)) in Format.eprintf "Cooltt server connection initialized@."; - socket - with Unix.Unix_error (Unix.ECONNREFUSED,_,_) -> - Format.eprintf "Error: Could not initialize cooltt server connection.@."; - failwith "Cooltt server init failed." + server := Some socket + with Unix.Unix_error _ -> + Format.eprintf "Error: Could not initialize cooltt server connection.@." -let close socket = - Unix.close socket +let close () = + match !server with + | Some socket -> + Unix.close socket; + server := None + | None -> () -let dispatch_goal socket ctx goal = - (* FIXME: Be smarter about the buffer sizes here. *) - let buf = Buffer.create 65536 in - J.to_buffer ~minify:true buf @@ Serialize.serialize_goal ctx goal; - let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in - Debug.print "Sent %n bytes to Server.@." nbytes; - () +let dispatch_goal ctx goal = + match !server with + | Some socket -> + begin + try + (* FIXME: Be smarter about the buffer sizes here. *) + let buf = Buffer.create 65536 in + J.to_buffer ~minify:true buf @@ Serialize.serialize_goal ctx goal; + let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in + Debug.print "Sent %n bytes to Server.@." nbytes; + () + with Unix.Unix_error _ -> + Format.eprintf "Cooltt server connection lost.@."; + close () + end + | None -> () diff --git a/src/frontend/Server.mli b/src/frontend/Server.mli index b16774e8a..de2164603 100644 --- a/src/frontend/Server.mli +++ b/src/frontend/Server.mli @@ -1,9 +1,7 @@ open Core open CodeUnit -type t +val init : int -> unit +val close : unit -> unit -val init : int -> t -val close : t -> unit - -val dispatch_goal : t -> (Ident.t * Syntax.tp) list -> Syntax.tp -> unit +val dispatch_goal : (Ident.t * Syntax.tp) list -> Syntax.tp -> unit From 331d422696a649845b2ef5248b12de1ca72dbc85 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 13:23:15 -0700 Subject: [PATCH 04/38] Add 'probe_goal' family of tactics --- src/core/Refiner.ml | 44 +++++++++++++++++++++++++++++--------------- src/core/Refiner.mli | 5 +++++ 2 files changed, 34 insertions(+), 15 deletions(-) diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 49761fddd..3215af879 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -68,14 +68,13 @@ module Probe : sig val probe_chk : string option -> T.Chk.tac -> T.Chk.tac val probe_boundary : T.Chk.tac -> T.Chk.tac -> T.Chk.tac val probe_syn : string option -> T.Syn.tac -> T.Syn.tac + + val probe_goal_chk : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> T.Chk.tac -> T.Chk.tac + val probe_goal_syn : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> T.Syn.tac -> T.Syn.tac end = struct - let print_state lbl tp : unit m = + let print_state lbl ctx tp : unit m = let* env = RM.read in - let cells = Env.locals env in - - RM.globally @@ - let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in () |> RM.emit (RefineEnv.location env) @@ fun fmt () -> Format.fprintf fmt "Emitted hole:@, @[%a@]@." (S.pp_sequent ~lbl ctx) tp @@ -98,15 +97,36 @@ struct () |> RM.emit (RefineEnv.location env) @@ fun fmt () -> Format.fprintf fmt "Emitted hole:@, @[%a@]@." (S.pp_partial_sequent bdry_sat ctx) (tm, stp) - let probe_chk name tac = - T.Chk.brule ~name:"probe_chk" @@ fun (tp, phi, clo) -> + let probe_goal_chk k tac = + T.Chk.brule ~name:"probe_goal_chk" @@ fun (tp, phi, clo) -> let* s = T.Chk.brun tac (tp, phi, clo) in let+ () = let* stp = RM.quote_tp @@ D.Sub (tp, phi, clo) in - print_state name stp + + let* env = RM.read in + let cells = Env.locals env in + RM.globally @@ + let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in + k ctx stp in s + let probe_goal_syn k tac = + T.Syn.rule ~name:"probe_goal_syn" @@ + let* s, tp = T.Syn.run tac in + let+ () = + let* stp = RM.quote_tp tp in + let* env = RM.read in + let cells = Env.locals env in + RM.globally @@ + let* ctx = GlobalUtil.destruct_cells @@ Bwd.to_list cells in + k ctx stp + in + s, tp + + let probe_chk name tac = + probe_goal_chk (print_state name) tac + let probe_boundary probe tac = T.Chk.brule ~name:"probe_boundary" @@ fun (tp, phi, clo) -> let* probe_tm = T.Chk.run probe tp in @@ -114,13 +134,7 @@ struct T.Chk.brun tac (tp, phi, clo) let probe_syn name tac = - T.Syn.rule ~name:"probe_syn" @@ - let* s, tp = T.Syn.run tac in - let+ () = - let* stp = RM.quote_tp tp in - print_state name stp - in - s, tp + probe_goal_syn (print_state name) tac end diff --git a/src/core/Refiner.mli b/src/core/Refiner.mli index 30d0f64b9..5478f7bce 100644 --- a/src/core/Refiner.mli +++ b/src/core/Refiner.mli @@ -1,6 +1,8 @@ (** This is the basis of trusted inference rules for cooltt. This module also contains some auxiliary tactics, but these don't need to be trusted so they should be moved elsewhere. *) +open CodeUnit + module D := Domain module S := Syntax module RM := Monads.RefineM @@ -23,6 +25,9 @@ module Probe : sig val probe_chk : string option -> Chk.tac -> Chk.tac val probe_boundary : Chk.tac -> Chk.tac -> Chk.tac val probe_syn : string option -> Syn.tac -> Syn.tac + + val probe_goal_chk : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> Chk.tac -> Chk.tac + val probe_goal_syn : ((Ident.t * S.tp) list -> S.tp -> unit RM.m) -> Syn.tac -> Syn.tac end module Dim : sig From 2eb241fdde12b23c6313cf90a92db1437cd6260e Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 13:24:19 -0700 Subject: [PATCH 05/38] Add server communication inside elaborator --- src/frontend/Elaborator.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 1df594007..1d22646d0 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -212,6 +212,7 @@ and chk_tm : CS.con -> T.Chk.tac = | CS.Hole (name, Some con) -> Refiner.Probe.probe_chk name @@ chk_tm con | CS.BoundaryHole None -> Refiner.Hole.unleash_hole None | CS.BoundaryHole (Some con) -> Refiner.Probe.probe_boundary (chk_tm con) (Refiner.Hole.silent_hole None) + | CS.ProbeHole -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) @@ Refiner.Hole.unleash_hole None | CS.Unfold (idents, c) -> (* TODO: move to a trusted rule *) T.Chk.brule @@ From bba971395c114533b45519c7565703db6894aab9 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 13:24:33 -0700 Subject: [PATCH 06/38] Server initialization + command line args --- src/bin/main.ml | 22 ++++++++++++++-------- src/frontend/Driver.ml | 10 ++++++++-- src/frontend/Driver.mli | 9 +++++++-- 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/bin/main.ml b/src/bin/main.ml index 1a3d429ef..cb2979d30 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -9,14 +9,15 @@ type options = { mode : [`Interactive | `Scripting of [`Stdin | `File of string]]; as_file : string option; width : int; - debug_mode : bool } + debug_mode : bool; + server_port : int option } -let main {mode; as_file; width; debug_mode} = +let main {mode; as_file; width; debug_mode; server_port} = 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; server_port} + | `Scripting input -> Driver.load_file {as_file; debug_mode; server_port} input with | Ok () -> `Ok () | Error () -> `Error (false, "encountered one or more errors") @@ -53,6 +54,11 @@ let opt_debug = in Arg.(value & flag & info ["debug"] ~doc) +let opt_server = + let doc = "Enable the cooltt hole server." + in + Arg.(value & opt (some int) None & info ["server"] ~doc ~docv:"PORT") + let myinfo = let doc = "elaborate and normalize terms in Cartesian cubical type theory" in let err_exit = Term.exit_info ~doc:"on ill-formed types or terms." 1 in @@ -67,14 +73,14 @@ let parse_mode = let quote s = "`" ^ s ^ "'" -let consolidate_options mode interactive width input_file as_file debug_mode : options Term.ret = +let consolidate_options mode interactive width input_file as_file debug_mode server_port : 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} + `Ok {mode = `Scripting input_file; as_file; width; debug_mode; server_port} | (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} + `Ok {mode = `Interactive; as_file; width; debug_mode; server_port} | Some `Interactive, _, _, Some _ | None, true, _, _ -> `Error (true, "interactive mode expects no input files") | Some `Scripting, true, _, _ -> @@ -84,7 +90,7 @@ let consolidate_options mode interactive width input_file as_file debug_mode : o 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)) + Term.(ret (const consolidate_options $ opt_mode $ opt_interactive $ opt_width $ opt_input_file $ opt_as_file $ opt_debug $ opt_server)) in let t = Term.ret @@ Term.(const main $ options) in Term.exit @@ Term.eval ~catch:true ~err:Format.std_formatter (t, myinfo) diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml index 8f8f0b7d6..56d53c434 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -16,6 +16,11 @@ module ST = RefineState module RMU = Monad.Util (RM) open Monad.Notation (RM) +type options = + { as_file : string option; + debug_mode : bool; + server_port : int option } + type status = (unit, unit) Result.t type continuation = Continue of (status RM.m -> status RM.m) | Quit type command = continuation RM.m @@ -209,11 +214,12 @@ and process_file input = Log.pp_error_message ~loc:(Some err.span) ~lvl:`Error pp_message @@ ErrorMessage {error = LexingError; last_token = err.last_token}; RM.ret @@ Error () -let load_file ~as_file ~debug_mode input = +let load_file {as_file; debug_mode; server_port} input = match load_current_library ~as_file input with | Error () -> Error () | Ok lib -> Debug.debug_mode debug_mode; + Option.iter Server.init server_port; let unit_id = assign_unit_id ~as_file input in RM.run_exn ST.init (Env.init lib) @@ RM.with_code_unit lib unit_id @@ @@ -244,7 +250,7 @@ let rec repl lib (ch : in_channel) lexbuf = close_in ch; RM.ret @@ Ok () -let do_repl ~as_file ~debug_mode = +let do_repl {as_file; debug_mode; _} = match load_current_library ~as_file `Stdin with | Error () -> Error () | Ok lib -> diff --git a/src/frontend/Driver.mli b/src/frontend/Driver.mli index 64506c06c..3535b5109 100644 --- a/src/frontend/Driver.mli +++ b/src/frontend/Driver.mli @@ -1,4 +1,9 @@ (* This is the top-level driver for the proof assistant. *) -val load_file : as_file:string option -> debug_mode:bool -> [`Stdin | `File of string] -> (unit, unit) result -val do_repl : as_file:string option -> debug_mode:bool -> (unit, unit) result +type options = + { as_file : string option; + debug_mode : bool; + server_port : int option } + +val load_file : options -> [`Stdin | `File of string] -> (unit, unit) result +val do_repl : options -> (unit, unit) result From e42d97071cbd7c7615289d059cc8f769872dfd0c Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Tue, 10 Aug 2021 13:24:49 -0700 Subject: [PATCH 07/38] Fix issue with emacs mode + extra args --- emacs/cooltt.el | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/emacs/cooltt.el b/emacs/cooltt.el index 43a7e5c74..c24cea32d 100644 --- a/emacs/cooltt.el +++ b/emacs/cooltt.el @@ -179,7 +179,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)) From 115b838e111d5f25c571e3bf18fdad5cba14b260 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 26 Aug 2021 14:59:37 -0700 Subject: [PATCH 08/38] Update protocol to perform more heavy lifting on the cooltt side --- src/frontend/Server.ml | 83 +++++++++++++++++++++++++++++++++++++++--- test/Test.ml | 4 +- 2 files changed, 81 insertions(+), 6 deletions(-) diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index ab615598b..511e1f1ba 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -1,5 +1,9 @@ +open Basis +open Bwd + open Core open CodeUnit +open Cubical module S = Syntax @@ -29,14 +33,83 @@ let close () = server := None | None -> () +let ppenv_bind env ident = + Pp.Env.bind env @@ Ident.to_string_opt ident + +let serialize_label (n : int) (str : string) (axes : (int * float) list) : J.value = + let pos = Array.make n (J.float 0.0) in + let _ = axes |> List.iter @@ fun (dim, p) -> + Array.set pos dim (J.float p) + in + `O [("position", `A (Array.to_list pos)); ("txt", `String str)] + +let dim_tm : S.t -> float = + function + | S.Dim0 -> -. 1.0 + | S.Dim1 -> 1.0 + | _ -> failwith "dim_tm: bad dim" + +(* Fetch a list of label positions from a cofibration. *) +let rec dim_from_cof (dims : (int option) bwd) (cof : S.t) : (int * 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" + +(* Create our list of labels from a boundary constraint. *) +let boundary_labels (num_dims : int) (dims : (int option) bwd) (env : Pp.env) (tm : S.t) : J.value list = + 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 num_dims lbl) @@ dim_from_cof (Snoc (dims, None)) bdry + in + match tm with + | S.CofSplit branches -> + let (_x, envx) = ppenv_bind env `Anon in + List.concat_map (go envx dims) branches + | _ -> [] + +let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = + let rec go dim_count dims env = + function + | [] -> + begin + match goal with + | S.Sub (_, _, bdry) -> + let num_dims = Bwd.length @@ Bwd.filter Option.is_some dims in + let labels = boundary_labels num_dims dims env bdry in + let context = Format.asprintf "%a" (S.pp_sequent ~lbl:None ctx) goal in + let msg = `O [ + ("dim", J.float @@ Int.to_float num_dims); + ("labels", `A labels); + ("context", `String context) + ] in + Some (`O [("DisplayGoal", msg)]) + | _ -> None + end + | (var, var_tp) :: ctx -> + let (_x, envx) = ppenv_bind env var in + match var_tp with + | S.TpDim -> go (dim_count + 1) (Snoc (dims, Some dim_count)) envx ctx + | _ -> go dim_count (Snoc (dims, None)) envx ctx + in go 0 Emp Pp.Env.emp ctx + let dispatch_goal ctx goal = - match !server with - | Some socket -> + match !server, serialize_boundary ctx goal with + | Some socket, Some msg -> begin try - (* FIXME: Be smarter about the buffer sizes here. *) let buf = Buffer.create 65536 in - J.to_buffer ~minify:true buf @@ Serialize.serialize_goal ctx goal; + J.to_buffer ~minify:true buf msg; let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in Debug.print "Sent %n bytes to Server.@." nbytes; () @@ -44,4 +117,4 @@ let dispatch_goal ctx goal = Format.eprintf "Cooltt server connection lost.@."; close () end - | None -> () + | _, _ -> () diff --git a/test/Test.ml b/test/Test.ml index 55838d0b5..6adaee535 100644 --- a/test/Test.ml +++ b/test/Test.ml @@ -1,4 +1,5 @@ open Frontend +open Driver let header fname = String.make 20 '-' ^ "[" ^ fname ^ "]" ^ String.make 20 '-' ^ "\n" @@ -6,7 +7,8 @@ let header fname = let execute_file fname = if String.equal (Filename.extension fname) ".cooltt" then let _ = print_string (header fname) in - ignore @@ Driver.load_file ~as_file:None ~debug_mode:false (`File fname) + let opts = { as_file = None; debug_mode = false; server_port = None } in + ignore @@ Driver.load_file opts (`File fname) let () = let cooltt_files = Sys.readdir "." in From f2b3c71e4d53afead817c08d0614538bcc4911b9 Mon Sep 17 00:00:00 2001 From: favonia Date: Thu, 26 Aug 2021 22:38:40 -0500 Subject: [PATCH 09/38] Update zsh completion --- zsh/_cooltt | 1 + 1 file changed, 1 insertion(+) diff --git a/zsh/_cooltt b/zsh/_cooltt index 2ccfb2584..4c107060e 100644 --- a/zsh/_cooltt +++ b/zsh/_cooltt @@ -8,4 +8,5 @@ _arguments ':' \ '(- :)--version[show version]' \ '(-w --width)'{-w,--width=}'[specify width for pretty printing]:width:' \ '(--debug)--debug[enable debug mode]' \ + '(--server)--server=[enable cooltt server]:port:' \ "1:CoolTT file:_files -g '*.cooltt'" From 5a8aeb111abb6ebf136e5d0103a0a630e1501d06 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 2 Sep 2021 10:02:35 -0700 Subject: [PATCH 10/38] Replace ProbeHole with Visualize --- src/frontend/ConcreteSyntaxData.ml | 2 +- src/frontend/Elaborator.ml | 2 +- src/frontend/Grammar.mly | 6 +++--- src/frontend/Lex.mll | 3 +-- 4 files changed, 6 insertions(+), 7 deletions(-) diff --git a/src/frontend/ConcreteSyntaxData.ml b/src/frontend/ConcreteSyntaxData.ml index b52dc6cef..5b2275c5b 100644 --- a/src/frontend/ConcreteSyntaxData.ml +++ b/src/frontend/ConcreteSyntaxData.ml @@ -45,7 +45,7 @@ and con_ = | Type | Hole of string option * con option | BoundaryHole of con option - | ProbeHole + | Visualize | Underscore | Unfold of Ident.t list * con | Generalize of Ident.t * con diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 1d22646d0..2645a3282 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -212,7 +212,7 @@ and chk_tm : CS.con -> T.Chk.tac = | CS.Hole (name, Some con) -> Refiner.Probe.probe_chk name @@ chk_tm con | CS.BoundaryHole None -> Refiner.Hole.unleash_hole None | CS.BoundaryHole (Some con) -> Refiner.Probe.probe_boundary (chk_tm con) (Refiner.Hole.silent_hole None) - | CS.ProbeHole -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) @@ Refiner.Hole.unleash_hole None + | CS.Visualize -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) @@ Refiner.Hole.unleash_hole None | CS.Unfold (idents, c) -> (* TODO: move to a trusted rule *) T.Chk.brule @@ diff --git a/src/frontend/Grammar.mly b/src/frontend/Grammar.mly index 6ec8a7f99..d8b3ac09d 100644 --- a/src/frontend/Grammar.mly +++ b/src/frontend/Grammar.mly @@ -33,7 +33,6 @@ %token NUMERAL %token ATOM %token HOLE_NAME -%token PROBE_HOLE %token LOCKED UNLOCK %token BANG COLON COLON_EQUALS PIPE COMMA DOT DOT_EQUALS SEMI RIGHT_ARROW RRIGHT_ARROW UNDERSCORE DIM COF BOUNDARY %token LPR RPR LBR RBR LSQ RSQ LBANG RBANG @@ -47,6 +46,7 @@ %token EXT %token COE COM HCOM HFILL %token QUIT NORMALIZE PRINT DEF AXIOM FAIL +%token VISUALIZE %token IMPORT %token ELIM %token SEMISEMI EOF @@ -237,8 +237,8 @@ plain_atomic_term_except_name: { Type } | name = HOLE_NAME { Hole (name, None) } - | PROBE_HOLE - { ProbeHole } + | VISUALIZE + { Visualize } | DIM { Dim } | COF diff --git a/src/frontend/Lex.mll b/src/frontend/Lex.mll index 5a0aa7953..c4f688165 100644 --- a/src/frontend/Lex.mll +++ b/src/frontend/Lex.mll @@ -22,6 +22,7 @@ let commands = ("#fail", FAIL); ("#normalize", NORMALIZE); ("#print", PRINT); + ("#viz", VISUALIZE); ("#quit", QUIT); ] @@ -174,8 +175,6 @@ and real_token = parse { HOLE_NAME None } | "!" { BANG } - | "!?" - { PROBE_HOLE } | "∂" (* XXX what to do with "∂i"? *) { BOUNDARY } | "true" | "⊤" From c30a9406e6b2cbd8a934d7734015e8e3b278a480 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 2 Sep 2021 10:07:02 -0700 Subject: [PATCH 11/38] Update syntax highlighting --- emacs/cooltt.el | 2 +- vim/syntax/cooltt.vim | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/emacs/cooltt.el b/emacs/cooltt.el index 285dd23b9..4c2d36ce0 100644 --- a/emacs/cooltt.el +++ b/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 diff --git a/vim/syntax/cooltt.vim b/vim/syntax/cooltt.vim index 0a6de9240..006db420f 100644 --- a/vim/syntax/cooltt.vim +++ b/vim/syntax/cooltt.vim @@ -26,7 +26,7 @@ syn keyword coolttKeyw locked unlock zero suc nat in fst snd elim unfold general syn keyword coolttKeyw cof sub ext coe hcom com hfill V vproj with struct sig syn keyword coolttDecl def axiom let import -syn keyword coolttCmd #normalize #print #quit #fail +syn keyword coolttCmd #normalize #print #quit #fail #viz syn match coolttSymb '=>\|[|,*×:;=≔_𝕀𝔽∂∧∨→⇒!]\|->\|tt\|ff\|⊤\|⊥' syn match coolttSymb '\\/\|/\\' From 10e4fffebeea9001294b0a4903798fbe6c24b55a Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 2 Sep 2021 11:16:02 -0700 Subject: [PATCH 12/38] Add ability to pass in server hostname, rework options handling a bit --- src/bin/main.ml | 70 +++++++++++++++++++++++++++-------------- src/frontend/Driver.ml | 6 ++-- src/frontend/Driver.mli | 2 +- src/frontend/Server.ml | 15 ++++++--- src/frontend/Server.mli | 2 +- 5 files changed, 62 insertions(+), 33 deletions(-) diff --git a/src/bin/main.ml b/src/bin/main.ml index cb2979d30..93b6b0201 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -5,19 +5,28 @@ let _ = Printexc.record_backtrace false; () +type mode = + [ `Interactive + | `Scripting of [`Stdin | `File of string] + ] + type options = - { mode : [`Interactive | `Scripting of [`Stdin | `File of string]]; + { mode : mode; as_file : string option; width : int; debug_mode : bool; - server_port : int option } + server_info : (string * int) option; + } + +let options mode as_file width debug_mode server_info = + { mode; as_file; width; debug_mode; server_info } -let main {mode; as_file; width; debug_mode; server_port} = +let main {mode; as_file; width; debug_mode; server_info} = Format.set_margin width; match match mode with - | `Interactive -> Driver.do_repl {as_file; debug_mode; server_port} - | `Scripting input -> Driver.load_file {as_file; debug_mode; server_port} input + | `Interactive -> Driver.do_repl {as_file; debug_mode; server_info} + | `Scripting input -> Driver.load_file {as_file; debug_mode; server_info} input with | Ok () -> `Ok () | Error () -> `Error (false, "encountered one or more errors") @@ -57,7 +66,17 @@ let opt_debug = let opt_server = let doc = "Enable the cooltt hole server." in - Arg.(value & opt (some int) None & info ["server"] ~doc ~docv:"PORT") + Arg.(value & flag & info ["server"] ~doc) + +let opt_server_hostname = + let doc = "The cooltt hole server hostname. If --server is not enabled, this does nothing." + in + Arg.(value & opt string "localhost" & info ["server-hostname"] ~doc ~docv:"HOSTNAME") + +let opt_server_port = + let doc = "The cooltt hole server port. If --server is not enabled, this does nothing." + in + Arg.(value & opt int 3001 & info ["server-port"] ~doc ~docv:"PORT") let myinfo = let doc = "elaborate and normalize terms in Cartesian cubical type theory" in @@ -73,24 +92,29 @@ let parse_mode = let quote s = "`" ^ s ^ "'" -let consolidate_options mode interactive width input_file as_file debug_mode server_port : 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; server_port} - | (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; server_port} - | 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 `Interactive, _, Some _ | None, true, _ -> + Error (`Msg "interactive mode expects no input files") + | Some `Scripting, true, _ -> + Error (`Msg "inconsistent mode assignment") + | Some (`Nonexistent s), _, _ -> + Error (`Msg ("no mode named " ^ quote s)) + +let consolidate_server_options server_enabled server_host server_port = + if server_enabled + then Some (server_host, server_port) + else None 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 $ opt_server)) - in + let opts_input = Term.(term_result ~usage:true (const consolidate_input_options $ opt_mode $ opt_interactive $ opt_input_file)) in + let opts_server = Term.(const consolidate_server_options $ opt_server $ opt_server_hostname $ opt_server_port) in + let options : options Term.t = Term.(const options $ opts_input $ opt_as_file $ opt_width $ opt_debug $ opts_server) in let t = Term.ret @@ Term.(const main $ options) in Term.exit @@ Term.eval ~catch:true ~err:Format.std_formatter (t, myinfo) diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml index 56d53c434..b3ad98694 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -19,7 +19,7 @@ open Monad.Notation (RM) type options = { as_file : string option; debug_mode : bool; - server_port : int option } + server_info : (string * int) option } type status = (unit, unit) Result.t type continuation = Continue of (status RM.m -> status RM.m) | Quit @@ -214,12 +214,12 @@ and process_file input = Log.pp_error_message ~loc:(Some err.span) ~lvl:`Error pp_message @@ ErrorMessage {error = LexingError; last_token = err.last_token}; RM.ret @@ Error () -let load_file {as_file; debug_mode; server_port} input = +let load_file {as_file; debug_mode; server_info} input = match load_current_library ~as_file input with | Error () -> Error () | Ok lib -> Debug.debug_mode debug_mode; - Option.iter Server.init server_port; + Option.iter (fun (hostname, port) -> Server.init hostname port) server_info; let unit_id = assign_unit_id ~as_file input in RM.run_exn ST.init (Env.init lib) @@ RM.with_code_unit lib unit_id @@ diff --git a/src/frontend/Driver.mli b/src/frontend/Driver.mli index 3535b5109..0fa4862a4 100644 --- a/src/frontend/Driver.mli +++ b/src/frontend/Driver.mli @@ -3,7 +3,7 @@ type options = { as_file : string option; debug_mode : bool; - server_port : int option } + server_info : (string * int) option } val load_file : options -> [`Stdin | `File of string] -> (unit, unit) result val do_repl : options -> (unit, unit) result diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index 511e1f1ba..9254d0203 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -15,14 +15,19 @@ module J = Ezjsonm let server : Unix.file_descr option ref = ref None -let init port = +let init host_name port = try Format.eprintf "Initializing cooltt server connection on port %n...@." port; let socket = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in - let localhost = Unix.inet_addr_of_string "127.0.0.1" in - let () = Unix.connect socket (Unix.ADDR_INET (localhost, port)) in - Format.eprintf "Cooltt server connection initialized@."; - server := Some socket + let host_entry = Unix.gethostbyname host_name in + begin + match CCArray.get_safe host_entry.h_addr_list 0 with + | Some addr -> + let () = Unix.connect socket (Unix.ADDR_INET (addr, port)) in + Format.eprintf "Cooltt server connection initialized@."; + server := Some socket + | None -> Format.eprintf "Error: Could not initialize cooltt server connection.@." + end with Unix.Unix_error _ -> Format.eprintf "Error: Could not initialize cooltt server connection.@." diff --git a/src/frontend/Server.mli b/src/frontend/Server.mli index de2164603..bc694a535 100644 --- a/src/frontend/Server.mli +++ b/src/frontend/Server.mli @@ -1,7 +1,7 @@ open Core open CodeUnit -val init : int -> unit +val init : string -> int -> unit val close : unit -> unit val dispatch_goal : (Ident.t * Syntax.tp) list -> Syntax.tp -> unit From a5681299ee1ef2b0d36d479ccd9ce857d7f7e0ca Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 22 Sep 2021 11:33:00 -0700 Subject: [PATCH 13/38] Update message format to track changes to coolttviz --- src/frontend/Server.ml | 30 +++++++++++++----------------- 1 file changed, 13 insertions(+), 17 deletions(-) diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml index 9254d0203..7d5b7b60b 100644 --- a/src/frontend/Server.ml +++ b/src/frontend/Server.ml @@ -41,12 +41,8 @@ let close () = let ppenv_bind env ident = Pp.Env.bind env @@ Ident.to_string_opt ident -let serialize_label (n : int) (str : string) (axes : (int * float) list) : J.value = - let pos = Array.make n (J.float 0.0) in - let _ = axes |> List.iter @@ fun (dim, p) -> - Array.set pos dim (J.float p) - in - `O [("position", `A (Array.to_list pos)); ("txt", `String str)] +let serialize_label (str : string) (pos : (string * float) list) : J.value = + `O [("position", `O (List.map (fun (nm, d) -> (nm, J.float d)) pos)); ("txt", `String str)] let dim_tm : S.t -> float = function @@ -55,7 +51,7 @@ let dim_tm : S.t -> float = | _ -> failwith "dim_tm: bad dim" (* Fetch a list of label positions from a cofibration. *) -let rec dim_from_cof (dims : (int option) bwd) (cof : S.t) : (int * float) list list = +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 @@ -66,7 +62,7 @@ let rec dim_from_cof (dims : (int option) bwd) (cof : S.t) : (int * float) list | _ -> failwith "dim_from_cof: bad cof" (* Create our list of labels from a boundary constraint. *) -let boundary_labels (num_dims : int) (dims : (int option) bwd) (env : Pp.env) (tm : S.t) : J.value list = +let boundary_labels (dims : (string option) bwd) (env : Pp.env) (tm : S.t) : J.value list = let rec go env dims (bdry, cons) = match cons with | S.CofSplit branches -> @@ -75,7 +71,7 @@ let boundary_labels (num_dims : int) (dims : (int option) bwd) (env : Pp.env) (t | _ -> let (_x, envx) = ppenv_bind env `Anon in let lbl = Format.asprintf "%a" (S.pp envx) cons in - List.map (serialize_label num_dims lbl) @@ dim_from_cof (Snoc (dims, None)) bdry + List.map (serialize_label lbl) @@ dim_from_cof (Snoc (dims, None)) bdry in match tm with | S.CofSplit branches -> @@ -84,17 +80,17 @@ let boundary_labels (num_dims : int) (dims : (int option) bwd) (env : Pp.env) (t | _ -> [] let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = - let rec go dim_count dims env = + let rec go dims env = function | [] -> begin match goal with | S.Sub (_, _, bdry) -> - let num_dims = Bwd.length @@ Bwd.filter Option.is_some dims in - let labels = boundary_labels num_dims dims env bdry in + let dim_names = Bwd.to_list @@ Bwd.filter_map Fun.id 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 = `O [ - ("dim", J.float @@ Int.to_float num_dims); + ("dims", `A (List.map J.string dim_names)); ("labels", `A labels); ("context", `String context) ] in @@ -102,11 +98,11 @@ let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option | _ -> None end | (var, var_tp) :: ctx -> - let (_x, envx) = ppenv_bind env var in + let (dim_name, envx) = ppenv_bind env var in match var_tp with - | S.TpDim -> go (dim_count + 1) (Snoc (dims, Some dim_count)) envx ctx - | _ -> go dim_count (Snoc (dims, None)) envx ctx - in go 0 Emp Pp.Env.emp ctx + | S.TpDim -> go (Snoc (dims, Some dim_name)) envx ctx + | _ -> go (Snoc (dims, None)) envx ctx + in go Emp Pp.Env.emp ctx let dispatch_goal ctx goal = match !server, serialize_boundary ctx goal with From 36717bdf643d9191162a3dc63a59a86a116d9f1a Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Thu, 23 Sep 2021 09:31:37 -0700 Subject: [PATCH 14/38] Fix Test Suite --- test/Test.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test/Test.ml b/test/Test.ml index b379c64b8..9dcf43c67 100644 --- a/test/Test.ml +++ b/test/Test.ml @@ -8,7 +8,7 @@ let execute_file fname = if String.equal (Filename.extension fname) ".cooltt" then try let _ = print_string (header fname) in - let opts = { as_file = None; debug_mode = false; server_port = None } in + let opts = { as_file = None; debug_mode = false; server_info = None } in ignore @@ Driver.load_file opts (`File fname) with e -> From 3d8480ae39f4b096585e7e9c405fd2f0117f7ce3 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 08:52:08 -0800 Subject: [PATCH 15/38] Remove old server code --- src/frontend/Elaborator.ml | 2 +- src/frontend/Server.ml | 121 ------------------------------------- src/frontend/Server.mli | 7 --- test/Test.ml | 2 +- 4 files changed, 2 insertions(+), 130 deletions(-) delete mode 100644 src/frontend/Server.ml delete mode 100644 src/frontend/Server.mli diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index 2645a3282..ebaf4fe8b 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -212,7 +212,7 @@ and chk_tm : CS.con -> T.Chk.tac = | CS.Hole (name, Some con) -> Refiner.Probe.probe_chk name @@ chk_tm con | CS.BoundaryHole None -> Refiner.Hole.unleash_hole None | CS.BoundaryHole (Some con) -> Refiner.Probe.probe_boundary (chk_tm con) (Refiner.Hole.silent_hole None) - | CS.Visualize -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret @@ Server.dispatch_goal ctx goal) @@ Refiner.Hole.unleash_hole None + | CS.Visualize -> Refiner.Probe.probe_goal_chk (fun ctx goal -> RM.ret ()) @@ Refiner.Hole.unleash_hole None | CS.Unfold (idents, c) -> (* TODO: move to a trusted rule *) T.Chk.brule @@ diff --git a/src/frontend/Server.ml b/src/frontend/Server.ml deleted file mode 100644 index 7d5b7b60b..000000000 --- a/src/frontend/Server.ml +++ /dev/null @@ -1,121 +0,0 @@ -open Basis -open Bwd - -open Core -open CodeUnit -open Cubical - -module S = Syntax - -module J = Ezjsonm - -(* [NOTE: Cooltt Server] - We use a 'ref' here to prevent having to thread down a server handle - deep into the guts of the elaborator. *) -let server : Unix.file_descr option ref = - ref None - -let init host_name port = - try - Format.eprintf "Initializing cooltt server connection on port %n...@." port; - let socket = Unix.socket Unix.PF_INET Unix.SOCK_STREAM 0 in - let host_entry = Unix.gethostbyname host_name in - begin - match CCArray.get_safe host_entry.h_addr_list 0 with - | Some addr -> - let () = Unix.connect socket (Unix.ADDR_INET (addr, port)) in - Format.eprintf "Cooltt server connection initialized@."; - server := Some socket - | None -> Format.eprintf "Error: Could not initialize cooltt server connection.@." - end - with Unix.Unix_error _ -> - Format.eprintf "Error: Could not initialize cooltt server connection.@." - -let close () = - match !server with - | Some socket -> - Unix.close socket; - server := None - | None -> () - -let ppenv_bind env ident = - Pp.Env.bind env @@ Ident.to_string_opt ident - -let serialize_label (str : string) (pos : (string * float) list) : J.value = - `O [("position", `O (List.map (fun (nm, d) -> (nm, J.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" - -(* Fetch a list of label positions from a cofibration. *) -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" - -(* Create our list of labels from a boundary constraint. *) -let boundary_labels (dims : (string option) bwd) (env : Pp.env) (tm : S.t) : J.value list = - 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 tm with - | S.CofSplit branches -> - let (_x, envx) = ppenv_bind env `Anon in - List.concat_map (go envx dims) branches - | _ -> [] - -let serialize_boundary (ctx : (Ident.t * S.tp) list) (goal : S.tp) : J.t option = - let rec go dims env = - function - | [] -> - begin - match goal with - | S.Sub (_, _, bdry) -> - let dim_names = Bwd.to_list @@ Bwd.filter_map Fun.id 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 = `O [ - ("dims", `A (List.map J.string dim_names)); - ("labels", `A labels); - ("context", `String context) - ] in - Some (`O [("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 dispatch_goal ctx goal = - match !server, serialize_boundary ctx goal with - | Some socket, Some msg -> - begin - try - let buf = Buffer.create 65536 in - J.to_buffer ~minify:true buf msg; - let nbytes = Unix.send socket (Buffer.to_bytes buf) 0 (Buffer.length buf) [] in - Debug.print "Sent %n bytes to Server.@." nbytes; - () - with Unix.Unix_error _ -> - Format.eprintf "Cooltt server connection lost.@."; - close () - end - | _, _ -> () diff --git a/src/frontend/Server.mli b/src/frontend/Server.mli deleted file mode 100644 index bc694a535..000000000 --- a/src/frontend/Server.mli +++ /dev/null @@ -1,7 +0,0 @@ -open Core -open CodeUnit - -val init : string -> int -> unit -val close : unit -> unit - -val dispatch_goal : (Ident.t * Syntax.tp) list -> Syntax.tp -> unit diff --git a/test/Test.ml b/test/Test.ml index 9dcf43c67..850e47f52 100644 --- a/test/Test.ml +++ b/test/Test.ml @@ -8,7 +8,7 @@ let execute_file fname = if String.equal (Filename.extension fname) ".cooltt" then try let _ = print_string (header fname) in - let opts = { as_file = None; debug_mode = false; server_info = None } in + let opts = { as_file = None; debug_mode = false; } in ignore @@ Driver.load_file opts (`File fname) with e -> From 2777db2a6c2a29d345f27b33076cb6e73e6fea49 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 08:53:05 -0800 Subject: [PATCH 16/38] Add a message queue for emitting metadata from the refiner --- src/basis/JobQueue.ml | 52 ++++++++++++++++++++++++++++++++++++++++ src/basis/JobQueue.mli | 31 ++++++++++++++++++++++++ src/basis/dune | 2 +- src/core/RefineMonad.ml | 11 +++++++++ src/core/RefineMonad.mli | 2 ++ src/core/RefineState.ml | 19 +++++++++++---- src/core/RefineState.mli | 5 +++- 7 files changed, 116 insertions(+), 6 deletions(-) create mode 100644 src/basis/JobQueue.ml create mode 100644 src/basis/JobQueue.mli diff --git a/src/basis/JobQueue.ml b/src/basis/JobQueue.ml new file mode 100644 index 000000000..d7f170f9c --- /dev/null +++ b/src/basis/JobQueue.ml @@ -0,0 +1,52 @@ +open Stdlib + +type read +type write + +type (_, 'a) t = + | Null : (write, 'a) t + | Queue : { queue : 'a Queue.t; mutex : Mutex.t; has_jobs : Condition.t } -> ('mode, 'a) t + +type 'a read_t = (read, 'a) t +type 'a write_t = (write, 'a) t + +let create () : (read, 'a) t = + let queue = Queue.create () in + let mutex = Mutex.create () in + let has_jobs = Condition.create () in + Queue { queue; mutex; has_jobs } + +let worker : (read, 'a) t -> (write, 'a) t = + fun (Queue job_queue) -> Queue job_queue + +let null = Null + +let enqueue msg : (write, 'a) t -> unit = + function + | Queue job_queue -> + Mutex.lock job_queue.mutex; + Queue.add msg job_queue.queue; + Condition.signal job_queue.has_jobs; + Mutex.unlock job_queue.mutex + | Null -> () + +let dequeue : (read, 'a) t -> 'a = + fun (Queue job_queue) -> + Mutex.lock job_queue.mutex; + let msg = + match Queue.take_opt job_queue.queue with + | Some msg -> msg + | None -> + Condition.wait job_queue.has_jobs job_queue.mutex; + Queue.take job_queue.queue + in + Mutex.unlock job_queue.mutex; + msg + +let drain : (read, 'a) t -> 'a Seq.t = + fun (Queue job_queue) -> + Mutex.lock job_queue.mutex; + let msgs = Queue.to_seq job_queue.queue in + Queue.clear job_queue.queue; + Mutex.unlock job_queue.mutex; + msgs diff --git a/src/basis/JobQueue.mli b/src/basis/JobQueue.mli new file mode 100644 index 000000000..a4f17fcb5 --- /dev/null +++ b/src/basis/JobQueue.mli @@ -0,0 +1,31 @@ +(** Thread-Safe Job Queues, with blocking reads. + + The model here is that we have a single "read" queue, + which may spawn off many workers that can write messages. *) + +type read +type write + +(** A simple, thread-safe queue. *) +type ('mode, 'a) t + +type 'a read_t = (read, 'a) t +type 'a write_t = (write, 'a) t + +(** Create a new job queue. *) +val create : unit -> (read, 'a) t + +(** Create a worker queue that may write to the original queue. *) +val worker : (read, 'a) t -> (write, 'a) t + +(** Create a queue that discards any messages placed on it. *) +val null : (write, 'a) t + +(** Place a message onto the job queue. *) +val enqueue : 'a -> (write, 'a) t -> unit + +(** Grab a message off the job queue, blocking if the queue is empty. *) +val dequeue : (read, 'a) t -> 'a + +(** Dequeue all messages off the queue. This will not block if the queue is empty. *) +val drain : (read, 'a) t -> 'a Seq.t diff --git a/src/basis/dune b/src/basis/dune index acaf8c306..37bf8c4e5 100644 --- a/src/basis/dune +++ b/src/basis/dune @@ -4,5 +4,5 @@ (:standard -w -32-38 -warn-error -a+31)) (preprocess (pps ppx_deriving.std)) - (libraries ezjsonm uuseg uuseg.string uutf containers) + (libraries ezjsonm uuseg uuseg.string uutf containers threads) (public_name cooltt.basis)) diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 345bd7d38..1d43e82f7 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -5,6 +5,7 @@ module S = Syntax module St = RefineState module Env = RefineEnv module Err = RefineError +module Msg = RefineMessage module Qu = Quote module Conv = Conversion @@ -167,3 +168,13 @@ let push_problem lbl = let update_span loc = scope @@ Env.set_location loc + +let emit_tp loc tp = + match loc with + | Some loc -> + let* st = get in + let* env = read in + let+ qtp = quote_tp tp in + St.emit_msg (Msg.TypeAt (loc, Env.pp_env env, qtp)) st + | None -> + ret () diff --git a/src/core/RefineMonad.mli b/src/core/RefineMonad.mli index e533d3481..3d3eab859 100644 --- a/src/core/RefineMonad.mli +++ b/src/core/RefineMonad.mli @@ -44,3 +44,5 @@ 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 diff --git a/src/core/RefineState.ml b/src/core/RefineState.ml index 511ac1c6f..ead3b7286 100644 --- a/src/core/RefineState.ml +++ b/src/core/RefineState.ml @@ -1,3 +1,4 @@ +open Basis open CodeUnit module IDMap = Map.Make (CodeUnitID) @@ -7,12 +8,17 @@ 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; + (** A message queue for emitting events that occured during refinement. *) + refiner_info : RefineMessage.t JobQueue.write_t + } -let init = +let init job_queue = { code_units = IDMap.empty; namespaces = IDMap.empty; - import_namespaces = IDMap.empty } + import_namespaces = IDMap.empty; + refiner_info = job_queue + } let get_unit id st = IDMap.find id st.code_units @@ -57,10 +63,15 @@ 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; + refiner_info = st.refiner_info + } let get_import path st = IDMap.find_opt path st.code_units let is_imported path st = IDMap.mem path st.code_units + +let emit_msg msg st = + JobQueue.enqueue msg st.refiner_info diff --git a/src/core/RefineState.mli b/src/core/RefineState.mli index 9f58e5d35..f7f6a3d35 100644 --- a/src/core/RefineState.mli +++ b/src/core/RefineState.mli @@ -1,9 +1,10 @@ +open Basis open CodeUnit module D = Domain type t -val init : t +val init : RefineMessage.t JobQueue.write_t -> t val get_unit : id -> t -> CodeUnit.t @@ -23,3 +24,5 @@ val is_imported : id -> t -> bool (** Create and add a new code unit. *) val init_unit : id -> t -> t + +val emit_msg : RefineMessage.t -> t -> unit From 2beea3aa95d15ca6474f92045f10742e653ad6b0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 08:58:05 -0800 Subject: [PATCH 17/38] Thread through a null job queue into the refiner --- src/frontend/Driver.ml | 9 ++++----- src/frontend/Driver.mli | 4 +++- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml index b3ad98694..9d8f333bd 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -19,7 +19,7 @@ open Monad.Notation (RM) type options = { as_file : string option; debug_mode : bool; - server_info : (string * int) option } + } type status = (unit, unit) Result.t type continuation = Continue of (status RM.m -> status RM.m) | Quit @@ -214,14 +214,13 @@ and process_file input = Log.pp_error_message ~loc:(Some err.span) ~lvl:`Error pp_message @@ ErrorMessage {error = LexingError; last_token = err.last_token}; RM.ret @@ Error () -let load_file {as_file; debug_mode; server_info} input = +let load_file {as_file; debug_mode} input = match load_current_library ~as_file input with | Error () -> Error () | Ok lib -> Debug.debug_mode debug_mode; - Option.iter (fun (hostname, port) -> Server.init hostname port) server_info; let unit_id = assign_unit_id ~as_file input in - RM.run_exn ST.init (Env.init lib) @@ + RM.run_exn (ST.init JobQueue.null) (Env.init lib) @@ RM.with_code_unit lib unit_id @@ process_file input @@ -257,6 +256,6 @@ let do_repl {as_file; debug_mode; _} = Debug.debug_mode debug_mode; let unit_id = assign_unit_id ~as_file `Stdin in let ch, lexbuf = Load.prepare_repl () in - RM.run_exn RefineState.init (Env.init lib) @@ + RM.run_exn (RefineState.init JobQueue.null) (Env.init lib) @@ RM.with_code_unit lib unit_id @@ repl lib ch lexbuf diff --git a/src/frontend/Driver.mli b/src/frontend/Driver.mli index 0fa4862a4..121818c27 100644 --- a/src/frontend/Driver.mli +++ b/src/frontend/Driver.mli @@ -1,9 +1,11 @@ (* This is the top-level driver for the proof assistant. *) +open Basis +open Core type options = { as_file : string option; debug_mode : bool; - server_info : (string * int) option } + } val load_file : options -> [`Stdin | `File of string] -> (unit, unit) result val do_repl : options -> (unit, unit) result From b03d146eadf359784c44bb7c9c4a441a9c0a4cc0 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 19:25:51 -0800 Subject: [PATCH 18/38] Start implementing LSP server --- cooltt.opam | 1 + src/server/LanguageServer.ml | 160 ++++++++++++++++++++++++++++++++++ src/server/LanguageServer.mli | 1 + src/server/LspLwt.ml | 123 ++++++++++++++++++++++++++ src/server/LspLwt.mli | 13 +++ src/server/dune | 8 ++ 6 files changed, 306 insertions(+) create mode 100644 src/server/LanguageServer.ml create mode 100644 src/server/LanguageServer.mli create mode 100644 src/server/LspLwt.ml create mode 100644 src/server/LspLwt.mli create mode 100644 src/server/dune diff --git a/cooltt.opam b/cooltt.opam index 124a27199..9676279ba 100644 --- a/cooltt.opam +++ b/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" diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml new file mode 100644 index 000000000..7999539ec --- /dev/null +++ b/src/server/LanguageServer.ml @@ -0,0 +1,160 @@ +open Basis +open Frontend +open Core +open CodeUnit + +open Lsp.Types + +module RPC = Jsonrpc +module Request = Lsp.Client_request +module Notification = Lsp.Client_notification +module Broadcast = Lsp.Server_notification + +type rpc_message = RPC.Id.t option RPC.Message.t +type rpc_request = RPC.Message.request +type rpc_notification = RPC.Message.notification + +type 'resp request = 'resp Lsp.Client_request.t +type notification = Lsp.Client_notification.t + +type server = + { lsp_io : LspLwt.io; + mutable should_shutdown : bool + } + +type lsp_error = + | DecodeError of string + | HandshakeError of string + | ShutdownError of string + | UnknownRequest of string + | UnknownNotification of string + +exception LspError of lsp_error + +open LspLwt.Notation + +(* Notifications *) + +(* Requests *) +let handle_notification : server -> string -> notification -> unit Lwt.t = + fun server mthd -> + function + | _ -> raise (LspError (UnknownNotification mthd)) + +let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = + fun server mthd -> + function + | Initialize _ -> + raise (LspError (HandshakeError "Server can only recieve a single initialization request.")) + | Shutdown -> + Lwt.return () + | _ -> raise (LspError (UnknownRequest mthd)) + +(* Main Event Loop *) +let on_notification server (notif : rpc_notification) = + match Notification.of_jsonrpc notif with + | Ok n -> handle_notification server notif.method_ n + | Error err -> + raise (LspError (DecodeError err)) + +let on_request server (req : rpc_request) = + match Request.of_jsonrpc req with + | Ok (E r) -> + let+ resp = handle_request server req.method_ r in + let json = Request.yojson_of_result r resp in + RPC.Response.ok req.id json + | Error err -> + raise (LspError (DecodeError err)) + +let on_message server (msg : rpc_message) = + match msg.id with + | None -> on_notification server { msg with id = () } + | Some id -> + let* resp = on_request server { msg with id } in + LspLwt.send server.lsp_io (RPC.Response resp) + +(** Attempt to recieve a request from the client. *) +let recv_request server = + let+ msg = LspLwt.recv server.lsp_io in + Option.bind msg @@ + function + | (Jsonrpc.Message ({ id = Some id; _ } as msg)) -> Some { msg with id } + | _ -> None + +(** Attempt to recieve a notification from the client. *) +let recv_notification server = + let+ msg = LspLwt.recv server.lsp_io in + Option.bind msg @@ + function + | (Jsonrpc.Message ({ id = None; _ } as msg)) -> Some { msg with id = () } + | _ -> None + +(* Initialization *) + +let server_capabilities = + ServerCapabilities.create () + +(** Perform the LSP initialization handshake. + https://microsoft.github.io/language-server-protocol/specifications/specification-current/#initialize *) +let initialize server = + let* req = recv_request server in + match req with + | Some req -> + begin + match Request.of_jsonrpc req with + | Ok (E (Initialize _ as init_req)) -> + let* _ = LspLwt.log server.lsp_io "Initializing..." in + let resp = InitializeResult.create ~capabilities:server_capabilities () in + let json = Request.yojson_of_result init_req resp in + LspLwt.send server.lsp_io (RPC.Response (RPC.Response.ok req.id json)) + | Ok (E _) -> + raise (LspError (HandshakeError "Initialization must begin with an initialize request.")) + | Error err -> + raise (LspError (HandshakeError err)) + end + | None -> + raise (LspError (HandshakeError "Initialization must begin with a request.")) + +(* Shutdown *) + +(** Perform the LSP shutdown sequence. + See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#exit *) +let shutdown server = + let* notif = recv_notification server in + match notif with + | Some notif -> + begin + match Notification.of_jsonrpc notif with + | Ok Exit -> + Lwt.return () + | Ok _ -> + raise (LspError (ShutdownError "The only notification that can be recieved after a shutdown request is exit.")) + | Error err -> + raise (LspError (ShutdownError err)) + end + | None -> + raise (LspError (ShutdownError "No requests can be recieved after a shutdown request.")) + +let rec event_loop server = + let* msg = LspLwt.recv server.lsp_io in + match msg with + | Some (Jsonrpc.Message msg) -> + let* _ = on_message server msg in + if server.should_shutdown + then + shutdown server + else + event_loop server + | _ -> + let+ _ = LspLwt.log server.lsp_io "Recieved an invalid message. Shutting down..." in + () + +let run () = + let server = { + lsp_io = LspLwt.init (); + should_shutdown = false + } in + let _ = Lwt_main.run @@ + let* _ = initialize server in + event_loop server + in Ok () diff --git a/src/server/LanguageServer.mli b/src/server/LanguageServer.mli new file mode 100644 index 000000000..a67608424 --- /dev/null +++ b/src/server/LanguageServer.mli @@ -0,0 +1 @@ +val run : unit -> (unit, unit) result diff --git a/src/server/LspLwt.ml b/src/server/LspLwt.ml new file mode 100644 index 000000000..811746503 --- /dev/null +++ b/src/server/LspLwt.ml @@ -0,0 +1,123 @@ +(** LSP Server IO, implemented using LWT. *) +module LwtIO = Lwt_io +open Lsp.Import + +type io = { ic : LwtIO.input_channel; + oc : LwtIO.output_channel; + logc : LwtIO.output_channel + } + +let init () = + { ic = LwtIO.stdin; oc = LwtIO.stdout; logc = LwtIO.stderr } + +module Notation = struct + let (let*) = Lwt.bind + let (let+) m f = Lwt.map f m + let (and*) = Lwt.both +end + +open Notation + +(** See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#headerPart *) +module Header = struct + type t = { content_length : int; + content_type : string + } + + let empty = { content_length = -1; + content_type = "application/vscode-jsonrpc; charset=utf-8" + } + + let create ~(content_length : int) : t = + { empty with content_length } + + let is_content_length key = + String.equal (String.lowercase_ascii @@ String.trim key) "content-length" + + let is_content_type key = + String.equal (String.lowercase_ascii @@ String.trim key) "content-type" + + (* NOTE: We should never really recieve an invalid header, as + that would indicate a broken client implementation. Therefore, + we just bail out when we see an invalid header, as there's + way we can really recover anyways. *) + type header_error = + | InvalidHeader of string + | InvalidContentLength of int + + exception HeaderError of header_error + + (** Read the header section of an LSP message. *) + let read (io : io) : t Lwt.t = + let rec loop headers = + Lwt.bind (LwtIO.read_line io.ic) @@ + function + | "" -> Lwt.return headers + | line -> + match String.split_on_char ~sep:':' @@ String.trim line with + | [key; value] when is_content_length key -> + let content_length = + match int_of_string_opt value with + | Some n -> n + | None -> raise (HeaderError (InvalidHeader line)) + in loop { headers with content_length } + | [key; value] when is_content_type key -> + let content_type = String.trim value in + loop { headers with content_type } + | [_; _] -> loop headers + | _ -> raise (HeaderError (InvalidHeader line)) + in + loop empty |> Lwt.map @@ fun headers -> + if headers.content_length < 0 then + raise (HeaderError (InvalidContentLength headers.content_length)) + else + headers + + let crlf = "\r\n" + + let write (io : io) (headers : t) : unit Lwt.t = + LwtIO.fprintf io.oc "Content-Type: %s\r\nContent-Length: %d\r\n\r\n" headers.content_type headers.content_length +end + +let read_content (io : io) : string option Lwt.t = + let action = + let* header = Header.read io in + let len = header.content_length in + let buffer = Bytes.create len in + let rec loop bytes_read = + if bytes_read < len then + let* n = LwtIO.read_into io.ic buffer bytes_read (len - bytes_read) in + loop (bytes_read + n) + else + Lwt.return @@ Some (Bytes.to_string buffer) + in loop 0 + in + Lwt.catch (fun () -> action) @@ + function + | Sys_error _ -> Lwt.return None + | End_of_file -> Lwt.return None + | exn -> Lwt.fail exn + +let read_json (io : io) : Json.t option Lwt.t = + let+ contents = read_content io in + Option.map Json.of_string contents + +let recv (io : io) : Jsonrpc.packet option Lwt.t = + let+ json = read_json io in + json |> Option.map @@ fun json -> + let open Json.O in + let req json = Jsonrpc.Message (Jsonrpc.Message.either_of_yojson json) in + let resp json = Jsonrpc.Response (Jsonrpc.Response.t_of_yojson json) in + (req <|> resp) json + +let send (io : io) (packet : Jsonrpc.packet) : unit Lwt.t = + let json = Jsonrpc.yojson_of_packet packet in + let data = Json.to_string json in + let content_length = String.length data in + let header = Header.create ~content_length in + let* _ = Header.write io header in + let* _ = LwtIO.write io.oc data in + LwtIO.flush io.oc + +let log (io : io) (msg : string) : unit Lwt.t = + LwtIO.fprintf io.logc "[LOG] %s@." msg diff --git a/src/server/LspLwt.mli b/src/server/LspLwt.mli new file mode 100644 index 000000000..3c58b9a1a --- /dev/null +++ b/src/server/LspLwt.mli @@ -0,0 +1,13 @@ +type io + +val init : unit -> io + +module Notation : sig + val (let*) : 'a Lwt.t -> ('a -> 'b Lwt.t) -> 'b Lwt.t + val (let+) : 'a Lwt.t -> ('a -> 'b) -> 'b Lwt.t + val (and*) : 'a Lwt.t -> 'b Lwt.t -> ('a * 'b) Lwt.t +end + +val recv : io -> Jsonrpc.packet option Lwt.t +val send : io -> Jsonrpc.packet -> unit Lwt.t +val log : io -> string -> unit Lwt.t diff --git a/src/server/dune b/src/server/dune new file mode 100644 index 000000000..166b2f72a --- /dev/null +++ b/src/server/dune @@ -0,0 +1,8 @@ +(library + (name Server) + (libraries bantorra cooltt.basis cooltt.cubical cooltt.core cooltt.frontend lsp lwt lwt.unix) + (preprocess + (pps ppx_deriving.std)) + (flags + (:standard -w -32-37-38 -warn-error -a+31)) + (public_name cooltt.server)) \ No newline at end of file From af99c13839d500e23fa80a8d5dfa6a7bf992d3e2 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 19:54:56 -0800 Subject: [PATCH 19/38] Fix some issues with the core lsp impl --- src/server/LanguageServer.ml | 39 ++++++++++++++++++++++++++++++++---- src/server/LspLwt.ml | 27 ++++++++++++++++--------- 2 files changed, 53 insertions(+), 13 deletions(-) diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index 7999539ec..99023ae9c 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -31,6 +31,15 @@ type lsp_error = exception LspError of lsp_error +let () = Printexc.register_printer @@ + function + | LspError (DecodeError err) -> Some (Format.asprintf "Lsp Error: Couldn't decode %s" err) + | LspError (HandshakeError err) -> Some (Format.asprintf "Lsp Error: Invalid initialization handshake %s" err) + | LspError (ShutdownError err) -> Some (Format.asprintf "Lsp Error: Invalid shutdown sequence %s" err) + | LspError (UnknownRequest err) -> Some (Format.asprintf "Lsp Error: Unknown request %s" err) + | LspError (UnknownNotification err) -> Some (Format.asprintf "Lsp Error: Unknown notification %s" err) + | _ -> None + open LspLwt.Notation (* Notifications *) @@ -39,7 +48,11 @@ open LspLwt.Notation let handle_notification : server -> string -> notification -> unit Lwt.t = fun server mthd -> function - | _ -> raise (LspError (UnknownNotification mthd)) + | TextDocumentDidOpen doc -> + let+ _ = LspLwt.log server.lsp_io "Loading File..." in + () + | _ -> + raise (LspError (UnknownNotification mthd)) let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = fun server mthd -> @@ -52,12 +65,14 @@ let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = (* Main Event Loop *) let on_notification server (notif : rpc_notification) = + let* _ = LspLwt.log server.lsp_io notif.method_ in match Notification.of_jsonrpc notif with | Ok n -> handle_notification server notif.method_ n | Error err -> raise (LspError (DecodeError err)) let on_request server (req : rpc_request) = + let* _ = LspLwt.log server.lsp_io req.method_ in match Request.of_jsonrpc req with | Ok (E r) -> let+ resp = handle_request server req.method_ r in @@ -106,7 +121,21 @@ let initialize server = let* _ = LspLwt.log server.lsp_io "Initializing..." in let resp = InitializeResult.create ~capabilities:server_capabilities () in let json = Request.yojson_of_result init_req resp in - LspLwt.send server.lsp_io (RPC.Response (RPC.Response.ok req.id json)) + let* _ = LspLwt.send server.lsp_io (RPC.Response (RPC.Response.ok req.id json)) in + let* notif = recv_notification server in + begin + match notif with + | Some notif -> + begin + match Notification.of_jsonrpc notif with + | Ok (Initialized _) -> + Lwt.return () + | _ -> + raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) + end + | None -> + raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) + end | Ok (E _) -> raise (LspError (HandshakeError "Initialization must begin with an initialize request.")) | Error err -> @@ -154,7 +183,9 @@ let run () = lsp_io = LspLwt.init (); should_shutdown = false } in - let _ = Lwt_main.run @@ + let action = let* _ = initialize server in event_loop server - in Ok () + in + let _ = Lwt_main.run @@ Lwt.catch (fun () -> action) (fun exn -> LspLwt.log server.lsp_io (Printexc.to_string exn)) in + Ok () diff --git a/src/server/LspLwt.ml b/src/server/LspLwt.ml index 811746503..ea96f9b28 100644 --- a/src/server/LspLwt.ml +++ b/src/server/LspLwt.ml @@ -18,6 +18,12 @@ end open Notation +(* Logging *) + +(** Log out a message to stderr. *) +let log (io : io) (msg : string) : unit Lwt.t = + LwtIO.fprintl io.logc msg + (** See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#headerPart *) module Header = struct type t = { content_length : int; @@ -43,10 +49,16 @@ module Header = struct way we can really recover anyways. *) type header_error = | InvalidHeader of string - | InvalidContentLength of int + | InvalidContentLength of string exception HeaderError of header_error + let () = Printexc.register_printer @@ + function + | HeaderError (InvalidHeader err) -> Some (Format.asprintf "HeaderError: Invalid Header %s" err) + | HeaderError (InvalidContentLength n) -> Some (Format.asprintf "HeaderError: Invalid Content Length '%s'" n) + | _ -> None + (** Read the header section of an LSP message. *) let read (io : io) : t Lwt.t = let rec loop headers = @@ -57,24 +69,23 @@ module Header = struct match String.split_on_char ~sep:':' @@ String.trim line with | [key; value] when is_content_length key -> let content_length = - match int_of_string_opt value with + match int_of_string_opt (String.trim value) with | Some n -> n - | None -> raise (HeaderError (InvalidHeader line)) + | None -> raise (HeaderError (InvalidContentLength value)) in loop { headers with content_length } | [key; value] when is_content_type key -> let content_type = String.trim value in loop { headers with content_type } | [_; _] -> loop headers - | _ -> raise (HeaderError (InvalidHeader line)) + | _ -> + raise (HeaderError (InvalidHeader line)) in loop empty |> Lwt.map @@ fun headers -> if headers.content_length < 0 then - raise (HeaderError (InvalidContentLength headers.content_length)) + raise (HeaderError (InvalidContentLength (string_of_int headers.content_length))) else headers - let crlf = "\r\n" - let write (io : io) (headers : t) : unit Lwt.t = LwtIO.fprintf io.oc "Content-Type: %s\r\nContent-Length: %d\r\n\r\n" headers.content_type headers.content_length end @@ -119,5 +130,3 @@ let send (io : io) (packet : Jsonrpc.packet) : unit Lwt.t = let* _ = LwtIO.write io.oc data in LwtIO.flush io.oc -let log (io : io) (msg : string) : unit Lwt.t = - LwtIO.fprintf io.logc "[LOG] %s@." msg From 3435bfacc07eefe68498f0a21433fd7d6e1e4594 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 21:58:55 -0800 Subject: [PATCH 20/38] Add 'Executor.ml' for running server actions --- src/server/Executor.ml | 100 +++++++++++++++++++++++++++++++++++ src/server/Executor.mli | 3 ++ src/server/LanguageServer.ml | 98 ++++++++++++++++++++++++++-------- 3 files changed, 179 insertions(+), 22 deletions(-) create mode 100644 src/server/Executor.ml create mode 100644 src/server/Executor.mli diff --git a/src/server/Executor.ml b/src/server/Executor.ml new file mode 100644 index 000000000..0fa861ee0 --- /dev/null +++ b/src/server/Executor.ml @@ -0,0 +1,100 @@ +open Basis +open Core +open Frontend + +open CodeUnit +open DriverMessage + +module CS = ConcreteSyntax +module ST = RefineState +module Env = RefineEnv +module RM = RefineMonad +open Monad.Notation (RM) + +open Lsp.Types + +(* State *) + +type state = { refiner_state : RefineState.t; + refiner_env : RefineEnv.t; + diagnostics : Diagnostic.t list + } + +let diagnostic severity info message = + match Option.map Pos.located info with + | Some range -> Diagnostic.create ~range ~severity ~message () + | None -> failwith "[FIXME] Basis.Basis.diagnostic: Handle missing locations" + +(* Effects *) + +(** Lift a refiner computation into an LWT promise. *) +let lift_rm (st : state) (m : 'a RM.m) : ('a * state) Lwt.t = + st |> Lwt.wrap1 @@ fun st -> + RM.run_exn st.refiner_state st.refiner_env @@ + let* r = m in + let+ refiner_state = RM.get in + r, { st with refiner_state } + +let lift_rm_ st m = + Lwt.map snd (lift_rm st m) + +(* Actions *) + +(** Parse a file. *) +let parse_file (path : string) = + path |> Lwt.wrap1 @@ fun path -> + (* FIXME: proper error handling here *) + Result.get_ok @@ Load.load_file (`File path) + +(** Elaborate a single definition. *) +let elab_definition (st : state) (name : Ident.t) (args : CS.cell list) (tp : CS.con) (def : CS.con) = + lift_rm_ st @@ + let* (tp, tm) = Elaborator.elaborate_typed_term (Ident.to_string name) args tp def in + let+ _ = RM.add_global name tp (Some tm) in + () + +(* NOTE: Maybe it makes sense to rethink how messaging works *) +let print_ident (st : state) (ident : Ident.t CS.node) = + let action = + let* x = RM.resolve ident.node in + match x with + | `Global sym -> + let* vtp, con = RM.get_global sym in + let* tp = RM.quote_tp vtp in + let* tm = + match con with + | None -> RM.ret None + | Some con -> + let* tm = RM.quote_con vtp con in + RM.ret @@ Some tm + in + (* [TODO: Reed M, 24/11/2021] Rethink messaging? *) + let msg = Format.asprintf "%a" + pp_message @@ OutputMessage (Definition { ident = ident.node; tp; tm }) + in + RM.ret @@ diagnostic DiagnosticSeverity.Information ident.info msg + | _ -> RM.ret @@ diagnostic DiagnosticSeverity.Error ident.info "Unbound identifier" + in + lift_rm st action |> Lwt.map @@ fun (d, st) -> { st with diagnostics = d::st.diagnostics } + +(* FIXME: Handle the rest of the commands *) +let elab_decl (st : state) (decl : CS.decl) = + match decl with + | CS.Def { name; args; def = Some def; tp } -> + elab_definition st name args tp def + | CS.Print ident -> + print_ident st ident + | _ -> Lwt.return st + +let elaborate_file (lib : Bantorra.Manager.library) (path : string) : Diagnostic.t list Lwt.t = + let open LspLwt.Notation in + let* sign = parse_file path in + let elab_queue = JobQueue.create () in + let worker = JobQueue.worker elab_queue in + let unit_id = CodeUnitID.file path in + (* [TODO: Reed M, 24/11/2021] I don't love how the code unit stuff works here, perhaps it's time to rethink? *) + let refiner_state = ST.init_unit unit_id @@ ST.init worker in + let refiner_env = Env.set_current_unit_id unit_id (Env.init lib) in + let diagnostics = [] in + let* st = Lwt_list.fold_left_s elab_decl { refiner_state; refiner_env; diagnostics } sign in + Lwt.return st.diagnostics diff --git a/src/server/Executor.mli b/src/server/Executor.mli new file mode 100644 index 000000000..ccc2a7269 --- /dev/null +++ b/src/server/Executor.mli @@ -0,0 +1,3 @@ +open Basis + +val elaborate_file : Bantorra.Manager.library -> string -> Lsp.Types.Diagnostic.t list Lwt.t diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index 99023ae9c..8b8a81563 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -19,6 +19,7 @@ type notification = Lsp.Client_notification.t type server = { lsp_io : LspLwt.io; + library : Bantorra.Manager.library; mutable should_shutdown : bool } @@ -42,18 +43,37 @@ let () = Printexc.register_printer @@ open LspLwt.Notation +(* Server Notifications *) +let broadcast server notif = + let msg = Broadcast.to_jsonrpc notif in + LspLwt.send server.lsp_io (RPC.Message { msg with id = None }) + +let publish_diagnostics server path (diagnostics : Diagnostic.t list) = + let uri = DocumentUri.of_path path in + let params = PublishDiagnosticsParams.create ~uri ~diagnostics () in + broadcast server (PublishDiagnostics params) + + (* Notifications *) -(* Requests *) let handle_notification : server -> string -> notification -> unit Lwt.t = fun server mthd -> function | TextDocumentDidOpen doc -> - let+ _ = LspLwt.log server.lsp_io "Loading File..." in - () + let path = DocumentUri.to_path @@ doc.textDocument.uri in + let* _ = LspLwt.log server.lsp_io ("Loading File " ^ path) in + let* diagnostics = Executor.elaborate_file server.library path in + publish_diagnostics server path diagnostics + | DidSaveTextDocument doc -> + let path = DocumentUri.to_path @@ doc.textDocument.uri in + let* _ = LspLwt.log server.lsp_io ("Reloading File " ^ path) in + let* diagnostics = Executor.elaborate_file server.library path in + publish_diagnostics server path diagnostics | _ -> raise (LspError (UnknownNotification mthd)) +(* Requests *) + let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = fun server mthd -> function @@ -89,16 +109,16 @@ let on_message server (msg : rpc_message) = LspLwt.send server.lsp_io (RPC.Response resp) (** Attempt to recieve a request from the client. *) -let recv_request server = - let+ msg = LspLwt.recv server.lsp_io in +let recv_request lsp_io = + let+ msg = LspLwt.recv lsp_io in Option.bind msg @@ function | (Jsonrpc.Message ({ id = Some id; _ } as msg)) -> Some { msg with id } | _ -> None (** Attempt to recieve a notification from the client. *) -let recv_notification server = - let+ msg = LspLwt.recv server.lsp_io in +let recv_notification lsp_io = + let+ msg = LspLwt.recv lsp_io in Option.bind msg @@ function | (Jsonrpc.Message ({ id = None; _ } as msg)) -> Some { msg with id = () } @@ -107,29 +127,60 @@ let recv_notification server = (* Initialization *) let server_capabilities = - ServerCapabilities.create () + let textDocumentSync = + let opts = TextDocumentSyncOptions.create + ~change:(TextDocumentSyncKind.None) + ~save:(`SaveOptions (SaveOptions.create ~includeText:false ())) + () + in + `TextDocumentSyncOptions opts + in + ServerCapabilities.create + ~textDocumentSync + () + +let library_manager = + match Bantorra.Manager.init ~anchor:"cooltt-lib" ~routers:[] with + | Ok ans -> ans + | Error (`InvalidRouter err) -> raise (LspError (HandshakeError err)) (* this should not happen! *) + +let initialize_library root = + match + match root with + | Some path -> Bantorra.Manager.load_library_from_dir library_manager path + | None -> Bantorra.Manager.load_library_from_cwd library_manager + with + | Ok (lib, _) -> lib + | Error (`InvalidLibrary err) -> raise (LspError (HandshakeError err)) + +let get_root (init_params : InitializeParams.t) : string option = + match init_params.rootUri with + | Some uri -> Some (DocumentUri.to_path uri) + | None -> Option.join init_params.rootPath (** Perform the LSP initialization handshake. https://microsoft.github.io/language-server-protocol/specifications/specification-current/#initialize *) -let initialize server = - let* req = recv_request server in +let initialize lsp_io = + let* req = recv_request lsp_io in match req with | Some req -> begin match Request.of_jsonrpc req with - | Ok (E (Initialize _ as init_req)) -> - let* _ = LspLwt.log server.lsp_io "Initializing..." in + | Ok (E (Initialize init_params as init_req)) -> + let* _ = LspLwt.log lsp_io "Initializing..." in let resp = InitializeResult.create ~capabilities:server_capabilities () in let json = Request.yojson_of_result init_req resp in - let* _ = LspLwt.send server.lsp_io (RPC.Response (RPC.Response.ok req.id json)) in - let* notif = recv_notification server in + let* _ = LspLwt.send lsp_io (RPC.Response (RPC.Response.ok req.id json)) in + let* notif = recv_notification lsp_io in begin match notif with | Some notif -> begin match Notification.of_jsonrpc notif with | Ok (Initialized _) -> - Lwt.return () + let root = get_root init_params in + let+ _ = LspLwt.log lsp_io ("Root: " ^ Option.value root ~default:"") in + { lsp_io; should_shutdown = false; library = initialize_library root } | _ -> raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) end @@ -149,7 +200,7 @@ let initialize server = (** Perform the LSP shutdown sequence. See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#exit *) let shutdown server = - let* notif = recv_notification server in + let* notif = recv_notification server.lsp_io in match notif with | Some notif -> begin @@ -178,14 +229,17 @@ let rec event_loop server = let+ _ = LspLwt.log server.lsp_io "Recieved an invalid message. Shutting down..." in () +let print_exn lsp_io exn = + let msg = Printexc.to_string exn + and stack = Printexc.get_backtrace () in + LspLwt.log lsp_io (String.concat "\n" [msg; stack]) + let run () = - let server = { - lsp_io = LspLwt.init (); - should_shutdown = false - } in + let () = Printexc.record_backtrace true in + let lsp_io = LspLwt.init () in let action = - let* _ = initialize server in + let* server = initialize lsp_io in event_loop server in - let _ = Lwt_main.run @@ Lwt.catch (fun () -> action) (fun exn -> LspLwt.log server.lsp_io (Printexc.to_string exn)) in + let _ = Lwt_main.run @@ Lwt.catch (fun () -> action) (print_exn lsp_io) in Ok () From 0b24b1ce5c5d76c0ca9ffd2ea9a7e0df31760ac5 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 21:59:23 -0800 Subject: [PATCH 21/38] Add emacs config for lsp integration --- emacs/cooltt-lsp.el | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 emacs/cooltt-lsp.el diff --git a/emacs/cooltt-lsp.el b/emacs/cooltt-lsp.el new file mode 100644 index 000000000..262ea3995 --- /dev/null +++ b/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 "-i")) + :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 From 10e5aaf0503f5bb4fa48aa392cdbbf4b30153be8 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 22:00:21 -0800 Subject: [PATCH 22/38] Pull 'elaborate_typed_term' into the elaborator --- src/frontend/Elaborator.ml | 9 +++++++++ src/frontend/Elaborator.mli | 3 +++ 2 files changed, 12 insertions(+) diff --git a/src/frontend/Elaborator.ml b/src/frontend/Elaborator.ml index ebaf4fe8b..aaf92fc3a 100644 --- a/src/frontend/Elaborator.ml +++ b/src/frontend/Elaborator.ml @@ -450,3 +450,12 @@ let rec modifier_ (con : CS.con) = let modifier con = Option.fold ~none:(RM.ret Yuujinchou.Pattern.any) ~some:modifier_ con + +(* Helpers *) +let elaborate_typed_term name (args : CS.cell list) tp tm = + RM.push_problem name @@ + let* tp = RM.push_problem "tp" @@ T.Tp.run @@ chk_tp_in_tele args tp in + let* vtp = RM.lift_ev @@ Sem.eval_tp tp in + let* tm = RM.push_problem "tm" @@ T.Chk.run (chk_tm_in_tele args tm) vtp in + let+ vtm = RM.lift_ev @@ Sem.eval tm in + vtp, vtm diff --git a/src/frontend/Elaborator.mli b/src/frontend/Elaborator.mli index 6a8296144..c12abaf25 100644 --- a/src/frontend/Elaborator.mli +++ b/src/frontend/Elaborator.mli @@ -1,4 +1,5 @@ open Core +open CodeUnit module CS := ConcreteSyntax module S := Syntax module RM := Monads.RefineM @@ -12,3 +13,5 @@ val chk_tm : CS.con -> Chk.tac val chk_tm_in_tele : CS.cell list -> CS.con -> Chk.tac val syn_tm : CS.con -> Syn.tac val modifier : CS.con option -> [> `Print of string option] Yuujinchou.Pattern.t RM.m + +val elaborate_typed_term : string -> CS.cell list -> CS.con -> CS.con -> (D.tp * D.con) RM.m From c5f6839ff55163f24a549320eef65ecaa88a0186 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 22:17:30 -0800 Subject: [PATCH 23/38] Remove job queue in favor of metadata list --- src/basis/JobQueue.ml | 52 -------------------------------------- src/basis/JobQueue.mli | 31 ----------------------- src/basis/dune | 2 +- src/core/RefineMetadata.ml | 10 ++++++++ src/core/RefineMonad.ml | 6 ++--- src/core/RefineState.ml | 13 +++++----- src/core/RefineState.mli | 4 +-- src/frontend/Driver.ml | 4 +-- src/server/Executor.ml | 15 ++++++++--- 9 files changed, 36 insertions(+), 101 deletions(-) delete mode 100644 src/basis/JobQueue.ml delete mode 100644 src/basis/JobQueue.mli create mode 100644 src/core/RefineMetadata.ml diff --git a/src/basis/JobQueue.ml b/src/basis/JobQueue.ml deleted file mode 100644 index d7f170f9c..000000000 --- a/src/basis/JobQueue.ml +++ /dev/null @@ -1,52 +0,0 @@ -open Stdlib - -type read -type write - -type (_, 'a) t = - | Null : (write, 'a) t - | Queue : { queue : 'a Queue.t; mutex : Mutex.t; has_jobs : Condition.t } -> ('mode, 'a) t - -type 'a read_t = (read, 'a) t -type 'a write_t = (write, 'a) t - -let create () : (read, 'a) t = - let queue = Queue.create () in - let mutex = Mutex.create () in - let has_jobs = Condition.create () in - Queue { queue; mutex; has_jobs } - -let worker : (read, 'a) t -> (write, 'a) t = - fun (Queue job_queue) -> Queue job_queue - -let null = Null - -let enqueue msg : (write, 'a) t -> unit = - function - | Queue job_queue -> - Mutex.lock job_queue.mutex; - Queue.add msg job_queue.queue; - Condition.signal job_queue.has_jobs; - Mutex.unlock job_queue.mutex - | Null -> () - -let dequeue : (read, 'a) t -> 'a = - fun (Queue job_queue) -> - Mutex.lock job_queue.mutex; - let msg = - match Queue.take_opt job_queue.queue with - | Some msg -> msg - | None -> - Condition.wait job_queue.has_jobs job_queue.mutex; - Queue.take job_queue.queue - in - Mutex.unlock job_queue.mutex; - msg - -let drain : (read, 'a) t -> 'a Seq.t = - fun (Queue job_queue) -> - Mutex.lock job_queue.mutex; - let msgs = Queue.to_seq job_queue.queue in - Queue.clear job_queue.queue; - Mutex.unlock job_queue.mutex; - msgs diff --git a/src/basis/JobQueue.mli b/src/basis/JobQueue.mli deleted file mode 100644 index a4f17fcb5..000000000 --- a/src/basis/JobQueue.mli +++ /dev/null @@ -1,31 +0,0 @@ -(** Thread-Safe Job Queues, with blocking reads. - - The model here is that we have a single "read" queue, - which may spawn off many workers that can write messages. *) - -type read -type write - -(** A simple, thread-safe queue. *) -type ('mode, 'a) t - -type 'a read_t = (read, 'a) t -type 'a write_t = (write, 'a) t - -(** Create a new job queue. *) -val create : unit -> (read, 'a) t - -(** Create a worker queue that may write to the original queue. *) -val worker : (read, 'a) t -> (write, 'a) t - -(** Create a queue that discards any messages placed on it. *) -val null : (write, 'a) t - -(** Place a message onto the job queue. *) -val enqueue : 'a -> (write, 'a) t -> unit - -(** Grab a message off the job queue, blocking if the queue is empty. *) -val dequeue : (read, 'a) t -> 'a - -(** Dequeue all messages off the queue. This will not block if the queue is empty. *) -val drain : (read, 'a) t -> 'a Seq.t diff --git a/src/basis/dune b/src/basis/dune index 37bf8c4e5..acaf8c306 100644 --- a/src/basis/dune +++ b/src/basis/dune @@ -4,5 +4,5 @@ (:standard -w -32-38 -warn-error -a+31)) (preprocess (pps ppx_deriving.std)) - (libraries ezjsonm uuseg uuseg.string uutf containers threads) + (libraries ezjsonm uuseg uuseg.string uutf containers) (public_name cooltt.basis)) diff --git a/src/core/RefineMetadata.ml b/src/core/RefineMetadata.ml new file mode 100644 index 000000000..80af3e7f3 --- /dev/null +++ b/src/core/RefineMetadata.ml @@ -0,0 +1,10 @@ +open Basis +open CodeUnit + +module D = Domain +module S = Syntax + +type t = + | TypeAt of LexingUtil.span * Pp.env * S.tp + + diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 1d43e82f7..417805801 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -5,7 +5,7 @@ module S = Syntax module St = RefineState module Env = RefineEnv module Err = RefineError -module Msg = RefineMessage +module Metadata = RefineMetadata module Qu = Quote module Conv = Conversion @@ -174,7 +174,7 @@ let emit_tp loc tp = | Some loc -> let* st = get in let* env = read in - let+ qtp = quote_tp tp in - St.emit_msg (Msg.TypeAt (loc, Env.pp_env env, qtp)) st + let* qtp = quote_tp tp in + modify (St.add_metadata (Metadata.TypeAt (loc, Env.pp_env env, qtp))) | None -> ret () diff --git a/src/core/RefineState.ml b/src/core/RefineState.ml index ead3b7286..b5699fd4a 100644 --- a/src/core/RefineState.ml +++ b/src/core/RefineState.ml @@ -3,6 +3,7 @@ open CodeUnit module IDMap = Map.Make (CodeUnitID) module D = Domain +module Metadata = RefineMetadata type t = { code_units : CodeUnit.t IDMap.t; (** The binding namespace for each code unit. *) @@ -10,14 +11,14 @@ type t = { code_units : CodeUnit.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. *) - refiner_info : RefineMessage.t JobQueue.write_t + metadata : Metadata.t list } -let init job_queue = +let init = { code_units = IDMap.empty; namespaces = IDMap.empty; import_namespaces = IDMap.empty; - refiner_info = job_queue + metadata = [] } let get_unit id st = @@ -64,7 +65,7 @@ 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; - refiner_info = st.refiner_info + metadata = st.metadata } let get_import path st = @@ -73,5 +74,5 @@ let get_import path st = let is_imported path st = IDMap.mem path st.code_units -let emit_msg msg st = - JobQueue.enqueue msg st.refiner_info +let add_metadata data st = + { st with metadata = data :: st.metadata } diff --git a/src/core/RefineState.mli b/src/core/RefineState.mli index f7f6a3d35..cecae2837 100644 --- a/src/core/RefineState.mli +++ b/src/core/RefineState.mli @@ -4,7 +4,7 @@ module D = Domain type t -val init : RefineMessage.t JobQueue.write_t -> t +val init : t val get_unit : id -> t -> CodeUnit.t @@ -25,4 +25,4 @@ val is_imported : id -> t -> bool (** Create and add a new code unit. *) val init_unit : id -> t -> t -val emit_msg : RefineMessage.t -> t -> unit +val add_metadata : RefineMetadata.t -> t -> t diff --git a/src/frontend/Driver.ml b/src/frontend/Driver.ml index 9d8f333bd..b0b6f5a5a 100644 --- a/src/frontend/Driver.ml +++ b/src/frontend/Driver.ml @@ -220,7 +220,7 @@ let load_file {as_file; debug_mode} input = | Ok lib -> Debug.debug_mode debug_mode; let unit_id = assign_unit_id ~as_file input in - RM.run_exn (ST.init JobQueue.null) (Env.init lib) @@ + RM.run_exn ST.init (Env.init lib) @@ RM.with_code_unit lib unit_id @@ process_file input @@ -256,6 +256,6 @@ let do_repl {as_file; debug_mode; _} = Debug.debug_mode debug_mode; let unit_id = assign_unit_id ~as_file `Stdin in let ch, lexbuf = Load.prepare_repl () in - RM.run_exn (RefineState.init JobQueue.null) (Env.init lib) @@ + RM.run_exn RefineState.init (Env.init lib) @@ RM.with_code_unit lib unit_id @@ repl lib ch lexbuf diff --git a/src/server/Executor.ml b/src/server/Executor.ml index 0fa861ee0..eb5745c4e 100644 --- a/src/server/Executor.ml +++ b/src/server/Executor.ml @@ -7,6 +7,7 @@ open DriverMessage module CS = ConcreteSyntax module ST = RefineState +module Err = RefineError module Env = RefineEnv module RM = RefineMonad open Monad.Notation (RM) @@ -81,7 +82,15 @@ let print_ident (st : state) (ident : Ident.t CS.node) = let elab_decl (st : state) (decl : CS.decl) = match decl with | CS.Def { name; args; def = Some def; tp } -> - elab_definition st name args tp def + begin + Lwt.catch (fun () -> elab_definition st name args tp def) @@ + function + | Err.RefineError (e, span) -> + let msg = Format.asprintf "%a" Err.pp e in + let d = diagnostic DiagnosticSeverity.Error span msg in + Lwt.return { st with diagnostics = d :: st.diagnostics } + | err -> raise err + end | CS.Print ident -> print_ident st ident | _ -> Lwt.return st @@ -89,11 +98,9 @@ let elab_decl (st : state) (decl : CS.decl) = let elaborate_file (lib : Bantorra.Manager.library) (path : string) : Diagnostic.t list Lwt.t = let open LspLwt.Notation in let* sign = parse_file path in - let elab_queue = JobQueue.create () in - let worker = JobQueue.worker elab_queue in let unit_id = CodeUnitID.file path in (* [TODO: Reed M, 24/11/2021] I don't love how the code unit stuff works here, perhaps it's time to rethink? *) - let refiner_state = ST.init_unit unit_id @@ ST.init worker in + let refiner_state = ST.init_unit unit_id @@ ST.init in let refiner_env = Env.set_current_unit_id unit_id (Env.init lib) in let diagnostics = [] in let* st = Lwt_list.fold_left_s elab_decl { refiner_state; refiner_env; diagnostics } sign in From 1306aaca11372efe235b3acd7163a66f6c4c59e6 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 22:27:37 -0800 Subject: [PATCH 24/38] Update main.ml with server command --- emacs/cooltt-lsp.el | 2 +- src/bin/dune | 2 +- src/bin/main.ml | 46 +++++++++++++++++---------------------------- 3 files changed, 19 insertions(+), 31 deletions(-) diff --git a/emacs/cooltt-lsp.el b/emacs/cooltt-lsp.el index 262ea3995..04f771d2e 100644 --- a/emacs/cooltt-lsp.el +++ b/emacs/cooltt-lsp.el @@ -6,7 +6,7 @@ (lsp-register-client (make-lsp-client - :new-connection (lsp-stdio-connection (list cooltt-command "-i")) + :new-connection (lsp-stdio-connection (list cooltt-command "--mode" "server")) :major-modes '(cooltt-mode) :server-id 'cooltt)) diff --git a/src/bin/dune b/src/bin/dune index 5d3b6ddfa..cb6dc5573 100644 --- a/src/bin/dune +++ b/src/bin/dune @@ -2,7 +2,7 @@ (executables (names main) - (libraries cooltt.frontend cmdliner)) + (libraries cooltt.frontend cooltt.server cmdliner)) (install (section bin) diff --git a/src/bin/main.ml b/src/bin/main.ml index 93b6b0201..eb50e45c4 100644 --- a/src/bin/main.ml +++ b/src/bin/main.ml @@ -1,3 +1,4 @@ +open Server open Frontend open Cmdliner @@ -8,6 +9,7 @@ let _ = type mode = [ `Interactive | `Scripting of [`Stdin | `File of string] + | `Server ] type options = @@ -15,18 +17,18 @@ type options = as_file : string option; width : int; debug_mode : bool; - server_info : (string * int) option; } -let options mode as_file width debug_mode server_info = - { mode; as_file; width; debug_mode; server_info } +let options mode as_file width debug_mode = + { mode; as_file; width; debug_mode } -let main {mode; as_file; width; debug_mode; server_info} = +let main {mode; as_file; width; debug_mode; _} = Format.set_margin width; match match mode with - | `Interactive -> Driver.do_repl {as_file; debug_mode; server_info} - | `Scripting input -> Driver.load_file {as_file; debug_mode; server_info} 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") @@ -35,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,21 +65,6 @@ let opt_debug = in Arg.(value & flag & info ["debug"] ~doc) -let opt_server = - let doc = "Enable the cooltt hole server." - in - Arg.(value & flag & info ["server"] ~doc) - -let opt_server_hostname = - let doc = "The cooltt hole server hostname. If --server is not enabled, this does nothing." - in - Arg.(value & opt string "localhost" & info ["server-hostname"] ~doc ~docv:"HOSTNAME") - -let opt_server_port = - let doc = "The cooltt hole server port. If --server is not enabled, this does nothing." - in - Arg.(value & opt int 3001 & info ["server-port"] ~doc ~docv:"PORT") - let myinfo = let doc = "elaborate and normalize terms in Cartesian cubical type theory" in let err_exit = Term.exit_info ~doc:"on ill-formed types or terms." 1 in @@ -88,6 +75,7 @@ let parse_mode = function | "interactive" -> `Interactive | "scripting" -> `Scripting + | "server" -> `Server | s -> `Nonexistent s let quote s = "`" ^ s ^ "'" @@ -100,21 +88,21 @@ let consolidate_input_options mode interactive input_file : (mode, [`Msg of stri 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 consolidate_server_options server_enabled server_host server_port = - if server_enabled - then Some (server_host, server_port) - else None - let () = let opts_input = Term.(term_result ~usage:true (const consolidate_input_options $ opt_mode $ opt_interactive $ opt_input_file)) in - let opts_server = Term.(const consolidate_server_options $ opt_server $ opt_server_hostname $ opt_server_port) in - let options : options Term.t = Term.(const options $ opts_input $ opt_as_file $ opt_width $ opt_debug $ opts_server) 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) From a72fd57c104159de002375b134fc08d7a200a13e Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 22:51:25 -0800 Subject: [PATCH 25/38] Add type hovers --- src/core/RefineState.ml | 3 +++ src/core/RefineState.mli | 2 ++ src/core/Tactic.ml | 11 +++++++-- src/server/Executor.ml | 7 +++--- src/server/Executor.mli | 3 ++- src/server/IntervalTree.ml | 33 ++++++++++++++++++++++++++ src/server/IntervalTree.mli | 14 +++++++++++ src/server/LanguageServer.ml | 45 ++++++++++++++++++++++++++++-------- src/server/Pos.ml | 22 ++++++++++++++++++ src/server/Pos.mli | 12 ++++++++++ 10 files changed, 136 insertions(+), 16 deletions(-) create mode 100644 src/server/IntervalTree.ml create mode 100644 src/server/IntervalTree.mli create mode 100644 src/server/Pos.ml create mode 100644 src/server/Pos.mli diff --git a/src/core/RefineState.ml b/src/core/RefineState.ml index b5699fd4a..c2575826f 100644 --- a/src/core/RefineState.ml +++ b/src/core/RefineState.ml @@ -76,3 +76,6 @@ let is_imported path st = let add_metadata data st = { st with metadata = data :: st.metadata } + +let get_metadata st = + st.metadata diff --git a/src/core/RefineState.mli b/src/core/RefineState.mli index cecae2837..18dc39e7b 100644 --- a/src/core/RefineState.mli +++ b/src/core/RefineState.mli @@ -26,3 +26,5 @@ val is_imported : id -> t -> bool val init_unit : id -> t -> t val add_metadata : RefineMetadata.t -> t -> t + +val get_metadata : t -> RefineMetadata.t list diff --git a/src/core/Tactic.ml b/src/core/Tactic.ml index 0f291b01c..b4bbc459a 100644 --- a/src/core/Tactic.ml +++ b/src/core/Tactic.ml @@ -142,9 +142,11 @@ struct function | Chk (name, tac) -> rule ~name @@ fun tp -> + let* _ = RM.emit_tp loc tp in RM.update_span loc @@ tac tp | BChk (name, tac) -> - brule ~name @@ fun goal -> + brule ~name @@ fun ((tp, cof, bdry) as goal) -> + let* _ = RM.emit_tp loc (D.Sub (tp, cof, bdry)) in RM.update_span loc @@ tac goal let syn (tac : Syn.tac) : tac = @@ -176,7 +178,12 @@ struct tac let update_span loc (name, tac) = - (name, RM.update_span loc tac) + let tac' = + let* (tm, tp) = RM.update_span loc tac in + let+ _ = RM.emit_tp loc tp in + (tm, tp) + in + (name, tac') let ann (tac_tm : Chk.tac) (tac_tp : Tp.tac) : tac = rule @@ diff --git a/src/server/Executor.ml b/src/server/Executor.ml index eb5745c4e..f9a7f25a3 100644 --- a/src/server/Executor.ml +++ b/src/server/Executor.ml @@ -9,6 +9,7 @@ module CS = ConcreteSyntax module ST = RefineState module Err = RefineError module Env = RefineEnv +module Metadata = RefineMetadata module RM = RefineMonad open Monad.Notation (RM) @@ -95,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 Lwt.t = +let elaborate_file (lib : Bantorra.Manager.library) (path : string) : (Diagnostic.t list * Metadata.t list) Lwt.t = let open LspLwt.Notation in let* sign = parse_file path in let unit_id = CodeUnitID.file path in @@ -103,5 +104,5 @@ let elaborate_file (lib : Bantorra.Manager.library) (path : string) : Diagnostic let refiner_state = ST.init_unit unit_id @@ ST.init in let refiner_env = Env.set_current_unit_id unit_id (Env.init lib) in let diagnostics = [] in - let* st = Lwt_list.fold_left_s elab_decl { refiner_state; refiner_env; diagnostics } sign in - Lwt.return st.diagnostics + let+ st = Lwt_list.fold_left_s elab_decl { refiner_state; refiner_env; diagnostics } sign in + (st.diagnostics, ST.get_metadata st.refiner_state) diff --git a/src/server/Executor.mli b/src/server/Executor.mli index ccc2a7269..d50be82e3 100644 --- a/src/server/Executor.mli +++ b/src/server/Executor.mli @@ -1,3 +1,4 @@ open Basis +open Core -val elaborate_file : Bantorra.Manager.library -> string -> Lsp.Types.Diagnostic.t list Lwt.t +val elaborate_file : Bantorra.Manager.library -> string -> (Lsp.Types.Diagnostic.t list * RefineMetadata.t list) Lwt.t diff --git a/src/server/IntervalTree.ml b/src/server/IntervalTree.ml new file mode 100644 index 000000000..e0602bafa --- /dev/null +++ b/src/server/IntervalTree.ml @@ -0,0 +1,33 @@ +type 'a t = + | Nil + | Node of Pos.t * Pos.t * 'a * 'a t * ('a t) * ('a t) + +let empty = Nil + +let rec lookup pos = + function + | Nil -> None + | Node (lo, hi, u, cover, l, r) -> + if (pos < lo) then + lookup pos l + else if (hi < pos) then + lookup pos r + else + match lookup pos cover with + | Some ui -> Some ui + | None -> Some u + +let rec insert lo hi u = + function + | Nil -> Node (lo, hi, u, Nil, Nil, Nil) + | Node (lo', hi', u', cover, l, r) -> + if (hi < lo') then + Node (lo', hi', u', cover, insert lo hi u l, r) + else if (hi' < lo) then + Node (lo', hi', u', cover, l, insert lo hi u r) + else if (lo <= lo' && hi' <= hi) then + Node (lo, hi, u, (Node (lo', hi', u', cover, Nil, Nil)), l, r) + else + Node (lo', hi', u', insert lo hi u cover, l, r) + +let of_list xs = List.fold_left (fun t (lo, hi, u) -> insert lo hi u t) empty xs diff --git a/src/server/IntervalTree.mli b/src/server/IntervalTree.mli new file mode 100644 index 000000000..02ad08d58 --- /dev/null +++ b/src/server/IntervalTree.mli @@ -0,0 +1,14 @@ +(** Interval Trees. *) + +type 'a t + +val empty : 'a t + +(** Insert an element into the tree. *) +val insert : Pos.t -> Pos.t -> 'a -> 'a t -> 'a t + +(** Lookup a point in the tree, returning the element with the smallest + interval containing the point *) +val lookup : Pos.t -> 'a t -> 'a option + +val of_list : (Pos.t * Pos.t * 'a) list -> 'a t diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index 8b8a81563..e1b719f1a 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -20,7 +20,8 @@ type notification = Lsp.Client_notification.t type server = { lsp_io : LspLwt.io; library : Bantorra.Manager.library; - mutable should_shutdown : bool + mutable should_shutdown : bool; + mutable hover_info : string IntervalTree.t } type lsp_error = @@ -56,24 +57,37 @@ let publish_diagnostics server path (diagnostics : Diagnostic.t list) = (* Notifications *) +let update_metadata server metadata = + let update = + function + | RefineMetadata.TypeAt (span, env, tp) -> + let info = Format.asprintf "%a" (Syntax.pp_tp env) tp in + server.hover_info <- IntervalTree.insert (Pos.of_lex_pos span.start) (Pos.of_lex_pos span.stop) info server.hover_info + in List.iter update metadata + +let load_file server (uri : DocumentUri.t) = + let path = DocumentUri.to_path uri in + let* _ = LspLwt.log server.lsp_io ("Loading File " ^ path) in + let* (diagnostics, metadata) = Executor.elaborate_file server.library path in + let+ _ = publish_diagnostics server path diagnostics in + update_metadata server metadata + let handle_notification : server -> string -> notification -> unit Lwt.t = fun server mthd -> function | TextDocumentDidOpen doc -> - let path = DocumentUri.to_path @@ doc.textDocument.uri in - let* _ = LspLwt.log server.lsp_io ("Loading File " ^ path) in - let* diagnostics = Executor.elaborate_file server.library path in - publish_diagnostics server path diagnostics + load_file server doc.textDocument.uri | DidSaveTextDocument doc -> - let path = DocumentUri.to_path @@ doc.textDocument.uri in - let* _ = LspLwt.log server.lsp_io ("Reloading File " ^ path) in - let* diagnostics = Executor.elaborate_file server.library path in - publish_diagnostics server path diagnostics + load_file server doc.textDocument.uri | _ -> raise (LspError (UnknownNotification mthd)) (* Requests *) +let hover server (opts : HoverParams.t) = + IntervalTree.lookup (Pos.of_lsp_pos opts.position) server.hover_info |> Option.map @@ fun info -> + Hover.create ~contents:(`MarkedString { value = info; language = None }) () + let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = fun server mthd -> function @@ -81,6 +95,8 @@ let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = raise (LspError (HandshakeError "Server can only recieve a single initialization request.")) | Shutdown -> Lwt.return () + | TextDocumentHover opts -> + Lwt.return @@ hover server opts | _ -> raise (LspError (UnknownRequest mthd)) (* Main Event Loop *) @@ -135,8 +151,13 @@ let server_capabilities = in `TextDocumentSyncOptions opts in + let hoverProvider = + let opts = HoverOptions.create () + in `HoverOptions opts + in ServerCapabilities.create ~textDocumentSync + ~hoverProvider () let library_manager = @@ -180,7 +201,11 @@ let initialize lsp_io = | Ok (Initialized _) -> let root = get_root init_params in let+ _ = LspLwt.log lsp_io ("Root: " ^ Option.value root ~default:"") in - { lsp_io; should_shutdown = false; library = initialize_library root } + { lsp_io; + should_shutdown = false; + library = initialize_library root; + hover_info = IntervalTree.empty; + } | _ -> raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) end diff --git a/src/server/Pos.ml b/src/server/Pos.ml new file mode 100644 index 000000000..820c5e351 --- /dev/null +++ b/src/server/Pos.ml @@ -0,0 +1,22 @@ +open Basis +open Frontend +open Lsp.Types + +module CS = ConcreteSyntax + +type t = { row : int; col : int } + +let of_lex_pos (pos : LexingUtil.position) : t = + { row = pos.pos_lnum; col = pos.pos_cnum - pos.pos_bol } + +let of_lsp_pos (pos : Position.t) : t = + { row = pos.line + 1; col = pos.character } + +let to_lsp_pos (pos : t) : Position.t = + Position.create ~line:(pos.row - 1) ~character:pos.col + +let to_lsp_range (start : t) (stop : t) : Range.t = + Range.create ~start:(to_lsp_pos start) ~end_:(to_lsp_pos stop) + +let located (span : LexingUtil.span) : Range.t = + to_lsp_range (of_lex_pos span.start) (of_lex_pos span.stop) diff --git a/src/server/Pos.mli b/src/server/Pos.mli new file mode 100644 index 000000000..6440697c6 --- /dev/null +++ b/src/server/Pos.mli @@ -0,0 +1,12 @@ +open Basis +open Frontend + +type t = { row : int; col : int } + +val of_lex_pos : LexingUtil.position -> t +val of_lsp_pos : Lsp.Types.Position.t -> t + +val to_lsp_pos : t -> Lsp.Types.Position.t +val to_lsp_range : t -> t -> Lsp.Types.Range.t + +val located : LexingUtil.span -> Lsp.Types.Range.t From f018ff65b6628c74447a55fb87189a1e43f34785 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Wed, 24 Nov 2021 22:51:53 -0800 Subject: [PATCH 26/38] Tweak printing for subtypes with trivial cofibrations --- src/core/Syntax.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/core/Syntax.ml b/src/core/Syntax.ml index 803ff1c10..518a726d6 100644 --- a/src/core/Syntax.ml +++ b/src/core/Syntax.ml @@ -521,6 +521,9 @@ struct (pp_tp envx P.(right_of times)) fam | Signature fields -> Format.fprintf fmt "sig %a" (pp_sign env) fields + | Sub (tp, Cof (Cof.Join []), _) -> + Format.fprintf fmt "%a" + (pp_tp env penv) tp | Sub (tp, phi, tm) -> let _x, envx = ppenv_bind env `Anon in Format.fprintf fmt "@[sub %a %a@ %a@]" From f2b74ff3fdf94622862f1dd308e7e1396203fe1b Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Sat, 27 Nov 2021 19:21:07 -0800 Subject: [PATCH 27/38] [WIP] Start working on holes/commands --- src/core/RefineMetadata.ml | 3 ++ src/core/RefineMonad.ml | 9 ++++- src/core/RefineMonad.mli | 1 + src/core/Refiner.ml | 4 +- src/server/IntervalTree.ml | 47 +++++++++++++++-------- src/server/IntervalTree.mli | 10 ++++- src/server/LanguageServer.ml | 72 +++++++++++++++++++++++++++++++----- src/server/LspLwt.ml | 4 +- src/server/LspLwt.mli | 2 +- src/server/Pos.ml | 13 +++++-- src/server/Pos.mli | 8 +++- 11 files changed, 136 insertions(+), 37 deletions(-) diff --git a/src/core/RefineMetadata.ml b/src/core/RefineMetadata.ml index 80af3e7f3..8ba595372 100644 --- a/src/core/RefineMetadata.ml +++ b/src/core/RefineMetadata.ml @@ -4,7 +4,10 @@ open CodeUnit module D = Domain module S = Syntax +type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp } + type t = | TypeAt of LexingUtil.span * Pp.env * S.tp + | HoleAt of LexingUtil.span * Pp.env * hole diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 417805801..8aab51d4d 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -172,9 +172,16 @@ let update_span loc = let emit_tp loc tp = match loc with | Some loc -> - let* st = get in let* env = read in let* qtp = quote_tp tp in modify (St.add_metadata (Metadata.TypeAt (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))) + | None -> ret () diff --git a/src/core/RefineMonad.mli b/src/core/RefineMonad.mli index 3d3eab859..5fd17535d 100644 --- a/src/core/RefineMonad.mli +++ b/src/core/RefineMonad.mli @@ -46,3 +46,4 @@ 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 diff --git a/src/core/Refiner.ml b/src/core/Refiner.ml index 3215af879..5d967824b 100644 --- a/src/core/Refiner.ml +++ b/src/core/Refiner.ml @@ -125,7 +125,9 @@ struct s, tp let probe_chk name tac = - probe_goal_chk (print_state name) tac + (* FIXME: We shouldn't print here, as that would muck up stdout for the Language Server *) + (* probe_goal_chk (print_state name) tac *) + probe_goal_chk RM.emit_hole tac let probe_boundary probe tac = T.Chk.brule ~name:"probe_boundary" @@ fun (tp, phi, clo) -> diff --git a/src/server/IntervalTree.ml b/src/server/IntervalTree.ml index e0602bafa..ddf53fb8d 100644 --- a/src/server/IntervalTree.ml +++ b/src/server/IntervalTree.ml @@ -1,33 +1,48 @@ type 'a t = | Nil - | Node of Pos.t * Pos.t * 'a * 'a t * ('a t) * ('a t) + | Node of Pos.range * 'a * 'a t * 'a t * 'a t let empty = Nil let rec lookup pos = function | Nil -> None - | Node (lo, hi, u, cover, l, r) -> - if (pos < lo) then + | Node (range, u, l, inner, r) -> + if (pos < range.start) then lookup pos l - else if (hi < pos) then + else if (range.stop < pos) then lookup pos r else - match lookup pos cover with + match lookup pos inner with | Some ui -> Some ui | None -> Some u -let rec insert lo hi u = +let rec containing (range : Pos.range) = function - | Nil -> Node (lo, hi, u, Nil, Nil, Nil) - | Node (lo', hi', u', cover, l, r) -> - if (hi < lo') then - Node (lo', hi', u', cover, insert lo hi u l, r) - else if (hi' < lo) then - Node (lo', hi', u', cover, l, insert lo hi u r) - else if (lo <= lo' && hi' <= hi) then - Node (lo, hi, u, (Node (lo', hi', u', cover, Nil, Nil)), l, r) + | Nil -> [] + | Node (range', u, l, inner, r) -> + if (range.stop < range'.start) then + containing range l + else if (range'.stop < range.start) then + containing range r + else if (range.start <= range'.start && range'.stop <= range.stop) then + [] else - Node (lo', hi', u', insert lo hi u cover, l, r) + u :: containing range inner -let of_list xs = List.fold_left (fun t (lo, hi, u) -> insert lo hi u t) empty xs +let rec insert (range : Pos.range) u = + function + | Nil -> Node (range, u, Nil, Nil, Nil) + | Node (range', u', l, inner, r) -> + if (range.stop < range'.start) then + Node (range', u', insert range u l, inner, r) + else if (range'.stop < range.start) then + Node (range', u', l, inner, insert range u r) + else if (range.start <= range'.start && range'.stop <= range.stop) then + (* The span we are inserting contains range', so we make a new node, and add range' to the interior. *) + Node (range, u, l, (Node (range', u', Nil, inner, Nil)), r) + else + (* range' contains the span we are trying to insert, so we insert it into the interior. *) + Node (range', u', l, insert range u inner, r) + +let of_list xs = List.fold_left (fun t (range, u) -> insert range u t) empty xs diff --git a/src/server/IntervalTree.mli b/src/server/IntervalTree.mli index 02ad08d58..9966334b6 100644 --- a/src/server/IntervalTree.mli +++ b/src/server/IntervalTree.mli @@ -5,10 +5,16 @@ type 'a t val empty : 'a t (** Insert an element into the tree. *) -val insert : Pos.t -> Pos.t -> 'a -> 'a t -> 'a t +val insert : Pos.range -> 'a -> 'a t -> 'a t + +(** Construct an interval tree from a list of ranges. *) +val of_list : (Pos.range * 'a) list -> 'a t (** Lookup a point in the tree, returning the element with the smallest interval containing the point *) val lookup : Pos.t -> 'a t -> 'a option -val of_list : (Pos.t * Pos.t * 'a) list -> 'a t +(** Get all elements that lie contain a provided range. *) +val containing : Pos.range -> 'a t -> 'a list + + diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index e1b719f1a..15f9e754d 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -3,12 +3,17 @@ open Frontend open Core open CodeUnit +module S = Syntax +module D = Domain +module Metadata = RefineMetadata + open Lsp.Types module RPC = Jsonrpc module Request = Lsp.Client_request module Notification = Lsp.Client_notification module Broadcast = Lsp.Server_notification +module Json = Lsp.Import.Json type rpc_message = RPC.Id.t option RPC.Message.t type rpc_request = RPC.Message.request @@ -17,11 +22,15 @@ type rpc_notification = RPC.Message.notification type 'resp request = 'resp Lsp.Client_request.t type notification = Lsp.Client_notification.t +type hole = Hole of { ctx : (Ident.t * S.tp) list; goal : S.tp } + type server = { lsp_io : LspLwt.io; library : Bantorra.Manager.library; + (* FIXME: We should probably thread this through. *) mutable should_shutdown : bool; - mutable hover_info : string IntervalTree.t + mutable hover_info : string IntervalTree.t; + mutable holes : Metadata.hole IntervalTree.t } type lsp_error = @@ -60,14 +69,16 @@ let publish_diagnostics server path (diagnostics : Diagnostic.t list) = let update_metadata server metadata = let update = function - | RefineMetadata.TypeAt (span, env, tp) -> - let info = Format.asprintf "%a" (Syntax.pp_tp env) tp in - server.hover_info <- IntervalTree.insert (Pos.of_lex_pos span.start) (Pos.of_lex_pos span.stop) info server.hover_info + | Metadata.TypeAt (span, pp_env, tp) -> + let info = Format.asprintf "%a" (Syntax.pp_tp pp_env) tp in + server.hover_info <- IntervalTree.insert (Pos.of_lex_span span) info server.hover_info + | Metadata.HoleAt (span, _, hole) -> + server.holes <- IntervalTree.insert (Pos.of_lex_span span) hole server.holes in List.iter update metadata let load_file server (uri : DocumentUri.t) = let path = DocumentUri.to_path uri in - let* _ = LspLwt.log server.lsp_io ("Loading File " ^ path) in + let* _ = LspLwt.log server.lsp_io "Loading File: %s" path in let* (diagnostics, metadata) = Executor.elaborate_file server.library path in let+ _ = publish_diagnostics server path diagnostics in update_metadata server metadata @@ -82,12 +93,41 @@ let handle_notification : server -> string -> notification -> unit Lwt.t = | _ -> raise (LspError (UnknownNotification mthd)) +(* Code Actions/Commands *) + +let supported_commands = ["cooltt.visualize"] + (* Requests *) let hover server (opts : HoverParams.t) = IntervalTree.lookup (Pos.of_lsp_pos opts.position) server.hover_info |> Option.map @@ fun info -> Hover.create ~contents:(`MarkedString { value = info; language = None }) () +let codeAction server (opts : CodeActionParams.t) = + let holes = IntervalTree.containing (Pos.of_lsp_range opts.range) server.holes in + let actions = + holes |> List.map @@ fun (Metadata.Hole {ctx; tp}) -> + let kind = CodeActionKind.Other "cooltt.hole.visualize" in + let command = Command.create + ~title:"visualize" + ~command:"cooltt.visualize" + ~arguments:[] + () in + let action = CodeAction.create + ~title:"visualize hole" + ~kind + ~command + () + in + `CodeAction action + + in + Lwt.return @@ Some actions + +let executeCommand server (opts : ExecuteCommandParams.t) = + let+ _ = LspLwt.log server.lsp_io "Execute Command: %s" opts.command in + `Null + let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = fun server mthd -> function @@ -97,18 +137,20 @@ let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = Lwt.return () | TextDocumentHover opts -> Lwt.return @@ hover server opts + | CodeAction opts -> codeAction server opts + | ExecuteCommand opts -> executeCommand server opts | _ -> raise (LspError (UnknownRequest mthd)) (* Main Event Loop *) let on_notification server (notif : rpc_notification) = - let* _ = LspLwt.log server.lsp_io notif.method_ in + let* _ = LspLwt.log server.lsp_io "Notification: %s" notif.method_ in match Notification.of_jsonrpc notif with | Ok n -> handle_notification server notif.method_ n | Error err -> raise (LspError (DecodeError err)) let on_request server (req : rpc_request) = - let* _ = LspLwt.log server.lsp_io req.method_ in + let* _ = LspLwt.log server.lsp_io "Request: %s" req.method_ in match Request.of_jsonrpc req with | Ok (E r) -> let+ resp = handle_request server req.method_ r in @@ -155,9 +197,18 @@ let server_capabilities = let opts = HoverOptions.create () in `HoverOptions opts in + let codeActionProvider = + let opts = CodeActionOptions.create ~codeActionKinds:[CodeActionKind.Other "cooltt.hole.visualize"] () in + `CodeActionOptions opts + in + let executeCommandProvider = + ExecuteCommandOptions.create ~commands:supported_commands () + in ServerCapabilities.create ~textDocumentSync ~hoverProvider + ~codeActionProvider + ~executeCommandProvider () let library_manager = @@ -198,13 +249,14 @@ let initialize lsp_io = | Some notif -> begin match Notification.of_jsonrpc notif with - | Ok (Initialized _) -> + | Ok Initialized -> let root = get_root init_params in - let+ _ = LspLwt.log lsp_io ("Root: " ^ Option.value root ~default:"") in + let+ _ = LspLwt.log lsp_io "Root: %s" (Option.value root ~default:"") in { lsp_io; should_shutdown = false; library = initialize_library root; hover_info = IntervalTree.empty; + holes = IntervalTree.empty } | _ -> raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) @@ -257,7 +309,7 @@ let rec event_loop server = let print_exn lsp_io exn = let msg = Printexc.to_string exn and stack = Printexc.get_backtrace () in - LspLwt.log lsp_io (String.concat "\n" [msg; stack]) + LspLwt.log lsp_io "%s\n%s" msg stack let run () = let () = Printexc.record_backtrace true in diff --git a/src/server/LspLwt.ml b/src/server/LspLwt.ml index ea96f9b28..3b7774da6 100644 --- a/src/server/LspLwt.ml +++ b/src/server/LspLwt.ml @@ -21,8 +21,8 @@ open Notation (* Logging *) (** Log out a message to stderr. *) -let log (io : io) (msg : string) : unit Lwt.t = - LwtIO.fprintl io.logc msg +let log (io : io) (msg : ('a, unit, string, unit Lwt.t) format4) : 'a = + LwtIO.fprintlf io.logc msg (** See https://microsoft.github.io/language-server-protocol/specifications/specification-current/#headerPart *) module Header = struct diff --git a/src/server/LspLwt.mli b/src/server/LspLwt.mli index 3c58b9a1a..8d375af2c 100644 --- a/src/server/LspLwt.mli +++ b/src/server/LspLwt.mli @@ -10,4 +10,4 @@ end val recv : io -> Jsonrpc.packet option Lwt.t val send : io -> Jsonrpc.packet -> unit Lwt.t -val log : io -> string -> unit Lwt.t +val log : io -> ('a, unit, string, unit Lwt.t) format4 -> 'a diff --git a/src/server/Pos.ml b/src/server/Pos.ml index 820c5e351..e2c51bc4e 100644 --- a/src/server/Pos.ml +++ b/src/server/Pos.ml @@ -5,6 +5,7 @@ open Lsp.Types module CS = ConcreteSyntax type t = { row : int; col : int } +type range = { start : t; stop: t } let of_lex_pos (pos : LexingUtil.position) : t = { row = pos.pos_lnum; col = pos.pos_cnum - pos.pos_bol } @@ -12,11 +13,17 @@ let of_lex_pos (pos : LexingUtil.position) : t = let of_lsp_pos (pos : Position.t) : t = { row = pos.line + 1; col = pos.character } +let of_lex_span (span : LexingUtil.span) : range = + { start = of_lex_pos span.start; stop = of_lex_pos span.stop } + +let of_lsp_range (range : Range.t) : range = + { start = of_lsp_pos (range.start); stop = of_lsp_pos range.end_ } + let to_lsp_pos (pos : t) : Position.t = Position.create ~line:(pos.row - 1) ~character:pos.col -let to_lsp_range (start : t) (stop : t) : Range.t = - Range.create ~start:(to_lsp_pos start) ~end_:(to_lsp_pos stop) +let to_lsp_range (r : range) : Range.t = + Range.create ~start:(to_lsp_pos r.start) ~end_:(to_lsp_pos r.stop) let located (span : LexingUtil.span) : Range.t = - to_lsp_range (of_lex_pos span.start) (of_lex_pos span.stop) + to_lsp_range @@ of_lex_span span diff --git a/src/server/Pos.mli b/src/server/Pos.mli index 6440697c6..e65b5d979 100644 --- a/src/server/Pos.mli +++ b/src/server/Pos.mli @@ -7,6 +7,12 @@ val of_lex_pos : LexingUtil.position -> t val of_lsp_pos : Lsp.Types.Position.t -> t val to_lsp_pos : t -> Lsp.Types.Position.t -val to_lsp_range : t -> t -> Lsp.Types.Range.t + +type range = { start : t; stop: t } + +val of_lex_span : LexingUtil.span -> range +val of_lsp_range : Lsp.Types.Range.t -> range + +val to_lsp_range : range -> Lsp.Types.Range.t val located : LexingUtil.span -> Lsp.Types.Range.t From 26c8989468a7636674518279c1da325dc9866bef Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 28 Nov 2021 21:29:02 -0600 Subject: [PATCH 28/38] Add segment trees --- src/basis/SegmentTree.ml | 59 +++++++++++++++++++++++++++++++++++++++ src/basis/SegmentTree.mli | 15 ++++++++++ 2 files changed, 74 insertions(+) create mode 100644 src/basis/SegmentTree.ml create mode 100644 src/basis/SegmentTree.mli diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml new file mode 100644 index 000000000..3bd3214f5 --- /dev/null +++ b/src/basis/SegmentTree.ml @@ -0,0 +1,59 @@ +module type POSITION = +sig + include Map.OrderedType + val cut_span_after : t -> t * t -> t * t + val cut_span_before : t -> t * t -> t * t +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 +end + +module Make : S = functor (Pos : POSITION) -> +struct + + module Span = struct + type t = Pos.t * Pos.t + let compare = CCPair.compare Pos.compare (CCOrd.opp Pos.compare) + end + + module SegTree = CCMap.Make(Span) + + type !+'a t = 'a SegTree.t + + let lookup pos t = + match SegTree.find_last_opt (fun k -> Span.compare k (pos,pos) <= 0) t with + | None -> None + | Some ((_, stop), v) -> + if Pos.compare stop pos >= 0 then Some v else None + + let of_sorted_list l = + let rec loop tree stack l = + match l, stack with + | _, [] -> SegTree.add_list tree stack + | [], x :: l -> loop tree [x] l + | (((xstart, xstop) as xk, xv) as x) :: stack, (((ystart, ystop), _) as y :: l) -> + if Pos.compare ystop xstart < 0 then + loop tree (y :: x :: stack) l + else if Pos.compare xstop ystart < 0 then + loop (SegTree.add xk xv tree) stack (y :: l) + else + (let tree = + if Pos.compare xstart ystart < 0 then + SegTree.add (Pos.cut_span_after ystart xk) xv tree + else + tree + in + if Pos.compare xstop ystop > 0 then + loop tree (y :: (Pos.cut_span_before ystop 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.(>|=) Span.compare fst) l) +end diff --git a/src/basis/SegmentTree.mli b/src/basis/SegmentTree.mli new file mode 100644 index 000000000..ce48e750b --- /dev/null +++ b/src/basis/SegmentTree.mli @@ -0,0 +1,15 @@ +module type POSITION = +sig + include Map.OrderedType + val cut_span_after : t -> t * t -> t * t + val cut_span_before : t -> t * t -> t * t +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 +end + +module Make : S From ea219882bed4f4b9ff7a7dd1e2fa27edb80aaadd Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 28 Nov 2021 21:30:42 -0600 Subject: [PATCH 29/38] Remove stupid parentheses --- src/basis/SegmentTree.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml index 3bd3214f5..101050137 100644 --- a/src/basis/SegmentTree.ml +++ b/src/basis/SegmentTree.ml @@ -41,16 +41,16 @@ struct else if Pos.compare xstop ystart < 0 then loop (SegTree.add xk xv tree) stack (y :: l) else - (let tree = - if Pos.compare xstart ystart < 0 then - SegTree.add (Pos.cut_span_after ystart xk) xv tree - else - tree - in - if Pos.compare xstop ystop > 0 then - loop tree (y :: (Pos.cut_span_before ystop xk, xv) :: stack) l - else - loop tree stack (y :: l)) + let tree = + if Pos.compare xstart ystart < 0 then + SegTree.add (Pos.cut_span_after ystart xk) xv tree + else + tree + in + if Pos.compare xstop ystop > 0 then + loop tree (y :: (Pos.cut_span_before ystop xk, xv) :: stack) l + else + loop tree stack (y :: l) in loop SegTree.empty [] l From a9e2309b4b433f1146c8eaf418de2dc7de0f3590 Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 28 Nov 2021 22:04:06 -0600 Subject: [PATCH 30/38] Refactor and clean up code --- src/basis/SegmentTree.ml | 38 ++++++++++++++++++++------------------ src/basis/SegmentTree.mli | 5 +++-- src/server/Pos.ml | 12 ++++++++++++ src/server/Pos.mli | 5 +---- 4 files changed, 36 insertions(+), 24 deletions(-) diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml index 101050137..7202becc6 100644 --- a/src/basis/SegmentTree.ml +++ b/src/basis/SegmentTree.ml @@ -1,59 +1,61 @@ module type POSITION = sig include Map.OrderedType - val cut_span_after : t -> t * t -> t * t - val cut_span_before : t -> t * t -> t * t + 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 of_list : ((Pos.t * Pos.t) * 'a) list -> 'a t + val of_list : (Pos.range * 'a) list -> 'a t val lookup : Pos.t -> 'a t -> 'a option end module Make : S = functor (Pos : POSITION) -> struct - module Span = struct - type t = Pos.t * Pos.t - let compare = CCPair.compare Pos.compare (CCOrd.opp Pos.compare) + 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(Span) + module SegTree = CCMap.Make(Range) type !+'a t = 'a SegTree.t let lookup pos t = - match SegTree.find_last_opt (fun k -> Span.compare k (pos,pos) <= 0) t with + match SegTree.find_last_opt (fun k -> Range.compare k {start = pos; stop = pos} <= 0) t with | None -> None - | Some ((_, stop), v) -> - if Pos.compare stop pos >= 0 then Some v else None + | Some (r, v) -> + if Pos.compare r.stop pos >= 0 then Some v else None let of_sorted_list l = let rec loop tree stack l = match l, stack with | _, [] -> SegTree.add_list tree stack | [], x :: l -> loop tree [x] l - | (((xstart, xstop) as xk, xv) as x) :: stack, (((ystart, ystop), _) as y :: l) -> - if Pos.compare ystop xstart < 0 then + | ((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 xstop ystart < 0 then + 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 xstart ystart < 0 then - SegTree.add (Pos.cut_span_after ystart xk) xv 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 xstop ystop > 0 then - loop tree (y :: (Pos.cut_span_before ystop xk, xv) :: stack) l + 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.(>|=) Span.compare fst) l) + of_sorted_list (CCList.sort (CCOrd.(>|=) Range.compare fst) l) end diff --git a/src/basis/SegmentTree.mli b/src/basis/SegmentTree.mli index ce48e750b..c8afc2a9d 100644 --- a/src/basis/SegmentTree.mli +++ b/src/basis/SegmentTree.mli @@ -1,8 +1,9 @@ module type POSITION = sig include Map.OrderedType - val cut_span_after : t -> t * t -> t * t - val cut_span_before : t -> t * t -> t * t + 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) -> diff --git a/src/server/Pos.ml b/src/server/Pos.ml index e2c51bc4e..fd24d1acd 100644 --- a/src/server/Pos.ml +++ b/src/server/Pos.ml @@ -5,8 +5,20 @@ open Lsp.Types module CS = ConcreteSyntax type t = { row : int; col : int } + type range = { start : t; stop: t } +(* these functions might result into invalid positions such as + "row 10, col 0" or "row 1, col 100" (where there are only 99 + characters at row 1), but the correctness of range lookup + should not be (hopefully) intact. *) +let minus_one p = {p with col = p.col - 1} +let plus_one p = {p with col = p.col + 1} +let cut_range_after p r = {r with stop = minus_one p} +let cut_range_before p r = {r with start = plus_one p} + +let compare p1 p2 = CCOrd.(int p1.row p2.row (int, p1.col, p2.col)) + let of_lex_pos (pos : LexingUtil.position) : t = { row = pos.pos_lnum; col = pos.pos_cnum - pos.pos_bol } diff --git a/src/server/Pos.mli b/src/server/Pos.mli index e65b5d979..82974db88 100644 --- a/src/server/Pos.mli +++ b/src/server/Pos.mli @@ -1,15 +1,12 @@ open Basis -open Frontend -type t = { row : int; col : int } +include SegmentTree.POSITION val of_lex_pos : LexingUtil.position -> t val of_lsp_pos : Lsp.Types.Position.t -> t val to_lsp_pos : t -> Lsp.Types.Position.t -type range = { start : t; stop: t } - val of_lex_span : LexingUtil.span -> range val of_lsp_range : Lsp.Types.Range.t -> range From 425b0f0e8eeed7f984c1893eb1b22185da7ac9c5 Mon Sep 17 00:00:00 2001 From: favonia Date: Sun, 28 Nov 2021 22:14:25 -0600 Subject: [PATCH 31/38] Add a README --- src/server/README.mkd | 16 ++++++++++++++++ 1 file changed, 16 insertions(+) create mode 100644 src/server/README.mkd diff --git a/src/server/README.mkd b/src/server/README.mkd new file mode 100644 index 000000000..aa42a1199 --- /dev/null +++ b/src/server/README.mkd @@ -0,0 +1,16 @@ +# Primitive Language Server for 😎tt + +## Setting for `coc.nvim` + +```json +{ + "languageserver": { + "cooltt-lsp": { + "command": "opam", + "args": ["exec", "--", "cooltt", "--mode", "server"], + "rootPatterns": ["cooltt-lib"], + "filetypes": ["cooltt"] + } + } +} +``` From 6ad519652c1ed224261b6f93d5c04d466849b06b Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 16:23:00 -0800 Subject: [PATCH 32/38] Add visualize code action --- src/server/Actions.ml | 118 +++++++++++++++++++++++++++++++++++++++++ src/server/Actions.mli | 11 ++++ 2 files changed, 129 insertions(+) create mode 100644 src/server/Actions.ml create mode 100644 src/server/Actions.mli diff --git a/src/server/Actions.ml b/src/server/Actions.ml new file mode 100644 index 000000000..782a9c383 --- /dev/null +++ b/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 diff --git a/src/server/Actions.mli b/src/server/Actions.mli new file mode 100644 index 000000000..2a694bd28 --- /dev/null +++ b/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 From 75cb4305a85cc9647c50c43a4f8b2b1c46055d53 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 16:23:19 -0800 Subject: [PATCH 33/38] Wire up code actions --- src/server/LanguageServer.ml | 38 ++++++++++++++++-------------------- 1 file changed, 17 insertions(+), 21 deletions(-) diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index 15f9e754d..38448c580 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -1,7 +1,9 @@ open Basis +open Bwd open Frontend open Core open CodeUnit +open Cubical module S = Syntax module D = Domain @@ -94,7 +96,6 @@ let handle_notification : server -> string -> notification -> unit Lwt.t = raise (LspError (UnknownNotification mthd)) (* Code Actions/Commands *) - let supported_commands = ["cooltt.visualize"] (* Requests *) @@ -106,26 +107,17 @@ let hover server (opts : HoverParams.t) = let codeAction server (opts : CodeActionParams.t) = let holes = IntervalTree.containing (Pos.of_lsp_range opts.range) server.holes in let actions = - holes |> List.map @@ fun (Metadata.Hole {ctx; tp}) -> - let kind = CodeActionKind.Other "cooltt.hole.visualize" in - let command = Command.create - ~title:"visualize" - ~command:"cooltt.visualize" - ~arguments:[] - () in - let action = CodeAction.create - ~title:"visualize hole" - ~kind - ~command - () - in - `CodeAction action + holes |> List.filter_map @@ fun (Metadata.Hole {ctx; tp}) -> + Actions.Visualize.create ctx tp + |> Option.map @@ fun action -> `CodeAction action in Lwt.return @@ Some actions let executeCommand server (opts : ExecuteCommandParams.t) = - let+ _ = LspLwt.log server.lsp_io "Execute Command: %s" opts.command in + let* _ = Actions.Visualize.execute opts.arguments in + let ppargs = Format.asprintf "%a" (Format.pp_print_option (Format.pp_print_list Json.pp)) opts.arguments in + let+ _ = LspLwt.log server.lsp_io "Execute Command: %s %s" opts.command ppargs in `Null let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = @@ -292,11 +284,19 @@ let shutdown server = | None -> raise (LspError (ShutdownError "No requests can be recieved after a shutdown request.")) +let print_exn lsp_io exn = + let msg = Printexc.to_string exn + and stack = Printexc.get_backtrace () in + LspLwt.log lsp_io "%s\n%s" msg stack + let rec event_loop server = let* msg = LspLwt.recv server.lsp_io in match msg with | Some (Jsonrpc.Message msg) -> - let* _ = on_message server msg in + let* _ = Lwt.catch + (fun () -> on_message server msg) + (print_exn server.lsp_io) + in if server.should_shutdown then shutdown server @@ -306,10 +306,6 @@ let rec event_loop server = let+ _ = LspLwt.log server.lsp_io "Recieved an invalid message. Shutting down..." in () -let print_exn lsp_io exn = - let msg = Printexc.to_string exn - and stack = Printexc.get_backtrace () in - LspLwt.log lsp_io "%s\n%s" msg stack let run () = let () = Printexc.record_backtrace true in From 45042bef64690380d4b62c3351f301b5df8e3f13 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 19:17:30 -0800 Subject: [PATCH 34/38] Fix minor bug in SegmentTree --- src/basis/SegmentTree.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml index 7202becc6..5a9d88ab2 100644 --- a/src/basis/SegmentTree.ml +++ b/src/basis/SegmentTree.ml @@ -34,7 +34,7 @@ struct 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) -> From 16ddd81bdfb8178143e883706bf0137a1b3d3b93 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 19:18:56 -0800 Subject: [PATCH 35/38] Add some extra stuff to the segment tree API --- src/basis/SegmentTree.ml | 14 +++++++++++++- src/basis/SegmentTree.mli | 6 +++++- 2 files changed, 18 insertions(+), 2 deletions(-) diff --git a/src/basis/SegmentTree.ml b/src/basis/SegmentTree.ml index 5a9d88ab2..9c1aab754 100644 --- a/src/basis/SegmentTree.ml +++ b/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,6 +36,10 @@ 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 stack, l with @@ -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 diff --git a/src/basis/SegmentTree.mli b/src/basis/SegmentTree.mli index c8afc2a9d..46b4a19cd 100644 --- a/src/basis/SegmentTree.mli +++ b/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 From 75e8550815a75207bba126bce3a83c9f3304a823 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 19:19:20 -0800 Subject: [PATCH 36/38] Add pp_range --- src/server/Pos.ml | 5 +++++ src/server/Pos.mli | 2 ++ 2 files changed, 7 insertions(+) diff --git a/src/server/Pos.ml b/src/server/Pos.ml index fd24d1acd..9cc1d6731 100644 --- a/src/server/Pos.ml +++ b/src/server/Pos.ml @@ -39,3 +39,8 @@ let to_lsp_range (r : range) : Range.t = let located (span : LexingUtil.span) : Range.t = to_lsp_range @@ of_lex_span span + +let pp_range fmt range = + Format.fprintf fmt "[%d:%d]-[%d:%d]" + range.start.row range.start.col + range.stop.row range.stop.col diff --git a/src/server/Pos.mli b/src/server/Pos.mli index 82974db88..2e320baa0 100644 --- a/src/server/Pos.mli +++ b/src/server/Pos.mli @@ -13,3 +13,5 @@ val of_lsp_range : Lsp.Types.Range.t -> range val to_lsp_range : range -> Lsp.Types.Range.t val located : LexingUtil.span -> Lsp.Types.Range.t + +val pp_range : Format.formatter -> range -> unit From 34fcefab1f714ba9e68281dee48c2126bde7af3b Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 19:19:46 -0800 Subject: [PATCH 37/38] Rework how metadata is stored --- src/core/RefineMetadata.ml | 13 ------------- src/core/RefineMonad.ml | 6 +++--- src/core/RefineState.ml | 33 +++++++++++++++++++++++++++------ src/core/RefineState.mli | 15 +++++++++++++-- 4 files changed, 43 insertions(+), 24 deletions(-) delete mode 100644 src/core/RefineMetadata.ml diff --git a/src/core/RefineMetadata.ml b/src/core/RefineMetadata.ml deleted file mode 100644 index 8ba595372..000000000 --- a/src/core/RefineMetadata.ml +++ /dev/null @@ -1,13 +0,0 @@ -open Basis -open CodeUnit - -module D = Domain -module S = Syntax - -type hole = Hole of { ctx : (Ident.t * S.tp) list; tp : S.tp } - -type t = - | TypeAt of LexingUtil.span * Pp.env * S.tp - | HoleAt of LexingUtil.span * Pp.env * hole - - diff --git a/src/core/RefineMonad.ml b/src/core/RefineMonad.ml index 8aab51d4d..7de26444f 100644 --- a/src/core/RefineMonad.ml +++ b/src/core/RefineMonad.ml @@ -174,7 +174,7 @@ 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 () @@ -182,6 +182,6 @@ 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 () diff --git a/src/core/RefineState.ml b/src/core/RefineState.ml index c2575826f..5ef3ff440 100644 --- a/src/core/RefineState.ml +++ b/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 diff --git a/src/core/RefineState.mli b/src/core/RefineState.mli index 18dc39e7b..54aaba0e0 100644 --- a/src/core/RefineState.mli +++ b/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 From 0b0db0694caeb88e2a64e49607a5546966986e52 Mon Sep 17 00:00:00 2001 From: Reed Mullanix Date: Mon, 29 Nov 2021 19:20:00 -0800 Subject: [PATCH 38/38] Remove IntervalTree --- src/server/Executor.ml | 2 +- src/server/Executor.mli | 2 +- src/server/IntervalTree.ml | 48 ------------------------ src/server/IntervalTree.mli | 20 ---------- src/server/LanguageServer.ml | 71 +++++++++++++++++++----------------- 5 files changed, 39 insertions(+), 104 deletions(-) delete mode 100644 src/server/IntervalTree.ml delete mode 100644 src/server/IntervalTree.mli diff --git a/src/server/Executor.ml b/src/server/Executor.ml index f9a7f25a3..181ea216f 100644 --- a/src/server/Executor.ml +++ b/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 diff --git a/src/server/Executor.mli b/src/server/Executor.mli index d50be82e3..0b21b2ab1 100644 --- a/src/server/Executor.mli +++ b/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 diff --git a/src/server/IntervalTree.ml b/src/server/IntervalTree.ml deleted file mode 100644 index ddf53fb8d..000000000 --- a/src/server/IntervalTree.ml +++ /dev/null @@ -1,48 +0,0 @@ -type 'a t = - | Nil - | Node of Pos.range * 'a * 'a t * 'a t * 'a t - -let empty = Nil - -let rec lookup pos = - function - | Nil -> None - | Node (range, u, l, inner, r) -> - if (pos < range.start) then - lookup pos l - else if (range.stop < pos) then - lookup pos r - else - match lookup pos inner with - | Some ui -> Some ui - | None -> Some u - -let rec containing (range : Pos.range) = - function - | Nil -> [] - | Node (range', u, l, inner, r) -> - if (range.stop < range'.start) then - containing range l - else if (range'.stop < range.start) then - containing range r - else if (range.start <= range'.start && range'.stop <= range.stop) then - [] - else - u :: containing range inner - -let rec insert (range : Pos.range) u = - function - | Nil -> Node (range, u, Nil, Nil, Nil) - | Node (range', u', l, inner, r) -> - if (range.stop < range'.start) then - Node (range', u', insert range u l, inner, r) - else if (range'.stop < range.start) then - Node (range', u', l, inner, insert range u r) - else if (range.start <= range'.start && range'.stop <= range.stop) then - (* The span we are inserting contains range', so we make a new node, and add range' to the interior. *) - Node (range, u, l, (Node (range', u', Nil, inner, Nil)), r) - else - (* range' contains the span we are trying to insert, so we insert it into the interior. *) - Node (range', u', l, insert range u inner, r) - -let of_list xs = List.fold_left (fun t (range, u) -> insert range u t) empty xs diff --git a/src/server/IntervalTree.mli b/src/server/IntervalTree.mli deleted file mode 100644 index 9966334b6..000000000 --- a/src/server/IntervalTree.mli +++ /dev/null @@ -1,20 +0,0 @@ -(** Interval Trees. *) - -type 'a t - -val empty : 'a t - -(** Insert an element into the tree. *) -val insert : Pos.range -> 'a -> 'a t -> 'a t - -(** Construct an interval tree from a list of ranges. *) -val of_list : (Pos.range * 'a) list -> 'a t - -(** Lookup a point in the tree, returning the element with the smallest - interval containing the point *) -val lookup : Pos.t -> 'a t -> 'a option - -(** Get all elements that lie contain a provided range. *) -val containing : Pos.range -> 'a t -> 'a list - - diff --git a/src/server/LanguageServer.ml b/src/server/LanguageServer.ml index 38448c580..301933f0d 100644 --- a/src/server/LanguageServer.ml +++ b/src/server/LanguageServer.ml @@ -7,7 +7,8 @@ open Cubical module S = Syntax module D = Domain -module Metadata = RefineMetadata +module Metadata = RefineState.Metadata +module RangeTree = SegmentTree.Make(Pos) open Lsp.Types @@ -24,15 +25,13 @@ type rpc_notification = RPC.Message.notification type 'resp request = 'resp Lsp.Client_request.t type notification = Lsp.Client_notification.t -type hole = Hole of { ctx : (Ident.t * S.tp) list; goal : S.tp } - type server = { lsp_io : LspLwt.io; library : Bantorra.Manager.library; (* FIXME: We should probably thread this through. *) - mutable should_shutdown : bool; - mutable hover_info : string IntervalTree.t; - mutable holes : Metadata.hole IntervalTree.t + should_shutdown : bool; + hover_info : string RangeTree.t; + holes : RefineState.Metadata.hole RangeTree.t } type lsp_error = @@ -69,23 +68,26 @@ let publish_diagnostics server path (diagnostics : Diagnostic.t list) = (* Notifications *) let update_metadata server metadata = - let update = - function - | Metadata.TypeAt (span, pp_env, tp) -> - let info = Format.asprintf "%a" (Syntax.pp_tp pp_env) tp in - server.hover_info <- IntervalTree.insert (Pos.of_lex_span span) info server.hover_info - | Metadata.HoleAt (span, _, hole) -> - server.holes <- IntervalTree.insert (Pos.of_lex_span span) hole server.holes - in List.iter update metadata - -let load_file server (uri : DocumentUri.t) = + let hover_info : string RangeTree.t = + Metadata.type_spans metadata + |> List.map (fun (span, ppenv, tp) -> (Pos.of_lex_span span, Format.asprintf "%a" (Syntax.pp_tp ppenv) tp)) + |> RangeTree.of_list + in + let holes = + Metadata.holes metadata + |> List.map (fun (span, hole) -> (Pos.of_lex_span span, hole)) + |> RangeTree.of_list + in + { server with hover_info; holes } + +let load_file server (uri : DocumentUri.t) : server Lwt.t = let path = DocumentUri.to_path uri in let* _ = LspLwt.log server.lsp_io "Loading File: %s" path in let* (diagnostics, metadata) = Executor.elaborate_file server.library path in let+ _ = publish_diagnostics server path diagnostics in update_metadata server metadata -let handle_notification : server -> string -> notification -> unit Lwt.t = +let handle_notification : server -> string -> notification -> server Lwt.t = fun server mthd -> function | TextDocumentDidOpen doc -> @@ -101,34 +103,34 @@ let supported_commands = ["cooltt.visualize"] (* Requests *) let hover server (opts : HoverParams.t) = - IntervalTree.lookup (Pos.of_lsp_pos opts.position) server.hover_info |> Option.map @@ fun info -> + RangeTree.lookup (Pos.of_lsp_pos opts.position) server.hover_info |> Option.map @@ fun info -> Hover.create ~contents:(`MarkedString { value = info; language = None }) () let codeAction server (opts : CodeActionParams.t) = - let holes = IntervalTree.containing (Pos.of_lsp_range opts.range) server.holes in + let holes = RangeTree.containing (Pos.of_lsp_pos opts.range.start) server.holes in let actions = holes |> List.filter_map @@ fun (Metadata.Hole {ctx; tp}) -> Actions.Visualize.create ctx tp |> Option.map @@ fun action -> `CodeAction action in - Lwt.return @@ Some actions + Lwt.return @@ (Some actions, server) let executeCommand server (opts : ExecuteCommandParams.t) = let* _ = Actions.Visualize.execute opts.arguments in let ppargs = Format.asprintf "%a" (Format.pp_print_option (Format.pp_print_list Json.pp)) opts.arguments in let+ _ = LspLwt.log server.lsp_io "Execute Command: %s %s" opts.command ppargs in - `Null + (`Null, server) -let handle_request : type resp. server -> string -> resp request -> resp Lwt.t = +let handle_request : type resp. server -> string -> resp request -> (resp * server) Lwt.t = fun server mthd -> function | Initialize _ -> raise (LspError (HandshakeError "Server can only recieve a single initialization request.")) | Shutdown -> - Lwt.return () + Lwt.return ((), { server with should_shutdown = true }) | TextDocumentHover opts -> - Lwt.return @@ hover server opts + Lwt.return @@ (hover server opts, server) | CodeAction opts -> codeAction server opts | ExecuteCommand opts -> executeCommand server opts | _ -> raise (LspError (UnknownRequest mthd)) @@ -141,22 +143,23 @@ let on_notification server (notif : rpc_notification) = | Error err -> raise (LspError (DecodeError err)) -let on_request server (req : rpc_request) = +let on_request server (req : rpc_request) : (RPC.Response.t * server) Lwt.t = let* _ = LspLwt.log server.lsp_io "Request: %s" req.method_ in match Request.of_jsonrpc req with | Ok (E r) -> - let+ resp = handle_request server req.method_ r in + let+ (resp, server) = handle_request server req.method_ r in let json = Request.yojson_of_result r resp in - RPC.Response.ok req.id json + (RPC.Response.ok req.id json, server) | Error err -> raise (LspError (DecodeError err)) -let on_message server (msg : rpc_message) = +let on_message server (msg : rpc_message) : server Lwt.t = match msg.id with | None -> on_notification server { msg with id = () } | Some id -> - let* resp = on_request server { msg with id } in - LspLwt.send server.lsp_io (RPC.Response resp) + let* (resp, server) = on_request server { msg with id } in + let+ _ = LspLwt.send server.lsp_io (RPC.Response resp) in + server (** Attempt to recieve a request from the client. *) let recv_request lsp_io = @@ -247,8 +250,8 @@ let initialize lsp_io = { lsp_io; should_shutdown = false; library = initialize_library root; - hover_info = IntervalTree.empty; - holes = IntervalTree.empty + hover_info = RangeTree.empty; + holes = RangeTree.empty } | _ -> raise (LspError (HandshakeError "Initialization must complete with an initialized notification.")) @@ -293,9 +296,9 @@ let rec event_loop server = let* msg = LspLwt.recv server.lsp_io in match msg with | Some (Jsonrpc.Message msg) -> - let* _ = Lwt.catch + let* server = Lwt.catch (fun () -> on_message server msg) - (print_exn server.lsp_io) + (fun exn -> Lwt.map (fun _ -> server) (print_exn server.lsp_io exn)) in if server.should_shutdown then