summaryrefslogtreecommitdiff
path: root/edit-lens/src/Control/DFST
diff options
context:
space:
mode:
Diffstat (limited to 'edit-lens/src/Control/DFST')
-rw-r--r--edit-lens/src/Control/DFST/Lens.lhs110
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
6module Control.DFST.Lens 7module Control.DFST.Lens
@@ -42,9 +43,10 @@ import qualified Data.Algorithm.Diff as Diff
42 43
43import Data.Monoid 44import Data.Monoid
44import Data.Bool (bool) 45import Data.Bool (bool)
45import Data.Maybe (fromMaybe) 46import Data.Maybe (fromMaybe, maybeToList, listToMaybe)
46import Data.Function (on) 47import Data.Function (on)
47import Data.Foldable (toList) 48import Data.Foldable (toList)
49import Data.List (partition)
48 50
49import Debug.Trace 51import Debug.Trace
50 52
@@ -65,22 +67,35 @@ stringEdits :: Traversal' (StringEdits char) (StringEdit char)
65stringEdits = _StringEdits . traverse 67stringEdits = _StringEdits . traverse
66 68
67affected :: forall char. StringEdits char -> Maybe (Interval Natural) 69affected :: 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@.
74affected SEFail = Nothing 76affected SEFail = Nothing
75affected (StringEdits es) = Just $ go es Map.empty 77affected (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
174runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output) 189runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output)
175runDFSTAction' = runDFSTAction . Comp.composed 190runDFSTAction' = runDFSTAction . Comp.composed
176 191
177dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output) 192type Debug state input output = (Show state, Show input, Show output)
193
194type LState state input output = (Natural, (state, Maybe (input, Natural)))
195
196dfstLens :: 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)
178dfstLens dfst@DFST{..} = EditLens ground propR propL 197dfstLens 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
211strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym 283strDiff :: 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}