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

Commits: c5a6a62d by Soilih BEN SOILIH at 2021-12-18T01:30:56-05:00 -

- - - - - f498d2f1 by Soilih BEN SOILIH at 2021-12-18T13:20:12-05:00 -

- - - - - 39573a65 by Soilih BEN SOILIH at 2021-12-20T21:21:00-05:00 fixing...

- - - - -

4 changed files:

- src/elab.ml - src/lexp.ml - src/opslexp.ml - src/typer_lsp_server.ml

Changes:

===================================== src/elab.ml ===================================== @@ -71,17 +71,17 @@ let dloc = dummy_location

let parsing_internals = ref false let btl_folder = - + (* let cwd = Sys.getcwd () in let cdir = String.sub cwd 0 (String.length cwd) in let canal_entree = open_in (cdir ^ "/.configuration.txt") in let ligne1 = input_line canal_entree in let l = String.split_on_char ':' ligne1 in let m = String.split_on_char '"' (List.nth l 1) in - let filename = List.nth m 1 in + let filename = List.nth m 1 in*)

try Sys.getenv "TYPER_BUILTINS" - with Not_found -> filename ^ "/btl" + with Not_found -> "/home/soilih/Projet Maitrise/typer" (*filename*) ^ "/btl"

let fatal ?print_action ?loc fmt = Log.log_fatal ~section:"ELAB" ?print_action ?loc fmt

===================================== src/lexp.ml ===================================== @@ -530,7 +530,6 @@ let rec lexp_location e = | Cons (_,(l,_)) -> l | Case (l,_,_,_,_) -> l | Susp (e, _) -> lexp_location e - (* | Susp (_, e) -> lexp_location e *) | Metavar (_,_,(l,_)) -> l

===================================== src/opslexp.ml ===================================== @@ -766,15 +766,15 @@ and check'' erased ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> 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 + -> mkSusp ftype s (*if 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 erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with @@ -1133,15 +1133,15 @@ and get_type ctx e = | _,_ -> (log_tc_error ~loc:l "Wrong arg number to inductive type!"; s) in let s = mksubst S.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (arg_kind * vname * ltype) list) = match fieldtypes with | [] -> 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 + -> mkSusp ftype s(*if 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 erasale field: %s" label; etype)*) | (ak, vdef, ftype)::fieldtypes -> let fvdef vdef e loc lbl = match vdef with

===================================== src/typer_lsp_server.ml ===================================== @@ -94,24 +94,6 @@ let lsp_pos_of_pos_end_for_symbol (p:Source.Location.t) : Lsp.Types.Position.t = let lsp_range_of_loc_for_symbol (l:Source.Location.t) : Lsp.Types.Range.t = Lsp.Types.Range.create ~start:(lsp_pos_of_pos_start_for_symbol l) ~end_:(lsp_pos_of_pos_end_for_symbol l)

-let rec search_a_vname_with_a_given_position (vname_list: Util.vname list) (location : Source.Location.t): Util.vname = - match vname_list with - | [] -> let loc = Source.Location.dummy in - let s = Some "null" in - (loc,s) - | hd::tl -> - let (loc, _) = hd in - (* - let file = "position.txt" in - let oc = open_out file in (* create or truncate file, return channel *) - Printf.fprintf oc "loc.start_line = %d \n loc.start_column = %d \n location.start_line = %d \n location.start_column = %d \n " loc.start_line loc.start_column location.start_line location.start_column; (* write something *) - close_out oc; (* flush and close the channel *) - *) - if ((loc.start_line - 1) == location.start_line) - && ((loc.start_column - 1) == location.start_column) - then hd - else search_a_vname_with_a_given_position tl location -

let vname_to_lsp_loc ~(vname: Util.vname) ~uri : Lsp.Types.Location.t = let (location, _) = vname in @@ -146,19 +128,6 @@ let rec nearest_lexp_of_the_list (liste : (vname * Lexp.lexp * Lexp.ltype) list) then (nearest_lexp_of_the_list (hd::tl) cursor) else nearest_lexp_of_the_list (ml::tl) cursor

- - -let rec search_lexp_with_a_location (list_list: list_in_list) (location : Source.Location.t): Lexp.lexp option = - let tab = List.map (fun x -> let (a,b,c) = List.nth x 0 in (a,b,c)) list_list in - let lexp_list = List.map (fun x -> let (_,b,_) = x in b ) tab in - let rec foo (tab:Lexp.lexp list) (loc:Source.Location.t) = - match tab with - | [] -> None - | hd::tl -> let r = Lexp.lexp_location hd in - if ((r.start_line - 1) == loc.start_line) && ((r.start_column - 1) == loc.start_column) then Some hd - else foo tl loc - in - foo lexp_list location

(*compile a string and return the logs and ast*) let readstring (str:string) = @@ -267,6 +236,7 @@ module Compl = struct | Event -> Lsp.Types.CompletionItemKind.Event | Operator -> Lsp.Types.CompletionItemKind.Operator | TypeParameter -> Lsp.Types.CompletionItemKind.TypeParameter + (* let tranform_string (content:string) : (string * int * int) list = Base.String.split content ~on:'\n' |> @@ -277,7 +247,7 @@ module Compl = struct pos+1, (word,line+1,pos-1)) |> Base.snd) |> List.concat - *) +

