{-# LANGUAGE ViewPatterns #-}
{-# OPTIONS_GHC -fno-warn-incomplete-patterns #-}
  -- spurious warnings for view patterns
-- |
-- Copyright   : (c) 2010-12 Benedikt Schmidt
-- License     : GPL v3 (see LICENSE)
-- 
-- Maintainer  : Benedikt Schmidt <beschmi@gmail.com>
--
-- Positions and replacement in terms.
module Term.Positions where

import Term.VTerm
import Safe

-- Positions, subterm access, subterm replacement
----------------------------------------------------------------------

-- | A position in a term is a list of integers.
type Position = [Int]

-- | @t `atPos` p@ returns the subterm of term @t@ at position @p@.
--   The standard notation for @t `atPos` p@ is @t|_p@.
--   'atPos' accounts for AC symbols by interpreting n-ary operator
--   applications @*[t1,t2,..tk-1,tk]@ as binary applications
--   @t1*(t2*..(tk-1*tk)..)@.
atPos :: Ord a => Term a -> Position -> Term a
atPos t                                     []     = t
atPos (viewTerm -> FApp (AC _) (a:_))       (0:ps) =
    a `atPos` ps
atPos (viewTerm -> FApp (AC _) [_])         _      =
    error "Term.Positions.atPos: invalid position given"
atPos (viewTerm -> FApp fsym@(AC _) (_:as)) (1:ps) =
    (fApp fsym as) `atPos` ps
atPos (viewTerm -> FApp (AC _) [])          _      =
    error $ "Term.Positions.atPos: impossible, "
            ++"nullary AC symbol appliction"
atPos (viewTerm -> FApp  _ as)              (i:ps) = case atMay as i of
    Nothing -> error "Term.Positions.atPos: invalid position given"
    Just a  -> a `atPos` ps
atPos (viewTerm -> Lit _)                   (_:_)  =
    error "Term.Positions.atPos: invalid position given"


-- | @t `replacePos` (s,p)@ returns the term @t'@ where the subterm at position @p@
--   is replaced by @s@. The standard notation for @t `replacePos` (s,p)@ is @t[s]_p@.
--   'replacePos' accounts for AC symbols in the same ways as 'atPos'.
--   FIXME: The AC can be optimized.
replacePos :: Ord a => Term a -> (Term a, Position) -> Term a
replacePos _                                     (s,[])   = s
replacePos (viewTerm -> FApp fsym@(AC _) (a:as)) (s,0:ps) =
    fApp fsym ((a `replacePos` (s,ps)):as)
replacePos (viewTerm -> FApp fsym@(AC _) (a:as)) (s,1:ps) =
    fApp fsym [a, (fApp fsym as) `replacePos` (s,ps)]
replacePos (viewTerm -> FApp      (AC _) _)        _      =
    error "Term.Positions.replacePos: invalid position given"
replacePos (viewTerm -> FApp fsym as)            (s,i:ps) =
    if 0 <= i && i < length as
    then fApp fsym ((take i as)++[as!!i `replacePos` (s,ps)]++(drop (i+1) as))
    else error "Term.Positions.replacePos: invalid position given"
replacePos (viewTerm -> Lit _)        (_,_:_)             =
    error "Term.Positions.replacePos: invalid position given"

-- | @positionsNonVar t@ returns all the non-variable positions in the term @t@.
--   'positionsNonVar' accounts for AC symbols in the same ways as 'atPos'.
positionsNonVar :: (Show a, Show b) => VTerm a b -> [Position]
positionsNonVar =
    go
  where
    go (viewTerm -> Lit  (Con _))    = [[]]
    go (viewTerm -> Lit  (Var _))    = []
    go (viewTerm -> FApp (AC _)  as) = []:concat (zipWith (\i a -> map ((position i len)++) (go a))
                                                          [0..] as)
        where len = length as
    go (viewTerm -> FApp _       as) = []:concat (zipWith (\i a -> map (i:) (go a)) [0..] as)

    position i len | i == len - 1 = replicate i 1
                   | otherwise    = replicate i 1 ++ [0]