Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer

Commits: d076d86b by Soilih BEN SOILIH at 2021-04-17T09:09:25-06:00 empty

- - - - - 98f2b0c6 by Soilih BEN SOILIH at 2021-04-20T14:16:53-06:00 hover and definition

- - - - -

3 changed files:

- samples/acc.typer - src/typer_lsp_server.ml - typer.ml

Changes:

===================================== samples/acc.typer ===================================== @@ -20,4 +20,4 @@ map = lambda (a : Type) ≡> list = (cons 1 (cons 2 (cons 3 (cons 4 nil))));

% main = accumulate _+_ 0 list; -% main = map list (lambda x -> (x + 1)); \ No newline at end of file +% main = map list (lambda x -> (x + 1));

===================================== src/typer_lsp_server.ml ===================================== @@ -55,6 +55,32 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint

+let typer_pos_of_lsp_pos (p:Lsp.Types.Position.t) : Util.location * Util.location = + let start_pos = {file=""; line= p.line; column= p.character; docstr=""} in + let end_pos = {file=""; line= p.line; column= p.character + 1; docstr=""} in + (start_pos, end_pos) + +let lsp_pos_of_pos_start (p:Util.location) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.line) ~character:(p.column) + +let lsp_pos_of_pos_end (p:Util.location) : Lsp.Types.Position.t = + Lsp.Types.Position.create ~line:(p.line) ~character:(p.column + 1) +let lsp_range_of_loc (l:Util.location) : Lsp.Types.Range.t = + Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start l) ~end_:(lsp_pos_of_pos_end l) + +let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = + let (location, _) = vname in + Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc location) + +let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Util.location): Util.vname = + match vname_list with + | [] -> let loc = Util.dummy_location in + let s = Some "null" in + (loc,s) + | hd::tl -> let (loc, _) = hd in + if (loc.line == location.line) && (loc.column == location.column) then hd + else search_a_vname_with_a_given_position tl location + let readstring (str:string) = let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) @@ -101,7 +127,6 @@ class lsp_server = (* one env per document *) val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t = Hashtbl.create 96 - (* We define here a helper method that will: - process a document - store the state resulting from the processing @@ -130,8 +155,35 @@ class lsp_server = method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t = Hashtbl.remove buffers d.uri; Linol_lwt.return () + + method! on_req_definition ~notify_back ~uri ~pos _st = + match Hashtbl.find buffers uri with + + | state_after_processing -> let (log_list,ast) = state_after_processing in + let (list_list, ectx) = ast in + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in + let pi = List.map (fun x -> let (a,b,c) = x in a ) tab in + let loc = List.map (fun x -> vname_to_lsp_loc ~vname:x ~uri:uri) pi in + let ret = `Location loc in + Some ret + + + method! on_req_hover ~notify_back ~uri ~pos doc_state = + match Hashtbl.find buffers uri with + | state_after_processing -> let (log_list,ast) = state_after_processing in + let (list_list, ectx) = ast in + let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in + let pi = List.map (fun x -> let (a,b,c) = x in a ) tab in + let (loc_start, loc_end) = typer_pos_of_lsp_pos pos in + let vn = search_a_vname_with_a_given_position pi loc_start in + let range = lsp_range_of_loc loc_start in + let s = Util.get_vname_name vn in + let r = Lsp.Types.Hover.create + ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) + ~range:range () + in Some r

- end +end

(* Main code This is the code that creates an instance of the lsp server class

===================================== typer.ml ===================================== @@ -56,7 +56,7 @@ let arg_defs =

let main () = let usage = Sys.executable_name ^ " [options] <file1> [<file2>] …" in - Arg.parse arg_defs add_input_file usage; + Arg.parse arg_defs add_input_file usage; if !lsp_server then Typer_lsp_server.run () else (); let files = List.rev !arg_files in @@ -68,7 +68,6 @@ let main () = print_string welcome_msg; print_string (Fmt.make_sep '-'); flush stdout); - let i, ectx, rctx = try let ectx = Elab.default_ectx in @@ -89,7 +88,7 @@ let main () = -> REPL.handle_stopped_compilation ("Fatal user error: " ^ msg); exit 1 in - + if is_interactive then REPL.repl i ectx rctx

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/620fabd9f5c0134410051c22262882c12...