module Base.Subst
( Subst (..), IntSubst (..), idSubst, singleSubst, bindSubst, unbindSubst
, substToList, compose, substVar', isubstVar, restrictSubstTo
) where
import qualified Data.Map as Map
data Subst a b = Subst Bool (Map.Map a b)
deriving Int -> Subst a b -> ShowS
[Subst a b] -> ShowS
Subst a b -> String
(Int -> Subst a b -> ShowS)
-> (Subst a b -> String)
-> ([Subst a b] -> ShowS)
-> Show (Subst a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> Subst a b -> ShowS
forall a b. (Show a, Show b) => [Subst a b] -> ShowS
forall a b. (Show a, Show b) => Subst a b -> String
showList :: [Subst a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [Subst a b] -> ShowS
show :: Subst a b -> String
$cshow :: forall a b. (Show a, Show b) => Subst a b -> String
showsPrec :: Int -> Subst a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> Subst a b -> ShowS
Show
idSubst :: Subst a b
idSubst :: Subst a b
idSubst = Bool -> Map a b -> Subst a b
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
False Map a b
forall k a. Map k a
Map.empty
substToList :: Subst v e -> [(v, e)]
substToList :: Subst v e -> [(v, e)]
substToList (Subst _ sigma :: Map v e
sigma) = Map v e -> [(v, e)]
forall k a. Map k a -> [(k, a)]
Map.toList Map v e
sigma
singleSubst :: Ord v => v -> e -> Subst v e
singleSubst :: v -> e -> Subst v e
singleSubst v :: v
v e :: e
e = v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst v
v e
e Subst v e
forall a b. Subst a b
idSubst
bindSubst :: Ord v => v -> e -> Subst v e -> Subst v e
bindSubst :: v -> e -> Subst v e -> Subst v e
bindSubst v :: v
v e :: e
e (Subst comp :: Bool
comp sigma :: Map v e
sigma) = Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp (Map v e -> Subst v e) -> Map v e -> Subst v e
forall a b. (a -> b) -> a -> b
$ v -> e -> Map v e -> Map v e
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert v
v e
e Map v e
sigma
unbindSubst :: Ord v => v -> Subst v e -> Subst v e
unbindSubst :: v -> Subst v e -> Subst v e
unbindSubst v :: v
v (Subst comp :: Bool
comp sigma :: Map v e
sigma) = Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp (Map v e -> Subst v e) -> Map v e -> Subst v e
forall a b. (a -> b) -> a -> b
$ v -> Map v e -> Map v e
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete v
v Map v e
sigma
compose :: Ord v => Subst v e -> Subst v e -> Subst v e
compose :: Subst v e -> Subst v e -> Subst v e
compose sigma :: Subst v e
sigma sigma' :: Subst v e
sigma' =
Subst v e -> Subst v e
forall a b. Subst a b -> Subst a b
composed (((v, e) -> Subst v e -> Subst v e)
-> Subst v e -> [(v, e)] -> Subst v e
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((v -> e -> Subst v e -> Subst v e)
-> (v, e) -> Subst v e -> Subst v e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst) Subst v e
sigma' (Subst v e -> [(v, e)]
forall v e. Subst v e -> [(v, e)]
substToList Subst v e
sigma))
where composed :: Subst a b -> Subst a b
composed (Subst _ sigma'' :: Map a b
sigma'') = Bool -> Map a b -> Subst a b
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
True Map a b
sigma''
substVar' :: Ord v => (v -> e) -> (Subst v e -> e -> e)
-> Subst v e -> v -> e
substVar' :: (v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' var :: v -> e
var subst :: Subst v e -> e -> e
subst (Subst comp :: Bool
comp sigma :: Map v e
sigma) v :: v
v =
e -> (e -> e) -> Maybe e -> e
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (v -> e
var v
v) e -> e
subst' (v -> Map v e -> Maybe e
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup v
v Map v e
sigma)
where subst' :: e -> e
subst' = if Bool
comp then Subst v e -> e -> e
subst (Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp Map v e
sigma) else e -> e
forall a. a -> a
id
class IntSubst e where
ivar :: Int -> e
isubst :: Subst Int e -> e -> e
isubstVar :: IntSubst e => Subst Int e -> Int -> e
isubstVar :: Subst Int e -> Int -> e
isubstVar = (Int -> e) -> (Subst Int e -> e -> e) -> Subst Int e -> Int -> e
forall v e.
Ord v =>
(v -> e) -> (Subst v e -> e -> e) -> Subst v e -> v -> e
substVar' Int -> e
forall e. IntSubst e => Int -> e
ivar Subst Int e -> e -> e
forall e. IntSubst e => Subst Int e -> e -> e
isubst
restrictSubstTo :: Ord v => [v] -> Subst v e -> Subst v e
restrictSubstTo :: [v] -> Subst v e -> Subst v e
restrictSubstTo vs :: [v]
vs (Subst comp :: Bool
comp sigma :: Map v e
sigma) =
((v, e) -> Subst v e -> Subst v e)
-> Subst v e -> [(v, e)] -> Subst v e
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((v -> e -> Subst v e -> Subst v e)
-> (v, e) -> Subst v e -> Subst v e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry v -> e -> Subst v e -> Subst v e
forall v e. Ord v => v -> e -> Subst v e -> Subst v e
bindSubst) (Bool -> Map v e -> Subst v e
forall a b. Bool -> Map a b -> Subst a b
Subst Bool
comp Map v e
forall k a. Map k a
Map.empty)
(((v, e) -> Bool) -> [(v, e)] -> [(v, e)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((v -> [v] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [v]
vs) (v -> Bool) -> ((v, e) -> v) -> (v, e) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (v, e) -> v
forall a b. (a, b) -> a
fst) (Map v e -> [(v, e)]
forall k a. Map k a -> [(k, a)]
Map.toList Map v e
sigma))