module Zabt.Internal.Term where
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe (fromMaybe)
import Zabt.Arity
import Zabt.Visits
import Zabt.Internal.Index
import Zabt.Internal.Nameless
data Term v f a
= Term
{ free :: Set v
, project :: Nameless v f (Term v f) a
}
type Flat v f = Term v f G
freeVars :: Term v f a -> Set v
freeVars = free
embed :: (Ord v, Visits f) => Nameless v f (Term v f) a -> Term v f a
embed nls = case nls of
Free v -> Term (Set.singleton v) nls
Bound i -> Term Set.empty nls
Pattern f -> Term (vfoldMap free f) nls
Abstraction v nls' -> Term (free nls') nls
instance (Show v, Show (Nameless v f (Term v f) a)) => Show (Term v f a) where
showsPrec p t = showsPrec p (project t)
deriving instance (Eq v, Eq (f (Term v f))) => Eq (Term v f G)
deriving instance (Eq v, Eq (f (Term v f)), Eq (Term v f a)) => Eq (Term v f (B a))
deriving instance (Ord v, Ord (f (Term v f))) => Ord (Term v f G)
deriving instance (Ord v, Ord (f (Term v f)), Ord (Term v f a)) => Ord (Term v f (B a))
var :: (Visits f, Ord v) => v -> Flat v f
var v = embed (Free v)
abstract :: forall v f a . (Visits f, Ord v) => v -> Term v f a -> Term v f a
abstract name = go zero where
go :: forall a . Index -> Term v f a -> Term v f a
go idx t
| not (Set.member name (free t)) = t
| otherwise =
Term (Set.delete name (free t)) $ case project t of
Free v
| v == name -> Bound idx
| otherwise -> Free v
Bound{} -> project t
Abstraction v t' -> Abstraction v (go (next idx) t')
Pattern f -> Pattern (vmap (go idx) f)
substitute :: forall v f a . (Visits f, Ord v) => v -> (Term v f a -> Term v f a)
substitute = substitute' . var
substitute' :: forall v f a . (Visits f, Ord v) => Flat v f -> (Term v f a -> Term v f a)
substitute' value = go zero where
go :: forall a . Index -> Term v f a -> Term v f a
go idx t =
case project t of
Free v -> t
Bound idx'
| idx == idx' -> value
| otherwise -> t
Abstraction v t' -> embed (Abstraction v (go (next idx) t'))
Pattern f -> embed (Pattern (vmap (go idx) f))
subst :: forall v f a . (Visits f, Ord v) => (v -> Maybe (Flat v f)) -> (Term v f a -> Term v f a)
subst ss = go where
go :: forall a . Term v f a -> Term v f a
go t = case project t of
Free v -> fromMaybe t (ss v)
Bound _ -> t
Abstraction v t' -> embed (Abstraction v (go t'))
Pattern f -> embed (Pattern (vmap go f))
substMap :: forall v f a . (Visits f, Ord v) => Map v (Flat v f) -> (Term v f a -> Term v f a)
substMap ss = subst (`Map.lookup` ss)
subst1 :: forall v f a . (Visits f, Ord v) => (v, Flat v f) -> (Term v f a -> Term v f a)
subst1 (v, value) = subst (\v' -> if v == v' then Just value else Nothing)