Work on container transducers

1 files changed, 133 insertions, 6 deletions

diff --git a/edit-lens/src/Control/Edit/Container/Transducer.lhs b/edit-lens/src/Control/Edit/Container/Transducer.lhs
index 0173cc4..9db26db 100644
--- a/edit-lens/src/Control/Edit/Container/Transducer.lhs
+++ b/edit-lens/src/Control/Edit/Container/Transducer.lhs
@@ -1,8 +1,8 @@
 \begin{code}
-{-# LANGUAGE TemplateHaskell #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 
 module Control.Edit.Container.Transducer
-  ( ContainerTransducer{..}, ctStates
+  ( ContainerTransducer(..), ctStates
   , runCT, stepCT
   ) where
 
@@ -11,6 +11,8 @@ 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
   
@@ -19,8 +21,10 @@ 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
@@ -53,11 +57,134 @@ runCT ct@ContainerTransducer{ ctInitialState } input = runRWS (forMOf_ container
 \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
 
-data CTComplement state input output = CTComplement
-  {
-  }
+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 ]
 
--- Define edit-lens as span
+\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}