Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer

Commits: 810e0e5e by Soilih at 2022-07-27T00:11:35-04:00 adding a new type to specify the completion type

- - - - -

2 changed files:

- src/lsp_server_test.ml - src/typer_lsp_server.ml

Changes:

===================================== src/lsp_server_test.ml ===================================== @@ -11,7 +11,7 @@ let comp (a:string) (b:string) : string = 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 (_, 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 @@ -19,7 +19,7 @@ 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 ret' = (l_ctx_r, None, ltyp, (Expression l_ctx_r : Typer_lsp_server.completion_type), lvn,[]) in let (_,_,l_type,_,_,_) = Typer_lsp_server.browse_list_lexp [ret;ret'] pos in

let excpect = "excpected : " ^ expected ^ "\n" in @@ -41,7 +41,8 @@ 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" + (*hoverTest ctx name "multiply x y = x * y ;\nm = multiply 2 3;" (2,1) "##Int"*) + hoverTest ctx name "lst = cons 1 nil" (1,8) ""

let test_hover () = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in

===================================== 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 !" @@ -998,34 +1008,12 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) =

| Inductive (l, _label, args, cases) -> let lst = SMap.bindings cases 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 - | (_, vn, _)::tail - -> let ldum = Source.Location.dummy in - let mySmap = SMap.empty in - let tl_map = SMap.add "nokey" tail mySmap in - let lxp = Lexp.mkInductive - (ldum, (ldum, ""), tail, 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 tail (comp + 1)) - in foo' cursor ls 0 - ) - in + let rec foo2 cursor args comp = match args with | [] -> failwith "cursor is not on a vdef" | (_, vn, _)::tl - -> let ldum = Source.Location.dummy in + -> let ldum = Source.Location.dummy in let mySmap = SMap.empty in let tl_map = SMap.add "nokey" tl mySmap in let lxp = Lexp.mkInductive @@ -1038,6 +1026,17 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Some _ -> ret | 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 _ -> foo2 cursor args 0 @@ -1323,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 @@ -1338,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)

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/810e0e5eb03291742d7ea3f01928aad064...