-- | This module provides an efficient implementation of finitely
-- supported permutations of atoms.  Compositions and inverses can
-- both be computed with O(/n/) 'Map' lookup operations.
--
-- This module exposes implementation details of the Nominal library,
-- and should not normally be imported. Users of the library should
-- only import the top-level module "Nominal".

module Nominal.Permutation where

import Data.List
import Data.Map (Map)
import qualified Data.Map as Map

import Nominal.Atom

-- ----------------------------------------------------------------------
-- * The monoid of permutations

-- | The monoid of finitely supported permutations on atoms.
newtype Perm = Perm (Map Atom Atom)
             deriving (Perm -> Perm -> Bool
(Perm -> Perm -> Bool) -> (Perm -> Perm -> Bool) -> Eq Perm
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Perm -> Perm -> Bool
== :: Perm -> Perm -> Bool
$c/= :: Perm -> Perm -> Bool
/= :: Perm -> Perm -> Bool
Eq, Int -> Perm -> ShowS
[Perm] -> ShowS
Perm -> String
(Int -> Perm -> ShowS)
-> (Perm -> String) -> ([Perm] -> ShowS) -> Show Perm
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Perm -> ShowS
showsPrec :: Int -> Perm -> ShowS
$cshow :: Perm -> String
show :: Perm -> String
$cshowList :: [Perm] -> ShowS
showList :: [Perm] -> ShowS
Show)

-- | The identity permutation. O(1).
p_identity :: Perm
p_identity :: Perm
p_identity = Map Atom Atom -> Perm
Perm Map Atom Atom
forall k a. Map k a
Map.empty

-- | Compose two permutations. O(/m/) where /m/ is the size of the
-- right permutation.
p_composeR :: Perm -> Perm -> Perm
p_composeR :: Perm -> Perm -> Perm
p_composeR s :: Perm
s@(Perm Map Atom Atom
sigma) (Perm Map Atom Atom
tau) = Map Atom Atom -> Perm
Perm Map Atom Atom
rho
  where
    rho :: Map Atom Atom
rho = (Atom -> Atom -> Map Atom Atom -> Map Atom Atom)
-> Map Atom Atom -> Map Atom Atom -> Map Atom Atom
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Atom -> Atom -> Map Atom Atom -> Map Atom Atom
f Map Atom Atom
sigma Map Atom Atom
tau
    f :: Atom -> Atom -> Map Atom Atom -> Map Atom Atom
f Atom
a Atom
b Map Atom Atom
rho = Map Atom Atom
rho'
      where
        c :: Atom
c = Perm -> Atom -> Atom
p_apply_atom Perm
s Atom
b
        rho' :: Map Atom Atom
rho'
          | Atom
a Atom -> Atom -> Bool
forall a. Eq a => a -> a -> Bool
== Atom
c = Atom -> Map Atom Atom -> Map Atom Atom
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Atom
a Map Atom Atom
rho
          | Bool
otherwise = Atom -> Atom -> Map Atom Atom -> Map Atom Atom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Atom
a Atom
c Map Atom Atom
rho

-- | Compose two permutations. O(/n/) where /n/ is the size of the
-- left permutation.  This also requires the inverse of the right
-- permutation as an input.
p_composeL :: Perm -> Perm -> Perm -> Perm
p_composeL :: Perm -> Perm -> Perm -> Perm
p_composeL (Perm Map Atom Atom
sigma) (Perm Map Atom Atom
tau) t' :: Perm
t'@(Perm Map Atom Atom
tau_inv) = Map Atom Atom -> Perm
Perm Map Atom Atom
rho
  where
    rho :: Map Atom Atom
rho = (Atom -> Atom -> Map Atom Atom -> Map Atom Atom)
-> Map Atom Atom -> Map Atom Atom -> Map Atom Atom
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey Atom -> Atom -> Map Atom Atom -> Map Atom Atom
f Map Atom Atom
tau Map Atom Atom
sigma
    f :: Atom -> Atom -> Map Atom Atom -> Map Atom Atom
f Atom
a Atom
b Map Atom Atom
rho = Map Atom Atom
rho'
      where
        c :: Atom
c = Perm -> Atom -> Atom
p_apply_atom Perm
t' Atom
a
        rho' :: Map Atom Atom
rho'
          | Atom
c Atom -> Atom -> Bool
forall a. Eq a => a -> a -> Bool
== Atom
b = Atom -> Map Atom Atom -> Map Atom Atom
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Atom
c Map Atom Atom
rho
          | Bool
