--  Copyright (C) 2002-2003 David Roundy, 2010 Ganesh Sittampalam
module Darcs.Patch.Conflict
    ( Conflict(..)
    , ConflictDetails(..)
    , Mangled
    , Unravelled
    , mangleOrFail
    , combineConflicts
    , findConflicting
    ) where

import Darcs.Prelude

import Darcs.Patch.Commute ( Commute(..), commuteFL, commuteRL )
import Darcs.Patch.CommuteFn ( commuterIdFL )
import Darcs.Patch.CommuteNoConflicts ( CommuteNoConflicts(..) )
import Darcs.Patch.Permutations ()
import Darcs.Patch.FromPrim ( PrimOf )
import Darcs.Patch.Prim ( PrimMangleUnravelled(..), Mangled, Unravelled )
import Darcs.Patch.Show ( ShowPatch(..), ShowPatchFor(ForStorage), showPatch )
import Darcs.Patch.Witnesses.Ordered ( (:>)(..), FL(..), RL(..), mapFL, (+<<+) )
import Darcs.Util.Printer ( renderString, text, vcat, ($$) )

data ConflictDetails prim wX =
  ConflictDetails {
    forall (prim :: * -> * -> *) wX.
ConflictDetails prim wX -> Maybe (Mangled prim wX)
conflictMangled :: Maybe (Mangled prim wX),
    forall (prim :: * -> * -> *) wX.
ConflictDetails prim wX -> Unravelled prim wX
conflictParts :: Unravelled prim wX
  }

-- | For one conflict (a connected set of conflicting prims), store the
-- conflicting parts and, if possible, their mangled version.
mangleOrFail :: PrimMangleUnravelled prim
             => Unravelled prim wX -> ConflictDetails prim wX
mangleOrFail :: forall (prim :: * -> * -> *) wX.
PrimMangleUnravelled prim =>
Unravelled prim wX -> ConflictDetails prim wX
mangleOrFail Unravelled prim wX
parts =
  ConflictDetails {
    conflictMangled :: Maybe (Mangled prim wX)
conflictMangled = Unravelled prim wX -> Maybe (Mangled prim wX)
forall wX. Unravelled prim wX -> Maybe (Mangled prim wX)
forall (prim :: * -> * -> *) wX.
PrimMangleUnravelled prim =>
Unravelled prim wX -> Maybe (Mangled prim wX)
mangleUnravelled Unravelled prim wX
parts,
    conflictParts :: Unravelled prim wX
conflictParts = Unravelled prim wX
parts
  }

class Conflict p where
    isConflicted :: p wX wY ->  Bool
    -- | The first parameter is a context containing all patches
    -- preceding the ones for which we want to calculate the conflict
    -- resolution, which is the second parameter.
    -- Each element of the result list represents the resolution
    -- of one maximal set of transitively conflicting alternatives,
    -- in other words, a connected subset of the conflict graph.
    -- But the elements themselves must not conflict with each other,
    -- guaranteeing that they can be cleanly merged into a single 'FL' of prims.
    resolveConflicts :: RL p wO wX -> RL p wX wY -> [ConflictDetails (PrimOf p) wY]

-- | By definition, a conflicting patch is resolved if another patch
-- (that is not itself conflicted) depends on the conflict. If the
-- representation of conflicts is self-contained as it is for V1 and V2,
-- then we can calculate the maximal set of conflicting alternatives for
-- a conflict separately for each conflictor at the end of a repo.
-- This function can then be used to lift this to an 'RL' of patches.
--
-- So, when looking for conflicts in a list of patches, we go
-- through the whole list looking for individual patches that represent
-- a conflict. But then we try to commute them past all the
-- patches we've already seen. If we fail, i.e. there's something
-- that depends on the conflict, then we forget about the conflict;
-- this is the Nothing case of the 'commuteNoConflictsFL' call.
-- Otherwise the patch is now in the correct position to extract the
-- conflicting alternatives.
combineConflicts
    :: forall p wX wY. CommuteNoConflicts p
    => (forall wA wB. p wA wB -> [Unravelled (PrimOf p) wB])
    -> RL p wX wY -> [Unravelled (PrimOf p) wY]
