module Syntax.Class.Unifier
 (
    Unify(..)
--    U,
--    Substitutable(..),
--    Substitution, Replacement, nullSubst, (<~), insertApply,
--    Unifiable(mgu, unify, match, matchesWithSubs),
--    matches, matchesLs, equal, equalLs, subsumes, subsumesLs, unifyVar, 
--    matchesWithSubsLs,
--    matchVar, flush,
--    
--    
--    zipPairsWithM,
    
    )
    where

import Control.Monad
import Control.Monad.Trans
import Control.Monad.Error
import Control.Monad.State (MonadState, StateT, execStateT, put, get)

import Data.List (insert, intersperse)
import Data.Maybe (isJust)
import Data.Function
import qualified Data.Traversable as T (sequence)

import Syntax.Context
import Syntax.Class.Term
import Syntax.Class.Subst hiding (merge)
import qualified Syntax.Class.Subst as Subst

import Debug.Trace

  
class (Term t, Substitutable t) => Unify t where
    
                    
    -- | The matching algorithm. @t1 `match` t2@ iff t2 is more general than t1
    --   Note, that different from unify, where
    --   'unify t1 t2 == unify t2 t1', 'match t1 t2 == match t2 t1' iff 
    --   't1 == t2'
    --   Substitution includes the identity substitution on variables !!!
    match :: (Error e, MonadError e m) => t -> t -> C m (Subst t)
    
    matches :: Monad m => t -> t -> C m Bool
    matches t1 t2 = liftM (const True) (match t1 t2) `safeCatchErrorC` const (return False)
    
    matchL :: (Error e, MonadError e m) => [t] -> [t] -> C m (Subst t)
    matchL tl sl = mapM (uncurry match) (zip tl sl) >>= foldM Subst.merge nullSubst
    matchesL :: Monad m => [t] -> [t] -> C m Bool
    matchesL t1 t2 = liftM (const True) (matchL t1 t2) `safeCatchErrorC` const (return False)

    
zipPairsWithM :: (MonadError e m) => (a -> b -> m c) -> [a] -> [b] -> m [c]       
zipPairsWithM _  [] [] = return  []
zipPairsWithM _ _ []   = fail "zipPairWithM: Lists have different lengths"
zipPairsWithM _ [] _   = fail "zipPairWithM: Lists have different lengths"
zipPairsWithM f (x:xs) (y:ys) =  liftM2 (:) (f x y) (zipPairsWithM f xs ys)
             