@@ -1,175 +0,0 @@
1−
2−module TypeCheck where
3−
4−import Ast
5−import Control.Monad
6−import Control.Monad.Trans.Error
7−import Data.IORef
8−import Data.List (foldl', foldl1')
9−import qualified Data.Map as Map
10−import System.IO.Unsafe
11−import TypeHints
12−import Types
13−
14−{-- -- Testing Code
15−import Testing
16−typeCheck' s = str2expr s >>= typeCheck
17−--}
18−{--
19−instance Monad (Either e) where
20− return = Right
21− Right m >>= k = k m
22− Left e >>= _ = Left e
23−--}
24−typeCheck prog = unsafePerformIO $ do
25− tipe <- tc typeHints prog
26− case tipe of
27− Right t -> unify (ADT "Element") t
28− Left _ -> return tipe
29−
30−guess = liftM GuessT (newIORef Nothing)
31−
32−varType 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.
39−
40−tipe = return . Right
41−
42−tc :: Map.Map String Type -> Exp -> IO (Either String Type)
43−tc 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"
96−
97−unifyWith 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 }
103−
104−
105−check es = return . foldl1' f =<< sequence es
106− where f b e = case b of { Right _ -> e; Left _ -> b }
107−
108−checkBinop Cons t1 t2 = unify (ListT t1) t2
109−checkBinop Append t1 t2 = check [guess >>= unify t1 . ListT, unify t1 t2]
110−checkBinop 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) ]
115−checkBinop Apply t1 t2 = do { g <- guess
116− ; check [unify t1 (LambdaT t2 g), tipe g] }
117−checkBinop op t1 t2
118− | op `elem` [And, Or] = check [unify BoolT t1, unify BoolT t2]
119− | op `elem` [Equ, Neq] = check [guess >>= unify t1, unify t1 t2, tipe BoolT]
120− | op `elem` [Lt, Lte, Gt, Gte] =
121− check [unify NumberT t1, unify NumberT t2, tipe BoolT]
122− | op `elem` [Add, Sub, Mul, Div] = check [unify NumberT t1, unify NumberT t2]
123−
124−unify 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 ++ "'"
162−
163−unifyTmap tMap1 tMap2
164− | Map.keysSet tMap1 /= Map.keysSet tMap2 =
165− error "record unification failed"
166− | otherwise = Map.intersectionWith unify tMap1 tMap2
167−
168−t `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