summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Simon Van Casteren <simon.van.casteren@gmail.com>2020-01-11 21:51:21 +0100
committerGravatar Simon Van Casteren <simon.van.casteren@gmail.com>2020-01-11 21:51:21 +0100
commit0e6ae5392121aa2163199292963f0f98776b6790 (patch)
treeff5214a32a29373e77ec0e7b89d04413ae0ec173
parent9f002a8199a6cba79c3c965731bc9be72506b388 (diff)
Fixed review changes: Better foundInEnv naming, correct interpretation of
SgiSgn, fix uniq
-rw-r--r--src/getinfo.sig4
-rw-r--r--src/getinfo.sml35
-rw-r--r--src/lsp.sml14
3 files changed, 26 insertions, 27 deletions
diff --git a/src/getinfo.sig b/src/getinfo.sig
index 663a9a81..63850ef2 100644
--- a/src/getinfo.sig
+++ b/src/getinfo.sig
@@ -28,8 +28,8 @@
signature GET_INFO = sig
datatype foundInEnv = FoundStr of (string * Elab.sgn)
- | FoundCon of (string * Elab.kind)
- | FoundExp of (string * Elab.con)
+ | FoundKind of (string * Elab.kind)
+ | FoundCon of (string * Elab.con)
val findStringInEnv:
ElabEnv.env ->
diff --git a/src/getinfo.sml b/src/getinfo.sml
index 760a4d90..6adfbdcf 100644
--- a/src/getinfo.sml
+++ b/src/getinfo.sml
@@ -163,32 +163,31 @@ fun findFirstExpAfter env str fileName {line = line, char = char} =
datatype foundInEnv = FoundStr of (string * Elab.sgn)
- | FoundCon of (string * Elab.kind)
- | FoundExp of (string * Elab.con)
+ | FoundKind of (string * Elab.kind)
+ | FoundCon of (string * Elab.con)
fun getNameOfFoundInEnv (f: foundInEnv) =
case f of
FoundStr (x, _) => x
+ | FoundKind (x, _) => x
| FoundCon (x, _) => x
- | FoundExp (x, _) => x
fun filterSgiItems (items: Elab.sgn_item list) : foundInEnv list =
let
fun mapF item =
case item of
- (Elab.SgiVal (name, _, c), _) => [FoundExp (name, c)]
- | (Elab.SgiCon (name, _, k, _), _) => [FoundCon (name, k)]
+ (Elab.SgiVal (name, _, c), _) => [FoundCon (name, c)]
+ | (Elab.SgiCon (name, _, k, _), _) => [FoundKind (name, k)]
| (Elab.SgiDatatype ds, loc) =>
List.concat (List.map (fn (dtx, i, _, cs) =>
- FoundExp (dtx, (Elab.CNamed i, loc))
- :: List.map (fn (x, i, _) => FoundExp (x, (Elab.CRel i, loc))) cs) ds)
+ FoundCon (dtx, (Elab.CNamed i, loc))
+ :: List.map (fn (x, i, _) => FoundCon (x, (Elab.CRel i, loc))) cs) ds)
| (Elab.SgiDatatypeImp (x, i, _, _, _, _, cs), loc) =>
- FoundExp (x, (Elab.CNamed i, loc))
- :: List.map (fn (x, i, _) => FoundExp (x, (Elab.CRel i, loc))) cs
+ FoundCon (x, (Elab.CNamed i, loc))
+ :: List.map (fn (x, i, _) => FoundCon (x, (Elab.CRel i, loc))) cs
| (Elab.SgiStr (_, name, _, sgn), _) =>
[FoundStr (name, sgn)]
- | (Elab.SgiSgn (name, _, sgn), _) =>
- [FoundStr (name, sgn)]
+ | (Elab.SgiSgn (name, _, sgn), _) => []
| _ => []
in
List.concat (List.map mapF items)
@@ -208,7 +207,7 @@ fun resolvePrefixes
| SOME (FoundStr (name, sgn)) => (case ElabEnv.hnormSgn env sgn of
(Elab.SgnConst sgis, _) => resolvePrefixes env rest (filterSgiItems sgis)
| _ => [])
- | SOME (FoundExp (name, c)) =>
+ | SOME (FoundCon (name, c)) =>
let
val fields = case ElabOps.reduceCon env c of
(Elab.TRecord (Elab.CRecord (_, fields), l2_), l1_) =>
@@ -223,12 +222,12 @@ fun resolvePrefixes
| _ => []
val items =
List.mapPartial (fn (c1, c2) => case c1 of
- (Elab.CName fieldName, _) => SOME (FoundExp (fieldName, c2))
+ (Elab.CName fieldName, _) => SOME (FoundCon (fieldName, c2))
| _ => NONE) fields
in
resolvePrefixes env rest items
end
- | SOME (FoundCon (_, _)) => [])
+ | SOME (FoundKind (_, _)) => [])
fun findStringInEnv' (env: ElabEnv.env) (preferCon: bool) (str: string): (string (* prefix *) * foundInEnv option) =
@@ -236,8 +235,8 @@ fun findStringInEnv' (env: ElabEnv.env) (preferCon: bool) (str: string): (string
val splitted = List.map Substring.string (Substring.fields (fn c => c = #".") (Substring.full str))
val afterResolve = resolvePrefixes env (List.take (splitted, List.length splitted - 1))
( List.map (fn (name, (_, sgn)) => FoundStr (name, sgn)) (ElabEnv.dumpStrs env)
- @ List.map FoundCon (ElabEnv.dumpCs env)
- @ List.map FoundExp (ElabEnv.dumpEs env))
+ @ List.map FoundKind (ElabEnv.dumpCs env)
+ @ List.map FoundCon (ElabEnv.dumpEs env))
val query = List.last splitted
val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
in
@@ -249,8 +248,8 @@ fun matchStringInEnv' (env: ElabEnv.env) (str: string): (string (* prefix *) * f
val splitted = List.map Substring.string (Substring.fields (fn c => c = #".") (Substring.full str))
val afterResolve = resolvePrefixes env (List.take (splitted, List.length splitted - 1))
( List.map (fn (name, (_, sgn)) => FoundStr (name, sgn)) (ElabEnv.dumpStrs env)
- @ List.map FoundCon (ElabEnv.dumpCs env)
- @ List.map FoundExp (ElabEnv.dumpEs env))
+ @ List.map FoundKind (ElabEnv.dumpCs env)
+ @ List.map FoundCon (ElabEnv.dumpEs env))
val query = List.last splitted
val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
in
diff --git a/src/lsp.sml b/src/lsp.sml
index e29589c2..c99a6f2e 100644
--- a/src/lsp.sml
+++ b/src/lsp.sml
@@ -257,10 +257,10 @@ fun elabFile (state: state) (fileName: string): ({ decls: Elab.decl list, envBef
end
end
-fun uniq (comp: 'b -> 'b -> bool) (bs: 'b list) =
+fun uniq (eq: 'b -> 'b -> bool) (bs: 'b list) =
case bs of
[] => []
- | (l as b :: bs') => b :: uniq comp (List.filter (comp b) bs')
+ | (l as b :: bs') => b :: uniq eq (List.filter (fn a => not (eq a b)) bs')
fun elabFileAndSendDiags (state: state) (toclient: LspSpec.toclient) (documentUri: LspSpec.documentUri): unit =
let
@@ -326,7 +326,7 @@ fun getStringAtCursor
=
let
val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full text), #line pos)
- val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":"
+ val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":", #"@"
, #" ", #"\n", #"#", #",", #"*", #"\"", #"|", #"&", #"$", #"^", #"+", #";"]
val lineUntilCursor = Substring.slice (line, 0, SOME (#character pos))
val beforeCursor = Substring.string (Substring.taker (fn c => not (List.exists (fn c' => c = c') chars)) lineUntilCursor)
@@ -369,8 +369,8 @@ fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.
let
val desc = case f of
GetInfo.FoundStr (x, (_, sgn)) => formatTypeBox (P.PD.string (prefix ^ x), P.PD.string "module")
- | GetInfo.FoundCon (x, kind) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_kind env kind)
- | GetInfo.FoundExp (x, con) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_con env con)
+ | GetInfo.FoundKind (x, kind) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_kind env kind)
+ | GetInfo.FoundCon (x, con) => formatTypeBox (P.PD.string (prefix ^ x), ElabPrint.p_con env con)
in
LspSpec.Success (SOME {contents = ppToString desc 50})
end
@@ -395,8 +395,8 @@ fun handleCompletion (state: state) (p: LspSpec.completionReq) =
val completions = List.map
(fn f => case f of
GetInfo.FoundStr (x, _) => {label = prefix ^ x, kind = LspSpec.Module, detail = ""}
- | GetInfo.FoundCon (x, k) => {label = prefix ^ x, kind = LspSpec.Constructor, detail = ppToString (ElabPrint.p_kind env k) 200}
- | GetInfo.FoundExp (x, c) => {label = prefix ^ x, kind = LspSpec.Value, detail = ppToString (ElabPrint.p_con env c) 200}
+ | GetInfo.FoundKind (x, k) => {label = prefix ^ x, kind = LspSpec.Constructor, detail = ppToString (ElabPrint.p_kind env k) 200}
+ | GetInfo.FoundCon (x, c) => {label = prefix ^ x, kind = LspSpec.Value, detail = ppToString (ElabPrint.p_con env c) 200}
)
foundItems
in