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

Commits: 8190e3c3 by Soilih BEN SOILIH at 2021-08-28T23:44:36-06:00 complete_oth

- - - - - 6a99c654 by Soilih BEN SOILIH at 2021-09-02T09:32:47-06:00 list myers and completions

- - - - - d0cf7df3 by Soilih BEN SOILIH at 2021-09-02T11:13:18-06:00 fix completion

- - - - - da59e1c2 by Soilih BEN SOILIH at 2021-09-03T11:16:21-06:00 -

- - - - - 1339b2e0 by Soilih BEN SOILIH at 2021-09-03T12:55:17-06:00 fixing completion

- - - - - b178ecb3 by Soilih BEN SOILIH at 2021-09-03T12:56:45-06:00 fixing Myers.list

- - - - -

2 changed files:

- src/myers.ml - src/typer_lsp_server.ml

Changes:

===================================== src/myers.ml ===================================== @@ -143,4 +143,7 @@ let map f l = fold_right (fun x l' -> cons (f x) l') l nil let iteri f l = fold_left (fun i x -> f i x; i + 1) 0 l

let reverse (l : 'a myers) : 'a myers = - fold_left (fun cdr car -> cons car cdr) nil l + fold_left (fun cdr car -> cons car cdr) nil l + +let list (l : 'a myers ) : 'a list = + fold_right (fun myr lst -> myr::lst) l []

===================================== src/typer_lsp_server.ml ===================================== @@ -42,12 +42,17 @@ open Util type state_after_processing = (log_entry list * ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) ) + +(* transform a list of logs to a list of tuple +to facilitate the manipulation +*) let log_entry_to_list (tab:log_entry list) : ((string * int * int * int * int) * log_level * string) list = List.map (fun x -> let location = Option.get x.loc in ((location.file,location.start_line,location.start_column,location.end_line,location.end_column) ,x.level,x.msg) ) tab

+(* Typer log level to lsp log level *) let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = match level with | Error -> Lsp.Types.DiagnosticSeverity.Error @@ -55,6 +60,7 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint

+(* Typer location from a tuple *) let pos_of_tuple (p:int * int) : Source.Location.t = let (line,col) = p in let open Source.Location in @@ -62,11 +68,14 @@ let pos_of_tuple (p:int * int) : Source.Location.t = let typer_pos = {file = ""; start_line = line; start_column = col; end_line = line; end_column = col; doc = dc } in typer_pos

+(* Typer location from an lsp position *) let typer_pos_of_lsp_pos (p:Lsp.Types.Position.t) : Source.Location.t = let open Source.Location in let dc = Some "" in let typer_pos = {file = ""; start_line = p.line; start_column = p.character; end_line = p.line; end_column = p.character; doc = dc } in typer_pos + + let lsp_pos_of_pos_start (p:Source.Location.t) : Lsp.Types.Position.t = Lsp.Types.Position.create ~line:(p.start_line) ~character:(p.start_column)

@@ -98,6 +107,37 @@ let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (loca 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) + +(* This function calculates the euclidean distance between +two locations *) +let dist (loc1:Source.Location.t) (loc2:Source.Location.t) = + int_of_float ( + sqrt ( + (((float_of_int (loc1.start_line)) -. (float_of_int (loc2.start_line))) ** 2.0 ) + +. (((float_of_int (loc1.start_column)) -. (float_of_int (loc2.start_column))) ** 2.0 ) + ) + ) + + +(* This function extract all elements of a list in the list_list +and search the nearest to the cursor *) +let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) (cursor:Source.Location.t) = + + match liste with + | [] -> failwith "No Lexp found!!!" + | [n] -> let (_,lxp,_) = n in + lxp + | [hd;tl] -> let (_,lxp_hd,_) = hd in + let (_,lxp_tl,_) = tl in + if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_tl) cursor ) + then lxp_hd + else lxp_tl + | hd::ml::tl -> let (_,lxp_hd,_) = hd in + let (_,lxp_ml,_) = ml in + if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_ml) cursor ) + then (nearest_lexp_of_the_list (hd::tl) cursor) + else nearest_lexp_of_the_list (ml::tl) cursor +

let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) list list) (location : Source.Location.t): Lexp.lexp option = @@ -112,6 +152,7 @@ let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) in foo lexp_list location

+(*compile a string and return the logs and ast*) let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in @@ -120,17 +161,17 @@ let readstring (str:string) = (!Log.typer_log, ast)

let process_some_input_file (_file_contents : string) : state_after_processing = - (*Logs.err (fun k->k " %s" @@ "TEST TEST TEST");*) readstring _file_contents

