module Data.Generic.Diff (
diff,
patch,
diffL,
patchL,
compress,
EditScriptL(..),
EditScript,
Family(..),
Type(..),
(:=:)(..),
Con(..),
Nil(..),
Cons(..),
) where
type EditScript f x y = EditScriptL f (Cons x Nil) (Cons y Nil)
patch :: EditScript f x y -> x -> y
patch d x = case patchL d (CCons x CNil) of
CCons y CNil -> y
diff :: (Type f x, Type f y) => x -> y -> EditScript f x y
diff x y = diffL (CCons x CNil) (CCons y CNil)
patchL :: forall f txs tys . EditScriptL f txs tys -> txs -> tys
patchL (Ins c d) = insert c . patchL d
patchL (Del c d) = patchL d . delete c
patchL (Cpy c d) = insert c . patchL d . delete c
patchL (CpyTree d) = \(CCons x xs) -> CCons x . patchL d $ xs
diffL :: (Family f, List f txs, List f tys) => txs -> tys -> EditScriptL f txs tys
diffL x y = getEditScriptL $ diffLMemo x y
data Nil = CNil
data Cons x xs = CCons x xs
class Family f where
decEq :: f tx txs -> f ty tys -> Maybe (tx :=: ty, txs :=: tys)
fields :: f t ts -> t -> Maybe ts
apply :: f t ts -> ts -> t
string :: f t ts -> String
data a :=: b where
Refl :: a :=: a
class (Family f) => Type f t where
constructors :: [Con f t]
data Con :: (* -> * -> *) -> * -> * where
Concr :: (List f ts) => f t ts -> Con f t
Abstr :: (Eq t, List f ts) => (t -> f t ts) -> Con f t
class List f ts where
list :: IsList f ts
data IsList :: (* -> * -> *) -> * -> * where
IsNil :: IsList f Nil
IsCons :: (Type f t) => IsList f ts -> IsList f (Cons t ts)
instance List f Nil where
list = IsNil
instance (Type f t, List f ts) => List f (Cons t ts) where
list = IsCons list
data EditScriptL :: (* -> * -> *) -> * -> * -> * where
Ins :: (Type f t, List f ts, List f tys) => f t ts ->
EditScriptL f txs (Append ts tys) ->
EditScriptL f txs (Cons t tys)
Del :: (Type f t, List f ts, List f txs) => f t ts ->
EditScriptL f (Append ts txs) tys ->
EditScriptL f (Cons t txs) tys
Cpy :: (Type f t, List f ts, List f txs, List f tys) => f t ts ->
EditScriptL f (Append ts txs) (Append ts tys) ->
EditScriptL f (Cons t txs) (Cons t tys)
CpyTree :: (Type f t, List f txs, List f tys) =>
EditScriptL f txs tys ->
EditScriptL f (Cons t txs) (Cons t tys)
End :: EditScriptL f Nil Nil
type family Append txs tys :: *
type instance Append Nil tys = tys
type instance Append (Cons tx txs) tys = Cons tx (Append txs tys)
appendList :: IsList f txs -> IsList f tys -> IsList f (Append txs tys)
appendList IsNil isys = isys
appendList (IsCons isxs) isys = IsCons (appendList isxs isys)
append :: IsList f txs -> IsList f tys -> txs -> tys -> Append txs tys
append IsNil _ CNil ys = ys
append (IsCons isxs) isys (CCons x xs) ys = CCons x (append isxs isys xs ys)
instance Show (EditScriptL f txs tys) where
show (Ins c d) = "Ins " ++ string c ++ " $ " ++ show d
show (Del c d) = "Del " ++ string c ++ " $ " ++ show d
show (Cpy c d) = "Cpy " ++ string c ++ " $ " ++ show d
show (CpyTree d) = "CpyTree" ++ " $ " ++ show d
show End = "End"
delete :: (Type f t, List f ts, List f txs) => f t ts -> Cons t txs -> Append ts txs
delete c (CCons x xs) =
case fields c x of
Nothing -> error "Patching failed"
Just ts -> append (isList c) list ts xs
isList :: (Family f, List f ts) => f t ts -> IsList f ts
isList _ = list
insert :: (Type f t, List f ts, List f txs) => f t ts -> Append ts txs -> Cons t txs
insert c xs = CCons (apply c txs) tys
where (txs, tys) = split (isList c) xs
split :: IsList f txs -> Append txs tys -> (txs, tys)
split IsNil ys = (CNil, ys)
split (IsCons isxs) (CCons x xsys) = let (xs, ys) = split isxs xsys
in (CCons x xs, ys)
matchConstructor :: (Type f t) => t ->
(forall ts. f t ts -> IsList f ts -> ts -> r) -> r
matchConstructor = tryEach constructors
where
tryEach :: (Type f t) => [Con f t] -> t ->
(forall ts. f t ts -> IsList f ts -> ts -> r) -> r
tryEach (Concr c : cs) x k = matchOrRetry c cs x k
tryEach (Abstr c : cs) x k = matchOrRetry (c x) cs x k
tryEach [] _ _ = error "Incorrect Family or Type instance."
matchOrRetry :: (List f ts, Type f t) => f t ts -> [Con f t] -> t ->
(forall ts'. f t ts' -> IsList f ts' -> ts' -> r) -> r
matchOrRetry c cs x k = case fields c x of
Just ts -> k c (isList c) ts
Nothing -> tryEach cs x k
best :: EditScriptL f txs tys -> EditScriptL f txs tys -> EditScriptL f txs tys
best dx dy = bestSteps (steps dx) dx (steps dy) dy
data Nat = Zero | Succ Nat
deriving (Eq, Show)
steps :: EditScriptL f txs tys -> Nat
steps (Ins _ d) = Succ $ steps d
steps (Del _ d) = Succ $ steps d
steps (Cpy _ d) = Succ $ steps d
steps End = Zero
bestSteps :: Nat -> d -> Nat -> d -> d
bestSteps Zero x _ _ = x
bestSteps _ _ Zero y = y
bestSteps (Succ nx) x (Succ ny) y = bestSteps nx x ny y
data RListT :: (* -> * -> *) -> * -> * where
RList :: List f ts => RListT f ts
reify :: IsList f ts -> RListT f ts
reify IsNil = RList
reify (IsCons ists) = case reify ists of
RList -> RList
ins :: (Type f t) => IsList f ts -> IsList f tys ->
f t ts -> EditScriptL f txs (Append ts tys) -> EditScriptL f txs (Cons t tys)
ins ists isys =
case (reify ists, reify isys) of
(RList, RList) -> Ins
del :: (Type f t) => IsList f ts -> IsList f txs ->
f t ts -> EditScriptL f (Append ts txs) tys -> EditScriptL f (Cons t txs) tys
del ists isxs =
case (reify ists, reify isxs) of
(RList, RList) -> Del
cpy :: (Type f t) => IsList f ts -> IsList f txs -> IsList f tys ->
f t ts -> EditScriptL f (Append ts txs) (Append ts tys) ->
EditScriptL f (Cons t txs) (Cons t tys)
cpy ists isxs isys =
case (reify ists, reify isxs, reify isys) of
(RList, RList, RList) -> Cpy
compress :: (Family f) => EditScriptL f txs tys -> EditScriptL f txs tys
compress End = End
compress (Ins c d) = Ins c (compress d)
compress (Del c d) = Del c (compress d)
compress (CpyTree d) = CpyTree (compress d)
compress (Cpy c d) = let d' = compress d in
case copied (isList c) d' of
Just d'' -> CpyTree d''
Nothing -> Cpy c d'
copied :: (Family f) => IsList f ts ->
EditScriptL f (Append ts txs) (Append ts tys) -> Maybe (EditScriptL f txs tys)
copied IsNil d = Just d
copied (IsCons xs) (CpyTree d) = copied xs d
copied (IsCons _) _ = Nothing
data EditScriptLMemo :: (* -> * -> *) -> * -> * -> * where
CC :: (Type f tx, Type f ty, List f txs', List f tys') =>
f tx txs' -> f ty tys' ->
EditScriptL f (Cons tx txs) (Cons ty tys) ->
EditScriptLMemo f (Cons tx txs) (Append tys' tys) ->
EditScriptLMemo f (Append txs' txs) (Cons ty tys) ->
EditScriptLMemo f (Append txs' txs) (Append tys' tys) ->
EditScriptLMemo f (Cons tx txs) (Cons ty tys)
CN :: (Type f tx, List f txs') => f tx txs' ->
EditScriptL f (Cons tx txs) Nil ->
EditScriptLMemo f (Append txs' txs) Nil ->
EditScriptLMemo f (Cons tx txs) Nil
NC :: (Type f ty, List f tys') => f ty tys' ->
EditScriptL f Nil (Cons ty tys) ->
EditScriptLMemo f Nil (Append tys' tys) ->
EditScriptLMemo f Nil (Cons ty tys)
NN :: EditScriptL f Nil Nil ->
EditScriptLMemo f Nil Nil
diffLMemo :: (Family f, List f txs, List f tys) => txs -> tys -> EditScriptLMemo f txs tys
diffLMemo = diffLMemo' list list
diffLMemo' :: (Family f) => forall txs tys. IsList f txs -> IsList f tys ->
txs -> tys -> EditScriptLMemo f txs tys
diffLMemo' IsNil IsNil CNil CNil =
NN End
diffLMemo' (IsCons isxs) IsNil (CCons x xs) CNil =
matchConstructor x
(\ cx isxs' xs' ->
let d = diffLMemo' (appendList isxs' isxs) IsNil
(append isxs' isxs xs' xs) CNil
in cn isxs' isxs cx (del isxs' isxs cx (getEditScriptL d)) d)
diffLMemo' IsNil (IsCons isys) CNil (CCons y ys) =
matchConstructor y
(\ cy isys' ys' ->
let i = diffLMemo' IsNil (appendList isys' isys)
CNil (append isys' isys ys' ys)
in nc isys' isys cy (ins isys' isys cy (getEditScriptL i)) i)
diffLMemo' (IsCons isxs) (IsCons isys) (CCons x xs) (CCons y ys) =
matchConstructor x
(\ cx isxs' xs' ->
matchConstructor y
(\ cy isys' ys' ->
let c = diffLMemo' (appendList isxs' isxs) (appendList isys' isys)
(append isxs' isxs xs' xs) (append isys' isys ys' ys)
d = extendd isys' isys cy c
i = extendi isxs' isxs cx c
in cc isxs' isxs isys' isys cx cy
(bestEditScriptLMemo cx cy isxs' isxs isys' isys i d c) i d c))
getEditScriptL :: EditScriptLMemo f txs tys -> EditScriptL f txs tys
getEditScriptL (CC _ _ d _ _ _) = d
getEditScriptL (CN _ d _) = d
getEditScriptL (NC _ d _) = d
getEditScriptL (NN d) = d
bestEditScriptLMemo :: (Type f tx, Type f ty) => f tx txs' -> f ty tys' ->
IsList f txs' -> IsList f txs -> IsList f tys' -> IsList f tys ->
EditScriptLMemo f (Cons tx txs) (Append tys' tys) ->
EditScriptLMemo f (Append txs' txs) (Cons ty tys) ->
EditScriptLMemo f (Append txs' txs) (Append tys' tys) ->
EditScriptL f (Cons tx txs) (Cons ty tys)
bestEditScriptLMemo cx cy isxs' isxs isys' isys i d c = case decEq cx cy of
Just (Refl, Refl) -> cpy isxs' isxs isys cx (getEditScriptL c)
Nothing -> best (ins isys' isys cy (getEditScriptL i))
(del isxs' isxs cx (getEditScriptL d))
extendd :: (Type f ty) => IsList f tys' -> IsList f tys -> f ty tys' ->
EditScriptLMemo f txs' (Append tys' tys) ->
EditScriptLMemo f txs' (Cons ty tys)
extendd isys' isys cy dt@(NN d) = nc isys' isys cy (ins isys' isys cy d) dt
extendd isys' isys cy dt@(NC _ d _) = nc isys' isys cy (ins isys' isys cy d) dt
extendd isys' isys cy dt@(CN _ _ _) = extendd' isys' isys cy dt
extendd isys' isys cy dt@(CC _ _ _ _ _ _) = extendd' isys' isys cy dt
extendd' :: (Type f ty, Type f tx) => IsList f tys' -> IsList f tys -> f ty tys' ->
EditScriptLMemo f (Cons tx txs) (Append tys' tys) ->
EditScriptLMemo f (Cons tx txs) (Cons ty tys)
extendd' isys' isys cy dt =
extractd dt (\ isxs' isxs cx dt' ->
let i = dt
d = extendd isys' isys cy dt'
c = dt'
in cc isxs' isxs isys' isys cx cy (bestEditScriptLMemo cx cy isxs' isxs isys' isys i d c) i d c)
extendi :: (Type f tx) => IsList f txs' -> IsList f txs -> f tx txs' ->
EditScriptLMemo f (Append txs' txs) tys' ->
EditScriptLMemo f (Cons tx txs) tys'
extendi isxs' isxs cx dt@(NN d) = cn isxs' isxs cx (del isxs' isxs cx d) dt
extendi isxs' isxs cx dt@(CN _ d _) = cn isxs' isxs cx (del isxs' isxs cx d) dt
extendi isxs' isxs cx dt@(NC _ _ _) = extendi' isxs' isxs cx dt
extendi isxs' isxs cx dt@(CC _ _ _ _ _ _) = extendi' isxs' isxs cx dt
extendi' :: (Type f tx, Type f ty) => IsList f txs' -> IsList f txs -> f tx txs' ->
EditScriptLMemo f (Append txs' txs) (Cons ty tys) ->
EditScriptLMemo f (Cons tx txs) (Cons ty tys)
extendi' isxs' isxs cx dt =
extracti dt (\ isys' isys cy dt' ->
let i = extendi isxs' isxs cx dt'
d = dt
c = dt'
in cc isxs' isxs isys' isys cx cy
(bestEditScriptLMemo cx cy isxs' isxs isys' isys i d c)
i d c)
extractd :: (Type f tx) => EditScriptLMemo f (Cons tx txs) tys' ->
(forall txs'. IsList f txs' -> IsList f txs -> f tx txs' ->
EditScriptLMemo f (Append txs' txs) tys' -> r) -> r
extractd (CC c _ d' _ d _) k = k (isList c) (sourceTail d') c d
extractd (CN c d' d) k = k (isList c) (sourceTail d') c d
sourceTail :: EditScriptL f (Cons tx txs) tys -> IsList f txs
sourceTail (Ins _ d) = sourceTail d
sourceTail (Del _ _) = list
sourceTail (Cpy _ _) = list
extracti :: (Type f ty) => EditScriptLMemo f txs' (Cons ty tys) ->
(forall tys'. IsList f tys' -> IsList f tys -> f ty tys' ->
EditScriptLMemo f txs' (Append tys' tys) -> r) -> r
extracti (CC _ c d i _ _) k = k (isList c) (targetTail d) c i
extracti (NC c d i) k = k (isList c) (targetTail d) c i
targetTail :: EditScriptL f txs (Cons ty tys) -> IsList f tys
targetTail (Ins _ _) = list
targetTail (Del _ d) = targetTail d
targetTail (Cpy _ _) = list
nc :: (Type f t) => IsList f ts -> IsList f tys ->
f t ts -> EditScriptL f Nil (Cons t tys) ->
EditScriptLMemo f Nil (Append ts tys) -> EditScriptLMemo f Nil (Cons t tys)
nc ists isys =
case (reify ists, reify isys) of
(RList, RList) -> NC
cn :: (Type f t) => IsList f ts -> IsList f txs ->
f t ts -> EditScriptL f (Cons t txs) Nil ->
EditScriptLMemo f (Append ts txs) Nil -> EditScriptLMemo f (Cons t txs) Nil
cn ists isxs =
case (reify ists, reify isxs) of
(RList, RList) -> CN
cc :: (Type f tx, Type f ty) =>
IsList f txs' -> IsList f txs -> IsList f tys' -> IsList f tys ->
f tx txs' -> f ty tys' -> EditScriptL f (Cons tx txs) (Cons ty tys) ->
EditScriptLMemo f (Cons tx txs) (Append tys' tys) ->
EditScriptLMemo f (Append txs' txs) (Cons ty tys) ->
EditScriptLMemo f (Append txs' txs) (Append tys' tys) ->
EditScriptLMemo f (Cons tx txs) (Cons ty tys)
cc isxs' isxs isys' isys =
case (reify isxs', reify isxs, reify isys', reify isys) of
(RList, RList, RList, RList) -> CC