> {-# OPTIONS_HADDOCK show-extensions #-}
> {-# Language
>   CPP,
>   FlexibleContexts,
>   FlexibleInstances,
>   MultiParamTypeClasses,
>   Trustworthy
>   #-}

#if !defined(MIN_VERSION_base)
# define MIN_VERSION_base(a,b,c) 0
#endif

> {-|
> Module    : LTK.FSA
> Copyright : (c) 2014-2023 Dakotah Lambert
> License   : MIT

> The purpose of this module is to define an interface to a generic,
> reusable impementation of finite-state automata (FSAs).  The primary
> motivation for this is to allow for efficient analysis of stringsets
> in a linguistic context, although the nature of the project should 
> allow more general use.
> -}
> module LTK.FSA
>        ( FSA(..)
>        , states
>        , isNull
>        , follow
>        , accepts
>        -- * Constructing simple automata
>        , totalWithAlphabet
>        , emptyWithAlphabet
>        , emptyLanguage
>        , singletonWithAlphabet
>        , singletonLanguage
>        -- * Derived automata
>        , brzozowskiDerivative
>        , loopify
>        , tierify
>        , neutralize
>        , quotLeft
>        , quotMid
>        , quotRight
>        , kleeneClosure
>        , powersetGraph
>        , syntacticMonoid
>        , residue
>        , coresidue
>        -- * Primitive ideals
>        , primitiveIdeal2
>        , primitiveIdealL
>        , primitiveIdealR
>        -- * Transformations
>        , flatIntersection
>        , flatUnion
>        , flatInfiltration
>        , flatShuffle
>        , LTK.FSA.reverse
>        , autDifference
>        , autInfiltration
>        , autShuffle
>        , complement
>        , complementDeterministic
>        , determinize
>        -- ** Minimization
>        , minimize
>        , minimizeDeterministic
>        , normalize
>        , trimUnreachables
>        -- *** Equivalence Classes
>        , minimizeOver
>        , nerode
>        , hEquivalence
>        , jEquivalence
>        , trivialUnder
>        -- ** Alphabetic Transformations
>        , extendAlphabetTo
>        , semanticallyExtendAlphabetTo
>        , contractAlphabetTo
>        , forceAlphabetTo
>        , desemantify
>        , renameSymbolsBy
>        -- ** Transformations of 'State' labels
>        , renameStatesBy
>        , renameStates
>        -- * Miscellaneous
>        , State(..)
>        , Symbol(..)
>        , unsymbols
>        , Transition(..)
>        , module LTK.Containers
>        ) where

> import Control.DeepSeq (NFData, rnf)
#if !MIN_VERSION_base(4,8,0)
> import Control.Applicative (Applicative, pure, (<*>))
> import Data.Functor ((<$>))
> import Data.Monoid (Monoid, mappend, mempty)
#endif
#if MIN_VERSION_base(4,9,0)
#if !MIN_VERSION_base(4,11,0)
> import safe Data.Semigroup (Semigroup, (<>))
#endif
#endif
> import Data.Maybe (fromMaybe)
> import Data.Set (Set)
> import qualified Data.Set as Set
> import qualified Data.Map.Lazy as Map

> import Control.Parallel (par, pseq)

> import LTK.Containers


Data Structures
===============

An FSA has four main parts:

* a set of symbols representing its alphabet
* a set of edges that describe transitions from state to state
* a set of initial states, from which computations begin
* a set of final states, which determine computational success

Further, given an FSA F, if for every symbol a in the alphabet of F
and for every state q in the set of states in F, there exists exactly
one edge exiting q labelled with a, and if F has exactly one initial
state, then F can be described as a deterministic finite-state
automaton, or DFA.  Determinism allows for useful optimizations in
some operations, but can be slow to verify.  This module sacrifices
space for speed, treating determinism as a property of the datatype
itself.

> -- |A finite-state automaton (FSA) is represented by a directed
> -- graph, the edges of which are labelled by formal symbols.
> data FSA n e
>     = FSA
>       { -- |@since 0.3
>         forall n e. FSA n e -> Set e
sigma            ::  Set e
>       , forall n e. FSA n e -> Set (Transition n e)
transitions      ::  Set (Transition n e)
>       , forall n e. FSA n e -> Set (State n)
initials         ::  Set (State n)
>       , forall n e. FSA n e -> Set (State n)
finals           ::  Set (State n)
>       , forall n e. FSA n e -> Bool
isDeterministic  ::  Bool
>       }
>     deriving (Int -> FSA n e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show e, Show n) => Int -> FSA n e -> ShowS
forall n e. (Show e, Show n) => [FSA n e] -> ShowS
forall n e. (Show e, Show n) => FSA n e -> String
showList :: [FSA n e] -> ShowS
$cshowList :: forall n e. (Show e, Show n) => [FSA n e] -> ShowS
show :: FSA n e -> String
$cshow :: forall n e. (Show e, Show n) => FSA n e -> String
showsPrec :: Int -> FSA n e -> ShowS
$cshowsPrec :: forall n e. (Show e, Show n) => Int -> FSA n e -> ShowS
Show, ReadPrec [FSA n e]
ReadPrec (FSA n e)
ReadS [FSA n e]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall n e. (Read e, Read n, Ord e, Ord n) => ReadPrec [FSA n e]
forall n e. (Read e, Read n, Ord e, Ord n) => ReadPrec (FSA n e)
forall n e.
(Read e, Read n, Ord e, Ord n) =>
Int -> ReadS (FSA n e)
forall n e. (Read e, Read n, Ord e, Ord n) => ReadS [FSA n e]
readListPrec :: ReadPrec [FSA n e]
$creadListPrec :: forall n e. (Read e, Read n, Ord e, Ord n) => ReadPrec [FSA n e]
readPrec :: ReadPrec (FSA n e)
$creadPrec :: forall n e. (Read e, Read n, Ord e, Ord n) => ReadPrec (FSA n e)
readList :: ReadS [FSA n e]
$creadList :: forall n e. (Read e, Read n, Ord e, Ord n) => ReadS [FSA n e]
readsPrec :: Int -> ReadS (FSA n e)
$creadsPrec :: forall n e.
(Read e, Read n, Ord e, Ord n) =>
Int -> ReadS (FSA n e)
Read)

> -- |The collection of all states in an FSA.
> states :: (Ord e, Ord n) => FSA n e -> Set (State n)
> states :: forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f = forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll [forall n e. FSA n e -> Set (State n)
initials FSA n e
f, forall n e. FSA n e -> Set (State n)
finals FSA n e
f, Set (State n)
others]
>    where others :: Set (State n)
others           = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse forall {c} {n} {e}.
Container c (State n) =>
Transition n e -> c -> c
extractStates forall c a. Container c a => c
empty Set (Transition n e)
ts
>          extractStates :: Transition n e -> c -> c
extractStates Transition n e
t  = forall c a. Container c a => a -> c -> c
insert (forall n e. Transition n e -> State n
source Transition n e
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a. Container c a => a -> c -> c
insert (forall n e. Transition n e -> State n
destination Transition n e
t)
>          ts :: Set (Transition n e)
ts               = forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
f

> -- |An automaton accepting every string over a given alphabet.
> totalWithAlphabet :: (Ord e, Enum n, Ord n) => Set e -> FSA n e
> totalWithAlphabet :: forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet Set e
as = forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA Set e
as Set (Transition n e)
trans (forall c a. Container c a => a -> c
singleton State n
q) (forall c a. Container c a => a -> c
singleton State n
q) Bool
True
>     where trans :: Set (Transition n e)
trans  = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                    (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall n e. Symbol e -> State n -> State n -> Transition n e
`Transition` State n
q) State n
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Symbol e
Symbol)
>                    Set e
as
>           q :: State n
q      = forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum Int
0

> -- |An automaton accepting no strings over a given alphabet.
> emptyWithAlphabet :: (Ord e, Enum n, Ord n) => Set e -> FSA n e
> emptyWithAlphabet :: forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
emptyWithAlphabet Set e
as = (forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet Set e
as) {finals :: Set (State n)
finals = forall c a. Container c a => c
empty}

> -- |A specialization of 'emptyWithAlphabet' where the alphabet
> -- is itself empty.
> emptyLanguage :: (Ord e, Ord n, Enum n) => FSA n e
> emptyLanguage :: forall e n. (Ord e, Ord n, Enum n) => FSA n e
emptyLanguage = forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
emptyWithAlphabet forall c a. Container c a => c
empty

A singleton FSA is one that accepts exactly one (possibly-empty)
string.  The number of states in such an FSA is equal to the length of
the string plus two.

> -- |An automaton that accepts only the given string,
> -- over a given alphabet.
> singletonWithAlphabet :: (Ord e, Enum n, Ord n) =>
>                          Set e -> [e] -> FSA n e
> singletonWithAlphabet :: forall e n. (Ord e, Enum n, Ord n) => Set e -> [e] -> FSA n e
singletonWithAlphabet Set e
as [e]
str
>     = FSA
>       { sigma :: Set e
sigma = Set e
as
>       , transitions :: Set (Transition n e)
transitions = [e] -> Set (Transition n e)
trans [e]
str
>       , initials :: Set (State n)
initials = Set (State n)
begins
>       , finals :: Set (State n)
finals = Set (State n)
fins
>       , isDeterministic :: Bool
isDeterministic = Bool
True
>       }
>     where trans :: [e] -> Set (Transition n e)
trans [e]
xs = [e] -> n -> Set (Transition n e)
trans' [e]
xs (forall a. Enum a => Int -> a
toEnum Int
1) forall c a. Container c a => c -> c -> c
`union` Set (Transition n e)
failTransitions
>           trans' :: [e] -> n -> Set (Transition n e)
trans' [] n
n
>               = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (\e
a -> forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (forall e. e -> Symbol e
Symbol e
a) (forall n. n -> State n
State n
n) State n
qfail) Set e
as
>           trans' (e
x:[e]
xs) n
n
>               = let m :: n
m = forall a. Enum a => a -> a
succ n
n
>                 in forall c a. Container c a => c -> c -> c
union ([e] -> n -> Set (Transition n e)
trans' [e]
xs n
m) forall a b. (a -> b) -> a -> b
$
>                    forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                    (\e
y ->
>                     forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (forall e. e -> Symbol e
Symbol e
y) (forall n. n -> State n
State n
n) forall a b. (a -> b) -> a -> b
$
>                     if e
x forall a. Eq a => a -> a -> Bool
== e
y then forall n. n -> State n
State n
m else State n
qfail
>                    ) Set e
as
>           qfail :: State n
qfail = forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum Int
0
>           failTransitions :: Set (Transition n e)
failTransitions
>               = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                 (\e
a -> forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (forall e. e -> Symbol e
Symbol e
a) State n
qfail State n
qfail)
>                 Set e
as
>           begins :: Set (State n)
begins  =  forall c a. Container c a => a -> c
singleton (forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum Int
1)
>           qlast :: Int
qlast   =  (forall a. Num a => a -> a -> a
+ Int
1) forall a b. (a -> b) -> a -> b
$ forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size [e]
str
>           fins :: Set (State n)
fins    =  forall c a. Container c a => a -> c
singleton (forall n. n -> State n
State forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum Int
qlast)

> -- |An automaton that accepts only the given string,
> -- over the minimal alphabet required to represent this string.
> singletonLanguage :: (Ord e, Enum n, Ord n) => [e] -> FSA n e
> singletonLanguage :: forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage [e]
s = forall e n. (Ord e, Enum n, Ord n) => Set e -> [e] -> FSA n e
singletonWithAlphabet (forall a. Ord a => [a] -> Set a
Set.fromList [e]
s) [e]
s


Formal Symbols
--------------

The edges of an FSA are labelled by either a formal symbol or the
pseudo-symbol Epsilon.  Specifically, an edge labelled by Epsilon
represents a transition that may occur without consuming any further
input.


> -- |The label of a 'Transition'.
> data Symbol e = Epsilon  -- ^The edge may be taken without consuming input.
>               | Symbol e -- ^The edge requires consuming this symbol.
>               deriving (Symbol e -> Symbol e -> Bool
forall e. Eq e => Symbol e -> Symbol e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Symbol e -> Symbol e -> Bool
$c/= :: forall e. Eq e => Symbol e -> Symbol e -> Bool
== :: Symbol e -> Symbol e -> Bool
$c== :: forall e. Eq e => Symbol e -> Symbol e -> Bool
Eq, Symbol e -> Symbol e -> Bool
Symbol e -> Symbol e -> Ordering
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
forall {e}. Ord e => Eq (Symbol e)
forall e. Ord e => Symbol e -> Symbol e -> Bool
forall e. Ord e => Symbol e -> Symbol e -> Ordering
forall e. Ord e => Symbol e -> Symbol e -> Symbol e
min :: Symbol e -> Symbol e -> Symbol e
$cmin :: forall e. Ord e => Symbol e -> Symbol e -> Symbol e
max :: Symbol e -> Symbol e -> Symbol e
$cmax :: forall e. Ord e => Symbol e -> Symbol e -> Symbol e
>= :: Symbol e -> Symbol e -> Bool
$c>= :: forall e. Ord e => Symbol e -> Symbol e -> Bool
> :: Symbol e -> Symbol e -> Bool
$c> :: forall e. Ord e => Symbol e -> Symbol e -> Bool
<= :: Symbol e -> Symbol e -> Bool
$c<= :: forall e. Ord e => Symbol e -> Symbol e -> Bool
< :: Symbol e -> Symbol e -> Bool
$c< :: forall e. Ord e => Symbol e -> Symbol e -> Bool
compare :: Symbol e -> Symbol e -> Ordering
$ccompare :: forall e. Ord e => Symbol e -> Symbol e -> Ordering
Ord, ReadPrec [Symbol e]
ReadPrec (Symbol e)
ReadS [Symbol e]
forall e. Read e => ReadPrec [Symbol e]
forall e. Read e => ReadPrec (Symbol e)
forall e. Read e => Int -> ReadS (Symbol e)
forall e. Read e => ReadS [Symbol e]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Symbol e]
$creadListPrec :: forall e. Read e => ReadPrec [Symbol e]
readPrec :: ReadPrec (Symbol e)
$creadPrec :: forall e. Read e => ReadPrec (Symbol e)
readList :: ReadS [Symbol e]
$creadList :: forall e. Read e => ReadS [Symbol e]
readsPrec :: Int -> ReadS (Symbol e)
$creadsPrec :: forall e. Read e => Int -> ReadS (Symbol e)
Read, Int -> Symbol e -> ShowS
forall e. Show e => Int -> Symbol e -> ShowS
forall e. Show e => [Symbol e] -> ShowS
forall e. Show e => Symbol e -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Symbol e] -> ShowS
$cshowList :: forall e. Show e => [Symbol e] -> ShowS
show :: Symbol e -> String
$cshow :: forall e. Show e => Symbol e -> String
showsPrec :: Int -> Symbol e -> ShowS
$cshowsPrec :: forall e. Show e => Int -> Symbol e -> ShowS
Show)

The Symbol type is used to adjoin Epsilon to an alphabet.  We often
want only the real portion of a string, where instances of Epsilon are
not important.  The 'unsymbols' function does this transformation:

    unsymbols [Symbol 'a', Epsilon, Symbol 'b', Epsilon] :: [Char]

becomes simply

    "ab".

This transformed a [Symbol Char] to a [Char].  The container type need not
be the same though:

    unsymbols [Symbol 'a', Epsilon, Symbol 'b', Epsilon] :: Set Char

becomes

    fromList ['a', 'b'].

> -- |Remove 'Epsilon' from a 'Collapsible' of 'Symbol'
> -- and present the unwrapped results as a new 'Container'.
> unsymbols :: (Collapsible s, Container c e, Monoid c) => s (Symbol e) -> c
> unsymbols :: forall (s :: * -> *) c e.
(Collapsible s, Container c e, Monoid c) =>
s (Symbol e) -> c
unsymbols = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall a. Monoid a => a -> a -> a
mappend forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {c} {a}. Container c a => Symbol a -> c
f) forall a. Monoid a => a
mempty
>     where f :: Symbol a -> c
f (Symbol a
x)  =  forall c a. Container c a => a -> c
singleton a
x
>           f Symbol a
_           =  forall c a. Container c a => c
empty

States
------

> -- |A vertex of the graph representation of an 'FSA' is a 'State',
> -- which can be labelled with any arbitrary value, so long as every
> -- vertex of a single automaton is labelled with a distinct value
> -- of the same type.
> newtype State n = State {forall n. State n -> n
nodeLabel :: n} deriving (State n -> State n -> Bool
forall n. Eq n => State n -> State n -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: State n -> State n -> Bool
$c/= :: forall n. Eq n => State n -> State n -> Bool
== :: State n -> State n -> Bool
$c== :: forall n. Eq n => State n -> State n -> Bool
Eq, State n -> State n -> Bool
State n -> State n -> Ordering
State n -> State n -> State n
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
forall {n}. Ord n => Eq (State n)
forall n. Ord n => State n -> State n -> Bool
forall n. Ord n => State n -> State n -> Ordering
forall n. Ord n => State n -> State n -> State n
min :: State n -> State n -> State n
$cmin :: forall n. Ord n => State n -> State n -> State n
max :: State n -> State n -> State n
$cmax :: forall n. Ord n => State n -> State n -> State n
>= :: State n -> State n -> Bool
$c>= :: forall n. Ord n => State n -> State n -> Bool
> :: State n -> State n -> Bool
$c> :: forall n. Ord n => State n -> State n -> Bool
<= :: State n -> State n -> Bool
$c<= :: forall n. Ord n => State n -> State n -> Bool
< :: State n -> State n -> Bool
$c< :: forall n. Ord n => State n -> State n -> Bool
compare :: State n -> State n -> Ordering
$ccompare :: forall n. Ord n => State n -> State n -> Ordering
Ord, ReadPrec [State n]
ReadPrec (State n)
ReadS [State n]
forall n. Read n => ReadPrec [State n]
forall n. Read n => ReadPrec (State n)
forall n. Read n => Int -> ReadS (State n)
forall n. Read n => ReadS [State n]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [State n]
$creadListPrec :: forall n. Read n => ReadPrec [State n]
readPrec :: ReadPrec (State n)
$creadPrec :: forall n. Read n => ReadPrec (State n)
readList :: ReadS [State n]
$creadList :: forall n. Read n => ReadS [State n]
readsPrec :: Int -> ReadS (State n)
$creadsPrec :: forall n. Read n => Int -> ReadS (State n)
Read, Int -> State n -> ShowS
forall n. Show n => Int -> State n -> ShowS
forall n. Show n => [State n] -> ShowS
forall n. Show n => State n -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [State n] -> ShowS
$cshowList :: forall n. Show n => [State n] -> ShowS
show :: State n -> String
$cshow :: forall n. Show n => State n -> String
showsPrec :: Int -> State n -> ShowS
$cshowsPrec :: forall n. Show n => Int -> State n -> ShowS
Show)

