module Term.Substitution (
composeVFresh
, freshToFree
, freshToFreeAvoiding
, freshToFreeAvoidingFast
, freeToFreshRaw
, module Term.LTerm
, module Term.Substitution.SubstVFree
, module Term.Substitution.SubstVFresh
) where
import Term.LTerm
import Term.Substitution.SubstVFree
import Term.Substitution.SubstVFresh
import Extension.Prelude
import Control.Monad.Bind
import Control.Basics
composeVFresh :: (IsConst c, Show (Lit c LVar))
=> LSubstVFresh c -> LSubst c -> LSubstVFresh c
composeVFresh s1_0 s2 =
freeToFreshRaw (s1 `compose` s2)
where
s1 = freshToFreeAvoidingFast (extendWithRenaming (varsRange s2) s1_0) (s2,s1_0)
freshToFree :: (MonadFresh m, IsConst c)
=> SubstVFresh c LVar -> m (Subst c LVar)
freshToFree subst = (`evalBindT` noBindings) $ do
let slist = sortOn (size . snd) $ substToListVFresh subst
substFromList <$> mapM convertMapping slist
where
convertMapping (lv,t) = (lv,) <$> mapFrees (Arbitrary importVar) t
where
importVar v = importBinding (\s i -> LVar s (lvarSort v) i) v (namehint v)
namehint v = case viewTerm t of
Lit (Var _) -> lvarName lv
_ -> lvarName v
freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar
freshToFreeAvoiding s t = freshToFree s `evalFreshAvoiding` t
freshToFreeAvoidingFast :: (HasFrees t, Ord c) => LSubstVFresh c -> t -> LSubst c
freshToFreeAvoidingFast s t =
substFromList . renameMappings . substToListVFresh $ s
where
renameMappings l = zip (map fst l) (rename (map snd l) `evalFreshAvoiding` t)
freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVar
freeToFreshRaw s@(Subst _) = substFromListVFresh $ substToList s