hdiff 0.0.0 → 0.0.1
raw patch · 24 files changed
+190/−190 lines, 24 filesdep ~generics-mrsop
Dependency ranges changed: generics-mrsop
Files
- executables/HDiff.hs +2/−1
- executables/Languages/Clojure/AST.hs +12/−13
- executables/Languages/Interface.hs +23/−26
- executables/Languages/Lines.hs +5/−11
- executables/Languages/Lua.hs +11/−12
- executables/Languages/While.hs +4/−10
- hdiff.cabal +5/−5
- src/Data/Exists.hs +7/−3
- src/Data/HDiff/Change.hs +1/−0
- src/Data/HDiff/Change/Apply.hs +7/−7
- src/Data/HDiff/Change/Classify.hs +6/−5
- src/Data/HDiff/Change/Thinning.hs +4/−2
- src/Data/HDiff/Change/TreeEditDistance.hs +35/−34
- src/Data/HDiff/Diff.hs +9/−8
- src/Data/HDiff/Diff/Types.hs +1/−1
- src/Data/HDiff/Example.hs +9/−9
- src/Data/HDiff/MetaVar.hs +6/−5
- src/Data/HDiff/Patch.hs +7/−6
- src/Data/HDiff/Patch/Merge.hs +5/−7
- src/Data/HDiff/Patch/Show.hs +10/−9
- src/Data/HDiff/Patch/Thinning.hs +5/−1
- src/Data/HDiff/Patch/TreeEditDistance.hs +11/−10
- src/Generics/MRSOP/HDiff/Renderer.hs +1/−1
- src/Languages/RTree.hs +4/−4
executables/HDiff.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-}@@ -348,6 +349,6 @@ 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'+ if fb' == fa' then return ExitSuccess else return (ExitFailure 2)
executables/Languages/Clojure/AST.hs view
@@ -1,14 +1,16 @@-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE BangPatterns #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE TypeSynonymInstances #-}-{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE BangPatterns #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-+{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-}+{-# OPTIONS_GHC -Wno-orphans #-} module Languages.Clojure.AST where import Data.Type.Equality@@ -22,7 +24,6 @@ import Generics.MRSOP.HDiff.Digest import Generics.MRSOP.HDiff.Renderer - data SepExprList = Nil | Cons Expr !Sep SepExprList @@ -69,8 +70,6 @@ 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
executables/Languages/Interface.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE DataKinds #-}@@ -22,9 +23,8 @@ import Generics.MRSOP.HDiff.Renderer import Generics.MRSOP.HDiff.Digest - data LangParser :: * where- LangParser :: (LangCnstr ki fam codes ix)+ LangParser :: (LangCnstr ki fam codes ix, EqHO ki , ShowHO ki) -- |Language extension => String -- |Parser that@@ -32,23 +32,22 @@ -> LangParser data VectorOf (a :: *) (n :: Nat) :: * where- V0 :: VectorOf a Z- VS :: a -> VectorOf a n -> VectorOf a (S n)+ 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 _ 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)+ = (HasDatatypeInfo ki fam codes, RendererHO ki, IsNat ix, DigestibleHO ki, TestEquality ki) -- |Given a list of languages, parses a number of files withParsedEl :: LangParser- -> VectorOf FilePath (S n)+ -> VectorOf FilePath ('S n) -> (forall kon (ki :: kon -> *) fam codes ix- . (LangCnstr ki fam codes ix)- => VectorOf (Fix ki codes ix) (S n)+ . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)+ => VectorOf (Fix ki codes ix) ('S n) -> IO res) -> ExceptT String IO res withParsedEl (LangParser ext parser) vec f@@ -60,24 +59,23 @@ -> (FilePath -> IO (Fix ki codes ix)) -> FilePath -> ExceptT String IO (Fix ki codes ix)- parseWithExt ext parser file- | ("." ++ ext) `isSuffixOf` file = liftIO $ parser file+ parseWithExt e p file+ | ("." ++ ext) `isSuffixOf` file = liftIO $ p file | otherwise- = throwError ("Wrong Extension; expecting: " ++ show ext ++ "\n")+ = throwError ("Wrong Extension; expecting: " ++ show e ++ "\n") -- |Tries a variety of parsers on a number of -- files. withParsedEls :: [LangParser]- -> VectorOf FilePath (S n)+ -> VectorOf FilePath ('S n) -> (forall kon (ki :: kon -> *) fam codes ix- . (LangCnstr ki fam codes ix)- => VectorOf (Fix ki codes ix) (S n)+ . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki)+ => 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+withParsedEls (p:ps) files f = withParsedEl p files f+ <|> withParsedEls ps files f -- * Fixed interface for one, two and three files@@ -91,36 +89,35 @@ withParsed1 :: [LangParser] -> FilePath -> (forall kon (ki :: kon -> *) fam codes ix- . (LangCnstr ki fam codes ix)+ . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki) => Fix ki codes ix -> IO res) -> IO res withParsed1 parsers file f = redirectErr $ withParsedEls parsers (VS file V0)- $ \(VS file V0) -> f file+ $ \(VS x V0) -> f x - withParsed2 :: [LangParser] -> FilePath -> FilePath -> (forall kon (ki :: kon -> *) fam codes ix- . (LangCnstr ki fam codes ix)+ . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki) => 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+ $ \(VS x (VS y V0)) -> f x y withParsed3 :: [LangParser] -> FilePath -> FilePath -> FilePath -> (forall kon (ki :: kon -> *) fam codes ix- . (LangCnstr ki fam codes ix)+ . (LangCnstr ki fam codes ix , EqHO ki , ShowHO ki) => 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+ $ \(VS x (VS y (VS z V0))) -> f x y z
executables/Languages/Lines.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-}@@ -9,22 +10,18 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeApplications #-}+{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} 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 @@ -45,14 +42,11 @@ data W :: WKon -> * where W_String :: String -> W WString -instance EqHO W where- eqHO (W_String s) (W_String ss) = s == ss+deriving instance Show (W x)+deriving instance Eq (W x) 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.
executables/Languages/Lua.hs view
@@ -1,14 +1,15 @@-{-# LANGUAGE TemplateHaskell #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE TypeSynonymInstances #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE CPP #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE CPP #-}+ module Languages.Lua where #ifdef ENABLE_LUA_SUPPORT@@ -56,8 +57,6 @@ 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
executables/Languages/While.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-}@@ -9,7 +10,7 @@ {-# LANGUAGE GADTs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeApplications #-}-{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-missing-signatures #-} {-# OPTIONS_GHC -Wno-missing-pattern-synonym-signatures #-} module Languages.While where @@ -76,20 +77,13 @@ 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+deriving instance Eq (W x)+deriving instance Show (W x) 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.
hdiff.cabal view
@@ -4,10 +4,10 @@ -- -- see: https://github.com/sol/hpack ----- hash: b37884aac4ee07f3aa56e35f35c9f4e9a3e6f1e608768849bd352a9ec364a3c0+-- hash: 2a593069031274f1574dee4f16bb500347e9eeba60f7a3faaaf2b3e92fc9c7b8 name: hdiff-version: 0.0.0+version: 0.0.1 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@@ -58,7 +58,7 @@ , bytestring , containers , cryptonite- , generics-mrsop >=2.1.0+ , generics-mrsop >=2.2.0 , generics-mrsop-gdiff , hspec , memory@@ -88,7 +88,7 @@ , bytestring , containers , cryptonite- , generics-mrsop >=2.1.0+ , generics-mrsop >=2.2.0 , generics-mrsop-gdiff , gitrev , hdiff@@ -122,7 +122,7 @@ , bytestring , containers , cryptonite- , generics-mrsop >=2.1.0+ , generics-mrsop >=2.2.0 , generics-mrsop-gdiff , hdiff , hspec
src/Data/Exists.hs view
@@ -1,6 +1,7 @@-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE GADTs #-} module Data.Exists where data Exists (f :: k -> *) :: * where@@ -14,4 +15,7 @@ exElim :: (forall x . f x -> a) -> Exists f -> a exElim f (Exists x) = f x++instance (forall i . Show (x i)) => Show (Exists x) where+ show (Exists x) = show x
src/Data/HDiff/Change.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE TypeOperators #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}
src/Data/HDiff/Change/Apply.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE TupleSections #-}@@ -63,8 +64,7 @@ -- |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)+type Applicable ki codes phi = (TestEquality ki , TestEquality phi , HasIKProjInj ki phi ) -- |We try to unify @pa@ and @pq@ onto @ea@. The idea is that -- we instantiate the variables of @pa@ with their corresponding expression@@ -72,7 +72,7 @@ -- we ignore whatever was on @ea@ and give that variable instead. -- -- We are essentially applying -genericApply :: (Applicable ki codes phi)+genericApply :: (Applicable ki codes phi , EqHO phi , EqHO ki) => CChange ki codes at -> Holes ki codes phi at -> Either (ApplicationErr ki codes phi) (Holes ki codes phi at)@@ -100,13 +100,13 @@ -- |@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)+pmatch :: (Applicable ki codes phi , EqHO phi , EqHO ki) => 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)+pmatch' :: (Applicable ki codes phi , EqHO phi , EqHO ki) => Subst ki codes phi -> Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix@@ -114,7 +114,7 @@ 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+ | oa == ox = return s | otherwise = throwError (IncompatibleOpqs oa ox) pmatch' s pa@(HPeel _ ca ppa) x@(HPeel _ cx px) = case testEquality ca cx of@@ -143,7 +143,7 @@ -- |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)+substInsert :: (Applicable ki codes phi , EqHO ki , EqHO phi) => Subst ki codes phi -> MetaVarIK ki ix -> Holes ki codes phi ix
src/Data/HDiff/Change/Classify.hs view
@@ -1,8 +1,9 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}-{-# OPTIONS_GHC -Wno-orphans #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-}+{-# OPTIONS_GHC -Wno-orphans #-} -- |change classification algorithm module Data.HDiff.Change.Classify where
src/Data/HDiff/Change/Thinning.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-}@@ -42,6 +43,7 @@ (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@@ -110,7 +112,7 @@ (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+ go p q | p == q = return p | otherwise = throwError (IncompatibleTerms p q) -- Whenever we see a variable being matched against a term@@ -132,7 +134,7 @@ -- 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)+ Just q' -> unless (q' == q) $ void $ utxThin q' q
src/Data/HDiff/Change/TreeEditDistance.hs view
@@ -1,8 +1,9 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-} module Data.HDiff.Change.TreeEditDistance where import qualified Data.Map as M@@ -33,11 +34,11 @@ = LC Int a (ListES a) | LD Int a (ListES a) | LI Int a (ListES a)- | LNil+ | LLP_Nil deriving (Eq , Show) cost :: ListES a -> Int-cost LNil = 0+cost LLP_Nil = 0 cost (LC c _ _) = c cost (LI c _ _) = c cost (LD c _ _) = c@@ -46,18 +47,18 @@ -- For example, -- -- > λ> lcs [0,1,2] [0,1,1,1,2]--- > LC 0 (LC 1 (LI 1 (LI 1 (LC 2 LNil))))+-- > LC 0 (LC 1 (LI 1 (LI 1 (LC 2 LLP_Nil)))) -- -- 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))))+-- > LC 0 (LI 1 (LI 1 (LC 1 (LC 2 LLP_Nil)))) -- -- 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 LLP_Nil = LLP_Nil 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))@@ -90,7 +91,7 @@ return $ res lcs'' :: STRef s (Table a) -> [a] -> [a] -> ST s (ListES a)- lcs'' _ [] [] = return LNil+ lcs'' _ [] [] = return LLP_Nil 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) =@@ -122,7 +123,7 @@ 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))+ in runExcept (runReaderT (compress <$> delPhase (del :* Nil) (ins :* Nil)) (s , ves)) type ToES ki codes = ReaderT (Subst ki codes (MetaVarIK ki) , ListES Int) (Except String)@@ -151,13 +152,13 @@ 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+ case GD.cofHeq 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+ case GD.cofHeq v v' of Just (Refl , Refl) -> gcpy v (compress e) Nothing -> gins v (compress $ GD.Del c' v' e) compress (GD.Ins _ v e)@@ -168,7 +169,7 @@ 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 Nil = 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)@@ -176,7 +177,7 @@ 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 Nil = 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)@@ -184,35 +185,35 @@ 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 Nil = 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+listAssoc LP_Nil _ _ = Refl+listAssoc (LP_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+listDrop LP_Nil a = a+listDrop (LP_Cons x) (LP_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.ES0 = LP_Nil+esDelListPrf (GD.Cpy _ v e) = LP_Cons $ listDrop (cofListPrf v) (esDelListPrf e)+esDelListPrf (GD.Del _ v e) = LP_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.ES0 = LP_Nil+esInsListPrf (GD.Cpy _ v e) = LP_Cons $ listDrop (cofListPrf v) (esInsListPrf e)+esInsListPrf (GD.Ins _ v e) = LP_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.ConstrK _) = LP_Nil cofListPrf (GD.ConstrI _ p) = p esDelListProxy :: GD.ES ki codes ds is -> Proxy ds@@ -275,7 +276,7 @@ then throwError "delSync: var mismatch" else do t <- fetch var- es0 <- delOnly (t :* NP0)+ es0 <- delOnly (t :* Nil) es1 <- local (second (const es')) $ delPhase ds is return (appendES es0 es1)@@ -297,7 +298,7 @@ then throwError "insSync: var mismatch" else do t <- fetch var- es0 <- insOnly (t :* NP0)+ es0 <- insOnly (t :* Nil) es1 <- local (second (const es')) $ insPhase ds is return (appendES es0 es1)@@ -313,7 +314,7 @@ then throwError "insSync: var mismatch" else do t <- fetch var- es0 <- cpyOnly (t :* NP0)+ es0 <- cpyOnly (t :* Nil) es1 <- local (second (const es')) $ delPhase ds' is case testEquality var var'' of@@ -322,21 +323,21 @@ -- Otherwise, we must enter the deletion phase until -- we find it. _ -> delPhase ds (Hole' var :* is)- LNil -> throwError "insSync: premature LNil"+ LLP_Nil -> throwError "insSync: premature LLP_Nil" 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 Nil 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 Nil = delOnly ds insPhase ds (i :* is) = case i of Hole _ var -> insSync var ds is
src/Data/HDiff/Diff.hs view
@@ -1,11 +1,12 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE PatternSynonyms #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-} module Data.HDiff.Diff ( diffOpts' , diffOpts
src/Data/HDiff/Diff/Types.hs view
@@ -45,7 +45,7 @@ -- |Specifies the options for the diffing algorithm data DiffOptions = DiffOptions- -- |Minimum height of trees considered for sharing+ -- ^ Minimum height of trees considered for sharing { doMinHeight :: Int , doOpaqueHandling :: DiffOpaques , doMode :: DiffMode
src/Data/HDiff/Example.hs view
@@ -111,23 +111,23 @@ unif1 = HPeel' CZ (HOpq' (SInt 100) :* Hole' (NA_I $ Const 1) :* Hole' (NA_I $ Const 2)- :* NP0)+ :* Nil) unif12 :: TreeTerm unif12 = HPeel' CZ (HOpq' (SInt 500) :* Hole' (NA_I $ Const 1) :* Hole' (NA_I $ Const 2)- :* NP0)+ :* Nil) unif2 :: TreeTerm unif2 = HPeel' CZ (HOpq' (SInt 200) :* Hole' (NA_I $ Const 4) :* Hole' (NA_I $ Const 5)- :* NP0)+ :* Nil) unif22 :: TreeTerm unif22 = HPeel' CZ (HOpq' (SInt 500) :* Hole' (NA_I $ Const 4) :* Hole' (NA_I $ Const 5)- :* NP0)+ :* Nil) @@ -140,9 +140,9 @@ :* 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)+ :* HPeel' (CS (CS CZ)) Nil+ :* HPeel' (CS (CS CZ)) Nil+ :* Nil)+ :* HPeel' (CS (CS CZ)) Nil+ :* Nil) -}
src/Data/HDiff/MetaVar.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE PolyKinds #-}@@ -33,12 +34,12 @@ 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 (ShowHO f , Show x) => Show (Annotate x f k) where+ show (Annotate i f)+ = show 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 (EqHO f , Eq x) => Eq (Annotate x f k) where+ (==) (Annotate x1 f1) (Annotate x2 f2) = x1 == x2 && f1 == f2 instance (TestEquality ki) => TestEquality (Annotate x ki) where testEquality (Annotate _ x) (Annotate _ y)
src/Data/HDiff/Patch.hs view
@@ -1,8 +1,9 @@-{-# LANGUAGE TupleSections #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE TupleSections #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE GADTs #-} module Data.HDiff.Patch where import Control.Monad.State@@ -160,7 +161,7 @@ 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)+ | 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
src/Data/HDiff/Patch/Merge.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE TypeSynonymInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}@@ -67,6 +68,7 @@ -- of @p@ so that it could be applied to an element in the -- image of @q@. (//) :: ( Applicable ki codes (Holes2 ki codes)+ , EqHO ki , ShowHO ki , HasDatatypeInfo ki fam codes ) => Patch ki codes ix@@ -83,7 +85,7 @@ -- 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)+ . ( Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki , HasDatatypeInfo ki fam codes ) => RawPatch ki codes at@@ -135,10 +137,6 @@ 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@@ -150,7 +148,7 @@ -- 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))+process :: (Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki) => HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> ProcessOutcome ki codes process sp sq =@@ -203,7 +201,7 @@ -- |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))+ step2 :: (Applicable ki codes (Holes2 ki codes) , EqHO ki , ShowHO ki) => HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> ExceptT String (State (Subst ki codes (Holes2 ki codes))) () step2 pp qq = do
src/Data/HDiff/Patch/Show.hs view
@@ -1,10 +1,11 @@-{-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}-{-# OPTIONS_GHC -Wno-orphans #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# 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@@ -124,8 +125,8 @@ => 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)+ (holesPretty (Proxy :: Proxy fam) id (pretty . show) del)+ (holesPretty (Proxy :: Proxy fam) id (pretty . show) ins) show _ = undefined -- ghc seems to really want this to see the patterns are complete.
src/Data/HDiff/Patch/Thinning.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE ConstraintKinds #-}@@ -20,12 +21,15 @@ import Data.HDiff.Change import qualified Data.HDiff.Change.Thinning as CT -thin :: (ShowHO ki , TestEquality ki, EqHO ki)+thin :: forall ki codes at+ . (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 :: RawPatch ki codes at' -> RawPatch ki codes at'+ -> Either (CT.ThinningErr ki codes) (CChange ki codes at') go cp cq = let cp' = distrCChange cp cq' = distrCChange cq in CT.thin cp' (domain cq')
src/Data/HDiff/Patch/TreeEditDistance.hs view
@@ -1,9 +1,10 @@-{-# LANGUAGE ViewPatterns #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE ScopedTypeVariables #-} module Data.HDiff.Patch.TreeEditDistance where import Data.Type.Equality@@ -29,13 +30,13 @@ <$> toES' ppa px listId :: ListPrf a -> ListPrf a :~: ListPrf (a :++: '[]) -listId Nil = Refl-listId (Cons a) = case listId a of- Refl -> Refl+listId LP_Nil = Refl+listId (LP_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' Nil Nil = return GD.ES0 toES' (p :* ps) (x :* xs) = TED.appendES <$> toES p x <*> toES' ps xs
src/Generics/MRSOP/HDiff/Renderer.hs view
@@ -44,7 +44,7 @@ -> Constr (Lkup ix codes) c -> NP (Const (Doc ann)) (Lkup c (Lkup ix codes)) -> Doc ann-renderNP pf sty idx c NP0+renderNP pf sty idx c Nil = sty $ PP.pretty (constructorName (constrInfoFor pf idx c)) renderNP pf sty idx c p = let ci = constrInfoFor pf idx c
src/Languages/RTree.hs view
@@ -1,3 +1,4 @@+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TupleSections #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE FlexibleInstances #-}@@ -40,8 +41,7 @@ data W :: WKon -> * where W_String :: String -> W 'WString -instance EqHO W where- eqHO (W_String s) (W_String ss) = s == ss+deriving instance Eq (W x) instance DigestibleHO W where digestHO (W_String s) = hashStr s@@ -49,8 +49,8 @@ instance RendererHO W where renderHO (W_String s) = pretty s -instance ShowHO W where- showHO (W_String s) = s+instance Show (W x) where+ show (W_String s) = s instance TestEquality W where testEquality (W_String _) (W_String _) = Just Refl