-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Pattern-Expression-based differencing of arbitrary types.
--   
--   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.
@package hdiff
@version 0.0.1

module Data.Exists
data Exists (f :: k -> *) :: *
[Exists] :: f x -> Exists f
exMap :: (forall x. f x -> g x) -> Exists f -> Exists g
exMapM :: Monad m => (forall x. f x -> m (g x)) -> Exists f -> m (Exists g)
exElim :: (forall x. f x -> a) -> Exists f -> a
instance forall k (x :: k -> *). (forall (i :: k). GHC.Show.Show (x i)) => GHC.Show.Show (Data.Exists.Exists x)

module Data.WordTrie

-- | A Trie indexed by <a>Word64</a>s.
data Trie a
Fork :: Maybe a -> Map Word64 (Trie a) -> Trie a
[trieVal] :: Trie a -> Maybe a
[trieMap] :: Trie a -> Map Word64 (Trie a)

-- | The empty trie
empty :: Trie a

-- | Inserts or modifies an element to a trie
insertWith :: a -> (a -> a) -> [Word64] -> Trie a -> Trie a

-- | Inserts a value overwriting any previous value associated with this
--   key
insert :: a -> [Word64] -> Trie a -> Trie a

-- | Performs a lookup on a trie
lookup :: [Word64] -> Trie a -> Maybe a

-- | Computes the intersection of two tries
zipWith :: (a -> b -> c) -> Trie a -> Trie b -> Trie c

-- | Maps over the trie carrying an accumulating parameter around
mapAccum :: (a -> b -> (a, c)) -> a -> Trie b -> (a, Trie c)

-- | Flattens a trie into a list
toList :: Trie a -> [([Word64], a)]
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.WordTrie.Trie a)
instance GHC.Show.Show a => GHC.Show.Show (Data.WordTrie.Trie a)
instance GHC.Base.Functor Data.WordTrie.Trie

module Data.HDiff.Diff.Types

-- | Controls the sharing of opaque values.
data DiffOpaques

-- | Never share opaque values
DO_Never :: DiffOpaques

-- | Only share opaque values that appear on the spine.
DO_OnSpine :: DiffOpaques

-- | Handle values of type <tt>K k</tt> normally, as we handle recursive
--   trees, of type <tt>I i</tt>.
DO_AsIs :: DiffOpaques

-- | Diffing Algorithm modes. This is better illustrated with an example.
--   Supposte we have the following source and destination trees:
--   
--   <pre>
--   src = Bin (Bin t k) u
--   dst = Bin (Bin t k) t
--   </pre>
data DiffMode

-- | The <i>proper share</i> algorithm will only share the trees that are
--   supposed to be a proper share. With the src and dst above, it will
--   produce:
--   
--   <pre>
--   diff src dst = Bin (Bin 0 1) u |-&gt; Bin (Bin 0 1) 0
--   </pre>
--   
--   A good intuition is that this approach will prefer maximum sharing as
--   opposed to sharing bigger trees.
DM_ProperShare :: DiffMode

-- | The first algoritm we produced. Does not share nested trees. In fact,
--   with this mode we will get the following result:
--   
--   <pre>
--   diff src dst = Bin 0 u |-&gt; Bin 0 t
--   </pre>
DM_NoNested :: DiffMode

-- | Similar to <tt>git --patience</tt>, we share only unique trees. In
--   this example, this would result in the same as <a>DM_NoNested</a>, but
--   if we take <tt>u = (Bin t k)</tt>, no sharing would be performed
--   whatsoever.
DM_Patience :: DiffMode

-- | Specifies the options for the diffing algorithm
data DiffOptions

-- | Minimum height of trees considered for sharing
DiffOptions :: Int -> DiffOpaques -> DiffMode -> DiffOptions
[doMinHeight] :: DiffOptions -> Int
[doOpaqueHandling] :: DiffOptions -> DiffOpaques
[doMode] :: DiffOptions -> DiffMode
diffOptionsDefault :: DiffOptions

-- | The data structure that captures which subtrees are shared between
--   source and destination. Besides providing an efficient answer to the
--   query: "is this tree shared?", it also gives a unique identifier to
--   that tree, allowing us to easily build our n-holed treefix.
type IsSharedMap = Trie MetavarAndArity
data MetavarAndArity
MAA :: Int -> Int -> MetavarAndArity
[getMetavar] :: MetavarAndArity -> Int
[getArity] :: MetavarAndArity -> Int

-- | A tree smaller than the minimum height will never be shared.
type MinHeight = Int
instance GHC.Show.Show Data.HDiff.Diff.Types.MetavarAndArity
instance GHC.Classes.Eq Data.HDiff.Diff.Types.MetavarAndArity
instance GHC.Show.Show Data.HDiff.Diff.Types.DiffOptions
instance GHC.Classes.Eq Data.HDiff.Diff.Types.DiffOptions
instance GHC.Enum.Enum Data.HDiff.Diff.Types.DiffMode
instance GHC.Show.Show Data.HDiff.Diff.Types.DiffMode
instance GHC.Classes.Eq Data.HDiff.Diff.Types.DiffMode
instance GHC.Show.Show Data.HDiff.Diff.Types.DiffOpaques
instance GHC.Classes.Eq Data.HDiff.Diff.Types.DiffOpaques

module Generics.MRSOP.HDiff.Digest

-- | Our digests come from Blake2s_256
newtype Digest
Digest :: Digest Blake2s_256 -> Digest
[getDigest] :: Digest -> Digest Blake2s_256

-- | Unpacks a digest into a list of Word64.
toW64s :: Digest -> [Word64]

-- | Process an <a>SNat</a> into a <a>Word64</a>. This is useful in order
--   to use type-level info as salt.
snat2W64 :: SNat n -> Word64

-- | Auxiliar hash function with the correct types instantiated.
hash :: ByteString -> Digest

-- | Auxiliar hash functions for strings
hashStr :: String -> Digest

-- | Concatenates digests together and hashes the result.
digestConcat :: [Digest] -> Digest

-- | A Value is digestible if we know how to hash it.
class Digestible (v :: *)
digest :: Digestible v => v -> Digest

-- | A functor is digestible if we can hash its value pointwise.
class DigestibleHO (f :: k -> *)
digestHO :: forall ki. DigestibleHO f => f ki -> Digest

