generics-mrsop-gdiff 0.0.1 → 0.0.2

raw patch · 8 files changed

+983/−44 lines, 8 filesdep ~basedep ~generics-mrsopPVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base, generics-mrsop

API changes (from Hackage documentation)

Files

• generics-mrsop-gdiff.cabal +39/−34
• src/Generics/MRSOP/GDiff.hs +4/−5
• src/Generics/MRSOP/GDiff/Util.hs +5/−5
• src/Generics/MRSOP/STDiff.hs +104/−0
• src/Generics/MRSOP/STDiff/Compute.hs +365/−0
• src/Generics/MRSOP/STDiff/Enum.hs +94/−0
• src/Generics/MRSOP/STDiff/Merge.hs +187/−0
• src/Generics/MRSOP/STDiff/Types.hs +185/−0

@@ -1,37 +1,42 @@-name:                generics-mrsop-gdiff+-- This file has been generated from package.yaml by hpack version 0.28.2.+--+-- see: https://github.com/sol/hpack+--+-- hash: 0efe06cb6c261c979c1bb69945d291c4d6d3d9eae84840801fabae96a8592ee2 --- The package version.  See the Haskell package versioning policy (PVP) --- for standards guiding when and how versions should be incremented.--- https://wiki.haskell.org/Package_versioning_policy--- PVP summary:      +------- breaking API changes---                   | +----- non-breaking API additions---                   | | +--- code changes with no API change-version:             0.0.1-license:             BSD3-license-file:        LICENSE-synopsis:            Reimplementation of the `gdiff` algorithm for `generics-mrsop`-description:         Here we port the gdiff algorithm and library to work over the generics-mrsop, enabling code that relies on the later library to access the gdiff algorithm. -author:              Arian van Putten and Victor Miraldo-maintainer:          arian.vanputten@gmail.com v.cacciarimiraldo@gmail.com-category:            Generics-build-type:          Simple-cabal-version:       >=1.10+name:           generics-mrsop-gdiff+version:        0.0.2+synopsis:       Reimplementation of the gdiff algorithm for generics-mrsop+description:    Here we port the gdiff algorithm and library to work over the generics-mrsop, enabling code that relies on the later library to access the gdiff algorithm. Moreover, we also bring in the utilities for converting a gdiff patch into a more structured version, facilitating merging. For some literature on the topic check Arian's MSc thesis at <https://dspace.library.uu.nl/handle/1874/380853> or our TyDe 2017 paper at <https://victorcmiraldo.github.io/data/tyde2017.pdf>.+category:       Generics+homepage:       https://github.com/VictorCMiraldo/generics-mrsop-gdiff#readme+bug-reports:    https://github.com/VictorCMiraldo/generics-mrsop-gdiff/issues+author:         Arian van Putten and Victor Miraldo+maintainer:     Victor Miraldo <v.cacciarimiraldo@gmail.com>+license:        BSD3+license-file:   LICENSE+build-type:     Simple+cabal-version:  >= 1.10 -library-  ghc-options:-    -O2 -Wall+source-repository head+  type: git+  location: https://github.com/VictorCMiraldo/generics-mrsop-gdiff -  exposed-modules: -    Generics.MRSOP.GDiff-    Generics.MRSOP.GDiff.Util- -  -- Other library packages from which modules are imported.-  build-depends:       base < 5,-                       generics-mrsop >= 2.2.0-  -  -- Directories containing source files.-  hs-source-dirs:      src-  -  -- Base language which the package is written in.-  default-language:    Haskell2010-  +library+  exposed-modules:+      Generics.MRSOP.GDiff+      Generics.MRSOP.GDiff.Util+      Generics.MRSOP.STDiff+      Generics.MRSOP.STDiff.Compute+      Generics.MRSOP.STDiff.Enum+      Generics.MRSOP.STDiff.Merge+      Generics.MRSOP.STDiff.Types+  other-modules:+      Paths_generics_mrsop_gdiff+  hs-source-dirs:+      src/+  ghc-options: -Wall+  build-depends:+      base >=4.9 && <5+    , generics-mrsop >=2.3.0+  default-language: Haskell2010

