[Typer] [Git][monnier/typer][soilih] 8 commits: --check option

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

Commits: 00aedd1e by Soilih BEN SOILIH at 2022-01-01T15:57:53-05:00 --check option

- - - - - 88f2d406 by Soilih BEN SOILIH at 2022-01-14T09:57:19-05:00 -

- - - - - 82287d46 by Soilih BEN SOILIH at 2022-01-14T23:15:24-05:00 -

- - - - - b507e826 by Soilih BEN SOILIH at 2022-01-14T23:17:06-05:00 -

- - - - - 5f0880d8 by Soilih at 2022-01-18T14:33:26-07:00 -

- - - - - 686c9db9 by Soilih at 2022-01-18T15:13:19-07:00 -

- - - - - 490e89eb by Soilih at 2022-01-19T15:58:21-07:00 -

- - - - - 61ce32fe by Soilih at 2022-01-19T16:20:53-07:00 handle internal errors with diagnostics

- - - - -

4 changed files:

- .vscode/launch.json - src/opslexp.ml - src/typer_lsp_server.ml - typer.ml

Changes:

===================================== .vscode/launch.json ===================================== @@ -4,6 +4,7 @@ // For more information, visit: https://go.microsoft.com/fwlink/?linkid=830387 "version": "0.2.0", "configurations": [ + { "type": "pwa-chrome", "request": "launch",

===================================== src/opslexp.ml ===================================== @@ -772,9 +772,9 @@ and check'' erased ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1139,9 +1139,9 @@ and get_type ctx e = | [] -> log_tc_error ~loc:l "Tuple has no field named: %s" label; etype | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> if not (ak = Aerasable) then mkSusp ftype s (* Yay! We found our field! *) - else (log_tc_error ~loc:l "Can't Proj an erasale field: %s" label; etype) + else (log_tc_error ~loc:l "Can't Proj an erasalbe field: %s" label; etype) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with

===================================== src/typer_lsp_server.ml ===================================== @@ -41,8 +41,10 @@ open Util

type list_in_list = (vname * Lexp.lexp * Lexp.ltype) list list

+type syntax_tree = (list_in_list * Debruijn.elab_context) + type state_after_processing = (log_entry list * - (list_in_list * Debruijn.elab_context) * ((int * int) option ref) + (syntax_tree option) * ((int * int) option ref) )

(* @@ -76,6 +78,7 @@ let log_level_to_severity (level:log_level) : Lsp.Types.DiagnosticSeverity.t = | Info -> Lsp.Types.DiagnosticSeverity.Information | _ -> Lsp.Types.DiagnosticSeverity.Hint

+ (* Typer location from a tuple *) let pos_of_tuple (p:int * int) : Source.Location.t = let (line,col) = p in @@ -99,6 +102,7 @@ let lsp_pos_of_pos_end (p:Source.Location.t) : Lsp.Types.Position.t = let lsp_range_of_loc (l:Source.Location.t) : Lsp.Types.Range.t = Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start l) ~end_:(lsp_pos_of_pos_end l)

+ let lsp_pos_of_pos_start_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t = Lsp.Types.Position.create ~line:(p.start_line - 1) ~character:(p.start_column)

@@ -113,6 +117,7 @@ let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = let (location, _) = vname in Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc location)

+ (* This function calculates the euclidean distance between two locations *) let dist (loc1:Source.Location.t) (loc2:Source.Location.t) = @@ -143,13 +148,41 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) else nearest_lexp_of_the_list (ml::tl) cursor

