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