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

Commits: 98548aee by Soilih BEN SOILIH at 2021-08-17T23:00:07-06:00 completion from buffer

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -177,7 +177,7 @@ module Compl = struct label = label ; newText = newText ; detail = detail ; - kind = kind + kind = kind } in ret ) tup @@ -300,11 +300,11 @@ module Compl = struct Str.string_match reg x.label 0 ) liste - | _ -> List.filter (fun x -> - let reg = match_str str in - Str.string_match reg x.label 0 - ) - liste + | _ -> List.filter (fun x -> + let reg = match_str str in + Str.string_match reg x.label 0 + ) + liste end

(*==============completion============================*) @@ -446,8 +446,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

| Arrow (ak, v, t1, l, t2) -> ( + + let (_,_,k1,_) = browse_lexp ctx t1 cursor in let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - match Opslexp.sort_compose ctx nctx l ak t1 t2 with + let (_,_,k2,_) = browse_lexp nctx t2 cursor in + match Opslexp.sort_compose ctx nctx l ak k1 k2 with | SortResult k -> (nctx, None, k, location) | SortInvalid -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) @@ -459,7 +462,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in let a = browse_lexp ctx' e cursor in let b = browse_lexp ctx t cursor in - let c = (ctx,None,t,l) in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,e),l) in browse_list_lexp ([a;b;c]) cursor

| Call (f, args) @@ -718,6 +721,57 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte

(*====================================Definition===================================*)

+(*====================================Compl===================================*) + +let find_compl_location (*(ctx:Debruijn.lexp_context)*) (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list = + + let (_,vr,_,loc) = ret in + + match vr with + | None -> [] + | Some v -> let ((_,c),_) = v in + let cp = Option.get c in + let label = cp in + let range = Compl.lsp_range_of_a_tuple + (loc.start_line,(loc.end_column - String.length cp)) + (loc.end_line, loc.end_column) + in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:cp in + let kind = Lsp.Types.CompletionItemKind.Text in + let detail = "detail " ^ cp in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:detail () + in + [ci] + + let trans_listlist_l (ctx:Debruijn.lexp_context) (list_list:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lst = update_the_context ctx list_list in + let nlst = List.map ( fun x -> + let (lctx,liste) = x in + let (_,lxp,_) = List.nth liste 0 in + browse_lexp lctx lxp cursor + ) lst in + List.filter (fun x -> + let (_,v,_,_) = x in + match v with + | None -> false + | Some v -> true + ) nlst + + + let complete_oth (str:string) (liste: (Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) list) = + match str with + | str -> List.filter (fun x -> + let (_,v,_,_) = x in + let ((_,s),_) = Option.get v in + let reg = Compl.match_str str in + Str.string_match reg (Option.get s) 0 + ) + liste + +(*====================================Compl===================================*) +

(* Lsp server class This is the main point of interaction beetween the code checking documents @@ -803,7 +857,7 @@ class lsp_server = let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,lexp) = lexp_search ctx list_list typer_loc in - let (l_ctx,_, l_type,location) = browse_lexp lctx lexp typer_loc in + let (l_ctx,_,l_type,location) = browse_lexp lctx lexp typer_loc in let range = lsp_range_of_loc location in let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create @@ -843,22 +897,43 @@ 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 trans_string = Compl.tranform_string doc_state.content in + | state_after_processing -> let (_,ast) = state_after_processing in + let (list_list, _) = ast in + let typer_loc = typer_pos_of_lsp_pos pos in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let rlst = trans_listlist_l ctx list_list typer_loc in + let trans_string = Compl.tranform_string doc_state.content in let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in - let typer_loc = typer_pos_of_lsp_pos pos in - let path = "/home/soilih/Bureau/test/compl.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 path in - let c = "-----------------\n mot:" ^ word ^ "\n-------------\n" in - - output_string oc (c); - close_out oc; - let range = Compl.lsp_range_of_a_tuple (typer_loc.start_line,(typer_loc.end_column - String.length word)) (typer_loc.end_line, typer_loc.end_column) in + let tab_comp = complete_oth word rlst in + let r = List.map ( fun x -> + let (_,v,_,_) = x in + let ((_,s),_) = Option.get v in + let st = Option.get s in + let label = st in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(st) in + let kind = Lsp.Types.CompletionItemKind.Text in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:st () + in + ci

+ ) tab_comp in + (* + let path = "/home/soilih/Bureau/test/compl.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 path in + let c = "-----------------\n mot:" ^ word ^ "\n-------------\n" in + output_string oc (c); + close_out oc; + *) + + + (* let tab_compl = Compl.complete word (Compl.t_from_tuple Compl.exemple_liste) in

@@ -874,7 +949,7 @@ class lsp_server = ci

) tab_compl in - + *) let e = Some (`List r) in let f = Linol_lwt.return e in f

@@ -909,10 +984,11 @@ let sep name s = output_string oc content; close_out oc

+ let test () = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let name = "/home/soilih/Bureau/test/test.txt" in - (*sep name "INT"; + sep name "INT"; hoverTest ctx name "e = 12 ;" (1,1) "##Int"; hoverTest ctx name "e = 12 ;" (1,5) "##Int"; sep name "STRING"; @@ -953,7 +1029,7 @@ let test () = hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "##Type"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "##Int"; - hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)";*) + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; sep name "ARROW"; hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; @@ -966,7 +1042,7 @@ let test () = hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; - hoverTest ctx name "v = Int -> Int ;" (1,1) ""(*; + hoverTest ctx name "v = Int -> Int ;" (1,1) ""; sep name "INDUCTIVE"; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; @@ -1002,7 +1078,7 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,4) ""; hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,13) ""; hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,4) ""; - hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,14) ""*) + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,14) ""

(*=======================================Test======================================*)

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