-- | Authenticates a <tt>HPeel</tt> without caring for the type
--   information. Only use this if you are sure of what you are doing, as
--   there can be colissions. For example:
--   
--   <pre>
--   data A = A1 B | A2 Int Int
--   data B = B1 A | B2 Int Int 
--   </pre>
--   
--   <pre>
--   xA :: NP ann (Lkup 1 codesA)
--   xB :: NP ann (Lkup 1 codesB)
--   
--   authPeel' f 0 (CS CZ) xA == authPeel' f 0 (CS CZ) xB
--   </pre>
--   
--   That's because <tt>A2</tt> and <tt>B2</tt> have the exact same
--   signature and are within the exact same position within the datatype.
--   We must use the salt to pass type information:
--   
--   <pre>
--   authPeel' f (snat2W64 IdxA) (CS CZ) xA
--     =/ authPeel' f (snat2W64 IdxB) (CS CZ) xB
--   </pre>
--   
--   One should stick to <a>authPeel</a> whenever in doubt.
authPeel' :: forall sum ann i. (forall ix. ann ix -> Digest) -> Word64 -> Constr sum i -> NP ann (Lkup i sum) -> Digest

-- | This function correctly salts <a>authPeel'</a> and produces a unique
--   hash per constructor.
authPeel :: forall codes ix ann i. IsNat ix => (forall iy. ann iy -> Digest) -> Proxy codes -> Proxy ix -> Constr (Lkup ix codes) i -> NP ann (Lkup i (Lkup ix codes)) -> Digest
instance GHC.Show.Show Generics.MRSOP.HDiff.Digest.Digest
instance GHC.Classes.Eq Generics.MRSOP.HDiff.Digest.Digest
instance Generics.MRSOP.HDiff.Digest.DigestibleHO (Data.Functor.Const.Const Data.Void.Void)
instance Generics.MRSOP.HDiff.Digest.Digestible GHC.Word.Word64


-- | Here we perform a bunch of preprocessing steps from a <a>Fix</a> into
--   a <a>AnnFix</a> with the correct information for both driving the
--   algorithm and efficiently storing digests alongside the structure.
module Data.HDiff.Diff.Preprocess

-- | We precompute the digest of a tree and its height and annotate our
--   fixpoints with this data before going forward and computing a diff.
data PrepData a
PrepData :: Digest -> Int -> a -> PrepData a
[treeDigest] :: PrepData a -> Digest
[treeHeight] :: PrepData a -> Int
[treeParm] :: PrepData a -> a

-- | A <a>PrepFix</a> is a prepared fixpoint. In our case, it is just a
--   <a>HolesAnn</a> with the prepared data inside of it.
type PrepFix a ki codes phi = HolesAnn (Const (PrepData a)) ki codes phi

-- | Here we receive an expression with holes an annotate it with hashes
--   and height information at every node.
preprocess :: forall ki codes phi at. (DigestibleHO ki, DigestibleHO phi) => Holes ki codes phi at -> PrepFix () ki codes phi at
instance GHC.Show.Show a => GHC.Show.Show (Data.HDiff.Diff.Preprocess.PrepData a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.HDiff.Diff.Preprocess.PrepData a)


-- | Defines a unified interface for writing pretty printers. We force the
--   definition of pretty printers in this way to be able to use this very
--   pretty printer to render a <a>UTx</a> in the same style as the rest of
--   the ast.
module Generics.MRSOP.HDiff.Renderer
class RendererHO f
renderHO :: RendererHO f => f x -> Doc ann

-- | Default rendering of constructors
renderView :: HasDatatypeInfo ki fam codes => Proxy fam -> (forall k. ki k -> Doc ann) -> SNat ix -> View ki (Const (Doc ann)) (Lkup ix codes) -> Doc ann

-- | Default rendering of NP's with Docs inside
renderNP :: HasDatatypeInfo ki fam codes => Proxy fam -> (Doc ann -> Doc ann) -> SNat ix -> Constr (Lkup ix codes) c -> NP (Const (Doc ann)) (Lkup c (Lkup ix codes)) -> Doc ann

-- | Renders elements of the family
renderEl :: forall ki fam codes ix ann. (Family ki fam codes, HasDatatypeInfo ki fam codes, IsNat ix) => (forall k. ki k -> Doc ann) -> El fam ix -> Doc ann

-- | Renders a fixpoint
renderFix :: forall ki fam codes ix ann. (HasDatatypeInfo ki fam codes, IsNat ix) => (forall k. ki k -> Doc ann) -> Fix ki codes ix -> Doc ann

module Generics.MRSOP.HDiff.Holes

-- | Pretty-prints a treefix using a specific function to print holes.
holesPretty :: forall ki fam codes f at ann. (HasDatatypeInfo ki fam codes, RendererHO ki) => Proxy fam -> (Doc ann -> Doc ann) -> (forall at'. f at' -> Doc ann) -> Holes ki codes f at -> Doc ann