Transitions
-----------

If a state is the vertex of a graph, then a transition is its edge.
Since an FSA is represented by a directed graph, there are three
components to a transition: an edge label, and two states.  If a
computation in the first state encounters a symbol matching the
transition's edge label, then it moves to the second state.

> -- |The edges of an 'FSA'.
> data Transition n e
>     = Transition
>       { forall n e. Transition n e -> Symbol e
edgeLabel   :: Symbol e
>       , forall n e. Transition n e -> State n
source      :: State n
>       , forall n e. Transition n e -> State n
destination :: State n
>       }
>     deriving (Transition n e -> Transition n e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e.
(Eq e, Eq n) =>
Transition n e -> Transition n e -> Bool
/= :: Transition n e -> Transition n e -> Bool
$c/= :: forall n e.
(Eq e, Eq n) =>
Transition n e -> Transition n e -> Bool
== :: Transition n e -> Transition n e -> Bool
$c== :: forall n e.
(Eq e, Eq n) =>
Transition n e -> Transition n e -> Bool
Eq, Transition n e -> Transition n e -> Bool
Transition n e -> Transition n e -> Ordering
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
forall {n} {e}. (Ord e, Ord n) => Eq (Transition n e)
forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Bool
forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Ordering
forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Transition n e
min :: Transition n e -> Transition n e -> Transition n e
$cmin :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Transition n e
max :: Transition n e -> Transition n e -> Transition n e
$cmax :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Transition n e
>= :: Transition n e -> Transition n e -> Bool
$c>= :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Bool
> :: Transition n e -> Transition n e -> Bool
$c> :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Bool
<= :: Transition n e -> Transition n e -> Bool
$c<= :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Bool
< :: Transition n e -> Transition n e -> Bool
$c< :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Bool
compare :: Transition n e -> Transition n e -> Ordering
$ccompare :: forall n e.
(Ord e, Ord n) =>
Transition n e -> Transition n e -> Ordering
Ord, Int -> Transition n e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show e, Show n) => Int -> Transition n e -> ShowS
forall n e. (Show e, Show n) => [Transition n e] -> ShowS
forall n e. (Show e, Show n) => Transition n e -> String
showList :: [Transition n e] -> ShowS
$cshowList :: forall n e. (Show e, Show n) => [Transition n e] -> ShowS
show :: Transition n e -> String
$cshow :: forall n e. (Show e, Show n) => Transition n e -> String
showsPrec :: Int -> Transition n e -> ShowS
$cshowsPrec :: forall n e. (Show e, Show n) => Int -> Transition n e -> ShowS
Show, ReadPrec [Transition n e]
ReadPrec (Transition n e)
ReadS [Transition n e]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall n e. (Read e, Read n) => ReadPrec [Transition n e]
forall n e. (Read e, Read n) => ReadPrec (Transition n e)
forall n e. (Read e, Read n) => Int -> ReadS (Transition n e)
forall n e. (Read e, Read n) => ReadS [Transition n e]
readListPrec :: ReadPrec [Transition n e]
$creadListPrec :: forall n e. (Read e, Read n) => ReadPrec [Transition n e]
readPrec :: ReadPrec (Transition n e)
$creadPrec :: forall n e. (Read e, Read n) => ReadPrec (Transition n e)
readList :: ReadS [Transition n e]
$creadList :: forall n e. (Read e, Read n) => ReadS [Transition n e]
readsPrec :: Int -> ReadS (Transition n e)
$creadsPrec :: forall n e. (Read e, Read n) => Int -> ReadS (Transition n e)
Read)


Class Instances
===============

Here we define class instances for FSAs and their component types.


Symbol
------

> instance Functor Symbol
>     where fmap :: forall a b. (a -> b) -> Symbol a -> Symbol b
fmap a -> b
_ Symbol a
Epsilon     =  forall e. Symbol e
Epsilon
>           fmap a -> b
f (Symbol a
e)  =  forall e. e -> Symbol e
Symbol (a -> b
f a
e)

> instance (NFData e) => NFData (Symbol e)
>     where rnf :: Symbol e -> ()
rnf Symbol e
Epsilon     =  ()
>           rnf (Symbol e
e)  =  forall a. NFData a => a -> ()
rnf e
e


State
-----

> instance Functor State
>     where fmap :: forall a b. (a -> b) -> State a -> State b
fmap a -> b
f = forall n. n -> State n
State forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> b
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> instance Applicative State
>     where pure :: forall n. n -> State n
pure   =  forall n. n -> State n
State
>           <*> :: forall a b. State (a -> b) -> State a -> State b
(<*>)  =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> instance Monad State
>     where State a
a >>= :: forall a b. State a -> (a -> State b) -> State b
>>= a -> State b
f  =  a -> State b
f forall a b. (a -> b) -> a -> b
$ forall n. State n -> n
nodeLabel State a
a
#if !MIN_VERSION_base(4,8,0)
>           return    =  pure
#endif

#if MIN_VERSION_base(4,9,0)
Semigroup instance to satisfy base-4.11

> instance (Semigroup n) => Semigroup (State n)
>     where <> :: State n -> State n -> State n
(<>) = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Semigroup a => a -> a -> a
(<>)
#endif

> instance (Monoid n) => Monoid (State n)
>     where mempty :: State n
mempty   =  forall n. n -> State n
State forall a. Monoid a => a
mempty

#if MIN_VERSION_base(4,11,0)
> -- mappend will eventually be removed
#elif MIN_VERSION_base(4,9,0)
>           mappend  = (<>)
#else
>           mappend  =  fmap . nodeLabel . fmap mappend
#endif

> instance (NFData n) => NFData (State n)
>     where rnf :: State n -> ()
rnf (State n
n) = forall a. NFData a => a -> ()
rnf n
n


Transition
----------

> instance (NFData n, NFData e) => NFData (Transition n e)
>     where rnf :: Transition n e -> ()
rnf Transition n e
t = forall a. NFData a => a -> ()
rnf (forall n e. Transition n e -> Symbol e
edgeLabel Transition n e
t) seq :: forall a b. a -> b -> b
`seq`
>                   forall a. NFData a => a -> ()
rnf (forall n e. Transition n e -> State n
source Transition n e
t)    seq :: forall a b. a -> b -> b
`seq`
>                   forall a. NFData a => a -> ()
rnf (forall n e. Transition n e -> State n
destination Transition n e
t)

> newtype Noitisnart e n = Noitisnart { forall e n. Noitisnart e n -> Transition n e
transition :: Transition n e }

> instance Functor (Transition n)
>     where fmap :: forall a b. (a -> b) -> Transition n a -> Transition n b
fmap a -> b
f Transition n a
t = Transition n a
t { edgeLabel :: Symbol b
edgeLabel = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall n e. Transition n e -> Symbol e
edgeLabel Transition n a
t) }

> instance Functor (Noitisnart e)
>     where fmap :: forall a b. (a -> b) -> Noitisnart e a -> Noitisnart e b
fmap a -> b
f = forall e n. Transition n e -> Noitisnart e n
Noitisnart forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}. Transition a e -> Transition b e
fmap' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. Noitisnart e n -> Transition n e
transition
>               where fmap' :: Transition a e -> Transition b e
fmap' Transition a e
t
>                         = Transition a e
t { source :: State b
source       =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall n e. Transition n e -> State n
source Transition a e
t)
>                             , destination :: State b
destination  =  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (forall n e. Transition n e -> State n
destination Transition a e
t)
>                             }


FSA
---

FSAs represent languages, so it makes sense to use equivalence of the
represented languages as the criterion for equivalence of the FSAs
themselves.  First, an FSA represents the empty language if it has
no reachable accepting states:

> -- |True iff the input accepts no strings.
> isNull :: (Ord e, Ord n) => FSA n e -> Bool
> isNull :: forall e n. (Ord e, Ord n) => FSA n e -> Bool
isNull = (forall a. Eq a => a -> a -> Bool
== forall c a. Container c a => c
empty) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. FSA n e -> Set (State n)
finals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables

Two FSAs are considered equal iff they are isomorphic.

> instance (Ord e, Ord n) => Eq (FSA n e)
>     where FSA n e
a == :: FSA n e -> FSA n e -> Bool
== FSA n e
b = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> Bool
isomorphic (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n e
a) (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n e
b)

Calls to `isomorphic` should work for NFAs as well as DFAs, but in the
current implementation, in general, will not.  This is because
multiple start states are combined with the cartesian product to
create c, rather than mapped from a to their counterparts in b, a much
harder problem.

> isomorphic :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e -> Bool
> isomorphic :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> Bool
isomorphic FSA n1 e
a FSA n2 e
b = (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n1 e
a         forall a. Eq a => a -> a -> Bool
== forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n2 e
b)          Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
initials FSA n1 e
a) forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
initials FSA n2 e
b))  Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a)   forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
finals FSA n2 e
b))    Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n1 e
a)   forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n2 e
b))    Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
initials FSA n1 e
a) forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
initials FSA (Maybe n1, Maybe n2) e
c))  Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a)   forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall n e. FSA n e -> Set (State n)
finals FSA (Maybe n1, Maybe n2) e
c))    Bool -> Bool -> Bool
&&
>                  (forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n1 e
a)   forall a. Eq a => a -> a -> Bool
== Integer
s)
>     where c :: FSA (Maybe n1, Maybe n2) e
c  =  forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion FSA n1 e
a FSA n2 e
b
>           s :: Integer
s  =  forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall n. n -> State n
State (forall a. Maybe a
Nothing, forall a. Maybe a
Nothing) forall a. Eq a => a -> a -> Bool
/=) forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (Maybe n1, Maybe n2) e
c

A Set of FSAs could be useful, and an Ord instance is needed for that.
If two automata are equal, they should certainly compare EQ.
If A is a subset of B, compare A B ought be LT and the reverse GT.
When neither is a subset of the other, they are incomparable by this
measure, so instead they are compared by a standard Haskell comparison
of tuples consisting of their alphabets, transitions, initial states,
and final states.

> instance (Ord e, Ord n) => Ord (FSA n e)
>     where compare :: FSA n e -> FSA n e -> Ordering
compare FSA n e
a FSA n e
b
>               | FSA n e
a forall a. Eq a => a -> a -> Bool
== FSA n e
b                  =  Ordering
EQ
>               | forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
b) (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
a)  =  Ordering
LT
>               | forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
a) (forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
b)  =  Ordering
GT
>               | Bool
otherwise               =  forall a. Ord a => a -> a -> Ordering
compare (forall {n} {e}.
FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
g FSA n e
a) (forall {n} {e}.
FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
g FSA n e
b)
>               where f :: (Ord e, Ord n) => FSA n e -> FSA Integer e
>                     f :: forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates
>                     g :: FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
g FSA n e
x = (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
x, forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
x, forall n e. FSA n e -> Set (State n)
initials FSA n e
x, forall n e. FSA n e -> Set (State n)
finals FSA n e
x)

> instance (Enum n, Ord n, Ord e) => Container (FSA n e) [e]
>     where isEmpty :: FSA n e -> Bool
isEmpty       =  forall e n. (Ord e, Ord n) => FSA n e -> Bool
isNull
>           isIn :: Eq [e] => FSA n e -> [e] -> Bool
isIn          =  forall e n. (Ord e, Ord n) => FSA n e -> [e] -> Bool
accepts
>           union :: FSA n e -> FSA n e -> FSA n e
union         =  forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion
>           intersection :: Eq [e] => FSA n e -> FSA n e -> FSA n e
intersection  =  forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection
>           difference :: Eq [e] => FSA n e -> FSA n e -> FSA n e
difference    =  forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e
autDifference
>           empty :: FSA n e
empty         =  forall e n. (Ord e, Ord n, Enum n) => FSA n e
emptyLanguage
>           singleton :: [e] -> FSA n e
singleton     =  forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage
>           symmetricDifference :: Eq [e] => FSA n e -> FSA n e -> FSA n e
symmetricDifference
>               =  forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e
-> FSA n2 e
-> FSA
     (Maybe (Maybe n1, Maybe n2), Maybe (Set (Maybe n1, Maybe n2))) e
autSymmetricDifference

Here we consider FSAs to be Semigroups (and Monoids) under concatenation

#if MIN_VERSION_base(4,9,0)
Semigroup instance to satisfy base-4.9

> instance (Enum n, Ord n, Ord e) => Semigroup (FSA n e)
>     where <> :: FSA n e -> FSA n e -> FSA n e
(<>) = forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
autConcatenation
#endif

> instance (Enum n, Ord n, Ord e) => Monoid (FSA n e)
>     where mempty :: FSA n e
mempty   =  forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage forall c a. Container c a => c
empty

#if MIN_VERSION_base(4,11,0)
-- mappend will eventually be removed
#elif MIN_VERSION_base(4,9,0)

>           mappend = (<>)

#else

>           mappend  =  apply autConcatenation

#endif

> apply :: (Ord e, Ord n1, Ord n2, Enum n2) =>
>          (a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
> apply :: forall e n1 n2 a b.
(Ord e, Ord n1, Ord n2, Enum n2) =>
(a -> b -> FSA n1 e) -> a -> b -> FSA n2 e
apply a -> b -> FSA n1 e
f = forall a b c. ((a, b) -> c) -> a -> b -> c
curry (forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry a -> b -> FSA n1 e
f)

> pfold :: (a -> a -> a) -> [a] -> a
> pfold :: forall a. (a -> a -> a) -> [a] -> a
pfold = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> Tree a
treeFromList) forall a. (a -> a -> a) -> Tree a -> a
treeFold

It is better to use flatIntersection and flatUnion than the
appropriate fold, because the flat- functions take advantage
of parallelism if possible.

> -- |Intersect all given automata, in parallel if possible.
> -- An empty intersection is undefined.
> -- In theory it should be the total language over the
> -- total alphabet, but the latter cannot be defined.
> -- Intermediate results are evaluated to normal form.
> flatIntersection :: (Enum n, Ord n, NFData n, Ord e, NFData e) =>
>                     [FSA n e] -> FSA n e
> flatIntersection :: forall n e.
(Enum n, Ord n, NFData n, Ord e, NFData e) =>
[FSA n e] -> FSA n e
flatIntersection [] = forall a. HasCallStack => String -> a
error String
"Cannot take a nullary intersection"
> flatIntersection [FSA n e]
xs = forall a. (a -> a -> a) -> [a] -> a
pfold forall {n1} {e} {n1} {n2}.
(NFData n1, NFData e, Ord e, Ord n1, Ord n2, Ord n1, Enum n1) =>
FSA n1 e -> FSA n2 e -> FSA n1 e
i [FSA n e]
xs
>     where i :: FSA n1 e -> FSA n2 e -> FSA n1 e
i FSA n1 e
a FSA n2 e
b = let x :: FSA n1 e
x = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection FSA n1 e
a FSA n2 e
b
>                   in forall a. NFData a => a -> ()
rnf FSA n1 e
x seq :: forall a b. a -> b -> b
`seq` FSA n1 e
x

> -- |Union all given automata, in parallel if possible.
> -- An empty union is defined as the empty language over
> -- an empty alphabet.
> -- Intermediate results are evaluated to normal form.
> flatUnion :: (Enum n, Ord n, NFData n, Ord e, NFData e) =>
>              [FSA n e] -> FSA n e
> flatUnion :: forall n e.
(Enum n, Ord n, NFData n, Ord e, NFData e) =>
[FSA n e] -> FSA n e
flatUnion []  =  forall e n. (Ord e, Ord n, Enum n) => FSA n e
emptyLanguage
> flatUnion [FSA n e]
xs  =  forall a. (a -> a -> a) -> [a] -> a
pfold forall {n1} {e} {n1} {n2}.
(NFData n1, NFData e, Ord e, Ord n1, Ord n2, Ord n1, Enum n1) =>
FSA n1 e -> FSA n2 e -> FSA n1 e
u [FSA n e]
xs
>     where u :: FSA n1 e -> FSA n2 e -> FSA n1 e
u FSA n1 e
a FSA n2 e
b = let x :: FSA n1 e
x = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion FSA n1 e
a FSA n2 e
b
>                   in forall a. NFData a => a -> ()
rnf FSA n1 e
x seq :: forall a b. a -> b -> b
`seq` FSA n1 e
x

