Work on propL

3 files changed, 142 insertions, 23 deletions

diff --git a/edit-lens/src/Control/DFST.lhs b/edit-lens/src/Control/DFST.lhs
index 9bd1629..eae2e66 100644
--- a/edit-lens/src/Control/DFST.lhs
+++ b/edit-lens/src/Control/DFST.lhs
@@ -41,8 +41,6 @@ data DFST state input output = DFST
 
 toFST :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> FST (state, Maybe (input, Natural)) input output
 -- ^ Split apart non-singleton outputs into a series of epsilon-transitions
---
--- This function is currently invalid since multiple out-edges in the `DFST` visit the same intermediate states (we should label intermediate states not only with an ordinal but also with the input Symbol from the `DFST`)
 toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) handleTransition
   where
     initialFST = FST
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index eafa458..35a7d38 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -1,6 +1,7 @@
 \begin{code}
 {-# LANGUAGE ScopedTypeVariables
            , TemplateHaskell
+           , ConstraintKinds
 #-}
 
 module Control.DFST.Lens
@@ -42,9 +43,10 @@ import qualified Data.Algorithm.Diff as Diff
 
 import Data.Monoid
 import Data.Bool (bool)
-import Data.Maybe (fromMaybe)
+import Data.Maybe (fromMaybe, maybeToList, listToMaybe)
 import Data.Function (on)
 import Data.Foldable (toList)
+import Data.List (partition)
 
 import Debug.Trace
 
@@ -65,22 +67,35 @@ stringEdits :: Traversal' (StringEdits char) (StringEdit char)
 stringEdits = _StringEdits . traverse
 
 affected :: forall char. StringEdits char -> Maybe (Interval Natural)
--- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ the following holds:
+-- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ of sufficient length the following holds:
 --
 --   - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@
 --   - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@
 --
--- TODO
+-- Intuitively: for any character @c@ of the new string @str `apply` es@ there exists a corresponding character in @str@ (offset by either 0 or a constant shift @k@) if the index of @c@ is /not/ contained in @affected es@.
 affected SEFail = Nothing
-affected (StringEdits es) = Just $ go es Map.empty
+affected (StringEdits es) = Just . toInterval $ go es Map.empty
   where
-    go :: Seq (StringEdit char) -> Map Natural Integer -> Interval Natural
-    go Seq.Empty _       = Int.empty
-    go (es :> e) offsets = traceShow offsets $ Int.hull (Int.singleton p') $ go es offsets'
+    toInterval :: Map Natural Integer -> Interval Natural
+    toInterval map
+      | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map
+      = let
+          maxV' = maximum . (0 :) $ do
+            offset <- [0..maxK]
+            v <- maybeToList $ Map.lookup (maxK - offset) map
+            v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0)
+            guard $ v' >= succ offset
+            return $ v' - offset
+        in (minK Int.... maxK + maxV')
+      | otherwise
+      = Int.empty
+    go :: Seq (StringEdit char) -> Map Natural Integer -> Map Natural Integer
+    go Seq.Empty offsets = offsets
+    go (es :> e) offsets = go es offsets'
       where
         p = e ^. sePos
         p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets
-        offsets' = Map.alter ((\i -> i <$ guard (i /= 0)) . myOffset . fromMaybe 0) p offsets
+        offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets
         myOffset :: Integer -> Integer
         myOffset
           | Insert _ _ <- e = pred
@@ -174,7 +189,11 @@ type DFSTComplement state input output = Compositions (DFSTAction state input ou
 runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output)
 runDFSTAction' = runDFSTAction . Comp.composed
 
-dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output)
+type Debug state input output = (Show state, Show input, Show output)
+
+type LState state input output = (Natural, (state, Maybe (input, Natural)))
+
+dfstLens :: forall state input output. (Ord state, Ord input, Ord output, Debug state input output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output)
 dfstLens dfst@DFST{..} = EditLens ground propR propL
   where
     ground :: DFSTComplement state input output
@@ -185,28 +204,81 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
     propR (c, StringEdits Seq.Empty) = (c, mempty)
     propR (c, StringEdits (es :> e))
       | fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'')
