Soilihi BEN SOILIHI BOINA pushed to branch soilih at Stefan / Typer
Commits: 5025a06d by Soilih BEN SOILIH at 2021-07-13T10:53:05-06:00 test hover
- - - - - 29b5783a by Soilih BEN SOILIH at 2021-07-13T10:55:44-06:00 test hover.
- - - - -
1 changed file:
- src/typer_lsp_server.ml
Changes:
===================================== src/typer_lsp_server.ml ===================================== @@ -55,6 +55,12 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint
+let pos_of_tuple (p:int * int) : Source.Location.t = + let (line,col) = p in + let open Source.Location in + let dc = Some "" in + let typer_pos = {file = ""; start_line = line; start_column = col; end_line = line; end_column = col; doc = dc } in + typer_pos
let typer_pos_of_lsp_pos (p:Lsp.Types.Position.t) : Source.Location.t = let open Source.Location in @@ -287,17 +293,17 @@ end else foo (ml::tl) cursor in foo lexp_list cursor
- let browse_list_lexp (tab:(Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = + let browse_list_lexp (tab:(Debruijn.lexp_context * Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = let rec foo tab cursor = match tab with | [] -> failwith "Liste vide!" | [n] -> n - | [hd;tl] -> let (_,loc_hd) = hd in - let (_,loc_tl) = tl in + | [hd;tl] -> let (_,_,loc_hd) = hd in + let (_,_,loc_tl) = tl in if (dist loc_hd cursor < dist loc_tl cursor ) then hd else tl - |hd::ml::tl -> let (_,loc_hd) = hd in - let (_,loc_ml) = ml in + |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) else foo (ml::tl) cursor in foo tab cursor @@ -330,26 +336,27 @@ end (lctx,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) : Lexp.lexp * Source.Location.t = + let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp * Source.Location.t =
let open Elexp in let location = Lexp.lexp_location e in match Lexp.lexp_lexp' e with - | Imm (Float (_, _)) -> (Debruijn.type_float, location) - | Imm (Integer (_, _)) -> (Debruijn.type_int, location) - | Imm (String (_, _)) -> (Debruijn.type_string, location) - | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (Debruijn.type_string, location) - | SortLevel SLz -> (Debruijn.type_level, location) + | Imm (Float (_, _)) -> (ctx, Debruijn.type_float, location) + | Imm (Integer (_, _)) -> (ctx, Debruijn.type_int, location) + | Imm (String (_, _)) -> (ctx, Debruijn.type_string, location) + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> (ctx, Debruijn.type_string, location) + | SortLevel SLz -> (ctx, Debruijn.type_level, location) | SortLevel (SLsucc e) - -> (Debruijn.type_level, location) + -> (ctx, Debruijn.type_level, location) | SortLevel (SLlub (e1, e2)) - -> (Debruijn.type_level, location) + -> (ctx, Debruijn.type_level, location) | Sort (l, Stype e) - -> (Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location) - | Sort (_, StypeLevel) -> (Debruijn.sort_omega, location) - | Sort (_, StypeOmega) -> (Debruijn.sort_omega, location) - | Builtin (_, t)-> (t, location) - | Var (((l, name), idx) as v) -> (Debruijn.lctx_lookup_type ctx v, location) + -> (ctx, Lexp.mkSort (l, Stype (Lexp.mkSortLevel (SLsucc e))), location) + | Sort (_, StypeLevel) -> (ctx, Debruijn.sort_omega, location) + | Sort (_, StypeOmega) -> (ctx, Debruijn.sort_omega, location) + | Builtin (_, t)-> (ctx, t, location) + | Var (((l, name), idx) as v) -> + (ctx, Debruijn.lctx_lookup_type ctx v, location) | Susp (e, s) -> browse_lexp ctx (Lexp.push_susp e s) cursor | Let (l, defs, e) -> let ctx' = @@ -364,31 +371,32 @@ end defs in
- let (ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in + let (ctx'', ret,loc) = browse_list_lexp ((browse_lexp ctx' e cursor)::tab) cursor in
- (Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc) + (ctx'', Lexp.mkSusp ret (Opslexp.lexp_defs_subst l Subst.identity defs),loc)
| Arrow (ak, v, t1, l, t2) -> ( let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in match Opslexp.sort_compose ctx nctx l ak t1 t2 with - | SortResult k -> (k, location) + | SortResult k -> (nctx, k, location) | SortInvalid - -> (Lexp.mkSort (l, StypeOmega), location) + -> (nctx, Lexp.mkSort (l, StypeOmega), location) | SortK1NotType - -> (Lexp.mkSort (l, StypeOmega), location) + -> (nctx, Lexp.mkSort (l, StypeOmega), location) | SortK2NotType - -> (Lexp.mkSort (l, StypeOmega), location) + -> (nctx, 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 (ret,loc) = browse_list_lexp (a::b::[]) cursor in - (Lexp.mkArrow (ak, v, t, l,ret), loc) + let c = (ctx,t,l) in + let (ctx'',ret,loc) = browse_list_lexp (a::b::c::[]) cursor in + (ctx'', ret, loc)
| Call (f, args) -> ( - let fonc = browse_lexp ctx f cursor in + let fonc = browse_lexp ctx f cursor in let args_list = List.map (fun (_ , e) -> browse_lexp ctx e cursor) args @@ -398,14 +406,15 @@ end )
| Inductive (l, _label, args, cases) - ->( + ->( + let rec arg_loop ctx erased args = match args with | [] -> let level = SMap.fold (fun _ case level -> - let (level, _, _, _) = + let (level, rctx, _, _) = List.fold_left (fun (level, ictx, erased, n) (ak, v, t) -> ((let lwhnf = Opslexp.lexp_whnf t ictx in @@ -415,10 +424,6 @@ end -> level | Sort (_, Stype level') -> Opslexp.mkSLlub ctx level - (* We need to unshift because the final type - * cannot refer to the fields! *) - (* FIXME: If it does refer, - * we get an ugly error! *) (Lexp.mkSusp level' (Lexp.sunshift n)) | _tt -> level), Debruijn.lctx_extend ictx v Variable t, @@ -428,7 +433,7 @@ end case in level) cases (Lexp.mkSortLevel SLz) in - Lexp.mkSort (l, Stype level) + Lexp.mkSort (l, Stype level) | (ak, v, t)::args -> let _k = t in Lexp.mkArrow (ak, v, t, Lexp.lexp_location t, @@ -436,7 +441,7 @@ end (Opslexp.dbset_push ak erased) args) in let tct = arg_loop ctx Debruijn.set_empty args in - (tct, location) + (ctx, tct, location) )
| Case (l, e, ret, branches, default) @@ -524,12 +529,12 @@ end let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp ctx d cursor) :: !candidats; + candidats := (browse_lexp nctx d cursor) :: !candidats; browse_lexp nctx d cursor | None - -> if diff > 0 then (); (Lexp.impossible, Source.Location.dummy) + -> if diff > 0 then (); (ctx, Lexp.impossible, Source.Location.dummy) ) - | _,_ -> (Lexp.impossible, Source.Location.dummy) ; + | _,_ -> (ctx, Lexp.impossible, Source.Location.dummy) ;
browse_list_lexp !candidats cursor
@@ -560,18 +565,17 @@ end | (_ak, ((l,_) as vd), atype) :: fargs -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l, buildtype fargs) in - (buildtype fargs, location) + (ctx, buildtype fargs, location) with Not_found - -> (Debruijn.type_int, location) + -> (ctx, Debruijn.type_int, location) ) - | _ -> (Debruijn.type_int, location)) + | _ -> (ctx, Debruijn.type_int, location))
| Metavar (idx, s, _) -> (match Lexp.metavar_lookup idx with | MVal e -> let e = Lexp.push_susp e s in - let (e', loc) = browse_lexp ctx e cursor in - (e',loc) - | MVar (_, t, _) -> (Lexp.push_susp t s, location)) + browse_lexp ctx e cursor + | MVar (_, t, _) -> (ctx, Lexp.push_susp t s, location))
let lexp_parcourir ctx e = let lctx = Debruijn.ectx_to_lctx ctx in @@ -588,27 +592,29 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Sour let open Elexp in (*let location = Lexp.lexp_location e in*) match Lexp.lexp_lexp' e with - | Imm (Float (_, _)) -> Source.Location.dummy - | Imm (Integer (_, _)) -> Source.Location.dummy - | Imm (String (_, _)) -> Source.Location.dummy - | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> Source.Location.dummy + | Imm (Float (l, _)) -> l + | Imm (Integer (l, _)) -> l + | Imm (String (l, _)) -> l + | Imm (Block (l, _)) -> l + | Imm (Symbol (l,_)) -> l + | Imm (Node (_, _)) -> Source.Location.dummy | SortLevel SLz -> Source.Location.dummy | SortLevel (SLsucc e) -> Source.Location.dummy | SortLevel (SLlub (e1, e2)) -> Source.Location.dummy - | Sort (l, Stype e) -> Source.Location.dummy - | Sort (_, StypeLevel) -> Source.Location.dummy - | Sort (_, StypeOmega) -> Source.Location.dummy - | Builtin (_, t) -> Source.Location.dummy - | Var (((l, name), idx) as v) -> Source.Location.dummy + | Sort (l, Stype e) -> l + | Sort (l, StypeLevel) -> l + | Sort (l, StypeOmega) -> l + | Builtin ((l,_), t) -> l + | Var (((l, name), idx) as v) -> l | Susp (e, s) -> Source.Location.dummy | Let (l, defs, e) -> Source.Location.dummy - | Arrow (ak, v, t1, l, t2) -> Source.Location.dummy - | Lambda (ak, ((l,_) as v), t, e) -> Source.Location.dummy + | Arrow (ak, v, t1, l, t2) -> let (l,_) = v in l + | Lambda (ak, ((l,_) as v), t, e) -> l | Call (f, args) -> Source.Location.dummy - | Inductive (l, _label, args, cases) -> Source.Location.dummy - | Case (l, e, ret, branches, default) -> Source.Location.dummy - | Cons (t, (_l, name)) -> Source.Location.dummy - | Metavar (idx, s, _) -> Source.Location.dummy + | Inductive (l, _label, args, cases) -> l + | Case (l, e, ret, branches, default) -> l + | Cons (t, (_l, name)) -> _l + | Metavar (idx, s, (l,_)) -> l
(*====================================Definition===================================*)
@@ -667,7 +673,10 @@ class lsp_server = (*let r = Option.get(search_lexp_with_a_location list_list typer_loc) in*) let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,lexp) = lexp_search ctx list_list typer_loc in - let loc = find_def_location lctx lexp typer_loc in + let (l_ctx, l_lexp,_) = browse_lexp lctx lexp typer_loc in + let (_, db_index) = lexp in(*let loc = find_def_location lctx lexp typer_loc in*) + (*failwith (string_of_int (Myers.length l_ctx));*) + let ((loc,_),_,_) = Myers.nth db_index l_ctx in let l = Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc loc) in @@ -675,7 +684,6 @@ class lsp_server = let f = Linol_lwt.return (Some ret) in f
- method! on_req_hover ~notify_back ~id ~uri ~pos doc_state = match Hashtbl.find buffers uri with
@@ -684,7 +692,7 @@ class lsp_server = let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,lexp) = lexp_search ctx list_list typer_loc in - let (l_type,location) = browse_lexp lctx lexp typer_loc in + let (l_ctx, l_type,location) = browse_lexp lctx lexp typer_loc in let range = lsp_range_of_loc location in let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create @@ -717,7 +725,7 @@ class lsp_server = emacs. It makes completion too slow *) Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; """; "'"; "/"; "@"; "<"] ~resolveProvider:true () in - { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider } + { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider}
(* provisional, to be done later *) @@ -754,12 +762,133 @@ class lsp_server =
end
+ +(*=======================================Test======================================*) +let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) = + let (_, ast) = readstring content in + let (list_list, _) = ast in + let (l,c) = position in + let pos = pos_of_tuple position in + let (lctx,lexp) = lexp_search ctx list_list pos in + let (_, l_type,_) = browse_lexp lctx lexp pos in + let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\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 sep name s = + let content = "/*-----------------------------" ^ 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 () = + 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); + hoverTest ctx name "e = 12 ;" (1,5); + sep name "STRING"; + hoverTest ctx name "s = "hejej" ;" (1,1); + hoverTest ctx name "s = "hejej" ;" (1,8); + sep name "FLOAT"; + hoverTest ctx name "f = 12.3 ;" (1,1); + hoverTest ctx name "f = 12.3 ;" (1,6); + sep name "LAMBDA"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1); + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8); + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13); + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,19); + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,21); + sep name "FUNCTION(LAMBDA)"; + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,10); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,12); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,17); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,19); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,22); + hoverTest ctx name "multiply x y z = _*_ x y ;" (1,24); + sep name "CALL"; + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1); + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,7); + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,13); + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,15); + hoverTest ctx name "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,19); + sep name "BUILTIN"; + hoverTest ctx name "foo = ##Int ;" (1,1); + hoverTest ctx name "foo = ##Int ;" (1,9); + sep name "SUSP"; + hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,1); + hoverTest ctx name "foo = ##Int ; \n\n\nv = foo ;" (4,6); + sep name "LIST"; + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1); + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8); + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12); + hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27); + sep name "ARROW"; + hoverTest ctx name "type Floo = bar Int Int ;" (1,1); + 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 "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 "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 => "h"\n\n| false => "jj" ;" (1,1); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (1,5); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (1,14); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,4); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (3,13); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,4); + hoverTest ctx name "foo x = case x\n\n| true => "h"\n\n| false => "jj" ;" (5,14) + + +(*=======================================Test======================================*) + + (* Main code This is the code that creates an instance of the lsp server class and runs it as a task. *) let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); + test (); 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/ba970f5cec20dca8236971c1352bfeaf8...