> {-# 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-2021 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
>        -- * Constructing simple automata
>        , totalWithAlphabet
>        , emptyWithAlphabet
>        , emptyLanguage
>        , singletonWithAlphabet
>        , singletonLanguage
>        -- * Derived automata
>        , brzozowskiDerivative
>        , quotLeft
>        , quotMid
>        , quotRight
>        , kleeneClosure
>        , powersetGraph
>        , syntacticMonoid
>        , residue
>        , coresidue
>        -- * Primitive ideals
>        , primitiveIdeal2
>        , primitiveIdealL
>        , primitiveIdealR
>        -- * Transformations
>        , flatIntersection
>        , flatUnion
>        , LTK.FSA.reverse
>        , complement
>        , complementDeterministic
>        , determinize
>        -- ** Minimization
>        , minimize
>        , minimizeDeterministic
>        , normalize
>        , trimUnreachables
>        -- *** Equivalence Classes
>        , minimizeOver
>        , nerode
>        , hEquivalence
>        , jEquivalence
>        , trivialUnder
>        -- ** Alphabetic Transformations
>        , extendAlphabetTo
>        , semanticallyExtendAlphabetTo
>        , tierify
>        , 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.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
>         FSA n e -> Set e
sigma            ::  Set e
>       , FSA n e -> Set (Transition n e)
transitions      ::  Set (Transition n e)
>       , FSA n e -> Set (State n)
initials         ::  Set (State n)
>       , FSA n e -> Set (State n)
finals           ::  Set (State n)
>       , FSA n e -> Bool
isDeterministic  ::  Bool
>       }
>     deriving (Int -> FSA n e -> ShowS
[FSA n e] -> ShowS
FSA n e -> String
(Int -> FSA n e -> ShowS)
-> (FSA n e -> String) -> ([FSA n e] -> ShowS) -> Show (FSA n e)
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)
Int -> ReadS (FSA n e)
ReadS [FSA n e]
(Int -> ReadS (FSA n e))
-> ReadS [FSA n e]
-> ReadPrec (FSA n e)
-> ReadPrec [FSA n e]
-> Read (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 :: FSA n e -> Set (State n)
states FSA n e
f = [Set (State n)] -> Set (State n)
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll [FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
f, FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
f, Set (State n)
others]
>    where others :: Set (State n)
others           = (Transition n e -> Set (State n) -> Set (State n))
-> Set (State n) -> Set (Transition n e) -> Set (State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse Transition n e -> Set (State n) -> Set (State n)
forall c n e. Container c (State n) => Transition n e -> c -> c
extractStates Set (State n)
forall c a. Container c a => c
empty Set (Transition n e)
ts
>          extractStates :: Transition n e -> c -> c
extractStates Transition n e
t  = State n -> c -> c
forall c a. Container c a => a -> c -> c
insert (Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
t) (c -> c) -> (c -> c) -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> c -> c
forall c a. Container c a => a -> c -> c
insert (Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t)
>          ts :: Set (Transition n e)
ts               = FSA n e -> Set (Transition n e)
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 :: Set e -> FSA n e
totalWithAlphabet Set e
as = Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
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 (State n -> Set (State n)
forall c a. Container c a => a -> c
singleton State n
q) (State n -> Set (State n)
forall c a. Container c a => a -> c
singleton State n
q) Bool
True
>     where trans :: Set (Transition n e)
trans  = (e -> Transition n e) -> Set e -> Set (Transition n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                    ((Symbol e -> State n -> Transition n e)
-> State n -> Symbol e -> Transition n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip ((Symbol e -> State n -> State n -> Transition n e)
-> State n -> Symbol e -> State n -> Transition n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip Symbol e -> State n -> State n -> Transition n e
forall n e. Symbol e -> State n -> State n -> Transition n e
Transition State n
q) State n
q (Symbol e -> Transition n e)
-> (e -> Symbol e) -> e -> Transition n e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Symbol e
forall e. e -> Symbol e
Symbol)
>                    Set e
as
>           q :: State n
q      = n -> State n
forall n. n -> State n
State (n -> State n) -> n -> State n
forall a b. (a -> b) -> a -> b
$ Int -> n
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 :: Set e -> FSA n e
emptyWithAlphabet Set e
as = (Set e -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet Set e
as) {finals :: Set (State n)
finals = Set (State n)
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 :: FSA n e
emptyLanguage = Set e -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
emptyWithAlphabet Set e
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 :: Set e -> [e] -> FSA n e
singletonWithAlphabet Set e
as [e]
str
>     = FSA :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
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 = Set (Transition n e)
-> Set (Transition n e) -> Set (Transition n e)
forall c a. Container c a => c -> c -> c
union ([e] -> n -> Set (Transition n e)
trans' [e]
xs (Int -> n
forall a. Enum a => Int -> a
toEnum Int
1)) Set (Transition n e)
failTransitions
>           trans' :: [e] -> n -> Set (Transition n e)
trans' [] n
n
>               = (e -> Transition n e) -> Set e -> Set (Transition n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (\e
a -> Symbol e -> State n -> State n -> Transition n e
forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (e -> Symbol e
forall e. e -> Symbol e
Symbol e
a) (n -> State n
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 = n -> n
forall a. Enum a => a -> a
succ n
n
>                 in Set (Transition n e)
-> Set (Transition n e) -> Set (Transition n e)
forall c a. Container c a => c -> c -> c
union ([e] -> n -> Set (Transition n e)
trans' [e]
xs n
m) (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e) -> Set (Transition n e)
forall a b. (a -> b) -> a -> b
$
>                    (e -> Transition n e) -> Set e -> Set (Transition n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                    (\e
y ->
>                     Symbol e -> State n -> State n -> Transition n e
forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (e -> Symbol e
forall e. e -> Symbol e
Symbol e
y) (n -> State n
forall n. n -> State n
State n
n) (State n -> Transition n e) -> State n -> Transition n e
forall a b. (a -> b) -> a -> b
$
>                     if (e
x e -> e -> Bool
forall a. Eq a => a -> a -> Bool
== e
y)
>                     then n -> State n
forall n. n -> State n
State n
m
>                     else State n
qfail
>                    ) Set e
as
>           qfail :: State n
qfail = n -> State n
forall n. n -> State n
State (n -> State n) -> n -> State n
forall a b. (a -> b) -> a -> b
$ Int -> n
forall a. Enum a => Int -> a
toEnum Int
0
>           failTransitions :: Set (Transition n e)
failTransitions
>               = (e -> Transition n e) -> Set e -> Set (Transition n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                 (\e
a -> Symbol e -> State n -> State n -> Transition n e
forall n e. Symbol e -> State n -> State n -> Transition n e
Transition (e -> Symbol e
forall e. e -> Symbol e
Symbol e
a) State n
qfail State n
qfail)
>                 Set e
as
>           begins :: Set (State n)
begins  =  State n -> Set (State n)
forall c a. Container c a => a -> c
singleton (n -> State n
forall n. n -> State n
State (n -> State n) -> n -> State n
forall a b. (a -> b) -> a -> b
$ Int -> n
forall a. Enum a => Int -> a
toEnum Int
1)
>           qlast :: Int
qlast   =  (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ [e] -> Int
forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size [e]
str
>           fins :: Set (State n)
fins    =  State n -> Set (State n)
forall c a. Container c a => a -> c
singleton (n -> State n
forall n. n -> State n
State (n -> State n) -> n -> State n
forall a b. (a -> b) -> a -> b
$ Int -> n
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 :: [e] -> FSA n e
singletonLanguage [e]
s = Set e -> [e] -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => Set e -> [e] -> FSA n e
singletonWithAlphabet ([e] -> Set e
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
(Symbol e -> Symbol e -> Bool)
-> (Symbol e -> Symbol e -> Bool) -> Eq (Symbol e)
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, Eq (Symbol e)
Eq (Symbol e)
-> (Symbol e -> Symbol e -> Ordering)
-> (Symbol e -> Symbol e -> Bool)
-> (Symbol e -> Symbol e -> Bool)
-> (Symbol e -> Symbol e -> Bool)
-> (Symbol e -> Symbol e -> Bool)
-> (Symbol e -> Symbol e -> Symbol e)
-> (Symbol e -> Symbol e -> Symbol e)
-> Ord (Symbol e)
Symbol e -> Symbol e -> Bool
Symbol e -> Symbol e -> Ordering
Symbol e -> Symbol e -> Symbol e
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
$cp1Ord :: forall e. Ord e => Eq (Symbol e)
Ord, ReadPrec [Symbol e]
ReadPrec (Symbol e)
Int -> ReadS (Symbol e)
ReadS [Symbol e]
(Int -> ReadS (Symbol e))
-> ReadS [Symbol e]
-> ReadPrec (Symbol e)
-> ReadPrec [Symbol e]
-> Read (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
[Symbol e] -> ShowS
Symbol e -> String
(Int -> Symbol e -> ShowS)
-> (Symbol e -> String) -> ([Symbol e] -> ShowS) -> Show (Symbol e)
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 :: s (Symbol e) -> c
unsymbols = (Symbol e -> c -> c) -> c -> s (Symbol e) -> c
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (c -> c -> c
forall a. Monoid a => a -> a -> a
mappend (c -> c -> c) -> (Symbol e -> c) -> Symbol e -> c -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol e -> c
forall p a. Container p a => Symbol a -> p
f) c
forall a. Monoid a => a
mempty
>     where f :: Symbol a -> p
f (Symbol a
x)  =  a -> p
forall c a. Container c a => a -> c
singleton a
x
>           f Symbol a
_           =  p
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.
> data State n = State {State n -> n
nodeLabel :: n} deriving (State n -> State n -> Bool
(State n -> State n -> Bool)
-> (State n -> State n -> Bool) -> Eq (State n)
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, Eq (State n)
Eq (State n)
-> (State n -> State n -> Ordering)
-> (State n -> State n -> Bool)
-> (State n -> State n -> Bool)
-> (State n -> State n -> Bool)
-> (State n -> State n -> Bool)
-> (State n -> State n -> State n)
-> (State n -> State n -> State n)
-> Ord (State n)
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
$cp1Ord :: forall n. Ord n => Eq (State n)
Ord, ReadPrec [State n]
ReadPrec (State n)
Int -> ReadS (State n)
ReadS [State n]
(Int -> ReadS (State n))
-> ReadS [State n]
-> ReadPrec (State n)
-> ReadPrec [State n]
-> Read (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
[State n] -> ShowS
State n -> String
(Int -> State n -> ShowS)
-> (State n -> String) -> ([State n] -> ShowS) -> Show (State n)
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
>       { Transition n e -> Symbol e
edgeLabel   :: (Symbol e)
>       , Transition n e -> State n
source      :: (State n)
>       , Transition n e -> State n
destination :: (State n)
>       }
>     deriving (Transition n e -> Transition n e -> Bool
(Transition n e -> Transition n e -> Bool)
-> (Transition n e -> Transition n e -> Bool)
-> Eq (Transition n e)
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, Eq (Transition n e)
Eq (Transition n e)
-> (Transition n e -> Transition n e -> Ordering)
-> (Transition n e -> Transition n e -> Bool)
-> (Transition n e -> Transition n e -> Bool)
-> (Transition n e -> Transition n e -> Bool)
-> (Transition n e -> Transition n e -> Bool)
-> (Transition n e -> Transition n e -> Transition n e)
-> (Transition n e -> Transition n e -> Transition n e)
-> Ord (Transition n e)
Transition n e -> Transition n e -> Bool
Transition n e -> Transition n e -> Ordering
Transition n e -> Transition n e -> Transition n e
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
$cp1Ord :: forall n e. (Ord e, Ord n) => Eq (Transition n e)
Ord, Int -> Transition n e -> ShowS
[Transition n e] -> ShowS
Transition n e -> String
(Int -> Transition n e -> ShowS)
-> (Transition n e -> String)
-> ([Transition n e] -> ShowS)
-> Show (Transition n e)
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)
Int -> ReadS (Transition n e)
ReadS [Transition n e]
(Int -> ReadS (Transition n e))
-> ReadS [Transition n e]
-> ReadPrec (Transition n e)
-> ReadPrec [Transition n e]
-> Read (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 :: (a -> b) -> Symbol a -> Symbol b
fmap a -> b
_ Symbol a
Epsilon     =  Symbol b
forall e. Symbol e
Epsilon
>           fmap a -> b
f (Symbol a
e)  =  b -> Symbol b
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)  =  e -> ()
forall a. NFData a => a -> ()
rnf e
e


State
-----

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

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

> instance Monad State
>     where return :: a -> State a
return   =  a -> State a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
>           State a
a >>= :: State a -> (a -> State b) -> State b
>>= a -> State b
f  =  a -> State b
f (a -> State b) -> a -> State b
forall a b. (a -> b) -> a -> b
$ State a -> a
forall n. State n -> n
nodeLabel State a
a

#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
(<>) = (n -> n) -> State n -> State n
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((n -> n) -> State n -> State n)
-> (State n -> n -> n) -> State n -> State n -> State n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (n -> n) -> n -> n
forall n. State n -> n
nodeLabel (State (n -> n) -> n -> n)
-> (State n -> State (n -> n)) -> State n -> n -> n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> n -> n) -> State n -> State (n -> n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n -> n
forall a. Semigroup a => a -> a -> a
(<>)
#endif

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

> instance (NFData n) => NFData (State n)
>     where rnf :: State n -> ()
rnf (State n
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 = Symbol e -> ()
forall a. NFData a => a -> ()
rnf (Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel Transition n e
t) () -> () -> ()
`seq`
>                   State n -> ()
forall a. NFData a => a -> ()
rnf (Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
t)    () -> () -> ()
`seq`
>                   State n -> ()
forall a. NFData a => a -> ()
rnf (Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t)

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

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

> instance Functor (Noitisnart e)
>     where fmap :: (a -> b) -> Noitisnart e a -> Noitisnart e b
fmap a -> b
f = Transition b e -> Noitisnart e b
forall e n. Transition n e -> Noitisnart e n
Noitisnart (Transition b e -> Noitisnart e b)
-> (Noitisnart e a -> Transition b e)
-> Noitisnart e a
-> Noitisnart e b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition a e -> Transition b e
forall e. Transition a e -> Transition b e
fmap' (Transition a e -> Transition b e)
-> (Noitisnart e a -> Transition a e)
-> Noitisnart e a
-> Transition b e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Noitisnart e a -> Transition a e
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       =  (a -> b) -> State a -> State b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Transition a e -> State a
forall n e. Transition n e -> State n
source Transition a e
t)
>                             , destination :: State b
destination  =  (a -> b) -> State a -> State b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f (Transition a e -> State a
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 :: FSA n e -> Bool
isNull = (Set (State n) -> Set (State n) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n)
forall c a. Container c a => c
empty) (Set (State n) -> Bool)
-> (FSA n e -> Set (State n)) -> FSA n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals (FSA n e -> Set (State n))
-> (FSA n e -> FSA n e) -> FSA n e -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
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 = FSA Integer e -> FSA Integer e -> Bool
forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> Bool
isomorphic (FSA n e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n e
a) (FSA n e -> FSA Integer e
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 :: FSA n1 e -> FSA n2 e -> Bool
isomorphic FSA n1 e
a FSA n2 e
b = (FSA n1 e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n1 e
a         Set e -> Set e -> Bool
forall a. Eq a => a -> a -> Bool
== FSA n2 e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n2 e
b)          Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
initials FSA n1 e
a) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n2) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n2 e -> Set (State n2)
forall n e. FSA n e -> Set (State n)
initials FSA n2 e
b))  Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a)   Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n2) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n2 e -> Set (State n2)
forall n e. FSA n e -> Set (State n)
finals FSA n2 e
b))    Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n1 e
a)   Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n2) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n2 e -> Set (State n2)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n2 e
b))    Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
initials FSA n1 e
a) Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State (Maybe n1, Maybe n2)) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA (Maybe n1, Maybe n2) e -> Set (State (Maybe n1, Maybe n2))
forall n e. FSA n e -> Set (State n)
initials FSA (Maybe n1, Maybe n2) e
c))  Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a)   Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State (Maybe n1, Maybe n2)) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA (Maybe n1, Maybe n2) e -> Set (State (Maybe n1, Maybe n2))
forall n e. FSA n e -> Set (State n)
finals FSA (Maybe n1, Maybe n2) e
c))    Bool -> Bool -> Bool
&&
>                  (Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n1 e -> Set (State n1)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n1 e
a)   Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
s)
>     where c :: FSA (Maybe n1, Maybe n2) e
c  =  FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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  =  Set (State (Maybe n1, Maybe n2)) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (Set (State (Maybe n1, Maybe n2)) -> Integer)
-> (Set (State (Maybe n1, Maybe n2))
    -> Set (State (Maybe n1, Maybe n2)))
