\begin{comment}
\begin{code}
{-# LANGUAGE ScopedTypeVariables
#-}

{-|
Description: Finite state transducers with epsilon-transitions
-}
module Control.FST
  ( FST(..)
  -- * Using FSTs
  , runFST, runFST', step
  -- * Constructing FSTs
  , wordFST
  -- * Operations on FSTs
  , productFST, restrictOutput, restrictFST
  -- * Debugging Utilities
  , liveFST, dotFST
  ) where

import Data.Map.Lazy (Map, (!?), (!))
import qualified Data.Map.Lazy as Map

import Data.Set (Set)
import qualified Data.Set as Set

import Data.Sequence (Seq)
import qualified Data.Sequence as Seq

import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust, isNothing)

import Numeric.Natural

import Control.Lens

import Control.Monad.State.Strict

import Text.PrettyPrint.Leijen (Pretty(..))
import qualified Text.PrettyPrint.Leijen as PP

import Data.Bool (bool)
import Data.Monoid ((<>))

import Text.Dot

\end{code}
\end{comment}

\begin{defn}[Finite state transducers]
Unter einem finite state transducer verstehen wir ein 6-Tupel $(\Sigma, \Delta, Q, I, F, E)$ mit $\Sigma$ dem endlichen Eingabe-Alphabet, $\Delta$ dem endlichen Ausgabe-Alphabet, $Q$ einer endlichen Menge an Zuständen, $I \subset Q$ der Menge von initialen Zuständen, $F \subset Q$ der Menge von akzeptierenden Endzuständen, und $E \subset Q \times (\Sigma \cup \{ \epsilon \}) \times (\Delta \cup \{ \epsilon \}) \times Q$ der Transitionsrelation.

Semantisch ist ein finite state transducer ein endlicher Automat erweitert um die Fähigkeit bei Zustandsübergängen ein Symbol aus seinem Ausgabe-Alphabet an ein Ausgabe-Wort anzuhängen.

In Haskell lockern wir die Anforderung, dass die Ein- und Ausgabe-Alphabete endlich sein müssen und annotieren sie nur im Typsystem.
Zudem speichern wir die Transitionsrelation als multimap um effiziente lookups von Zustand-Eingabe-Paaren zu ermöglichen.

\begin{code}
data FST state input output = FST
  { stInitial :: Set state
  , stTransition :: Map (state, Maybe input) (Set (state, Maybe output))
  , stAccept :: Set state
  } deriving (Show, Read)
\end{code}
\end{defn}