combineConflicts :: forall (p :: * -> * -> *) wX wY.
CommuteNoConflicts p =>
(forall wA wB. p wA wB -> [Unravelled (PrimOf p) wB])
-> RL p wX wY -> [Unravelled (PrimOf p) wY]
combineConflicts forall wA wB. p wA wB -> [Unravelled (PrimOf p) wB]
resolveOne RL p wX wY
x = RL p wX wY -> FL p wY wY -> [Unravelled (PrimOf p) wY]
forall wM. RL p wX wM -> FL p wM wY -> [Unravelled (PrimOf p) wY]
rcs RL p wX wY
x FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL
  where
    rcs :: RL p wX wM -> FL p wM wY -> [Unravelled (PrimOf p) wY]
    rcs :: forall wM. RL p wX wM -> FL p wM wY -> [Unravelled (PrimOf p) wY]
rcs RL p wX wM
NilRL FL p wM wY
_ = []
    rcs (RL p wX wY
ps :<: p wY wM
p) FL p wM wY
passedby
      | [Unravelled (PrimOf p) wM] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (p wY wM -> [Unravelled (PrimOf p) wM]
forall wA wB. p wA wB -> [Unravelled (PrimOf p) wB]
resolveOne p wY wM
p) = FL p wM wY
-> [Unravelled (PrimOf p) wY] -> [Unravelled (PrimOf p) wY]
forall a b. a -> b -> b
seq FL p wM wY
passedby [Unravelled (PrimOf p) wY]
rest -- TODO why seq here?
      | Bool
otherwise =
        case CommuteFn p p -> CommuteFn p (FL p)