-- | Zips a <a>Holes</a> and a generic value together. Returns <a>mzero</a>
--   whenever the structure of the value is not compatible with that
--   requird by the <i>holed</i> value.
holesZipRep :: MonadPlus m => Holes ki codes f at -> NA ki (Fix ki codes) at -> m (Holes ki codes (f :*: NA ki (Fix ki codes)) at)
class HasIKProjInj (ki :: kon -> *) (f :: Atom kon -> *)
konInj :: HasIKProjInj ki f => ki k -> f ( 'K k)
varProj :: HasIKProjInj ki f => Proxy ki -> f x -> Maybe (IsI x)
data IsI :: Atom kon -> *
[IsI] :: IsNat i => IsI ( 'I i)
getIsISNat :: IsI ( 'I i) -> SNat i
type HolesTestEqualityCnstr ki f = (TestEquality ki, TestEquality f, HasIKProjInj ki f)
instance forall kon (ki :: kon -> *) (f :: Generics.MRSOP.Base.Universe.Atom kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Generics.MRSOP.HDiff.Holes.HolesTestEqualityCnstr ki f => Data.Type.Equality.TestEquality (Generics.MRSOP.Holes.Holes ki codes f)
instance forall kon (ki :: kon -> *) (phi :: Generics.MRSOP.Base.Universe.Atom kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Generics.MRSOP.HDiff.Holes.HasIKProjInj ki phi => Generics.MRSOP.HDiff.Holes.HasIKProjInj ki (Generics.MRSOP.Holes.Holes ki codes phi)


-- | Exports a bunch of functionality for handling metavariables both over
--   recursive positions only, with <a>MetaVarI</a> and over recursive
--   positions and constants, <a>MetaVarIK</a>.
module Data.HDiff.MetaVar

-- | Given a functor from <tt>Nat</tt> to <tt>*</tt>, lift it to work over
--   <tt>Atom</tt> by forcing the atom to be an <a>I</a>.
data ForceI :: (Nat -> *) -> Atom kon -> *
[ForceI] :: IsNat i => {unForceI :: f i} -> ForceI f ( 'I i)

-- | A <a>MetaVarI</a> can only take place of a recursive position.
type MetaVarI = ForceI (Const Int)

-- | This is isomorphic to <tt>const x &amp;&amp;&amp; f</tt> on the type
--   level.
data Annotate (x :: *) (f :: k -> *) :: k -> *
[Annotate] :: x -> f i -> Annotate x f i

-- | A <a>MetaVarIK</a> can be over a opaque type and a recursive position
--   
--   We keep the actual value of the constant around purely because
--   sometimes we need to compare the indexes for equality. It is possible
--   to remove that but this will require some instance like <a>IsNat</a>
--   to be bubbled up all the way to generics-mrsop.
--   
--   TODO: add a <tt>IsOpq</tt> instance and remove Annotate altogether. we
--   need a method with type <tt>defOpq :: Proxy k -&gt; ki k</tt>, we can
--   then piggyback on <a>testEquality</a> for ki. The <a>HasIKProjInj</a>
--   instance is part of this same hack.
type MetaVarIK ki = NA (Annotate Int ki) (Const Int)

-- | Returns the metavariable forgetting about type information
metavarGet :: MetaVarIK ki at -> Int

-- | Adds a number to a metavar
metavarAdd :: Int -> MetaVarIK ki at -> MetaVarIK ki at

-- | Retrieves the int inside a existential <a>MetaVarIK</a>
metavarIK2Int :: Exists (MetaVarIK ki) -> Int

-- | Retrieves the int inside a existential <a>MetaVarI</a>
metavarI2Int :: Exists MetaVarI -> Int

-- | Injects a metavar over recursive positions into one over opaque types
--   and recursive positions
metavarI2IK :: MetaVarI ix -> MetaVarIK ki ix
instance forall kon (ki :: kon -> *). Generics.MRSOP.HDiff.Digest.DigestibleHO ki => Generics.MRSOP.HDiff.Digest.DigestibleHO (Data.HDiff.MetaVar.MetaVarIK ki)
instance forall kon (ki :: kon -> *). Generics.MRSOP.HDiff.Holes.HasIKProjInj ki (Data.HDiff.MetaVar.MetaVarIK ki)
instance forall kon (ki :: kon -> *). GHC.Classes.Eq (Data.Exists.Exists (Data.HDiff.MetaVar.MetaVarIK ki))
instance forall kon (ki :: kon -> *). GHC.Classes.Ord (Data.Exists.Exists (Data.HDiff.MetaVar.MetaVarIK ki))
instance forall k1 (f :: k1 -> *) x (k2 :: k1). (Generics.MRSOP.Util.ShowHO f, GHC.Show.Show x) => GHC.Show.Show (Data.HDiff.MetaVar.Annotate x f k2)
instance forall k1 (f :: k1 -> *) x (k2 :: k1). (Generics.MRSOP.Util.EqHO f, GHC.Classes.Eq x) => GHC.Classes.Eq (Data.HDiff.MetaVar.Annotate x f k2)
instance forall k (ki :: k -> *) x. Data.Type.Equality.TestEquality ki => Data.Type.Equality.TestEquality (Data.HDiff.MetaVar.Annotate x ki)
instance GHC.Classes.Eq (Data.Exists.Exists Data.HDiff.MetaVar.MetaVarI)
instance GHC.Classes.Ord (Data.Exists.Exists Data.HDiff.MetaVar.MetaVarI)

module Data.HDiff.Diff.Modes

-- | A predicate indicating whether a tree can be shared.
type CanShare ki codes phi = forall a ix. PrepFix a ki codes phi ix -> Bool
extractHoles :: DiffMode -> CanShare ki codes phi -> IsSharedMap -> Delta (PrepFix a ki codes phi) at -> Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at
extractProperShare :: CanShare ki codes phi -> IsSharedMap -> PrepFix a ki codes phi at -> Holes ki codes (Sum phi (MetaVarIK ki)) at
tagProperShare :: forall a ki codes phi at. IsSharedMap -> PrepFix a ki codes phi at -> PrepFix (Int, Bool) ki codes phi at
properShare :: forall ki codes phi at. CanShare ki codes phi -> IsSharedMap -> PrepFix (Int, Bool) ki codes phi at -> Holes ki codes (Sum phi (MetaVarIK ki)) at
extractPatience :: CanShare ki codes phi -> IsSharedMap -> PrepFix a ki codes phi at -> Holes ki codes (Sum phi (MetaVarIK ki)) at
patience :: forall ki codes phi at a. CanShare ki codes phi -> IsSharedMap -> PrepFix a ki codes phi at -> Holes ki codes (Sum phi (MetaVarIK ki)) at
extractNoNested :: CanShare ki codes phi -> IsSharedMap -> Delta (PrepFix a ki codes phi) at -> Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at
noNested :: forall ki codes phi at a. CanShare ki codes phi -> IsSharedMap -> PrepFix a ki codes phi at -> Holes ki codes (Sum phi (Const Int :*: PrepFix a ki codes phi)) at

module Data.HDiff.Change

-- | A <a>CChange</a>, or, closed change, consists in a declaration of
--   metavariables and two contexts. The precondition is that every
--   variable declared occurs at least once in ctxDel and that every
--   variable that occurs in ctxIns is declared.
data CChange ki codes at
[CMatch] :: {cCtxVars :: Set (Exists (MetaVarIK ki)), cCtxDel :: Holes ki codes (MetaVarIK ki) at, cCtxIns :: Holes ki codes (MetaVarIK ki) at} -> CChange ki codes at

-- | smart constructor for <a>CChange</a>. Enforces the invariant
cmatch :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> CChange ki codes at
cmatch' :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Maybe (CChange ki codes at)

-- | A <a>Domain</a> is just a deletion context. Type-synonym helps us
--   identify what's what on the algorithms below.
type Domain ki codes = Holes ki codes (MetaVarIK ki)
domain :: CChange ki codes at -> Domain ki codes at
unCMatch :: CChange ki codes at -> (Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)) at

-- | Returns the maximum variable in a change
cMaxVar :: CChange ki codes at -> Int

-- | Alpha-equality for <a>CChange</a>
changeEq :: EqHO ki => CChange ki codes at -> CChange ki codes at -> Bool

-- | Issues a copy, this is a closed change analogous to &gt; x -&gt; x
changeCopy :: MetaVarIK ki at -> CChange ki codes at

-- | Checks whetehr a change is a copy.
isCpy :: EqHO ki => CChange ki codes at -> Bool
makeCopyFrom :: CChange ki codes at -> CChange ki codes at

-- | Renames all changes within a <a>Holes</a> so that their variable names
--   will not clash.
cWithDisjNamesFrom :: CChange ki codes at -> CChange ki codes at -> CChange ki codes at

-- | A Utx with closed changes distributes over a closed change
distrCChange :: Holes ki codes (CChange ki codes) at -> CChange ki codes at

-- | A <a>OChange</a>, or, open change, is analogous to a <a>CChange</a>,
--   but has a list of free variables. These are the ones that appear in
--   <a>oCtxIns</a> but not in <a>oCtxDel</a>
data OChange ki codes at
[OMatch] :: {oCtxVDel :: Set (Exists (MetaVarIK ki)), oCtxVIns :: Set (Exists (MetaVarIK ki)), oCtxDel :: Holes ki codes (MetaVarIK ki) at, oCtxIns :: Holes ki codes (MetaVarIK ki) at} -> OChange ki codes at

-- | Given two treefixes, constructs and classifies a change from them.
change :: Holes ki codes (MetaVarIK ki) at -> Holes ki codes (MetaVarIK ki) at -> Sum (OChange ki codes) (CChange ki codes) at
type Holes2 ki codes = Holes ki codes (MetaVarIK ki) :*: Holes ki codes (MetaVarIK ki)
type HolesHoles2 ki codes = Holes ki codes (Holes2 ki codes)
fst' :: (f :*: g) x -> f x
snd' :: (f :*: g) x -> g x
scDel :: HolesHoles2 ki codes at -> Holes ki codes (MetaVarIK ki) at
scIns :: HolesHoles2 ki codes at -> Holes ki codes (MetaVarIK ki) at
utx2distr :: HolesHoles2 ki codes at -> Holes2 ki codes at
utx22change :: HolesHoles2 ki codes at -> Maybe (CChange ki codes at)
change2holes2 :: EqHO ki => CChange ki codes at -> HolesHoles2 ki codes at
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Generics.MRSOP.HDiff.Holes.HasIKProjInj ki (Data.HDiff.Change.Holes2 ki codes)
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Generics.MRSOP.HDiff.Holes.HasIKProjInj ki (Data.HDiff.Change.CChange ki codes)
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). Data.Type.Equality.TestEquality ki => Data.Type.Equality.TestEquality (Data.HDiff.Change.CChange ki codes)
instance forall k (f :: k -> *) (g :: k -> *). Data.Type.Equality.TestEquality f => Data.Type.Equality.TestEquality (f Generics.MRSOP.Util.:*: g)


-- | change classification algorithm
module Data.HDiff.Change.Classify
getConstrSNat :: IsNat n => Constr sum n -> SNat n
holesGetMultiplicities :: Int -> Holes ki codes f at -> [Exists (Holes ki codes f)]
data ChangeClass
CPerm :: ChangeClass
CMod :: ChangeClass
CId :: ChangeClass
CIns :: ChangeClass
CDel :: ChangeClass
changeClassify :: (EqHO ki, TestEquality ki) => CChange ki codes at -> ChangeClass
isIns :: (TestEquality ki, EqHO ki) => CChange ki codes ix -> Bool
isDel :: (TestEquality ki, EqHO ki) => CChange ki codes ix -> Bool
instance GHC.Classes.Ord Data.HDiff.Change.Classify.ChangeClass
instance GHC.Show.Show Data.HDiff.Change.Classify.ChangeClass
instance GHC.Classes.Eq Data.HDiff.Change.Classify.ChangeClass
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]). (Generics.MRSOP.Util.EqHO ki, Data.Type.Equality.TestEquality ki) => GHC.Classes.Eq (Data.Exists.Exists (Generics.MRSOP.Holes.Holes ki codes (Data.HDiff.MetaVar.MetaVarIK ki)))


-- | Defines the application function for a <a>CChange</a>
module Data.HDiff.Change.Apply

-- | Application might fail with some <a>ApplicationErr</a> describing the
--   point of failure.
data ApplicationErr :: (kon -> *) -> [[[Atom kon]]] -> (Atom kon -> *) -> *
[UndefinedVar] :: Int -> ApplicationErr ki codes phi
[FailedContraction] :: Int -> Holes ki codes phi ix -> Holes ki codes phi ix -> ApplicationErr ki codes phi
[IncompatibleTypes] :: ApplicationErr ki codes phi
[IncompatibleOpqs] :: ki k -> ki k -> ApplicationErr ki codes phi
[IncompatibleHole] :: Holes ki codes (MetaVarIK ki) ix -> phi ix -> ApplicationErr ki codes phi
[IncompatibleTerms] :: Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix -> ApplicationErr ki codes phi

-- | A instantiation substitution from metavariable numbers to some treefix
type Subst ki codes phi = Map Int (Exists (Holes ki codes phi))
type Applicable ki codes phi = (TestEquality ki, TestEquality phi, HasIKProjInj ki phi)

-- | We try to unify <tt>pa</tt> and <tt>pq</tt> onto <tt>ea</tt>. The idea
--   is that we instantiate the variables of <tt>pa</tt> with their
--   corresponding expression on <tt>x</tt>, and substitute those in
--   <tt>ea</tt>. Whereas if we reach a variable in <tt>x</tt> we ignore
--   whatever was on <tt>ea</tt> and give that variable instead.
--   
--   We are essentially applying
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)

-- | Specializes <a>genericApply</a> to work over terms of our language,
--   ie, <a>NA</a>s
termApply :: forall ki codes at. (ShowHO ki, EqHO ki, TestEquality ki) => CChange ki codes at -> NA ki (Fix ki codes) at -> Either String (NA ki (Fix ki codes) at)

-- | <tt>pmatch pa x</tt> traverses <tt>pa</tt> and <tt>x</tt>
--   instantiating the variables of <tt>pa</tt>. Upon sucessfully
--   instantiating the variables, returns the substitution.
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' :: (Applicable ki codes phi, EqHO phi, EqHO ki) => Subst ki codes phi -> Holes ki codes (MetaVarIK ki) ix -> Holes ki codes phi ix -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)

-- | Given a <a>MetaVarIK</a> and a <a>Holes</a>, decide whether their
--   indexes are equal.
idxDecEq :: forall ki codes phi at ix. (TestEquality ki, TestEquality phi, HasIKProjInj ki phi) => Holes ki codes phi at -> MetaVarIK ki ix -> Maybe (at :~: ix)

-- | 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, EqHO ki, EqHO phi) => Subst ki codes phi -> MetaVarIK ki ix -> Holes ki codes phi ix -> Except (ApplicationErr ki codes phi) (Subst ki codes phi)

