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

Commits: a3ccd6b2 by Soilih BEN SOILIH at 2021-05-20T19:39:18-06:00 resolve completion, diagnostics problems...case still not working*

- - - - -

4 changed files:

- src/elab.ml - src/lexp.ml - src/log.ml - src/typer_lsp_server.ml

Changes:

===================================== src/elab.ml ===================================== @@ -170,21 +170,6 @@ let elab_check_proper_type (ctx : elab_context) ltp var = -> " of var `" ^ name ^ "`")); raise e

-let elab_check_proper_type_lsp (ctx : elab_context) ltp var = -try elab_check_sort ctx (OL.check (ectx_to_lctx ctx) ltp) var ltp -with e -> match e with - | _ -> - info - ~print_action:(fun _ -> - print_lexp_ctx (ectx_to_lctx ctx); print_newline () - ) - ~loc:(lexp_location ltp) - ("Exception while checking type `" ^ (lexp_string ltp) ^ "`" - ^ (match var with - | (_, None) -> "" - | (_, Some name) - -> " of var `" ^ name ^ "`")); - raise e let elab_check_def (ctx : elab_context) var lxp ltype = let lctx = ectx_to_lctx ctx in let loc = lexp_location lxp in @@ -212,6 +197,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = then elab_check_proper_type ctx ltype var else + ( + if !Log.lsp_enabled then fatal ~print_action:(fun _ -> List.iter print_indent_line [ @@ -222,43 +209,8 @@ let elab_check_def (ctx : elab_context) var lxp ltype = ]) ~loc "Type check error: ¡¡ctx_define error!!" - -let elab_check_def_lsp (ctx : elab_context) var lxp ltype = - let lctx = ectx_to_lctx ctx in - let loc = lexp_location lxp in - - let ltype' = try OL.check lctx lxp - with e -> match e with - | _ -> - info - ~print_action:(fun _ -> - lexp_print_details lxp (); - print_lexp_ctx (ectx_to_lctx ctx); - print_newline () - ) - ~loc - "Error while type-checking"; - raise e in - if (try OL.conv_p (ectx_to_lctx ctx) ltype ltype' - with e -> - info ~print_action:(lexp_print_details lxp) - ~loc - ("Exception while conversion-checking types: " - ^ lexp_string ltype ^ " and " ^ lexp_string ltype'); - raise e) - then - elab_check_proper_type ctx ltype var - else - fatal - ~print_action:(fun _ -> - List.iter print_indent_line [ - (match var with (_, Some n) -> n | _ -> "<anon>") - ^ " = " ^ lexp_string lxp ^ " !: " ^ lexp_string ltype; - " because"; - lexp_string ltype' ^ " != " ^ lexp_string ltype - ]) - ~loc - "Type check error: ¡¡ctx_define error!!" + else () + )

let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; @@ -268,10 +220,6 @@ let ctx_define (ctx: elab_context) var lxp ltype = elab_check_def ctx var lxp ltype; ectx_extend ctx var (LetDef (0, lxp)) ltype

