module HOL.Type
where
import Data.Maybe (isJust)
import System.IO.Unsafe (unsafePerformIO)
import System.Mem.StableName (makeStableName)
import HOL.Data
import qualified HOL.TypeData as TypeData
import qualified HOL.TypeOp as TypeOp
import qualified HOL.TypeVar as TypeVar
dest :: Type -> TypeData
dest :: Type -> TypeData
dest (Type TypeData
d TypeId
_ Size
_ Set TypeVar
_) = TypeData
d
mk :: TypeData -> Type
mk :: TypeData -> Type
mk TypeData
d =
TypeData -> TypeId -> Size -> Set TypeVar -> Type
Type TypeData
d TypeId
i Size
sz Set TypeVar
vs
where
i :: TypeId
i = IO TypeId -> TypeId
forall a. IO a -> a
unsafePerformIO (TypeData -> IO TypeId
forall a. a -> IO (StableName a)
makeStableName (TypeData -> IO TypeId) -> TypeData -> IO TypeId
forall a b. (a -> b) -> a -> b
$! TypeData
d)
sz :: Size
sz = TypeData -> Size
TypeData.size TypeData
d
vs :: Set TypeVar
vs = TypeData -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
TypeVar.vars TypeData
d
mkVar :: TypeVar -> Type
mkVar :: TypeVar -> Type
mkVar = TypeData -> Type
mk (TypeData -> Type) -> (TypeVar -> TypeData) -> TypeVar -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeVar -> TypeData
TypeData.mkVar
destVar :: Type -> Maybe TypeVar
destVar :: Type -> Maybe TypeVar
destVar = TypeData -> Maybe TypeVar
TypeData.destVar (TypeData -> Maybe TypeVar)
-> (Type -> TypeData) -> Type -> Maybe TypeVar
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
isVar :: Type -> Bool
isVar :: Type -> Bool
isVar = Maybe TypeVar -> Bool
forall a. Maybe a -> Bool
isJust (Maybe TypeVar -> Bool) -> (Type -> Maybe TypeVar) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe TypeVar
destVar
eqVar :: TypeVar -> Type -> Bool
eqVar :: TypeVar -> Type -> Bool
eqVar TypeVar
v = TypeVar -> TypeData -> Bool
TypeData.eqVar TypeVar
v (TypeData -> Bool) -> (Type -> TypeData) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
mkOp :: TypeOp -> [Type] -> Type
mkOp :: TypeOp -> [Type] -> Type
mkOp TypeOp
t = TypeData -> Type
mk (TypeData -> Type) -> ([Type] -> TypeData) -> [Type] -> Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> [Type] -> TypeData
TypeData.mkOp TypeOp
t
destOp :: Type -> Maybe (TypeOp,[Type])
destOp :: Type -> Maybe (TypeOp, [Type])
destOp = TypeData -> Maybe (TypeOp, [Type])
TypeData.destOp (TypeData -> Maybe (TypeOp, [Type]))
-> (Type -> TypeData) -> Type -> Maybe (TypeOp, [Type])
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
isOp :: Type -> Bool
isOp :: Type -> Bool
isOp = Maybe (TypeOp, [Type]) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (TypeOp, [Type]) -> Bool)
-> (Type -> Maybe (TypeOp, [Type])) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (TypeOp, [Type])
destOp
destGivenOp :: TypeOp -> Type -> Maybe [Type]
destGivenOp :: TypeOp -> Type -> Maybe [Type]
destGivenOp TypeOp
t = TypeOp -> TypeData -> Maybe [Type]
TypeData.destGivenOp TypeOp
t (TypeData -> Maybe [Type])
-> (Type -> TypeData) -> Type -> Maybe [Type]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
isGivenOp :: TypeOp -> Type -> Bool
isGivenOp :: TypeOp -> Type -> Bool
isGivenOp TypeOp
t = Maybe [Type] -> Bool
forall a. Maybe a -> Bool
isJust (Maybe [Type] -> Bool) -> (Type -> Maybe [Type]) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> Type -> Maybe [Type]
destGivenOp TypeOp
t
size :: Type -> Size
size :: Type -> Size
size (Type TypeData
_ TypeId
_ Size
s Set TypeVar
_) = Size
s
isNullaryOp :: TypeOp -> Type -> Bool
isNullaryOp :: TypeOp -> Type -> Bool
isNullaryOp TypeOp
t = TypeOp -> TypeData -> Bool
TypeData.isNullaryOp TypeOp
t (TypeData -> Bool) -> (Type -> TypeData) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
destUnaryOp :: TypeOp -> Type -> Maybe Type
destUnaryOp :: TypeOp -> Type -> Maybe Type
destUnaryOp TypeOp
t = TypeOp -> TypeData -> Maybe Type
TypeData.destUnaryOp TypeOp
t (TypeData -> Maybe Type)
-> (Type -> TypeData) -> Type -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
isUnaryOp :: TypeOp -> Type -> Bool
isUnaryOp :: TypeOp -> Type -> Bool
isUnaryOp TypeOp
t = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> Type -> Maybe Type
destUnaryOp TypeOp
t
destBinaryOp :: TypeOp -> Type -> Maybe (Type,Type)
destBinaryOp :: TypeOp -> Type -> Maybe (Type, Type)
destBinaryOp TypeOp
t = TypeOp -> TypeData -> Maybe (Type, Type)
TypeData.destBinaryOp TypeOp
t (TypeData -> Maybe (Type, Type))
-> (Type -> TypeData) -> Type -> Maybe (Type, Type)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> TypeData
dest
isBinaryOp :: TypeOp -> Type -> Bool
isBinaryOp :: TypeOp -> Type -> Bool
isBinaryOp TypeOp
t = Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Type) -> Bool)
-> (Type -> Maybe (Type, Type)) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeOp -> Type -> Maybe (Type, Type)
destBinaryOp TypeOp
t
alpha :: Type
alpha :: Type
alpha = TypeVar -> Type
mkVar TypeVar
TypeVar.alpha
beta :: Type
beta :: Type
beta = TypeVar -> Type
mkVar TypeVar
TypeVar.beta
bool :: Type
bool :: Type
bool = TypeOp -> [Type] -> Type
mkOp TypeOp
TypeOp.bool []
isBool :: Type -> Bool
isBool :: Type -> Bool
isBool = TypeOp -> Type -> Bool
isNullaryOp TypeOp
TypeOp.bool
mkPred :: Type -> Type
mkPred :: Type -> Type
mkPred Type
a = Type -> Type -> Type
mkFun Type
a Type
bool
destPred :: Type -> Maybe Type
destPred :: Type -> Maybe Type
destPred Type
ty = do
(Type
a,Type
b) <- Type -> Maybe (Type, Type)
destFun Type
ty
if Type -> Bool
isBool Type
b then Type -> Maybe Type
forall a. a -> Maybe a
Just Type
a else Maybe Type
forall a. Maybe a
Nothing
isPred :: Type -> Bool
isPred :: Type -> Bool
isPred = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
destPred
mkRel :: Type -> Type -> Type
mkRel :: Type -> Type -> Type
mkRel Type
a Type
b = Type -> Type -> Type
mkFun Type
a (Type -> Type) -> Type -> Type
forall a b. (a -> b) -> a -> b
$ Type -> Type
mkPred Type
b
destRel :: Type -> Maybe (Type,Type)
destRel :: Type -> Maybe (Type, Type)
destRel Type
ty = do
(Type
a,Type
p) <- Type -> Maybe (Type, Type)
destFun Type
ty
Type
b <- Type -> Maybe Type
destPred Type
p
(Type, Type) -> Maybe (Type, Type)
forall (m :: * -> *) a. Monad m => a -> m a
return (Type
a,Type
b)
isRel :: Type -> Bool
isRel :: Type -> Bool
isRel = Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Type) -> Bool)
-> (Type -> Maybe (Type, Type)) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type)
destRel
mkFun :: Type -> Type -> Type
mkFun :: Type -> Type -> Type
mkFun Type
d Type
r = TypeOp -> [Type] -> Type
mkOp TypeOp
TypeOp.fun [Type
d,Type
r]
destFun :: Type -> Maybe (Type,Type)
destFun :: Type -> Maybe (Type, Type)
destFun = TypeOp -> Type -> Maybe (Type, Type)
destBinaryOp TypeOp
TypeOp.fun
isFun :: Type -> Bool
isFun :: Type -> Bool
isFun = Maybe (Type, Type) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Type, Type) -> Bool)
-> (Type -> Maybe (Type, Type)) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type)
destFun
domain :: Type -> Maybe Type
domain :: Type -> Maybe Type
domain = ((Type, Type) -> Type) -> Maybe (Type, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type, Type) -> Type
forall a b. (a, b) -> a
fst (Maybe (Type, Type) -> Maybe Type)
-> (Type -> Maybe (Type, Type)) -> Type -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type)
destFun
range :: Type -> Maybe Type
range :: Type -> Maybe Type
range = ((Type, Type) -> Type) -> Maybe (Type, Type) -> Maybe Type
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Type, Type) -> Type
forall a b. (a, b) -> b
snd (Maybe (Type, Type) -> Maybe Type)
-> (Type -> Maybe (Type, Type)) -> Type -> Maybe Type
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe (Type, Type)
destFun
listMkFun :: [Type] -> Type -> Type
listMkFun :: [Type] -> Type -> Type
listMkFun [Type]
tys Type
ty = (Type -> Type -> Type) -> Type -> [Type] -> Type
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Type -> Type -> Type
mkFun Type
ty [Type]
tys
stripFun :: Type -> ([Type],Type)
stripFun :: Type -> ([Type], Type)
stripFun Type
ty =
case Type -> Maybe (Type, Type)
destFun Type
ty of
Maybe (Type, Type)
Nothing -> ([],Type
ty)
Just (Type
d,Type
r) -> let ([Type]
ds,Type
rb) = Type -> ([Type], Type)
stripFun Type
r in (Type
d Type -> [Type] -> [Type]
forall a. a -> [a] -> [a]
: [Type]
ds, Type
rb)
ind :: Type
ind :: Type
ind = TypeOp -> [Type] -> Type
mkOp TypeOp
TypeOp.ind []
isInd :: Type -> Bool
isInd :: Type -> Bool
isInd = TypeOp -> Type -> Bool
isNullaryOp TypeOp
TypeOp.ind
mkEq :: Type -> Type
mkEq :: Type -> Type
mkEq Type
a = Type -> Type -> Type
mkRel Type
a Type
a
destEq :: Type -> Maybe Type
destEq :: Type -> Maybe Type
destEq Type
ty = do
(Type
a,Type
b) <- Type -> Maybe (Type, Type)
destRel Type
ty
if Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
b then Type -> Maybe Type
forall a. a -> Maybe a
Just Type
a else Maybe Type
forall a. Maybe a
Nothing
isEq :: Type -> Bool
isEq :: Type -> Bool
isEq = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
destEq
mkSelect :: Type -> Type
mkSelect :: Type -> Type
mkSelect Type
a = Type -> Type -> Type
mkFun (Type -> Type -> Type
mkFun Type
a Type
bool) Type
a
destSelect :: Type -> Maybe Type
destSelect :: Type -> Maybe Type
destSelect Type
ty = do
(Type
p,Type
a) <- Type -> Maybe (Type, Type)
destFun Type
ty
Type
b <- Type -> Maybe Type
destPred Type
p
if Type
a Type -> Type -> Bool
forall a. Eq a => a -> a -> Bool
== Type
b then Type -> Maybe Type
forall a. a -> Maybe a
Just Type
a else Maybe Type
forall a. Maybe a
Nothing
isSelect :: Type -> Bool
isSelect :: Type -> Bool
isSelect = Maybe Type -> Bool
forall a. Maybe a -> Bool
isJust (Maybe Type -> Bool) -> (Type -> Maybe Type) -> Type -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Type -> Maybe Type
destSelect