Soilihi BEN SOILIHI BOINA pushed to branch minimal-server at Stefan / Typer

Commits: edafb37e by Soilih at 2022-07-11T00:00:15-04:00 -

- - - - - b9524636 by Soilih at 2022-07-11T00:02:33-04:00 -

- - - - - fdaf0fca by Soilih at 2022-07-11T22:19:05-04:00 modify browse_lexp and browse_defs

- - - - -

1 changed file:

- src/typer_lsp_server.ml

Changes:

===================================== src/typer_lsp_server.ml ===================================== @@ -370,20 +370,21 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> Debruijn.lctx_extend ctx v ForwardRef t) ctx defs in - let br_lst = List.fold_left - (fun lst (vn, _, _) -> - vn::lst - ) lst_in defs - in let tab = List.map - (fun (_, lxp, _) -> - browse_lexp ctx' lxp cursor br_lst + (fun (vn, lxp, _) -> + browse_lexp ctx' lxp cursor (vn::lst_in) + ) + defs + in + let tab' = List.map + (fun (vn, _, ltp) -> + (ctx', None, ltp, None, Lexp.lexp_location ltp, (vn::lst_in)) ) defs in

(*let lt = (ctx,None, Lexp.mkSusp (Opslexp.get_type ctx e) (Opslexp.lexp_defs_subst l Subst.identity defs),l) in*) - browse_list_lexp ((browse_lexp ctx' e cursor br_lst)::tab) cursor + browse_list_lexp (List.append ((browse_lexp ctx' e cursor lst_in)::tab) tab') cursor

| Arrow (ak, v, t1, l, t2) -> ( @@ -401,11 +402,11 @@ let update_the_context (ctx: Debruijn.lexp_context) (liste : syntax_tree ) : (De -> (nctx, None, Lexp.mkSort (l, StypeOmega), None, location, lst_in) )

- | Lambda (_, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in + | Lambda (ak, ((l,_) as v), t, e) -> let ctx' = Debruijn.lctx_extend ctx v Variable t in let a = browse_lexp ctx' e cursor lst_in in let b = browse_lexp ctx t cursor lst_in in (*let etp = Opslexp.get_type ctx' e in - let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp),l) in*) + let c = (ctx,None, Lexp.mkArrow (ak,v,t,l,etp), None, l, lst_in) in*) let d = (ctx, None, t, None, l, lst_in) in browse_list_lexp ([a;b;d]) cursor

@@ -914,9 +915,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | Imm (Block (_, _) | Symbol _ | Node (_, _)) -> None | SortLevel SLz -> None | SortLevel (SLsucc e) -> browse_defs e cursor - | SortLevel (SLlub (e1, e2)) -> if not ((browse_defs e1 cursor) = None) then - browse_defs e1 cursor - else browse_defs e2 cursor + | SortLevel (SLlub (e1, e2)) -> let ret = browse_defs e1 cursor in + (match ret with + | Some _ -> ret + | None -> browse_defs e2 cursor) | Sort (_, Stype e) -> browse_defs e cursor | Sort (_, StypeLevel) -> None | Sort (_, StypeOmega) -> None @@ -937,48 +939,66 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = match ctx_list with | [] -> failwith "No variable found on the cursor!" | (_, _, ltp)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs ltp cursor - else foo'' tl cursor (comp + 1) + -> let ret = browse_defs ltp cursor in + (match ret with + | None -> foo'' tl cursor (comp + 1) + | Some _ -> ret) in let rec foo' (ctx_list: (vname * Lexp.lexp * Lexp.lexp) list) cursor comp = match ctx_list with - | [] -> foo'' ctx_list cursor comp + | [] -> foo'' defs cursor comp | (_, lxp, _)::tl - -> if (not ((browse_defs lxp cursor) = None)) then - browse_defs lxp cursor - else foo' tl cursor (comp + 1) + -> let ret = browse_defs lxp cursor in + (match ret with + | None -> foo' tl cursor (comp + 1) + | Some _ -> ret) in try foo defs cursor 0 with _ - -> if (not ((browse_defs el cursor) = None)) then - browse_defs el cursor - else foo' defs cursor 0 - ) + -> let ret = browse_defs el cursor in + (match ret with + | None -> foo' defs cursor 0 + | Some _ -> ret))

| Arrow (_, v, t1, _, t2) -> if (vn_on_the_cursor v cursor) then Some (t2, v, 0) - else (if not ((browse_defs t1 cursor) = None) then - browse_defs t1 cursor - else browse_defs t2 cursor - ) + else (let ret = browse_defs t1 cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t2 cursor)

| Lambda (_, 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 (if not ((browse_defs e cursor) = None) then - browse_defs e cursor - else browse_defs t cursor - ) + else (let ret = browse_defs e cursor in + match ret with + | Some _ -> ret + | None -> browse_defs t cursor)

- | Call (f, args) -> if not ((browse_defs f cursor) = None) then - browse_defs f cursor - else ( - List.fold_right (fun (_, lxp) _ret -> - browse_defs lxp cursor) args None - ) + | Call (f, args) -> (let ret = browse_defs f cursor in + match ret with + | Some _ -> ret + | None -> (List.fold_right (fun (_, lxp) _ret -> + browse_defs lxp cursor) args None))

- | Inductive _ -> None + | Inductive (l, _label, args, cases) + (*(Lexp.arg_kind * vname * Lexp.lexp) list SMap.t*) + -> let (_, lst) = List.hd (SMap.bindings cases) in + let rec foo cursor lst = + match lst with + | [] -> failwith "cursor is not on a vdef" + | (_, vn, lxp)::tl + -> if (vn_on_the_cursor vn cursor) then Some (lxp, vn, List.length tl) + else( + let ret = browse_defs lxp cursor in + match ret with + | Some _ -> ret + | None -> foo cursor tl) + in + ( + try foo cursor lst + with _ -> foo cursor args + ) | Proj (_, e, (_, _)) -> browse_defs e cursor | Case (_, e, _, branches, _) ->

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