-let ctx_define_lsp (ctx: elab_context) var lxp ltype = - elab_check_def_lsp ctx var lxp ltype; - ectx_extend ctx var (LetDef (0, lxp)) ltype - let ctx_define_rec (ctx: elab_context) decls = let nctx = ectx_extend_rec ctx decls in let _ = List.fold_left (fun n (var, _lxp, ltp) @@ -1277,8 +1225,6 @@ and infer_and_generalize_def (ctx : elab_context) se = t in (e', t')

-(*====================premier=========================*) - and lexp_decls_1 (sdecls : sexp list) (* What's already parsed *) (tokens : token list) (* Rest of input *) @@ -1418,151 +1364,6 @@ and lexp_decls_1 pending_decls pending_defs in (Log.stop_on_error (); res))

-(*====================premier=========================*) - -(*====================second=========================*) - -and lexp_decls_1_lsp -(sdecls : sexp list) (* What's already parsed *) -(tokens : token list) (* Rest of input *) -(ectx : elab_context) (* External ctx. *) -(nctx : elab_context) (* New context. *) -(pending_decls : Source.Location.t SMap.t) (* Pending type decls. *) -(pending_defs : (symbol * sexp) list) (* Pending definitions. *) -: (vname * lexp * ltype) list * sexp list * token list * elab_context = - - let rec lexp_decls_1_lsp sdecls tokens nctx pending_decls pending_defs = - let sdecl, sdecls, toks = - match (sdecls, tokens) with - | (s :: sdecls, _) -> Some s, sdecls, tokens - | ([], []) -> None, [], [] - | ([], _) -> - let (s, toks) = sexp_parse_all (ectx_get_grammar nctx) - tokens (Some ";") in - Some s, [], toks in - let recur prepend_sdecls nctx pending_decls pending_defs = - lexp_decls_1_lsp (List.append prepend_sdecls sdecls) - toks nctx pending_decls pending_defs in - match sdecl with - | None -> (if not (SMap.is_empty pending_decls) then - let (s, loc) = SMap.choose pending_decls in - error ~loc ("Variable `" ^ s ^ "` declared but not defined!") - else - assert (pending_defs == [])); - [], [], [], nctx - - | Some (Symbol (_, "")) - -> recur [] nctx pending_decls pending_defs - - | Some (Node (Symbol (_, ("_;_" (* | "_;" | ";_" *))), sdecls')) - -> recur sdecls' nctx pending_decls pending_defs - - | Some (Node (Symbol (loc, "_:_"), args) as thesexp) - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol (loc, vname); stp] - -> let ltp = infer_and_generalize_type nctx stp (loc, Some vname) in - if SMap.mem vname pending_decls then - (* Don't burp: take'em all and unify! *) - let pt_idx = senv_lookup vname nctx in - (* Take the previous type annotation. *) - let pt = match Myers.nth pt_idx (ectx_to_lctx nctx) with - | (_, ForwardRef, t) -> push_susp t (S.shift (pt_idx + 1)) - | _ -> Log.internal_error "Var not found at its index!" in - (* Unify it with the new one. *) - let _ = match Unif.unify ltp pt (ectx_to_lctx nctx) with - | (_::_) - -> lexp_error loc ltp - ("New type annotation `" - ^ lexp_string ltp ^ "` incompatible with previous `" - ^ lexp_string pt ^ "`") - | [] -> () in - recur [] nctx pending_decls pending_defs - else if List.exists (fun ((_, vname'), _) -> vname = vname') - pending_defs then - (error ~loc ("Variable `" ^ vname ^ "` already defined!"); - recur [] nctx pending_decls pending_defs) - else recur [] (ectx_extend nctx (loc, Some vname) ForwardRef ltp) - (SMap.add vname loc pending_decls) - pending_defs - | _ -> error ~loc ("Invalid type declaration syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) - - | Some (Node (Symbol (l, "_=_") as head, args) as thesexp) - (* FIXME: Move this to a "special form"! *) - -> (match args with - | [Symbol ((l, vname)); sexp] - when SMap.is_empty pending_decls - -> assert (pending_defs == []); - (* Used to be true before we added define-operator. *) - (* assert (ectx == nctx); *) - let (lexp, ltp) = infer_and_generalize_def nctx sexp in - let var = (l, Some vname) in - (* Lexp decls are always recursive, so we have to shift by 1 to - * account for the extra var (ourselves). *) - [(var, mkSusp lexp (S.shift 1), ltp)], sdecls, toks, - ctx_define_lsp nctx var lexp ltp - - | [Symbol (l, vname); sexp] - -> if SMap.mem vname pending_decls then - let decl_loc = SMap.find vname pending_decls in - let v = - let doc = - match decl_loc.doc, l.doc with - | Some (doc), Some (doc') - -> Some (Printf.sprintf "%s\n%s" doc doc') - | Some (doc), None | None, Some (doc) -> Some (doc) - | None, None -> None; - in - ({l with doc}, vname) - in - let pending_decls = SMap.remove vname pending_decls in - let pending_defs = ((v, sexp) :: pending_defs) in - if SMap.is_empty pending_decls then - let nctx = ectx_new_scope nctx in - let decls, nctx = lexp_check_decls ectx nctx pending_defs in - decls, sdecls, toks, nctx - else - recur [] nctx pending_decls pending_defs - - else - (error ~loc:l ("`" ^ vname ^ "` defined but not declared!"); - recur [] nctx pending_decls pending_defs) - - | [Node (Symbol s, args) as d; body] - -> (* FIXME: Make it a macro (and don't hardcode `lambda_->_`)! *) - recur [Node (head, - [Symbol s; - Node (Symbol (sexp_location d, "lambda_->_"), - [sexp_u_list args; body])])] - nctx pending_decls pending_defs - - | _ -> error ~loc:l ("Invalid definition syntax : `" ^ - (sexp_string thesexp) ^ "`"); - recur [] nctx pending_decls pending_defs) - - | Some (Node (Symbol (l, "define-operator"), args)) - (* FIXME: Move this to a "special form"! *) - -> recur [] (sdform_define_operator nctx l args None) - pending_decls pending_defs - - | Some (Node (Symbol ((_l, _) as v), sargs)) - -> (* expand macro and get the generated declarations *) - let sdecl' = lexp_decls_macro v sargs nctx in - recur [sdecl'] nctx pending_decls pending_defs - - | Some sexp - -> error ~loc:(sexp_location sexp) "Invalid declaration syntax"; - recur [] nctx pending_decls pending_defs - - in (EV.set_getenv nctx; - let res = lexp_decls_1_lsp sdecls tokens nctx - pending_decls pending_defs in - (Log.stop_on_error (); res)) - -(*====================second=========================*) - (* Why is the return value a list of list? - each `(vname * lexp * ltype)` is a definition - each `(vname * lexp * ltype) list` is a list of definitions which can refer @@ -1581,19 +1382,7 @@ and lexp_p_decls (sdecls : sexp list) (tokens : token list) (ctx : elab_context) let declss, nnctx = impl sdecls tokens nctx in 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_lsp 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) @@ -2170,13 +1959,6 @@ 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 * --------------------------------------------------------- *) (* Because we cant include Elab in eval.ml *)

