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

Commits: 10ccddf1 by Soilih BEN SOILIH at 2021-05-14T09:33:40-06:00 -

- - - - -

2 changed files:

- src/elab.ml - src/typer_lsp_server.ml

Changes:

===================================== src/elab.ml ===================================== @@ -1379,6 +1379,18 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) decls :: declss, nnctx in impl sdecls tokens ctx

+and lexp_p_decls_for_lsp (sdecls : sexp list) (tokens : token list) (ctx : elab_context) + : ((vname * lexp * ltype) list list * elab_context) = + let rec impl sdecls tokens ctx = + match (sdecls, tokens) with + | ([], []) -> [], ectx_new_scope ctx + | _ -> + let decls, sdecls, tokens, nctx = + lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + let declss, nnctx = impl sdecls tokens nctx in + decls :: declss, nnctx in + impl sdecls tokens ctx + and lexp_parse_all (p: sexp list) (ctx: elab_context) : lexp list = let res = List.map (fun pe -> let e, _ = infer pe ctx in e) p in (Log.stop_on_error (); res) @@ -1955,6 +1967,12 @@ let lexp_decl_str str ctx = let tokens = lex_source source tenv in lexp_p_decls [] tokens ctx

+let lexp_decl_str_for_lsp str ctx = + let tenv = default_stt in + let source = new Source.source_string str in + let tokens = lex_source source tenv in + lexp_p_decls_for_lsp [] tokens ctx +

(* Eval String * --------------------------------------------------------- *)

===================================== src/typer_lsp_server.ml ===================================== @@ -105,7 +105,7 @@ let readstring (str:string) = Log.clear_log () ; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str str ectx in + let ast = Elab.lexp_decl_str_for_lsp str ectx in (!Log.typer_log, ast)

let process_some_input_file (_file_contents : string) : state_after_processing = @@ -169,7 +169,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list ) )

- let browse_list_lexp (tab:Lexp.lexp list) (cursor:Source.Location.t) = + let find_the_nearest_lexp (tab:Lexp.lexp list) (cursor:Source.Location.t) = let rec foo tab cursor = match tab with | [] -> failwith "Liste vide!" @@ -180,6 +180,21 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list else foo (ml::tl) cursor in foo tab cursor

+ let browse_list_lexp (tab:(Lexp.lexp * Source.Location.t) list) (cursor:Source.Location.t) = + let rec foo tab cursor = + match tab with + | [] -> failwith "Liste vide!" + | [n] -> n + | [hd;tl] -> let (_,loc_hd) = hd in + let (_,loc_tl) = tl in + if (dist loc_hd cursor < dist loc_tl cursor ) then hd + else tl + |hd::ml::tl -> let (_,loc_hd) = hd in + let (_,loc_ml) = ml in + if (dist loc_hd cursor < dist loc_ml cursor ) then (foo (hd::tl) cursor) + else foo (ml::tl) cursor + in foo tab cursor + let pos_in_lexp_interval (tab:Lexp.lexp list) (cursor:Source.Location.t) = let open Source.Location in let rec foo tab cursor = @@ -195,7 +210,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list

let lexp_search (tab:Lexp.lexp list) (cursor:Source.Location.t) = try pos_in_lexp_interval tab cursor - with exn -> browse_list_lexp tab cursor + with exn -> find_the_nearest_lexp tab cursor

(* search the type of a lexp browsing a lexp*) let rec browse_lexp ctx e cursor = @@ -246,8 +261,9 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let ft = Opslexp.get_type ctx f in

match Opslexp.lexp'_whnf ft ctx with - | Arrow (ak', _v, t1, _l, t2) -> let e = lexp_search (List.map (fun (_, e) -> e) args) cursor in - browse_lexp ctx e cursor + | Arrow (ak', _v, t1, _l, t2) -> let e = browse_list_lexp (List.map (fun (_, e) -> (e, Lexp.lexp_location e)) args) cursor in + let (e',_) = e in + browse_lexp ctx e' cursor | _ -> browse_lexp ctx ft cursor )

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