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

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

module HOL.TypeData
where

import qualified Data.List as List
import Data.Maybe (isJust)

import HOL.Data

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

-- Variables

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

-- Operators

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

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

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

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