Juillet 2022 - Typer - mailman.iro.umontreal.ca

[Git][monnier/typer][wop-server] tests for the server
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 31 Jul '22

31 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer Commits: ad338dec by Soilih at 2022-07-31T13:49:01-04:00 tests for the server - - - - - 1 changed file: - src/lsp_server_test.ml Changes: ===================================== src/lsp_server_test.ml ===================================== @@ -1,4 +1,17 @@ (* +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +************************* TEST THE SERVER *************************** +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +*) + + +(** * * * HOVER @@ -7,8 +20,8 @@ **) let comp (a:string) (b:string) : string = - if (String.equal a b) then "/*******-----:-):-):-):-):-):-):-)__________SUCCESS_______:-):-):-):-):-):-):-)-----*******/\n\n\n" - else "/*******-----:-(:-(:-(:-(:-(:-(:-(____FAILED___:-(:-(:-(:-(:-(:-(:-(-----*******/\n\n\n" + 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 @@ -16,11 +29,16 @@ 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 (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, (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 lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in +let (_, _, l_type, _, _, _) = Typer_lsp_server.browse_lexp ctx lexp pos [] in let excpect = "excpected : " ^ expected ^ "\n" in let output = "output : " ^ (Lexp.lexp_string_for_lsp l_type) ^ "\n\n" in @@ -45,118 +63,125 @@ let test_hover_rapide () = hoverTest ctx name "lst = cons 1 nil" (1,8) "" 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) "" + 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 ##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" (* @@ -193,7 +218,7 @@ let afficher_lst code filename = ) x ) list_list -(* +(** * * * BREADCRUMBS @@ -218,4 +243,160 @@ let testerBread cursor str = 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 + 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, _) = 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 lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in + let ret = Typer_lsp_server.browse_lexp ctx lexp pos [] in + let loc = Typer_lsp_server.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, _) = 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 lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in + ( + match Typer_lsp_server.browse_lexp ctx lexp pos [] with + | (_, _, _, Expression l_ctx, _, _) + -> let my_str = Typer_lsp_server.split_string_line content (l + 1) in + let word = Typer_lsp_server.use_search_word my_str sep_list c "" in + let range = Typer_lsp_server.lsp_range_of_a_tuple + (pos.start_line,(pos.end_column - String.length word)) + (pos.end_line, pos.end_column) + in + let filtred_list = Typer_lsp_server.filter_lctx l_ctx [] in + let comp_list = Typer_lsp_server.ctx_to_ci_list filtred_list range in + let comp_list_ret = Typer_lsp_server.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 = Typer_lsp_server.split_string_line content (l + 1) in + let word = Typer_lsp_server.use_search_word my_str sep_list c "" in + let range = Typer_lsp_server.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, _) = Typer_lsp_server.compile_string content in + let (list_list, _) = Option.get ast in + let pos = Typer_lsp_server.pos_of_tuple position in + let lexp = Typer_lsp_server.trans_list_in_list_to_let list_list in + let (lxp, vn, idx) = try Option.get (Typer_lsp_server.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 = Typer_lsp_server.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 *************************** +********************************************************************* +********************************************************************* +********************************************************************* +********************************************************************* +*) \ No newline at end of file View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ad338dec5e71760c22feaf471e6a1f9d4… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/ad338dec5e71760c22feaf471e6a1f9d4… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][wop-server] adding a new type to specify the completion type
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 27 Jul '22

27 Jul '22

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

1 0

[Git][monnier/typer][wop-server] -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 25 Jul '22

25 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer Commits: 0d31fe12 by Soilih at 2022-07-25T12:13:18-04:00 - - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -843,7 +843,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 +889,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 +901,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 +937,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) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/0d31fe1265fe71556f1e6741f0f159f18… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/0d31fe1265fe71556f1e6741f0f159f18… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][SimonJ] 2 commits: Corrige arrays->list
by Simon Janssen (＠JanssenSimon) 20 Jul '22

