@@ -1,610 +0,0 @@
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−-----------------------------------------------------------------------------
14−
15−{-# LANGUAGE DeriveDataTypeable #-}
16−
17−module PureScript.TypeChecker.Types (
18− TypeConstraint(..),
19− TypeSolution(..),
20− typeOf
21−) where
22−
23−import Data.List
24−import Data.Function
25−import qualified Data.Data as D
26−import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
27−
28−import PureScript.Values
29−import PureScript.Types
30−import PureScript.Kinds
31−import PureScript.Names
32−import PureScript.TypeChecker.Monad
33−import PureScript.TypeChecker.Kinds
34−import PureScript.TypeChecker.Synonyms
35−import PureScript.CodeGen.Pretty.Types
36−import PureScript.CodeGen.Pretty.Kinds
37−import PureScript.CodeGen.Pretty.Values
38−
39−import Control.Monad.State
40−import Control.Monad.Error
41−
42−import Control.Applicative
43−import Control.Arrow (Kleisli(..), (***), (&&&))
44−import qualified Control.Category as C
45−
46−import qualified Data.Map as M
47−
48−data TypeConstraintOrigin
49− = ValueOrigin Value
50− | BinderOrigin Binder
51− | AssignmentTargetOrigin AssignmentTarget deriving (Show, D.Data, D.Typeable)
52−
53−prettyPrintOrigin :: TypeConstraintOrigin -> String
54−prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
55−prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
56−prettyPrintOrigin (AssignmentTargetOrigin assign) = prettyPrintAssignmentTarget assign
57−
58−data TypeConstraint
59− = TypeConstraint Int Type TypeConstraintOrigin
60− | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
61−
62−newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
63−
64−emptyTypeSolution :: TypeSolution
65−emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
66−
67−typeOf :: Ident -> Value -> Check PolyType
68−typeOf 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
80−
81−allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
82−allUnknownsBecameQuantified 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
97−
98−findUnknownTypes :: (D.Data d) => d -> [Int]
99−findUnknownTypes = everything (++) (mkQ [] f)
100− where
101− f :: Type -> [Int]
102− f (TUnknown n) = [n]
103− f _ = []
104−
105−findTypeVars :: (D.Data d) => d -> [String]
106−findTypeVars = everything (++) (mkQ [] f)
107− where
108− f :: Type -> [String]
109− f (TypeVar v) = [v]
110− f _ = []
111−
112−findUnknownRows :: (D.Data d) => d -> [Int]
113−findUnknownRows = everything (++) (mkQ [] f)
114− where
115− f :: Row -> [Int]
116− f (RUnknown n) = [n]
117− f _ = []
118−
119−varIfUnknown :: Type -> PolyType
120−varIfUnknown 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
146−
147−replaceTypeVars :: M.Map String Type -> Type -> Type
148−replaceTypeVars 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
154−
155−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
156−replaceVarsWithUnknowns 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
178−
179−replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
180−replaceAllTypeSynonyms 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
184−
185−desaturateAllTypeSynonyms :: (D.Data d) => d -> d
186−desaturateAllTypeSynonyms = everywhere (mkT $ replace)
187− where
188− replace (SaturatedTypeSynonym name args) = foldl (\t arg -> TypeApp t arg) (TypeConstructor name) args
189− replace t = t
190−
191−replaceType :: (D.Data d) => Int -> Type -> d -> d
192−replaceType n t = everywhere (mkT go)
193− where
194− go (TUnknown m) | m == n = t
195− go t = t
196−
197−replaceRow :: (D.Data d) => Int -> Row -> d -> d
198−replaceRow n r = everywhere (mkT go)
199− where
200− go (RUnknown m) | m == n = r
201− go r = r
202−
203−typeOccursCheck :: Int -> Type -> Check ()
204−typeOccursCheck u (TUnknown _) = return ()
205−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
206−
207−rowOccursCheck :: Int -> Row -> Check ()
208−rowOccursCheck u (RUnknown _) = return ()
209−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
210−
211−occursCheck :: (D.Data d) => Int -> d -> Bool
212−occursCheck 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
218−
219−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
220−typeConstraints _ v@(NumericLiteral _) = do
221− me <- fresh
222− return ([TypeConstraint me Number (ValueOrigin v)], me)
223−typeConstraints _ v@(StringLiteral _) = do
224− me <- fresh
225− return ([TypeConstraint me String (ValueOrigin v)], me)
226−typeConstraints _ v@(BooleanLiteral _) = do
227− me <- fresh
228− return ([TypeConstraint me Boolean (ValueOrigin v)], me)
229−typeConstraints 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)
234−typeConstraints m u@(Unary op val) = do
235− (cs, n1) <- typeConstraints m val
236− me <- fresh
237− return (cs ++ unaryOperatorConstraints u op n1 me, me)
238−typeConstraints 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)
243−typeConstraints 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)
252−typeConstraints 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)
257−typeConstraints 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)
262−typeConstraints 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)
268−typeConstraints 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)
274−typeConstraints 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)
287−typeConstraints 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)
292−typeConstraints 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)
300−typeConstraints 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)
305−typeConstraints 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)
310−typeConstraints 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)
315−
316−unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
317−unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
318−unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
319−unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
320−
321−binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
322−binaryOperatorConstraints v Add = symBinOpConstraints v Number
323−binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
324−binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
325−binaryOperatorConstraints v Divide = symBinOpConstraints v Number
326−binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
327−binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
328−binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
329−binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
330−binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
331−binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
332−binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
333−binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
334−binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
335−binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
336−binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
337−binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
338−binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
339−binaryOperatorConstraints v And = symBinOpConstraints v Boolean
340−binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
341−binaryOperatorConstraints v Concat = symBinOpConstraints v String
342−
343−equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
344−equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
345−
346−symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
347−symBinOpConstraints v ty left right result = asymBinOpConstraints v ty ty left right result
348−
349−asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
350−asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
351−
352−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
353−typeConstraintsForBinder _ NullBinder = return ([], M.empty)
354−typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
355−typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
356−typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
357−typeConstraintsForBinder val b@(VarBinder name) = do
358− me <- fresh
359− return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
360−typeConstraintsForBinder 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"
367−typeConstraintsForBinder 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"
377−typeConstraintsForBinder 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)
390−typeConstraintsForBinder 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)
400−typeConstraintsForBinder 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)
404−typeConstraintsForBinder 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)
408−
409−constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
410−constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
411−
412−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
413−typeConstraintsForBinders _ _ _ [] = return []
414−typeConstraintsForBinders 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)
419−
420−assignVariable :: Ident -> M.Map Ident Int -> Check ()
421−assignVariable name m =
422− case M.lookup name m of
423− Nothing -> return ()
424− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
425−
426−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
427−typeConstraintsForStatement 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)
431−typeConstraintsForStatement 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)
435−typeConstraintsForStatement 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)
439−typeConstraintsForStatement m mass ret (If ifst) = do
440− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
441− return $ (cs, allCodePathsReturn, mass)
442−typeConstraintsForStatement 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)
449−typeConstraintsForStatement 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)
457−typeConstraintsForStatement 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)
460−
461−typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
462−typeConstraintsForIfStatement 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)
466−typeConstraintsForIfStatement 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)
471−
472−typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
473−typeConstraintsForElseStatement m mass ret (Else elses) = do
474− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
475− return (cs, allCodePathsReturn)
476−typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
477− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
478− return (cs, allCodePathsReturn)
479−
480−typeConstraintsForAssignmentTarget :: M.Map Ident Int -> M.Map Ident Int -> Int -> AssignmentTarget -> Check [TypeConstraint]
481−typeConstraintsForAssignmentTarget 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)]
486−typeConstraintsForAssignmentTarget 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
491−typeConstraintsForAssignmentTarget 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
496−
497−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
498−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
499−typeConstraintsForBlock 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)
507−
508−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
509−solveTypeConstraints [] s = return s
510−solveTypeConstraints 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'
518−solveTypeConstraints (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'
526−
527−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
528−substituteTypeInConstraint n s (TypeConstraint m t v)
529− | n == m = unifyTypes v s t
530− | otherwise = return [TypeConstraint m (replaceType n s t) v]
531−substituteTypeInConstraint n s (RowConstraint m r v)
532− = return [RowConstraint m (replaceType n s r) v]
533−
534−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
535−substituteRowInConstraint n r (TypeConstraint m t v)
536− = return [TypeConstraint m (replaceRow n r t) v]
537−substituteRowInConstraint n r (RowConstraint m r1 v)
538− | m == n = unifyRows v r r1
539− | otherwise = return [RowConstraint m (replaceRow n r r1) v]
540−
541−unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
542−unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
543−unifyTypes o (TUnknown u) t = do
544− typeOccursCheck u t
545− return [TypeConstraint u t o]
546−unifyTypes o t (TUnknown u) = do
547− typeOccursCheck u t
548− return [TypeConstraint u t o]
549−unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
550− fmap concat $ zipWithM (unifyTypes o) args1 args2
551−unifyTypes 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"
559−unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
560−unifyTypes _ Number Number = return []
561−unifyTypes _ String String = return []
562−unifyTypes _ Boolean Boolean = return []
563−unifyTypes o (Array s) (Array t) = unifyTypes o s t
564−unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
565−unifyTypes 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
570−unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
571−unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
572−unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
573− cs1 <- unifyTypes o t1 t3
574− cs2 <- unifyTypes o t2 t4
575− return $ cs1 ++ cs2
576−unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
577−
578−unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
579−unifyRows 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))