> -- |Shuffle all given automata, in parallel if possible.
> -- An empty shuffle is defined as the singleton language over
> -- an empty alphabet containing only the empty string.
> -- Intermediate results are evaluated to normal form.
> --
> -- @since 1.1
> flatShuffle :: (Enum n, Ord n, NFData n, Ord e, NFData e) =>
>                [FSA n e] -> FSA n e
> flatShuffle :: forall n e.
(Enum n, Ord n, NFData n, Ord e, NFData e) =>
[FSA n e] -> FSA n e
flatShuffle []  =  forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage []
> flatShuffle [FSA n e]
xs  =  forall a. (a -> a -> a) -> [a] -> a
pfold forall {n1} {e} {n1} {n2}.
(NFData n1, NFData e, Ord e, Ord n1, Ord n2, Ord n1, Enum n1) =>
FSA n1 e -> FSA n2 e -> FSA n1 e
s [FSA n e]
xs
>     where s :: FSA n1 e -> FSA n2 e -> FSA n1 e
s FSA n1 e
a FSA n2 e
b = let x :: FSA n1 e
x = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autShuffle FSA n1 e
a FSA n2 e
b
>                   in forall a. NFData a => a -> ()
rnf FSA n1 e
x seq :: forall a b. a -> b -> b
`seq` FSA n1 e
x

> -- |Infiltrate all given automata, in parallel if possible.
> -- An empty infiltration is defined as the singleton language over
> -- an empty alphabet containing only the empty string.
> -- Intermediate results are evaluated to normal form.
> --
> -- @since 1.1
> flatInfiltration :: (Enum n, Ord n, NFData n, Ord e, NFData e) =>
>                [FSA n e] -> FSA n e
> flatInfiltration :: forall n e.
(Enum n, Ord n, NFData n, Ord e, NFData e) =>
[FSA n e] -> FSA n e
flatInfiltration []  =  forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage []
> flatInfiltration [FSA n e]
xs  =  forall a. (a -> a -> a) -> [a] -> a
pfold forall {n1} {e} {n1} {n2}.
(NFData n1, NFData e, Ord e, Ord n1, Ord n2, Ord n1, Enum n1) =>
FSA n1 e -> FSA n2 e -> FSA n1 e
s [FSA n e]
xs
>     where s :: FSA n1 e -> FSA n2 e -> FSA n1 e
s FSA n1 e
a FSA n2 e
b = let x :: FSA n1 e
x = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autInfiltration FSA n1 e
a FSA n2 e
b
>                   in forall a. NFData a => a -> ()
rnf FSA n1 e
x seq :: forall a b. a -> b -> b
`seq` FSA n1 e
x

> instance (NFData n, NFData e) => NFData (FSA n e)
>     where rnf :: FSA n e -> ()
rnf (FSA Set e
a Set (Transition n e)
t Set (State n)
i Set (State n)
f Bool
d)
>               = forall a. NFData a => a -> ()
rnf Set e
a seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Set (Transition n e)
t seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Set (State n)
i seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Set (State n)
f seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Bool
d

> instance HasAlphabet (FSA n)
>     where alphabet :: forall e. FSA n e -> Set e
alphabet = forall n e. FSA n e -> Set e
sigma


Acceptance and the Transition Function
======================================

To determine whether an FSA accepts a string of Symbols, there must
exist a mechanism to determine which State to enter upon consuming a
Symbol.  The set of Transitions describes the map, and we will use
that to define the transition function.

> data ID n e = ID (State n) [Symbol e] deriving (ID n e -> ID n e -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall n e. (Eq n, Eq e) => ID n e -> ID n e -> Bool
/= :: ID n e -> ID n e -> Bool
$c/= :: forall n e. (Eq n, Eq e) => ID n e -> ID n e -> Bool
== :: ID n e -> ID n e -> Bool
$c== :: forall n e. (Eq n, Eq e) => ID n e -> ID n e -> Bool
Eq, ID n e -> ID n e -> Bool
ID n e -> ID n e -> Ordering
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
forall {n} {e}. (Ord n, Ord e) => Eq (ID n e)
forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Bool
forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Ordering
forall n e. (Ord n, Ord e) => ID n e -> ID n e -> ID n e
min :: ID n e -> ID n e -> ID n e
$cmin :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> ID n e
max :: ID n e -> ID n e -> ID n e
$cmax :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> ID n e
>= :: ID n e -> ID n e -> Bool
$c>= :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Bool
> :: ID n e -> ID n e -> Bool
$c> :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Bool
<= :: ID n e -> ID n e -> Bool
$c<= :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Bool
< :: ID n e -> ID n e -> Bool
$c< :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Bool
compare :: ID n e -> ID n e -> Ordering
$ccompare :: forall n e. (Ord n, Ord e) => ID n e -> ID n e -> Ordering
Ord, ReadPrec [ID n e]
ReadPrec (ID n e)
ReadS [ID n e]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall n e. (Read n, Read e) => ReadPrec [ID n e]
forall n e. (Read n, Read e) => ReadPrec (ID n e)
forall n e. (Read n, Read e) => Int -> ReadS (ID n e)
forall n e. (Read n, Read e) => ReadS [ID n e]
readListPrec :: ReadPrec [ID n e]
$creadListPrec :: forall n e. (Read n, Read e) => ReadPrec [ID n e]
readPrec :: ReadPrec (ID n e)
$creadPrec :: forall n e. (Read n, Read e) => ReadPrec (ID n e)
readList :: ReadS [ID n e]
$creadList :: forall n e. (Read n, Read e) => ReadS [ID n e]
readsPrec :: Int -> ReadS (ID n e)
$creadsPrec :: forall n e. (Read n, Read e) => Int -> ReadS (ID n e)
Read, Int -> ID n e -> ShowS
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall n e. (Show n, Show e) => Int -> ID n e -> ShowS
forall n e. (Show n, Show e) => [ID n e] -> ShowS
forall n e. (Show n, Show e) => ID n e -> String
showList :: [ID n e] -> ShowS
$cshowList :: forall n e. (Show n, Show e) => [ID n e] -> ShowS
show :: ID n e -> String
$cshow :: forall n e. (Show n, Show e) => ID n e -> String
showsPrec :: Int -> ID n e -> ShowS
$cshowsPrec :: forall n e. (Show n, Show e) => Int -> ID n e -> ShowS
Show)

> state :: ID n e -> State n
> state :: forall n e. ID n e -> State n
state (ID State n
a [Symbol e]
_) = State n
a

> string :: ID n e -> [Symbol e]
> string :: forall n e. ID n e -> [Symbol e]
string (ID State n
_ [Symbol e]
xs) = [Symbol e]
xs

> epsilonClosure :: (Ord e, Ord n) =>
>                   FSA n e -> Set (State n) -> Set (State n)
> epsilonClosure :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa Set (State n)
qs
>     | forall n e. FSA n e -> Bool
isDeterministic FSA n e
fsa  = Set (State n)
qs
>     | Bool
otherwise            = Set (State n) -> Set (State n) -> Set (State n)
epsilonClosure' Set (State n)
qs Set (State n)
qs
>     where epsilons :: Set (Transition n e)
epsilons = forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic forall n e. Transition n e -> Symbol e
edgeLabel forall e. Symbol e
Epsilon (forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa)
>           epsilonClosure' :: Set (State n) -> Set (State n) -> Set (State n)
epsilonClosure' Set (State n)
seen Set (State n)
new
>               | forall c a. Container c a => c -> Bool
isEmpty Set (State n)
new  =  Set (State n)
seen
>               | Bool
otherwise    =  Set (State n) -> Set (State n) -> Set (State n)
epsilonClosure'
>                                 (Set (State n)
seen forall c a. Container c a => c -> c -> c
`union` Set (State n)
closure)
>                                 (forall c a. (Container c a, Eq a) => c -> c -> c
difference Set (State n)
closure Set (State n)
seen)
>               where seens :: Set (Transition n e)
seens    =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
new forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source) Set (Transition n e)
epsilons
>                     closure :: Set (State n)
closure  =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination Set (Transition n e)
seens

> step :: (Ord e, Ord n) => FSA n e -> Set (ID n e) -> Set (ID n e)
> step :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (ID n e) -> Set (ID n e)
step FSA n e
fsa Set (ID n e)
ids
>     | Set (ID n e)
filteredIDs forall a. Eq a => a -> a -> Bool
== forall c a. Container c a => c
empty  =  forall c a. Container c a => c
empty
>     | Bool
otherwise             =  forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. ID n e -> Set (ID n e)
next) forall c a. Container c a => c
empty Set (ID n e)
filteredIDs
>     where ts :: Set (Transition n e)
ts = forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa
>           filterID :: ID n e -> ID n e
filterID ID n e
i = forall n e. State n -> [Symbol e] -> ID n e
ID (forall n e. ID n e -> State n
state ID n e
i) (forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall a. Eq a => a -> a -> Bool
/= forall e. Symbol e
Epsilon) (forall n e. ID n e -> [Symbol e]
string ID n e
i))
>           filteredIDs :: Set (ID n e)
filteredIDs = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall {e} {n}. Eq e => ID n e -> ID n e
filterID Set (ID n e)
ids
>           next :: ID n e -> Set (ID n e)
next ID n e
i
>               | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol e]
s     = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall n e. State n -> [Symbol e] -> ID n e
`ID` []) Set (State n)
closure
>               | Bool
otherwise  = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall n e. State n -> [Symbol e] -> ID n e
`ID` forall a. [a] -> [a]
tail [Symbol e]
s) Set (State n)
outStates
>               where s :: [Symbol e]
s = forall n e. ID n e -> [Symbol e]
string ID n e
i
>                     closure :: Set (State n)
closure = forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa (forall c a. Container c a => a -> c
singleton (forall n e. ID n e -> State n
state ID n e
i))
>                     outStates :: Set (State n)
outStates  = forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa
>                                  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination
>                                  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
closure forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source)
>                                  forall a b. (a -> b) -> a -> b
$ forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic forall n e. Transition n e -> Symbol e
edgeLabel
>                                    (forall a. [a] -> a
head [Symbol e]
s) Set (Transition n e)
ts

We should not have to produce IDs ourselves.  We can define the transition
function `delta` from an FSA, a symbol, and a state to a set of states:

> delta :: (Ord e, Ord n) =>
>          FSA n e -> Symbol e -> Set (State n) -> Set (State n)
> delta :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f Symbol e
x = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. ID n e -> State n
state forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (ID n e) -> Set (ID n e)
step FSA n e
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall n e. State n -> [Symbol e] -> ID n e
`ID` [Symbol e
x])

> compute :: (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
> compute :: forall e n. (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
fsa [Symbol e]
str = forall a. (a -> Bool) -> (a -> a) -> a -> a
until (forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. ID n e -> [Symbol e]
string)) (forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (ID n e) -> Set (ID n e)
step FSA n e
fsa) Set (ID n e)
initialIDs
>     where initialIDs :: Set (ID n e)
initialIDs = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall n e. State n -> [Symbol e] -> ID n e
`ID` [Symbol e]
str) Set (State n)
expandedInitials
>           expandedInitials :: Set (State n)
expandedInitials = forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa

> -- |Returns whether the given 'FSA' lands in a final state
> -- after processing the given sequence.
> --
> -- @since 1.1
> accepts :: (Ord e, Ord n) => FSA n e -> [e] -> Bool
> accepts :: forall e n. (Ord e, Ord n) => FSA n e -> [e] -> Bool
accepts FSA n e
fsa = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. ID n e -> State n
state
>               forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
fsa forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall e. e -> Symbol e
Symbol

The Brzozowski derivative of an FSA with respect to some string
is an FSA representing the valid continuations from that string.

> -- |Return an FSA representing possible continuations from a given
> -- sequence of symbols.  If the input automaton is not complete
> -- then the output may have no states when given incompatible input.
> --
> -- @since 1.0
> brzozowskiDerivative :: (Ord e, Ord n) => [e] -> FSA n e -> FSA n e
> brzozowskiDerivative :: forall e n. (Ord e, Ord n) => [e] -> FSA n e -> FSA n e
brzozowskiDerivative [e]
xs FSA n e
f = forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables
>                             forall a b. (a -> b) -> a -> b
$ FSA n e
f { initials :: Set (State n)
initials = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. ID n e -> State n
state forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
f
>                                              forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall e. e -> Symbol e
Symbol [e]
xs}

A generalization of the Brzozowski derivative is the left quotient
of a language by another language.  In fact, the following operations,
quotLeft, quotRight, and quotMid, offer a start toward computing
in the free group rather than the free monoid generated by the alphabet.

> -- |Return an FSA representing possible continuations in the second
> -- language from strings in the first language.
> -- In other words, @quotLeft a b@ returns \(\{w : x\in a, xw\in b\}\).
> --
> -- @since 1.0
> quotLeft :: (Ord e, Ord n1, Ord n2) =>
>             FSA n1 e -> FSA n2 e
>          -> FSA (Maybe (Either n1 ()), Maybe n2) e
> quotLeft :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe (Either n1 ()), Maybe n2) e
quotLeft FSA n1 e
a FSA n2 e
b = FSA (Maybe (Either n1 ()), Maybe n2) e
p { initials :: Set (State (Maybe (Either n1 ()), Maybe n2))
initials = Set (State (Maybe (Either n1 ()), Maybe n2))
i
>                  , isDeterministic :: Bool
isDeterministic = Bool
d }
>     where a' :: FSA (Either n1 ()) e
a' = forall {e}. FSA (Either n1 ()) e -> FSA (Either n1 ()) e
x (forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
autConcatenation (forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables FSA n1 e
a) FSA () e
t)
>           x :: FSA (Either n1 ()) e -> FSA (Either n1 ()) e
x FSA (Either n1 ()) e
m = FSA (Either n1 ()) e
m {finals :: Set (State (Either n1 ()))
finals = forall n e. FSA n e -> Set (State n)
finals FSA (Either n1 ()) e
m forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n. n -> State n
State Set (Either n1 ())
f}
>           t :: FSA () e
t  = forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet (forall n e. FSA n e -> Set e
sigma FSA n1 e
a forall a. Ord a => Set a -> Set a -> Set a
`Set.union` forall n e. FSA n e -> Set e
sigma FSA n2 e
b)
>           p :: FSA (Maybe (Either n1 ()), Maybe n2) e
p  = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection FSA (Either n1 ()) e
a' (forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables FSA n2 e
b)
>           f :: Set (Either n1 ())
f  = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall a b. a -> Either a b
Left forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a
>           i :: Set (State (Maybe (Either n1 ()), Maybe n2))
i  = forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ( forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Either n1 ())
f)
>                     forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel) forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (Maybe (Either n1 ()), Maybe n2) e
p
>           d :: Bool
d  = forall n e. FSA n e -> Bool
isDeterministic FSA (Maybe (Either n1 ()), Maybe n2) e
p Bool -> Bool -> Bool
&& forall a. Set a -> Int
Set.size Set (State (Maybe (Either n1 ()), Maybe n2))
i forall a. Eq a => a -> a -> Bool
== Int
1

Doing quotRight similarly should be fairly simple,
but it's easier to just do left-quotient on reversals.

> -- |Return an FSA representing possible strings in the first language
> -- which end with a string in the second language.
> -- In other words, @quotRight a b@ is \(\{w : wx\in a, x\in b\}\).
> --
> -- @since 1.0
> quotRight :: (Ord e, Ord n1, Ord n2) =>
>              FSA n1 e -> FSA n2 e -> FSA Integer e
> quotRight :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA Integer e
quotRight FSA n1 e
a FSA n2 e
b = forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse
>                 forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe (Either n1 ()), Maybe n2) e
quotLeft (forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse FSA n2 e
b) (forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse FSA n1 e
a)

> -- |@quotMid a b c@ is \(\{wz : wx\in a, yx\in b, yz\in c\}\).
> -- This lifts strings to a group, placing b-inverse between a and c.
> -- The time complexity of this function is abysmal,
> -- performing a left and a right quotient for each state in @b@.
> --
> -- @since 1.0
> quotMid :: (Ord e, Ord n1, Ord n2, Ord n3) =>
>            FSA n1 e -> FSA n2 e -> FSA n3 e -> FSA Integer e
> quotMid :: forall e n1 n2 n3.
(Ord e, Ord n1, Ord n2, Ord n3) =>
FSA n1 e -> FSA n2 e -> FSA n3 e -> FSA Integer e
quotMid FSA n1 e
a FSA n2 e
b FSA n3 e
c = forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall {n1}. (Ord n1, Enum n1) => State Integer -> FSA n1 e
bridge forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA Integer e
b'
>     where a' :: FSA Integer e
a' = forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n1 e
a
>           b' :: FSA Integer e
b' = forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n2 e
b
>           c' :: FSA Integer e
c' = forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n3 e
c
>           bridge :: State Integer -> FSA n1 e
bridge State Integer
n = let b1 :: FSA Integer e
b1 = FSA Integer e
b' {initials :: Set (State Integer)
initials = forall a. a -> Set a
Set.singleton State Integer
n}
>                          b2 :: FSA Integer e
b2 = FSA Integer e
b' {finals :: Set (State Integer)
finals = forall a. a -> Set a
Set.singleton State Integer
n}
>                      in forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates
>                         (forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA Integer e
quotRight FSA Integer e
a' FSA Integer e
b1
>                          forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
`autConcatenation` forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe (Either n1 ()), Maybe n2) e
quotLeft FSA Integer e
b2 FSA Integer e
c')


Logical Operators
=================

> combine :: State a -> State b -> State (a, b)
> combine :: forall a b. State a -> State b -> State (a, b)
combine State a
q1 State b
q2 = (,) forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State a
q1 forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> State b
q2

> makePairs :: (Ord a, Ord b) => Set a -> Set b -> Set (a, b)
> makePairs :: forall a b. (Ord a, Ord b) => Set a -> Set b -> Set (a, b)
makePairs Set a
xs Set b
ys = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. a -> Set (a, b)
f) forall c a. Container c a => c
empty Set a
xs
>     where f :: a -> Set (a, b)
f a
x = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((,) a
x) Set b
ys

