git.iko.soy/rowtype-yoga/purescript-native
on e7dfe87 help sign in
rowtype-yoga/purescript-native/src/PureScript/TypeChecker/Types.hs
619 lines 28 kB history raw
1-----------------------------------------------------------------------------
2--
3-- Module : PureScript.TypeChecker.Types
4-- Copyright : (c) Phil Freeman 2013
5-- License : MIT
6--
7-- Maintainer : Phil Freeman <paf31@cantab.net>
8-- Stability : experimental
9-- Portability :
10--
11-- |
12--
13-----------------------------------------------------------------------------
15{-# LANGUAGE DeriveDataTypeable #-}
17module PureScript.TypeChecker.Types (
18 TypeConstraint(..),
19 TypeSolution(..),
20 typeOf
21) where
23import Debug.Trace
25import Data.List
26import Data.Function
27import qualified Data.Data as D
28import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
30import PureScript.Values
31import PureScript.Types
32import PureScript.Kinds
33import PureScript.Names
34import PureScript.TypeChecker.Monad
35import PureScript.TypeChecker.Kinds
36import PureScript.TypeChecker.Synonyms
37import PureScript.CodeGen.Pretty.Types
38import PureScript.CodeGen.Pretty.Kinds
39import PureScript.CodeGen.Pretty.Values
41import Control.Monad.State
42import Control.Monad.Error
44import Control.Applicative
45import Control.Arrow (Kleisli(..), (***), (&&&))
46import qualified Control.Category as C
48import qualified Data.Map as M
50data TypeConstraintOrigin
51 = ValueOrigin Value
52 | BinderOrigin Binder
53 | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
55prettyPrintOrigin :: TypeConstraintOrigin -> String
56prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
57prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
58prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
60data TypeConstraint
61 = TypeConstraint Int Type TypeConstraintOrigin
62 | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
64newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
66emptyTypeSolution :: TypeSolution
67emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
69typeOf :: Ident -> Value -> Check PolyType
70typeOf name val = do
71 (cs, n) <- case val of
72 Abs _ _ -> do
73 me <- fresh
74 (cs, n) <- typeConstraints (M.singleton name me) val
75 return (TypeConstraint me (TUnknown n) (ValueOrigin val): cs, n)
76 _ -> typeConstraints M.empty val
77 desugared <- replaceAllTypeSynonyms cs
78 solution <- solveTypeConstraints desugared emptyTypeSolution
79 let ty = fst (runTypeSolution solution) n
80 allUnknownsBecameQuantified desugared solution ty
81 return $ varIfUnknown $ desaturateAllTypeSynonyms $ setifyAll ty
83allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
84allUnknownsBecameQuantified cs solution ty = do
85 let
86 typesMentioned = findUnknownTypes ty
87 unknownTypes = nub $ flip concatMap cs $ \c -> case c of
88 TypeConstraint u t _ -> u : findUnknownTypes t
89 RowConstraint _ r _ -> findUnknownTypes r
90 unsolvedTypes = filter (\n -> TUnknown n == fst (runTypeSolution solution) n) unknownTypes
91 guardWith "Unsolved type variable" $ null $ unsolvedTypes \\ typesMentioned
92 let
93 rowsMentioned = findUnknownRows ty
94 unknownRows = nub $ flip concatMap cs $ \c -> case c of
95 TypeConstraint _ t _ -> findUnknownRows t
96 RowConstraint u r _ -> u : findUnknownRows r
97 unsolvedRows = filter (\n -> RUnknown n == snd (runTypeSolution solution) n) unknownRows
98 guardWith "Unsolved row variable" $ null $ unsolvedRows \\ rowsMentioned
100setify :: Row -> Row
101setify = rowFromList . (M.toList . M.fromList *** id) . rowToList
103setifyAll :: (D.Data d) => d -> d
104setifyAll = everywhere (mkT setify)
106findUnknownTypes :: (D.Data d) => d -> [Int]
107findUnknownTypes = everything (++) (mkQ [] f)
108 where
109 f :: Type -> [Int]
110 f (TUnknown n) = [n]
111 f _ = []
113findTypeVars :: (D.Data d) => d -> [String]
114findTypeVars = everything (++) (mkQ [] f)
115 where
116 f :: Type -> [String]
117 f (TypeVar v) = [v]
118 f _ = []
120findUnknownRows :: (D.Data d) => d -> [Int]
121findUnknownRows = everything (++) (mkQ [] f)
122 where
123 f :: Row -> [Int]
124 f (RUnknown n) = [n]
125 f _ = []
127varIfUnknown :: Type -> PolyType
128varIfUnknown ty =
129 let
130 (ty', m) = flip runState M.empty $ everywhereM (flip extM g $ mkM f) ty
131 in
132 PolyType (sort $ nub $ M.elems m ++ findTypeVars ty) ty'
133 where
134 f :: Type -> State (M.Map Int String) Type
135 f (TUnknown n) = do
136 m <- get
137 case M.lookup n m of
138 Nothing -> do
139 let name = "t" ++ show (M.size m)
140 put $ M.insert n name m
141 return $ TypeVar name
142 Just name -> return $ TypeVar name
143 f t = return t
144 g :: Row -> State (M.Map Int String) Row
145 g (RUnknown n) = do
146 m <- get
147 case M.lookup n m of
148 Nothing -> do
149 let name = "r" ++ show (M.size m)
150 put $ M.insert n name m
151 return $ RowVar name
152 Just name -> return $ RowVar name
153 g r = return r
155replaceTypeVars :: M.Map String Type -> Type -> Type
156replaceTypeVars m = everywhere (mkT replace)
157 where
158 replace (TypeVar v) = case M.lookup v m of
159 Just ty -> ty
160 _ -> TypeVar v
161 replace t = t
163replaceVarsWithUnknowns :: [String] -> Type -> Check Type
164replaceVarsWithUnknowns idents = flip evalStateT M.empty . everywhereM (flip extM f $ mkM g)
165 where
166 f :: Type -> StateT (M.Map String Int) Check Type
167 f (TypeVar var) | var `elem` idents = do
168 m <- get
169 n <- lift fresh
170 case M.lookup var m of
171 Nothing -> do
172 put (M.insert var n m)
173 return $ TUnknown n
174 Just u -> return $ TUnknown u
175 f t = return t
176 g :: Row -> StateT (M.Map String Int) Check Row
177 g (RowVar var) | var `elem` idents = do
178 m <- get
179 n <- lift fresh
180 case M.lookup var m of
181 Nothing -> do
182 put (M.insert var n m)
183 return $ RUnknown n
184 Just u -> return $ RUnknown u
185 g r = return r
187replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
188replaceAllTypeSynonyms d = do
189 env <- getEnv
190 let syns = map (\(name, (args, _)) -> (name, length args)) . M.toList $ typeSynonyms env
191 either throwError return $ saturateAllTypeSynonyms syns d
193desaturateAllTypeSynonyms :: (D.Data d) => d -> d
194desaturateAllTypeSynonyms = everywhere (mkT $ replace)
195 where
196 replace (SaturatedTypeSynonym name args) = foldl (\t arg -> TypeApp t arg) (TypeConstructor name) args
197 replace t = t
199replaceType :: (D.Data d) => Int -> Type -> d -> d
200replaceType n t = everywhere (mkT go)
201 where
202 go (TUnknown m) | m == n = t
203 go t = t
205replaceRow :: (D.Data d) => Int -> Row -> d -> d
206replaceRow n r = everywhere (mkT go)
207 where
208 go (RUnknown m) | m == n = r
209 go r = r
211typeOccursCheck :: Int -> Type -> Check ()
212typeOccursCheck u (TUnknown _) = return ()
213typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
215rowOccursCheck :: Int -> Row -> Check ()
216rowOccursCheck u (RUnknown _) = return ()
217rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
219occursCheck :: (D.Data d) => Int -> d -> Bool
220occursCheck u = everything (||) $ flip extQ g $ mkQ False f
221 where
222 f (TUnknown u') | u' == u = True
223 f _ = False
224 g (RUnknown u') | u' == u = True
225 g _ = False
227typesToRow :: [(String, Type)] -> Row
228typesToRow [] = REmpty
229typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
231rowToList :: Row -> ([(String, Type)], Row)
232rowToList (RCons name ty row) = let (tys, rest) = rowToList row
233 in ((name, ty):tys, rest)
234rowToList r = ([], r)
236rowFromList :: ([(String, Type)], Row) -> Row
237rowFromList ([], r) = r
238rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
240ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
241ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
243typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
244typeConstraints _ v@(NumericLiteral _) = do
245 me <- fresh
246 return ([TypeConstraint me Number (ValueOrigin v)], me)
247typeConstraints _ v@(StringLiteral _) = do
248 me <- fresh
249 return ([TypeConstraint me String (ValueOrigin v)], me)
250typeConstraints _ v@(BooleanLiteral _) = do
251 me <- fresh
252 return ([TypeConstraint me Boolean (ValueOrigin v)], me)
253typeConstraints m v@(ArrayLiteral vals) = do
254 all <- mapM (typeConstraints m) vals
255 let (cs, ns) = (concat . map fst &&& map snd) all
256 me <- fresh
257 return (cs ++ zipWith (\n el -> TypeConstraint me (Array $ TUnknown n) (ValueOrigin el)) ns vals, me)
258typeConstraints m u@(Unary op val) = do
259 (cs, n1) <- typeConstraints m val
260 me <- fresh
261 return (cs ++ unaryOperatorConstraints u op n1 me, me)
262typeConstraints m b@(Binary op left right) = do
263 (cs1, n1) <- typeConstraints m left
264 (cs2, n2) <- typeConstraints m right
265 me <- fresh
266 return (cs1 ++ cs2 ++ binaryOperatorConstraints b op n1 n2 me, me)
267typeConstraints m v@(ObjectLiteral ps) = do
268 ensureNoDuplicateProperties ps
269 all <- mapM (typeConstraints m . snd) ps
270 let (cs, ns) = (concat . map fst &&& map snd) all
271 me <- fresh
272 let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
273 return ((TypeConstraint me (Object (typesToRow tys)) (ValueOrigin v)) : cs, me)
274typeConstraints m v@(ObjectUpdate o ps) = do
275 ensureNoDuplicateProperties ps
276 (cs1, n1) <- typeConstraints m o
277 all <- mapM (typeConstraints m . snd) ps
278 let (cs2, ns) = (concat . map fst &&& map snd) all
279 row <- fresh
280 let tys = zipWith (\(name, _) u -> (name, TUnknown u)) ps ns
281 return (TypeConstraint n1 (Object (rowFromList (tys, RUnknown row))) (ValueOrigin v) : cs1 ++ cs2, n1)
282typeConstraints m v@(Indexer index val) = do
283 (cs1, n1) <- typeConstraints m index
284 (cs2, n2) <- typeConstraints m val
285 me <- fresh
286 return ((TypeConstraint n1 Number (ValueOrigin index)) : (TypeConstraint n2 (Array (TUnknown me)) (ValueOrigin v)) : cs1 ++ cs2, me)
287typeConstraints m v@(Accessor prop val) = do
288 (cs, n1) <- typeConstraints m val
289 me <- fresh
290 rest <- fresh
291 return ((TypeConstraint n1 (Object (RCons prop (TUnknown me) (RUnknown rest))) (ValueOrigin v)) : cs, me)
292typeConstraints m v@(Abs args ret) = do
293 ns <- replicateM (length args) fresh
294 let m' = m `M.union` M.fromList (zipWith (,) args ns)
295 (cs, n') <- typeConstraints m' ret
296 me <- fresh
297 return ((TypeConstraint me (Function (map TUnknown ns) (TUnknown n')) (ValueOrigin v)) : cs, me)
298typeConstraints m v@(App f xs) = do
299 (cs1, n1) <- typeConstraints m f
300 all <- mapM (typeConstraints m) xs
301 let (cs2, ns) = (concat . map fst &&& map snd) all
302 me <- fresh
303 return ((TypeConstraint n1 (Function (map TUnknown ns) (TUnknown me)) (ValueOrigin v)) : cs1 ++ cs2, me)
304typeConstraints m v@(Var var) =
305 case M.lookup var m of
306 Nothing -> do
307 env <- getEnv
308 case M.lookup var (names env) of
309 Nothing -> throwError $ show var ++ " is undefined"
310 Just (PolyType idents ty, _) -> do
311 me <- fresh
312 replaced <- replaceVarsWithUnknowns idents ty
313 return ([TypeConstraint me replaced (ValueOrigin v)], me)
314 Just u -> do
315 me <- fresh
316 return ([TypeConstraint u (TUnknown me) (ValueOrigin v)], me)
317typeConstraints m (Block ss) = do
318 ret <- fresh
319 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m M.empty ret ss
320 guardWith "Block is missing a return statement" allCodePathsReturn
321 return (cs, ret)
322typeConstraints m v@(Constructor c) = do
323 env <- getEnv
324 case M.lookup c (dataConstructors env) of
325 Nothing -> throwError $ "Constructor " ++ c ++ " is undefined"
326 Just (PolyType idents ty) -> do
327 me <- fresh
328 replaced <- replaceVarsWithUnknowns idents ty
329 return ([TypeConstraint me replaced (ValueOrigin v)], me)
330typeConstraints m (Case val binders) = do
331 (cs1, n1) <- typeConstraints m val
332 ret <- fresh
333 cs2 <- typeConstraintsForBinders m n1 ret binders
334 return (cs1 ++ cs2, ret)
335typeConstraints m v@(IfThenElse cond th el) = do
336 (cs1, n1) <- typeConstraints m cond
337 (cs2, n2) <- typeConstraints m th
338 (cs3, n3) <- typeConstraints m el
339 return (TypeConstraint n1 Boolean (ValueOrigin cond) : TypeConstraint n2 (TUnknown n3) (ValueOrigin v) : cs1 ++ cs2 ++ cs3, n2)
340typeConstraints m v@(TypedValue val poly@(PolyType idents ty)) = do
341 kind <- kindOf poly
342 guardWith ("Expected type of kind *, was " ++ prettyPrintKind kind) $ kind == Star
343 (cs, n1) <- typeConstraints m val
344 return (TypeConstraint n1 ty (ValueOrigin v) : cs, n1)
346unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
347unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
348unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
349unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
351binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
352binaryOperatorConstraints v Add = symBinOpConstraints v Number
353binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
354binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
355binaryOperatorConstraints v Divide = symBinOpConstraints v Number
356binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
357binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
358binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
359binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
360binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
361binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
362binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
363binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
364binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
365binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
366binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
367binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
368binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
369binaryOperatorConstraints v And = symBinOpConstraints v Boolean
370binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
371binaryOperatorConstraints v Concat = symBinOpConstraints v String
373equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
374equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
376symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
377symBinOpConstraints v ty left right result = asymBinOpConstraints v ty ty left right result
379asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
380asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
382typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
383typeConstraintsForBinder _ NullBinder = return ([], M.empty)
384typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
385typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
386typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
387typeConstraintsForBinder val b@(VarBinder name) = do
388 me <- fresh
389 return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
390typeConstraintsForBinder val b@(NullaryBinder ctor) = do
391 env <- getEnv
392 case M.lookup ctor (dataConstructors env) of
393 Just (PolyType args ret) -> do
394 ret' <- replaceVarsWithUnknowns args ret
395 return ([TypeConstraint val ret' (BinderOrigin b)], M.empty)
396 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
397typeConstraintsForBinder val b@(UnaryBinder ctor binder) = do
398 env <- getEnv
399 case M.lookup ctor (dataConstructors env) of
400 Just (PolyType idents f@(Function [_] _)) -> do
401 obj <- fresh
402 (Function [ty] ret) <- replaceVarsWithUnknowns idents f
403 (cs, m1) <- typeConstraintsForBinder obj binder
404 return ((TypeConstraint val ret (BinderOrigin b)) : (TypeConstraint obj ty (BinderOrigin b)) : cs, m1)
405 Just _ -> throwError $ ctor ++ " is not a unary constructor"
406 _ -> throwError $ "Constructor " ++ ctor ++ " is not defined"
407typeConstraintsForBinder val b@(ObjectBinder props) = do
408 row <- fresh
409 rest <- fresh
410 (cs, m1) <- typeConstraintsForProperties row (RUnknown rest) props
411 return ((TypeConstraint val (Object (RUnknown row)) (BinderOrigin b)) : cs, m1)
412 where
413 typeConstraintsForProperties :: Int -> Row -> [(String, Binder)] -> Check ([TypeConstraint], M.Map Ident Int)
414 typeConstraintsForProperties nrow row [] = return ([RowConstraint nrow row (BinderOrigin b)], M.empty)
415 typeConstraintsForProperties nrow row ((name, binder):binders) = do
416 propTy <- fresh
417 (cs1, m1) <- typeConstraintsForBinder propTy binder
418 (cs2, m2) <- typeConstraintsForProperties nrow (RCons name (TUnknown propTy) row) binders
419 return (cs1 ++ cs2, M.union m1 m2)
420typeConstraintsForBinder val b@(ArrayBinder binders rest) = do
421 el <- fresh
422 all <- mapM (typeConstraintsForBinder el) binders
423 let (cs1, m1) = (concat . map fst &&& M.unions . map snd) all
424 let arrayConstraint = TypeConstraint val (Array (TUnknown el)) (BinderOrigin b)
425 case rest of
426 Nothing -> return (arrayConstraint : cs1, m1)
427 Just binder -> do
428 (cs2, m2) <- typeConstraintsForBinder val binder
429 return (arrayConstraint : cs1 ++ cs2, M.union m1 m2)
430typeConstraintsForBinder val b@(NamedBinder name binder) = do
431 me <- fresh
432 (cs, m) <- typeConstraintsForBinder val binder
433 return (TypeConstraint me (TUnknown val) (BinderOrigin b) : cs, M.insert name me m)
434typeConstraintsForBinder val b@(GuardedBinder cond binder) = do
435 (cs1, m) <- typeConstraintsForBinder val binder
436 (cs2, n) <- typeConstraints m cond
437 return (TypeConstraint n Boolean (ValueOrigin cond) : cs1 ++ cs2, m)
439constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
440constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
442typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
443typeConstraintsForBinders _ _ _ [] = return []
444typeConstraintsForBinders m nval ret ((binder, val):bs) = do
445 (cs1, m1) <- typeConstraintsForBinder nval binder
446 (cs2, n2) <- typeConstraints (M.union m m1) val
447 cs3 <- typeConstraintsForBinders m nval ret bs
448 return ((TypeConstraint n2 (TUnknown ret) (BinderOrigin binder)) : cs1 ++ cs2 ++ cs3)
450assignVariable :: Ident -> M.Map Ident Int -> Check ()
451assignVariable name m =
452 case M.lookup name m of
453 Nothing -> return ()
454 Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
456typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
457typeConstraintsForStatement m mass ret (VariableIntroduction name val) = do
458 assignVariable name (m `M.union` mass)
459 (cs1, n1) <- typeConstraints m val
460 return $ (cs1, False, M.insert name n1 mass)
461typeConstraintsForStatement m mass ret (Assignment ident val) = do
462 (cs1, n1) <- typeConstraints m val
463 case M.lookup ident mass of
464 Nothing -> throwError $ "No local variable with name " ++ show ident
465 Just ty -> do
466 return (TypeConstraint n1 (TUnknown ty) (AssignmentTargetOrigin ident) : cs1, False, mass)
467typeConstraintsForStatement m mass ret (While val inner) = do
468 (cs1, n1) <- typeConstraints m val
469 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret inner
470 return $ ((TypeConstraint n1 Boolean (ValueOrigin val)) : cs1 ++ cs2, allCodePathsReturn, mass)
471typeConstraintsForStatement m mass ret (If ifst) = do
472 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
473 return $ (cs, allCodePathsReturn, mass)
474typeConstraintsForStatement m mass ret (For ident start end inner) = do
475 assignVariable ident (m `M.union` mass)
476 (cs1, n1) <- typeConstraints (m `M.union` mass) start
477 (cs2, n2) <- typeConstraints (m `M.union` mass) end
478 let mass1 = M.insert ident n1 mass
479 (cs3, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
480 return $ ((TypeConstraint n1 Number (ValueOrigin start)) : (TypeConstraint n2 Number (ValueOrigin end)) : cs1 ++ cs2 ++ cs3, allCodePathsReturn, mass)
481typeConstraintsForStatement m mass ret (ForEach ident vals inner) = do
482 assignVariable ident (m `M.union` mass)
483 val <- fresh
484 (cs1, n1) <- typeConstraints (m `M.union` mass) vals
485 let mass1 = M.insert ident val mass
486 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock (m `M.union` mass1) mass1 ret inner
487 guardWith "Cannot return from within a foreach block" $ not allCodePathsReturn
488 return $ ((TypeConstraint n1 (Array (TUnknown val)) (ValueOrigin vals)) : cs1 ++ cs2, False, mass)
489typeConstraintsForStatement m mass ret (Return val) = do
490 (cs1, n1) <- typeConstraints (m `M.union` mass) val
491 return ((TypeConstraint n1 (TUnknown ret) (ValueOrigin val)) : cs1, True, mass)
493typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
494typeConstraintsForIfStatement m mass ret (IfStatement val thens Nothing) = do
495 (cs1, n1) <- typeConstraints m val
496 (cs2, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret thens
497 return ((TypeConstraint n1 Boolean (ValueOrigin val)) : cs1 ++ cs2, allCodePathsReturn)
498typeConstraintsForIfStatement m mass ret (IfStatement val thens (Just elses)) = do
499 (cs1, n1) <- typeConstraints m val
500 (cs2, allCodePathsReturn1, _) <- typeConstraintsForBlock m mass ret thens
501 (cs3, allCodePathsReturn2) <- typeConstraintsForElseStatement m mass ret elses
502 return ((TypeConstraint n1 Boolean (ValueOrigin val)) : cs1 ++ cs2 ++ cs3, allCodePathsReturn1 && allCodePathsReturn2)
504typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
505typeConstraintsForElseStatement m mass ret (Else elses) = do
506 (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
507 return (cs, allCodePathsReturn)
508typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
509 (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
510 return (cs, allCodePathsReturn)
512typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
513typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
514typeConstraintsForBlock m mass ret (s:ss) = do
515 (cs1, b1, mass1) <- typeConstraintsForStatement (m `M.union` mass) mass ret s
516 case (b1, ss) of
517 (True, []) -> return (cs1, True, mass1)
518 (True, _) -> throwError "Unreachable code"
519 (False, ss) -> do
520 (cs2, b2, mass2) <- typeConstraintsForBlock m mass1 ret ss
521 return (cs1 ++ cs2, b2, mass2)
523solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
524solveTypeConstraints [] s = return s
525solveTypeConstraints all@(TypeConstraint n t o:cs) s = do
526 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
527 typeOccursCheck n t
528 let s' = let (f, g) = runTypeSolution s
529 in TypeSolution (replaceType n t . f, replaceType n t . g)
530 cs' <- fmap concat $ mapM (substituteTypeInConstraint n t) cs
531 return (cs', s')
532 solveTypeConstraints cs' s'
533solveTypeConstraints (RowConstraint n r o:cs) s = do
534 (cs', s') <- rethrow (\err -> "Error in " ++ prettyPrintOrigin o ++ ": " ++ err) $ do
535 rowOccursCheck n r
536 let s' = let (f, g) = runTypeSolution s
537 in TypeSolution $ (replaceRow n r . f, replaceRow n r . g)
538 cs' <- fmap concat $ mapM (substituteRowInConstraint n r) cs
539 return (cs', s')
540 solveTypeConstraints cs' s'
542substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
543substituteTypeInConstraint n s (TypeConstraint m t v)
544 | n == m = unifyTypes v s t
545 | otherwise = return [TypeConstraint m (replaceType n s t) v]
546substituteTypeInConstraint n s (RowConstraint m r v)
547 = return [RowConstraint m (replaceType n s r) v]
549substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
550substituteRowInConstraint n r (TypeConstraint m t v)
551 = return [TypeConstraint m (replaceRow n r t) v]
552substituteRowInConstraint n r (RowConstraint m r1 v)
553 | m == n = unifyRows v r r1
554 | otherwise = return [RowConstraint m (replaceRow n r r1) v]
556unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
557unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
558unifyTypes o (TUnknown u) t = do
559 typeOccursCheck u t
560 return [TypeConstraint u t o]
561unifyTypes o t (TUnknown u) = do
562 typeOccursCheck u t
563 return [TypeConstraint u t o]
564unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
565 fmap concat $ zipWithM (unifyTypes o) args1 args2
566unifyTypes o (SaturatedTypeSynonym name args) ty = do
567 env <- getEnv
568 case M.lookup name (typeSynonyms env) of
569 Just (synArgs, body) -> do
570 let m = M.fromList $ zip synArgs args
571 let replaced = replaceTypeVars m body
572 unifyTypes o replaced ty
573 Nothing -> error "Type synonym was not defined"
574unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
575unifyTypes _ Number Number = return []
576unifyTypes _ String String = return []
577unifyTypes _ Boolean Boolean = return []
578unifyTypes o (Array s) (Array t) = unifyTypes o s t
579unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
580unifyTypes o (Function args1 ret1) (Function args2 ret2) = do
581 guardWith "Function applied to incorrect number of args" $ length args1 == length args2
582 cs1 <- fmap concat $ zipWithM (unifyTypes o) args1 args2
583 cs2 <- unifyTypes o ret1 ret2
584 return $ cs1 ++ cs2
585unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
586unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
587unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
588 cs1 <- unifyTypes o t1 t3
589 cs2 <- unifyTypes o t2 t4
590 return $ cs1 ++ cs2
591unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
593unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
594unifyRows o r1 r2 =
595 let
596 (s1, r1') = rowToList r1
597 (s2, r2') = rowToList r2
598 int = [ (t1, t2) | (name, t1) <- s1, (name', t2) <- s2, name == name' ]
599 sd1 = [ (name, t1) | (name, t1) <- s1, not (elem name (map fst s2)) ]
600 sd2 = [ (name, t2) | (name, t2) <- s2, not (elem name (map fst s1)) ]
601 in do
602 cs1 <- fmap concat $ mapM (uncurry $ unifyTypes o) int
603 cs2 <- unifyRows' o sd1 r1' sd2 r2'
604 return $ cs1 ++ cs2
605 where
606 unifyRows' :: TypeConstraintOrigin -> [(String, Type)] -> Row -> [(String, Type)] -> Row -> Check [TypeConstraint]
607 unifyRows' o [] (RUnknown u) sd r = do
608 rowOccursCheck u r
609 return [RowConstraint u (rowFromList (sd, r)) o]
610 unifyRows' o sd r [] (RUnknown u) = do
611 rowOccursCheck u r
612 return [RowConstraint u (rowFromList (sd, r)) o]
613 unifyRows' o ns@((name, ty):row) r others (RUnknown u) | not (occursCheck u (ty, row)) = do
614 u' <- fresh
615 cs <- unifyRows' o row r others (RUnknown u')
616 return (RowConstraint u (RCons name ty (RUnknown u')) o : cs)
617 unifyRows' _ [] REmpty [] REmpty = return []
618 unifyRows' _ [] (RowVar v1) [] (RowVar v2) | v1 == v2 = return []
619 unifyRows' _ sd1 r1 sd2 r2 = throwError $ "Cannot unify " ++ prettyPrintRow (rowFromList (sd1, r1)) ++ " with " ++ prettyPrintRow (rowFromList (sd2, r2)) ++ "."