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

Commits: f7f9c37f by Soilih at 2022-06-01T10:08:42-04:00 -

- - - - - 500b8fb7 by Soilih at 2022-06-01T13:42:10-04:00 -

- - - - - 8ca46ab9 by Soilih at 2022-06-01T14:42:53-04:00 adding completion with Proj constructor

- - - - -

2 changed files:

- src/typer_lsp_server.ml - typer.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -459,11 +459,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De )

| Proj (l, lxp, (_, _)) - -> - let candidats = (browse_lexp ctx lxp cursor lst_in):: + -> + let candidats = (browse_lexp ctx lxp cursor lst_in):: (ctx, None, (Opslexp.get_type ctx e_in), Some (Opslexp.get_type ctx lxp), l, lst_in) :: [] in - browse_list_lexp candidats cursor + browse_list_lexp candidats cursor

| Case (l, e, _, branches, default) -> @@ -742,7 +742,7 @@ let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) =

(* List of separators that delimit a word *) -let sep_list = [';';',';'(';')';' ';'{';'}'] +let sep_list = [';';',';'(';')';' ';'{';'}';'.']

let split_string_line (content:string) (line:int) = @@ -1236,19 +1236,17 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f

- method! on_req_completion ~notify_back:_ ~id:_ ~uri ~pos ~ctx:_ doc_state = + method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with

- | document_state -> let (_,ast,cur) = document_state in - cur := Some (pos.line, pos.character); + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (pos.line,pos.character); let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - (* let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_, lexp, _) = vx in - *) - let lexp = trans_list_in_list_to_let list_list in + let ((lvn,_),lexp,ltyp) = vx in + (*let lexp = trans_list_in_list_to_let list_list in*)

(* let trans_string = Compl.tranform_string doc_state.content in @@ -1256,14 +1254,14 @@ class lsp_server = let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in *)

- match browse_lexp ctx lexp typer_loc [] with + match browse_lexp lctx lexp typer_loc [] with

| (l_ctx,_,_, None,_,_) -> let my_str = split_string_line doc_state.content (pos.line + 1) in let word = use_search_word my_str sep_list pos.character "" in let range = lsp_range_of_a_tuple - (typer_loc.start_line,(typer_loc.start_column - String.length word)) + (typer_loc.start_line,(typer_loc.end_column - String.length word)) (typer_loc.end_line, typer_loc.end_column) in let filtred_list = filter_lctx l_ctx [] in @@ -1273,10 +1271,10 @@ class lsp_server = let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f

- | (_, _, _, Some lxp, _, _) - -> ( - match Lexp.lexp_lexp' lxp with - | Inductive (_, (_, _label), _fargs, constructors) + | (lctx, _, _, Some lxp, _,_) + -> (let ret = Opslexp.lexp_whnf lxp lctx in + match Lexp.lexp_lexp' ret with + | Inductive (_, (_,label), fargs, constructors) when SMap.cardinal constructors = 1 -> let my_str = split_string_line doc_state.content (pos.line + 1) in let word = use_search_word my_str sep_list pos.character "" in @@ -1291,15 +1289,15 @@ class lsp_server = let str = Option.get s in let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in let kind = Lsp.Types.CompletionItemKind.Function in - let ci = Lsp.Types.CompletionItem.create + let ci = Lsp.Types.CompletionItem.create ~label:str ~kind:kind ~textEdit:textEdit ~detail:(Lexp.lexp_string_for_lsp t) () in ci ) fieldtypes in - let e = Some (`List comp_list) in - let f = Linol_lwt.return e in f + let e = Some (`List comp_list) in + let f = Linol_lwt.return e in f | _ -> failwith "Our Lexp is not an Inductive Type!!!" )

===================================== typer.ml ===================================== @@ -102,7 +102,7 @@ let run_main argv =

let main () = if !lsp_server then Typer_lsp_server.run () - else (); + else let command, argv = if Array.length Sys.argv <= 1 then "repl", [||]

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/8f23b3470dcd115470055142bcb399b8e...