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