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/Lens.lhs | 110 +++++++++++++++++++++++++++++------- 1 file changed, 91 insertions(+), 19 deletions(-) (limited to 'edit-lens/src/Control/DFST') 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} -- cgit v1.2.3