@@ -1,619 +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 Debug.Trace
24−
25−import Data.List
26−import Data.Function
27−import qualified Data.Data as D
28−import Data.Generics (everywhere, everywhereM, everything, mkT, mkM, mkQ, extM, extQ)
29−
30−import PureScript.Values
31−import PureScript.Types
32−import PureScript.Kinds
33−import PureScript.Names
34−import PureScript.TypeChecker.Monad
35−import PureScript.TypeChecker.Kinds
36−import PureScript.TypeChecker.Synonyms
37−import PureScript.CodeGen.Pretty.Types
38−import PureScript.CodeGen.Pretty.Kinds
39−import PureScript.CodeGen.Pretty.Values
40−
41−import Control.Monad.State
42−import Control.Monad.Error
43−
44−import Control.Applicative
45−import Control.Arrow (Kleisli(..), (***), (&&&))
46−import qualified Control.Category as C
47−
48−import qualified Data.Map as M
49−
50−data TypeConstraintOrigin
51− = ValueOrigin Value
52− | BinderOrigin Binder
53− | AssignmentTargetOrigin Ident deriving (Show, D.Data, D.Typeable)
54−
55−prettyPrintOrigin :: TypeConstraintOrigin -> String
56−prettyPrintOrigin (ValueOrigin val) = prettyPrintValue val
57−prettyPrintOrigin (BinderOrigin binder) = prettyPrintBinder binder
58−prettyPrintOrigin (AssignmentTargetOrigin ident) = show ident
59−
60−data TypeConstraint
61− = TypeConstraint Int Type TypeConstraintOrigin
62− | RowConstraint Int Row TypeConstraintOrigin deriving (Show, D.Data, D.Typeable)
63−
64−newtype TypeSolution = TypeSolution { runTypeSolution :: (Int -> Type, Int -> Row) }
65−
66−emptyTypeSolution :: TypeSolution
67−emptyTypeSolution = TypeSolution (TUnknown, RUnknown)
68−
69−typeOf :: Ident -> Value -> Check PolyType
70−typeOf 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
82−
83−allUnknownsBecameQuantified :: [TypeConstraint] -> TypeSolution -> Type -> Check ()
84−allUnknownsBecameQuantified 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
99−
100−setify :: Row -> Row
101−setify = rowFromList . (M.toList . M.fromList *** id) . rowToList
102−
103−setifyAll :: (D.Data d) => d -> d
104−setifyAll = everywhere (mkT setify)
105−
106−findUnknownTypes :: (D.Data d) => d -> [Int]
107−findUnknownTypes = everything (++) (mkQ [] f)
108− where
109− f :: Type -> [Int]
110− f (TUnknown n) = [n]
111− f _ = []
112−
113−findTypeVars :: (D.Data d) => d -> [String]
114−findTypeVars = everything (++) (mkQ [] f)
115− where
116− f :: Type -> [String]
117− f (TypeVar v) = [v]
118− f _ = []
119−
120−findUnknownRows :: (D.Data d) => d -> [Int]
121−findUnknownRows = everything (++) (mkQ [] f)
122− where
123− f :: Row -> [Int]
124− f (RUnknown n) = [n]
125− f _ = []
126−
127−varIfUnknown :: Type -> PolyType
128−varIfUnknown 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
154−
155−replaceTypeVars :: M.Map String Type -> Type -> Type
156−replaceTypeVars 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
162−
163−replaceVarsWithUnknowns :: [String] -> Type -> Check Type
164−replaceVarsWithUnknowns 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
186−
187−replaceAllTypeSynonyms :: (D.Data d) => d -> Check d
188−replaceAllTypeSynonyms 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
192−
193−desaturateAllTypeSynonyms :: (D.Data d) => d -> d
194−desaturateAllTypeSynonyms = everywhere (mkT $ replace)
195− where
196− replace (SaturatedTypeSynonym name args) = foldl (\t arg -> TypeApp t arg) (TypeConstructor name) args
197− replace t = t
198−
199−replaceType :: (D.Data d) => Int -> Type -> d -> d
200−replaceType n t = everywhere (mkT go)
201− where
202− go (TUnknown m) | m == n = t
203− go t = t
204−
205−replaceRow :: (D.Data d) => Int -> Row -> d -> d
206−replaceRow n r = everywhere (mkT go)
207− where
208− go (RUnknown m) | m == n = r
209− go r = r
210−
211−typeOccursCheck :: Int -> Type -> Check ()
212−typeOccursCheck u (TUnknown _) = return ()
213−typeOccursCheck u t = when (occursCheck u t) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintType t
214−
215−rowOccursCheck :: Int -> Row -> Check ()
216−rowOccursCheck u (RUnknown _) = return ()
217−rowOccursCheck u r = when (occursCheck u r) $ throwError $ "Occurs check failed: " ++ show u ++ " = " ++ prettyPrintRow r
218−
219−occursCheck :: (D.Data d) => Int -> d -> Bool
220−occursCheck 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
226−
227−typesToRow :: [(String, Type)] -> Row
228−typesToRow [] = REmpty
229−typesToRow ((name, ty):tys) = RCons name ty (typesToRow tys)
230−
231−rowToList :: Row -> ([(String, Type)], Row)
232−rowToList (RCons name ty row) = let (tys, rest) = rowToList row
233− in ((name, ty):tys, rest)
234−rowToList r = ([], r)
235−
236−rowFromList :: ([(String, Type)], Row) -> Row
237−rowFromList ([], r) = r
238−rowFromList ((name, t):ts, r) = RCons name t (rowFromList (ts, r))
239−
240−ensureNoDuplicateProperties :: [(String, Value)] -> Check ()
241−ensureNoDuplicateProperties ps = guardWith "Duplicate property names" $ length (nub . map fst $ ps) == length ps
242−
243−typeConstraints :: M.Map Ident Int -> Value -> Check ([TypeConstraint], Int)
244−typeConstraints _ v@(NumericLiteral _) = do
245− me <- fresh
246− return ([TypeConstraint me Number (ValueOrigin v)], me)
247−typeConstraints _ v@(StringLiteral _) = do
248− me <- fresh
249− return ([TypeConstraint me String (ValueOrigin v)], me)
250−typeConstraints _ v@(BooleanLiteral _) = do
251− me <- fresh
252− return ([TypeConstraint me Boolean (ValueOrigin v)], me)
253−typeConstraints 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)
258−typeConstraints m u@(Unary op val) = do
259− (cs, n1) <- typeConstraints m val
260− me <- fresh
261− return (cs ++ unaryOperatorConstraints u op n1 me, me)
262−typeConstraints 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)
267−typeConstraints 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)
274−typeConstraints 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)
282−typeConstraints 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)
287−typeConstraints 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)
292−typeConstraints 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)
298−typeConstraints 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)
304−typeConstraints 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)
317−typeConstraints 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)
322−typeConstraints 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)
330−typeConstraints 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)
335−typeConstraints 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)
340−typeConstraints 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)
345−
346−unaryOperatorConstraints :: Value -> UnaryOperator -> Int -> Int -> [TypeConstraint]
347−unaryOperatorConstraints v Negate val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
348−unaryOperatorConstraints v Not val result = [TypeConstraint val Boolean (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
349−unaryOperatorConstraints v BitwiseNot val result = [TypeConstraint val Number (ValueOrigin v), TypeConstraint result Number (ValueOrigin v)]
350−
351−binaryOperatorConstraints :: Value -> BinaryOperator -> Int -> Int -> Int -> [TypeConstraint]
352−binaryOperatorConstraints v Add = symBinOpConstraints v Number
353−binaryOperatorConstraints v Subtract = symBinOpConstraints v Number
354−binaryOperatorConstraints v Multiply = symBinOpConstraints v Number
355−binaryOperatorConstraints v Divide = symBinOpConstraints v Number
356−binaryOperatorConstraints v Modulus = symBinOpConstraints v Number
357−binaryOperatorConstraints v LessThan = asymBinOpConstraints v Number Boolean
358−binaryOperatorConstraints v LessThanOrEqualTo = asymBinOpConstraints v Number Boolean
359−binaryOperatorConstraints v GreaterThan = asymBinOpConstraints v Number Boolean
360−binaryOperatorConstraints v GreaterThanOrEqualTo = asymBinOpConstraints v Number Boolean
361−binaryOperatorConstraints v BitwiseAnd = symBinOpConstraints v Number
362−binaryOperatorConstraints v BitwiseOr = symBinOpConstraints v Number
363−binaryOperatorConstraints v BitwiseXor = symBinOpConstraints v Number
364−binaryOperatorConstraints v ShiftLeft = symBinOpConstraints v Number
365−binaryOperatorConstraints v ShiftRight = symBinOpConstraints v Number
366−binaryOperatorConstraints v ZeroFillShiftRight = symBinOpConstraints v Number
367−binaryOperatorConstraints v EqualTo = equalityBinOpConstraints v
368−binaryOperatorConstraints v NotEqualTo = equalityBinOpConstraints v
369−binaryOperatorConstraints v And = symBinOpConstraints v Boolean
370−binaryOperatorConstraints v Or = symBinOpConstraints v Boolean
371−binaryOperatorConstraints v Concat = symBinOpConstraints v String
372−
373−equalityBinOpConstraints :: Value -> Int -> Int -> Int -> [TypeConstraint]
374−equalityBinOpConstraints v left right result = [TypeConstraint left (TUnknown right) (ValueOrigin v), TypeConstraint result Boolean (ValueOrigin v)]
375−
376−symBinOpConstraints :: Value -> Type -> Int -> Int -> Int -> [TypeConstraint]
377−symBinOpConstraints v ty left right result = asymBinOpConstraints v ty ty left right result
378−
379−asymBinOpConstraints :: Value -> Type -> Type -> Int -> Int -> Int -> [TypeConstraint]
380−asymBinOpConstraints v ty res left right result = [TypeConstraint left ty (ValueOrigin v), TypeConstraint right ty (ValueOrigin v), TypeConstraint result res (ValueOrigin v)]
381−
382−typeConstraintsForBinder :: Int -> Binder -> Check ([TypeConstraint], M.Map Ident Int)
383−typeConstraintsForBinder _ NullBinder = return ([], M.empty)
384−typeConstraintsForBinder val b@(StringBinder _) = constantBinder b val String
385−typeConstraintsForBinder val b@(NumberBinder _) = constantBinder b val Number
386−typeConstraintsForBinder val b@(BooleanBinder _) = constantBinder b val Boolean
387−typeConstraintsForBinder val b@(VarBinder name) = do
388− me <- fresh
389− return ([TypeConstraint me (TUnknown val) (BinderOrigin b)], M.singleton name me)
390−typeConstraintsForBinder 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"
397−typeConstraintsForBinder 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"
407−typeConstraintsForBinder 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)
420−typeConstraintsForBinder 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)
430−typeConstraintsForBinder 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)
434−typeConstraintsForBinder 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)
438−
439−constantBinder :: Binder -> Int -> Type -> Check ([TypeConstraint], M.Map Ident Int)
440−constantBinder b val ty = return ([TypeConstraint val ty (BinderOrigin b)], M.empty)
441−
442−typeConstraintsForBinders :: M.Map Ident Int -> Int -> Int -> [(Binder, Value)] -> Check [TypeConstraint]
443−typeConstraintsForBinders _ _ _ [] = return []
444−typeConstraintsForBinders 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)
449−
450−assignVariable :: Ident -> M.Map Ident Int -> Check ()
451−assignVariable name m =
452− case M.lookup name m of
453− Nothing -> return ()
454− Just _ -> throwError $ "Variable with name " ++ show name ++ " already exists."
455−
456−typeConstraintsForStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> Statement -> Check ([TypeConstraint], Bool, M.Map Ident Int)
457−typeConstraintsForStatement 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)
461−typeConstraintsForStatement 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)
467−typeConstraintsForStatement 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)
471−typeConstraintsForStatement m mass ret (If ifst) = do
472− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
473− return $ (cs, allCodePathsReturn, mass)
474−typeConstraintsForStatement 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)
481−typeConstraintsForStatement 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)
489−typeConstraintsForStatement 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)
492−
493−typeConstraintsForIfStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> IfStatement -> Check ([TypeConstraint], Bool)
494−typeConstraintsForIfStatement 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)
498−typeConstraintsForIfStatement 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)
503−
504−typeConstraintsForElseStatement :: M.Map Ident Int -> M.Map Ident Int -> Int -> ElseStatement -> Check ([TypeConstraint], Bool)
505−typeConstraintsForElseStatement m mass ret (Else elses) = do
506− (cs, allCodePathsReturn, _) <- typeConstraintsForBlock m mass ret elses
507− return (cs, allCodePathsReturn)
508−typeConstraintsForElseStatement m mass ret (ElseIf ifst) = do
509− (cs, allCodePathsReturn) <- typeConstraintsForIfStatement m mass ret ifst
510− return (cs, allCodePathsReturn)
511−
512−typeConstraintsForBlock :: M.Map Ident Int -> M.Map Ident Int -> Int -> [Statement] -> Check ([TypeConstraint], Bool, M.Map Ident Int)
513−typeConstraintsForBlock _ mass _ [] = return ([], False, mass)
514−typeConstraintsForBlock 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)
522−
523−solveTypeConstraints :: [TypeConstraint] -> TypeSolution -> Check TypeSolution
524−solveTypeConstraints [] s = return s
525−solveTypeConstraints 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'
533−solveTypeConstraints (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'
541−
542−substituteTypeInConstraint :: Int -> Type -> TypeConstraint -> Check [TypeConstraint]
543−substituteTypeInConstraint n s (TypeConstraint m t v)
544− | n == m = unifyTypes v s t
545− | otherwise = return [TypeConstraint m (replaceType n s t) v]
546−substituteTypeInConstraint n s (RowConstraint m r v)
547− = return [RowConstraint m (replaceType n s r) v]
548−
549−substituteRowInConstraint :: Int -> Row -> TypeConstraint -> Check [TypeConstraint]
550−substituteRowInConstraint n r (TypeConstraint m t v)
551− = return [TypeConstraint m (replaceRow n r t) v]
552−substituteRowInConstraint n r (RowConstraint m r1 v)
553− | m == n = unifyRows v r r1
554− | otherwise = return [RowConstraint m (replaceRow n r r1) v]
555−
556−unifyTypes :: TypeConstraintOrigin -> Type -> Type -> Check [TypeConstraint]
557−unifyTypes _ (TUnknown u1) (TUnknown u2) | u1 == u2 = return []
558−unifyTypes o (TUnknown u) t = do
559− typeOccursCheck u t
560− return [TypeConstraint u t o]
561−unifyTypes o t (TUnknown u) = do
562− typeOccursCheck u t
563− return [TypeConstraint u t o]
564−unifyTypes o (SaturatedTypeSynonym name1 args1) (SaturatedTypeSynonym name2 args2) | name1 == name2 =
565− fmap concat $ zipWithM (unifyTypes o) args1 args2
566−unifyTypes 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"
574−unifyTypes o ty s@(SaturatedTypeSynonym _ _) = unifyTypes o s ty
575−unifyTypes _ Number Number = return []
576−unifyTypes _ String String = return []
577−unifyTypes _ Boolean Boolean = return []
578−unifyTypes o (Array s) (Array t) = unifyTypes o s t
579−unifyTypes o (Object row1) (Object row2) = unifyRows o row1 row2
580−unifyTypes 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
585−unifyTypes _ (TypeVar v1) (TypeVar v2) | v1 == v2 = return []
586−unifyTypes _ (TypeConstructor c1) (TypeConstructor c2) | c1 == c2 = return []
587−unifyTypes o (TypeApp t1 t2) (TypeApp t3 t4) = do
588− cs1 <- unifyTypes o t1 t3
589− cs2 <- unifyTypes o t2 t4
590− return $ cs1 ++ cs2
591−unifyTypes _ t1 t2 = throwError $ "Cannot unify " ++ prettyPrintType t1 ++ " with " ++ prettyPrintType t2 ++ "."
592−
593−unifyRows :: TypeConstraintOrigin -> Row -> Row -> Check [TypeConstraint]
594−unifyRows 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)) ++ "."