+let construct_log_exec str s : Log.log_entry list = + let lst = String.split_on_char '\n' str in + let open Source.Location in + let l = { + file = ""; + start_line = 0; + start_column = 0; + end_line = ((List.length lst) - 1); + end_column = ((String.length str) - 1) + } + in + let open Log in + let log_entry = { + level = Log.Error; + kind = (Some "ERROR"); + section = None; + print_action = None ; + loc = (Some l); + msg = s; + } + in + [log_entry] + + (*compile a string and return the logs and ast*) let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in - (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str str ectx in - (!Log.typer_log, ast, ref None) + + match Elab.lexp_decl_str str ectx with + + | (ast:syntax_tree) -> (!Log.typer_log, Some ast, ref None) + | exception Internal_error msg -> (construct_log_exec str msg, None, ref None) + | exception Stop_compilation msg -> (construct_log_exec str msg, None, ref None) + | exception User_error msg -> (construct_log_exec str msg, None, ref None)

let process_some_input_file (_file_contents : string) : state_after_processing = readstring _file_contents @@ -162,7 +195,6 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let (loc, lev, msg) = x in let ( file ,start_line,start_column,end_line,end_column) = loc in let severity = log_level_to_severity lev in - let message = msg ^ " in file: " ^ file in let start_pos = Lsp.Types.Position.create ~line:start_line ~character:start_column in let end_pos = Lsp.Types.Position.create ~line:end_line ~character:end_column in let range = Lsp.Types.Range.create ~start:start_pos ~end_:end_pos in @@ -170,10 +202,12 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list ~range:range ~severity:severity ~source:"typerlsp" - ~message:message + ~message:msg in diagnostic ) log_tab + +

(*==============completion============================*)

@@ -194,13 +228,13 @@ module Compl = struct detail:string; kind:k } - let lsp_pos_of_a_tuple (a,b) : Lsp.Types.Position.t = Lsp.Types.Position.create ~line:(a) ~character:(b)

let lsp_range_of_a_tuple (a,b) (x,y) : Lsp.Types.Range.t = Lsp.Types.Range.create ~start:(lsp_pos_of_a_tuple (a,b)) ~end_:(lsp_pos_of_a_tuple (x,y))

+ let t_from_tuple (tup : (int * string * string * string * k) list) : t list = List.map (fun x -> let (id,label,newText,detail,kind) = x in @@ -222,7 +256,6 @@ module Compl = struct (1, "add", "add()", "add a element to a list", Method); (1, "pop", "pop()", "remove a element from a list", Method); ] - let createKind (element:t) = match element.kind with | Text -> Lsp.Types.CompletionItemKind.Text @@ -342,6 +375,9 @@ module Compl = struct ) liste *) + + + end

(*==============completion============================*) @@ -360,7 +396,6 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D in foo (ctx: Debruijn.lexp_context) liste []

- (*====================================Lexp parcourir===================================*)

(* find the nearest lexp using Euclidean distance @@ -434,7 +469,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor) else foo (ml::tl) cursor in foo tab cursor - + (* Find the lexp the cursor on or the nearest one *) let lexp_search (ctx: Debruijn.lexp_context) (lst:list_in_list) (cursor:Source.Location.t) = try pos_in_lexp_interval ctx lst cursor @@ -640,11 +675,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D | [] -> () | (ak, (_, Some fn), ftype)::_ when fn = label (* We found our field! *) - -> if ak = Aerasable + -> if not (ak = Aerasable) then let a = Lexp.mkSusp ftype s in candidats := (browse_lexp ctx a cursor):: !candidats; - else failwith "Fail Here!!!" + else (Log.log_error ~loc:l "Can't Proj an erasalbe field: %s" label) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -789,6 +824,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D

(*====================================Lexp parcourir===================================*)

+ + (*==================================Parcourir les définitions==========================*) let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = let ((loc, oename), dbi) = v in @@ -810,6 +847,8 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = -> Log.log_fatal ~loc "DeBruijn index %d of `%s` out of bounds" dbi (Lexp.maybename oename)

+ + let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = let rec foo tab cursor = match tab with @@ -821,6 +860,7 @@ let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = 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) @@ -982,6 +1022,8 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Loc | Metavar (idx, s, _) -> None

+ + (*==================================Parcourir les définitions==========================*)

(* Search if the vname is in the context *) @@ -1008,7 +1050,7 @@ let use_search_name_in_ctx lctx lxp = | Some _-> let lx = Lexp.mkVar (vn,i) in Lexp.lexp_string lx

