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

module Control.Edit.Container.Transducer
  ( ContainerTransducer(..), ctStates
  , runCT, stepCT
  ) where

import Control.Edit.Container
import Data.Map.Strict (Map, (!?))
import qualified Data.Map.Strict as Map
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Sequence (Seq(..), (><))
import qualified Data.Sequence as Seq

import Control.Monad.RWS.Strict
  
import Control.Monad.Writer.Class
import Control.Monad.Reader.Class
import Control.Monad.State.Class

import Control.Lens
import Control.Lens.Edit

import Data.Maybe
import Data.Foldable


data ContainerTransducer state input output = ContainerTransducer
  { ctInitialState :: state
  , ctTransition :: Map (state, Content input) (ContainerEdits output, state)
    -- ^ States are stable (and produce no output) by default
  }

ctStates :: Ord state => ContainerTransducer state input output -> Set state
ctStates ContainerTransducer{..} = Map.foldrWithKey' (\(s1, _) (_, s2) -> Set.insert s1 . Set.insert s2) (Set.singleton ctInitialState) ctTransition

stepCT :: ( Ord state, Ord (Content input)
          , MonadReader (ContainerTransducer state input output) m
          , MonadState state m
          , MonadWriter (ContainerEdits output) m
          ) => Content input -> m ()
stepCT x = do
  ContainerTransducer{ ctTransition } <- ask
  state <- get
  let (output, newState) = fromMaybe (mempty, state) $ ctTransition !? (state, x)
  put newState
  tell output

runCT :: ( Ord state, Ord (Content input)
         , FoldableContainer input
         ) => ContainerTransducer state input output
           -> input
           -> ContainerEdits output
runCT ct@ContainerTransducer{ ctInitialState } input = runRWS (forMOf_ containerContent input stepCT) ct ctInitialState ^. _3
\end{code}

\begin{code}
class Ord a => HasRanges a where
  data Range a :: *
  bounds :: Getter (Range a) (a, a)
  range :: Iso' (Set a) (Range a)
  within :: a -> Range a -> Bool
  within x xs = Set.member x $ xs ^. from range
  below :: a -> Range a -> Bool
  below x xs = x < min
    where (min, _) = xs ^. bounds
  above :: a -> Range a -> Bool
  above x xs = x > max
    where (_, max) = xs ^. bounds
  insert :: Range a -> a -> Range a
  insert xs x = xs & under range (Set.insert x)
  singleton :: a -> Range a
  singleton = view range . Set.singleton

type PositionAction state output = Map state (ContainerEdits output, state)
  
data ContainerAction state input output
  = CALeaf { caPos :: Position input
           , caContent :: Content input
           , caAction :: PositionAction state output
           , caOutputPos :: Range Natural
           }
  | CABranch { caRange :: Range (Position input)
             , caAction :: PositionAction state output
             , caLeft :: ContainerAction state input output
             , caRight :: ContainerAction state input output
             , caOutputPos :: Range Natural
             }
  | CATip

-- type ContainerAction state input output = Map ((Position input, Seq (Content input), Position input)) (Map state (ContainerEdits output, state))

instance HasRanges Natural where
  data Range Natural = NatInterval Natural Natural -- @NatInterval x y@ is the interval of natural numbers z such that x <= z < y
                     | NatSet (Set Natural)
  bounds = to bounds'
    where
      bounds' (NatInterval min max) = (min, max)
      bounds' (NatSet set) = (Set.findMin set, Set.findMax set)
  range = iso fromSet toSet
    where
      fromSet set
        | Set.null set = NatInterval 0 0
        | otherwise = Set.foldl' insert (Set.empty ^. range) set
      toSet (NatInterval x y)
        | x < y = Set.fromAscList [x..pred y]
        | otherwise = Set.empty
  insert i@(NatInterval x y) z
    | x < y
    , z == pred x = NatInterval z y
    | x < y
    , z == succ y = NatInterval x z
    | x >= y = NatInterval z (succ z)
    | otherwise = NatSet $ (i ^. from range) `Set.union` Set.singleton z
  insert (NatSet set) z = fromMaybe (NatSet $ Set.insert z set) $ foldlM insert' (NatInterval 0 0) set
    where
      insert' r x = case insert r x of
        r'@(NatInterval _ _) -> Just r
        _ -> Nothing

caRange' :: HasRanges (Position input) => ContainerAction state input output -> Range (Position input)
caRange' (CALeaf tPos _ _) = singleton tPos
caRange' (CABranch r _ _ _) = r
caRange' CATip = Set.empty ^. range

