module StringRewriting.KnuthBendix (
    Order,
    knuthBendix,
    knuthBendixBy,
    module StringRewriting,
  ) where

import StringRewriting

import qualified Math.Algebra.Group.StringRewriting as SR

type Order a = a -> a -> Ordering

type GenOrder = Order Generator

data GenWithOrder = GWO
  { GenWithOrder -> GenOrder
genOrder :: GenOrder
  , GenWithOrder -> Generator
gen :: Generator
  }

instance Eq GenWithOrder where
    (GWO GenOrder
f Generator
x) == :: GenWithOrder -> GenWithOrder -> Bool
== (GWO GenOrder
_ Generator
y) = GenOrder
f Generator
x Generator
y Ordering -> Ordering -> Bool
forall a. Eq a => a -> a -> Bool
== Ordering
EQ

instance Ord GenWithOrder where
    compare :: GenWithOrder -> GenWithOrder -> Ordering
compare (GWO GenOrder
f Generator
x) (GWO GenOrder
_ Generator
y) = GenOrder
f Generator
x Generator
y

knuthBendix :: Set (Pair GWord) -> GeneratorsDescr -> StringRewriting
knuthBendix :: Set (Pair GWord) -> GeneratorsDescr -> StringRewriting
knuthBendix = GenOrder -> Set (Pair GWord) -> GeneratorsDescr -> StringRewriting
knuthBendixBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering) -> (Generator -> Int) -> GenOrder
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` Generator -> Int
numGenerator)

mapPair :: (a -> b) -> (a, a) -> (b, b)
mapPair :: (a -> b) -> (a, a) -> (b, b)
mapPair a -> b
f (a
x, a
y) = (a -> b
f a
x, a -> b
f a
y)

knuthBendixBy ::
    GenOrder ->
    Set (Pair GWord) ->
    GeneratorsDescr ->
    StringRewriting
knuthBendixBy :: GenOrder -> Set (Pair GWord) -> GeneratorsDescr -> StringRewriting
knuthBendixBy GenOrder
ord =
    Rules -> GeneratorsDescr -> StringRewriting
stringRewriting (Rules -> GeneratorsDescr -> StringRewriting)
-> (Set (Pair GWord) -> Rules)
-> Set (Pair GWord)
-> GeneratorsDescr
-> StringRewriting
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    [Rule] -> Rules
forall c v. UnsafeListable c v => [v] -> c
fromList ([Rule] -> Rules)
-> (Set (Pair GWord) -> [Rule]) -> Set (Pair GWord) -> Rules
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ((GWord, GWord) -> Rule) -> [(GWord, GWord)] -> [Rule]
forall a b. (a -> b) -> [a] -> [b]
map ((GWord -> GWord -> Rule) -> (GWord, GWord) -> Rule
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry GWord -> GWord -> Rule
rule) ([(GWord, GWord)] -> [Rule])
-> (Set (Pair GWord) -> [(GWord, GWord)])
-> Set (Pair GWord)
-> [Rule]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ((([GenWithOrder], [GenWithOrder]) -> (GWord, GWord))
-> [([GenWithOrder], [GenWithOrder])] -> [(GWord, GWord)]
forall a b. (a -> b) -> [a] -> [b]
map((([GenWithOrder], [GenWithOrder]) -> (GWord, GWord))
 -> [([GenWithOrder], [GenWithOrder])] -> [(GWord, GWord)])
-> ((GenWithOrder -> Generator)
    -> ([GenWithOrder], [GenWithOrder]) -> (GWord, GWord))
-> (GenWithOrder -> Generator)
-> [([GenWithOrder], [GenWithOrder])]
-> [(GWord, GWord)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.([GenWithOrder] -> GWord)
-> ([GenWithOrder], [GenWithOrder]) -> (GWord, GWord)
forall a b. (a -> b) -> (a, a) -> (b, b)
mapPair(([GenWithOrder] -> GWord)
 -> ([GenWithOrder], [GenWithOrder]) -> (GWord, GWord))
-> ((GenWithOrder -> Generator) -> [GenWithOrder] -> GWord)
-> (GenWithOrder -> Generator)
-> ([GenWithOrder], [GenWithOrder])
-> (GWord, GWord)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(GenWithOrder -> Generator) -> [GenWithOrder] -> GWord
forall a b. (a -> b) -> [a] -> [b]
map) GenWithOrder -> Generator
gen ([([GenWithOrder], [GenWithOrder])] -> [(GWord, GWord)])
-> (Set (Pair GWord) -> [([GenWithOrder], [GenWithOrder])])
-> Set (Pair GWord)
-> [(GWord, GWord)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    [([GenWithOrder], [GenWithOrder])]
-> [([GenWithOrder], [GenWithOrder])]
forall a. Ord a => [([a], [a])] -> [([a], [a])]
SR.knuthBendix ([([GenWithOrder], [GenWithOrder])]
 -> [([GenWithOrder], [GenWithOrder])])
-> (Set (Pair GWord) -> [([GenWithOrder], [GenWithOrder])])
-> Set (Pair GWord)
-> [([GenWithOrder], [GenWithOrder])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    (Pair [GenWithOrder] -> ([GenWithOrder], [GenWithOrder]))
-> [Pair [GenWithOrder]] -> [([GenWithOrder], [GenWithOrder])]
forall a b. (a -> b) -> [a] -> [b]
map Pair [GenWithOrder] -> ([GenWithOrder], [GenWithOrder])
forall a. Pair a -> (a, a)
unPair ([Pair [GenWithOrder]] -> [([GenWithOrder], [GenWithOrder])])
-> (Set (Pair GWord) -> [Pair [GenWithOrder]])
-> Set (Pair GWord)
-> [([GenWithOrder], [GenWithOrder])]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    ((Pair GWord -> Pair [GenWithOrder])
-> [Pair GWord] -> [Pair [GenWithOrder]]
forall a b. (a -> b) -> [a] -> [b]
map((Pair GWord -> Pair [GenWithOrder])
 -> [Pair GWord] -> [Pair [GenWithOrder]])
-> ((Generator -> GenWithOrder)
    -> Pair GWord -> Pair [GenWithOrder])
-> (Generator -> GenWithOrder)
-> [Pair GWord]
-> [Pair [GenWithOrder]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(GWord -> [GenWithOrder]) -> Pair GWord -> Pair [GenWithOrder]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap((GWord -> [GenWithOrder]) -> Pair GWord -> Pair [GenWithOrder])
-> ((Generator -> GenWithOrder) -> GWord -> [GenWithOrder])
-> (Generator -> GenWithOrder)
-> Pair GWord
-> Pair [GenWithOrder]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Generator -> GenWithOrder) -> GWord -> [GenWithOrder]
forall a b. (a -> b) -> [a] -> [b]
map) (GenOrder -> Generator -> GenWithOrder
GWO GenOrder
ord) ([Pair GWord] -> [Pair [GenWithOrder]])
-> (Set (Pair GWord) -> [Pair GWord])
-> Set (Pair GWord)
-> [Pair [GenWithOrder]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
    Set (Pair GWord) -> [Pair GWord]
forall c v. Listable c v => c -> [v]
toList