{- |
module: $Header$
description: Higher order logic types
license: MIT

maintainer: Joe Leslie-Hurd <joe@gilith.com>
stability: provisional
portability: portable
-}

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

-------------------------------------------------------------------------------
-- Constructors and destructors
-------------------------------------------------------------------------------

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

-- Variables

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

-- Operators

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 is measured as the number of TypeData constructors
-------------------------------------------------------------------------------

size :: Type -> Size
size :: Type -> Size
size (Type TypeData
_ TypeId
_ Size
s Set TypeVar
_) = Size
s

-------------------------------------------------------------------------------
-- Type syntax
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Named type variables (used in standard axioms)
-------------------------------------------------------------------------------

alpha :: Type
alpha :: Type
alpha = TypeVar -> Type
mkVar TypeVar
TypeVar.alpha

beta :: Type
beta :: Type
beta = TypeVar -> Type
mkVar TypeVar
TypeVar.beta

-------------------------------------------------------------------------------
-- Primitive types
-------------------------------------------------------------------------------

-- Booleans

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

-- Function spaces

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)

-- Individuals

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

-------------------------------------------------------------------------------
-- Types of primitive constants
-------------------------------------------------------------------------------

-- Equality

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

-- Hilbert's choice operator

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