module Language.SequentCore.Syntax (
Value(..), Cont(..), Command(..), Bind(..), Alt(..), AltCon(..),
SeqCoreValue, SeqCoreCont, SeqCoreCommand, SeqCoreBind, SeqCoreBndr,
SeqCoreAlt,
mkCommand, valueCommand, varCommand, mkCompute, lambdas, addLets,
collectLambdas, collectArgs, collectTypeArgs, collectTypeAndOtherArgs,
partitionTypes, isLambda,
isTypeValue, isCoValue, isErasedValue, isRuntimeValue,
isTrivial, isTrivialValue, isTrivialCont, isReturnCont,
commandAsSaturatedCall, asSaturatedCall, asValueCommand,
valueArity, valueType, contOuterType, commandType,
contIdTag, isContId, asContId,
(=~=), AlphaEq(..), AlphaEnv, HasId(..)
) where
import Language.SequentCore.Pretty ()
import Coercion ( Coercion, coercionType, coercionKind )
import CoreSyn ( AltCon(..), Tickish, isRuntimeVar )
import DataCon ( DataCon, dataConRepType )
import Id ( Id, isDataConWorkId_maybe, idArity, idType
, idUnique, setIdUnique )
import Literal ( Literal, litIsTrivial, literalType )
import Outputable
import Pair ( pSnd )
import Type ( Type, KindOrType )
import qualified Type
import TysPrim
import Unique ( newTagUnique, unpkUnique )
import Var ( Var, isId )
import VarEnv
import Data.Maybe
data Value b = Lit Literal
| Var Id
| Lam b (Command b)
| Cons DataCon [Value b]
| Compute (Command b)
| Type Type
| Coercion Coercion
| Cont (Cont b)
data Cont b = App (Value b) (Cont b)
| Case b Type [Alt b] (Cont b)
| Cast Coercion (Cont b)
| Tick (Tickish Id) (Cont b)
| Jump ContId
| Return
type ContId = Id
data Command b = Command {
cmdLet :: [Bind b]
, cmdValue :: Value b
, cmdCont :: Cont b
}
data Bind b = NonRec b (Value b)
| Rec [(b, Value b)]
data Alt b = Alt AltCon [b] (Command b)
type SeqCoreBndr = Var
type SeqCoreValue = Value Var
type SeqCoreCont = Cont Var
type SeqCoreCommand = Command Var
type SeqCoreBind = Bind Var
type SeqCoreAlt = Alt Var
mkCommand :: [Bind b] -> Value b -> Cont b -> Command b
mkCommand binds val@(Var f) cont
| Just ctor <- isDataConWorkId_maybe f
, Just (args, cont') <- ctorCall
= mkCommand binds (Cons ctor args) cont'
where
ctorCall
| 0 <- idArity f
= Just ([], cont)
| otherwise
= asSaturatedCall val cont
mkCommand binds (Compute (Command { cmdLet = binds'
, cmdValue = val'
, cmdCont = Return {} })) cont
= mkCommand (binds ++ binds') val' cont
mkCommand binds val cont
= Command { cmdLet = binds, cmdValue = val, cmdCont = cont }
valueCommand :: Value b -> Command b
valueCommand (Compute c) = c
valueCommand v = Command { cmdLet = [], cmdValue = v, cmdCont = Return }
varCommand :: Id -> Command b
varCommand x = valueCommand (Var x)
mkCompute :: Command b -> Value b
mkCompute comm
| Just val <- asValueCommand comm
= val
| otherwise
= Compute comm
lambdas :: [b] -> Command b -> Value b
lambdas xs body = mkCompute $ foldr (\x c -> valueCommand (Lam x c)) body xs
addLets :: [Bind b] -> Command b -> Command b
addLets [] c = c
addLets bs c = c { cmdLet = bs ++ cmdLet c }
collectLambdas :: Value b -> ([b], Command b)
collectLambdas (Lam x c)
| Just v <- asValueCommand c
= let (xs, c') = collectLambdas v
in (x : xs, c')
| otherwise
= ([x], c)
collectLambdas v
= ([], valueCommand v)
collectArgs :: Cont b -> ([Value b], Cont b)
collectArgs (App v k)
= (v : vs, k')
where (vs, k') = collectArgs k
collectArgs k
= ([], k)
collectTypeArgs :: Cont b -> ([KindOrType], Cont b)
collectTypeArgs (App (Type ty) k)
= (ty : tys, k')
where (tys, k') = collectTypeArgs k
collectTypeArgs k
= ([], k)
collectTypeAndOtherArgs :: Cont b -> ([KindOrType], [Value b], Cont b)
collectTypeAndOtherArgs k
= let (tys, k') = collectTypeArgs k
(vs, k'') = collectArgs k'
in (tys, vs, k'')
partitionTypes :: [Value b] -> ([KindOrType], [Value b])
partitionTypes (Type ty : vs) = (ty : tys, vs')
where (tys, vs') = partitionTypes vs
partitionTypes vs = ([], vs)
isLambda :: Command b -> Bool
isLambda (Command { cmdLet = [], cmdCont = Return {}, cmdValue = Lam {} })
= True
isLambda _
= False
isTypeValue :: Value b -> Bool
isTypeValue (Type _) = True
isTypeValue _ = False
isCoValue :: Value b -> Bool
isCoValue (Coercion _) = True
isCoValue _ = False
isErasedValue :: Value b -> Bool
isErasedValue (Type _) = True
isErasedValue (Coercion _) = True
isErasedValue _ = False
isRuntimeValue :: Value b -> Bool
isRuntimeValue v = not (isErasedValue v)
isTrivial :: HasId b => Command b -> Bool
isTrivial c
= null (cmdLet c) &&
isTrivialCont (cmdCont c) &&
isTrivialValue (cmdValue c)
isTrivialValue :: HasId b => Value b -> Bool
isTrivialValue (Lit l) = litIsTrivial l
isTrivialValue (Lam x c) = not (isRuntimeVar (identifier x)) && isTrivial c
isTrivialValue (Compute _) = False
isTrivialValue (Cont k)
= case k of
Return -> True
Jump _ -> True
_ -> False
isTrivialValue _ = True
isTrivialCont :: Cont b -> Bool
isTrivialCont Return = True
isTrivialCont (Cast _ k) = isTrivialCont k
isTrivialCont (App v k) = isErasedValue v && isTrivialCont k
isTrivialCont _ = False
isReturnCont :: Cont b -> Bool
isReturnCont Return = True
isReturnCont _ = False
commandAsSaturatedCall :: Command b -> Maybe (Value b, [Value b], Cont b)
commandAsSaturatedCall c
= do
let val = cmdValue c
(args, cont) <- asSaturatedCall val (cmdCont c)
return $ (val, args, cont)
asSaturatedCall :: Value b -> Cont b -> Maybe ([Value b], Cont b)
asSaturatedCall val cont
| 0 < arity, arity <= length args
= Just (args, others)
| otherwise
= Nothing
where
arity = valueArity val
(args, others) = collectArgs cont
asValueCommand :: Command b -> Maybe (Value b)
asValueCommand (Command { cmdLet = [], cmdValue = v, cmdCont = Return })
= Just v
asValueCommand _
= Nothing
valueType :: SeqCoreValue -> Type
valueType (Lit l) = literalType l
valueType (Var x) = idType x
valueType (Lam b c) = idType b `Type.mkFunTy` commandType c
valueType (Cons con as) = res_ty
where
(tys, _) = partitionTypes as
(_, res_ty) = Type.splitFunTys (dataConRepType con `Type.applyTys` tys)
valueType (Compute c) = commandType c
valueType other = pprTrace "valueType" (ppr other) alphaTy
contOuterType :: Type -> SeqCoreCont -> Type
contOuterType ty k@App {} = contOuterType res_ty k'
where
(tys, _, k') = collectTypeAndOtherArgs k
(_, res_ty) = Type.splitFunTys (ty `Type.applyTys` tys)
contOuterType _ (Case _ ty _ k) = contOuterType ty k
contOuterType _ (Cast co k) = contOuterType (pSnd $ coercionKind co) k
contOuterType ty (Tick _ k) = contOuterType ty k
contOuterType _ (Jump x) = snd $ Type.splitFunTy (idType x)
contOuterType ty Return = ty
commandType :: SeqCoreCommand -> Type
commandType Command { cmdValue = v, cmdCont = k }
= contOuterType (valueType v) k
valueArity :: Value b -> Int
valueArity (Var x)
| isId x = idArity x
valueArity v
= let (xs, _) = collectLambdas v in length xs
contIdTag :: Char
contIdTag = 'Q'
isContId :: Id -> Bool
isContId x = tag == contIdTag where (tag, _) = unpkUnique (idUnique x)
asContId :: Id -> ContId
asContId x = x `setIdUnique` uniq'
where
uniq' = newTagUnique (idUnique x) contIdTag
class HasId a where
identifier :: a -> Id
instance HasId Var where
identifier x = x
type AlphaEnv = RnEnv2
infix 4 =~=, `aeq`
class AlphaEq a where
aeq :: a -> a -> Bool
aeqIn :: AlphaEnv -> a -> a -> Bool
aeq = aeqIn emptyAlphaEnv
emptyAlphaEnv :: AlphaEnv
emptyAlphaEnv = mkRnEnv2 emptyInScopeSet
(=~=) :: AlphaEq a => a -> a -> Bool
(=~=) = aeq
instance HasId b => AlphaEq (Value b) where
aeqIn _ (Lit l1) (Lit l2)
= l1 == l2
aeqIn env (Lam b1 c1) (Lam b2 c2)
= aeqIn (rnBndr2 env (identifier b1) (identifier b2)) c1 c2
aeqIn env (Type t1) (Type t2)
= aeqIn env t1 t2
aeqIn env (Coercion co1) (Coercion co2)
= aeqIn env co1 co2
aeqIn env (Var x1) (Var x2)
= env `rnOccL` x1 == env `rnOccR` x2
aeqIn env (Compute c1) (Compute c2)
= aeqIn env c1 c2
aeqIn env (Cont k1) (Cont k2)
= aeqIn env k1 k2
aeqIn _ _ _
= False
instance HasId b => AlphaEq (Cont b) where
aeqIn env (App c1 k1) (App c2 k2)
= aeqIn env c1 c2 && aeqIn env k1 k2
aeqIn env (Case x1 t1 as1 k1) (Case x2 t2 as2 k2)
= aeqIn env' t1 t2 && aeqIn env' as1 as2 && aeqIn env' k1 k2
where env' = rnBndr2 env (identifier x1) (identifier x2)
aeqIn env (Cast co1 k1) (Cast co2 k2)
= aeqIn env co1 co2 && aeqIn env k1 k2
aeqIn env (Tick ti1 k1) (Tick ti2 k2)
= ti1 == ti2 && aeqIn env k1 k2
aeqIn env (Jump x1) (Jump x2)
= env `rnOccL` x1 == env `rnOccR` x2
aeqIn _ Return Return
= True
aeqIn _ _ _
= False
instance HasId b => AlphaEq (Command b) where
aeqIn env
(Command { cmdLet = bs1, cmdValue = v1, cmdCont = c1 })
(Command { cmdLet = bs2, cmdValue = v2, cmdCont = c2 })
| Just env' <- aeqBindsIn env bs1 bs2
= aeqIn env' v1 v2 && aeqIn env' c1 c2
| otherwise
= False
aeqBindsIn :: HasId b => AlphaEnv -> [Bind b] -> [Bind b] -> Maybe AlphaEnv
aeqBindsIn env [] []
= Just env
aeqBindsIn env (b1:bs1) (b2:bs2)
= aeqBindIn env b1 b2 >>= \env' -> aeqBindsIn env' bs1 bs2
aeqBindsIn _ _ _
= Nothing
aeqBindIn :: HasId b => AlphaEnv -> Bind b -> Bind b -> Maybe AlphaEnv
aeqBindIn env (NonRec x1 c1) (NonRec x2 c2)
= if aeqIn env' c1 c2 then Just env' else Nothing
where env' = rnBndr2 env (identifier x1) (identifier x2)
aeqBindIn env (Rec bs1) (Rec bs2)
= if and $ zipWith alpha bs1 bs2 then Just env' else Nothing
where
alpha :: HasId b => (b, Value b) -> (b, Value b) -> Bool
alpha (_, c1) (_, c2)
= aeqIn env' c1 c2
env'
= rnBndrs2 env (map (identifier . fst) bs1) (map (identifier . fst) bs2)
aeqBindIn _ _ _
= Nothing
instance HasId b => AlphaEq (Alt b) where
aeqIn env (Alt a1 xs1 c1) (Alt a2 xs2 c2)
= a1 == a2 && aeqIn env' c1 c2
where
env' = rnBndrs2 env (map identifier xs1) (map identifier xs2)
instance AlphaEq Type where
aeqIn env t1 t2
| Just x1 <- Type.getTyVar_maybe t1
, Just x2 <- Type.getTyVar_maybe t2
= env `rnOccL` x1 == env `rnOccR` x2
| Just (f1, a1) <- Type.splitAppTy_maybe t1
, Just (f2, a2) <- Type.splitAppTy_maybe t2
= f1 `alpha` f2 && a1 `alpha` a2
| Just n1 <- Type.isNumLitTy t1
, Just n2 <- Type.isNumLitTy t2
= n1 == n2
| Just s1 <- Type.isStrLitTy t1
, Just s2 <- Type.isStrLitTy t2
= s1 == s2
| Just (a1, r1) <- Type.splitFunTy_maybe t1
, Just (a2, r2) <- Type.splitFunTy_maybe t2
= a1 `alpha` a2 && r1 `alpha` r2
| Just (c1, as1) <- Type.splitTyConApp_maybe t1
, Just (c2, as2) <- Type.splitTyConApp_maybe t2
= c1 == c2 && as1 `alpha` as2
| Just (x1, t1') <- Type.splitForAllTy_maybe t1
, Just (x2, t2') <- Type.splitForAllTy_maybe t2
= aeqIn (rnBndr2 env x1 x2) t1' t2'
| otherwise
= False
where
alpha a1 a2 = aeqIn env a1 a2
instance AlphaEq Coercion where
aeqIn env co1 co2 = aeqIn env (coercionType co1) (coercionType co2)
instance AlphaEq a => AlphaEq [a] where
aeqIn env xs ys = and $ zipWith (aeqIn env) xs ys
instance HasId b => AlphaEq (Bind b) where
aeqIn env b1 b2 = isJust $ aeqBindIn env b1 b2