> makeJustPairs :: (Ord a, Ord b) =>
>                  Set (State a) -> Set (State b) ->
>                  Set (State (Maybe a), State (Maybe b))
> makeJustPairs :: forall a b.
(Ord a, Ord b) =>
Set (State a)
-> Set (State b) -> Set (State (Maybe a), State (Maybe b))
makeJustPairs Set (State a)
xs Set (State b)
ys = forall a b. (Ord a, Ord b) => Set a -> Set b -> Set (a, b)
makePairs (forall {a}. Set (State a) -> Set (State (Maybe a))
justify Set (State a)
xs) (forall {a}. Set (State a) -> Set (State (Maybe a))
justify Set (State b)
ys)
>     where justify :: Set (State a) -> Set (State (Maybe a))
justify = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just)

The Cartesian construction for automata is closely related to the
tensor product of graphs.  Given two automata, M1 and M2, we construct
a new automata M3 such that:

* states(M3) is a subset of the Cartesian product of
  (states(M1) or Nothing) with (states(M2) or Nothing)
* Any lack of explicit transition in either M1 or M2 is
  considered a transition to Nothing in that automaton.
  This effectively makes each input total.
* If (q1, q2) and (q1', q2') are states of M3,
  then there is a transition from (q1, q2) to (q1', q2')
  iff there exists both a transition from q1 to q1' in M1
  and a transition from q2 to q2' in M2.

This construction results in an automaton that tracks a string through
both of its input automata.  States may be tagged as accepting to
obtain either an intersection or a union:

* For a intersection, a state (q1, q2) in states(M3) is accepting
  iff q1 is accepting in M1 and q2 is accepting in M2.
* For a union, a state (q1, q2) in states(M3) is accepting
  iff q1 is accepting in M1 or q2 is accepting in M2.

In either case, the set of initial states in the new automaton is
equal to the Cartesian product of the initial states of M1 with
the initial states of M2.

The Cartesian construction preserves determinism
and guarantees totality of the result.
We will slightly generalize this construction,
with options for whether to trace the machines in sync,
out of sync, or both

> pairTrace :: (Ord e, Ord n1, Ord n2) =>
>              Bool -> Bool
>           -> (Bool -> Bool -> Bool) -> FSA n1 e -> FSA n2 e
>           -> FSA (Maybe n1, Maybe n2) e
> pairTrace :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
Bool
-> Bool
-> (Bool -> Bool -> Bool)
-> FSA n1 e
-> FSA n2 e
-> FSA (Maybe n1, Maybe n2) e
pairTrace Bool
sync Bool
unsync Bool -> Bool -> Bool
isFinal' FSA n1 e
f1 FSA n2 e
f2
>     = FSA { sigma :: Set e
sigma            =  Set e
alpha
>           , transitions :: Set (Transition (Maybe n1, Maybe n2) e)
transitions      =  Set (Transition (Maybe n1, Maybe n2) e)
ts
>           , initials :: Set (State (Maybe n1, Maybe n2))
initials         =  Set (State (Maybe n1, Maybe n2))
qi
>           , finals :: Set (State (Maybe n1, Maybe n2))
finals           =  Set (State (Maybe n1, Maybe n2))
qf
>           , isDeterministic :: Bool
isDeterministic  =  Bool
isDet
>           }
>     where alpha :: Set e
alpha  =  forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n1 e
f1 forall c a. Container c a => c -> c -> c
`union` forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n2 e
f2
>           isDet :: Bool
isDet  =  Bool -> Bool
not Bool
unsync
>                     Bool -> Bool -> Bool
&& forall n e. FSA n e -> Bool
isDeterministic FSA n1 e
f1 Bool -> Bool -> Bool
&& forall n e. FSA n e -> Bool
isDeterministic FSA n2 e
f2
>                     Bool -> Bool -> Bool
&& forall a. Set a -> Int
Set.size Set (State (Maybe n1, Maybe n2))
qi forall a. Eq a => a -> a -> Bool
== Int
1
>           qi :: Set (State (Maybe n1, Maybe n2))
qi     =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall a b. State a -> State b -> State (a, b)
combine)
>                     forall a b. (a -> b) -> a -> b
$ forall a b.
(Ord a, Ord b) =>
Set (State a)
-> Set (State b) -> Set (State (Maybe a), State (Maybe b))
makeJustPairs
>                       (forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n1 e
f1 forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n1 e
f1)
>                       (forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n2 e
f2 forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n2 e
f2)
>           isFinal :: State (Maybe n1, Maybe n2) -> Bool
isFinal State (Maybe n1, Maybe n2)
q
>               = let ~(Maybe n1
a,Maybe n2
b)  =  forall n. State n -> n
nodeLabel State (Maybe n1, Maybe n2)
q
>                     f :: FSA a e -> Maybe a -> Bool
f FSA a e
m     =  forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (forall n e. FSA n e -> Set (State n)
finals FSA a e
m) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. n -> State n
State)
>                 in Bool -> Bool -> Bool
isFinal' (forall {a} {e}. Ord a => FSA a e -> Maybe a -> Bool
f FSA n1 e
f1 Maybe n1
a) (forall {a} {e}. Ord a => FSA a e -> Maybe a -> Bool
f FSA n2 e
f2 Maybe n2
b)
>           (Set (State (Maybe n1, Maybe n2))
_,Set (State (Maybe n1, Maybe n2))
_,Set (Transition (Maybe n1, Maybe n2) e)
ts,Set (State (Maybe n1, Maybe n2))
qf)
>               = forall a. (a -> Bool) -> (a -> a) -> a -> a
until
>                 (\(Set (State (Maybe n1, Maybe n2))
new, Set (State (Maybe n1, Maybe n2))
_, Set (Transition (Maybe n1, Maybe n2) e)
_, Set (State (Maybe n1, Maybe n2))
_) -> forall c a. Container c a => c -> Bool
isEmpty Set (State (Maybe n1, Maybe n2))
new)
>                 (\(Set (State (Maybe n1, Maybe n2))
new, Set (State (Maybe n1, Maybe n2))
prev, Set (Transition (Maybe n1, Maybe n2) e)
partial, Set (State (Maybe n1, Maybe n2))
fins) ->
>                  let exts :: Set (Transition (Maybe n1, Maybe n2) e)
exts   =  forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe n1, Maybe n2)
-> Set (Transition (Maybe n1, Maybe n2) e)
extensions)
>                                forall c a. Container c a => c
empty Set (State (Maybe n1, Maybe n2))
new
>                      seen :: Set (State (Maybe n1, Maybe n2))
seen   =  Set (State (Maybe n1, Maybe n2))
new forall c a. Container c a => c -> c -> c
`union` Set (State (Maybe n1, Maybe n2))
prev
>                      dests :: Set (State (Maybe n1, Maybe n2))
dests  =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination Set (Transition (Maybe n1, Maybe n2) e)
exts
>                      fins' :: Set (State (Maybe n1, Maybe n2))
fins'  =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep State (Maybe n1, Maybe n2) -> Bool
isFinal Set (State (Maybe n1, Maybe n2))
dests
>                  in ( forall c a. (Container c a, Eq a) => c -> c -> c
difference Set (State (Maybe n1, Maybe n2))
dests Set (State (Maybe n1, Maybe n2))
seen
>                     , Set (State (Maybe n1, Maybe n2))
seen
>                     , Set (Transition (Maybe n1, Maybe n2) e)
exts forall c a. Container c a => c -> c -> c
`union` Set (Transition (Maybe n1, Maybe n2) e)
partial
>                     , Set (State (Maybe n1, Maybe n2))
fins forall c a. Container c a => c -> c -> c
`union` Set (State (Maybe n1, Maybe n2))
fins'
>                     )
>                 )
>                 (Set (State (Maybe n1, Maybe n2))
qi, forall c a. Container c a => c
empty, forall c a. Container c a => c
empty, forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep State (Maybe n1, Maybe n2) -> Bool
isFinal Set (State (Maybe n1, Maybe n2))
qi)
>           extensions :: State (Maybe n1, Maybe n2)
-> Set (Transition (Maybe n1, Maybe n2) e)
extensions State (Maybe n1, Maybe n2)
q  =  forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe n1, Maybe n2)
-> Symbol e -> Set (Transition (Maybe n1, Maybe n2) e)
exts' State (Maybe n1, Maybe n2)
q) forall c a. Container c a => c
empty
>                            forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall e. e -> Symbol e
Symbol Set e
alpha
>           exts' :: State (Maybe n1, Maybe n2)
-> Symbol e -> Set (Transition (Maybe n1, Maybe n2) e)
exts' State (Maybe n1, Maybe n2)
q Symbol e
x     =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall n e. Symbol e -> State n -> State n -> Transition n e
Transition Symbol e
x State (Maybe n1, Maybe n2)
q) forall a b. (a -> b) -> a -> b
$ Symbol e
-> State (Maybe n1, Maybe n2) -> Set (State (Maybe n1, Maybe n2))
nexts Symbol e
x State (Maybe n1, Maybe n2)
q
>           nexts :: Symbol e
-> State (Maybe n1, Maybe n2) -> Set (State (Maybe n1, Maybe n2))
nexts Symbol e
x State (Maybe n1, Maybe n2)
q     =  let n1 :: Set (State (Maybe n1))
n1   =  forall {a} {e}.
(Ord a, Ord e) =>
Symbol e -> FSA a e -> State (Maybe a) -> Set (State (Maybe a))
nexts' Symbol e
x FSA n1 e
f1 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst State (Maybe n1, Maybe n2)
q
>                                n2 :: Set (State (Maybe n2))
n2   =  forall {a} {e}.
(Ord a, Ord e) =>
Symbol e -> FSA a e -> State (Maybe a) -> Set (State (Maybe a))
nexts' Symbol e
x FSA n2 e
f2 forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd State (Maybe n1, Maybe n2)
q
>                                f :: State a -> Set (State (a, Maybe n2))
f State a
a  =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall a b. State a -> State b -> State (a, b)
combine State a
a) Set (State (Maybe n2))
n2
>                            in forall c a. Container c a => c -> c -> c
union
>                               (if Bool
unsync
>                                then forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                                     (forall a b. State a -> State b -> State (a, b)
`combine` forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd State (Maybe n1, Maybe n2)
q) Set (State (Maybe n1))
n1
>                                     forall c a. Container c a => c -> c -> c
`union`
>                                     forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                                     (forall a b. State a -> State b -> State (a, b)
combine (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst State (Maybe n1, Maybe n2)
q)) Set (State (Maybe n2))
n2
>                                else forall c a. Container c a => c
empty)
>                               (if Bool
sync
>                                then forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {a}. State a -> Set (State (a, Maybe n2))
f) forall c a. Container c a => c
empty Set (State (Maybe n1))
n1
>                                else forall c a. Container c a => c
empty)
>           nexts' :: Symbol e -> FSA a e -> State (Maybe a) -> Set (State (Maybe a))
nexts' Symbol e
x FSA a e
f    =  forall b a. b -> (a -> b) -> Maybe a -> b
maybe
>                            (forall c a. Container c a => a -> c
singleton forall a b. (a -> b) -> a -> b
$ forall n. n -> State n
State forall a. Maybe a
Nothing)
>                            (forall {a} {e}.
(Ord a, Ord e) =>
Symbol e -> FSA a e -> State a -> Set (State (Maybe a))
mDests Symbol e
x FSA a e
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. n -> State n
State) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel
>           mDests :: Symbol e -> FSA a e -> State a -> Set (State (Maybe a))
mDests Symbol e
x FSA a e
f State a
q
>               | forall c a. Container c a => c -> Bool
isEmpty Set (State a)
exts  =  forall c a. Container c a => a -> c
singleton forall a b. (a -> b) -> a -> b
$ forall n. n -> State n
State forall a. Maybe a
Nothing
>               | Bool
otherwise     =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just) Set (State a)
exts
>               where exts :: Set (State a)
exts = forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA a e
f Symbol e
x forall a b. (a -> b) -> a -> b
$ forall c a. Container c a => a -> c
singleton State a
q

> cartesianConstruction :: (Ord e, Ord n1, Ord n2) =>
>                          (Bool -> Bool -> Bool) -> FSA n1 e -> FSA n2 e
>                       -> FSA (Maybe n1, Maybe n2) e
> cartesianConstruction :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
(Bool -> Bool -> Bool)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
cartesianConstruction = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
Bool
-> Bool
-> (Bool -> Bool -> Bool)
-> FSA n1 e
-> FSA n2 e
-> FSA (Maybe n1, Maybe n2) e
pairTrace Bool
True Bool
False

> autIntersection :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>                    FSA (Maybe n1, Maybe n2) e
> autIntersection :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
(Bool -> Bool -> Bool)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
cartesianConstruction Bool -> Bool -> Bool
(&&)

> autUnion :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>             FSA (Maybe n1, Maybe n2) e
> autUnion :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
(Bool -> Bool -> Bool)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
cartesianConstruction Bool -> Bool -> Bool
(||)

For the difference A - B, the final states are those that are
accepting in A and non-accepting in B.

Note that the relative complement requires functionality.  Consider
the case of (A - B) where B is nondeterministic in such a way that
there exists a string w for which a computation leads to both an
accepting state qa and a nonaccepting state qn.  Suppose that w leads
to an accepting state in A, qf.  Then the cartesian construction will
contain both (qf, qa) and (qf, qn).

When selecting states to be accepting, (qf, qn) will be included since
qn is nonaccepting in B, and (qf, qn) will be excluded since qa is
accepting in B.  This is not what we want, as it means that w is still
accepted.  Thus we cannot use the cartesian construction to gain an
advantage over the naive implementation (A & not B).

> -- |Returns an 'FSA' accepting all and only those strings
> -- accepted by the first input but rejected by the second.
> --
> -- @since 1.1
> autDifference :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>                  FSA (Maybe n1, Maybe (Set n2)) e
> autDifference :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e
autDifference = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
complement) forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection

Much like the one-sided difference, the symmetric difference of two
automata relies on determinism.

> autSymmetricDifference :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>                           FSA (Maybe (Maybe n1, Maybe n2),
>                                Maybe (Set (Maybe n1, Maybe n2))) e
> autSymmetricDifference :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e
-> FSA n2 e
-> FSA
     (Maybe (Maybe n1, Maybe n2), Maybe (Set (Maybe n1, Maybe n2))) e
autSymmetricDifference FSA n1 e
f1 FSA n2 e
f2
>     = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e
autDifference (forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion FSA n1 e
f1 FSA n2 e
f2) forall a b. (a -> b) -> a -> b
$ forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection FSA n1 e
f1 FSA n2 e
f2

For a total functional FSA, the complement can be obtained by simply
inverting the notion of accepting states.  Totality is necessary, as
any sink-states in the original will be accepting in the complement.
Functionality is necessary, as:

        -> (0)  -a-> ((1)) -a)        (x) is a state, ((x)) is accepting
            |                         -a-> represents a transition on a
            +----a->  (2)  -a)        -a) represents a self-edge on a

becomes under this construction:

        ->((0)) -a->  (1)  -a)
           |
           +-----a-> ((2)) -a)

and the string "a" is accepted in both.

> -- |Returns an 'FSA' accepting all and only those strings not
> -- accepted by the input.
> complement :: (Ord e, Ord n) => FSA n e -> FSA (Set n) e
> complement :: forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
complement = forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
complementDeterministic forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
determinize

> -- |Returns the 'complement' of a deterministic 'FSA'.
> -- The precondition that the input is deterministic
> -- is not checked.
> complementDeterministic :: (Ord e, Ord n) => FSA n e -> FSA n e
> complementDeterministic :: forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
complementDeterministic FSA n e
f = FSA n e
f { finals :: Set (State n)
finals = forall c a. (Container c a, Eq a) => c -> c -> c
difference (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f) (forall n e. FSA n e -> Set (State n)
finals FSA n e
f) }

> -- |@(residue a b)@ is equivalent to @(difference a b)@.
> -- In the context of an approximation and its source,
> -- represents the strings accepted by the approximation
> -- that should not be.
> residue :: (Ord n, Ord e, Enum n) => FSA n e -> FSA n e -> FSA n e
> residue :: forall n e. (Ord n, Ord e, Enum n) => FSA n e -> FSA n e -> FSA n e
residue = forall a b c. ((a, b) -> c) -> a -> b -> c
curry (forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall c a. (Container c a, Eq a) => c -> c -> c
difference)

> -- |@(coresidue a b)@ is equivalent to @(complement (residue a b))@.
> -- In the context of an approximation and its source,
> -- represents unmet constraints of the source.
> coresidue :: (Ord n, Ord e, Enum n) => FSA n e -> FSA n e -> FSA n e
> coresidue :: forall n e. (Ord n, Ord e, Enum n) => FSA n e -> FSA n e -> FSA n e
coresidue FSA n e
a = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>               forall c a. Container c a => c -> c -> c
union (forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
complement FSA n e
a)

The shuffle product of two languages can be constructed
similarly to their intersection.
The difference is that in the standard Cartesian construction,
an edge follows its labeling symbol in both source automata,
while in the shuffle product it follows in only one.
Thus rather than one out-edge per symbol per state,
there are two.

> -- |Returns the shuffle product of its two input autamata.
> --
> -- @since 1.1
> autShuffle :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e
>            -> FSA (Maybe n1, Maybe n2) e
> autShuffle :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autShuffle = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
Bool
-> Bool
-> (Bool -> Bool -> Bool)
-> FSA n1 e
-> FSA n2 e
-> FSA (Maybe n1, Maybe n2) e
pairTrace Bool
False Bool
True Bool -> Bool -> Bool
(&&)

