module Renaming(rename)where


import Data.List (findIndex)
import Control.Monad.State

import Type
import Vars
import Subst


-- | State for a list of variablenames.
type VarState a = State [VarName] a


-- | 'rename' takes a list of forbidden variablenames and a Rule. It then renames
-- all variables in the rule by using 'freshVars' and avoiding the forbidden names.
rename :: [VarName] -> Rule -> Rule
rename f r = let f'             = (allVars r) ++ f -- add all varnames from thr rule to forbidden
                 r'@(Rule t ts) = replaceUnder r f' -- rename all underscores
                 sub            = getSub f ((allVars r') ++ f') -- get substitutions from old varnames to renamed varnames
             in Rule (apply sub t) (map (apply sub) ts) -- apply substitution to rename vars

-- | 'replaceUnder' takes a Rule and and a list of forbidden variablenames and
-- calls evalState which calls 'replaceS' and adds alls varnames to the forbidden list
replaceUnder :: Rule -> [VarName]  -> Rule
replaceUnder r vs = evalState (replaceS r) $ (allVars r) ++ vs

-- | 'replaceS' takes a Rule and replaces all underscores in the variablenames
-- of the rule with fitting names avoiding the forbidden names.
replaceS :: Rule -> VarState Rule
replaceS (Rule t ts) = do t'  <- replaceT t -- check if t is an underscore and if needed replace it
                          -- map over the list of terms and replace each underscore in any term
                          ts' <- mapM replaceT ts
                          return (Rule t' ts') -- return rule with renamed underscores
  where
   -- | 'replaceT' checks if a Term is an underscore or contains an underscore.
   -- If it does it replaces the underscore by getting the list of forbidden
   -- variablenames, using 'getVars'' to get a new variablename that is valid,
   -- saving the new name and the orginial forbidden list and returning the new name.
   replaceT :: Term -> VarState Term
   replaceT (Var x) = if x == "_"
                      then do -- varname is "_"„
                           vs <- get -- get list of forbidden names
                           let new = ((getVars' 0 1 vs) !! 0) -- get new valid name
                           put (new:vs) -- add new name to forbidden list
                           return (Var new) -- return new name
                      else return (Var x) -- varname not "_"
   replaceT (Comb c cs) = do x <- mapM replaceT cs -- replace every underscore in the list of terms
                             return (Comb c x) -- return comb with renamed list of terms

-- | 'replaceUnderscores' takes a Rule and a list of forbidden variablenames and
-- renames all variables in the Rule avoiding the forbidden and the old names.
replaceUnderscores :: Rule -> [VarName] -> Rule
replaceUnderscores (Rule r rs) badVars =
        let (_, rs') = replaceRecL badVars (r:rs)
        in Rule (head rs')(drop 1 rs')

  where replaceRec :: [VarName] -> Term -> ([VarName], Term)
        replaceRec vs (Var x)   = if x == "_"
                                  then let new = (getVars' 0 1 vs) !! 0
                                       in ((new:vs), (Var new))
                                  else (vs,(Var x))
        replaceRec vs (Comb c [])   = (vs, Comb c [])
        replaceRec vs (Comb c t) = let (vs', t') = replaceRecL vs t
                                    in (vs', (Comb c t'))

        replaceRecL :: [VarName] -> [Term] -> ([VarName], [Term])
        replaceRecL vs [] = (vs, [])
        replaceRecL vs (t:ts) = let (vs', t')   = replaceRec vs t
                                    (vs'', ts') = replaceRecL vs' ts
                                 in (vs'', (t':ts'))

-- | 'getSub' takes a list of variablenames and a list of forbidden variablenames
-- and creates a substitution.
getSub :: [VarName] -> [VarName] -> Subst
getSub oVars f = let f' = altVars $ oVars ++ f -- add new varnames, and original varnames to the forbidden list, get new var names
                -- create substitution from old name to new names, compose all substitutions into one with foldl
                in foldl compose empty $ zipWith (\old new -> single old (Var new)) oVars f'

-- | 'altVars' takes a list of variablenames and returns a list of new alternative variables.
altVars :: [VarName] -> [VarName]
altVars xs = getVars' 0 (length xs) xs

-- | 'getVars'' takes an index, a length and a list of variablenames. It uses
-- 'freshVars' to get a list of new names which are completely different from the old list.
getVars' :: Int -> Int -> [VarName] -> [VarName]
getVars' i n xs = let fVars = drop i $ take (i+n) freshVars -- use drop and take to specify which indices get taken
                  -- find the last index where a variable is also an element of the forbidden names
                  in case findIndex (\x -> elem x xs) (reverse fVars) of
                      -- if there is an index get new varnames starting at that index
                      (Just x)  -> getVars' (i+(n-x)) n xs
                      -- if not return the list of new names
                      (Nothing) -> fVars