+(*Return the diagnostics of a document state *) let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list = let (log, _) = _state in let log_tab = log_entry_to_list log in List.map (fun x -> let (loc, lev, msg) = x in - let (_ (*file*) ,start_line,start_column,end_line,end_column) = loc in + let ( file ,start_line,start_column,end_line,end_column) = loc in let severity = log_level_to_severity lev in - let message = msg in + let message = msg ^ " in file: " ^ file in let start_pos = Lsp.Types.Position.create ~line:start_line ~character:start_column in let end_pos = Lsp.Types.Position.create ~line:end_line ~character:end_column in let range = Lsp.Types.Range.create ~start:start_pos ~end_:end_pos in @@ -309,6 +350,9 @@ end

(*==============completion============================*)

+(*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 : (vname * Lexp.lexp * Lexp.ltype) list list ) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list =

let rec foo (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp * Lexp.ltype) list list ) (list_ret: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) = @@ -325,15 +369,9 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

(* find the nearest lexp using Euclidean distance like if a buffer is an orthonormal landmark *) - - let dist (loc1:Source.Location.t) (loc2:Source.Location.t) = - int_of_float ( - sqrt ( - (((float_of_int (loc1.start_line)) -. (float_of_int (loc2.start_line))) ** 2.0 ) - +. (((float_of_int (loc1.start_column)) -. (float_of_int (loc2.start_column))) ** 2.0 ) - ) - )

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

let lstr = update_the_context ctx lst in @@ -342,7 +380,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp match ls with | [] -> failwith "No Lexp found!" | hd::tl -> let (lctx_hd, hdl) = hd in - let (_,lxp,_) = List.nth hdl 0 in + let lxp = nearest_lexp_of_the_list hdl cursor in let location = Lexp.lexp_location lxp in if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) && @@ -351,6 +389,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp else foo tl cursor in foo lstr cursor

+ (* Find the nearest lexp to the cursor *) let find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) =

let lstr = update_the_context ctx lst in @@ -360,12 +399,12 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp match ls with | [] -> failwith "No Lexp found!" | [n] -> let (lctx,l) = n in - let (_,lxp,_) = List.nth l 0 in + let lxp = nearest_lexp_of_the_list l cursor in (lctx,lxp) | [hd;tl] -> let (lctx_hd,hdl) = hd in let (lctx_tl,tll) = tl in - let (_,lxp,_) = List.nth hdl 0 in - let (_,lxp',_) = List.nth tll 0 in + let lxp = nearest_lexp_of_the_list hdl cursor in + let lxp' = nearest_lexp_of_the_list tll cursor in if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) then (lctx_hd,lxp) else @@ -374,14 +413,16 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | hd::ml::tl -> let (lctx_hd,hdl) = hd in let (lctx_ml,mll) = ml in - let (_,lxp,_) = List.nth hdl 0 in - let (_,lxp',_) = List.nth mll 0 in + let lxp = nearest_lexp_of_the_list hdl cursor in + let lxp' = nearest_lexp_of_the_list mll cursor in if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor

in foo lstr cursor

+ (* Take a list of the results of browse_lexp + and return the nearest to the cursor *) let browse_list_lexp (tab:(Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = let rec foo tab cursor = match tab with @@ -397,12 +438,12 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp else foo (ml::tl) cursor in foo tab cursor

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

- (* search the type of a lexp browsing a lexp*) + (* search the type of a lexp browsing a lexp *) let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t =

let open Elexp in @@ -440,10 +481,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

(*let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in*)

- browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor - + browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor

- | Arrow (ak, v, t1, l, t2) -> (

@@ -459,10 +498,12 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | SortK2NotType -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) ) + | 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, Lexp.mkArrow (ak,v,t,l,e),l) in + let etp = Opslexp.get_type ctx' e in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in browse_list_lexp ([a;b;c]) cursor

| Call (f, args) @@ -658,7 +699,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | _,_ -> (ctx, None, Lexp.impossible, Source.Location.dummy) ;

browse_list_lexp !candidats cursor - )

@@ -723,7 +763,7 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte

