From 8ef0d043574638a48c71b7c4c9844fc05973f13d Mon Sep 17 00:00:00 2001 From: Simon Van Casteren Date: Fri, 13 Dec 2019 09:58:15 +0100 Subject: Added completion suggestions for types --- src/elab_env.sig | 4 ++-- src/elab_env.sml | 20 ++++++++++++++----- src/lsp.sml | 58 +++++++++++++++++++++++++++++++++++++------------------- 3 files changed, 56 insertions(+), 26 deletions(-) diff --git a/src/elab_env.sig b/src/elab_env.sig index 55909b53..fb95d68e 100644 --- a/src/elab_env.sig +++ b/src/elab_env.sig @@ -61,6 +61,7 @@ signature ELAB_ENV = sig val lookupCNamed : env -> int -> string * Elab.kind * Elab.con option val lookupC : env -> string -> Elab.kind var + val matchCByPrefix: env -> string -> (string * Elab.kind) list val pushDatatype : env -> int -> string list -> (string * int * Elab.con option) list -> env type datatyp @@ -85,8 +86,7 @@ signature ELAB_ENV = sig val pushENamedAs : env -> string -> int -> Elab.con -> env val lookupENamed : env -> int -> string * Elab.con val checkENamed : env -> int -> bool - val matchNamedEByPrefix: env -> string -> (string * Elab.con) list - val matchRelEByPrefix: env -> string -> (string * Elab.con) list + val matchEByPrefix: env -> string -> (string * Elab.con) list val lookupE : env -> string -> Elab.con var diff --git a/src/elab_env.sml b/src/elab_env.sml index e79b665d..34071664 100644 --- a/src/elab_env.sml +++ b/src/elab_env.sml @@ -404,6 +404,14 @@ fun lookupC (env : env) x = | SOME (Rel' x) => Rel x | SOME (Named' x) => Named x +fun matchCByPrefix (env: env) (prefix: string): (string * kind) list = + List.mapPartial (fn (name, value) => if String.isPrefix prefix name + then case value of + Rel' (_, x) => SOME (name, x) + | Named' (_, x) => SOME (name, x) + else NONE) + (SM.listItemsi (#renameC env)) + fun pushDatatype (env : env) n xs xncs = let val dk = U.classifyDatatype xncs @@ -932,11 +940,13 @@ fun lookupENamed (env : env) n = NONE => raise UnboundNamed n | SOME x => x -fun matchNamedEByPrefix (env: env) (str: string) = - List.filter (fn (name,con) => String.isPrefix str name) (IM.listItems (#namedE env)) - -fun matchRelEByPrefix (env: env) (str: string) = - List.filter (fn (name,con) => String.isPrefix str name) (#relE env) +fun matchEByPrefix (env: env) (prefix: string): (string * con) list = + List.mapPartial (fn (name, value) => if String.isPrefix prefix name + then case value of + Rel' (_, x) => SOME (name, x) + | Named' (_, x) => SOME (name, x) + else NONE) + (SM.listItemsi (#renameE env)) fun checkENamed (env : env) n = Option.isSome (IM.find (#namedE env, n)) diff --git a/src/lsp.sml b/src/lsp.sml index 2c9aab56..2d80479b 100644 --- a/src/lsp.sml +++ b/src/lsp.sml @@ -762,7 +762,7 @@ fun readFile (fileName: string): string = end -(* TODO I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *) +(* TODO PERF BIG I couldn't figure out how to print just to a string, so writing to a temp file, then reading it, then deleting it, ... *) fun ppToString (pp: Print.PD.pp_desc) (width: int): string = let val tempfile = OS.FileSys.tmpName () @@ -827,7 +827,7 @@ fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (search | (Elab.SgiCon (name, _, _, con), _) => if String.isPrefix searchStr name then [{ label = prefix ^ name - , kind = LspSpec.Variable + , kind = LspSpec.Value , detail = ppToString (ElabPrint.p_con env con) 150 }] else [] @@ -874,6 +874,7 @@ fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (search List.concat (List.map mapF items) end +(* TODO TOCHECK look at con's to specify "kind" more accurately *) fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completionItem list = let val splitted = Substring.fields (fn c => c = #".") (Substring.full str) @@ -882,18 +883,35 @@ fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completion (_ :: []) => if str = "" then [] - else (List.map (fn (name,con) => - { label = name - , kind = LspSpec.Variable - , detail = ppToString (ElabPrint.p_con env con) 150 - }) - (ElabEnv.matchRelEByPrefix env str - @ ElabEnv.matchNamedEByPrefix env str)) + else + let + val matchingEs = ElabEnv.matchEByPrefix env str (* function params, let bindings and top-level bindings. Should we discern between Rel and Named? *) + val expressionCompletions = List.map (fn (name,con) => + { label = name + , kind = LspSpec.Value + , detail = ppToString (ElabPrint.p_con env con) 150 + }) matchingEs + val matchingStrs = ElabEnv.matchStrByPrefix env str + val structureCompletions = List.map (fn (name,(_,sgn)) => + { label = name + , kind = LspSpec.Module + , detail = "" + }) matchingStrs + val matchingCons = ElabEnv.matchCByPrefix env str + val conCompletions = List.map (fn (name,kind) => + { label = name + , kind = LspSpec.Constructor (* TODO probably wrong... *) + , detail = ppToString (ElabPrint.p_kind env kind) 150 + }) matchingCons + in + expressionCompletions @ structureCompletions @ conCompletions + end | (r :: str :: []) => if Char.isUpper (Substring.sub (r, 0)) - then (* r should be a structure *) + then + (* Completing STRUCTURE *) let - (* TODO Perf: first match and then equal is not perfect *) + (* TODO PERF SMALL: first match and then equal is not perfect *) val foundStrs = ElabEnv.matchStrByPrefix env (Substring.string r) val filteredStrs = List.filter (fn (name,_) => name = Substring.string r) foundStrs in @@ -903,13 +921,13 @@ fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completion getCompletionsFromSignatureItems env (name ^ ".") (Substring.string str) sgis | _ => []) end - else (* r should be a record *) - (* TODO is it correct to first try RelE and then NamedE? *) + else + (* Completing RECORD *) + (* TODO TOCHECK is it correct to first try RelE and then NamedE? *) let - (* TODO Perf: first match and then equal is not perfect *) - val foundRelEs = ElabEnv.matchRelEByPrefix env (Substring.string r) - val foundNamedEs = ElabEnv.matchNamedEByPrefix env (Substring.string r) - val filteredEs = List.filter (fn (name,_) => name = Substring.string r) (foundRelEs @ foundNamedEs) + (* TODO PERF SMALL: first match and then equal is not perfect *) + val foundEs = ElabEnv.matchEByPrefix env (Substring.string r) + val filteredEs = List.filter (fn (name,_) => name = Substring.string r) foundEs in (case List.map (fn (name, c) => (name, ElabOps.reduceCon env c)) filteredEs of [] => [] @@ -917,10 +935,12 @@ fun findMatchingStringInEnv (env: ElabEnv.env) (str: string): LspSpec.completion getCompletionsFromFields env (name ^ ".") (Substring.string str) fields | _ => []) end - | _ => [] + | _ => + (* TODO NOTIMPLEMENTED submodules / nested records *) + [] end -(* TODO can we use the real parser to figure out what we're typing (exp, con, field, etc) to predict better? *) +(* TODO IDEA can we use the real parser to figure out what we're typing (exp, con, field, etc) to predict better? *) fun handleCompletion (state: state) (p: LspSpec.completionReq) = let val fileName = #path (#uri (#textDocument p)) -- cgit v1.2.3