{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls #-}
{-# LANGUAGE StandaloneDeriving, DeriveDataTypeable, FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses, DeriveFunctor, ScopedTypeVariables #-}
-- |
-- Copyright : (c) 2010, 2011 Benedikt Schmidt
-- License : GPL v3 (see LICENSE)
--
-- Maintainer : Benedikt Schmidt <beschmi@gmail.com>
--
-- Standard and fresh substitutions.
module Term.Substitution (
-- ** Composition of fresh and free substitutions
composeVFresh
-- ** Conversion between fresh and free
, freshToFree
, freshToFreeAvoiding
, freshToFreeAvoidingFast
, freeToFreshRaw
-- ** Convenience exports
, 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
-- Composition of VFresh and VFresh substitutions
----------------------------------------------------------------------
-- | @composeVFresh s1 s2@ composes the fresh substitution s1 and the free substitution s2.
-- The result is the fresh substitution s = s1.s2.
composeVFresh :: (IsConst c, Show (Lit c LVar))
=> LSubstVFresh c -> LSubst c -> LSubstVFresh c
composeVFresh s1_0 s2 =
-- all variables in vrange(s1.s2) originate from s1 and can be considered fresh.
freeToFreshRaw (s1 `compose` s2)
where
s1 = freshToFreeAvoidingFast (extendWithRenaming (varsRange s2) s1_0) (s2,s1_0)
-- Conversion between substitutions
----------------------------------------------------------------------
-- | @freshToFree s@ converts the bound variables in @s@ to free variables
-- using fresh variable names. We try to preserve variables names if possible.
freshToFree :: (MonadFresh m, IsConst c)
=> SubstVFresh c LVar -> m (Subst c LVar)
freshToFree subst = (`evalBindT` noBindings) $ do
let slist = sortOn (size . snd) $ substToListVFresh subst
-- import oldvar ~> newvar mappings first, keep namehint from oldvar
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 -- keep name of oldvar
_ -> lvarName v
-- | @freshToFreeAvoiding s t@ converts all fresh variables in the range of
-- @s@ to free variables avoiding free variables in @t@. This function tries
-- to reuse variable names from the domain of the substitution if possible.
freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar
freshToFreeAvoiding s t = freshToFree s `evalFreshAvoiding` t
-- | @freshToFreeAvoidingFast s t@ converts all fresh variables in the range of
-- @s@ to free variables avoiding free variables in @t@. This function does
-- not try to reuse variable names from the domain of the substitution.
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 s@ considers all variables in the range of @s@ as fresh.
freeToFreshRaw :: Subst c LVar -> SubstVFresh c LVar
freeToFreshRaw s@(Subst _) = substFromListVFresh $ substToList s