~jojo/Carth

69f159f135a35769afb1389bbe48ba28b1fafe65 — JoJo 1 year, 10 months ago 8495cf0
Simplify error-region parsing in TypeErr using tokenTree everywhere
3 files changed, 48 insertions(+), 72 deletions(-)

M src/Parse.hs
M src/SrcPos.hs
M src/TypeErr.hs
M src/Parse.hs => src/Parse.hs +17 -17
@@ 12,18 12,8 @@ module Parse
    , Source
    , parse
    , parse'
    , parseTokenTreeOrRest
    , toplevels
    , reserveds
    , ns_scheme
    , ns_pat
    , ns_small'
    , eConstructor
    , ns_expr
    , ns_big
    , ns_parens
    , def
    , getSrcPos
    , ns_tokenTree
    )
where



@@ 110,12 100,22 @@ parseModule filepath dir m visiteds nexts = do
parse' :: Parser a -> FilePath -> Source -> Either String a
parse' p name src = first errorBundlePretty (Mega.parse p name src)

-- | For use in TypeErr to get the length of the tokentree to draw a squiggly
--   line under it.
ns_tokenTree :: Parser ()
ns_tokenTree = choice
    [str $> (), num $> (), ident $> (), ns_parens (many tokenTree) $> ()]
    where tokenTree = andSkipSpaceAfter ns_tokenTree
-- | For use in module TypeErr to get the length of the tokentree to draw a
--   squiggly line under it.
parseTokenTreeOrRest :: Source -> Either String String
parseTokenTreeOrRest = parse' tokenTreeOrRest ""
  where
    tokenTreeOrRest =
        fmap fst (Mega.match (ns_tokenTree <|> (restOfInput $> ())))
    ns_tokenTree =
        choice
            [ str $> ()
            , num $> ()
            , ident $> ()
            , ns_parens (many tokenTree) $> ()
            ]
    tokenTree = andSkipSpaceAfter ns_tokenTree
    restOfInput = many Mega.anySingle

toplevels :: Parser ([Import], [Def], [TypeDef], [Extern])
toplevels = do

M src/SrcPos.hs => src/SrcPos.hs +0 -1
@@ 17,7 17,6 @@ newtype SrcPos = SrcPos SourcePos

data WithPos a = WithPos SrcPos a


class HasPos a where
    getPos :: a -> SrcPos


M src/TypeErr.hs => src/TypeErr.hs +31 -54
@@ 2,32 2,29 @@

module TypeErr (TypeErr(..), printErr) where

import qualified Text.Megaparsec as Mega
import Text.Megaparsec.Pos
import Data.Functor
import Control.Applicative
import Text.Megaparsec (SourcePos(..), unPos)

import Misc
import SrcPos
import Ast
import PrettyAst ()
import qualified Parse
import Parse


