summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSimon Van Casteren <simon.van.casteren@gmail.com>2020-01-10 02:25:45 +0100
committerSimon Van Casteren <simon.van.casteren@gmail.com>2020-01-10 02:25:45 +0100
commitce6bae891c6d1e22e61a1fb54ce3ecd08ca31891 (patch)
treee6681735be997d9d6e2c34d6adb327638fcc2ee1
parent028f15cce127360f29afa41754aab3816718492f (diff)
Refactor to do all matching on strings, more precise and faster
-rw-r--r--src/elab_env.sig6
-rw-r--r--src/elab_env.sml28
-rw-r--r--src/getinfo.sig34
-rw-r--r--src/getinfo.sml511
-rw-r--r--src/lsp.sml229
5 files changed, 291 insertions, 517 deletions
diff --git a/src/elab_env.sig b/src/elab_env.sig
index fb95d68e..4f994221 100644
--- a/src/elab_env.sig
+++ b/src/elab_env.sig
@@ -61,7 +61,6 @@ 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
@@ -86,7 +85,6 @@ 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 matchEByPrefix: env -> string -> (string * Elab.con) list
val lookupE : env -> string -> Elab.con var
@@ -102,8 +100,10 @@ signature ELAB_ENV = sig
val lookupStrNamed : env -> int -> string * Elab.sgn
val lookupStr : env -> string -> (int * Elab.sgn) option
- val matchStrByPrefix: env -> string -> (string * (int * Elab.sgn)) list
+ val dumpCs: env -> (string * Elab.kind) list
+ val dumpEs: env -> (string * Elab.con) list
+ val dumpStrs: env -> (string * (int * Elab.sgn)) list
val edeclBinds : env -> Elab.edecl -> env
val declBinds : env -> Elab.decl -> env
diff --git a/src/elab_env.sml b/src/elab_env.sml
index f492bc94..5fa32cd2 100644
--- a/src/elab_env.sml
+++ b/src/elab_env.sml
@@ -404,14 +404,6 @@ 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
@@ -940,13 +932,6 @@ fun lookupENamed (env : env) n =
NONE => raise UnboundNamed n
| SOME x => x
-(* TODO Why does this work better than using #renameE? *)
-fun matchEByPrefix (env: env) (prefix: string): (string * con) list =
- List.mapPartial (fn (name, value) => if String.isPrefix prefix name
- then SOME (name, value)
- else NONE)
- (#relE env @ IM.listItems (#namedE env))
-
fun checkENamed (env : env) n =
Option.isSome (IM.find (#namedE env, n))
@@ -1000,8 +985,17 @@ fun lookupStrNamed (env : env) n =
| SOME x => x
fun lookupStr (env : env) x = SM.find (#renameStr env, x)
-fun matchStrByPrefix (env: env) prefix =
- List.filter (fn (name,_) => String.isPrefix prefix name) (SM.listItemsi (#renameStr env))
+
+fun dumpCs (env: env): (string * kind) list =
+ List.map (fn (name, value) => case value of
+ Rel' (_, x) => (name, x)
+ | Named' (_, x) => (name, x))
+ (SM.listItemsi (#renameC env))
+(* TODO try again with #renameE *)
+fun dumpEs (env: env): (string * con) list =
+ #relE env @ IM.listItems (#namedE env)
+fun dumpStrs (env: env) =
+ SM.listItemsi (#renameStr env)
fun sgiSeek (sgi, (sgns, strs, cons)) =
case sgi of
diff --git a/src/getinfo.sig b/src/getinfo.sig
index 50eee70a..663a9a81 100644
--- a/src/getinfo.sig
+++ b/src/getinfo.sig
@@ -27,28 +27,24 @@
signature GET_INFO = sig
- datatype item =
- Kind of Elab.kind
- | Con of Elab.con
- | Exp of Elab.exp
- | Sgn_item of Elab.sgn_item
- | Sgn of Elab.sgn
- | Str of Elab.str
- | Decl of Elab.decl
+ datatype foundInEnv = FoundStr of (string * Elab.sgn)
+ | FoundCon of (string * Elab.kind)
+ | FoundExp of (string * Elab.con)
- val getInfo:
+ val findStringInEnv:
ElabEnv.env ->
Elab.str' ->
string (* fileName *) ->
- { line: int , character: int} ->
- { smallest : { span : ErrorMsg.span
- , item : item
- , env : ElabEnv.env }
- , smallestgoodpart : { span : ErrorMsg.span
- , desc : Print.PD.pp_desc
- , env : ElabEnv.env
- , item : item
- } option
-}
+ {line: int, char: int} ->
+ string (* query *) ->
+ (ElabEnv.env * string (* prefix *) * foundInEnv option)
+
+ val matchStringInEnv:
+ ElabEnv.env ->
+ Elab.str' ->
+ string (* fileName *) ->
+ {line: int, char: int} ->
+ string (* query *) ->
+ (ElabEnv.env * string (* prefix *) * foundInEnv list)
end
diff --git a/src/getinfo.sml b/src/getinfo.sml
index 5a0fe752..f18d0638 100644
--- a/src/getinfo.sml
+++ b/src/getinfo.sml
@@ -30,21 +30,19 @@ structure GetInfo :> GET_INFO = struct
structure U = ElabUtilPos
structure E = ElabEnv
structure L = Elab
-structure P = Print
-fun isPosIn (file: string) (row: int) (col: int) (span: ErrorMsg.span) =
+fun isPosIn (file: string) (line: int) (char: int) (span: ErrorMsg.span) =
let
val start = #first span
val end_ = #last span
in
OS.Path.base file = OS.Path.base (#file span)
andalso
- (#line start < row orelse
- #line start = row andalso #char start <= col)
+ (#line start < line orelse
+ #line start = line andalso #char start <= char)
andalso
- (#line end_ > row orelse
- #line end_ = row andalso #char end_ >= col)
-
+ (#line end_ > line orelse
+ #line end_ = line andalso #char end_ >= char)
end
fun isSmallerThan (s1: ErrorMsg.span) (s2: ErrorMsg.span) =
@@ -63,8 +61,8 @@ datatype item =
| Str of L.str
| Decl of L.decl
-fun getSpan (f: item * E.env) =
- case #1 f of
+fun getSpan (f: item) =
+ case f of
Kind k => #2 k
| Con c => #2 c
| Exp e => #2 e
@@ -73,310 +71,215 @@ fun getSpan (f: item * E.env) =
| Str s => #2 s
| Decl d => #2 d
-(* Just use ElabPrint functions. *)
-(* These are better for compiler error messages, but it's better than nothing *)
-fun printLiterally {span = span, item = item, env = env} =
- P.box [ case item of
- Kind k => P.box [P.PD.string "KIND: ", ElabPrint.p_kind env k]
- | Con c => P.box [P.PD.string "CON: ", ElabPrint.p_con env c]
- | Exp e => P.box [P.PD.string "EXP: ", ElabPrint.p_exp env e]
- | Sgn_item si => P.box [P.PD.string "SGN_ITEM: ", ElabPrint.p_sgn_item env si]
- | Sgn s => P.box [P.PD.string "SGN: ", ElabPrint.p_sgn env s]
- | Str s => P.box [P.PD.string "STR: ", ElabPrint.p_str env s]
- | Decl d => P.box [P.PD.string "DECL: ", ElabPrint.p_decl env d]
- ]
-fun getInfo env str fileName {line = row, character = col} =
+fun findInStr (f: ElabEnv.env -> item (* curr *) -> item (* prev *) -> bool)
+ (init: item)
+ env str fileName {line = line, char = char}: {item: item, env: ElabEnv.env} =
let
val () = U.mliftConInCon := E.mliftConInCon
+ val {env: ElabEnv.env, found: Elab.decl option} =
+ (case str of
+ L.StrConst decls =>
+ List.foldl (fn (d, acc as {env, found}) =>
+ if #line (#last (#2 d)) < line
+ then {env = E.declBinds env d, found = found}
+ else
+ if #line (#first (#2 d)) <= line andalso line <= #line (#last (#2 d))
+ then {env = env, found = SOME d}
+ else {env = env, found = found})
+ {env = env, found = NONE} decls
+ | _ => { env = env, found = NONE })
+ val dummyResult = (init, env)
+ val result =
+ case found of
+ NONE => dummyResult
+ | SOME d =>
+ U.Decl.foldB
+ { kind = fn (env, i, acc as (prev, env')) => if f env (Kind i) prev then (Kind i, env) else acc,
+ con = fn (env, i, acc as (prev, env')) => if f env (Con i) prev then (Con i, env) else acc,
+ exp = fn (env, i, acc as (prev, env')) => if f env (Exp i) prev then (Exp i, env) else acc,
+ sgn_item = fn (env, i, acc as (prev, env')) => if f env (Sgn_item i) prev then (Sgn_item i, env) else acc,
+ sgn = fn (env, i, acc as (prev, env')) => if f env (Sgn i) prev then (Sgn i, env) else acc,
+ str = fn (env, i, acc as (prev, env')) => if f env (Str i) prev then (Str i, env) else acc,
+ decl = fn (env, i, acc as (prev, env')) => if f env (Decl i) prev then (Decl i, env) else acc,
+ bind = fn (env, binder) =>
+ case binder of
+ U.Decl.RelK x => E.pushKRel env x
+ | U.Decl.RelC (x, k) => E.pushCRel env x k
+ | U.Decl.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co
+ | U.Decl.RelE (x, c) => E.pushERel env x c
+ | U.Decl.NamedE (x, c) => #1 (E.pushENamed env x c)
+ | U.Decl.Str (x, n, sgn) => #1 (E.pushStrNamed env x sgn)
+ | U.Decl.Sgn (x, n, sgn) => #1 (E.pushSgnNamed env x sgn)
+ }
+ env dummyResult d
+ in
+ {item = #1 result, env = #2 result}
+ end
- (* Adding previous declarations in file to environment *)
- (* "open <mod>" statements are already translated during elaboration *)
- (* They get added to the env here "unprefixed" *)
- val env = (case str of
- L.StrConst decls =>
- List.foldl (fn (d, env) =>
- if #line (#first (#2 d)) <= row
- andalso #char (#first (#2 d)) <= col
- then E.declBinds env d
- else env) env decls
- | _ => env)
+fun findSmallestSpan env str fileName {line = line, char = char} =
+ let
+ fun fitsAndIsSmaller (env: ElabEnv.env) (curr: item) (prev: item) =
+ isPosIn fileName line char (getSpan curr) andalso isSmallerThan (getSpan curr) (getSpan prev)
+ val init = Str (str, { file = fileName
+ , first = { line = 0, char = 0}
+ , last = { line = Option.getOpt (Int.maxInt, 99999), char = 0} })
+ in
+ findInStr fitsAndIsSmaller init env str fileName {line = line, char = char}
+ end
- (* This isn't very precise since we use the span of the parent exp/decl/etc *)
- (* to find the "smallest part" *)
- fun printPat env (pat: L.pat) =
- if isPosIn fileName row col (#2 pat)
- then
- case #1 pat of
- L.PVar (str, c) => SOME (P.box [ P.PD.string str
- , P.PD.string " : "
- , ElabPrint.p_con env c])
- | L.PCon (_, _, _, SOME p) => printPat env p
- | L.PRecord fields => (case List.mapPartial (fn field => printPat env (#2 field)) fields of
- [] => NONE
- | first :: _ => SOME first)
- | _ => NONE
- else NONE
+fun findFirstExpAfter env str fileName {line = line, char = char} =
+ let
+ fun currIsAfterPosAndBeforePrev (env: ElabEnv.env) (curr: item) (prev: item) =
+ (* curr is an exp *)
+ (case curr of Exp _ => true | _ => false)
+ andalso
+ (* curr is after input pos *)
+ ( line < #line (#first (getSpan curr))
+ orelse ( line = #line (#first (getSpan curr))
+ andalso char < #char (#first (getSpan curr))))
+ andalso
+ (* curr is before prev *)
+ (#line (#first (getSpan curr)) < #line (#first (getSpan prev))
+ orelse
+ (#line (#first (getSpan curr)) = #line (#first (getSpan prev))
+ andalso #char (#first (getSpan curr)) < #char (#first (getSpan prev))))
+ val init = Exp (Elab.EPrim (Prim.Int 0),
+ { file = fileName
+ , first = { line = Option.getOpt (Int.maxInt, 99999), char = Option.getOpt (Int.maxInt, 99999)}
+ , last = { line = Option.getOpt (Int.maxInt, 99999), char = Option.getOpt (Int.maxInt, 99999)} })
+ in
+ findInStr currIsAfterPosAndBeforePrev init env str fileName {line = line, char = char}
+ end
- fun isXmlTag env c =
- case c of
- L.CApp
- ((L.CApp
- ((L.CApp
- (( L.CApp
- (( L.CApp
- ((L.CNamed n, _) , _)
- , _)
- , _)
- , _)
- , _)
- , _)
- , _)
- , _)
- , _) =>
- (case E.lookupCNamed env n of
- ("tag", _, _) => true
- | _ => false)
- | _ => false
- fun formatTypeBox (a: P.PD.pp_desc, b: P.PD.pp_desc) =
- P.PD.hvBox (P.PD.PPS.Rel 0, [a,
- P.PD.string ": ",
- P.PD.break {nsp = 0, offset = 2},
- b])
-
- (* TODO We lose some really useful information, like eg. inferred parameters, *)
- (* which we do have in the actual items (L.Decl, L.Exp, etc) *)
- (* but not when we do a lookup into the Env *)
- (* TODO Rename? *)
- fun printGoodPart env f span =
- (case f of
- Exp (L.EPrim p, _) =>
- let
- val rendered = formatTypeBox ( Prim.p_t p
- , P.PD.string (case p of
- Prim.Int _ => "int"
- | Prim.Float _ => "float"
- | Prim.String _ => "string"
- | Prim.Char _ => "char"))
- in
- case p of
- Prim.String (_, str) =>
- if Substring.foldl (fn (c, acc) => acc andalso c = #" ") true (Substring.full str)
- then NONE
- else SOME rendered
- | _ => SOME (rendered)
- end
- | Exp (L.ERel n, _) =>
- SOME ((let val found = E.lookupERel env n
- in
- formatTypeBox ( P.PD.string (#1 found)
- , ElabPrint.p_con env (#2 found))
- end)
- handle E.UnboundRel _ => P.PD.string ("UNBOUND_REL" ^ Int.toString n))
- | Exp (L.ENamed n, span) =>
- ((let
- val found = E.lookupENamed env n
- val rendered = formatTypeBox ( P.PD.string (#1 found)
- , ElabPrint.p_con env (#2 found))
- (* val () = if #1 found = "body" *)
- (* then Print.eprint (ElabPrint.p_con env (#2 found)) *)
- (* else () *)
- in
- (* case #2 found of *)
- (* (L.TFun ((L.CUnit, _), (c, _)), _) => *)
- (* (if isXmlTag env c *)
- (* then SOME (P.box [ P.PD.string "<" *)
- (* , P.PD.string ( #1 found) *)
- (* , P.PD.string ">" *)
- (* ]) *)
- (* else SOME rendered) *)
- (* | _ => *) SOME rendered
- end)
- handle E.UnboundNamed _ => SOME (P.PD.string ("UNBOUND_NAMED" ^ Int.toString n)))
- | Exp (L.EAbs (varName, domain, _, _), _) =>
- if isPosIn fileName row col (#2 domain)
- then
- SOME (formatTypeBox ( P.PD.string varName
- , ElabPrint.p_con env domain)
- )
- else NONE
- | Exp (L.EField (e, c, {field, ...}), loc) =>
- SOME (formatTypeBox ( P.box [ElabPrint.p_exp env e,
- P.PD.string ".",
- ElabPrint.p_con env c]
- , ElabPrint.p_con env field))
- | Exp (L.EModProj ( m1 (* number (= "name") of top level module *)
- , ms (* names of submodules - possibly none *)
- , x (* identifier *)), loc) =>
- (let
- val (m1name, m1sgn) = E.lookupStrNamed env m1
- val (str, sgn) = foldl (fn (m, (str, sgn)) =>
- case E.projectStr env {sgn = sgn, str = str, field = m} of
- NONE => raise Fail ("Couldn't find Structure: " ^ m)
- | SOME sgn => ((L.StrProj (str, m), loc), sgn))
- ((L.StrVar m1, loc), m1sgn)
- ms
- val t = case E.projectVal env {sgn = sgn, str = str, field = x} of
- NONE => raise Fail ("Couldn't find identifier: " ^ x)
- | SOME t => t
- in
- case (m1name, x) of
- (* Stripping these because XML desugaring adds these with small spans and crowd out the stuff you want to see *)
- ("Basis", "cdata") => NONE
- | ("Top", "txt") => NONE
- | ("Basis", "join") => NONE
- | ("Basis", "bind") => NONE
- | ("Basis", "sql_subset") => NONE
- | ("Basis", "sql_subset_all") => NONE
- | ("Basis", "sql_query") => NONE
- | ("Basis", "sql_query1") => NONE
- | ("Basis", "sql_eq") => NONE
- | ("Basis", "sql_inner_join") => NONE
- (* | ("Basis", "sql_field") => NONE *)
- | ("Basis", "sql_binary") => NONE
- | _ =>
- SOME (formatTypeBox ( P.p_list_sep (P.PD.string ".") P.PD.string (m1name :: ms @ [x])
- , ElabPrint.p_con env t))
- end
- handle E.UnboundNamed _ => SOME (P.PD.string ("Module not found: " ^ Int.toString m1)))
- | Exp (L.ELet (edecls, _, _), _) =>
- let
- val found = List.mapPartial
- (fn (edecl, loc) =>
- if isPosIn fileName row col loc
- then
- case edecl of
- L.EDVal (pat, _, _) => printPat env pat
- | L.EDValRec ((x, c, _) :: _) =>
- SOME (formatTypeBox ( P.PD.string x
- , ElabPrint.p_con env c))
- | _ => NONE
- else NONE)
- edecls
- in
- if List.length found > 0
- then SOME (List.hd found)
- else NONE
- end
- | Exp (L.ECase (_, pats, _), _) =>
- (case List.find (fn ((pat', loc), exp) => isPosIn fileName row col loc) pats of
- NONE => NONE
- | SOME (pat, _) => printPat env pat)
- | Exp e => NONE
- | Kind k => NONE
- | Con c => NONE
- | Sgn_item si => NONE
- | Sgn s => NONE
- | Str s => NONE
- | Decl (L.DVal (x, _, con, _), _) =>
- SOME (formatTypeBox ( P.PD.string x
- , ElabPrint.p_con env con ))
- | Decl (L.DValRec decls, _) =>
- (* valrecs don't have nice spans per declaration so we find the *)
- (* declaration for which the con starts closest *)
- let
- val res =
- List.foldl (fn (decl, accO) =>
- let
- val distanceFromRow = Int.abs (#line (#first (#2 (#3 decl))) - row)
- val accDistanceFromRow = case accO of
- NONE => Option.getOpt (Int.maxInt, 99999)
- | SOME acc => Int.abs (#line (#first (#2 (#3 acc))) - row)
- in
- if distanceFromRow < accDistanceFromRow andalso distanceFromRow <= 1
- then SOME decl
- else accO
- end)
- NONE
- decls
- in
- case res of
- NONE => NONE
- | SOME (x, _, con, _) =>
- SOME (formatTypeBox ( P.PD.string x
- , ElabPrint.p_con env con))
- end
- | Decl d => NONE
- )
+datatype foundInEnv = FoundStr of (string * Elab.sgn)
+ | FoundCon of (string * Elab.kind)
+ | FoundExp of (string * Elab.con)
- fun add (env: ElabEnv.env) (item: item) (span: ErrorMsg.span) (acc: { smallest : { span : ErrorMsg.span
- , item : item
- , env : ElabEnv.env }
- , smallestgoodpart : { span : ErrorMsg.span
- , desc : P.PD.pp_desc
- , env : ElabEnv.env
- , item : item
- } option
- }
- ) =
- if not (isPosIn fileName row col span)
- then
- acc
- else
- let
- val smallest =
- if isSmallerThan span (#span (#smallest acc))
- then {span = span, item = item, env = env}
- else #smallest acc
- val smallestgoodpart =
- case #smallestgoodpart acc of
- NONE =>
- (case printGoodPart env item span of
- NONE => NONE
- | SOME desc => SOME {desc = desc, span = span, env = env, item = item})
- | SOME (prev as {desc = desc', span = span', env = env', item = item'}) =>
- if
- isSmallerThan span span'
- then
- (case printGoodPart env item span of
- NONE => SOME prev
- | SOME desc => SOME {desc = desc, span = span, env = env, item = item})
- else SOME prev
- in
- {smallest = smallest, smallestgoodpart = smallestgoodpart}
- end
+fun getNameOfFoundInEnv (f: foundInEnv) =
+ case f of
+ FoundStr (x, _) => x
+ | FoundCon (x, _) => x
+ | FoundExp (x, _) => x
- (* Look for item at input position *)
- (* We're looking for two things simultaneously: *)
- (* 1. The "smallest" part, ie. the one of which the source span is the smallest *)
- (* 2. The "smallestgoodpart" part, ie. the one of which the source span is the smallest AND has a special case in printGoodPart *)
- (* If we end up with a smallestgoodpart, we'll show that one since that one is probably more useful *)
- (* TODO source spans of XML and SQL sources are weird and you end *)
- (* up with eg: a span from eg 1-5 and another from 2-6, makes no sense? *)
- (* That's one of the reasons why we're searching for the two things mentioned above *)
- val result =
- U.Decl.foldB
- { kind = fn (env, (k, span), acc) => add env (Kind (k, span)) span acc,
- con = fn (env, (k, span), acc) => add env (Con (k, span)) span acc,
- exp = fn (env, (k, span), acc) => add env (Exp (k, span)) span acc,
- sgn_item = fn (env, (k, span), acc) => add env (Sgn_item (k, span)) span acc,
- sgn = fn (env, (k, span), acc) => add env (Sgn (k, span)) span acc,
- str = fn (env, (k, span), acc) => add env (Str (k, span)) span acc,
- decl = fn (env, (k, span), acc) => add env (Decl (k, span)) span acc,
- bind = fn (env, binder) =>
- case binder of
- U.Decl.RelK x => E.pushKRel env x
- | U.Decl.RelC (x, k) => E.pushCRel env x k
- | U.Decl.NamedC (x, n, k, co) => E.pushCNamedAs env x n k co
- | U.Decl.RelE (x, c) => E.pushERel env x c
- | U.Decl.NamedE (x, c) => #1 (E.pushENamed env x c)
- | U.Decl.Str (x, n, sgn) => #1 (E.pushStrNamed env x sgn)
- | U.Decl.Sgn (x, n, sgn) => #1 (E.pushSgnNamed env x sgn)
- }
- env
- { smallestgoodpart = NONE
- , smallest = { item = Str (str, { file = fileName
- , first = { line = 0, char = 0}
- , last = { line = Option.getOpt (Int.maxInt, 99999), char = 0} })
- , span = { file = fileName
- , first = { line = 0, char = 0}
- , last = { line = Option.getOpt (Int.maxInt, 99999), char = 0} }
- , env = env }
- }
- ( L.DStr (Compiler.moduleOf "fileName", 0, (L.SgnError, ErrorMsg.dummySpan), (str, {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos}))
- , {file = fileName, first = ErrorMsg.dummyPos, last = ErrorMsg.dummyPos})
+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.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)
+ | (Elab.SgiDatatypeImp (x, i, _, _, _, _, cs), loc) =>
+ FoundExp (x, (Elab.CNamed i, loc))
+ :: List.map (fn (x, i, _) => FoundExp (x, (Elab.CRel i, loc))) cs
+ | (Elab.SgiStr (_, name, _, sgn), _) =>
+ [FoundStr (name, sgn)]
+ | (Elab.SgiSgn (name, _, sgn), _) =>
+ [FoundStr (name, sgn)]
+ | _ => []
+ in
+ List.concat (List.map mapF items)
+ end
+
+fun resolvePrefixes
+ (env: ElabEnv.env)
+ (prefixes: string list)
+ (items : foundInEnv list)
+ : foundInEnv list
+ =
+ case prefixes of
+ [] => items
+ | first :: rest =>
+ (case List.find (fn item => getNameOfFoundInEnv item = first) items of
+ NONE => []
+ | SOME (FoundStr (name, sgn)) => (case ElabEnv.hnormSgn env sgn of
+ (Elab.SgnConst sgis, _) => resolvePrefixes env rest (filterSgiItems sgis)
+ | _ => [])
+ | SOME (FoundExp (name, c)) =>
+ let
+ val fields = case ElabOps.reduceCon env c of
+ (Elab.TRecord (Elab.CRecord (_, fields), l2_), l1_) =>
+ fields
+ | ( ( Elab.CApp
+ ( ( (Elab.CApp
+ ( ( Elab.CModProj (_, _, "sql_table") , l4_)
+ , ( Elab.CRecord (_, fields) , l3_)))
+ , l2_)
+ , _))
+ , l1_) => fields
+ | _ => []
+ val items =
+ List.mapPartial (fn (c1, c2) => case c1 of
+ (Elab.CName fieldName, _) => SOME (FoundExp (fieldName, c2))
+ | _ => NONE) fields
+ in
+ resolvePrefixes env rest items
+ end
+ | SOME (FoundCon (_, _)) => [])
+
+
+fun findStringInEnv' (env: ElabEnv.env) (preferCon: bool) (str: string): (string (* prefix *) * foundInEnv option) =
+ let
+ 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))
+ val query = List.last splitted
+ val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
+ in
+ (prefix, List.find (fn i => getNameOfFoundInEnv i = query) afterResolve)
+ end
+
+fun matchStringInEnv' (env: ElabEnv.env) (str: string): (string (* prefix *) * foundInEnv list) =
+ let
+ 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))
+ val query = List.last splitted
+ val prefix = String.extract (str, 0, SOME (String.size str - String.size query))
+ in
+ (prefix, List.filter (fn i => String.isPrefix query (getNameOfFoundInEnv i)) afterResolve)
+ end
+
+fun getDesc item =
+ case item of
+ Kind (_, s) => "Kind " ^ ErrorMsg.spanToString s
+ | Con (_, s) => "Con " ^ ErrorMsg.spanToString s
+ | Exp (_, s) => "Exp " ^ ErrorMsg.spanToString s
+ | Sgn_item (_, s) => "Sgn_item " ^ ErrorMsg.spanToString s
+ | Sgn (_, s) => "Sgn " ^ ErrorMsg.spanToString s
+ | Str (_, s) => "Str " ^ ErrorMsg.spanToString s
+ | Decl (_, s) => "Decl " ^ ErrorMsg.spanToString s
+
+fun matchStringInEnv env str fileName pos query: (ElabEnv.env * string (* prefix *) * foundInEnv list) =
+ let
+ val {item = _, env} = findSmallestSpan env str fileName pos
+ val (prefix, matches) = matchStringInEnv' env query
+ in
+ (env, prefix, matches)
+ end
+
+fun findStringInEnv env str fileName pos (query: string): (ElabEnv.env * string (* prefix *) * foundInEnv option) =
+ let
+ val {item, env} = findSmallestSpan env str fileName pos
+ val env = case item of
+ Exp (L.ECase _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp (L.ELet _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp (L.EAbs _, _) => #env (findFirstExpAfter env str fileName pos)
+ | Exp e => env
+ | Con _ => #env (findFirstExpAfter env str fileName pos)
+ | _ => #env (findFirstExpAfter env str fileName pos)
+ val preferCon = case item of Con _ => true
+ | _ => false
+ val (prefix, found) = findStringInEnv' env preferCon query
in
- result
+ (env, prefix, found)
end
end
diff --git a/src/lsp.sml b/src/lsp.sml
index 856b7ab8..e29589c2 100644
--- a/src/lsp.sml
+++ b/src/lsp.sml
@@ -1,7 +1,8 @@
-structure C = Compiler
-
structure Lsp :> LSP = struct
+structure C = Compiler
+structure P = Print
+
val debug = LspSpec.debug
structure SK = struct
@@ -317,6 +318,35 @@ fun ppToString (pp: Print.PD.pp_desc) (width: int): string =
res
end
+fun getStringAtCursor
+ (stopAtCursor: bool)
+ (text: string)
+ (pos: LspSpec.position)
+ : string
+ =
+ let
+ val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full text), #line pos)
+ 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)
+ val afterCursor = if stopAtCursor
+ then ""
+ else let
+ val lineAfterCursor = Substring.slice (line, #character pos, NONE)
+ in
+ Substring.string (Substring.takel (fn c => not (List.exists (fn c' => c = c') (#"." :: chars))) lineAfterCursor)
+ end
+ in
+ beforeCursor ^ afterCursor
+ end
+
+fun formatTypeBox (a: P.PD.pp_desc, b: P.PD.pp_desc) =
+ P.PD.hvBox (P.PD.PPS.Rel 0, [a,
+ P.PD.string ": ",
+ P.PD.break {nsp = 0, offset = 2},
+ b])
+
fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.result =
let
val fileName = #path (#uri (#textDocument p))
@@ -326,177 +356,27 @@ fun handleHover (state: state) (p: LspSpec.hoverReq): LspSpec.hoverResp LspSpec.
NONE => LspSpec.Success NONE
| SOME s =>
let
+ val searchString = getStringAtCursor false (#text s) (#position p)
val env = #envBeforeThisModule s
val decls = #decls s
val loc = #position p
- val result = GetInfo.getInfo env (Elab.StrConst decls) fileName { line = #line loc + 1
- , character = #character loc + 1}
+ val (env, prefix, found) = GetInfo.findStringInEnv env (Elab.StrConst decls) fileName { line = #line loc + 1
+ , char = #character loc + 1} searchString
in
- case #smallestgoodpart result of
+ case found of
NONE => LspSpec.Success NONE
- | SOME {desc = desc, ...} =>
- LspSpec.Success (SOME {contents = ppToString desc 50})
+ | SOME f =>
+ 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)
+ in
+ LspSpec.Success (SOME {contents = ppToString desc 50})
+ end
end
end
-fun getCompletionsFromFields (env: ElabEnv.env) (prefix: string) (searchStr: string) (fields: (Elab.con * Elab.con) list): LspSpec.completionItem list =
- let
- fun mapF (c1, c2) =
- case c1 of
- (Elab.CName fieldName, _) =>
- if String.isPrefix searchStr fieldName
- then SOME { label = prefix ^ fieldName
- , kind = LspSpec.Field
- , detail = ppToString (ElabPrint.p_con env c2) 200
- }
- else NONE
- | _ => NONE
- in
- List.mapPartial mapF fields
- end
-
-fun getCompletionsFromSignatureItems (env: ElabEnv.env) (prefix: string) (searchStr: string) (items: Elab.sgn_item list): LspSpec.completionItem list =
- let
- fun mapF item =
- case item of
- (Elab.SgiVal (name, _, con), _) =>
- if String.isPrefix searchStr name
- then [{ label = prefix ^ name
- , kind = LspSpec.Value
- , detail = ppToString (ElabPrint.p_con env con) 200
- }]
- else []
- | (Elab.SgiCon (name, _, _, con), _) =>
- if String.isPrefix searchStr name
- then [{ label = prefix ^ name
- , kind = LspSpec.Value
- , detail = ppToString (ElabPrint.p_con env con) 200
- }]
- else []
- | (Elab.SgiDatatype cs, _) =>
- (List.concat
- (List.map (fn (constr as (dtName, n, xs, constrs)) =>
- (* Copied from elab_print *)
- let
- val k = (Elab.KType, ErrorMsg.dummySpan)
- val env = ElabEnv.pushCNamedAs env dtName n k NONE
- val env = List.foldl (fn (x, env) => ElabEnv.pushCRel env x k) env xs
- val typeVarsString = List.foldl (fn (x, acc) => acc ^ " " ^ x) "" xs
- in
- List.mapPartial (fn (constrName, _, conO) =>
- if String.isPrefix searchStr constrName
- then SOME { label = prefix ^ constrName
- , kind = LspSpec.Function
- , detail = case conO of
- NONE => dtName ^ typeVarsString
- | SOME con => ppToString (ElabPrint.p_con env con) 200 ^ " -> " ^ dtName ^ typeVarsString
- }
- else NONE) constrs
- end)
- cs))
- | (Elab.SgiDatatypeImp _, _) =>
- (* TODO ??? no idea what this is *)
- []
- | (Elab.SgiStr (_, name, _, _), _) =>
- if String.isPrefix searchStr name
- then [{ label = prefix ^ name
- , kind = LspSpec.Module
- , detail = ""
- }]
- else []
- | (Elab.SgiClass (name, _, _, con), _) =>
- if String.isPrefix searchStr name
- then [{ label = prefix ^ name
- , kind = LspSpec.Class
- , detail = ppToString (ElabPrint.p_con env con) 200
- }]
- else []
- | _ => []
- in
- 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)
- in
- case splitted of
- (_ :: []) =>
- if str = ""
- then []
- 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) 200
- }) 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) 200
- }) matchingCons
- in
- expressionCompletions @ structureCompletions @ conCompletions
- end
- | (r :: str :: []) =>
- if Char.isUpper (Substring.sub (r, 0))
- then
- (* Completing STRUCTURE *)
- let
- (* 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
- (case List.map (fn (name, (i, sgn)) => (name, ElabEnv.hnormSgn env sgn)) filteredStrs of
- [] => []
- | (name, (Elab.SgnConst sgis, _)) :: _ =>
- getCompletionsFromSignatureItems env (name ^ ".") (Substring.string str) sgis
- | _ => [])
- end
- else
- (* Completing RECORD *)
- (* TODO TOCHECK is it correct to first try RelE and then NamedE? *)
- let
- (* 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
- val reduced = List.map (fn (name, c) =>
- (name, ElabOps.reduceCon env c)
- handle ex => (name, (Elab.CUnit, ErrorMsg.dummySpan)))
- filteredEs
- in
- case reduced of
- [] => []
- | (name, (Elab.TRecord (Elab.CRecord (_, fields), l2_), l1_)) :: _ =>
- getCompletionsFromFields env (name ^ ".") (Substring.string str) fields
- | (name,
- ( ( Elab.CApp
- ( ( (Elab.CApp
- ( ( Elab.CModProj (_, _, "sql_table")
- , l4_)
- , ( Elab.CRecord (_, fields)
- , l3_)))
- , l2_)
- , _))
- , l1_)) :: _ =>
- getCompletionsFromFields env (name ^ ".") (Substring.string str) fields
- | _ => []
- end
- | _ =>
- (* TODO NOTIMPLEMENTED submodules / nested records *)
- []
- end
-
(* 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
@@ -508,19 +388,20 @@ fun handleCompletion (state: state) (p: LspSpec.completionReq) =
| SOME s =>
let
val pos = #position p
- val line = List.nth (Substring.fields (fn c => c = #"\n") (Substring.full (#text s)), #line pos)
- val chars = [ (* #".", *) #"(", #")", #"{", #"}", #"[", #"]", #"<", #">", #"-", #"=", #":"
- , #" ", #"\n", #"#", #",", #"*", #"\"", #"|", #"&", #"$", #"^", #"+", #";"]
- val lineUntilPos = Substring.slice (line, 0, SOME (#character pos))
- val searchStr = Substring.string (Substring.taker (fn c => not (List.exists (fn c' => c = c') chars)) lineUntilPos)
+ val searchStr = getStringAtCursor true (#text s) pos
val env = #envBeforeThisModule s
val decls = #decls s
- val getInfoRes = GetInfo.getInfo env (Elab.StrConst decls) fileName { line = #line pos + 1
- , character = #character pos + 1}
- val envOfSmallest = #env (#smallest getInfoRes)
+ val (env, prefix, foundItems) = GetInfo.matchStringInEnv env (Elab.StrConst decls) fileName { line = #line pos + 1, char = #character pos + 1} searchStr
+ 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}
+ )
+ foundItems
in
LspSpec.Success { isIncomplete = false
- , items = findMatchingStringInEnv envOfSmallest searchStr}
+ , items = completions }
end
end