2013-04-08 00:55:34 +00:00
|
|
|
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
|
2013-02-04 10:56:22 +00:00
|
|
|
module Types.Substitutions (subst,
|
|
|
|
occurs,
|
|
|
|
freeVars,
|
|
|
|
concretize,
|
|
|
|
rescheme,
|
2013-04-08 00:55:34 +00:00
|
|
|
generalize,
|
|
|
|
superize) where
|
2012-08-09 14:38:18 +00:00
|
|
|
|
2013-02-06 11:04:55 +00:00
|
|
|
import Ast
|
2013-05-29 23:20:38 +00:00
|
|
|
import Located
|
2013-04-08 00:55:34 +00:00
|
|
|
import Control.Monad (liftM, liftM2)
|
|
|
|
import Control.Monad.State (runState, State, get, put)
|
2013-04-10 02:50:56 +00:00
|
|
|
import Data.List (nub)
|
2012-08-09 14:38:18 +00:00
|
|
|
import qualified Data.Set as Set
|
2012-12-25 08:39:18 +00:00
|
|
|
import qualified Data.Map as Map
|
2012-08-09 14:38:18 +00:00
|
|
|
import Guid
|
2013-04-10 02:50:56 +00:00
|
|
|
import Types.Types
|
2012-08-09 14:38:18 +00:00
|
|
|
|
2012-11-29 06:16:08 +00:00
|
|
|
class Subst a where
|
|
|
|
subst :: [(X,Type)] -> a -> a
|
|
|
|
|
|
|
|
instance Subst Type where
|
2012-12-25 08:39:18 +00:00
|
|
|
subst ss t =
|
|
|
|
case t of
|
|
|
|
VarT x -> case lookup x ss of
|
|
|
|
Nothing -> VarT x
|
|
|
|
Just (Super _) -> VarT x
|
|
|
|
Just t -> t
|
|
|
|
LambdaT t1 t2 -> LambdaT (subst ss t1) (subst ss t2)
|
|
|
|
ADT name ts -> ADT name (subst ss ts)
|
|
|
|
RecordT fs t -> RecordT (Map.map (subst ss) fs) (subst ss t)
|
|
|
|
EmptyRecord -> EmptyRecord
|
|
|
|
Super ts -> Super ts
|
2012-11-29 06:16:08 +00:00
|
|
|
|
|
|
|
instance Subst Scheme where
|
|
|
|
subst ss (Forall vs cs t) = Forall vs (subst ss cs) (subst ss t)
|
|
|
|
|
|
|
|
instance Subst Constraint where
|
|
|
|
subst ss (t1 :=: t2) = subst ss t1 :=: subst ss t2
|
|
|
|
subst ss (t :<: super) = subst ss t :<: super
|
|
|
|
subst ss (x :<<: poly) = x :<<: subst ss poly
|
|
|
|
|
2013-05-29 23:20:38 +00:00
|
|
|
instance Subst a => Subst (Located a) where
|
|
|
|
subst ss (L str span c) = L str span (subst ss c)
|
2012-11-29 06:16:08 +00:00
|
|
|
|
|
|
|
instance Subst a => Subst [a] where
|
|
|
|
subst ss as = map (subst ss) as
|
2012-08-09 14:38:18 +00:00
|
|
|
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2012-11-29 06:16:08 +00:00
|
|
|
class FreeVars a where
|
|
|
|
freeVars :: a -> [X]
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2012-11-29 06:16:08 +00:00
|
|
|
instance FreeVars Type where
|
2013-04-08 00:55:34 +00:00
|
|
|
freeVars t =
|
|
|
|
case t of
|
|
|
|
VarT v -> [v]
|
|
|
|
LambdaT t1 t2 -> freeVars t1 ++ freeVars t2
|
|
|
|
ADT _ ts -> concatMap freeVars ts
|
|
|
|
RecordT fs t -> freeVars (concat $ Map.elems fs) ++ freeVars t
|
|
|
|
EmptyRecord -> []
|
|
|
|
Super _ -> []
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2012-11-29 06:16:08 +00:00
|
|
|
instance FreeVars Constraint where
|
|
|
|
freeVars (t1 :=: t2) = freeVars t1 ++ freeVars t2
|
|
|
|
freeVars (t1 :<: t2) = freeVars t1 ++ freeVars t2
|
|
|
|
freeVars (x :<<: Forall xs cs t) = filter (`notElem` xs) frees
|
|
|
|
where frees = concatMap freeVars cs ++ freeVars t
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2013-05-29 23:20:38 +00:00
|
|
|
instance FreeVars a => FreeVars (Located a) where
|
|
|
|
freeVars (L _ _ c) = freeVars c
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2012-12-25 08:39:18 +00:00
|
|
|
instance FreeVars a => FreeVars [a] where
|
|
|
|
freeVars = concatMap freeVars
|
2012-10-18 09:19:09 +00:00
|
|
|
|
2013-01-03 08:28:54 +00:00
|
|
|
occurs x t = x `elem` freeVars t
|
2012-11-29 06:16:08 +00:00
|
|
|
|
2013-05-29 23:20:38 +00:00
|
|
|
concretize :: Scheme -> GuidCounter (Type, [Located Constraint])
|
2012-11-29 06:16:08 +00:00
|
|
|
concretize (Forall xs cs t) = do
|
|
|
|
ss <- zip xs `liftM` mapM (\_ -> liftM VarT guid) xs
|
|
|
|
return (subst ss t, subst ss cs)
|
|
|
|
|
|
|
|
rescheme :: Scheme -> GuidCounter Scheme
|
|
|
|
rescheme (Forall xs cs t) = do
|
|
|
|
xs' <- mapM (const guid) xs
|
|
|
|
let ss = zip xs (map VarT xs')
|
|
|
|
return $ Forall xs' (subst ss cs) (subst ss t)
|
2012-08-09 14:38:18 +00:00
|
|
|
|
|
|
|
generalize :: [X] -> Scheme -> GuidCounter Scheme
|
|
|
|
generalize exceptions (Forall xs cs t) = rescheme (Forall (xs ++ frees) cs t)
|
2012-11-29 06:16:08 +00:00
|
|
|
where allFrees = Set.fromList $ freeVars t ++ concatMap freeVars cs
|
2012-08-09 14:38:18 +00:00
|
|
|
frees = Set.toList $ Set.difference allFrees (Set.fromList exceptions)
|
2013-04-08 00:55:34 +00:00
|
|
|
|
2013-04-10 02:50:56 +00:00
|
|
|
newtype Superize a = S { runSuper :: State ([X], [X], [X]) a }
|
2013-04-08 00:55:34 +00:00
|
|
|
deriving (Monad)
|
|
|
|
|
|
|
|
superize :: String -> Type -> GuidCounter Scheme
|
|
|
|
superize name tipe =
|
2013-04-10 02:50:56 +00:00
|
|
|
do constraints <- liftM concat $
|
|
|
|
sequence [ mapM (<: nmbr) (nub ns)
|
|
|
|
, mapM (<: apnd) (nub as)
|
|
|
|
, mapM (<: comp) (nub cs) ]
|
|
|
|
return (Forall (concat [ns,as,cs]) constraints tipe')
|
2013-04-08 00:55:34 +00:00
|
|
|
where
|
2013-04-10 02:50:56 +00:00
|
|
|
(tipe', (ns,as,cs)) = runState (runSuper (go tipe)) ([],[],[])
|
|
|
|
t <: super = do x <- guid
|
2013-05-29 23:20:38 +00:00
|
|
|
return $ L (Just name) NoSpan (VarT t :<: super x)
|
2013-04-10 02:50:56 +00:00
|
|
|
|
|
|
|
nmbr t = number
|
|
|
|
apnd t = appendable t
|
|
|
|
comp t = comparable t
|
|
|
|
|
2013-04-08 00:55:34 +00:00
|
|
|
go :: Type -> Superize Type
|
|
|
|
go t =
|
|
|
|
case t of
|
|
|
|
EmptyRecord -> return t
|
|
|
|
Super _ -> return t
|
|
|
|
VarT _ -> return t
|
2013-04-08 08:48:30 +00:00
|
|
|
LambdaT t1 t2 -> liftM2 LambdaT (go t1) (go t2)
|
2013-04-10 02:50:56 +00:00
|
|
|
ADT "Number" [VarT t] -> addNumber t
|
|
|
|
ADT "Appendable" [VarT t] -> addAppendable t
|
|
|
|
ADT "Comparable" [VarT t] -> addComparable t
|
2013-04-08 08:48:30 +00:00
|
|
|
ADT name ts -> liftM (ADT name) (mapM go ts)
|
|
|
|
RecordT fs t -> liftM2 RecordT fs' (go t)
|
2013-04-08 00:55:34 +00:00
|
|
|
where pairs = Map.toList fs
|
|
|
|
fs' = do ps <- mapM (\(f,t) -> liftM ((,) f) (mapM go t)) pairs
|
|
|
|
return (Map.fromList ps)
|
|
|
|
|
2013-04-10 02:50:56 +00:00
|
|
|
add :: (X -> ([X],[X],[X]) -> ([X],[X],[X])) -> X -> Superize Type
|
|
|
|
add f v = S $ do (ns, as, cs) <- get
|
|
|
|
put $ f v (ns, as, cs)
|
|
|
|
return (VarT v)
|
|
|
|
|
|
|
|
addNumber = add (\n (ns,as,cs) -> (n:ns,as,cs))
|
|
|
|
addAppendable = add (\a (ns,as,cs) -> (ns,a:as,cs))
|
|
|
|
addComparable = add (\c (ns,as,cs) -> (ns,as,c:cs))
|