===================================== src/lexp.ml ===================================== @@ -827,6 +827,25 @@ let pretty_ppctx = ("print_implicit", Bool (false)); ("grammar" , Predtl (default_grammar))]

+(*Pretty ppctx for lsp*) + +let pretty_ppctx_for_lsp = + List.fold_left (fun map (key, v) -> SMap.add key v map) + SMap.empty + [("pretty" , Bool (true) ); (* print with new lines and indents *) + ("print_type" , Bool (true) ); (* print inferred Type *) + ("print_dbi" , Bool (false)); (* print dbi index *) + ("indent_size" , Int (2) ); (* indent step *) + ("color" , Bool (false) ); (* use console color to display hints *) + ("separate_decl" , Bool (true) ); (* print newline between declarations *) + ("indent_level" , Int (0) ); (* current indent level *) + ("col_max" , Int (80) ); (* col_size + col_ofsset <= col_max *) + ("col_size" , Int (0) ); (* current column size *) + ("col_ofsset" , Int (0) ); (* if col does not start at 0 *) + ("print_erasable", Bool (false)); + ("print_implicit", Bool (false)); + ("grammar" , Predtl (default_grammar))] + (* debug_ppctx is a ref so we can modify it in the REPL *) let debug_ppctx = ref ( List.fold_left (fun map (key, v) -> SMap.add key v map) @@ -837,6 +856,16 @@ let debug_ppctx = ref ( ("print_implicit", Bool (true)); ("separate_decl" , Bool (false) );])

