git.iko.soy/elk
on a587ff5 help sign in
elk/src/Types/TypeCheck.hs
175 lines 6.5 kB history raw
2module TypeCheck where
4import Ast
5import Control.Monad
6import Control.Monad.Trans.Error
7import Data.IORef
8import Data.List (foldl', foldl1')
9import qualified Data.Map as Map
10import System.IO.Unsafe
11import TypeHints
12import Types
14{-- -- Testing Code
15import Testing
16typeCheck' s = str2expr s >>= typeCheck
17--}
18{--
19instance Monad (Either e) where
20 return = Right
21 Right m >>= k = k m
22 Left e >>= _ = Left e
23--}
24typeCheck prog = unsafePerformIO $ do
25 tipe <- tc typeHints prog
26 case tipe of
27 Right t -> unify (ADT "Element") t
28 Left _ -> return tipe
30guess = liftM GuessT (newIORef Nothing)
32varType env x =
33 case Map.lookup x env of
34 Just t -> return $ Right t
35 Nothing -> liftM Right $ guess
36 -- return . Left $ "Variable '" ++ x ++ "' is not bound to a value!"
37 -- This is no good because some fundamental functions are only
38 -- defined in JS, but it is the right thing to do.
40tipe = return . Right
42tc :: Map.Map String Type -> Exp -> IO (Either String Type)
43tc env exp =
44 case exp of
45 Number _ -> tipe NumberT
46 Var x -> varType env x
47 Str _ -> tipe StringT
48 Chr _ -> tipe CharT
49 Boolean _ -> tipe BoolT
50 List es -> do
51 either_ts <- liftM sequence $ mapM (tc env) es
52 case either_ts of
53 Right [] -> liftM (Right . ListT) guess
54 Right (t:ts) ->
55 return . liftM ListT =<< foldl' func (return $ Right t) ts
56 where func iet t = do
57 et <- iet
58 case et of { Right t' -> unify t t'
59 ; _ -> return et }
60 Left err -> return $ Left err
61 Range start end -> return . liftM ListT =<< unifyWith env start end unify
62 Tuple es -> return . liftM TupleT . sequence =<< mapM (tc env) es
63{--
64 Record r -> do
65 rList <- mapM (\(x,v) -> tc env v >>= tipe . (,) x) $
66 Map.toList r
67 tipe . RecordT $ Map.fromList rList
68 Access e x -> do
69 t <- tc env e
70 let err = error $ "Field '" ++ x ++
71 "' does not exist in record '" ++ show t ++ "'."
72 case t of
73 RecordT tRec -> tipe $ Map.findWithDefault err x tRec
74 GuessT _ -> guess
75 _ -> error $ "Expecting a record, but saw '" ++
76 show t ++ "' instead."
77--}
78 Binop op e1 e2 -> unifyWith env e1 e2 (checkBinop op)
79 Lambda x e -> do g <- guess
80 return . liftM (LambdaT g) =<< tc (Map.insert x g env) e
81 App e1 e2 -> do
82 g <- guess
83 unifyWith env e1 e2 $
84 \ta tb -> do
85 either_lam <- unify ta (LambdaT tb g)
86 case either_lam of { Right t -> return $ Right g
87 ; Left _ -> return either_lam }
88 Let x e1 e2 -> tc env (App (Lambda x e2) e1)
89 If eb et ef -> do
90 either_tb <- unifyWith env eb (Boolean True) unify
91 case either_tb of
92 Right _ -> unifyWith env et ef unify
93 Left _ -> return either_tb
94 _ -> return . Right =<< guess
95 -- return . Left $ "Failure during type-checking: not implemented yet"
97unifyWith env e1 e2 f = do
98 t1 <- tc env e1
99 t2 <- tc env e2
100 case (t1, t2) of { (Right ta, Right tb) -> f ta tb
101 ; (Left _, _) -> return t1
102 ; (_, Left _) -> return t2 }
105check es = return . foldl1' f =<< sequence es
106 where f b e = case b of { Right _ -> e; Left _ -> b }
108checkBinop Cons t1 t2 = unify (ListT t1) t2
109checkBinop Append t1 t2 = check [guess >>= unify t1 . ListT, unify t1 t2]
110checkBinop Compose t1 t2 = do
111 ga <- guess; gb <- guess; gc <- guess
112 check [ unify t2 (LambdaT ga gb)
113 , unify t1 (LambdaT gb gc)
114 , tipe (LambdaT ga gc) ]
115checkBinop Apply t1 t2 = do { g <- guess
116 ; check [unify t1 (LambdaT t2 g), tipe g] }
117checkBinop op t1 t2
118 | elem op [And, Or] = check [unify BoolT t1, unify BoolT t2]
119 | elem op [Equ, Neq] = check [guess >>= unify t1, unify t1 t2, tipe BoolT]
120 | elem op [Lt, Lte, Gt, Gte] =
121 check [unify NumberT t1, unify NumberT t2, tipe BoolT]
122 | elem op [Add, Sub, Mul, Div] = check [unify NumberT t1, unify NumberT t2]
124unify t1 t2
125 | t1 == t2 = tipe t1
126 | otherwise =
127 case (t1,t2) of
128 (StringT, _) -> unify (ListT CharT) t2
129 (_, StringT) -> unify t1 (ListT CharT)
130 (ListT t1', ListT t2') -> return . fmap ListT =<< unify t1' t2'
131 (TupleT ts1, TupleT ts2) ->
132 return . fmap TupleT . sequence =<< zipWithM unify ts1 ts2
133{--
134 (RecordT tMap1, RecordT tMap2) ->
135 tipe . RecordT =<< unifyTmap tMap1 tMap2
136--}
137 (GuessT ref, _) ->
138 if t2 `contains` ref then
139 return . Left $ "Cannot construct infinite type: " ++
140 show t1 ++ " = " ++ show t2
141 else do
142 g <- readIORef ref
143 case g of
144 Just t1' -> unify t1' t2
145 Nothing -> writeIORef ref (Just t2) >> tipe t1
146 (_, GuessT ref) -> -- unify t2 t1
147 if t1 `contains` ref then
148 return . Left $ "Cannot construct infinite type: " ++
149 show t1 ++ " = " ++ show t2
150 else do
151 g <- readIORef ref
152 case g of
153 Just t2' -> unify t1 t2'
154 Nothing -> writeIORef ref (Just t1) >> tipe t2
155 (LambdaT t1a t1b, LambdaT t2a t2b) -> do
156 ta <- unify t1a t2a
157 tb <- unify t1b t2b
158 return $ liftM2 LambdaT ta tb
159 (_, _) -> return . Left $
160 "Type Error: saw type '" ++ show t2 ++
161 "' but expecting type '" ++ show t1 ++ "'"
163unifyTmap tMap1 tMap2
164 | Map.keysSet tMap1 /= Map.keysSet tMap2 =
165 error "record unification failed"
166 | otherwise = Map.intersectionWith unify tMap1 tMap2
168t `contains` ref =
169 case t of
170 ListT t' -> t' `contains` ref
171 TupleT ts -> any (`contains` ref) ts
172 LambdaT t1 t2 -> t1 `contains` ref || t2 `contains` ref
173 {- RecordT (Map.Map String Type)-}
174 GuessT ref' -> ref == ref'
175 _ -> False