20 Jul '22

Simon Janssen pushed to branch SimonJ at Stefan / Typer Commits: b5b56a92 by JanssenSimon at 2022-07-11T12:07:25-04:00 Corrige arrays->list - - - - - 0c224c20 by JanssenSimon at 2022-07-20T11:17:32-04:00 Fix les bogues avec execvp - - - - - 2 changed files: - btl/unix.typer - src/tunix.ml Changes: ===================================== btl/unix.typer ===================================== @@ -6,7 +6,7 @@ File_link = Built-in "File.link" : String -> String -> IO Unit; File_symlink = Built-in "File.symlink" : String -> String -> IO Unit; File_rename = Built-in "File.rename" : String -> String -> IO Unit; Proc_fork = Built-in "Proc.fork" : Unit -> Int; -Proc_execvp = Built-in "Proc.execvp" : Array String -> IO Unit; +Proc_execvp = Built-in "Proc.execvp" : List String -> IO Unit; File_stdin = Built-in "File.stdin" : Unit -> FileHandle; ===================================== src/tunix.ml ===================================== @@ -81,15 +81,15 @@ let rec extract_strings tlist = match tlist with | _ -> error dloc "Argument of extract_strings not a list" (* test this function ^ *) let proc_execvp loc _depth args_val = match args_val with - | [Vcons ((_, "args"), [program; args])] + | [Vcons ((_, _), [program; args])] -> (match program with | Vstring proc - -> Vcommand (fun () -> try Unix.execvp proc (Array.of_list (extract_strings args)); - with Unix.Unix_error(_, _, _) -> - error loc "Process exited with error code." - tunit) - | _ -> error loc "Problem with list of String arguments in Proc.execvp") - | _ -> error loc "Proc.execvp expects a String argument (program name) and a list of String arguments." + -> Vcommand (fun () -> try Unix.execvp proc (Array.of_list (extract_strings args)) with + | Unix.Unix_error(_, _, _) -> error loc "Process exited with error code." + | _ -> error loc "Something went terribly wrong when executing the process." + tunit) + | _ -> error loc "Proc.execvp expects a list of >String arguments<.") + | _ -> error loc "Proc.execvp expects a >list< of String arguments." let builtin_functions = [ ("File.unlink" , file_unlink,1); View it on GitLab: https://gitlab.com/monnier/typer/-/compare/e23a685d4b233d23b592d2cb97dddc22… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/e23a685d4b233d23b592d2cb97dddc22… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][wop-server] -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 18 Jul '22

18 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer Commits: e743b867 by Soilih at 2022-07-18T12:01:25-04:00 - - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -997,22 +997,50 @@ 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 lst = SMap.bindings cases in let rec foo cursor lst = match lst 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) + | (_, 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 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 ( try foo cursor lst - with _ -> foo cursor args + with _ -> foo2 cursor args 0 ) | Proj (_, e, (_, _)) -> browse_defs e cursor | Case (_, e, _, branches, _) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e743b86711314671dab2e959e57776c21… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/e743b86711314671dab2e959e57776c21… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] searching better the element's type the cursor is on
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Jul '22

13 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: debc7c1f by Soilih at 2022-07-13T23:43:43-04:00 searching better the element's type the cursor is on - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -281,6 +281,16 @@ 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) = @@ -291,31 +301,37 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | [hd;tl] -> let (_, _, lhd, _, loc_hd, _) = hd in let (_, _, ltl, _, loc_tl, _) = tl in let open Source.Location in - 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 - ) + + if (cursor_in_a_loc loc_hd cursor) + then hd + else ( + if (cursor_in_a_loc loc_tl cursor) + then tl else ( - if (dist loc_hd cursor < dist loc_tl cursor ) then hd - else tl + 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::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) @@ -377,8 +393,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De defs in let tab' = List.map - (fun (vn, _, ltp) -> - (ctx', None, ltp, None, Lexp.lexp_location ltp, (vn::lst_in)) + (fun ((l, _), _, ltp) -> + (ctx', None, ltp, None, l, lst_in) ) defs in @@ -789,7 +805,6 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = else foo (ml::tl) cursor in foo tab cursor - let vn_on_the_cursor (vn:vname) (cursor:location) : bool = let (l,_) = vn in if ((cursor.start_column >= l.start_column) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/debc7c1fc74f9b220c2b4446fe3814059… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/debc7c1fc74f9b220c2b4446fe3814059… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][wop-server] searching better the element's type the cursor is on
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 13 Jul '22

