From a5689e0dc96262a4df06b6363855d597ad377841 Mon Sep 17 00:00:00 2001 From: Gregor Kleen Date: Mon, 7 May 2018 16:50:09 +0200 Subject: DFST lenses now pass some rudimentary tests --- edit-lens/src/Data/String/DFST/Lens.lhs | 78 +++++++++++++++++++++++++++------ 1 file changed, 65 insertions(+), 13 deletions(-) (limited to 'edit-lens/src/Data/String/DFST/Lens.lhs') diff --git a/edit-lens/src/Data/String/DFST/Lens.lhs b/edit-lens/src/Data/String/DFST/Lens.lhs index 2111ca4..9def01b 100644 --- a/edit-lens/src/Data/String/DFST/Lens.lhs +++ b/edit-lens/src/Data/String/DFST/Lens.lhs @@ -1,6 +1,15 @@ \begin{code} +{-# LANGUAGE ScopedTypeVariables +#-} + module Data.String.DFST.Lens - ( + ( StringEdit(..) + , StringEdits(..) + , insert, delete + , DFSTAction(..), DFSTComplement + , dfstLens + , module Data.String.DFST + , module Control.Lens.Edit ) where import Data.String.DFST @@ -11,10 +20,23 @@ import Numeric.Natural import Data.Sequence (Seq((:<|), (:|>))) import qualified Data.Sequence as Seq +import Data.Compositions.Snoc (Compositions) +import qualified Data.Compositions.Snoc as Comp + +import Data.Algorithm.Diff (Diff, getDiff) +import qualified Data.Algorithm.Diff as Diff + +import Data.Monoid + + data StringEdit = Insert Natural Char | Delete Natural deriving (Eq, Ord, Show, Read) +sePos :: StringEdit -> Natural +sePos (Insert pos _) = pos +sePos (Delete pos ) = pos + data StringEdits = StringEdits (Seq StringEdit) | SEFail deriving (Eq, Ord, Show, Read) @@ -74,26 +96,56 @@ Gegeben eine Sequenz (`StringEdits`) von zu übersetzenden Änderungen genügt e Wir definieren zunächst die \emph{Wirkung} eines DFST auf einen festen String als eine Abbildung `state -> (state, String)`, die den aktuellen Zustand vorm Parsen des Strings auf den Zustand danach und die (womöglich leere) Ausgabe schickt. Diese Wirkungen bilden einen Monoiden analog zu Endomorphismen, wobei die Resultat-Strings concateniert werden. -Die Unterliegende Idee ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller möglich Präfixe und Suffixe zu halten. +Die Unterliegende Idee ist nun im Komplement der edit-lens eine Liste von Wirkungen (eine für jedes Zeichen der Eingabe des DFSTs) und einen Cache der monoidalen Summen aller kontinuirlichen Teillisten zu halten. Da wir wissen welche Stelle im input-String von einem gegebenen edit betroffen ist können wir, anhand der Wirkung des Teilstücks bis zu jener Stelle, den output-String in einen durch den edit unveränderten Prefix und einen womöglich betroffenen Suffix unterteilen. Die Wirkung ab der betroffenen Stelle im input-String können wir also Komposition der Wirkung der durch den edit betroffenen Stelle und derer aller Zeichen danach bestimmen. Nun gilt es nur noch die Differenz (als `StringEdits`) des vorherigen Suffixes im output-String und des aus der gerade berechneten Wirkung Bestimmten zu bestimmen. + +% TODO propL \begin{code} -data DFSTAction state = DFSTBranch (Map state (state, String)) (DFSTAction state) (DFSTAction state) +data DFSTAction state = DFSTAction { runDFSTAction :: state -> (state, String -> String)} -% TODO propL, Transduktor invertieren? - | DFSTLeaf +instance Monoid (DFSTAction state) where + mempty = DFSTAction $ \x -> (x, id) + (DFSTAction f) `mappend` (DFSTAction g) = DFSTAction $ \s -> let ((f -> (s', out')), out) = g s in (s', out' . out) -dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTAction state) StringEdits StringEdits -dfstLens DFST{..} = EditLens ground propR propL - where - ground :: DFSTAction state - ground = DFSTLeaf +type DFSTComplement state = Compositions (DFSTAction state) - propR :: (DFSTAction state, StringEdits) -> (DFSTAction state, StringEdits) - propR = undefined - propL :: (DFSTAction state, StringEdits) -> (DFSTAction state, StringEdits) +dfstLens :: forall state. Ord state => DFST state -> EditLens (DFSTComplement state) StringEdits StringEdits +dfstLens dfst@DFST{..} = EditLens ground propR propL + where + ground :: DFSTComplement state + ground = Comp.fromList [] + + propR :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits) + propR (c, SEFail) = (c, SEFail) + propR (c, StringEdits (es :|> e)) = (c', es' <> shiftBy (length $ pOutput []) (strDiff sOutput sOutput')) + where + (cSuffix, cPrefix) = Comp.splitAt (Comp.length c - (fromEnum $ sePos e)) 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) id) + (pState, pOutput) = runDFSTAction (Comp.composed cPrefix) stInitial + (_, sOutput ) = runDFSTAction (Comp.composed cSuffix ) pState + (_, sOutput') = runDFSTAction (Comp.composed cSuffix') pState + (c', es') = propR (cSuffix' <> cPrefix, StringEdits es) + shiftBy (toEnum -> n) (StringEdits es) = StringEdits $ shiftBy' n <$> es + shiftBy' n' (Insert n c) = Insert (n + n') c + shiftBy' n' (Delete n) = Delete (n + n') + propR (c, mempty) = (c, mempty) + + + propL :: (DFSTComplement state, StringEdits) -> (DFSTComplement state, StringEdits) propL = undefined + +strDiff :: (String -> String) -> (String -> String) -> StringEdits +-- ^ @strDiff a b@ calculates a set of edits, which, when applied to @a@, produce @b@, where both @a@ and @b@ are given as diff-lists of chars +strDiff a b = snd . foldr toEdit (0, mempty) $ getDiff (a []) (b []) + where + toEdit :: Diff Char -> (Natural, StringEdits) -> (Natural, StringEdits) + 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) \end{code} -- cgit v1.2.3