Closely related is the infiltration product,
in which an edge may follow its labeling symbol
in one source, the other, or both simultaneously.

> -- |Returns the infiltration product of its two input autamata.
> --
> -- @since 1.1
> autInfiltration :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e
>                 -> FSA (Maybe n1, Maybe n2) e
> autInfiltration :: forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autInfiltration = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
Bool
-> Bool
-> (Bool -> Bool -> Bool)
-> FSA n1 e
-> FSA n2 e
-> FSA (Maybe n1, Maybe n2) e
pairTrace Bool
True Bool
True Bool -> Bool -> Bool
(&&)


Other Combinations
==================

> autConcatenation :: (Ord n1, Ord n2, Ord e) =>
>                     FSA n1 e -> FSA n2 e
>                  -> FSA (Either n1 n2) e
> autConcatenation :: forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
autConcatenation FSA n1 e
f1 FSA n2 e
f2
>     = FSA
>       { sigma :: Set e
sigma = forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n1 n2) e
f1' forall c a. Container c a => c -> c -> c
`union` forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n1 n2) e
f2'
>       , transitions :: Set (Transition (Either n1 n2) e)
transitions
>           = forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll
>             [ forall n e. FSA n e -> Set (Transition n e)
transitions FSA (Either n1 n2) e
f1'
>             , forall n e. FSA n e -> Set (Transition n e)
transitions FSA (Either n1 n2) e
f2'
>             , Set (Transition (Either n1 n2) e)
combiningTransitions
>             ]
>       , initials :: Set (State (Either n1 n2))
initials = forall n e. FSA n e -> Set (State n)
initials FSA (Either n1 n2) e
f1'
>       , finals :: Set (State (Either n1 n2))
finals   = forall n e. FSA n e -> Set (State n)
finals FSA (Either n1 n2) e
f2'
>       , isDeterministic :: Bool
isDeterministic = Bool
False
>       }
>     where f1' :: FSA (Either n1 n2) e
f1' = forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic forall a b. a -> Either a b
Left FSA n1 e
f1
>           f2' :: FSA (Either n1 n2) e
f2' = forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic forall a b. b -> Either a b
Right FSA n2 e
f2
>           combiningTransitions :: Set (Transition (Either n1 n2) e)
combiningTransitions = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}.
State (Either n1 n2) -> Set (Transition (Either n1 n2) e)
cts) forall c a. Container c a => c
empty
>                                  (forall n e. FSA n e -> Set (State n)
finals FSA (Either n1 n2) e
f1')
>           cts :: State (Either n1 n2) -> Set (Transition (Either n1 n2) e)
cts State (Either n1 n2)
f = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                   (\State (Either n1 n2)
i ->
>                    Transition
>                    { edgeLabel :: Symbol e
edgeLabel = forall e. Symbol e
Epsilon
>                    , source :: State (Either n1 n2)
source = State (Either n1 n2)
f
>                    , destination :: State (Either n1 n2)
destination = State (Either n1 n2)
i
>                    }
>                   )
>                   (forall n e. FSA n e -> Set (State n)
initials FSA (Either n1 n2) e
f2')

> -- |The Kleene Closure of an automaton is
> -- the free monoid under concatenation generated by all strings
> -- in the automaton's represented stringset.
> -- The resulting automaton is nondeterministic.
> kleeneClosure :: (Ord n, Ord e) => FSA n e -> FSA (Either n Bool) e
> kleeneClosure :: forall n e. (Ord n, Ord e) => FSA n e -> FSA (Either n Bool) e
kleeneClosure FSA n e
f
>     = FSA
>       { sigma :: Set e
sigma = forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n Bool) e
f'
>       , transitions :: Set (Transition (Either n Bool) e)
transitions
>           = forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll [ forall n e. FSA n e -> Set (Transition n e)
transitions FSA (Either n Bool) e
f'
>                      , Set (Transition (Either n Bool) e)
toOldInitials
>                      , Set (Transition (Either n Bool) e)
toNewFinal
>                      ]
>       , initials :: Set (State (Either n Bool))
initials = forall c a. Container c a => a -> c
singleton forall {a}. State (Either a Bool)
ni
>       , finals :: Set (State (Either n Bool))
finals = forall c a. Container c a => a -> c
singleton forall {a}. State (Either a Bool)
nf
>       , isDeterministic :: Bool
isDeterministic = Bool
False
>       }
>     where f' :: FSA (Either n Bool) e
f' = forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic forall a b. a -> Either a b
Left FSA n e
f
>           ni :: State (Either a Bool)
ni = forall n. n -> State n
State (forall a b. b -> Either a b
Right Bool
False)
>           nf :: State (Either a Bool)
nf = forall n. n -> State n
State (forall a b. b -> Either a b
Right Bool
True)
>           toOldInitials :: Set (Transition (Either n Bool) e)
toOldInitials = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {e}.
Ord e =>
State (Either n Bool) -> Set (Transition (Either n Bool) e)
cts) forall c a. Container c a => c
empty
>                           (forall c a. Container c a => a -> c -> c
insert forall {a}. State (Either a Bool)
ni (forall n e. FSA n e -> Set (State n)
finals FSA (Either n Bool) e
f'))
>           cts :: State (Either n Bool) -> Set (Transition (Either n Bool) e)
cts State (Either n Bool)
q = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                   (\State (Either n Bool)
i ->
>                    Transition
>                    { edgeLabel :: Symbol e
edgeLabel = forall e. Symbol e
Epsilon
>                    , source :: State (Either n Bool)
source = State (Either n Bool)
q
>                    , destination :: State (Either n Bool)
destination = State (Either n Bool)
i
>                    }
>                   )
>                   (forall n e. FSA n e -> Set (State n)
initials FSA (Either n Bool) e
f')
>           toNewFinal :: Set (Transition (Either n Bool) e)
toNewFinal = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                        (\State (Either n Bool)
q ->
>                         Transition
>                         { edgeLabel :: Symbol e
edgeLabel = forall e. Symbol e
Epsilon
>                         , source :: State (Either n Bool)
source = State (Either n Bool)
q
>                         , destination :: State (Either n Bool)
destination = forall {a}. State (Either a Bool)
nf
>                         }
>                        )
>                        (forall c a. Container c a => a -> c -> c
insert forall {a}. State (Either a Bool)
ni (forall n e. FSA n e -> Set (State n)
finals FSA (Either n Bool) e
f'))


Minimization
============

In general, operations on FSAs have run time proportional to some
(increasing) function of how many states the FSA has.  With this in
mind, we provide a function to make an FSA as small as possible
without loss of information.

We begin by constructing the set of Myhill-Nerode equivalence classes
for the states of the input FSA, then simply replace each state by its
equivalence class.

> -- |Returns a deterministic 'FSA' recognizing the same stringset
> -- as the input, with a minimal number of states.
> minimize :: (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
> minimize :: forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize = forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
minimizeDeterministic forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
determinize

> -- |Returns a deterministic 'FSA' recognizing the same stringset
> -- as the input, with a minimal number of states.
> -- The precondition that the input is deterministic
> -- is not checked.
> minimizeDeterministic :: (Ord e, Ord n) => FSA n e -> FSA (Set n) e
> minimizeDeterministic :: forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
minimizeDeterministic = forall {n} {e}. FSA n e -> FSA n e
setD forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
(FSA n e -> Set (Set (State n))) -> FSA n e -> FSA (Set n) e
minimizeOver forall e n. (Ord e, Ord n) => FSA n e -> Set (Set (State n))
nerode
>     where setD :: FSA n e -> FSA n e
setD FSA n e
f = FSA n e
f {isDeterministic :: Bool
isDeterministic = Bool
True}

> -- |Returns a non-necessarily deterministic 'FSA'
> -- minimized over a given relation.
> -- Some, but not all, relations do guarantee deterministic output.
> -- The precondition that the input is deterministic
> -- is not checked.
> minimizeOver :: (Ord e, Ord n) =>
>                 (FSA n e -> Set (Set (State n))) -> FSA n e -> FSA (Set n) e
> minimizeOver :: forall e n.
(Ord e, Ord n) =>
(FSA n e -> Set (Set (State n))) -> FSA n e -> FSA (Set n) e
minimizeOver FSA n e -> Set (Set (State n))
r FSA n e
fsa = FSA
>                      { sigma :: Set e
sigma = forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa
>                      , transitions :: Set (Transition (Set n) e)
transitions = Set (Transition (Set n) e)
trans
>                      , initials :: Set (State (Set n))
initials = Set (State (Set n))
qi
>                      , finals :: Set (State (Set n))
finals = Set (State (Set n))
fin
>                      , isDeterministic :: Bool
isDeterministic = Bool
False
>                      }
>     where classes :: Set (Set (State n))
classes = FSA n e -> Set (Set (State n))
r FSA n e
fsa
>           classOf :: State n -> State (Set n)
classOf State n
x = forall n. n -> State n
State forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n. State n -> n
nodeLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll forall a b. (a -> b) -> a -> b
$
>                       forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => a -> c -> Bool
contains State n
x) Set (Set (State n))
classes
>           qi :: Set (State (Set n))
qi = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> State (Set n)
classOf forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa
>           fin :: Set (State (Set n))
fin = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> State (Set n)
classOf forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa
>           trans :: Set (Transition (Set n) e)
trans = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                   (\Transition n e
t ->
>                    Transition n e
t
>                    { source :: State (Set n)
source = State n -> State (Set n)
classOf (forall n e. Transition n e -> State n
source Transition n e
t)
>                    , destination :: State (Set n)
destination = State n -> State (Set n)
classOf (forall n e. Transition n e -> State n
destination Transition n e
t)
>                    }
>                   ) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa

> -- |Two strings \(u\) and \(v\) are equivalent iff
> -- for all strings \(w\), \(uw\) and \(vw\) lead to
> -- states in the same equivalence class.
> nerode :: (Ord e, Ord n) => FSA n e -> Set (Set (State n))
> nerode :: forall e n. (Ord e, Ord n) => FSA n e -> Set (Set (State n))
nerode FSA n e
fsa = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> Set (State n)
eqClass Set (State n)
sts
>     where sts :: Set (State n)
sts = forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa
>           i :: Set (State n, State n)
i = forall c a. Container c a => c -> c -> c
union Set (State n, State n)
i' forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\State n
x -> (State n
x, State n
x)) Set (State n)
sts
>           i' :: Set (State n, State n)
i' = forall c a. (Container c a, Eq a) => c -> c -> c
difference (forall a. Ord a => Set a -> Set (a, a)
pairs Set (State n)
sts) forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n, State n)
distinguishedPairs FSA n e
fsa
>           eqClass :: State n -> Set (State n)
eqClass State n
x = forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll
>                       [ forall c a. Container c a => a -> c
singleton State n
x
>                       , forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic forall a b. (a, b) -> a
fst State n
x Set (State n, State n)
i
>                       , forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((forall a. Eq a => a -> a -> Bool
== State n
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) Set (State n, State n)
i
>                       ]

The easiest way to construct the equivalence classes is to iteratively
build a set of known-distinct pairs.  In the beginning we know that
any accepting state is distinct from any non-accepting state.  At each
further iteration, two states p and q are distinct if there exists
some symbol x such that delta<sub>x</sub>(p) is distinct from
delta<sub>x</sub>(q).

When an iteration completes without updating the set of known-distinct
pairs, the algorithm is finished; all possible distinctions have been
discovered.  The Myhill-Nerode equivalence class of a state p, then,
is the set of states not distinct from p.

> distinguishedPairs :: (Ord e, Ord n) => FSA n e -> Set (State n, State n)
> distinguishedPairs :: forall e n. (Ord e, Ord n) => FSA n e -> Set (State n, State n)
distinguishedPairs FSA n e
fsa = forall a b. (a, b) -> a
fst (Set (State n, State n), Set (State n, State n))
result
>     where allPairs :: Set (State n, State n)
allPairs = forall a. Ord a => Set a -> Set (a, a)
pairs (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa)
>           initiallyDistinguished :: Set (State n, State n)
initiallyDistinguished
>               = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Set a -> a -> Set (a, a)
pairs' (forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa)) forall c a. Container c a => c
empty forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                 forall c a. (Container c a, Eq a) => c -> c -> c
difference (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa
>           f :: Set (State n, State n) -> (State n, State n) -> Bool
f Set (State n, State n)
d (State n
a, State n
b) = forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n, State n) -> State n -> State n -> Bool
areDistinguishedByOneStep FSA n e
fsa Set (State n, State n)
d State n
a State n
b
>           result :: (Set (State n, State n), Set (State n, State n))
result = forall a. (a -> Bool) -> (a -> a) -> a -> a
until
>                    (\(Set (State n, State n)
x, Set (State n, State n)
y) -> forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State n, State n)
x forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State n, State n)
y)
>                    (\(Set (State n, State n)
x, Set (State n, State n)
_) ->
>                     ( forall c a. Container c a => c -> c -> c
union Set (State n, State n)
x forall a b. (a -> b) -> a -> b
$
>                       forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Set (State n, State n) -> (State n, State n) -> Bool
f Set (State n, State n)
x) (forall c a. (Container c a, Eq a) => c -> c -> c
difference Set (State n, State n)
allPairs Set (State n, State n)
x)
>                     , Set (State n, State n)
x
>                     )
>                    )
>                    (Set (State n, State n)
initiallyDistinguished, forall c a. Container c a => c
empty)

> areDistinguishedByOneStep :: (Ord e, Ord n) =>
>                              FSA n e ->
>                              Set (State n, State n) ->
>                              State n ->
>                              State n ->
>                              Bool
> areDistinguishedByOneStep :: forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n, State n) -> State n -> State n -> Bool
areDistinguishedByOneStep FSA n e
fsa Set (State n, State n)
knownDistinct State n
p State n
q
>     | forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n, State n)
knownDistinct (forall a. Ord a => a -> a -> (a, a)
makePair State n
p State n
q) = Bool
True
>     | Bool
otherwise = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n, State n)
knownDistinct) Set (State n, State n)
newPairs
>     where destinations :: State n -> e -> Set (State n)
destinations State n
s e
x = forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
fsa (forall e. e -> Symbol e
Symbol e
x) (forall c a. Container c a => a -> c
singleton State n
s)
>           newPairs' :: e -> Set (State n, State n)
newPairs' e
a = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ord a => Set a -> a -> Set (a, a)
pairs' (State n -> e -> Set (State n)
destinations State n
q e
a))
>                         forall c a. Container c a => c
empty
>                         (State n -> e -> Set (State n)
destinations State n
p e
a)
>           newPairs :: Set (State n, State n)
newPairs = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Set (State n, State n)
newPairs') forall c a. Container c a => c
empty (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa)

We only need to check each pair of states once: (1, 2) and (2, 1) are
equivalent in this sense.  Since they are not equivalent in Haskell,
we define a function to ensure that each pair is only built in one
direction.

> makePair :: (Ord a) => a -> a -> (a, a)
> makePair :: forall a. Ord a => a -> a -> (a, a)
makePair a
a a
b = (forall a. Ord a => a -> a -> a
min a
a a
b, forall a. Ord a => a -> a -> a
max a
a a
b)

> pairs :: (Ord a) => Set a -> Set (a, a)
> pairs :: forall a. Ord a => Set a -> Set (a, a)
pairs Set a
xs = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set (a, a)
f) forall c a. Container c a => c
empty Set a
xs
>     where f :: a -> Set (a, a)
f a
x = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((,) a
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> Set a -> (Set a, Set a)
Set.split a
x Set a
xs

> pairs' :: (Ord a) => Set a -> a -> Set (a, a)
> pairs' :: forall a. Ord a => Set a -> a -> Set (a, a)
pairs' Set a
xs a
x = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall a. Ord a => a -> a -> (a, a)
makePair a
x) Set a
xs

An FSA is certainly not minimal if there are states that cannot be
reached by any path from the initial state.  We can trim those.

> -- |The input automaton with unreachable states removed.
> --
> -- @since 1.0
> trimUnreachables :: (Ord e, Ord n) => FSA n e -> FSA n e
> trimUnreachables :: forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables FSA n e
fsa = forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA Set e
alpha Set (Transition n e)
trans Set (State n)
qi Set (State n)
fin (forall n e. FSA n e -> Bool
isDeterministic FSA n e
fsa)
>     where alpha :: Set e
alpha  =  forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa
>           qi :: Set (State n)
qi     =  forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa
>           fin :: Set (State n)
fin    =  forall c a. (Container c a, Eq a) => c -> c -> c
intersection Set (State n)
reachables forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa
>           trans :: Set (Transition n e)
trans  =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
reachables forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
source) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
fsa
>           reachables :: Set (State n)
reachables = Set (State n) -> Set (State n)
reachables' Set (State n)
qi
>           reachables' :: Set (State n) -> Set (State n)
reachables' Set (State n)
qs
>               | Set (State n)
newqs forall a. Eq a => a -> a -> Bool
== Set (State n)
qs  =  Set (State n)
qs
>               | Bool
otherwise    =  Set (State n) -> Set (State n)
reachables' Set (State n)
newqs
>               where initialIDs :: Symbol e -> Set (ID n e)
initialIDs Symbol e
a = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall n e. State n -> [Symbol e] -> ID n e
`ID` [Symbol e
a]) Set (State n)
qs
>                     next :: Set (State n)
next = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse
>                            (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. ID n e -> State n
state forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (ID n e) -> Set (ID n e)
step FSA n e
fsa forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                             forall {e}. Symbol e -> Set (ID n e)
initialIDs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e. e -> Symbol e
Symbol
>                            )
>                            forall c a. Container c a => c
empty
>                            Set e
alpha
>                     newqs :: Set (State n)
newqs = Set (State n)
next forall c a. Container c a => c -> c -> c
`union` Set (State n)
qs

