module DDC.Type.Check.Context
( Mode (..)
, Exists (..)
, typeOfExists
, takeExists
, Elem (..)
, Role (..)
, Context (..)
, emptyContext
, Pos (..)
, markContext
, popToPos
, pushType, pushTypes, memberType
, pushKind, pushKinds, memberKind, memberKindBind
, pushExists
, lookupType
, lookupKind
, lookupExistsEq
, locationOfExists
, updateExists
, applyContextEither
, applySolvedEither
, effectSupported
, liftTypes
, lowerTypes)
where
import DDC.Type.Exp
import DDC.Type.Pretty
import DDC.Type.Transform.BoundT
import DDC.Type.Equiv
import DDC.Type.Compounds
import DDC.Base.Pretty ()
import Data.Maybe
import qualified DDC.Type.Sum as Sum
import qualified Data.IntMap.Strict as IntMap
import Data.IntMap.Strict (IntMap)
import qualified Data.Set as Set
import Data.Set (Set)
import Prelude hiding ((<$>))
data Mode n
= Recon
| Synth
| Check (Type n)
deriving (Show, Eq)
instance (Eq n, Pretty n) => Pretty (Mode n) where
ppr mode
= case mode of
Recon -> text "RECON"
Synth -> text "SYNTH"
Check t -> text "CHECK" <+> parens (ppr t)
data Exists n
= Exists !Int !(Kind n)
deriving (Show)
instance Eq (Exists n) where
(==) (Exists i1 _) (Exists i2 _) = i1 == i2
(/=) (Exists i1 _) (Exists i2 _) = i1 /= i2
instance Ord (Exists n) where
compare (Exists i1 _) (Exists i2 _)
= compare i1 i2
instance Pretty (Exists n) where
ppr (Exists i _) = text "?" <> ppr i
typeOfExists :: Exists n -> Type n
typeOfExists (Exists n k)
= TCon (TyConExists n k)
takeExists :: Type n -> Maybe (Exists n)
takeExists tt
= case tt of
TCon (TyConExists n k) -> Just (Exists n k)
_ -> Nothing
data Context n
= Context
{
contextGenPos :: !Int
, contextGenExists :: !Int
, contextElems :: ![Elem n]
, contextSolved :: IntMap (Type n) }
deriving Show
instance (Pretty n, Eq n) => Pretty (Context n) where
ppr (Context genPos genExists ls _solved)
= text "Context "
<$> text " genPos = " <> int genPos
<$> text " genExists = " <> int genExists
<$> indent 2
(vcat $ [int i <> (indent 4 $ ppr l)
| l <- reverse ls
| i <- [0..]])
data Pos
= Pos !Int
deriving (Show, Eq)
instance Pretty Pos where
ppr (Pos p)
= text "*" <> int p
data Elem n
= ElemPos !Pos
| ElemKind !(Bind n) !Role
| ElemType !(Bind n)
| ElemExistsDecl !(Exists n)
| ElemExistsEq !(Exists n) !(Type n)
deriving (Show, Eq)
data Role
= RoleConcrete
| RoleAbstract
deriving (Show, Eq)
instance (Pretty n, Eq n) => Pretty (Elem n) where
ppr ll
= case ll of
ElemPos p
-> ppr p
ElemKind b role
-> ppr (binderOfBind b)
<+> text "::"
<+> (ppr $ typeOfBind b)
<+> text "@" <> ppr role
ElemType b
-> ppr (binderOfBind b)
<+> text "::"
<+> (ppr $ typeOfBind b)
ElemExistsDecl i
-> ppr i
ElemExistsEq i t
-> ppr i <+> text "=" <+> ppr t
instance Pretty Role where
ppr role
= case role of
RoleConcrete -> text "Concrete"
RoleAbstract -> text "Abstract"
emptyContext :: Context n
emptyContext
= Context 0 0 [] IntMap.empty
pushType :: Bind n -> Context n -> Context n
pushType b ctx
= ctx { contextElems = ElemType b : contextElems ctx }
pushTypes :: [Bind n] -> Context n -> Context n
pushTypes bs ctx
= foldl (flip pushType) ctx bs
pushKind :: Bind n -> Role -> Context n -> Context n
pushKind b role ctx
= ctx { contextElems = ElemKind b role : contextElems ctx }
pushKinds :: [(Bind n, Role)] -> Context n -> Context n
pushKinds brs ctx
= foldl (\ctx' (b, r) -> pushKind b r ctx') ctx brs
pushExists :: Exists n -> Context n -> Context n
pushExists i ctx
= ctx { contextElems = ElemExistsDecl i : contextElems ctx }
markContext :: Context n -> (Context n, Pos)
markContext ctx
= let p = contextGenPos ctx
pos = Pos p
in ( ctx { contextGenPos = p + 1
, contextElems = ElemPos pos : contextElems ctx }
, pos )
popToPos :: Pos -> Context n -> Context n
popToPos pos ctx
= ctx { contextElems = go $ contextElems ctx }
where
go [] = []
go (ElemPos pos' : ls)
| pos' == pos = ls
| otherwise = go ls
go (_ : ls) = go ls
lookupType :: Eq n => Bound n -> Context n -> Maybe (Type n)
lookupType u ctx
= case u of
UPrim{} -> Nothing
UName n -> goName n (contextElems ctx)
UIx ix -> goIx ix 0 (contextElems ctx)
where
goName _n [] = Nothing
goName n (ElemType (BName n' t) : ls)
| n == n' = Just t
| otherwise = goName n ls
goName n (_ : ls)
= goName n ls
goIx _ix _d [] = Nothing
goIx ix d (ElemType (BAnon t) : ls)
| ix == d = Just t
| otherwise = goIx ix (d + 1) ls
goIx ix d (_ : ls)
= goIx ix d ls
lookupKind :: Eq n => Bound n -> Context n -> Maybe (Kind n, Role)
lookupKind u ctx
= case u of
UPrim{} -> Nothing
UName n -> goName n (contextElems ctx)
UIx ix -> goIx ix 0 (contextElems ctx)
where
goName _n [] = Nothing
goName n (ElemKind (BName n' t) role : ls)
| n == n' = Just (t, role)
| otherwise = goName n ls
goName n (_ : ls)
= goName n ls
goIx _ix _d [] = Nothing
goIx ix d (ElemKind (BAnon t) role : ls)
| ix == d = Just (t, role)
| otherwise = goIx ix (d + 1) ls
goIx ix d (_ : ls)
= goIx ix d ls
lookupExistsEq :: Exists n -> Context n -> Maybe (Type n)
lookupExistsEq i ctx
= go (contextElems ctx)
where go [] = Nothing
go (ElemExistsEq i' t : _)
| i == i' = Just t
go (_ : ls) = go ls
memberType :: Eq n => Bound n -> Context n -> Bool
memberType u ctx = isJust $ lookupType u ctx
memberKind :: Eq n => Bound n -> Context n -> Bool
memberKind u ctx = isJust $ lookupKind u ctx
memberKindBind :: Eq n => Bind n -> Context n -> Bool
memberKindBind b ctx
= case b of
BName n _ -> memberKind (UName n) ctx
_ -> False
locationOfExists
:: Exists n
-> Context n
-> Maybe Int
locationOfExists x ctx
= go 0 (contextElems ctx)
where go !_ix [] = Nothing
go !ix (ElemExistsDecl x' : moar)
| x == x' = Just ix
| otherwise = go (ix + 1) moar
go !ix (ElemExistsEq x' _ : moar)
| x == x' = Just ix
| otherwise = go (ix + 1) moar
go !ix (_ : moar)
= go (ix + 1) moar
updateExists
:: [Exists n]
-> Exists n
-> Type n
-> Context n
-> Maybe (Context n)
updateExists isMore iEx@(Exists iEx' _) tEx ctx
= case go $ contextElems ctx of
Just elems'
-> Just $ ctx { contextElems = elems'
, contextSolved = IntMap.insert iEx' tEx (contextSolved ctx) }
Nothing -> Nothing
where
go ll
= case ll of
l@ElemPos{} : ls
| Just ls' <- go ls -> Just (l : ls')
l@ElemKind{} : ls
| Just ls' <- go ls -> Just (l : ls')
l@ElemType{} : ls
| Just ls' <- go ls -> Just (l : ls')
l@(ElemExistsDecl i) : ls
| i == iEx
-> Just $ (ElemExistsEq i tEx : [ElemExistsDecl n' | n' <- isMore]) ++ ls
| Just ls' <- go ls -> Just (l : ls')
l@ElemExistsEq{} : ls
| Just ls' <- go ls -> Just (l : ls')
_ -> Just ll
liftTypes :: Ord n => Int -> Context n -> Context n
liftTypes n ctx
= ctx { contextElems = go $ contextElems ctx }
where
go [] = []
go (ElemType b : ls) = ElemType (liftT n b) : go ls
go (l:ls) = l : go ls
lowerTypes :: Ord n => Int -> Context n -> Context n
lowerTypes n ctx
= ctx { contextElems = go $ contextElems ctx }
where
go [] = []
go (ElemType b : ls) = ElemType (lowerT n b) : go ls
go (l:ls) = l : go ls
applyContextEither
:: Ord n
=> Context n
-> Set Int
-> Type n
-> Either (Type n, Type n) (Type n)
applyContextEither ctx is tt
= case tt of
TVar{}
-> return tt
TCon (TyConExists i k)
| Just t <- lookupExistsEq (Exists i k) ctx
-> if Set.member i is
then Left (tt, t)
else applyContextEither ctx (Set.insert i is) t
TCon{}
-> return tt
TForall b t
-> do tb' <- applySolvedEither ctx is (typeOfBind b)
let b' = replaceTypeOfBind tb' b
t' <- applySolvedEither ctx is t
return $ TForall b' t'
TApp t1 t2
-> do t1' <- applySolvedEither ctx is t1
t2' <- applySolvedEither ctx is t2
return $ TApp t1' t2'
TSum ts
-> do tss' <- mapM (applyContextEither ctx is)
$ Sum.toList ts
return $ TSum
$ Sum.fromList (Sum.kindOfSum ts) tss'
applySolvedEither
:: Ord n
=> Context n
-> Set Int
-> Type n
-> Either (Type n, Type n) (Type n)
applySolvedEither ctx is tt
= case tt of
TVar{}
-> return tt
TCon (TyConExists i k)
| Just t <- IntMap.lookup i (contextSolved ctx)
-> if Set.member i is
then Left (tt, t)
else applySolvedEither ctx (Set.insert i is) t
| Just t <- lookupExistsEq (Exists i k) ctx
-> if Set.member i is
then Left (tt, t)
else applySolvedEither ctx (Set.insert i is) t
TCon {}
-> return tt
TForall b t
-> do tb' <- applySolvedEither ctx is (typeOfBind b)
let b' = replaceTypeOfBind tb' b
t' <- applySolvedEither ctx is t
return $ TForall b' t'
TApp t1 t2
-> do t1' <- applySolvedEither ctx is t1
t2' <- applySolvedEither ctx is t2
return $ TApp t1' t2'
TSum ts
-> do tss' <- mapM (applySolvedEither ctx is)
$ Sum.toList ts
return $ TSum
$ Sum.fromList (Sum.kindOfSum ts) tss'
effectSupported
:: (Ord n, Show n)
=> Effect n
-> Context n
-> Maybe (Effect n)
effectSupported eff ctx
| TSum ts <- eff
= listToMaybe $ concat [ maybeToList $ effectSupported e ctx
| e <- Sum.toList ts ]
| TVar {} <- eff
= Nothing
| TCon (TyConBound _ k) <- eff
, k == kEffect
= Nothing
| TApp (TCon (TyConSpec tc)) _t2 <- eff
, elem tc [TcConRead, TcConWrite, TcConAlloc]
, any (\b -> equivT (typeOfBind b) eff)
[ b | ElemType b <- contextElems ctx ]
= Nothing
| TApp (TCon (TyConSpec tc)) (TVar u) <- eff
, elem tc [TcConRead, TcConWrite, TcConAlloc]
= case lookupKind u ctx of
Just (_, RoleConcrete) -> Just eff
Just (_, RoleAbstract) -> Nothing
Nothing -> Nothing
| otherwise
= Just eff