module Control.Monad.Unify.Class where

import Prelude (Unit, unit, ($))

import Control.Applicative (pure)
import Control.Bind (bind)
import Control.MonadPlus (class MonadPlus, empty)
import Control.Monad.State.Trans (StateT)
import Control.Monad.Reader.Trans (ReaderT)
import Control.Monad.Trans.Class (lift)
import Data.Traversable (class Traversable, traverse)
import Data.Tuple (Tuple(..))
import Data.Lazy (Lazy, force)
import Data.Ord (class Ord)

data Stream k = StreamCons k (Lazy (Stream k))

pop :: forall k. Stream k -> Tuple k (Stream k)
pop (StreamCons k lks) = Tuple k (force lks)

class Ord k <= UnificationVariable k where
    variables :: Stream k

data ComparisonAction k f
    = Merge k k
    | Store k (f k)
    | Fail

class (Unifiable k f, MonadPlus m) <= MonadUnify k f m | m -> k, m -> f where
    fresh :: m k
    merge :: k -> k -> m Unit
    store :: k -> f k -> m Unit
    reify :: f k -> m (f k)

class (UnificationVariable k, Traversable f) <= Unifiable k f where
    variable :: k -> f k
    squash :: f (f k) -> f k
    alongside :: f k -> f k -> f (ComparisonAction k f)

unify :: forall k f m. MonadUnify k f m => f k -> f k -> m Unit
unify f1 f2 =
    do
       _ <- traverse process $ alongside f1 f2
       pure unit
    where
      process (Merge k1 k2) = merge k1 k2
      process (Store k f) = store k f
      process Fail = empty

instance MonadUnify k f m => MonadUnify k f (StateT s m) where
    fresh = lift fresh
    merge m k = lift $ merge m k
    store k f = lift $ store k f
    reify f = lift $ reify f

instance MonadUnify k f m => MonadUnify k f (ReaderT r m) where
    fresh = lift fresh
    merge m k = lift $ merge m k
    store k f = lift $ store k f
    reify f = lift $ reify f