module HOL.TypeVar
where
import qualified Data.Foldable as Foldable
import Data.Set (Set)
import qualified Data.Set as Set
import HOL.Name
import HOL.Data
mk :: Name -> TypeVar
mk :: Name -> TypeVar
mk = Name -> TypeVar
TypeVar
dest :: TypeVar -> Name
dest :: TypeVar -> Name
dest (TypeVar Name
n) = Name
n
eqName :: Name -> TypeVar -> Bool
eqName :: Name -> TypeVar -> Bool
eqName Name
n (TypeVar Name
m) = Name
m Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n
alpha :: TypeVar
alpha :: TypeVar
alpha = Name -> TypeVar
mk (String -> Name
mkGlobal String
"A")
beta :: TypeVar
beta :: TypeVar
beta = Name -> TypeVar
mk (String -> Name
mkGlobal String
"B")
class HasVars a where
vars :: a -> Set TypeVar
instance HasVars TypeVar where
vars :: TypeVar -> Set TypeVar
vars = TypeVar -> Set TypeVar
forall a. a -> Set a
Set.singleton
instance HasVars a => HasVars [a] where
vars :: [a] -> Set TypeVar
vars = (a -> Set TypeVar) -> [a] -> Set TypeVar
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars
instance HasVars a => HasVars (Set a) where
vars :: Set a -> Set TypeVar
vars = (a -> Set TypeVar) -> Set a -> Set TypeVar
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars
instance HasVars TypeData where
vars :: TypeData -> Set TypeVar
vars (VarType TypeVar
v) = TypeVar -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars TypeVar
v
vars (OpType TypeOp
_ [Type]
tys) = [Type] -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars [Type]
tys
instance HasVars Type where
vars :: Type -> Set TypeVar
vars (Type TypeData
_ TypeId
_ Size
_ Set TypeVar
vs) = Set TypeVar
vs
instance HasVars Var where
vars :: Var -> Set TypeVar
vars (Var Name
_ Type
ty) = Type -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Type
ty
instance HasVars TermData where
vars :: TermData -> Set TypeVar
vars (ConstTerm Const
_ Type
ty) = Type -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Type
ty
vars (VarTerm Var
v) = Var -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Var
v
vars (AppTerm Term
f Term
x) = Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Term
f) (Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Term
x)
vars (AbsTerm Var
v Term
b) = Set TypeVar -> Set TypeVar -> Set TypeVar
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Var -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Var
v) (Term -> Set TypeVar
forall a. HasVars a => a -> Set TypeVar
vars Term
b)
instance HasVars Term where
vars :: Term -> Set TypeVar
vars (Term TermData
_ TermId
_ Size
_ Type
_ Set TypeVar
vs Set Var
_) = Set TypeVar
vs