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

27 Sep 2021


      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...
-- 
View it on GitLab: https://gitlab.com/monnier/typer/-/commit/9d9ea020a8374265e9c72b83c66b6a59c4...
You're receiving this email because of your account on gitlab.com.





    