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

Commits: 21e78719 by Soilih at 2022-09-14T22:01:03-04:00 fix-tests

- - - - -

5 changed files:

- emacs/typer-mode.el - src/elab.ml - src/typer_lsp_server.ml - typer.ml - typer_server.ml

Changes:

===================================== emacs/typer-mode.el ===================================== @@ -279,7 +279,7 @@ (easy-menu-add typer-mode-menu) )

- (defvar typer-lsp-server-command '("typer" "--lsp")) + (defvar typer-lsp-server-command '("typer")) (with-eval-after-load 'lsp-mode (lsp-register-client (make-lsp-client :new-connection

===================================== src/elab.ml ===================================== @@ -72,9 +72,9 @@ let dloc = dummy_location let parsing_internals = ref false

let str_ref = ref "" -let btl_folder = +let btl_folder = try Sys.getenv "TYPER_BUILTINS" - with Not_found -> let strl = String.split_on_char '/' Sys.executable_name in + with Not_found -> let strl = String.split_on_char '/' Sys.executable_name in for i = 1 to (List.length strl) -2 do str_ref := !str_ref ^ "/" ^ (List.nth strl i) done;

===================================== src/typer_lsp_server.ml ===================================== @@ -431,7 +431,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> (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 + | Lambda (_, ((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 @@ -1010,7 +1010,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | None -> (List.fold_right (fun (_, lxp) _ret -> browse_defs lxp cursor) args None))

- | Inductive (l, _label, args, cases) + | Inductive (_, _label, args, cases) -> let lst = SMap.bindings cases in

let rec foo2 cursor args comp = @@ -1034,7 +1034,7 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = match lst with | [] -> failwith "cursor is not on a vdef" | (_, ls)::tl - -> (let rec foo' cursor ls comp = + -> (let foo' cursor ls comp = match ls with | [] -> foo cursor tl | _ -> foo2 cursor ls comp @@ -1306,7 +1306,7 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f

- method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = + method! on_req_completion ~notify_back:_ ~id:_ ~uri ~pos ~ctx:_ doc_state = match Hashtbl.find buffers uri with

| state_after_processing -> let (_,ast,cur) = state_after_processing in @@ -1344,7 +1344,7 @@ class lsp_server = | (lctx, _, _, FieldName lxp, _,_) -> (let ret = Opslexp.lexp_whnf lxp lctx in match Lexp.lexp_lexp' ret with - | Inductive (_, (_,label), fargs, constructors) + | Inductive (_, (_, _), _, constructors) when SMap.cardinal constructors = 1 -> 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 @@ -1481,7 +1481,7 @@ let comp (a:string) (b:string) : string = 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 hoverTest (ctx:Debruijn.lexp_context) (output_file_path:string) (content:string) (position: int * int) (expected:string) = let (_, ast, _) = compile_string content in let (list_list, _) = Option.get ast in let (l,c) = position in @@ -1506,135 +1506,135 @@ let input = "input : " ^ content ^ "\n" in let res = "result : " ^ (comp expected s) 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 +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc (sep ^ input ^ pos ^ excpect ^ output ^ res ^ sep ); close_out oc

-let sep name s = +let sep output_file_path s = let content = "\n\n\n/*-----------------------------" ^ s ^ "-----------------------------------*/\n\n\n" in -let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in +let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc content; close_out oc

-let test_hover () = + +let test_hover output_file_path () = 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,24) "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"; - 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;" + sep output_file_path "INT"; + hoverTest ctx output_file_path "e = 12 ;" (1,1) "Int"; + hoverTest ctx output_file_path "e = 12 ;" (1,5) "Int"; + sep output_file_path "STRING"; + hoverTest ctx output_file_path "s = "hejej" ;" (1,1) "String"; + hoverTest ctx output_file_path "s = "hejej" ;" (1,8) "String"; + sep output_file_path "FLOAT"; + hoverTest ctx output_file_path "f = 12.3 ;" (1,1) "Float"; + hoverTest ctx output_file_path "f = 12.3 ;" (1,6) "Float"; + sep output_file_path "LAMBDA"; + hoverTest ctx output_file_path "l = (lambda x -> _+_ x 2) ;" (1,1) "(x : ##Int) -> Int"; + hoverTest ctx output_file_path "l = (lambda x -> _+_ x 2) ;" (1,8) "Int"; + hoverTest ctx output_file_path "l = (lambda x -> _+_ x 2) ;" (1,13) "Int"; + hoverTest ctx output_file_path "l = (lambda x y -> _+_ x y) ;" (1,24) "Int"; + hoverTest ctx output_file_path "l = (lambda x -> _+_ x 2) ;" (1,19) "(Int -> (Int -> Int))"; + hoverTest ctx output_file_path "l = (lambda x -> _+_ x 2) ;" (1,21) "Int"; + hoverTest ctx output_file_path "l = (lambda x y -> x + y) ;" (1,20) "Int"; + hoverTest ctx output_file_path "l = (lambda x y -> x + y) ;" (1,24) "Int"; + hoverTest ctx output_file_path "l = (lambda x y -> _+_ x y) ;" (1,24) "Int"; + hoverTest ctx output_file_path "l = (lambda x y -> _+_ x y) ;" (1,26) "Int"; + sep output_file_path "FUNCTION(LAMBDA)"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,1) "(ℓ : ##TypeLevel) ≡> (τ : (##Type_ ℓ)) ≡> (x : ##Int) -> (y : ##Int) -> (z : τ) -> Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,10) "Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,12) "Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,14) "τ"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,18) "(Int -> (Int -> Int))"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,21) "Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ;" (1,23) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,1) "(x : ##Int) -> (y : ##Int) -> (z : ##Int) -> Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,10) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,12) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,14) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,18) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,20) "(Int -> (Int -> Int))"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,22) "Int"; + hoverTest ctx output_file_path "multiply x y z = x + y + z ;" (1,26) "Int"; + sep output_file_path "CALL"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,1) "Int"; + hoverTest ctx output_file_path "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 output_file_path "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,13) "Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,15) "Int"; + hoverTest ctx output_file_path "multiply x y z = _*_ x y ; \n\n\ne = multiply 2 3 "h" ;" (4,19) "String"; + sep output_file_path "BUILTIN"; + hoverTest ctx output_file_path "foo = ##Int ;" (1,1) "Type"; + hoverTest ctx output_file_path "foo = ##Int ;" (1,9) "Type"; + sep output_file_path "SUSP"; + hoverTest ctx output_file_path "foo = ##Int ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; + hoverTest ctx output_file_path "foo = ##Int ; \n\n\nv = foo ;" (4,6) "(##Type_ ##TypeLevel.z)"; + hoverTest ctx output_file_path "foo = ##String ; \n\n\nv = foo ;" (4,1) "(##Type_ (##TypeLevel.succ ##TypeLevel.z))"; + hoverTest ctx output_file_path "foo = ##Type ; \n\n\nv = foo ;" (4,1) "(##Type_ ##TypeLevel.z)"; + sep output_file_path "LIST"; + hoverTest ctx output_file_path "lst = cons 2 ( (cons 1 ) nil ) ;" (1,1) "(List ##Int)"; + hoverTest ctx output_file_path "lst = cons 2 ( (cons 1 ) nil ) ;" (1,8) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (a -> ((List ℓ a) -> (List ℓ a)))"; + hoverTest ctx output_file_path "lst = cons 2 ( (cons 1 ) nil ) ;" (1,12) "Int"; + hoverTest ctx output_file_path "lst = cons 2 ( (cons 1 ) nil ) ;" (1,27) "(ℓ : TypeLevel) ≡> (a : (##Type_ ℓ)) ≡> (List ℓ a)"; + sep output_file_path "TUPLE"; + hoverTest ctx output_file_path "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 output_file_path "tup = (1,2,"str",false) ;" (1,8) "Int"; + hoverTest ctx output_file_path "tup = (1,2,"str",false) ;" (1,10) "Int"; + hoverTest ctx output_file_path "tup = (1,2,"str",false) ;" (1,15) "String"; + hoverTest ctx output_file_path "tup = (1,2,"str",false) ;" (1,21) "Bool"; + sep output_file_path "ARROW"; + hoverTest ctx output_file_path "type Floo = bar Int Int ;" (1,1) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,17) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,29) ""; + hoverTest ctx output_file_path "v = Int -> Int ;" (1,1) ""; + sep output_file_path "INDUCTIVE"; + hoverTest ctx output_file_path "type Floo = bar Int Int ;" (1,7) ""; + hoverTest ctx output_file_path "type Floo = bar Int Int ;" (1,18) ""; + hoverTest ctx output_file_path "type Floo = bar Int Int ;" (1,22) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,1) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,19) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (1,26) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,1) ""; + hoverTest ctx output_file_path "floo = typecons (floo) (bar Int Int) ;\n\n\nbar = datacons floo bar ;" (4,10) ""; + hoverTest ctx output_file_path "Bool = typecons (Bool) (true) (false);" (1,1) ""; + hoverTest ctx output_file_path "Bool = typecons (Bool) (true) (false);" (1,10) ""; + hoverTest ctx output_file_path "Bool = typecons (Bool) (true) (false);" (1,18) ""; + hoverTest ctx output_file_path "Bool = typecons (Bool) (true) (false);" (1,24) ""; + hoverTest ctx output_file_path "Bool = typecons (Bool) (true) (false);" (1,32) ""; + sep output_file_path "METAVAR"; + hoverTest ctx output_file_path "x : ?t = 3 ;" (1,1) "τ"; + hoverTest ctx output_file_path "x : ?t = 3 ;" (1,6) "τ"; + hoverTest ctx output_file_path "f x = _+_ ?y x ;" (1,1) "(y : Int) => (x : ##Int) -> Int"; + hoverTest ctx output_file_path "f x = _+_ ?y x ;" (1,3) "Int"; + hoverTest ctx output_file_path "f x = _+_ ?y x ;" (1,12) "Int"; + hoverTest ctx output_file_path "f x = _+_ ?y x ;" (1,14) "Int"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,1) "Int"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,6) "Int"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (1,10) "Int"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,1) "Int"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,11) "τ"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,15) "τ"; + hoverTest ctx output_file_path "x : ?t ; x = 3 ;\n\n\nfoo = let x : ?t = 3 in x;" (4,25) "Int"; + sep output_file_path "LET"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,1) "Int"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,11) "Int"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,19) "Int"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,31) "Int"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,36) "Int"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,38) "(Int -> (Int -> Int))"; + hoverTest ctx output_file_path "bar = let x = 1 ; y = 2 ; z = 6 in x + y + z ;" (1,44) "Int"; + sep output_file_path "CASE"; + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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;" + hoverTest ctx output_file_path "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"

@@ -1646,14 +1646,14 @@ let test_hover () = * **)

-let afficher_lst code filename = - let ch = open_in code in +let afficher_lst code_path output_file_path = + let ch = open_in code_path in let content = really_input_string ch (in_channel_length ch) in close_in ch; let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in List.iteri (fun i x -> - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc ("\n\n---------------liste: " ^ (string_of_int i) ^ " --------------\n\n"); close_out oc; List.iteri (fun _j (y : Util.vname * Lexp.lexp * Lexp.ltype)-> @@ -1666,7 +1666,7 @@ let afficher_lst code filename = (string_of_int l.end_line) ^ "\ncolumn: " ^ (string_of_int l.start_column) ^ " - " ^ (string_of_int l.end_column) ^ "\n\n" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 filename in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc output; close_out oc; ) x @@ -1679,8 +1679,11 @@ let afficher_lst code filename = * * **) -let testerBread cursor str = - let (_,ast,_) = compile_string str in +let testerBread cursor code_path output_file_path = + let ch = open_in code_path in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in let typer_loc = pos_of_tuple cursor in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in @@ -1691,13 +1694,9 @@ let testerBread cursor str = let (_,st) = x in (Option.get st) ^ " > " ^ str ) "" lst in - let name = "/home/soilih/Bureau/test/symbol.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc ("bread: " ^ str ^ "\n")

-let bread_test = - testerBread (2,2) "multiply _x = \nlet lst = cons 2 nil in\nlst" - (** * * @@ -1706,8 +1705,11 @@ let bread_test = * **)

-let defTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) = - let (_, ast, _) = compile_string content in +let defTest (ctx:Debruijn.lexp_context) (output_file_path:string) (code_path:string) (position: int * int) = + let ch = open_in code_path in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in let (l, c) = position in let pos = pos_of_tuple position in @@ -1721,16 +1723,14 @@ let defTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (positio 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 + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc (sep ^ input ^ pos ^ output ^ sep ); close_out oc

-let test_definition () = +let test_definition (output_file_path:string) (code_path:string) (pos: int * int) = 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) + defTest ctx output_file_path code_path pos

(* List of separators that delimit a word *) let sep_list = [';';',';'(';')';' ';'{';'}';'.'] @@ -1743,8 +1743,11 @@ let sep_list = [';';',';'(';')';' ';'{';'}';'.'] * **)

-let completionTest (ctx:Debruijn.lexp_context) (content:string) (position: int * int) = - let (_, ast, _) = compile_string content in +let completionTest (ctx:Debruijn.lexp_context) (code_path:string) (position: int * int) = + let ch = open_in code_path in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in let (l, c) = position in let pos = pos_of_tuple position in @@ -1769,7 +1772,7 @@ let completionTest (ctx:Debruijn.lexp_context) (content:string) (position: int | (lctx, _, _, FieldName lxp, _,_) -> (let ret = Opslexp.lexp_whnf lxp lctx in match Lexp.lexp_lexp' ret with - | Inductive (_, (_,label), fargs, constructors) + | Inductive (_, (_, _), _, constructors) when Util.SMap.cardinal constructors = 1 -> let my_str = split_string_line content (l + 1) in let word = use_search_word my_str sep_list c "" in @@ -1799,21 +1802,22 @@ let completionTest (ctx:Debruijn.lexp_context) (content:string) (position: int ) )

-let test_completion () = +let test_completion output_file_path code_path (pos : int * int) = 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 ret = completionTest ctx code_path pos 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 + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path in output_string oc wr; close_out oc

-let highlightTest(ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) = - let (_, ast, _) = compile_string content in +let highlightTest (output_file_path:string) (code_path:string) (position: int * int) = + let ch = open_in code_path in + let content = really_input_string ch (in_channel_length ch) in + close_in ch; + let (_,ast,_) = compile_string content in let (list_list, _) = Option.get ast in let pos = pos_of_tuple position in let lexp = trans_list_in_list_to_let list_list in @@ -1832,14 +1836,12 @@ let highlightTest(ctx:Debruijn.lexp_context) (name:string) (content:string) (po ^ "-" ^ ((string_of_int l.end_column)) ^ ")" ) ret "" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in + let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 output_file_path 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) +let test_highlight output_file_path code_path (pos: int * int) = + highlightTest output_file_path code_path pos

(* @@ -1862,7 +1864,6 @@ let test_highlight () = and runs it as a task. *) let run () = ignore (Log.lsp_enabled := true); - test_hover (); let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in

===================================== typer.ml ===================================== @@ -27,12 +27,6 @@ open Printf

let arg_batch = ref true

-(* -boolean used to start the LSP server. -made true for testing -*) -let lsp_server = ref true -

let add_input_file, list_input_files = let files = ref [] in @@ -43,9 +37,6 @@ let arg_defs = Arg.String Log.set_typer_log_level_str, "Set the logging level");

- ("--lsp", Arg.Unit (fun _ -> let _ = lsp_server := true - in ()), "Enable Typer LSP server"); - ("--check", Arg.Set Elab.elab_check, "Enable Checking");

("-v", Arg.Unit Log.increment_log_level, "Increment verbosity");

===================================== typer_server.ml ===================================== @@ -21,4 +21,5 @@ * with this program. If not, see http://www.gnu.org/licenses/. * *)

-let () = Typerserver.Typer_lsp_server.run () +let () = + Typerserver.Typer_lsp_server.run ()

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/21e78719e52ee95aa47cffa82377bd2790...