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

Commits: 17cc8120 by Soilih at 2022-03-11T19:55:55-05:00 update highlight and references

- - - - - 928ea462 by Soilih at 2022-03-11T19:56:17-05:00 Merge branch 'soilih-test-avec-ast' into soilih

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -890,8 +890,7 @@ let tup_browse_defs_in_ctx (lctx: Debruijn.lexp_context) lxp (vn : vname) (curso else foo tl str rlst in foo lctx_l str []

- -let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname) ret = +let rec find_references (lxp: Lexp.lexp) (vr: vname) idx_vr ret = match Lexp.lexp_lexp' lxp with | Imm (Float (_, _)) | Imm (Integer (_, _)) @@ -904,28 +903,20 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname) | Sort (_, StypeLevel) -> ret | Sort (_, StypeOmega) -> ret | Builtin (_, t) -> ret - | Var ((vn, idx) as v) - -> let (vn_ret,_,_) = Debruijn.lctx_lookup ctx v in - let (_,vrn) = vr in - let stri = try Option.get vrn - with exe -> failwith "Our Var doesn't have a string" - in - let (_, vn_ret') = vn_ret in - let str = try Option.get vn_ret' - with exe -> failwith "Our Reference doesn't have a string" - in - if (String.equal str stri) then vn::ret - else ret + | Var (vn, idx) + -> if (Int.equal idx idx_vr) then + vn::ret + else ret | Arrow (ak, v, t1, l, t2) - -> find_references ctx t2 vr ret + -> find_references t2 vr idx_vr ret | Lambda (ak, v, t, e) - -> find_references ctx e vr (find_references ctx t vr ret) + -> find_references e vr idx_vr (find_references t vr idx_vr ret) | Call (f, args) -> ret - | Let (l, defs, el) -> find_references ctx el vr ret + | Let (l, defs, el) -> find_references el vr idx_vr ret | Inductive (l, _label, args, cases) -> ( - let rec arg_loop ctx args = + let rec arg_loop args = match args with (*| Inductive of U.location * label * ((arg_kind * vname * ltype) list) (* formal Args *) @@ -934,17 +925,16 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname) -> let lst = SMap.fold (fun _ case (lst: vname list) -> - let (_, ret_list) = + let ret_list = List.fold_left ( - fun (ictx, tab) (ak, v, t) -> + fun tab (ak, v, t) -> ( - let nctx = Debruijn.lctx_extend ictx v Variable t in - (Debruijn.lctx_extend ictx v Variable t, - (List.append tab (find_references nctx t vr ret))) + + (List.append tab (find_references t vr idx_vr ret)) ) ) - (ctx, [] ) + [] case in ret_list @@ -953,20 +943,19 @@ let rec find_references (ctx:Debruijn.lexp_context) (lxp: Lexp.lexp) (vr: vname) lst

| (ak, v, t)::args - -> let ctx' = Debruijn.lctx_extend ctx v Variable t in - find_references ctx' t vr (find_references ctx' t vr ret) - in - arg_loop ctx args + -> find_references t vr idx_vr (find_references t vr idx_vr ret) + in + arg_loop args ) (* | Case of U.location * lexp - * ltype (* The type of the return value of all branches *) - * (U.location * (arg_kind * vname) list * lexp) SMap.t - * (vname * lexp) option (* Default. *) + * ltype (* The type of the return value of all branches *) + * (U.location * (arg_kind * vname) list * lexp) SMap.t + * (vname * lexp) option (* Default. *) *) | _ -> ret - -let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.Location.t) : (Debruijn.lexp_context * Lexp.lexp * vname) option = + +let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.Location.t) : (Lexp.lexp * vname * int) option =

match Lexp.lexp_lexp' lxp with

@@ -988,25 +977,24 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L List.fold_left (fun ctx (v, _e, t) -> (Debruijn.lctx_extend ctx v ForwardRef t)) ctx defs in - let rec foo ctx' (ctx_list: Debruijn.env_elem list) cursor = + let rec foo (ctx_list: Debruijn.env_elem list) cursor comp = match ctx_list with | [] -> failwith "No Variable in the cursor" | ((l, (Some vn) as v),_,_)::tl - -> if (vn_on_the_cursor v cursor) then Some (ctx', el, v) - else foo ctx' tl cursor - | _::tl -> foo ctx' tl cursor + -> if (vn_on_the_cursor v cursor) then Some (el, v, comp) + else foo tl cursor (comp + 1) + | _::tl -> foo tl cursor (comp + 1) in let ctx_list = Myers.list ctx' in - foo ctx' ctx_list cursor + foo ctx_list cursor 0

