Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits: 9a56ef06 by Soilih BEN SOILIH at 2021-11-04T09:51:17-04:00 -
- - - - - c136a43a by Soilih BEN SOILIH at 2021-11-05T17:13:24-04:00 -
- - - - - e43859b8 by Soilih BEN SOILIH at 2021-11-05T20:12:15-04:00 value in ctx
- - - - - 615c5f4a by Soilih BEN SOILIH at 2021-11-10T22:27:14-05:00 -
- - - - - b91bb767 by Soilih BEN SOILIH at 2021-11-14T08:28:41-05:00 fixing type printing
- - - - - c71f00d0 by Soilih BEN SOILIH at 2021-11-14T08:30:04-05:00 -
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
===================================== src/typer_lsp_server.ml ===================================== @@ -772,18 +772,46 @@ let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = | ForwardRef-> None | LetDef (idx,lxp) -> Some (idx,lxp)
+(* Search if the vname is in the context *) +let search_name_in_ctx (lctx: Debruijn.lexp_context) (lxp: Lexp.lexp) = + let lctx_l = Myers.list lctx in + let rec foo lst comp rlst = + match lst with + | [] -> rlst + | ((vn, Lexp.LetDef (idx, lxpv), _) as hd)::tl + -> if String.equal (Lexp.lexp_string lxp) (Lexp.lexp_string lxpv) then + foo tl (comp + 1) ((hd,comp)::rlst) + else foo tl (comp + 1) rlst + | _::tl -> foo tl (comp + 1) rlst + in foo lctx_l 0 [] + +(* use search_name_in_ctx *) +let use_search_name_in_ctx lctx lxp = + let rlst = search_name_in_ctx lctx lxp in + match rlst with + | [] -> failwith "no name found !!!" + | hd::_ -> let (((l,s) as vn,vrbd,ltp),i) = hd in + match s with + | None -> failwith "no name found !!!" + | Some _-> let lx = Lexp.mkVar (vn,i) in + Lexp.lexp_string lx + + (* 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 rlctx = List.rev lctx 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 + | ((vn, LetDef (idx, lxpv), _) as hd)::tl + -> let lx = Lexp.mkVar (vn,comp) in + if Opslexp.conv_p lctxm lx lxp then (hd, comp) + else foo tl lxp (comp + 1) + | _::tl -> foo tl lxp (comp + 1) + + in foo lctx lxp 0
(* Search the key of a varbind in senv_type *) let key_of_varbind (ectx: Debruijn.elab_context) (el: Debruijn.env_elem) (idx: int): string = @@ -817,28 +845,25 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte
(*=====================================Symbols=====================================*)
-let filter_the_list_list (list_list: list_in_list) : list_in_list = +let filter_the_list_list (list_list: (vname * Lexp.lexp * Lexp.lexp) list) : (vname * Lexp.lexp * Lexp.lexp) list = List.filter ( fun x -> - let ((_,s),_,_) = List.nth x 0 in + let ((_,s),_,_) = x in match s with | None -> false | Some _ -> true ) list_list
-let take_all_list_el (list_list: list_in_list) = +let take_all_list_el (list_list: list_in_list) : (vname * Lexp.lexp * Lexp.lexp) list = let rec foo (ll:list_in_list) ret_list = match list_list with | [] -> ret_list - | [n] -> List.append n ret_list - | [hd;tl] -> let apl = List.append hd tl in - List.append apl ret_list - | hd::ml::tl -> let apl = List.append hd ml in - foo tl (List.append apl ret_list) + | hd::tl -> foo tl (List.append hd ret_list) in foo list_list []
+ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = - let filtred_list = filter_the_list_list list_list in - let lst = take_all_list_el filtred_list in + let lst = take_all_list_el list_list in + let filtred_list = filter_the_list_list lst in List.map ( fun x -> let ((l,s),_,_) = x in let range = lsp_range_of_loc_for_symbol l in @@ -849,7 +874,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = ~range:range ~selectionRange:range () - ) lst + ) filtred_list
(*=====================================End Symbols=================================*)
@@ -1129,8 +1154,8 @@ 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 = try search_the_key ectx l_type - with exe -> Lexp.lexp_string_for_lsp l_type + let s = try use_search_name_in_ctx l_ctx 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 @@ -1186,7 +1211,7 @@ class lsp_server =
let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f - + (* method! on_req_symbol ~notify_back ~id ~uri () =
match Hashtbl.find buffers uri with @@ -1195,7 +1220,7 @@ class lsp_server = let r = create_symbols list_list in let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f - + *) end
@@ -1348,6 +1373,23 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,14) ""
+let testSymbols (content:string) = + let (_, (list_list,_)) = readstring content in + (*let res = create_symbols list_list in*) + let res = take_all_list_el list_list in + let name = "/home/soilih/Bureau/test/symbol.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + (* + List.iteri (fun i (x : Lsp.Types.DocumentSymbol.t) -> + let st = "\n" ^ (string_of_int i) ^ " : " ^ (x.name) ^ "\n" in + output_string oc st + ) res; + *) + output_string oc (string_of_int (List.length res)); + close_out oc + + let testS () = + testSymbols "multiply x y z = _*_ x y ;"
(*=======================================Test======================================*)
@@ -1359,6 +1401,7 @@ let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); (*test ();*) + (*testS ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/4e3f9651133236b3213e12cd2b326a084...