otherwise = Atom -> Atom -> Map Atom Atom -> Map Atom Atom
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Atom
c Atom
b Map Atom Atom
rho

-- | Apply a permutation to an atom. O(1).
p_apply_atom :: Perm -> Atom -> Atom
p_apply_atom :: Perm -> Atom -> Atom
p_apply_atom (Perm Map Atom Atom
sigma) Atom
a =
  case Atom -> Map Atom Atom -> Maybe Atom
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Atom
a Map Atom Atom
sigma of
    Maybe Atom
Nothing -> Atom
a
    Just Atom
b -> Atom
b

-- | Swap /a/ and /b/. O(1).
p_swap :: Atom -> Atom -> Perm
p_swap :: Atom -> Atom -> Perm
p_swap Atom
a Atom
b
  | Atom
a Atom -> Atom -> Bool
forall a. Eq a => a -> a -> Bool
== Atom
b = Perm
p_identity
  | Bool
otherwise = Map Atom Atom -> Perm
Perm (Atom -> Atom -> Map Atom Atom
forall k a. k -> a -> Map k a
Map.singleton Atom
a Atom
b Map Atom Atom -> Map Atom Atom -> Map Atom Atom
forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Atom -> Atom -> Map Atom Atom
forall k a. k -> a -> Map k a
Map.singleton Atom
b Atom
a)

-- | Return the domain of a permutation. O(n).
p_domain :: Perm -> [Atom]
p_domain :: Perm -> [Atom]
p_domain (Perm Map Atom Atom
sigma) = Map Atom Atom -> [Atom]
forall k a. Map k a -> [k]
Map.keys Map Atom Atom
sigma

-- ----------------------------------------------------------------------
-- * The group of permutations

-- | The group of finitely supported permutations on atoms.  This is
-- an abstract type with no exposed structure.
data NominalPermutation = Permutation Perm Perm
  -- ^ Implementation note: If we used 'Perm' directly, inverting a
  -- permutation would be O(n). We make inverting O(1) by storing a
  -- permutation together with its inverse. Because of laziness, the
  -- inverse will not be computed unless it is used.
  deriving (NominalPermutation -> NominalPermutation -> Bool
(NominalPermutation -> NominalPermutation -> Bool)
-> (NominalPermutation -> NominalPermutation -> Bool)
-> Eq NominalPermutation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NominalPermutation -> NominalPermutation -> Bool
== :: NominalPermutation -> NominalPermutation -> Bool
$c/= :: NominalPermutation -> NominalPermutation -> Bool
/= :: NominalPermutation -> NominalPermutation -> Bool
Eq)

-- | A type synonym.
type Permutation = NominalPermutation

-- | The identity permutation. O(1).
perm_identity :: Permutation
perm_identity :: NominalPermutation
perm_identity = Perm -> Perm -> NominalPermutation
Permutation Perm
p_identity Perm
p_identity

-- | Compose two permutations. O(/m/) where /m/ is the size of the
-- right permutation.
perm_composeR :: Permutation -> Permutation -> Permutation
perm_composeR :: NominalPermutation -> NominalPermutation -> NominalPermutation
perm_composeR (Permutation Perm
sigma Perm
sinv) (Permutation Perm
tau Perm
tinv) = Perm -> Perm -> NominalPermutation
Permutation Perm
rho Perm
rinv
  where
    rho :: Perm
rho = Perm -> Perm -> Perm
p_composeR Perm
sigma Perm
tau
    rinv :: Perm
rinv = Perm -> Perm -> Perm -> Perm
p_composeL Perm
tinv Perm
sinv Perm
sigma

-- | Compose two permutations. O(/n/) where /n/ is the size of the
-- left permutation.
perm_composeL :: Permutation -> Permutation -> Permutation
perm_composeL :: NominalPermutation -> NominalPermutation -> NominalPermutation
perm_composeL (Permutation Perm
sigma Perm
sinv) (Permutation Perm
tau Perm
tinv) = Perm -> Perm -> NominalPermutation
Permutation Perm
rho Perm
rinv
  where
    rho :: Perm
rho = Perm -> Perm -> Perm -> Perm
p_composeL Perm
sigma Perm
tau Perm
tinv
    rinv :: Perm
rinv = Perm -> Perm -> Perm
p_composeR Perm
tinv Perm
sinv

-- | Invert a permutation. O(1).
perm_invert :: Permutation -> Permutation
perm_invert :: NominalPermutation -> NominalPermutation
perm_invert (Permutation Perm
sigma Perm
sinv) = Perm -> Perm -> NominalPermutation
Permutation Perm
sinv Perm
sigma

