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