-> Set (State (Maybe n1, Maybe n2))
-> Integer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State (Maybe n1, Maybe n2) -> Bool)
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (State (Maybe n1, Maybe n2) -> State (Maybe n1, Maybe n2) -> Bool
forall a. Eq a => a -> a -> Bool
(/=) ((Maybe n1, Maybe n2) -> State (Maybe n1, Maybe n2)
forall n. n -> State n
State (Maybe n1
forall a. Maybe a
Nothing, Maybe n2
forall a. Maybe a
Nothing))) (Set (State (Maybe n1, Maybe n2)) -> Integer)
-> Set (State (Maybe n1, Maybe n2)) -> Integer
forall a b. (a -> b) -> a -> b
$ FSA (Maybe n1, Maybe n2) e -> Set (State (Maybe n1, Maybe n2))
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 FSA n e -> FSA n e -> Bool
forall a. Eq a => a -> a -> Bool
== FSA n e
b                  =  Ordering
EQ
>               | FSA Integer e -> FSA Integer e -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (FSA n e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
b) (FSA n e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
a)  =  Ordering
LT
>               | FSA Integer e -> FSA Integer e -> Bool
forall c a. (Container c a, Eq a) => c -> c -> Bool
isSubsetOf (FSA n e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
a) (FSA n e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
f FSA n e
b)  =  Ordering
GT
>               | Bool
otherwise               =  (Set e, Set (Transition n e), Set (State n), Set (State n))
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
-> Ordering
forall a. Ord a => a -> a -> Ordering
compare (FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
forall n e.
FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
g FSA n e
a) (FSA n e
-> (Set e, Set (Transition n e), Set (State n), Set (State n))
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 :: FSA n e -> FSA Integer e
f = FSA n e -> FSA Integer e
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 = (FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
x, FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
x, FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
x, FSA n e -> Set (State n)
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       =  FSA n e -> Bool
forall e n. (Ord e, Ord n) => FSA n e -> Bool
isNull
>           isIn :: FSA n e -> [e] -> Bool
isIn          =  FSA n e -> [e] -> Bool
forall e n. (Ord e, Ord n) => FSA n e -> [e] -> Bool
accepts
>           union :: FSA n e -> FSA n e -> FSA n e
union         =  (FSA n e -> FSA n e -> FSA (Maybe n, Maybe n) e)
-> 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 FSA n e -> FSA n e -> FSA (Maybe n, Maybe n) e
forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion
>           intersection :: FSA n e -> FSA n e -> FSA n e
intersection  =  (FSA n e -> FSA n e -> FSA (Maybe n, Maybe n) e)
-> 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 FSA n e -> FSA n e -> FSA (Maybe n, Maybe n) e
forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection
>           difference :: FSA n e -> FSA n e -> FSA n e
difference    =  (FSA n e -> FSA n e -> FSA (Maybe n, Maybe (Set n)) e)
-> 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 FSA n e -> FSA n e -> FSA (Maybe n, Maybe (Set n)) e
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         =  FSA n e
forall e n. (Ord e, Ord n, Enum n) => FSA n e
emptyLanguage
>           singleton :: [e] -> FSA n e
singleton     =  [e] -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage
>           symmetricDifference :: FSA n e -> FSA n e -> FSA n e
symmetricDifference
>               =  (FSA n e
 -> FSA n e
 -> FSA
      (Maybe (Maybe n, Maybe n), Maybe (Set (Maybe n, Maybe n))) e)
-> 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 FSA n e
-> FSA n e
-> FSA (Maybe (Maybe n, Maybe n), Maybe (Set (Maybe n, Maybe n))) e
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
(<>) = FSA n e -> FSA n e -> FSA n e
forall a. Monoid a => a -> a -> a
mappend
#endif

> instance (Enum n, Ord n, Ord e) => Monoid (FSA n e)
>     where mempty :: FSA n e
mempty   =  [e] -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => [e] -> FSA n e
singletonLanguage [e]
forall c a. Container c a => c
empty
>           mappend :: FSA n e -> FSA n e -> FSA n e
mappend  =  (FSA n e -> FSA n e -> FSA (Either n n) e)
-> 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 FSA n e -> FSA n e -> FSA (Either n n) e
forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
autConcatenation

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

> pfold :: (a -> a -> a) -> [a] -> a
> pfold :: (a -> a -> a) -> [a] -> a
pfold = ((Tree a -> a) -> [a] -> a)
-> ((a -> a -> a) -> Tree a -> a) -> (a -> a -> a) -> [a] -> a
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Tree a -> a) -> ([a] -> Tree a) -> [a] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [a] -> Tree a
forall a. [a] -> Tree a
treeFromList) (a -> a -> a) -> Tree a -> a
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 :: [FSA n e] -> FSA n e
flatIntersection [] = String -> FSA n e
forall a. HasCallStack => String -> a
error String
"Cannot take a nullary intersection"
> flatIntersection [FSA n e]
xs = (FSA n e -> FSA n e -> FSA n e) -> [FSA n e] -> FSA n e
forall a. (a -> a -> a) -> [a] -> a
pfold FSA n e -> FSA n e -> FSA n e
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 = FSA (Set (Set (Maybe n1, Maybe n2))) e -> FSA n1 e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates (FSA (Set (Set (Maybe n1, Maybe n2))) e -> FSA n1 e)
-> (FSA (Maybe n1, Maybe n2) e
    -> FSA (Set (Set (Maybe n1, Maybe n2))) e)
-> FSA (Maybe n1, Maybe n2) e
-> FSA n1 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (Maybe n1, Maybe n2) e
-> FSA (Set (Set (Maybe n1, Maybe n2))) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize (FSA (Maybe n1, Maybe n2) e -> FSA n1 e)
-> FSA (Maybe n1, Maybe n2) e -> FSA n1 e
forall a b. (a -> b) -> a -> b
$ FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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 FSA n1 e -> ()
forall a. NFData a => a -> ()
rnf FSA n1 e
x () -> FSA n1 e -> FSA n1 e
`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 :: [FSA n e] -> FSA n e
flatUnion []  =  FSA n e
forall e n. (Ord e, Ord n, Enum n) => FSA n e
emptyLanguage
> flatUnion [FSA n e]
xs  =  (FSA n e -> FSA n e -> FSA n e) -> [FSA n e] -> FSA n e
forall a. (a -> a -> a) -> [a] -> a
pfold FSA n e -> FSA n e -> FSA n e
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 = FSA (Set (Set (Maybe n1, Maybe n2))) e -> FSA n1 e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates (FSA (Set (Set (Maybe n1, Maybe n2))) e -> FSA n1 e)
-> (FSA (Maybe n1, Maybe n2) e
    -> FSA (Set (Set (Maybe n1, Maybe n2))) e)
-> FSA (Maybe n1, Maybe n2) e
-> FSA n1 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (Maybe n1, Maybe n2) e
-> FSA (Set (Set (Maybe n1, Maybe n2))) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize (FSA (Maybe n1, Maybe n2) e -> FSA n1 e)
-> FSA (Maybe n1, Maybe n2) e -> FSA n1 e
forall a b. (a -> b) -> a -> b
$ FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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 FSA n1 e -> ()
forall a. NFData a => a -> ()
rnf FSA n1 e
x () -> FSA n1 e -> FSA n1 e
`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)
>               = Set e -> ()
forall a. NFData a => a -> ()
rnf Set e
a () -> () -> ()
`seq` Set (Transition n e) -> ()
forall a. NFData a => a -> ()
rnf Set (Transition n e)
t () -> () -> ()
`seq` Set (State n) -> ()
forall a. NFData a => a -> ()
rnf Set (State n)
i () -> () -> ()
`seq` Set (State n) -> ()
forall a. NFData a => a -> ()
rnf Set (State n)
f () -> () -> ()
`seq` Bool -> ()
forall a. NFData a => a -> ()
rnf Bool
d