- + (* Search if the is the given value in the context *) let value_in_ctx (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : Debruijn.env_elem * int = let (_, _, lctxm, _) = ectx in @@ -1057,7 +1099,6 @@ let rec find_def_location lctx cursor (ret : Debruijn.lexp_context * (((Source.L

(*=====================================Symbols=====================================*)

-(* let filter_the_list_list (list_list: (vname * Lexp.lexp * Lexp.lexp) list) : (vname * Lexp.lexp * Lexp.lexp) list = List.filter ( fun x -> let ((_,s),_,_) = x in @@ -1088,7 +1129,7 @@ let create_symbols (list_list: list_in_list) : Lsp.Types.DocumentSymbol.t list = ~selectionRange:range () ) filtred_list - *) + let kind_bread (e: Lexp.lexp) : Lsp.Types.SymbolKind.t = let open Elexp in match Lexp.lexp_lexp' e with @@ -1118,6 +1159,20 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. () ) lst

+ +let create_breadcrumbs2 (vn: vname) : Lsp.Types.DocumentSymbol.t list = + match vn with + | (l,(Some s)) -> let range = lsp_range_of_loc_for_symbol l in + let r = Lsp.Types.DocumentSymbol.create + ~name:s + ~detail:s + ~kind:(Lsp.Types.SymbolKind.Variable) + ~range:range + ~selectionRange:range + () + in [r] + | _ -> failwith "No breadcrumbs beacause the is no variable." + (*=====================================End Symbols=================================*)

(*====================================Compl===================================*) @@ -1159,14 +1214,16 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. ) nlst *)

+ + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = let open Elexp in match Lexp.lexp_lexp' e with | Lambda (ak, (l,_), t, e) -> Lsp.Types.CompletionItemKind.Function | Cons (t, (_l, name)) -> Lsp.Types.CompletionItemKind.Constructor | _ -> Lsp.Types.CompletionItemKind.Variable - - + + let kind_of_a_varbind (element : Debruijn.env_elem ) : Lsp.Types.CompletionItemKind.t = let (_,vrb,_) = element in match vrb with @@ -1174,6 +1231,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. | ForwardRef -> Lsp.Types.CompletionItemKind.Variable | LetDef (_,lxp) -> kind_of_a_lexp lxp

+ + (* Filter the list by the vname with the string option *) let rec filter_lctx (lctx: Debruijn.env_elem Myers.myers) (ret: Debruijn.env_elem list) : Debruijn.env_elem list = match lctx with @@ -1183,7 +1242,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol.

| None -> filter_lctx tl ret | Some _ -> filter_lctx tl (hd::ret) - + + let construct_highlights (lst: Debruijn.env_elem list) : Lsp.Types.DocumentHighlight.t list = List.map ( fun (x: Debruijn.env_elem) -> let ((l,s),_,_) = x in @@ -1200,6 +1260,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. in Lsp.Types.Location.create ~uri:uri ~range:range ) lst + + (* Transform a context to a list of completion item *) let ctx_to_ci_list ctx (lctx : Debruijn.env_elem list) (range:Lsp.Types.Range.t) = List.map ( fun (x: Debruijn.env_elem) -> @@ -1218,7 +1280,9 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. ci

) lctx - + + + (* Verify if a string contains some other *) let string_contain (substr:string) (str:string) : bool = let r = ref 0 in @@ -1260,7 +1324,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. if ( ihd < iml ) then str_order (char_list_to_str (ml::tl)) str else false - + + (* Filter completions list by a string *) let complete_oth (str:string) (liste: Lsp.Types.CompletionItem.t list) = match liste with @@ -1272,13 +1337,18 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. List.filter (fun (x:Lsp.Types.CompletionItem.t) -> str_order str x.label ) lst + + + (* List of separators that delimit a word *) let sep_list = [';';',';'(';')';'.';' ';'{';'}']

+ let split_string_line (content:string) (line:int) = let str_list = String.split_on_char '\n' content in List.nth str_list (line - 1)

+ (* Find the word in which the cursor is *) let rec search_word_in_cursor (str:string) (char_list:char list) (pos:int) (ret:string) : string = if (String.equal str "") then "" @@ -1291,6 +1361,10 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. | 0 -> search_word_in_cursor str char_list pos ret | _ -> search_word_in_cursor str char_list (pos - 1) ret

+ let trans_list_in_list_to_let (lst: list_in_list) : Lexp.lexp = + let lst_in_lst = take_all_list_el lst in + Lexp.mkLet (Source.Location.dummy,lst_in_lst,Lexp.impossible) +

(*====================================Compl===================================*)

@@ -1353,13 +1427,14 @@ class lsp_server = method on_notif_doc_did_close ~notify_back:_ d : unit Linol_lwt.t = Hashtbl.remove buffers d.uri; Linol_lwt.return () - + (*method! config_hover = Some (`Bool true)*)

(*method! config_definition = Some (`Bool true)*)

(*method! config_symbol = Some (`Bool true)*) - + + method! config_modify_capabilities arg = let completionProvider = Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; """; "'"; "/"; "@"; "<"] @@ -1390,13 +1465,14 @@ class lsp_server = Lsp.Types.ServerCapabilities.documentHighlightProvider = Some documentHighlightProvider; Lsp.Types.ServerCapabilities.documentSymbolProvider = Some (`DocumentSymbolOptions documentSymbol)*) } +

method! on_req_definition ~notify_back ~id ~uri ~pos _st = match Hashtbl.find buffers uri with

| state_after_processing -> let (_,ast,cur) = state_after_processing in cur := Some (pos.line,pos.character); - let (list_list, _) = ast in + let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,vx) = lexp_search ctx list_list typer_loc in @@ -1410,12 +1486,11 @@ class lsp_server = let f = Linol_lwt.return (Some ret) in f

+ method! on_req_hover ~notify_back ~id ~uri ~pos doc_state = match Hashtbl.find buffers uri with - - | state_after_processing -> let (_,ast,cur) = state_after_processing in - cur := Some (pos.line,pos.character); - let (list_list, ectx) = ast in + | state_after_processing -> let (_,ast,_) = state_after_processing in + let (list_list, _) = Option.get ast in let typer_loc = typer_pos_of_lsp_pos pos in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (lctx,vx) = lexp_search ctx list_list typer_loc in @@ -1442,102 +1517,101 @@ class lsp_server = let e = Some r in let f = Linol_lwt.return e in f

+ + method! on_req_symbol ~notify_back ~id ~uri () =

- 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 - cur := Some (pos.line,pos.character); - let (list_list, _) = ast in - let typer_loc = typer_pos_of_lsp_pos pos in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_,lexp,_) = vx in - let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in - - (* - let trans_string = Compl.tranform_string doc_state.content in - let fbyline = Compl.list_filter_by_line trans_string (pos.line + 1) in - let word = Compl.find_the_nearest_compl fbyline ((pos.line + 1),pos.character) in - *) - - 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 - - let range = Compl.lsp_range_of_a_tuple - (typer_loc.start_line,(typer_loc.end_column - String.length word)) - (typer_loc.end_line, typer_loc.end_column) + let (list_list, _) = Option.get ast in + let (line, col) as cr = try Option.get !cur + with exe -> failwith "Cannot find the cursor position" in - - let filtred_list = filter_lctx l_ctx [] in - let comp_list = ctx_to_ci_list l_ctx filtred_list range in - let comp_list_ret = complete_oth word comp_list in - - let e = Some (`List comp_list_ret) in - let f = Linol_lwt.return e in f - (* - method! on_req_symbol ~notify_back ~id ~uri () = - - match Hashtbl.find buffers uri with - - | state_after_processing -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in - let typer_loc = pos_of_tuple (Int.max_int,Int.max_int) in + let pos = pos_of_tuple cr in(* + ignore(failwith "line: " ^ (string_of_int pos.start_line) + ^ "column: " ^ string_of_int pos.start_column);*) + (*let typer_loc = pos_of_tuple (Int.max_int,Int.max_int) in*) let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (lctx,vx) = lexp_search_deeper ctx list_list pos in let (_,lexp,_) = vx in + let (_,vn,_) = try Option.get (browse_defs lctx lexp pos) + with exe -> failwith ("no Variable in line " ^ (string_of_int line) + ^ " and column " ^ (string_of_int col) + ) + in + let r = create_breadcrumbs2 vn in + (* let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in let filtred_list = filter_lctx l_ctx [] in let r = create_breadcrumbs filtred_list in + *) let e = Some (`DocumentSymbol r) in let f = Linol_lwt.return e in f + +

