diff --git a/src/Commands.newt b/src/Commands.newt index c768cf9..bc4f0ff 100644 --- a/src/Commands.newt +++ b/src/Commands.newt @@ -16,7 +16,6 @@ import Data.SortedMap import Lib.Parser import Lib.Syntax import Lib.Parser.Impl -import Lib.Error -- For now we cheat and assume capitalized directories are a module component decomposeName : String → String × String @@ -235,7 +234,7 @@ introActions (Just $ Unsolved fc qn ctx vty User constraints) = pure $ map makeEdit cons ) $ \ err => do putStrLn "Got error in introActions:" - putStrLn $ showError "" err + putStrLn $ show err pure Nil where introDCon : QName × Int × Tm → List String diff --git a/src/LSP.newt b/src/LSP.newt index 47ef6b6..93bb7c8 100644 --- a/src/LSP.newt +++ b/src/LSP.newt @@ -3,6 +3,7 @@ module LSP import Prelude import Lib.Common import Lib.Eval +import Lib.Error import Lib.Types import Lib.TopContext import Lib.Tokenizer @@ -15,7 +16,7 @@ import Node import Commands import Lib.ProcessDecl import Lib.Prettier -import Lib.Error + import Lib.CompileJS import Lib.CompileScheme @@ -104,7 +105,7 @@ hoverInfo uri line col = unsafePerformIO $ do putStrLn $ "Nothing to see here" pure $ js_castBool True | Left err => do - putStrLn $ showError "" err + putStrLn $ show err pure $ jsonToJObject JsonNull modifyIORef state $ { topContext := top } let location = JsonObj $ ("uri", JsonStr fc.file) :: ("range", fcToRange fc) :: Nil @@ -124,7 +125,7 @@ codeActionInfo uri line col = unsafePerformIO $ do pure actions).runM st.topContext | Left err => do putStrLn "ACTIONS ERROR" - putStrLn $ showError "" err + putStrLn $ show err pure js_null modifyIORef state $ { topContext := top } pure $ jsonToJObject $ JsonArray $ map actionToJson actions @@ -161,12 +162,13 @@ codeActionInfo uri line col = unsafePerformIO $ do :: ("edit", (single "changes" $ single uri $ JsonArray $ map editToJson edits)) :: Nil -errorToDiag : Error -> Json -errorToDiag err = - JsonObj +errorToDiag : Error -> M Json +errorToDiag err = do + msg <- prettyErrorMsg err + pure $ JsonObj $ ("severity", JsonInt 1) :: ("range", fcToRange (getFC err)) - :: ("message", JsonStr (errorMsg err)) + :: ("message", JsonStr msg) :: ("source", JsonStr "newt") -- what is this key for? :: Nil -- These shouldn't escape @@ -242,14 +244,21 @@ checkFile fn = unsafePerformIO $ do -- pull out errors and infos top <- getTop - let errors = map (errorToDiag) top.currentMod.modErrors + errors <- traverse (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 + putStrLn $ show err + pure $ jsonToJObject $ JsonArray + [ JsonObj $ ("severity", JsonInt 1) + :: ("range", fcToRange (getFC err)) + :: ("message", JsonStr (errorMsg err)) + :: ("source", JsonStr "newt") -- what is this key for? + :: Nil + ] + -- Cache loaded modules modifyIORef state $ { topContext := top } pure $ jsonToJObject $ JsonArray json diff --git a/src/Lib/Derive.newt b/src/Lib/Derive.newt index b1a7421..a3417e7 100644 --- a/src/Lib/Derive.newt +++ b/src/Lib/Derive.newt @@ -5,7 +5,7 @@ import Lib.Common import Lib.Types import Lib.Syntax import Lib.TopContext -import Lib.Error + import Lib.Elab -- (lookupDCon) import Lib.Prettier diff --git a/src/Lib/Elab.newt b/src/Lib/Elab.newt index 30a7eac..03cc922 100644 --- a/src/Lib/Elab.newt +++ b/src/Lib/Elab.newt @@ -13,7 +13,6 @@ import Lib.Util import Lib.TopContext import Lib.Syntax import Lib.Types -import Lib.Error vprint : Context -> Val -> M String vprint ctx v = do @@ -28,9 +27,6 @@ collectDecl ((FunDef fc nm cl) :: rest@(FunDef _ nm' cl' :: xs)) = else (FunDef fc nm cl :: collectDecl rest) collectDecl (x :: xs) = x :: collectDecl xs --- TODO Move this, so we don't need to import all of Elab -rpprint : List String → Tm → String -rpprint names tm = render 90 $ pprint names tm showCtx : Context -> M String showCtx ctx = @@ -144,7 +140,7 @@ findMatches ctx ty ((name, type) :: xs) = do setMetaContext mc (_::_ name) <$> findMatches ctx ty xs) (\ err => do - debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{showError "" err}" + debug $ \ _ => "No match \{show ty} \{rpprint Nil type} \{show err}" setMetaContext mc findMatches ctx ty xs) @@ -166,7 +162,7 @@ contextMatches ctx ty = go (zip ctx.env ctx.types) tm <- quote ctx.lvl tm (_::_ (tm, vty)) <$> go xs) (\ err => do - debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{showError "" err}" + debug $ \ _ => "No match \{show ty} \{rpprint (names ctx) type} \{show err}" setMetaContext mc go xs) @@ -394,7 +390,7 @@ solve env m sp t = do -- Will this get is into trouble? Right ren <- tryError $ invert l sp | Left err => do - debug $ \ _ => "postpone constraint \{showError "" err}" + debug $ \ _ => "postpone constraint \{show err}" addConstraint env m sp t -- force unlet hack <- quote l t @@ -588,10 +584,7 @@ unifyCatch fc ctx ty' ty = do res <- catchError (unify ctx.env UNormal ty' ty) $ \err => do let names = map fst ctx.types debug $ \ _ => "fail \{show ty'} \{show ty}" - a <- quote ctx.lvl ty' - b <- quote ctx.lvl ty - let msg = "unification failure: \{errorMsg err}\n failed to unify \{rpprint names a}\n with \{rpprint names b}\n " - throwError (E fc msg) + throwError $ UnificationError fc names ty' ty err case res of MkResult Nil => pure MkUnit cs => do diff --git a/src/Lib/Error.newt b/src/Lib/Error.newt index fc3abf4..55e2d5d 100644 --- a/src/Lib/Error.newt +++ b/src/Lib/Error.newt @@ -1,30 +1,26 @@ module Lib.Error import Prelude +import Lib.Types +import Lib.Eval import Lib.Common --- I'll want to get Context / Val in some of these --- and a pretty printer in the monad -data Error - = E FC String - | ENotInScope FC String - | Postpone FC QName String +prettyErrorMsg : Error -> M String +prettyErrorMsg (E x str) = pure str +prettyErrorMsg (ENotInScope x nm) = pure "\{nm} not in scope" +prettyErrorMsg (Postpone x k str) = pure str +prettyErrorMsg (UnificationError fc names a b err) = do + let lvl = length' names + a <- quote lvl a + b <- quote lvl b + pure "unification failure: \{errorMsg err}\n failed to unify \{rpprint names a}\n with \{rpprint names b}\n " - -instance HasFC Error where - getFC (E x str) = x - getFC (ENotInScope x _) = x - getFC (Postpone x k str) = x - -errorMsg : Error -> String -errorMsg (E x str) = str -errorMsg (ENotInScope x nm) = "\{nm} not in scope" -errorMsg (Postpone x k str) = str - -showError : (src : String) -> Error -> String -showError src err = - let fc = getFC err - in "ERROR at \{show $ getFC err}: \{errorMsg err}\n" ++ go fc 0 (lines src) +-- Use prettyError when possible +showError : (src : String) -> Error -> M String +showError src err = do + let fc = getFC err + msg <- prettyErrorMsg err + pure $ "ERROR at \{show fc}: \{msg}\n" ++ go fc 0 (lines src) where go : FC → Int → List String → String go fc l Nil = "" @@ -35,3 +31,4 @@ showError src err = else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go fc (l + 1) xs else go fc (l + 1) xs + diff --git a/src/Lib/Eval.newt b/src/Lib/Eval.newt index f94a272..480ea7e 100644 --- a/src/Lib/Eval.newt +++ b/src/Lib/Eval.newt @@ -9,7 +9,7 @@ import Lib.TopContext import Data.IORef import Data.SnocList import Data.SortedMap -import Lib.Error + eval : Env -> Tm -> M Val @@ -329,7 +329,7 @@ zonkApp top l env t sp = do x <- zonk top l env t' pure x) (\err => do - debug $ \_ => "result err \{showError "" err}" + debug $ \_ => "result err \{show err}" pure $ appSpine t' sp) where -- lookup name and return Def if flagged inline diff --git a/src/Lib/Parser/Impl.newt b/src/Lib/Parser/Impl.newt index 28ac1df..76dfd23 100644 --- a/src/Lib/Parser/Impl.newt +++ b/src/Lib/Parser/Impl.newt @@ -7,7 +7,7 @@ import Data.String import Data.Int import Data.List1 import Data.SortedMap -import Lib.Error +import Lib.Types TokenList : U TokenList = List BTok diff --git a/src/Lib/ProcessDecl.newt b/src/Lib/ProcessDecl.newt index d8ff3e8..28e2df9 100644 --- a/src/Lib/ProcessDecl.newt +++ b/src/Lib/ProcessDecl.newt @@ -6,7 +6,7 @@ import Data.String import Lib.Common import Lib.Elab -import Lib.Error + import Lib.Parser import Lib.Syntax import Data.SortedMap diff --git a/src/Lib/ProcessModule.newt b/src/Lib/ProcessModule.newt index a25392f..a8f1035 100644 --- a/src/Lib/ProcessModule.newt +++ b/src/Lib/ProcessModule.newt @@ -146,7 +146,7 @@ processModule importFC repo stk modns = do top <- getTop -- print errors (for batch processing case) - for_ (reverse top.currentMod.modErrors) $ \ err => putStrLn $ showError src err + for_ (reverse top.currentMod.modErrors) $ showError src >=> putStrLn -- update modules with result, leave the rest of context in case this is top file top <- getTop diff --git a/src/Lib/Tokenizer.newt b/src/Lib/Tokenizer.newt index fa36748..fdfd990 100644 --- a/src/Lib/Tokenizer.newt +++ b/src/Lib/Tokenizer.newt @@ -12,7 +12,7 @@ import Lib.Token import Lib.Common import Data.String import Data.SnocList -import Lib.Error +import Lib.Types standalone : List Char standalone = unpack "()\\{}[],.@;" diff --git a/src/Lib/TopContext.newt b/src/Lib/TopContext.newt index 660ed51..c7e2af1 100644 --- a/src/Lib/TopContext.newt +++ b/src/Lib/TopContext.newt @@ -6,7 +6,7 @@ import Data.String import Prelude import Lib.Common import Lib.Types -import Lib.Error + -- TODO move the def in here (along with M) or merge this into types -- The Monad can be its own file if we pull all of the monad update functions there. diff --git a/src/Lib/Types.newt b/src/Lib/Types.newt index 19ded78..4f788df 100644 --- a/src/Lib/Types.newt +++ b/src/Lib/Types.newt @@ -3,7 +3,6 @@ module Lib.Types import Prelude import Lib.Common import Lib.Prettier -import Lib.Error import Data.IORef import Data.SnocList @@ -235,6 +234,33 @@ data MetaKind = Normal | User | AutoSolve | ErrorHole derive Show MetaKind derive Eq MetaKind +rpprint : List String → Tm → String +rpprint names tm = render 90 $ pprint names tm + +-- In types so we can have Val / Tm / Context +data Error + = E FC String + | ENotInScope FC String + | Postpone FC QName String + | UnificationError FC (List String) Val Val Error + +instance HasFC Error where + getFC (E x str) = x + getFC (UnificationError fc _ _ _ _) = fc + getFC (ENotInScope x _) = x + getFC (Postpone x k str) = x + +-- Non-pretty version, there is an in-monad prettyErrorMsg in Lib.Error +errorMsg : Error -> String +errorMsg (E x str) = str +errorMsg (ENotInScope x nm) = "\{nm} not in scope" +errorMsg (Postpone x k str) = str +errorMsg (UnificationError fc names a b err) = + "unification failure: \{errorMsg err}\n failed to unify \{show a}\n with \{show b}\n " + +instance Show Error where + show err = "ERROR at \{show $ getFC err}: \{errorMsg err}\n" + -- constrain meta applied to val to be a val data MConstraint = MkMc FC Env (SnocList Val) Val @@ -536,4 +562,3 @@ profile desc work = do end <- getTime putStrLn "PROF \{desc} \{show $ end - start} ms" pure res - diff --git a/src/Main.newt b/src/Main.newt index 66540da..48bfed7 100644 --- a/src/Main.newt +++ b/src/Main.newt @@ -8,6 +8,7 @@ import Lib.CompileJS import Lib.CompileScheme import Lib.Parser import Lib.Elab +import Lib.Error import Lib.Util import Lib.Parser.Impl import Lib.Prettier @@ -20,7 +21,6 @@ import Lib.Syntax import Lib.ReplParser import Node import Revision -import Lib.Error dirFileSource : String → FileSource dirFileSource base = MkFileSource base $ \fc fn => do @@ -177,10 +177,10 @@ runCommand DumpTop = do runString : String → M Unit runString line = do let (Right toks) = tokenise "" line - | Left err => putStrLn (showError line err) + | Left err => showError line err >>= putStrLn let (Right cmd) = parse "" parseCommand toks - | Left err => putStrLn (showError line err) - catchError (runCommand cmd) (\ err => putStrLn $ showError line err) + | Left err => showError line err >>= putStrLn + catchError (runCommand cmd) (showError line >=> putStrLn) runRepl : M Unit runRepl = do diff --git a/src/Prelude.newt b/src/Prelude.newt index 7ca0520..52e115e 100644 --- a/src/Prelude.newt +++ b/src/Prelude.newt @@ -102,7 +102,7 @@ class Monad (m : U → U) where bind : ∀ a b. m a → (a → m b) → m b pure : ∀ a. a → m a -infixl 1 _>>=_ _>>_ +infixl 1 _>>=_ _>>_ _>=>_ _>>=_ : ∀ m a b. {{Monad m}} → (m a) → (a → m b) → m b ma >>= amb = bind ma amb @@ -112,6 +112,9 @@ ma >> mb = bind ma (\ _ => mb) join : ∀ m a. {{Monad m}} → m (m a) → m a join mma = mma >>= id +_>=>_ : ∀ m a b c. {{Monad m}} → (a → m b) → (b → m c) → a → m c +(mab >=> mac) a = mab a >>= mac + -- Equality infixl 1 _≡_