module Data.Comp.Variables (
HasVars(..),
Subst,
CxtSubst,
varsToHoles,
containsVar,
variables,
variableList,
variables',
substVars,
appSubst,
compSubst) where
import Data.Comp.Term
import Data.Comp.Sum
import Data.Comp.Algebra
import Data.Foldable
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Map (Map)
import qualified Data.Map as Map
import Prelude hiding (or, foldl)
type CxtSubst h a f v = Map v (Cxt h f a)
type Subst f v = CxtSubst NoHole Nothing f v
class HasVars f v where
isVar :: f a -> Maybe v
isVar _ = Nothing
instance (HasVars f v, HasVars g v) => HasVars (f :+: g) v where
isVar (Inl v) = isVar v
isVar (Inr v) = isVar v
instance HasVars f v => HasVars (Cxt h f) v where
isVar (Term t) = isVar t
isVar _ = Nothing
varsToHoles :: (Functor f, HasVars f v) => Term f -> Context f v
varsToHoles = cata alg
where alg t = case isVar t of
Just v -> Hole v
Nothing -> Term t
containsVarAlg :: (Eq v, HasVars f v, Foldable f) => v -> Alg f Bool
containsVarAlg v t = local || or t
where local = case isVar t of
Just v' -> v == v'
Nothing -> False
containsVar :: (Eq v, HasVars f v, Foldable f, Functor f)
=> v -> Cxt h f a -> Bool
containsVar v = free (containsVarAlg v) (const False)
variablesAlg :: (Ord v, HasVars f v, Foldable f)
=> Alg f (Set v)
variablesAlg t = foldl Set.union local t
where local = case isVar t of
Just v -> Set.singleton v
Nothing -> Set.empty
variableListAlg :: (Ord v, HasVars f v, Foldable f)
=> Alg f [v]
variableListAlg t = foldl (++) local t
where local = case isVar t of
Just v -> [v]
Nothing -> []
variableList :: (Ord v, HasVars f v, Foldable f, Functor f)
=> Cxt h f a -> [v]
variableList = free variableListAlg (const [])
variables :: (Ord v, HasVars f v, Foldable f, Functor f)
=> Cxt h f a -> Set v
variables = free variablesAlg (const Set.empty)
variables' :: (Ord v, HasVars f v, Foldable f, Functor f)
=> Const f -> Set v
variables' c = case isVar c of
Nothing -> Set.empty
Just v -> Set.singleton v
substAlg :: (HasVars f v) => (v -> Maybe (Cxt h f a)) -> Alg f (Cxt h f a)
substAlg f t = fromMaybe (Term t) (isVar t >>= f)
class SubstVars v t a where
substVars :: (v -> Maybe t) -> a -> a
appSubst :: (Ord v, SubstVars v t a) => Map v t -> a -> a
appSubst subst = substVars f
where f v = Map.lookup v subst
instance (Ord v, HasVars f v, Functor f) => SubstVars v (Cxt h f a) (Cxt h f a) where
substVars f (Term v) = substAlg f $ fmap (substVars f) v
substVars _ (Hole a) = Hole a
instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where
substVars f = fmap (substVars f)
compSubst :: (Ord v, HasVars f v, Functor f)
=> CxtSubst h a f v -> CxtSubst h a f v -> CxtSubst h a f v
compSubst s1 s2 = fmap (appSubst s1) s2 `Map.union` s1