module Data.Comp.Variables
(
HasVars(..),
Subst,
CxtSubst,
varsToHoles,
containsVar,
variables,
variableList,
variables',
substVars,
appSubst,
compSubst,
getBoundVars
) where
import Data.Comp.Algebra
import Data.Comp.Derive
import Data.Comp.Number
import Data.Comp.Term
import Data.Foldable hiding (elem, notElem)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Prelude hiding (foldl, or)
type CxtSubst h a f v = Map v (Cxt h f a)
type Subst f v = CxtSubst NoHole () f v
class HasVars f v where
isVar :: f a -> Maybe v
isVar _ = Nothing
bindsVars :: Ord a => f a -> Map a (Set v)
bindsVars _ = Map.empty
$(derive [liftSum] [''HasVars])
isVar' :: (HasVars f v, Ord v) => Set v -> f a -> Maybe v
isVar' b t = do v <- isVar t
if v `Set.member` b
then Nothing
else return v
getBoundVars :: (HasVars f v, Traversable f) => f a -> f (Set v, a)
getBoundVars t = let n = number t
m = bindsVars n
trans x = (Map.findWithDefault Set.empty x m, unNumbered x)
in fmap trans n
fmapBoundVars :: (HasVars f v, Traversable f) => (Set v -> a -> b) -> f a -> f b
fmapBoundVars f t = let n = number t
m = bindsVars n
trans x = f (Map.findWithDefault Set.empty x m) (unNumbered x)
in fmap trans n
foldlBoundVars :: (HasVars f v, Traversable f) => (b -> Set v -> a -> b) -> b -> f a -> b
foldlBoundVars f e t = let n = number t
m = bindsVars n
trans x y = f x (Map.findWithDefault Set.empty y m) (unNumbered y)
in foldl trans e n
varsToHoles :: (Traversable f, HasVars f v, Ord v) => Term f -> Context f v
varsToHoles t = cata alg t Set.empty
where alg :: (Traversable f, HasVars f v, Ord v) => Alg f (Set v -> Context f v)
alg t vars = case isVar t of
Just v | not (v `Set.member` vars) -> Hole v
_ -> Term $ fmapBoundVars run t
where
run newVars f = f $ newVars `Set.union` vars
containsVarAlg :: (Eq v, HasVars f v, Traversable f, Ord v) => v -> Alg f Bool
containsVarAlg v t = foldlBoundVars run local t
where local = case isVar t of
Just v' -> v == v'
Nothing -> False
run acc vars b = acc || (not (v `Set.member` vars) && b)
containsVar :: (Eq v, HasVars f v, Traversable f, Ord v)
=> v -> Cxt h f a -> Bool
containsVar v = free (containsVarAlg v) (const False)
variablesAlg :: (Ord v, HasVars f v, Traversable f) => Alg f (Set v)
variablesAlg t = foldlBoundVars run local t
where local = case isVar t of
Just v -> Set.singleton v
Nothing -> Set.empty
run acc bvars vars = acc `Set.union` (vars `Set.difference` bvars)
variableList :: (Ord v, HasVars f v, Traversable f) => Cxt h f a -> [v]
variableList = Set.toList . variables
variables :: (Ord v, HasVars f v, Traversable 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
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, Traversable f)
=> SubstVars v (Cxt h f a) (Cxt h f a) where
substVars subst = doSubst Set.empty
where doSubst _ (Hole a) = Hole a
doSubst b (Term t) = case isVar' b t >>= subst of
Just new -> new
Nothing -> Term $ fmapBoundVars run t
where run vars = doSubst (b `Set.union` vars)
instance (SubstVars v t a, Functor f) => SubstVars v t (f a) where
substVars f = fmap (substVars f)
compSubst :: (Ord v, HasVars f v, Traversable 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