From db70fb1c2dfe059c662fed9731bc9dd7ee380114 Mon Sep 17 00:00:00 2001
From: Gregor Kleen <gkleen@yggdrasil.li>
Date: Tue, 22 May 2018 15:31:08 +0200
Subject: Work on propL

---
 edit-lens/src/Control/DFST/Lens.lhs | 57 ++++++++++++++++++++++++++++++++++---
 1 file changed, 53 insertions(+), 4 deletions(-)

(limited to 'edit-lens/src/Control/DFST/Lens.lhs')

diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 0976314..eafa458 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -14,14 +14,25 @@ module Control.DFST.Lens
   ) where
 
 import Control.DFST
+import Control.FST hiding (stInitial, stTransition, stAccept)
+import qualified Control.FST as FST (stInitial, stTransition, stAccept)
 import Control.Lens.Edit
 import Control.Lens
 import Control.Lens.TH
 import Control.Edit
 
+import Control.Monad
+
 import Numeric.Natural
+import Numeric.Interval (Interval, (...))
+import qualified Numeric.Interval as Int
+
 import Data.Sequence (Seq((:<|), (:|>)))
 import qualified Data.Sequence as Seq
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Map (Map)
+import qualified Data.Map as Map
 
 import Data.Compositions.Snoc (Compositions)
 import qualified Data.Compositions.Snoc as Comp
@@ -30,9 +41,13 @@ import Data.Algorithm.Diff (Diff, getDiff)
 import qualified Data.Algorithm.Diff as Diff
 
 import Data.Monoid
+import Data.Bool (bool)
+import Data.Maybe (fromMaybe)
 import Data.Function (on)
 import Data.Foldable (toList)
 
+import Debug.Trace
+
 
 data StringEdit char = Insert { _sePos :: Natural, _seInsertion :: char }
                      | Delete { _sePos :: Natural }
@@ -49,6 +64,28 @@ makePrisms ''StringEdits
 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 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
+affected SEFail = Nothing
+affected (StringEdits es) = Just $ 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'
+      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
+        myOffset :: Integer -> Integer
+        myOffset
+          | Insert _ _ <- e = pred
+          | Delete _   <- e = succ
+
 insert :: Natural -> char -> StringEdits char
 insert n c = StringEdits .  Seq.singleton $ Insert n c
   
@@ -130,10 +167,13 @@ data DFSTAction state input output = DFSTAction { runDFSTAction :: state -> (sta
 
 instance Monoid (DFSTAction state input output) where
   mempty = DFSTAction $ \x -> (x, Seq.empty)
-  (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out <> out')
+  DFSTAction f `mappend` DFSTAction g = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out <> out')
 
 type DFSTComplement state input output = Compositions (DFSTAction state input output)
 
+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)
 dfstLens dfst@DFST{..} = EditLens ground propR propL
   where
@@ -142,7 +182,10 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
 
     propR :: (DFSTComplement state input output, StringEdits input) -> (DFSTComplement state input output, StringEdits output)
     propR (c, SEFail) = (c, SEFail)
-    propR (c, StringEdits (es :|> e)) = (c', es' <> es'')
+    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)
       where
         (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
         cSuffix'
@@ -153,11 +196,17 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
         (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState
         (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
         es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput
-    propR (c, StringEdits Seq.Empty) = (c, mempty)
         
 
     propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
-    propL = undefined
+    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
+      where
+        (_, prevOut) = runDFSTAction (Comp.composed 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@
-- 
cgit v1.2.3