summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 09:58:15 +0100
committerGravatar Simon Van Casteren <simonvancasteren@localhost.localdomain>2019-12-13 11:46:57 +0100
commit8ef0d043574638a48c71b7c4c9844fc05973f13d (patch)
tree07ec3be0290dceff29227edffe0b7ef1b11097de
parent171ba38b23b6acfdb28a0b591d26d3e4bb87458b (diff)
Added completion suggestions for types
-rw-r--r--src/elab_env.sig4
-rw-r--r--src/elab_env.sml20
-rw-r--r--src/lsp.sml58
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))