-- | Apply a permutation to an atom. O(1).
perm_apply_atom :: Permutation -> Atom -> Atom
perm_apply_atom :: NominalPermutation -> Atom -> Atom
perm_apply_atom (Permutation Perm
sigma Perm
sinv) = Perm -> Atom -> Atom
p_apply_atom Perm
sigma

-- | Swap /a/ and /b/. O(1).
perm_swap :: Atom -> Atom -> Permutation
perm_swap :: Atom -> Atom -> NominalPermutation
perm_swap Atom
a Atom
b = Perm -> Perm -> NominalPermutation
Permutation Perm
sigma Perm
sigma
  where
    sigma :: Perm
sigma = Atom -> Atom -> Perm
p_swap Atom
a Atom
b

-- | Swap the given pairs of atoms.
perm_swaps :: [(Atom,Atom)] -> Permutation
perm_swaps :: [(Atom, Atom)] -> NominalPermutation
perm_swaps [] = NominalPermutation
perm_identity
perm_swaps ((Atom
a,Atom
b):[(Atom, Atom)]
xs) = Atom -> Atom -> NominalPermutation
perm_swap Atom
a Atom
b NominalPermutation -> NominalPermutation -> NominalPermutation
`perm_composeL` [(Atom, Atom)] -> NominalPermutation
perm_swaps [(Atom, Atom)]
xs

-- | The domain of a permutation. O(/n/).
perm_domain :: Permutation -> [Atom]
perm_domain :: NominalPermutation -> [Atom]
perm_domain (Permutation Perm
sigma Perm
sinv) = Perm -> [Atom]
p_domain Perm
sigma

-- | Make a permutation from a list of swaps. This is mostly useful
-- for testing. O(/n/).
perm_of_swaps :: [(Atom, Atom)] -> Permutation
perm_of_swaps :: [(Atom, Atom)] -> NominalPermutation
perm_of_swaps [(Atom, Atom)]
xs = [(Atom, Atom)] -> NominalPermutation
aux [(Atom, Atom)]
xs where
  aux :: [(Atom, Atom)] -> NominalPermutation
aux [] = NominalPermutation
perm_identity
  aux ((Atom
a,Atom
b):[(Atom, Atom)]
t) = Atom -> Atom -> NominalPermutation
perm_swap Atom
a Atom
b NominalPermutation -> NominalPermutation -> NominalPermutation
`perm_composeL` [(Atom, Atom)] -> NominalPermutation
perm_of_swaps [(Atom, Atom)]
t

-- | Turn a permutation into a list of swaps. This is mostly useful
-- for testing. O(/n/).
swaps_of_perm :: Permutation -> [(Atom, Atom)]
swaps_of_perm :: NominalPermutation -> [(Atom, Atom)]
swaps_of_perm NominalPermutation
sigma = [ (Atom, Atom)
y | Just (Atom, Atom)
y <- [Maybe (Atom, Atom)]
ys ]
  where
    domain :: [Atom]
domain = NominalPermutation -> [Atom]
perm_domain NominalPermutation
sigma
    (NominalPermutation
tau, [Maybe (Atom, Atom)]
ys) = (NominalPermutation
 -> Atom -> (NominalPermutation, Maybe (Atom, Atom)))
-> NominalPermutation
-> [Atom]
-> (NominalPermutation, [Maybe (Atom, Atom)])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL NominalPermutation
-> Atom -> (NominalPermutation, Maybe (Atom, Atom))
f NominalPermutation
sigma [Atom]
domain
    f :: NominalPermutation
-> Atom -> (NominalPermutation, Maybe (Atom, Atom))
f NominalPermutation
acc Atom
a
      | Atom
a Atom -> Atom -> Bool
forall a. Eq a => a -> a -> Bool
== Atom
b = (NominalPermutation
acc', Maybe (Atom, Atom)
forall a. Maybe a
Nothing)
      | Bool
otherwise = (NominalPermutation
acc', (Atom, Atom) -> Maybe (Atom, Atom)
forall a. a -> Maybe a
Just (Atom
a, Atom
b))
      where
        b :: Atom
b = NominalPermutation -> Atom -> Atom
perm_apply_atom NominalPermutation
acc Atom
a
        acc' :: NominalPermutation
acc' = NominalPermutation -> NominalPermutation -> NominalPermutation
perm_composeL (Atom -> Atom -> NominalPermutation
perm_swap Atom
a Atom
b) NominalPermutation
acc