data TypeErr
    = StartNotDefined
    | InvalidUserTypeSig SrcPos Scheme Scheme
    | CtorArityMismatch SrcPos (Id Big) Int Int
    | CtorArityMismatch SrcPos (Id 'Big) Int Int
    | ConflictingPatVarDefs SrcPos String
    | UndefCtor SrcPos String
    | UndefVar SrcPos String
    | InfType SrcPos Type Type TVar Type
    | UnificationFailed SrcPos Type Type Type Type
    | ConflictingTypeDef (Id Big)
    | ConflictingCtorDef (Id Big)
    | ConflictingTypeDef (Id 'Big)
    | ConflictingCtorDef (Id 'Big)
    | RedundantCase SrcPos
    | InexhaustivePats SrcPos String
    | ExternNotMonomorphic (Id Small) TVar
    | ExternNotMonomorphic (Id 'Small) TVar
    | FoundHole SrcPos
    | RecTypeDef String SrcPos
    | UndefType SrcPos String


@@ 44,95 41,74 @@ printErr :: TypeErr -> IO ()
printErr = \case
    StartNotDefined -> putStrLn "Error: start not defined"
    InvalidUserTypeSig p s1 s2 ->
        posd p scheme
        posd p
            $ ("Invalid user type signature " ++ pretty s1)
            ++ (", expected " ++ pretty s2)
    CtorArityMismatch p c arity nArgs ->
        posd p pat
        posd p
            $ ("Arity mismatch for constructor `" ++ pretty c)
            ++ ("` in pattern.\nExpected " ++ show arity)
            ++ (", found " ++ show nArgs)
    ConflictingPatVarDefs p v ->
        posd p var
        posd p
            $ "Conflicting definitions for variable `"
            ++ v
            ++ "` in pattern."
    UndefCtor p c ->
        posd p eConstructor $ "Undefined constructor `" ++ c ++ "`"
    UndefVar p v -> posd p var $ "Undefined variable `" ++ v ++ "`"
    UndefCtor p c -> posd p $ "Undefined constructor `" ++ c ++ "`"
    UndefVar p v -> posd p $ "Undefined variable `" ++ v ++ "`"
    InfType p t1 t2 a t ->
        posd p defOrExpr
        posd p
            $ "Infinite type: "
            ++ (pretty a ++ " ~ " ++ pretty t)
            ++ ("\nExpected type: " ++ pretty t1)
            ++ ("\nFound type: " ++ pretty t2)
    UnificationFailed p t1 t2 t'1 t'2 ->
        posd p defOrExpr
        posd p
            $ ("Couldn't match type " ++ pretty t'2 ++ " with " ++ pretty t'1)
            ++ (".\nExpected type: " ++ pretty t1)
            ++ (".\nFound type: " ++ pretty t2 ++ ".")
    ConflictingTypeDef (Id (WithPos p x)) ->
        posd p big $ "Conflicting definitions for type `" ++ x ++ "`."
        posd p $ "Conflicting definitions for type `" ++ x ++ "`."
    ConflictingCtorDef (Id (WithPos p x)) ->
        posd p big $ "Conflicting definitions for constructor `" ++ x ++ "`."
    RedundantCase p -> posd p pat $ "Redundant case in pattern match."
        posd p $ "Conflicting definitions for constructor `" ++ x ++ "`."
    RedundantCase p -> posd p $ "Redundant case in pattern match."
    InexhaustivePats p patStr ->
        posd p defOrExpr
            $ "Inexhaustive patterns: "
            ++ patStr
            ++ " not covered."
        posd p $ "Inexhaustive patterns: " ++ patStr ++ " not covered."
    ExternNotMonomorphic name tv -> case tv of
        TVExplicit (Id (WithPos p tv')) ->
            posd p tvar
            posd p
                $ ("Extern " ++ pretty name ++ " is not monomorphic. ")
                ++ ("Type variable " ++ tv' ++ " encountered in type signature")
        TVImplicit _ -> ice "TVImplicit in prettyErr ExternNotMonomorphic"
    FoundHole p -> posd p var $ "Found hole"
    FoundHole p -> posd p $ "Found hole"
    RecTypeDef x p ->
        posd p big
        posd p
            $ ("Type `" ++ x ++ "` ")
            ++ "has infinite size due to recursion without indirection.\n"
            ++ "Insert a pointer at some point to make it representable."
    UndefType p x -> posd p big $ "Undefined type `" ++ x ++ "`."
    UndefType p x -> posd p $ "Undefined type `" ++ x ++ "`."
    UnboundTVar p ->
        posd p defOrExpr
        posd p
            $ "Could not fully infer type of expression.\n"
            ++ "Type annotations needed."
    WrongStartType (WithPos p s) ->
        posd p scheme
        posd p
            $ "Incorrect type of `start`.\n"
            ++ ("Expected: " ++ pretty startType)
            ++ ("\nFound: " ++ pretty s)
    RecursiveVarDef (WithPos p x) ->
        posd p var
        posd p
            $ ("Non-function variable definition `" ++ x ++ "` is recursive.")
    TypeInstArityMismatch p t expected found ->
        posd p tokenTree
        posd p
            $ ("Arity mismatch for instantiation of type `" ++ t)
            ++ ("`.\nExpected " ++ show expected)
            ++ (", found " ++ show found)
    ConflictingVarDef p x ->
        posd p tokenTree $ "Conflicting definitions for variable `" ++ x ++ "`."
  where
    -- | Used to handle that the position of the generated nested lambdas of a
    --   definition of the form `(define (foo a b ...) ...)` is set to the
    --   top-level position.
    defOrExpr =
        (Parse.ns_parens . Parse.def =<< Parse.getSrcPos)
            <||> Parse.ns_expr
            <||> wholeLine
    scheme = Parse.ns_scheme <||> wholeLine
    pat = Parse.ns_pat <||> wholeLine
    var = Parse.ns_small' <||> wholeLine
    tvar = var
    eConstructor = Parse.eConstructor <||> wholeLine
    big = Parse.ns_big
    wholeLine = many Mega.anySingle
    tokenTree = Parse.ns_tokenTree
    (<||>) pa pb = (Mega.try pa $> ()) <|> (pb $> ())
        posd p $ "Conflicting definitions for variable `" ++ x ++ "`."

posd :: SrcPos -> Parse.Parser a -> Message -> IO ()
posd (SrcPos pos@(SourcePos f lineN colN)) parser msg = do
posd :: SrcPos -> Message -> IO ()
posd (SrcPos pos@(SourcePos f lineN colN)) msg = do
    src <- readFile f
    let (lineN', colN') = (unPos lineN, unPos colN)
        lines' = lines src


@@ 143,13 119,14 @@ posd (SrcPos pos@(SourcePos f lineN colN)) parser msg = do
            then drop (colN' - 1) line
            else
                ice
                    "col num in SourcePos is greater than num of cols in src line"
                $ "col num in SourcePos is greater than "
                ++ "num of cols in src line"
        lineNS = show lineN'
        pad = length lineNS + 1
        s = either
            (\e -> ice ("posd: msg=|" ++ msg ++ "|,err=|" ++ show e ++ "|"))
            id
            (Parse.parse' (fmap fst (Mega.match parser)) "" rest)
            (parseTokenTreeOrRest rest)
    putStrLn $ unlines
        [ sourcePosPretty pos ++ ": Error:"
        , indent pad ++ "|"