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
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
|
{-# LANGUAGE TupleSections #-}
module Typecheck
(inferExpr,
checkExpr,
wellFormed,
Environment,
bool
)
where
import Syntax
import Control.Monad.Except
type Environment = [(Idnt,Typ)]
type Error = Except String
assertInt :: Typ -> Expr -> Error ()
assertInt TInt _ = return ()
assertInt t e = throwError $ "Expected type of expression "++ show e ++ " to be (TInt), instead got" ++ show t
assertRec :: Typ -> Expr -> Error TypeDict
assertRec (TRecord ts) _ = return ts
assertRec t e = throwError $ "Expected type of expression "++ show e ++ " to be (TRecord _), instead got" ++ show t
assertVar :: Typ -> Expr -> Error TypeDict
assertVar (TVariant ts) _ = return ts
assertVar t e = throwError $ "Expected type of expression "++ show e ++ " to be (TVariant _), instead got" ++ show t
assertPtr :: Typ -> Expr -> Error Typ
assertPtr (TPtr t) _ = return t
assertPtr t e = throwError $ "Expected type of expression "++ show e ++ " to be (TPtr _), instead got" ++ show t
envlookup :: Idnt -> TypeDict -> Expr -> Error Typ
envlookup name env expr = case lookup name env of
Just t -> return t
Nothing -> throwError $ "Variable "++ name ++ "not defined in expr" ++ show expr
insert :: Idnt -> Typ -> Environment -> TypeDict
insert v t l = (v,t):l
subset ::Show a=> [Idnt] -> [Idnt]-> a -> Error ()
subset [] _ _= return ()
subset (x:xs) l a= if x `elem` l then subset xs l a else throwError $ "Case "++ show x ++ "not checked in case/match" ++ show a
inferExpr :: Expr -> Environment -> Error Typ
inferExpr e@(Var name) env = envlookup name env e
inferExpr (IntLit _) _ = return TInt
inferExpr (Record ts) env = do
tts <- mapM (\(v,e) -> (v,) <$> inferExpr e env) ts
return $ TRecord tts
inferExpr ee@(Variant t v e) env = do
ts <- assertVar t e
tt <- envlookup v ts ee
checkExpr e env tt
return t
inferExpr (Add e1 e2) env = do
checkExpr e1 env TInt
checkExpr e2 env TInt
return TInt
inferExpr (Mult e1 e2) env = do
checkExpr e1 env TInt
checkExpr e2 env TInt
return TInt
inferExpr (Neg e) env = do
checkExpr e env TInt
return TInt
inferExpr (Deref e1) env = do
t <- inferExpr e1 env
tt <- assertPtr t e1
return tt
inferExpr c@(Match e cases) env = do
varType <- inferExpr e env
variants <- assertVar varType e
caseTypes <- mapM (\(v,bind,e) ->(v,) <$> do
tt <- envlookup v variants e
inferExpr e (insert bind tt env)) cases
subset (map fst variants) (map (\(_,v,_)->v) cases) c
ret <- allSame caseTypes
return $ snd ret
where
allSame :: [(Idnt,Typ)] -> Error (Idnt,Typ)
allSame (x:[]) = return x
allSame [] = throwError $ "Empty case "++ show c
allSame ((xx,x):xs) = do
(v,t) <- allSame xs
if t==x then return (v,t) else
throwError $ "Different types in branches " ++ show v ++ "," ++ show xx ++ "of expression" ++ show c
inferExpr (Proj name e) env = do
t <- inferExpr e env
tt <- assertRec t e
case lookup name tt of
Just typ -> return typ
Nothing -> throwError $ "Record " ++show e ++ "doesn't have field" ++ name
inferExpr (Annot e t) env = do
checkExpr e env t
return t
checkExpr :: Expr -> Environment -> Typ -> Error ()
checkExpr e@(Add e1 e2) env t = do
assertInt t e
checkExpr e1 env TInt
checkExpr e2 env TInt
checkExpr e@(Mult e1 e2) env t = do
assertInt t e
checkExpr e1 env TInt
checkExpr e2 env TInt
checkExpr e@(Neg ee) env t = do
assertInt t e
checkExpr ee env TInt
checkExpr (Deref e1) env t = do
checkExpr e1 env (TPtr t)
checkExpr e env t = do
t' <- inferExpr e env
if t == t' then return ()
else throwError $ "Expected type of expression " ++
show e ++ " to be"++ show t ++" instead got" ++ show t'
bool = TVariant [("True",TRecord []),("False", TRecord [])]
cenvlookup ::(Show a,Eq a) => a-> [(a,b)] -> Com -> Error b
cenvlookup name env c = case lookup name env of
Just t -> return t
Nothing -> throwError $ "name "++ show name ++ "not visible in expr" ++ show c
wellFormed :: Com ->Environment -> FuncEnv-> Error ()
wellFormed Skip _ _= return ()
wellFormed (Seq s1 s2) env fe = do
wellFormed s1 env fe
wellFormed s2 env fe
wellFormed (If e c1 c2) env fe = do
checkExpr e env bool
wellFormed c1 env fe
wellFormed c2 env fe
wellFormed (While e c) env fe= do
checkExpr e env bool
wellFormed c env fe
wellFormed c@(Asgn v e) env _ = do
vt <- cenvlookup v env c
et <- inferExpr e env
if vt==et then return ()
else throwError $ "Variable " ++ show v ++ "::" ++ show vt ++ " was assigned expression " ++ show e ++ "::" ++ show et
wellFormed (Decl v e c) env fe= do
et <- inferExpr e env
wellFormed c (insert v et env) fe
wellFormed (Alloc v e c) env fe = do
et <- inferExpr e env
wellFormed c (insert v (TPtr et) env) fe
wellFormed c@(Save v e) env _ = do
vt <- cenvlookup v env c
et <- inferExpr e env
if vt==TPtr et then return ()
else throwError $ "Expression" ++ show e ++ "::" ++ show et ++ " was saved to pointer "++show v ++ " of type" ++ show vt
wellFormed c@(SMatch e cases) env fe= do
varType <- inferExpr e env
variants <- assertVar varType e
mapM (\(v,bind,c) -> do
tt <- envlookup v variants e
wellFormed c (insert bind tt env) fe) cases
subset (map fst variants) (map (\(_,v,_)->v) cases) c
return ()
wellFormed c@(FunctionCall v f args) env fa= do
(FuncSign argTypes retType) <- cenvlookup f fa c
vt <- cenvlookup v env c
if vt/=retType then throwError $ "Returned function type"++show retType++" doesn't match up with variable type " ++show vt ++ " in " ++ show c
else argsOk args argTypes
where argsOk:: [Expr] ->[Typ] ->Error ()
argsOk [] [] =return ()
argsOk (_:_) [] = throwError $ "Too many arguments in function call" ++ show c
argsOk [] (_:_) = throwError $ "Not enough arguments in function call" ++ show c
argsOk (x:xs) (y:ys) = do
checkExpr x env y
argsOk xs ys
|
