From db70fb1c2dfe059c662fed9731bc9dd7ee380114 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Tue, 22 May 2018 15:31:08 +0200 Subject: Work on propL --- edit-lens/src/Control/DFST/Lens.lhs | 57 ++++++++++++++++++++++++++++++++++--- edit-lens/src/Control/FST.lhs | 24 ++++++++-------- 2 files changed, 65 insertions(+), 16 deletions(-) (limited to 'edit-lens/src') 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} -- cgit v1.2.3