~jojo/Carth

ref: 65fedc5ad30893bac36f128dac201ff7081f8e1b Carth/src/TypeErr.hs -rw-r--r-- 5.6 KiB
65fedc5aJoJo Allow Box in pattern to dereference 1 year, 10 months ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
{-# LANGUAGE LambdaCase, FlexibleContexts, DataKinds #-}

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

import Misc
import SrcPos
import Ast
import qualified Parse

import qualified Text.Megaparsec as Mega
import Text.Megaparsec.Pos
import Data.Functor
import Control.Applicative

data TypeErr
    = StartNotDefined
    | InvalidUserTypeSig SrcPos Scheme Scheme
    | 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)
    | RedundantCase SrcPos
    | InexhaustivePats SrcPos String
    | ExternNotMonomorphic (Id Small) TVar
    | FoundHole SrcPos
    | RecTypeDef String SrcPos
    | UndefType SrcPos String
    | UnboundTVar SrcPos
    | WrongStartType (WithPos Scheme)
    | RecursiveVarDef (WithPos String)
    deriving Show

type Message = String

printErr :: TypeErr -> IO ()
printErr = \case
    StartNotDefined -> putStrLn "Error: start not defined"
    InvalidUserTypeSig p s1 s2 ->
        posd p scheme
            $ ("Invalid user type signature " ++ pretty s1)
            ++ (", expected " ++ pretty s2)
    CtorArityMismatch p c arity nArgs ->
        posd p pat
            $ ("Arity mismatch for constructor `" ++ pretty c)
            ++ ("` in pattern.\nExpected " ++ show arity)
            ++ (", found " ++ show nArgs)
    ConflictingPatVarDefs p v ->
        posd p var
            $ "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 ++ "`"
    InfType p t1 t2 a t ->
        posd p defOrExpr
            $ "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
            $ ("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 ++ "`."
    ConflictingCtorDef (Id (WithPos p x)) ->
        posd p big $ "Conflicting definitions for constructor `" ++ x ++ "`."
    RedundantCase p -> posd p pat $ "Redundant case in pattern match."
    InexhaustivePats p patStr ->
        posd p defOrExpr
            $ "Inexhaustive patterns: "
            ++ patStr
            ++ " not covered."
    ExternNotMonomorphic name tv -> case tv of
        TVExplicit (Id (WithPos p tv')) ->
            posd p tvar
                $ ("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"
    RecTypeDef x p ->
        posd p big
            $ ("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 ++ "` in constructor"
    UnboundTVar p ->
        posd p defOrExpr
            $ "Could not fully infer type of expression.\n"
            ++ "Type annotations needed."
    WrongStartType (WithPos p s) ->
        posd p scheme
            $ "Incorrect type of `start`.\n"
            ++ ("Expected: " ++ pretty startType)
            ++ ("\nFound: " ++ pretty s)
    RecursiveVarDef (WithPos p x) ->
        posd p var
            $ ("Non-function variable definition `" ++ x ++ "` is recursive.")
  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
    (<||>) pa pb = (Mega.try pa $> ()) <|> (pb $> ())

posd :: SrcPos -> Parse.Parser a -> Message -> IO ()
posd (SrcPos pos@(SourcePos f lineN colN)) parser msg = do
    src <- readFile f
    let (lineN', colN') = (unPos lineN, unPos colN)
        lines' = lines src
        line = if (lineN' <= length lines')
            then lines' !! (lineN' - 1)
            else ice "line num in SourcePos is greater than num of lines in src"
        rest = if (colN' <= length line)
            then drop (colN' - 1) line
            else
                ice
                    "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)
    putStrLn $ unlines
        [ sourcePosPretty pos ++ ": Error:"
        , indent pad ++ "|"
        , lineNS ++ " | " ++ line
        -- Find the span (end-pos) of the item in the source by applying the same
        -- parser that gave the item, starting at its SourcePos
        , indent pad ++ "|" ++ indent (colN') ++ replicate (length s) '^'
        , msg
        ]