caAction' :: ContainerAction state input output -> PositionAction state output
caAction' CATip = Map.empty
caAction' x = caAction x

conc :: Ord state
     => PositionAction state output
     -> PositionAction state output
     -> PositionAction state output
f `conc` g = Map.fromList [ (st, fromMaybe (mempty, st') $ f !? st') | (st, x@(_, st')) <- Map.toAscList g ]

\end{code}

Für die Zwecke eines Container-Transducers sehen wir Container als eine Sequenz von edits auf $\text{init}$.

Das Komplement der transducer-edit-linse ist ein binärbaum dessen Zweige beschriftet sind mit der vom Teilbaum betrachteten input Container-Positionen, der Wirkung des gesamten Teilbaums (d.h. die Transitionsfunktion für den Zustand und den produzierten Output (eine Teilsequenz der edits des output containers)), und den betroffenen output Positionen.
Die Blätter beschriften wir mit einer einzigen betrachteten Position im input-Container, dem beim verarbeiten angetroffenen Inhalt, der Wirkung dieses konkreten Inhalts, und den betroffenen output Positionen.

Zur Verarbeitung eines edits auf dem input lokalisieren wir zunächst dessen Wirkung in unserem Komplement-Baum.
Handelt es sich um einen edit auf einer Position im input können wir für das betroffene Blatt eine neue Wirkung berechnen, anhand der Transitionsfunktion des transducers und dem im komplement gespeicherten alten Wert.
Wir können nun nicht vermeiden von den output edits zu fordern eine Gruppe zu sein, da wir gezwungen sind einen edit zu produzieren, der auf dem Resultat des vorherigen Laufes, zumindest den alten, bei der betroffenen transition edit rückgängig zu machen.

Beweisskizze:
 Betrachte als input den trivialen container mit nur einer shape und darin belegten position.
 Als edits auf dem Inhalt jenes containers nehmen wir Replace.
 Nimm $e_o$ einen edit auf dem output-Container.
 Obda ist $e_o$ die Wirkung von $\text{Replace}(c)$ unter $\text{diffContTrans}$ auf $(\text{init}, \text{init_C}, \text{init})$ (Konstruiere hierfür einen geeigneten Transducer)
 Betrachte nun $\text{Replace}(c)$ gefolgt von $\text{Replace}(\text{init})$ unter $\text{diffContTrans}$ auf $\text{init}$.
 Für das Ergebnis $e_o^{-1}$ muss gelten, dass $e_o^{-1} \circ e_o = \text{id}$.
 Wir haben also Inverse für beliebige Elemente des edit-monoiden auf dem Output; also eine Gruppe auf edits auf dem Output die kompatibel ist mit der bestehenden monoid struktur.
 
\begin{code}
diffContTrans :: forall state input output.
                 ( Container input, Container output
                 , Ord state, Ord (Content input)
                 , HasRanges (Position input)
                 )
              => ContainerTransducer state input output
              -> EditLens (ContainerAction state input output) (ContainerEdits input) (ContainerEdits output)
diffContTrans ContainerTransducer{..} = EditLens CATip forward backward
  where
    forward (cAct, Seq.Empty) = (cAct, Seq.empty)
    forward (cAct, xs) = foldr' (\x (cAct', ys) -> over _2 (ys ><) $ go cAct' x) (cAct, Seq.empty) xs
      where
        go :: ContainerAction state input output
           -> ContainerEdit input
           -> (ContainerAction state input output, ContainerEdits output)
        go ca Fail = (ca, Seq.singleton Fail)
        go CATip _ = (CATip, mempty)
        go ca@(CALeaf tPos content pAct) (ModContent pos cEdit)
          | pos == tPos
          , Just content' <- content `apply` cEdit
          = (CALeaf tPos content' $ Map.fromAscList [ (s, a) | ((s, c), a) <- Map.toAscList ctTransition, c == content' ], undefined)
          | otherwise = (ca, Seq.singleton Fail)
        go ca@(CABranch range act left right) e@(ModContent pos _)
          | pos `within` caRange' left
          = let (left', es) = go left e in (CABranch range (caAction' right `conc` caAction' left') left' right, es)
          | pos `within` caRange' right
          = let (right', es) = go right e in (CABranch range (caAction' right' `conc` caAction' left) left right', es)
          | otherwise = (ca, Seq.singleton Fail)
        go cAct (ModShape cShape perm) = undefined

    backward = undefined
\end{code}