From 890414175e966bcf7c41dcd4b544bf4af3e6ae8d Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Mon, 18 Jun 2018 11:38:58 +0200 Subject: Work on propL --- edit-lens/src/Control/DFST.lhs | 2 - edit-lens/src/Control/DFST/Lens.lhs | 110 +++++++++++++++++++++++++++++------- edit-lens/src/Control/FST.lhs | 53 ++++++++++++++++- 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 -- cgit v1.2.3