+(*debug ppctx for lsp*) + +let debug_ppctx_for_lsp = ref ( + List.fold_left (fun map (key, v) -> SMap.add key v map) + pretty_ppctx_for_lsp + [("pretty" , Bool (false) ); + ("print_dbi" , Bool (false) ); + ("print_erasable", Bool (true)); + ("print_implicit", Bool (true)); + ("separate_decl" , Bool (false) );]) let smap_bool s ctx = match SMap.find s ctx with Bool b -> b | _ -> failwith "Unreachable" and smap_int s ctx = @@ -1115,6 +1144,9 @@ and lexp_str_decls ctx decls = [] decls in List.rev ret

+(*print string of a type in lsp *) +let lexp_string_for_lsp e = lexp_cstring (!debug_ppctx_for_lsp) e + (** Syntactic equality (i.e. without β). *******)

let rec eq e1 e2 =

===================================== src/log.ml ===================================== @@ -22,6 +22,10 @@ this program. If not, see http://www.gnu.org/licenses/. *)

open Util

+(*lsp enabled or no*) + +let lsp_enabled = ref false + (* LOGGING LEVELS *)

type log_level = Nothing | Fatal | Error | Warning | Info | Debug @@ -187,6 +191,8 @@ let log_fatal ?section ?print_action ?loc m = typer_log_config.print_at_log <- true; log_msg Fatal ~kind:"[X] Fatal " ?section ?print_action ?loc m; internal_error "Compiler Fatal Error" + + let log_error = log_msg Error ?kind:None let log_warning = log_msg Warning ?kind:None let log_info = log_msg Info ?kind:None @@ -195,16 +201,22 @@ let log_debug = log_msg Debug ?kind:None let stop_on_error () = let count = error_count () in if (0 < count) then + ( + if !lsp_enabled then stop_compilation ("Compiler stopped after: "^(string_of_int count)^" errors\n") - + else () + ) let stop_on_warning () = stop_on_error (); let count = warning_count () in if (0 < count) then + ( + if !lsp_enabled then stop_compilation ("Compiler stopped after: "^(string_of_int count)^" warnings\n") - + else () + ) (* Compiler Internal Debug print *) let debug_msg expr = if Debug <= typer_log_config.level then (print_string expr; flush stdout)

