module Syntax.Class.Term (
    -- * Class Definition
    Term(..), 
    -- * Data Types
    Position(..), isSubPos,
    -- * Constructors
    (°),
--    Hole(..),
    
--    Substitutable(..),
--    Substitution, Replacement, nullSubst, (<~), insertApply,
    
    Size(..), compareSizeLinear, compareSizePairwise,
    
    -- Auxiliary functions
    mapGetPos, applyAtIndex, applyAtIndexM,
    subtermAt, subtermOf, sameSymAt, getVarPos, hasVars, getVars, getVars',
    getPos, varAtPos, applyAtPos, getVarNames, substitute, replaceTerm,
    mapTermM, mapTerm, foldTerm, anySubterm,

    )where

--import Syntax.Ppr
import Syntax.Name
import qualified Data.List as L
import qualified Data.Set as S
import Data.Maybe (fromMaybe, isJust, maybeToList)
import Data.Function
import Control.Monad
import Control.Monad.Error
import Control.Monad.Identity (runIdentity)

-- | Composed 'Position' defining positions in terms
data Position = Root
              -- | P Int -- zero-based
              | Int `Dot` Position
    deriving( Eq )

instance Ord Position where
    compare Root Root = EQ
    compare Root _    = LT
    compare _ Root    = GT
    compare (Dot i p) (Dot i' p')
        | p == p'    = compare i i'
        | otherwise  = compare p p'
        
instance Show Position where
    show Root       = "R"
    --show (P i)      = show i
    show (Dot i p)  = (show i) ++ "." ++ (show p)



