Something went wrong. Try again.
Newt - a dependent typed programming language
This is a mirror of the main github repository. newt.cloakedarrow.com
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233module Lib.Errorimport Preludeimport Lib.Typesimport Lib.Evalimport Lib.CommonprettyErrorMsg : Error -> M StringprettyErrorMsg (E x str) = pure strprettyErrorMsg (ENotInScope x nm) = pure "\{nm} not in scope"prettyErrorMsg (Postpone x str) = pure strprettyErrorMsg (UnificationError fc names a b err) = do let lvl = length' names pure "unification failure: \{errorMsg err}\n failed to unify \{rpprint names a}\n with \{rpprint names b}\n "-- Use prettyError when possibleshowError : (src : String) -> Error -> M StringshowError 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 = "" go fc l (x :: xs) = if l == fcLine fc then let width = fc.bnds.endCol - fc.bnds.startCol in " \{x}\n \{padding (fcCol fc) ' '}\{padding width '^'}\n" else if fcLine fc - 3 < l then " " ++ x ++ "\n" ++ go fc (l + 1) xs else go fc (l + 1) xs