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