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

Commits: fde849c9 by Soilih BEN SOILIH at 2021-05-17T14:24:34-06:00 update completion, diagnostics

- - - - -

2 changed files:

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

Changes:

===================================== src/elab.ml ===================================== @@ -170,6 +170,21 @@ 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 @@ -208,6 +223,43 @@ 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!!" + let ctx_extend (ctx: elab_context) (var : vname) def ltype = elab_check_proper_type ctx ltype var; ectx_extend ctx var def ltype @@ -216,6 +268,10 @@ 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) @@ -1221,6 +1277,8 @@ 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 *) @@ -1360,6 +1418,151 @@ 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 @@ -1386,7 +1589,7 @@ and lexp_p_decls_for_lsp (sdecls : sexp list) (tokens : token list) (ctx : elab_ | ([], []) -> [], ectx_new_scope ctx | _ -> let decls, sdecls, tokens, nctx = - lexp_decls_1 sdecls tokens ctx ctx SMap.empty [] in + 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

===================================== src/typer_lsp_server.ml ===================================== @@ -243,8 +243,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list let _ = List.fold_left (fun n (_v, e, t) -> n - 1) (List.length defs) defs in - let (e',_) = browse_lexp ctx e cursor in - (Lexp.mkSusp e' (Opslexp.lexp_defs_subst l Subst.identity defs), Lexp.lexp_location e') + let (e',loc) = browse_lexp ctx e cursor in + (Lexp.mkSusp e' (Opslexp.lexp_defs_subst l Subst.identity defs),loc)

| Arrow (ak, v, t1, l, t2) -> ( @@ -258,8 +258,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | SortK2NotType -> (Lexp.mkSort (l, StypeOmega), location) ) - | Lambda (ak, ((l,_) as v), t, e) -> let (e',_) = browse_lexp ctx e cursor in - (Lexp.mkArrow (ak, v, t, l,e'), Lexp.lexp_location e') + | Lambda (ak, ((l,_) as v), t, e) -> let (e',loc) = browse_lexp ctx e cursor in + (Lexp.mkArrow (ak, v, t, l,e'), loc)

| Call (f, args) -> ( @@ -313,7 +313,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list 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. *) -> ( @@ -397,6 +397,7 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | _,_ -> ()); (ret,location) ) + *) | Cons (t, (_l, name)) -> (match Opslexp.lexp'_whnf t ctx with | Inductive (l, _, fargs, constructors) @@ -430,8 +431,8 @@ let diagnostics (_state : state_after_processing) : Lsp.Types.Diagnostic.t list | Metavar (idx, s, _) -> (match Lexp.metavar_lookup idx with | MVal e -> let e = Lexp.push_susp e s in - let (e',_) = browse_lexp ctx e cursor in - (e',Lexp.lexp_location e') + let (e', loc) = browse_lexp ctx e cursor in + (e',loc) | MVar (_, t, _) -> (Lexp.push_susp t s, location))

let lexp_parcourir ctx e = @@ -542,6 +543,10 @@ 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 () + (* provisional, to be done later *) method! on_req_completion ~notify_back ~id ~uri ~pos ~ctx doc_state = match Hashtbl.find buffers uri with @@ -553,7 +558,7 @@ class lsp_server = let range = lsp_range_of_loc typer_loc in let r = List.map (fun x -> let label = x in - let textEdit = Lsp.Types.TextEdit.create ~range:range ~newText:(little_fonc x) in + let textEdit = `TextEdit (Lsp.Types.TextEdit.create ~range:range ~newText:(little_fonc x)) in let kind = little_kind x in let detail = little_detail x in let ci = Lsp.Types.CompletionItem.create

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