Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer
Commits: e743b867 by Soilih at 2022-07-18T12:01:25-04:00 -
- - - - - 0d31fe12 by Soilih at 2022-07-25T12:13:18-04:00 -
- - - - - 810e0e5e by Soilih at 2022-07-27T00:11:35-04:00 adding a new type to specify the completion type
- - - - - ad338dec by Soilih at 2022-07-31T13:49:01-04:00 tests for the server
- - - - - ff970015 by Soilih at 2022-08-18T14:54:37-04:00 tests
- - - - -
2 changed files:
- − src/lsp_server_test.ml - src/typer_lsp_server.ml
Changes:
===================================== src/lsp_server_test.ml deleted ===================================== @@ -1,220 +0,0 @@ -(* -* -* -* HOVER -* -* -**) - -let comp (a:string) (b:string) : string = - if (String.equal a b) then "/*******-----:-):-):-):-):-):-):-)__________SUCCESS_______:-):-):-):-):-):-):-)-----*******/\n\n\n" - else "/*******-----:-(:-(:-(:-(:-(:-(:-(____FAILED___:-(:-(:-(:-(:-(:-(:-(-----*******/\n\n\n" - -let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = -let (_, ast,_) = Typer_lsp_server.compile_string content in -let (list_list, _) = Option.get ast in -let (l,c) = position in -let pos = Typer_lsp_server.pos_of_tuple position in - -let (lctx,vx) = Typer_lsp_server.lexp_search ctx list_list pos in -let ((lvn,_),lexp,ltyp) = vx in -let (l_ctx_r,_,_,_,_,_) as ret = Typer_lsp_server.browse_lexp lctx lexp pos [] in -let ret' = (l_ctx_r, None, ltyp, None, lvn,[]) in -let (_,_,l_type,_,_,_) = Typer_lsp_server.browse_list_lexp [ret;ret'] pos in - -let excpect = "excpected : " ^ expected ^ "\n" in -let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in -let input = "input : " ^ content ^ "\n" in -let res = "result : " ^ (comp expected (Lexp.lexp_string_for_lsp l_type)) in -let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in -let sep = "################################################\n" in -let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in -output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); -close_out oc - -let sep name s = -let content = "\n\n\n/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in -let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in -output_string oc content; -close_out oc - -let test_hover_rapide () = - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let name = "/home/soilih/Bureau/test/test.txt" in - hoverTest ctx name "multiply x y = x * y ;\nm = multiply 2 3;" (2,1) "##Int" - -let test_hover () = -let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in -let name = "/home/soilih/Bureau/test/test.txt" in -sep name "INT"; -hoverTest ctx name "e = 12 ;" (1,1) "##Int"; -hoverTest ctx name "e = 12 ;" (1,5) "##Int"; -sep name "STRING"; -hoverTest ctx name "s = "hejej" ;" (1,1) "##String"; -hoverTest ctx name "s = "hejej" ;" (1,8) "##String"; -sep name "FLOAT"; -hoverTest ctx name "f = 12.3 ;" (1,1) "##Float"; -hoverTest ctx name "f = 12.3 ;" (1,6) "##Float"; -sep name "LAMBDA"; -hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; -hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int"; -hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##Int"; -hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,23) ""; -hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; -hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "##Int"; -hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,20) "##Int"; -hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,24) "##Int"; -hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "##Int"; -hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,26) "##Int"; -sep name "FUNCTION(LAMBDA)"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,14) "τ"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,18) "(Int -> (Int -> Int))"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,21) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ;" (1,23) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,1) "(x : ##Int) -> (y : ##Int) -> (z : ##Int) -> Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,10) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,12) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,14) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,18) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,20) "(Int -> (Int -> Int))"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,22) "##Int"; -hoverTest ctx name "multiply x y z = x + y + z ;" (1,26) "##Int"; -sep name "CALL"; -hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; -hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,13) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,15) "##Int"; -hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,19) "##String"; -sep name "BUILTIN"; -hoverTest ctx name "foo = ##Int ;" (1,1) "##Type"; -hoverTest ctx name "foo = ##Int ;" (1,9) "##Type"; -sep name "SUSP"; -hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; -hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)"; -hoverTest ctx name "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; -hoverTest ctx name "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; -sep name "LIST"; -hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "(List ##TypeLevel.z ##Int)"; -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)"; -sep name "TUPLE"; -hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ; \n\n\ntup = (1,2,"str",lst) ;" (4,1) "typecons (Tuple) (cons ##Int ##Int ##String (List ##TypeLevel.z ##Int))"; -hoverTest ctx name "tup = (1,2,"str",false) ;" (1,8) "##Int"; -hoverTest ctx name "tup = (1,2,"str",false) ;" (1,10) "##Int"; -hoverTest ctx name "tup = (1,2,"str",false) ;" (1,15) "##String"; -hoverTest ctx name "tup = (1,2,"str",false) ;" (1,21) "Bool"; -sep name "ARROW"; -hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; -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) ""; -sep name "INDUCTIVE"; -hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; -hoverTest ctx name "type Floo = bar Int Int ;" (1,18) ""; -hoverTest ctx name "type Floo = bar Int Int ;" (1,22) ""; -hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1) ""; -hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19) ""; -hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) ""; -hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) ""; -hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; -hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; -hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; -hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18) ""; -hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24) ""; -hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32) ""; -sep name "METAVAR"; -hoverTest ctx name "x : ?t = 3 ;" (1,1) ""; -hoverTest ctx name "x : ?t = 3 ;" (1,6) ""; -hoverTest ctx name "f x = _+_ ?y x ;" (1,1) ""; -hoverTest ctx name "f x = _+_ ?y x ;" (1,3) ""; -hoverTest ctx name "f x = _+_ ?y x ;" (1,12) ""; -hoverTest ctx name "f x = _+_ ?y x ;" (1,14) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15) ""; -hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,24) ""; -sep name "LET"; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,10) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,18) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,26) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,35) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,37) ""; -hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,41) ""; -sep name "CASE"; -hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,1) ""; -hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,5) ""; -hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (1,14) ""; -hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (3,4) ""; -hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (3,13) ""; -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) "" - - -(* -* -* -* AFFICHER LA LISTE DE LISTE -* -* -**) - -let afficher_lst code filename = - let ch = open_in code in - let content = really_input_string ch (in_channel_length ch) in - close_in ch; - let (_,ast,_) = Typer_lsp_server.compile_string content in - let (list_list, _) = Option.get ast in - List.iteri (fun i x -> - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in - output_string oc ("\n\n---------------liste: " ^ (string_of_int i) ^ " --------------\n\n"); - close_out oc; - List.iteri (fun _j (y : Util.vname * Lexp.lexp * Lexp.ltype)-> - let (vn,_,_) = y in - let (l,ss) = vn in - let s = try Option.get ss - with _ -> failwith "The Var doesn't have a string!" - in - let output = "Var: " ^ s ^ "\nline: " ^ (string_of_int l.start_line) ^ " - " ^ - (string_of_int l.end_line) ^ "\ncolumn: " ^ (string_of_int l.start_column) ^ " - " - ^ (string_of_int l.end_column) ^ "\n\n" - in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in - output_string oc output; - close_out oc; - ) x - ) list_list - -(* -* -* -* BREADCRUMBS -* -* -**) -let testerBread cursor str = - let (_,ast,_) = Typer_lsp_server.compile_string str in - let (list_list, _) = Option.get ast in - let typer_loc = Typer_lsp_server.pos_of_tuple cursor in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in - let (_,_,_,_,_,lst) = Typer_lsp_server.browse_lexp ctx lexp typer_loc [] in - let str = List.fold_left ( - fun str x -> - let (_,st) = x in - (Option.get st) ^ " > " ^ str - ) "" lst in - let name = "/home/soilih/Bureau/test/symbol.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in - output_string oc ("bread: " ^ str ^ "\n") - -let bread_test = - afficher_lst "/home/soilih/Bureau/exemple.typer" "/home/soilih/Bureau/test/highlight.txt"; - testerBread (2,2) "multiply _x = \nlet lst = cons 2 nil in\nlst" \ No newline at end of file
===================================== src/typer_lsp_server.ml ===================================== @@ -46,6 +46,10 @@ type syntax_tree_elab_ctx = (syntax_tree * Debruijn.elab_context) type document_state = (log_entry list * (syntax_tree_elab_ctx option) * ((int * int) option ref))
+type completion_type = + | Expression of Debruijn.lexp_context + | FieldName of Lexp.lexp + let lsp_pos_of_a_tuple (a,b) : Lsp.Types.Position.t = Lsp.Types.Position.create ~line:(a) ~character:(b)
@@ -118,6 +122,52 @@ let dist (loc1:Source.Location.t) (loc2:Source.Location.t) = +. (((float_of_int (loc1.start_column)) -. (float_of_int (loc2.start_column))) ** 2.0 ) )
+(*Check if the cursor is in a location*) +let cursor_in_a_loc (lxp_loc: location) (cursor: location) : bool = + if ((cursor.start_line >= lxp_loc.start_line) + && (cursor.end_line <= lxp_loc.end_line) + && (cursor.start_column >= lxp_loc.start_column) + && (cursor.end_column <= lxp_loc.end_column) + ) + then true + else false + +(*take two locations and return true if the first is the nearest + and false if it's the second*) +let two_loc loc1 loc2 cursor = + if (cursor_in_a_loc loc1 cursor) + then true + else ( + if (cursor_in_a_loc loc2 cursor) + then false + else ( + if ((Int.equal loc1.start_line cursor.start_line) + && (Int.equal loc2.start_line cursor.start_line)) + then ( + if (dist loc1 cursor < dist loc2 cursor ) then true + else false + ) + else ( + if ((Int.equal loc1.start_line cursor.start_line) + && (not (Int.equal loc2.start_line cursor.start_line))) + then ( + true + ) + else ( + if ((not (Int.equal loc1.start_line cursor.start_line)) + && (Int.equal loc2.start_line cursor.start_line)) + then false + else ( + if (dist loc1 cursor < dist loc2 cursor ) then true + else false + ) + ) + ) + ) + ) + + +
(* This function extract all elements of a list in the list_list and search the nearest to the cursor *) @@ -281,60 +331,20 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De
in foo lstr cursor
- (*Check if the cursor is in a location*) - let cursor_in_a_loc (lxp_loc: location) (cursor: location) : bool = - if ((cursor.start_line >= lxp_loc.start_line) - && (cursor.end_line <= lxp_loc.end_line) - && (cursor.start_column >= lxp_loc.start_column) - && (cursor.end_column <= lxp_loc.end_column) - ) - then true - else false - (* 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 * Lexp.lexp option * Source.Location.t * vname list) list) (cursor:Source.Location.t) = + let browse_list_lexp (tab:(Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * completion_type * Source.Location.t * vname list) list) (cursor:Source.Location.t) = let rec foo tab cursor = match tab with | [] -> failwith "Liste vide!" | [n] -> n - | [hd;tl] -> let (_, _, lhd, _, loc_hd, _) = hd in - let (_, _, ltl, _, loc_tl, _) = tl in - let open Source.Location in - - if (cursor_in_a_loc loc_hd cursor) - then hd - else ( - if (cursor_in_a_loc loc_tl cursor) - then tl - else ( - if ((Int.equal loc_hd.start_line cursor.start_line) - && (Int.equal loc_tl.start_line cursor.start_line)) - then ( - if (dist loc_hd cursor < dist loc_tl cursor ) then hd - else tl - ) - else ( - if ((Int.equal loc_hd.start_line cursor.start_line) - && (not (Int.equal loc_tl.start_line cursor.start_line))) - then ( - hd - ) - else ( - if ((not (Int.equal loc_hd.start_line cursor.start_line)) - && (Int.equal loc_tl.start_line cursor.start_line)) - then tl - else ( - if (dist loc_hd cursor < dist loc_tl cursor ) then hd - else tl - ) - ) - ) - ) - ) + | [hd;tl] -> let (_, _, _, _, loc_hd, _) = hd in + let (_, _, _, _, loc_tl, _) = tl in + if(two_loc loc_hd loc_tl cursor) then hd + else tl |hd::ml::tl -> let (_, _, _, _, loc_hd, _) = hd in let (_, _, _, _, loc_ml, _) = ml in - if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor) + if (two_loc loc_hd loc_ml cursor) then (foo (hd::tl) cursor) else foo (ml::tl) cursor in foo tab cursor
@@ -357,28 +367,28 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De (* search the type of a lexp browsing a lexp *) let rec browse_lexp (ctx:Debruijn.lexp_context) (e_in:Lexp.lexp) (cursor:Source.Location.t) lst_in : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp - * Lexp.lexp option * Source.Location.t * vname list = + * completion_type * Source.Location.t * vname list =
let open Elexp in let location = Lexp.lexp_location e_in in match Lexp.lexp_lexp' e_in with - | Imm (Float (_, _)) -> (ctx, None, Debruijn.type_float, None, location, lst_in) - | Imm (Integer (_, _)) -> (ctx, None, Debruijn.type_int, None, location, lst_in) - | Imm (String (_, _)) -> (ctx, None, Debruijn.type_string, None, location, lst_in) + | Imm (Float (_, _)) -> (ctx, None, Debruijn.type_float, Expression ctx, location, lst_in) + | Imm (Integer (_, _)) -> (ctx, None, Debruijn.type_int, Expression ctx, location, lst_in) + | Imm (String (_, _)) -> (ctx, None, Debruijn.type_string, Expression ctx, location, lst_in) | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (ctx, None, Debruijn.type_string, None, location, lst_in) - | SortLevel SLz -> (ctx, None, Debruijn.type_level, None, location, lst_in) + -> (ctx, None, Debruijn.type_string, Expression ctx, location, lst_in) + | SortLevel SLz -> (ctx, None, Debruijn.type_level, Expression ctx, location, lst_in) | SortLevel (SLsucc _) - -> (ctx, None, Debruijn.type_level, None, location, lst_in) + -> (ctx, None, Debruijn.type_level, Expression ctx, location, lst_in) | SortLevel (SLlub (_, _)) - -> (ctx, None, Debruijn.type_level, None, location, lst_in) + -> (ctx, None, Debruijn.type_level, Expression ctx, location, lst_in) | Sort (l, Stype e) - -> (ctx, None, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), None, location, lst_in) - | Sort (_, StypeLevel) -> (ctx, None, Debruijn.sort_omega, None, location, lst_in) - | Sort (_, StypeOmega) -> (ctx, None, Debruijn.sort_omega, None, location, lst_in) - | Builtin (_, t)-> (ctx, None, t, None, location, lst_in) + -> (ctx, None, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), Expression ctx, location, lst_in) + | Sort (_, StypeLevel) -> (ctx, None, Debruijn.sort_omega, Expression ctx, location, lst_in) + | Sort (_, StypeOmega) -> (ctx, None, Debruijn.sort_omega, Expression ctx, location, lst_in) + | Builtin (_, t)-> (ctx, None, t, Expression ctx, location, lst_in) | Var (((l, _), _) as v) -> - (ctx, Some v, Debruijn.lctx_lookup_type ctx v, None, l, lst_in) + (ctx, Some v, Debruijn.lctx_lookup_type ctx v, Expression ctx, l, lst_in) | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor lst_in | Let (_, defs, e) -> let ctx' = @@ -394,7 +404,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De in let tab' = List.map (fun ((l, _), _, ltp) -> - (ctx', None, ltp, None, l, lst_in) + (ctx', None, ltp, Expression ctx', l, lst_in) ) defs in @@ -409,13 +419,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in let (_,_,k2,_,_,_) = browse_lexp nctx t2 cursor lst_in in match Opslexp.sort_compose ctx nctx l ak k1 k2 with - | SortResult k -> (nctx, None, k, None, location, lst_in) + | SortResult k -> (nctx, None, k, Expression nctx, location, lst_in) | SortInvalid - -> (nctx, None, Lexp.mkSort (l, StypeOmega), None, location, lst_in) + -> (nctx, None, Lexp.mkSort (l, StypeOmega), Expression nctx, location, lst_in) | SortK1NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), None, location, lst_in) + -> (nctx, None, Lexp.mkSort (l, StypeOmega), Expression nctx, location, lst_in) | SortK2NotType - -> (nctx, None, Lexp.mkSort (l, StypeOmega), None, location, lst_in) + -> (nctx, None, Lexp.mkSort (l, StypeOmega), Expression nctx, location, lst_in) )
| Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in @@ -423,7 +433,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De let b = browse_lexp ctx t cursor lst_in in (*let etp = Opslexp.get_type ctx' e in let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp), None, l, lst_in) in*) - let d = (ctx, None, t, None, l, lst_in) in + let d = (ctx, None, t, Expression ctx, l, lst_in) in browse_list_lexp ([a;b;d]) cursor
| Call (f, args) @@ -472,7 +482,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De ) cases (Lexp.mkSortLevel SLz, []) in - browse_list_lexp ((ctx, None, level, None, l, lst_in)::tab) cursor + browse_list_lexp ((ctx, None, level, Expression ctx, l, lst_in)::tab) cursor
| (_, v, t)::args -> let ctx' = Debruijn.lctx_extend ctx v Variable t in @@ -488,7 +498,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> 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 + FieldName (Opslexp.get_type ctx lxp), l, lst_in) :: [] in browse_list_lexp candidats cursor
| Case (l, e, _, branches, default) @@ -609,17 +619,17 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | (_ak, ((l,_) as vd), atype) :: fargs -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l, buildtype fargs) in - (ctx, None, buildtype fargs, None, location, lst_in) + (ctx, None, buildtype fargs, Expression ctx, location, lst_in) with Not_found - -> (ctx, None, Debruijn.type_int, None, location, lst_in) + -> (ctx, None, Debruijn.type_int, Expression ctx, location, lst_in) ) - | _ -> (ctx, None, Debruijn.type_int, None, location, lst_in)) + | _ -> (ctx, None, Debruijn.type_int, Expression ctx, location, lst_in))
| Metavar (idx, s, _) -> (match Lexp.metavar_lookup idx with | MVal e -> let e = Lexp.push_susp e s in browse_lexp ctx e cursor lst_in - | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, None, location, lst_in)) + | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, Expression ctx, location, lst_in))
(*====================================Lexp parcourir===================================*) @@ -655,7 +665,7 @@ let use_search_name_in_ctx lctx lxp =
(*====================================Definition===================================*)
-let find_def_location (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Lexp.lexp option * Source.Location.t * vname list) : Source.Location.t = +let find_def_location (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * completion_type * Source.Location.t * vname list) : Source.Location.t = let (lctx,vr,_,_,_,_) = ret in match vr with | None -> failwith "No defintion found !" @@ -843,7 +853,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Sort (_, StypeLevel) -> ret | Sort (_, StypeOmega) -> ret | Susp (e, s) -> find_references (Lexp.push_susp e s) vr idx_vr ret - | Builtin (_, _) -> ret + | Builtin (_, e) -> find_references e vr idx_vr ret | Var (vn, idx) -> let (l, v1) = vn in let (_, v2) = vr in @@ -889,11 +899,11 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = let (ret_list,_) = List.fold_left ( - fun (ret,i) (_, _v, t) -> + fun (ret, i) (_, _v, t) -> ( (((find_references t vr i ret)), i + 1) ) - ) (ret,i) case + ) (ret, i) case in ret_list ) @@ -901,7 +911,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = lst
| (_, _, t)::args - -> arg_loop args (i+1) (find_references t vr i ret_lst) + -> arg_loop args (i + 1) (find_references t vr i ret_lst) in arg_loop args 0 ret ) @@ -937,7 +947,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Sort (_, Stype e) -> browse_defs e cursor | Sort (_, StypeLevel) -> None | Sort (_, StypeOmega) -> None - | Builtin (_, _) -> None + | Builtin (_, e) -> browse_defs e cursor | Var _ -> None | Susp (e, s) -> browse_defs (Lexp.push_susp e s) cursor | Let (_, defs, el) @@ -997,22 +1007,39 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = browse_defs lxp cursor) args None))
| Inductive (l, _label, args, cases) - (*(Lexp.arg_kind * vname * Lexp.lexp) list SMap.t*) - -> let (_, lst) = List.hd (SMap.bindings cases) in - let rec foo cursor lst = - match lst with + -> let lst = SMap.bindings cases in + + let rec foo2 cursor args comp = + match args with | [] -> failwith "cursor is not on a vdef" - | (_, vn, lxp)::tl - -> if (vn_on_the_cursor vn cursor) then Some (lxp, vn, List.length tl) + | (_, vn, _)::tl + -> let ldum = Source.Location.dummy in + let mySmap = SMap.empty in + let tl_map = SMap.add "nokey" tl mySmap in + let lxp = Lexp.mkInductive + (ldum, (ldum, ""), tl, tl_map) + in + if (vn_on_the_cursor vn cursor) then Some (lxp, vn, -comp) else( let ret = browse_defs lxp cursor in match ret with | Some _ -> ret - | None -> foo cursor tl) - in + | None -> foo2 cursor tl (comp + 1)) + in + let rec foo cursor lst = + match lst with + | [] -> failwith "cursor is not on a vdef" + | (_, ls)::tl + -> (let rec foo' cursor ls comp = + match ls with + | [] -> foo cursor tl + | _ -> foo2 cursor ls comp + in foo' cursor ls 0 + ) + in ( try foo cursor lst - with _ -> foo cursor args + with _ -> foo2 cursor args 0 ) | Proj (_, e, (_, _)) -> browse_defs e cursor | Case (_, e, _, branches, _) @@ -1295,7 +1322,7 @@ class lsp_server =
match browse_lexp ctx lexp typer_loc [] with
- | (l_ctx,_,_, None,_,_) + | (_, _, _, Expression l_ctx, _, _) -> 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 @@ -1310,7 +1337,7 @@ class lsp_server = let e = Some (`List comp_list_ret) in let f = Linol_lwt.return e in f
- | (lctx, _, _, Some lxp, _,_) + | (lctx, _, _, FieldName lxp, _,_) -> (let ret = Opslexp.lexp_whnf lxp lctx in match Lexp.lexp_lexp' ret with | Inductive (_, (_,label), fargs, constructors) @@ -1423,11 +1450,415 @@ class lsp_server = end
+ + +(* +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +************************* TEST THE SERVER *************************** +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +*) + + +(** +* +* +* HOVER +* +* +**) + +let comp (a:string) (b:string) : string = + if (String.equal a b) then "*******-------__________SUCCESS__________-------*******\n\n\n" + else "-------*******__________FAILED__________*******-------\n\n\n" + +let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = +let (_, ast, _) = compile_string content in +let (list_list, _) = Option.get ast in +let (l,c) = position in +let pos = pos_of_tuple position in + +(* +let (lctx, vx) = lexp_search ctx list_list pos in +let ((lvn, _), lexp, ltyp) = vx in +let (l_ctx_r,_,_,_,_,_) as ret = browse_lexp lctx lexp pos [] in +let ret' = (l_ctx_r, None, ltyp, (Expression l_ctx_r : completion_type), lvn,[]) in +let (_,_,l_type,_,_,_) = browse_list_lexp [ret;ret'] pos in +*) + +let lexp = trans_list_in_list_to_let list_list in +let (l_ctx, _, l_type, _, _, _) = browse_lexp ctx lexp pos [] in +let s = try use_search_name_in_ctx l_ctx l_type + with _ -> Lexp.lexp_string_for_lsp l_type +in +let excpect = "excpected : " ^ expected ^ "\n" in +let output = "output : " ^ s ^ "\n\n" in +let input = "input : " ^ content ^ "\n" in +let res = "result : " ^ (comp expected s) in +let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in +let sep = "################################################\n" in +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in +output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); +close_out oc + +let sep name s = +let content = "\n\n\n/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in +output_string oc content; +close_out oc + +let test_hover () = + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let name = "/home/soilih/Bureau/test/test.txt" in + sep name "INT"; + hoverTest ctx name "e = 12 ;" (1,1) "Int"; + hoverTest ctx name "e = 12 ;" (1,5) "Int"; + sep name "STRING"; + hoverTest ctx name "s = "hejej" ;" (1,1) "String"; + hoverTest ctx name "s = "hejej" ;" (1,8) "String"; + sep name "FLOAT"; + hoverTest ctx name "f = 12.3 ;" (1,1) "Float"; + hoverTest ctx name "f = 12.3 ;" (1,6) "Float"; + sep name "LAMBDA"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21) "Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,20) "Int"; + hoverTest ctx name "l = (lambda x y -> x + y) ;" (1,24) "Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,24) "Int"; + hoverTest ctx name "l = (lambda x y -> _+_ x y) ;" (1,26) "Int"; + sep name "FUNCTION(LAMBDA)"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,14) "τ"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,18) "(Int -> (Int -> Int))"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,21) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,23) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,1) "(x : ##Int) -> (y : ##Int) -> (z : ##Int) -> Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,10) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,12) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,14) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,18) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,20) "(Int -> (Int -> Int))"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,22) "Int"; + hoverTest ctx name "multiply x y z = x + y + z ;" (1,26) "Int"; + sep name "CALL"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,13) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,15) "Int"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,19) "String"; + sep name "BUILTIN"; + hoverTest ctx name "foo = ##Int ;" (1,1) "Type"; + hoverTest ctx name "foo = ##Int ;" (1,9) "Type"; + sep name "SUSP"; + hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; + hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)"; + hoverTest ctx name "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; + hoverTest ctx name "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; + sep name "LIST"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "(List ##Int)"; + 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)"; + sep name "TUPLE"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ; \n\n\ntup = (1,2,"str",lst) ;" (4,1) "typecons (Tuple) (cons ##Int ##Int ##String (List ##TypeLevel.z ##Int))"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,8) "Int"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,10) "Int"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,15) "String"; + hoverTest ctx name "tup = (1,2,"str",false) ;" (1,21) "Bool"; + sep name "ARROW"; + hoverTest ctx name "type Floo = bar Int Int ;" (1,1) ""; + 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) ""; + sep name "INDUCTIVE"; + hoverTest ctx name "type Floo = bar Int Int ;" (1,7) ""; + hoverTest ctx name "type Floo = bar Int Int ;" (1,18) ""; + hoverTest ctx name "type Floo = bar Int Int ;" (1,22) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) ""; + hoverTest ctx name "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; + hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,1) ""; + hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,10) ""; + hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,18) ""; + hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,24) ""; + hoverTest ctx name "Bool = typecons (Bool) (true) (false);" (1,32) ""; + sep name "METAVAR"; + hoverTest ctx name "x : ?t = 3 ;" (1,1) "τ"; + hoverTest ctx name "x : ?t = 3 ;" (1,6) "τ"; + hoverTest ctx name "f x = _+_ ?y x ;" (1,1) "(y : Int) => (x : ##Int) -> Int"; + hoverTest ctx name "f x = _+_ ?y x ;" (1,3) "Int"; + hoverTest ctx name "f x = _+_ ?y x ;" (1,12) "Int"; + hoverTest ctx name "f x = _+_ ?y x ;" (1,14) "Int"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1) "Int"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6) "Int"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10) "Int"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1) "Int"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11) "τ"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15) "τ"; + hoverTest ctx name "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,25) "Int"; + sep name "LET"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1) "Int"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,11) "Int"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,19) "Int"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,31) "Int"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,36) "Int"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,38) "(Int -> (Int -> Int))"; + hoverTest ctx name "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,44) "Int"; + sep name "CASE"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (2,1) "((List Int) -> (Option Int))"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (2,7) "List Int"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (2,18) "List Int"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (3,11) "Int"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (3,33) "Int"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (4,11) "Int"; + hoverTest ctx name "last : List Int -> Option Int ;\nlast lst = case lst\n | cons just_one nil => some just_one\n | cons first list_tl => last list_tl;" + (4,18) "List Int" + + +(* +* +* +* AFFICHER LA LISTE DE LISTE +* +* +**) + +let afficher_lst code filename = + let ch = open_in code in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = compile_string content in + let (list_list, _) = Option.get ast in + List.iteri (fun i x -> + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + output_string oc ("\n\n---------------liste: " ^ (string_of_int i) ^ " --------------\n\n"); + close_out oc; + List.iteri (fun _j (y : Util.vname * Lexp.lexp * Lexp.ltype)-> + let (vn,_,_) = y in + let (l,ss) = vn in + let s = try Option.get ss + with _ -> failwith "The Var doesn't have a string!" + in + let output = "Var: " ^ s ^ "\nline: " ^ (string_of_int l.start_line) ^ " - " ^ + (string_of_int l.end_line) ^ "\ncolumn: " ^ (string_of_int l.start_column) ^ " - " + ^ (string_of_int l.end_column) ^ "\n\n" + in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + output_string oc output; + close_out oc; + ) x + ) list_list + +(** +* +* +* BREADCRUMBS +* +* +**) +let testerBread cursor str = + let (_,ast,_) = compile_string str in + let (list_list, _) = Option.get ast in + let typer_loc = pos_of_tuple cursor in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let lexp = trans_list_in_list_to_let list_list in + let (_,_,_,_,_,lst) = browse_lexp ctx lexp typer_loc [] in + let str = List.fold_left ( + fun str x -> + let (_,st) = x in + (Option.get st) ^ " > " ^ str + ) "" lst in + let name = "/home/soilih/Bureau/test/symbol.txt" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + output_string oc ("bread: " ^ str ^ "\n") + +let bread_test = + testerBread (2,2) "multiply _x = \nlet lst = cons 2 nil in\nlst" + +(** +* +* +* GoTo Definition +* +* +**) + +let defTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) = + let (_, ast, _) = compile_string content in + let (list_list, _) = Option.get ast in + let (l, c) = position in + let pos = pos_of_tuple position in + + let lexp = trans_list_in_list_to_let list_list in + let ret = browse_lexp ctx lexp pos [] in + let loc = find_def_location ret in + + let output = "output-:- " ^ "line: " ^ (string_of_int (loc.start_line)) + ^ "column: " ^ (string_of_int (loc.start_column)) ^ "\n\n" in + let input = "input : " ^ content ^ "\n" in + let pos = "position : line " ^ (string_of_int l) ^ " character " ^ (string_of_int c) ^ "\n" in + let sep = "################################################\n" in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + output_string oc (sep ^ input ^ pos ^ output ^ sep ); + close_out oc + + +let test_definition () = + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let name = "/home/soilih/Bureau/test/test.txt" in + defTest ctx name "multiply : ? ;\nmultiply x y = _*_ x y ;\nsix = multiply 2 3" (2,20); + defTest ctx name "multiply : ? ;\nmultiply x y = _*_ x y ;\nsix = multiply 2 3" (3,10) + +(* List of separators that delimit a word *) +let sep_list = [';';',';'(';')';' ';'{';'}';'.'] + +(** +* +* +* Completion +* +* +**) + +let completionTest (ctx:Debruijn.lexp_context) (content:string) (position: int * int) = + let (_, ast, _) = compile_string content in + let (list_list, _) = Option.get ast in + let (l, c) = position in + let pos = pos_of_tuple position in + let lexp = trans_list_in_list_to_let list_list in + ( + match browse_lexp ctx lexp pos [] with + | (_, _, _, Expression l_ctx, _, _) + -> let my_str = split_string_line content (l + 1) in + let word = use_search_word my_str sep_list c "" in + let range = lsp_range_of_a_tuple + (pos.start_line,(pos.end_column - String.length word)) + (pos.end_line, pos.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 + List.map (fun (x : Lsp.Types.CompletionItem.t) -> + let detail = Option.get x.detail in + x.label ^ " (" ^ detail ^ ")") + comp_list_ret + + | (lctx, _, _, FieldName lxp, _,_) + -> (let ret = Opslexp.lexp_whnf lxp lctx in + match Lexp.lexp_lexp' ret with + | Inductive (_, (_,label), fargs, constructors) + when Util.SMap.cardinal constructors = 1 + -> let my_str = split_string_line content (l + 1) in + let word = use_search_word my_str sep_list c "" in + let range = lsp_range_of_a_tuple + (pos.start_line,(pos.end_column - String.length word)) + (pos.end_line, pos.end_column) + in + let (_, fieldtypes) = List.hd (Util.SMap.bindings constructors) in + let comp_list = + List.map ( fun (x : Lexp.arg_kind * Util.vname * Lexp.lexp) -> + let (_,(_,s),t) = x in + 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 + ~label:str ~kind:kind + ~textEdit:textEdit ~detail:(Lexp.lexp_string_for_lsp t) () + in + ci + ) fieldtypes + in + List.map (fun (x : Lsp.Types.CompletionItem.t) -> + let detail = Option.get x.detail in + x.label ^ " (" ^ detail ^ ")") + comp_list + | _ -> failwith "Our Lexp is not an Inductive Type!!!" + ) + ) + +let test_completion () = + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let name = "/home/soilih/Bureau/test/completion.txt" in + let ret = completionTest ctx "multiply : ? ;\nmultiply x y = _*_ x y ;\nn = m" (3,5) in + (*let ret' = completionTest ctx "multiply : ? ;\nmultiply x y = _*_ x y ;\nn = list.m" (3,10) in*) + let wr = List.fold_right (fun (s : string) r -> + r ^ s ^ "\n" + ) ret "" + in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + output_string oc wr; + close_out oc + +let highlightTest(ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) = + let (_, ast, _) = compile_string content in + let (list_list, _) = Option.get ast in + let pos = pos_of_tuple position in + let lexp = trans_list_in_list_to_let list_list in + let (lxp, vn, idx) = try Option.get (browse_defs lexp pos) + with _ + -> Log.log_error ~loc:(Lexp.lexp_location lexp) "No highlight found!"; + (Lexp.impossible, (Util.dummy_location, None), 0) + in + let ret = find_references lxp vn idx [vn] in + let ret' = List.fold_right (fun (vn: Util.vname) r -> + let (l, s) = vn in + let s' = Option.get s in + r ^ s' ^ " (l: " ^ ((string_of_int l.start_line)) + ^ "-" ^ ((string_of_int l.end_line)) + ^ " c: " ^ ((string_of_int l.start_column)) + ^ "-" ^ ((string_of_int l.end_column)) ^ ")" + ) ret "" + in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + output_string oc ret'; + close_out oc + +let test_highlight () = + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + let name = "/home/soilih/Bureau/test/highlight.txt" in + highlightTest ctx name "multiply : ? ;\nmultiply x y = _*_ x y ;\nsix = multiply 2 3 ;\ndix = multiply 2 5" (2,4) + + +(* +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +************************ END OF THE TESTS *************************** +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +*) + + + + (* Main code This is the code that creates an instance of the lsp server class and runs it as a task. *) let run () = ignore (Log.lsp_enabled := true); + test_hover (); 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/debc7c1fc74f9b220c2b4446fe3814059...
Afficher les réponses par date