{-# 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"