[Typer] [Git][monnier/typer][soilih] considerate vname loc and ltype

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

Commits: 9d9ea020 by Soilih BEN SOILIH at 2021-09-27T15:05:21-06:00 considerate vname loc and ltype

- - - - -

2 changed files:

- src/REPL.ml - src/typer_lsp_server.ml

Changes:

===================================== src/REPL.ml ===================================== @@ -150,6 +150,8 @@ let eval_interactive

List.iter interactive#process_decls ldecls; print_and_clear_log (); + + List.iter Lexp.lexp_print lexprs;

let values = List.map interactive#eval_expr lexprs in List.iter (Eval.print_eval_result i) values;

===================================== src/typer_lsp_server.ml ===================================== @@ -125,13 +125,12 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list)

match liste with | [] -> failwith "No Lexp found!!!" - | [n] -> let (_,lxp,_) = n in - lxp + | [n] -> n | [hd;tl] -> let (_,lxp_hd,_) = hd in let (_,lxp_tl,_) = tl in if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_tl) cursor ) - then lxp_hd - else lxp_tl + then hd + else tl | hd::ml::tl -> let (_,lxp_hd,_) = hd in let (_,lxp_ml,_) = ml in if (dist (Lexp.lexp_location lxp_hd) cursor < dist (Lexp.lexp_location lxp_ml) cursor ) @@ -376,16 +375,17 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

let lstr = update_the_context ctx lst in

- let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) = match ls with | [] -> failwith "No Lexp found!" | hd::tl -> let (lctx_hd, hdl) = hd in - let lxp = nearest_lexp_of_the_list hdl cursor in + let v = nearest_lexp_of_the_list hdl cursor in + let (_,lxp,_) = v in let location = Lexp.lexp_location lxp in if ((location.start_line <= cursor.start_line && location.start_column <= cursor.start_column) && (location.end_line >= cursor.end_line && location.end_column >= cursor.end_column)) - then (lctx_hd,lxp) + then (lctx_hd, v) else foo tl cursor in foo lstr cursor

@@ -394,18 +394,18 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

let lstr = update_the_context ctx lst in

- let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : Debruijn.lexp_context * Lexp.lexp = + let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) =

match ls with | [] -> failwith "No Lexp found!" | [n] -> let (lctx,l) = n in - let lxp = nearest_lexp_of_the_list l cursor in - (lctx,lxp) + let v = nearest_lexp_of_the_list l cursor in + (lctx,v) | [hd;tl] -> let (lctx_hd,hdl) = hd in let (lctx_tl,tll) = tl in - let lxp = nearest_lexp_of_the_list hdl cursor in - let lxp' = nearest_lexp_of_the_list tll cursor in - if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + let (_,x,_) as lxp = nearest_lexp_of_the_list hdl cursor in + let (_,y,_) as lxp' = nearest_lexp_of_the_list tll cursor in + if (dist (Lexp.lexp_location x) cursor < dist (Lexp.lexp_location y) cursor ) then (lctx_hd,lxp) else ( @@ -413,9 +413,9 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | hd::ml::tl -> let (lctx_hd,hdl) = hd in let (lctx_ml,mll) = ml in - let lxp = nearest_lexp_of_the_list hdl cursor in - let lxp' = nearest_lexp_of_the_list mll cursor in - if (dist (Lexp.lexp_location lxp) cursor < dist (Lexp.lexp_location lxp') cursor ) + let (_,x,_) as lxp = nearest_lexp_of_the_list hdl cursor in + let (_,y,_) as lxp' = nearest_lexp_of_the_list mll cursor in + if (dist (Lexp.lexp_location x) cursor < dist (Lexp.lexp_location y) cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor

@@ -502,9 +502,10 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | 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 etp = Opslexp.get_type ctx' e in - let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in - browse_list_lexp ([a;b;c]) cursor + (*let etp = Opslexp.get_type ctx' e in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) + let d = (ctx,None, t,l) in + browse_list_lexp ([a;b;d]) cursor

| Call (f, args) -> ( @@ -789,7 +790,7 @@ let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * str 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 + let (_,lxp,_) = nearest_lexp_of_the_list liste cursor in browse_lexp lctx lxp cursor ) lst in List.filter (fun x -> @@ -983,7 +984,8 @@ class lsp_server = 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,lexp) = lexp_search ctx list_list typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let (_,lexp,_) = vx in let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in let loc = find_def_location l_ctx ret in let l = Lsp.Types.Location.create @@ -1000,8 +1002,11 @@ class lsp_server = 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,lexp) = lexp_search ctx list_list typer_loc in - let (l_ctx,_,l_type,location) = browse_lexp lctx lexp typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let ((lvn,_),lexp,ltyp) = vx in + let (l_ctx_r,_,_,_) as ret = browse_lexp lctx lexp typer_loc in + 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 r = Lsp.Types.Hover.create @@ -1045,7 +1050,8 @@ class lsp_server = 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,lexp) = lexp_search ctx list_list typer_loc in + let (lctx,vx) = lexp_search ctx list_list typer_loc in + let (_,lexp,_) = vx in let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in

(* @@ -1083,15 +1089,17 @@ let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (posit 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 (lctx,vx) = lexp_search ctx list_list pos in + let (_,lexp,_) = vx in let (_,_, l_type,_) = browse_lexp lctx lexp 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 ^ output ^ res ^ sep ); + output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); close_out oc

let sep name s = @@ -1114,21 +1122,27 @@ let test () = 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) "##Type"; - hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "##Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; + hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,8) "(x : ##Int) -> Int"; hoverTest ctx name "l = (lambda x -> _+_ x 2) ;" (1,13) "##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"; sep name "FUNCTION(LAMBDA)"; - hoverTest ctx name "multiply x y z = _*_ x y ;" (1,1) "##TypeLevel"; + 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,19) "(Int -> (Int -> Int))"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,19) "##Int"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,23) "##Int"; - hoverTest ctx name "multiply x y z = x + y + z ;" (1,28) "##Int"; - hoverTest ctx name "multiply x y z = _*_ x y ;" (1,26) "##Int"; + 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) "(ℓ : ##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,7) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; @@ -1141,6 +1155,8 @@ let test () = 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) "##Type"; hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; @@ -1148,6 +1164,10 @@ let test () = hoverTest ctx name "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; 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) ""; @@ -1156,10 +1176,6 @@ let test () = 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) ""; @@ -1195,6 +1211,9 @@ let test () = 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======================================*) @@ -1206,7 +1225,7 @@ let test () = let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); - (*test ();*) + 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/-/commit/9d9ea020a8374265e9c72b83c66b6a59c4...