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

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

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

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

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

-------------------------------------------------------------------------------
-- Free variables
-------------------------------------------------------------------------------

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

-------------------------------------------------------------------------------
-- Fresh variables
-------------------------------------------------------------------------------

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