> {-# OPTIONS_HADDOCK show-extensions #-}
> {-|
> Module:     LTK.Tiers
> Copyright:  (c) 2019 Dakotah Lambert
> Licence:    MIT

> If an FSA defines a stringset that is the preprojection
> of some other stringset over a smaller alphabet,
> the functions in this module can determine what that alphabet is
> and return the appropriate projective automaton.
> -}
> module LTK.Tiers (tier, project) where

> import LTK.FSA
> import Data.Set (Set)
> import qualified Data.Set as Set

If a given FSA is the preprojection of some constraint,
then symbols are freely insertable and deletable
if they do not appear in the associated projection.
For a normal-form DFA, then,
these symbols are self loops on every state.

> -- |Determine the tier alphabet for which the given FSA is a preprojection.
> -- This could simply be the entire alphabet of the FSA.
> -- Precondition: the given FSA must be in normal form.
> tier :: (Ord n, Ord e) => FSA n e -> Set e
> tier :: FSA n e -> Set e
tier FSA n e
fsa = Set e -> Set e -> Set e
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (FSA n e -> Set e
forall (g :: * -> *) e. HasAlphabet g => g e -> Set e
alphabet FSA n e
fsa) (Set e -> Set e) -> Set e -> Set e
forall a b. (a -> b) -> a -> b
$ Set (Symbol e) -> Set e
forall (s :: * -> *) c e.
(Collapsible s, Container c e, Monoid c) =>
s (Symbol e) -> c
unsymbols Set (Symbol e)
tc
>     where f :: State n -> Set (Symbol e)
f State n
q  =  (Transition n e -> Symbol e)
-> Set (Transition n e) -> Set (Symbol e)
forall a b. (a -> b) -> Set a -> Set b
Set.mapMonotonic Transition n e -> Symbol e
forall n e. Transition n e -> Symbol e
edgeLabel (Set (Transition n e) -> Set (Symbol e))
-> (Set (Transition n e) -> Set (Transition n e))
-> Set (Transition n e)
-> Set (Symbol e)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
>                   (Transition n e -> Bool)
-> Set (Transition n e) -> Set (Transition n e)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\Transition n e
t -> Transition n e -> State n
forall n e. Transition n e -> State n
source Transition n e
t State n -> State n -> Bool
forall a. Eq a => a -> a -> Bool
== State n
q Bool -> Bool -> Bool
&& Transition n e -> State n
forall n e. Transition n e -> State n
destination Transition n e
t State n -> State n -> Bool
forall a. Eq a => a -> a -> Bool
== State n
q) (Set (Transition n e) -> Set (Symbol e))
-> Set (Transition n e) -> Set (Symbol 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
>           tc :: Set (Symbol e)
tc   =  Set (Set (Symbol e)) -> Set (Symbol e)
forall c a (s :: * -> *).
(Container c a, Eq a, Collapsible s) =>
s c -> c
intersectAll ((State n -> Set (Symbol e))
-> Set (State n) -> Set (Set (Symbol e))
forall (s :: * -> *) b1 b a.
(Collapsible s, Container (s b1) b) =>
(a -> b) -> s a -> s b1
tmap State n -> Set (Symbol e)
f (Set (State n) -> Set (Set (Symbol e)))
-> Set (State n) -> Set (Set (Symbol e))
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)

> -- |Remove symbols not relevant to the given FSA's associated projection
> -- (as determined by @tier@).
> -- Precondition: the given FSA must be in normal form.
> project :: (Ord n, Ord e) => FSA n e -> FSA n e
> project :: FSA n e -> FSA n e
project FSA n e
fsa = Set e -> FSA n e -> FSA n e
forall a b. (Ord a, Ord b) => Set b -> FSA a b -> FSA a b
contractAlphabetTo (FSA n e -> Set e
forall n e. (Ord n, Ord e) => FSA n e -> Set e
tier FSA n e
fsa) FSA n e
fsa

If the projection is SL, the given FSA is TSL.
If the projection is LT, the given FSA is TLT.
etc.