packages feed

hdiff (empty) → 0.0.0

raw patch · 40 files changed

+5296/−0 lines, 40 filesdep +QuickCheckdep +basedep +bytestring

Dependencies added: QuickCheck, base, bytestring, containers, cryptonite, generics-mrsop, generics-mrsop-gdiff, gitrev, hdiff, hspec, language-lua, memory, mtl, optparse-applicative, parsec, prettyprinter, prettyprinter-ansi-terminal, text

Files

+ LICENSE view
@@ -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.
+ executables/HDiff.hs view
@@ -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)
+ executables/Languages/Clojure.hs view
@@ -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
+ executables/Languages/Clojure/AST.hs view
@@ -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 |]
+ executables/Languages/Clojure/Parser.hs view
@@ -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)
+ executables/Languages/Interface.hs view
@@ -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
+ executables/Languages/Lines.hs view
@@ -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)+
+ executables/Languages/Lua.hs view
@@ -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
+ executables/Languages/While.hs view
@@ -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+
+ hdiff.cabal view
@@ -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 <v.cacciarimiraldo@gmail.com>+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
+ src/Data/Exists.hs view
@@ -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+
+ src/Data/HDiff/Change.hs view
@@ -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+
+ src/Data/HDiff/Change/Apply.hs view
@@ -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+
+ src/Data/HDiff/Change/Classify.hs view
@@ -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+
+ src/Data/HDiff/Change/Thinning.hs view
@@ -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+
+ src/Data/HDiff/Change/TreeEditDistance.hs view
@@ -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) +
+ src/Data/HDiff/Diff.hs view
@@ -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})
+ src/Data/HDiff/Diff/Modes.hs view
@@ -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))+
+ src/Data/HDiff/Diff/Preprocess.hs view
@@ -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 ()
+ src/Data/HDiff/Diff/Types.hs view
@@ -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
+ src/Data/HDiff/Example.hs view
@@ -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)+-}
+ src/Data/HDiff/MetaVar.hs view
@@ -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+
+ src/Data/HDiff/Patch.hs view
@@ -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
+ src/Data/HDiff/Patch/Merge.hs view
@@ -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
+ src/Data/HDiff/Patch/Show.hs view
@@ -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 ' ']
+ src/Data/HDiff/Patch/Thinning.hs view
@@ -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
+ src/Data/HDiff/Patch/TreeEditDistance.hs view
@@ -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+
+ src/Data/WordTrie.hs view
@@ -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
+ src/Generics/MRSOP/HDiff/Digest.hs view
@@ -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)+
+ src/Generics/MRSOP/HDiff/Holes.hs view
@@ -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+
+ src/Generics/MRSOP/HDiff/Renderer.hs view
@@ -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+
+ src/Languages/RTree.hs view
@@ -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)++
+ src/Languages/RTree/Diff.hs view
@@ -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
+ tests/Data/Digems/Change/ClassifySpec.hs view
@@ -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]+
+ tests/Data/Digems/Change/TreeEditDistanceSpec.hs view
@@ -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
+ tests/Data/Digems/DiffSpec.hs view
@@ -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
+ tests/Data/Digems/Patch/MergeSpec.hs view
@@ -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]
+ tests/Data/Digems/Patch/ThinningSpec.hs view
@@ -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)++
+ tests/Data/Digems/PatchSpec.hs view
@@ -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+
+ tests/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}