{-# LANGUAGE TupleSections, ScopedTypeVariables #-} module SemigroupPresentation.Solver ( Depth, Rule, solve, module SemigroupPresentation, ) where import SemigroupPresentation import Containers.Pair (swap) import Data.List (find, sortBy) type Depth = Maybe Int data RuleType = Direct Int | Inverse Int deriving (RuleType -> RuleType -> Bool (RuleType -> RuleType -> Bool) -> (RuleType -> RuleType -> Bool) -> Eq RuleType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: RuleType -> RuleType -> Bool $c/= :: RuleType -> RuleType -> Bool == :: RuleType -> RuleType -> Bool $c== :: RuleType -> RuleType -> Bool Eq, Eq RuleType Eq RuleType -> (RuleType -> RuleType -> Ordering) -> (RuleType -> RuleType -> Bool) -> (RuleType -> RuleType -> Bool) -> (RuleType -> RuleType -> Bool) -> (RuleType -> RuleType -> Bool) -> (RuleType -> RuleType -> RuleType) -> (RuleType -> RuleType -> RuleType) -> Ord RuleType RuleType -> RuleType -> Bool RuleType -> RuleType -> Ordering RuleType -> RuleType -> RuleType forall a. Eq a -> (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: RuleType -> RuleType -> RuleType $cmin :: RuleType -> RuleType -> RuleType max :: RuleType -> RuleType -> RuleType $cmax :: RuleType -> RuleType -> RuleType >= :: RuleType -> RuleType -> Bool $c>= :: RuleType -> RuleType -> Bool > :: RuleType -> RuleType -> Bool $c> :: RuleType -> RuleType -> Bool <= :: RuleType -> RuleType -> Bool $c<= :: RuleType -> RuleType -> Bool < :: RuleType -> RuleType -> Bool $c< :: RuleType -> RuleType -> Bool compare :: RuleType -> RuleType -> Ordering $ccompare :: RuleType -> RuleType -> Ordering $cp1Ord :: Eq RuleType Ord) type Rule = (GWord, GWord) solve :: MonadFail m => String -> SemigroupPresentation -> Depth -> String -> m [Rule] solve :: String -> SemigroupPresentation -> Depth -> String -> m [Rule] solve String strRes SemigroupPresentation sp Depth depth String strIni = do let gd :: GeneratorsDescr gd = SemigroupPresentation spSemigroupPresentation -> Getting GeneratorsDescr SemigroupPresentation GeneratorsDescr -> GeneratorsDescr forall s a. s -> Getting a s a -> a ^.Getting GeneratorsDescr SemigroupPresentation GeneratorsDescr Lens' SemigroupPresentation GeneratorsDescr generatorsDescr [Generator] gwRes <- (String -> m Generator) -> [String] -> m [Generator] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse (GeneratorsDescr gd GeneratorsDescr -> String -> m Generator forall c k v (m :: * -> *). (Indexable c k v, MonadFail m) => c -> k -> m v !?) ([String] -> m [Generator]) -> [String] -> m [Generator] forall a b. (a -> b) -> a -> b $ String -> [String] words String strRes [Generator] gwIni <- (String -> m Generator) -> [String] -> m [Generator] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse (GeneratorsDescr gd GeneratorsDescr -> String -> m Generator forall c k v (m :: * -> *). (Indexable c k v, MonadFail m) => c -> k -> m v !?) ([String] -> m [Generator]) -> [String] -> m [Generator] forall a b. (a -> b) -> a -> b $ String -> [String] words String strIni let rels :: [Pair [Generator]] rels = SemigroupPresentation spSemigroupPresentation -> Getting Relations SemigroupPresentation Relations -> Relations forall s a. s -> Getting a s a -> a ^.Getting Relations SemigroupPresentation Relations Lens' SemigroupPresentation Relations relations Relations -> (Relations -> [Pair [Generator]]) -> [Pair [Generator]] forall a b. a -> (a -> b) -> b & Relations -> [Pair [Generator]] forall c v. Listable c v => c -> [v] toList rules :: Map RuleType Rule rules = [(RuleType, Rule)] -> Map RuleType Rule forall c v. FastUnsafeListable c v => [v] -> c fromDistinctAscList ([(RuleType, Rule)] -> Map RuleType Rule) -> [(RuleType, Rule)] -> Map RuleType Rule forall a b. (a -> b) -> a -> b $ [RuleType] -> [Rule] -> [(RuleType, Rule)] forall a b. [a] -> [b] -> [(a, b)] zip (Int -> RuleType Direct (Int -> RuleType) -> [Int] -> [RuleType] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Int 0..]) (Pair [Generator] -> Rule forall a. Pair a -> (a, a) unPair (Pair [Generator] -> Rule) -> [Pair [Generator]] -> [Rule] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Pair [Generator]] rels) [(RuleType, Rule)] -> [(RuleType, Rule)] -> [(RuleType, Rule)] forall a. [a] -> [a] -> [a] ++ [RuleType] -> [Rule] -> [(RuleType, Rule)] forall a b. [a] -> [b] -> [(a, b)] zip (Int -> RuleType Inverse (Int -> RuleType) -> [Int] -> [RuleType] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Int 0..]) (Pair [Generator] -> Rule forall a. Pair a -> (a, a) unPair (Pair [Generator] -> Rule) -> (Pair [Generator] -> Pair [Generator]) -> Pair [Generator] -> Rule forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> Pair [Generator] -> Pair [Generator] forall a. Pair a -> Pair a swap (Pair [Generator] -> Rule) -> [Pair [Generator]] -> [Rule] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [Pair [Generator]] rels) fs :: [([RuleType], [Generator])] fs = Map RuleType Rule -> [Generator] -> [([RuleType], [Generator])] firstStep Map RuleType Rule rules [Generator] gwIni gwsNext :: [[Generator]] gwsNext = (([RuleType], [Generator]) -> [Generator]) -> [([RuleType], [Generator])] -> [[Generator]] forall a b. (a -> b) -> [a] -> [b] map ([RuleType], [Generator]) -> [Generator] forall a b. (a, b) -> b snd [([RuleType], [Generator])] fs [Generator] -> Set [Generator] -> Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> m [Rule] forall (m :: * -> *). MonadFail m => [Generator] -> Set [Generator] -> Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> m [Rule] solve' [Generator] gwRes ([[Generator]] -> Set [Generator] forall c v. UnsafeListable c v => [v] -> c fromList ([[Generator]] -> Set [Generator]) -> [[Generator]] -> Set [Generator] forall a b. (a -> b) -> a -> b $ [Generator] gwIni [Generator] -> [[Generator]] -> [[Generator]] forall c v. Insertable c v => v -> c -> c +> [[Generator]] gwsNext) Map RuleType Rule rules Depth depth [([RuleType], [Generator])] fs solve' :: MonadFail m => GWord -> Set GWord -> Map RuleType Rule -> Depth -> [([RuleType], GWord)] -> m [Rule] solve' :: [Generator] -> Set [Generator] -> Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> m [Rule] solve' [Generator] _ Set [Generator] _ Map RuleType Rule _ Depth _ [] = String -> m [Rule] forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Analysis depth limit reached" solve' [Generator] res Set [Generator] rgws Map RuleType Rule rs Depth d [([RuleType], [Generator])] gws = let ([([RuleType], [Generator])] gwsOth, [([RuleType], [Generator])] gwsNew) = Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> ([([RuleType], [Generator])], [([RuleType], [Generator])]) minStep Map RuleType Rule rs Depth d [([RuleType], [Generator])] gws in case (([RuleType], [Generator]) -> Bool) -> [([RuleType], [Generator])] -> Maybe ([RuleType], [Generator]) forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a find (([Generator] -> [Generator] -> Bool forall a. Eq a => a -> a -> Bool == [Generator] res) ([Generator] -> Bool) -> (([RuleType], [Generator]) -> [Generator]) -> ([RuleType], [Generator]) -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . ([RuleType], [Generator]) -> [Generator] forall a b. (a, b) -> b snd) [([RuleType], [Generator])] gwsNew of Just ([RuleType] rts, [Generator] _) -> (RuleType -> m Rule) -> [RuleType] -> m [Rule] forall (t :: * -> *) (f :: * -> *) a b. (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b) traverse (Map RuleType Rule rs Map RuleType Rule -> RuleType -> m Rule forall c k v (m :: * -> *). (Indexable c k v, MonadFail m) => c -> k -> m v !?) ([RuleType] -> m [Rule]) -> [RuleType] -> m [Rule] forall a b. (a -> b) -> a -> b $ [RuleType] -> [RuleType] forall a. [a] -> [a] reverse [RuleType] rts Maybe ([RuleType], [Generator]) Nothing -> do let gws' :: [([RuleType], [Generator])] gws' = [([RuleType], [Generator])] gwsOth [([RuleType], [Generator])] -> [([RuleType], [Generator])] -> [([RuleType], [Generator])] forall a. [a] -> [a] -> [a] ++ (([RuleType], [Generator]) -> Bool) -> [([RuleType], [Generator])] -> [([RuleType], [Generator])] forall a. (a -> Bool) -> [a] -> [a] filter (([Generator] -> Set [Generator] -> Bool forall c v. Containable c v => v -> c -> Bool `notMember` Set [Generator] rgws) ([Generator] -> Bool) -> (([RuleType], [Generator]) -> [Generator]) -> ([RuleType], [Generator]) -> Bool forall b c a. (b -> c) -> (a -> b) -> a -> c . ([RuleType], [Generator]) -> [Generator] forall a b. (a, b) -> b snd) [([RuleType], [Generator])] gwsNew rgws' :: Set [Generator] rgws' = Set [Generator] rgws Set [Generator] -> Set [Generator] -> Set [Generator] forall c. Operable c => c -> c -> c \/ [[Generator]] -> Set [Generator] forall c v. UnsafeListable c v => [v] -> c fromList (([RuleType], [Generator]) -> [Generator] forall a b. (a, b) -> b snd (([RuleType], [Generator]) -> [Generator]) -> [([RuleType], [Generator])] -> [[Generator]] forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b <$> [([RuleType], [Generator])] gwsNew) [Generator] -> Set [Generator] -> Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> m [Rule] forall (m :: * -> *). MonadFail m => [Generator] -> Set [Generator] -> Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> m [Rule] solve' [Generator] res Set [Generator] rgws' Map RuleType Rule rs Depth d [([RuleType], [Generator])] gws' firstStep :: Map RuleType Rule -> GWord -> [([RuleType], GWord)] firstStep :: Map RuleType Rule -> [Generator] -> [([RuleType], [Generator])] firstStep Map RuleType Rule rs [Generator] gw = do (RuleType rt, [Generator] gw') <- Map RuleType Rule -> [Generator] -> [(RuleType, [Generator])] step Map RuleType Rule rs [Generator] gw ([RuleType], [Generator]) -> [([RuleType], [Generator])] forall (m :: * -> *) a. Monad m => a -> m a return ([RuleType rt], [Generator] gw') minStep :: Map RuleType Rule -> Depth -> [([RuleType], GWord)] -> ([([RuleType], GWord)], [([RuleType], GWord)]) minStep :: Map RuleType Rule -> Depth -> [([RuleType], [Generator])] -> ([([RuleType], [Generator])], [([RuleType], [Generator])]) minStep Map RuleType Rule _ Depth _ [] = ([], []) minStep Map RuleType Rule rs Depth d [([RuleType], [Generator])] gws = let (([RuleType] rts, [Generator] gw) : [([RuleType], [Generator])] gws') = (([RuleType], [Generator]) -> ([RuleType], [Generator]) -> Ordering) -> [([RuleType], [Generator])] -> [([RuleType], [Generator])] forall a. (a -> a -> Ordering) -> [a] -> [a] sortBy (Int -> Int -> Ordering forall a. Ord a => a -> a -> Ordering compare (Int -> Int -> Ordering) -> (([RuleType], [Generator]) -> Int) -> ([RuleType], [Generator]) -> ([RuleType], [Generator]) -> Ordering forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c `on` ([Generator] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length ([Generator] -> Int) -> (([RuleType], [Generator]) -> [Generator]) -> ([RuleType], [Generator]) -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . ([RuleType], [Generator]) -> [Generator] forall a b. (a, b) -> b snd)) [([RuleType], [Generator])] gws in ([([RuleType], [Generator])] gws', case Depth d of Just Int d' | [RuleType] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [RuleType] rts Int -> Int -> Bool forall a. Ord a => a -> a -> Bool >= Int d' -> [] Depth _ -> do (RuleType rt, [Generator] gw') <- Map RuleType Rule -> [Generator] -> [(RuleType, [Generator])] step Map RuleType Rule rs [Generator] gw ([RuleType], [Generator]) -> [([RuleType], [Generator])] forall (m :: * -> *) a. Monad m => a -> m a return (RuleType rtRuleType -> [RuleType] -> [RuleType] forall a. a -> [a] -> [a] :[RuleType] rts, [Generator] gw') ) step :: Map RuleType Rule -> GWord -> [(RuleType, GWord)] step :: Map RuleType Rule -> [Generator] -> [(RuleType, [Generator])] step Map RuleType Rule rs [Generator] gw = do (RuleType rt, Rule rule) <- Map RuleType Rule -> [(RuleType, Rule)] forall c v. Listable c v => c -> [v] toList Map RuleType Rule rs [Generator] gw' <- Rule -> [Generator] -> [[Generator]] forall a. Eq a => ([a], [a]) -> [a] -> [[a]] allRewrites Rule rule [Generator] gw (RuleType, [Generator]) -> [(RuleType, [Generator])] forall (m :: * -> *) a. Monad m => a -> m a return (RuleType rt, [Generator] gw') allRewrites :: Eq a => ([a], [a]) -> [a] -> [[a]] allRewrites :: ([a], [a]) -> [a] -> [[a]] allRewrites ([a] from, [a] to) [a] ini = do Int i <- [Int 0..[a] -> Int forall (t :: * -> *) a. Foldable t => t a -> Int length [a] ini] let ([a] s, [a] f) = Int -> [a] -> ([a], [a]) forall a. Int -> [a] -> ([a], [a]) splitAt Int i [a] ini [a] f' <- [a] from [a] -> [a] -> [[a]] forall (m :: * -> *) a. (MonadFail m, Eq a) => [a] -> [a] -> m [a] `prefixOf` [a] f [a] -> [[a]] forall (m :: * -> *) a. Monad m => a -> m a return ([a] -> [[a]]) -> [a] -> [[a]] forall a b. (a -> b) -> a -> b $ [a] s [a] -> [a] -> [a] forall a. [a] -> [a] -> [a] ++ [a] to [a] -> [a] -> [a] forall a. [a] -> [a] -> [a] ++ [a] f' prefixOf :: (MonadFail m, Eq a) => [a] -> [a] -> m [a] prefixOf :: [a] -> [a] -> m [a] prefixOf [] [a] s = [a] -> m [a] forall (m :: * -> *) a. Monad m => a -> m a return [a] s prefixOf [a] _ [] = String -> m [a] forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Substring longer than string" prefixOf (a c1:[a] t) (a c2:[a] s) | a c1 a -> a -> Bool forall a. Eq a => a -> a -> Bool == a c2 = [a] -> [a] -> m [a] forall (m :: * -> *) a. (MonadFail m, Eq a) => [a] -> [a] -> m [a] prefixOf [a] t [a] s | Bool otherwise = String -> m [a] forall (m :: * -> *) a. MonadFail m => String -> m a fail String "Substring is not prefix of string"