let list_filter_by_line (liste: (string * int * int) list) (line:int) : (string * int * int) list = List.filter (fun (word,w_line,w_column) -> w_line == line) liste @@ -291,7 +261,7 @@ module Compl = struct liste in word - + let dist_compl (loc1:string * int * int) (loc2:int * int) = let (_,loc1_sl,loc1_sc) = loc1 in let (loc2_sl,loc2_sc) = loc2 in @@ -301,7 +271,8 @@ module Compl = struct +. (((float_of_int (loc1_sc)) -. (float_of_int (loc2_sc))) ** 2.0 ) ) ) - + + let rec find_the_nearest_compl (liste:(string * int * int) list) (pos:int * int) : string =

match liste with @@ -312,7 +283,8 @@ module Compl = struct |hd::ml::tl -> if ((dist_compl hd pos) < (dist_compl ml pos)) then (find_the_nearest_compl (hd::tl) pos) else find_the_nearest_compl (ml::tl) pos

- + *) + (* let match_str (str:string) : Str.regexp = str |> Str.quote @@ -355,6 +327,7 @@ module Compl = struct Str.string_match reg x.label 0 ) liste + *) end

(*==============completion============================*) @@ -639,7 +612,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D let it, aargs = call_split etype in match Opslexp.lexp'_whnf it ctx, aargs with | Inductive (_, _, fargs, constructors), aargs - when SMap.cardinal constructors != 1 + when SMap.cardinal constructors = 1 -> let rec mksubst s fargs aargs = match fargs, aargs with | [], [] -> s @@ -647,7 +620,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D -> mksubst (Subst.cons aarg s) fargs aargs | _,_ -> s in let s = mksubst Subst.identity fargs aargs in - let fieldtypes = SMap.find label constructors in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = match fieldtypes with | [] -> () @@ -800,20 +773,336 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : list_in_list ) : (D browse_lexp ctx e cursor | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location))

- let lexp_parcourir ctx e = - let lctx = Debruijn.ectx_to_lctx ctx in - let location = Lexp.lexp_location e in - (Opslexp.get_type lctx e , location) - (*====================================Lexp parcourir===================================*)