-- | Instantiates the metavariables in the given term using the
--   substitution in the state
transport :: Applicable ki codes phi => Holes ki codes (MetaVarIK ki) ix -> Subst ki codes phi -> Except (ApplicationErr ki codes phi) (Holes ki codes phi ix)

-- | Looks for the value of a <tt>MetaVarIK ki ix</tt> in the substitution
--   in our state. Returns <tt>Nothing</tt> when the variables is not found
--   or throws <a>IncompatibleTypes</a> when the value registered in the
--   substitution is of type <tt>iy</tt> with <tt>ix /= iy</tt>.
lookupVar :: forall ki codes phi ix. Applicable ki codes phi => MetaVarIK ki ix -> Subst ki codes phi -> Except (ApplicationErr ki codes phi) (Maybe (Holes ki codes phi ix))
instance forall kon (ki :: kon -> *) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (phi :: Generics.MRSOP.Base.Universe.Atom kon -> *). GHC.Show.Show (Data.HDiff.Change.Apply.ApplicationErr ki codes phi)

module Data.HDiff.Patch

-- | Instead of keeping unecessary information, a <a>RawPatch</a> will
--   factor out the common prefix before the actual changes.
type RawPatch ki codes = Holes ki codes (CChange ki codes)

-- | A <a>Patch</a> is a <a>RawPatch</a> instantiated to <a>I</a> atoms.
type Patch ki codes ix = Holes ki codes (CChange ki codes) ( 'I ix)
patchEq :: EqHO ki => RawPatch ki codes at -> RawPatch ki codes at -> Bool
patchIsCpy :: EqHO ki => RawPatch ki codes at -> Bool
patchMaxVar :: RawPatch ki codes at -> Int

-- | Calling <tt>p <a>withFreshNamesFrom</a> q</tt> will return an alpha
--   equivalent version of <tt>p</tt> that has no name clasehs with
--   <tt>q</tt>.
withFreshNamesFrom :: RawPatch ki codes at -> RawPatch ki codes at -> RawPatch ki codes at

-- | Computes the <i>cost</i> of a <a>Patch</a>. This is in the sense of
--   edit-scripts where it counts how many constructors are being inserted
--   and deleted.
patchCost :: RawPatch ki codes at -> Int

-- | Applying a patch is trivial, we simply project the deletion treefix
--   and inject the valuation into the insertion.
apply :: (TestEquality ki, EqHO ki, ShowHO ki, IsNat ix) => Patch ki codes ix -> Fix ki codes ix -> Either String (Fix ki codes ix)

-- | The predicate <tt>composes qr pq</tt> checks whether <tt>qr</tt> is
--   immediatly applicable to the codomain of <tt>pq</tt>.
composes :: (ShowHO ki, EqHO ki, TestEquality ki) => RawPatch ki codes at -> RawPatch ki codes at -> Bool
applicableTo :: (ShowHO ki, EqHO ki, TestEquality ki) => Holes ki codes (MetaVarIK ki) ix -> Holes ki codes (MetaVarIK ki) ix -> Bool
substInsert' :: (ShowHO ki, EqHO ki, TestEquality ki) => String -> Subst ki codes (MetaVarIK ki) -> MetaVarIK ki ix -> Holes ki codes (MetaVarIK ki) ix -> Except (ApplicationErr ki codes (MetaVarIK ki)) (Subst ki codes (MetaVarIK ki))

module Data.HDiff.Diff

-- | Diffs two generic merkelized structures. The outline of the process
--   is:
--   
--   i) Annotate each tree with the info we need (digest and height) ii)
--   Build the sharing trie iii) Identify the proper shares iv) Substitute
--   the proper shares by a metavar in both the source and deletion context
--   v) Extract the spine and compute the closure.
diffOpts' :: forall ki codes phi at. (EqHO ki, DigestibleHO ki, DigestibleHO phi) => DiffOptions -> Holes ki codes phi at -> Holes ki codes phi at -> (Int, Delta (Holes ki codes (Sum phi (MetaVarIK ki))) at)

