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

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

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

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

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

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

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")

-------------------------------------------------------------------------------
-- Collecting type variables
-------------------------------------------------------------------------------

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