-      | otherwise                                     = (c', SEFail)
+      | otherwise                                               = (c', SEFail)
       where
         (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
         cSuffix'
           | Delete _       <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe
           | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) Seq.empty)
-        (pState, pOutput)  = runDFSTAction (Comp.composed cPrefix) stInitial
-        (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState
-        (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState
+        (pState, pOutput)  = runDFSTAction' cPrefix stInitial
+        (_, sOutput ) = runDFSTAction' cSuffix  pState
+        (_, sOutput') = runDFSTAction' cSuffix' pState
         (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
         es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput
         
 
     propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
-    propL (c, SEFail) = (c, SEFail)
     propL (c, StringEdits Seq.Empty) = (c, mempty)
     propL (c, es) = fromMaybe (c, SEFail) $ do
       newOut <- prevOut `apply` es
-      let outFST = wordFST newOut `productFST` toFST dfst
-      return undefined
+      affected' <- affected es
+      let outFST :: FST (LState state input output) input output
+          outFST = wordFST newOut `productFST` toFST dfst
+          inflate by int
+            | Int.null int = Int.empty
+            | inf >= by = inf - by Int.... sup + by
+            | otherwise = 0 Int.... sup + by
+            where
+              (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int
+          fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected'
+            where
+              max :: Num a => a
+              max = fromIntegral $ Seq.length newOut
+              all = 0 Int.... max
+          runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality)
+                       -> [(Seq ((Natural, (state, Maybe (input, Natural))), Maybe output), StringEdits input)]
+          runCandidates ((,) <$> Int.inf <*> Int.sup -> (fInf, fSup)) = continueRun (Seq.empty, mempty) c
+            where
+              continueRun :: (Seq (LState state input output, Maybe output), StringEdits input)
+                          -> DFSTComplement state input output
+                          -> [(Seq (LState state input output, Maybe output), StringEdits input)]
+              continueRun (run, inEdits) c' = do
+                let
+                  current :: LState state input output
+                  current
+                    | Seq.Empty <- run      = (0, (stInitial, Nothing))
+                    | (_ :> (st, _)) <- run = st
+                  current' :: state
+                  current' = let (_, (st, _)) = current
+                              in st
+                  (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe
+                  pos :: Natural
+                  pos = fromIntegral $ Comp.length c - Comp.length c'
+                  next' :: state
+                  next' = fst . runDFSTAction' step $ current'
+                  outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)]
+                  outgoing current = let go (st, minS) os acc
+                                           | st == current = ($ acc) $ Set.fold (\(st', moutS) -> (. ((st', minS, moutS) :))) id os
+                                           | otherwise     = acc
+                                      in Map.foldrWithKey go [] $ FST.stTransition outFST 
+                  isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool
+                  isPreferred ((_, (st, Nothing)), _, _) = st == next'
+                  isPreferred (st, _, _) = any isPreferred $ outgoing st
+                  (preferred, alternate) = partition isPreferred $ outgoing current
+                  options
+                    | pos >= fInf = preferred ++ alternate
+                    | otherwise   = preferred
+                (next, inS, outS) <- options
+                let acc = (run :> (next, outS), undefined {- TODO -})
+                bool id (acc :) (next `Set.member` FST.stAccept outFST) $ continueRun acc c''
+                
+              
+      -- Properties of the edits computed are determined mostly by the order candidates are generated below
+      chosenRun <- listToMaybe . (\x -> trace (show $ map fst x) x) $ fragmentIntervals >>= runCandidates
+      
+      return $ traceShow chosenRun undefined
       where
-        (_, prevOut) = runDFSTAction (Comp.composed c) stInitial
+        (_, prevOut) = runDFSTAction' c stInitial
 
 strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym
 -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@
@@ -214,6 +286,6 @@ strDiff a b = snd . foldr toEdit (0, mempty) $ (getDiff `on` toList) a b
   where
     toEdit :: Diff sym -> (Natural, StringEdits sym) -> (Natural, StringEdits sym)
     toEdit (Diff.Both _ _) (n, es) = (succ n, es)
-    toEdit (Diff.First _ ) (n, es) = (succ n, delete n <> es)
-    toEdit (Diff.Second c) (n, es) = (succ (succ n), insert n c <> es)
+    toEdit (Diff.First _ ) (n, es) = (n, delete n <> es)
+    toEdit (Diff.Second c) (n, es) = (succ n, insert n c <> es)
 \end{code}
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index 4f1f364..9298e11 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -24,11 +24,11 @@ import qualified Data.Set as Set
 import Data.Sequence (Seq)
 import qualified Data.Sequence as Seq
 
-import Data.Maybe (mapMaybe, fromMaybe)
+import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust)
 
 import Numeric.Natural
 
-import Control.Lens.TH
+import Control.Lens
 
 import Control.Monad.State.Strict
 
@@ -59,6 +59,55 @@ instance (Show state, Show input, Show output) => Pretty (FST state input output
       list :: [PP.Doc] -> PP.Doc
       list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space)
 
+runFST :: forall input output state. (Ord input, Ord output, Ord state) => FST state input output -> Seq input -> [Seq output]
+runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST'
+  where
+    catMaybes = fmap fromJust . Seq.filter isJust
+
+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 Seq.Empty = guardAccept $ (\(_, st, _) -> (st, Seq.Empty)) <$> step fst Nothing Nothing
+runFST' fst cs = guardAccept $ do
+  initial <- view _2 <$> step fst Nothing Nothing
+  go (initial, Seq.Empty) cs
+  where
+    guardAccept res = do
+      (initial, path) <- res
+      let
+        finalState
+          | (_ :> (st, _)) <- path = st
+          | otherwise              = initial
+      guard $ finalState `Set.member` stAccept
+      return res
+
+    go :: (state, Seq (state, Maybe output)) -> Seq input-> [(state, Seq (state, Maybe output))]
+    go (initial, path) cs = do
+      let
+        current
+          | (_ :> (st, _)) <- path = st
+          | otherwise              = initial
+      (head, next, out) <- step fst (Just current) (Seq.lookup 0 cs)
+      let
+        nPath = path :> (next, out)
+        ncs = maybe id (:<) head cs
+      go (initial, nPath) ncs
+      
+
+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
+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
+  
+
 wordFST :: forall input output. Seq output -> FST Natural input output
 -- ^ @wordFST str@ is the linear FST generating @str@ as output when given no input
 wordFST outs = FST