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.lhs57
1 files changed, 53 insertions, 4 deletions
diff --git a/edit-lens/src/Control/DFST/Lens.lhs b/edit-lens/src/Control/DFST/Lens.lhs
index 0976314..eafa458 100644
--- a/edit-lens/src/Control/DFST/Lens.lhs
+++ b/edit-lens/src/Control/DFST/Lens.lhs
@@ -14,14 +14,25 @@ module Control.DFST.Lens
14 ) where 14 ) where
15 15
16import Control.DFST 16import Control.DFST
17import Control.FST hiding (stInitial, stTransition, stAccept)
18import qualified Control.FST as FST (stInitial, stTransition, stAccept)
17import Control.Lens.Edit 19import Control.Lens.Edit
18import Control.Lens 20import Control.Lens
19import Control.Lens.TH 21import Control.Lens.TH
20import Control.Edit 22import Control.Edit
21 23
24import Control.Monad
25
22import Numeric.Natural 26import Numeric.Natural
27import Numeric.Interval (Interval, (...))
28import qualified Numeric.Interval as Int
29
23import Data.Sequence (Seq((:<|), (:|>))) 30import Data.Sequence (Seq((:<|), (:|>)))
24import qualified Data.Sequence as Seq 31import qualified Data.Sequence as Seq
32import Data.Set (Set)
33import qualified Data.Set as Set
34import Data.Map (Map)
35import qualified Data.Map as Map
25 36
26import Data.Compositions.Snoc (Compositions) 37import Data.Compositions.Snoc (Compositions)
27import qualified Data.Compositions.Snoc as Comp 38import qualified Data.Compositions.Snoc as Comp
@@ -30,9 +41,13 @@ import Data.Algorithm.Diff (Diff, getDiff)
30import qualified Data.Algorithm.Diff as Diff 41import qualified Data.Algorithm.Diff as Diff
31 42
32import Data.Monoid 43import Data.Monoid
44import Data.Bool (bool)
45import Data.Maybe (fromMaybe)
33import Data.Function (on) 46import Data.Function (on)
34import Data.Foldable (toList) 47import Data.Foldable (toList)
35 48
49import Debug.Trace
50
36 51
37data StringEdit char = Insert { _sePos :: Natural, _seInsertion :: char } 52data StringEdit char = Insert { _sePos :: Natural, _seInsertion :: char }
38 | Delete { _sePos :: Natural } 53 | Delete { _sePos :: Natural }
@@ -49,6 +64,28 @@ makePrisms ''StringEdits
49stringEdits :: Traversal' (StringEdits char) (StringEdit char) 64stringEdits :: Traversal' (StringEdits char) (StringEdit char)
50stringEdits = _StringEdits . traverse 65stringEdits = _StringEdits . traverse
51 66
67affected :: 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:
69--
70-- - 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@
72--
73-- TODO
74affected SEFail = Nothing
75affected (StringEdits es) = Just $ go es Map.empty
76 where
77 go :: Seq (StringEdit char) -> Map Natural Integer -> Interval Natural
78 go Seq.Empty _ = Int.empty
79 go (es :> e) offsets = traceShow offsets $ Int.hull (Int.singleton p') $ go es offsets'
80 where
81 p = e ^. sePos
82 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
84 myOffset :: Integer -> Integer
85 myOffset
86 | Insert _ _ <- e = pred
87 | Delete _ <- e = succ
88
52insert :: Natural -> char -> StringEdits char 89insert :: Natural -> char -> StringEdits char
53insert n c = StringEdits . Seq.singleton $ Insert n c 90insert n c = StringEdits . Seq.singleton $ Insert n c
54 91
@@ -130,10 +167,13 @@ data DFSTAction state input output = DFSTAction { runDFSTAction :: state -> (sta
130 167
131instance Monoid (DFSTAction state input output) where 168instance Monoid (DFSTAction state input output) where
132 mempty = DFSTAction $ \x -> (x, Seq.empty) 169 mempty = DFSTAction $ \x -> (x, Seq.empty)
133 (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out <> out') 170 DFSTAction f `mappend` DFSTAction g = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out <> out')
134 171
135type DFSTComplement state input output = Compositions (DFSTAction state input output) 172type DFSTComplement state input output = Compositions (DFSTAction state input output)
136 173
174runDFSTAction' :: DFSTComplement state input output -> state -> (state, Seq output)
175runDFSTAction' = runDFSTAction . Comp.composed
176
137dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output) 177dfstLens :: forall state input output. (Ord state, Ord input, Ord output) => DFST state input output -> EditLens (DFSTComplement state input output) (StringEdits input) (StringEdits output)
138dfstLens dfst@DFST{..} = EditLens ground propR propL 178dfstLens dfst@DFST{..} = EditLens ground propR propL
139 where 179 where
@@ -142,7 +182,10 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
142 182
143 propR :: (DFSTComplement state input output, StringEdits input) -> (DFSTComplement state input output, StringEdits output) 183 propR :: (DFSTComplement state input output, StringEdits input) -> (DFSTComplement state input output, StringEdits output)
144 propR (c, SEFail) = (c, SEFail) 184 propR (c, SEFail) = (c, SEFail)
145 propR (c, StringEdits (es :|> e)) = (c', es' <> es'') 185 propR (c, StringEdits Seq.Empty) = (c, mempty)
186 propR (c, StringEdits (es :> e))
187 | fst (runDFSTAction' c' stInitial) `Set.member` stAccept = (c', es' <> es'')
188 | otherwise = (c', SEFail)
146 where 189 where
147 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c 190 (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (e ^. sePos . from enum)) c
148 cSuffix' 191 cSuffix'
@@ -153,11 +196,17 @@ dfstLens dfst@DFST{..} = EditLens ground propR propL
153 (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState 196 (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState
154 (c', es') = propR (cSuffix' <> cPrefix, StringEdits es) 197 (c', es') = propR (cSuffix' <> cPrefix, StringEdits es)
155 es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput 198 es'' = strDiff sOutput sOutput' & stringEdits . sePos . from enum +~ Seq.length pOutput
156 propR (c, StringEdits Seq.Empty) = (c, mempty)
157 199
158 200
159 propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input) 201 propL :: (DFSTComplement state input output, StringEdits output) -> (DFSTComplement state input output, StringEdits input)
160 propL = undefined 202 propL (c, SEFail) = (c, SEFail)
203 propL (c, StringEdits Seq.Empty) = (c, mempty)
204 propL (c, es) = fromMaybe (c, SEFail) $ do
205 newOut <- prevOut `apply` es
206 let outFST = wordFST newOut `productFST` toFST dfst
207 return undefined
208 where
209 (_, prevOut) = runDFSTAction (Comp.composed c) stInitial
161 210
162strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym 211strDiff :: forall sym. Eq sym => Seq sym -> Seq sym -> StringEdits sym
163-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@ 212-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@