-- | @isSubPos p1 p2 == True@ iff there is a direct path downwards in the term 
--   tree from p2 to p1 
isSubPos :: Position -> Position -> Bool
isSubPos _ Root = True
isSubPos (Dot i p) (Dot i' p') = (i == i') && isSubPos p p'
    
---- | Data type for holes in terms
--data Hole = Hole



-- | Infix constructor for 'Position's
infixr 5 °
(°) :: Int              -- ^ the nth sub-term (zero-based) 
    -> Position         -- ^ a position in a term
    -> Position         -- ^ the resulting position, pointing at the nth sub-term
                        --   of the given position
-- Root ° i = (P i)
i ° p | i >= 0      = i `Dot` p
      | otherwise   = error $ "Terms.(°): Illegal position, no subternms " ++
                              "with index < 0 !"


-- | Count the ctor symbols in a term
class Size t where
    size :: t -> Int
    size = flip sizeS 0 
    
    sizeS :: t -> Int -> Int
    
instance Size t => Size [t] where
    sizeS l = (+ (foldl (flip sizeS) 0 l))

compareSizeLinear :: (Size t) => [t] -> [t] -> Ordering
compareSizeLinear = compare `on` size  
  
compareSizePairwise :: (Size t) => [t] -> [t] -> Ordering
compareSizePairwise  [] [] = EQ
compareSizePairwise  x  [] = GT
compareSizePairwise  [] y  = LT
compareSizePairwise (x:xs) (y:ys) =
    let o = on compare size x y
    in if o == EQ then compareSizePairwise xs ys else o

{- |
    The class definition of 'Term's. Defining operations common to all terms
-}
class (Eq t, Show t) => Term t where
   
    -- |Returns the positions of a subterm @s@ in a term @t@. I
--    getPos          :: t                 -- ^ the term
--                    -> t                 -- ^ the subterm
--                    -> [Position]        -- ^ the positions
                    
    -- | Returns 'true' if both terms have the same constructor symbol at the
    --   root position, 'False' otherwise
    sameSymAtRoot :: t -> t -> Bool
    
    -- | semantical equivalence of terms, may take different syntactic representations
    --   of semantically equivalent terms in account. Eg. infix vs prefix
    equal :: t -> t -> Bool
    
    -- | Inverse of subterms, @root t $ subterms t = t@ 
    root :: t -> ([t] -> t)
             
    -- |Returns the immediate subterms of a term (which may be holes)
    --  E.g.: subterms f(a,b) ~~> [a,b]               
    subterms        :: t -> [t]
      
    -- | Given a term 't' and a Name 'n', returns a variable of type 'v' with name 'n'
    --   The first argument is moe or less to dissolve the functional 
    --   dependencies.
    toVar :: t -> Name -> t
    getVar :: t -> Maybe Name
    isVar :: t -> Bool
    isVar = isJust . getVar

mapTermM :: (Monad m, Term t) => (t -> m t) -> t -> m t
mapTermM f t = f =<< liftM (root t) new_subtermsM
    where
        new_subtermsM = mapM (mapTermM f) (subterms t)

mapTerm :: Term t => (t -> t) -> t -> t
mapTerm f t = f $ root t new_subterms
    where
        new_subterms = map (mapTerm f) (subterms t)

foldTerm :: Term t => (t -> a -> a) -> a -> t -> a
foldTerm f a t = f t (foldr (.) id (map (flip (foldTerm f)) (subterms t)) a)

anySubterm :: Term t => (t -> Bool) -> t -> Bool
anySubterm p = foldTerm (\t b -> b || p t) False

subtermOf       :: (Term t) => t -> t -> Bool
subtermOf t s = not . null $ getPos t s
-- | returns subterm @s@ at position @p@ in term @t@, and 'Nothing' if there
--   is either no such position in this term, or no term at this position
--   (e.g. the term is a section of an infix operator)    
subtermAt         :: (Term t) => t                 -- ^ the term @t@
                -> Position            -- ^ a position @p@
                -> Maybe t             -- ^ subterm @s@ in @t@ at position @p@
subtermAt t Root      = return t
subtermAt t (Dot i p) =
    (subterms t) !?! i >>=  flip subtermAt p
--    noHole "Terms.subterm: No subterm at position" r

applyAtPos :: (Term t) => (t -> t) -> Position -> t -> t
applyAtPos f Root t = f t
applyAtPos f (i `Dot` pos) t = (root t)(applyAtIndex (subterms t) i (applyAtPos f pos))

-- @getPos t s@ returns all position in @t@ that are equal to @s@
getPos :: (Term t) => t -> t -> [Position]
getPos t s  
    | t == s    = [Root]
    | otherwise =  mapGetPos (subterms t) s

-- | @replace s1 s2 t@ replaces all occurences of subterm @s1@ by term @s2@ in @t@
replaceTerm :: (Term t) => t -> t -> t -> t
replaceTerm s1 s2 t 
    | s1 == t   = s2
    | otherwise = let sts = subterms t
                  in if null sts then t
                       else root t $ map (replaceTerm s1 s2)(subterms t)
--    = trace (show  (getPos t s1)) $ 
--    foldl (flip (substitute s2)) t (getPos t s1)

-- | Returns 'True' if both terms have the same constructor symbol at 
--   'Position' @p@ or both have a variable. 'false' otherwise.
sameSymAt :: (Term t) => Position -> t -> t ->Bool
sameSymAt p t1 t2 = fromMaybe False $ liftM2 sameSymAtRoot (subtermAt t1 p)(subtermAt t2 p)

--subtermsNoHole :: (Term t) => t -> [t]
--subtermsNoHole t = filter (== hole) (subterms t)


-- < Returns 'True' if the term 't' contains variables
hasVars         :: (Term t) => t -> Bool
hasVars = not.null.getVars

varAtPos :: (Term t) => t -> Position -> Bool
varAtPos t p = fromMaybe False $ liftM isVar $ subtermAt t p

-- |Returns a (unique) list of all variable names in t
getVarNames     :: (Term t) => t -> [Name]
getVarNames = L.nub . foldTerm (maybe id (:) . getVar) []
     
-- |Returns a list of all variable position in t
getVarPos       :: (Term t) => t -> [(t,[Position])]
getVarPos t     =  [(st,getPos t st) | st <- (getVars' t)]

-- |Returns a (unique) list of all variables in t
getVars         :: (Term t) => t -> [t]
getVars = L.nub . getVars'
    
-- |Returns a list of all variables in t
getVars'         :: (Term t) => t -> [t]
getVars' t
    | isVar t   = [t]
    | otherwise = concatMap getVars' $ subterms t

ctorAtPos :: (Term t) => t -> Position -> Bool
ctorAtPos t p = not $ varAtPos t p
    
--noHole          :: (Term t) => String
--                -> t
--                -> Maybe t
--noHole s t = if t == hole then fail s else return t

                    
-- |Subsitute subterm at position @p@ in term @t@ with term @s@
--  If there is no such position @p@, @t@ is returned.
substitute      :: (Term t) =>
                   t                 -- ^ the substitute @s@
                -> Position          -- ^ the postion @p@
                -> t                 -- ^ the initial term @t@
                -> t                 -- ^ the result
substitute s p t = applyAtPos (\_ -> s) p t        

     
--------------------------------------------------------------------------------
-- General auxiliary functions for 'Term's
--------------------------------------------------------------------------------  
-- |This monster applies 'getPos' to a list of terms and keeps track of the 
--  argument position.
mapGetPos :: (Term x) => [x] -> x -> [Position]                              
mapGetPos ts s = concat $ snd $ L.mapAccumL (\i t -> (i+1, map (i°) (getPos t s))) 0 ts
       
-- | Applys a function @f@ at the nth element i of a list (zero-based)
applyAtIndexM  :: (Monad m) => [a] -> Int -> (a -> m a) -> (m [a])
applyAtIndexM xs n _ | n < 0 = fail "Terms.applyAtIndex: negative index"
applyAtIndexM [] _ _        =  fail "Terms.applyAtIndex: index too large"
applyAtIndexM (x:xs) 0 f    =  do {fx <- (f x); return (fx:xs) }
applyAtIndexM (x:xs) n f    =  do {fxs <- (applyAtIndexM xs (n-1) f); return (x:fxs)}
     
-- | Applys a function @f@ at the nth element i of a list (zero-based)
applyAtIndex  :: [a] -> Int -> (a -> a) -> [a]
applyAtIndex xs n f = runIdentity $ applyAtIndexM xs n (return . f)

-- | /Secure/ 'Prelude.!!'
infix 5 !?!
(!?!) :: [a] -> Int -> Maybe a
[] !?! i        = Nothing -- Terms.applyAtIndex: index too large
(x:xs) !?! i
    | i < 0     = Nothing -- Terms.applyAtIndex: negative index
    | i == 0    = return x
    | otherwise = xs  !?! (i-1)
