module HOL.TypeData
where
import qualified Data.List as List
import Data.Maybe (isJust)
import HOL.Data
mkVar :: TypeVar -> TypeData
mkVar :: TypeVar -> TypeData
mkVar = TypeVar -> TypeData
VarType
destVar :: TypeData -> Maybe TypeVar
destVar :: TypeData -> Maybe TypeVar
destVar (VarType TypeVar
v) = TypeVar -> Maybe TypeVar
forall a. a -> Maybe a
Just TypeVar
v
destVar TypeData
_ = Maybe TypeVar
forall a. Maybe a
Nothing
isVar :: TypeData -> Bool
isVar :: TypeData -> Bool
isVar = Maybe TypeVar -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TypeVar -> Bool)
-> (TypeData -> Maybe TypeVar) -> TypeData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeData -> Maybe TypeVar
destVar
eqVar :: TypeVar -> TypeData -> Bool
eqVar :: TypeVar -> TypeData -> Bool
eqVar TypeVar
v TypeData
d =
case TypeData -> Maybe TypeVar
destVar TypeData
d of
Just TypeVar
w -> TypeVar
w TypeVar -> TypeVar -> Bool
forall a. Eq a => a -> a -> Bool
== TypeVar
v
Maybe TypeVar
Nothing -> Bool
False
mkOp :: TypeOp -> [Type] -> TypeData
mkOp :: TypeOp -> [Type] -> TypeData
mkOp = TypeOp -> [Type] -> TypeData
OpType
destOp :: TypeData -> Maybe (TypeOp,[Type])
destOp :: TypeData -> Maybe (TypeOp, [Type])
destOp (OpType TypeOp
t [Type]
tys) = (TypeOp, [Type]) -> Maybe (TypeOp, [Type])
forall a. a -> Maybe a
Just (TypeOp
t,[Type]
tys)
destOp TypeData
_ = Maybe (TypeOp, [Type])
forall a. Maybe a
Nothing
isOp :: TypeData -> Bool
isOp :: TypeData -> Bool
isOp = Maybe (TypeOp, [Type]) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (TypeOp, [Type]) -> Bool)
-> (TypeData -> Maybe (TypeOp, [Type])) -> TypeData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeData -> Maybe (TypeOp, [Type])
destOp
destGivenOp :: TypeOp -> TypeData -> Maybe [Type]
destGivenOp :: TypeOp -> TypeData -> Maybe [Type]
destGivenOp TypeOp
t TypeData
d =
case TypeData -> Maybe (TypeOp, [Type])
destOp TypeData
d of
Just (TypeOp
u,[Type]
tys) -> if TypeOp
u TypeOp -> TypeOp -> Bool
forall a. Eq a => a -> a -> Bool
== TypeOp
t then [Type] -> Maybe [Type]
forall a. a -> Maybe a
Just [Type]
tys else Maybe [Type]
forall a. Maybe a
Nothing
Maybe (TypeOp, [Type])
Nothing -> Maybe [Type]
forall a. Maybe a
Nothing
isGivenOp :: TypeOp -> TypeData -> Bool
isGivenOp :: TypeOp -> TypeData -> Bool
isGivenOp TypeOp
t = Maybe [Type] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [Type] -> Bool)
-> (TypeData -> Maybe [Type]) -> TypeData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> TypeData -> Maybe [Type]
destGivenOp TypeOp
t
size :: TypeData -> Size
size :: TypeData -> Size
size (VarType TypeVar
_) = Size
1
size (OpType TypeOp
_ [Type]
tys) =
(Size -> Type -> Size) -> Size -> [Type] -> Size
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Size -> Type -> Size
add Size
1 [Type]
tys
where
add :: Size -> Type -> Size
add Size
n (Type TypeData
_ TypeId
_ Size
s Set TypeVar
_) = Size
n Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
s
isNullaryOp :: TypeOp -> TypeData -> Bool
isNullaryOp :: TypeOp -> TypeData -> Bool
isNullaryOp TypeOp
t TypeData
d =
case TypeOp -> TypeData -> Maybe [Type]
destGivenOp TypeOp
t TypeData
d of
Just [Type]
tys -> [Type] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Type]
tys
Maybe [Type]
Nothing -> Bool
False
destUnaryOp :: TypeOp -> TypeData -> Maybe Type
destUnaryOp :: TypeOp -> TypeData -> Maybe Type
destUnaryOp TypeOp
t TypeData
d =
case TypeOp -> TypeData -> Maybe [Type]
destGivenOp TypeOp
t TypeData
d of
Just [Type
ty] -> Type -> Maybe Type
forall a. a -> Maybe a
Just Type
ty
Maybe [Type]
_ -> Maybe Type
forall a. Maybe a
Nothing
isUnaryOp :: TypeOp -> TypeData -> Bool
isUnaryOp :: TypeOp -> TypeData -> Bool
isUnaryOp TypeOp
t = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool)
-> (TypeData -> Maybe Type) -> TypeData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> TypeData -> Maybe Type
destUnaryOp TypeOp
t
destBinaryOp :: TypeOp -> TypeData -> Maybe (Type,Type)
destBinaryOp :: TypeOp -> TypeData -> Maybe (Type, Type)
destBinaryOp TypeOp
t TypeData
d =
case TypeOp -> TypeData -> Maybe [Type]
destGivenOp TypeOp
t TypeData
d of
Just [Type
ty0,Type
ty1] -> (Type, Type) -> Maybe (Type, Type)
forall a. a -> Maybe a
Just (Type
ty0,Type
ty1)
Maybe [Type]
_ -> Maybe (Type, Type)
forall a. Maybe a
Nothing
isBinaryOp :: TypeOp -> TypeData -> Bool
isBinaryOp :: TypeOp -> TypeData -> Bool
isBinaryOp TypeOp
t = Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Type) -> Bool)
-> (TypeData -> Maybe (Type, Type)) -> TypeData -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> TypeData -> Maybe (Type, Type)
destBinaryOp TypeOp
t