===================================== src/typer_lsp_server.ml ===================================== @@ -103,9 +103,10 @@ let rec search_lexp_with_a_location (lexp_list: Lexp.lexp list) (location : Sour

let readstring (str:string) = Log.clear_log () ; + Arg.Set Log.lsp_enabled; let ectx = Elab.default_ectx in (*let rctx = Elab.default_rctx in*) - let ast = Elab.lexp_decl_str_for_lsp str ectx in + let ast = Elab.lexp_decl_str str ectx in (!Log.typer_log, ast)

let process_some_input_file (_file_contents : string) : state_after_processing = @@ -263,14 +264,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list

| Call (f, args) -> ( - let ft = Opslexp.get_type ctx f in - - match Opslexp.lexp'_whnf ft ctx with - | 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 - ) + let fonc = browse_lexp ctx f cursor in + let args_list = List.map (fun (_ , e) -> browse_lexp ctx e cursor) args in + browse_list_lexp (fonc::args_list) cursor + )

| Inductive (l, _label, args, cases) ->( @@ -312,12 +309,13 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list args) in let tct = arg_loop ctx Debruijn.set_empty args in (tct, location) - ) - (* + ) | Case (l, e, ret, branches, default) (* FIXME: Check that the return type isn't TypeLevel. *) - -> ( - let call_split e = + -> + ( + + let call_split (e: Lexp.lexp) = match Lexp.lexp_lexp' e with | Call (f, args) -> (f, args) | _ -> (e,[]) in @@ -329,10 +327,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let elvl = match Opslexp.lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l | _ -> Debruijn.level0 in - let it, aargs = call_split etype in - let nerased = Opslexp.nerased_let defs Debruijn.set_empty in - let subst = Subst.shift 1 in let erased = Debruijn.set_empty 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 = @@ -344,7 +340,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list -> 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 nerased = + 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 @@ -354,10 +350,10 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list (Lexp.Anormal, hlxp); (* Lexp of the branch head *) (Lexp.Anormal, tlxp)]) in (* Target lexp *) (* The eq proof is erasable. *) - let nerased = Opslexp.dbset_push Lexp.Aerasable nerased in let nctx = Debruijn.lexp_ctx_cons ctx (l, None) Variable eqty in - (nerased, nctx) in - SMap.iter + (erased, nctx) in + + let foo = (fun name (l, vdefs, branch) -> let fieldtypes = SMap.find name constructors in let rec mkctx erased ctx s hlxp vdefs fieldtypes = @@ -368,36 +364,43 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | (ak, vdef)::vdefs, (_ak', _vdef', ftype)::fieldtypes -> mkctx (Opslexp.dbset_push ak erased) (Debruijn.lexp_ctx_cons ctx vdef Variable (Lexp.mkSusp ftype s)) - (ssink vdef s) - (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, mkVar (vdef, 0))])) + (Lexp.ssink vdef s) + (Lexp.mkCall (Lexp.mkSusp hlxp (Subst.shift 1), [(ak, Lexp.mkVar (vdef, 0))])) vdefs fieldtypes - | _,_ -> ((erased, ctx, hlxp)) in + | _,_ -> (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 nerased in - (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1)))) - branches; - let diff = SMap.cardinal constructors - SMap.cardinal branches in + let (nerased, nctx) = ctx_extend_with_eq nctx subst hlxp in + browse_lexp ctx branch cursor; + (Lexp.mkSusp ret (Subst.shift ((List.length fieldtypes) + 1))) + ) + in + let lst = foo (Lexp.get_name branches) branches in + let brch = SMap.bindings lst in + + let diff = SMap.cardinal constructors - SMap.cardinal brch in (match default with | Some (v, d) -> if diff <= 0 then (); let nctx = (Debruijn.lctx_extend ctx v (LetDef (0, e)) etype) in let nerased = Debruijn.set_sink 1 erased in let subst = Subst.shift 1 in - let hlxp = mkVar ((l, None), 0) in + let hlxp = Lexp.mkVar ((l, None), 0) in let (nerased, nctx) = - ctx_extend_with_eq nctx subst hlxp nerased in + ctx_extend_with_eq nctx subst hlxp in (Lexp.mkSusp ret (Subst.shift 2)) | None -> if diff > 0 then () ) - | _,_ -> ()); + | _,_ -> ())); (ret,location) + ) - *) + + | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -518,7 +521,7 @@ class lsp_server = let ctx = Debruijn.ectx_to_lctx (Elab.default_ectx) in let (l_type,location) = browse_lexp ctx lexp typer_loc in let range = lsp_range_of_loc location in - let s = Lexp.lexp_string l_type in + let s = Lexp.lexp_string_for_lsp l_type in let r = Lsp.Types.Hover.create ~contents:(`MarkedString {Lsp.Types.MarkedString.value=s; language=None}) ~range:range () @@ -543,10 +546,15 @@ class lsp_server = let e = Linol_lwt.return h in e | _ -> assert false

- method! config_modify_capabilities compl = - let t = Lsp.Types.CompletionOptions.create ~workDoneProgress:true ~resolveProvider:true () in - Lsp.Types.ServerCapabilities.create ~completionProvider:t () - + method! config_modify_capabilities arg = + let completionProvider = + (* TODO even if this re-enabled in general, it should stay disabled for + emacs. It makes completion too slow *) + Lsp.Types.CompletionOptions.create ~triggerCharacters:[ "."; "#"; """; "'"; "/"; "@"; "<"] + ~resolveProvider:true () in + { arg with Lsp.Types.ServerCapabilities.completionProvider = Some completionProvider } + + (* provisional, to be done later *) method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with

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