| Arrow (ak, v, t1, l, t2) - -> let nctx = Debruijn.lexp_ctx_cons ctx v Variable t1 in - if (vn_on_the_cursor v cursor) then - Some (nctx, t2, v) + -> if (vn_on_the_cursor v cursor) then + Some (t2, v, 0) else None

- | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in - if (vn_on_the_cursor v cursor) then Some (ctx', e, v) + | Lambda (ak, ((l,_) as v), t, e) -> (*let ctx' = Debruijn.lctx_extend ctx v Variable t in*) + if (vn_on_the_cursor v cursor) then Some (e, v, 0) else None

| Call (f, args) -> None @@ -1018,88 +1006,41 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L 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 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 -> - 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 _ = - 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 - -> candidats := ((Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)), vdef)::!candidats; - 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 - ignore(ctx_extend_with_eq nctx subst hlxp) - ) - brch - in - () - - | _,_ -> () ; + let vn_lst = SMap.fold + (fun name (l, vdefs, branch) (lst: (vname * Lexp.lexp * int) list) + -> let fieldtypes = SMap.find name constructors in + let collect vdefs fieldtypes comp = + match vdefs, fieldtypes with + | [], [] -> lst + | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes + -> (vdef, branch, comp)::(_vdef', branch, comp)::lst + | _,_ -> lst in + collect vdefs fieldtypes 0 + ) + branches [] + in + candidats := vn_lst + + | _,_ -> failwith "Case on a non-inductive type!" ; ); - let rec cands (lst: (Debruijn.lexp_context * vname) list) = + let rec cands (lst: (vname * Lexp.lexp * int) list) = match lst with | [] -> failwith "No Valid Candidate" - | hd::tl -> let (ctx,(l,s)) = hd in + | hd::tl -> let ((l,s), lxp, comp) = hd in if (l.start_column <= cursor.start_column && l.end_column >= cursor.end_column ) then hd else cands tl in - let (lctx,vn) = cands !candidats in - Some (lctx, e, vn) + let (vn, lxp, comp) = cands !candidats in + Some (lxp, vn, comp)

| Cons (t, (_l, name)) -> None @@ -1107,6 +1048,7 @@ let rec browse_defs (ctx:Debruijn.lexp_context) (lxp:Lexp.lexp) (cursor:Source.L -> None

+ let construct_highlights (lst: vname list) : Lsp.Types.DocumentHighlight.t list = List.map ( fun (x: vname) -> let (l,_) = x in @@ -1720,15 +1662,8 @@ class lsp_server = 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 (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos params.position in - let typer_loc' = { - typer_loc - with - start_line = typer_loc.start_line + 1; - end_line = typer_loc.end_line + 1 - } - in let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in (* let (lctx,vx) = lexp_search_deeper ctx list_list typer_loc in @@ -1736,10 +1671,10 @@ class lsp_server = (Debruijn.lexp_context * Lexp.lexp * vname) *) let lexp = trans_list_in_list_to_let list_list in - let (l_ctx,lxp,vn) = try Option.get (browse_defs ctx lexp typer_loc') - with exe -> failwith "No highlight found !!!" + let (lxp, vn, idx) = try Option.get (browse_defs ctx lexp typer_loc) + with exe -> failwith "No highlight found !!!" in - let ret = find_references l_ctx lxp vn [vn] in + let ret = find_references lxp vn idx [vn] in let r = construct_highlights ret in let e = Some r in let f = Linol_lwt.return e in f @@ -1749,15 +1684,8 @@ class lsp_server = 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 (list_list, _) = ast in let typer_loc = typer_pos_of_lsp_pos params.position in - let typer_loc' = { - typer_loc - with - start_line = typer_loc.start_line + 1; - end_line = typer_loc.end_line + 1 - } - in (*failwith ("(" ^ (string_of_int typer_loc.start_line) ^ "," ^ (string_of_int typer_loc.start_column) ^ ")");*) let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in (* @@ -1765,10 +1693,10 @@ class lsp_server = let (_,lexp,_) = vx in *) let lexp = trans_list_in_list_to_let list_list in - let (l_ctx,lxp,vn) = try Option.get (browse_defs ctx lexp typer_loc') - with exe -> failwith "No reference found !!!" + let (lxp, vn, idx) = try Option.get (browse_defs ctx lexp typer_loc) + with exe -> failwith "No reference found !!!" in - let ret = find_references l_ctx lxp vn [vn] in + let ret = find_references lxp vn idx [vn] in let r = construct_references params.textDocument.uri ret in let e = Some r in let f = Linol_lwt.return e in f @@ -1776,6 +1704,7 @@ class lsp_server = | _ -> super#on_request_unhandled ~notify_back ~id req ) in f req + *)

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