diff options
Diffstat (limited to 'edit-lens/src/Control/DFST')
-rw-r--r-- | edit-lens/src/Control/DFST/Lens.lhs | 110 |
1 files changed, 91 insertions, 19 deletions
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 @@ | |||
1 | \begin{code} | 1 | \begin{code} |
2 | {-# LANGUAGE ScopedTypeVariables | 2 | {-# LANGUAGE ScopedTypeVariables |
3 | , TemplateHaskell | 3 | , TemplateHaskell |
4 | , ConstraintKinds | ||
4 | #-} | 5 | #-} |
5 | 6 | ||
6 | module Control.DFST.Lens | 7 | module Control.DFST.Lens |
@@ -42,9 +43,10 @@ import qualified Data.Algorithm.Diff as Diff | |||
42 | 43 | ||
43 | import Data.Monoid | 44 | import Data.Monoid |
44 | import Data.Bool (bool) | 45 | import Data.Bool (bool) |
45 | import Data.Maybe (fromMaybe) | 46 | import Data.Maybe (fromMaybe, maybeToList, listToMaybe) |
46 | import Data.Function (on) | 47 | import Data.Function (on) |
47 | import Data.Foldable (toList) | 48 | import Data.Foldable (toList) |
49 | import Data.List (partition) | ||
48 | 50 | ||
49 | import Debug.Trace | 51 | import Debug.Trace |
50 | 52 | ||
@@ -65,22 +67,35 @@ stringEdits :: Traversal' (StringEdits char) (StringEdit char) | |||
65 | stringEdits = _StringEdits . traverse | 67 | stringEdits = _StringEdits . traverse |
66 | 68 | ||
67 | affected :: forall char. StringEdits char -> Maybe (Interval Natural) | 69 | affected :: forall char. StringEdits char -> Maybe (Interval Natural) |
68 | -- ^ For a given set of edits @es@ return the interval @i = a ... b@ such that for any given string @str@ the following holds: | 70 | -- ^ 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: |
69 | -- | 71 | -- |
70 | -- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@ | 72 | -- - For all @n :: Natural@: @n < a ==> str ! n == (str `apply` es) ! n@ |
71 | -- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@ | 73 | -- - There exists a @k :: Integer@ such that for all @n :: Integer@: @n > b ==> str ! (n + k) == (str `apply` es) ! n@ |
72 | -- | 74 | -- |
73 | -- TODO | 75 | -- 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@. |
74 | affected SEFail = Nothing | 76 | affected SEFail = Nothing |
75 | affected (StringEdits es) = Just $ go es Map.empty | 77 | affected (StringEdits es) = Just . toInterval $ go es Map.empty |
76 | where | 78 | where |
77 | go :: Seq (StringEdit char) -> Map Natural Integer -> Interval Natural | 79 | toInterval :: Map Natural Integer -> Interval Natural |
78 | go Seq.Empty _ = Int.empty | 80 | toInterval map |
79 | go (es :> e) offsets = traceShow offsets $ Int.hull (Int.singleton p') $ go es offsets' | 81 | | Just (((minK, _), _), ((maxK, _), _)) <- (,) <$> Map.minViewWithKey map <*> Map.maxViewWithKey map |
82 | = let | ||
83 | maxV' = maximum . (0 :) $ do | ||
84 | offset <- [0..maxK] | ||
85 | v <- maybeToList $ Map.lookup (maxK - offset) map | ||
86 | v' <- maybeToList . fmap fromInteger $ negate v <$ guard (v <= 0) | ||
87 | guard $ v' >= succ offset | ||
88 | return $ v' - offset | ||
89 | in (minK Int.... maxK + maxV') | ||
90 | | otherwise | ||
91 | = Int.empty | ||
92 | go :: Seq (StringEdit char) -> Map Natural Integer -> Map Natural Integer | ||
93 | go Seq.Empty offsets = offsets | ||
94 | go (es :> e) offsets = go es offsets' | ||
80 | where | 95 | where |
81 | p = e ^. sePos | 96 | p = e ^. sePos |
82 | p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets | 97 | p' = fromIntegral $ Map.foldrWithKey (\k o p -> bool (fromIntegral p) (o + p) $ k < fromIntegral p) (fromIntegral p) offsets |
83 | offsets' = Map.alter ((\i -> i <$ guard (i /= 0)) . myOffset . fromMaybe 0) p offsets | 98 | offsets' = Map.alter (Just . myOffset . fromMaybe 0) p offsets |
84 | myOffset :: Integer -> Integer | 99 | myOffset :: Integer -> Integer |
85 | myOffset | 100 | myOffset |
86 | | Insert _ _ <- e = pred | 101 | | Insert _ _ <- e = pred |
@@ -174,7 +189,11 @@ type DFSTComplement state input output = Compositions (DFSTAction state input ou | |||
174 | runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output) | 189 | runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output) |
175 | runDFSTAction' = runDFSTAction . Comp.composed | 190 | runDFSTAction' = runDFSTAction . Comp.composed |
176 | 191 | ||
177 | dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output) | 192 | type Debug state input output = (Show state, Show input, Show output) |
193 | |||
194 | type LState state input output = (Natural, (state, Maybe (input, Natural))) | ||
195 | |||
196 | 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) | ||
178 | dfstLens dfst@DFST{..} = EditLens ground propR propL | 197 | dfstLens dfst@DFST{..} = EditLens ground propR propL |
179 | where | 198 | where |
180 | ground :: DFSTComplement state input output | 199 | ground :: DFSTComplement state input output |
@@ -185,28 +204,81 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL | |||
185 | propR (c, StringEdits Seq.Empty) = (c, mempty) | 204 | propR (c, StringEdits Seq.Empty) = (c, mempty) |
186 | propR (c, StringEdits (es :> e)) | 205 | propR (c, StringEdits (es :> e)) |
187 | | fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'') | 206 | | fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'') |
188 | | otherwise = (c', SEFail) | 207 | | otherwise = (c', SEFail) |
189 | where | 208 | where |
190 | (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c | 209 | (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c |
191 | cSuffix' | 210 | cSuffix' |
192 | | Delete _ <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe | 211 | | Delete _ <- e = Comp.take (pred $ Comp.length cSuffix) cSuffix -- TODO unsafe |
193 | | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) Seq.empty) | 212 | | Insert _ nChar <- e = cSuffix <> Comp.singleton (DFSTAction $ \x -> runDFST' dfst x (pure nChar) Seq.empty) |
194 | (pState, pOutput) = runDFSTAction (Comp.composed cPrefix) stInitial | 213 | (pState, pOutput) = runDFSTAction' cPrefix stInitial |
195 | (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState | 214 | (_, sOutput ) = runDFSTAction' cSuffix pState |
196 | (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState | 215 | (_, sOutput') = runDFSTAction' cSuffix' pState |
197 | (c', es') = propR (cSuffix' <> cPrefix, StringEdits es) | 216 | (c', es') = propR (cSuffix' <> cPrefix, StringEdits es) |
198 | es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput | 217 | es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput |
199 | 218 | ||
200 | 219 | ||
201 | propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input) | 220 | propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input) |
202 | propL (c, SEFail) = (c, SEFail) | ||
203 | propL (c, StringEdits Seq.Empty) = (c, mempty) | 221 | propL (c, StringEdits Seq.Empty) = (c, mempty) |
204 | propL (c, es) = fromMaybe (c, SEFail) $ do | 222 | propL (c, es) = fromMaybe (c, SEFail) $ do |
205 | newOut <- prevOut `apply` es | 223 | newOut <- prevOut `apply` es |
206 | let outFST = wordFST newOut `productFST` toFST dfst | 224 | affected' <- affected es |
207 | return undefined | 225 | let outFST :: FST (LState state input output) input output |
226 | outFST = wordFST newOut `productFST` toFST dfst | ||
227 | inflate by int | ||
228 | | Int.null int = Int.empty | ||
229 | | inf >= by = inf - by Int.... sup + by | ||
230 | | otherwise = 0 Int.... sup + by | ||
231 | where | ||
232 | (inf, sup) = (,) <$> Int.inf <*> Int.sup $ int | ||
233 | fragmentIntervals = (++ [all]) . takeWhile (not . Int.isSubsetOf (0 Int.... max)) $ inflate <$> 0 : [ 2^n | n <- [0..ceiling (logBase 2.0 max)] ] <*> pure affected' | ||
234 | where | ||
235 | max :: Num a => a | ||
236 | max = fromIntegral $ Seq.length newOut | ||
237 | all = 0 Int.... max | ||
238 | runCandidates :: Interval Natural -- ^ Departure from complement-run only permitted within interval (to guarantee locality) | ||
239 | -> [(Seq ((Natural, (state, Maybe (input, Natural))), Maybe output), StringEdits input)] | ||
240 | runCandidates ((,) <$> Int.inf <*> Int.sup -> (fInf, fSup)) = continueRun (Seq.empty, mempty) c | ||
241 | where | ||
242 | continueRun :: (Seq (LState state input output, Maybe output), StringEdits input) | ||
243 | -> DFSTComplement state input output | ||
244 | -> [(Seq (LState state input output, Maybe output), StringEdits input)] | ||
245 | continueRun (run, inEdits) c' = do | ||
246 | let | ||
247 | current :: LState state input output | ||
248 | current | ||
249 | | Seq.Empty <- run = (0, (stInitial, Nothing)) | ||
250 | | (_ :> (st, _)) <- run = st | ||
251 | current' :: state | ||
252 | current' = let (_, (st, _)) = current | ||
253 | in st | ||
254 | (c'', step) = Comp.splitAt (pred $ Comp.length c') c' -- TODO: unsafe | ||
255 | pos :: Natural | ||
256 | pos = fromIntegral $ Comp.length c - Comp.length c' | ||
257 | next' :: state | ||
258 | next' = fst . runDFSTAction' step $ current' | ||
259 | outgoing :: LState state input output -> [(LState state input output, Maybe input, Maybe output)] | ||
260 | outgoing current = let go (st, minS) os acc | ||
261 | | st == current = ($ acc) $ Set.fold (\(st', moutS) -> (. ((st', minS, moutS) :))) id os | ||
262 | | otherwise = acc | ||
263 | in Map.foldrWithKey go [] $ FST.stTransition outFST | ||
264 | isPreferred :: (LState state input output, Maybe input, Maybe output) -> Bool | ||
265 | isPreferred ((_, (st, Nothing)), _, _) = st == next' | ||
266 | isPreferred (st, _, _) = any isPreferred $ outgoing st | ||
267 | (preferred, alternate) = partition isPreferred $ outgoing current | ||
268 | options | ||
269 | | pos >= fInf = preferred ++ alternate | ||
270 | | otherwise = preferred | ||
271 | (next, inS, outS) <- options | ||
272 | let acc = (run :> (next, outS), undefined {- TODO -}) | ||
273 | bool id (acc :) (next `Set.member` FST.stAccept outFST) $ continueRun acc c'' | ||
274 | |||
275 | |||
276 | -- Properties of the edits computed are determined mostly by the order candidates are generated below | ||
277 | chosenRun <- listToMaybe . (\x -> trace (show $ map fst x) x) $ fragmentIntervals >>= runCandidates | ||
278 | |||
279 | return $ traceShow chosenRun undefined | ||
208 | where | 280 | where |
209 | (_, prevOut) = runDFSTAction (Comp.composed c) stInitial | 281 | (_, prevOut) = runDFSTAction' c stInitial |
210 | 282 | ||
211 | strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym | 283 | strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym |
212 | -- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@ | 284 | -- ^ @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 | |||
214 | where | 286 | where |
215 | toEdit :: Diff sym -> (Natural, StringEdits sym) -> (Natural, StringEdits sym) | 287 | toEdit :: Diff sym -> (Natural, StringEdits sym) -> (Natural, StringEdits sym) |
216 | toEdit (Diff.Both _ _) (n, es) = (succ n, es) | 288 | toEdit (Diff.Both _ _) (n, es) = (succ n, es) |
217 | toEdit (Diff.First _ ) (n, es) = (succ n, delete n <> es) | 289 | toEdit (Diff.First _ ) (n, es) = (n, delete n <> es) |
218 | toEdit (Diff.Second c) (n, es) = (succ (succ n), insert n c <> es) | 290 | toEdit (Diff.Second c) (n, es) = (succ n, insert n c <> es) |
219 | \end{code} | 291 | \end{code} |