-(* Verify if there is a varbind *) -let verify_varbind (env: Debruijn.env_elem) : (int * Lexp.lexp) option = - let (_,vrbd,_) = env in - match vrbd with - | Variable - | ForwardRef-> None - | LetDef (idx,lxp) -> Some (idx,lxp) +(*==================================Parcourir les définitions==========================*) +let def_loc_search (ctx : Debruijn.lexp_context) (v: vref) = + let ((loc, oename), dbi) = v in + try + let ((l,_),_,_) as ret = Myers.nth dbi ctx in + let _ = match (ret, oename) with + | (((_, Some name), _, _), Some ename) + -> if not (ename = name) then + Log.log_fatal + ~loc + ({|DeBruijn index %d refers to wrong name. |} + ^^ {|Expected: "%s" got "%s"|}) + dbi ename name + | _ -> () in + + l + with + | Not_found + -> 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 + | [] -> failwith "Liste vide!" + | [n] -> n + | [hd;tl] -> if (dist hd cursor < dist tl cursor ) then hd + else tl + |hd::ml::tl -> if (dist hd cursor < dist ml cursor ) then (foo (hd::tl) cursor) + else foo (ml::tl) cursor +in foo tab cursor + +(* +let rec browse_defs (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) = + + match Lexp.lexp_lexp' e with + + | Imm (Float (_, _)) + | Imm (Integer (_, _)) + | Imm (String (_, _)) -> None + | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None + | SortLevel SLz -> None + | SortLevel (SLsucc e) -> None + | SortLevel (SLlub (e1, e2)) -> None + | Sort (l, Stype e) -> None + | Sort (_, StypeLevel) -> None + | Sort (_, StypeOmega) -> None + | Builtin (_, t) -> None + | Var (vn, idx) + -> Some (e,vn,idx) + | Susp (e, s) -> None + | Let (l, defs, e) + -> let ctx' = + List.fold_left (fun ctx (v, _e, t) + -> (Debruijn.lctx_extend ctx v ForwardRef t)) + ctx defs in + let rec foo ctx defs cursor ret_list = + match defs with + | [] -> ret_list + | hd::tl -> let (vn,lxp,ltp) = hd in + foo ctx tl cursor ((browse_defs ctx lxp cursor)::ret_list) + in + let tab = List.map + (fun (vn,lxp,ltp) -> + browse_defs ctx' lxp cursor + ) + defs + in + + (browse_defs ctx' e cursor)::tab + + | Arrow (ak, v, t1, l, t2) + -> ( + + let (_,_,k1,_) = browse_lexp ctx t1 cursor in + let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in + let (_,_,k2,_) = browse_lexp nctx t2 cursor in + match Opslexp.sort_compose ctx nctx l ak k1 k2 with + | SortResult k -> (nctx, None, k, location) + | SortInvalid + -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) + | SortK1NotType + -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) + | SortK2NotType + -> (nctx, None, Lexp.mkSort (l, StypeOmega), location) + ) + + | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in + let a = browse_lexp ctx' e cursor in + let b = browse_lexp ctx t cursor in + (*let etp = Opslexp.get_type ctx' e in + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) + let d = (ctx,None, t,l) in + browse_list_lexp ([a;b;d]) cursor + + | Call (f, args) + -> ( + let fonc = browse_lexp ctx f cursor in + let args_list = List.map + (fun (_ , e) -> browse_lexp ctx e cursor) + args + in + + browse_list_lexp (fonc::args_list) cursor + ) + + | Inductive (l, _label, args, cases) + -> + ( + let rec arg_loop ctx args = + + match args with + + | [] + -> let (level, tab) = + SMap.fold + (fun _ case (level,tab) -> + let ((level, _, _), tab) = + List.fold_left + ( + fun ((level, ictx, n), tab) (ak, v, t) -> + ( + ((let lwhnf = Opslexp.lexp_whnf (Opslexp.get_type ictx t) ictx in + match Lexp.lexp_lexp' lwhnf with + | Sort (_, Stype _) + when ak == Pexp.Aerasable + -> level + | Sort (_, Stype level') + -> Opslexp.mkSLlub ctx level + (Lexp.mkSusp level' (Lexp.sunshift n)) + | _tt -> level), + Debruijn.lctx_extend ictx v Variable t, + n + 1), + ((browse_lexp ictx t cursor)::tab) + ) + ) + ((level, ctx, 0), [] ) + case in + (level, tab) + ) + cases + (Lexp.mkSortLevel SLz, []) in + browse_list_lexp ((ctx, None,level,l)::tab) cursor + + | (ak, v, t)::args + -> let ctx' = Debruijn.lctx_extend ctx v Variable t in + browse_list_lexp + ( + (browse_lexp ctx' t cursor)::(arg_loop ctx' args)::[] + ) cursor + in + arg_loop ctx args + ) + + | Proj (l, e, (loc, label)) + -> let candidats = ref [] in + ( + let call_split (e: Lexp.lexp) = + match Lexp.lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + candidats := (browse_lexp ctx e cursor):: !candidats; + let etype = Opslexp.get_type ctx e in + let it, aargs = call_split etype in + match Opslexp.lexp'_whnf it ctx, aargs with + | Inductive (_, _, fargs, constructors), aargs + when SMap.cardinal constructors = 1 + -> let rec mksubst s fargs aargs = + match fargs, aargs with + | [], [] -> s + | _farg::fargs, (_ak, aarg)::aargs + -> mksubst (Subst.cons aarg s) fargs aargs + | _,_ -> s in + let s = mksubst Subst.identity fargs aargs in + let (_,fieldtypes) = List.hd (SMap.bindings constructors) in + let rec getfieldtype s (fieldtypes : (Pexp.arg_kind * vname * Lexp.ltype) list) = + match fieldtypes with + | [] -> () + | (ak, (_, Some fn), ftype)::_ when fn = label + (* We found our field! *) + -> if ak = Aerasable + then + let a = Lexp.mkSusp ftype s in + candidats := (browse_lexp ctx a cursor):: !candidats; + else () + | (ak, vdef, ftype)::fieldtypes + -> let fvdef vdef e loc lbl = + match vdef with + |(l, Some n) -> Lexp.mkProj (loc, e, lbl) + |_ -> Lexp.impossible in + let fieldref = fvdef vdef e l (loc, label) in + getfieldtype (Subst.cons fieldref s) fieldtypes in + getfieldtype s fieldtypes; () + | Inductive _, _ + -> () + | _,_ -> ()); + browse_list_lexp !candidats cursor + + | Case (l, e, ret, branches, default) + -> + let candidats = ref [] in + + let call_split (e: Lexp.lexp) = + match Lexp.lexp_lexp' e with + | Call (f, args) -> (f, args) + | _ -> (e,[]) in + candidats := (browse_lexp ctx e cursor):: !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 + | _ -> Debruijn.level0 in + let erased = Debruijn.set_empty in + + let it, aargs = call_split etype in + ( + match Opslexp.lexp'_whnf it ctx, aargs with + + | Inductive (_, _, fargs, constructors), aargs -> + let rec mksubst s fargs aargs = + 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 + let ctx_extend_with_eq ctx subst hlxp = + let tlxp = Lexp.mkSusp e subst in + let tltp = Lexp.mkSusp etype subst in + let tlvl = Lexp.mkSusp elvl subst in + let eqty = Lexp.mkCall (Debruijn.type_eq, + [(Lexp.Aerasable, tlvl); (* Typelevel *) + (Lexp.Aerasable, tltp); (* Inductive type *) + (Lexp.Anormal, hlxp); (* Lexp of the branch head *) + (Lexp.Anormal, tlxp)]) in (* Target lexp *) + (* The eq proof is erasable. *) + let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in + (erased, nctx) in + + let brch = SMap.bindings branches in + let lst = + List.map + ( + fun (name, (l, vdefs, branch)) + -> let fieldtypes = SMap.find name constructors in + let rec mkctx erased ctx s hlxp vdefs fieldtypes = + match vdefs, fieldtypes with + | [], [] -> (erased, ctx, hlxp) + (* 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)) + (Lexp.ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) + vdefs fieldtypes + | _,_ -> (erased, ctx, hlxp) in + let hctor = + Lexp.mkCall (Lexp.mkCons (it, (l, name)), + List.map (fun (_, a) -> (Pexp.Aerasable, a)) aargs) in + let (nerased, nctx, hlxp) = + mkctx erased ctx s hctor vdefs fieldtypes in + let subst = Subst.shift (List.length vdefs) in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + candidats := (browse_lexp nctx branch cursor) :: !candidats; + ) + brch + in + + let diff = SMap.cardinal constructors - List.length lst in + ( + match default with + | Some (v, d) + -> if diff <= 0 then (); + 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) :: !candidats; + () + | None + -> if diff > 0 then (); () + ) + | _,_ -> () ; + ); + browse_list_lexp !candidats cursor + | Cons (t, (_l, name)) + -> (match Opslexp.lexp'_whnf t ctx with + | Inductive (l, _, fargs, constructors) + -> (try + let fieldtypes = Util.SMap.find name constructors in + let rec indtype fargs start_index = + match fargs with + | [] -> [] + | (ak, vd, _)::fargs -> (ak, Lexp.mkVar (vd, start_index)) + :: indtype fargs (start_index - 1) in + let rec fieldargs ftypes = + match ftypes with + | [] -> let nargs = List.length fieldtypes + List.length fargs in + Lexp.mkCall (Lexp.mkSusp t (Subst.shift nargs), + indtype fargs (nargs - 1)) + | (ak, vd, ftype) :: ftypes + -> Lexp.mkArrow (ak, vd, ftype, Lexp.lexp_location ftype, + fieldargs ftypes) in + let rec buildtype fargs = + match fargs with + | [] -> fieldargs fieldtypes + | (_ak, ((l,_) as vd), atype) :: fargs + -> Lexp.mkArrow (Pexp.Aerasable, vd, atype, l, + buildtype fargs) in + (ctx, None, buildtype fargs, location) + with Not_found + -> (ctx, None, Debruijn.type_int, location) + ) + | _ -> (ctx, None, Debruijn.type_int, location)) + + | Metavar (idx, s, _) + -> (match Lexp.metavar_lookup idx with + | MVal e -> let e = Lexp.push_susp e s in + browse_lexp ctx e cursor + | MVar (_, t, _) -> (ctx, None, Lexp.push_susp t s, location)) +*) +(*==================================Parcourir les définitions==========================*)

(* Search if the vname is in the context *) let search_name_in_ctx (lctx: Debruijn.lexp_context) (lxp: Lexp.lexp) = @@ -873,13 +1162,13 @@ let search_the_key (ectx: Debruijn.elab_context) (lxp: Lexp.lexp) : string =

(*====================================Definition===================================*)

-let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t = +let rec find_def_location lctx cursor (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Source.Location.t =

- let (ctx,vr,_,loc) = ret in + let (_,vr,_,_) = ret in

match vr with - | None -> loc - | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup ctx v in + | None -> cursor + | Some v -> let ((l,_),_,_) = Debruijn.lctx_lookup lctx v in

{l with start_line = (l.start_line - 1); end_line = (l.end_line - 1)}

@@ -888,6 +1177,7 @@ let rec find_def_location (ctx:Debruijn.lexp_context) (ret : Debruijn.lexp_conte

(*=====================================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 @@ -918,7 +1208,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 @@ -951,7 +1241,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. (*=====================================End Symbols=================================*)

(*====================================Compl===================================*) - + (* let lsp_compl_from_var (ret : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t) : Lsp.Types.CompletionItem.t list =

let (_,vr,_,loc) = ret in @@ -973,7 +1263,7 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. ~textEdit:textEdit ~detail:detail () in [ci] - + let trans_listlist_by_var (ctx:Debruijn.lexp_context) (list_list:list_in_list) (cursor:Source.Location.t) = let lst = update_the_context ctx list_list in let nlst = List.map ( fun x -> @@ -987,7 +1277,8 @@ let create_breadcrumbs (lst: Debruijn.env_elem list) : Lsp.Types.DocumentSymbol. | None -> false | Some v -> true ) nlst - + *) + let kind_of_a_lexp (e: Lexp.lexp) : Lsp.Types.CompletionItemKind.t = let open Elexp in match Lexp.lexp_lexp' e with @@ -1229,7 +1520,7 @@ class lsp_server = let (lctx,vx) = lexp_search ctx list_list typer_loc in let (_,lexp,_) = vx in let (l_ctx, idx,_ ,_ ) as ret = browse_lexp lctx lexp typer_loc in - let loc = find_def_location l_ctx ret in + let loc = find_def_location lctx typer_loc ret in let l = Lsp.Types.Location.create ~uri:uri ~range:(lsp_range_of_loc loc) in @@ -1293,7 +1584,7 @@ class lsp_server =

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 @@ -1309,6 +1600,7 @@ class lsp_server = 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 =

@@ -1351,7 +1643,7 @@ class lsp_server = | _ -> super#on_request_unhandled ~notify_back ~id req ) in f req - + *) end

@@ -1504,23 +1796,7 @@ let test () = hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,4) ""; hoverTest ctx name "foo x = case x\n\n| true => "true"\n\n| false => "false" ;" (5,14) ""

-let testSymbols (content:string) = - let (_, (list_list,_)) = readstring content in - (*let res = create_symbols list_list in*) - let res = take_all_list_el list_list in - let name = "/home/soilih/Bureau/test/symbol.txt" in - let oc = open_out_gen [Open_creat; Open_text; Open_append] 0o640 name in - (* - List.iteri (fun i (x : Lsp.Types.DocumentSymbol.t) -> - let st = "\n" ^ (string_of_int i) ^ " : " ^ (x.name) ^ "\n" in - output_string oc st - ) res; - *) - output_string oc (string_of_int (List.length res)); - close_out oc - - let testS () = - testSymbols "multiply x y z = _*_ x y ;" +

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

@@ -1532,7 +1808,6 @@ let run () = ignore (Arg.Set Log.lsp_enabled); Logs.set_level ~all:true (Some Logs.Debug); (*test ();*) - (*testS ();*) let s = new lsp_server in let server = Linol_lwt.Jsonrpc2.create_stdio s in let task = Linol_lwt.Jsonrpc2.run server in

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