Typer Janvier 2022

typer@iro.umontreal.ca

1 participants
5 discussions

[Git][monnier/typer] Pushed new branch diagnostics_and_highlight_and_references
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 25 Jan '22

25 Jan '22

Soilihi BEN SOILIHI BOINA pushed new branch diagnostics_and_highlight_and_references at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/diagnostics_and_highlight_and_refer… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer] Pushed new branch diagnostics
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 25 Jan '22

25 Jan '22

Soilihi BEN SOILIHI BOINA pushed new branch diagnostics at Stefan / Typer -- View it on GitLab: https://gitlab.com/monnier/typer/-/tree/diagnostics You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][add-proj] 2 commits: -
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 19 Jan '22

19 Jan '22

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 29526c1c by Soilih at 2022-01-17T16:15:35-07:00 - - - - - - ec5e23bf by Soilih at 2022-01-19T23:30:01-07:00 fix unused var issues - - - - - 5 changed files: - src/elab.ml - src/elexp.ml - src/eval.ml - src/lexp.ml - src/opslexp.ml Changes: ===================================== src/elab.ml ===================================== @@ -1727,7 +1727,7 @@ let sform_letin ctx loc sargs ot = match sargs with | _ -> sexp_error loc "Unrecognized let_in_ expression"; sform_dummy_ret ctx loc -let sform_proj ctx loc sargs ot = +let sform_proj ctx loc sargs _ = match sargs with | [lxp;(Symbol (loca,str))] -> let (ret,_) = infer lxp ctx in ===================================== src/elexp.ml ===================================== @@ -140,7 +140,7 @@ and elexp_string lxp = | Imm(s) -> sexp_string s | Builtin((_, s)) -> s | Var((_, s), i) -> L.maybename s ^ "[" ^ string_of_int i ^ "]" - | Proj (l,lxp,i) + | Proj (_,lxp,i) -> "( _._ " ^ elexp_string lxp ^ " " ^ (string_of_int i) ^ " )" | Cons (_, (_, s)) -> "datacons(" ^ s ^")" ===================================== src/eval.ml ===================================== @@ -467,7 +467,7 @@ let rec eval lxp (ctx : Env.runtime_env) (trace : eval_debug_info): (value_type) -> let vt = eval' e ctx in ( match vt with - | Vcons (symbol, vtl) -> List.nth vtl i + | Vcons (_, vtl) -> List.nth vtl i | _ -> error loc "Connot find a value in position %d \n" i ===================================== src/lexp.ml ===================================== @@ -985,7 +985,7 @@ and lexp_str ctx (exp : lexp) : string = | Var ((_loc, name), idx) -> maybename name ^ (index idx) ; - | Proj (l,lxp,(loc,str)) + | Proj (_,lxp,(_,str)) -> "( _._ " ^ lexp_str' lxp ^ " " ^ str ^ " )" | Metavar (idx, subst, (_loc, name)) ===================================== src/opslexp.ml ===================================== @@ -748,7 +748,7 @@ and check'' erased ctx e = let tct = arg_loop ctx erased args in tct | Proj (l, e, (loc, label)) - ->( let call_split e = + -> ( let call_split e = match lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in @@ -774,10 +774,10 @@ and check'' erased ctx e = -> 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) - | (ak, vdef, ftype)::fieldtypes + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -965,7 +965,7 @@ and fv (e : lexp) : (DB.set * mv_set) = | Sort (_, (StypeOmega | StypeLevel)) -> fv_empty | Builtin _ -> fv_empty | Var (_, i) -> (DB.set_singleton i, mv_set_empty) - | Proj (l,lxp,lbl) -> fv lxp + | Proj (_,lxp,_) -> fv lxp | Susp (e, s) -> fv (push_susp e s) | Let (_, defs, e) -> let len = List.length defs in @@ -1082,10 +1082,10 @@ and get_type ctx e = -> 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) - | (ak, vdef, ftype)::fieldtypes + | (_, vdef, _)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with - |(l, Some n) -> mkProj (loc, e, lbl) + |(_, Some _) -> mkProj (loc, e, lbl) |_ -> Lexp.impossible in let fieldref = fvdef vdef e l (loc, label) in getfieldtype (S.cons fieldref s) fieldtypes in @@ -1226,7 +1226,7 @@ let pos_of_label lctx label t : int = | _ -> (e,[]) in let it, aargs = call_split t in match lexp'_whnf it lctx, aargs with - | Inductive (_, _, fargs, constructors), aargs + | Inductive (_, _, _, constructors), _ when SMap.cardinal constructors = 1 -> let bindings = SMap.bindings constructors in let find_the_pos label (lst : (string * (arg_kind * vname * ltype) list) list) c = @@ -1236,7 +1236,7 @@ let pos_of_label lctx label t : int = match l with | [] -> failwith "label not found!" | hd::tl -> match hd with - | (ak, (loc, Some vn), ltp ) + | (_, (_, Some vn), _ ) -> let (_,st) = label in if (String.equal vn st) then c else foo label tl (c + 1) View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6a7a6f997f9cbaf7a28134706de2bbd4… -- View it on GitLab: https://gitlab.com/monnier/typer/-/compare/6a7a6f997f9cbaf7a28134706de2bbd4… You're receiving this email because of your account on gitlab.com.

1 0

[Git][monnier/typer][soilih] 8 commits: --check option
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 19 Jan '22

19 Jan '22

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

1 0

[Git][monnier/typer][add-proj] fixing add-proj
by Soilihi BEN SOILIHI BOINA (＠BenSoilih) 17 Jan '22

17 Jan '22

Soilihi BEN SOILIHI BOINA pushed to branch add-proj at Stefan / Typer Commits: 6a7a6f99 by Soilih at 2022-01-17T00:51:24-07:00 fixing add-proj - - - - - 1 changed file: - src/opslexp.ml Changes: ===================================== src/opslexp.ml ===================================== @@ -771,8 +771,8 @@ 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 - then mkSusp ftype s (* Yay! We found our field! *) + -> 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) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = @@ -1079,7 +1079,7 @@ 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) | (ak, vdef, ftype)::fieldtypes View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6a7a6f997f9cbaf7a28134706de2bbd48… -- View it on GitLab: https://gitlab.com/monnier/typer/-/commit/6a7a6f997f9cbaf7a28134706de2bbd48… You're receiving this email because of your account on gitlab.com.

1 0

2024

2023

2022

2021

2020

2019

2018

2017

2016

Typer Janvier 2022