{-| 
  The module "Antiunifier" defines antiunification for terms in a general way.  
-}
module Syntax.Class.Antiunifier
    ( 
    -- * The class Antiunifiable
    AU, getMap, getCnt, putImg,
    AUnify(aunify, lgg),
    lggL,
   
    roots, sameRoots,

    
    ) where

import Prelude hiding ((<$>))

import Syntax.Name
import Syntax.Class.Term
import Syntax.Context

import Text.PrettyPrint.ANSI.Leijen

import Control.Monad.State 
import Control.Monad.Error

import qualified Data.Map as M
import Data.List (transpose, find)
import Data.Function (on)

import Debug.Trace

data (Pretty t) => VIMap t = VI { unVI :: (Int,[([t],t)]) } deriving (Show)

instance (Pretty t) => Pretty (VIMap t) where
    pretty (VI (i,l)) = text "VIMAP" <$> int i <$> vsep (map pretty l)
 
emptyVIMap :: (Pretty t) => VIMap t 
emptyVIMap = VI (0,[])  

type AU m t = StateT (VIMap t) (C m)

getMap :: (Monad m, Pretty t) => AU m t [([t], t)]
getMap = gets $ snd . unVI

getCnt :: (Monad m, Pretty t) =>  AU m t Int
getCnt = gets $ fst . unVI

incrCnt :: (Monad m, Pretty t) => AU m t ()
incrCnt = do (VI (c,m)) <- get; put $ VI (c+1,m)

putImg :: (Monad m, Pretty t) => t -> [t] -> AU m t ()
putImg t i = do (VI (c,m)) <- get; put (VI (c,(i,t):m)); incrCnt

class AUnify t where
    aunify :: (Error e, MonadError e m) => [t] -> AU m t t
   
    lgg :: (Error e, MonadError e m, Pretty t) =>  [t] -> C m t
    lgg  ts = evalStateT (aunify ts) emptyVIMap
    


lggL :: (Pretty t, AUnify t, Error e, MonadError e m) => [[t]] -> C m [t]
lggL ls = evalStateT (mapM aunify ls)  emptyVIMap
  
                        
roots :: (Term t) => [t] -> ([t] -> t)
roots = root . head 

sameRoots :: (Term t) => [t] -> Bool
sameRoots []  = error "sameRoot: empty List"
sameRoots [x] = True
sameRoots (x1:x2:xs) = sameSymAtRoot x1 x2 && sameRoots (x2:xs)
