Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer

Commits: d659bbe9 by Soilih at 2022-04-30T18:26:49-04:00 -

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -39,13 +39,12 @@ open Log open Util

-type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list +type syntax_tree = (vname * Lexp.lexp * Lexp.ltype) list list

-type syntax_tree = (list_in_list * Debruijn.elab_context) +type syntax_tree_elab_ctx = (syntax_tree * Debruijn.elab_context)

-type state_after_processing = (log_entry list * - (syntax_tree option) * ((int * int) option ref) - ) +type document_state = (log_entry list * (syntax_tree_elab_ctx option) + * ((int * int) option ref))

(* @@ -179,21 +178,21 @@ let construct_log_exec str s : Log.log_entry list =

(*compile a string and return the logs and ast*) -let readstring (str:string) = +let compile_string (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in match Elab.lexp_decl_str str ectx with - | (ast:syntax_tree) -> (!Log.typer_log, Some ast, ref None) + | (ast:syntax_tree_elab_ctx) -> (!Log.typer_log, Some ast, ref None) | exception Internal_error msg -> (construct_log_exec str msg, None, ref None) | exception Stop_compilation msg -> (construct_log_exec str msg, None, ref None) | exception User_error msg -> (construct_log_exec str msg, None, ref None)

-let process_some_input_file (_file_contents : string) : state_after_processing = - readstring _file_contents +let process_some_input_file (_file_contents : string) : document_state = + compile_string _file_contents

(*Return the diagnostics of a document state *) -let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = +let diagnostics (_state : document_state) : Lsp.Types.Diagnostic.t list = let (log, _, _) = _state in let log_tab = log_entry_to_list log in List.map (fun x -> @@ -212,8 +211,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list diagnostic ) log_tab

-let trans_list_in_list_to_let (lst: list_in_list) : Lexp.lexp = - let rec foo (lst: list_in_list) = +let trans_list_in_list_to_let (lst: syntax_tree) : Lexp.lexp = + let rec foo (lst: syntax_tree) = match lst with | [] -> Lexp.impossible | hd::tl -> let rec foo_in_foo (ls : (vname * Lexp.lexp * Lexp.lexp) list) = @@ -229,9 +228,9 @@ in foo lst (*Update the context of a list_list and returns the updated context with the list all in a list *) -let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list = +let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list =

- let rec foo (ctx: Debruijn.lexp_context) (liste : list_in_list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = + let rec foo (ctx: Debruijn.lexp_context) (liste : syntax_tree ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = match liste with | [] -> list_ret | hd::tl -> let lctx = Debruijn.lctx_extend_rec ctx hd in @@ -247,7 +246,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D

(* Return a lexp if the cursor is between his start and end position *) - let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: list_in_list) (cursor:Source.Location.t) = + let pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: syntax_tree) (cursor:Source.Location.t) =

let lstr = update_the_context ctx lst in

@@ -266,7 +265,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D in foo lstr cursor

(* Find the nearest lexp to the cursor *) - let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) =

let lstr = update_the_context ctx lst in

@@ -317,13 +316,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D

(* Find the lexp the cursor on or the nearest one *) - let lexp_search (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let lexp_search (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) = try pos_in_lexp_interval ctx lst cursor with exn -> find_the_nearest_lexp ctx lst cursor

(* If lexp_search didn't find something, give the last context and a dummy lexp *) - let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:syntax_tree) (cursor:Source.Location.t) = let lstr = update_the_context ctx lst in let lstr_rev = List.rev lstr in let (last_ctx,_) = List.hd lstr_rev in @@ -595,9 +594,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D | MVal e -> let e = Lexp.push_susp e s in browse_lexp ctx e cursor lst_in | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, None, location, lst_in)) - - -

(*====================================Lexp parcourir===================================*)

@@ -1052,7 +1048,7 @@ class lsp_server = inherit Linol_lwt.Jsonrpc2.server as super

(* one env per document *) - val buffers: (Lsp.Types.DocumentUri.t, state_after_processing) Hashtbl.t + val buffers: (Lsp.Types.DocumentUri.t, document_state) Hashtbl.t = Hashtbl.create 96 (* We define here a helper method that will: - process a document @@ -1138,7 +1134,7 @@ class lsp_server = method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (pos.line,pos.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in @@ -1172,7 +1168,7 @@ class lsp_server =

method! on_req_hover ~notify_back:_ ~id:_ ~uri ~pos _ = match Hashtbl.find buffers uri with - | state_after_processing -> let (_,ast,_) = state_after_processing in + | document_state -> let (_,ast,_) = document_state in let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let typer_loc' = { @@ -1180,16 +1176,17 @@ class lsp_server = end_line = typer_loc.start_line + 1 } in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + (* let lexp = trans_list_in_list_to_let list_list in let (l_ctx,_,l_type,_,location,_) = browse_lexp ctx lexp typer_loc' [] in - (* + *) let (lctx,vx) = lexp_search ctx list_list typer_loc' in let ((lvn,_),lexp,ltyp) = vx in

let (l_ctx_r,_,_,_,_,_) as ret = browse_lexp lctx lexp typer_loc' [] in let ret' = (l_ctx_r,None,ltyp,None,lvn,[]) in let (l_ctx,_,l_type,_,location,_) = browse_list_lexp [ret;ret'] typer_loc in - *) + let range = lsp_range_of_loc location in let range' = Lsp.Types.Range.{ start = { range.start with line = range.start.line - 1 } ; @@ -1209,7 +1206,7 @@ class lsp_server = method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (pos.line,pos.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in @@ -1276,7 +1273,7 @@ class lsp_server =

match Hashtbl.find buffers uri with

- | state_after_processing -> let (_,ast, cur) = state_after_processing in + | document_state -> let (_,ast, cur) = document_state in let (list_list, _) = Option.get ast in let typer_loc = pos_of_tuple (Option.get !cur) in let typer_loc' = { @@ -1302,7 +1299,7 @@ class lsp_server = | TextDocumentHighlight params -> ( match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (params.position.line,params.position.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos params.position in @@ -1325,7 +1322,7 @@ class lsp_server = | TextDocumentReferences params -> ( match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing -> let (_,ast,cur) = state_after_processing in + | document_state -> let (_,ast,cur) = document_state in cur := Some (params.position.line,params.position.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos params.position in @@ -1357,7 +1354,7 @@ let afficher_lst code filename = let ch = open_in code in let content = really_input_string ch (in_channel_length ch) in close_in ch; - let (_,ast,_) = readstring content in + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in List.iteri (fun i x -> let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in @@ -1380,7 +1377,7 @@ let afficher_lst code filename = ) list_list

let testerBread cursor str = - let (_,ast,_) = readstring str in + let (_,ast,_) = compile_string str in let (list_list, _) = Option.get ast in let typer_loc = pos_of_tuple cursor in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/d659bbe972bedbbecc0309a90bce781a45...