Soilihi BEN SOILIHI BOINA pushed to branch typer-lsp-server at Stefan / Typer
Commits: 715e3ba7 by Soilih at 2022-08-26T13:24:02-04:00 -
- - - - - c8d3df40 by Simon Génier at 2022-08-26T14:23:13-04:00 Fix Typerserver build with Dune.
- - - - - 21e78719 by Soilih at 2022-09-14T22:01:03-04:00 fix-tests
- - - - -
7 changed files:
- dune - emacs/typer-mode.el - src/dune - src/elab.ml - src/typer_lsp_server.ml - typer.ml - + typer_server.ml
Changes:
===================================== dune ===================================== @@ -13,3 +13,10 @@ (modules debug_util) (libraries typerlib) (modes byte native)) + +(executable + (name typer_server) + (promote (until-clean)) + (modules typer_server) + (libraries typerlib typerserver) + (modes byte native)) \ No newline at end of file
===================================== 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/dune ===================================== @@ -1,7 +1,12 @@ ;; -*- lisp-data -*-
(library + (modules :standard \ typer_lsp_server) (name typerlib) - (libraries zarith str linol linol-lwt - lsp jsonrpc)) + (libraries zarith str))
+(library + (modules typer_lsp_server) + (flags (:standard -warn-error -A)) + (name typerserver) + (libraries typerlib linol linol-lwt lsp jsonrpc))
===================================== 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 ===================================== @@ -36,17 +36,20 @@ Diagnostics includes all the warnings, errors and messages that the processing of a document are expected to be able to return. *) -open Log + +open Typerlib + +open Log open Util
type syntax_tree = (vname * Lexp.lexp * Lexp.ltype) list list
type syntax_tree_elab_ctx = (syntax_tree * Debruijn.elab_context)
-type document_state = (log_entry list * (syntax_tree_elab_ctx option) +type document_state = (log_entry list * (syntax_tree_elab_ctx option) * ((int * int) option ref))
-type completion_type = +type completion_type = | Expression of Debruijn.lexp_context | FieldName of Lexp.lexp
@@ -428,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 @@ -511,8 +514,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De | _ -> (e,[]) in candidats := (browse_lexp ctx e cursor lst_in):: !candidats; let etype = Opslexp.get_type ctx e in - (* FIXME save the type in the case lexp instead of recomputing - it over and over again *) let ekind = Opslexp.get_type ctx etype in let elvl = match Opslexp.lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l @@ -528,8 +529,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De match fargs, aargs with | [], [] -> s | _farg::fargs, (_ak, aarg)::aargs - (* We don't check aarg's type, because we assume that `check` - * returns a valid type. *) -> mksubst (Subst.cons aarg s) fargs aargs | _,_ -> s in let s = mksubst Subst.identity fargs aargs in @@ -547,7 +546,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De (erased, nctx) in
let brch = SMap.bindings branches in - let lst = + let _ = List.map ( fun (name, (l, vdefs, branch)) @@ -558,8 +557,12 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De (* FIXME: If ak is Aerasable, make sure the var only * appears in type annotations. *) | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes - -> mkctx (Opslexp.dbset_push ak erased) - (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) + -> let (loc, _) = vdef in + let ctx' = Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s) in + let _ = candidats := (ctx', None, ftype, Expression ctx', loc, lst_in):: !candidats + in + mkctx (Opslexp.dbset_push ak erased) + ctx' (Lexp.ssink vdef s) (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) vdefs fieldtypes @@ -576,20 +579,21 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De brch in
- let diff = SMap.cardinal constructors - List.length lst in ( match default with | Some (v, d) - -> if diff <= 0 then (); + -> + let (loc, _) = v in let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in let subst = Subst.shift 1 in let hlxp = Lexp.mkVar ((l, None), 0) in let (_, nctx) = ctx_extend_with_eq nctx subst hlxp in - candidats := (browse_lexp nctx d cursor lst_in) :: !candidats; + let ret = (nctx, None, etype, Expression nctx, loc, lst_in) in + candidats := ret :: (browse_lexp nctx d cursor lst_in) :: !candidats; () | None - -> if diff > 0 then (); () + -> () ) | _,_ -> () ; ); @@ -1006,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 = @@ -1030,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 @@ -1302,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 @@ -1340,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 @@ -1477,11 +1481,11 @@ 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 (_, ast, _) = compile_string content in -let (list_list, _) = Option.get ast in -let (l,c) = position in -let pos = pos_of_tuple position in +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 + let pos = pos_of_tuple position in
(* let (lctx, vx) = lexp_search ctx list_list pos in @@ -1502,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"
@@ -1642,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)-> @@ -1662,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 @@ -1675,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 @@ -1687,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" - (** * * @@ -1702,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 @@ -1717,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 = [';';',';'(';')';' ';'{';'}';'.'] @@ -1739,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 @@ -1765,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 @@ -1795,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 @@ -1828,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
(* @@ -1858,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"); @@ -68,8 +59,6 @@ let compile_main argv = let repl_main argv = let usage = Sys.executable_name ^ " repl [options] [<file>] …" in Arg.parse_argv argv arg_defs add_input_file usage; - if !lsp_server then Typer_lsp_server.run () - else (); print_string (Fmt.make_title " TYPER REPL "); print_endline " Typer 0.0.0 - Interpreter - (c) 2016-2021"; print_newline ();
===================================== typer_server.ml ===================================== @@ -0,0 +1,25 @@ +(* +* Copyright (C) 2020, 2021 Free Software Foundation, Inc. +* +* Author: Soilihi BEN SOILIHI BOINA ben.soilihi.boina.soilihi@umontreal.ca +* Keywords: languages, lisp, dependent types. +* Description: this file define the entry of the server +* +* This file is part of Typer. +* +* Typer is free software; you can redistribute it and/or modify it under the +* terms of the GNU General Public License as published by the Free Software +* Foundation, either version 3 of the License, or (at your option) any +* later version. +* +* Typer is distributed in the hope that it will be useful, but WITHOUT ANY +* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS +* FOR A PARTICULAR PURPOSE. See the GNU General Public License for +* more details. +* +* You should have received a copy of the GNU General Public License along +* with this program. If not, see http://www.gnu.org/licenses/. +* *) + +let () = + Typerserver.Typer_lsp_server.run ()
View it on GitLab: https://gitlab.com/monnier/typer/-/compare/ff9700154c1f0ccfe285d383cb13d8c22...