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

Commits: 645d3261 by Soilih BEN SOILIH at 2021-10-14T00:39:33-06:00 -

- - - - - 09aacbad by Soilih BEN SOILIH at 2021-10-14T22:37:00-06:00 fix the completion problem at the end of the file

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -377,7 +377,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp

let rec foo (ls: (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype) list) list) (cursor:Source.Location.t) : (Debruijn.lexp_context * (vname * Lexp.lexp * Lexp.ltype)) = match ls with - | [] -> failwith "No Lexp found!" + | [] -> failwith "No Lexp Found!" | hd::tl -> let (lctx_hd, hdl) = hd in let v = nearest_lexp_of_the_list hdl cursor in let (_,lxp,_) = v in @@ -443,6 +443,15 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp try pos_in_lexp_interval ctx lst cursor with exn -> find_the_nearest_lexp ctx lst cursor

+ (* If lexp_search didn't find something, give the last context + and a dummy lexp *) + let lexp_search_deeper (ctx: Debruijn.lexp_context) (lst:(vname * Lexp.lexp * Lexp.ltype) list list) (cursor:Source.Location.t) = + let lstr = update_the_context ctx lst in + let lstr_rev = List.rev lstr in + let (last_ctx,_) = List.hd lstr_rev in + try lexp_search ctx lst cursor + with exn -> (last_ctx,((Source.Location.dummy,None),Lexp.impossible, Lexp.impossible)) + (* search the type of a lexp browsing a lexp *) let rec browse_lexp (ctx:Debruijn.lexp_context) (e:Lexp.lexp) (cursor:Source.Location.t) : Debruijn.lexp_context * (((Source.Location.t * string option) * int) option) * Lexp.lexp * Source.Location.t =

@@ -610,14 +619,13 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp ) | 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; + 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 *) @@ -626,7 +634,8 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp | Sort (_, Stype l) -> l | _ -> Debruijn.level0 in let erased = Debruijn.set_empty in - let it, aargs = call_split etype in + + let it, aargs = call_split etype in ( match Opslexp.lexp'_whnf it ctx, aargs with

@@ -653,35 +662,35 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp 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 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 ( @@ -693,9 +702,7 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : (vname * Lexp.lexp 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 (); () @@ -1050,7 +1057,7 @@ class lsp_server = 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 ctx list_list typer_loc 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

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