> {-# OPTIONS_HADDOCK show-extensions #-}
>
> module LTK.Decide.GLPT (isGLPT, isGLPTM) where
> import qualified Data.Set as Set
> import LTK.FSA
> import LTK.Algebra
>
>
>
>
> isGLPT :: (Ord n, Ord e) => FSA n e -> Bool
> isGLPT :: FSA n e -> Bool
isGLPT = FSA ([Maybe n], [Symbol e]) e -> Bool
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
isGLPTM (FSA ([Maybe n], [Symbol e]) e -> Bool)
-> (FSA n e -> FSA ([Maybe n], [Symbol e]) e) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA ([Maybe n], [Symbol e]) e
forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid
J-trivial means MaM = MbM in all and only those cases where a=b
We're asking if X=e*M_e*e is J-trivial
That is, if for all a,b in X, XaX=XbX iff a=b.
It does not appear that a shortcut like that used to test for
local J-triviality is viable. If it turns out to be, then this
file will shrink dramatically and this test will speed up quite
a bit.
>
> isGLPTM :: (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Bool
> isGLPTM :: FSA (n, [Symbol e]) e -> Bool
isGLPTM FSA (n, [Symbol e]) e
m = (T n e -> Bool) -> [T n e] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all T n e -> Bool
f ([T n e] -> Bool) -> [T n e] -> Bool
forall a b. (a -> b) -> a -> b
$ Set (T n e) -> [T n e]
forall a. Set a -> [a]
Set.toList Set (T n e)
i
> where i :: Set (T n e)
i = FSA (n, [Symbol e]) e -> Set (T n e)
forall n e. (Ord n, Ord e) => FSA (n, [Symbol e]) e -> Set (T n e)
idempotents FSA (n, [Symbol e]) e
m
> x :: T n e -> [T n e]
x = Set (T n e) -> [T n e]
forall a. Set a -> [a]
Set.toList (Set (T n e) -> [T n e])
-> (T n e -> Set (T n e)) -> T n e -> [T n e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (n, [Symbol e]) e -> T n e -> Set (T n e)
forall n e. (Ord n, Ord e) => FSA (S n e) e -> T n e -> Set (T n e)
emee FSA (n, [Symbol e]) e
m
> f :: T n e -> Bool
f T n e
e = [Set (T n e)] -> Bool
forall a. Eq a => [a] -> Bool
isDistinct ([Set (T n e)] -> Bool)
-> ([T n e] -> [Set (T n e)]) -> [T n e] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (T n e -> Set (T n e)) -> [T n e] -> [Set (T n e)]
forall a b. (a -> b) -> [a] -> [b]
map (T n e -> T n e -> Set (T n e)
forall a. T n e -> State (a, [Symbol e]) -> Set (T n e)
g T n e
e) ([T n e] -> Bool) -> [T n e] -> Bool
forall a b. (a -> b) -> a -> b
$ T n e -> [T n e]
x T n e
e
> g :: T n e -> State (a, [Symbol e]) -> Set (T n e)
g T n e
e State (a, [Symbol e])
h = [Set (T n e)] -> Set (T n e)
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set (T n e)] -> Set (T n e)) -> [Set (T n e)] -> Set (T n e)
forall a b. (a -> b) -> a -> b
$ ([Symbol e] -> Set (T n e)) -> [[Symbol e]] -> [Set (T n e)]
forall a b. (a -> b) -> [a] -> [b]
map (([Symbol e] -> T n e -> Set (T n e))
-> T n e -> [Symbol e] -> Set (T n e)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (FSA (n, [Symbol e]) e -> [Symbol e] -> T n e -> Set (T n e)
forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (n, [Symbol e]) e
m) T n e
qi)
> [T n e -> [Symbol e]
forall a c. State (a, c) -> c
label T n e
a [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ State (a, [Symbol e]) -> [Symbol e]
forall a c. State (a, c) -> c
label State (a, [Symbol e])
h [Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ T n e -> [Symbol e]
forall a c. State (a, c) -> c
label T n e
b
> | T n e
a <- T n e -> [T n e]
x T n e
e, T n e
b <- T n e -> [T n e]
x T n e
e]
> qi :: T n e
qi = Set (T n e) -> T n e
forall a. Set a -> a
Set.findMin (Set (T n e) -> T n e) -> Set (T n e) -> T n e
forall a b. (a -> b) -> a -> b
$ FSA (n, [Symbol e]) e -> Set (T n e)
forall n e. FSA n e -> Set (State n)
initials FSA (n, [Symbol e]) e
m
> label :: State (a, c) -> c
label = (a, c) -> c
forall a b. (a, b) -> b
snd ((a, c) -> c) -> (State (a, c) -> (a, c)) -> State (a, c) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (a, c) -> (a, c)
forall n. State n -> n
nodeLabel
> isDistinct :: Eq a => [a] -> Bool
> isDistinct :: [a] -> Bool
isDistinct [] = Bool
True
> isDistinct (a
x:[a]
xs) = Bool -> Bool
not (a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem a
x [a]
xs) Bool -> Bool -> Bool
&& [a] -> Bool
forall a. Eq a => [a] -> Bool
isDistinct [a]
xs