diff options
-rw-r--r-- | edit-lens/src/Control/DFST.lhs | 2 | ||||
-rw-r--r-- | edit-lens/src/Control/DFST/Lens.lhs | 110 | ||||
-rw-r--r-- | 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 | |||
41 | 41 | ||
42 | toFST :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> FST (state, Maybe (input, Natural)) input output | 42 | toFST :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> FST (state, Maybe (input, Natural)) input output |
43 | -- ^ Split apart non-singleton outputs into a series of epsilon-transitions | 43 | -- ^ Split apart non-singleton outputs into a series of epsilon-transitions |
44 | -- | ||
45 | -- 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`) | ||
46 | toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) handleTransition | 44 | toFST DFST{..} = flip execState initialFST $ forM_ (Map.toList stTransition) handleTransition |
47 | where | 45 | where |
48 | initialFST = FST | 46 | 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 @@ | |||
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} |
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 | |||
24 | import Data.Sequence (Seq) | 24 | import Data.Sequence (Seq) |
25 | import qualified Data.Sequence as Seq | 25 | import qualified Data.Sequence as Seq |
26 | 26 | ||
27 | import Data.Maybe (mapMaybe, fromMaybe) | 27 | import Data.Maybe (mapMaybe, fromMaybe, isJust, fromJust) |
28 | 28 | ||
29 | import Numeric.Natural | 29 | import Numeric.Natural |
30 | 30 | ||
31 | import Control.Lens.TH | 31 | import Control.Lens |
32 | 32 | ||
33 | import Control.Monad.State.Strict | 33 | import Control.Monad.State.Strict |
34 | 34 | ||
@@ -59,6 +59,55 @@ instance (Show state, Show input, Show output) => Pretty (FST state input output | |||
59 | list :: [PP.Doc] -> PP.Doc | 59 | list :: [PP.Doc] -> PP.Doc |
60 | list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space) | 60 | list = PP.encloseSep (PP.lbracket PP.<> PP.space) (PP.space PP.<> PP.rbracket) (PP.comma PP.<> PP.space) |
61 | 61 | ||
62 | runFST :: forall input output state. (Ord input, Ord output, Ord state) => FST state input output -> Seq input -> [Seq output] | ||
63 | runFST = fmap (map $ catMaybes . fmap (view _2) . view _2) . runFST' | ||
64 | where | ||
65 | catMaybes = fmap fromJust . Seq.filter isJust | ||
66 | |||
67 | runFST' :: forall input output state. (Ord input, Ord output, Ord state) | ||
68 | => FST state input output | ||
69 | -> Seq input | ||
70 | -> [(state, Seq (state, Maybe output))] -- ^ Tuples of initial state and chosen transitions; not neccessarily finite | ||
71 | -- ^ Compute all possible runs on the given input | ||
72 | runFST' fst Seq.Empty = guardAccept $ (\(_, st, _) -> (st, Seq.Empty)) <$> step fst Nothing Nothing | ||
73 | runFST' fst cs = guardAccept $ do | ||
74 | initial <- view _2 <$> step fst Nothing Nothing | ||
75 | go (initial, Seq.Empty) cs | ||
76 | where | ||
77 | guardAccept res = do | ||
78 | (initial, path) <- res | ||
79 | let | ||
80 | finalState | ||
81 | | (_ :> (st, _)) <- path = st | ||
82 | | otherwise = initial | ||
83 | guard $ finalState `Set.member` stAccept | ||
84 | return res | ||
85 | |||
86 | go :: (state, Seq (state, Maybe output)) -> Seq input-> [(state, Seq (state, Maybe output))] | ||
87 | go (initial, path) cs = do | ||
88 | let | ||
89 | current | ||
90 | | (_ :> (st, _)) <- path = st | ||
91 | | otherwise = initial | ||
92 | (head, next, out) <- step fst (Just current) (Seq.lookup 0 cs) | ||
93 | let | ||
94 | nPath = path :> (next, out) | ||
95 | ncs = maybe id (:<) head cs | ||
96 | go (initial, nPath) ncs | ||
97 | |||
98 | |||
99 | step :: forall input output state. (Ord input, Ord output, Ord state) | ||
100 | => FST state input output | ||
101 | -> Maybe state -- ^ Current state | ||
102 | -> Maybe input -- ^ Head of remaining input | ||
103 | -> [(Maybe input, state, Maybe output)] -- ^ Tuples of unconsumed input, next state, and produced output | ||
104 | step FST{..} Nothing inS = (\s -> (inS, s, Nothing)) <$> Set.toList stInitial | ||
105 | step FST{..} (Just c) inS = let | ||
106 | consuming = fromMaybe Set.empty $ Map.lookup (c, inS) stTransition | ||
107 | unconsuming = fromMaybe Set.empty $ Map.lookup (c, Nothing) stTransition | ||
108 | in Set.toList $ Set.map (\(n, mOut) -> (Nothing, n, mOut)) consuming `Set.union` Set.map (\(n, mOut) -> (inS, n, mOut)) unconsuming | ||
109 | |||
110 | |||
62 | wordFST :: forall input output. Seq output -> FST Natural input output | 111 | wordFST :: forall input output. Seq output -> FST Natural input output |
63 | -- ^ @wordFST str@ is the linear FST generating @str@ as output when given no input | 112 | -- ^ @wordFST str@ is the linear FST generating @str@ as output when given no input |
64 | wordFST outs = FST | 113 | wordFST outs = FST |