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
|
{-# LANGUAGE TupleSections #-}
module Typecheck
(inferExpr,
checkExpr,
wellFormed,
Environment,
)
where
import Syntax
--import Control.Monad
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
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 :: Idnt -> TypeDict -> Com -> Error Typ
cenvlookup name env c = case lookup name env of
Just t -> return t
Nothing -> throwError $ "Variable "++ name ++ "not defined in expr" ++ show c
wellFormed :: Com ->Environment -> Error ()
wellFormed Skip _= return ()
wellFormed (Seq s1 s2) env = do
wellFormed s1 env
wellFormed s2 env
wellFormed (If e c1 c2) env = do
checkExpr e env bool
wellFormed c1 env
wellFormed c2 env
wellFormed (While e c) env = do
checkExpr e env bool
wellFormed c env
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= do
et <- inferExpr e env
wellFormed c (insert v et env)
wellFormed (Alloc v e c) env = do
et <- inferExpr e env
wellFormed c (insert v (TPtr et) env)
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 = 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)) cases
subset (map fst variants) (map (\(_,v,_)->v) cases) c
return ()
|
