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