-- Required for Show instances
{-# LANGUAGE FlexibleContexts, UndecidableInstances #-}
-- Required more generally
{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}

{-# OPTIONS_GHC -Wall -fwarn-tabs #-}
----------------------------------------------------------------
--                                                  ~ 2012.02.17
-- |
-- Module      :  Control.Unification.Types
-- Copyright   :  Copyright (c) 2007--2012 wren ng thornton
-- License     :  BSD
-- Maintainer  :  wren@community.haskell.org
-- Stability   :  experimental
-- Portability :  semi-portable (MPTCs, fundeps,...)
--
-- This module defines the classes and primitive types used by
-- unification and related functions.
----------------------------------------------------------------
module Control.Unification.Types
    (
    -- * Mutable terms
      MutTerm(..)
    , freeze
    , unfreeze
    -- * Errors
    , UnificationFailure(..)
    -- * Basic type classes
    , Unifiable(..)
    , Variable(..)
    , BindingMonad(..)
    -- * Weighted path compression
    , Rank(..)
    , RankedBindingMonad(..)
    ) where

import Prelude hiding (mapM, sequence, foldr, foldr1, foldl, foldl1)

import Data.Word               (Word8)
import Data.Functor.Fixedpoint (Fix(..))
import Data.Traversable        (Traversable(..))
import Control.Applicative     (Applicative(..), (<$>))
import Control.Monad.Error     (Error(..))
----------------------------------------------------------------
----------------------------------------------------------------

-- | The type of terms generated by structures @t@ over variables
-- @v@. The structure type should implement 'Unifiable' and the
-- variable type should implement 'Variable'. The 'Show' instance
-- doesn't show the constructors, for legibility.
data MutTerm v t
    = MutVar  !v
    | MutTerm !(t (MutTerm v t))


instance (Show v, Show (t (MutTerm v t))) =>
    Show (MutTerm v t)
    where
    showsPrec p (MutVar  v) = showsPrec p v
    showsPrec p (MutTerm t) = showsPrec p t


-- | /O(n)/. Embed a pure term as a mutable term.
unfreeze :: (Functor t) => Fix t -> MutTerm v t
unfreeze = MutTerm . fmap unfreeze . unFix


-- | /O(n)/. Extract a pure term from a mutable term, or return
-- @Nothing@ if the mutable term actually contains variables. N.B.,
-- this function is pure, so you should manually apply bindings
-- before calling it.
freeze :: (Traversable t) => MutTerm v t -> Maybe (Fix t)
freeze (MutVar  _) = Nothing
freeze (MutTerm t) = Fix <$> mapM freeze t


----------------------------------------------------------------
-- TODO: provide zipper context so better error messages can be generated.
--
-- | The possible failure modes that could be encountered in
-- unification and related functions. While many of the functions
-- could be given more accurate types if we used ad-hoc combinations
-- of these constructors (i.e., because they can only throw one of
-- the errors), the extra complexity is not considered worth it.
data UnificationFailure v t
    
    = OccursIn v (MutTerm v t)
        -- ^ A cyclic term was encountered (i.e., the variable
        -- occurs free in a term it would have to be bound to in
        -- order to succeed). Infinite terms like this are not
        -- generally acceptable, so we do not support them. In logic
        -- programming this should simply be treated as unification
        -- failure; in type checking this should result in a \"could
        -- not construct infinite type @a = Foo a@\" error.
        --
        -- Note that since, by default, the library uses visited-sets
        -- instead of the occurs-check these errors will be thrown
        -- at the point where the cycle is dereferenced\/unrolled
        -- (e.g., when applying bindings), instead of at the time
        -- when the cycle is created. However, the arguments to
        -- this constructor should express the same context as if
        -- we had performed the occurs-check, in order for error
        -- messages to be intelligable.
    
    | TermMismatch (t (MutTerm v t)) (t (MutTerm v t))
        -- ^ The top-most level of the terms do not match (according
        -- to 'zipMatch'). In logic programming this should simply
        -- be treated as unification failure; in type checking this
        -- should result in a \"could not match expected type @Foo@
        -- with inferred type @Bar@\" error.
    
    | UnknownError String
        -- ^ Required for the @Error@ instance, which in turn is
        -- required to appease @ErrorT@ in the MTL. We do not use
        -- this anywhere.


-- Can't derive this because it's an UndecidableInstance
instance (Show (t (MutTerm v t)), Show v) =>
    Show (UnificationFailure v t)
    where
    -- TODO: implement 'showsPrec' instead
    show (OccursIn     v  t)  = "OccursIn ("++show v++") ("++show t++")"
    show (TermMismatch tl tr) = "TermMismatch ("++show tl++") ("++show tr++")"
    show (UnknownError msg)   = "UnknownError: "++msg

instance Error (UnificationFailure v t) where
    noMsg  = UnknownError ""
    strMsg = UnknownError

----------------------------------------------------------------

-- | An implementation of syntactically unifiable structure. The
-- @Traversable@ constraint is there because we also require terms
-- to be functors and require the distributivity of 'sequence' or
-- 'mapM'.
class (Traversable t) => Unifiable t where
    
    -- | Perform one level of equality testing for terms. If the
    -- term constructors are unequal then return @Nothing@; if they
    -- are equal, then return the one-level spine filled with pairs
    -- of subterms to be recursively checked.
    zipMatch :: t a -> t b -> Maybe (t (a,b))


-- | An implementation of unification variables.
class Variable v where
    
    -- | Determine whether two variables are equal /as variables/,
    -- without considering what they are bound to. The default
    -- implementation is:
    --
    -- > eqVar x y = getVarID x == getVarID y
    eqVar :: v -> v -> Bool
    eqVar x y = getVarID x == getVarID y
    
    -- | Return a unique identifier for this variable, in order to
    -- support the use of visited-sets instead of occurs-checks.
    getVarID :: v -> Int


----------------------------------------------------------------

-- | The basic class for generating, reading, and writing to bindings
-- stored in a monad. These three functionalities could be split
-- apart, but are combined in order to simplify contexts. Also,
-- because most functions reading bindings will also perform path
-- compression, there's no way to distinguish \"true\" mutation
-- from mere path compression.
--
-- The superclass constraints are there to simplify contexts, since
-- we make the same assumptions everywhere we use @BindingMonad@.

class (Unifiable t, Variable v, Applicative m, Monad m) =>
    BindingMonad v t m | m -> v t
    where
    
    -- | Given a variable pointing to @MutTerm v t@, return the
    -- term it's bound to, or @Nothing@ if the variable is unbound.
    lookupVar :: v -> m (Maybe (MutTerm v t))
    
    
    -- | Generate a new free variable guaranteed to be fresh in
    -- @m@.
    freeVar :: m v
    
    
    -- | Generate a new variable (fresh in @m@) bound to the given
    -- term. The default implementation is:
    --
    -- > newVar t = do { v <- freeVar ; bindVar v t ; return v }
    newVar :: MutTerm v t -> m v
    newVar t = do { v <- freeVar ; bindVar v t ; return v }
    
    
    -- | Bind a variable to a term, overriding any previous binding.
    bindVar :: v -> MutTerm v t -> m ()


----------------------------------------------------------------
-- | The target of variables for 'RankedBindingMonad's. In order
-- to support weighted path compression, each variable is bound to
-- both another term (possibly) and also a \"rank\" which is related
-- to the length of the variable chain to the term it's ultimately
-- bound to.
--
-- The rank can be at most @log V@, where @V@ is the total number
-- of variables in the unification problem. Thus, A @Word8@ is
-- sufficient for @2^(2^8)@ variables, which is far more than can
-- be indexed by 'getVarID' even on 64-bit architectures.
data Rank v t =
    Rank {-# UNPACK #-} !Word8 !(Maybe (MutTerm v t))

-- Can't derive this because it's an UndecidableInstance
instance (Show v, Show (t (MutTerm v t))) =>
    Show (Rank v t)
    where
    show (Rank n mb) = "Rank "++show n++" "++show mb

-- TODO: flatten the Rank.Maybe.MutTerm so that we can tell that if semiprune returns a bound variable then it's bound to a term (not another var)?

{-
instance Monoid (Rank v t) where
    mempty = Rank 0 Nothing
    mappend (Rank l mb) (Rank r _) = Rank (max l r) mb
-}


-- | An advanced class for 'BindingMonad's which also support
-- weighted path compression. The weightedness adds non-trivial
-- implementation complications; so even though weighted path
-- compression is asymptotically optimal, the constant factors may
-- make it worthwhile to stick with the unweighted path compression
-- supported by 'BindingMonad'.

class (BindingMonad v t m) => RankedBindingMonad v t m | m -> v t where
    -- | Given a variable pointing to @MutTerm v t@, return its
    -- rank and the term it's bound to.
    lookupRankVar :: v -> m (Rank v t)
    
    -- | Increase the rank of a variable by one.
    incrementRank :: v -> m ()
    
    -- | Bind a variable to a term and increment the rank at the
    -- same time. The default implementation is:
    --
    -- > incrementBindVar v t = do { incrementRank v ; bindVar v t }
    incrementBindVar :: v -> MutTerm v t -> m ()
    incrementBindVar v t = do { incrementRank v ; bindVar v t }

----------------------------------------------------------------
----------------------------------------------------------- fin.