Work on propL

1 files changed, 91 insertions, 19 deletions

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}