module Term.Substitution.SubstVFree (
Subst(..)
, applyVTerm
, applyLit
, substFromList
, substFromMap
, emptySubst
, compose
, applySubst
, restrict
, mapRange
, varsRange
, dom
, range
, imageOf
, substToListOn
, substToList
, Apply(..)
, prettySubst
, LSubst
, LNSubst
, prettyLNSubst
) where
import Term.LTerm
import Term.Rewriting.Definitions
import Text.PrettyPrint.Highlight
import Logic.Connectives
import Utils.Misc
import Data.Maybe
import Data.Map ( Map )
import qualified Data.Map as M
import qualified Data.Set as S
import Data.List
import Data.Binary
import Control.Applicative
import Control.DeepSeq
newtype Subst c v = Subst { sMap :: Map v (VTerm c v) }
deriving ( Eq, Ord, NFData, Binary )
type LSubst c = Subst c LVar
type LNSubst = Subst Name LVar
applyLit :: IsVar v => Subst c v -> Lit c v -> VTerm c v
applyLit subst v@(Var i) = fromMaybe (lit v) $ M.lookup i (sMap subst)
applyLit _ c@(Con _) = lit c
applyVTerm :: (IsConst c, IsVar v, Ord c) => Subst c v -> VTerm c v -> VTerm c v
applyVTerm subst t = case viewTerm t of
Lit l -> applyLit subst l
FApp (AC o) ts -> fAppAC o (map (applyVTerm subst) ts)
FApp (NonAC o) ts -> fAppNonAC o (map (applyVTerm subst) ts)
FApp List ts -> fAppList (map (applyVTerm subst) ts)
substFromList :: IsVar v => [(v, VTerm c v)] -> Subst c v
substFromList xs =
Subst (M.fromList [ (v,t) | (v,t) <- xs, not (equalToVar t v) ])
equalToVar :: IsVar v => VTerm c v -> v -> Bool
equalToVar (viewTerm -> Lit (Var v')) v = v == v'
equalToVar _ _ = False
substFromMap :: IsVar v => Map v (VTerm c v) -> Subst c v
substFromMap = Subst . M.filterWithKey (\v t -> not $ equalToVar t v)
emptySubst :: Subst c v
emptySubst = Subst M.empty
applySubst :: (IsConst c, IsVar v)
=> Subst c v -> Subst c v -> Subst c v
applySubst subst subst' = mapRange (applyVTerm subst) subst'
compose :: (IsConst c, IsVar v)
=> Subst c v -> Subst c v -> Subst c v
compose s1 s2 =
Subst $ sMap (applySubst s1 s2) `M.union` sMap (restrict (dom s1 \\ dom s2) s1)
restrict :: IsVar v => [v] -> Subst c v -> Subst c v
restrict vs (Subst smap) = Subst (M.filterWithKey (\v _ -> v `elem` vs) smap)
mapRange :: (IsConst c, IsVar v, IsConst c2)
=> (VTerm c v -> VTerm c2 v)
-> Subst c v -> Subst c2 v
mapRange f subst@(Subst _) =
Subst $ M.mapMaybeWithKey (\i t -> filterRefl i (f t)) (sMap subst)
where
filterRefl i (viewTerm -> Lit (Var j)) | i == j = Nothing
filterRefl _ t = Just t
dom :: Subst c v -> [v]
dom = M.keys . sMap
range :: Subst c v -> [VTerm c v]
range = M.elems . sMap
varsRange :: IsVar v => Subst c v -> [v]
varsRange = varsVTerm . fAppList . range
substToList :: Subst c v -> [(v,VTerm c v)]
substToList = M.toList . sMap
substToListOn :: (IsConst c, IsVar v) => [v] -> Subst c v -> [VTerm c v]
substToListOn vs subst = map (applyLit subst) (map Var vs)
imageOf :: IsVar v => Subst c v -> v -> Maybe (VTerm c v)
imageOf subst i = M.lookup i (sMap subst)
instance (Show v, Show c) => Show (Subst c v) where
show subst@(Subst _) = "{" ++ mappings ++"}"
where
mappings =
intercalate ", " [ show t ++" <~ "++show v | (v,t) <- substToList subst ]
instance Sized (Subst c v) where
size = sum . map size . range
instance Ord c => HasFrees (LSubst c) where
foldFrees f = foldFrees f . sMap
mapFrees f = (substFromList <$>) . mapFrees f . substToList
class Apply t where
apply :: LNSubst -> t -> t
instance Apply LVar where
apply subst x = maybe x extractVar $ imageOf subst x
where
extractVar (viewTerm -> Lit (Var x')) = x'
extractVar t =
error $ "apply (LVar): variable '" ++ show x ++
"' substituted with term '" ++ show t ++ "'"
instance Apply LNTerm where
apply subst = applyVTerm subst
instance Apply BLVar where
apply _ x@(Bound _) = x
apply subst x@(Free v) = maybe x extractVar $ imageOf subst v
where
extractVar (viewTerm -> Lit (Var v')) = Free v'
extractVar _t =
error $ "apply (BLVar): variable '" ++ show v ++
"' substituted with term '"
instance Apply BLTerm where
apply subst = (`bindTerm` applyBLLit)
where
applyBLLit :: Lit Name BLVar -> BLTerm
applyBLLit l@(Var (Free v)) =
maybe (lit l) (fmapTerm (fmap Free)) (imageOf subst v)
applyBLLit l = lit l
instance Apply () where
apply _ = id
instance Apply Char where
apply _ = id
instance Apply Int where
apply _ = id
instance Apply Bool where
apply _ = id
instance (Apply a, Apply b) => Apply (a, b) where
apply subst (x,y) = (apply subst x, apply subst y)
instance Apply a => Apply (Maybe a) where
apply subst = fmap (apply subst)
instance (Apply a, Apply b) => Apply (Either a b) where
apply subst = either (Left . apply subst) (Right . apply subst)
instance Apply a => Apply [a] where
apply subst = fmap (apply subst)
instance Apply a => Apply (Conj a) where
apply subst = fmap (apply subst)
instance Apply a => Apply (Disj a) where
apply subst = fmap (apply subst)
instance (Ord a, Apply a) => Apply (S.Set a) where
apply subst = S.map (apply subst)
instance Apply t => Apply (Equal t) where
apply subst = fmap (apply subst)
prettySubst :: (Ord c, Ord v, HighlightDocument d)
=> (v -> d) -> (Lit c v -> d) -> Subst c v -> [d]
prettySubst ppVar ppLit =
map pp . M.toList . equivClasses . substToList
where
pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <>
(fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}"
prettyLNSubst :: (Show (Lit c LVar), Ord c, HighlightDocument d)
=> LSubst c -> d
prettyLNSubst = vcat . prettySubst (text . show) (text . show)