An FSA will often contain states from which no path at all leads to an
accepting state.  These represent failure to match a pattern, which
can be represented equally well by explicit lack of a transition.
Thus we can safely remove them.  Given that we already have a function
to remove states that cannot be reached, the simplest way to remove
these fail-states is to trim the unreachable states in the reversal of
the FSA.

> -- |The reversal of an automaton accepts the reversals of all
> -- strings accepted by the original.
> reverse :: (Ord e, Ord n) => FSA n e -> FSA n e
> reverse :: forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
reverse FSA n e
f = FSA n e
f { isDeterministic :: Bool
isDeterministic = Bool
False
>               , transitions :: Set (Transition n e)
transitions = FSA n e -> Set (Transition n e)
reverseTransitions FSA n e
f
>               , initials :: Set (State n)
initials = forall n e. FSA n e -> Set (State n)
finals FSA n e
f
>               , finals :: Set (State n)
finals = forall n e. FSA n e -> Set (State n)
initials FSA n e
f
>               }
>     where reverseTransition :: Transition n e -> Transition n e
reverseTransition Transition n e
t = Transition n e
t { source :: State n
source = forall n e. Transition n e -> State n
destination Transition n e
t
>                                   , destination :: State n
destination = forall n e. Transition n e -> State n
source Transition n e
t
>                                   }
>           reverseTransitions :: FSA n e -> Set (Transition n e)
reverseTransitions = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall {n} {e}. Transition n e -> Transition n e
reverseTransition forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. FSA n e -> Set (Transition n e)
transitions

> trimFailStates :: (Ord e, Ord n) => FSA n e -> FSA n e
> trimFailStates :: forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimFailStates = forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse

> -- |Returns a normal form of the input.
> -- An FSA is in normal form if it is minimal and deterministic,
> -- and contains neither unreachable states nor nonaccepting sinks.
> -- Node labels are irrelevant, so 'Int' is used as a small
> -- representation.
> normalize :: (Ord e, Ord n) => FSA n e -> FSA Integer e
> normalize :: forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize = forall {n} {e} {n}.
(Ord n, Ord e, Ord n, Enum n) =>
FSA n e -> FSA n e
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimFailStates forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables
>     where f :: FSA n e -> FSA n e
f FSA n e
fsa
>               | forall c a. Container c a => c -> Bool
isEmpty (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa) = forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
complementDeterministic forall a b. (a -> b) -> a -> b
$
>                                        forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa)
>               | Bool
otherwise            = forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates FSA n e
fsa


J-Minimization
==============

Note that a state in an FSA is a representation of a (set of)
string(s).  The standard minimization algorithm considers two strings
w and v equivalent iff for all u, wu and vu are the same state or
otherwise equivalent by a recursive application of this definition.

A different equivalence relation exists, though.  Consider a syntactic
monoid M.  Then two elements w and v are J-equivalent iff the
two-sides ideals MwM and MvM are equal.

This is not equivalent to the statement that wM and vM are equivalent
as well as Mw and Mv.  There are stringsets for which two or more
elements are considered distinct when looking at each one-sided ideal
but are actually equivalent in terms of their two-sided ideals.

> -- |Given an automaton whose syntactic monoid is \(M\),
> -- two strings \(u\) and \(v\) are equivalent iff
> -- \(MuM=MvM\)
> jEquivalence :: (Ord e, Ord n) =>
>                 FSA ([Maybe n], [Symbol e]) e ->
>                 Set (Set (State ([Maybe n], [Symbol e])))
> jEquivalence :: forall e n.
(Ord e, Ord n) =>
FSA ([Maybe n], [Symbol e]) e
-> Set (Set (State ([Maybe n], [Symbol e])))
jEquivalence FSA ([Maybe n], [Symbol e]) e
f = forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy (forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdeal2 FSA ([Maybe n], [Symbol e]) e
f) (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA ([Maybe n], [Symbol e]) e
f)

The primitive left-ideal of an element x of the syntactic monoid is
the set of elements {ax} for all elements a:

> -- |The primitive left ideal.
> --
> -- @since 0.2
> primitiveIdealL :: (Ord n, Ord e) => FSA (n, [Symbol e]) e ->
>                    State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
> primitiveIdealL :: forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdealL FSA (n, [Symbol e]) e
f State (n, [Symbol e])
x = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse
>                       (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (n, [Symbol e]) e
f (forall a b. (a, b) -> b
snd forall a b. (a -> b) -> a -> b
$ forall n. State n -> n
nodeLabel State (n, [Symbol e])
x))
>                       forall c a. Container c a => c
empty forall a b. (a -> b) -> a -> b
$
>                       forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (n, [Symbol e]) e
f

> -- |The generalized \(\delta\) function,
> -- follow each symbol in a string in order.
> --
> -- @since 0.2
> follow :: (Ord n, Ord e) => FSA n e ->
>           [Symbol e] -> State n -> Set (State n)
> follow :: forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA n e
f [Symbol e]
xs State n
q = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall a b c. (a -> b -> c) -> b -> a -> c
flip forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f) forall a. a -> a
id [Symbol e]
xs forall a b. (a -> b) -> a -> b
$ forall c a. Container c a => a -> c
singleton State n
q

The primitive right-ideal is {xa} for all a,
i.e. the reachability relation.
We already have a function that computes this: @epsilonClosure@.
In order to make use of that, we just replace every edge by Epsilon.
Ideally we would use an uninhabited type for the alphabet,
but since Haskell does not have such a type out of the box,
we use the unit type @()@ instead.

> ignoreSymbols :: (Ord n, Ord e) => FSA n e -> FSA n ()
> ignoreSymbols :: forall n e. (Ord n, Ord e) => FSA n e -> FSA n ()
ignoreSymbols FSA n e
f = FSA n e
f { sigma :: Set ()
sigma = forall c a. Container c a => c
empty
>                     , transitions :: Set (Transition n ())
transitions = forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map forall {n} {e} {e}. Transition n e -> Transition n e
x (forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
f)
>                     , isDeterministic :: Bool
isDeterministic = Bool
False
>                     }
>     where x :: Transition n e -> Transition n e
x Transition n e
t = Transition n e
t {edgeLabel :: Symbol e
edgeLabel = forall e. Symbol e
Epsilon}

> -- |The primitive right ideal.
> --
> -- @since 0.2
> primitiveIdealR :: (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
> primitiveIdealR :: forall n e. (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
primitiveIdealR FSA n e
f State n
x = forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure (forall n e. (Ord n, Ord e) => FSA n e -> FSA n ()
ignoreSymbols FSA n e
f) forall a b. (a -> b) -> a -> b
$ forall c a. Container c a => a -> c
singleton State n
x

Then the two-sided ideal is {axb} for all a and b,
i.e. the right-ideals of every left-ideal (or v.v.).

> -- |The primitive two-sided ideal.
> --
> -- @since 0.2
> primitiveIdeal2 :: (Ord n, Ord e) => FSA (n, [Symbol e]) e ->
>                    State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
> primitiveIdeal2 :: forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdeal2 FSA (n, [Symbol e]) e
f = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
primitiveIdealR FSA (n, [Symbol e]) e
f) forall c a. Container c a => c
empty forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                     forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdealL FSA (n, [Symbol e]) e
f

> -- |An automaton is considered trivial under some equivalence relation
> -- if each of its equivalence classes is singleton.
> --
> -- @since 0.2
> trivialUnder :: (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
> trivialUnder :: forall n e. (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
trivialUnder FSA n e -> Set (Set (State n))
f = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((forall a. Eq a => a -> a -> Bool
== Integer
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize) forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (Set (State n))
f


H-Minimization
==============

Where two strings are J-equivalent iff their two-sided ideals are equal,
they are H-equivalent if their corresponding one-sided ideals are equal.
That is, w is equivalent to v iff wM == vM and Mw == Mv.

> -- |Given an automaton whose syntactic monoid is \(M\),
> -- two strings \(u\) and \(v\) are equivalent if
> -- \(Mu=Mv\) and \(uM=vM\).
> --
> -- @since 0.2
> hEquivalence :: (Ord n, Ord e) =>
>                 FSA (n, [Symbol e]) e -> Set (Set (State (n, [Symbol e])))
> hEquivalence :: forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e -> Set (Set (State (n, [Symbol e])))
hEquivalence FSA (n, [Symbol e]) e
f = forall a n.
(Ord a, Ord n) =>
(n -> a) -> Set (Set n) -> Set (Set n)
refinePartitionBy (forall n e. (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
primitiveIdealR FSA (n, [Symbol e]) e
f) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                  forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy (forall n e.
(Ord n, Ord e) =>
FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdealL FSA (n, [Symbol e]) e
f) forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA (n, [Symbol e]) e
f


Determinization
================

Converting a non-deterministic FSA to a deterministic one (DFA) can
improve the speed of determining whether the language represented by
the FSA contains a string.  Further, both complexity-classification
and minimization require DFAs as input.

> metaFlip :: Ord n => Set (State n) -> State (Set n)
> metaFlip :: forall n. Ord n => Set (State n) -> State (Set n)
metaFlip = forall n. n -> State n
State forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall n. State n -> n
nodeLabel

> powersetConstruction :: (Ord e, Ord n) =>
>                         FSA n e ->
>                         Set (State n) ->
>                         (Set (State n) -> Bool) ->
>                         FSA (Set n) e
> powersetConstruction :: forall e n.
(Ord e, Ord n) =>
FSA n e
-> Set (State n) -> (Set (State n) -> Bool) -> FSA (Set n) e
powersetConstruction FSA n e
f Set (State n)
start Set (State n) -> Bool
isFinal = forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
f) Set (Transition (Set n) e)
trans Set (State (Set n))
qi Set (State (Set n))
fin Bool
True
>     where qi :: Set (State (Set n))
qi = forall c a. Container c a => a -> c
singleton (forall n. Ord n => Set (State n) -> State (Set n)
metaFlip Set (State n)
start)
>           buildTransition :: e -> Set (State n) -> (e, Set (State n), Set (State n))
buildTransition e
a Set (State n)
q = (e
a, Set (State n)
q, forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f (forall e. e -> Symbol e
Symbol e
a) Set (State n)
q)
>           buildTransitions' :: Set (State n) -> Set (e, Set (State n), Set (State n))
buildTransitions' Set (State n)
q
>               = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (e -> Set (State n) -> (e, Set (State n), Set (State n))
`buildTransition` Set (State n)
q) forall a b. (a -> b) -> a -> b
$ forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
f
>           buildTransitions :: Set (Set (State n)) -> Set (e, Set (State n), Set (State n))
buildTransitions = forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> Set (e, Set (State n), Set (State n))
buildTransitions') forall c a. Container c a => c
empty
>           (Set (e, Set (State n), Set (State n))
trans',Set (Set (State n))
qs,Set (Set (State n))
_)
>               = forall a. (a -> Bool) -> (a -> a) -> a -> a
until
>                 (\(Set (e, Set (State n), Set (State n))
_, Set (Set (State n))
b, Set (Set (State n))
c) -> forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (Set (State n))
b forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (Set (State n))
c)
>                 (\(Set (e, Set (State n), Set (State n))
a, Set (Set (State n))
b, Set (Set (State n))
c) ->
>                  let d :: Set (e, Set (State n), Set (State n))
d = Set (Set (State n)) -> Set (e, Set (State n), Set (State n))
buildTransitions (forall c a. (Container c a, Eq a) => c -> c -> c
difference Set (Set (State n))
c Set (Set (State n))
b)
>                  in ( Set (e, Set (State n), Set (State n))
a forall c a. Container c a => c -> c -> c
`union` Set (e, Set (State n), Set (State n))
d
>                     , Set (Set (State n))
c
>                     , forall c a. Container c a => c -> c -> c
union Set (Set (State n))
c forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (\(e
_, Set (State n)
_, Set (State n)
z) -> Set (State n)
z) Set (e, Set (State n), Set (State n))
d
>                     )
>                 )
>                 (forall c a. Container c a => c
empty, forall c a. Container c a => c
empty, forall c a. Container c a => a -> c
singleton Set (State n)
start)
>           makeRealTransition :: (e, Set (State n), Set (State n)) -> Transition (Set n) e
makeRealTransition (e
a, Set (State n)
b, Set (State n)
c)
>               = Transition
>                 { edgeLabel :: Symbol e
edgeLabel = forall e. e -> Symbol e
Symbol e
a
>                 , source :: State (Set n)
source = forall n. Ord n => Set (State n) -> State (Set n)
metaFlip Set (State n)
b
>                 , destination :: State (Set n)
destination = forall n. Ord n => Set (State n) -> State (Set n)
metaFlip Set (State n)
c
>                 }
>           trans :: Set (Transition (Set n) e)
trans = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall {n} {e}.
Ord n =>
(e, Set (State n), Set (State n)) -> Transition (Set n) e
makeRealTransition Set (e, Set (State n), Set (State n))
trans'
>           fin :: Set (State (Set n))
fin = forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall n. Ord n => Set (State n) -> State (Set n)
metaFlip forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep Set (State n) -> Bool
isFinal Set (Set (State n))
qs

> -- |Returns a deterministic automaton representing the same
> -- stringset as the potentially nondeterministic input.
> determinize :: (Ord e, Ord n) => FSA n e -> FSA (Set n) e
> determinize :: forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
determinize FSA n e
f
>     | forall n e. FSA n e -> Bool
isDeterministic FSA n e
f = forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic forall c a. Container c a => a -> c
singleton FSA n e
f
>     | Bool
otherwise = forall e n.
(Ord e, Ord n) =>
FSA n e
-> Set (State n) -> (Set (State n) -> Bool) -> FSA (Set n) e
powersetConstruction FSA n e
f (forall n e. FSA n e -> Set (State n)
initials FSA n e
f) Set (State n) -> Bool
isFinal
>     where isFinal :: Set (State n) -> Bool
isFinal = forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (forall n e. FSA n e -> Set (State n)
finals FSA n e
f)) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
f


The Powerset Graph
==================

When determinizing an FSA, we use a powerset construction building out
from the set of initial states.  We can use the same construction but
begin instead with the set of all states to obtain a different
powerset graph.  Though there are many possible initial conditions,
including the one used for determinization, we call this particular
instance *the* powerset graph.  If our source FSA happens to be
normalized, we can gather a lot of information from this graph.

We will tag any states not disjoint from the set of final states in
the source as accepting.

> -- |Given an automaton \(M\) with stateset \(Q\),
> -- the powerset graph of \(M\) is an automaton with
> -- stateset in the powerset of \(Q\).
> -- From a node \(\{q_1,q_2,\ldots,q_n\}\),
> -- there is an edge labelled \(\sigma\) that leads to
> -- \(\{\delta(q_1,\sigma), \delta(q_2,\sigma), \ldots, \delta(q_n, \sigma)\}\),
> -- where \(\delta\) is the transition function of the input.
> -- The initial state is \(Q\), and the result is complete.
> powersetGraph :: (Ord e, Ord n) => FSA n e -> FSA (Set n) e
> powersetGraph :: forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
powersetGraph FSA n e
f = forall e n.
(Ord e, Ord n) =>
FSA n e
-> Set (State n) -> (Set (State n) -> Bool) -> FSA (Set n) e
powersetConstruction FSA n e
f (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f) Set (State n) -> Bool
hasAccept
>     where hasAccept :: Set (State n) -> Bool
hasAccept Set (State n)
qs = forall c a. (Container c a, Eq a) => c -> c -> c
intersection (forall n e. FSA n e -> Set (State n)
finals FSA n e
f) Set (State n)
qs forall a. Eq a => a -> a -> Bool
/= forall c a. Container c a => c
empty


The Syntactic Monoid
====================

In the powerset graph (PSG), states are labelled by sets of states.
For all states Q and symbols x, there is an edge labelled by x from Q
to the state labelled by Q' such that for all q' in Q', there exists
some q in Q such that q goes to q' on x.  The syntactic monoid differs
in that the states are effectively labelled by functions.  Here we
will use lists of the form [q_0, q_1, ..., q_n].

The syntactic monoid a DFA whose states are labelled [0, 1, ..., n]
will always contain the state [0, 1, ..., n].  This is the initial
state.  There exist edges between states are found by mapping over the
list.  That is, if delta is the transition function from QxSigma->Q:

    delta' [q_0, ..., q_n] x = [delta q_0 x, ..., delta q_n x]

Any state labelled by a function mapping an initial state to a final
state is considered accepting in the syntactic monoid.

> -- |Given an automaton \(M\) with stateset \(Q\),
> -- the syntactic monoid of \(M\) is an automaton with
> -- stateset in \((Q\rightarrow Q)\).
> -- Here these functions are represented by lists,
> -- where \(q_i\) maps to the \(i^\text{th}\) element of the list.
> -- From a node \(\langle q_1,q_2,\ldots,q_n\rangle\),
> -- there is an edge labelled \(\sigma\) that leads to
> -- \(\langle\delta(q_1,\sigma), \delta(q_2,\sigma), \ldots, \delta(q_n, \sigma)\rangle\),
> -- where \(\delta\) is the transition function of the input.
> -- The initial state is the identity function, and the result is complete.
> syntacticMonoid :: (Ord e, Ord n) =>
>                    FSA n e -> FSA ([Maybe n], [Symbol e]) e
> syntacticMonoid :: forall e n.
(Ord e, Ord n) =>
FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid FSA n e
m = FSA { sigma :: Set e
sigma = forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
m
>                         , transitions :: Set (Transition ([Maybe n], [Symbol e]) e)
transitions = Set (Transition ([Maybe n], [Symbol e]) e)
t
>                         , initials :: Set (State ([Maybe n], [Symbol e]))
initials = Set (State ([Maybe n], [Symbol e]))
i
>                         , finals :: Set (State ([Maybe n], [Symbol e]))
finals = Set (State ([Maybe n], [Symbol e]))
f
>                         , isDeterministic :: Bool
isDeterministic = Bool
True
>                         }
>     where i :: Set (State ([Maybe n], [Symbol e]))
i   =  forall c a. Container c a => a -> c
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) []) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just) forall a b. (a -> b) -> a -> b
$ [State n]
s
>           s :: [State n]
s   =  forall a. Set a -> [a]
Set.toList (forall n e. FSA n e -> Set (State n)
initials FSA n e
m) forall a. [a] -> [a] -> [a]
++
>                  forall a. Set a -> [a]
Set.toList (forall c a. (Container c a, Eq a) => c -> c -> c
difference (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
m) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n e
m)
>           n :: Int
n   =  forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size (forall n e. FSA n e -> Set (State n)
initials FSA n e
m)
>           i' :: Set (State ([Maybe n], [Symbol e]))
i'  =  if forall c a. (Container c a, Eq a) => c -> c -> c
intersection (forall n e. FSA n e -> Set (State n)
finals FSA n e
m) (forall n e. FSA n e -> Set (State n)
initials FSA n e
m) forall a. Eq a => a -> a -> Bool
/= forall c a. Container c a => c
empty
>                  then Set (State ([Maybe n], [Symbol e]))
i
>                  else forall c a. Container c a => c
empty
>           (Set (Transition ([Maybe n], [Symbol e]) e)
t,Set (State ([Maybe n], [Symbol e]))
_,Set (State ([Maybe n], [Symbol e]))
f,Set (State ([Maybe n], [Symbol e]))
_)
>               = forall e n.
(Ord e, Ord n) =>
FSA n e
-> Int
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
syntacticMonoid' FSA n e
m Int
n (forall c a. Container c a => c
empty, Set (State ([Maybe n], [Symbol e]))
i, Set (State ([Maybe n], [Symbol e]))
i', Set (State ([Maybe n], [Symbol e]))
i)

