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

Commits: 53c2f370 by Soilih BEN SOILIH at 2021-10-16T20:13:25-04:00 -

- - - - - acf01ebf by Soilih BEN SOILIH at 2021-10-17T03:06:02-04:00 adding symbols

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -39,8 +39,10 @@ open Log open Util

+type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list + type state_after_processing = (log_entry list * - ((vname * Lexp.lexp * Lexp.ltype) list list * Debruijn.elab_context) + (list_in_list * Debruijn.elab_context) )

(* transform a list of logs to a list of tuple @@ -139,7 +141,7 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list)

-let rec search_lexp_with_a_location (list_list: (vname * Lexp.lexp * Lexp.ltype) list list) (location : Source.Location.t): Lexp.lexp option = +let rec search_lexp_with_a_location (list_list: list_in_list) (location : Source.Location.t): Lexp.lexp option = let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in let rec foo (tab:Lexp.lexp list) (loc:Source.Location.t) = @@ -352,9 +354,9 @@ end (*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 update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_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) = + let rec foo (ctx: Debruijn.lexp_context) (liste : list_in_list ) (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 @@ -371,7 +373,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

(* 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 pos_in_lexp_interval (ctx: Debruijn.lexp_context) (lst: list_in_list) (cursor:Source.Location.t) =

let lstr = update_the_context ctx lst in

@@ -390,7 +392,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp 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 find_the_nearest_lexp (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) =

let lstr = update_the_context ctx lst in

@@ -439,13 +441,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp 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) = + let lexp_search (ctx: Debruijn.lexp_context) (lst:list_in_list) (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:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:list_in_list) (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 @@ -753,6 +755,41 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

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

+(* Verify if there is a varbind *) +let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = + let (_,vrbd,_) = env in + match vrbd with + | Variable + | ForwardRef-> None + | LetDef (idx,lxp) -> Some (idx,lxp) + +(* Search if the is the given value in the context *) +let value_in_ctx (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : Debruijn.env_elem * int = + let (_, _, lctxm, _) = ectx in + let lctx = Myers.list lctxm in + let rec foo (lctx: Debruijn.env_elem list) (lxp: Lexp.lexp) (comp:int)= + match lctx with + | [] -> failwith "The value is not in ectx !" + | hd::tl -> match verify_varbind hd with + | None -> foo tl lxp (comp + 1) + | Some (idx,lxpv) -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then (hd, comp) + else foo tl lxp (comp + 1) + in foo lctx lxp 1 + +(* Search the key of a varbind in senv_type *) +let key_of_varbind (ectx: Debruijn.elab_context) (el: Debruijn.env_elem) (idx: int): string = + let (_, (_,snty), _, _) = ectx in + let sntyb = SMap.bindings snty in + let foo (lst: (string * int) list) (id: int) : string = + let (str,_) = List.find (fun (s,i) -> Int.equal i id) lst + in str + in foo sntyb idx + + +(*use value_in_ctx and key_of_varbind *) +let search_the_key (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : string = + let (vlr, idx) = value_in_ctx ectx lxp in + key_of_varbind ectx vlr idx

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

@@ -769,37 +806,71 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte

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

+(*=====================================Symbols=====================================*) + +let filter_the_list_list (list_list: list_in_list) : list_in_list = + List.filter ( fun x -> + let ((_,s),_,_) = List.nth x 0 in + match s with + | None -> false + | Some _ -> true + ) list_list + +let take_all_list_el (list_list: list_in_list) = + let rec foo (ll:list_in_list) ret_list = + match list_list with + | [] -> [] + | hd::tl -> let hdl = List.nth hd 0 in + foo tl (hdl::ret_list) + in foo list_list [] + +let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = + let lst = take_all_list_el list_list in + List.map ( fun x -> + let ((l,s),_,_) = x in + let range = lsp_range_of_loc l in + let nm = Option.get s in + Lsp.Types.DocumentSymbol.create + ~name:nm + ~kind:Lsp.Types.SymbolKind.Variable + ~range:range + ~selectionRange:range + () + ) lst + +(*=====================================End Symbols=================================*) + (*====================================Compl===================================*)

-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 - - 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 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 trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + 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_by_var (ctx:Debruijn.lexp_context) (list_list:list_in_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,_) = nearest_lexp_of_the_list liste cursor in browse_lexp lctx lxp cursor - ) lst in + ) lst in List.filter (fun x -> let (_,v,_,_) = x in match v with @@ -807,107 +878,107 @@ let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * str | Some v -> true ) nlst

- let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = - let open Elexp in - match Lexp.lexp_lexp' e with - | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function - | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor - | _ -> Lsp.Types.CompletionItemKind.Variable - - - 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),_,t) = 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:(Lexp.lexp_string t) () - 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) - - let str_to_char_list (str: string) : char list = - let char_list = ref [] in - for i=0 to ((String.length str) - 1) do - char_list := (str.[i])::(!char_list) - done; - List.rev !char_list + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = + let open Elexp in + match Lexp.lexp_lexp' e with + | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function + | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor + | _ -> Lsp.Types.CompletionItemKind.Variable

- let char_list_to_str (char_list: char list) : string = - match char_list with - | [] -> "" - | _ -> List.fold_left (fun x y -> x ^ (String.make 1 y)) "" char_list

- let char_index (str:string) (chr:char) : int = - try String.index str chr - with e -> String.index str (Char.uppercase_ascii chr) - let rec str_order (substr:string) (str:string) : bool = - match str_to_char_list substr with - | [] -> false - | [hd] -> string_contain (String.make 1 hd) str - | [hd;tl] -> let ihd = char_index str hd in - let itl = char_index str tl in - if (ihd < itl) then true + 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),_,t) = 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:(Lexp.lexp_string t) () + 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) + + let str_to_char_list (str: string) : char list = + let char_list = ref [] in + for i=0 to ((String.length str) - 1) do + char_list := (str.[i])::(!char_list) + done; + List.rev !char_list + + let char_list_to_str (char_list: char list) : string = + match char_list with + | [] -> "" + | _ -> List.fold_left (fun x y -> x ^ (String.make 1 y)) "" char_list + + let char_index (str:string) (chr:char) : int = + try String.index str chr + with e -> String.index str (Char.uppercase_ascii chr) + let rec str_order (substr:string) (str:string) : bool = + match str_to_char_list substr with + | [] -> false + | [hd] -> string_contain (String.make 1 hd) str + | [hd;tl] -> let ihd = char_index str hd in + let itl = char_index str tl in + if (ihd < itl) then true + else false + | hd::ml::tl -> let ihd = char_index str hd in + let iml = char_index str ml in + if ( ihd < iml ) then + str_order (char_list_to_str (ml::tl)) str else false - | hd::ml::tl -> let ihd = char_index str hd in - let iml = char_index str ml in - if ( ihd < iml ) then - str_order (char_list_to_str (ml::tl)) str - else false - - (* Filter completions list by a string *) - let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = - match liste with - | [] -> liste - | _ -> let lst = List.filter (fun (x:Lsp.Types.CompletionItem.t) -> - string_contain str x.label - ) liste - in - List.filter (fun (x:Lsp.Types.CompletionItem.t) -> - str_order str x.label - ) lst - (* 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) + + (* Filter completions list by a string *) + let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = + match liste with + | [] -> liste + | _ -> let lst = List.filter (fun (x:Lsp.Types.CompletionItem.t) -> + string_contain str x.label + ) liste + in + List.filter (fun (x:Lsp.Types.CompletionItem.t) -> + str_order str x.label + ) lst + (* 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 = @@ -1006,7 +1077,7 @@ class lsp_server = match Hashtbl.find buffers uri with

| state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in + let (list_list, ectx) = 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 ctx list_list typer_loc in @@ -1015,7 +1086,10 @@ class lsp_server = let ret' = (l_ctx_r,None,ltyp,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 s = Lexp.lexp_string_for_lsp l_type in + let s = try search_the_key ectx l_type + with exe -> Lexp.lexp_string_for_lsp l_type + in + (*let s = Lexp.lexp_string_for_lsp l_type in*) let r = Lsp.Types.Hover.create ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) ~range:range () @@ -1053,34 +1127,42 @@ 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) = 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 (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_,lexp,_) = vx 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 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 comp_list_ret = complete_oth word comp_list in - - let e = Some (`List comp_list_ret) in - let f = Linol_lwt.return e in f + | 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 (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx 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 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 comp_list_ret = complete_oth word comp_list in + + let e = Some (`List comp_list_ret) in + let f = Linol_lwt.return e in f + + method! on_req_symbol ~notify_back ~id ~uri () = + let doc_ = self#find_doc uri in + let doc_state = Option.get doc_ in + let (_,(list_list, _)) = readstring doc_state.content in + let r = create_symbols list_list in + let e = Some (`DocumentSymbol r) in + let f = Linol_lwt.return e in f

end

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/09aacbad9a1e1f80a174bd165b6f1188a...