> instance HasAlphabet (FSA n)
>     where alphabet :: FSA n e -> Set e
alphabet = FSA n e -> Set e
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
(ID n e -> ID n e -> Bool)
-> (ID n e -> ID n e -> Bool) -> Eq (ID n e)
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, Eq (ID n e)
Eq (ID n e)
-> (ID n e -> ID n e -> Ordering)
-> (ID n e -> ID n e -> Bool)
-> (ID n e -> ID n e -> Bool)
-> (ID n e -> ID n e -> Bool)
-> (ID n e -> ID n e -> Bool)
-> (ID n e -> ID n e -> ID n e)
-> (ID n e -> ID n e -> ID n e)
-> Ord (ID n e)
ID n e -> ID n e -> Bool
ID n e -> ID n e -> Ordering
ID n e -> ID n e -> ID n e
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
$cp1Ord :: forall n e. (Ord n, Ord e) => Eq (ID n e)
Ord, ReadPrec [ID n e]
ReadPrec (ID n e)
Int -> ReadS (ID n e)
ReadS [ID n e]
(Int -> ReadS (ID n e))
-> ReadS [ID n e]
-> ReadPrec (ID n e)
-> ReadPrec [ID n e]
-> Read (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
[ID n e] -> ShowS
ID n e -> String
(Int -> ID n e -> ShowS)
-> (ID n e -> String) -> ([ID n e] -> ShowS) -> Show (ID n e)
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 :: ID n e -> State n
state (ID State n
a [Symbol e]
_) = State n
a

> string :: ID n e -> [Symbol e]
> string :: 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 :: FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa Set (State n)
qs
>     | FSA n e -> Bool
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 = (Transition n e -> Symbol e)
-> Symbol e -> Set (Transition n e) -> Set (Transition n e)
forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel Symbol e
forall e. Symbol e
Epsilon (FSA n e -> Set (Transition n e)
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
>               | Set (State n) -> Bool
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) -> Set (State n) -> Set (State n)
forall c a. Container c a => c -> c -> c
union Set (State n)
seen Set (State n)
closure)
>                                 (Set (State n) -> Set (State n) -> Set (State n)
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    =  (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
new (State n -> Bool)
-> (Transition n e -> State n) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source) Set (Transition n e)
epsilons
>                     closure :: Set (State n)
closure  =  (Transition n e -> State n)
-> Set (Transition n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Transition n e -> State n
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 :: 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 Set (ID n e) -> Set (ID n e) -> Bool
forall a. Eq a => a -> a -> Bool
== Set (ID n e)
forall c a. Container c a => c
empty  =  Set (ID n e)
forall c a. Container c a => c
empty
>     | Bool
otherwise             =  (ID n e -> Set (ID n e) -> Set (ID n e))
-> Set (ID n e) -> Set (ID n e) -> Set (ID n e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (ID n e) -> Set (ID n e) -> Set (ID n e)
forall c a. Container c a => c -> c -> c
union (Set (ID n e) -> Set (ID n e) -> Set (ID n e))
-> (ID n e -> Set (ID n e))
-> ID n e
-> Set (ID n e)
-> Set (ID n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ID n e -> Set (ID n e)
next) Set (ID n e)
forall c a. Container c a => c
empty Set (ID n e)
filteredIDs
>     where ts :: Set (Transition n e)
ts = FSA n e -> Set (Transition n e)
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 = State n -> [Symbol e] -> ID n e
forall n e. State n -> [Symbol e] -> ID n e
ID (ID n e -> State n
forall n e. ID n e -> State n
state ID n e
i) ((Symbol e -> Bool) -> [Symbol e] -> [Symbol e]
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Symbol e -> Symbol e -> Bool
forall a. Eq a => a -> a -> Bool
/= Symbol e
forall e. Symbol e
Epsilon) (ID n e -> [Symbol e]
forall n e. ID n e -> [Symbol e]
string ID n e
i))
>           filteredIDs :: Set (ID n e)
filteredIDs = (ID n e -> ID n e) -> Set (ID n e) -> Set (ID n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ID n e -> ID n e
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
>               | [Symbol e] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Symbol e]
s     = (State n -> ID n e) -> Set (State n) -> Set (ID n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((State n -> [Symbol e] -> ID n e)
-> [Symbol e] -> State n -> ID n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip State n -> [Symbol e] -> ID n e
forall n e. State n -> [Symbol e] -> ID n e
ID []) Set (State n)
closure
>               | Bool
otherwise  = (State n -> ID n e) -> Set (State n) -> Set (ID n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((State n -> [Symbol e] -> ID n e)
-> [Symbol e] -> State n -> ID n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip State n -> [Symbol e] -> ID n e
forall n e. State n -> [Symbol e] -> ID n e
ID ([Symbol e] -> [Symbol e]
forall a. [a] -> [a]
tail [Symbol e]
s)) Set (State n)
outStates
>               where s :: [Symbol e]
s = ID n e -> [Symbol e]
forall n e. ID n e -> [Symbol e]
string ID n e
i
>                     closure :: Set (State n)
closure = FSA n e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa (State n -> Set (State n)
forall c a. Container c a => a -> c
singleton (ID n e -> State n
forall n e. ID n e -> State n
state ID n e
i))
>                     outStates :: Set (State n)
outStates  = FSA n e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa (Set (State n) -> Set (State n))
-> (Set (Transition n e) -> Set (State n))
-> Set (Transition n e)
-> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                                  (Transition n e -> State n)
-> Set (Transition n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Transition n e -> State n
forall n e. Transition n e -> State n
destination (Set (Transition n e) -> Set (State n))
-> (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e)
-> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                                  (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
closure (State n -> Bool)
-> (Transition n e -> State n) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source) (Set (Transition n e) -> Set (State n))
-> Set (Transition n e) -> Set (State n)
forall a b. (a -> b) -> a -> b
$
>                                  (Transition n e -> Symbol e)
-> Symbol e -> Set (Transition n e) -> Set (Transition n e)
forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel ([Symbol e] -> Symbol e
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 :: FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f Symbol e
x = (ID n e -> State n) -> Set (ID n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ID n e -> State n
forall n e. ID n e -> State n
state (Set (ID n e) -> Set (State n))
-> (Set (State n) -> Set (ID n e))
-> Set (State n)
-> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (ID n e) -> Set (ID n e)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (ID n e) -> Set (ID n e)
step FSA n e
f (Set (ID n e) -> Set (ID n e))
-> (Set (State n) -> Set (ID n e)) -> Set (State n) -> Set (ID n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n -> ID n e) -> Set (State n) -> Set (ID n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((State n -> [Symbol e] -> ID n e)
-> [Symbol e] -> State n -> ID n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip State n -> [Symbol e] -> ID n e
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 :: FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
fsa [Symbol e]
str = (Set (ID n e) -> Bool)
-> (Set (ID n e) -> Set (ID n e)) -> Set (ID n e) -> Set (ID n e)
forall a. (a -> Bool) -> (a -> a) -> a -> a
until ((ID n e -> Bool) -> Set (ID n e) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
allS ([Symbol e] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Symbol e] -> Bool) -> (ID n e -> [Symbol e]) -> ID n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ID n e -> [Symbol e]
forall n e. ID n e -> [Symbol e]
string)) (FSA n e -> Set (ID n e) -> Set (ID n e)
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 = (State n -> ID n e) -> Set (State n) -> Set (ID n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((State n -> [Symbol e] -> ID n e)
-> [Symbol e] -> State n -> ID n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip State n -> [Symbol e] -> ID n e
forall n e. State n -> [Symbol e] -> ID n e
ID [Symbol e]
str) Set (State n)
expandedInitials
>           expandedInitials :: Set (State n)
expandedInitials = FSA n e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure FSA n e
fsa (Set (State n) -> Set (State n)) -> Set (State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa

> accepts :: (Ord e, Ord n) => FSA n e -> [e] -> Bool
> accepts :: FSA n e -> [e] -> Bool
accepts FSA n e
fsa = (State n -> Bool) -> Set (State n) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa)) (Set (State n) -> Bool) -> ([e] -> Set (State n)) -> [e] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ID n e -> State n) -> Set (ID n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ID n e -> State n
forall n e. ID n e -> State n
state (Set (ID n e) -> Set (State n))
-> ([e] -> Set (ID n e)) -> [e] -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>               FSA n e -> [Symbol e] -> Set (ID n e)
forall e n. (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
fsa ([Symbol e] -> Set (ID n e))
-> ([e] -> [Symbol e]) -> [e] -> Set (ID n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (e -> Symbol e) -> [e] -> [Symbol e]
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap e -> Symbol e
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 :: [e] -> FSA n e -> FSA n e
brzozowskiDerivative [e]
xs FSA n e
f = FSA n e -> FSA n e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables
>                             (FSA n e -> FSA n e) -> FSA n e -> FSA n e
forall a b. (a -> b) -> a -> b
$ FSA n e
f { initials :: Set (State n)
initials = (ID n e -> State n) -> Set (ID n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ID n e -> State n
forall n e. ID n e -> State n
state (Set (ID n e) -> Set (State n))
-> ([Symbol e] -> Set (ID n e)) -> [Symbol e] -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> [Symbol e] -> Set (ID n e)
forall e n. (Ord e, Ord n) => FSA n e -> [Symbol e] -> Set (ID n e)
compute FSA n e
f
>                                              ([Symbol e] -> Set (State n)) -> [Symbol e] -> Set (State n)
forall a b. (a -> b) -> a -> b
$ (e -> Symbol e) -> [e] -> [Symbol e]
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap e -> Symbol e
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 :: 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' = FSA (Either n1 ()) e -> FSA (Either n1 ()) e
forall e. FSA (Either n1 ()) e -> FSA (Either n1 ()) e
x (FSA n1 e -> FSA () e -> FSA (Either n1 ()) e
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 -> FSA n1 e
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 = FSA (Either n1 ()) e -> Set (State (Either n1 ()))
forall n e. FSA n e -> Set (State n)
finals FSA (Either n1 ()) e
m Set (State (Either n1 ()))
-> Set (State (Either n1 ())) -> Set (State (Either n1 ()))
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` (Either n1 () -> State (Either n1 ()))
-> Set (Either n1 ()) -> Set (State (Either n1 ()))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Either n1 () -> State (Either n1 ())
forall n. n -> State n
State Set (Either n1 ())
f}
>           t :: FSA () e
t  = Set e -> FSA () e
forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet (FSA n1 e -> Set e
forall n e. FSA n e -> Set e
sigma FSA n1 e
a Set e -> Set e -> Set e
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` FSA n2 e -> Set e
forall n e. FSA n e -> Set e
sigma FSA n2 e
b)
>           p :: FSA (Maybe (Either n1 ()), Maybe n2) e
p  = FSA (Either n1 ()) e
-> FSA n2 e -> FSA (Maybe (Either n1 ()), Maybe n2) e
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' (FSA n2 e -> FSA n2 e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables FSA n2 e
b)
>           f :: Set (Either n1 ())
f  = (State n1 -> Either n1 ()) -> Set (State n1) -> Set (Either n1 ())
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (n1 -> Either n1 ()
forall a b. a -> Either a b
Left (n1 -> Either n1 ())
-> (State n1 -> n1) -> State n1 -> Either n1 ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n1 -> n1
forall n. State n -> n
nodeLabel) (Set (State n1) -> Set (Either n1 ()))
-> Set (State n1) -> Set (Either n1 ())
forall a b. (a -> b) -> a -> b
$ FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
finals FSA n1 e
a
>           i :: Set (State (Maybe (Either n1 ()), Maybe n2))
i  = (State (Maybe (Either n1 ()), Maybe n2) -> Bool)
-> Set (State (Maybe (Either n1 ()), Maybe n2))
-> Set (State (Maybe (Either n1 ()), Maybe n2))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ( Bool -> (Either n1 () -> Bool) -> Maybe (Either n1 ()) -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Either n1 () -> Set (Either n1 ()) -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set (Either n1 ())
f)
>                     (Maybe (Either n1 ()) -> Bool)
-> (State (Maybe (Either n1 ()), Maybe n2) -> Maybe (Either n1 ()))
-> State (Maybe (Either n1 ()), Maybe n2)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe (Either n1 ()), Maybe n2) -> Maybe (Either n1 ())
forall a b. (a, b) -> a
fst ((Maybe (Either n1 ()), Maybe n2) -> Maybe (Either n1 ()))
-> (State (Maybe (Either n1 ()), Maybe n2)
    -> (Maybe (Either n1 ()), Maybe n2))
-> State (Maybe (Either n1 ()), Maybe n2)
-> Maybe (Either n1 ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe (Either n1 ()), Maybe n2)
-> (Maybe (Either n1 ()), Maybe n2)
forall n. State n -> n
nodeLabel) (Set (State (Maybe (Either n1 ()), Maybe n2))
 -> Set (State (Maybe (Either n1 ()), Maybe n2)))
-> Set (State (Maybe (Either n1 ()), Maybe n2))
-> Set (State (Maybe (Either n1 ()), Maybe n2))
forall a b. (a -> b) -> a -> b
$ FSA (Maybe (Either n1 ()), Maybe n2) e
-> Set (State (Maybe (Either n1 ()), Maybe n2))
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  = FSA (Maybe (Either n1 ()), Maybe n2) e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA (Maybe (Either n1 ()), Maybe n2) e
p Bool -> Bool -> Bool
&& Set (State (Maybe (Either n1 ()), Maybe n2)) -> Int
forall a. Set a -> Int
Set.size Set (State (Maybe (Either n1 ()), Maybe n2))
i Int -> Int -> Bool
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 :: FSA n1 e -> FSA n2 e -> FSA Integer e
quotRight FSA n1 e
a FSA n2 e
b = FSA (Maybe (Either n2 ()), Maybe n1) e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize (FSA (Maybe (Either n2 ()), Maybe n1) e -> FSA Integer e)
-> (FSA (Maybe (Either n2 ()), Maybe n1) e
    -> FSA (Maybe (Either n2 ()), Maybe n1) e)
-> FSA (Maybe (Either n2 ()), Maybe n1) e
-> FSA Integer e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (Maybe (Either n2 ()), Maybe n1) e
-> FSA (Maybe (Either n2 ()), Maybe n1) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse
>                 (FSA (Maybe (Either n2 ()), Maybe n1) e -> FSA Integer e)
-> FSA (Maybe (Either n2 ()), Maybe n1) e -> FSA Integer e
forall a b. (a -> b) -> a -> b
$ FSA n2 e -> FSA n1 e -> FSA (Maybe (Either n2 ()), Maybe n1) e
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 n2 e -> FSA n2 e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse FSA n2 e
b) (FSA n1 e -> FSA n1 e
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 :: 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 = [FSA Integer e] -> FSA Integer e
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll ([FSA Integer e] -> FSA Integer e)
-> (Set (State Integer) -> [FSA Integer e])
-> Set (State Integer)
-> FSA Integer e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State Integer -> FSA Integer e)
-> [State Integer] -> [FSA Integer e]
forall a b. (a -> b) -> [a] -> [b]
map State Integer -> FSA Integer e
forall n1. (Ord n1, Enum n1) => State Integer -> FSA n1 e
bridge ([State Integer] -> [FSA Integer e])
-> (Set (State Integer) -> [State Integer])
-> Set (State Integer)
-> [FSA Integer e]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State Integer) -> [State Integer]
forall a. Set a -> [a]
Set.toList (Set (State Integer) -> FSA Integer e)
-> Set (State Integer) -> FSA Integer e
forall a b. (a -> b) -> a -> b
$ FSA Integer e -> Set (State Integer)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA Integer e
b'
>     where a' :: FSA Integer e
a' = FSA n1 e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n1 e
a
>           b' :: FSA Integer e
b' = FSA n2 e -> FSA Integer e
forall e n. (Ord e, Ord n) => FSA n e -> FSA Integer e
normalize FSA n2 e
b
>           c' :: FSA Integer e
c' = FSA n3 e -> FSA Integer e
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 = State Integer -> Set (State Integer)
forall a. a -> Set a
Set.singleton State Integer
n}
>                          b2 :: FSA Integer e
b2 = FSA Integer e
b' {finals :: Set (State Integer)
finals = State Integer -> Set (State Integer)
forall a. a -> Set a
Set.singleton State Integer
n}
>                      in (FSA (Either Integer (Maybe (Either Integer ()), Maybe Integer)) e
-> FSA n1 e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates
>                          (FSA Integer e -> FSA Integer e -> FSA Integer e
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
>                           FSA Integer e
-> FSA (Maybe (Either Integer ()), Maybe Integer) e
-> FSA
     (Either Integer (Maybe (Either Integer ()), Maybe Integer)) e
forall n1 n2 e.
(Ord n1, Ord n2, Ord e) =>
FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
`autConcatenation` FSA Integer e
-> FSA Integer e
-> FSA (Maybe (Either Integer ()), Maybe Integer) e
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 :: State a -> State b -> State (a, b)
combine State a
q1 State b
q2 = (,) (a -> b -> (a, b)) -> State a -> State (b -> (a, b))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> State a
q1 State (b -> (a, b)) -> State b -> State (a, b)
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 :: Set a -> Set b -> Set (a, b)
makePairs Set a
xs Set b
ys = (a -> Set (a, b) -> Set (a, b))
-> Set (a, b) -> Set a -> Set (a, b)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (a, b) -> Set (a, b) -> Set (a, b)
forall c a. Container c a => c -> c -> c
union (Set (a, b) -> Set (a, b) -> Set (a, b))
-> (a -> Set (a, b)) -> a -> Set (a, b) -> Set (a, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set (a, b)
forall a. a -> Set (a, b)
f) Set (a, b)
forall c a. Container c a => c
empty Set a
xs
>     where f :: a -> Set (a, b)
f a
x = (b -> (a, b)) -> Set b -> Set (a, b)
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 :: Set (State a)
-> Set (State b) -> Set (State (Maybe a), State (Maybe b))
makeJustPairs Set (State a)
xs Set (State b)
ys = Set (State (Maybe a))
-> Set (State (Maybe b)) -> Set (State (Maybe a), State (Maybe b))
forall a b. (Ord a, Ord b) => Set a -> Set b -> Set (a, b)
makePairs (Set (State a) -> Set (State (Maybe a))
forall a. Set (State a) -> Set (State (Maybe a))
justify Set (State a)
xs) (Set (State b) -> Set (State (Maybe b))
forall a. Set (State a) -> Set (State (Maybe a))
justify Set (State b)
ys)
>     where justify :: Set (State a) -> Set (State (Maybe a))
justify = (State a -> State (Maybe a))
-> Set (State a) -> Set (State (Maybe a))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((a -> Maybe a) -> State a -> State (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
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.

> cartesianConstruction :: (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)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
cartesianConstruction Bool -> Bool -> Bool
isFinal' FSA n1 e
f1 FSA n2 e
f2
>     = FSA :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
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  =  Set e -> Set e -> Set e
forall c a. Container c a => c -> c -> c
union (FSA n1 e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n1 e
f1) (FSA n2 e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n2 e
f2)
>           isDet :: Bool
isDet  =  FSA n1 e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n1 e
f1 Bool -> Bool -> Bool
&& FSA n2 e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n2 e
f2
>           qi :: Set (State (Maybe n1, Maybe n2))
qi     =  ((State (Maybe n1), State (Maybe n2))
 -> State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1), State (Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((State (Maybe n1)
 -> State (Maybe n2) -> State (Maybe n1, Maybe n2))
-> (State (Maybe n1), State (Maybe n2))
-> State (Maybe n1, Maybe n2)
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry State (Maybe n1) -> State (Maybe n2) -> State (Maybe n1, Maybe n2)
forall a b. State a -> State b -> State (a, b)
combine) (Set (State (Maybe n1), State (Maybe n2))
 -> Set (State (Maybe n1, Maybe n2)))
-> Set (State (Maybe n1), State (Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall a b. (a -> b) -> a -> b
$
>                     Set (State n1)
-> Set (State n2) -> Set (State (Maybe n1), State (Maybe n2))
forall a b.
(Ord a, Ord b) =>
Set (State a)
-> Set (State b) -> Set (State (Maybe a), State (Maybe b))
makeJustPairs (FSA n1 e -> Set (State n1)
forall n e. FSA n e -> Set (State n)
initials FSA n1 e
f1) (FSA n2 e -> Set (State n2)
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)  =  State (Maybe n1, Maybe n2) -> (Maybe n1, Maybe n2)
forall n. State n -> n
nodeLabel State (Maybe n1, Maybe n2)
q
>                      f :: FSA n e -> Maybe n -> Bool
f FSA n e
m    =  Bool -> (n -> Bool) -> Maybe n -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
m) (State n -> Bool) -> (n -> State n) -> n -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> State n
forall n. n -> State n
State)
>                  in Bool -> Bool -> Bool
isFinal' (FSA n1 e -> Maybe n1 -> Bool
forall n e. Ord n => FSA n e -> Maybe n -> Bool
f FSA n1 e
f1 Maybe n1
a) (FSA n2 e -> Maybe n2 -> Bool
forall n e. Ord n => FSA n e -> Maybe n -> 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)
>               = ((Set (State (Maybe n1, Maybe n2)),
  Set (State (Maybe n1, Maybe n2)),
  Set (Transition (Maybe n1, Maybe n2) e),
  Set (State (Maybe n1, Maybe n2)))
 -> Bool)
-> ((Set (State (Maybe n1, Maybe n2)),
     Set (State (Maybe n1, Maybe n2)),
     Set (Transition (Maybe n1, Maybe n2) e),
     Set (State (Maybe n1, Maybe n2)))
    -> (Set (State (Maybe n1, Maybe n2)),
        Set (State (Maybe n1, Maybe n2)),
        Set (Transition (Maybe n1, Maybe n2) e),
        Set (State (Maybe n1, Maybe n2))))
-> (Set (State (Maybe n1, Maybe n2)),
    Set (State (Maybe n1, Maybe n2)),
    Set (Transition (Maybe n1, Maybe n2) e),
    Set (State (Maybe n1, Maybe n2)))
-> (Set (State (Maybe n1, Maybe n2)),
    Set (State (Maybe n1, Maybe n2)),
    Set (Transition (Maybe n1, Maybe n2) e),
    Set (State (Maybe n1, Maybe n2)))
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))
_) -> Set (State (Maybe n1, Maybe n2)) -> Bool
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   =  (State (Maybe n1, Maybe n2)
 -> Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e))
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (State (Maybe n1, Maybe n2))
-> Set (Transition (Maybe n1, Maybe n2) e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
forall c a. Container c a => c -> c -> c
union (Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e))
-> (State (Maybe n1, Maybe n2)
    -> Set (Transition (Maybe n1, Maybe n2) e))
-> State (Maybe n1, Maybe n2)
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe n1, Maybe n2)
-> Set (Transition (Maybe n1, Maybe n2) e)
extensions)
>                                Set (Transition (Maybe n1, Maybe n2) e)
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))
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall c a. Container c a => c -> c -> c
union Set (State (Maybe n1, Maybe n2))
new Set (State (Maybe n1, Maybe n2))
prev
>                      dests :: Set (State (Maybe n1, Maybe n2))
dests  =  (Transition (Maybe n1, Maybe n2) e -> State (Maybe n1, Maybe n2))
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (State (Maybe n1, Maybe n2))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Transition (Maybe n1, Maybe n2) e -> State (Maybe n1, Maybe n2)
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'  =  (State (Maybe n1, Maybe n2) -> Bool)
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
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 ( Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
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)
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
forall c a. Container c a => c -> c -> c
union Set (Transition (Maybe n1, Maybe n2) e)
exts Set (Transition (Maybe n1, Maybe n2) e)
partial
>                     , Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall c a. Container c a => c -> c -> c
union Set (State (Maybe n1, Maybe n2))
fins Set (State (Maybe n1, Maybe n2))
fins'
>                     )
>                 )
>                 (Set (State (Maybe n1, Maybe n2))
qi, Set (State (Maybe n1, Maybe n2))
forall c a. Container c a => c
empty, Set (Transition (Maybe n1, Maybe n2) e)
forall c a. Container c a => c
empty, (State (Maybe n1, Maybe n2) -> Bool)
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
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 =  (Symbol e
 -> Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e))
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Symbol e)
-> Set (Transition (Maybe n1, Maybe n2) e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
forall c a. Container c a => c -> c -> c
union (Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e)
 -> Set (Transition (Maybe n1, Maybe n2) e))
