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

Commits: 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) -> ( @@ -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,46 +939,47 @@ 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 (l, _label, args, cases) (*(Lexp.arg_kind * vname * Lexp.lexp) list SMap.t*) @@ -987,10 +990,10 @@ let browse_list_defs (tab : Source.Location.t list) (cursor:Source.Location.t) = | (_, vn, lxp)::tl -> if (vn_on_the_cursor vn cursor) then Some (lxp, vn, List.length tl) else( - if (not ((browse_defs lxp cursor) = None)) - then (browse_defs lxp cursor) - else foo cursor tl - ) + let ret = browse_defs lxp cursor in + match ret with + | Some _ -> ret + | None -> foo cursor tl) in ( try foo cursor lst

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/fdaf0fcaad9547264c98eb1d3d35c5a80c...