> syntacticMonoid' :: (Ord e, Ord n) => FSA n e -> Int ->
>                     ( Set (Transition ([Maybe n], [Symbol e]) e)
>                     , Set (State ([Maybe n], [Symbol e]))
>                     , Set (State ([Maybe n], [Symbol e]))
>                     , Set (State ([Maybe n], [Symbol e]))
>                     ) ->
>                     ( Set (Transition ([Maybe n], [Symbol e]) e)
>                     , Set (State ([Maybe n], [Symbol e]))
>                     , Set (State ([Maybe n], [Symbol e]))
>                     , Set (State ([Maybe n], [Symbol e]))
>                     )
> syntacticMonoid' :: forall e n.
(Ord e, Ord n) =>
FSA n e
-> Int
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
syntacticMonoid' FSA n e
f Int
n former :: (Set (Transition ([Maybe n], [Symbol e]) e),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])))
former@(Set (Transition ([Maybe n], [Symbol e]) e)
ot, Set (State ([Maybe n], [Symbol e]))
os, Set (State ([Maybe n], [Symbol e]))
ofi, Set (State ([Maybe n], [Symbol e]))
s)
>     | forall c a. Container c a => c -> Bool
isEmpty Set (State ([Maybe n], [Symbol e]))
s  =  (Set (Transition ([Maybe n], [Symbol e]) e),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])))
former
>     | Bool
otherwise  =  forall e n.
(Ord e, Ord n) =>
FSA n e
-> Int
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
-> (Set (Transition ([Maybe n], [Symbol e]) e),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])),
    Set (State ([Maybe n], [Symbol e])))
syntacticMonoid' FSA n e
f Int
n (Set (Transition ([Maybe n], [Symbol e]) e),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])))
next
>     where next :: (Set (Transition ([Maybe n], [Symbol e]) e),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])),
 Set (State ([Maybe n], [Symbol e])))
next      =  ( Set (Transition ([Maybe n], [Symbol e]) e)
nt forall c a. Container c a => c -> c -> c
`union` Set (Transition ([Maybe n], [Symbol e]) e)
ot
>                        , Set (State ([Maybe n], [Symbol e]))
ns forall c a. Container c a => c -> c -> c
`union` Set (State ([Maybe n], [Symbol e]))
os
>                        , Set (State ([Maybe n], [Symbol e]))
nf forall c a. Container c a => c -> c -> c
`union` Set (State ([Maybe n], [Symbol e]))
ofi
>                        , Set (State ([Maybe n], [Symbol e]))
ns
>                        )
>           alpha :: Set e
alpha     =  forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
f
>           move :: e
-> State ([Maybe n], [Symbol e])
-> Transition ([Maybe n], [Symbol e]) e
move e
a State ([Maybe n], [Symbol e])
q  =  forall (c :: * -> *) a b e.
(Container (c (State (a, b))) (State (a, b)), Collapsible c,
 Eq a) =>
c (State (a, b)) -> Transition (a, b) e -> Transition (a, b) e
replaceDestinationFromMap (Set (State ([Maybe n], [Symbol e]))
s forall c a. Container c a => c -> c -> c
`union` Set (State ([Maybe n], [Symbol e]))
os) forall a b. (a -> b) -> a -> b
$
>                        Transition
>                        { edgeLabel :: Symbol e
edgeLabel = forall e. e -> Symbol e
Symbol e
a
>                        , source :: State ([Maybe n], [Symbol e])
source = State ([Maybe n], [Symbol e])
q
>                        , destination :: State ([Maybe n], [Symbol e])
destination = forall {s :: * -> *} {b1} {f :: * -> *}.
(Container (s b1) (Maybe n), Functor f, Collapsible s) =>
Symbol e -> f (s (Maybe n), [Symbol e]) -> f (s b1, [Symbol e])
move' (forall e. e -> Symbol e
Symbol e
a) State ([Maybe n], [Symbol e])
q
>                        }
>           move' :: Symbol e -> f (s (Maybe n), [Symbol e]) -> f (s b1, [Symbol e])
move' Symbol e
a
>               = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
>                 (forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
bimap
>                  (forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Maybe a
Nothing
>                         forall a b. (a -> b) -> a -> b
$ forall {l :: * -> *} {a} {a}.
(Eq (l (State a)), Container (l (State a)) a, Linearizable l) =>
l (State a) -> Maybe a
pull forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f Symbol e
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a. Container c a => a -> c
singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. n -> State n
State))
>                  (forall a. [a] -> [a] -> [a]
++ [Symbol e
a]))
>           pull :: l (State a) -> Maybe a
pull l (State a)
xs   =  if l (State a)
xs forall a. Eq a => a -> a -> Bool
== forall c a. Container c a => c
empty
>                        then forall a. Maybe a
Nothing
>                        else forall n. State n -> n
nodeLabel forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just (forall (l :: * -> *) a. Linearizable l => l a -> a
chooseOne l (State a)
xs)
>           nt :: Set (Transition ([Maybe n], [Symbol e]) e)
nt        =  forall (c :: * -> *) n n' e.
(Container (c (Transition (n, n') e)) (Transition (n, n') e),
 Collapsible c, Ord n, Ord n', Ord e) =>
c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst forall a b. (a -> b) -> a -> b
$
>                        forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall c a. Container c a => c -> c -> c
union forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Set (Transition ([Maybe n], [Symbol e]) e)
nt') forall c a. Container c a => c
empty Set e
alpha
>           nt' :: e -> Set (Transition ([Maybe n], [Symbol e]) e)
nt' e
a     =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (e
-> State ([Maybe n], [Symbol e])
-> Transition ([Maybe n], [Symbol e]) e
move e
a) Set (State ([Maybe n], [Symbol e]))
s
>           ns :: Set (State ([Maybe n], [Symbol e]))
ns        =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => c -> a -> Bool
isNotIn Set (State [Maybe n])
os' forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst)
>                        forall a b. (a -> b) -> a -> b
$ forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall n e. Transition n e -> State n
destination Set (Transition ([Maybe n], [Symbol e]) e)
nt
>           nf :: Set (State ([Maybe n], [Symbol e]))
nf        =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep forall {b}. State ([Maybe n], b) -> Bool
hasFinal Set (State ([Maybe n], [Symbol e]))
ns
>           os' :: Set (State [Maybe n])
os'       =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> a
fst) Set (State ([Maybe n], [Symbol e]))
os
>           fins :: [Maybe n]
fins      =  forall n. State n -> n
nodeLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. a -> Maybe a
Just)
>                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
f
>           hasFinal :: State ([Maybe n], b) -> Bool
hasFinal  =  Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a. Container c a => c -> Bool
isEmpty forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c a. (Container c a, Eq a) => c -> c -> c
intersection [Maybe n]
fins
>                        forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Int -> [a] -> [a]
take Int
n forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> replaceDestinationFromMap ::
>     (Container (c (State (a, b))) (State (a, b)), Collapsible c, Eq a) =>
>     c (State (a, b)) -> Transition (a, b) e -> Transition (a, b) e
> replaceDestinationFromMap :: forall (c :: * -> *) a b e.
(Container (c (State (a, b))) (State (a, b)), Collapsible c,
 Eq a) =>
c (State (a, b)) -> Transition (a, b) e -> Transition (a, b) e
replaceDestinationFromMap c (State (a, b))
m Transition (a, b) e
t
>     | forall c a. Container c a => c -> Bool
isEmpty c (State (a, b))
m' =  Transition (a, b) e
t
>     | Bool
otherwise  =  Transition (a, b) e
t {destination :: State (a, b)
destination = forall (l :: * -> *) a. Linearizable l => l a -> a
chooseOne c (State (a, b))
m'}
>     where m' :: c (State (a, b))
m'  =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall a. Eq a => a -> a -> Bool
(==) (forall {c} {b}. State (c, b) -> c
fn forall a b. (a -> b) -> a -> b
$ forall n e. Transition n e -> State n
destination Transition (a, b) e
t) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {c} {b}. State (c, b) -> c
fn) c (State (a, b))
m
>           fn :: State (c, b) -> c
fn  =  forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel

