module Term.Substitution.SubstVFresh (
SubstVFresh(..)
, substFromListVFresh
, emptySubstVFresh
, restrictVFresh
, mapRangeVFresh
, extendWithRenaming
, varsRangeVFresh
, domVFresh
, rangeVFresh
, isRenaming
, imageOfVFresh
, substToListVFresh
, prettySubstVFresh
, renameFresh
, renameFreshAvoiding
, removeRenamings
, LSubstVFresh
, LNSubstVFresh
, prettyLSubstVFresh
, prettyDisjLNSubstsVFresh
) where
import Term.LTerm
import Text.PrettyPrint.Highlight
import Control.Applicative
import Control.Monad.Fresh
import Control.DeepSeq
import Logic.Connectives
import Utils.Misc
import Data.Map ( Map )
import qualified Data.Map as M
import qualified Data.Set as S
import Data.List
import Data.Traversable hiding ( mapM )
import Data.Binary
import Data.Monoid ( mempty )
newtype SubstVFresh c v = SubstVFresh { svMap :: Map v (VTerm c v) }
deriving ( Eq, Ord, NFData, Binary )
type LSubstVFresh c = SubstVFresh c LVar
type LNSubstVFresh = SubstVFresh Name LVar
substFromListVFresh :: IsVar v => [(v, VTerm c v)] -> SubstVFresh c v
substFromListVFresh xs = SubstVFresh (M.fromList xs)
emptySubstVFresh :: SubstVFresh c v
emptySubstVFresh = SubstVFresh M.empty
restrictVFresh :: IsVar v => [v] -> SubstVFresh c v -> SubstVFresh c v
restrictVFresh vs (SubstVFresh smap) = SubstVFresh (M.filterWithKey (\v _ -> v `elem` vs) smap)
mapRangeVFresh :: (IsConst c, IsVar v, IsConst c2)
=> (VTerm c v -> VTerm c2 v)
-> SubstVFresh c v -> SubstVFresh c2 v
mapRangeVFresh f subst = SubstVFresh $ M.map f (svMap subst)
extendWithRenaming :: (Ord c, Show (Lit c LVar))
=> [LVar] -> SubstVFresh c LVar -> SubstVFresh c LVar
extendWithRenaming vs0 s =
substFromListVFresh $
substToListVFresh s ++ substToListVFresh (renameFreshAvoiding s2 (varsRangeVFresh s))
where s2 = substFromListVFresh [(v, lit (Var v)) | v <- vs ]
vs = vs0 \\ domVFresh s
domVFresh :: SubstVFresh c v -> [v]
domVFresh = M.keys . svMap
rangeVFresh :: SubstVFresh c v -> [VTerm c v]
rangeVFresh = M.elems . svMap
varsRangeVFresh :: IsVar v => SubstVFresh c v -> [v]
varsRangeVFresh = varsVTerm . fAppList . rangeVFresh
isRenamedVar :: LVar -> LSubstVFresh c -> Bool
isRenamedVar lv subst =
case viewTerm <$> imageOfVFresh subst lv of
Just (Lit (Var lv')) | lvarSort lv == lvarSort lv' ->
lv' `notElem` (varsVTerm . fAppList $ [ t | (v,t) <- substToListVFresh subst, v /= lv ])
_ -> False
isRenaming :: LSubstVFresh c -> Bool
isRenaming subst = all (`isRenamedVar` subst) $ domVFresh subst
imageOfVFresh :: IsVar v => SubstVFresh c v -> v -> Maybe (VTerm c v)
imageOfVFresh subst i = M.lookup i (svMap subst)
substToListVFresh :: SubstVFresh c v -> [(v,VTerm c v)]
substToListVFresh = M.toList . svMap
renameFresh :: (Ord c, MonadFresh m) => SubstVFresh c LVar -> m (SubstVFresh c LVar)
renameFresh subst = substFromListVFresh . zip (map fst slist) <$> rename (map snd slist)
where slist = substToListVFresh subst
renameFreshAvoiding :: (Ord c, HasFrees t) => LSubstVFresh c -> t -> SubstVFresh c LVar
renameFreshAvoiding s t = renameFresh s `evalFreshAvoiding` t
removeRenamings :: LSubstVFresh c -> LSubstVFresh c
removeRenamings s =
substFromListVFresh $ filter (not . (`isRenamedVar` s) . fst) $ substToListVFresh s
instance (Show c, Show v) => Show (SubstVFresh c v) where
show subst = "VFresh: {" ++ mappings ++"}"
where
mappings = intercalate ", " [ show t ++" <~ "++show v | (v,t) <- substToListVFresh subst ]
instance Sized (SubstVFresh c v) where
size = sum . map size . rangeVFresh
instance HasFrees (SubstVFresh n LVar) where
foldFrees f = foldFrees f . M.keys . svMap
foldFreesOcc _ _ = const mempty
mapFrees f =
(substFromListVFresh <$>) . traverse mapDomain . substToListVFresh
where
mapDomain (v, t) = (,t) <$> mapFrees f v
prettySubstVFresh :: (Ord c, Ord v, HighlightDocument d, Show c, Show v)
=> (v -> d) -> (Lit c v -> d) -> SubstVFresh c v -> [d]
prettySubstVFresh ppVar ppLit =
map pp . M.toList . equivClasses . substToListVFresh
where
pp (t, vs) = prettyTerm ppLit t <-> operator_ " <~ {" <>
(fsep $ punctuate comma $ map ppVar $ S.toList vs) <> operator_ "}"
prettyLSubstVFresh :: (Show (Lit c LVar), Ord c, HighlightDocument d, Show c)
=> LSubstVFresh c -> d
prettyLSubstVFresh = vcat . prettySubstVFresh (text . show) (text . show)
prettyDisjLNSubstsVFresh :: Document d => Disj LNSubstVFresh -> d
prettyDisjLNSubstsVFresh (Disj substs) =
numbered' (map ppConj substs)
where
ppConj = vcat . map prettyEq . substToListVFresh
prettyEq (a,b) =
prettyNTerm (lit (Var a)) $$ nest (6::Int) (text "=" <-> prettyNTerm b)