module Syntax.UnifyExp (
    
    Unify(..), AUnify(..)
    
    )where

import Data.Function (on)
import Data.List (transpose, find)

import Control.Monad.Error

import Syntax.Class
import Syntax.Context
import Syntax.Expressions
import Syntax.Type
import Syntax.Name
import Syntax.UnifyTy
import Syntax.Ppr

import Debug.Trace

instance Unify TExp where

    -- matching wildcards 
    match s@(TWildE i1 _) t     = checkMatch s t >> return nullSubst
    -- matching variables    
    match s@(TVarE i1 t1) t@(TVarE i2 t2)     = do 
        checkMatch s t
        if (i1 == i2) && (t1 == t2) then return nullSubst else return (i2 <~ s)
--        checkMatch s t >> return (i2 <~ s) -- is wrong but works better
    match s          t@(TVarE i _)          = checkMatch s t >> return (i <~ s)    
    match s t = if sameSymAtRoot s t 
                  then (matchL `on` subterms) s t
                  else nomatch "match (215)"  $ (show s) ++ "\n" ++(show t) ++ "\n"
            

-- | Auxiliary to bind terms to variable, check for consistency
varBind (TVarE n _ )(TVarE n' _)| n == n' = return nullSubst
varBind (TWildE _ _) _                    = return nullSubst -- TODO: ?create substitution?
varBind (TVarE n _)    t        
    | n `elem` getVarNames t             = throwError . strMsg $ "varBind: Occurs check failed!"
    | otherwise                          = return (n <~ t)   
varBind _ _                              = throwError . strMsg $ "varBind: Cannot bind to non-variable term"

instance AUnify TExp where
    aunify [] = error "aunify: empty list"
    aunify t | all isWild t = return (head t)
    aunify t
        | checkAU t   = let nonWilds = filter (not . isWild) t
                            wildSubterms = map (tWildE "x" . typeOf) . subterms $ head nonWilds
                            l = [ if isWild e then wildSubterms else subterms e | e <- t ]
                        in if [] `elem` l then return (head nonWilds)
                           else liftM (roots nonWilds) $ mapM aunify (transpose l)
        | otherwise   = bindVarAU t

checkAU l = let l' = filter (not . isWild) l
            in sameRoots l' && not (all isVar l')

bindVarAU :: (Error e, MonadError e m) => [TExp] -> AU m TExp TExp
bindVarAU img = getMap >>= maybe (mkVar img) (return . snd) . find matchimg
  where matchimg (img', _) = and $ zipWith equal img img'

mkVar :: (Error e, MonadError e m) => [TExp] -> AU m TExp TExp
mkVar vimg = do 
    vnm <- getCnt >>= return . mkName . ('a':) . show
    vty <- lift $ lgg (map typeOf vimg)
    var <- return $ TVarE  vnm vty
    putImg var vimg
    return var  
    
nomatch :: (Error e, MonadError e m) => String -> String -> m a
nomatch l s = throwError . strMsg $ "Expressions." ++ l ++ ": No Match! " ++ s