(*====================================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 lsp_compl_from_var (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

@@ -745,11 +785,11 @@ let find_compl_location (*(ctx:Debruijn.lexp_context)*) (ret : Debruijn.lexp_con in [ci]

- let trans_listlist_l (ctx:Debruijn.lexp_context) (list_list:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let trans_listlist_by_var (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 + let lxp = nearest_lexp_of_the_list liste cursor in browse_lexp lctx lxp cursor ) lst in List.filter (fun x -> @@ -757,19 +797,107 @@ let find_compl_location (*(ctx:Debruijn.lexp_context)*) (ret : Debruijn.lexp_con 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 + ) nlst + + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = + let open Elexp in + match Lexp.lexp_lexp' e with + | Imm (Float (_, _)) + | Imm (Integer (_, _)) + | Imm (String (_, _)) + | Imm (Block (_, _) | Symbol _ | Node (_, _)) + | SortLevel SLz -> Lsp.Types.CompletionItemKind.Variable + | SortLevel (SLsucc e) -> Lsp.Types.CompletionItemKind.Variable + | SortLevel (SLlub (e1, e2)) -> Lsp.Types.CompletionItemKind.Variable + | Sort (l, Stype e) -> Lsp.Types.CompletionItemKind.Variable + | Sort (_, StypeLevel) + | Sort (_, StypeOmega) -> Lsp.Types.CompletionItemKind.Variable + | Builtin (_, t) -> Lsp.Types.CompletionItemKind.Variable + | Var ((l, name), idx) -> Lsp.Types.CompletionItemKind.Variable + | Susp (e, s) -> Lsp.Types.CompletionItemKind.Variable + | Let (l, defs, e) -> Lsp.Types.CompletionItemKind.Variable + | Arrow (ak, v, t1, l, t2) -> Lsp.Types.CompletionItemKind.Variable + | Inductive (l, _label, args, cases) -> Lsp.Types.CompletionItemKind.Variable + | Case (l, e, ret, branches, default) -> Lsp.Types.CompletionItemKind.Variable + | Metavar (idx, s, _) -> Lsp.Types.CompletionItemKind.Variable + | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function + | Call (f, args) -> Lsp.Types.CompletionItemKind.Function + | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor

+ let kind_of_a_varbind (element : Debruijn.env_elem ) : Lsp.Types.CompletionItemKind.t = + let (_,vrb,_) = element in + match vrb with + | Variable + | ForwardRef -> Lsp.Types.CompletionItemKind.Variable + | LetDef (_,lxp) -> kind_of_a_lexp lxp + + (* Filter the list by the vname with the string option *) + let rec filter_lctx (lctx: Debruijn.env_elem Myers.myers) (ret: Debruijn.env_elem list) : Debruijn.env_elem list = + match lctx with + | Mnil -> ret + | Mcons (hd,tl,_,_) -> let ((_,s),_,_) = hd in + match s with + + | None -> filter_lctx tl ret + | Some _ -> filter_lctx tl (hd::ret) + + + (* Transform a context to a list of completion item *) + let ctx_to_ci_list (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = + List.map ( fun (x: Debruijn.env_elem) -> + let ((_,s),_,_) = x in + let str = Option.get s in + let label = str in + let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(str) in + let kind = kind_of_a_varbind x in + let ci = Lsp.Types.CompletionItem.create + ~label:label ~kind:kind + ~textEdit:textEdit ~detail:str () + in + ci + + ) lctx + + (* Verify if a string contains some other *) + let string_contain (substr:string) (str:string) : bool = + let r = ref 0 in + for i=0 to ((String.length substr) - 1) do + if ( + String.contains str (Char.lowercase_ascii substr.[i]) + || String.contains str (Char.uppercase_ascii substr.[i]) + ) + then r := !r + 1 + else r := !r + 0 + done; + Int.equal !r (String.length substr) + + (* Filter completions list by a string *) + let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = + match liste with + | [] -> liste + | _ -> List.filter (fun (x:Lsp.Types.CompletionItem.t) -> + string_contain str x.label + ) liste + (* List of separators that delimit a word *) + let sep_list = [';';',';'(';')';'.';' ';'{';'}'] + + let split_string_line (content:string) (line:int) = + let str_list = String.split_on_char '\n' content in + List.nth str_list (line - 1) + + (* Find the word in which the cursor is *) + let rec search_word_in_cursor (str:string) (char_list:char list) (pos:int) (ret:string) : string = + if (String.equal str "") then "" + else if (Int.equal pos 0) then String.make 1 str.[pos] ^ ret + else if (List.exists (fun x -> Char.equal x str.[pos]) char_list) then ret + else search_word_in_cursor str char_list (pos - 1) ((String.make 1 str.[pos]) ^ ret) + + let use_search_word (str:string) (char_list:char list) (pos:int) (ret:string) : string = + match pos with + | 0 -> search_word_in_cursor str char_list pos ret + | _ -> search_word_in_cursor str char_list (pos - 1) ret + + (*====================================Compl===================================*)

@@ -901,56 +1029,27 @@ class lsp_server = 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 (lctx,lexp) = lexp_search ctx list_list typer_loc in + let (l_ctx,_,_,_) = browse_lexp lctx lexp 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 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 - - - let r = List.map (fun (x:Compl.t) -> - let label = x.label in - let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(x.newText) in - let kind = Compl.createKind x in - let detail = x.detail in - let ci = Lsp.Types.CompletionItem.create - ~label:label ~kind:kind - ~textEdit:textEdit ~detail:detail () - in - ci - - ) tab_compl in - *) - let e = Some (`List r) in + 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 = 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 filtred_list = filter_lctx l_ctx [] in + let comp_list = ctx_to_ci_list filtred_list range in + + let e = Some (`List comp_list) in let f = Linol_lwt.return e in f

end

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/98548aee56fe1da1ddfe7fb0f815fa6f6...