module HOL.Var
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 -> Type -> Var
mk :: Name -> Type -> Var
mk = Name -> Type -> Var
Var
dest :: Var -> (Name,Type)
dest :: Var -> (Name, Type)
dest (Var Name
n Type
ty) = (Name
n,Type
ty)
name :: Var -> Name
name :: Var -> Name
name (Var Name
n Type
_) = Name
n
typeOf :: Var -> Type
typeOf :: Var -> Type
typeOf (Var Name
_ Type
ty) = Type
ty
class HasFree a where
free :: a -> Set Var
freeIn :: Var -> a -> Bool
freeIn Var
v a
x = Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v (a -> Set Var
forall a. HasFree a => a -> Set Var
free a
x)
notFreeIn :: Var -> a -> Bool
notFreeIn Var
v a
x = Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember Var
v (a -> Set Var
forall a. HasFree a => a -> Set Var
free a
x)
closed :: a -> Bool
closed = Set Var -> Bool
forall a. Set a -> Bool
Set.null (Set Var -> Bool) -> (a -> Set Var) -> a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set Var
forall a. HasFree a => a -> Set Var
free
instance HasFree Var where
free :: Var -> Set Var
free = Var -> Set Var
forall a. a -> Set a
Set.singleton
instance HasFree a => HasFree [a] where
free :: [a] -> Set Var
free = (a -> Set Var) -> [a] -> Set Var
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set Var
forall a. HasFree a => a -> Set Var
free
instance HasFree a => HasFree (Set a) where
free :: Set a -> Set Var
free = (a -> Set Var) -> Set a -> Set Var
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
Foldable.foldMap a -> Set Var
forall a. HasFree a => a -> Set Var
free
instance HasFree TermData where
free :: TermData -> Set Var
free (ConstTerm Const
_ Type
_) = Set Var
forall a. Set a
Set.empty
free (VarTerm Var
v) = Var -> Set Var
forall a. HasFree a => a -> Set Var
free Var
v
free (AppTerm Term
f Term
x) = Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
Set.union (Term -> Set Var
forall a. HasFree a => a -> Set Var
free Term
f) (Term -> Set Var
forall a. HasFree a => a -> Set Var
free Term
x)
free (AbsTerm Var
v Term
b) =
if Var -> Set Var -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Var
v Set Var
bf then Var -> Set Var -> Set Var
forall a. Ord a => a -> Set a -> Set a
Set.delete Var
v Set Var
bf else Set Var
bf
where
bf :: Set Var
bf = Term -> Set Var
forall a. HasFree a => a -> Set Var
free Term
b
instance HasFree Term where
free :: Term -> Set Var
free (Term TermData
_ TermId
_ Size
_ Type
_ Set TypeVar
_ Set Var
vs) = Set Var
vs
renameAvoiding :: Set Name -> Var -> Var
renameAvoiding :: Set Name -> Var -> Var
renameAvoiding Set Name
avoid Var
v =
if Name
n' Name -> Name -> Bool
forall a. Eq a => a -> a -> Bool
== Name
n then Var
v else Name -> Type -> Var
Var Name
n' Type
ty
where
Var Name
n Type
ty = Var
v
n' :: Name
n' = Set Name -> Name -> Name
variantAvoiding Set Name
avoid Name
n