diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2018, Victor Miraldo and Alejandro Serrano + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/executables/HDiff.hs b/executables/HDiff.hs new file mode 100644 --- /dev/null +++ b/executables/HDiff.hs @@ -0,0 +1,353 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE CPP #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +-- |Illustrates the usage of MRSOP with a custom +-- opaque type universe and the use of HDiff to +-- compute diffs over various languages. +-- +module Main (main) where + +import System.IO +import System.Exit +import Control.Monad +import Control.Applicative +import Data.Foldable (asum) + +import Development.GitRev +import Options.Applicative +import Data.Semigroup ((<>)) + +import Data.Maybe (isJust) +import qualified Data.List as L (lookup) +import Data.Type.Equality + +import Generics.MRSOP.Base hiding (Infix) +import Generics.MRSOP.HDiff.Renderer +import Generics.MRSOP.HDiff.Digest + +import qualified Generics.MRSOP.GDiff as GDiff + +import qualified Data.HDiff.Patch as D +import qualified Data.HDiff.Diff as D +import qualified Data.HDiff.Patch.Merge as D +import qualified Data.HDiff.Patch.TreeEditDistance as TED +import Data.HDiff.Patch.Show +import qualified Data.HDiff.Change as D +import qualified Data.HDiff.Change.TreeEditDistance as TEDC + +import Languages.Interface +import qualified Languages.While as While +import qualified Languages.Lines as Lines + +#ifdef ENABLE_LUA_SUPPORT +import qualified Languages.Lua as Lua +#endif + +#ifdef ENABLE_CLOJURE_SUPPORT +import qualified Languages.Clojure as Clj +#endif + + + -- |The parsers that we support +mainParsers :: [LangParser] +mainParsers + = [LangParser "while" (fmap (dfrom . into @While.FamStmt) . While.parseFile) +#ifdef ENABLE_LUA_SUPPORT + ,LangParser "lua" (fmap (dfrom . into @Lua.FamStmt) . Lua.parseFile) +#endif +#ifdef ENABLE_CLOJURE_SUPPORT + ,LangParser "clj" (fmap (dfrom . into @Clj.FamExpr) . Clj.parseFile) +#endif + ,LangParser "lines" (fmap (dfrom . into @Lines.FamStmt) . Lines.parseFile) + ] + +--------------------------- +-- * Cmd Line Options + +data PatchOrChange + = Patch | Chg + deriving (Eq , Show) + +data Options + = AST { optFileA :: FilePath + } + | GDiff { optFileA :: FilePath + , optFileB :: FilePath + , showES :: Bool + } + | Diff { optFileA :: FilePath + , optFileB :: FilePath + , testApply :: Bool + , minHeight :: Int + , diffMode :: D.DiffMode + , opqHandling :: D.DiffOpaques + , toEditScript :: Maybe PatchOrChange + , showES :: Bool + } + | Merge { optFileA :: FilePath + , optFileO :: FilePath + , optFileB :: FilePath + , minHeight :: Int + , diffMode :: D.DiffMode + , opqHandling :: D.DiffOpaques + } + deriving (Eq , Show) + +astOpts :: Parser Options +astOpts = AST <$> argument str (metavar "FILE") + +showesOpt :: Parser Bool +showesOpt = switch (long "show-es" <> help "Display the generated edit script" <> hidden) + +minheightOpt :: Parser Int +minheightOpt = option auto $ + long "min-height" + <> short 'm' + <> showDefault + <> value 1 + <> metavar "INT" + <> help "Minimum height of subtrees considered for sharing" + <> hidden + +readmOneOf :: [(String, a)] -> ReadM a +readmOneOf = maybeReader . flip L.lookup + +diffmodeOpt :: Parser D.DiffMode +diffmodeOpt = option (readmOneOf [("proper" , D.DM_ProperShare) + ,("nonest" , D.DM_NoNested) + ,("patience", D.DM_Patience) + ]) + ( long "diff-mode" + <> short 'd' + <> metavar "proper | nonest | patience ; default: proper" + <> value D.DM_ProperShare + <> help aux + <> hidden) + where + aux = unwords + ["Controls how context extraction works. If you are unaware about how" + ,"this works, check 'Data.HDiff.Diff.Types' and 'Data.HDiff.Diff.Modes'" + ,"for more information." + ] + + +opqhandlingOpt :: Parser D.DiffOpaques +opqhandlingOpt = option (readmOneOf [("never" , D.DO_Never) + ,("spine" , D.DO_OnSpine) + ,("always", D.DO_AsIs) + ]) + ( long "diff-opq" + <> short 'k' + <> metavar "never | spine | always ; default: spine" + <> value D.DO_OnSpine + <> help aux + <> hidden) + where + aux = unwords + ["Controls how to handle opaque values. We either treat them like normal" + ,"trees, with 'always', never share them, or share only the opaque values" + ,"that end up on the spine" + ] + +toesOpt :: Parser (Maybe PatchOrChange) +toesOpt = flag' (Just Patch) ( long "patch-to-es" + <> help "Translates a patch to an edit script at the patch level" + <> hidden) + <|> flag' (Just Chg) ( long "change-to-es" + <> help ("Translates a patch to an edit script at the change" + ++ " level; does so by using distrCChange on the patch") + <> hidden) + <|> pure Nothing + +gdiffOpts :: Parser Options +gdiffOpts = GDiff <$> argument str (metavar "OLDFILE") + <*> argument str (metavar "NEWFILE") + <*> showesOpt + +diffOpts :: Parser Options +diffOpts = + Diff <$> argument str (metavar "OLDFILE") + <*> argument str (metavar "NEWFILE") + <*> switch ( long "test-apply" + -- TODO: check this doc + <> help "Attempts application; returns ExitFailure if apply fails." + <> hidden) + <*> minheightOpt + <*> diffmodeOpt + <*> opqhandlingOpt + <*> toesOpt + <*> showesOpt + +mergeOpts :: Parser Options +mergeOpts = + Merge <$> argument str (metavar "MYFILE") + <*> argument str (metavar "OLDFILE") + <*> argument str (metavar "YOURFILE") + <*> minheightOpt + <*> diffmodeOpt + <*> opqhandlingOpt + +parseOptions :: Parser Options +parseOptions = hsubparser + ( command "ast" (info astOpts + (progDesc "Parses and displays an ast")) + <> command "gdiff" (info gdiffOpts + (progDesc "Runs Generics.MRSOP.GDiff on the targets")) + <> command "diff" (info diffOpts + (progDesc "Runs Data.HDiff.Diff on the targes")) + <> command "merge" (info mergeOpts + (progDesc "Runs the merge algorithm on the specified files")) + ) <|> diffOpts + +data Verbosity + = Quiet + | Normal + | Loud + | VeryLoud + deriving (Eq, Show) + +verbosity :: Parser Verbosity +verbosity = asum + [ flag' Quiet ( long "quiet" + <> short 'q' + <> help "Runs on quiet mode; almost no information out" + <> hidden ) + , flag' Loud ( long "verbose" + <> short 'v' + <> help "Runs with a more output than normal" + <> hidden ) + , flag' VeryLoud ( long "debug" + <> internal ) + , pure Normal + ] + +data OptionMode + = OptAST | OptDiff | OptMerge | OptGDiff + deriving (Eq , Show) + +optionMode :: Options -> OptionMode +optionMode (AST _) = OptAST +optionMode (GDiff _ _ _) = OptGDiff +optionMode (Merge _ _ _ _ _ _) = OptMerge +optionMode (Diff _ _ _ _ _ _ _ _) = OptDiff + +main :: IO () +main = execParser fullOpts >>= \(verb , opts) + -> case optionMode opts of + OptAST -> mainAST verb opts + OptDiff -> mainDiff verb opts + OptGDiff -> mainGDiff verb opts + OptMerge -> mainMerge verb opts + >>= exitWith + where + fullOpts = info ((,) <$> verbosity <*> parseOptions <**> helper) + $ fullDesc + <> header ("digem v0.0.0 [" ++ $(gitBranch) ++ "@" ++ $(gitHash) ++ "]") + <> progDesc "Runs digem with the specified command, 'diff' is the default command." + <> footer "Run digem COMMAND --help for more help on specific commands" + +putStrLnErr :: String -> IO () +putStrLnErr = hPutStrLn stderr + +-- * Generic interface + +mainAST :: Verbosity -> Options -> IO ExitCode +mainAST v opts = withParsed1 mainParsers (optFileA opts) + $ \fa -> do + unless (v == Quiet) $ putStrLn (show (renderFix renderHO fa)) + return ExitSuccess + +-- |Applies a patch to an element and either checks it is equal to +-- another element, or returns the result. +tryApply :: (EqHO ki , ShowHO ki , TestEquality ki , IsNat ix, RendererHO ki + ,HasDatatypeInfo ki fam codes) + => Verbosity + -> D.Patch ki codes ix + -> Fix ki codes ix + -> Maybe (Fix ki codes ix) + -> IO (Maybe (Fix ki codes ix)) +tryApply v patch fa fb + = case D.apply patch fa of + Left err -> hPutStrLn stderr "!! apply failed" + >> hPutStrLn stderr (" " ++ err) + >> when (v == Loud) + (hPutStrLn stderr (show $ renderFix renderHO fa)) + >> exitFailure + Right b' -> return $ maybe (Just b') (const Nothing) fb + +-- |Runs our diff algorithm with particular options parsed +-- from the CLI options. +diffWithOpts :: ( EqHO ki , ShowHO ki , TestEquality ki , IsNat ix, RendererHO ki + , DigestibleHO ki, HasDatatypeInfo ki fam codes) + => Options + -> Fix ki codes ix + -> Fix ki codes ix + -> IO (D.Patch ki codes ix) +diffWithOpts opts fa fb = do + let localopts = D.DiffOptions (minHeight opts) (opqHandling opts) (diffMode opts) + return (D.diffOpts localopts fa fb) + +mainGDiff :: Verbosity -> Options -> IO ExitCode +mainGDiff _ opts = withParsed2 mainParsers (optFileA opts) (optFileB opts) + $ \fa fb -> do + let es = GDiff.diff' fa fb + putStrLn ("tree-edit-distance: " ++ show (GDiff.cost es)) + when (showES opts) (putStrLn $ show es) + return ExitSuccess + +mainDiff :: Verbosity -> Options -> IO ExitCode +mainDiff v opts = withParsed2 mainParsers (optFileA opts) (optFileB opts) + $ \fa fb -> do + patch <- diffWithOpts opts fa fb + unless (v == Quiet) $ displayRawPatch stdout patch + when (testApply opts) $ void (tryApply v patch fa (Just fb)) + when (isJust (toEditScript opts)) $ do + let (role , ees) = case toEditScript opts of + Just Patch -> ("patch" , TED.toES patch (NA_I fa)) + Just Chg -> ("change", TEDC.toES (D.distrCChange patch) (NA_I fa)) + case ees of + Left err -> putStrLnErr ("!! " ++ err) + Right es -> putStrLn ("tree-edit-distance: " ++ role ++ " " ++ show (GDiff.cost es)) + >> when (v == Loud) (putStrLn $ show es) + return ExitSuccess + +mainMerge :: Verbosity -> Options -> IO ExitCode +mainMerge v opts = withParsed3 mainParsers (optFileA opts) (optFileO opts) (optFileB opts) + $ \fa fo fb -> do + when (v == Loud) $ do + putStrLnErr $ "O: " ++ optFileO opts + putStrLnErr $ "A: " ++ optFileA opts + putStrLnErr $ "B: " ++ optFileB opts + patchOA <- diffWithOpts opts fo fa + patchOB <- diffWithOpts opts fo fb + let resAB = patchOA D.// patchOB + let resBA = patchOB D.// patchOA + when (v == VeryLoud) $ do + putStrLnErr $ "O->A/O->B " ++ replicate 55 '#' + displayPatchC stderr resAB + putStrLnErr $ "O->B/O->A " ++ replicate 55 '#' + displayPatchC stderr resBA + case (,) <$> D.noConflicts resAB <*> D.noConflicts resBA of + Nothing -> putStrLnErr " !! Conflicts O->A/O->B !!" + >> putStrLnErr (unlines (map (" - " ++) (D.getConflicts resAB))) + >> putStrLnErr " !! Conflicts O->B/O->A !!" + >> putStrLnErr (unlines (map (" - " ++) (D.getConflicts resBA))) + >> return (ExitFailure 1) + Just (ab , ba) -> do + when (v == Loud) (putStrLnErr "!! apply ba fa") + Just fb' <- tryApply v ba fa Nothing + when (v == Loud) (putStrLnErr "!! apply ab fb") + Just fa' <- tryApply v ab fb Nothing + if eqFix eqHO fb' fa' + then return ExitSuccess + else return (ExitFailure 2) diff --git a/executables/Languages/Clojure.hs b/executables/Languages/Clojure.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Clojure.hs @@ -0,0 +1,26 @@ +{-# LANGUAGE CPP #-} +module Languages.Clojure + ( module AST + , parseFile + ) where + +#ifdef ENABLE_CLOJURE_SUPPORT + +import Languages.Clojure.AST as AST +import qualified Languages.Clojure.Parser as Parser + +parseFile :: FilePath -> IO Expr +parseFile fname = do + x <- Parser.parseFile fname + case x of + Left e -> print e >> fail "parse error" + Right r -> return r + +#else + +import Data.Proxy as AST + +parseFile :: FilePath -> IO a +parseFile = error "enable clojure support" + +#endif diff --git a/executables/Languages/Clojure/AST.hs b/executables/Languages/Clojure/AST.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Clojure/AST.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE BangPatterns #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Languages.Clojure.AST where + +import Data.Type.Equality + +import Data.Text.Prettyprint.Doc (pretty) + +import Data.Text +import Data.Text.Encoding (encodeUtf8) +import Generics.MRSOP.TH +import Generics.MRSOP.Base +import Generics.MRSOP.HDiff.Digest +import Generics.MRSOP.HDiff.Renderer + + +data SepExprList = + Nil + | Cons Expr !Sep SepExprList + deriving (Show) + +data Sep = Space | Comma | NewLine | EmptySep deriving (Show, Eq) + +data Expr = Special !FormTy Expr + | Dispatch Expr + | Collection !CollTy SepExprList + | Term Term + | Comment !Text + | Seq Expr Expr + | Empty + deriving (Show) + +data FormTy = Quote | SQuote | UnQuote | DeRef | Meta deriving (Show, Eq) + +data CollTy = Vec | Set | Parens deriving (Show, Eq) + +data Term = TaggedString !Tag !Text + deriving (Show) + +data Tag = String | Var deriving (Show, Eq) + + + +data ConflictResult a = NoConflict | ConflictAt a + deriving (Show, Eq) + +data CljKon = CljText +data CljSingl (kon :: CljKon) :: * where + SCljText :: Text -> CljSingl 'CljText + +instance RendererHO CljSingl where + renderHO (SCljText t) = pretty (unpack t) + +instance Digestible Text where + digest = hash . encodeUtf8 + +instance DigestibleHO CljSingl where + digestHO (SCljText text) = digest text + + +deriving instance Show (CljSingl k) +deriving instance Eq (CljSingl k) +instance ShowHO CljSingl where showHO = show +instance EqHO CljSingl where eqHO = (==) + +instance TestEquality CljSingl where + testEquality (SCljText _) (SCljText _) = Just Refl + + +deriveFamilyWith ''CljSingl [t| Expr |] diff --git a/executables/Languages/Clojure/Parser.hs b/executables/Languages/Clojure/Parser.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Clojure/Parser.hs @@ -0,0 +1,181 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DataKinds #-} + +module Languages.Clojure.Parser + ( parseTop + , parse + , parseFile + , parseTest + , parseAsExprList + + -- AST + , Expr(..) + , FormTy(..) + , CollTy(..) + , Term(..) + , Tag(..) + , SepExprList(..) + , Sep(..) + ) where + +import Text.Parsec hiding (Empty) +import Text.Parsec.Token hiding (braces, parens, brackets, identifier, operator) +import Text.Parsec.Language +import Data.Char hiding (Space) +import qualified Data.Text as T +import Data.Proxy + +import Languages.Clojure.AST + +lexer = makeTokenParser javaStyle + { identStart = alphaNum <|> oneOf "_':*-&." + , identLetter = alphaNum <|> oneOf ":_.'-/^?!><*#\"\\" <|> satisfy isSymbol + } + +parseSeq :: Parsec String () Expr +parseSeq = do + p1 <- parseExpr + whiteSpace lexer + p2 <- (try parseSeq <|> parseEmptyProgram) + return $ Seq p1 p2 + +parseTop = whiteSpace lexer *> (try parseSeq <|> parseEmptyProgram) <* eof + +parseAsExprList = do + top <- parseTop + return $ walkSeq top + -- whiteSpace lexer *> (many parseSingleExpr) <* whiteSpace lexer <* eof +walkSeq (Seq a (Empty )) = a : [] +walkSeq (Seq a b ) = a : walkSeq b +walkSeq (Empty ) = [Empty ] +walkSeq e = error $ "nowalk" ++ show e + +parseExpr = choice + [ try parseSpecial + , try parseDispatch + , parseCollection + , parseComment + , parseTerm + ] + +parseEmptyProgram = do + return $ Empty + +parseTerm = do + term <- parseTaggedString + return $ Term term + +parseCollection = choice [ parseParens, parseVec, parseSet ] + +parseSpecial = do + ident <- parseSpecialIdent + expr <- parseExpr + return $ Special ident expr + +parseSpecialIdent = choice + [ Quote <$ char '\'' + , SQuote <$ char '`' + , UnQuote <$ char '~' + , DeRef <$ char '@' + , Meta <$ char '^' + ] + +parseTaggedString = choice [parseString, parseVar] + +parseDispatch = do + char '#' + disp <- parseDispatchable + return $ Dispatch disp + where + parseDispatchable = choice + [ parseExpr + , parseRegExp + , parseTaggedLit + ] + --- ref: https://yobriefca.se/blog/2014/05/19/the-weird-and-wonderful-characters-of-clojure/ + -- parseParens covers the function marco + -- parseTaggedLit covers the var macro (as identifiers can start with a quote (')) + parseRegExp = do + regExp <- parseString + return $ Term regExp + + parseTaggedLit = do + tLit <- parseVar + return $ Term tLit + + -- parseMeta = do + -- start <- getPosition + -- meta <- parseMetadata + -- end <- getPosition + -- return $ Term meta (mkRange start end) + +parseComment = do + char ';' + comment <- manyTill anyChar (newline <|> eofS) + -- single line comment, if we parse end here we have parsed newline as well + return $ Comment (T.pack comment) + +eofS = do + eof + return '\n' + +parens p = between (symbol lexer "(") (string ")") p +braces p = between (symbol lexer "{") (string "}") p +brackets p = between (symbol lexer "[") (string "]") p + + +parseSet = do + contents <- braces parseSepExprList + end <- getPosition + return $ Collection Set contents + +parseVec = do + contents <- brackets parseSepExprList + return $ Collection Vec contents + +parseParens = do + contents <- parens parseSepExprList + return $ Collection Parens contents + +parseSepExprList = parseSepExprList1 <|> parseEmptyList + +parseEmptyList = do + return $ Nil + +parseSepExprList1 = do + x <- parseExpr + sep <- parseSep + xs <- parseSepExprList + return $ Cons x sep xs + +parseSep = choice + [ Comma <$ lexeme lexer (char ',') + , NewLine <$ lexeme lexer (many1 endOfLine) + , Space <$ lexeme lexer (many1 (space <|> tab)) + , EmptySep <$ (lookAhead (anyChar) <|> eofS) + ] +parseString = do + qstring <- quotedString + return $ TaggedString String (T.pack qstring) + where + quotedString :: Parsec String () String + quotedString = do + char '"' + x <- many (try (try (string "\\\\") <|> string "\\\"") <|> fmap pure (noneOf "\"")) + char '"' + return $ concat x + +parseVar = do + vstring <- (identifier) + return $ TaggedString Var (T.pack vstring) + +identifier = do + c <- alphaNum <|> oneOf ":!#$%&*+./<=>?@\\^|-~_'," + cs <- many (alphaNum <|> oneOf ":!?#$%&*+-/.<=>'?@^|~_'^\"\\" <|> satisfy isSymbol) + return (c:cs) + + +parseFile :: FilePath -> IO (Either ParseError Expr) +parseFile fname = do + input <- readFile fname + return (runParser parseTop () fname input) diff --git a/executables/Languages/Interface.hs b/executables/Languages/Interface.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Interface.hs @@ -0,0 +1,126 @@ +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE TypeApplications #-} +module Languages.Interface where + +import Data.List (isSuffixOf) +import Data.Type.Equality + +import Control.Applicative +import Control.Monad.Except + +import System.IO +import System.Exit + +import Generics.MRSOP.Util +import Generics.MRSOP.Base hiding (Infix) +import Generics.MRSOP.HDiff.Renderer +import Generics.MRSOP.HDiff.Digest + + +data LangParser :: * where + LangParser :: (LangCnstr ki fam codes ix) + -- |Language extension + => String + -- |Parser that + -> (FilePath -> IO (Fix ki codes ix)) + -> LangParser + +data VectorOf (a :: *) (n :: Nat) :: * where + V0 :: VectorOf a Z + VS :: a -> VectorOf a n -> VectorOf a (S n) + +vecMapM :: (Monad m) => (a -> m b) -> VectorOf a n -> m (VectorOf b n) +vecMapM f V0 = return V0 +vecMapM f (VS x xs) = VS <$> f x <*> vecMapM f xs + +type LangCnstr ki fam codes ix + = (HasDatatypeInfo ki fam codes , EqHO ki , RendererHO ki , IsNat ix, ShowHO ki + ,DigestibleHO ki,TestEquality ki) + +-- |Given a list of languages, parses a number of files +withParsedEl :: LangParser + -> VectorOf FilePath (S n) + -> (forall kon (ki :: kon -> *) fam codes ix + . (LangCnstr ki fam codes ix) + => VectorOf (Fix ki codes ix) (S n) + -> IO res) + -> ExceptT String IO res +withParsedEl (LangParser ext parser) vec f + = do fs <- vecMapM (parseWithExt ext parser) vec + liftIO $ f fs + where + parseWithExt :: (HasDatatypeInfo ki fam codes) + => String + -> (FilePath -> IO (Fix ki codes ix)) + -> FilePath + -> ExceptT String IO (Fix ki codes ix) + parseWithExt ext parser file + | ("." ++ ext) `isSuffixOf` file = liftIO $ parser file + | otherwise + = throwError ("Wrong Extension; expecting: " ++ show ext ++ "\n") + +-- |Tries a variety of parsers on a number of +-- files. +withParsedEls :: [LangParser] + -> VectorOf FilePath (S n) + -> (forall kon (ki :: kon -> *) fam codes ix + . (LangCnstr ki fam codes ix) + => VectorOf (Fix ki codes ix) (S n) + -> IO res) + -> ExceptT String IO res +withParsedEls [] _ _ = throwError "No parser succeeded\n" +withParsedEls (p:ps) files f + = withParsedEl p files f + <|> withParsedEls ps files f + + +-- * Fixed interface for one, two and three files + +redirectErr :: ExceptT String IO a -> IO a +redirectErr f = runExceptT f >>= either myerr return + where + myerr str = hPutStrLn stderr str + >> exitWith (ExitFailure 10) + +withParsed1 :: [LangParser] + -> FilePath + -> (forall kon (ki :: kon -> *) fam codes ix + . (LangCnstr ki fam codes ix) + => Fix ki codes ix + -> IO res) + -> IO res +withParsed1 parsers file f + = redirectErr + $ withParsedEls parsers (VS file V0) + $ \(VS file V0) -> f file + + +withParsed2 :: [LangParser] + -> FilePath -> FilePath + -> (forall kon (ki :: kon -> *) fam codes ix + . (LangCnstr ki fam codes ix) + => Fix ki codes ix -> Fix ki codes ix + -> IO res) + -> IO res +withParsed2 parsers a b f + = redirectErr + $ withParsedEls parsers (VS a (VS b V0)) + $ \(VS a (VS b V0)) -> f a b + +withParsed3 :: [LangParser] + -> FilePath -> FilePath -> FilePath + -> (forall kon (ki :: kon -> *) fam codes ix + . (LangCnstr ki fam codes ix) + => Fix ki codes ix -> Fix ki codes ix -> Fix ki codes ix + -> IO res) + -> IO res +withParsed3 parsers a b c f + = redirectErr + $ withParsedEls parsers (VS a (VS b (VS c V0))) + $ \(VS a (VS b (VS c V0))) -> f a b c diff --git a/executables/Languages/Lines.hs b/executables/Languages/Lines.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Lines.hs @@ -0,0 +1,71 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +module Languages.Lines where + +import System.IO +import Data.Type.Equality +import Data.Text.Prettyprint.Doc (pretty) +import Data.Text.Prettyprint.Doc.Render.Text +import qualified Data.Text as T + +import Generics.MRSOP.Base hiding (Infix) +import Generics.MRSOP.Util +import Generics.MRSOP.TH +import Generics.MRSOP.HDiff.Renderer +import Generics.MRSOP.HDiff.Digest + +import Debug.Trace + +----------------------- +-- * Parser + +-- |We must have a dedicated type 'Line' to make sure +-- we duplicate lines. If we use just @Stmt [String]@ +-- the content of the lines will be seen as an opaque type. +-- Opaque values are NOT shared by design. +data Stmt = Stmt [Line] + +data Line = Line String + +-- |Custom Opaque type +data WKon = WString + +-- |And their singletons. +-- +-- Note we need instances of Eq1, Show1 and DigestibleHO +data W :: WKon -> * where + W_String :: String -> W WString + +instance EqHO W where + eqHO (W_String s) (W_String ss) = s == ss + +instance DigestibleHO W where + digestHO (W_String s) = hashStr s + +instance ShowHO W where + showHO (W_String s) = s + +-- Now we derive the 'Family' instance +-- using 'W' for the constants. +deriveFamilyWithTy [t| W |] [t| Stmt |] + +instance RendererHO W where + renderHO (W_String s) = pretty s + +instance TestEquality W where + testEquality (W_String _) (W_String _) = Just Refl + +parseFile :: String -> IO Stmt +parseFile file = + do program <- readFile file + return (Stmt $ map Line $ lines program) + diff --git a/executables/Languages/Lua.hs b/executables/Languages/Lua.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/Lua.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE CPP #-} +module Languages.Lua where + +#ifdef ENABLE_LUA_SUPPORT + +import Language.Lua.Syntax +import qualified Language.Lua.Parser as Lua + +import Data.Text (Text) +import Data.Text.Encoding (encodeUtf8) +import Data.Type.Equality + +import Data.Proxy +import Data.Functor.Const +import Data.Functor.Sum +import Data.Text.Prettyprint.Doc hiding (braces,parens,semi) +import qualified Data.Text.Prettyprint.Doc as PP (braces,parens,semi) +import Data.Text.Prettyprint.Doc.Render.Text +import qualified Data.Text as T + +import System.Exit +import System.IO + +import Generics.MRSOP.TH +import Generics.MRSOP.Base +import Generics.MRSOP.Util + +import Generics.MRSOP.HDiff.Digest +import Generics.MRSOP.HDiff.Renderer + +data LuaKon = LuaText | LuaBool +data LuaSingl (kon :: LuaKon) :: * where + SLuaText :: Text -> LuaSingl LuaText + SLuaBool :: Bool -> LuaSingl LuaBool + +instance RendererHO LuaSingl where + renderHO (SLuaText t) = pretty (T.unpack t) + renderHO (SLuaBool b) = pretty b + +instance Digestible Text where + digest = hash . encodeUtf8 + +instance DigestibleHO LuaSingl where + digestHO (SLuaText text) = digest text + digestHO (SLuaBool bool) = hashStr (show bool) + +deriving instance Show (LuaSingl k) +deriving instance Eq (LuaSingl k) +instance ShowHO LuaSingl where showHO = show +instance EqHO LuaSingl where eqHO = (==) + +instance TestEquality LuaSingl where + testEquality (SLuaText _) (SLuaText _) = Just Refl + testEquality (SLuaBool _) (SLuaBool _) = Just Refl + testEquality _ _ = Nothing + +deriveFamilyWith ''LuaSingl [t| Block |] + +parseFile :: String -> IO Block +parseFile file = do + res <- Lua.parseFile file + case res of + Left e -> hPutStrLn stderr (show e) >> exitWith (ExitFailure 10) + Right r -> return r + +type W = LuaSingl +type Stmt = Block +type FamStmt = FamBlock +type CodesStmt = CodesBlock + +#endif diff --git a/executables/Languages/While.hs b/executables/Languages/While.hs new file mode 100644 --- /dev/null +++ b/executables/Languages/While.hs @@ -0,0 +1,252 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} +module Languages.While where + +import Text.ParserCombinators.Parsec +import Text.ParserCombinators.Parsec.Expr +import Text.ParserCombinators.Parsec.Language +import qualified Text.ParserCombinators.Parsec.Token as Token + +import Control.Monad +import Data.Type.Equality +import Data.Text.Prettyprint.Doc (pretty) + +import Generics.MRSOP.Base hiding (Infix) +import Generics.MRSOP.TH +import Generics.MRSOP.HDiff.Renderer +import Generics.MRSOP.HDiff.Digest + +import System.IO +import System.Exit + +----------------------- +-- * Parser + +data BExpr = BoolConst Bool + | Not BExpr + | BBinary BBinOp BExpr BExpr + | RBinary RBinOp AExpr AExpr + deriving (Show , Eq) + +data BBinOp = And | Or deriving (Show , Eq) + +data RBinOp = Greater | Less | Equal deriving (Show , Eq) + +data AExpr = Var String + | IntConst Integer + | Neg AExpr + | ABinary ABinOp AExpr AExpr + | ARange AExpr AExpr + deriving (Show , Eq) + +data ABinOp = Add + | Subtract + | Multiply + | Reminder + | Divide + | Power + deriving (Show , Eq) + +data Stmt = Seq [Stmt] + | Assign String AExpr + | If BExpr Stmt Stmt + | While BExpr Stmt + | Skip + deriving (Show , Eq) + +-- |Custom Opaque type +data WKon = WInt | WString | WBool + +-- |And their singletons. +-- +-- Note we need instances of EqHO, ShowHO and DigestibleHO +data W :: WKon -> * where + W_Integer :: Integer -> W 'WInt + W_String :: String -> W 'WString + W_Bool :: Bool -> W 'WBool + +instance EqHO W where + eqHO (W_Integer i) (W_Integer j) = i == j + eqHO (W_String s) (W_String ss) = s == ss + eqHO (W_Bool b) (W_Bool c) = b == c + +instance DigestibleHO W where + digestHO (W_Integer i) = hashStr (show i) + digestHO (W_String s) = hashStr s + digestHO (W_Bool b) = hashStr (show b) + +instance ShowHO W where + showHO (W_Integer i) = show i + showHO (W_String s) = s + showHO (W_Bool b) = show b + +-- Now we derive the 'Family' instance +-- using 'W' for the constants. +deriveFamilyWithTy [t| W |] [t| Stmt |] + +instance RendererHO W where + renderHO (W_Integer i) = pretty i + renderHO (W_String s) = pretty s + renderHO (W_Bool b) = pretty b + +instance TestEquality W where + testEquality (W_Integer _) (W_Integer _) = Just Refl + testEquality (W_String _) (W_String _) = Just Refl + testEquality (W_Bool _) (W_Bool _) = Just Refl + testEquality _ _ = Nothing + +-- ** Parser definition + +languageDef = + emptyDef { Token.commentStart = "/*" + , Token.commentEnd = "*/" + , Token.commentLine = "//" + , Token.identStart = letter + , Token.identLetter = alphaNum + , Token.reservedNames = [ "if" + , "then" + , "else" + , "while" + , "do" + , "skip" + , "true" + , "false" + , "not" + , "and" + , "or" + , "range" + ] + , Token.reservedOpNames = ["+", "-", "*", "^", "/", ":=" , "%" + , "<", ">", "and", "or", "not" , "==" + ] + } +lexer = Token.makeTokenParser languageDef +identifier = Token.identifier lexer -- parses an identifier +reserved = Token.reserved lexer -- parses a reserved name +reservedOp = Token.reservedOp lexer -- parses an operator +parseBraces = Token.braces lexer +parseParens = Token.parens lexer -- parses surrounding parenthesis: + -- parseParens p + -- takes care of the parenthesis and + -- uses p to parse what's inside them +integer = Token.integer lexer -- parses an integer +parseSemi = Token.semi lexer -- parses a parseSemicolon +whiteSpace = Token.whiteSpace lexer -- parses whitespace + +whileParser :: Parser Stmt +whileParser = whiteSpace >> sequenceOfStmt + +statement :: Parser Stmt +statement = statement' + <|> parseBraces sequenceOfStmt + +sequenceOfStmt = + do list <- (many statement') + -- If there's only one statement return it without using Seq. + return $ if length list == 1 then head list else Seq list + +statement' :: Parser Stmt +statement' = ifStmt + <|> whileStmt + <|> (skipStmt <* parseSemi) + <|> (assignStmt <* parseSemi) + +ifStmt :: Parser Stmt +ifStmt = + do reserved "if" + cond <- bExpression + reserved "then" + stmt1 <- statement + reserved "else" + stmt2 <- statement + return $ If cond stmt1 stmt2 + +whileStmt :: Parser Stmt +whileStmt = + do reserved "while" + cond <- bExpression + reserved "do" + stmt <- statement + return $ While cond stmt + +assignStmt :: Parser Stmt +assignStmt = + do var <- identifier + reservedOp ":=" + expr <- aExpression + return $ Assign var expr + +skipStmt :: Parser Stmt +skipStmt = reserved "skip" >> return Skip + +aExpression :: Parser AExpr +aExpression = buildExpressionParser aOperators aTerm + +bExpression :: Parser BExpr +bExpression = buildExpressionParser bOperators bTerm + +aOperators = [ [Prefix (reservedOp "-" >> return (Neg )) ] + , [Infix (reservedOp "^" >> return (ABinary Power )) AssocLeft] + , [Infix (reservedOp "*" >> return (ABinary Multiply)) AssocLeft, + Infix (reservedOp "/" >> return (ABinary Divide )) AssocLeft, + Infix (reservedOp "%" >> return (ABinary Reminder)) AssocLeft] + , [Infix (reservedOp "+" >> return (ABinary Add )) AssocLeft, + Infix (reservedOp "-" >> return (ABinary Subtract)) AssocLeft] + ] + +bOperators = [ [Prefix (reservedOp "not" >> return (Not )) ] + , [Infix (reservedOp "and" >> return (BBinary And )) AssocLeft, + Infix (reservedOp "or" >> return (BBinary Or )) AssocLeft] + ] + +aTerm = parseParens aExpression + <|> liftM Var identifier + <|> liftM IntConst integer + <|> (reserved "range" >> liftM2 ARange aExpression aExpression) + +bTerm = parseParens bExpression + <|> (reserved "true" >> return (BoolConst True )) + <|> (reserved "false" >> return (BoolConst False)) + <|> rExpression + +rExpression = + do a1 <- aExpression + op <- relation + a2 <- aExpression + return $ RBinary op a1 a2 + +relation = (reservedOp ">" >> return Greater) + <|> (reservedOp "<" >> return Less) + <|> (reservedOp "==" >> return Equal) + +parseString :: String -> Stmt +parseString str = + case parse whileParser "" str of + Left e -> error $ show e + Right r -> r + +testString :: String -> IO () +testString str + = do let stmt = parseString str + putStrLn $ show $ renderEl renderHO (into @FamStmt stmt) + +parseFile :: String -> IO Stmt +parseFile file = + do program <- readFile file + case parse whileParser "" program of + Left e -> hPutStrLn stderr (show e) >> exitWith (ExitFailure 10) + Right r -> return r + +type Block = Stmt + diff --git a/hdiff.cabal b/hdiff.cabal new file mode 100644 --- /dev/null +++ b/hdiff.cabal @@ -0,0 +1,134 @@ +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.31.2. +-- +-- see: https://github.com/sol/hpack +-- +-- hash: b37884aac4ee07f3aa56e35f35c9f4e9a3e6f1e608768849bd352a9ec364a3c0 + +name: hdiff +version: 0.0.0 +synopsis: Pattern-Expression-based differencing of arbitrary types. +description: This package provides an executable and a library to compute and manipulate pattern-expression based differences between values of arbitrary datatypes. For more detailed information check the README at our GitHub page. +category: Other +homepage: https://github.com/VictorCMiraldo/hdiff#readme +bug-reports: https://github.com/VictorCMiraldo/hdiff/issues +maintainer: Victor Miraldo +license: MIT +license-file: LICENSE +build-type: Simple + +source-repository head + type: git + location: https://github.com/VictorCMiraldo/hdiff + +library + exposed-modules: + Data.Exists + Data.HDiff.Change + Data.HDiff.Change.Apply + Data.HDiff.Change.Classify + Data.HDiff.Change.Thinning + Data.HDiff.Change.TreeEditDistance + Data.HDiff.Diff + Data.HDiff.Diff.Modes + Data.HDiff.Diff.Preprocess + Data.HDiff.Diff.Types + Data.HDiff.Example + Data.HDiff.MetaVar + Data.HDiff.Patch + Data.HDiff.Patch.Merge + Data.HDiff.Patch.Show + Data.HDiff.Patch.Thinning + Data.HDiff.Patch.TreeEditDistance + Data.WordTrie + Generics.MRSOP.HDiff.Digest + Generics.MRSOP.HDiff.Holes + Generics.MRSOP.HDiff.Renderer + Languages.RTree + Languages.RTree.Diff + other-modules: + Paths_hdiff + hs-source-dirs: + src/ + ghc-options: -Wall + build-depends: + QuickCheck + , base >=4.9 && <5 + , bytestring + , containers + , cryptonite + , generics-mrsop >=2.1.0 + , generics-mrsop-gdiff + , hspec + , memory + , mtl + , prettyprinter + , prettyprinter-ansi-terminal + , text + default-language: Haskell2010 + +executable hdiff + main-is: HDiff.hs + other-modules: + Languages.Clojure + Languages.Clojure.AST + Languages.Clojure.Parser + Languages.Interface + Languages.Lines + Languages.Lua + Languages.While + Paths_hdiff + hs-source-dirs: + executables + ghc-options: -Wno-overlapping-patterns -Wno-inaccessible-code -Wno-incomplete-patterns -Wno-incomplete-uni-patterns -Wno-incomplete-record-updates + build-depends: + QuickCheck + , base >=4.9 && <5 + , bytestring + , containers + , cryptonite + , generics-mrsop >=2.1.0 + , generics-mrsop-gdiff + , gitrev + , hdiff + , hspec + , language-lua + , memory + , mtl + , optparse-applicative + , parsec + , prettyprinter + , prettyprinter-ansi-terminal + , text + default-language: Haskell2010 + +test-suite spec + type: exitcode-stdio-1.0 + main-is: Spec.hs + other-modules: + Data.Digems.Change.ClassifySpec + Data.Digems.Change.TreeEditDistanceSpec + Data.Digems.DiffSpec + Data.Digems.Patch.MergeSpec + Data.Digems.Patch.ThinningSpec + Data.Digems.PatchSpec + Paths_hdiff + hs-source-dirs: + tests + build-depends: + QuickCheck + , base >=4.9 && <5 + , bytestring + , containers + , cryptonite + , generics-mrsop >=2.1.0 + , generics-mrsop-gdiff + , hdiff + , hspec + , memory + , mtl + , prettyprinter + , prettyprinter-ansi-terminal + , text + default-language: Haskell2010 diff --git a/src/Data/Exists.hs b/src/Data/Exists.hs new file mode 100644 --- /dev/null +++ b/src/Data/Exists.hs @@ -0,0 +1,17 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GADTs #-} +module Data.Exists where + +data Exists (f :: k -> *) :: * where + Exists :: f x -> Exists f + +exMap :: (forall x . f x -> g x) -> Exists f -> Exists g +exMap f (Exists x) = Exists (f x) + +exMapM :: (Monad m) => (forall x . f x -> m (g x)) -> Exists f -> m (Exists g) +exMapM f (Exists x) = Exists <$> f x + +exElim :: (forall x . f x -> a) -> Exists f -> a +exElim f (Exists x) = f x + diff --git a/src/Data/HDiff/Change.hs b/src/Data/HDiff/Change.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Change.hs @@ -0,0 +1,219 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Data.HDiff.Change where + +import Control.Monad.Cont +import Control.Monad.State +import Data.Functor.Sum +import Data.Functor.Const +import qualified Data.Map as M +import qualified Data.Set as S +import Data.Type.Equality +---------------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Base +---------------------------------------- +import Data.Exists +import Data.HDiff.MetaVar +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Holes + +-- this has the ShowHO (Const a) instance +import Generics.MRSOP.AG () + + +-- |A 'CChange', or, closed change, consists in a declaration of metavariables +-- and two contexts. The precondition is that every variable declared +-- occurs at least once in ctxDel and that every variable that occurs in ctxIns +-- is declared. +-- +data CChange ki codes at where + CMatch :: { cCtxVars :: S.Set (Exists (MetaVarIK ki)) + , cCtxDel :: Holes ki codes (MetaVarIK ki) at + , cCtxIns :: Holes ki codes (MetaVarIK ki) at } + -> CChange ki codes at + +-- |smart constructor for 'CChange'. Enforces the invariant +cmatch :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at + -> CChange ki codes at +cmatch del ins = maybe (error "Data.HDiff.Change.cmatch: invariant failure") id + $ cmatch' del ins + +cmatch' :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at + -> Maybe (CChange ki codes at) +cmatch' del ins = + let vi = holesGetHolesAnnWith'' Exists ins + vd = holesGetHolesAnnWith'' Exists del + in if vi == vd + then Just $ CMatch vi del ins + else Nothing + +-- |A 'Domain' is just a deletion context. Type-synonym helps us +-- identify what's what on the algorithms below. +type Domain ki codes = Holes ki codes (MetaVarIK ki) + +domain :: CChange ki codes at -> Domain ki codes at +domain = cCtxDel + + +unCMatch :: CChange ki codes at -> (Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)) at +unCMatch (CMatch _ del ins) = del :*: ins + +-- |Returns the maximum variable in a change +cMaxVar :: CChange ki codes at -> Int +cMaxVar = maybe 0 id . S.lookupMax . S.map (exElim metavarGet) . cCtxVars + +instance HasIKProjInj ki (CChange ki codes) where + konInj k = CMatch S.empty (HOpq' k) (HOpq' k) + varProj pk (CMatch _ (Hole _ h) _) = varProj pk h + varProj _ (CMatch _ (HPeel _ _ _) _) = Just IsI + varProj _ (CMatch _ _ _) = Nothing + +instance (TestEquality ki) => TestEquality (CChange ki codes) where + testEquality (CMatch _ x _) (CMatch _ y _) + = testEquality x y + +-- |Alpha-equality for 'CChange' +changeEq :: (EqHO ki) => CChange ki codes at -> CChange ki codes at -> Bool +changeEq (CMatch v1 d1 i1) (CMatch v2 d2 i2) + = S.size v1 == S.size v2 && aux + where + aux :: Bool + aux = (`runCont` id) $ + callCC $ \exit -> flip evalStateT M.empty $ do + _ <- holesMapM (uncurry' (reg (cast exit))) (holesLCP d1 d2) + _ <- holesMapM (uncurry' (chk (cast exit))) (holesLCP i1 i2) + return True + + cast :: (Bool -> Cont Bool b) + -> Bool -> Cont Bool (Const () a) + cast f b = (const (Const ())) <$> f b + + reg :: (Bool -> Cont Bool (Const () at)) + -> Holes ki codes (MetaVarIK ki) at + -> Holes ki codes (MetaVarIK ki) at + -> StateT (M.Map Int Int) (Cont Bool) (Const () at) + reg _ (Hole' m1) (Hole' m2) + = modify (M.insert (metavarGet m1) (metavarGet m2)) + >> return (Const ()) + reg exit _ _ + = lift $ exit False + + chk :: (Bool -> Cont Bool (Const () at)) + -> Holes ki codes (MetaVarIK ki) at + -> Holes ki codes (MetaVarIK ki) at + -> StateT (M.Map Int Int) (Cont Bool) (Const () at) + chk exit (Hole' m1) (Hole' m2) + = do st <- get + case M.lookup (metavarGet m1) st of + Nothing -> lift $ exit False + Just r -> if r == metavarGet m2 + then return (Const ()) + else lift $ exit False + chk exit _ _ = lift (exit False) + +-- |Issues a copy, this is a closed change analogous to +-- > \x -> x +changeCopy :: MetaVarIK ki at -> CChange ki codes at +changeCopy vik = CMatch (S.singleton (Exists vik)) (Hole' vik) (Hole' vik) + +-- |Checks whetehr a change is a copy. +isCpy :: (EqHO ki) => CChange ki codes at -> Bool +isCpy (CMatch _ (Hole' v1) (Hole' v2)) + -- arguably, we don't even need that since changes are closed. + = metavarGet v1 == metavarGet v2 +isCpy _ = False + +makeCopyFrom :: CChange ki codes at -> CChange ki codes at +makeCopyFrom chg = case cCtxDel chg of + Hole _ var -> changeCopy var + HPeel _ _ _ -> changeCopy (NA_I (Const 0)) + HOpq _ k -> changeCopy (NA_K (Annotate 0 k)) + +-- |Renames all changes within a 'Holes' so that their +-- variable names will not clash. +cWithDisjNamesFrom :: CChange ki codes at + -> CChange ki codes at + -> CChange ki codes at +cWithDisjNamesFrom (CMatch vs del ins) q + = let vmax = cMaxVar q + 1 + in CMatch (S.map (exMap $ metavarAdd vmax) vs) + (holesMap (metavarAdd vmax) del) + (holesMap (metavarAdd vmax) ins) + +-- |A Utx with closed changes distributes over a closed change +-- +distrCChange :: Holes ki codes (CChange ki codes) at -> CChange ki codes at +distrCChange = naiveDistr -- . alphaRenameChanges + where + naiveDistr utx = + let vars = S.foldl' S.union S.empty + $ holesGetHolesAnnWith'' cCtxVars utx + del = holesJoin $ holesMap cCtxDel utx + ins = holesJoin $ holesMap cCtxIns utx + in CMatch vars del ins + +-- |A 'OChange', or, open change, is analogous to a 'CChange', +-- but has a list of free variables. These are the ones that appear +-- in 'oCtxIns' but not in 'oCtxDel' +data OChange ki codes at where + OMatch :: { oCtxVDel :: S.Set (Exists (MetaVarIK ki)) + , oCtxVIns :: S.Set (Exists (MetaVarIK ki)) + , oCtxDel :: Holes ki codes (MetaVarIK ki) at + , oCtxIns :: Holes ki codes (MetaVarIK ki) at } + -> OChange ki codes at + +-- |Given two treefixes, constructs and classifies a change from +-- them. +change :: Holes ki codes (MetaVarIK ki) at + -> Holes ki codes (MetaVarIK ki) at + -> Sum (OChange ki codes) (CChange ki codes) at +change utx uty = let vx = holesGetHolesAnnWith'' Exists utx + vy = holesGetHolesAnnWith'' Exists uty + in if vx == vy + then InR $ CMatch vx utx uty + else InL $ OMatch vx vy utx uty + +----------------------------- +-- Alternate representations + +type Holes2 ki codes + = Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki) +type HolesHoles2 ki codes + = Holes ki codes (Holes2 ki codes) + +fst' :: (f :*: g) x -> f x +fst' (Pair a _) = a + +snd' :: (f :*: g) x -> g x +snd' (Pair _ b) = b + +scDel :: HolesHoles2 ki codes at + -> Holes ki codes (MetaVarIK ki) at +scDel = holesJoin . holesMap fst' + +scIns :: HolesHoles2 ki codes at + -> Holes ki codes (MetaVarIK ki) at +scIns = holesJoin . holesMap snd' + +utx2distr :: HolesHoles2 ki codes at -> Holes2 ki codes at +utx2distr x = (scDel x :*: scIns x) + +utx22change :: HolesHoles2 ki codes at -> Maybe (CChange ki codes at) +utx22change x = cmatch' (scDel x) (scIns x) + +change2holes2 :: (EqHO ki) => CChange ki codes at -> HolesHoles2 ki codes at +change2holes2 (CMatch _ del ins) = holesLCP del ins + +instance (TestEquality f) => TestEquality (f :*: g) where + testEquality x y = testEquality (fst' x) (fst' y) + +instance HasIKProjInj ki (Holes2 ki codes) where + konInj ki = (konInj ki :*: konInj ki) + varProj p (Pair f _) = varProj p f + diff --git a/src/Data/HDiff/Change/Apply.hs b/src/Data/HDiff/Change/Apply.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Change/Apply.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- |Defines the application function for a 'Data.HDiff.Change.CChange' +module Data.HDiff.Change.Apply where + +import Data.Proxy +import Data.Type.Equality +import Data.Functor.Const +import qualified Data.Map as M +import Control.Monad.Except + +import Data.Exists +import Data.HDiff.MetaVar +import Data.HDiff.Change + +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Holes + +-- * Generic Application +-- +-- $genapply +-- +-- A 'CChange' can be applied to any treefix by pattern matching +-- over the deletion context and instantiating over the insertion context. + +-- |Application might fail with some 'ApplicationErr' describing +-- the point of failure. +data ApplicationErr :: (kon -> *) -> [[[Atom kon]]] -> (Atom kon -> *) -> * where + UndefinedVar :: Int -> ApplicationErr ki codes phi + FailedContraction :: Int + -> Holes ki codes phi ix + -> Holes ki codes phi ix + -> ApplicationErr ki codes phi + IncompatibleTypes :: ApplicationErr ki codes phi + IncompatibleOpqs :: ki k + -> ki k + -> ApplicationErr ki codes phi + IncompatibleHole :: Holes ki codes (MetaVarIK ki) ix + -> phi ix + -> ApplicationErr ki codes phi + IncompatibleTerms :: Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes phi ix + -> ApplicationErr ki codes phi + +instance Show (ApplicationErr ki codes phi) where + show (UndefinedVar i) = "(UndefinedVar " ++ show i ++ ")" + show (FailedContraction i _ _) = "(FailedContraction " ++ show i ++ ")" + show (IncompatibleTerms _ _) = "IncompatibleTerms" + show (IncompatibleOpqs _ _) = "IncompatibleOpq" + show (IncompatibleHole _ _) = "IncompatibleHole" + show (IncompatibleTypes) = "IncompatibleTypes" + +-- |A instantiation substitution from metavariable numbers to some treefix +type Subst ki codes phi = M.Map Int (Exists (Holes ki codes phi)) + +type Applicable ki codes phi = (ShowHO ki , EqHO ki , TestEquality ki , TestEquality phi + , HasIKProjInj ki phi , EqHO phi) + +-- |We try to unify @pa@ and @pq@ onto @ea@. The idea is that +-- we instantiate the variables of @pa@ with their corresponding expression +-- on @x@, and substitute those in @ea@. Whereas if we reach a variable in @x@ +-- we ignore whatever was on @ea@ and give that variable instead. +-- +-- We are essentially applying +genericApply :: (Applicable ki codes phi) + => CChange ki codes at + -> Holes ki codes phi at + -> Either (ApplicationErr ki codes phi) (Holes ki codes phi at) +genericApply chg x = runExcept (pmatch (cCtxDel chg) x >>= transport (cCtxIns chg)) + +-- |Specializes 'genericApply' to work over terms of our language, ie, 'NA's +termApply :: forall ki codes at + . (ShowHO ki , EqHO ki , TestEquality ki) + => CChange ki codes at + -> NA ki (Fix ki codes) at + -> Either String (NA ki (Fix ki codes) at) +termApply chg = either (Left . show) (holes2naM cast) + . genericApply chg + . na2holes + where + -- cast is used only to fool the compiler here! Since the + -- Holes comes from 'utxStiff', it has no occurence of 'HolesHole' + -- and hence genericApply will return a term with no such + -- occurence. Yet, it requires a EqHO instance for phi, so + -- we provide one + cast :: MetaVarIK ki ix + -> Either String (NA ki (Fix ki codes) ix) + cast _ = Left "Data.HDiff.Change.Apply: impossible" + + +-- |@pmatch pa x@ traverses @pa@ and @x@ instantiating the variables of @pa@. +-- Upon sucessfully instantiating the variables, returns the substitution. +pmatch :: (Applicable ki codes phi) + => Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes phi ix + -> Except (ApplicationErr ki codes phi) (Subst ki codes phi) +pmatch pat = pmatch' M.empty pat + +pmatch' :: (Applicable ki codes phi) + => Subst ki codes phi + -> Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes phi ix + -> Except (ApplicationErr ki codes phi) (Subst ki codes phi) +pmatch' s (Hole _ var) x = substInsert s var x +pmatch' _ pa (Hole _ var) = throwError (IncompatibleHole pa var) +pmatch' s (HOpq _ oa) (HOpq _ ox) + | eqHO oa ox = return s + | otherwise = throwError (IncompatibleOpqs oa ox) +pmatch' s pa@(HPeel _ ca ppa) x@(HPeel _ cx px) = + case testEquality ca cx of + Nothing -> throwError (IncompatibleTerms pa x) + Just Refl -> getConst <$> + cataNPM (\y (Const val) -> fmap Const (uncurry' (pmatch' val) y)) + (return $ Const s) + (zipNP ppa px) + +-- |Given a 'MetaVarIK' and a 'Holes', decide whether their indexes +-- are equal. +idxDecEq :: forall ki codes phi at ix + . (TestEquality ki , TestEquality phi, HasIKProjInj ki phi) + => Holes ki codes phi at + -> MetaVarIK ki ix + -> Maybe (at :~: ix) +idxDecEq utx (NA_K (Annotate _ k)) = testEquality utx (konInj k) +idxDecEq utx i@(NA_I _) + = case varProj (Proxy :: Proxy ki) utx of + Nothing -> Nothing + Just prf@IsI -> apply (Refl :: 'I :~: 'I) + <$> testEquality (getIsISNat prf) (getSNatI i) + where + getSNatI :: MetaVarIK ki ('I i) -> SNat i + getSNatI (NA_I _) = getSNat (Proxy :: Proxy i) + +-- |Attempts to insert a new binding into a substitution. If the variable is already +-- bound, we check the existing binding for equality +substInsert :: (Applicable ki codes phi) + => Subst ki codes phi + -> MetaVarIK ki ix + -> Holes ki codes phi ix + -> Except (ApplicationErr ki codes phi) (Subst ki codes phi) +substInsert s var new = case M.lookup (metavarGet var) s of + Nothing -> return $ M.insert (metavarGet var) (Exists new) s + Just (Exists old) -> case testEquality old new of + Nothing -> throwError IncompatibleTypes + Just Refl -> if old == new + then return s + else throwError (FailedContraction (metavarGet var) old new) + +-- |Instantiates the metavariables in the given term +-- using the substitution in the state +transport :: (Applicable ki codes phi) + => Holes ki codes (MetaVarIK ki) ix + -> Subst ki codes phi + -> Except (ApplicationErr ki codes phi) (Holes ki codes phi ix) +transport (Hole _ var) s = lookupVar var s + >>= maybe (throwError $ UndefinedVar $ metavarGet var) + return +transport (HOpq _ oy) _ = return $ HOpq' oy +transport (HPeel _ cy py) s = HPeel' cy <$> mapNPM (flip transport s) py + +-- |Looks for the value of a @MetaVarIK ki ix@ in the substitution +-- in our state. Returns @Nothing@ when the variables is not found +-- or throws 'IncompatibleTypes' when the value registered in the +-- substitution is of type @iy@ with @ix /= iy@. +lookupVar :: forall ki codes phi ix + . (Applicable ki codes phi) + => MetaVarIK ki ix + -> Subst ki codes phi + -> Except (ApplicationErr ki codes phi) (Maybe (Holes ki codes phi ix)) +lookupVar var subst = do + case M.lookup (metavarGet var) subst of + Nothing -> return Nothing + Just r -> Just <$> cast r + where + cast :: Exists (Holes ki codes phi) + -> Except (ApplicationErr ki codes phi) (Holes ki codes phi ix) + cast (Exists res) = case idxDecEq res var of + Nothing -> throwError IncompatibleTypes + Just Refl -> return res + diff --git a/src/Data/HDiff/Change/Classify.hs b/src/Data/HDiff/Change/Classify.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Change/Classify.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-orphans #-} +-- |change classification algorithm +module Data.HDiff.Change.Classify where + +import Data.List (nub) +import Data.Proxy +import Data.Type.Equality +------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +------------------------------- +import Data.Exists +import Data.HDiff.Change +import Data.HDiff.MetaVar + +----------------------------------------- +-- Change Classification algo + +instance (EqHO ki , TestEquality ki) => Eq (Exists (Holes ki codes (MetaVarIK ki))) where + (Exists v) == (Exists u) = + case testEquality v u of + Nothing -> False + Just Refl -> v == u + +getConstrSNat :: (IsNat n) => Constr sum n -> SNat n +getConstrSNat _ = getSNat (Proxy :: Proxy n) + +holesGetMultiplicities :: Int -> Holes ki codes f at -> [Exists (Holes ki codes f)] +holesGetMultiplicities k utx + | holesArity utx == k = [Exists utx] + | otherwise = case utx of + HPeel _ _ p -> concat $ elimNP (holesGetMultiplicities k) p + _ -> [] + + +data ChangeClass + = CPerm | CMod | CId | CIns | CDel + deriving (Eq , Show , Ord) + +changeClassify :: (EqHO ki , TestEquality ki) + => CChange ki codes at -> ChangeClass +changeClassify c + | isCpy c = CId + | otherwise = + let mis = holesGetMultiplicities 0 (cCtxIns c) + mds = holesGetMultiplicities 0 (cCtxDel c) + vi = holesGetHolesAnnWith' metavarGet (cCtxIns c) + vd = holesGetHolesAnnWith' metavarGet (cCtxDel c) + -- permutes = vi == vd + dups = vi /= nub vi || vd /= nub vd + in case (length mis , length mds) of + (0 , 0) -> CPerm -- can't duplicate as one variable on one side would + -- be left unused; Can't have that so a tree with + -- multiplicity 0 would be there + (0 , _) -> if dups then CMod else CDel + (_ , 0) -> if dups then CMod else CIns + (_ , _) -> if mis == mds then CPerm else CMod + +isIns , isDel :: (TestEquality ki , EqHO ki) => CChange ki codes ix -> Bool +isIns c = changeClassify c == CIns +isDel c = changeClassify c == CDel + diff --git a/src/Data/HDiff/Change/Thinning.hs b/src/Data/HDiff/Change/Thinning.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Change/Thinning.hs @@ -0,0 +1,191 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Data.HDiff.Change.Thinning where + +import Data.Type.Equality +import qualified Data.Map as M +import qualified Data.Set as S +import Control.Monad.Writer +import Control.Monad.Except +import Control.Monad.State +--------------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +--------------------------------------- +import Data.Exists +import Data.HDiff.MetaVar +import Data.HDiff.Change +import Data.HDiff.Change.Apply + +import Debug.Trace + +type ThinningErr ki codes = ApplicationErr ki codes (MetaVarIK ki) + +-- Haskell tends to want a type-signature for some non-trivial lifts. +lift' :: (Monad m) => m a -> StateT (Subst ki codes (MetaVarIK ki)) m a +lift' = lift + +thin :: (ShowHO ki , TestEquality ki, EqHO ki) + => CChange ki codes at + -> Domain ki codes at + -> Either (ApplicationErr ki codes (MetaVarIK ki)) + (CChange ki codes at) +thin chg dom = uncurry' cmatch <$> thinUTx2 (cCtxDel chg :*: cCtxIns chg) dom + +tr :: (ShowHO ki , TestEquality ki, EqHO ki) + => CChange ki codes at + -> CChange ki codes at + -> Either (ApplicationErr ki codes (Holes2 ki codes)) + (CChange ki codes at) +tr (CMatch _ dp ip) q = do + xx <- genericApply q (holesLCP dp ip) + let xd = holesJoin $ holesMap fst' xx + let xi = holesJoin $ holesMap snd' xx + return $ CMatch S.empty xd xi +{- + sigmaD <- pmatch qd pd + sigmaI <- pmatch qd pi + resD <- transport qi sigmaD + resI <- transport qi sigmaI + return (cmatch resD resI) +-} + +thinUTx2 :: (ShowHO ki , TestEquality ki, EqHO ki) + => Holes2 ki codes at + -> Domain ki codes at + -> Either (ApplicationErr ki codes (MetaVarIK ki)) + (Holes2 ki codes at) +thinUTx2 (del :*: ins) dom = runExcept $ do + sigma <- flip execStateT M.empty $ utxThin del dom + sigma' <- minimize sigma + del' <- refine del sigma' + ins' <- refine ins sigma' + return $ del' :*: ins' + +thin' :: (ShowHO ki , TestEquality ki, EqHO ki) + => Holes2 ki codes at + -> Holes2 ki codes at + -> Either (ApplicationErr ki codes (MetaVarIK ki)) + (Holes2 ki codes at) +thin' (delP :*: insP) (delQ :*: insQ) = runExcept $ do + sigma <- flip execStateT M.empty $ utxThin delP delQ + sigma' <- minimize sigma + del <- refine delP sigma' + insP' <- refine insP sigma' + insQ' <- refine insQ sigma' + qi <- trace "b" $ (pmatch del insQ' >>= transport insP') + return $ insP' :*: qi + + + + + +-- |The @thin' p q@ function is where work where we produce the +-- map that will be applied to 'p' in order to thin it. +-- This function does /NOT/ minimize this map. +-- +utxThin :: (ShowHO ki , TestEquality ki, EqHO ki) + => Holes ki codes (MetaVarIK ki) at + -> Domain ki codes at + -> StateT (Subst ki codes (MetaVarIK ki)) + (Except (ThinningErr ki codes)) + () +utxThin p0 q0 = void $ holesMapM (uncurry' go) $ holesLCP p0 q0 + where + go :: (ShowHO ki , TestEquality ki, EqHO ki) + => Holes ki codes (MetaVarIK ki) at + -> Domain ki codes at + -> StateT (Subst ki codes (MetaVarIK ki)) + (Except (ThinningErr ki codes)) + (Holes ki codes (MetaVarIK ki) at) + go p (Hole _ var) = record_eq var p >> return p + go p@(Hole _ var) q = record_eq var q >> return p + go p q | eqHO p q = return p + | otherwise = throwError (IncompatibleTerms p q) + + -- Whenever we see a variable being matched against a term + -- we record the equivalence. First we make sure we did not + -- record such equivalence yet, otherwise, we recursively thin + record_eq :: (ShowHO ki , TestEquality ki, EqHO ki) + => MetaVarIK ki at + -> Holes ki codes (MetaVarIK ki) at + -> StateT (Subst ki codes (MetaVarIK ki)) + (Except (ThinningErr ki codes)) + () + record_eq var q = do + sigma <- get + mterm <- lift (lookupVar var sigma) + case mterm of + -- First time we see 'var', we instantiate it and get going. + Nothing -> when (q /= Hole' var) + $ modify (M.insert (metavarGet var) (Exists q)) + -- It's not the first time we thin 'var'; previously, we had + -- that 'var' was supposed to be p'. We will check whether it + -- is the same as q, if not, we will have to thin p' with q. + Just q' -> unless (eqHO q' q) + $ void $ utxThin q' q + + + +-- |The minimization step performs the 'occurs' check and removes +-- unecessary steps. For example; +-- +-- > sigma = fromList +-- > [ (0 , bin 1 2) +-- > , (1 , bin 4 4) ] +-- +-- Then, @minimize sigma@ will return @fromList [(0 , bin (bin 4 4) 2)]@ +-- +minimize :: forall ki codes + . (ShowHO ki, EqHO ki , TestEquality ki) + => Subst ki codes (MetaVarIK ki) + -> Except (ThinningErr ki codes) (Subst ki codes (MetaVarIK ki)) +minimize sigma = whileM sigma [] $ \s _ + -> M.fromList <$> (mapM (secondF (exMapM go)) (M.toList s)) + where + secondF :: (Functor m) => (a -> m b) -> (x , a) -> m (x , b) + secondF f (x , a) = (x,) <$> f a + + -- The actual engine of the 'minimize' function is thinning the + -- variables that appear in the image of the substitution under production. + -- We use the writer monad to inform us wich variables have been fully + -- eliminated. Once this process returns no eliminated variables, + -- we are done. + go :: Holes ki codes (MetaVarIK ki) at + -> WriterT [Int] (Except (ThinningErr ki codes)) + (Holes ki codes (MetaVarIK ki) at) + go = holesRefineVarsM $ \_ var -> do + mterm <- lift (lookupVar var sigma) + case mterm of + Nothing -> return (Hole' var) + Just r -> tell [metavarGet var] + >> return r + + whileM :: (Monad m, Show x) + => a -> [x] -> (a -> [x] -> WriterT [x] m a) -> m a + whileM a xs f = runWriterT (f a xs) + >>= \(x' , xs') -> if null xs' + then return x' + else whileM x' xs' f + + +-- |This is similar to 'transport', but does not throw errors +-- on undefined variables. +refine :: (ShowHO ki , TestEquality ki , EqHO ki) + => Holes ki codes (MetaVarIK ki) ix + -> Subst ki codes (MetaVarIK ki) + -> Except (ThinningErr ki codes) (Holes ki codes (MetaVarIK ki) ix) +refine (Hole _ var) s = lookupVar var s >>= return . maybe (Hole' var) id +refine (HOpq _ oy) _ = return $ HOpq' oy +refine (HPeel _ cy py) s = HPeel' cy <$> mapNPM (flip refine s) py + diff --git a/src/Data/HDiff/Change/TreeEditDistance.hs b/src/Data/HDiff/Change/TreeEditDistance.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Change/TreeEditDistance.hs @@ -0,0 +1,345 @@ +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Data.HDiff.Change.TreeEditDistance where + +import qualified Data.Map as M +import Data.STRef +import Data.Proxy +import Data.Type.Equality +import Control.Arrow (second) +import Control.Monad.ST +import Control.Monad.Except +import Control.Monad.Reader + +import Generics.MRSOP.Holes +import Generics.MRSOP.Base +import qualified Generics.MRSOP.GDiff as GD + +import Data.Exists +import Data.HDiff.MetaVar +import Data.HDiff.Change +import Data.HDiff.Change.Apply + +-- import Debug.Trace + +-------------------------------------------- +-- * Regular Longest Common Subsequence * -- +-------------------------------------------- + +data ListES a + = LC Int a (ListES a) + | LD Int a (ListES a) + | LI Int a (ListES a) + | LNil + deriving (Eq , Show) + +cost :: ListES a -> Int +cost LNil = 0 +cost (LC c _ _) = c +cost (LI c _ _) = c +cost (LD c _ _) = c + +-- Will make sure to copy just the last bit on a row of things. +-- For example, +-- +-- > λ> lcs [0,1,2] [0,1,1,1,2] +-- > LC 0 (LC 1 (LI 1 (LI 1 (LC 2 LNil)))) +-- +-- Note how the 1 is copied to the first position, then +-- the other ones are inserted. +-- +-- > λ> pushCopiesIns $ lcsW (const 1) [0,1,2] [0,1,1,1,2] +-- > LC 0 (LI 1 (LI 1 (LC 1 (LC 2 LNil)))) +-- +-- Here instead, we insert two 1's then copy the last one. +-- This really helps with synchronization. +pushCopiesIns :: (Eq a) => ListES a -> ListES a +pushCopiesIns LNil = LNil +pushCopiesIns (LC _ c (LI _ c' es)) + | c == c' = LI 0 c' (pushCopiesIns (LC 0 c es)) + | otherwise = LC 0 c (pushCopiesIns (LI 0 c' es)) +pushCopiesIns (LC _ c es) = LC 0 c (pushCopiesIns es) +pushCopiesIns (LI _ c es) = LI 0 c (pushCopiesIns es) +pushCopiesIns (LD _ c es) = LD 0 c (pushCopiesIns es) + + +meet :: ListES a -> ListES a -> ListES a +meet a b + | cost a <= cost b = a + | otherwise = b + +type Table a = M.Map (Int , Int) (ListES a) + +-- Memoized longest-common-subsequence with parametrizable weight +lcsW :: forall a . (Eq a) => (a -> Int) -> [a] -> [a] -> ListES a +lcsW weight xs0 ys0 = runST $ do + tbl <- newSTRef M.empty + lcs' tbl xs0 ys0 + where + lcs' :: STRef s (Table a) -> [a] -> [a] -> ST s (ListES a) + lcs' tbl xs ys = do + let ix = (length xs , length ys) + m <- readSTRef tbl + case M.lookup ix m of + Just res -> return res + Nothing -> do res <- lcs'' tbl xs ys + modifySTRef tbl (M.insert ix res) + return $ res + + lcs'' :: STRef s (Table a) -> [a] -> [a] -> ST s (ListES a) + lcs'' _ [] [] = return LNil + lcs'' tbl (x:xs) [] = lcs' tbl xs [] >>= \d -> return (LD (weight x + cost d) x d) + lcs'' tbl [] (y:ys) = lcs' tbl [] ys >>= \i -> return (LI (weight y + cost i) y i) + lcs'' tbl (x:xs) (y:ys) = + do i <- lcs' tbl (x:xs) ys + c <- lcs' tbl xs ys + d <- lcs' tbl xs (y:ys) + let di = meet (LD (weight x + cost d) x d) (LI (weight y + cost i) y i) + return $ if x == y then meet (LC (cost c) x c) di else di + +--------------------------------------------- +-- * Translating Changes to Edit Scripts * -- +--------------------------------------------- + +fromNA :: NA ki (Fix ki codes) at -> Holes ki codes (MetaVarIK ki) at +fromNA = na2holes + +toES :: (EqHO ki , ShowHO ki , TestEquality ki) + => CChange ki codes at -> NA ki (Fix ki codes) at + -> Either String (GD.ES ki codes '[ at ] '[ at ]) +toES (CMatch _ del ins) elm = + -- Since we can't have duplications or swaps in the edit-script + -- world, we must decide which variables will be copied. + -- To do that, we will run a least-common-subsequence weighting + -- each variable by the size of the tree it was instantiated too. + let vd = reverse $ holesGetHolesAnnWith' metavarGet del + vi = reverse $ holesGetHolesAnnWith' metavarGet ins + in case runExcept (pmatch del (fromNA elm)) of + Left err -> Left ("Element not in domain. " ++ show err) + Right s -> + let sizes_s = M.map (exElim holesSize) s + ves = pushCopiesIns $ lcsW (\v -> sizes_s M.! v) vd vi + in runExcept (runReaderT (compress <$> delPhase (del :* NP0) (ins :* NP0)) (s , ves)) + +type ToES ki codes = ReaderT (Subst ki codes (MetaVarIK ki) , ListES Int) + (Except String) + +askSubst :: ToES ki codes (Subst ki codes (MetaVarIK ki)) +askSubst = asks fst + +askListES :: ToES ki codes (ListES Int) +askListES = asks snd + +gcpy :: GD.Cof ki codes at l + -> GD.ES ki codes (l :++: ds) (l :++: is) + -> GD.ES ki codes (at : ds) (at : is) +gcpy c e = GD.Cpy (GD.cost e) c e + +gins :: GD.Cof ki codes at l + -> GD.ES ki codes ds (l :++: is) + -> GD.ES ki codes ds (at : is) +gins c e = GD.Ins (1 + GD.cost e) c e + +gdel :: GD.Cof ki codes at l + -> GD.ES ki codes (l :++: ds) is + -> GD.ES ki codes (at : ds) is +gdel c e = GD.Del (1 + GD.cost e) c e + +compress :: (EqHO ki , TestEquality ki) => GD.ES ki codes is ds -> GD.ES ki codes is ds +compress GD.ES0 = GD.ES0 +compress (GD.Del _ v (GD.Ins c' v' e)) = + case GD.heqCof v v' of + Just (Refl , Refl) -> gcpy v (compress e) + Nothing -> gdel v (compress $ GD.Ins c' v' e) +compress (GD.Del _ v e) + = gdel v $ compress e +compress (GD.Ins _ v (GD.Del c' v' e)) = + case GD.heqCof v v' of + Just (Refl , Refl) -> gcpy v (compress e) + Nothing -> gins v (compress $ GD.Del c' v' e) +compress (GD.Ins _ v e) + = gins v $ compress e +compress (GD.Cpy _ v e) + = gcpy v (compress e) + +cpyOnly :: (EqHO ki , ShowHO ki , TestEquality ki) + => NP (Holes ki codes (MetaVarIK ki)) xs + -> ToES ki codes (GD.ES ki codes xs xs) +cpyOnly NP0 = return GD.ES0 +cpyOnly (Hole _ var :* xs) = fetch var >>= cpyOnly . (:* xs) +cpyOnly (HOpq _ k :* xs) = gcpy (GD.ConstrK k) <$> cpyOnly xs +cpyOnly (HPeel _ c d :* xs) = gcpy (GD.ConstrI c (listPrfNP d)) <$> cpyOnly (appendNP d xs) + +delOnly :: (EqHO ki , ShowHO ki , TestEquality ki) + => NP (Holes ki codes (MetaVarIK ki)) ds + -> ToES ki codes (GD.ES ki codes ds '[]) +delOnly NP0 = return GD.ES0 +delOnly (Hole _ var :* xs) = fetch var >>= delOnly . (:* xs) +delOnly (HOpq _ k :* xs) = gdel (GD.ConstrK k) <$> delOnly xs +delOnly (HPeel _ c d :* xs) = gdel (GD.ConstrI c (listPrfNP d)) <$> delOnly (appendNP d xs) + +insOnly :: (EqHO ki , ShowHO ki , TestEquality ki) + => NP (Holes ki codes (MetaVarIK ki)) is + -> ToES ki codes (GD.ES ki codes '[] is) +insOnly NP0 = return GD.ES0 +insOnly (Hole _ var :* xs) = fetch var >>= insOnly . (:* xs) +insOnly (HOpq _ k :* xs) = gins (GD.ConstrK k) <$> insOnly xs +insOnly (HPeel _ c d :* xs) = gins (GD.ConstrI c (listPrfNP d)) <$> insOnly (appendNP d xs) + +listAssoc :: ListPrf a -> Proxy b -> Proxy c + -> ListPrf ((a :++: b) :++: c) :~: ListPrf (a :++: (b :++: c)) +listAssoc Nil _ _ = Refl +listAssoc (Cons pa) pb pc = case listAssoc pa pb pc of + Refl -> Refl + +listDrop :: ListPrf i -> ListPrf (i :++: t) -> ListPrf t +listDrop Nil a = a +listDrop (Cons x) (Cons a) = listDrop x a + +esDelListPrf :: GD.ES ki codes ds is -> ListPrf ds +esDelListPrf GD.ES0 = Nil +esDelListPrf (GD.Cpy _ v e) = Cons $ listDrop (cofListPrf v) (esDelListPrf e) +esDelListPrf (GD.Del _ v e) = Cons $ listDrop (cofListPrf v) (esDelListPrf e) +esDelListPrf (GD.Ins _ _ e) = esDelListPrf e + +esInsListPrf :: GD.ES ki codes ds is -> ListPrf is +esInsListPrf GD.ES0 = Nil +esInsListPrf (GD.Cpy _ v e) = Cons $ listDrop (cofListPrf v) (esInsListPrf e) +esInsListPrf (GD.Ins _ v e) = Cons $ listDrop (cofListPrf v) (esInsListPrf e) +esInsListPrf (GD.Del _ _ e) = esInsListPrf e + +cofListPrf :: GD.Cof ki codes at l -> ListPrf l +cofListPrf (GD.ConstrK _) = Nil +cofListPrf (GD.ConstrI _ p) = p + +esDelListProxy :: GD.ES ki codes ds is -> Proxy ds +esDelListProxy _ = Proxy + +esDelListProxy' :: GD.ES ki codes (d : ds) is -> Proxy ds +esDelListProxy' _ = Proxy + +esInsListProxy :: GD.ES ki codes ds is -> Proxy is +esInsListProxy _ = Proxy + +esInsListProxy' :: GD.ES ki codes ds (i : is) -> Proxy is +esInsListProxy' _ = Proxy + +esDelCong :: ListPrf ds :~: ListPrf ds' -> GD.ES ki codes ds is -> GD.ES ki codes ds' is +esDelCong Refl = id + +esInsCong :: ListPrf is :~: ListPrf is' -> GD.ES ki codes ds is -> GD.ES ki codes ds is' +esInsCong Refl = id + +appendES :: GD.ES ki codes ds is + -> GD.ES ki codes ds' is' + -> GD.ES ki codes (ds :++: ds') (is :++: is') +appendES GD.ES0 b = b +appendES x@(GD.Del _ v a) b = + case appendES a b of + res -> case listAssoc (cofListPrf v) (esDelListProxy' x) (esDelListProxy b) of + prf -> gdel v $ esDelCong prf res +appendES x@(GD.Ins _ v a) b = + case appendES a b of + res -> case listAssoc (cofListPrf v) (esInsListProxy' x) (esInsListProxy b) of + prf -> gins v $ esInsCong prf res +appendES x@(GD.Cpy _ v a) b = + case appendES a b of + res -> case listAssoc (cofListPrf v) (esInsListProxy' x) (esInsListProxy b) of + prf -> case listAssoc (cofListPrf v) (esDelListProxy' x) (esDelListProxy b) of + prf' -> gcpy v $ esDelCong prf' $ esInsCong prf res + +fetch :: (EqHO ki , ShowHO ki , TestEquality ki) + => MetaVarIK ki at + -> ToES ki codes (Holes ki codes (MetaVarIK ki) at) +fetch var = do + sigma <- askSubst + case runExcept (lookupVar var sigma) of + Left err -> throwError $ "fetch: " ++ show err + Right Nothing -> throwError $ "fetch: var not found" + Right (Just t) -> return t + +delSync :: (EqHO ki , ShowHO ki , TestEquality ki) + => MetaVarIK ki at + -> NP (Holes ki codes (MetaVarIK ki)) ds + -> NP (Holes ki codes (MetaVarIK ki)) is + -> ToES ki codes (GD.ES ki codes (at ': ds) is) +delSync var ds is = do + ls <- askListES + case ls of + -- This variable is meant to be 'deleted'; so we put the right + -- number of dels there. + LD _ var' es' -> if var' /= metavarGet var + then throwError "delSync: var mismatch" + else do + t <- fetch var + es0 <- delOnly (t :* NP0) + es1 <- local (second (const es')) + $ delPhase ds is + return (appendES es0 es1) + -- Otherwise, we delegate the sharing to the insertion phase + -- This is by convention. + _ -> insPhase (Hole' var :* ds) is + +insSync :: (EqHO ki , ShowHO ki , TestEquality ki) + => MetaVarIK ki at + -> NP (Holes ki codes (MetaVarIK ki)) ds + -> NP (Holes ki codes (MetaVarIK ki)) is + -> ToES ki codes (GD.ES ki codes ds (at ': is)) +insSync var ds is = do + ls <- askListES + case ls of + -- This variable is meant to be 'deleted'; so we put the right + -- number of ins there. + LI _ var' es' -> if var' /= metavarGet var + then throwError "insSync: var mismatch" + else do + t <- fetch var + es0 <- insOnly (t :* NP0) + es1 <- local (second (const es')) + $ insPhase ds is + return (appendES es0 es1) + -- Otherwise, if this is a deletion, we sent iy back to the delete phase + LD _ _var' _es' -> delPhase ds (Hole' var :* is) + + -- Last case, it's an actual share; we gotta remove the var from the deletion + -- list and proceed. + LC _ var' es' -> case ds of + -- If the copy is already there, we take it + (Hole' var'' :* ds') -> + if var' /= metavarGet var + then throwError "insSync: var mismatch" + else do + t <- fetch var + es0 <- cpyOnly (t :* NP0) + es1 <- local (second (const es')) + $ delPhase ds' is + case testEquality var var'' of + Just Refl -> return $ appendES es0 es1 + Nothing -> throwError "insSync: types mismatch" + -- Otherwise, we must enter the deletion phase until + -- we find it. + _ -> delPhase ds (Hole' var :* is) + LNil -> throwError "insSync: premature LNil" + +delPhase , insPhase + :: (EqHO ki , ShowHO ki , TestEquality ki) + => NP (Holes ki codes (MetaVarIK ki)) ds + -> NP (Holes ki codes (MetaVarIK ki)) is + -> ToES ki codes (GD.ES ki codes ds is) +delPhase NP0 is = insOnly is +delPhase (d :* ds) is = + case d of + Hole _ var -> delSync var ds is + HOpq _ k -> gdel (GD.ConstrK k) <$> insPhase ds is + HPeel _ c p -> gdel (GD.ConstrI c (listPrfNP p)) <$> insPhase (appendNP p ds) is + +insPhase ds NP0 = delOnly ds +insPhase ds (i :* is) = + case i of + Hole _ var -> insSync var ds is + HOpq _ k -> gins (GD.ConstrK k) <$> delPhase ds is + HPeel _ c p -> gins (GD.ConstrI c (listPrfNP p)) <$> delPhase ds (appendNP p is) + diff --git a/src/Data/HDiff/Diff.hs b/src/Data/HDiff/Diff.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Diff.hs @@ -0,0 +1,215 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +module Data.HDiff.Diff + ( diffOpts' + , diffOpts + , diff + , DiffMode(..) + , module Data.HDiff.Diff.Types + ) where + +import qualified Data.Set as S +import Data.Void +import Data.Functor.Const +import Data.Functor.Sum + +import Control.Monad.State + +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Digest + +import qualified Data.WordTrie as T +import Data.HDiff.Diff.Types +import Data.HDiff.Diff.Modes +import Data.HDiff.Diff.Preprocess +import Data.HDiff.Patch +import Data.HDiff.MetaVar +import Data.HDiff.Change + +-- |We use a number of 'PrePatch'es, that is, a utx with a distinguished prefix +-- and some pair of 'Holes's inside. +type PrePatch ki codes phi = Holes ki codes (Holes ki codes phi :*: Holes ki codes phi) + +-- * Diffing +-- + +-- |Given a merkelized fixpoint, builds a trie of hashes of +-- every subtree, as long as they are taller than +-- minHeight. This trie keeps track of the arity, so +-- we can later annotate the trees that can be propper shares. +buildArityTrie :: DiffOptions -> PrepFix a ki codes phi ix -> T.Trie Int +buildArityTrie opts df = go df T.empty + where + ins :: Digest -> T.Trie Int -> T.Trie Int + ins = T.insertWith 1 (+1) . toW64s + + minHeight = doMinHeight opts + + go :: PrepFix a ki codes phi ix -> T.Trie Int -> T.Trie Int + go (HOpq (Const prep) _) t + -- We only populat the sharing map if opaques are supposed + -- to be handled as recursive trees + | doOpaqueHandling opts == DO_AsIs = ins (treeDigest prep) t + | otherwise = t + -- TODO: think about holes. I'm posponing this until + -- we actually use diffing things holes. + go (Hole (Const _) _) t = t + go (HPeel (Const prep) _ p) t + | treeHeight prep <= minHeight = t + | otherwise + = ins (treeDigest prep) $ getConst + $ cataNP (\af -> Const . go af . getConst) (Const t) p + +-- |Given two merkelized trees, returns the trie that indexes +-- the subtrees that belong in both, ie, +-- +-- @forall t . t `elem` buildSharingTrie x y +-- ==> t `subtree` x && t `subtree` y@ +-- +-- Moreover, we keep track of both the metavariable supposed +-- to be associated with a tree and the tree's arity. +-- +buildSharingTrie :: DiffOptions + -> PrepFix a ki codes phi ix + -> PrepFix a ki codes phi ix + -> (Int , IsSharedMap) +buildSharingTrie opts x y + = T.mapAccum (\i ar -> (i+1 , MAA i ar) ) 0 + $ T.zipWith (+) (buildArityTrie opts x) + (buildArityTrie opts y) + +-- |Given two treefixes, we will compute the longest path from +-- the root that they overlap and will factor it out. +-- This is somehow analogous to a @zipWith@. Moreover, however, +-- we also copy the opaque values present in the spine by issuing +-- /"copy"/ changes +extractSpine :: forall ki codes phi at + . (EqHO ki) + => DiffOpaques + -> (forall ix . phi ix -> MetaVarIK ki ix) + -> Int + -> Holes ki codes phi at + -> Holes ki codes phi at + -> Holes ki codes (Sum (OChange ki codes) (CChange ki codes)) at +extractSpine dopq meta maxI dx dy + = holesMap (uncurry' change) + $ issueOpqCopiesSpine + $ holesLCP dx dy + where + issueOpqCopiesSpine + = flip evalState maxI + . holesRefineAnnM (\_ (x :*: y) -> return $ Hole' $ holesMap meta x + :*: holesMap meta y) + (const $ if dopq == DO_OnSpine + then doCopy + else noCopy) + + noCopy :: ki k -> State Int (PrePatch ki codes (MetaVarIK ki) ('K k)) + noCopy kik = return (HOpq' kik) + + doCopy :: ki k -> State Int (PrePatch ki codes (MetaVarIK ki) ('K k)) + doCopy ki = do + i <- get + put (i+1) + let ann = NA_K . Annotate i $ ki + return $ Hole' (Hole' ann :*: Hole' ann) + + +-- |Combines changes until they are closed +close :: Holes ki codes (Sum (OChange ki codes) (CChange ki codes)) at + -> Holes ki codes (CChange ki codes) at +close utx = case closure utx of + InR cc -> cc + InL (OMatch used unused del ins) + -> Hole' $ CMatch (S.union used unused) del ins + where + closure :: Holes ki codes (Sum (OChange ki codes) (CChange ki codes)) at + -> Sum (OChange ki codes) (Holes ki codes (CChange ki codes)) at + closure (HOpq _ k) = InR $ HOpq' k + closure (Hole _ (InL oc)) = InL oc + closure (Hole _ (InR cc)) = InR $ Hole' cc + -- There is some magic going on here. First we compute + -- the recursive closures and check whether any of them is open. + -- If not, we are done. + -- Otherwise, we apply a bunch of "monad distributive properties" around. + closure (HPeel _ cx dx) + = let aux = mapNP closure dx + in case mapNPM fromInR aux of + Just np -> InR $ HPeel' cx np + Nothing -> let chgs = mapNP (either' InL (InR . distrCChange)) aux + dels = mapNP (either' oCtxDel cCtxDel) chgs + inss = mapNP (either' oCtxIns cCtxIns) chgs + vx = S.unions $ elimNP (either'' oCtxVDel cCtxVars) chgs + vy = S.unions $ elimNP (either'' oCtxVIns cCtxVars) chgs + in if vx == vy + then InR (Hole' $ CMatch vx (HPeel' cx dels) (HPeel' cx inss)) + else InL (OMatch vx vy (HPeel' cx dels) (HPeel' cx inss)) + + fromInR :: Sum f g x -> Maybe (g x) + fromInR (InL _) = Nothing + fromInR (InR x) = Just x + + +-- |Diffs two generic merkelized structures. +-- The outline of the process is: +-- +-- i) Annotate each tree with the info we need (digest and height) +-- ii) Build the sharing trie +-- iii) Identify the proper shares +-- iv) Substitute the proper shares by a metavar in +-- both the source and deletion context +-- v) Extract the spine and compute the closure. +-- +diffOpts' :: forall ki codes phi at + . (EqHO ki , DigestibleHO ki , DigestibleHO phi) + => DiffOptions + -> Holes ki codes phi at + -> Holes ki codes phi at + -> (Int , Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at) +diffOpts' opts x y + = let dx = preprocess x + dy = preprocess y + (i, sh) = buildSharingTrie opts dx dy + dx' = tagProperShare sh dx + dy' = tagProperShare sh dy + delins = extractHoles (doMode opts) mkCanShare sh (dx' :*: dy') + in (i , delins) + where + mkCanShare :: forall a ix + . PrepFix a ki codes phi ix + -> Bool + mkCanShare (HOpq _ _) + = doOpaqueHandling opts == DO_AsIs + mkCanShare pr + = doMinHeight opts < treeHeight (getConst $ holesAnn pr) + +-- |When running the diff for two fixpoints, we can +-- cast the resulting deletion and insertion context into +-- an actual patch. +diffOpts :: (EqHO ki , DigestibleHO ki , IsNat ix) + => DiffOptions + -> Fix ki codes ix + -> Fix ki codes ix + -> Patch ki codes ix +diffOpts opts x y + = let (i , del :*: ins) = diffOpts' opts (na2holes $ NA_I x) + (na2holes $ NA_I y) + in close (extractSpine (doOpaqueHandling opts) cast i del ins) + where + cast :: Sum (Const Void) f i -> f i + cast (InR fi) = fi + cast (InL _) = error "impossible" + +diff :: (EqHO ki , DigestibleHO ki , IsNat ix) + => MinHeight + -> Fix ki codes ix + -> Fix ki codes ix + -> Patch ki codes ix +diff h = diffOpts (diffOptionsDefault { doMinHeight = h}) diff --git a/src/Data/HDiff/Diff/Modes.hs b/src/Data/HDiff/Diff/Modes.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Diff/Modes.hs @@ -0,0 +1,208 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +module Data.HDiff.Diff.Modes where + +import qualified Data.Set as S +import Data.Functor.Const +import Data.Functor.Sum + +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Digest + +import qualified Data.WordTrie as T +import Data.HDiff.Diff.Preprocess +import Data.HDiff.Diff.Types +import Data.HDiff.MetaVar + +-- |A predicate indicating whether a tree can be shared. +type CanShare ki codes phi = forall a ix . PrepFix a ki codes phi ix -> Bool + +extractHoles :: DiffMode + -> CanShare ki codes phi + -> IsSharedMap + -> Delta (PrepFix a ki codes phi) at + -> Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at +extractHoles DM_NoNested h tr sd + = extractNoNested h tr sd +extractHoles DM_ProperShare h tr (src :*: dst) + = (extractProperShare h tr src :*: extractProperShare h tr dst) +extractHoles DM_Patience h tr (src :*: dst) + = (extractPatience h tr src :*: extractPatience h tr dst) + +-- ** Proper Shares + +extractProperShare :: CanShare ki codes phi + -> IsSharedMap + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at +extractProperShare h tr a = properShare h tr (tagProperShare tr a) + +tagProperShare :: forall a ki codes phi at + . IsSharedMap + -> PrepFix a ki codes phi at + -> PrepFix (Int , Bool) ki codes phi at +tagProperShare ism = holesSynthesize pHole pOpq pPeel + where + myar :: PrepData a -> Int + myar = maybe 0 getArity . flip T.lookup ism . toW64s . treeDigest + + -- A leaf is always a proper share. Since it has no subtrees, + -- none if its subtrees can appear outside the leaf under scrutiny + -- by construction. + pHole :: Const (PrepData a) ix -> phi ix + -> Const (PrepData (Int , Bool)) ix + pHole (Const pd) _ = Const $ pd { treeParm = (myar pd , True) } + + pOpq :: Const (PrepData a) ('K k) -> ki k + -> Const (PrepData (Int , Bool)) ('K k) + pOpq (Const pd) _ = Const $ pd { treeParm = (myar pd , True) } + + pPeel :: Const (PrepData a) ('I i) + -> Constr sum n + -> NP (Const (PrepData (Int, Bool))) (Lkup n sum) + -> Const (PrepData (Int, Bool)) ('I i) + pPeel (Const pd) _ p + = let maxar = maximum (0 : elimNP (fst . treeParm . getConst) p) + myar' = myar pd + in Const $ pd { treeParm = (max maxar myar' , myar' >= maxar) } + +properShare :: forall ki codes phi at + . CanShare ki codes phi + -> IsSharedMap + -> PrepFix (Int , Bool) ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at +properShare h tr pr + = let prep = getConst $ holesAnn pr + isPS = snd $ treeParm prep + in if not (isPS && h pr) + then properShare' pr + else case T.lookup (toW64s $ treeDigest prep) tr of + Nothing -> properShare' pr + Just i -> mkHole (getMetavar i) pr + where + -- TODO: Abstract the properShare', noNested' and patience' + -- into a single function, remove 'CanShare' from these specific functions + -- and make the life of whoever is making an extraction strategy + -- simpler. + properShare' :: PrepFix (Int , Bool) ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at + properShare' (Hole _ d) = Hole' (InL d) + properShare' (HOpq _ k) = HOpq' k + properShare' (HPeel _ c d) = HPeel' c (mapNP (properShare h tr) d) + + mkHole :: Int + -> PrepFix (Int , Bool) ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at + mkHole _ (Hole _ d) = Hole' (InL d) + mkHole v (HPeel _ _ _) = Hole' (InR (NA_I (Const v))) + mkHole v (HOpq _ k) = Hole' (InR (NA_K (Annotate v k))) + +-- ** Patience + +extractPatience :: CanShare ki codes phi + -> IsSharedMap + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at +extractPatience h tr a = patience h tr a + +patience :: forall ki codes phi at a + . CanShare ki codes phi + -> IsSharedMap + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at +patience h tr pr + = if not (h pr) + then patience' pr + else case T.lookup (toW64s $ treeDigest $ getConst $ holesAnn pr) tr of + Nothing -> patience' pr + Just i | getArity i == 2 -> mkHole (getMetavar i) pr + | otherwise -> patience' pr + where + patience' :: PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at + patience' (Hole _ d) = Hole' (InL d) + patience' (HOpq _ k) = HOpq' k + patience' (HPeel _ c d) = HPeel' c (mapNP (patience h tr) d) + + mkMetaVar :: PrepFix a ki codes phi at + -> Int + -> MetaVarIK ki at + mkMetaVar (Hole _ _) _ = error "This should be impossible" + mkMetaVar (HPeel _ _ _) v = NA_I (Const v) + mkMetaVar (HOpq _ k) v = NA_K (Annotate v k) + + mkHole :: Int + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (MetaVarIK ki)) at + mkHole _ (Hole _ d) = Hole' (InL d) + mkHole v x = Hole' (InR $ mkMetaVar x v) + + + +-- ** No Nested + +extractNoNested :: CanShare ki codes phi + -> IsSharedMap + -> Delta (PrepFix a ki codes phi) at + -> Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at +extractNoNested h tr (src :*: dst) + = let del' = noNested h tr src + ins' = noNested h tr dst + holes = holesGetHolesAnnWith'' getHole del' + `S.intersection` + holesGetHolesAnnWith'' getHole ins' + del = holesRefineAnn (const (refineHole holes)) HOpq del' + ins = holesRefineAnn (const (refineHole holes)) HOpq ins' + in (del :*: ins) + where + getHole :: Sum phi (Const Int :*: f) at -> Maybe Int + getHole (InL _) = Nothing + getHole (InR (Const v :*: _)) = Just v + + mkMetaVar :: PrepFix a ki codes phi at + -> Int + -> MetaVarIK ki at + mkMetaVar (Hole _ _) _ = error "This should be impossible" + mkMetaVar (HPeel _ _ _) v = NA_I (Const v) + mkMetaVar (HOpq _ k) v = NA_K (Annotate v k) + + refineHole :: S.Set (Maybe Int) + -> Sum phi (Const Int :*: PrepFix a ki codes phi) ix + -> Holes ki codes (Sum phi (MetaVarIK ki)) ix + refineHole _ (InL phi) = Hole' (InL phi) + refineHole s (InR (Const i :*: f)) + | Just i `S.member` s = Hole' (InR $ mkMetaVar f i) + | otherwise = holesMapAnn InL (const $ Const ()) f + +noNested :: forall ki codes phi at a + . CanShare ki codes phi + -> IsSharedMap + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (Const Int :*: PrepFix a ki codes phi)) at +noNested h tr pr + = if not (h pr) + then noNested' pr + else case T.lookup (toW64s $ treeDigest $ getConst $ holesAnn pr) tr of + Nothing -> noNested' pr + Just i -> mkHole (getMetavar i) pr + where + noNested' :: PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (Const Int :*: PrepFix a ki codes phi)) at + noNested' (Hole _ d) = Hole' (InL d) + noNested' (HOpq _ k) = HOpq' k + noNested' (HPeel _ c d) = HPeel' c (mapNP (noNested h tr) d) + + mkHole :: Int + -> PrepFix a ki codes phi at + -> Holes ki codes (Sum phi (Const Int :*: PrepFix a ki codes phi)) at + mkHole _ (Hole _ d) = Hole' (InL d) + mkHole v x = Hole' (InR (Const v :*: x)) + diff --git a/src/Data/HDiff/Diff/Preprocess.hs b/src/Data/HDiff/Diff/Preprocess.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Diff/Preprocess.hs @@ -0,0 +1,67 @@ +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- |Here we perform a bunch of preprocessing steps +-- from a 'Generics.MRSOP.Base.Fix' into +-- a 'Generics.MRSOP.Base.AnnFix' with the correct +-- information for both driving the algorithm +-- and efficiently storing digests alongside +-- the structure. +module Data.HDiff.Diff.Preprocess where + +import Data.Proxy +import Data.Functor.Const + +import Generics.MRSOP.Base +import Generics.MRSOP.Holes + +import Generics.MRSOP.HDiff.Digest + +-- |We precompute the digest of a tree and its height +-- and annotate our fixpoints with this data before +-- going forward and computing a diff. +data PrepData a = PrepData + { treeDigest :: Digest + , treeHeight :: Int + , treeParm :: a + } deriving (Eq , Show) + +-- |A 'PrepFix' is a prepared fixpoint. In our case, it is +-- just a 'HolesAnn' with the prepared data inside of it. +type PrepFix a ki codes phi + = HolesAnn (Const (PrepData a)) ki codes phi + +-- |Here we receive an expression with holes an annotate +-- it with hashes and height information at every node. +preprocess :: forall ki codes phi at + . (DigestibleHO ki, DigestibleHO phi) + => Holes ki codes phi at + -> PrepFix () ki codes phi at +preprocess = holesSynthesize (const ppHole) (const ppOpq) ppPeel + where + pCodes :: Proxy codes + pCodes = Proxy + + safeMax [] = 0 + safeMax l = maximum l + + ppHole :: forall at' . phi at' -> Const (PrepData ()) at' + ppHole x = Const $ PrepData (digestHO x) 1 () + + ppOpq :: forall k . ki k -> Const (PrepData ()) ('K k) + ppOpq x = Const $ PrepData (digestHO x) 1 () + + ppPeel :: forall i x + . IsNat x + => Const () ('I x) + -> Constr (Lkup x codes) i + -> NP (Const (PrepData ())) (Lkup i (Lkup x codes)) + -> Const (PrepData ()) ('I x) + ppPeel _ c p + = let pix :: Proxy x + pix = Proxy + + dig = authPeel (treeDigest . getConst) pCodes pix c p + h = 1 + safeMax (elimNP (treeHeight . getConst) p) + in Const $ PrepData dig h () diff --git a/src/Data/HDiff/Diff/Types.hs b/src/Data/HDiff/Diff/Types.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Diff/Types.hs @@ -0,0 +1,68 @@ +module Data.HDiff.Diff.Types where + +import qualified Data.WordTrie as T + +-- |Controls the sharing of opaque values. +data DiffOpaques + -- |Never share opaque values + = DO_Never + -- |Only share opaque values that appear + -- on the spine. + | DO_OnSpine + -- |Handle values of type @K k@ normally, + -- as we handle recursive trees, of type @I i@. + | DO_AsIs + deriving (Eq , Show) + +-- |Diffing Algorithm modes. This is better illustrated with an +-- example. Supposte we have the following source and destination +-- trees: +-- +-- > src = Bin (Bin t k) u +-- > dst = Bin (Bin t k) t +-- +data DiffMode + -- |The /proper share/ algorithm will only share the trees that are + -- supposed to be a proper share. With the src and dst above, + -- it will produce: + -- + -- > diff src dst = Bin (Bin 0 1) u |-> Bin (Bin 0 1) 0 + -- + -- A good intuition is that this approach will prefer maximum sharing + -- as opposed to sharing bigger trees. + = DM_ProperShare + -- |The first algoritm we produced. Does not share nested trees. In fact, + -- with this mode we will get the following result: + -- + -- > diff src dst = Bin 0 u |-> Bin 0 t + | DM_NoNested + -- |Similar to @git --patience@, we share only unique trees. + -- In this example, this would result in the same as 'DM_NoNested', + -- but if we take @u = (Bin t k)@, no sharing would be performed + -- whatsoever. + | DM_Patience + deriving (Eq , Show , Enum) + +-- |Specifies the options for the diffing algorithm +data DiffOptions = DiffOptions + -- |Minimum height of trees considered for sharing + { doMinHeight :: Int + , doOpaqueHandling :: DiffOpaques + , doMode :: DiffMode + } deriving (Eq , Show) + +diffOptionsDefault :: DiffOptions +diffOptionsDefault = DiffOptions 1 DO_OnSpine DM_ProperShare + +-- |The data structure that captures which subtrees are shared +-- between source and destination. Besides providing an efficient +-- answer to the query: "is this tree shared?", it also gives a +-- unique identifier to that tree, allowing us to easily +-- build our n-holed treefix. +type IsSharedMap = T.Trie MetavarAndArity + +data MetavarAndArity = MAA { getMetavar :: Int , getArity :: Int } + deriving (Eq , Show) + +-- |A tree smaller than the minimum height will never be shared. +type MinHeight = Int diff --git a/src/Data/HDiff/Example.hs b/src/Data/HDiff/Example.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Example.hs @@ -0,0 +1,148 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Data.HDiff.Example where + +import qualified Data.Set as S +import Data.Functor.Const + +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import Generics.MRSOP.Opaque +import Generics.MRSOP.TH + +import Generics.MRSOP.HDiff.Digest +import Data.HDiff.Patch +import Data.HDiff.Diff +import Data.HDiff.MetaVar +import Data.HDiff.Change + +instance DigestibleHO Singl where + digestHO (SString s) = hashStr s + digestHO (SInt s) = hashStr (show s) + digestHO _ = error "No one told me!" + +-- |2-3-Trees declaration +data Tree23 + = Node2 Int Tree23 Tree23 + | Node3 Int Tree23 Tree23 Tree23 + | Leaf + deriving (Eq , Show) + +deriveFamily [t| Tree23 |] +{- +instance Renderer Singl FamTree23 CodesTree23 where + renderK _ (SString s) = pretty s + renderK _ (SInt i) = pretty i + + renderI _ IdxTree23 Leaf_ = pretty "leaf" + renderI _ IdxTree23 (Node2_ i dl dr) + = tupled [pretty "Node2" <+> getConst dr <+> getConst dr] + renderI _ IdxTree23 (Node3_ i dl dm dr) + = tupled [pretty "Node3" <+> getConst dl <+> getConst dm <+> getConst dr] +-} + +mt1 , mt2 , mt3 , mt4 :: Tree23 +mt1 = Node2 10 Leaf Leaf +mt2 = Node3 20 Leaf mt1 Leaf +mt3 = Node2 30 Leaf Leaf +mt4 = Node3 50 mt1 mt2 mt3 + +big1 , big2 , big3 :: Tree23 +big1 = Node3 100 + (Node2 200 mt4 mt3) + (Node2 100 Leaf mt1) + (Node3 300 Leaf mt4 Leaf) +big3 = Node3 100 + (Node2 200 mt4 mt3) + (Node2 100 Leaf mt1) + (Node3 300 Leaf Leaf Leaf) + +big2 = Node2 100 + (Node2 800 mt4 mt3) + (Node2 200 mt4 (Node3 300 mt1 mt3 Leaf)) + +tr :: Tree23 -> Fix Singl CodesTree23 'Z +tr = dfrom . into + +dgms :: Tree23 -> Tree23 -> Patch Singl CodesTree23 'Z +dgms x y = diff 1 (dfrom $ into x) (dfrom $ into y) + +o , p , q :: Tree23 +o = Node2 10 (Node3 100 Leaf Leaf Leaf) (Node2 1000 Leaf Leaf) +p = Node2 20 (Node3 100 (Node2 50 Leaf Leaf) Leaf Leaf) (Node2 1000 Leaf Leaf) +q = Node2 10 (Node3 100 Leaf Leaf Leaf) (Node3 200 Leaf Leaf (Node2 1000 Leaf Leaf)) +{- +import Generics.MRSOP.Examples.SimpTH + + + + +type MyFix = Fix Singl CodesStmtString + +tr :: Decl String -> MyFix (S (S Z)) +tr = dfrom . into @FamStmtString + +genFib :: MyFix (S (S Z)) +genFib = tr $ test1 "fib" "n" "aux" + +genFib2 :: MyFix (S (S Z)) +genFib2 = tr $ test1 "fab" "m" "b" +-} + +type TreeTerm = Holes Singl CodesTree23 (MetaVarIK Singl) ('I 'Z) + +unif1 :: TreeTerm +unif1 = HPeel' CZ (HOpq' (SInt 100) + :* Hole' (NA_I $ Const 1) + :* Hole' (NA_I $ Const 2) + :* NP0) +unif12 :: TreeTerm +unif12 = HPeel' CZ (HOpq' (SInt 500) + :* Hole' (NA_I $ Const 1) + :* Hole' (NA_I $ Const 2) + :* NP0) + +unif2 :: TreeTerm +unif2 = HPeel' CZ (HOpq' (SInt 200) + :* Hole' (NA_I $ Const 4) + :* Hole' (NA_I $ Const 5) + :* NP0) +unif22 :: TreeTerm +unif22 = HPeel' CZ (HOpq' (SInt 500) + :* Hole' (NA_I $ Const 4) + :* Hole' (NA_I $ Const 5) + :* NP0) + + + +change1 = CMatch S.empty unif1 unif12 +change2 = CMatch S.empty unif2 unif22 + +{- +unif2 :: TreeTerm +unif2 = HPeel' CZ (HOpq' (SInt 100) + :* HPeel' (CS CZ) + (Hole' (NA_K $ Annotate 6 (SInt 42)) + :* Hole' (NA_I $ Const 2) + :* HPeel' (CS (CS CZ)) NP0 + :* HPeel' (CS (CS CZ)) NP0 + :* NP0) + :* HPeel' (CS (CS CZ)) NP0 + :* NP0) +-} diff --git a/src/Data/HDiff/MetaVar.hs b/src/Data/HDiff/MetaVar.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/MetaVar.hs @@ -0,0 +1,109 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE MultiParamTypeClasses #-} +-- |Exports a bunch of functionality for handling metavariables +-- both over recursive positions only, with 'MetaVarI' and over +-- recursive positions and constants, 'MetaVarIK'. +module Data.HDiff.MetaVar where + +import Data.Function (on) +import Data.Functor.Const +import Data.Type.Equality +-------------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Base +-------------------------------------- +import Data.Exists +import Generics.MRSOP.HDiff.Digest +import Generics.MRSOP.HDiff.Holes + +-- |Given a functor from @Nat@ to @*@, lift it to work over @Atom@ +-- by forcing the atom to be an 'I'. +data ForceI :: (Nat -> *) -> Atom kon -> * where + ForceI :: (IsNat i) => { unForceI :: f i } -> ForceI f ('I i) + +-- |A 'MetaVarI' can only take place of a recursive position. +type MetaVarI = ForceI (Const Int) + +-- |This is isomorphic to @const x &&& f@ on the type level. +data Annotate (x :: *) (f :: k -> *) :: k -> * where + Annotate :: x -> f i -> Annotate x f i + +instance (ShowHO f , Show x) => ShowHO (Annotate x f) where + showHO (Annotate i f) + = showHO f ++ "[" ++ show i ++ "]" + +instance (EqHO f , Eq x) => EqHO (Annotate x f) where + eqHO (Annotate x1 f1) (Annotate x2 f2) = x1 == x2 && eqHO f1 f2 + +instance (TestEquality ki) => TestEquality (Annotate x ki) where + testEquality (Annotate _ x) (Annotate _ y) + = testEquality x y + +-- |A 'MetaVarIK' can be over a opaque type and a recursive position +-- +-- We keep the actual value of the constant around purely because +-- sometimes we need to compare the indexes for equality. It is possible +-- to remove that but this will require some instance like 'IsNat' +-- to be bubbled up all the way to generics-mrsop. +-- +-- TODO: add a 'IsOpq' instance and remove Annotate altogether. +-- we need a method with type @defOpq :: Proxy k -> ki k@, +-- we can then piggyback on 'testEquality' for ki. +-- The 'HasIKProjInj' instance is part of this same hack. +type MetaVarIK ki = NA (Annotate Int ki) (Const Int) + +instance (DigestibleHO ki) => DigestibleHO (MetaVarIK ki) where + digestHO (NA_I (Const i)) = hashStr ("vari" ++ show i) + digestHO (NA_K (Annotate i _)) = hashStr ("vark" ++ show i) + +-- |Returns the metavariable forgetting about type information +metavarGet :: MetaVarIK ki at -> Int +metavarGet = elimNA go getConst + where go (Annotate x _) = x + +-- |Adds a number to a metavar +metavarAdd :: Int -> MetaVarIK ki at -> MetaVarIK ki at +metavarAdd n (NA_K (Annotate i x)) = NA_K $ Annotate (n + i) x +metavarAdd n (NA_I (Const i)) = NA_I $ Const (n + i) + +-- TODO: Goes away with Annotate +instance HasIKProjInj ki (MetaVarIK ki) where + konInj k = NA_K (Annotate 0 k) + varProj _ (NA_I _) = Just IsI + varProj _ _ = Nothing + +-- * Existential MetaVars + +-- |Retrieves the int inside a existential 'MetaVarIK' +metavarIK2Int :: Exists (MetaVarIK ki) -> Int +metavarIK2Int (Exists (NA_I (Const i))) = i +metavarIK2Int (Exists (NA_K (Annotate i _))) = i + +-- |Retrieves the int inside a existential 'MetaVarI' +metavarI2Int :: Exists MetaVarI -> Int +metavarI2Int (Exists (ForceI (Const i))) = i + +-- |Injects a metavar over recursive positions +-- into one over opaque types and recursive positions +metavarI2IK :: MetaVarI ix -> MetaVarIK ki ix +metavarI2IK (ForceI x) = NA_I x + +-- ** Instances over 'Exists' + +instance Eq (Exists MetaVarI) where + (==) = (==) `on` metavarI2Int + +instance Ord (Exists MetaVarI) where + compare = compare `on` metavarI2Int + +instance Eq (Exists (MetaVarIK ki)) where + (==) = (==) `on` metavarIK2Int + +instance Ord (Exists (MetaVarIK ki)) where + compare = compare `on` metavarIK2Int + diff --git a/src/Data/HDiff/Patch.hs b/src/Data/HDiff/Patch.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Patch.hs @@ -0,0 +1,202 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +module Data.HDiff.Patch where + +import Control.Monad.State +import Control.Monad.Except +import Data.Type.Equality +import qualified Data.Set as S +import qualified Data.Map as M +import Data.Functor.Const +------------------------------------ +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +------------------------------------ +import Generics.MRSOP.HDiff.Holes +import Data.Exists +import Data.HDiff.MetaVar +import Data.HDiff.Change +import Data.HDiff.Change.Apply + + +-- * Patches +-- +-- $patchintro +-- +-- A patch consists in two treefixes, for deletion +-- and insertion respectively and a set of swaps +-- and contractions of their holes. In Haskell, this +-- is too intricate to write on the type level, so +-- we place unique identifiers in the holes +-- and work with the invariant: +-- +-- > nub (forget ctxDel :: [Int]) == nub (forget ctxIns) +-- +-- Where @forget@ returns the values in the holes. +-- + +-- |Instead of keeping unecessary information, a 'RawPatch' will +-- factor out the common prefix before the actual changes. +-- +type RawPatch ki codes = Holes ki codes (CChange ki codes) + +-- |A 'Patch' is a 'RawPatch' instantiated to 'I' atoms. +type Patch ki codes ix = Holes ki codes (CChange ki codes) ('I ix) + + +-- ** Patch Alpha Equivalence + +patchEq :: (EqHO ki) => RawPatch ki codes at -> RawPatch ki codes at -> Bool +patchEq p q = and $ holesGetHolesAnnWith' (uncurry' go) $ holesLCP p q + where + go :: (EqHO ki) => RawPatch ki codes at -> RawPatch ki codes at -> Bool + go c d = changeEq (distrCChange c) (distrCChange d) + +patchIsCpy :: (EqHO ki) => RawPatch ki codes at -> Bool +patchIsCpy = and . holesGetHolesAnnWith' isCpy + +-- ** Functionality over a 'Patch' + +patchMaxVar :: RawPatch ki codes at -> Int +patchMaxVar = flip execState 0 . holesMapM localMax + where + localMax r@(CMatch vars _ _) + = let m = (1+) . maybe 0 id . S.lookupMax $ S.map (exElim metavarGet) vars + in modify (max m) >> return r + +-- |Calling @p `withFreshNamesFrom` q@ will return an alpha equivalent +-- version of @p@ that has no name clasehs with @q@. +withFreshNamesFrom :: RawPatch ki codes at + -> RawPatch ki codes at + -> RawPatch ki codes at +withFreshNamesFrom p q = holesMap (changeAdd (patchMaxVar q + 1)) p + where + changeAdd :: Int -> CChange ki codes at -> CChange ki codes at + changeAdd n (CMatch vs del ins) + = CMatch (S.map (exMap (metavarAdd n)) vs) + (holesMap (metavarAdd n) del) + (holesMap (metavarAdd n) ins) + + +-- |Computes the /cost/ of a 'Patch'. This is in the sense +-- of edit-scripts where it counts how many constructors +-- are being inserted and deleted. +patchCost :: RawPatch ki codes at -> Int +patchCost = sum . holesGetHolesAnnWith' go + where + go :: CChange ki codes at -> Int + go (CMatch _ d i) = holesSize d + holesSize i + + +-- ** Applying a Patch +-- +-- $applyingapatch +-- +-- Patch application really is trivial. Say we +-- are applying a patch @p@ against an element @x@, +-- first we match @x@ with the @ctxDel p@; upon +-- a succesfull match we record, in a 'Valuation', +-- which tree fell in which hole. +-- Then, we use the same valuation to inject +-- those trees into @ctxIns p@. +-- +-- The only slight trick is that we need to +-- wrap our trees in existentials inside our valuation. + +-- |Applying a patch is trivial, we simply project the +-- deletion treefix and inject the valuation into the insertion. +apply :: (TestEquality ki , EqHO ki , ShowHO ki, IsNat ix) + => Patch ki codes ix + -> Fix ki codes ix + -> Either String (Fix ki codes ix) +apply patch x0 + = holesZipRep patch (NA_I x0) + >>= holesMapM (uncurry' termApply) + >>= holes2naM Right + >>= return . unNA_I + where + unNA_I :: NA f g ('I i) -> g i + unNA_I (NA_I x) = x + +-- ** Specializing a Patch + +-- |The predicate @composes qr pq@ checks whether @qr@ is immediatly applicable +-- to the codomain of @pq@. +composes :: (ShowHO ki , EqHO ki , TestEquality ki) + => RawPatch ki codes at + -> RawPatch ki codes at + -> Bool +composes qr0 pq0 = and $ holesGetHolesAnnWith' getConst + $ holesMap (uncurry' go) $ holesLCP qr0 pq0 + where + go :: (ShowHO ki , EqHO ki , TestEquality ki) + => RawPatch ki codes at + -> RawPatch ki codes at + -> Const Bool at + go qr pq = + let cqr = distrCChange qr + cpq = distrCChange pq + in Const $ applicableTo (cCtxDel cqr) (cCtxIns cpq) + +applicableTo :: (ShowHO ki , EqHO ki , TestEquality ki) + => Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes (MetaVarIK ki) ix + -> Bool +applicableTo pat = either (const False) (const True) + . runExcept + . go M.empty M.empty pat + where + go :: (ShowHO ki , EqHO ki , TestEquality ki) + => Subst ki codes (MetaVarIK ki) + -> Subst ki codes (MetaVarIK ki) + -> Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes (MetaVarIK ki) ix + -> Except (ApplicationErr ki codes (MetaVarIK ki)) + (Subst ki codes (MetaVarIK ki) , Subst ki codes (MetaVarIK ki)) + go l r (Hole _ var) ex = (,r) <$> substInsert' "l" l var ex + go l r pa (Hole _ var) = (l,) <$> substInsert' "r" r var pa + go l r (HOpq _ oa) (HOpq _ ox) + | eqHO oa ox = return (l , r) + | otherwise = throwError (IncompatibleOpqs oa ox) + go l r pa@(HPeel _ ca ppa) x@(HPeel _ cx px) = + case testEquality ca cx of + Nothing -> throwError (IncompatibleTerms pa x) + Just Refl -> getConst <$> + cataNPM (\(pa' :*: px') (Const (vl , vr)) + -> fmap Const $ go vl vr pa' px') + (return $ Const $ (l ,r)) + (zipNP ppa px) + +substInsert' :: (ShowHO ki , EqHO ki , TestEquality ki) + => String + -> Subst ki codes (MetaVarIK ki) + -> MetaVarIK ki ix + -> Holes ki codes (MetaVarIK ki) ix + -> Except (ApplicationErr ki codes (MetaVarIK ki)) (Subst ki codes (MetaVarIK ki)) +substInsert' _ s var new = case M.lookup (metavarGet var) s of + Nothing -> return $ M.insert (metavarGet var) + (Exists $ new) s + Just (Exists old) -> case testEquality old new of + Nothing -> throwError IncompatibleTypes + Just Refl -> case old `specializesTo` new of + Just res -> return $ M.insert (metavarGet var) (Exists $ res) s + Nothing -> throwError (FailedContraction (metavarGet var) old new) + where + specializesTo :: (EqHO ki) + => Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes (MetaVarIK ki) ix + -> Maybe (Holes ki codes (MetaVarIK ki) ix) + specializesTo m n = fmap holesJoin + $ holesMapM (uncurry' go) + $ holesLCP m n + + go :: Holes ki codes (MetaVarIK ki) ix + -> Holes ki codes (MetaVarIK ki) ix + -> Maybe (Holes ki codes (MetaVarIK ki) ix) + go (Hole _ _) r = Just r + go l (Hole _ _) = Just l + go _ _ = Nothing diff --git a/src/Data/HDiff/Patch/Merge.hs b/src/Data/HDiff/Patch/Merge.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Patch/Merge.hs @@ -0,0 +1,222 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Data.HDiff.Patch.Merge where + +import Data.Functor.Sum +import qualified Data.Map as M + +import Control.Monad.State +import Control.Monad.Writer hiding (Sum) +import Control.Monad.Except + +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes + +import Data.Exists +import Data.HDiff.Patch +import Data.HDiff.Change +import Data.HDiff.Change.Apply +import Data.HDiff.Change.Thinning +import Data.HDiff.MetaVar + +-- * Merging Treefixes +-- +-- $mergingtreefixes +-- +-- After merging two patches, we might end up with a conflict. +-- That is, two changes that can't be reconciled. + +-- |Hence, a conflict is simply two changes together. +data Conflict :: (kon -> *) -> [[[Atom kon]]] -> Atom kon -> * where + Conflict :: String + -> RawPatch ki codes at + -> RawPatch ki codes at + -> Conflict ki codes at + +-- |A 'PatchC' is a patch with potential conflicts inside +type PatchC ki codes ix + = Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) ('I ix) + +-- |Tries to cast a 'PatchC' back to a 'Patch'. Naturally, +-- this is only possible if the patch has no conflicts. +noConflicts :: PatchC ki codes ix -> Maybe (Patch ki codes ix) +noConflicts = holesMapM rmvInL + where + rmvInL (InL _) = Nothing + rmvInL (InR x) = Just x + +-- |Returns the labels of the conflicts ina a patch. +getConflicts :: (ShowHO ki) => PatchC ki codes ix -> [String] +getConflicts = snd . runWriter . holesMapM go + where + go x@(InL (Conflict str _ _)) = tell [str] >> return x + go x = return x + + +-- |A merge of @p@ over @q@, denoted @p // q@, is the adaptation +-- of @p@ so that it could be applied to an element in the +-- image of @q@. +(//) :: ( Applicable ki codes (Holes2 ki codes) + , HasDatatypeInfo ki fam codes + ) + => Patch ki codes ix + -> Patch ki codes ix + -> PatchC ki codes ix +p // q = holesJoin $ holesMap (uncurry' reconcile) + $ holesLCP p + $ q `withFreshNamesFrom` p + + +-- |The 'reconcile' function will try to reconcile disagreeing +-- patches. +-- +-- Precondition: before calling @reconcile p q@, make sure +-- @p@ and @q@ are different. +reconcile :: forall ki codes fam at + . ( Applicable ki codes (Holes2 ki codes) + , HasDatatypeInfo ki fam codes + ) + => RawPatch ki codes at + -> RawPatch ki codes at + -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at +reconcile p q + -- If both patches are alpha-equivalent, we return a copy. + | patchEq p q = Hole' $ InR $ makeCopyFrom (distrCChange p) + -- Otherwise, this is slightly more involved, but it is intuitively simple. + | otherwise = + -- First we translate both patches to a 'spined change' representation. + let sp = holesJoin $ holesMap (uncurry' holesLCP . unCMatch) p + sq = holesJoin $ holesMap (uncurry' holesLCP . unCMatch) q -- spinedChange q + in case process sp sq of + CantReconcile err -> Hole' $ InL $ Conflict err p q + ReturnNominator -> holesMap InR p + InstDenominator v -> Hole' $ + case runExcept $ transport (scIns sq) v of + Left err -> InL $ Conflict (show err) p q + Right r -> case utx22change r of + Nothing -> InL $ Conflict "chg" p q + Just res -> InR res + +data ProcessOutcome ki codes + = ReturnNominator + | InstDenominator (Subst ki codes (Holes2 ki codes)) + | CantReconcile String + +-- |Checks whether a variable is a rawCpy, note that we need +-- a map that checks occurences of this variable. +rawCpy :: M.Map Int Int + -> Holes2 ki codes at + -> Bool +rawCpy ar (Hole' v1 :*: Hole' v2) = metavarGet v1 == metavarGet v2 + && M.lookup (metavarGet v1) ar == Just 1 +rawCpy _ _ = False + +simpleCopy :: Holes2 ki codes at -> Bool +simpleCopy (Hole' v1 :*: Hole' v2) = metavarGet v1 == metavarGet v2 +simpleCopy _ = False + +isLocalIns :: Holes2 ki codes at -> Bool +isLocalIns (Hole _ _ :*: HPeel _ _ _) = True +isLocalIns _ = False + +arityMap :: Holes ki codes (MetaVarIK ki) at -> M.Map Int Int +arityMap = go . holesGetHolesAnnWith' metavarGet + where + go [] = M.empty + go (v:vs) = M.alter (Just . maybe 1 (+1)) v (go vs) + + +instance ShowHO x => Show (Exists x) where + show (Exists x) = showHO x + +-- |This will process two changes, represented as a spine and +-- inner changes, into a potential merged patch. The result of @process sp sq@ +-- is supposed to instruct how to construct a patch that +-- can be applied to the image @sq@. +-- +-- We do so by traversing the places where both @sp@ and @sq@ differ. +-- While we perform this traversal we instantiate a valuation of +-- potential substitutions, which might be needed in case we +-- need to adapt @sp@ to @sq@. After we are done, we know whether +-- we need to adapt @sp@, return @sp@ as is, or there is a conflict. +-- +process :: (Applicable ki codes (Holes2 ki codes)) + => HolesHoles2 ki codes at -> HolesHoles2 ki codes at + -> ProcessOutcome ki codes +process sp sq = + case and <$> mapM (exElim $ uncurry' step1) phiD of + Nothing -> CantReconcile "p1n" + Just True -> if any (exElim $ uncurry' insins) phiID + then CantReconcile "p1ii" + else ReturnNominator + Just False -> + let partial = runState (runExceptT $ mapM_ (exElim $ uncurry' step2) phiID) M.empty + in case partial of + (Left err , _) -> CantReconcile $ "p2n: " ++ err + (Right () , s) -> InstDenominator s + where + (delsp :*: _) = utx2distr sp + phiD = holesGetHolesAnnWith' Exists $ holesLCP delsp sq + phiID = holesGetHolesAnnWith' Exists $ holesLCP sp sq + + -- The thing is, 'chg' is a true copy only if v2 occurs only once + -- within the whole of 'sq' + -- counts how many times a variable appears in 'sq' + varmap = arityMap (snd' (utx2distr sq)) + {- + m var = maybe 0 id $ M.lookup var varmap + + maxVar = case M.toDescList varmap of + [] -> 0 + ((v,_):_) -> v + -} + + -- |Step1 checks that the own-variable mappings of the + -- anti-unification of (scDel p) and q is of a specific shape. + step1 :: Holes ki codes (MetaVarIK ki) at -> HolesHoles2 ki codes at + -> Maybe Bool + -- If the deletion context of the numerator requires an opaque + -- fixed value and the denominator performs any change other + -- than a copy, this is a del/mod conflict. + step1 (HOpq _ _) (Hole _ chg) + | simpleCopy chg = Just True + | otherwise = Nothing + -- If the numerator imposes no restriction in what it accepts here, + -- we return true for this hole + step1 (Hole _ _) _ = Just True + -- If the numerator expects something specific but the denominator + -- merely copies, we still return true + step1 _ (Hole _ chg) = Just $ rawCpy varmap chg + -- Any other situation requires further analisys. + step1 _ _ = Just False + + -- |Step2 checks a condition for the own-variable mappints + -- of the anti-unification of p and q! note this is different + -- altogether from step 1!!! + step2 :: (Applicable ki codes (Holes2 ki codes)) + => HolesHoles2 ki codes at -> HolesHoles2 ki codes at + -> ExceptT String (State (Subst ki codes (Holes2 ki codes))) () + step2 pp qq = do + s <- lift get + let del = scDel qq + case thinUTx2 (utx2distr pp) del of + Left e -> throwError ("th: " ++ show e) + Right pp0 -> do + let pp' = uncurry' holesLCP pp0 + case runExcept (pmatch' s del pp') of + Left e -> throwError (show e) + Right s' -> put s' >> return () + + insins :: HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> Bool + insins (Hole _ pp) (Hole _ qq) = isLocalIns pp && isLocalIns qq + insins _ _ = False diff --git a/src/Data/HDiff/Patch/Show.hs b/src/Data/HDiff/Patch/Show.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Patch/Show.hs @@ -0,0 +1,190 @@ +{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Data.HDiff.Patch.Show where + +import System.IO +import Data.Proxy +import Data.Functor.Const +import Data.Functor.Sum +import Data.Text.Prettyprint.Doc +import Data.Text.Prettyprint.Doc.Render.Terminal +import qualified Data.Text.Prettyprint.Doc.Render.Text as Text +import qualified Data.Text as T + +import Generics.MRSOP.Base hiding (Infix) +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Holes +import Generics.MRSOP.HDiff.Renderer + +import qualified Data.HDiff.Change as D +import qualified Data.HDiff.Patch.Merge as D +import qualified Data.HDiff.MetaVar as D + +-- |Given a label and a doc, @spliced l d = "[" ++ l ++ "|" ++ d ++ "|]"@ +spliced :: Doc ann -> Doc ann -> Doc ann +spliced lbl d = brackets (lbl <> surround d (pretty "| ") (pretty " |")) + +metavarPretty :: (Doc AnsiStyle -> Doc AnsiStyle) -> D.MetaVarIK ki ix -> Doc AnsiStyle +metavarPretty sty (NA_I (Const i)) + = sty $ spliced (pretty "I") (pretty i) +metavarPretty sty (NA_K (D.Annotate i _)) + = sty $ spliced (pretty "K") (pretty i) + +-- when using emacs, the output of the repl is in red; +-- hence, life is easier when we show a different color isntead. +-- btw, emacs only interprets dull colors. +myred , mygreen , mydullred , mydullgreen :: AnsiStyle +myred = colorDull Yellow +mygreen = colorDull Green +mydullred = colorDull Yellow +mydullgreen = colorDull Green + +{- +-- |Shows a conflict in a pretty fashion +conflictPretty :: (HasDatatypeInfo ki fam codes) + => (forall k . ki k -> Doc AnsiStyle) + -> Sum D.MetaVar (D.Conflict ki codes) at -> Doc AnsiStyle +conflictPretty renderK (InL v) + = metavarPretty v +conflictPretty renderK (InR (D.Conflict l r)) + = let dl = utxPretty (Proxy :: Proxy fam) metavarPretty renderK l + dr = utxPretty (Proxy :: Proxy fam) metavarPretty renderK r + in annotate (color Red) + $ spliced (annotate bold $ pretty "C") + (hsep [dl , pretty "<|>" , dr ]) +-} + +-- |Pretty prints a patch on the terminal +showRawPatch :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Holes ki codes (D.CChange ki codes) v + -> [String] +showRawPatch patch + = doubleColumn 75 + (holesPretty (Proxy :: Proxy fam) id prettyCChangeDel patch) + (holesPretty (Proxy :: Proxy fam) id prettyCChangeIns patch) + where + prettyCChangeDel :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => D.CChange ki codes at + -> Doc AnsiStyle + prettyCChangeDel (D.CMatch _ del _) + = holesPretty (Proxy :: Proxy fam) + (annotate myred) + (metavarPretty (annotate mydullred)) + del + + prettyCChangeIns :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => D.CChange ki codes at + -> Doc AnsiStyle + prettyCChangeIns (D.CMatch _ _ ins) + = holesPretty (Proxy :: Proxy fam) + (annotate mygreen) + (metavarPretty (annotate mydullgreen)) + ins + +showPatchC :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Holes ki codes (Sum (D.Conflict ki codes) (D.CChange ki codes)) at + -> [String] +showPatchC patch + = doubleColumn 75 + (holesPretty (Proxy :: Proxy fam) id prettyConfDel patch) + (holesPretty (Proxy :: Proxy fam) id prettyConfIns patch) + where + prettyConfDel :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Sum (D.Conflict ki codes) (D.CChange ki codes) at + -> Doc AnsiStyle + prettyConfDel (InL (D.Conflict lbl _ _)) + = annotate (color Blue) (pretty $ show lbl) + prettyConfDel (InR (D.CMatch _ del _)) + = holesPretty (Proxy :: Proxy fam) + (annotate myred) + (metavarPretty (annotate mydullred)) + del + + prettyConfIns :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Sum (D.Conflict ki codes) (D.CChange ki codes) at + -> Doc AnsiStyle + prettyConfIns (InL (D.Conflict lbl _ _)) + = annotate (color Blue) (pretty $ show lbl) + prettyConfIns (InR (D.CMatch _ _ ins)) + = holesPretty (Proxy :: Proxy fam) + (annotate mygreen) + (metavarPretty (annotate mydullgreen)) + ins + +instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , RendererHO ki) + => Show (Holes ki codes (D.CChange ki codes) at) where + show = unlines . showRawPatch + +instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , RendererHO ki , ShowHO phi) + => Show (Delta (Holes ki codes phi) at) where + show (del :*: ins) + = unlines $ doubleColumn 75 + (holesPretty (Proxy :: Proxy fam) id (pretty . showHO) del) + (holesPretty (Proxy :: Proxy fam) id (pretty . showHO) ins) + show _ = undefined -- ghc seems to really want this to see the patterns are complete. + + +instance (HasDatatypeInfo ki fam codes , RendererHO ki) + => Show (D.CChange ki codes at) where + show (D.CMatch _ del ins) = unlines $ doubleColumn 75 + (holesPretty (Proxy :: Proxy fam) id (metavarPretty (annotate mydullred)) del) + (holesPretty (Proxy :: Proxy fam) id (metavarPretty (annotate mydullgreen)) ins) + + +instance {-# OVERLAPPING #-} (HasDatatypeInfo ki fam codes , RendererHO ki) + => Show (Holes ki codes (Sum (D.Conflict ki codes) (D.CChange ki codes)) at) where + show = unlines . showPatchC + +-- |Outputs the result of 'showPatchC' to the specified handle +displayPatchC :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Handle + -> Holes ki codes (Sum (D.Conflict ki codes) (D.CChange ki codes)) at + -> IO () +displayPatchC hdl = mapM_ (hPutStrLn hdl) . showPatchC + +-- |Outputs the result of 'showRawPatch' to the specified handle +displayRawPatch :: (HasDatatypeInfo ki fam codes , RendererHO ki) + => Handle + -> Holes ki codes (D.CChange ki codes) at + -> IO () +displayRawPatch hdl = mapM_ (hPutStrLn hdl) . showRawPatch + +-- |Displays two docs in a double column fashion +-- +-- This is a hacky function. We need to render both the colored +-- and the non-colored versions to calculate +-- the width spacing correctly (see @complete@ in the where clause) +-- +doubleColumn :: Int -> Doc AnsiStyle -> Doc AnsiStyle -> [String] +doubleColumn maxWidth da db + = let pgdim = LayoutOptions (AvailablePerLine maxWidth 1) + lyout = layoutSmart pgdim + -- colored versions + ta = T.lines . renderStrict $ lyout da + tb = T.lines . renderStrict $ lyout db + -- non colored versions + sta = T.lines . Text.renderStrict $ lyout da + w = 1 + maximum (0 : map T.length sta) + stb = T.lines . Text.renderStrict $ lyout db + compA = if length ta >= length tb + then 0 + else length tb - length ta + compB = if length tb >= length ta + then 0 + else length ta - length tb + fta = (zip ta sta) ++ replicate compA ((id &&& id) $ T.replicate w $ T.singleton ' ') + ftb = (zip tb stb) ++ replicate compB ((id &&& id) $ T.empty) + in map (\(la , lb) -> T.unpack . T.concat + $ [ complete w la + , T.pack " -|+ " + , fst lb + ]) + (zip fta ftb) + where + complete n (clr , nocolor) + = T.concat [clr , T.replicate (n - T.length nocolor) $ T.singleton ' '] diff --git a/src/Data/HDiff/Patch/Thinning.hs b/src/Data/HDiff/Patch/Thinning.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Patch/Thinning.hs @@ -0,0 +1,37 @@ +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Data.HDiff.Patch.Thinning where + +import Data.Type.Equality +--------------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Holes +--------------------------------------- +import Data.HDiff.Patch +import Data.HDiff.Change +import qualified Data.HDiff.Change.Thinning as CT + +thin :: (ShowHO ki , TestEquality ki, EqHO ki) + => RawPatch ki codes at + -> RawPatch ki codes at + -> Either (CT.ThinningErr ki codes) (RawPatch ki codes at) +thin p q = holesMapM (uncurry' go) $ holesLCP p (q `withFreshNamesFrom` p) + where + go cp cq = let cp' = distrCChange cp + cq' = distrCChange cq + in CT.thin cp' (domain cq') + +unsafeThin :: (ShowHO ki , TestEquality ki, EqHO ki) + => RawPatch ki codes at + -> RawPatch ki codes at + -> RawPatch ki codes at +unsafeThin p q = either (error . show) id $ thin p q diff --git a/src/Data/HDiff/Patch/TreeEditDistance.hs b/src/Data/HDiff/Patch/TreeEditDistance.hs new file mode 100644 --- /dev/null +++ b/src/Data/HDiff/Patch/TreeEditDistance.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE ViewPatterns #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Data.HDiff.Patch.TreeEditDistance where + +import Data.Type.Equality + +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import qualified Generics.MRSOP.GDiff as GD + +import Data.HDiff.Patch +import qualified Data.HDiff.Change.TreeEditDistance as TED + +toES :: (EqHO ki , ShowHO ki , TestEquality ki) + => RawPatch ki codes at -> NA ki (Fix ki codes) at + -> Either String (GD.ES ki codes '[ at ] '[ at ]) +toES (Hole _ chg) x = TED.toES chg x +toES (HOpq _ _) (NA_K ox) = Right $ TED.gcpy (GD.ConstrK ox) GD.ES0 +toES (HPeel _ ca ppa) (NA_I (Fix (sop -> Tag cx px))) = + case testEquality ca cx of + Nothing -> Left "unapplicable" + Just Refl -> (TED.gcpy (GD.ConstrI ca (listPrfNP ppa)) + . TED.esDelCong (listId (listPrfNP ppa)) + . TED.esInsCong (listId (listPrfNP ppa))) + <$> toES' ppa px + +listId :: ListPrf a -> ListPrf a :~: ListPrf (a :++: '[]) +listId Nil = Refl +listId (Cons a) = case listId a of + Refl -> Refl + +toES' :: (EqHO ki , ShowHO ki , TestEquality ki) + => NP (RawPatch ki codes) sum -> PoA ki (Fix ki codes) sum + -> Either String (GD.ES ki codes sum sum) +toES' NP0 NP0 = return GD.ES0 +toES' (p :* ps) (x :* xs) = TED.appendES <$> toES p x <*> toES' ps xs + diff --git a/src/Data/WordTrie.hs b/src/Data/WordTrie.hs new file mode 100644 --- /dev/null +++ b/src/Data/WordTrie.hs @@ -0,0 +1,65 @@ +{-# LANGUAGE TupleSections #-} +module Data.WordTrie where + +import Prelude hiding (lookup,zipWith) +import Control.Arrow ((***), first, second) + +import qualified Data.Map as M +import qualified Data.List as L +import Data.Word (Word64) + +-- |A Trie indexed by 'Word64's. +data Trie a = Fork + { trieVal :: Maybe a + , trieMap :: M.Map Word64 (Trie a) + } deriving (Eq) + +instance Show a => Show (Trie a) where + show = unlines . map show . toList + +instance Functor Trie where + fmap f (Fork v m) = Fork (f <$> v) (fmap (fmap f) m) + +-- |The empty trie +empty :: Trie a +empty = Fork Nothing M.empty + +-- |Inserts or modifies an element to a trie +insertWith :: a -> (a -> a) -> [Word64] -> Trie a -> Trie a +insertWith x f = L.foldl' navigate insHere + where + insHere (Fork (Just val) m) = Fork (Just $ f val) m + insHere (Fork Nothing m) = Fork (Just x) m + + navigate c w64 (Fork v m) + = Fork v (M.alter (maybe (Just (c empty)) (Just . c)) w64 m) + +-- |Inserts a value overwriting any previous value associated +-- with this key +insert :: a -> [Word64] -> Trie a -> Trie a +insert x = insertWith x (const x) + +-- |Performs a lookup on a trie +lookup :: [Word64] -> Trie a -> Maybe a +lookup = L.foldl' navigate trieVal + where + navigate c w64 tr = M.lookup w64 (trieMap tr) >>= c + +-- |Computes the intersection of two tries +zipWith :: (a -> b -> c) -> Trie a -> Trie b -> Trie c +zipWith f (Fork va ma) (Fork vb mb) + = Fork (f <$> va <*> vb) (M.intersectionWith (zipWith f) ma mb) + +-- |Maps over the trie carrying an accumulating parameter +-- around +mapAccum :: (a -> b -> (a, c)) -> a -> Trie b -> (a, Trie c) +mapAccum f acc (Fork vb mb) + = let (acc' , vc) = maybe (acc , Nothing) ((id *** Just) . f acc) vb + in (id *** Fork vc) $ M.mapAccum (mapAccum f) acc' mb + +-- |Flattens a trie into a list +toList :: Trie a -> [([Word64] , a)] +toList (Fork va ma) = maybe id ((:) . ([],)) va + $ concatMap (distr1 . second toList) $ M.toList ma + where + distr1 (w , rest) = map (first (w:)) rest diff --git a/src/Generics/MRSOP/HDiff/Digest.hs b/src/Generics/MRSOP/HDiff/Digest.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/HDiff/Digest.hs @@ -0,0 +1,127 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE ScopedTypeVariables #-} +module Generics.MRSOP.HDiff.Digest where + +import Data.Proxy +import Data.Functor.Const +import Data.Void +import Data.Word (Word8,Word64) +import Data.Bits +import Data.List (splitAt,foldl') +import qualified Data.ByteString as BS +import qualified Data.ByteString.Char8 as BS8 +import qualified Data.ByteArray as BA +import qualified Data.ByteArray.Mapping as BA + +import qualified Crypto.Hash as Hash +import qualified Crypto.Hash.Algorithms as Hash (Blake2s_256) + +import Generics.MRSOP.Base + +-- |Our digests come from Blake2s_256 +newtype Digest + = Digest { getDigest :: Hash.Digest Hash.Blake2s_256 } + deriving (Eq , Show) + +-- |Unpacks a digest into a list of Word64. +toW64s :: Digest -> [Word64] +toW64s = map combine . chunksOf 8 . BA.unpack . getDigest + where + chunksOf n l + | length l <= n = [l] + | otherwise = let (h , t) = splitAt n l + in h : chunksOf n t + + -- precondition: length must be 8!!! + combine :: [Word8] -> Word64 + combine = foldl' (\acu (n , next) + -> shiftL (fromIntegral next) (8*n) .|. acu) 0 + . zip [0,8,16,24,32,40,48,56] + +-- |Process an 'SNat' into a 'Word64'. This is useful +-- in order to use type-level info as salt. +snat2W64 :: SNat n -> Word64 +snat2W64 SZ = 0 +snat2W64 (SS c) = 1 + snat2W64 c + +-- |Auxiliar hash function with the correct types instantiated. +hash :: BS.ByteString -> Digest +hash = Digest . Hash.hash + +-- |Auxiliar hash functions for strings +hashStr :: String -> Digest +hashStr = hash . BS8.pack + +-- |Concatenates digests together and hashes the result. +digestConcat :: [Digest] -> Digest +digestConcat = hash . BA.concat . map getDigest + +-- |A Value is digestible if we know how to hash it. +class Digestible (v :: *) where + digest :: v -> Digest + +-- |A Word64 is digestible +instance Digestible Word64 where + digest = hash . BA.fromW64BE + +-- |A functor is digestible if we can hash its +-- value pointwise. +class DigestibleHO (f :: k -> *) where + digestHO :: forall ki . f ki -> Digest + +instance DigestibleHO (Const Void) where + digestHO (Const _impossible) = error "DigestibleHO (Const Void)" + +-- |Authenticates a 'HPeel' without caring for the type +-- information. Only use this if you are sure of what you are +-- doing, as there can be colissions. For example: +-- +-- > data A = A1 B | A2 Int Int +-- > data B = B1 A | B2 Int Int +-- +-- > xA :: NP ann (Lkup 1 codesA) +-- > xB :: NP ann (Lkup 1 codesB) +-- > +-- > authPeel' f 0 (CS CZ) xA == authPeel' f 0 (CS CZ) xB +-- +-- That's because @A2@ and @B2@ have the exact same signature +-- and are within the exact same position within the datatype. +-- We must use the salt to pass type information: +-- +-- > authPeel' f (snat2W64 IdxA) (CS CZ) xA +-- > =/ authPeel' f (snat2W64 IdxB) (CS CZ) xB +-- +-- One should stick to 'authPeel' whenever in doubt. +authPeel' :: forall sum ann i + . (forall ix . ann ix -> Digest) + -> Word64 + -> Constr sum i + -> NP ann (Lkup i sum) + -> Digest +authPeel' proj salt cnstr p + = digestConcat $ ([digest (constr2W64 cnstr) , digest salt] ++) + $ elimNP proj p + where + -- We are mapping Constr and SNat's to + -- Word64 because these are better handled by the 'memory' + -- library. + constr2W64 :: Constr sum' n -> Word64 + constr2W64 CZ = 0 + constr2W64 (CS c) = 1 + constr2W64 c + +-- |This function correctly salts 'authPeel'' and produces +-- a unique hash per constructor. +authPeel :: forall codes ix ann i + . IsNat ix + => (forall iy . ann iy -> Digest) + -> Proxy codes + -> Proxy ix + -> Constr (Lkup ix codes) i + -> NP ann (Lkup i (Lkup ix codes)) + -> Digest +authPeel proj _ pix = authPeel' proj (snat2W64 $ getSNat pix) + diff --git a/src/Generics/MRSOP/HDiff/Holes.hs b/src/Generics/MRSOP/HDiff/Holes.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/HDiff/Holes.hs @@ -0,0 +1,112 @@ +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-orphans #-} +module Generics.MRSOP.HDiff.Holes where + +import Data.Proxy +import Data.Functor.Const +import Data.Type.Equality + +import Control.Monad.Identity + +import qualified Data.Text.Prettyprint.Doc as PP +-------------------------------- +import Generics.MRSOP.Util +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +-------------------------------- +import Generics.MRSOP.HDiff.Renderer + +-- |Pretty-prints a treefix using a specific function to +-- print holes. +holesPretty :: forall ki fam codes f at ann + . (HasDatatypeInfo ki fam codes , RendererHO ki) + => Proxy fam + -> (PP.Doc ann -> PP.Doc ann) -- ^ styling + -> (forall at' . f at' -> PP.Doc ann) + -> Holes ki codes f at + -> PP.Doc ann +holesPretty _pfam sty sx (Hole _ x) + = sty $ sx x +holesPretty _pfam sty _sx (HOpq _ k) + = sty $ renderHO k +holesPretty pfam sty sx utx@(HPeel _ c rest) + = renderNP pfam sty (holesSNat utx) c + $ mapNP (Const . holesPretty pfam sty sx) rest + + +-- |Zips a 'Holes' and a generic value together. Returns +-- 'mzero' whenever the structure of the value is not compatible +-- with that requird by the /holed/ value. +holesZipRep :: (MonadPlus m) + => Holes ki codes f at + -> NA ki (Fix ki codes) at + -> m (Holes ki codes (f :*: NA ki (Fix ki codes)) at) +holesZipRep (Hole a i) x = return $ Hole a (i :*: x) +holesZipRep (HOpq a k) _ = return $ HOpq a k +holesZipRep (HPeel a c d) (NA_I x) + | Tag cx dx <- sop (unFix x) + = case testEquality c cx of + Nothing -> mzero + Just Refl -> HPeel a cx <$> mapNPM (uncurry' holesZipRep) (zipNP d dx) + + +-- * Test Equality Instance +-- +-- Are two treefixes indexes over the same atom? + +-- TODO: remove this class too! +-- this is the same hack as Data.HDiff.Diff.MetaVar.Annotate +-- All we need is a class 'IsOpq' comming from mrsop that +-- allows us to compare the indexes of 'ki' for equality. +class HasIKProjInj (ki :: kon -> *) (f :: Atom kon -> *) where + konInj :: ki k -> f ('K k) + varProj :: Proxy ki -> f x -> Maybe (IsI x) + +instance (HasIKProjInj ki phi) => HasIKProjInj ki (Holes ki codes phi) where + konInj = HOpq' + varProj pr (Hole _ h) = varProj pr h + varProj _ (HPeel _ _ _) = Just IsI + varProj _ (HOpq _ _) = Nothing + +data IsI :: Atom kon -> * where + IsI :: (IsNat i) => IsI ('I i) + +getIsISNat :: IsI ('I i) -> SNat i +getIsISNat IsI = getSNat (Proxy :: Proxy i) + +type HolesTestEqualityCnstr ki f + = (TestEquality ki , TestEquality f , HasIKProjInj ki f) + +instance (HolesTestEqualityCnstr ki f) + => TestEquality (Holes ki codes f) where + testEquality (HOpq _ kx) (HOpq _ ky) + = testEquality kx ky >>= return . apply (Refl :: 'K :~: 'K) + testEquality (Hole _ v) (Hole _ u) + = testEquality v u + testEquality (HOpq _ kx) (Hole _ v) + = testEquality (konInj kx) v + testEquality (Hole _ v) (HOpq _ ky) + = testEquality v (konInj ky) + testEquality x@(HPeel _ _ _) (Hole _ u) + = do i@IsI <- varProj (Proxy :: Proxy ki) u + Refl <- testEquality (holesSNat x) (getIsISNat i) + return Refl + testEquality (Hole _ u) x@(HPeel _ _ _) + = do i@IsI <- varProj (Proxy :: Proxy ki) u + Refl <- testEquality (holesSNat x) (getIsISNat i) + return Refl + testEquality x@(HPeel _ _ _) y@(HPeel _ _ _) + = do Refl <- testEquality (holesSNat x) (holesSNat y) + return Refl + testEquality (HOpq _ _) (HPeel _ _ _) = Nothing + testEquality (HPeel _ _ _) (HOpq _ _) = Nothing + diff --git a/src/Generics/MRSOP/HDiff/Renderer.hs b/src/Generics/MRSOP/HDiff/Renderer.hs new file mode 100644 --- /dev/null +++ b/src/Generics/MRSOP/HDiff/Renderer.hs @@ -0,0 +1,79 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE ScopedTypeVariables #-} +-- |Defines a unified interface for writing +-- pretty printers. We force the definition of pretty +-- printers in this way to be able to use this very +-- pretty printer to render a 'Generics.MRSOP.HDiff.Treefix.UTx' +-- in the same style as the rest of the ast. +-- +module Generics.MRSOP.HDiff.Renderer where + +import Data.Proxy +import Data.Functor.Const + +import Data.Text.Prettyprint.Doc (Doc) +import qualified Data.Text.Prettyprint.Doc as PP + +import Generics.MRSOP.Util +import Generics.MRSOP.Base + +class RendererHO f where + renderHO :: f x -> Doc ann + +-- |Default rendering of constructors +renderView :: (HasDatatypeInfo ki fam codes) + => Proxy fam + -> (forall k . ki k -> Doc ann) + -> SNat ix + -> View ki (Const (Doc ann)) (Lkup ix codes) + -> Doc ann +renderView pf renderK idx (Tag c p) + = renderNP pf id idx c (mapNP (Const . elimNA renderK getConst) p) + +-- |Default rendering of NP's with Docs inside +renderNP :: (HasDatatypeInfo ki fam codes) + => Proxy fam + -> (PP.Doc ann -> PP.Doc ann) + -> SNat ix + -> Constr (Lkup ix codes) c + -> NP (Const (Doc ann)) (Lkup c (Lkup ix codes)) + -> Doc ann +renderNP pf sty idx c NP0 + = sty $ PP.pretty (constructorName (constrInfoFor pf idx c)) +renderNP pf sty idx c p + = let ci = constrInfoFor pf idx c + in PP.parens $ PP.vcat [ sty $ PP.pretty (constructorName ci) + , PP.indent 1 (PP.vsep (elimNP getConst p)) + ] + +-- |Renders elements of the family +renderEl :: forall ki fam codes ix ann + . (Family ki fam codes , HasDatatypeInfo ki fam codes , IsNat ix) + => (forall k . ki k -> Doc ann) + -> El fam ix + -> Doc ann +renderEl renderK = renderFix renderK . dfrom + +-- |Renders a fixpoint +renderFix :: forall ki fam codes ix ann + . (HasDatatypeInfo ki fam codes , IsNat ix) + => (forall k . ki k -> Doc ann) + -> Fix ki codes ix + -> Doc ann +renderFix renderK = getConst . cata renderAlg + where + renderAlg :: forall iy + . (IsNat iy) + => Rep ki (Const (Doc ann)) (Lkup iy codes) + -> Const (Doc ann) iy + renderAlg = Const . renderView (Proxy :: Proxy fam) + renderK + (getSNat (Proxy :: Proxy iy)) + . sop + diff --git a/src/Languages/RTree.hs b/src/Languages/RTree.hs new file mode 100644 --- /dev/null +++ b/src/Languages/RTree.hs @@ -0,0 +1,118 @@ +{-# LANGUAGE TupleSections #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE TypeSynonymInstances #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE DeriveDataTypeable #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# OPTIONS_GHC -Wno-missing-signatures #-} +{-# OPTIONS_GHC -Wno-incomplete-patterns #-} +{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} +module Languages.RTree where + +import Data.Type.Equality + +import Generics.MRSOP.Base +import Generics.MRSOP.TH +import Generics.MRSOP.HDiff.Digest +import Generics.MRSOP.HDiff.Renderer + +import Data.Text.Prettyprint.Doc (pretty) + +import Control.Monad +import Test.QuickCheck + +data RTree = String :>: [RTree] + deriving (Eq , Show) + +height :: RTree -> Int +height (_ :>: []) = 0 +height (_ :>: ns) = 1 + maximum (map height ns) + +data WKon = WString + +data W :: WKon -> * where + W_String :: String -> W 'WString + +instance EqHO W where + eqHO (W_String s) (W_String ss) = s == ss + +instance DigestibleHO W where + digestHO (W_String s) = hashStr s + +instance RendererHO W where + renderHO (W_String s) = pretty s + +instance ShowHO W where + showHO (W_String s) = s + +instance TestEquality W where + testEquality (W_String _) (W_String _) = Just Refl + +deriveFamilyWith ''W [t| RTree |] + +genConName :: Gen String +genConName = (:[]) <$> choose ('a' , 'm') + +genTree :: Int -> Gen RTree +genTree h + | h <= 0 = (:>:) <$> genConName <*> pure [] + | otherwise = (:>:) <$> genConName <*> genChildren + where + genChildren = do + x <- choose (0, 4) + vectorOf x $ genTree (h-1) + +insertAt :: Int -> a -> [a] -> [a] +insertAt 0 x xs = x : xs +insertAt n x (y : ys) = y : insertAt (n-1) x ys + +genInsHere :: RTree -> Gen RTree +genInsHere t = do + n <- genConName + k <- choose (0 , 3) + ns <- vectorOf k (genTree (height t)) + k' <- if length ns == 0 + then return 0 + else choose (0 , length ns - 1) + return (n :>: insertAt k' t ns) + +genSimilarTrees :: Int -> Gen (RTree , RTree) +genSimilarTrees h = do + l <- genSimilarTreesN 2 h + let [t1 , t2] = l + return (t1 , t2) + +genSimilarTreesN :: Int -> Int -> Gen [RTree] +genSimilarTreesN n0 h = do + t <- genTree h + (t:) <$> replicateM (n0-1) (go (height t) 1 t) + where + go :: Int -> Int -> RTree -> Gen RTree + go ht ch (n :>: ns) = do + ns' <- mapM (go ht (ch + 1)) ns + n' <- frequency [ (ht , return n) + , (ch , genConName) ] + frequency $ [ (ch , genInsHere (n' :>: ns')) + , (ht , return (n' :>: ns')) + ] ++ (if length ns > 0 + then [ (ch , elements ns') ] -- genDelHere + else [] ) + +instance Arbitrary RTree where + arbitrary = sized $ \n -> choose (1 , n `div` 2) >>= genTree + +genSimilarTrees' :: Gen (RTree , RTree) +genSimilarTrees' = choose (0 , 4) >>= genSimilarTrees + +genSimilarTrees'' :: Gen (RTree , RTree , RTree) +genSimilarTrees'' = choose (0 , 4) >>= genSimilarTreesN 3 + >>= \[t1 , t2 , t3] -> return (t1 , t2 , t3) + + diff --git a/src/Languages/RTree/Diff.hs b/src/Languages/RTree/Diff.hs new file mode 100644 --- /dev/null +++ b/src/Languages/RTree/Diff.hs @@ -0,0 +1,60 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +module Languages.RTree.Diff where + +import Data.Functor.Const +import Data.Void + +import Generics.MRSOP.Base +import Generics.MRSOP.Holes +import Generics.MRSOP.HDiff.Digest + +import Languages.RTree +import Data.HDiff.Patch +import Data.HDiff.Change +import Data.HDiff.Diff +import Data.HDiff.Diff.Preprocess + +type PatchRTree = Patch W CodesRTree 'Z + +rbin :: RTree -> RTree -> RTree +rbin l r = "bin" :>: [l , r] + +rlf :: String -> RTree +rlf = (:>: []) + +x1 , y1 :: RTree +x1 = rbin (rbin (rlf "t") (rbin (rlf "u") (rlf "f"))) (rlf "k") +y1 = rbin (rbin (rlf "t") (rbin (rlf "u") (rlf "f"))) (rlf "t") + +digemRTreeH :: Int -> RTree -> RTree -> PatchRTree +digemRTreeH h a b = diff h (dfrom $ into @FamRTree a) + (dfrom $ into @FamRTree b) + +digemRTreeHM :: DiffMode -> Int -> RTree -> RTree -> PatchRTree +digemRTreeHM m h a b = diffOpts (diffOptionsDefault { doMode = m + , doMinHeight = h + , doOpaqueHandling = DO_OnSpine }) + (dfrom $ into @FamRTree a) + (dfrom $ into @FamRTree b) + +rtreeMerkle :: RTree -> Digest +rtreeMerkle a = getDig $ preprocess (na2holes $ NA_I $ dfrom $ into @FamRTree a) + where + getDig :: PrepFix a ki codes (Const Void) ix -> Digest + getDig = treeDigest . getConst . holesAnn + +digemRTree :: RTree -> RTree -> PatchRTree +digemRTree a b = diff 1 (dfrom $ into @FamRTree a) + (dfrom $ into @FamRTree b) + +applyRTree :: PatchRTree -> RTree -> Either String RTree +applyRTree p x = either Left (Right . unEl . dto @'Z . unFix) + $ apply p (dfrom $ into @FamRTree x) + +applyRTreeC :: CChange W CodesRTree ('I 'Z) -> RTree -> Either String RTree +applyRTreeC p x = applyRTree (Hole' p) x + +applyRTree' :: PatchRTree -> RTree -> Maybe RTree +applyRTree' p = either (const Nothing) Just . applyRTree p diff --git a/tests/Data/Digems/Change/ClassifySpec.hs b/tests/Data/Digems/Change/ClassifySpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/Change/ClassifySpec.hs @@ -0,0 +1,117 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +module Data.Digems.Change.ClassifySpec (spec) where + +import qualified Data.Set as S + +import Generics.MRSOP.Base +import Generics.MRSOP.Util +import Generics.MRSOP.Holes + +import Data.Exists +import Data.Digems.Patch +import Data.Digems.Diff +import Data.Digems.Patch.Show +import Data.Digems.MetaVar +import Data.Digems.Change +import Data.Digems.Change.Classify +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + +-------------------------------------------- +-- ** Change Classification Unit Tests + +changeClassDual :: ChangeClass -> ChangeClass +changeClassDual CDel = CIns +changeClassDual CIns = CDel +changeClassDual x = x + +mustClassifyAs :: String -> RTree -> RTree -> [ChangeClass] -> SpecWith (Arg Bool) +mustClassifyAs lbl a b cls = do + it (lbl ++ ": change class") $ do + let patch = digemRTree a b + in cls == holesGetHolesAnnWith' changeClassify patch + + +---------------- +-- Example 1 + +a1 , b1 :: RTree +a1 = "a" :>: [ "b" :>: [] + , "c" :>: [] + , "d" :>: [] + ] + +b1 = "a" :>: [ "b'" :>: [] + , "d" :>: [] + ] + + +--------------- +-- Example 2 + +a2 , b2 :: RTree +a2 = "x" :>: [ "k" :>: [] , "u" :>: []] +b2 = "x" :>: [ "u" :>: [] , "k" :>: []] + + +--------------- +-- Example 3 + +a3 , b3 :: RTree +a3 = "x" :>: [ "k" :>: [ "a" :>: [] ] ] +b3 = "x" :>: [ "k" :>: [] , "a" :>: [] ] + +---------------- +-- Example 4 + +a4 , b4 :: RTree +a4 = "x" :>: [ "a" :>: [ "b" :>: [] ] , "c" :>: [] ] +b4 = "x" :>: [ "a" :>: [ "b" :>: ["c" :>: []]]] + +---------------- +-- Example 5 + +a5 , b5 :: RTree +a5 = "x" :>: [ "a" :>: [] , "b" :>: [] ] +b5 = "x" :>: [ "a" :>: [] , "new" :>: [] , "b" :>: [] ] + +---------------- +-- Example 6 + +a6 , b6 :: RTree +a6 = "x" :>: [ "a" :>: [] , "b" :>: [ "k" :>: [] ] ] +b6 = "x" :>: [ "a" :>: [] , "new" :>: [] , "b'" :>: [ "k" :>: [] ] ] + +---------------- +-- Example 7 + +a7 , b7 :: RTree +a7 = "x" :>: [ "a" :>: [ "aa" :>: [] , "ab" :>: []] , "b" :>: [ "bb" :>: [] ] ] +b7 = "x" :>: [ "a" :>: [ "aa" :>: [] , "ab" :>: [] , "bb" :>: [] ] , "bb" :>: [] ] + +---------------- +-- Example 8 + +a8 , b8 :: RTree +a8 = "x" :>: [ "y" :>: [] ] +b8 = "a" :>: [ "b" :>: [] , "x" :>: [ "y" :>: [] ] , "c" :>: [] ] + + +spec :: Spec +spec = do + describe "changeClassify: manual examples" $ do + mustClassifyAs "1" a1 b1 [CDel , CMod , CId] + mustClassifyAs "2" a2 b2 [CPerm , CId] + mustClassifyAs "3" a3 b3 [CPerm , CId] + mustClassifyAs "4" a4 b4 [CPerm , CId] + mustClassifyAs "5" a5 b5 [CIns , CId , CId] + mustClassifyAs "6" a6 b6 [CMod , CId , CId] + mustClassifyAs "7" a7 b7 [CMod , CId] + mustClassifyAs "8" a8 b8 [CIns] + diff --git a/tests/Data/Digems/Change/TreeEditDistanceSpec.hs b/tests/Data/Digems/Change/TreeEditDistanceSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/Change/TreeEditDistanceSpec.hs @@ -0,0 +1,50 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +module Data.Digems.Change.TreeEditDistanceSpec (spec) where + +import Generics.MRSOP.Base +import Generics.MRSOP.Util +import qualified Generics.MRSOP.GDiff as GDiff + +import Data.Digems.Patch +import Data.Digems.Patch.Show +import Data.Digems.MetaVar +import Data.Digems.Change +import qualified Data.Digems.Change.TreeEditDistance as TED + +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + +a1 , b1 :: RTree +a1 = "m" :>: ["m" :>: [],"b" :>: [],"d" :>: [],"a" :>: []] +b1 = "j" :>: ["m" :>: [],"l" :>: ["k" :>: [],"k" :>: [],"k" :>: [],"b" :>: []],"k" :>: [],"d" :>: ["f" :>: [],"i" :>: []]] + +a2 , b2 :: RTree +a2 = "i" :>: [] +b2 = "h" :>: [ "i" :>: []] + +is_the_same_as_gdiff :: Property +is_the_same_as_gdiff = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + es0 = GDiff.diff @FamRTree @_ @CodesRTree t1 t2 + in case TED.toES (distrCChange patch) (NA_I $ deep t1) of + Left err -> counterexample err False + Right es1 -> GDiff.cost es1 === GDiff.cost es0 + +is_better_than_gdiff :: Property +is_better_than_gdiff = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + es0 = GDiff.diff @FamRTree @_ @CodesRTree t1 t2 + in patchCost patch <= GDiff.cost es0 + + +spec :: Spec +spec = do + describe "Change.toES" $ do + xit "computes the same distance as generics-mrsop-gdiff" $ + property is_better_than_gdiff diff --git a/tests/Data/Digems/DiffSpec.hs b/tests/Data/Digems/DiffSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/DiffSpec.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE TypeApplications #-} +module Data.Digems.DiffSpec (spec) where + +import qualified Data.Set as S + +import Generics.MRSOP.Holes + +import Data.Digems.Diff +import Data.Digems.MetaVar +import Data.Digems.Change +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + + +diff_wellscoped_changes :: DiffMode -> Property +diff_wellscoped_changes mode = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTreeHM mode 1 t1 t2 + in conjoin $ holesGetHolesAnnWith' go patch + where + go :: CChange W CodesRTree ix -> Property + go (CMatch vars del ins) + = let vd = holesGetHolesAnnWith'' metavarGet del + vi = holesGetHolesAnnWith'' metavarGet ins + v = S.map metavarIK2Int vars + in v === vd .&&. vi === v + +apply_correctness :: DiffMode -> Property +apply_correctness mode = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTreeHM mode 1 t1 t2 + in case applyRTree patch t1 of + Left err -> counterexample ("Apply failed with: " ++ err) False + Right r -> property $ t2 == r + +diffModeSpec :: DiffMode -> Spec +diffModeSpec mode = do + describe "diff" $ do + it "produce well-scoped changes" $ do + diff_wellscoped_changes mode + describe "apply" $ do + it "is correct" $ do + apply_correctness mode + +spec :: Spec +spec = do + flip mapM_ (enumFrom (toEnum 0)) $ \m -> + describe ("Extraction (" ++ show m ++ ")") $ diffModeSpec m diff --git a/tests/Data/Digems/Patch/MergeSpec.hs b/tests/Data/Digems/Patch/MergeSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/Patch/MergeSpec.hs @@ -0,0 +1,441 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +module Data.Digems.Patch.MergeSpec (spec) where + +import Generics.MRSOP.Base + +import Data.Digems.Patch +import Data.Digems.Diff +import Data.Digems.Patch.Merge +import Data.Digems.Change +import Data.Digems.Change.Thinning +import Data.Digems.Change.Apply +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + +import Control.Monad.Except + +-------------------------------------------- +-- ** Merge Properties + +{- +merge_id :: Property +merge_id = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + iden = digemRTree t1 t1 + mpid = patch // iden + midp = iden // patch + in case (,) <$> noConflicts mpid <*> noConflicts midp of + Nothing -> expectationFailure + $ unwords [ "has conflicts:" + , unwords $ getConflicts mpid + , ";;" + , unwords $ getConflicts midp + ] + Just (pid , idp) -> + case (,) <$> applyRTree pid t1 <*> applyRTree idp t2 of + Left err -> expectationFailure ("apply failed: " ++ err) + Right (r1 , r2) -> (r1 , r2) `shouldBe` (t2 , t2) + + +merge_diag :: Property +merge_diag = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + in case noConflicts (patch // patch) of + Nothing -> expectationFailure "has conflicts" + Just p -> case applyRTree' p t2 of + Nothing -> expectationFailure "apply failed" + Just r -> r `shouldBe` t2 +-} + +-------------------------------------------- +-- ** Manual Merge Examples + +data MergeOutcome + = MergeOk + | MergeDiffers + | ApplyFailed + | HasConflicts + deriving (Eq , Show) + +expectMerge :: DiffMode + -> MergeOutcome -> String -> RTree -> RTree -> RTree + -> SpecWith (Arg Property) +expectMerge mode expt lbl a o b = do + it (lbl ++ ": " ++ show expt) $ + doMerge mode a o b `shouldBe` expt + +doMerge :: DiffMode -> RTree -> RTree -> RTree -> MergeOutcome +doMerge mode a o b + = let a' = dfrom $ into @FamRTree a + b' = dfrom $ into @FamRTree b + o' = dfrom $ into @FamRTree o + -- VCM: Funny... with DM_ProperShare and DM_NoNested + -- we see the same hspec restuls, but with DM_Patience + -- we get a different result altogether. + oa = digemRTreeHM mode 1 o a + ob = digemRTreeHM mode 1 o b + oaob = oa // ob + oboa = ob // oa + in case (,) <$> noConflicts oaob <*> noConflicts oboa of + Just (ab , ba) + -> case (,) <$> apply ab b' <*> apply ba a' of + Right (c1 , c2) + | eqFix eqHO c1 c2 -> MergeOk + | otherwise -> MergeDiffers + Left _ -> ApplyFailed + Nothing -> HasConflicts + + +mustMerge :: DiffMode -> String -> RTree -> RTree -> RTree -> SpecWith (Arg Property) +mustMerge m = expectMerge m MergeOk + +xexpectMerge :: MergeOutcome -> String -> String -> RTree -> RTree -> RTree + -> SpecWith (Arg Property) +xexpectMerge expt reason lbl a o b = do + it (lbl ++ ": " ++ show expt) $ + pendingWith reason + + + +---------------------- +-- Example 1 + +a1 , o1 , b1 :: RTree +a1 = "a" :>: [ "b" :>: [] + , "c" :>: [] + , "d" :>: [] + ] + +o1 = "a" :>: [ "b" :>: [] + , "d" :>: [] + ] + +b1 = "a" :>: [ "b'" :>: [] + , "d" :>: [] + ] + +------------------- +-- Example 2 + +a2, o2, b2 :: RTree +a2 = "b" :>: [ "u" :>: [ "3" :>: [] ] , ".." :>: [] ] + +o2 = "b" :>: [ "b" :>: [ "u" :>: [ "3" :>: [] ] , ".." :>: [] ] + , "." :>: [] + ] + +b2 = "b" :>: [ "b" :>: [ "u" :>: [ "4" :>: [] ] , "u" :>: [ ".." :>: [] ] ] + , "." :>: [] + ] + +----------------- +-- Example 3 + +a3 , o3 , b3 :: RTree +a3 = "x'" :>: [ "y" :>: [] , "z" :>: [] ] + +o3 = "x" :>: [ "y" :>: [] , "z" :>: [] ] + +b3 = "x" :>: [ "y'" :>: [] ] + +--------------------------------- +-- Example 4 + +a4 , o4 , b4 :: RTree +a4 = "y" :>: [] +o4 = "x" :>: [] +b4 = "y" :>: [] + +--------------------------------- +-- Example 5 + +a5 , o5 , b5 :: RTree +a5 = "x" :>: [ "k" :>: [] , "u" :>: []] +o5 = "x" :>: [ "u" :>: [] , "k" :>: []] +b5 = "x" :>: [ "y" :>: ["u" :>: [] , "k" :>: [] ] + , "u" :>: [] , "k" :>: [] ] + +--------------------------------- +-- Example 6 + +a6 , o6 , b6 :: RTree +a6 = "x" :>: [ "u" :>: []] +o6 = "x" :>: [ "u" :>: [] , "k" :>: []] +b6 = "x" :>: [ "y" :>: ["u" :>: [] , "k" :>: [] ] + , "u" :>: [] , "k" :>: [] ] + + +--------------------------------- +-- Example 7 + +a7 , o7 , b7 :: RTree +a7 = "x" :>: [ "u" :>: [ "b" :>: [] ] , "l" :>: [] ] +o7 = "x" :>: [ "a" :>: [] , "u" :>: [ "b" :>: [] ] , "k" :>: [] , "l" :>: []] +b7 = "y" :>: [ "a" :>: [] , "u" :>: [ "b" :>: [] ] , "k" :>: [] , "new" :>: [] , "l" :>: []] + +--------------------------------- +-- Example 8 + +a8 , o8 , b8 :: RTree +a8 = "x" :>: [ "k" :>: [] , "u" :>: []] +o8 = "x" :>: [ "u" :>: [] , "k" :>: []] +b8 = "x" :>: [ "u" :>: [] , "a" :>: [] , "k" :>: []] + +--------------------------------- +-- Example 9 + +a9 , o9 , b9 :: RTree +a9 = "x" :>: [ "k" :>: [] , "u" :>: []] +o9 = "x" :>: [ "u" :>: [] , "k" :>: []] +b9 = "x" :>: [ "u'" :>: [] , "k" :>: []] + + +-- Now we follow with triples that must NOT merge + +-------------------------------- +-- Example 10 + +a10 , o10 , b10 :: RTree +a10 = "x" :>: [ "u" :>: [] , "a" :>: [] , "k" :>: []] +o10 = "x" :>: [ "u" :>: [] , "k" :>: []] +b10 = "x" :>: [ "u" :>: [] , "b" :>: [] , "k" :>: []] + +------------------------------ +-- Example 11 + +a11 , o11 , b11 :: RTree +a11 = "x" :>: [ "u" :>: [] , "a" :>: []] +o11 = "x" :>: [ "u" :>: [] , "b" :>: []] +b11 = "x" :>: [ "u" :>: [] , "c" :>: []] + +----------------------------- +-- Example 12 + +a12 , o12 , b12 :: RTree +a12 = "f" :>: ["j" :>: []] +o12 = "f" :>: ["a" :>: []] +b12 = "e" :>: [] + +---------------------------- +-- Example 13 + +a13 , o13 , b13 :: RTree +a13 = "a" :>: [] +o13 = "d" :>: ["i" :>: []] +b13 = "a" :>: ["j" :>: ["i" :>: []]] + +--------------------------- +-- Example 14 + +a14 , o14 , b14 :: RTree +a14 = "l" :>: [] +o14 = "k" :>: ["b" :>: [],"l" :>: []] +b14 = "f" :>: ["k" :>: [],"b" :>: []] + +--------------------------- +-- Example 15 + +a15 , o15 , b15 :: RTree +a15 = "g" :>: [] +o15 = "i" :>: ["g" :>: [],"c" :>: []] +b15 = "g" :>: ["k" :>: [],"l" :>: []] + +------------------------ +-- Example 16 + +a16 , o16 , b16 :: RTree +a16 = "j" :>: [] +o16 = "g" :>: ["f" :>: [],"j" :>: []] +b16 = "e" :>: ["a" :>: [],"a" :>: [],"f" :>: []] + +------------------------ +-- Example 17 + +a17 , o17 , b17 :: RTree +a17 = "j" :>: ["f" :>: []] +o17 = "e" :>: ["f" :>: [],"f" :>: [],"m" :>: []] +b17 = "j" :>: ["g" :>: ["c" :>: [],"c" :>: [],"h" :>: [],"f" :>: []]] + +------------------------ +-- Example 18 + +a18 , o18 , b18 :: RTree +a18 = "r" :>: [ "a" :>: [] , "a" :>: []] +o18 = "r" :>: [ "a" :>: [] , "c" :>: []] +b18 = "r" :>: [ "b" :>: [] , "c" :>: [] ] + +------------------------- +-- Example 19 + +a19 , o19 , b19 :: RTree +a19 = "c" :>: ["c" :>: []] +o19 = "c" :>: ["m" :>: ["a" :>: []]] +b19 = "f" :>: ["c" :>: [],"c" :>: [],"c" :>: [],"k" :>: []] + +------------------------ +-- Example 20 + +a20 , o20 , b20 :: RTree + +a20 = "x" :>: ["a" :>: [] , "c" :>: [] , "d" :>: [] , "b" :>: []] +o20 = "x" :>: ["a" :>: [] , "b" :>: []] +b20 = "x" :>: ["a" :>: [] , "c" :>: [] , "b" :>: []] + +{- +cc :: RTree -> RTree -> RTree -> Bool +cc a o b = + let p = distrCChange $ digemRTree o a + q = distrCChange $ digemRTree o b + in case (,) <$> thin p (domain q) <*> thin q (domain p) of + Left err -> error "imp; its a span!" + Right (p' , q') + -> ( changeEq q q' && changeEq p p') + || ( changeEq q q' && not (changeEq p p')) + || (not (changeEq q q') && changeEq p p') +-} + +oa9 = digemRTree o9 a9 +ob9 = digemRTree o9 b9 + +oa8 = digemRTree o8 a8 +ob8 = digemRTree o8 b8 `withFreshNamesFrom` oa8 + +coa8 = distrCChange oa8 +cob8 = distrCChange ob8 + +myprocess ca cb = + let Right ca' = thin ca (domain cb) + Right cb' = thin cb (domain ca) + newinsa = pmatch (cCtxDel ca') (cCtxDel cb') >>= transport (cCtxIns ca') + in case runExcept newinsa of + Left err -> error ("impossible: " ++ show err) + Right r -> (r , cCtxDel cb' , cCtxIns cb') + +{- +mymerge :: RTree -> RTree -> RTree -> IO () +mymerge a o b = do + let oa = digemRTree o a + let ob = digemRTree o b `withFreshNamesFrom` oa + let ca' = distrCChange oa + let cb' = distrCChange ob + let (ca , d , cb) = myprocess ca' cb' + let (i , res) = diff' 0 d ca + let (_ , res') = diff' 0 d cb + print res + putStrLn "-----------------" + print res' +-} +{- +p = distrCChange oa8 +q = distrCChange ob8 +thinned p q = uncurry' cmatch <$> thin' (cCtxDel p :*: cCtxIns p) + (cCtxDel q :*: cCtxIns q) + +mymerge p q = do + p' <- thin p (domain q) + q' <- thin q (domain p) + if changeEq q' q + then return p + else case tr p' q' of + Left err -> error $ show err + Right r -> return r +-} + +myDigemRTree = digemRTreeHM DM_ProperShare 1 + +oa1 = myDigemRTree o1 a1 +ob1 = myDigemRTree o1 b1 + +oa2 = myDigemRTree o2 a2 +ob2 = myDigemRTree o2 b2 + +oa7 = myDigemRTree o7 a7 +ob7 = myDigemRTree o7 b7 + +oa5 = myDigemRTree o5 a5 +ob5 = myDigemRTree o5 b5 + +oa6 = myDigemRTree o6 a6 +ob6 = myDigemRTree o6 b6 + +oa12 = myDigemRTree o12 a12 +ob12 = myDigemRTree o12 b12 + +oa13 = myDigemRTree o13 a13 +ob13 = myDigemRTree o13 b13 + +oa14 = myDigemRTree o14 a14 +ob14 = myDigemRTree o14 b14 + +oa15 = myDigemRTree o15 a15 +ob15 = myDigemRTree o15 b15 + +oa16 = myDigemRTree o16 a16 +ob16 = myDigemRTree o16 b16 + +oa17 = myDigemRTree o17 a17 +ob17 = myDigemRTree o17 b17 + +oa18 = myDigemRTree o18 a18 +ob18 = myDigemRTree o18 b18 + +oa19 = myDigemRTree o19 a19 +ob19 = myDigemRTree o19 b19 + +oa20 = myDigemRTree o20 a20 +ob20 = myDigemRTree o20 b20 + +gen3Trees :: Gen (RTree , RTree , RTree) +gen3Trees = choose (0 , 4) + >>= genSimilarTreesN 3 + >>= \[a , o , b] -> return (a , o , b) + +spec :: Spec +spec = do + -- describe "properties" $ do + -- it "p // id == p && id // p == id" $ merge_id + -- it "p // p == id" $ merge_diag + + flip mapM_ (enumFrom (toEnum 0)) $ \m -> do + describe ("merge: manual examples (" ++ show m ++ ")") $ do + mustMerge m "01" a1 o1 b1 + mustMerge m "02" a2 o2 b2 + mustMerge m "03" a3 o3 b3 + mustMerge m "04" a4 o4 b4 + if m == DM_Patience + then expectMerge m HasConflicts "05" a5 o5 b5 + else mustMerge m "05" a5 o5 b5 + if m == DM_Patience + then expectMerge m HasConflicts "06" a6 o6 b6 + else mustMerge m "06" a6 o6 b6 + mustMerge m "07" a7 o7 b7 + mustMerge m "08" a8 o8 b8 + mustMerge m "09" a9 o9 b9 + + expectMerge m HasConflicts "10" a10 o10 b10 + expectMerge m HasConflicts "11" a11 o11 b11 + expectMerge m HasConflicts "12" a12 o12 b12 + + mustMerge m "13" a13 o13 b13 + + expectMerge m HasConflicts "14" a14 o14 b14 + expectMerge m HasConflicts "15" a15 o15 b15 + expectMerge m HasConflicts "16" a16 o16 b16 + if m == DM_Patience + then mustMerge m "17" a17 o17 b17 + else expectMerge m HasConflicts "17" a17 o17 b17 + + mustMerge m "18" a18 o18 b18 + mustMerge m "19" a19 o19 b19 + xexpectMerge MergeOk "What to do with self-contained ins-ins?" "20" a20 o20 b20 + + describe ("merge: conflict or ok (" ++ show m ++ ")") $ do + it "contains no apply fail or merge differs" $ property $ + forAll gen3Trees $ \(a , o , b) + -> doMerge m a o b `elem` [MergeOk , HasConflicts] diff --git a/tests/Data/Digems/Patch/ThinningSpec.hs b/tests/Data/Digems/Patch/ThinningSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/Patch/ThinningSpec.hs @@ -0,0 +1,159 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +module Data.Digems.Patch.ThinningSpec (spec) where + +import qualified Data.Set as S + +import Generics.MRSOP.Base +import Generics.MRSOP.Util +import Generics.MRSOP.Holes + +import Data.Functor.Const +import Data.Exists +import Data.Digems.Patch +import Data.Digems.Diff +import Data.Digems.Patch.Show +import Data.Digems.Patch.Thinning as PT +import qualified Data.Digems.Change.Thinning as CT +import Data.Digems.MetaVar +import Data.Digems.Change +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + +import Control.Monad.State +import Control.Monad.Cont +import qualified Data.Map as M + +context_alpha_eq :: (EqHO ki) + => Holes ki codes (MetaVarIK ki) at + -> Holes ki codes (MetaVarIK ki) at + -> Bool +context_alpha_eq x y = aux + where + aux :: Bool + aux = (`runCont` id) $ + callCC $ \exit -> flip evalStateT M.empty $ do + holesMapM (uncurry' (check (cast exit $ False))) (holesLCP x y) + return True + + cast :: (Bool -> Cont Bool b) + -> Bool -> Cont Bool (Const () a) + cast f b = (const (Const ())) <$> f b + + check :: (Cont Bool (Const () at)) + -> Holes ki codes (MetaVarIK ki) at + -> Holes ki codes (MetaVarIK ki) at + -> StateT (M.Map Int Int) (Cont Bool) (Const () at) + check exitF (Hole _ vx) (Hole _ vy) = do + m <- get + case M.lookup (metavarGet vx) m of + Nothing -> modify (M.insert (metavarGet vx) (metavarGet vy)) + >> return (Const ()) + Just vz -> if metavarGet vy /= vz + then lift exitF + else return (Const ()) + check exitF _ _ = lift exitF + +thin_domain_eq :: DiffMode -> Property +thin_domain_eq mode = forAll genSimilarTrees'' $ \(a , o , b) + -> let oa = digemRTreeHM mode 1 o a + ob = digemRTreeHM mode 1 o b + in case (,) <$> PT.thin oa ob <*> PT.thin ob oa of + Left err -> counterexample ("Thinning failed with: " ++ show err) False + Right (oa' , ob') -> + property $ context_alpha_eq + (domain $ distrCChange oa') + (domain $ distrCChange ob') + +----------------------------- + +thin_respect_spans :: DiffMode -> Property +thin_respect_spans mode = forAll genSimilarTrees'' $ \(a , o , b) + -> let oa = digemRTreeHM mode 1 o a + ob = digemRTreeHM mode 1 o b + in case PT.thin oa ob of + Left err -> counterexample ("Thinning failed with: " ++ show err) False + Right oa' -> property $ applyRTree oa' o == Right a + +--------------------------- + +thin_pp_is_p :: DiffMode -> Property +thin_pp_is_p mode = forAll genSimilarTrees' $ \(a , b) + -> let ab = digemRTreeHM mode 1 a b + in case PT.thin ab ab of + Left err -> counterexample ("Thinning failed with: " ++ show err) False + Right ab' -> property $ patchEq ab ab' + + +------------------------------- + +lf :: String -> RTree +lf x = x :>: [] + +bin :: RTree -> RTree -> RTree +bin l r = "bin" :>: [l , r] + +a1 , o1 , b1 :: RTree +a1 = bin (bin (lf "w") (lf "z")) (bin (lf "x") (lf "y")) +o1 = bin (bin (lf "x") (lf "y")) (bin (lf "w") (lf "z")) +b1 = bin (bin (lf "y") (lf "x")) (bin (lf "w") (lf "z")) + +oa1 = digemRTree o1 a1 +ob1 = digemRTree o1 b1 `withFreshNamesFrom` oa1 + +coa1 = distrCChange oa1 +cob1 = distrCChange ob1 + +--------------------- + +a2 , o2 , b2 :: RTree +a2 = "e" :>: ["j" :>: []] +o2 = "e" :>: ["a" :>: ["j" :>: []],"a" :>: ["j" :>: []]] +b2 = "a" :>: ["j" :>: [],"e" :>: []] + +oa2 = digemRTree o2 a2 +ob2 = digemRTree o2 b2 `withFreshNamesFrom` oa2 + +coa2 = distrCChange oa2 +cob2 = distrCChange ob2 + +----------------------- +-- + +a3 , o3 , b3 :: RTree +a3 = "e" :>: ["a" :>: [], "B" :>: [], "c" :>: []] +o3 = "e" :>: ["a" :>: [], "b" :>: [], "c" :>: []] +b3 = "e" :>: ["A" :>: [], "b" :>: [], "c" :>: []] + +oa3 = digemRTree o3 a3 +ob3 = digemRTree o3 b3 + +a4 = "k" :>: ["b" :>: [],"f" :>: []] +o4 = "k" :>: ["b" :>: [],"b" :>: []] +b4 = "k" :>: ["m" :>: [],"b" :>: []] + +oa4 = digemRTree o4 a4 +ob4 = digemRTree o4 b4 + +Right coa4 = PT.thin oa4 ob4 +Right cob4 = PT.thin ob4 oa4 + +ca = domain $ distrCChange coa4 +cb = domain $ distrCChange cob4 + +ok = context_alpha_eq ca cb + +spec :: Spec +spec = do + flip mapM_ (enumFrom (toEnum 0)) $ \m -> do + describe ("thin (" ++ show m ++ ")") $ do + it "is always possible for spans" $ property (thin_respect_spans m) + it "is symmetric w.r.t. domains" $ property (thin_domain_eq m) + it "respects: thin p p == p" $ property (thin_pp_is_p m) + + diff --git a/tests/Data/Digems/PatchSpec.hs b/tests/Data/Digems/PatchSpec.hs new file mode 100644 --- /dev/null +++ b/tests/Data/Digems/PatchSpec.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} +module Data.Digems.PatchSpec (spec) where + +import qualified Data.Set as S +import Data.Functor.Const + +import Generics.MRSOP.Base +import Generics.MRSOP.Util +import Generics.MRSOP.Holes + +import Data.Exists +import Data.Digems.Patch +import Data.Digems.Diff +import Data.Digems.Patch.Show +import Data.Digems.MetaVar +import Data.Digems.Change +import Languages.RTree +import Languages.RTree.Diff + +import Test.QuickCheck +import Test.Hspec + +---------------------------------------------- + +copy_composes :: Property +copy_composes = forAll genSimilarTrees' $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + cpy = Hole' (changeCopy (NA_I (Const 0))) :: PatchRTree + in composes patch cpy .&&. composes cpy patch + +composes_correct :: Property +composes_correct = forAll (choose (0 , 4) >>= genSimilarTreesN 3) + $ \[a , b , c] -> + let ab = digemRTree a b + bc = digemRTree b c + in composes bc ab + +{- + NOT TRUE!!!! + + check: ("f" :>: ["i" :>: [],"j" :>: [],"a" :>: []],"j" :>: []) + +composes_non_reflexive :: Property +composes_non_reflexive = forAll (genSimilarTrees' `suchThat` uncurry (/=)) + $ \(t1 , t2) + -> let patch = digemRTree t1 t2 + in composes patch patch === False +-} + +spec :: Spec +spec = do + describe "composes" $ do + it "has copy as left and right id" $ property copy_composes + it "is correct" $ property composes_correct + diff --git a/tests/Spec.hs b/tests/Spec.hs new file mode 100644 --- /dev/null +++ b/tests/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}