224 lines
7.6 KiB
Agda
224 lines
7.6 KiB
Agda
module LSP
|
||
|
||
import Prelude
|
||
import Lib.Common
|
||
import Lib.Eval
|
||
import Lib.Types
|
||
import Lib.TopContext
|
||
import Lib.Tokenizer
|
||
import Lib.Parser
|
||
import Lib.Parser.Impl
|
||
import Lib.ProcessModule
|
||
import Data.SortedMap
|
||
import Data.IORef
|
||
import Node
|
||
import Commands
|
||
import Lib.ProcessDecl
|
||
import Lib.Prettier
|
||
import Lib.Error
|
||
|
||
pfunc js_castArray : Array JSObject → JSObject := `x => x`
|
||
pfunc js_castInt : Int → JSObject := `x => x`
|
||
pfunc js_castBool : Bool → JSObject := `x => x`
|
||
pfunc js_castStr : String → JSObject := `x => x`
|
||
pfunc js_null : JSObject := `null`
|
||
pfunc js_castObj : Array (String × JSObject) → JSObject := `(data) => {
|
||
let rval = {}
|
||
for (let x of data) rval[x.h2] = x.h3
|
||
return rval
|
||
}`
|
||
|
||
-- need case split
|
||
jsonToJObject : Json → JSObject
|
||
jsonToJObject (JsonInt x) = js_castInt x
|
||
jsonToJObject (JsonNull) = js_null
|
||
jsonToJObject (JsonArray xs) = js_castArray $ listToArray $ map jsonToJObject xs
|
||
jsonToJObject (JsonBool x) = js_castBool x
|
||
jsonToJObject (JsonStr x) = js_castStr x
|
||
-- IMPERROR - if I leave off the `map` I get an error that is hard to sort out
|
||
jsonToJObject (JsonObj xs) = js_castObj $ listToArray $ map (mapSnd jsonToJObject) xs
|
||
|
||
record LSPState where
|
||
topContext : TopContext
|
||
baseDir : String
|
||
files : SortedMap String String
|
||
|
||
state : IORef LSPState
|
||
state = unsafePerformIO $ newIORef $ MkLSPState emptyTop "" emptyMap
|
||
|
||
resetState : String → IO Unit
|
||
resetState base = do
|
||
putStrLn "Reset base to \{base}"
|
||
writeIORef state $ MkLSPState emptyTop base emptyMap
|
||
|
||
lspFileSource : IO FileSource
|
||
lspFileSource = do
|
||
st <- readIORef state
|
||
pure $ MkFileSource st.baseDir $ \fc fn => do
|
||
let fn = st.baseDir ++ "/" ++ fn
|
||
let (Nothing) = lookupMap' fn st.files
|
||
| Just src => pure (fn,src)
|
||
let fn' = case split fn "file://" of
|
||
x :: fn :: _ => fn
|
||
_ => fn
|
||
(Right src) <- liftIO {M} $ readFile fn'
|
||
| Left err => throwError $ E fc "error reading \{fn}: \{show err}"
|
||
pure (fn,src)
|
||
|
||
updateFile : String → String → Unit
|
||
updateFile fn src = unsafePerformIO $ do
|
||
st <- readIORef state
|
||
modifyIORef state [ files $= updateMap fn src ]
|
||
let st = the LSPState $ [ files $= updateMap fn src ] st
|
||
let (base,modName) = decomposeName fn
|
||
Right (ctx,_) <- (invalidateModule modName).runM st.topContext
|
||
| _ => writeIORef state st
|
||
modifyIORef state [ topContext := ctx ]
|
||
|
||
|
||
fcToRange : FC → Json
|
||
fcToRange (MkFC uri (MkBounds sr sc er ec)) =
|
||
JsonObj $ ("start", mkPosition sr sc) :: ("end", mkPosition er (ec)) :: Nil
|
||
where
|
||
mkPosition : Int → Int → Json
|
||
mkPosition l c = JsonObj $ ("line", JsonInt l) :: ("character", JsonInt c) :: Nil
|
||
|
||
hoverInfo : String → Int → Int → JSObject
|
||
hoverInfo uri line col = unsafePerformIO $ do
|
||
let (base,modns) = decomposeName uri
|
||
putStrLn "Hover \{uri} base \{base} mod \{modns}"
|
||
st <- readIORef state
|
||
if (st.baseDir /= base)
|
||
then resetState base
|
||
else pure MkUnit
|
||
st <- readIORef state
|
||
repo <- lspFileSource
|
||
-- We're proactively running check if there is no module information, make sure we save it
|
||
Right (top, Just (msg, fc)) <- (getHoverInfo repo modns line col).runM st.topContext
|
||
| Right (top, _) => do
|
||
modifyIORef state $ [ topContext := top ]
|
||
putStrLn $ "Nothing to see here"
|
||
pure $ jsonToJObject JsonNull
|
||
| Left err => do
|
||
putStrLn $ showError "" err
|
||
pure $ jsonToJObject JsonNull
|
||
modifyIORef state $ [ topContext := top ]
|
||
let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil
|
||
pure $ jsonToJObject $ JsonObj $ ("info", JsonStr msg) :: ("location", location) :: Nil
|
||
|
||
codeActionInfo : String → Int → Int → JSObject
|
||
codeActionInfo uri line col = unsafePerformIO $ do
|
||
let (base,modns) = decomposeName uri
|
||
putStrLn "Action \{uri} base \{base} mod \{modns}"
|
||
st <- readIORef state
|
||
if (st.baseDir /= base) then resetState base else pure MkUnit
|
||
st <- readIORef state
|
||
repo <- lspFileSource
|
||
Right (top, actions) <- (do
|
||
actions <- getActions repo modns line col
|
||
putStrLn "\{show $ length' actions} actions"
|
||
pure actions).runM st.topContext
|
||
| Left err => do
|
||
putStrLn "ACTIONS ERROR"
|
||
putStrLn $ showError "" err
|
||
pure js_null
|
||
modifyIORef state $ [ topContext := top ]
|
||
pure $ jsonToJObject $ JsonArray $ map actionToJson actions
|
||
where
|
||
single : String → Json → Json
|
||
single k v = JsonObj $ (k,v) :: Nil
|
||
|
||
editToJson : FileEdit → Json
|
||
editToJson (MkEdit fc text) =
|
||
JsonObj
|
||
$ ("range", fcToRange fc)
|
||
:: ("newText", JsonStr text)
|
||
:: Nil
|
||
|
||
actionToJson : CodeAction → Json
|
||
actionToJson (CaseSplitAction edits) =
|
||
JsonObj
|
||
$ ("title", JsonStr "Case split")
|
||
:: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits))
|
||
:: Nil
|
||
actionToJson (Intro name edit) =
|
||
JsonObj
|
||
$ ("title", JsonStr "Intro \{name}")
|
||
:: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
|
||
:: Nil
|
||
actionToJson (ImportAction name edit) =
|
||
JsonObj
|
||
$ ("title", JsonStr "Import \{name}")
|
||
:: ("edit", (single "changes" $ single uri $ JsonArray $ editToJson edit :: Nil))
|
||
:: Nil
|
||
actionToJson (AddMissingAction edits) =
|
||
JsonObj
|
||
$ ("title", JsonStr "Add missing cases")
|
||
:: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits))
|
||
:: Nil
|
||
|
||
errorToDiag : Error -> Json
|
||
errorToDiag err =
|
||
JsonObj
|
||
$ ("severity", JsonInt 1)
|
||
:: ("range", fcToRange (getFC err))
|
||
:: ("message", JsonStr (errorMsg err))
|
||
:: ("source", JsonStr "newt") -- what is this key for?
|
||
:: Nil
|
||
-- These shouldn't escape
|
||
errorToDiag (Postpone fc qn msg) = errorToDiag $ E fc "Postpone \{show qn} \{msg}"
|
||
|
||
|
||
getInfos : M (List Json)
|
||
getInfos = do
|
||
top <- getTop
|
||
go Nil $ listValues $ top.currentMod.modMetaCtx.metas
|
||
where
|
||
go : List Json → List MetaEntry → M (List Json)
|
||
go acc Nil = pure acc
|
||
go acc (Unsolved fc k ctx ty User cons :: rest) = do
|
||
ty' <- quote ctx.lvl ty
|
||
let names = map fst ctx.types
|
||
let dispType = render 90 $ pprint names ty'
|
||
dispEnv <- dumpEnv ctx
|
||
let msg = "\{dispEnv}\n--------\n\{dispType}"
|
||
let diag = JsonObj
|
||
$ ("severity", JsonInt 3)
|
||
:: ("range", fcToRange fc)
|
||
:: ("message", JsonStr msg)
|
||
:: ("source", JsonStr "newt") -- what is this key for?
|
||
:: Nil
|
||
go (diag :: acc) rest
|
||
go acc (_ :: es) = go acc es
|
||
|
||
checkFile : String → JSObject
|
||
checkFile fn = unsafePerformIO $ do
|
||
let (base,modName) = decomposeName fn
|
||
|
||
putStrLn "Checking \{fn} base \{base} mod \{modName}"
|
||
st <- readIORef state
|
||
if (st.baseDir /= base)
|
||
then resetState base
|
||
else pure MkUnit
|
||
repo <- lspFileSource
|
||
(Right (top, json)) <- (do
|
||
putStrLn "processModule"
|
||
mod <- processModule emptyFC repo Nil modName
|
||
modifyTop [ currentMod := mod; ops := mod.modOps ]
|
||
|
||
-- pull out errors and infos
|
||
top <- getTop
|
||
let errors = map (errorToDiag) top.currentMod.modErrors
|
||
infos <- getInfos
|
||
pure $ infos ++ errors
|
||
).runM st.topContext
|
||
| Left err => do
|
||
putStrLn "**** Error without updating top:"
|
||
putStrLn $ showError "" err
|
||
pure $ jsonToJObject $ JsonArray $ errorToDiag err :: Nil
|
||
-- Cache loaded modules
|
||
modifyIORef state $ [ topContext := top ]
|
||
pure $ jsonToJObject $ JsonArray json
|
||
|
||
#export updateFile checkFile hoverInfo codeActionInfo
|