- - method! on_request_unhandled ~notify_back ~id req = + method! on_request_unhandled ~notify_back ~id req =

- let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t = - fun req -> - - (match req with + let f :type r. r Lsp.Client_request.t -> r Linol_lwt.Jsonrpc2.IO.t = + fun req -> + + (match req with | TextDocumentHighlight params - -> ( - match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing - -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in - let typer_loc = pos_of_tuple - (params.position.line,params.position.character) in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_,lexp,_) = vx in - let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in - let filtred_list = filter_lctx l_ctx [] in - let hi = construct_highlights filtred_list in - let e = Some hi in - let f = Linol_lwt.return e in f) - | TextDocumentReferences params - -> ( - match Hashtbl.find buffers params.textDocument.uri with - | state_after_processing - -> let (_,ast) = state_after_processing in - let (list_list, _) = ast in - let typer_loc = pos_of_tuple - (params.position.line,params.position.character) in - let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in - let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in - let (_,lexp,_) = vx in - let (l_ctx,_,_,_) = browse_lexp lctx lexp typer_loc in - let filtred_list = filter_lctx l_ctx [] in - let hi = construct_references (params.textDocument.uri) filtred_list in - let e = Some hi in - let f = Linol_lwt.return e in f) + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (params.position.line,params.position.character); + let (list_list, _) = Option.get ast in + let typer_loc = typer_pos_of_lsp_pos params.position in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + (* + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + *) + let lexp = trans_list_in_list_to_let list_list in + let (_,vn,_) = try Option.get (browse_defs ctx lexp typer_loc) + with exe -> failwith "oupsssss....." + in + let (l,_) = vn in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + let dh = Lsp.Types.DocumentHighlight.create ~range:range () in + let r = [dh] in + let e = Some r in + let f = Linol_lwt.return e in f + ) + | TextDocumentReferences params + -> ( + match Hashtbl.find buffers params.textDocument.uri with + | state_after_processing -> let (_,ast,cur) = state_after_processing in + cur := Some (params.position.line,params.position.character); + let (list_list, _) = Option.get ast in + let typer_loc = typer_pos_of_lsp_pos params.position in + let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in + (* + let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in + let (_,lexp,_) = vx in + *) + let lexp = trans_list_in_list_to_let list_list in + let (_,vn,_) = try Option.get (browse_defs ctx lexp typer_loc) + with exe -> failwith "oupsssss.....2222" + in + let (l,_) = vn in + let range = Compl.lsp_range_of_a_tuple + (l.start_line,l.start_column) (l.end_line,l.end_column) + in + let dh = Lsp.Types.Location.create ~uri:(params.textDocument.uri) ~range:range in + let r = [dh] in + let e = Some r in + let f = Linol_lwt.return e in f + ) | _ -> super#on_request_unhandled ~notify_back ~id req - ) - in f req - *) + ) + in f req + end

- (*=======================================Test======================================*)

let comp (a:string) (b:string) : string = @@ -1546,7 +1620,7 @@ let comp (a:string) (b:string) : string =

let hoverTest (ctx:Debruijn.lexp_context) (name:string) (content:string) (position: int * int) (expected:string) = let (_, ast,_) = readstring content in - let (list_list, _) = ast in + let (list_list, _) = Option.get ast in let (l,c) = position in let pos = pos_of_tuple position in

@@ -1695,6 +1769,7 @@ let time f a b = fx

+ (*=======================================Test======================================*)

@@ -1703,7 +1778,6 @@ let time f a b = and runs it as a task. *) let run () = ignore (Arg.Set Log.lsp_enabled); - Logs.set_level ~all:true (Some Logs.Debug); (*test ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in

===================================== typer.ml ===================================== @@ -45,6 +45,8 @@ let arg_defs =

("--lsp", Arg.Set lsp_server, "Enable Typer LSP server");

+ ("--check", Arg.Set Elab.elab_check, "Enable Checking"); + ("-v", Arg.Unit Log.increment_log_level, "Increment verbosity");

("-Vfull-lctx",

View it on GitLab: https://gitlab.com/monnier/typer/-/compare/dd13976d45936915f1cd9fb9446af0b22...