{# LANGUAGE ViewPatterns #}
{# LANGUAGE PolyKinds #}
{# LANGUAGE FlexibleContexts #}
{# LANGUAGE DataKinds #}
{# LANGUAGE TypeFamilies #}
{# LANGUAGE ConstraintKinds #}
{# LANGUAGE TypeApplications #}
{# LANGUAGE ScopedTypeVariables #}
{# LANGUAGE TypeOperators #}
{# LANGUAGE RankNTypes #}
{# LANGUAGE GADTs #}
module Generics.MRSOP.STDiff.Compute where
import Data.Function (on)
import Data.Ord (comparing)
import Data.List (maximumBy)
import Data.Coerce
import Data.Proxy
import Data.Type.Equality
import Data.Functor.Const
import Generics.MRSOP.Base
import Generics.MRSOP.AG
import qualified Generics.MRSOP.GDiff as GDiff
import Generics.MRSOP.GDiff.Util
import Generics.MRSOP.STDiff.Types
import Data.Maybe (fromJust)
 * Annotating Trees

 $annotating

 First we use /gdiff/ to annotate the source and destination
 forests before translating them to a 'Generics.MRSOP.STDiff.Almu'
 The idea being that the information comming from /gdiff/ is sufficient
 to know which constructors are copies and which have been modified.
 Annotations to be placed throughout the tree.
data Ann = Modify  Copy deriving Show
 Adds an annotated constructor to a product of atoms.
injCofAnn :: GDiff.Cof ki codes a t
> Const ann ix
> PoA ki (AnnFix ki codes (Const ann)) t
> NA ki (AnnFix ki codes (Const ann)) a
injCofAnn (GDiff.ConstrI c _) ann xs = NA_I (AnnFix (coerce ann) $ inj c xs)
injCofAnn (GDiff.ConstrK k) _ _ = NA_K k
 Inserts an annotated constructor at the head of a
 product of atoms.
insCofAnn :: GDiff.Cof ki codes a t
> Const ann ix
> PoA ki (AnnFix ki codes (Const ann)) (t :++: as)
> PoA ki (AnnFix ki codes (Const ann)) (a ': as)
insCofAnn (GDiff.ConstrK k) _ xs = NA_K k :* xs
insCofAnn (GDiff.ConstrI c prf) ann xs =
let (xs0, xs1) = split prf xs
in injCofAnn (GDiff.ConstrI c prf) ann xs0 :* xs1
{
 In Agda, it would be the following. However, I'm not sure
 it is possible to carry around the IsJust constraint in Haskell
 hence, we will be partial instead
 annsource : ∀{txs tys}(xs : ⟦ txs ⟧A*)(p : ES txs tys)
 → (hip : IsJust (applyES p xs))
 → ⟦ txs ⟧Aₐ*

 However, it's morally total if you know beforehand that the
 patch is gonna apply. Which we know by construction everywhere we use this
 , so we can just `fromJust` it where appropriate

 WARNING: Morally dubious, but we know that this edit script was
 generated hte same time as the datatype, so it should never
 fail to apply

 TODO: Actually make it return Maybe and be honest
}
 Annotates the source of an edit script.
annSrc :: (EqHO ki , IsNat ix)
=> Fix ki codes ix  ^
> GDiff.ES ki codes '[ 'I ix] ys
> AnnFix ki codes (Const Ann) ix
annSrc x0 es0 = case annSrc' (NA_I x0 :* Nil) es0 of
(NA_I y :* Nil) > y
where
annSrc' :: EqHO ki
=> PoA ki (Fix ki codes) xs
> GDiff.ES ki codes xs ys
> PoA ki (AnnFix ki codes (Const Ann)) xs
annSrc' _ GDiff.ES0 = Nil
annSrc' Nil _ = Nil
annSrc' xs (GDiff.Ins _ _ es) = annSrc' xs es
annSrc' (x :* xs) (GDiff.Del _ c es) =
let poa = fromJust $ GDiff.matchCof c x
in insCofAnn c (Const Modify) (annSrc' (appendNP poa xs) es)
annSrc' (x :* xs) (GDiff.Cpy _ c es) =
let poa = fromJust $ GDiff.matchCof c x
in insCofAnn c (Const Copy) (annSrc' (appendNP poa xs) es)
 Annotates the destination of an edit script.
annDest :: (EqHO ki , IsNat ix)
=> Fix ki codes ix  ^
> GDiff.ES ki codes xs '[ 'I ix]
> AnnFix ki codes (Const Ann) ix
annDest x0 es0 = case annDest' (NA_I x0 :* Nil) es0 of
(NA_I y :* Nil) > y
where
annDest' :: EqHO ki
=> PoA ki (Fix ki codes) ys
> GDiff.ES ki codes xs ys
> PoA ki (AnnFix ki codes (Const Ann)) ys
annDest' _ GDiff.ES0 = Nil
annDest' Nil _ = Nil
annDest' (x :* xs) (GDiff.Del _ _ es) = annDest' (x :* xs) es
annDest' (x :* xs) (GDiff.Ins _ c es)
= let poa = fromJust $ GDiff.matchCof c x
in insCofAnn c (Const Modify) (annDest' (appendNP poa xs) es)
annDest' (x :* xs) (GDiff.Cpy _ c es) =
let poa = fromJust $ GDiff.matchCof c x
in insCofAnn c (Const Copy) (annDest' (appendNP poa xs) es)
 * Differencing Annotated Trees

 $diffann

 Once we have annotated the trees on the source and destination of the
 edit script, we can easily diff them in the /stdiff/ style.

 ** Stiff Patches

 $stiffpatches

 We call a patch /stiff/ if it has no copies. It is trivial
 to produce sauch a patch given two elements. We simply delete
 the entire source and insert the entire destination.
stiffAlmu :: (TestEquality ki, EqHO ki)
=> Fix ki codes ix  ^
> Fix ki codes iy
> Almu ki codes ix iy
stiffAlmu (Fix rep1) (Fix rep2) = Spn (stiffSpine rep1 rep2)
stiffSpine :: (TestEquality ki, EqHO ki)
=> Rep ki (Fix ki codes) xs  ^
> Rep ki (Fix ki codes) ys
> Spine ki codes xs ys
stiffSpine (sop > Tag c1 p1) (sop > Tag c2 p2) = SChg c1 c2 (stiffAl p1 p2)
stiffAt :: (TestEquality ki, EqHO ki)
=> NA ki (Fix ki codes) x  ^
> NA ki (Fix ki codes) x
> At ki codes x
stiffAt (NA_K x) (NA_K y) = AtSet (Trivial x y)
stiffAt (NA_I x) (NA_I y) = AtFix (stiffAlmu x y)
stiffAl :: (TestEquality ki, EqHO ki)
=> PoA ki (Fix ki codes) xs  ^
> PoA ki (Fix ki codes) ys
> Al ki codes xs ys
stiffAl Nil Nil = A0
stiffAl (x :* xs) Nil = ADel x (stiffAl xs Nil)
stiffAl Nil (y :* ys) = AIns y (stiffAl Nil ys)
stiffAl (x :* xs) (y :* ys) =
case testEquality x y of
Just Refl > AX (stiffAt x y) (stiffAl xs ys)
Nothing > AIns y (ADel x (stiffAl xs ys))
 ** Copy Counting

 $copycounting

 In order to decide which path to follow from the roof to the
 leaves whenver we are faced with a choice, we will precompute
 the amount of copies present in each subtree.
 Algebra for counting copies.
copiesAlgebra :: Const Ann ix  ^
> Rep ki (Const Int) xs
> Const Int ix
copiesAlgebra (Const ann) r
= let inAnn = elimRep (const 0) getConst sum r
in Const $ case ann of
Modify > inAnn
Copy > 1 + inAnn
 Annotates the tree with how many copies are underneath each node
 (inclusive with self)

 > copies Copy = 1 + copies children
 > copies Modify = copies children

countCopies :: IsNat ix
=> AnnFix ki codes (Const Ann) ix  ^
> AnnFix ki codes (Const Int :*: Const Ann) ix
countCopies = synthesizeAnn (\ca r > copiesAlgebra ca (mapRep getFst r) :*: ca)
where
getFst :: (a :*: b) x > a x
getFst (x :*: _) = x
 Returns whether or not a subtree constains any copies.
hasCopies :: AnnFix ki codes (Const Int :*: chi) ix > Bool
hasCopies (AnnFix (Const x :*: _) _) = x > 0
 Easily retrieves annotations
myGetAnn :: (Const Int :*: Const Ann) x > Ann
myGetAnn (_ :*: Const ann) = ann
myGetAnnAt :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) ('I x) > Ann
myGetAnnAt (NA_I (AnnFix ann _)) = myGetAnn ann
 Easily retrieves annotations
myGetCopies :: (Const Int :*: Const Ann) x > Int
myGetCopies (Const copies :*: _) = copies
myForgetAnn :: NA ki (AnnFix ki codes (Const Int :*: Const Ann)) at
> NA ki (Fix ki codes) at
myForgetAnn = mapNA id forgetAnn
 ** Computing the Patch

 $computing

 Given trees annotated with information about each of their constructors
 and how many of those are supposed to be copied, we can finally
 deterministically translate two tress into a patch.
data InsOrDel (ki :: kon > *) (codes :: [[[Atom kon]]]) :: (Nat > Nat > *) > * where
CtxIns :: InsOrDel ki codes (Almu ki codes)
CtxDel :: InsOrDel ki codes (AlmuMin ki codes)
 Finds the element in the @PoA ... xs@ with the most copies
 and diff the given @AnnFix@.

 PRECONDITION: The @PoA .. xs@ must contain at least one tree with
 a copy. Always guard this call with 'hasCopies'


diffCtx :: forall ki codes p ix xs
. (EqHO ki, TestEquality ki, IsNat ix)
=> InsOrDel ki codes p
> AnnFix ki codes (Const Int :*: Const Ann) ix
> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs
> Ctx ki codes p ix xs
diffCtx cid x xs
= let maxIdx = fst $ maximumBy (comparing snd) zipped
zipped = zip [0 .. ] elimmed
elimmed = elimNP (elimNA (const 0) (myGetCopies . getAnn)) xs
in drop' maxIdx xs
where
drop' :: Int
> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) ys
> Ctx ki codes p ix ys
drop' _ Nil = error "unreachable"
drop' 0 (NA_I y :* ys) =
case cid of
CtxIns > H (diffAlmu x y) (mapNP myForgetAnn ys)
CtxDel > H (AlmuMin (diffAlmu y x)) (mapNP myForgetAnn ys)
drop' n (y :* ys) = T (myForgetAnn y) (drop' (n  1) ys)
  Takes two annotated trees, and produces a patch
diffAlmu :: forall ki codes ix iy
. (EqHO ki, IsNat ix, IsNat iy, TestEquality ki)
=> AnnFix ki codes (Const Int :*: Const Ann) ix  ^
> AnnFix ki codes (Const Int :*: Const Ann) iy
> Almu ki codes ix iy
diffAlmu x@(AnnFix ann1 rep1) y@(AnnFix ann2 rep2) =
case (myGetAnn ann1, myGetAnn ann2) of
(Copy, Copy) > Spn (diffSpine (getSNat $ Proxy @ix) (getSNat $ Proxy @iy) rep1 rep2)
(Copy, Modify) >
if hasCopies y then diffIns x rep2 else stiffAlmu (forgetAnn x) (forgetAnn y)
(Modify, Copy) >
if hasCopies x then diffDel rep1 y else stiffAlmu (forgetAnn x) (forgetAnn y)
(Modify, Modify) >
if hasCopies x then diffDel rep1 y else stiffAlmu (forgetAnn x) (forgetAnn y)
where
diffIns :: AnnFix ki codes (Const Int :*: Const Ann) ix
> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup iy codes)
> Almu ki codes ix iy
diffIns x1 rep = case sop rep of Tag c xs > Ins c (diffCtx CtxIns x1 xs)
diffDel :: Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup ix codes)
> AnnFix ki codes (Const Int :*: Const Ann) iy
> Almu ki codes ix iy
diffDel rep x1 = case sop rep of Tag c xs > Del c (diffCtx CtxDel x1 xs)
  Takes two annotated 'Rep's, and produces a patch
diffSpine :: forall ki codes ix iy
. (TestEquality ki, EqHO ki, IsNat ix, IsNat iy)
=> SNat ix  ^ We need these to identify the mutrec family
> SNat iy
> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup ix codes)
> Rep ki (AnnFix ki codes (Const Int :*: Const Ann)) (Lkup iy codes)
> Spine ki codes (Lkup ix codes) (Lkup iy codes)
diffSpine six siy s1@(sop > Tag c1 p1) s2@(sop > Tag c2 p2) =
case testEquality six siy of
Just Refl >
if (eqHO `on` mapRep forgetAnn) s1 s2
then Scp
else case testEquality c1 c2 of
Just Refl >
SCns c1 (mapNP (\(a :*: b) > diffAt a b) (zipNP p1 p2))
Nothing > SChg c1 c2 (diffAl p1 p2)
Nothing > SChg c1 c2 (diffAl p1 p2)
diffAl :: forall ki codes xs ys
. (EqHO ki, TestEquality ki)
=> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) xs  ^
> PoA ki (AnnFix ki codes (Const Int :*: Const Ann)) ys
> Al ki codes xs ys
diffAl Nil Nil = A0
diffAl Nil (y :* ys) = AIns (mapNA id forgetAnn y) (diffAl Nil ys)
diffAl (x :* xs) Nil = ADel (mapNA id forgetAnn x) (diffAl xs Nil)
diffAl (x@(NA_K k1) :* xs) (y@(NA_K k2) :* ys) =
case testEquality k1 k2 of
Just Refl > AX (diffAt x y) (diffAl xs ys)
Nothing > AIns (mapNA id forgetAnn y) (ADel (mapNA id forgetAnn x) (diffAl xs ys))
diffAl (x@(NA_K _) :* xs) (y@(NA_I _) :* ys) =
case myGetAnnAt y of
Modify > AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
Copy > ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
diffAl (x@(NA_I _) :* xs) (y@(NA_K _) :* ys) =
case myGetAnnAt x of
Modify > ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
Copy > AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
diffAl (x@(NA_I _) :* xs) (y@(NA_I _) :* ys) =
case (myGetAnnAt x, myGetAnnAt y) of
(Modify, _) > ADel (mapNA id forgetAnn x) (diffAl xs (y :* ys))
(Copy, Modify) > AIns (mapNA id forgetAnn y) (diffAl (x :* xs) ys)
(Copy, Copy) >
case testEquality x y of
Just Refl > AX (diffAt x y) (diffAl xs ys)
 NOTE we added this case
Nothing > AIns (mapNA id forgetAnn y) (ADel (mapNA id forgetAnn x) (diffAl xs ys))
diffAt :: (EqHO ki, TestEquality ki)
=> NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a  ^
> NA ki (AnnFix ki codes (Const Int :*: Const Ann)) a
> At ki codes a
diffAt (NA_K x) (NA_K y) = AtSet (Trivial x y)
diffAt (NA_I x) (NA_I y) = AtFix $ diffAlmu x y
 The interface function which witnesses thecomplete pipeline.
 its implementation is straightforward:

 > diff x y = let es = GDiff.diff' x y
 > ax = countCopies $ annSrc x es
 > ay = countCopies $ annDest y es
 > in diffAlmu ax ay

diff :: (EqHO ki , TestEquality ki , IsNat ix)
=> Fix ki codes ix  ^
> Fix ki codes ix
> Almu ki codes ix ix
diff x y = let es = GDiff.diff' x y
ax = countCopies $ annSrc x es
ay = countCopies $ annDest y es
in diffAlmu ax ay