-- | When running the diff for two fixpoints, we can cast the resulting
--   deletion and insertion context into an actual patch.
diffOpts :: (EqHO ki, DigestibleHO ki, IsNat ix) => DiffOptions -> Fix ki codes ix -> Fix ki codes ix -> Patch ki codes ix
diff :: (EqHO ki, DigestibleHO ki, IsNat ix) => MinHeight -> Fix ki codes ix -> Fix ki codes ix -> Patch ki codes ix

-- | Diffing Algorithm modes. This is better illustrated with an example.
--   Supposte we have the following source and destination trees:
--   
--   <pre>
--   src = Bin (Bin t k) u
--   dst = Bin (Bin t k) t
--   </pre>
data DiffMode

-- | The <i>proper share</i> algorithm will only share the trees that are
--   supposed to be a proper share. With the src and dst above, it will
--   produce:
--   
--   <pre>
--   diff src dst = Bin (Bin 0 1) u |-&gt; Bin (Bin 0 1) 0
--   </pre>
--   
--   A good intuition is that this approach will prefer maximum sharing as
--   opposed to sharing bigger trees.
DM_ProperShare :: DiffMode

-- | The first algoritm we produced. Does not share nested trees. In fact,
--   with this mode we will get the following result:
--   
--   <pre>
--   diff src dst = Bin 0 u |-&gt; Bin 0 t
--   </pre>
DM_NoNested :: DiffMode

-- | Similar to <tt>git --patience</tt>, we share only unique trees. In
--   this example, this would result in the same as <a>DM_NoNested</a>, but
--   if we take <tt>u = (Bin t k)</tt>, no sharing would be performed
--   whatsoever.
DM_Patience :: DiffMode

module Data.HDiff.Example