-> (Symbol e -> Set (Transition (Maybe n1, Maybe n2) e))
-> Symbol e
-> Set (Transition (Maybe n1, Maybe n2) e)
-> Set (Transition (Maybe n1, Maybe n2) e)
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) Set (Transition (Maybe n1, Maybe n2) e)
forall c a. Container c a => c
empty (Set (Symbol e) -> Set (Transition (Maybe n1, Maybe n2) e))
-> Set (Symbol e) -> Set (Transition (Maybe n1, Maybe n2) e)
forall a b. (a -> b) -> a -> b
$
>                           (e -> Symbol e) -> Set e -> Set (Symbol e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic e -> Symbol e
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    =  (State (Maybe n1, Maybe n2) -> Transition (Maybe n1, Maybe n2) e)
-> Set (State (Maybe n1, Maybe n2))
-> Set (Transition (Maybe n1, Maybe n2) e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (Symbol e
-> State (Maybe n1, Maybe n2)
-> State (Maybe n1, Maybe n2)
-> Transition (Maybe n1, Maybe n2) e
forall n e. Symbol e -> State n -> State n -> Transition n e
Transition Symbol e
x State (Maybe n1, Maybe n2)
q) (Set (State (Maybe n1, Maybe n2))
 -> Set (Transition (Maybe n1, Maybe n2) e))
-> Set (State (Maybe n1, Maybe n2))
-> Set (Transition (Maybe n1, Maybe n2) e)
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   =  Symbol e -> FSA n1 e -> State (Maybe n1) -> Set (State (Maybe 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 (State (Maybe n1) -> Set (State (Maybe n1)))
-> State (Maybe n1) -> Set (State (Maybe n1))
forall a b. (a -> b) -> a -> b
$ ((Maybe n1, Maybe n2) -> Maybe n1)
-> State (Maybe n1, Maybe n2) -> State (Maybe n1)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe n1, Maybe n2) -> Maybe n1
forall a b. (a, b) -> a
fst State (Maybe n1, Maybe n2)
q
>                               n2 :: Set (State (Maybe n2))
n2   =  Symbol e -> FSA n2 e -> State (Maybe n2) -> Set (State (Maybe 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 (State (Maybe n2) -> Set (State (Maybe n2)))
-> State (Maybe n2) -> Set (State (Maybe n2))
forall a b. (a -> b) -> a -> b
$ ((Maybe n1, Maybe n2) -> Maybe n2)
-> State (Maybe n1, Maybe n2) -> State (Maybe n2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Maybe n1, Maybe n2) -> Maybe n2
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  =  (State (Maybe n2) -> State (a, Maybe n2))
-> Set (State (Maybe n2)) -> Set (State (a, Maybe n2))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (State a -> State (Maybe n2) -> State (a, Maybe n2)
forall a b. State a -> State b -> State (a, b)
combine State a
a) Set (State (Maybe n2))
n2
>                           in (State (Maybe n1)
 -> Set (State (Maybe n1, Maybe n2))
 -> Set (State (Maybe n1, Maybe n2)))
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1))
-> Set (State (Maybe n1, Maybe n2))
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall c a. Container c a => c -> c -> c
union (Set (State (Maybe n1, Maybe n2))
 -> Set (State (Maybe n1, Maybe n2))
 -> Set (State (Maybe n1, Maybe n2)))
-> (State (Maybe n1) -> Set (State (Maybe n1, Maybe n2)))
-> State (Maybe n1)
-> Set (State (Maybe n1, Maybe n2))
-> Set (State (Maybe n1, Maybe n2))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe n1) -> Set (State (Maybe n1, Maybe n2))
forall a. State a -> Set (State (a, Maybe n2))
f) Set (State (Maybe n1, Maybe n2))
forall c a. Container c a => c
empty Set (State (Maybe n1))
n1
>           nexts' :: Symbol e -> FSA a e -> State (Maybe a) -> Set (State (Maybe a))
nexts' Symbol e
x FSA a e
f   =  Set (State (Maybe a))
-> (a -> Set (State (Maybe a))) -> Maybe a -> Set (State (Maybe a))
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
>                           (State (Maybe a) -> Set (State (Maybe a))
forall c a. Container c a => a -> c
singleton (State (Maybe a) -> Set (State (Maybe a)))
-> State (Maybe a) -> Set (State (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> State (Maybe a)
forall n. n -> State n
State Maybe a
forall a. Maybe a
Nothing)
>                           (Symbol e -> FSA a e -> State a -> Set (State (Maybe a))
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 (State a -> Set (State (Maybe a)))
-> (a -> State a) -> a -> Set (State (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> State a
forall n. n -> State n
State) (Maybe a -> Set (State (Maybe a)))
-> (State (Maybe a) -> Maybe a)
-> State (Maybe a)
-> Set (State (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Maybe a) -> Maybe a
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
>               | Set (State a) -> Bool
forall c a. Container c a => c -> Bool
isEmpty Set (State a)
exts  =  State (Maybe a) -> Set (State (Maybe a))
forall c a. Container c a => a -> c
singleton (State (Maybe a) -> Set (State (Maybe a)))
-> State (Maybe a) -> Set (State (Maybe a))
forall a b. (a -> b) -> a -> b
$ Maybe a -> State (Maybe a)
forall n. n -> State n
State Maybe a
forall a. Maybe a
Nothing
>               | Bool
otherwise     =  (State a -> State (Maybe a))
-> Set (State a) -> Set (State (Maybe a))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((a -> Maybe a) -> State a -> State (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just) Set (State a)
exts
>               where exts :: Set (State a)
exts = FSA a e -> Symbol e -> Set (State a) -> Set (State a)
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 (Set (State a) -> Set (State a)) -> Set (State a) -> Set (State a)
forall a b. (a -> b) -> a -> b
$ State a -> Set (State a)
forall c a. Container c a => a -> c
singleton State a
q

> autIntersection :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>                    FSA (Maybe n1, Maybe n2) e
> autIntersection :: FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autIntersection = (Bool -> Bool -> Bool)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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 :: FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
autUnion = (Bool -> Bool -> Bool)
-> FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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).

> autDifference :: (Ord e, Ord n1, Ord n2) => FSA n1 e -> FSA n2 e ->
>                  FSA (Maybe n1, Maybe (Set n2)) e
> autDifference :: FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e
autDifference = ((FSA (Set n2) e -> FSA (Maybe n1, Maybe (Set n2)) e)
 -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e)
-> (FSA n1 e -> FSA (Set n2) e -> FSA (Maybe n1, Maybe (Set n2)) e)
-> FSA n1 e
-> FSA n2 e
-> FSA (Maybe n1, Maybe (Set n2)) e
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((FSA (Set n2) e -> FSA (Maybe n1, Maybe (Set n2)) e)
-> (FSA n2 e -> FSA (Set n2) e)
-> FSA n2 e
-> FSA (Maybe n1, Maybe (Set n2)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n2 e -> FSA (Set n2) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
complement) FSA n1 e -> FSA (Set n2) e -> FSA (Maybe n1, Maybe (Set n2)) e
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 :: 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
>     = FSA (Maybe n1, Maybe n2) e
-> FSA (Maybe n1, Maybe n2) e
-> FSA
     (Maybe (Maybe n1, Maybe n2), Maybe (Set (Maybe n1, Maybe n2))) e
forall e n1 n2.
(Ord e, Ord n1, Ord n2) =>
FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe (Set n2)) e
autDifference (FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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) (FSA (Maybe n1, Maybe n2) e
 -> FSA
      (Maybe (Maybe n1, Maybe n2), Maybe (Set (Maybe n1, Maybe n2))) e)
-> FSA (Maybe n1, Maybe n2) e
-> FSA
     (Maybe (Maybe n1, Maybe n2), Maybe (Set (Maybe n1, Maybe n2))) e
forall a b. (a -> b) -> a -> b
$ FSA n1 e -> FSA n2 e -> FSA (Maybe n1, Maybe n2) e
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 :: FSA n e -> FSA (Set n) e
complement = FSA (Set n) e -> FSA (Set n) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
complementDeterministic (FSA (Set n) e -> FSA (Set n) e)
-> (FSA n e -> FSA (Set n) e) -> FSA n e -> FSA (Set n) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA (Set n) e
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 :: FSA n e -> FSA n e
complementDeterministic FSA n e
f = FSA n e
f { finals :: Set (State n)
finals = Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
difference (FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
f) (FSA n e -> Set (State n)
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 :: FSA n e -> FSA n e -> FSA n e
residue = ((FSA n e, FSA n e) -> FSA n e) -> FSA n e -> FSA n e -> FSA n e
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (FSA (Set (Set n)) e -> FSA n e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates (FSA (Set (Set n)) e -> FSA n e)
-> ((FSA n e, FSA n e) -> FSA (Set (Set n)) e)
-> (FSA n e, FSA n e)
-> FSA n e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA (Set (Set n)) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize (FSA n e -> FSA (Set (Set n)) e)
-> ((FSA n e, FSA n e) -> FSA n e)
-> (FSA n e, FSA n e)
-> FSA (Set (Set n)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FSA n e -> FSA n e -> FSA n e) -> (FSA n e, FSA n e) -> FSA n e
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry FSA n e -> FSA n e -> FSA n e
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 :: FSA n e -> FSA n e -> FSA n e
coresidue FSA n e
a = FSA (Set (Set n)) e -> FSA n e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates (FSA (Set (Set n)) e -> FSA n e)
-> (FSA n e -> FSA (Set (Set n)) e) -> FSA n e -> FSA n e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA (Set (Set n)) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize (FSA n e -> FSA (Set (Set n)) e)
-> (FSA n e -> FSA n e) -> FSA n e -> FSA (Set (Set n)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>               FSA n e -> FSA n e -> FSA n e
forall c a. Container c a => c -> c -> c
union (FSA (Set n) e -> FSA n e
forall e n n1.
(Ord e, Ord n, Ord n1, Enum n1) =>
FSA n e -> FSA n1 e
renameStates (FSA (Set n) e -> FSA n e) -> FSA (Set n) e -> FSA n e
forall a b. (a -> b) -> a -> b
$ FSA n e -> FSA (Set n) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
complement FSA n e
a)

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

> autConcatenation :: (Ord n1, Ord n2, Ord e) =>
>                     FSA n1 e -> FSA n2 e
>                  -> FSA (Either n1 n2) e
> autConcatenation :: FSA n1 e -> FSA n2 e -> FSA (Either n1 n2) e
autConcatenation FSA n1 e
f1 FSA n2 e
f2
>     = FSA :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA
>       { sigma :: Set e
sigma = Set e -> Set e -> Set e
forall c a. Container c a => c -> c -> c
union (FSA (Either n1 n2) e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n1 n2) e
f1') (FSA (Either n1 n2) e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n1 n2) e
f2')
>       , transitions :: Set (Transition (Either n1 n2) e)
transitions
>           = [Set (Transition (Either n1 n2) e)]
-> Set (Transition (Either n1 n2) e)
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll
>             [ FSA (Either n1 n2) e -> Set (Transition (Either n1 n2) e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA (Either n1 n2) e
f1'
>             , FSA (Either n1 n2) e -> Set (Transition (Either n1 n2) e)
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 = FSA (Either n1 n2) e -> Set (State (Either n1 n2))
forall n e. FSA n e -> Set (State n)
initials FSA (Either n1 n2) e
f1'
>       , finals :: Set (State (Either n1 n2))
finals   = FSA (Either n1 n2) e -> Set (State (Either n1 n2))
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' = (n1 -> Either n1 n2) -> FSA n1 e -> FSA (Either n1 n2) e
forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic n1 -> Either n1 n2
forall a b. a -> Either a b
Left FSA n1 e
f1
>           f2' :: FSA (Either n1 n2) e
f2' = (n2 -> Either n1 n2) -> FSA n2 e -> FSA (Either n1 n2) e
forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic n2 -> Either n1 n2
forall a b. b -> Either a b
Right FSA n2 e
f2
>           combiningTransitions :: Set (Transition (Either n1 n2) e)
combiningTransitions = (State (Either n1 n2)
 -> Set (Transition (Either n1 n2) e)
 -> Set (Transition (Either n1 n2) e))
-> Set (Transition (Either n1 n2) e)
-> Set (State (Either n1 n2))
-> Set (Transition (Either n1 n2) e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (Transition (Either n1 n2) e)
-> Set (Transition (Either n1 n2) e)
-> Set (Transition (Either n1 n2) e)
forall c a. Container c a => c -> c -> c
union (Set (Transition (Either n1 n2) e)
 -> Set (Transition (Either n1 n2) e)
 -> Set (Transition (Either n1 n2) e))
-> (State (Either n1 n2) -> Set (Transition (Either n1 n2) e))
-> State (Either n1 n2)
-> Set (Transition (Either n1 n2) e)
-> Set (Transition (Either n1 n2) e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Either n1 n2) -> Set (Transition (Either n1 n2) e)
forall e. State (Either n1 n2) -> Set (Transition (Either n1 n2) e)
cts) Set (Transition (Either n1 n2) e)
forall c a. Container c a => c
empty
>                                  (FSA (Either n1 n2) e -> Set (State (Either n1 n2))
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 = (State (Either n1 n2) -> Transition (Either n1 n2) e)
-> Set (State (Either n1 n2)) -> Set (Transition (Either n1 n2) e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                   (\State (Either n1 n2)
i ->
>                    Transition :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                    { edgeLabel :: Symbol e
edgeLabel = Symbol e
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
>                    }
>                   )
>                   (FSA (Either n1 n2) e -> Set (State (Either n1 n2))
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 :: FSA n e -> FSA (Either n Bool) e
kleeneClosure FSA n e
f
>     = FSA :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA
>       { sigma :: Set e
sigma = FSA (Either n Bool) e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA (Either n Bool) e
f'
>       , transitions :: Set (Transition (Either n Bool) e)
transitions
>           = [Set (Transition (Either n Bool) e)]
-> Set (Transition (Either n Bool) e)
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll [ FSA (Either n Bool) e -> Set (Transition (Either n Bool) e)
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 = State (Either n Bool) -> Set (State (Either n Bool))
forall c a. Container c a => a -> c
singleton State (Either n Bool)
forall a. State (Either a Bool)
ni
>       , finals :: Set (State (Either n Bool))
finals = State (Either n Bool) -> Set (State (Either n Bool))
forall c a. Container c a => a -> c
singleton State (Either n Bool)
forall a. State (Either a Bool)
nf
>       , isDeterministic :: Bool
isDeterministic = Bool
False
>       }
>     where f' :: FSA (Either n Bool) e
f' = (n -> Either n Bool) -> FSA n e -> FSA (Either n Bool) e
forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic n -> Either n Bool
forall a b. a -> Either a b
Left FSA n e
f
>           ni :: State (Either a Bool)
ni = Either a Bool -> State (Either a Bool)
forall n. n -> State n
State (Bool -> Either a Bool
forall a b. b -> Either a b
Right Bool
False)
>           nf :: State (Either a Bool)
nf = Either a Bool -> State (Either a Bool)
forall n. n -> State n
State (Bool -> Either a Bool
forall a b. b -> Either a b
Right Bool
True)
>           toOldInitials :: Set (Transition (Either n Bool) e)
toOldInitials = (State (Either n Bool)
 -> Set (Transition (Either n Bool) e)
 -> Set (Transition (Either n Bool) e))
-> Set (Transition (Either n Bool) e)
-> Set (State (Either n Bool))
-> Set (Transition (Either n Bool) e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (Transition (Either n Bool) e)
-> Set (Transition (Either n Bool) e)
-> Set (Transition (Either n Bool) e)
forall c a. Container c a => c -> c -> c
union (Set (Transition (Either n Bool) e)
 -> Set (Transition (Either n Bool) e)
 -> Set (Transition (Either n Bool) e))
-> (State (Either n Bool) -> Set (Transition (Either n Bool) e))
-> State (Either n Bool)
-> Set (Transition (Either n Bool) e)
-> Set (Transition (Either n Bool) e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (Either n Bool) -> Set (Transition (Either n Bool) e)
forall e.
Ord e =>
State (Either n Bool) -> Set (Transition (Either n Bool) e)
cts) Set (Transition (Either n Bool) e)
forall c a. Container c a => c
empty
>                           (State (Either n Bool)
-> Set (State (Either n Bool)) -> Set (State (Either n Bool))
forall c a. Container c a => a -> c -> c
insert State (Either n Bool)
forall a. State (Either a Bool)
ni (FSA (Either n Bool) e -> Set (State (Either n Bool))
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 = (State (Either n Bool) -> Transition (Either n Bool) e)
-> Set (State (Either n Bool))
-> Set (Transition (Either n Bool) e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                   (\State (Either n Bool)
i ->
>                    Transition :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                    { edgeLabel :: Symbol e
edgeLabel = Symbol e
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
>                    }
>                   )
>                   (FSA (Either n Bool) e -> Set (State (Either n Bool))
forall n e. FSA n e -> Set (State n)
initials FSA (Either n Bool) e
f')
>           toNewFinal :: Set (Transition (Either n Bool) e)
toNewFinal = (State (Either n Bool) -> Transition (Either n Bool) e)
-> Set (State (Either n Bool))
-> Set (Transition (Either n Bool) e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                        (\State (Either n Bool)
q ->
>                         Transition :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                         { edgeLabel :: Symbol e
edgeLabel = Symbol e
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)
forall a. State (Either a Bool)
nf
>                         }
>                        )
>                        (State (Either n Bool)
-> Set (State (Either n Bool)) -> Set (State (Either n Bool))
forall c a. Container c a => a -> c -> c
insert State (Either n Bool)
forall a. State (Either a Bool)
ni (FSA (Either n Bool) e -> Set (State (Either n Bool))
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 :: FSA n e -> FSA (Set (Set n)) e
minimize = FSA (Set n) e -> FSA (Set (Set n)) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set n) e
minimizeDeterministic (FSA (Set n) e -> FSA (Set (Set n)) e)
-> (FSA n e -> FSA (Set n) e) -> FSA n e -> FSA (Set (Set n)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA (Set n) e
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 :: FSA n e -> FSA (Set n) e
minimizeDeterministic = FSA (Set n) e -> FSA (Set n) e
forall n e. FSA n e -> FSA n e
setD (FSA (Set n) e -> FSA (Set n) e)
-> (FSA n e -> FSA (Set n) e) -> FSA n e -> FSA (Set n) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FSA n e -> Set (Set (State n))) -> FSA n e -> FSA (Set n) e
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))
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 :: (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 :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA
>                      { sigma :: Set e
sigma = FSA n e -> Set e
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 = Set n -> State (Set n)
forall n. n -> State n
State (Set n -> State (Set n))
-> (Set (Set (State n)) -> Set n)
-> Set (Set (State n))
-> State (Set n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n -> n) -> Set (State n) -> Set n
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> n
forall n. State n -> n
nodeLabel (Set (State n) -> Set n)
-> (Set (Set (State n)) -> Set (State n))
-> Set (Set (State n))
-> Set n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (Set (State n)) -> Set (State n)
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll (Set (Set (State n)) -> State (Set n))
-> Set (Set (State n)) -> State (Set n)
forall a b. (a -> b) -> a -> b
$
>                       (Set (State n) -> Bool)
-> Set (Set (State n)) -> Set (Set (State n))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (State n -> Set (State n) -> Bool
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 = (State n -> State (Set n)) -> Set (State n) -> Set (State (Set n))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> State (Set n)
classOf (Set (State n) -> Set (State (Set n)))
-> Set (State n) -> Set (State (Set n))
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa
>           fin :: Set (State (Set n))
fin = (State n -> State (Set n)) -> Set (State n) -> Set (State (Set n))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> State (Set n)
classOf (Set (State n) -> Set (State (Set n)))
-> Set (State n) -> Set (State (Set n))
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa
>           trans :: Set (Transition (Set n) e)
trans = (Transition n e -> Transition (Set n) e)
-> Set (Transition n e) -> Set (Transition (Set n) e)
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 (Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
t)
>                    , destination :: State (Set n)
destination = State n -> State (Set n)
classOf (Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t)
>                    }
>                   ) (Set (Transition n e) -> Set (Transition (Set n) e))
-> Set (Transition n e) -> Set (Transition (Set n) e)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (Transition n e)
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 :: FSA n e -> Set (Set (State n))
nerode FSA n e
fsa = (State n -> Set (State n)) -> Set (State n) -> Set (Set (State n))
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 = FSA n e -> Set (State n)
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 = Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. Container c a => c -> c -> c
union Set (State n, State n)
i' (Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n) -> Set (State n, State n)
forall a b. (a -> b) -> a -> b
$ (State n -> (State n, State n))
-> Set (State n) -> Set (State n, State n)
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' = Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. (Container c a, Eq a) => c -> c -> c
difference (Set (State n) -> Set (State n, State n)
forall a. Ord a => Set a -> Set (a, a)
pairs Set (State n)
sts) (Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n) -> Set (State n, State n)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n, State n)
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 = [Set (State n)] -> Set (State n)
forall c a (s :: * -> *).
(Container c a, Collapsible s) =>
s c -> c
unionAll
>                       [ State n -> Set (State n)
forall c a. Container c a => a -> c
singleton State n
x
>                       , ((State n, State n) -> State n)
-> Set (State n, State n) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (State n, State n) -> State n
forall a b. (a, b) -> b
snd (Set (State n, State n) -> Set (State n))
-> Set (State n, State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ ((State n, State n) -> State n)
-> State n -> Set (State n, State n) -> Set (State n, State n)
forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic (State n, State n) -> State n
forall a b. (a, b) -> a
fst State n
x Set (State n, State n)
i
>                       , ((State n, State n) -> State n)
-> Set (State n, State n) -> Set (State n)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (State n, State n) -> State n
forall a b. (a, b) -> a
fst (Set (State n, State n) -> Set (State n))
-> Set (State n, State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ ((State n, State n) -> Bool)
-> Set (State n, State n) -> Set (State n, State n)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep ((State n -> State n -> Bool
forall a. Eq a => a -> a -> Bool
== State n
x) (State n -> Bool)
-> ((State n, State n) -> State n) -> (State n, State n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n, State n) -> State n
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 :: FSA n e -> Set (State n, State n)
distinguishedPairs FSA n e
fsa = (Set (State n, State n), Set (State n, State n))
-> Set (State n, State n)
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 = Set (State n) -> Set (State n, State n)
forall a. Ord a => Set a -> Set (a, a)
pairs (FSA n e -> Set (State n)
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
>               = (State n -> Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n)
-> Set (State n)
-> Set (State n, State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. Container c a => c -> c -> c
union (Set (State n, State n)
 -> Set (State n, State n) -> Set (State n, State n))
-> (State n -> Set (State n, State n))
-> State n
-> Set (State n, State n)
-> Set (State n, State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> State n -> Set (State n, State n)
forall a. Ord a => Set a -> a -> Set (a, a)
pairs' (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa)) Set (State n, State n)
forall c a. Container c a => c
empty (Set (State n) -> Set (State n, State n))
-> (Set (State n) -> Set (State n))
-> Set (State n)
-> Set (State n, State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                 Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
difference (FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa) (Set (State n) -> Set (State n, State n))
-> Set (State n) -> Set (State n, State n)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
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) = FSA n e -> Set (State n, State n) -> State n -> State n -> Bool
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 = ((Set (State n, State n), Set (State n, State n)) -> Bool)
-> ((Set (State n, State n), Set (State n, State n))
    -> (Set (State n, State n), Set (State n, State n)))
-> (Set (State n, State n), Set (State n, State n))
-> (Set (State n, State n), Set (State n, State n))
forall a. (a -> Bool) -> (a -> a) -> a -> a
until
>                    (\(Set (State n, State n)
x, Set (State n, State n)
y) -> Set (State n, State n) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State n, State n)
x Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n, State n) -> Integer
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)
_) ->
>                     ( Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. Container c a => c -> c -> c
union Set (State n, State n)
x (Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n) -> Set (State n, State n)
forall a b. (a -> b) -> a -> b
$
>                       ((State n, State n) -> Bool)
-> Set (State n, State n) -> Set (State n, State n)
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) (Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
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, Set (State n, State n)
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 :: 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
>     | Set (State n, State n) -> (State n, State n) -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n, State n)
knownDistinct (State n -> State n -> (State n, State n)
forall a. Ord a => a -> a -> (a, a)
makePair State n
p State n
q) = Bool
True
>     | Bool
otherwise = ((State n, State n) -> Bool) -> Set (State n, State n) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (Set (State n, State n) -> (State n, State n) -> Bool
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 = FSA n e -> Symbol e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
fsa (e -> Symbol e
forall e. e -> Symbol e
Symbol e
x) (State n -> Set (State n)
forall c a. Container c a => a -> c
singleton State n
s)
>           newPairs' :: e -> Set (State n, State n)
newPairs' e
a = (State n -> Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n)
-> Set (State n)
-> Set (State n, State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. Container c a => c -> c -> c
union (Set (State n, State n)
 -> Set (State n, State n) -> Set (State n, State n))
-> (State n -> Set (State n, State n))
-> State n
-> Set (State n, State n)
-> Set (State n, State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> State n -> Set (State n, State n)
forall a. Ord a => Set a -> a -> Set (a, a)
pairs' (State n -> e -> Set (State n)
destinations State n
q e
a))
>                         Set (State n, State n)
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 = (e -> Set (State n, State n) -> Set (State n, State n))
-> Set (State n, State n) -> Set e -> Set (State n, State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (State n, State n)
-> Set (State n, State n) -> Set (State n, State n)
forall c a. Container c a => c -> c -> c
union (Set (State n, State n)
 -> Set (State n, State n) -> Set (State n, State n))
-> (e -> Set (State n, State n))
-> e
-> Set (State n, State n)
-> Set (State n, State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Set (State n, State n)
newPairs') Set (State n, State n)
forall c a. Container c a => c
empty (FSA n e -> Set e
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 :: a -> a -> (a, a)
makePair a
a a
b = (a -> a -> a
forall a. Ord a => a -> a -> a
min a
a a
b, a -> a -> a
forall a. Ord a => a -> a -> a
max a
a a
b)

> pairs :: (Ord a) => Set a -> Set (a, a)
> pairs :: Set a -> Set (a, a)
pairs Set a
xs = (a -> Set (a, a) -> Set (a, a))
-> Set (a, a) -> Set a -> Set (a, a)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (a, a) -> Set (a, a) -> Set (a, a)
forall c a. Container c a => c -> c -> c
union (Set (a, a) -> Set (a, a) -> Set (a, a))
-> (a -> Set (a, a)) -> a -> Set (a, a) -> Set (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Set (a, a)
f) Set (a, a)
forall c a. Container c a => c
empty Set a
xs
>     where f :: a -> Set (a, a)
f a
x = (a -> (a, a)) -> Set a -> Set (a, a)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((,) a
x) (Set a -> Set (a, a))
-> ((Set a, Set a) -> Set a) -> (Set a, Set a) -> Set (a, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set a, Set a) -> Set a
forall a b. (a, b) -> b
snd ((Set a, Set a) -> Set (a, a)) -> (Set a, Set a) -> Set (a, a)
forall a b. (a -> b) -> a -> b
$ a -> Set a -> (Set a, Set a)
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' :: Set a -> a -> Set (a, a)
pairs' Set a
xs a
x = (a -> (a, a)) -> Set a -> Set (a, a)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (a -> a -> (a, a)
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 :: FSA n e -> FSA n e
trimUnreachables FSA n e
fsa = Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
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 (FSA n e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n e
fsa)
>     where alpha :: Set e
alpha  =  FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa
>           qi :: Set (State n)
qi     =  FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
fsa
>           fin :: Set (State n)
fin    =  Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
intersection Set (State n)
reachables (Set (State n) -> Set (State n)) -> Set (State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
fsa
>           trans :: Set (Transition n e)
trans  =  (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn Set (State n)
reachables (State n -> Bool)
-> (Transition n e -> State n) -> Transition n e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> State n
forall n e. Transition n e -> State n
source) (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e) -> Set (Transition n e)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (Transition n e)
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 Set (State n) -> Set (State n) -> Bool
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 = (State n -> ID n e) -> Set (State n) -> Set (ID n e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((State n -> [Symbol e] -> ID n e)
-> [Symbol e] -> State n -> ID n e
forall a b c. (a -> b -> c) -> b -> a -> c
flip State n -> [Symbol e] -> ID n e
forall n e. State n -> [Symbol e] -> ID n e
ID (Symbol e
a Symbol e -> [Symbol e] -> [Symbol e]
forall a. a -> [a] -> [a]
: [])) Set (State n)
qs
>                     next :: Set (State n)
next = (e -> Set (State n) -> Set (State n))
-> Set (State n) -> Set e -> Set (State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse
>                            (Set (State n) -> Set (State n) -> Set (State n)
forall c a. Container c a => c -> c -> c
union (Set (State n) -> Set (State n) -> Set (State n))
-> (e -> Set (State n)) -> e -> Set (State n) -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ID n e -> State n) -> Set (ID n e) -> Set (State n)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ID n e -> State n
forall n e. ID n e -> State n
state (Set (ID n e) -> Set (State n))
-> (e -> Set (ID n e)) -> e -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (ID n e) -> Set (ID n e)
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) -> Set (ID n e))
-> (e -> Set (ID n e)) -> e -> Set (ID n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                             Symbol e -> Set (ID n e)
forall e. Symbol e -> Set (ID n e)
initialIDs (Symbol e -> Set (ID n e)) -> (e -> Symbol e) -> e -> Set (ID n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Symbol e
forall e. e -> Symbol e
Symbol
>                            )
>                            Set (State n)
forall c a. Container c a => c
empty
>                            Set e
alpha
>                     newqs :: Set (State n)
newqs = Set (State n) -> Set (State n) -> Set (State n)
forall c a. Container c a => c -> c -> c
union Set (State n)
next 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 :: 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 = FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
f
>               , finals :: Set (State n)
finals = FSA n e -> Set (State n)
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 = Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t
>                                   , destination :: State n
destination = Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
t
>                                   }
>           reverseTransitions :: FSA n e -> Set (Transition n e)
reverseTransitions = (Transition n e -> Transition n e)
-> Set (Transition n e) -> Set (Transition n e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Transition n e -> Transition n e
forall n e. Transition n e -> Transition n e
reverseTransition (Set (Transition n e) -> Set (Transition n e))
-> (FSA n e -> Set (Transition n e))
-> FSA n e
-> Set (Transition n e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions

> trimFailStates :: (Ord e, Ord n) => FSA n e -> FSA n e
> trimFailStates :: FSA n e -> FSA n e
trimFailStates = FSA n e -> FSA n e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
LTK.FSA.reverse (FSA n e -> FSA n e) -> (FSA n e -> FSA n e) -> FSA n e -> FSA n e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables (FSA n e -> FSA n e) -> (FSA n e -> FSA n e) -> FSA n e -> FSA n e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
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 :: FSA n e -> FSA Integer e
normalize = FSA (Set (Set n)) e -> FSA Integer e
forall n e n. (Ord n, Ord e, Ord n, Enum n) => FSA n e -> FSA n e
f (FSA (Set (Set n)) e -> FSA Integer e)
-> (FSA n e -> FSA (Set (Set n)) e) -> FSA n e -> FSA Integer e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (Set (Set n)) e -> FSA (Set (Set n)) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimFailStates (FSA (Set (Set n)) e -> FSA (Set (Set n)) e)
-> (FSA n e -> FSA (Set (Set n)) e)
-> FSA n e
-> FSA (Set (Set n)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA (Set (Set n)) e
forall e n. (Ord e, Ord n) => FSA n e -> FSA (Set (Set n)) e
minimize (FSA n e -> FSA (Set (Set n)) e)
-> (FSA n e -> FSA n e) -> FSA n e -> FSA (Set (Set n)) e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> FSA n e
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
>               | Set (State n) -> Bool
forall c a. Container c a => c -> Bool
isEmpty (FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
fsa) = FSA n e -> FSA n e
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
complementDeterministic (FSA n e -> FSA n e) -> FSA n e -> FSA n e
forall a b. (a -> b) -> a -> b
$
>                                        Set e -> FSA n e
forall e n. (Ord e, Enum n, Ord n) => Set e -> FSA n e
totalWithAlphabet (FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa)
>               | Bool
otherwise            = FSA n e -> FSA n e
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 :: FSA ([Maybe n], [Symbol e]) e
-> Set (Set (State ([Maybe n], [Symbol e])))
jEquivalence FSA ([Maybe n], [Symbol e]) e
f = (State ([Maybe n], [Symbol e])
 -> Set (State ([Maybe n], [Symbol e])))
-> Set (State ([Maybe n], [Symbol e]))
-> Set (Set (State ([Maybe n], [Symbol e])))
forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy (FSA ([Maybe n], [Symbol e]) e
-> State ([Maybe n], [Symbol e])
-> Set (State ([Maybe n], [Symbol e]))
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) (FSA ([Maybe n], [Symbol e]) e
-> Set (State ([Maybe n], [Symbol e]))
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 :: 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 = (State (n, [Symbol e])
 -> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse
>                       (Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e]))
forall c a. Container c a => c -> c -> c
union (Set (State (n, [Symbol e]))
 -> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> (State (n, [Symbol e]) -> Set (State (n, [Symbol e])))
-> State (n, [Symbol e])
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (n, [Symbol e]) e
-> [Symbol e]
-> State (n, [Symbol e])
-> Set (State (n, [Symbol e]))
forall n e.
(Ord n, Ord e) =>
FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA (n, [Symbol e]) e
f ((n, [Symbol e]) -> [Symbol e]
forall a b. (a, b) -> b
snd ((n, [Symbol e]) -> [Symbol e]) -> (n, [Symbol e]) -> [Symbol e]
forall a b. (a -> b) -> a -> b
$ State (n, [Symbol e]) -> (n, [Symbol e])
forall n. State n -> n
nodeLabel State (n, [Symbol e])
x))
>                       Set (State (n, [Symbol e]))
forall c a. Container c a => c
empty (Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e]))
forall a b. (a -> b) -> a -> b
$
>                       FSA (n, [Symbol e]) e -> Set (State (n, [Symbol e]))
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 :: FSA n e -> [Symbol e] -> State n -> Set (State n)
follow FSA n e
f [Symbol e]
xs State n
q = (Symbol e
 -> (Set (State n) -> Set (State n))
 -> Set (State n)
 -> Set (State n))
-> (Set (State n) -> Set (State n))
-> [Symbol e]
-> Set (State n)
-> Set (State n)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (((Set (State n) -> Set (State n))
 -> (Set (State n) -> Set (State n))
 -> Set (State n)
 -> Set (State n))
-> (Set (State n) -> Set (State n))
-> (Set (State n) -> Set (State n))
-> Set (State n)
-> Set (State n)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Set (State n) -> Set (State n))
-> (Set (State n) -> Set (State n))
-> Set (State n)
-> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ((Set (State n) -> Set (State n))
 -> (Set (State n) -> Set (State n))
 -> Set (State n)
 -> Set (State n))
-> (Symbol e -> Set (State n) -> Set (State n))
-> Symbol e
-> (Set (State n) -> Set (State n))
-> Set (State n)
-> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Symbol e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f) Set (State n) -> Set (State n)
forall a. a -> a
id [Symbol e]
xs (Set (State n) -> Set (State n)) -> Set (State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ State n -> Set (State n)
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 :: FSA n e -> FSA n ()
ignoreSymbols FSA n e
f = FSA n e
f { sigma :: Set ()
sigma = Set ()
forall c a. Container c a => c
empty
>                     , transitions :: Set (Transition n ())
transitions = (Transition n e -> Transition n ())
-> Set (Transition n e) -> Set (Transition n ())
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Transition n e -> Transition n ()
forall n e e. Transition n e -> Transition n e
x (FSA n e -> Set (Transition n e)
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 = Symbol e
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 :: FSA n e -> State n -> Set (State n)
primitiveIdealR FSA n e
f State n
x = FSA n () -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Set (State n) -> Set (State n)
epsilonClosure (FSA n e -> FSA n ()
forall n e. (Ord n, Ord e) => FSA n e -> FSA n ()
ignoreSymbols FSA n e
f) (Set (State n) -> Set (State n)) -> Set (State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ State n -> Set (State n)
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 :: FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
primitiveIdeal2 FSA (n, [Symbol e]) e
f = (State (n, [Symbol e])
 -> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e]))
forall c a. Container c a => c -> c -> c
union (Set (State (n, [Symbol e]))
 -> Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> (State (n, [Symbol e]) -> Set (State (n, [Symbol e])))
-> State (n, [Symbol e])
-> Set (State (n, [Symbol e]))
-> Set (State (n, [Symbol e]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
forall n e. (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
primitiveIdealR FSA (n, [Symbol e]) e
f) Set (State (n, [Symbol e]))
forall c a. Container c a => c
empty (Set (State (n, [Symbol e])) -> Set (State (n, [Symbol e])))
-> (State (n, [Symbol e]) -> Set (State (n, [Symbol e])))
-> State (n, [Symbol e])
-> Set (State (n, [Symbol e]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                     FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
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 :: (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
trivialUnder FSA n e -> Set (Set (State n))
f = (Set (State n) -> Bool) -> Set (Set (State n)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all ((Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
1) (Integer -> Bool)
-> (Set (State n) -> Integer) -> Set (State n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize) (Set (Set (State n)) -> Bool)
-> (FSA n e -> Set (Set (State n))) -> FSA n e -> Bool
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 :: FSA (n, [Symbol e]) e -> Set (Set (State (n, [Symbol e])))
hEquivalence FSA (n, [Symbol e]) e
f = (State (n, [Symbol e]) -> Set (State (n, [Symbol e])))
-> Set (Set (State (n, [Symbol e])))
-> Set (Set (State (n, [Symbol e])))
forall a n.
(Ord a, Ord n) =>
(n -> a) -> Set (Set n) -> Set (Set n)
refinePartitionBy (FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
forall n e. (Ord n, Ord e) => FSA n e -> State n -> Set (State n)
primitiveIdealR FSA (n, [Symbol e]) e
f) (Set (Set (State (n, [Symbol e])))
 -> Set (Set (State (n, [Symbol e]))))
-> (Set (State (n, [Symbol e]))
    -> Set (Set (State (n, [Symbol e]))))
-> Set (State (n, [Symbol e]))
-> Set (Set (State (n, [Symbol e])))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                  (State (n, [Symbol e]) -> Set (State (n, [Symbol e])))
-> Set (State (n, [Symbol e])) -> Set (Set (State (n, [Symbol e])))
forall a n. (Ord a, Ord n) => (n -> a) -> Set n -> Set (Set n)
partitionBy (FSA (n, [Symbol e]) e
-> State (n, [Symbol e]) -> Set (State (n, [Symbol e]))
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) (Set (State (n, [Symbol e])) -> Set (Set (State (n, [Symbol e]))))
-> Set (State (n, [Symbol e])) -> Set (Set (State (n, [Symbol e])))
forall a b. (a -> b) -> a -> b
$ FSA (n, [Symbol e]) e -> Set (State (n, [Symbol e]))
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 :: Set (State n) -> State (Set n)
metaFlip = Set n -> State (Set n)
forall n. n -> State n
State (Set n -> State (Set n))
-> (Set (State n) -> Set n) -> Set (State n) -> State (Set n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n -> n) -> Set (State n) -> Set n
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic State n -> n
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 :: 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 = Set e
-> Set (Transition (Set n) e)
-> Set (State (Set n))
-> Set (State (Set n))
-> Bool
-> FSA (Set n) e
forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA (FSA n e -> Set e
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 = State (Set n) -> Set (State (Set n))
forall c a. Container c a => a -> c
singleton (Set (State n) -> State (Set n)
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, FSA n e -> Symbol e -> Set (State n) -> Set (State n)
forall e n.
(Ord e, Ord n) =>
FSA n e -> Symbol e -> Set (State n) -> Set (State n)
delta FSA n e
f (e -> Symbol e
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
>               = (e -> (e, Set (State n), Set (State n)))
-> Set e -> Set (e, Set (State n), Set (State n))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (\e
a -> e -> Set (State n) -> (e, Set (State n), Set (State n))
buildTransition e
a Set (State n)
q) (Set e -> Set (e, Set (State n), Set (State n)))
-> Set e -> Set (e, Set (State n), Set (State n))
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set e
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 = (Set (State n)
 -> Set (e, Set (State n), Set (State n))
 -> Set (e, Set (State n), Set (State n)))
-> Set (e, Set (State n), Set (State n))
-> Set (Set (State n))
-> Set (e, Set (State n), Set (State n))
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (e, Set (State n), Set (State n))
-> Set (e, Set (State n), Set (State n))
-> Set (e, Set (State n), Set (State n))
forall c a. Container c a => c -> c -> c
union (Set (e, Set (State n), Set (State n))
 -> Set (e, Set (State n), Set (State n))
 -> Set (e, Set (State n), Set (State n)))
-> (Set (State n) -> Set (e, Set (State n), Set (State n)))
-> Set (State n)
-> Set (e, Set (State n), Set (State n))
-> Set (e, Set (State n), Set (State n))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> Set (e, Set (State n), Set (State n))
buildTransitions') Set (e, Set (State n), Set (State n))
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))
_)
>               = ((Set (e, Set (State n), Set (State n)), Set (Set (State n)),
  Set (Set (State n)))
 -> Bool)
-> ((Set (e, Set (State n), Set (State n)), Set (Set (State n)),
     Set (Set (State n)))
    -> (Set (e, Set (State n), Set (State n)), Set (Set (State n)),
        Set (Set (State n))))
-> (Set (e, Set (State n), Set (State n)), Set (Set (State n)),
    Set (Set (State n)))
-> (Set (e, Set (State n), Set (State n)), Set (Set (State n)),
    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) -> Set (Set (State n)) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (Set (State n))
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (Set (State n)) -> Integer
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 (Set (Set (State n)) -> Set (Set (State n)) -> Set (Set (State n))
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))
-> Set (e, Set (State n), Set (State n))
-> Set (e, Set (State n), Set (State n))
forall c a. Container c a => c -> c -> c
union Set (e, Set (State n), Set (State n))
a Set (e, Set (State n), Set (State n))
d
>                     , Set (Set (State n))
c
>                     , Set (Set (State n)) -> Set (Set (State n)) -> Set (Set (State n))
forall c a. Container c a => c -> c -> c
union Set (Set (State n))
c (Set (Set (State n)) -> Set (Set (State n)))
-> Set (Set (State n)) -> Set (Set (State n))
forall a b. (a -> b) -> a -> b
$ ((e, Set (State n), Set (State n)) -> Set (State n))
-> Set (e, Set (State n), Set (State n)) -> Set (Set (State n))
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
>                     )
>                 )
>                 (Set (e, Set (State n), Set (State n))
forall c a. Container c a => c
empty, Set (Set (State n))
forall c a. Container c a => c
empty, Set (State n) -> Set (Set (State n))
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 :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                 { edgeLabel :: Symbol e
edgeLabel = e -> Symbol e
forall e. e -> Symbol e
Symbol e
a
>                 , source :: State (Set n)
source = Set (State n) -> State (Set n)
forall n. Ord n => Set (State n) -> State (Set n)
metaFlip Set (State n)
b
>                 , destination :: State (Set n)
destination = Set (State n) -> State (Set n)
forall n. Ord n => Set (State n) -> State (Set n)
metaFlip Set (State n)
c
>                 }
>           trans :: Set (Transition (Set n) e)
trans = ((e, Set (State n), Set (State n)) -> Transition (Set n) e)
-> Set (e, Set (State n), Set (State n))
-> Set (Transition (Set n) e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic (e, Set (State n), Set (State n)) -> Transition (Set n) e
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 = (Set (State n) -> State (Set n))
-> Set (Set (State n)) -> Set (State (Set n))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic Set (State n) -> State (Set n)
forall n. Ord n => Set (State n) -> State (Set n)
metaFlip (Set (Set (State n)) -> Set (State (Set n)))
-> Set (Set (State n)) -> Set (State (Set n))
forall a b. (a -> b) -> a -> b
$ (Set (State n) -> Bool)
-> Set (Set (State n)) -> Set (Set (State n))
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 :: FSA n e -> FSA (Set n) e
determinize FSA n e
f
>     | FSA n e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n e
f = (n -> Set n) -> FSA n e -> FSA (Set n) e
forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic n -> Set n
forall c a. Container c a => a -> c
singleton FSA n e
f
>     | Bool
otherwise = FSA n e
-> Set (State n) -> (Set (State n) -> Bool) -> FSA (Set n) e
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 (FSA n e -> Set (State n)
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 = (State n -> Bool) -> Set (State n) -> Bool
forall (s :: * -> *) a. Collapsible s => (a -> Bool) -> s a -> Bool
anyS (Set (State n) -> State n -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
f)) (Set (State n) -> Bool)
-> (Set (State n) -> Set (State n)) -> Set (State n) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Set (State n) -> Set (State n)
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 :: FSA n e -> FSA (Set n) e
powersetGraph FSA n e
f = FSA n e
-> Set (State n) -> (Set (State n) -> Bool) -> FSA (Set n) e
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 (FSA n e -> Set (State n)
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 = Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
intersection (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
f) Set (State n)
qs Set (State n) -> Set (State n) -> Bool
forall a. Eq a => a -> a -> Bool
/= Set (State n)
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 :: FSA n e -> FSA ([Maybe n], [Symbol e]) e
syntacticMonoid FSA n e
m = FSA :: forall n e.
Set e
-> Set (Transition n e)
-> Set (State n)
-> Set (State n)
-> Bool
-> FSA n e
FSA { sigma :: Set e
sigma = FSA n e -> Set e
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   =  State ([Maybe n], [Symbol e])
-> Set (State ([Maybe n], [Symbol e]))
forall c a. Container c a => a -> c
singleton (State ([Maybe n], [Symbol e])
 -> Set (State ([Maybe n], [Symbol e])))
-> ([State n] -> State ([Maybe n], [Symbol e]))
-> [State n]
-> Set (State ([Maybe n], [Symbol e]))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Maybe n] -> ([Maybe n], [Symbol e]))
-> State [Maybe n] -> State ([Maybe n], [Symbol e])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Maybe n] -> [Symbol e] -> ([Maybe n], [Symbol e]))
-> [Symbol e] -> [Maybe n] -> ([Maybe n], [Symbol e])
forall a b c. (a -> b -> c) -> b -> a -> c
flip (,) [])  (State [Maybe n] -> State ([Maybe n], [Symbol e]))
-> ([State n] -> State [Maybe n])
-> [State n]
-> State ([Maybe n], [Symbol e])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                  [State (Maybe n)] -> State [Maybe n]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([State (Maybe n)] -> State [Maybe n])
-> ([State n] -> [State (Maybe n)]) -> [State n] -> State [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n -> State (Maybe n)) -> [State n] -> [State (Maybe n)]
forall a b. (a -> b) -> [a] -> [b]
map ((n -> Maybe n) -> State n -> State (Maybe n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> Maybe n
forall a. a -> Maybe a
Just) ([State n] -> Set (State ([Maybe n], [Symbol e])))
-> [State n] -> Set (State ([Maybe n], [Symbol e]))
forall a b. (a -> b) -> a -> b
$ [State n]
s
>           s :: [State n]
s   =  Set (State n) -> [State n]
forall a. Set a -> [a]
Set.toList (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
m) [State n] -> [State n] -> [State n]
forall a. [a] -> [a] -> [a]
++
>                  Set (State n) -> [State n]
forall a. Set a -> [a]
Set.toList (Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
difference (FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
m) (Set (State n) -> Set (State n)) -> Set (State n) -> Set (State n)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
m)
>           n :: Int
n   =  Set (State n) -> Int
forall (c :: * -> *) a b. (Collapsible c, Integral a) => c b -> a
size (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
m)
>           i' :: Set (State ([Maybe n], [Symbol e]))
i'  =  if Set (State n) -> Set (State n) -> Set (State n)
forall c a. (Container c a, Eq a) => c -> c -> c
intersection (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
m) (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
m) Set (State n) -> Set (State n) -> Bool
forall a. Eq a => a -> a -> Bool
/= Set (State n)
forall c a. Container c a => c
empty
>                  then Set (State ([Maybe n], [Symbol e]))
i
>                  else Set (State ([Maybe n], [Symbol e]))
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]))
_)
>               = 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])))
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 (Set (Transition ([Maybe n], [Symbol e]) e)
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' :: 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)
>     | Set (State ([Maybe n], [Symbol e])) -> Bool
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  =  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])))
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)
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
forall c a. Container c a => c -> c -> c
union Set (Transition ([Maybe n], [Symbol e]) e)
nt Set (Transition ([Maybe n], [Symbol e]) e)
ot, Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall c a. Container c a => c -> c -> c
union Set (State ([Maybe n], [Symbol e]))
ns Set (State ([Maybe n], [Symbol e]))
os, Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall c a. Container c a => c -> c -> c
union Set (State ([Maybe n], [Symbol e]))
nf Set (State ([Maybe n], [Symbol e]))
ofi, Set (State ([Maybe n], [Symbol e]))
ns)
>           alpha :: Set e
alpha     =  FSA n e -> Set e
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  =  Set (State ([Maybe n], [Symbol e]))
-> Transition ([Maybe n], [Symbol e]) e
-> Transition ([Maybe n], [Symbol e]) e
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]))
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall c a. Container c a => c -> c -> c
union Set (State ([Maybe n], [Symbol e]))
s Set (State ([Maybe n], [Symbol e]))
os) (Transition ([Maybe n], [Symbol e]) e
 -> Transition ([Maybe n], [Symbol e]) e)
-> Transition ([Maybe n], [Symbol e]) e
-> Transition ([Maybe n], [Symbol e]) e
forall a b. (a -> b) -> a -> b
$
>                        Transition :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                        { edgeLabel :: Symbol e
edgeLabel = e -> Symbol e
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 = Symbol e
-> State ([Maybe n], [Symbol e]) -> State ([Maybe n], [Symbol e])
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' (e -> Symbol e
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
>               = ((s b1, [Symbol e]) -> (s b1, [Symbol e]))
-> f (s b1, [Symbol e]) -> f (s b1, [Symbol e])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (([Symbol e] -> [Symbol e])
-> (s b1, [Symbol e]) -> (s b1, [Symbol e])
forall b c a. (b -> c) -> (a, b) -> (a, c)
mapsnd ([Symbol e] -> [Symbol e] -> [Symbol e]
forall a. [a] -> [a] -> [a]
++ [Symbol e
a])) (f (s b1, [Symbol e]) -> f (s b1, [Symbol e]))
-> (f (s (Maybe n), [Symbol e]) -> f (s b1, [Symbol e]))
-> f (s (Maybe n), [Symbol e])
-> f (s b1, [Symbol e])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                 ((s (Maybe n), [Symbol e]) -> (s b1, [Symbol e]))
-> f (s (Maybe n), [Symbol e]) -> f (s b1, [Symbol e])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
>                 ((s (Maybe n) -> s b1)
-> (s (Maybe n), [Symbol e]) -> (s b1, [Symbol e])
forall a b c. (a -> b) -> (a, c) -> (b, c)
mapfst ((s (Maybe n) -> s b1)
 -> (s (Maybe n), [Symbol e]) -> (s b1, [Symbol e]))
-> (s (Maybe n) -> s b1)
-> (s (Maybe n), [Symbol e])
-> (s b1, [Symbol e])
forall a b. (a -> b) -> a -> b
$
>                  (Maybe n -> Maybe n) -> s (Maybe n) -> s b1
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap
>                  (Maybe n -> (n -> Maybe n) -> Maybe n -> Maybe n
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Maybe n
forall a. Maybe a
Nothing ((n -> Maybe n) -> Maybe n -> Maybe n)
-> (n -> Maybe n) -> Maybe n -> Maybe n
forall a b. (a -> b) -> a -> b
$ Set (State n) -> Maybe n
forall (l :: * -> *) a a.
(Eq (l (State a)), Container (l (State a)) a, Linearizable l) =>
l (State a) -> Maybe a
pull (Set (State n) -> Maybe n) -> (n -> Set (State n)) -> n -> Maybe n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. FSA n e -> Symbol e -> Set (State n) -> Set (State n)
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 (Set (State n) -> Set (State n))
-> (n -> Set (State n)) -> n -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State n -> Set (State n)
forall c a. Container c a => a -> c
singleton (State n -> Set (State n)) -> (n -> State n) -> n -> Set (State n)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. n -> State n
forall n. n -> State n
State)
>                 )
>           pull :: l (State a) -> Maybe a
pull l (State a)
xs   =  if l (State a)
xs l (State a) -> l (State a) -> Bool
forall a. Eq a => a -> a -> Bool
== l (State a)
forall c a. Container c a => c
empty
>                        then Maybe a
forall a. Maybe a
Nothing
>                        else State (Maybe a) -> Maybe a
forall n. State n -> n
nodeLabel (State (Maybe a) -> Maybe a) -> State (Maybe a) -> Maybe a
forall a b. (a -> b) -> a -> b
$ (a -> Maybe a) -> State a -> State (Maybe a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> Maybe a
forall a. a -> Maybe a
Just (l (State a) -> State a
forall (l :: * -> *) a. Linearizable l => l a -> a
chooseOne l (State a)
xs)
>           nt :: Set (Transition ([Maybe n], [Symbol e]) e)
nt        =  Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
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 (Set (Transition ([Maybe n], [Symbol e]) e)
 -> Set (Transition ([Maybe n], [Symbol e]) e))
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
forall a b. (a -> b) -> a -> b
$
>                        (e
 -> Set (Transition ([Maybe n], [Symbol e]) e)
 -> Set (Transition ([Maybe n], [Symbol e]) e))
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set e
-> Set (Transition ([Maybe n], [Symbol e]) e)
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse (Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
forall c a. Container c a => c -> c -> c
union (Set (Transition ([Maybe n], [Symbol e]) e)
 -> Set (Transition ([Maybe n], [Symbol e]) e)
 -> Set (Transition ([Maybe n], [Symbol e]) e))
-> (e -> Set (Transition ([Maybe n], [Symbol e]) e))
-> e
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (Transition ([Maybe n], [Symbol e]) e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. e -> Set (Transition ([Maybe n], [Symbol e]) e)
nt') Set (Transition ([Maybe n], [Symbol e]) e)
forall c a. Container c a => c
empty Set e
alpha
>           nt' :: e -> Set (Transition ([Maybe n], [Symbol e]) e)
nt' e
a     =  (State ([Maybe n], [Symbol e])
 -> Transition ([Maybe n], [Symbol e]) e)
-> Set (State ([Maybe n], [Symbol e]))
-> Set (Transition ([Maybe n], [Symbol e]) e)
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        =  (State ([Maybe n], [Symbol e]) -> Bool)
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (Set (State [Maybe n]) -> State [Maybe n] -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isNotIn Set (State [Maybe n])
os' (State [Maybe n] -> Bool)
-> (State ([Maybe n], [Symbol e]) -> State [Maybe n])
-> State ([Maybe n], [Symbol e])
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (([Maybe n], [Symbol e]) -> [Maybe n])
-> State ([Maybe n], [Symbol e]) -> State [Maybe n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Maybe n], [Symbol e]) -> [Maybe n]
forall a b. (a, b) -> a
fst) (Set (State ([Maybe n], [Symbol e]))
 -> Set (State ([Maybe n], [Symbol e])))
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall a b. (a -> b) -> a -> b
$
>                        (Transition ([Maybe n], [Symbol e]) e
 -> State ([Maybe n], [Symbol e]))
-> Set (Transition ([Maybe n], [Symbol e]) e)
-> Set (State ([Maybe n], [Symbol e]))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap Transition ([Maybe n], [Symbol e]) e
-> State ([Maybe n], [Symbol e])
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        =  (State ([Maybe n], [Symbol e]) -> Bool)
-> Set (State ([Maybe n], [Symbol e]))
-> Set (State ([Maybe n], [Symbol e]))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep State ([Maybe n], [Symbol e]) -> Bool
forall b. State ([Maybe n], b) -> Bool
hasFinal Set (State ([Maybe n], [Symbol e]))
ns
>           os' :: Set (State [Maybe n])
os'       =  (State ([Maybe n], [Symbol e]) -> State [Maybe n])
-> Set (State ([Maybe n], [Symbol e])) -> Set (State [Maybe n])
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((([Maybe n], [Symbol e]) -> [Maybe n])
-> State ([Maybe n], [Symbol e]) -> State [Maybe n]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Maybe n], [Symbol e]) -> [Maybe n]
forall a b. (a, b) -> a
fst) Set (State ([Maybe n], [Symbol e]))
os
>           fins :: [Maybe n]
fins      =  State [Maybe n] -> [Maybe n]
forall n. State n -> n
nodeLabel (State [Maybe n] -> [Maybe n])
-> (Set (State n) -> State [Maybe n]) -> Set (State n) -> [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [State (Maybe n)] -> State [Maybe n]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence ([State (Maybe n)] -> State [Maybe n])
-> (Set (State n) -> [State (Maybe n)])
-> Set (State n)
-> State [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (State n -> State (Maybe n)) -> [State n] -> [State (Maybe n)]
forall a b. (a -> b) -> [a] -> [b]
map ((n -> Maybe n) -> State n -> State (Maybe n)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> Maybe n
forall a. a -> Maybe a
Just) ([State n] -> [State (Maybe n)])
-> (Set (State n) -> [State n])
-> Set (State n)
-> [State (Maybe n)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                        Set (State n) -> [State n]
forall a. Set a -> [a]
Set.toList (Set (State n) -> [Maybe n]) -> Set (State n) -> [Maybe n]
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
f
>           hasFinal :: State ([Maybe n], b) -> Bool
hasFinal  =  Bool -> Bool
not (Bool -> Bool)
-> (State ([Maybe n], b) -> Bool) -> State ([Maybe n], b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe n] -> Bool
forall c a. Container c a => c -> Bool
isEmpty ([Maybe n] -> Bool)
-> (State ([Maybe n], b) -> [Maybe n])
-> State ([Maybe n], b)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe n] -> [Maybe n] -> [Maybe n]
forall c a. (Container c a, Eq a) => c -> c -> c
intersection [Maybe n]
fins ([Maybe n] -> [Maybe n])
-> (State ([Maybe n], b) -> [Maybe n])
-> State ([Maybe n], b)
-> [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                        Int -> [Maybe n] -> [Maybe n]
forall a. Int -> [a] -> [a]
take Int
n ([Maybe n] -> [Maybe n])
-> (State ([Maybe n], b) -> [Maybe n])
-> State ([Maybe n], b)
-> [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([Maybe n], b) -> [Maybe n]
forall a b. (a, b) -> a
fst (([Maybe n], b) -> [Maybe n])
-> (State ([Maybe n], b) -> ([Maybe n], b))
-> State ([Maybe n], b)
-> [Maybe n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State ([Maybe n], b) -> ([Maybe n], b)
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 :: c (State (a, b)) -> Transition (a, b) e -> Transition (a, b) e
replaceDestinationFromMap c (State (a, b))
m Transition (a, b) e
t
>     | c (State (a, b)) -> Bool
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 = c (State (a, b)) -> State (a, b)
forall (l :: * -> *) a. Linearizable l => l a -> a
chooseOne c (State (a, b))
m'}
>     where m' :: c (State (a, b))
m'  =  (State (a, b) -> Bool) -> c (State (a, b)) -> c (State (a, b))
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==) (State (a, b) -> a
forall c b. State (c, b) -> c
fn (State (a, b) -> a) -> State (a, b) -> a
forall a b. (a -> b) -> a -> b
$ Transition (a, b) e -> State (a, b)
forall n e. Transition n e -> State n
destination Transition (a, b) e
t) (a -> Bool) -> (State (a, b) -> a) -> State (a, b) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (a, b) -> a
forall c b. State (c, b) -> c
fn) c (State (a, b))
m
>           fn :: State (c, b) -> c
fn  =  (c, b) -> c
forall a b. (a, b) -> a
fst ((c, b) -> c) -> (State (c, b) -> (c, b)) -> State (c, b) -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (c, b) -> (c, b)
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 :: c (Transition (n, n') e) -> c (Transition (n, n') e)
mergeByDestFst c (Transition (n, n') e)
l = c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
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)
forall c a. Container c a => c
empty c (Transition (n, n') e)
l

> 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' :: 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
>     | c (Transition (n, n') e) -> Bool
forall c a. Container c a => c -> Bool
isEmpty c (Transition (n, n') e)
l = c (Transition (n, n') e)
p
>     | Bool
otherwise
>           = c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
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)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall c a. Container c a => c -> c -> c
union c (Transition (n, n') e)
p   (c (Transition (n, n') e) -> c (Transition (n, n') e))
-> (c (Transition (n, n') e) -> c (Transition (n, n') e))
-> c (Transition (n, n') e)
-> c (Transition (n, n') e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>              Transition (n, n') e
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall c a. Container c a => a -> c -> c
insert Transition (n, n') e
x  (c (Transition (n, n') e) -> c (Transition (n, n') e))
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall a b. (a -> b) -> a -> b
$
>              (Transition (n, n') e -> Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (State (n, n') -> Transition (n, n') e -> Transition (n, n') e
forall n e. State n -> Transition n e -> Transition n e
set_dest (Transition (n, n') e -> State (n, n')
forall n e. Transition n e -> State n
destination Transition (n, n') e
x)) c (Transition (n, n') e)
sds
>             ) (c (Transition (n, n') e) -> c (Transition (n, n') e))
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall a b. (a -> b) -> a -> b
$ c (Transition (n, n') e)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
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)       =  c (Transition (n, n') e)
-> (Transition (n, n') e, c (Transition (n, n') e))
forall (l :: * -> *) a. Linearizable l => l a -> (a, l a)
choose c (Transition (n, n') e)
l
>           fnd :: Transition (c, b) e -> c
fnd           =  (c, b) -> c
forall a b. (a, b) -> a
fst ((c, b) -> c)
-> (Transition (c, b) e -> (c, b)) -> Transition (c, b) e -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (c, b) -> (c, b)
forall n. State n -> n
nodeLabel (State (c, b) -> (c, b))
-> (Transition (c, b) e -> State (c, b))
-> Transition (c, b) e
-> (c, b)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition (c, b) e -> State (c, b)
forall n e. Transition n e -> State n
destination
>           sds :: c (Transition (n, n') e)
sds           =  (Transition (n, n') e -> Bool)
-> c (Transition (n, n') e) -> c (Transition (n, n') e)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep (n -> n -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Transition (n, n') e -> n
forall c b e. Transition (c, b) e -> c
fnd Transition (n, n') e
x) (n -> Bool)
-> (Transition (n, n') e -> n) -> Transition (n, n') e -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition (n, n') e -> n
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 :: Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
extendAlphabetTo Set b
syms = FSA Integer b -> FSA a b -> FSA (Maybe Integer, Maybe 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 Integer b -> FSA a b -> FSA (Maybe Integer, Maybe a) b)
-> FSA Integer b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
forall a b. (a -> b) -> a -> b
$ Set b -> FSA Integer 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 :: 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) -> Set (Maybe b) -> Set (Maybe b)
forall c a. Container c a => c -> c -> c
union Set (Maybe b)
as Set (Maybe b)
new
>           , transitions :: Set (Transition a (Maybe b))
transitions = Set (Transition a (Maybe b))
-> Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b))
forall c a. Container c a => c -> c -> c
union Set (Transition a (Maybe b))
ts Set (Transition a (Maybe b))
ts'
>           }
>     where as :: Set (Maybe b)
as   =  FSA a (Maybe b) -> Set (Maybe b)
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa
>           new :: Set (Maybe b)
new  =  Set (Maybe b) -> Set (Maybe b) -> Set (Maybe b)
forall c a. (Container c a, Eq a) => c -> c -> c
difference ((b -> Maybe b) -> Set b -> Set (Maybe b)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic b -> Maybe b
forall a. a -> Maybe a
Just Set b
syms) Set (Maybe b)
as
>           ts :: Set (Transition a (Maybe b))
ts   =  FSA a (Maybe b) -> Set (Transition a (Maybe b))
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  =  Set (Transition n (Maybe b))
-> Set (Transition n (Maybe b)) -> Set (Transition n (Maybe b))
forall c a. Container c a => c -> c -> c
union ((Maybe b -> Transition n (Maybe b))
-> Set (Maybe b) -> Set (Transition n (Maybe b))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                          (\Maybe b
x -> Transition n e
e {edgeLabel :: Symbol (Maybe b)
edgeLabel = Maybe b -> Symbol (Maybe b)
forall e. e -> Symbol e
Symbol Maybe b
x}) Set (Maybe b)
new)
>           ts' :: Set (Transition a (Maybe b))
ts'  =  (Transition a (Maybe b)
 -> Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b)))
-> Set (Transition a (Maybe b))
-> Set (Transition a (Maybe b))
-> Set (Transition a (Maybe b))
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse Transition a (Maybe b)
-> Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b))
forall n e.
Ord n =>
Transition n e
-> Set (Transition n (Maybe b)) -> Set (Transition n (Maybe b))
f Set (Transition a (Maybe b))
forall c a. Container c a => c
empty (Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b)))
-> Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b))
forall a b. (a -> b) -> a -> b
$
>                   (Transition a (Maybe b) -> Symbol (Maybe b))
-> Symbol (Maybe b)
-> Set (Transition a (Maybe b))
-> Set (Transition a (Maybe b))
forall a b. (Ord a, Ord b) => (a -> b) -> b -> Set a -> Set a
extractMonotonic Transition a (Maybe b) -> Symbol (Maybe b)
forall n e. Transition n e -> Symbol e
edgeLabel (Maybe b -> Symbol (Maybe b)
forall e. e -> Symbol e
Symbol Maybe b
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 :: FSA a (Maybe b) -> FSA a b
desemantify FSA a (Maybe b)
fsa = (Maybe b -> b) -> FSA a (Maybe b) -> FSA a b
forall e e1 n.
(Ord e, Ord e1, Ord n) =>
(e -> e1) -> FSA n e -> FSA n e1
renameSymbolsByMonotonic (b -> (b -> b) -> Maybe b -> b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe b
forall a. HasCallStack => a
undefined b -> b
forall a. a -> a
id) (FSA a (Maybe b) -> FSA a b) -> FSA a (Maybe b) -> FSA a b
forall a b. (a -> b) -> a -> b
$
>                   Set (Maybe b) -> FSA a (Maybe b) -> FSA a (Maybe b)
forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo
>                   (Maybe b -> Set (Maybe b) -> Set (Maybe b)
forall a. Ord a => a -> Set a -> Set a
Set.delete Maybe b
forall a. Maybe a
Nothing (FSA a (Maybe b) -> Set (Maybe b)
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa))
>                   FSA a (Maybe b)
fsa

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 :: Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
tierify Set b
t FSA a (Maybe b)
fsa = Set b -> FSA a (Maybe b) -> FSA a (Maybe b)
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'   =  Set (Maybe b) -> FSA a (Maybe b) -> FSA a (Maybe b)
forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo ((b -> Maybe b) -> Set b -> Set (Maybe b)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap b -> Maybe b
forall a. a -> Maybe a
Just Set b
t) (FSA a (Maybe b) -> FSA a (Maybe b))
-> FSA a (Maybe b) -> FSA a (Maybe b)
forall a b. (a -> b) -> a -> b
$
>                   Set b -> FSA a (Maybe b) -> FSA a (Maybe 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       = Maybe b -> Set (Maybe b) -> Set (Maybe b)
forall c a. Container c a => a -> c -> c
insert Maybe b
forall a. Maybe a
Nothing (Set (Maybe b) -> Set (Maybe b)) -> Set (Maybe b) -> Set (Maybe b)
forall a b. (a -> b) -> a -> b
$ FSA a (Maybe b) -> Set (Maybe b)
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
f'
>                   , transitions :: Set (Transition a (Maybe b))
transitions = Set (Transition a (Maybe b))
-> Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b))
forall c a. Container c a => c -> c -> c
union (FSA a (Maybe b) -> Set (Transition a (Maybe b))
forall n e. FSA n e -> Set (Transition n e)
transitions FSA a (Maybe b)
f') (Set (Transition a (Maybe b)) -> Set (Transition a (Maybe b)))
-> (Set (State a) -> Set (Transition a (Maybe b)))
-> Set (State a)
-> Set (Transition a (Maybe b))
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                                   (State a -> Transition a (Maybe b))
-> Set (State a) -> Set (Transition a (Maybe b))
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic State a -> Transition a (Maybe b)
forall n a. State n -> Transition n (Maybe a)
l (Set (State a) -> Set (Transition a (Maybe b)))
-> Set (State a) -> Set (Transition a (Maybe b))
forall a b. (a -> b) -> a -> b
$ FSA a (Maybe b) -> Set (State a)
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 :: forall n e. Symbol e -> State n -> State n -> Transition n e
Transition
>                   { edgeLabel :: Symbol (Maybe a)
edgeLabel    =  Maybe a -> Symbol (Maybe a)
forall e. e -> Symbol e
Symbol Maybe a
forall a. Maybe a
Nothing
>                   , source :: State n
source       =  State n
q
>                   , destination :: State n
destination  =  State n
q
>                   }
>           as :: Set b
as   =  (Maybe b -> Set b -> Set b) -> Set b -> Set (Maybe b) -> Set b
forall (c :: * -> *) a b.
Collapsible c =>
(a -> b -> b) -> b -> c a -> b
collapse ((Set b -> Set b)
-> (b -> Set b -> Set b) -> Maybe b -> Set b -> Set b
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Set b -> Set b
forall a. a -> a
id b -> Set b -> Set b
forall c a. Container c a => a -> c -> c
insert) Set b
forall c a. Container c a => c
empty (Set (Maybe b) -> Set b) -> Set (Maybe b) -> Set b
forall a b. (a -> b) -> a -> b
$ FSA a (Maybe b) -> Set (Maybe b)
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA a (Maybe b)
fsa

> -- |Remove symbols from the alphabet of an automaton.
> contractAlphabetTo :: (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
> contractAlphabetTo :: Set b -> FSA a b -> FSA a b
contractAlphabetTo Set b
syms FSA a b
fsa = FSA a b -> FSA a b
forall e n. (Ord e, Ord n) => FSA n e -> FSA n e
trimUnreachables (FSA a b -> FSA a b) -> FSA a b -> FSA a b
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 = (Transition a b -> Bool)
-> Set (Transition a b) -> Set (Transition a b)
forall (s :: * -> *) a.
(Collapsible s, Container (s a) a) =>
(a -> Bool) -> s a -> s a
keep
>                   (Set (Symbol b) -> Symbol b -> Bool
forall c a. (Container c a, Eq a) => c -> a -> Bool
isIn
>                    (Symbol b -> Set (Symbol b) -> Set (Symbol b)
forall c a. Container c a => a -> c -> c
insert Symbol b
forall e. Symbol e
Epsilon (Set (Symbol b) -> Set (Symbol b))
-> Set (Symbol b) -> Set (Symbol b)
forall a b. (a -> b) -> a -> b
$ (b -> Symbol b) -> Set b -> Set (Symbol b)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic b -> Symbol b
forall e. e -> Symbol e
Symbol Set b
syms) (Symbol b -> Bool)
-> (Transition a b -> Symbol b) -> Transition a b -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                    Transition a b -> Symbol b
forall n e. Transition n e -> Symbol e
edgeLabel
>                   ) (Set (Transition a b) -> Set (Transition a b))
-> Set (Transition a b) -> Set (Transition a b)
forall a b. (a -> b) -> a -> b
$ FSA a b -> Set (Transition 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 :: Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
forceAlphabetTo Set b
syms = Set b
-> FSA (Maybe Integer, Maybe a) b -> FSA (Maybe Integer, Maybe a) b
forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo Set b
syms (FSA (Maybe Integer, Maybe a) b -> FSA (Maybe Integer, Maybe a) b)
-> (FSA a b -> FSA (Maybe Integer, Maybe a) b)
-> FSA a b
-> FSA (Maybe Integer, Maybe a) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set b -> FSA a b -> FSA (Maybe Integer, Maybe a) b
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 :: FSA n e -> FSA n1 e
renameStates FSA n e
fsa = (n -> n1) -> FSA n e -> FSA n1 e
forall e n n1.
(Ord e, Ord n, Ord n1) =>
(n -> n1) -> FSA n e -> FSA n1 e
renameStatesByMonotonic
>                    ((n -> Map n n1 -> n1) -> Map n n1 -> n -> n1
forall a b c. (a -> b -> c) -> b -> a -> c
flip (n1 -> n -> Map n n1 -> n1
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Int -> n1
forall a. Enum a => Int -> a
toEnum Int
0)) Map n n1
m)
>                    FSA n e
fsa
>     where m :: Map n n1
m = [(n, n1)] -> Map n n1
forall k a. [(k, a)] -> Map k a
Map.fromDistinctAscList ([(n, n1)] -> Map n n1)
-> (Set (State n) -> [(n, n1)]) -> Set (State n) -> Map n n1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([n] -> [n1] -> [(n, n1)]) -> [n1] -> [n] -> [(n, n1)]
forall a b c. (a -> b -> c) -> b -> a -> c
flip [n] -> [n1] -> [(n, n1)]
forall a b. [a] -> [b] -> [(a, b)]
zip (n1 -> [n1]
forall a. Enum a => a -> [a]
enumFrom (n1 -> [n1]) -> n1 -> [n1]
forall a b. (a -> b) -> a -> b
$ Int -> n1
forall a. Enum a => Int -> a
toEnum Int
1) ([n] -> [(n, n1)])
-> (Set (State n) -> [n]) -> Set (State n) -> [(n, n1)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>               (State n -> n) -> [State n] -> [n]
forall a b. (a -> b) -> [a] -> [b]
map State n -> n
forall n. State n -> n
nodeLabel ([State n] -> [n])
-> (Set (State n) -> [State n]) -> Set (State n) -> [n]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set (State n) -> [State n]
forall a. Set a -> [a]
Set.toAscList (Set (State n) -> Map n n1) -> Set (State n) -> Map n n1
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
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 :: (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      =  (Transition n e -> Transition n1 e)
-> Set (Transition n e) -> Set (Transition n1 e)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap (Noitisnart e n1 -> Transition n1 e
forall e n. Noitisnart e n -> Transition n e
transition (Noitisnart e n1 -> Transition n1 e)
-> (Transition n e -> Noitisnart e n1)
-> Transition n e
-> Transition n1 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> n1) -> Noitisnart e n -> Noitisnart e n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f (Noitisnart e n -> Noitisnart e n1)
-> (Transition n e -> Noitisnart e n)
-> Transition n e
-> Noitisnart e n1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> Noitisnart e n
forall e n. Transition n e -> Noitisnart e n
Noitisnart)
>                               (FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a)
>         , initials :: Set (State n1)
initials         =  (State n -> State n1) -> Set (State n) -> Set (State n1)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((n -> n1) -> State n -> State n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
a)
>         , finals :: Set (State n1)
finals           =  (State n -> State n1) -> Set (State n) -> Set (State n1)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((n -> n1) -> State n -> State n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
finals FSA n e
a)
>         , isDeterministic :: Bool
isDeterministic  =  FSA n e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n e
a Bool -> Bool -> Bool
&&
>                               Set (State n1) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set (State n1)
ns Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set (State n) -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n e -> Set (State n)
forall e n. (Ord e, Ord n) => FSA n e -> Set (State n)
states FSA n e
a)
>         }
>     where ns :: Set (State n1)
ns = (State n -> State n1) -> Set (State n) -> Set (State n1)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((n -> n1) -> State n -> State n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (FSA n e -> Set (State n)
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 :: (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  =  (Transition n e -> Transition n1 e)
-> Set (Transition n e) -> Set (Transition n1 e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic
>                           (Noitisnart e n1 -> Transition n1 e
forall e n. Noitisnart e n -> Transition n e
transition (Noitisnart e n1 -> Transition n1 e)
-> (Transition n e -> Noitisnart e n1)
-> Transition n e
-> Transition n1 e
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (n -> n1) -> Noitisnart e n -> Noitisnart e n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f (Noitisnart e n -> Noitisnart e n1)
-> (Transition n e -> Noitisnart e n)
-> Transition n e
-> Noitisnart e n1
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Transition n e -> Noitisnart e n
forall e n. Transition n e -> Noitisnart e n
Noitisnart) (Set (Transition n e) -> Set (Transition n1 e))
-> Set (Transition n e) -> Set (Transition n1 e)
forall a b. (a -> b) -> a -> b
$
>                           FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a
>         , initials :: Set (State n1)
initials     =  (State n -> State n1) -> Set (State n) -> Set (State n1)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((n -> n1) -> State n -> State n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (Set (State n) -> Set (State n1))
-> Set (State n) -> Set (State n1)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
forall n e. FSA n e -> Set (State n)
initials FSA n e
a
>         , finals :: Set (State n1)
finals       =  (State n -> State n1) -> Set (State n) -> Set (State n1)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((n -> n1) -> State n -> State n1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap n -> n1
f) (Set (State n) -> Set (State n1))
-> Set (State n) -> Set (State n1)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (State n)
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 :: (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      =  (Transition n e -> Transition n e1)
-> Set (Transition n e) -> Set (Transition n e1)
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap ((e -> e1) -> Transition n e -> Transition n e1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> e1
f) (Set (Transition n e) -> Set (Transition n e1))
-> Set (Transition n e) -> Set (Transition n e1)
forall a b. (a -> b) -> a -> b
$ FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a
>                         , isDeterministic :: Bool
isDeterministic  =  FSA n e -> Bool
forall n e. FSA n e -> Bool
isDeterministic FSA n e
a Bool -> Bool -> Bool
&& Bool
samea
>                         }
>     where alpha :: Set e1
alpha  =  (e -> e1) -> Set e -> Set e1
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap e -> e1
f (FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
a)
>           samea :: Bool
samea  =  Set e1 -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize Set e1
alpha Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Set e -> Integer
forall (c :: * -> *) b. Collapsible c => c b -> Integer
isize (FSA n e -> Set e
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 :: (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  =  (Transition n e -> Transition n e1)
-> Set (Transition n e) -> Set (Transition n e1)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic ((e -> e1) -> Transition n e -> Transition n e1
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap e -> e1
f) (FSA n e -> Set (Transition n e)
forall n e. FSA n e -> Set (Transition n e)
transitions FSA n e
a)
>         }
>     where alpha :: Set e1
alpha  =  (e -> e1) -> Set e -> Set e1
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic e -> e1
f (FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
a)

Mapping on tuples:

> mapfst :: (a -> b) -> (a, c) -> (b, c)
> mapfst :: (a -> b) -> (a, c) -> (b, c)
mapfst a -> b
f (a
a, c
b) = (a -> b
f a
a, c
b)

> mapsnd :: (b -> c) -> (a, b) -> (a, c)
> mapsnd :: (b -> c) -> (a, b) -> (a, c)
mapsnd b -> c
f (a
a, b
b) = (a
a, b -> c
f 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
(Tree a -> Tree a -> Bool)
-> (Tree a -> Tree a -> Bool) -> Eq (Tree a)
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, Eq (Tree a)
Eq (Tree a)
-> (Tree a -> Tree a -> Ordering)
-> (Tree a -> Tree a -> Bool)
-> (Tree a -> Tree a -> Bool)
-> (Tree a -> Tree a -> Bool)
-> (Tree a -> Tree a -> Bool)
-> (Tree a -> Tree a -> Tree a)
-> (Tree a -> Tree a -> Tree a)
-> Ord (Tree a)
Tree a -> Tree a -> Bool
Tree a -> Tree a -> Ordering
Tree a -> Tree a -> Tree a
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
$cp1Ord :: forall a. Ord a => Eq (Tree a)
Ord, ReadPrec [Tree a]
ReadPrec (Tree a)
Int -> ReadS (Tree a)
ReadS [Tree a]
(Int -> ReadS (Tree a))
-> ReadS [Tree a]
-> ReadPrec (Tree a)
-> ReadPrec [Tree a]
-> Read (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
[Tree a] -> ShowS
Tree a -> String
(Int -> Tree a -> ShowS)
-> (Tree a -> String) -> ([Tree a] -> ShowS) -> Show (Tree a)
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 :: [a] -> Tree a
treeFromList [] = String -> Tree a
forall a. HasCallStack => String -> a
error String
"No elements"
> treeFromList (a
x:[]) = a -> Tree a
forall a. a -> Tree a
Leaf a
x
> treeFromList [a]
xs = Tree a
ls' Tree a -> Tree a -> Tree a
forall a b. a -> b -> b
`par` Tree a
rs' Tree a -> Tree a -> Tree a
forall a b. a -> b -> b
`pseq` Tree a -> Tree a -> Tree a
forall a. Tree a -> Tree a -> Tree a
Tree Tree a
ls' Tree a
rs'
>     where ([a]
ls, [a]
rs)    =  [a] -> ([a], [a])
forall a. [a] -> ([a], [a])
evenOdds [a]
xs
>           (Tree a
ls', Tree a
rs')  =  ([a] -> Tree a
forall a. [a] -> Tree a
treeFromList [a]
ls, [a] -> Tree a
forall a. [a] -> Tree a
treeFromList [a]
rs)

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

> treeFold :: (a -> a -> a) -> Tree a -> a
> treeFold :: (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' a -> a -> a
forall a b. a -> b -> b
`par` a
r' a -> a -> a
forall a b. a -> b -> b
`pseq` (a
l' a -> a -> a
`op` a
r')
>     where l' :: a
l'  =  (a -> a -> a) -> Tree a -> a
forall a. (a -> a -> a) -> Tree a -> a
treeFold a -> a -> a
op Tree a
l
>           r' :: a
r'  =  (a -> a -> a) -> Tree a -> a
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 :: [a] -> ([a], [a])
evenOdds []        =  ([], [])
> evenOdds (a
a:[])    =  (a
a a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [], [])
> evenOdds (a
a:a
b:[a]
xs)  =  let ([a]
e, [a]
o) = [a] -> ([a], [a])
forall a. [a] -> ([a], [a])
evenOdds [a]
xs in (a
aa -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
e, a
ba -> [a] -> [a]
forall a. a -> [a] -> [a]
:[a]
o)