Work on propL

3 files changed, 66 insertions, 16 deletions

diff --git a/edit-lens/package.yaml b/edit-lens/package.yaml
index ec10b83..b506ec1 100644
--- a/edit-lens/package.yaml
+++ b/edit-lens/package.yaml
@@ -34,6 +34,7 @@ library:
     - Diff
     - mtl
     - wl-pprint
+    - intervals
   exposed-modules:
     - Control.Edit
     - Control.Lens.Edit
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@
diff --git a/edit-lens/src/Control/FST.lhs b/edit-lens/src/Control/FST.lhs
index d37072f..4f1f364 100644
--- a/edit-lens/src/Control/FST.lhs
+++ b/edit-lens/src/Control/FST.lhs
@@ -10,7 +10,7 @@ module Control.FST
   -- * Constructing FSTs
   , wordFST
   -- * Operations on FSTs
-  , productFST, invertFST, restrictFST
+  , productFST, restrictFST
   -- * Debugging Utilities
   , liveFST
   ) where
@@ -35,8 +35,6 @@ import Control.Monad.State.Strict
 import Text.PrettyPrint.Leijen (Pretty(..))
 import qualified Text.PrettyPrint.Leijen as PP
 
-import Debug.Trace
-
 data FST state input output = FST
   { stInitial :: Set state
   , stTransition :: Map (state, Maybe input) (Set (state, Maybe output))
@@ -45,7 +43,7 @@ data FST state input output = FST
 
 instance (Show state, Show input, Show output) => Pretty (FST state input output) where
   pretty FST{..} = PP.vsep
-    [ PP.text "Initial states:" PP.</> PP.hang 2 (PP.list . map (PP.text . show) $ Set.toAscList stInitial)
+    [ PP.text "Initial states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stInitial)
     , PP.text "State transitions:" PP.<$> PP.indent 2 (PP.vsep
         [        PP.text (show st)
           PP.<+> (PP.text "-" PP.<> PP.tupled [label inS, label outS] PP.<> PP.text "→")
@@ -53,14 +51,16 @@ instance (Show state, Show input, Show output) => Pretty (FST state input output
         | ((st, inS), to) <- Map.toList stTransition
         , (st', outS) <- Set.toAscList to
         ])
-    , PP.text "Accepting states:" PP.</> PP.hang 2 (PP.list . map (PP.text . show) $ Set.toAscList stAccept)
+    , PP.text "Accepting states:" PP.</> PP.hang 2 (list . map (PP.text . show) $ Set.toAscList stAccept)
     ]
     where
       label :: Show a => Maybe a -> PP.Doc
       label = maybe (PP.text "ɛ") (PP.text . show)
+      list :: [PP.Doc] -> PP.Doc
+      list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space)
 
 wordFST :: forall input output. Seq output -> FST Natural input output
--- ^ @wordFST str@ is the minimal FST generating @str@ as output when given no input
+-- ^ @wordFST str@ is the linear FST generating @str@ as output when given no input
 wordFST outs = FST
   { stInitial    = Set.singleton 0
   , stAccept     = Set.singleton l
@@ -77,7 +77,9 @@ wordFST outs = FST
 productFST :: forall state1 state2 input output. (Ord state1, Ord state2, Ord input, Ord output) => FST state1 input output -> FST state2 input output -> FST (state1, state2) input output
 -- ^ Cartesian product on states, logical conjunction on transitions and state-properties (initial and accept)
 --
--- This is most intuitive when thought of as the component-wise product of weighted FSTs with weights in the boolean semiring.
+-- This is the "natural" (that is component-wise) product when considering FSTs to be weighted in the boolean semiring.
+--
+-- Intuitively this corresponds to running both FSTs at the same time requiring them to produce the same output and "agree" (epsilon agreeing with every character) on their input.
 productFST fst1 fst2 = FST
   { stInitial    = stInitial fst1 `setProduct` stInitial fst2
   , stAccept     = stAccept fst1 `setProduct` stAccept fst2
@@ -99,6 +101,7 @@ productFST fst1 fst2 = FST
         out2 = (fromMaybe Set.empty $ stTransition fst2 !? (st2, inS)) `Set.union` (fromMaybe Set.empty $ stTransition fst2 !? (st2, Nothing))
 
 restrictFST :: forall state input output. (Ord state, Ord input, Ord output) => Set state -> FST state input output -> FST state input output
+-- ^ @restrictFST states fst@ removes from @fst@ all states not in @states@ including transitions leading to or originating from them
 restrictFST sts FST{..} = FST
   { stInitial    = stInitial `Set.intersection` sts
   , stAccept     = stAccept  `Set.intersection` sts
@@ -124,11 +127,8 @@ liveFST fst@FST{..} = flip execState Set.empty $ mapM_ (depthSearch Set.empty) s
       let acc' = Set.insert curr acc
           next = fromMaybe Set.empty $ stTransition' !? curr
       alreadyLive <- get
-      when (not . Set.null $ Set.insert curr next `Set.intersection` Set.union stAccept alreadyLive) $
+      when (curr `Set.member` Set.union stAccept alreadyLive) $
         modify $ Set.union acc'
+      alreadyLive <- get
       mapM_ (depthSearch acc') $ next `Set.difference` alreadyLive
-
-
-invertFST :: FST state input output -> Seq output -> Set (Seq input)
-invertFST = undefined
 \end{code}