-- | 2-3-Trees declaration
data Tree23
Node2 :: Int -> Tree23 -> Tree23 -> Tree23
Node3 :: Int -> Tree23 -> Tree23 -> Tree23 -> Tree23
Leaf :: Tree23
type FamTree23 = '[Tree23]
type CodesTree23 = '['['[ 'K  'KInt,  'I  'Z,  'I  'Z], '[ 'K  'KInt,  'I  'Z,  'I  'Z,  'I  'Z], '[]]]
pattern Leaf_ :: View kon_axLC phi_axLB (Lkup  'Z CodesTree23)
pattern Node3_ :: kon_axLA  'KInt -> phi_axLz  'Z -> phi_axLz  'Z -> phi_axLz  'Z -> View kon_axLA phi_axLz (Lkup  'Z CodesTree23)
pattern Node2_ :: kon_axLu  'KInt -> phi_axLt  'Z -> phi_axLt  'Z -> View kon_axLu phi_axLt (Lkup  'Z CodesTree23)
pattern IdxTree23 :: forall (a :: Nat). () => a ~# Z => SNat a
mt1 :: Tree23
mt2 :: Tree23
mt3 :: Tree23
mt4 :: Tree23
big1 :: Tree23
big2 :: Tree23
big3 :: Tree23
tr :: Tree23 -> Fix Singl CodesTree23  'Z
dgms :: Tree23 -> Tree23 -> Patch Singl CodesTree23  'Z
o :: Tree23
p :: Tree23
q :: Tree23
type TreeTerm = Holes Singl CodesTree23 (MetaVarIK Singl) ( 'I  'Z)
unif1 :: TreeTerm
unif12 :: TreeTerm
unif2 :: TreeTerm
unif22 :: TreeTerm
change1 :: CChange Singl CodesTree23 (I Z :: Atom Kon)
change2 :: CChange Singl CodesTree23 (I Z :: Atom Kon)
instance Generics.MRSOP.Base.Class.Family Generics.MRSOP.Opaque.Singl Data.HDiff.Example.FamTree23 Data.HDiff.Example.CodesTree23
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Generics.MRSOP.Opaque.Singl Data.HDiff.Example.FamTree23 Data.HDiff.Example.CodesTree23
instance GHC.Show.Show Data.HDiff.Example.Tree23
instance GHC.Classes.Eq Data.HDiff.Example.Tree23
instance Generics.MRSOP.HDiff.Digest.DigestibleHO Generics.MRSOP.Opaque.Singl

module Data.HDiff.Change.TreeEditDistance
data ListES a
LC :: Int -> a -> ListES a -> ListES a
LD :: Int -> a -> ListES a -> ListES a
LI :: Int -> a -> ListES a -> ListES a
LLP_Nil :: ListES a
cost :: ListES a -> Int
pushCopiesIns :: Eq a => ListES a -> ListES a
meet :: ListES a -> ListES a -> ListES a
type Table a = Map (Int, Int) (ListES a)
lcsW :: forall a. Eq a => (a -> Int) -> [a] -> [a] -> ListES a
fromNA :: NA ki (Fix ki codes) at -> Holes ki codes (MetaVarIK ki) at
toES :: (EqHO ki, ShowHO ki, TestEquality ki) => CChange ki codes at -> NA ki (Fix ki codes) at -> Either String (ES ki codes '[at] '[at])
type ToES ki codes = ReaderT (Subst ki codes (MetaVarIK ki), ListES Int) (Except String)
askSubst :: ToES ki codes (Subst ki codes (MetaVarIK ki))
askListES :: ToES ki codes (ListES Int)
gcpy :: Cof ki codes at l -> ES ki codes (l :++: ds) (l :++: is) -> ES ki codes (at : ds) (at : is)
gins :: Cof ki codes at l -> ES ki codes ds (l :++: is) -> ES ki codes ds (at : is)
gdel :: Cof ki codes at l -> ES ki codes (l :++: ds) is -> ES ki codes (at : ds) is
compress :: (EqHO ki, TestEquality ki) => ES ki codes is ds -> ES ki codes is ds
cpyOnly :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (Holes ki codes (MetaVarIK ki)) xs -> ToES ki codes (ES ki codes xs xs)
delOnly :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (Holes ki codes (MetaVarIK ki)) ds -> ToES ki codes (ES ki codes ds '[])
insOnly :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (Holes ki codes (MetaVarIK ki)) is -> ToES ki codes (ES ki codes '[] is)
listAssoc :: ListPrf a -> Proxy b -> Proxy c -> ListPrf ((a :++: b) :++: c) :~: ListPrf (a :++: (b :++: c))
listDrop :: ListPrf i -> ListPrf (i :++: t) -> ListPrf t
esDelListPrf :: ES ki codes ds is -> ListPrf ds
esInsListPrf :: ES ki codes ds is -> ListPrf is
cofListPrf :: Cof ki codes at l -> ListPrf l
esDelListProxy :: ES ki codes ds is -> Proxy ds
esDelListProxy' :: ES ki codes (d : ds) is -> Proxy ds
esInsListProxy :: ES ki codes ds is -> Proxy is
esInsListProxy' :: ES ki codes ds (i : is) -> Proxy is
esDelCong :: (ListPrf ds :~: ListPrf ds') -> ES ki codes ds is -> ES ki codes ds' is
esInsCong :: (ListPrf is :~: ListPrf is') -> ES ki codes ds is -> ES ki codes ds is'
appendES :: ES ki codes ds is -> ES ki codes ds' is' -> ES ki codes (ds :++: ds') (is :++: is')
fetch :: (EqHO ki, ShowHO ki, TestEquality ki) => MetaVarIK ki at -> ToES ki codes (Holes ki codes (MetaVarIK ki) at)
delSync :: (EqHO ki, ShowHO ki, TestEquality ki) => MetaVarIK ki at -> NP (Holes ki codes (MetaVarIK ki)) ds -> NP (Holes ki codes (MetaVarIK ki)) is -> ToES ki codes (ES ki codes (at : ds) is)
insSync :: (EqHO ki, ShowHO ki, TestEquality ki) => MetaVarIK ki at -> NP (Holes ki codes (MetaVarIK ki)) ds -> NP (Holes ki codes (MetaVarIK ki)) is -> ToES ki codes (ES ki codes ds (at : is))
delPhase :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (Holes ki codes (MetaVarIK ki)) ds -> NP (Holes ki codes (MetaVarIK ki)) is -> ToES ki codes (ES ki codes ds is)
insPhase :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (Holes ki codes (MetaVarIK ki)) ds -> NP (Holes ki codes (MetaVarIK ki)) is -> ToES ki codes (ES ki codes ds is)
instance GHC.Show.Show a => GHC.Show.Show (Data.HDiff.Change.TreeEditDistance.ListES a)
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.HDiff.Change.TreeEditDistance.ListES a)

module Data.HDiff.Patch.TreeEditDistance
toES :: (EqHO ki, ShowHO ki, TestEquality ki) => RawPatch ki codes at -> NA ki (Fix ki codes) at -> Either String (ES ki codes '[at] '[at])
listId :: ListPrf a -> ListPrf a :~: ListPrf (a :++: '[])
toES' :: (EqHO ki, ShowHO ki, TestEquality ki) => NP (RawPatch ki codes) sum -> PoA ki (Fix ki codes) sum -> Either String (ES ki codes sum sum)

module Data.HDiff.Change.Thinning
type ThinningErr ki codes = ApplicationErr ki codes (MetaVarIK ki)
lift' :: Monad m => m a -> StateT (Subst ki codes (MetaVarIK ki)) m a
thin :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (CChange ki codes at)
tr :: (ShowHO ki, TestEquality ki, EqHO ki) => CChange ki codes at -> CChange ki codes at -> Either (ApplicationErr ki codes (Holes2 ki codes)) (CChange ki codes at)
thinUTx2 :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Domain ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at)
thin' :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes2 ki codes at -> Holes2 ki codes at -> Either (ApplicationErr ki codes (MetaVarIK ki)) (Holes2 ki codes at)

-- | The <tt>thin' p q</tt> function is where work where we produce the map
--   that will be applied to <tt>p</tt> in order to thin it. This function
--   does <i>NOT</i> minimize this map.
utxThin :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) at -> Domain ki codes at -> StateT (Subst ki codes (MetaVarIK ki)) (Except (ThinningErr ki codes)) ()

-- | The minimization step performs the <tt>occurs</tt> check and removes
--   unecessary steps. For example;
--   
--   <pre>
--   sigma = fromList
--             [ (0 , bin 1 2)
--             , (1 , bin 4 4) ]
--   </pre>
--   
--   Then, <tt>minimize sigma</tt> will return <tt>fromList [(0 , bin (bin
--   4 4) 2)]</tt>
minimize :: forall ki codes. (ShowHO ki, EqHO ki, TestEquality ki) => Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Subst ki codes (MetaVarIK ki))

-- | This is similar to <a>transport</a>, but does not throw errors on
--   undefined variables.
refine :: (ShowHO ki, TestEquality ki, EqHO ki) => Holes ki codes (MetaVarIK ki) ix -> Subst ki codes (MetaVarIK ki) -> Except (ThinningErr ki codes) (Holes ki codes (MetaVarIK ki) ix)

module Data.HDiff.Patch.Thinning
thin :: forall ki codes at. (ShowHO ki, TestEquality ki, EqHO ki) => RawPatch ki codes at -> RawPatch ki codes at -> Either (ThinningErr ki codes) (RawPatch ki codes at)
unsafeThin :: (ShowHO ki, TestEquality ki, EqHO ki) => RawPatch ki codes at -> RawPatch ki codes at -> RawPatch ki codes at

module Data.HDiff.Patch.Merge

-- | Hence, a conflict is simply two changes together.
data Conflict :: (kon -> *) -> [[[Atom kon]]] -> Atom kon -> *
[Conflict] :: String -> RawPatch ki codes at -> RawPatch ki codes at -> Conflict ki codes at

-- | A <a>PatchC</a> is a patch with potential conflicts inside
type PatchC ki codes ix = Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) ( 'I ix)

-- | Tries to cast a <a>PatchC</a> back to a <a>Patch</a>. Naturally, this
--   is only possible if the patch has no conflicts.
noConflicts :: PatchC ki codes ix -> Maybe (Patch ki codes ix)

-- | Returns the labels of the conflicts ina a patch.
getConflicts :: ShowHO ki => PatchC ki codes ix -> [String]

-- | A merge of <tt>p</tt> over <tt>q</tt>, denoted <tt>p // q</tt>, is the
--   adaptation of <tt>p</tt> so that it could be applied to an element in
--   the image of <tt>q</tt>.
(//) :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => Patch ki codes ix -> Patch ki codes ix -> PatchC ki codes ix

-- | The <a>reconcile</a> function will try to reconcile disagreeing
--   patches.
--   
--   Precondition: before calling <tt>reconcile p q</tt>, make sure
--   <tt>p</tt> and <tt>q</tt> are different.
reconcile :: forall ki codes fam at. (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki, HasDatatypeInfo ki fam codes) => RawPatch ki codes at -> RawPatch ki codes at -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at
data ProcessOutcome ki codes
ReturnNominator :: ProcessOutcome ki codes
InstDenominator :: Subst ki codes (Holes2 ki codes) -> ProcessOutcome ki codes
CantReconcile :: String -> ProcessOutcome ki codes

-- | Checks whether a variable is a rawCpy, note that we need a map that
--   checks occurences of this variable.
rawCpy :: Map Int Int -> Holes2 ki codes at -> Bool
simpleCopy :: Holes2 ki codes at -> Bool
isLocalIns :: Holes2 ki codes at -> Bool
arityMap :: Holes ki codes (MetaVarIK ki) at -> Map Int Int

-- | This will process two changes, represented as a spine and inner
--   changes, into a potential merged patch. The result of <tt>process sp
--   sq</tt> is supposed to instruct how to construct a patch that can be
--   applied to the image <tt>sq</tt>.
--   
--   We do so by traversing the places where both <tt>sp</tt> and
--   <tt>sq</tt> differ. While we perform this traversal we instantiate a
--   valuation of potential substitutions, which might be needed in case we
--   need to adapt <tt>sp</tt> to <tt>sq</tt>. After we are done, we know
--   whether we need to adapt <tt>sp</tt>, return <tt>sp</tt> as is, or
--   there is a conflict.
process :: (Applicable ki codes (Holes2 ki codes), EqHO ki, ShowHO ki) => HolesHoles2 ki codes at -> HolesHoles2 ki codes at -> ProcessOutcome ki codes

module Data.HDiff.Patch.Show

-- | Given a label and a doc, <tt>spliced l d = "[" ++ l ++ "|" ++ d ++
--   "|]"</tt>
spliced :: Doc ann -> Doc ann -> Doc ann
metavarPretty :: (Doc AnsiStyle -> Doc AnsiStyle) -> MetaVarIK ki ix -> Doc AnsiStyle
myred :: AnsiStyle
mygreen :: AnsiStyle
mydullred :: AnsiStyle
mydullgreen :: AnsiStyle

-- | Pretty prints a patch on the terminal
showRawPatch :: (HasDatatypeInfo ki fam codes, RendererHO ki) => Holes ki codes (CChange ki codes) v -> [String]
showPatchC :: (HasDatatypeInfo ki fam codes, RendererHO ki) => Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at -> [String]

-- | Outputs the result of <a>showPatchC</a> to the specified handle
displayPatchC :: (HasDatatypeInfo ki fam codes, RendererHO ki) => Handle -> Holes ki codes (Sum (Conflict ki codes) (CChange ki codes)) at -> IO ()

-- | Outputs the result of <a>showRawPatch</a> to the specified handle
displayRawPatch :: (HasDatatypeInfo ki fam codes, RendererHO ki) => Handle -> Holes ki codes (CChange ki codes) at -> IO ()

-- | Displays two docs in a double column fashion
--   
--   This is a hacky function. We need to render both the colored and the
--   non-colored versions to calculate the width spacing correctly (see
--   <tt>complete</tt> in the where clause)
doubleColumn :: Int -> Doc AnsiStyle -> Doc AnsiStyle -> [String]
instance forall kon (ki :: kon -> *) (fam :: [*]) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (at :: Generics.MRSOP.Base.Universe.Atom kon). (Generics.MRSOP.Base.Metadata.HasDatatypeInfo ki fam codes, Generics.MRSOP.HDiff.Renderer.RendererHO ki) => GHC.Show.Show (Generics.MRSOP.Holes.Holes ki codes (Data.HDiff.Change.CChange ki codes) at)
instance forall kon (ki :: kon -> *) (fam :: [*]) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (phi :: Generics.MRSOP.Base.Universe.Atom kon -> *) (at :: Generics.MRSOP.Base.Universe.Atom kon). (Generics.MRSOP.Base.Metadata.HasDatatypeInfo ki fam codes, Generics.MRSOP.HDiff.Renderer.RendererHO ki, Generics.MRSOP.Util.ShowHO phi) => GHC.Show.Show (Generics.MRSOP.Util.Delta (Generics.MRSOP.Holes.Holes ki codes phi) at)
instance forall kon (ki :: kon -> *) (fam :: [*]) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (at :: Generics.MRSOP.Base.Universe.Atom kon). (Generics.MRSOP.Base.Metadata.HasDatatypeInfo ki fam codes, Generics.MRSOP.HDiff.Renderer.RendererHO ki) => GHC.Show.Show (Data.HDiff.Change.CChange ki codes at)
instance forall kon (ki :: kon -> *) (fam :: [*]) (codes :: [[[Generics.MRSOP.Base.Universe.Atom kon]]]) (at :: Generics.MRSOP.Base.Universe.Atom kon). (Generics.MRSOP.Base.Metadata.HasDatatypeInfo ki fam codes, Generics.MRSOP.HDiff.Renderer.RendererHO ki) => GHC.Show.Show (Generics.MRSOP.Holes.Holes ki codes (Data.Functor.Sum.Sum (Data.HDiff.Patch.Merge.Conflict ki codes) (Data.HDiff.Change.CChange ki codes)) at)

module Languages.RTree
data RTree
(:>:) :: String -> [RTree] -> RTree
height :: RTree -> Int
data WKon
WString :: WKon
data W :: WKon -> *
[W_String] :: String -> W  'WString
type FamRTree = '[RTree, [RTree]]
type CodesRTree = '['['[ 'K  'WString,  'I ( 'S  'Z)]], '['[], '[ 'I  'Z,  'I ( 'S  'Z)]]]
pattern ListRTree_Ifx1 :: phi_aEbA  'Z -> phi_aEbA ( 'S  'Z) -> View kon_aEbB phi_aEbA (Lkup ( 'S  'Z) CodesRTree)
pattern ListRTree_Ifx0 :: View kon_aEbx phi_aEbw (Lkup ( 'S  'Z) CodesRTree)
pattern RTree_Ifx0 :: kon_aEbv  'WString -> phi_aEbu ( 'S  'Z) -> View kon_aEbv phi_aEbu (Lkup  'Z CodesRTree)
pattern IdxListRTree :: forall (a :: Nat). () => forall (n :: Nat). (a ~# S n, n ~# Z) => SNat a
pattern IdxRTree :: forall (a :: Nat). () => a ~# Z => SNat a
genConName :: Gen String
genTree :: Int -> Gen RTree
insertAt :: Int -> a -> [a] -> [a]
genInsHere :: RTree -> Gen RTree
genSimilarTrees :: Int -> Gen (RTree, RTree)
genSimilarTreesN :: Int -> Int -> Gen [RTree]
genSimilarTrees' :: Gen (RTree, RTree)
genSimilarTrees'' :: Gen (RTree, RTree, RTree)
instance Generics.MRSOP.Base.Class.Family Languages.RTree.W Languages.RTree.FamRTree Languages.RTree.CodesRTree
instance Generics.MRSOP.Base.Metadata.HasDatatypeInfo Languages.RTree.W Languages.RTree.FamRTree Languages.RTree.CodesRTree
instance Test.QuickCheck.Arbitrary.Arbitrary Languages.RTree.RTree
instance GHC.Show.Show Languages.RTree.RTree
instance GHC.Classes.Eq Languages.RTree.RTree
instance GHC.Classes.Eq (Languages.RTree.W x)
instance Generics.MRSOP.HDiff.Digest.DigestibleHO Languages.RTree.W
instance Generics.MRSOP.HDiff.Renderer.RendererHO Languages.RTree.W
instance GHC.Show.Show (Languages.RTree.W x)
instance Data.Type.Equality.TestEquality Languages.RTree.W

module Languages.RTree.Diff
type PatchRTree = Patch W CodesRTree  'Z
rbin :: RTree -> RTree -> RTree
rlf :: String -> RTree
x1 :: RTree
y1 :: RTree
digemRTreeH :: Int -> RTree -> RTree -> PatchRTree
digemRTreeHM :: DiffMode -> Int -> RTree -> RTree -> PatchRTree
rtreeMerkle :: RTree -> Digest
digemRTree :: RTree -> RTree -> PatchRTree
applyRTree :: PatchRTree -> RTree -> Either String RTree
applyRTreeC :: CChange W CodesRTree ( 'I  'Z) -> RTree -> Either String RTree
applyRTree' :: PatchRTree -> RTree -> Maybe RTree