@@ -1,4 +1,3 @@-{-# LANGUAGE QuantifiedConstraints #-} {-# LANGUAGE PolyKinds            #-} {-# LANGUAGE FlexibleContexts     #-} {-# LANGUAGE DataKinds            #-}@@ -17,7 +16,7 @@ -- module Generics.MRSOP.GDiff   ( Cof(..)-  , cofIdx , cofWitnessI , cofHeq+  , cofIdx , cofWitnessI , cofHeq , matchCof   , ES(..)   , apply, apply' , applyES   , diff , diff'@@ -71,7 +70,7 @@ cofHeq (ConstrK x) (ConstrK y) =   case testEquality x y of     Just Refl ->-      if x == y+      if eqHO x y         then Just (Refl, Refl)         else Nothing     Nothing -> Nothing@@ -255,7 +254,7 @@          -> NA ki (Fix ki codes) a          -> Maybe (PoA ki (Fix ki codes) t) matchCof (ConstrI c1 _) (NA_I (Fix x)) = match c1 x-matchCof (ConstrK k) (NA_K k2) = guard (k == k2) >> Just Nil+matchCof (ConstrK k) (NA_K k2) = guard (eqHO k k2) >> Just Nil  -- we need to give Haskell a bit of a hint that Tyof codes c reduces to an IsList -- insCof is also really the only place where we _need_ IsList I think@@ -328,7 +327,7 @@ -- hence, we can not get the datatype info showCof :: forall ki fam codes a c.      (HasDatatypeInfo ki fam codes, ShowHO ki) => Cof ki codes a c -> String-showCof (ConstrK k) = show k+showCof (ConstrK k) = showHO k showCof x@(ConstrI c _) = constructorName . constrInfoLkup c $ datatypeInfo (Proxy @fam) (cofIdx x)  instance (HasDatatypeInfo ki fam codes, ShowHO ki) =>

@@ -1,9 +1,9 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators   #-}+{-# LANGUAGE TypeFamilies    #-}+{-# LANGUAGE DataKinds       #-}+{-# LANGUAGE GADTs           #-} {-# LANGUAGE ConstraintKinds #-}-{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE PolyKinds       #-}  -- | For the lack of a better name, here we put random stuff module Generics.MRSOP.GDiff.Util where

@@ -0,0 +1,104 @@+{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GADTs                 #-}+module Generics.MRSOP.STDiff+  ( module Generics.MRSOP.STDiff.Types+  , apply , merge , diff+  ) where++import Data.Proxy+import Data.Type.Equality hiding (apply)+import Control.Monad+import Generics.MRSOP.Base++import Generics.MRSOP.STDiff.Types+import Generics.MRSOP.STDiff.Merge+import Generics.MRSOP.STDiff.Compute+++applyAt :: EqHO ki+        => (At ki codes :*: NA ki (Fix ki codes)) a+        -> Either String (NA ki (Fix ki codes) a)+applyAt (AtSet (Trivial a' b) :*: NA_K a)  +  | eqHO a' b  = pure (NA_K a)+  | eqHO a' a  = pure (NA_K b)+  | otherwise = Left "atom"+applyAt (AtFix x :*: NA_I x') = NA_I <$> applyAlmu x x'++applyAl+  :: EqHO ki+  => Al ki codes xs ys+  -> PoA ki (Fix ki codes) xs+  -> Either String (PoA ki (Fix ki codes) ys)+applyAl A0 Nil = return Nil+applyAl (AX dx dxs) (x :* xs) =+  (:*) <$> applyAt (dx :*: x) <*> applyAl dxs xs+applyAl (AIns x dxs) xs =+  (x :*) <$> applyAl dxs xs +applyAl (ADel x dxs) (x' :* xs) =+  if eqHO x x' then applyAl dxs xs else Left "al del"+  -- applyAl dxs xs++testEquality' :: (TestEquality f)+              => f a -> f b -> Either String (a :~: b)+testEquality' x y = case testEquality x y of+  Just r -> Right r+  Nothing -> Left "err"++applySpine +  :: EqHO ki+  => SNat ix+  -> SNat iy+  -> Spine ki codes (Lkup ix codes) (Lkup iy codes)+  -> Rep ki (Fix ki codes) (Lkup ix codes)+  -> Either String (Rep ki (Fix ki codes) (Lkup iy codes))+applySpine _ _ Scp x = return x+applySpine ix iy (SCns c1 dxs) (sop -> Tag c2 xs) =  do+  Refl <- testEquality' ix iy+  Refl <- testEquality' c1 c2+  inj c2 <$> (mapNPM applyAt (zipNP dxs xs))+applySpine _ _ (SChg c1 c2 al) (sop -> Tag c3 xs) = do+  Refl <- testEquality' c1 c3+  inj c2 <$> applyAl al xs++insCtx+  :: (IsNat ix, EqHO ki)+  => InsCtx ki codes ix xs+  -> Fix ki codes ix+  -> Either String (PoA ki (Fix ki codes) xs)+insCtx (H x x2) x1 = (\xi -> NA_I xi :* x2) <$> applyAlmu x x1+insCtx (T x x2) x1 = (x :*) <$> insCtx x2 x1++delCtx+  :: (EqHO ki, IsNat ix)+  => DelCtx ki codes ix xs+  -> PoA ki (Fix ki codes) xs+  -> Either String (Fix ki codes ix)+delCtx (H spu _) (NA_I x :* _) = applyAlmu (unAlmuMin spu) x+delCtx (T _ al)  (_ :* p)      = delCtx al p++applyAlmu +  :: forall ki codes ix iy. (IsNat ix, IsNat iy, EqHO ki)+  => Almu ki codes ix iy+  -> Fix ki codes ix+  -> Either String (Fix ki codes iy)+applyAlmu (Spn spine) (Fix rep) = Fix <$> applySpine (getSNat (Proxy @ix)) (getSNat (Proxy @iy)) spine rep+applyAlmu (Ins c ctx) f@(Fix _) = Fix . inj c <$> insCtx ctx f+applyAlmu (Del c ctx) (Fix rep) = delCtx ctx <=< m2e . match c $ rep+  where+    m2e Nothing  = Left (show "del")+    m2e (Just r) = Right r++-- |Applies a patch to an element+apply :: forall ki codes ix iy+       . (IsNat ix, IsNat iy, EqHO ki)+      => Almu ki codes ix iy+      -> Fix ki codes ix+      -> Maybe (Fix ki codes iy)+apply almu x = case applyAlmu almu x of+                 Left  _ -> Nothing+                 Right y -> Just y

@@ -0,0 +1,365 @@+{-# 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+ -  ann-source : ∀{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 pre-compute+-- 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+

@@ -0,0 +1,94 @@+{-# LANGUAGE ViewPatterns          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE GADTs                 #-}+module Generics.MRSOP.STDiff.Enum (enumAlmu) where++import Control.Monad+import Control.Applicative+import Data.Type.Equality++import Generics.MRSOP.Base+import Generics.MRSOP.STDiff.Types++enumAt :: (MonadPlus m , TestEquality ki , EqHO ki)+       => NA ki (Fix ki codes) at+       -> NA ki (Fix ki codes) at+       -> m (At ki codes at)+enumAt (NA_I x) (NA_I y) = AtFix <$> enumAlmu x y+enumAt (NA_K x) (NA_K y) = return $ AtSet (Trivial x y)++enumAl :: (MonadPlus m , TestEquality ki , EqHO ki)+       => PoA ki (Fix ki codes) p1+       -> PoA ki (Fix ki codes) p2+       -> m (Al ki codes p1 p2)+enumAl Nil Nil = return A0+enumAl (x :* xs) Nil = ADel x <$> enumAl xs Nil+enumAl Nil (y :* ys) = AIns y <$> enumAl Nil ys+enumAl (x :* xs) (y :* ys)+  =     (ADel x <$> enumAl xs (y :* ys))+    <|> (AIns y <$> enumAl (x :* xs) ys)+    <|> case testEquality x y of+          Just Refl -> AX <$> (enumAt x y) <*> enumAl xs ys+          Nothing   -> mzero++enumSpn :: (MonadPlus m , TestEquality ki , EqHO ki)+        => SNat ix -> SNat iy+        -> Rep ki (Fix ki codes) (Lkup ix codes)+        -> Rep ki (Fix ki codes) (Lkup iy codes)+        -> m (Spine ki codes (Lkup ix codes) (Lkup iy codes))+enumSpn six siy (sop -> Tag cx px) (sop -> Tag cy py)+  = case testEquality six siy of+      Nothing -> SChg cx cy <$> enumAl px py+      Just Refl -> +        case testEquality cx cy of+           Nothing   -> SChg cx cy <$> enumAl px py+           Just Refl -> if eqHO px py+                        then return Scp+                        else SCns cx <$> mapNPM (uncurry' enumAt) (zipNP px py)++enumDelCtx :: forall m ki codes iy prod+            . (MonadPlus m , TestEquality ki , EqHO ki , IsNat iy)+           => PoA ki (Fix ki codes) prod+           -> Fix ki codes iy+           -> m (DelCtx ki codes iy prod)+enumDelCtx Nil            _ = mzero+enumDelCtx (NA_K x :* xs) f = T (NA_K x) <$> enumDelCtx xs f+enumDelCtx (NA_I x :* xs) f+  = (flip H xs . AlmuMin) <$> enumAlmu x f+    <|> T (NA_I x) <$> enumDelCtx xs f++enumInsCtx :: forall m ki codes iy prod+            . (MonadPlus m , TestEquality ki , EqHO ki , IsNat iy)+           => Fix ki codes iy+           -> PoA ki (Fix ki codes) prod+           -> m (InsCtx ki codes iy prod)+enumInsCtx _ Nil            = mzero+enumInsCtx f (NA_K x :* xs) = T (NA_K x) <$> enumInsCtx f xs+enumInsCtx f (NA_I x :* xs) +  = (flip H xs) <$> enumAlmu f x+    <|> T (NA_I x) <$> enumInsCtx f xs +    +-- |Enumerates all possible patches that transform a value into another+-- on a @MonadPlus@ instance; /WARNING: this function has impractical runtime performance and should not be used!!/+enumAlmu :: forall m ki codes ix iy+          . (MonadPlus m , TestEquality ki , EqHO ki , IsNat ix , IsNat iy)+         => Fix ki codes ix+         -> Fix ki codes iy+         -> m (Almu ki codes ix iy)+enumAlmu x y+  =    enumDel (sop $ unFix x) y+   <|> enumIns x (sop $ unFix y)+   <|> Spn <$> enumSpn (snatFixIdx x) (snatFixIdx y) (unFix x) (unFix y)+  where+    enumDel :: View ki (Fix ki codes) (Lkup ix codes)+            -> Fix ki codes iy+            -> m (Almu ki codes ix iy)+    enumDel (Tag c p) y0 = Del c <$> enumDelCtx p y0++    enumIns :: Fix ki codes ix+            -> View ki (Fix ki codes) (Lkup iy codes)+            -> m (Almu ki codes ix iy)+    enumIns x0 (Tag c p) = Ins c <$> enumInsCtx x0 p

@@ -0,0 +1,187 @@+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE GADTs                 #-}+{-# LANGUAGE PolyKinds             #-}+module Generics.MRSOP.STDiff.Merge (merge) where++import Data.Proxy+import Data.Type.Equality+import Control.Monad (guard)++import Generics.MRSOP.Base++import Generics.MRSOP.STDiff.Types++mergeAt :: EqHO ki+        => At ki codes a+        -> At ki codes a+        -> Maybe (At ki codes a)+mergeAt  (AtSet (Trivial k1 k2)) (AtSet (Trivial k3 k4)) = +   if eqHO k1 k2+   then pure $ AtSet $ Trivial k3 k4+   else if eqHO k3 k4+   then pure $ AtSet $ Trivial k3 k4+   else Nothing+mergeAt (AtFix x) (AtFix y) = AtFix <$> mergeAlmu x y++mergeAtAl :: EqHO ki+          => NP (At ki codes) xs+          -> Al ki codes xs ys+          -> Maybe (Al ki codes xs ys)+mergeAtAl Nil A0 = pure A0+mergeAtAl xs (AIns at al) = AIns at <$> mergeAtAl xs al+mergeAtAl (x :* xs) (ADel at al)+  | identityAt x = ADel at <$> mergeAtAl xs al+  | otherwise    = Nothing+mergeAtAl (x :* xs) (AX at al) = AX <$> (mergeAt x at)  <*> mergeAtAl xs al++identityAt :: (EqHO ki) => At ki codes a -> Bool+identityAt (AtFix (Spn Scp)) = True+identityAt (AtSet (Trivial k1 k2)) = eqHO k1 k2+identityAt _ = False++makeIdAt :: NA ki (Fix ki codes) a -> At ki codes a+makeIdAt (NA_I _) = AtFix (Spn Scp)+makeIdAt (NA_K k) = AtSet (Trivial k k)++mergeAlAt :: EqHO ki+          => Al ki codes xs ys+          -> NP (At ki codes) xs+          -> Maybe (NP (At ki codes) ys)+mergeAlAt A0 Nil = pure Nil+mergeAlAt (AIns at al) xs = (makeIdAt at :*) <$> mergeAlAt al xs+mergeAlAt (ADel _  al) (x :* xs)+  | identityAt x = mergeAlAt al xs+  | otherwise    = Nothing+mergeAlAt (AX a al)   (x :* xs) = (:*) <$> mergeAt a x <*> mergeAlAt al xs+++mergeAts :: EqHO ki+         => NP (At ki codes) xs+         -> NP (At ki codes) xs+         -> Maybe (NP (At ki codes) xs)+mergeAts Nil Nil = pure Nil+mergeAts (x :* xs) (y :* ys) = (:*) <$> mergeAt x y <*> mergeAts xs ys++mergeSpine :: EqHO ki+           => SNat ix+           -> SNat iy+           -> Spine ki codes (Lkup ix codes) (Lkup iy codes)+           -> Spine ki codes (Lkup ix codes) (Lkup iy codes)+           -> Maybe (Spine ki codes (Lkup ix codes) (Lkup iy codes))+mergeSpine _ _ Scp s = pure s+mergeSpine _ _ _ Scp = pure Scp+mergeSpine _ _ (SCns cx xs) (SCns cy ys) = do+  Refl <- testEquality cx cy+  SCns cx <$> mergeAts xs ys+mergeSpine _ _ (SCns cx xs) (SChg cy cz al) = do+  Refl <- testEquality cx cy+  SChg cy cz <$> mergeAtAl xs al+mergeSpine ix iy (SChg cx cy al) (SCns cz zs) = do+  Refl <- testEquality ix iy+  Refl <- testEquality cx cz+  SCns cy <$> mergeAlAt al zs+mergeSpine _ _ SChg{} SChg{} = Nothing++mergeCtxAt :: forall ki codes ix iy xs+            . (EqHO ki, IsNat ix, IsNat iy) +           => DelCtx ki codes iy xs+           -> NP (At ki codes) xs+           -> Maybe (Almu ki codes ix iy)+mergeCtxAt (H (AlmuMin almu') _) (AtFix almu :* xs) = do+  Refl <- testEquality (almuDest almu) (almuDest almu')+  x <- mergeAlmu almu' almu+  Refl <- testEquality (almuSrc x) (getSNat (Proxy @ix))+  guard (and $ elimNP identityAt xs)+  pure x+mergeCtxAt (T _ ctx) (x :* xs) = do+  guard (identityAt x)+  mergeCtxAt ctx xs++mergeAtCtx :: (EqHO ki, IsNat iy)+           => NP (At ki codes) xs+           -> DelCtx ki codes iy xs+           -> Maybe (DelCtx ki codes iy xs)+mergeAtCtx (AtFix almu :* xs) (H (AlmuMin almu') rest) = do+  Refl <- testEquality (almuDest almu) (almuDest almu')+  almu'' <- mergeAlmu almu almu'+  guard (and $ elimNP identityAt xs)+  pure $ H  (AlmuMin almu'') rest+mergeAtCtx (x :* xs) (T a  ctx) = do+   guard (identityAt x)+   T a  <$> mergeAtCtx xs ctx+mergeAtCtx Nil _ = error "unreachable" -- check x's type to be sure!++almuDest :: forall ix iy ki codes. IsNat iy => Almu ki codes ix iy -> SNat iy+almuDest _ = getSNat (Proxy @iy)++almuSrc :: forall ix iy ki codes. IsNat ix => Almu ki codes ix iy -> SNat ix+almuSrc _ = getSNat (Proxy @ix)++mergeCtxAlmu :: (EqHO ki, IsNat ix )+             => InsCtx ki codes ix xs+             -> Almu ki codes ix ix+             -> Maybe (NP (At ki codes) xs)+mergeCtxAlmu (H almu' rest) almu = do +  Refl <- testEquality (almuDest almu) (almuDest almu')+  x <- AtFix <$> mergeAlmu almu' almu+  pure $ x :* mapNP makeIdAt rest+mergeCtxAlmu (T a    ctx) almu = +  (makeIdAt a :*) <$> mergeCtxAlmu ctx almu++mergeAlmuCtx :: (EqHO ki, IsNat ix)+             => Almu ki codes ix ix+             -> InsCtx ki codes ix xs+             -> Maybe (InsCtx ki codes ix xs)+mergeAlmuCtx almu (H almu' rest) = do+  Refl <- testEquality (almuDest almu) (almuDest almu')+  almu'' <- mergeAlmu almu almu'+  pure (H almu'' rest)+mergeAlmuCtx almu (T a ctx) = T a <$> mergeAlmuCtx almu ctx++mergeAlmu :: forall ki codes ix iy+           . (EqHO ki, IsNat ix, IsNat iy)+          => Almu ki codes ix iy+          -> Almu ki codes ix iy+          -> Maybe (Almu ki codes ix iy)+mergeAlmu (Ins _ _) (Ins _ _) = Nothing+mergeAlmu (Ins c1 s1) (Spn s2) =  do+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))+  Spn . SCns c1 <$> mergeCtxAlmu s1 (Spn s2)+mergeAlmu (Ins c1 s1) (Del c2 s2) = do+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))+  Spn . SCns c1 <$> mergeCtxAlmu s1 (Del c2 s2)+mergeAlmu (Spn s1) (Ins c2 s2) = do+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))+  Ins c2 <$> (mergeAlmuCtx (Spn s1) s2)+mergeAlmu (Del c1 s1) (Ins c2 s2) = do+  Refl <- testEquality (getSNat (Proxy @ix)) (getSNat (Proxy @iy))+  Ins c2 <$> (mergeAlmuCtx (Del c1 s1) s2)++mergeAlmu (Spn s1) (Spn s2) = Spn <$> mergeSpine (getSNat (Proxy @ix)) (getSNat (Proxy @iy)) s1 s2+mergeAlmu (Spn Scp) (Del c2 s2) = pure $ Del c2 s2+mergeAlmu (Spn (SCns c1 at1)) (Del c2 s2) = do+  +  Refl <- testEquality c1 c2+  Del c1 <$> mergeAtCtx at1 s2+mergeAlmu (Spn (SChg _ _ _)) (Del _ _) = Nothing+mergeAlmu (Del _ _) (Spn Scp) = pure $ Spn Scp+mergeAlmu (Del c1 s1) (Spn (SCns c2 at2)) = do+  Refl <- testEquality c1 c2+  mergeCtxAt s1 at2+mergeAlmu (Del _ _) (Spn (SChg _ _ _)) = Nothing+mergeAlmu (Del _ _) (Del _ _) = Nothing++-- |Merges two patches in the /stdiff/ style. Satisfies the following+-- postcondition:+--+-- > if merge p q == Just pq && merge q p == Just qp+-- > then apply pq . q == apply qp . p+--+merge :: forall ki codes ix+       . (EqHO ki, IsNat ix)+      => Almu ki codes ix ix+      -> Almu ki codes ix ix+      -> Maybe (Almu ki codes ix ix)+merge = mergeAlmu

@@ -0,0 +1,185 @@+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE GADTs                 #-}+module Generics.MRSOP.STDiff.Types where++import Generics.MRSOP.Base++-- * Functorial Changes+--+-- $functorialchanges+--+-- Represents changes on the /first layer/ of two values of+-- mutually recursive families. For a more in-depth explanation+-- of the datatypes and their meaning we refer the interested reader+-- to the relevant literature:+--+--  - Miraldo, Dagand and Swierstra, TyDe 2017 <https://victorcmiraldo.github.io/data/tyde2017.pdf pdf>+--  - van Putten, MSc thesis <https://dspace.library.uu.nl/handle/1874/380853>+--++-- |Represents a change between two opaque values. When they+-- are equal represents a copy.+data TrivialK (ki :: kon -> *) :: kon -> * where+  Trivial :: ki kon -> ki kon -> TrivialK ki kon ++-- |Represents a change between two atoms, where an atom is+-- either a recursive or an opaque value.+data At (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Atom kon -> * where+  AtSet :: TrivialK ki kon                   -> At ki codes ('K kon)+  AtFix :: (IsNat ix) => Almu ki codes ix ix -> At ki codes ('I ix)++-- |Represents an alignment between two product of atoms.+data Al (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [Atom kon] -> [Atom kon] -> * where+  A0 :: Al ki codes '[] '[]+  AX :: At ki codes x -> Al ki codes xs ys -> Al ki codes (x ': xs)  (x ': ys)+  ADel :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes (x ': xs) ys+  AIns :: NA ki (Fix ki codes) x -> Al ki codes xs ys -> Al ki codes xs (x ': ys)++-- |Represents a change at the coproduct structure.+data Spine (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: [[Atom kon]] -> [[Atom kon]] -> * where+  Scp  :: Spine ki codes s1 s1+  SCns :: Constr s1 c1 +       -> NP (At ki codes) (Lkup c1 s1)+       -> Spine ki codes s1 s1+  SChg :: Constr s1 c1+       -> Constr s2 c2+       -> Al ki codes (Lkup c1 s1) (Lkup c2 s2)+       -> Spine ki codes s1 s2++-- * Fixpoint Changes+--+-- $fixpointchanges+--+-- The next datatypes represent a sequence of 'Spine', 'Al' and 'At' assembled+-- coupled with operators to describe changes in the recursive structure such+-- as inserting and deleting constructors.+++-- |Represents a /one-hole context/ over a @NP (NA ki (fix ki codes)) xs@ where+-- the hole is in a distinguished element indexed by @'I ix@ and is filled+-- with applying @p@ to the relevant indexes.+data Ctx (ki :: kon -> *) (codes :: [[[Atom kon]]]) (p :: Nat -> Nat -> *)+         (ix :: Nat) :: [Atom kon] -> * where+  H :: IsNat iy+    => p ix iy+    -> PoA ki (Fix ki codes) xs+    -> Ctx ki codes p ix ('I iy ': xs)+  T :: NA ki (Fix ki codes) a+    -> Ctx ki codes p ix xs+    -> Ctx ki codes p ix (a ': xs)++-- |Simple synonym for contexts.+type InsCtx ki codes ix xs = Ctx ki codes (Almu ki codes) ix xs++-- |A deletion context needs to swap the indexes in the hole, hence+-- we use a newtype for that.+type DelCtx ki codes ix xs = Ctx ki codes (AlmuMin ki codes) ix xs++-- |The newtype used to swap the indexes to |Almu|.+newtype AlmuMin ki codes ix iy = AlmuMin  { unAlmuMin :: Almu ki codes iy ix }++-- |Represent recursive spines.+data Almu (ki :: kon -> *) (codes :: [[[Atom kon]]]) :: Nat -> Nat -> * where+  Spn :: Spine ki codes (Lkup ix codes) (Lkup iy codes) -> Almu ki codes ix iy+  Ins :: Constr (Lkup iy codes) c+      -> InsCtx ki codes ix (Lkup c (Lkup iy codes)) -- its an ix with an iy typed-hoed+      -> Almu ki codes ix iy+  Del :: IsNat iy+      => Constr (Lkup ix codes) c+      -> DelCtx ki codes iy (Lkup c (Lkup ix codes))+      -> Almu ki codes ix iy++{-++{-+instance (ShowHO ki) => Show (At ki codes at) where+  show (AtSet t) = show t+  show (AtFix a) = a++instance ShowHO ki => Show (TrivialK ki x) where+  show (Trivial x y) = show x ++ "|" ++ show y+++-}  ++++{-+instance (HasDatatypeInfo ki fam codes, Show1 ki) => Show (Al ki codes xs ys) where+  show A0 = "A0"+  show (AX x xs) = "(AX " ++ show1 x  ++ " " ++ show xs  ++ ")"+  show (ADel x xs) = "(ADel " ++ show x  ++ " " ++ show xs  ++ ")"+  show (AIns x xs) = "(AIns " ++ show x  ++ " " ++ show xs  ++ ")"+-}++{-+instance (IsNat ix,IsNat iy, HasDatatypeInfo ki fam codes, Show1 ki) => Show (AlmuMin ki codes ix iy) where+  show (AlmuMin x) = show x+-}++-- | An NP p xs, but there exists an x in xs such that h x+--+-- Note that:  NP p xs <=> Ctx' p p xs+--+-- and that the list is never empty, because it contains at+-- least the pointed element+--+++instance (IsNat ix, HasDatatypeInfo ki fam codes, Show1 ki) => Show (InsCtx ki codes ix xs) where+  show (H p poa) = "(H " ++ show p ++ " " ++ show poa ++ ")"+  show (T n c)   = "(T " ++ show n  ++ " " ++ show c ++ ")"+instance (IsNat ix, HasDatatypeInfo ki fam codes, Show1 ki) => Show (DelCtx ki codes ix xs) where+  show (H p poa) = "(H " ++ show p ++ " " ++ show poa ++ ")"+  show (T n c)   = "(T " ++ show n  ++ " " ++ show c ++ ")"+++  -- TODO ins del+++instance forall ki fam codes ix iy. (IsNat ix, IsNat iy, Show1 ki, HasDatatypeInfo ki fam codes) => Show (Almu ki codes ix iy) where+  show (Spn s) = "(Spn " ++ showSpine (getSNat @ix Proxy) (getSNat @iy Proxy) s ++ ")"+  show (Ins c ic) = "(Ins " ++ showC c ++ " " ++ show ic ++ ")"+    where showC c = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) (getSNat @iy Proxy))+  show (Del c ic) = "(Del " ++ showC c ++ " " ++ show ic ++ ")"+    where showC c = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))++instance (Show1 p) => Show1 (NP p) where+  show1 np = parens . concat . intersperse " "  $ elimNP show1 np+    where+      parens x = "(" ++ x  ++ ")"+++showSpine :: forall ki fam codes ix iy. (Show1 ki, HasDatatypeInfo ki fam codes, IsNat ix,  IsNat iy) => SNat ix -> SNat iy -> Spine ki codes (Lkup ix codes) (Lkup iy codes) -> String+showSpine six siy Scp = "Scp"+showSpine six siy (SCns c x) =  "(Scns " ++ showC c six ++ " " ++ show1 x ++ ")" +    where showC c six = constructorName . constrInfoLkup c $ (datatypeInfo (Proxy @fam) six)+showSpine six siy (SChg c1 c2 a) = "(SChg " ++ showCX  ++ " " ++ showCY ++ " " ++ show a  ++ ")"+    where showCX = constructorName . constrInfoLkup c1 $ (datatypeInfo (Proxy @fam) six)+          showCY = constructorName . constrInfoLkup c2 $ (datatypeInfo (Proxy @fam) siy)+{-+instance (HasDatatypeInfo ki fam codes, Show1 ki) => Show (Spine ki codes x y) where+  show Scp = "COPY"+  show (SCns c x) = "(Scns " ++ showC c ++ " " ++ show1 x ++ ")" +    where +      showC +      showC c = constructorName . consterInfoLookup c (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))+  show (SChg c1 c2 a) = "(SChg " ++ showC c1  ++ " " ++ showC c2  ++ " " ++ show a  ++ ")"+    where showC c = constructorName . consterInfoLookup c (datatypeInfo (Proxy @fam) (getSNat @ix Proxy))+-}++-- OR what about:  ix iy+guard' :: String -> Bool -> Either String ()+guard' s False = Left s+guard' _ True  = Right ()++instance Show1 SNat where+  show1 = show . go+    where+     go :: SNat n -> Int+     go SZ = 0+     go (SS s) = 1 + go s++-}