{-# LANGUAGE TupleSections, TypeSynonymInstances, GADTs,FlexibleContexts,EmptyDataDecls,StandaloneDeriving, DeriveDataTypeable, FlexibleInstances, 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

  , 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 Data.Traversable hiding (mapM)
import Control.Applicative


-- 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))
              => SubstVFresh c LVar -> Subst c LVar -> SubstVFresh c LVar
composeVFresh s1_0 s2 =
    freeToFreshRaw (s1 `compose` s2)
  where
    s1 = freshToFreeAvoiding (extendWithRenaming (varsRange s2)  s1_0) (s2,s1_0)

-- Conversion between substitutions
----------------------------------------------------------------------

-- | @freshToFreeSimp 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,) <$> traverse importLit t
      where
        importLit (Con c) = return (Con c)
        importLit (Var v) =
            Var <$> importBinding (\s i -> LVar s (lvarSort v) i) v (namehint v)
        namehint v = case t of
            Lit (Var _) -> lvarName lv -- keep name of oldvar
            _           -> lvarName v

-- | @freshToFreeSimpAvoiding s t@ converts all fresh variables in the range of
--   @s@ to free variables avoiding free variables in @t@.
freshToFreeAvoiding :: (HasFrees t, IsConst c) => SubstVFresh c LVar -> t -> Subst c LVar
freshToFreeAvoiding s t = freshToFree s `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