\begin{eg} \label{eg:linebreak}
  Als wiederkehrendes Beispiel betrachten wir einen Transducer $L_{80} = (\Sigma, \Delta, Q, I, F, E)$, der für ein beliebiges Alphabet $\Sigma \supseteq \{ \text{\tt ' '}, \text{\tt \textbackslash n} \}$ durch Umwandlung zwischen Leerzeichen und Zeilenumbrüchen sicherstellt, dass jede Zeile des Ausgabetextes mindestens 80 Zeichen enthält, jedoch nur an Wortgrenzen umbricht:

  \begin{align*}
    \Delta & = \Sigma \\
    Q & = \{ 0, 1, \ldots, 80 \} \\
    I & = \{ 0 \} \\
    F & = Q \\
    E & = \{ (q, \sigma, \sigma, q + 1) \mid q \in Q \mysetminus \{ 80 \}, \sigma \in \Sigma \mysetminus \{ \text{\tt \textbackslash n} \} \} \\
      & \cup \{ (q, \text{\tt \textbackslash n}, \text{\tt ' '}, q + 1) \mid q \in Q \mysetminus \{ 80 \}, \sigma \in \Sigma \} \\
      & \cup \{ (80, \text{\tt ' '}, \text{\tt \textbackslash n}, 0), (80, \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, 0) \} \\
      & \cup \{ (80, \sigma, \sigma, 80) \mid \sigma \in \Sigma \mysetminus \{ \text{\tt ' '}, \text{\tt \textbackslash n} \} \}
  \end{align*}

  Siehe auch Abbildung~\ref{fig:linebreak}

  \begin{figure}[h]
    \centering
    \begin{tikzpicture}[->,auto,node distance=5cm]
      \node[initial,state,accepting] (0) {$0$};
      \node[state,accepting] (1) [right of=0] {$1$};
      \node[] (rest) [below of=1] {$\ldots$};
      \node[state,accepting] (i) [right of=rest,xshift=-2cm] {$i$};
      \node[state,accepting] (si) [below of=rest,yshift=2cm] {$i + 1$};
      \node[state,accepting] (80) [left of=rest] {$80$};

      \path (0) edge node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (1)
            (1) edge [bend left=20] node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (rest)
                edge [bend right=20] node [left] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (rest)
            (rest) edge node [below] {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (80)
                   edge [bend right=20] node [above] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (80)
            (i) edge [bend left=45] node {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n} \}$} (si)
                edge [bend left=10] node [left] {$(\text{\tt \textbackslash n}, \text{\tt ' '})$} (si)
            (80) edge [loop below] node [below] {$\{ (\sigma, \sigma) \mid \sigma \in \Sigma, \sigma \neq \text{\tt \textbackslash n}, \sigma \neq \text{\tt ' '} \}$} (80)
                 edge [bend left=20] node {$(\text{\tt \textbackslash n}, \text{\tt \textbackslash n})$} (0)
                 edge [bend right=20] node [right] {$(\text{\tt ' '}, \text{\tt \textbackslash n})$} (0);

      \draw[-] (rest)--(i.north);
      \draw[-] (rest)--(si.west);
    \end{tikzpicture}
    \caption{\label{fig:linebreak} Ein Transducer der, durch Übersetzung zwischen Leerzeichen und Zeilenumbrüchen, sicher stellt, dass jede Zeile eines Texts mindestens 80 Zeichen hat}
  \end{figure}
\end{eg}

