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 = TypeVar
dest :: TypeVar -> Name
dest (TypeVar n) = n
eqName :: Name -> TypeVar -> Bool
eqName n (TypeVar m) = m == n
alpha :: TypeVar
alpha = mk (mkGlobal "A")
beta :: TypeVar
beta = mk (mkGlobal "B")
class HasVars a where
vars :: a -> Set TypeVar
instance HasVars TypeVar where
vars = Set.singleton
instance HasVars a => HasVars [a] where
vars = Foldable.foldMap vars
instance HasVars a => HasVars (Set a) where
vars = Foldable.foldMap vars
instance HasVars TypeData where
vars (VarType v) = vars v
vars (OpType _ tys) = vars tys
instance HasVars Type where
vars (Type _ _ _ vs) = vs
instance HasVars Var where
vars (Var _ ty) = vars ty
instance HasVars TermData where
vars (ConstTerm _ ty) = vars ty
vars (VarTerm v) = vars v
vars (AppTerm f x) = Set.union (vars f) (vars x)
vars (AbsTerm v b) = Set.union (vars v) (vars b)
instance HasVars Term where
vars (Term _ _ _ _ vs _) = vs