{-# LANGUAGE PatternGuards #-}
----------------------------------------------------------------------
-- |
-- Module      :  Unbound.Perm
-- License     :  BSD-like (see LICENSE)
-- Maintainer  :  Stephanie Weirich <sweirich@cis.upenn.edu>
-- Portability :  portable
--
-- A slow, but hopefully correct implementation of permutations.
--
----------------------------------------------------------------------

module Unbound.PermM (
    Perm(..), permValid, single, compose, apply, support, isid, join, empty, restrict, mkPerm
  ) where

import Data.Monoid
import Data.List
import Data.Map (Map)
import Data.Function (on)
import qualified Data.Map as M
import qualified Data.Set as S
import Control.Arrow ((&&&))
import Control.Monad ((>=>))

-- | A /permutation/ is a bijective function from names to names
--   which is the identity on all but a finite set of names.  They
--   form the basis for nominal approaches to binding, but can
--   also be useful in general.
newtype Perm a = Perm (Map a a)

permValid :: Ord a => Perm a -> Bool
permValid (Perm p) = all (\(_,v) -> M.member v p) (M.assocs p)
  -- a Map sends every key uniquely to a value by construction.  So if
  -- every value is also a key, the sizes of the domain and range must
  -- be equal and hence the mapping is a bijection.

instance Ord a => Eq (Perm a) where
  (Perm p1) == (Perm p2) =
    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p1) &&
    all (\x -> M.findWithDefault x x p1 == M.findWithDefault x x p2) (M.keys p2)

instance Show a => Show (Perm a) where
  show (Perm p) = show p

-- | Apply a permutation to an element of the domain.
apply :: Ord a => Perm a -> a -> a
apply (Perm p) x = M.findWithDefault x x p

-- | Create a permutation which swaps two elements.
single :: Ord a => a -> a -> Perm a
single x y = if x == y then Perm M.empty else
    Perm (M.insert x y (M.insert y x M.empty))

-- | The empty (identity) permutation.
empty :: Perm a
empty = Perm M.empty

-- | Compose two permutations.  The right-hand permutation will be
--   applied first.
compose :: Ord a => Perm a -> Perm a -> Perm a
compose (Perm b) (Perm a) =
  Perm (M.fromList ([ (x,M.findWithDefault y y b) | (x,y) <- M.toList a]
         ++ [ (x, M.findWithDefault x x b) | x <- M.keys b, M.notMember x a]))

-- | Permutations form a monoid under composition.
instance Ord a => Monoid (Perm a) where
  mempty  = empty
  mappend = compose

-- | Is this the identity permutation?
isid :: Ord a => Perm a -> Bool
isid (Perm p) =
     M.foldrWithKey (\ a b r -> r && a == b) True p

-- | /Join/ two permutations by taking the union of their relation
--   graphs. Fail if they are inconsistent, i.e. map the same element
--   to two different elements.
join :: Ord a => Perm a -> Perm a -> Maybe (Perm a)
join (Perm p1) (Perm p2) =
     let overlap = M.intersectionWith (==) p1 p2 in
     if M.fold (&&) True overlap then
       Just (Perm (M.union p1 p2))
       else Nothing

-- | The /support/ of a permutation is the set of elements which are
--   not fixed.
support :: Ord a => Perm a -> [a]
support (Perm p) = [ x | x <- M.keys p, M.findWithDefault x x p /= x]

-- | Restrict a permutation to a certain domain.
restrict :: Ord a => Perm a -> [a] -> Perm a
restrict (Perm p) l = Perm (foldl' (\p' k -> M.delete k p') p l)

-- | A partial permutation consists of two maps, one in each direction
--   (inputs -> outputs and outputs -> inputs).
data PartialPerm a = PP (M.Map a a) (M.Map a a)
  deriving Show

emptyPP :: PartialPerm a
emptyPP = PP M.empty M.empty

extendPP :: Ord a => a -> a -> PartialPerm a -> Maybe (PartialPerm a)
extendPP x y pp@(PP mfwd mrev)
  | Just y' <- M.lookup x mfwd = if y == y' then Just pp
                                            else Nothing
  | Just x' <- M.lookup y mrev = if x == x' then Just pp
                                            else Nothing
  | otherwise = Just $ PP (M.insert x y mfwd) (M.insert y x mrev)

-- | Convert a partial permutation into a full permutation by closing
--   off any remaining open chains into a cycles.
ppToPerm :: Ord a => PartialPerm a -> Perm a
ppToPerm (PP mfwd mrev) = Perm $ foldr (uncurry M.insert) mfwd
                                       (map (findEnd &&& id) chainStarts)
        -- beginnings of open chains are elements which map to
        -- something in the forward direction but have no ancestor.
  where chainStarts = S.toList (M.keysSet mfwd `S.difference` M.keysSet mrev)
        findEnd x = case M.lookup x mfwd of
                      Nothing -> x
                      Just x' -> findEnd x'

-- | @mkPerm l1 l2@ creates a permutation that sends @l1@ to @l2@.
--   Fail if there is no such permutation, either because the lists
--   have different lengths or because they are inconsistent (which
--   can only happen if @l1@ or @l2@ have repeated elements).
mkPerm :: Ord a => [a] -> [a] -> Maybe (Perm a)
mkPerm xs ys
  | length xs /= length ys = Nothing
  | otherwise =
    fmap ppToPerm . ($emptyPP) . foldr (>=>) return $ zipWith extendPP xs ys