13 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer Commits: debc7c1f by Soilih at 2022-07-13T23:43:43-04:00 searching better the element's type the cursor is on - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -281,6 +281,16 @@ 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) = @@ -291,31 +301,37 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | [hd;tl] -> let (_, _, lhd, _, loc_hd, _) = hd in let (_, _, ltl, _, loc_tl, _) = tl in let open Source.Location in - 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 - ) + + if (cursor_in_a_loc loc_hd cursor) + then hd + else ( + if (cursor_in_a_loc loc_tl cursor) + then tl else ( - if (dist loc_hd cursor < dist loc_tl cursor ) then hd - else tl + 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::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) @@ -377,8 +393,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De defs in let tab' = List.map - (fun (vn, _, ltp) -> - (ctx', None, ltp, None, Lexp.lexp_location ltp, (vn::lst_in)) + (fun ((l, _), _, ltp) -> + (ctx', None, ltp, None, l, lst_in) ) defs in @@ -789,7 +805,6 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = else foo (ml::tl) cursor in foo tab cursor - let vn_on_the_cursor (vn:vname) (cursor:location) : bool = let (l,_) = vn in if ((cursor.start_column >= l.start_column) View it on GitLab: https://gitlab.com/monnier/typer/-/commit/debc7c1fc74f9b220c2b4446fe3814059… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/debc7c1fc74f9b220c2b4446fe3814059… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][wop-server] modify browse_lexp and browse_defs
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Jul '22

11 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch wop-server at Stefan / Typer Commits: fdaf0fca by Soilih at 2022-07-11T22:19:05-04:00 modify browse_lexp and browse_defs - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -370,20 +370,21 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> Debruijn.lctx_extend ctx v ForwardRef t) ctx defs in - let br_lst = List.fold_left - (fun lst (vn, _, _) -> - vn::lst - ) lst_in defs - in let tab = List.map - (fun (_, lxp, _) -> - browse_lexp ctx' lxp cursor br_lst + (fun (vn, lxp, _) -> + browse_lexp ctx' lxp cursor (vn::lst_in) + ) + defs + in + let tab' = List.map + (fun (vn, _, ltp) -> + (ctx', None, ltp, None, Lexp.lexp_location ltp, (vn::lst_in)) ) defs in (*let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in*) - browse_list_lexp ((browse_lexp ctx' e cursor br_lst)::tab) cursor + browse_list_lexp (List.append ((browse_lexp ctx' e cursor lst_in)::tab) tab') cursor | Arrow (ak, v, t1, l, t2) -> ( @@ -914,9 +915,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None | SortLevel SLz -> None | SortLevel (SLsucc e) -> browse_defs e cursor - | SortLevel (SLlub (e1, e2)) -> if not ((browse_defs e1 cursor) = None) then - browse_defs e1 cursor - else browse_defs e2 cursor + | SortLevel (SLlub (e1, e2)) -> let ret = browse_defs e1 cursor in + (match ret with + | Some _ -> ret + | None -> browse_defs e2 cursor) | Sort (_, Stype e) -> browse_defs e cursor | Sort (_, StypeLevel) -> None | Sort (_, StypeOmega) -> None @@ -937,46 +939,47 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = match ctx_list with | [] -> failwith "No variable found on the cursor!" | (_, _, ltp)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs ltp cursor - else foo'' tl cursor (comp + 1) + -> let ret = browse_defs ltp cursor in + (match ret with + | None -> foo'' tl cursor (comp + 1) + | Some _ -> ret) in let rec foo' (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = match ctx_list with - | [] -> foo'' ctx_list cursor comp + | [] -> foo'' defs cursor comp | (_, lxp, _)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs lxp cursor - else foo' tl cursor (comp + 1) + -> let ret = browse_defs lxp cursor in + (match ret with + | None -> foo' tl cursor (comp + 1) + | Some _ -> ret) in try foo defs cursor 0 with _ - -> if (not ((browse_defs el cursor) = None)) then - browse_defs el cursor - else foo' defs cursor 0 - ) + -> let ret = browse_defs el cursor in + (match ret with + | None -> foo' defs cursor 0 + | Some _ -> ret)) | Arrow (_, v, t1, _, t2) -> if (vn_on_the_cursor v cursor) then Some (t2, v, 0) - else (if not ((browse_defs t1 cursor) = None) then - browse_defs t1 cursor - else browse_defs t2 cursor - ) + else (let ret = browse_defs t1 cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t2 cursor) | Lambda (_, v, t, e) -> (*let ctx' = Debruijn.lctx_extend ctx v Variable t in*) if (vn_on_the_cursor v cursor) then Some (e, v, 0) - else (if not ((browse_defs e cursor) = None) then - browse_defs e cursor - else browse_defs t cursor - ) + else (let ret = browse_defs e cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t cursor) - | Call (f, args) -> if not ((browse_defs f cursor) = None) then - browse_defs f cursor - else ( - List.fold_right (fun (_, lxp) _ret -> - browse_defs lxp cursor) args None - ) + | Call (f, args) -> (let ret = browse_defs f cursor in + match ret with + | Some _ -> ret + | None -> (List.fold_right (fun (_, lxp) _ret -> + browse_defs lxp cursor) args None)) | Inductive (l, _label, args, cases) (*(Lexp.arg_kind * vname * Lexp.lexp) list SMap.t*) @@ -987,10 +990,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | (_, vn, lxp)::tl -> if (vn_on_the_cursor vn cursor) then Some (lxp, vn, List.length tl) else( - if (not ((browse_defs lxp cursor) = None)) - then (browse_defs lxp cursor) - else foo cursor tl - ) + let ret = browse_defs lxp cursor in + match ret with + | Some _ -> ret + | None -> foo cursor tl) in ( try foo cursor lst View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fdaf0fcaad9547264c98eb1d3d35c5a80… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fdaf0fcaad9547264c98eb1d3d35c5a80… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][minimal-server] 3 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 11 Jul '22

11 Jul '22

Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer Commits: edafb37e by Soilih at 2022-07-11T00:00:15-04:00 - - - - - - b9524636 by Soilih at 2022-07-11T00:02:33-04:00 - - - - - - fdaf0fca by Soilih at 2022-07-11T22:19:05-04:00 modify browse_lexp and browse_defs - - - - - 1 changed file: - src/typer_lsp_server.ml Changes: ===================================== src/typer_lsp_server.ml ===================================== @@ -370,20 +370,21 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> Debruijn.lctx_extend ctx v ForwardRef t) ctx defs in - let br_lst = List.fold_left - (fun lst (vn, _, _) -> - vn::lst - ) lst_in defs - in let tab = List.map - (fun (_, lxp, _) -> - browse_lexp ctx' lxp cursor br_lst + (fun (vn, lxp, _) -> + browse_lexp ctx' lxp cursor (vn::lst_in) + ) + defs + in + let tab' = List.map + (fun (vn, _, ltp) -> + (ctx', None, ltp, None, Lexp.lexp_location ltp, (vn::lst_in)) ) defs in (*let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in*) - browse_list_lexp ((browse_lexp ctx' e cursor br_lst)::tab) cursor + browse_list_lexp (List.append ((browse_lexp ctx' e cursor lst_in)::tab) tab') cursor | Arrow (ak, v, t1, l, t2) -> ( @@ -401,11 +402,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> (nctx, None, Lexp.mkSort (l, StypeOmega), None, location, lst_in) ) - | Lambda (_, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in + | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in let a = browse_lexp ctx' e cursor lst_in in 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),l) 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 browse_list_lexp ([a;b;d]) cursor @@ -914,9 +915,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None | SortLevel SLz -> None | SortLevel (SLsucc e) -> browse_defs e cursor - | SortLevel (SLlub (e1, e2)) -> if not ((browse_defs e1 cursor) = None) then - browse_defs e1 cursor - else browse_defs e2 cursor + | SortLevel (SLlub (e1, e2)) -> let ret = browse_defs e1 cursor in + (match ret with + | Some _ -> ret + | None -> browse_defs e2 cursor) | Sort (_, Stype e) -> browse_defs e cursor | Sort (_, StypeLevel) -> None | Sort (_, StypeOmega) -> None @@ -937,48 +939,66 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = match ctx_list with | [] -> failwith "No variable found on the cursor!" | (_, _, ltp)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs ltp cursor - else foo'' tl cursor (comp + 1) + -> let ret = browse_defs ltp cursor in + (match ret with + | None -> foo'' tl cursor (comp + 1) + | Some _ -> ret) in let rec foo' (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = match ctx_list with - | [] -> foo'' ctx_list cursor comp + | [] -> foo'' defs cursor comp | (_, lxp, _)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs lxp cursor - else foo' tl cursor (comp + 1) + -> let ret = browse_defs lxp cursor in + (match ret with + | None -> foo' tl cursor (comp + 1) + | Some _ -> ret) in try foo defs cursor 0 with _ - -> if (not ((browse_defs el cursor) = None)) then - browse_defs el cursor - else foo' defs cursor 0 - ) + -> let ret = browse_defs el cursor in + (match ret with + | None -> foo' defs cursor 0 + | Some _ -> ret)) | Arrow (_, v, t1, _, t2) -> if (vn_on_the_cursor v cursor) then Some (t2, v, 0) - else (if not ((browse_defs t1 cursor) = None) then - browse_defs t1 cursor - else browse_defs t2 cursor - ) + else (let ret = browse_defs t1 cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t2 cursor) | Lambda (_, v, t, e) -> (*let ctx' = Debruijn.lctx_extend ctx v Variable t in*) if (vn_on_the_cursor v cursor) then Some (e, v, 0) - else (if not ((browse_defs e cursor) = None) then - browse_defs e cursor - else browse_defs t cursor - ) + else (let ret = browse_defs e cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t cursor) - | Call (f, args) -> if not ((browse_defs f cursor) = None) then - browse_defs f cursor - else ( - List.fold_right (fun (_, lxp) _ret -> - browse_defs lxp cursor) args None - ) + | Call (f, args) -> (let ret = browse_defs f cursor in + match ret with + | Some _ -> ret + | None -> (List.fold_right (fun (_, lxp) _ret -> + browse_defs lxp cursor) args None)) - | Inductive _ -> 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 + | [] -> failwith "cursor is not on a vdef" + | (_, vn, lxp)::tl + -> if (vn_on_the_cursor vn cursor) then Some (lxp, vn, List.length tl) + else( + let ret = browse_defs lxp cursor in + match ret with + | Some _ -> ret + | None -> foo cursor tl) + in + ( + try foo cursor lst + with _ -> foo cursor args + ) | Proj (_, e, (_, _)) -> browse_defs e cursor | Case (_, e, _, branches, _) -> View it on GitLab: https://gitlab.com/monnier/typer/-/compare/045b1f20ed9ddc6200ce04c7cc0d84fb… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/045b1f20ed9ddc6200ce04c7cc0d84fb… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch SimonJ
by Simon Janssen (＠JanssenSimon) 11 Jul '22

11 Jul '22

Simon Janssen pushed new branch SimonJ at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/SimonJ You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Juillet 2022