> mergeByDestFst ::
>     ( Container (c (Transition (n, n') e)) (Transition (n, n') e)
>     , Collapsible c, Ord n, Ord n', Ord e
>     ) => c (Transition (n, n') e) -> c (Transition (n, n') e)
> mergeByDestFst :: forall (c :: * -> *) n n' e.
(Container (c (Transition (n, n') e)) (Transition (n, n') e),
 Collapsible c, Ord n, Ord n', Ord e) =>
c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst = forall (c :: * -> *) n n' e.
(Container (c (Transition (n, n') e)) (Transition (n, n') e),
 Collapsible c, Ord n, Ord n', Ord e) =>
c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst' forall c a. Container c a => c
empty

> mergeByDestFst' ::
>     ( Container (c (Transition (n, n') e)) (Transition (n, n') e)
>     , Collapsible c, Ord n, Ord n', Ord e
>     ) =>
>     c (Transition (n, n') e) -> c (Transition (n, n') e) ->
>     c (Transition (n, n') e)
> mergeByDestFst' :: forall (c :: * -> *) n n' e.
(Container (c (Transition (n, n') e)) (Transition (n, n') e),
 Collapsible c, Ord n, Ord n', Ord e) =>
c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst' c (Transition (n, n') e)
p c (Transition (n, n') e)
l
>     | forall c a. Container c a => c -> Bool
isEmpty c (Transition (n, n') e)
l = c (Transition (n, n') e)
p
>     | Bool
otherwise
>           = forall (c :: * -> *) n n' e.
(Container (c (Transition (n, n') e)) (Transition (n, n') e),
 Collapsible c, Ord n, Ord n', Ord e) =>
c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst'
>             (forall c a. Container c a => c -> c -> c
union c (Transition (n, n') e)
p   forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>              forall c a. Container c a => a -> c -> c
insert Transition (n, n') e
x  forall a b. (a -> b) -> a -> b
$
>              forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall {n} {e}. State n -> Transition n e -> Transition n e
set_dest (forall n e. Transition n e -> State n
destination Transition (n, n') e
x)) c (Transition (n, n') e)
sds
>             ) forall a b. (a -> b) -> a -> b
$ forall c a. (Container c a, Eq a) => c -> c -> c
difference c (Transition (n, n') e)
xs c (Transition (n, n') e)
sds
>     where (Transition (n, n') e
x, c (Transition (n, n') e)
xs)       =  forall (l :: * -> *) a. Linearizable l => l a -> (a, l a)
choose c (Transition (n, n') e)
l
>           fnd :: Transition (c, b) e -> c
fnd           =  forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n. State n -> n
nodeLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> State n
destination
>           sds :: c (Transition (n, n') e)
sds           =  forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall a. Eq a => a -> a -> Bool
(==) (forall {c} {b} {e}. Transition (c, b) e -> c
fnd Transition (n, n') e
x) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {c} {b} {e}. Transition (c, b) e -> c
fnd) c (Transition (n, n') e)
xs
>           set_dest :: State n -> Transition n e -> Transition n e
set_dest State n
d Transition n e
t  =  Transition n e
t {destination :: State n
destination = State n
d}


Alphabet Manipulation
=====================

> -- |Add missing symbols to the alphabet of an automaton.
> -- The result is an automaton with at least the provided alphabet
> -- that licenses exactly the same set of strings as the input.
> extendAlphabetTo :: (Ord a, Ord b) => Set b -> FSA a b ->
>                     FSA (Maybe Integer, Maybe a) b
> extendAlphabetTo :: forall a b.
(Ord a, Ord b) =>
Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
extendAlphabetTo Set b
syms = forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
emptyWithAlphabet Set b
syms

A "semantic automaton" is one in which a constraint is realized for
a universal alphabet.  This is achieved by using edges labelled by
'Nothing' to represent symbols not already included in the alphabet
and an extend function that takes these edges into account.

For example, consider the local and piecewise constraints:
* No A immediately follows another A, and
* No A follows another A.
As automata with alphabet {A} these constraints appear identical,
each licensing only the empty string and "A" itself.  But if the
alphabet were instead {A,B}, then they would instead license:
* B*A?(BA?)*, and
* B*A?B*, respectively.
Since the source automata for these constraints are identical,
no algorithm can know which variant to extend the alphabet to.
Encoding the universal alphabet in the transition graph with
semantic automata can prevent this issue by explicitly stating
which alternative is correct.

One caveat with the use of semantic automata is that before any
operation combines two or more automata, the inputs must have their
alphabets unified.

> -- |Add missing symbols to the alphabet of an automaton.
> -- As the symbol 'Nothing' is taken to represent
> -- any symbol not currently in the alphabet,
> -- new edges are added in parallel to existing edges labelled by 'Nothing'.
> semanticallyExtendAlphabetTo ::
>     (Ord a, Ord b) => Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
> semanticallyExtendAlphabetTo :: forall a b.
(Ord a, Ord b) =>
Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
semanticallyExtendAlphabetTo Set b
syms FSA a (Maybe b)
fsa
>     = FSA a (Maybe b)
fsa { sigma :: Set (Maybe b)
sigma       = Set (Maybe b)
as forall c a. Container c a => c -> c -> c
`union` Set (Maybe b)
new
>           , transitions :: Set (Transition a (Maybe b))
transitions = Set (Transition a (Maybe b))
ts forall c a. Container c a => c -> c -> c
`union` Set (Transition a (Maybe b))
ts'
>           }
>     where as :: Set (Maybe b)
as   =  forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa
>           new :: Set (Maybe b)
new  =  forall c a. (Container c a, Eq a) => c -> c -> c
difference (forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall a. a -> Maybe a
Just Set b
syms) Set (Maybe b)
as
>           ts :: Set (Transition a (Maybe b))
ts   =  forall n e. FSA n e -> Set (Transition n e)
transitions FSA a (Maybe b)
fsa
>           f :: Transition n e
-> Set (Transition n (Maybe b)) -> Set (Transition n (Maybe b))
f Transition n e
e  =  forall c a. Container c a => c -> c -> c
union (forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                          (\Maybe b
x -> Transition n e
e {edgeLabel :: Symbol (Maybe b)
edgeLabel = forall e. e -> Symbol e
Symbol Maybe b
x}) Set (Maybe b)
new)
>           ts' :: Set (Transition a (Maybe b))
ts'  =  forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse forall {n} {e}.
Ord n =>
Transition n e
-> Set (Transition n (Maybe b)) -> Set (Transition n (Maybe b))
f forall c a. Container c a => c
empty forall a b. (a -> b) -> a -> b
$
>                   forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic forall n e. Transition n e -> Symbol e
edgeLabel (forall e. e -> Symbol e
Symbol forall a. Maybe a
Nothing) Set (Transition a (Maybe b))
ts

> -- |Remove the semantic 'Nothing' edges from an automaton and reflect this
> -- change in the type.
> desemantify :: (Ord a, Ord b) => FSA a (Maybe b) -> FSA a b
> desemantify :: forall a b. (Ord a, Ord b) => FSA a (Maybe b) -> FSA a b
desemantify FSA a (Maybe b)
fsa = forall e e1 n.
(Ord e, Ord e1, Ord n) =>
(e -> e1) -> FSA n e -> FSA n e1
renameSymbolsByMonotonic (forall a. a -> Maybe a -> a
fromMaybe forall a. HasCallStack => a
undefined)
>                   forall a b. (a -> b) -> a -> b
$ forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo
>                     (forall a. Ord a => a -> Set a -> Set a
Set.delete forall a. Maybe a
Nothing (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa))
>                     FSA a (Maybe b)
fsa

> -- |Add self-loops on all symbols to all edges to compute
> -- an upward closure.
> --
> -- @since 1.1
> loopify :: (Ord a, Ord b) => FSA a b -> FSA a b
> loopify :: forall a b. (Ord a, Ord b) => FSA a b -> FSA a b
loopify FSA a b
fsa = FSA a b
fsa { transitions :: Set (Transition a b)
transitions = forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall n e. FSA n e -> Set (Transition n e)
transitions FSA a b
fsa) Set (Transition a b)
trs
>                   , isDeterministic :: Bool
isDeterministic = Bool
False
>                   }
>     where as :: [b]
as = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a b
fsa
>           qs :: [State a]
qs = forall a. Set a -> [a]
Set.toList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA a b
fsa
>           trs :: Set (Transition a b)
trs = forall a. Ord a => [a] -> Set a
Set.fromList forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap forall {e}. e -> [Transition a e]
sigmatr [b]
as
>           sigmatr :: e -> [Transition a e]
sigmatr e
x = forall a b. (a -> b) -> [a] -> [b]
map (\State a
q -> Transition
>                                  { edgeLabel :: Symbol e
edgeLabel = forall e. e -> Symbol e
Symbol e
x
>                                  ,  source :: State a
source = State a
q
>                                  , destination :: State a
destination = State a
q
>                                  }) [State a]
qs

Tierify:
* Ensure that all of T is accounted for in the input
* Remove symbols from the input that are not in T
* Insert self-loops on all symbols not in T, including:
  * the other symbols from the input's alphabet
  * the Nothing placeholder

> -- |Convert a semantic automaton that represents a Local constraint
> -- into a new one that represents the same constraint in the associated
> -- Tier-Local class.
> tierify :: (Ord a, Ord b) => Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
> tierify :: forall a b.
(Ord a, Ord b) =>
Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
tierify Set b
t FSA a (Maybe b)
fsa = forall a b.
(Ord a, Ord b) =>
Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
semanticallyExtendAlphabetTo Set b
as FSA a (Maybe b)
f''
>     where f' :: FSA a (Maybe b)
f'   =  forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo (forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall a. a -> Maybe a
Just Set b
t) forall a b. (a -> b) -> a -> b
$
>                   forall a b.
(Ord a, Ord b) =>
Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
semanticallyExtendAlphabetTo Set b
t FSA a (Maybe b)
fsa
>           f'' :: FSA a (Maybe b)
f''  =  FSA a (Maybe b)
f'
>                   { sigma :: Set (Maybe b)
sigma       = forall c a. Container c a => a -> c -> c
insert forall a. Maybe a
Nothing forall a b. (a -> b) -> a -> b
$ forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
f'
>                   , transitions :: Set (Transition a (Maybe b))
transitions = forall c a. Container c a => c -> c -> c
union (forall n e. FSA n e -> Set (Transition n e)
transitions FSA a (Maybe b)
f') forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                                   forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall {n} {a}. State n -> Transition n (Maybe a)
l forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA a (Maybe b)
f'
>                   }
>           l :: State n -> Transition n (Maybe a)
l State n
q  =  Transition
>                   { edgeLabel :: Symbol (Maybe a)
edgeLabel    =  forall e. e -> Symbol e
Symbol forall a. Maybe a
Nothing
>                   , source :: State n
source       =  State n
q
>                   , destination :: State n
destination  =  State n
q
>                   }
>           as :: Set b
as   =  forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id forall c a. Container c a => a -> c -> c
insert) forall c a. Container c a => c
empty forall a b. (a -> b) -> a -> b
$ forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa

> -- |Allow a given set of symbols to be freely inserted or deleted.
> -- In other words, make those symbols neutral.
> --
> -- @since 1.1
> neutralize :: (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
> neutralize :: forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
neutralize Set b
t FSA a b
fsa = FSA a b
fsa
>                    { sigma :: Set b
sigma = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set b
t forall a b. (a -> b) -> a -> b
$ forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a b
fsa
>                    , transitions :: Set (Transition a b)
transitions = forall n e. FSA n e -> Set (Transition n e)
transitions FSA a b
fsa
>                                    forall c a. Container c a => c -> c -> c
`union` Set (Transition a b)
loops
>                                    forall c a. Container c a => c -> c -> c
`union` Set (Transition a b)
omissions
>                    , isDeterministic :: Bool
isDeterministic = Bool
False
>                    }
>     where tsym :: [Symbol b]
tsym      =  forall a b. (a -> b) -> [a] -> [b]
map forall e. e -> Symbol e
Symbol forall a b. (a -> b) -> a -> b
$ forall a. Set a -> [a]
Set.toList Set b
t
>           x :: Transition n e -> Transition n e
x Transition n e
p       =  Transition n e
p { edgeLabel :: Symbol e
edgeLabel = forall e. Symbol e
Epsilon }
>           c :: Symbol e -> Set (Transition a e)
c Symbol e
s       =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall {e} {n}. Symbol e -> State n -> Transition n e
m Symbol e
s) (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA a b
fsa)
>           m :: Symbol e -> State n -> Transition n e
m Symbol e
s State n
q     =  Transition
>                        { edgeLabel :: Symbol e
edgeLabel    =  Symbol e
s
>                        , source :: State n
source       =  State n
q
>                        , destination :: State n
destination  =  State n
q
>                        }
>           loops :: Set (Transition a b)
loops     =  forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall {e}. Symbol e -> Set (Transition a e)
c [Symbol b]
tsym
>           omissions :: Set (Transition a b)
omissions =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap forall {n} {e} {e}. Transition n e -> Transition n e
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn [Symbol b]
tsym forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall n e. Transition n e -> Symbol e
edgeLabel)
>                        forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA a b
fsa

> -- |Remove symbols from the alphabet of an automaton.
> contractAlphabetTo :: (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
> contractAlphabetTo :: forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo Set b
syms FSA a b
fsa = forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables forall a b. (a -> b) -> a -> b
$
>                               FSA a b
fsa
>                               { sigma :: Set b
sigma       = Set b
syms
>                               , transitions :: Set (Transition a b)
transitions = Set (Transition a b)
trans
>                               }
>     where trans :: Set (Transition a b)
trans = forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep
>                   (forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn
>                    (forall c a. Container c a => a -> c -> c
insert forall e. Symbol e
Epsilon forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic forall e. e -> Symbol e
Symbol Set b
syms) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                    forall n e. Transition n e -> Symbol e
edgeLabel
>                   ) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA a b
fsa

> -- |Ignore the alphabet of an automaton and use a given alphabet instead.
> forceAlphabetTo :: (Ord a, Ord b) =>
>                    Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
> forceAlphabetTo :: forall a b.
(Ord a, Ord b) =>
Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
forceAlphabetTo Set b
syms = forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo Set b
syms forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b.
(Ord a, Ord b) =>
Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
extendAlphabetTo Set b
syms


Miscellaneous Functions
=======================

After several operations, the nodeLabel type of an FSA becomes a deep
mixture of pairs, maybes, and sets.  We can smash these into a smaller
type to improve memory usage and processing speed.

> -- |Equivalent to 'renameStatesBy' \(f\),
> -- where \(f\) is an arbitrary injective function.
> renameStates :: (Ord e, Ord n, Ord n1, Enum n1) => FSA n e -> FSA n1 e
> renameStates :: forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates FSA n e
fsa = forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic
>                    (forall a b c. (a -> b -> c) -> b -> a -> c
flip (forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (forall a. Enum a => Int -> a
toEnum Int
0)) Map n n1
m)
>                    FSA n e
fsa
>     where m :: Map n n1
m = forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b c. (a -> b -> c) -> b -> a -> c
flip forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Enum a => a -> [a]
enumFrom forall a b. (a -> b) -> a -> b
$ forall a. Enum a => Int -> a
toEnum Int
1) forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>               forall a b. (a -> b) -> [a] -> [b]
map forall n. State n -> n
nodeLabel forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toAscList forall a b. (a -> b) -> a -> b
$ forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa
> {-# INLINE[1] renameStates #-}
> {-# RULES
>   "renameStates/identity" renameStates = id
>   #-}

> -- |Transform the node labels of an automaton using a given function.
> -- If this function is not injective, the resulting FSA may not be
> -- deterministic even if the original was.
> renameStatesBy :: (Ord e, Ord n, Ord n1) =>
>                   (n -> n1) -> FSA n e -> FSA n1 e
> renameStatesBy :: forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesBy n -> n1
f FSA n e
a
>     = FSA n e
a { transitions :: Set (Transition n1 e)
transitions      =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall e n. Noitisnart e n -> Transition n e
transition forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. Transition n e -> Noitisnart e n
Noitisnart)
>                               (forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a)
>         , initials :: Set (State n1)
initials         =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (forall n e. FSA n e -> Set (State n)
initials FSA n e
a)
>         , finals :: Set (State n1)
finals           =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (forall n e. FSA n e -> Set (State n)
finals FSA n e
a)
>         , isDeterministic :: Bool
isDeterministic  =  forall n e. FSA n e -> Bool
isDeterministic FSA n e
a Bool -> Bool -> Bool
&&
>                               forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State n1)
ns forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
a)
>         }
>     where ns :: Set (State n1)
ns = forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
a)

> -- |Transform the node labels of an automaton using a given function.
> -- The precondition (that for all states x < y, f x < f y) is not checked.
> renameStatesByMonotonic :: (Ord e, Ord n, Ord n1) =>
>                            (n -> n1) -> FSA n e -> FSA n1 e
> renameStatesByMonotonic :: forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic n -> n1
f FSA n e
a
>     = FSA n e
a { transitions :: Set (Transition n1 e)
transitions  =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                           (forall e n. Noitisnart e n -> Transition n e
transition forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall e n. Transition n e -> Noitisnart e n
Noitisnart) forall a b. (a -> b) -> a -> b
$
>                           forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a
>         , initials :: Set (State n1)
initials     =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
initials FSA n e
a
>         , finals :: Set (State n1)
finals       =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (State n)
finals FSA n e
a
>         }

> -- |Transform the edge labels of an automaton using a given function.
> -- If this function is not injective, the resulting FSA may not be
> -- deterministic even if the original was.
> renameSymbolsBy :: (Ord e, Ord e1, Ord n) =>
>                    (e -> e1) -> FSA n e -> FSA n e1
> renameSymbolsBy :: forall e e1 n.
(Ord e, Ord e1, Ord n) =>
(e -> e1) -> FSA n e -> FSA n e1
renameSymbolsBy e -> e1
f FSA n e
a = FSA n e
a { sigma :: Set e1
sigma            =  Set e1
alpha
>                         , transitions :: Set (Transition n e1)
transitions      =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> e1
f) forall a b. (a -> b) -> a -> b
$ forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a
>                         , isDeterministic :: Bool
isDeterministic  =  forall n e. FSA n e -> Bool
isDeterministic FSA n e
a Bool -> Bool -> Bool
&& Bool
samea
>                         }
>     where alpha :: Set e1
alpha  =  forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap e -> e1
f (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
a)
>           samea :: Bool
samea  =  forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set e1
alpha forall a. Eq a => a -> a -> Bool
== forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
a)

> -- |Transform the edge labels of an automaton using a given function.
> -- The precondition (that for all symbols x < y, f x < f y) is not checked.
> renameSymbolsByMonotonic :: (Ord e, Ord e1, Ord n) =>
>                             (e -> e1) -> FSA n e -> FSA n e1
> renameSymbolsByMonotonic :: forall e e1 n.
(Ord e, Ord e1, Ord n) =>
(e -> e1) -> FSA n e -> FSA n e1
renameSymbolsByMonotonic e -> e1
f FSA n e
a
>     = FSA n e
a { sigma :: Set e1
sigma        =  Set e1
alpha
>         , transitions :: Set (Transition n e1)
transitions  =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> e1
f) (forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a)
>         }
>     where alpha :: Set e1
alpha  =  forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic e -> e1
f (forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
a)

Mapping on tuples:

> bimap :: (a -> c) -> (b -> d) -> (a, b) -> (c, d)
> bimap :: forall a c b d. (a -> c) -> (b -> d) -> (a, b) -> (c, d)
bimap a -> c
f b -> d
g (a
a, b
b) = (a -> c
f a
a, b -> d
g b
b)

A parallel fold implementation based on a tree.  The accumulating
function must be both associative and commutative, as the tree is
built in such a way that order of elements is not preserved.

> data Tree a = Leaf a | Tree (Tree a) (Tree a)
>               deriving (Tree a -> Tree a -> Bool
forall a. Eq a => Tree a -> Tree a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Tree a -> Tree a -> Bool
$c/= :: forall a. Eq a => Tree a -> Tree a -> Bool
== :: Tree a -> Tree a -> Bool
$c== :: forall a. Eq a => Tree a -> Tree a -> Bool
Eq, Tree a -> Tree a -> Bool
Tree a -> Tree a -> Ordering
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
forall {a}. Ord a => Eq (Tree a)
forall a. Ord a => Tree a -> Tree a -> Bool
forall a. Ord a => Tree a -> Tree a -> Ordering
forall a. Ord a => Tree a -> Tree a -> Tree a
min :: Tree a -> Tree a -> Tree a
$cmin :: forall a. Ord a => Tree a -> Tree a -> Tree a
max :: Tree a -> Tree a -> Tree a
$cmax :: forall a. Ord a => Tree a -> Tree a -> Tree a
>= :: Tree a -> Tree a -> Bool
$c>= :: forall a. Ord a => Tree a -> Tree a -> Bool
> :: Tree a -> Tree a -> Bool
$c> :: forall a. Ord a => Tree a -> Tree a -> Bool
<= :: Tree a -> Tree a -> Bool
$c<= :: forall a. Ord a => Tree a -> Tree a -> Bool
< :: Tree a -> Tree a -> Bool
$c< :: forall a. Ord a => Tree a -> Tree a -> Bool
compare :: Tree a -> Tree a -> Ordering
$ccompare :: forall a. Ord a => Tree a -> Tree a -> Ordering
Ord, ReadPrec [Tree a]
ReadPrec (Tree a)
ReadS [Tree a]
forall a. Read a => ReadPrec [Tree a]
forall a. Read a => ReadPrec (Tree a)
forall a. Read a => Int -> ReadS (Tree a)
forall a. Read a => ReadS [Tree a]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
readListPrec :: ReadPrec [Tree a]
$creadListPrec :: forall a. Read a => ReadPrec [Tree a]
readPrec :: ReadPrec (Tree a)
$creadPrec :: forall a. Read a => ReadPrec (Tree a)
readList :: ReadS [Tree a]
$creadList :: forall a. Read a => ReadS [Tree a]
readsPrec :: Int -> ReadS (Tree a)
$creadsPrec :: forall a. Read a => Int -> ReadS (Tree a)
Read, Int -> Tree a -> ShowS
forall a. Show a => Int -> Tree a -> ShowS
forall a. Show a => [Tree a] -> ShowS
forall a. Show a => Tree a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Tree a] -> ShowS
$cshowList :: forall a. Show a => [Tree a] -> ShowS
show :: Tree a -> String
$cshow :: forall a. Show a => Tree a -> String
showsPrec :: Int -> Tree a -> ShowS
$cshowsPrec :: forall a. Show a => Int -> Tree a -> ShowS
Show)

> treeFromList :: [a] -> Tree a
> treeFromList :: forall a. [a] -> Tree a
treeFromList []   =  forall a. HasCallStack => String -> a
error String
"No elements"
> treeFromList [a
x]  =  forall a. a -> Tree a
Leaf a
x
> treeFromList [a]
xs   =  Tree a
ls' forall a b. a -> b -> b
`par` Tree a
rs' forall a b. a -> b -> b
`pseq` forall a. Tree a -> Tree a -> Tree a
Tree Tree a
ls' Tree a
rs'
>     where ([a]
ls, [a]
rs)    =  forall a. [a] -> ([a], [a])
evenOdds [a]
xs
>           (Tree a
ls', Tree a
rs')  =  (forall a. [a] -> Tree a
treeFromList [a]
ls, forall a. [a] -> Tree a
treeFromList [a]
rs)

> instance NFData a => NFData (Tree a)
>     where rnf :: Tree a -> ()
rnf (Leaf a
a)    =  forall a. NFData a => a -> ()
rnf a
a
>           rnf (Tree Tree a
l Tree a
r)  =  forall a. NFData a => a -> ()
rnf Tree a
l seq :: forall a b. a -> b -> b
`seq` forall a. NFData a => a -> ()
rnf Tree a
r

> treeFold :: (a -> a -> a) -> Tree a -> a
> treeFold :: forall a. (a -> a -> a) -> Tree a -> a
treeFold a -> a -> a
_ (Leaf a
x) = a
x
> treeFold a -> a -> a
op (Tree Tree a
l Tree a
r) = a
l' forall a b. a -> b -> b
`par` a
r' forall a b. a -> b -> b
`pseq` (a
l' a -> a -> a
`op` a
r')
>     where l' :: a
l'  =  forall a. (a -> a -> a) -> Tree a -> a
treeFold a -> a -> a
op Tree a
l
>           r' :: a
r'  =  forall a. (a -> a -> a) -> Tree a -> a
treeFold a -> a -> a
op Tree a
r

Split a linked list into two smaller lists by taking the even and odd
elements.  This does not require computing the list's length, thus it
can be more efficient than splitting at the middle element.

The implementation of evenOdds given here will even work on an
infinite stream because it guarantees that elements are output
as soon as they are obtained.

> evenOdds :: [a] -> ([a],[a])
> evenOdds :: forall a. [a] -> ([a], [a])
evenOdds []        =  ([], [])
> evenOdds [a
a]       =  ([a
a], [])
> evenOdds (a
a:a
b:[a]
xs)  =  let ([a]
e, [a]
o) = forall a. [a] -> ([a], [a])
evenOdds [a]
xs in (a
aforall a. a -> [a] -> [a]
:[a]
e, a
bforall a. a -> [a] -> [a]
:[a]
o)