forall (p1 :: * -> * -> *) (p2 :: * -> * -> *).
CommuteFn p1 p2 -> CommuteFn p1 (FL p2)
commuterIdFL (:>) p p wX wY -> Maybe ((:>) p p wX wY)
CommuteFn p p
forall (p :: * -> * -> *) wX wY.
CommuteNoConflicts p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commuteNoConflicts (p wY wM
p p wY wM -> FL p wM wY -> (:>) p (FL p) wY wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wM wY
passedby) of
          Just (FL p wY wZ
_ :> p wZ wY
p') -> p wZ wY -> [Unravelled (PrimOf p) wY]
forall wA wB. p wA wB -> [Unravelled (PrimOf p) wB]
resolveOne p wZ wY
p' [Unravelled (PrimOf p) wY]
-> [Unravelled (PrimOf p) wY] -> [Unravelled (PrimOf p) wY]
forall a. [a] -> [a] -> [a]
++ [Unravelled (PrimOf p) wY]
rest
          Maybe ((:>) (FL p) p wY wY)
Nothing -> [Unravelled (PrimOf p) wY]
rest
      where
        rest :: [Unravelled (PrimOf p) wY]
rest = RL p wX wY -> FL p wY wY -> [Unravelled (PrimOf p) wY]
forall wM. RL p wX wM -> FL p wM wY -> [Unravelled (PrimOf p) wY]
rcs RL p wX wY
ps (p wY wM
p p wY wM -> FL p wM wY -> FL p wY wY
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wM wY
passedby)

-- | Find all patches in the context that conflict with a given patch,
-- commuting them to the head (past the patch in question).
--
-- This actually works by commuting the patch and its dependencies backward
-- until it becomes unconflicted, then minimizing the trailing patches by
-- re-commuting them backward as long as that keeps the patch unconflicted.
--
-- Precondition: the context must contain all conflicting patches.
findConflicting
  :: forall p wX wY wZ
   . (Commute p, Conflict p, ShowPatch p)
  => RL p wX wY
  -> p wY wZ
  -> (RL p :> p :> RL p) wX wZ
findConflicting :: forall (p :: * -> * -> *) wX wY wZ.
(Commute p, Conflict p, ShowPatch p) =>
RL p wX wY -> p wY wZ -> (:>) (RL p) (p :> RL p) wX wZ
findConflicting RL p wX wY
context p wY wZ
patch = (:>) (RL p) (FL p :> (p :> FL p)) wX wZ
-> (:>) (RL p) (p :> RL p) wX wZ
forall wA wB.
(:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
go (RL p wX wY
context RL p wX wY
-> (:>) (FL p) (p :> FL p) wY wZ
-> (:>) (RL p) (FL p :> (p :> FL p)) wX wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wY
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL FL p wY wY -> (:>) p (FL p) wY wZ -> (:>) (FL p) (p :> FL p) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
patch p wY wZ -> FL p wZ wZ -> (:>) p (FL p) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wZ
forall (a :: * -> * -> *) wX. FL a wX wX
NilFL) where
  go :: (RL p :> FL p :> p :> FL p) wA wB -> (RL p :> p :> RL p) wA wB
  go :: forall wA wB.
(:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
go (RL p wA wZ
ctx :> FL p wZ wZ
deps :> p wZ wZ
p :> FL p wZ wB
nondeps)
    | Bool -> Bool
not (p wZ wZ -> Bool
forall wX wY. p wX wY -> Bool
forall (p :: * -> * -> *) wX wY. Conflict p => p wX wY -> Bool
isConflicted p wZ wZ
p) = (:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
prune (RL p wA wZ
ctx RL p wA wZ -> FL p wZ wZ -> RL p wA wZ
forall (p :: * -> * -> *) wX wY wZ.
RL p wX wY -> FL p wY wZ -> RL p wX wZ
+<<+ FL p wZ wZ
deps RL p wA wZ
-> (:>) p (RL p :> FL p) wZ wB
-> (:>) (RL p) (p :> (RL p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p p wZ wZ -> (:>) (RL p) (FL p) wZ wB -> (:>) p (RL p :> FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
forall (a :: * -> * -> *) wX. RL a wX wX
NilRL RL p wZ wZ -> FL p wZ wB -> (:>) (RL p) (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
nondeps)
  go (RL p wA wZ
NilRL :> FL p wZ wZ
deps :> p wZ wZ
p :> FL p wZ wB
nondeps) =
    [Char] -> (:>) (RL p) (p :> RL p) wA wB
forall a. HasCallStack => [Char] -> a
error ([Char] -> (:>) (RL p) (p :> RL p) wA wB)
-> [Char] -> (:>) (RL p) (p :> RL p) wA wB
forall a b. (a -> b) -> a -> b
$ Doc -> [Char]
renderString (Doc -> [Char]) -> Doc -> [Char]
forall a b. (a -> b) -> a -> b
$ [Char] -> Doc
text [Char]
"precondition violated:" Doc -> Doc -> Doc
$$
      [Doc] -> Doc
vcat ((forall wW wZ. p wW wZ -> Doc) -> FL p wZ wZ -> [Doc]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL (ShowPatchFor -> p wW wZ -> Doc
forall wX wY. ShowPatchFor -> p wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
ForStorage) FL p wZ wZ
deps) Doc -> Doc -> Doc
$$
      [Char] -> Doc
text [Char]
"===============" Doc -> Doc -> Doc
$$
      [Char] -> Doc
text [Char]
"patch:" Doc -> Doc -> Doc
$$ (ShowPatchFor -> p wZ wZ -> Doc
forall wX wY. ShowPatchFor -> p wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
ForStorage) p wZ wZ
p Doc -> Doc -> Doc
$$
      [Char] -> Doc
text [Char]
"===============" Doc -> Doc -> Doc
$$
      [Doc] -> Doc
vcat ((forall wW wZ. p wW wZ -> Doc) -> FL p wZ wB -> [Doc]
forall (a :: * -> * -> *) b wX wY.
(forall wW wZ. a wW wZ -> b) -> FL a wX wY -> [b]
mapFL (ShowPatchFor -> p wW wZ -> Doc
forall wX wY. ShowPatchFor -> p wX wY -> Doc
forall (p :: * -> * -> *) wX wY.
ShowPatchBasic p =>
ShowPatchFor -> p wX wY -> Doc
showPatch ShowPatchFor
ForStorage) FL p wZ wB
nondeps)
  go (RL p wA wY
cs :<: p wY wZ
c :> FL p wZ wZ
deps :> p wZ wZ
p :> FL p wZ wB
nondeps) =
    case (:>) p (FL p) wY wZ -> Maybe ((:>) (FL p) p wY wZ)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p (FL p) wX wY -> Maybe ((:>) (FL p) p wX wY)
commuteFL (p wY wZ
c p wY wZ -> FL p wZ wZ -> (:>) p (FL p) wY wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wZ
deps) of
      Maybe ((:>) (FL p) p wY wZ)
Nothing -> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
go (RL p wA wY
cs RL p wA wY
-> (:>) (FL p) (p :> FL p) wY wB
-> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
c p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
deps FL p wY wZ -> (:>) p (FL p) wZ wB -> (:>) (FL p) (p :> FL p) wY wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p p wZ wZ -> FL p wZ wB -> (:>) p (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
nondeps)
      Just (FL p wY wZ
deps' :> p wZ wZ
c') ->
        case (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ)
forall wX wY. (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wZ
c' p wZ wZ -> p wZ wZ -> (:>) p p wZ wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p) of
          Maybe ((:>) p p wZ wZ)
Nothing -> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
go (RL p wA wY
cs RL p wA wY
-> (:>) (FL p) (p :> FL p) wY wB
-> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wY wZ
c p wY wZ -> FL p wZ wZ -> FL p wY wZ
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wZ
deps FL p wY wZ -> (:>) p (FL p) wZ wB -> (:>) (FL p) (p :> FL p) wY wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p p wZ wZ -> FL p wZ wB -> (:>) p (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wZ wB
nondeps)
          Just (p wZ wZ
p' :> p wZ wZ
c'') -> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (FL p :> (p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
go (RL p wA wY
cs RL p wA wY
-> (:>) (FL p) (p :> FL p) wY wB
-> (:>) (RL p) (FL p :> (p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wZ
deps' FL p wY wZ -> (:>) p (FL p) wZ wB -> (:>) (FL p) (p :> FL p) wY wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p' p wZ wZ -> FL p wZ wB -> (:>) p (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
c'' p wZ wZ -> FL p wZ wB -> FL p wZ wB
forall (a :: * -> * -> *) wX wY wZ.
a wX wY -> FL a wY wZ -> FL a wX wZ
:>: FL p wZ wB
nondeps)
  prune :: (RL p :> p :> RL p :> FL p) wA wB -> (RL p :> p :> RL p) wA wB
  prune :: forall wA wB.
(:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
prune (RL p wA wZ
ctx :> p wZ wZ
p :> RL p wZ wZ
rs :> FL p wZ wB
NilFL) = RL p wA wZ
ctx RL p wA wZ -> (:>) p (RL p) wZ wB -> (:>) (RL p) (p :> RL p) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p p wZ wZ -> RL p wZ wB -> (:>) p (RL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wB
RL p wZ wZ
rs
  prune (RL p wA wZ
ctx :> p wZ wZ
p :> RL p wZ wZ
rs :> p wZ wY
n :>: FL p wY wB
ns)
    | Just (p wZ wZ
n' :> RL p wZ wY
rs') <- (:>) (RL p) p wZ wY -> Maybe ((:>) p (RL p) wZ wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) (RL p) p wX wY -> Maybe ((:>) p (RL p) wX wY)
commuteRL (RL p wZ wZ
rs RL p wZ wZ -> p wZ wY -> (:>) (RL p) p wZ wY
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wY
n)
    , Just (p wZ wZ
n'' :> p wZ wZ
p') <- (:>) p p wZ wZ -> Maybe ((:>) p p wZ wZ)
forall wX wY. (:>) p p wX wY -> Maybe ((:>) p p wX wY)
forall (p :: * -> * -> *) wX wY.
Commute p =>
(:>) p p wX wY -> Maybe ((:>) p p wX wY)
commute (p wZ wZ
p p wZ wZ -> p wZ wZ -> (:>) p p wZ wZ
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
n')
    , Bool -> Bool
not (p wZ wZ -> Bool
forall wX wY. p wX wY -> Bool
forall (p :: * -> * -> *) wX wY. Conflict p => p wX wY -> Bool
isConflicted p wZ wZ
p') = (:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
prune (RL p wA wZ
ctx RL p wA wZ -> p wZ wZ -> RL p wA wZ
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wZ
n'' RL p wA wZ
-> (:>) p (RL p :> FL p) wZ wB
-> (:>) (RL p) (p :> (RL p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p' p wZ wZ -> (:>) (RL p) (FL p) wZ wB -> (:>) p (RL p :> FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wY
rs' RL p wZ wY -> FL p wY wB -> (:>) (RL p) (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wB
ns)
    | Bool
otherwise = (:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
forall wA wB.
(:>) (RL p) (p :> (RL p :> FL p)) wA wB
-> (:>) (RL p) (p :> RL p) wA wB
prune (RL p wA wZ
ctx RL p wA wZ
-> (:>) p (RL p :> FL p) wZ wB
-> (:>) (RL p) (p :> (RL p :> FL p)) wA wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> p wZ wZ
p p wZ wZ -> (:>) (RL p) (FL p) wZ wB -> (:>) p (RL p :> FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> RL p wZ wZ
rs RL p wZ wZ -> p wZ wY -> RL p wZ wY
forall (a :: * -> * -> *) wX wY wZ.
RL a wX wY -> a wY wZ -> RL a wX wZ
:<: p wZ wY
n RL p wZ wY -> FL p wY wB -> (:>) (RL p) (FL p) wZ wB
forall (a1 :: * -> * -> *) (a2 :: * -> * -> *) wX wY wZ.
a1 wX wZ -> a2 wZ wY -> (:>) a1 a2 wX wY
:> FL p wY wB
ns)