\begin{comment}
\begin{code}
instance (Show state, Show input, Show output, Ord state, Ord input, Ord output) => Pretty (FST state input output) where
  pretty fst@FST{..} = PP.vsep
    [ PP.text "Initial states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stInitial)
    , PP.text "State transitions:" PP.<$> PP.indent 2 (PP.vsep
        [        PP.text (bool " " "#" $ Set.member st live)
          PP.<+> PP.text (show st)
          PP.<+> (PP.text "-" PP.<> PP.tupled [label inS, label outS] PP.<> PP.text "→")
          PP.<+> PP.text (show st')
        | ((st, inS), to) <- Map.toList stTransition
        , (st', outS) <- Set.toAscList to
        ])
    , PP.text "Accepting states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stAccept)
    ]
    where
      label :: Show a => Maybe a -> PP.Doc
      label = PP.text . maybe "ɛ" show
      list :: [PP.Doc] -> PP.Doc
      list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space)
      live = liveFST fst
\end{code}
\end{comment}

\begin{defn}[Auswertung von FSTs]
Wir definieren die Auswertung von finite state transducers induktiv indem wir zunächst angeben wie ein einzelner Auswertungs-Schritt erfolgt.

Hierzu kommentieren wir die Haskell-Implementierung eines Auswertungs-Schritts.
Notwendigerweise ist die Auswertung eines FSTs nicht deterministisch, wir produzieren daher eine Liste von möglichen Resultaten in keiner besonderen Reihenfolge.

\begin{code}
step :: forall input output state. (Ord input, Ord output, Ord state)
     => FST state input output
     -> Maybe state -- ^ Current state
     -> Maybe input -- ^ Head of remaining input
     -> [(Maybe input, state, Maybe output)] -- ^ Tuples of unconsumed input, next state, and produced output
step FST{..} Nothing inS = (\s -> (inS, s, Nothing)) <$> Set.toList stInitial
\end{code}
Ist kein vorheriger Schritt erfolgt so wählen wir einen initialen Zustand, konsumieren keine Eingabe, und produzieren keine Ausgabe.

\begin{code}
step FST{..} (Just c) inS = let
  consuming = fromMaybe Set.empty $ Map.lookup (c, inS) stTransition
  unconsuming = fromMaybe Set.empty $ Map.lookup (c, Nothing) stTransition
  in Set.toList $ Set.map (\(n, mOut) -> (Nothing, n, mOut)) consuming `Set.union` Set.map (\(n, mOut) -> (inS, n, mOut)) unconsuming
\end{code}
Ansonsten wählen wir einen Eintrag aus der Transitionstabelle für den aktuellen Zustand, der entweder keine oder die gegebene Eingabe konsumiert.
Im Ergebnis geben wir den nächsten Zustand, die Ausgabe aus der Transitionstabelle, und ob die Eingabe konsumiert wurde an.

\begin{code}
runFST' :: forall input output state. (Ord input, Ord output, Ord state)
        => FST state input output
        -> Seq input
        -> [(state, Seq (state, Maybe output))] -- ^ Tuples of initial state and chosen transitions; not neccessarily finite
-- ^ Compute all possible runs on the given input
runFST' fst@FST{..} cs = do
  initial <- view _2 <$> step fst Nothing Nothing -- Nondeterministically choose an initial state
  go (initial, Seq.Empty) cs -- Recursively extend the run consisting of only the initial state
  where
    go :: (state, Seq (state, Maybe output)) -> Seq input-> [(state, Seq (state, Maybe output))]
    -- ^ Uses `step` on last state of run and nondeterministically chooses between alternatives given
\end{code}

Um alle möglichen Läufe auf einer gegebenen Eingabe zu berechnen wenden wir
rekursiv \texttt{step} auf den letzten Zustand des Laufs (und der verbleibenden
Eingabe) an bis keine Eingabe verbleibt und der letzte Zustand in der Menge der
akzeptierenden Endzustände liegt.

\begin{comment}
\begin{code}
    go (initial, path) cs = do
      let
        -- | Determine last state of the run
        current
          | (_ :> (st, _)) <- path = st
          | otherwise              = initial
      case step fst (Just current) (Seq.lookup 0 cs) of
        [] -> do
          guard $ current `Set.member` stAccept && Seq.null cs
          return (initial, path)
        xs -> do
          (head, next, out) <- xs
          let
            nPath = path :> (next, out)
            ncs
              | (_ :< cs') <- cs = maybe id (:<) head cs'
              | otherwise = Seq.Empty
          go (initial, nPath) ncs
\end{code}
\end{comment}
\end{defn}

Es ist gelegentlich nützlich nur die möglichen Ausgaben eines FST auf gegebener
Eingabe zu bestimmen, wir führen eine Hilfsfunktion auf Basis von
{\ttfamily runFST'} ein:

\begin{code}
runFST :: forall input output state. (Ord input, Ord output, Ord state) => FST state input output -> Seq input -> [Seq output]
-- ^ Compute all possible runs on the given input and return only their output
\end{code}
\begin{comment}
\begin{code}
runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
  where
    catMaybes = fmap fromJust . Seq.filter isJust
\end{code}
\end{comment}

Wir können das Produkt zweier FSTs definieren.
Intuitiv wollen wir beide FSTs gleichzeitig ausführen und dabei sicherstellen, dass Ein- und Ausgabe der FSTs übereinstimmen\footnote{Da wir $\epsilon$-Transitionen in FSTs erlauben müssen wir uns festlegen wann eine $\epsilon$-Transition übereinstimmt mit einer anderen Transition. Wir definieren, dass $\epsilon$ als Eingabe ausschließlich mit $\epsilon$ übereinstimmt.}.

Hierfür berechnen wir das Graphen-Produkt der FSTs:

\begin{defn}[FST-Produkt]
  Gegeben zwei finite state transducer $T = (\Sigma, \Delta, Q, I, F, E)$ und $T^\prime = (\Sigma^\prime, \Delta^\prime, Q^\prime, I^\prime, F^\prime, E^\prime)$ nennen wir $T^\times = (\Sigma^\times, \Delta^\times, Q^\times, I^\times, F^\times, E^\times)$ das Produkt $T^\times = T \times T^\prime$ von $T$ und $T^\prime$.

  $T^\times$ bestimmt sich als das Graphenprodukt der beiden, die FSTs unterliegenden Graphen, wobei wir die Zustandsübergänge als Kanten mit Gewichten aus dem Boolschen Semiring auffassen:

  \begin{align*}
    \Sigma^\times & = \Sigma \cap \Sigma^\prime \\
    \Delta^\times & = \Delta \cap \Delta^\prime \\
    Q^\times & = Q \times Q^\prime \\
    I^\times & = I \times I^\prime \\
    F^\times & = F \times F^\prime \\
    E^\times & \subset Q^\times \times (\Sigma^\times \cup \{ \epsilon \}) \times (\Delta^\times \cup \{ \epsilon \}) \times Q^\times \\
             & = \left \{ ((q, q^\prime), \sigma, \delta, (\bar{q}, \bar{q^\prime})) \colon (q, \sigma, \delta, \bar{q}) \in E, (q^\prime, \sigma^\prime, \delta^\prime, \bar{q^\prime}) \in E^\prime, \sigma = \sigma^\prime, \delta = \delta^\prime \right \}
  \end{align*}
\end{defn}

  
\begin{code}
productFST :: forall state1 state2 input output. (Ord state1, Ord state2, Ord input, Ord output) => FST state1 input output -> FST state2 input output -> FST (state1, state2) input output
-- ^ Cartesian product on states, logical conjunction on transitions and state-properties (initial and accept)
--
-- This is the "natural" (that is component-wise) product when considering FSTs to be weighted in the boolean semiring.
--
-- Intuitively this corresponds to running both FSTs at the same time requiring them to produce the same output and agree on their input.
\end{code}

\begin{comment}
\begin{code}
productFST fst1 fst2 = FST
  { stInitial    = Set.fromDistinctAscList $ stInitial fst1 `setProductList` stInitial fst2
  , stAccept     = Set.fromDistinctAscList $ stAccept fst1 `setProductList` stAccept fst2
  , stTransition = Map.fromSet transitions . Set.fromDistinctAscList . mapMaybe filterTransition $ Map.keysSet (stTransition fst1) `setProductList` Map.keysSet (stTransition fst2)
  }
  where
    setProductList :: forall a b. Set a -> Set b -> [(a, b)]
    setProductList as bs = (,) <$> Set.toAscList as <*> Set.toAscList bs
    filterTransition :: forall label. Eq label => ((state1, Maybe label), (state2, Maybe label)) -> Maybe ((state1, state2), Maybe label)
    filterTransition ((st1, l1), (st2, l2))
      | l1 == l2  = Just ((st1, st2), l1)
      | otherwise = Nothing
    transitions :: ((state1, state2), Maybe input) -> Set ((state1, state2), Maybe output)
    transitions ((st1, st2), inS) = Set.fromDistinctAscList . mapMaybe filterTransition $ out1 `setProductList` out2
      where
        out1 = fromMaybe Set.empty (stTransition fst1 !? (st1, inS)) `Set.union` fromMaybe Set.empty (stTransition fst1 !? (st1, Nothing))
        out2 = fromMaybe Set.empty (stTransition fst2 !? (st2, inS)) `Set.union` fromMaybe Set.empty (stTransition fst2 !? (st2, Nothing))
\end{code}
\end{comment}

Es ist später erforderlich einen FST derart einzuschränken, dass er eine gegebene Ausgabe produziert.

Hierzu nehmen wir das FST-Produkt mit einem FST, der, ungeachtet der Eingabe, immer die gegebene Ausgabe produziert.
Da die Ausgaben der beiden FSTs übereinstimmen müssen produziert das Produkt mit einem derartigen FST (solange dessen Ausgabe in keinem Sinne von der Eingabe abhängt) die gewünschte Ausgabe.

Zur Konstruktion eines derartigen \emph{Wort-FST}s nehmen wir Indizes im Ausgabe-Wort (natürliche Zahlen) als Zustände.
Übergänge sind immer entweder der Form $n \rightarrow \text{succ}(n)$, konsumieren keine Eingabe ($\epsilon$) und produzieren als Ausgabe das Zeichen am Index $n$ im Ausgabe-Wort, oder der Form $n \overset{(\sigma, \epsilon)}{\rightarrow} n$, für jedes Eingabesymbol $\sigma$ (um die Unabhängigkeit von der Eingabe sicherzustellen).
Weiter ist $0$ initial und $\text{length}(\text{Ausgabe})$ der einzige akzeptierende Endzustand.

\begin{code}
wordFST :: forall input output. (Ord input, Ord output) => Set input -> Seq output -> FST Natural input output
-- ^ @wordFST inps str@ is the linear FST generating @str@ as output when given any input with symbols in @inps@
\end{code}
  
\begin{comment}
\begin{code}
wordFST inps outs = FST
  { stInitial    = Set.singleton 0
  , stAccept     = Set.singleton l
  , stTransition = Map.fromSet next states
  }
  where
    l :: Natural
    l = fromIntegral $ Seq.length outs
    states :: Set (Natural, Maybe input)
    states
      | Seq.null outs = Set.empty
      | otherwise = Set.fromDistinctAscList [ (n, inp) | n <- [0..pred l], inp <- Nothing : map Just (Set.toList inps) ]
    next :: (Natural, Maybe input) -> Set (Natural, Maybe output)
    next (i, _) = Set.fromList
      [ (succ i, Just . Seq.index outs $ fromIntegral i)
      , (i, Nothing)
      ]
\end{code}
\end{comment}

\begin{eg} \label{eg:w100}
  Der zum Wort $w = 1\, 2\, \ldots\, 80\, \text{\tt \textbackslash n}\, 81\, \ldots\, 98$ gehörige Wort-FST $W_w = ( \Sigma, \Delta, Q, I, F, E)$ für ein beliebiges Eingabe-Alphabet $\Sigma$ ist:

  \begin{align*}
    \Delta & = \{ 1, 2, \ldots, 98, \text{\tt \textbackslash n} \} \\
    Q & = \{ 0, 1, \ldots, 99 \} \\
    I & = \{ 0 \} \\
    F & = \{ 99 \} \\
    E & = \{ (i, \sigma, w_i, i + 1) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \} \\
      & \cup \{ (i, \sigma, \epsilon, i) \mid \sigma \in \Sigma \cup \{ \epsilon \}, i \in Q \mysetminus \{ 99 \} \}
  \end{align*}

  Siehe auch Abbildung~\ref{fig:w100}.

  \begin{figure}[h]
    \centering
    \begin{tikzpicture}[->,auto,node distance=5cm]
      \node[initial,state] (0) {$0$};
      \node[] (rest) [right of=0] {$\ldots$};
      \node[state,accepting] (99) [right of=rest] {$99$};

      \path (0) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (0)
                edge node {$\{ (\sigma, 1) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (rest)
            (rest) edge node {$\{ (\sigma, 98) \mid \sigma \in \Sigma \cup \{ \epsilon \} \}$} (99)
            (99) edge [loop above] node {$\{(\sigma, \epsilon) \mid \sigma \in \Sigma \}$} (99);
    \end{tikzpicture}

    \caption{\label{fig:w100} Der Wort-FST eines längeren Wortes}
  \end{figure}
\end{eg}

Da \texttt{wordFST} zur Konstruktion eine komprehensive Menge aller Eingabesymbole benötigt verwenden wir im folgenden eine optimierte Variante des Produkts mit einem Wort-FST.

\begin{code}
restrictOutput :: forall state input output. (Ord state, Ord input, Ord output) => Seq output -> FST state input output -> FST (Natural, state) input output
-- ^ @restrictOutput out@ is equivalent to @productFST (wordFST inps out)@ where @inps@ is a comprehensive set of all input symbols @inp :: input@
\end{code}

\begin{eg} \label{eg:l80timesw100}
  Der FST $L_{80}$ aus Beispiel \autoref{eg:linebreak} eingeschränkt auf das Wort $w$ aus Beispiel \autoref{eg:w100} (also $W_w \times L_{80}$) ist:

  \begin{align*}
    \Sigma^\times & = \{1, 2, \ldots, 99, \text{\tt \textbackslash n}, \text{\tt ' '} \} \\
    \Delta^\times & = \{1, 2, \ldots, 99, \text{\tt \textbackslash n} \} \\
    Q^\times & = \{ (\sigma, p) \mid \sigma \in \{ 0_{W_w}, \ldots, 99_{W_w} \}, p \in \{ 0_{L_{80}}, \ldots, 80_{L_{80}} \} \} \\
    I^\times & = \{ (0_{W_w}, 0_{L_{80}}) \} \\
    F^\times & = \{ (99_{W_w}, p) \mid p \in \{ 0_{L_{80}}, \ldots, 80_{L_{80}} \} \} \\
    E^\times & = \{ ((i, q), w_i, w_i, (i + 1, q + 1)) \mid q \in Q \mysetminus \{ 80 \}, i \in Q \mysetminus \{ 99 \} \} \\
             & \cup \{ ((80, 80), \text{\tt \textbackslash n}, \text{\tt \textbackslash n}, (81, 0)) \}
  \end{align*}

  Siehe auch Abbildung~\ref{fig:l80timesw100}.

  \begin{figure}[h]
    \centering
    \begin{tikzpicture}[->,auto,node distance=5cm]
      \node[initial,state] (0) {$0_{W_w}\, 0_{L_{80}}$};
      \node[] (rest1) [right of=0] {$\ldots$};
      \node[state] (80) [right of=rest1] {$80_{W_w}\, 80_{L_{80}}$};
      \node[state] (81) [below of=0] {$81_{W_w}\, 0_{L_{80}}$};
      \node[] (rest2) [right of=81] {$\ldots$};
      \node[state,accepting] (99) [right of=rest2] {$99_{W_w}\, 19_{L_{80}}$};

      \path (0) edge node {$(1, 1)$} (rest1)
            (rest1) edge node {$(80, 80)$} (80)
            (80) edge node {$(\text{\tt \textbackslash n}, \text{\tt \textbackslash n})$} (81)
            (81) edge node {$(81, 81)$} (rest2)
            (rest2) edge node {$(98, 98)$} (99);
    \end{tikzpicture}

    \caption{\label{fig:l80timesw100} Die Einschränkung des Automaten aus Abbildung \ref{fig:linebreak} auf das Wort aus Abbildung \ref{fig:w100}}
  \end{figure}
\end{eg}

\begin{rem}
  Es ist bemerkenswert, dass in Beispiel \ref{eg:l80timesw100} die Zirkuläre Struktur von $L_{80}$ durch Produkt mit einem Wort verloren geht.

  I.\@A.\@ ist das Produkt eines beliebigen FST mit einem Wort-FST zwar nicht azyklisch, erbt jedoch die lineare Struktur des Wort-FST in dem Sinne, dass Fortschritt in Richtung der akzeptierenden Zustände nur möglich ist indem der $(i, \sigma, w_i, i + 1)$-Klasse von Transitionen des Wort-FSTs gefolgt wird.
\end{rem}
  
\begin{comment}
\begin{code}
restrictOutput out FST{..} = FST
  { stInitial    = Set.mapMonotonic (0,) stInitial
  , stAccept     = Set.mapMonotonic (l,) stAccept
  , stTransition = Map.filter (not . Set.null) $ Map.fromList (concatMap noProgress $ Map.toList stTransition) `Map.union` Map.fromSet transitions (Set.fromDistinctAscList [((wSt, inSt), inSym) | wSt <- Set.toAscList wordStates, (inSt, inSym) <- Set.toAscList $ Map.keysSet stTransition])
  }
  where
    l :: Natural
    l = fromIntegral $ Seq.length out
    wordStates :: Set Natural
    wordStates
      | Seq.null out = Set.empty
      | otherwise = Set.fromDistinctAscList [0..pred l]
    noProgress :: ((state, Maybe input), Set (state, Maybe output)) -> [(((Natural, state), Maybe input), Set ((Natural, state), Maybe output))]
    noProgress ((inSt, inSym), outs)
      = [ (((wState, inSt), inSym), Set.mapMonotonic (\(outSt, Nothing) -> ((wState, outSt), Nothing)) noOutput) | wState <- Set.toList wordStates, not $ Set.null noOutput ]
      where
        noOutput = Set.filter (\(_, outSym) -> isNothing outSym) outs
    transitions :: ((Natural, state), Maybe input) -> Set ((Natural, state), Maybe output)
    transitions ((l, inSt), inSym) = Set.fromDistinctAscList [ ((succ l, outSt), outSym) | (outSt, outSym@(Just _)) <- Set.toAscList $ stTransition ! (inSt, inSym), outSym == Seq.lookup (fromIntegral l) out ]
\end{code}
\end{comment}

\begin{comment}
\begin{code}
restrictFST :: forall state input output. (Ord state, Ord input, Ord output) => Set state -> FST state input output -> FST state input output
-- ^ @restrictFST states fst@ removes from @fst@ all states not in @states@ including transitions leading to or originating from them
restrictFST sts FST{..} = FST
  { stInitial    = stInitial `Set.intersection` sts
  , stAccept     = stAccept  `Set.intersection` sts
  , stTransition = Map.mapMaybeWithKey restrictTransition stTransition
  }
  where
    restrictTransition :: (state, Maybe input) -> Set (state, Maybe output) -> Maybe (Set (state, Maybe output))
    restrictTransition (st, _) tos = tos' <$ guard (st `Set.member` sts)
      where
        tos' = Set.filter (\(st', _) -> st' `Set.member` sts) tos
      

liveFST :: forall state input output. (Ord state, Ord input, Ord output, Show state) => FST state input output -> Set state
-- ^ Compute the set of "live" states (with no particular complexity)
--
-- A state is "live" iff there is a path from it to an accepting state and a path from an initial state to it
liveFST fst@FST{..} = flip execState (Set.empty) . depthSearch Set.empty $ Set.toList stInitial
  where
    stTransition' :: Map state (Set state)
    stTransition' = Map.map (Set.map (\(st, _) -> st)) $ Map.mapKeysWith Set.union (\(st, _) -> st) stTransition
    depthSearch :: Set state -> [state] -> State (Set state) ()
    depthSearch acc [] = return ()
    depthSearch acc (curr : queue) = do
      let acc' = Set.insert curr acc
          next = fromMaybe Set.empty $ stTransition' !? curr
      alreadyLive <- get
      when (curr `Set.member` Set.union stAccept alreadyLive) $
        modify $ Set.union acc'
      depthSearch acc' $ filter (not . flip Set.member next) queue ++ Set.toList (next `Set.difference` acc')

dotFST :: forall state input output. (Ord state, Ord input, Ord output, Show state, Show input, Show output) => FST state input output -> Dot ()
dotFST FST{..} = do
  let
    stTransition' = concatMap (\(f, ts) -> (f,) <$> Set.toList ts) $ Map.toList stTransition
    states = stInitial <> stAccept <> foldMap (Set.singleton . fst . fst) stTransition' <> foldMap (Set.singleton . fst . snd) stTransition'
  stateIds <- sequence . (flip Map.fromSet) states $ \st -> node
    [ ("label", show st)
    , ("peripheries", bool "1" "2" $ st `Set.member` stAccept)
    ]
  forM_ stInitial $ \st -> do
    init <- node [ ("label", ""), ("shape", "none") ]
    init .->. (stateIds ! st)
  forM_ stTransition' $ \((f, inS), (t, outS)) -> do
    edge (stateIds ! f) (stateIds ! t)
      [ ("label", show (inS, outS))
      ]
\end{code}
\end{comment}