module Test.Credit.Deque.ImplicitCat where

import Prelude hiding (head, tail, concat)
import Control.Monad (join, when)
import Prettyprinter (Pretty)
import Control.Monad.Credit
import Test.Credit
import Test.Credit.Deque.Base
import qualified Test.Credit.Deque.Base as D
import qualified Test.Credit.Deque.Bankers as D

data ImplicitCat a m
  = Shallow (D.BDeque a m)
  | Deep (D.BDeque a m) -- ^ (>= 3 elements)
         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
         (D.BDeque a m) -- ^ (>= 2 elements)
         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
         (D.BDeque a m) -- ^ (>= 3 elements)

data ILazyCon m a where
  IPay :: (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)) -> m b -> ILazyCon m b
  ILazy :: m a -> ILazyCon m a

instance MonadCredit m => HasStep (ILazyCon m) m where
  step :: forall a. ILazyCon m a -> m a
step (IPay Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
_ m a
m) = m a
m
  step (ILazy m a
m) = m a
m

data CmpdElem a m
  = Simple (D.BDeque a m)
  | Cmpd (D.BDeque a m) -- ^ (>= 2 elements)
         (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
         (D.BDeque a m) -- ^ (>= 2 elements)

-- The O(1) unshared cost of operations
-- Each thunk in the program requires at most 5 * cost credits to run
-- except for the thunks returned by uncons/unsnoc which require
-- 6 * cost credits to run.
cost :: Credit
cost :: Credit
cost = Credit
3 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
forall a. HasCallStack => a
undefined (Any -> DequeOp Any
forall a. a -> DequeOp a
Cons Any
forall a. HasCallStack => a
undefined) Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
forall a. HasCallStack => a
undefined DequeOp Any
forall a. DequeOp a
Uncons)

deepDanger :: D.BDeque a m -> Credit
deepDanger :: forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
d = if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 then Credit
cost else Credit
0

deep :: MonadCredit m
     => D.BDeque a m
     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
     -> D.BDeque a m
     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
     -> D.BDeque a m
     -> m (ImplicitCat a m)
deep :: forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r = do
  -- a `hasAtLeast` (4 * deepDanger f + deepDanger r)
  -- b `hasAtLeast` (deepDanger f + 4 * deepDanger r)
  ImplicitCat a m -> m (ImplicitCat a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImplicitCat a m -> m (ImplicitCat a m))
-> ImplicitCat a m -> m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> ImplicitCat a m
forall a (m :: * -> *).
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> ImplicitCat a m
Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r

icreditWith :: MonadCredit m => Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
icreditWith :: forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
icreditWith Thunk m (ILazyCon m) (ImplicitCat a m)
t Credit
c = do
  Thunk m (ILazyCon m) (ImplicitCat a m)
-> (ImplicitCat a m -> m ())
-> (ILazyCon m (ImplicitCat a m) -> m ())
-> m ()
forall (m :: * -> *) (t :: * -> *) a b.
MonadLazy m =>
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
forall (t :: * -> *) a b.
Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b
lazymatch Thunk m (ILazyCon m) (ImplicitCat a m)
t (\ImplicitCat a m
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()) ((ILazyCon m (ImplicitCat a m) -> m ()) -> m ())
-> (ILazyCon m (ImplicitCat a m) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \ILazyCon m (ImplicitCat a m)
t'' -> case ILazyCon m (ImplicitCat a m)
t'' of
    ILazy m (ImplicitCat a m)
_ ->   Thunk m (ILazyCon m) (ImplicitCat a m)
t  Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
forall (m :: * -> *) (t :: * -> *) a.
MonadCredit m =>
Thunk m t a -> Credit -> m ()
forall (t :: * -> *) a. Thunk m t a -> Credit -> m ()
`creditWith` Credit
c
    IPay Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
t' m (ImplicitCat a m)
_ -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
t' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) (t :: * -> *) a.
MonadCredit m =>
Thunk m t a -> Credit -> m ()
forall (t :: * -> *) a. Thunk m t a -> Credit -> m ()
`creditWith` Credit
c

cmpdDanger :: D.BDeque a m -> Credit
cmpdDanger :: forall a (m :: * -> *). BDeque a m -> Credit
cmpdDanger BDeque a m
d = if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 then Credit
cost else Credit
0

cmpd :: MonadCredit m
     => D.BDeque a m
     -> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
     -> D.BDeque a m
     -> m (CmpdElem a m)
cmpd :: forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (CmpdElem a m)
cmpd BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c BDeque a m
r = CmpdElem a m -> m (CmpdElem a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (CmpdElem a m -> m (CmpdElem a m))
-> CmpdElem a m -> m (CmpdElem a m)
forall a b. (a -> b) -> a -> b
$ BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> CmpdElem a m
forall a (m :: * -> *).
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> CmpdElem a m
Cmpd BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c BDeque a m
r

isEmpty :: ImplicitCat a m -> Bool
isEmpty :: forall a (m :: * -> *). ImplicitCat a m -> Bool
isEmpty (Shallow BDeque a m
d) = BDeque a m -> Bool
forall a (m :: * -> *). BDeque a m -> Bool
D.isEmpty BDeque a m
d
isEmpty (Deep BDeque a m
_ Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
_ BDeque a m
_ Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
_ BDeque a m
_) = Bool
False

share :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m, D.BDeque a m, D.BDeque a m)
share :: forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m, BDeque a m, BDeque a m)
share BDeque a m
f BDeque a m
r = do
  Maybe (BDeque a m, a)
fu <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
f
  Maybe (a, BDeque a m)
ru <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
r
  case (Maybe (BDeque a m, a)
fu, Maybe (a, BDeque a m)
ru) of
    (Just (BDeque a m
fi, a
fl), Just (a
rh, BDeque a m
rt)) -> do
      BDeque a m
m <- a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
fl (BDeque a m -> m (BDeque a m)) -> m (BDeque a m) -> m (BDeque a m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
rh (BDeque a m -> m (BDeque a m)) -> m (BDeque a m) -> m (BDeque a m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< m (BDeque a m)
forall (m :: * -> *) a. MonadInherit m => m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
D.empty
      (BDeque a m, BDeque a m, BDeque a m)
-> m (BDeque a m, BDeque a m, BDeque a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((BDeque a m, BDeque a m, BDeque a m)
 -> m (BDeque a m, BDeque a m, BDeque a m))
-> (BDeque a m, BDeque a m, BDeque a m)
-> m (BDeque a m, BDeque a m, BDeque a m)
forall a b. (a -> b) -> a -> b
$ (BDeque a m
fi, BDeque a m
m, BDeque a m
rt)
    (Maybe (BDeque a m, a), Maybe (a, BDeque a m))
_ -> String -> m (BDeque a m, BDeque a m, BDeque a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"share: empty deque"

dappendL :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)
dappendL :: forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
d1 BDeque a m
d2 = do
  Maybe (BDeque a m, a)
d1' <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
d1
  case Maybe (BDeque a m, a)
d1' of
    Maybe (BDeque a m, a)
Nothing -> BDeque a m -> m (BDeque a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BDeque a m
d2
    Just (BDeque a m
d1i, a
d1l) -> BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
d1i (BDeque a m -> m (BDeque a m)) -> m (BDeque a m) -> m (BDeque a m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
d1l BDeque a m
d2

dappendR :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)
dappendR :: forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
d1 BDeque a m
d2 = do
  Maybe (a, BDeque a m)
d2' <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
d2
  case Maybe (a, BDeque a m)
d2' of
    Maybe (a, BDeque a m)
Nothing -> BDeque a m -> m (BDeque a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BDeque a m
d1
    Just (a
d2h, BDeque a m
d2t) -> m (m (BDeque a m)) -> m (BDeque a m)
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (m (m (BDeque a m)) -> m (BDeque a m))
-> m (m (BDeque a m)) -> m (BDeque a m)
forall a b. (a -> b) -> a -> b
$ BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR (BDeque a m -> BDeque a m -> m (BDeque a m))
-> m (BDeque a m) -> m (BDeque a m -> m (BDeque a m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> a -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> a -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
D.snoc BDeque a m
d1 a
d2h m (BDeque a m -> m (BDeque a m))
-> m (BDeque a m) -> m (m (BDeque a m))
forall a b. m (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> BDeque a m -> m (BDeque a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure BDeque a m
d2t

-- 5 * cost
concat' :: MonadInherit m => ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' (Shallow BDeque a m
d1) (Shallow BDeque a m
d2) = do
  if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
4 then BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
d1 BDeque a m
d2
  else if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
4 then BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
d1 BDeque a m
d2
  else do
    (BDeque a m
f, BDeque a m
m, BDeque a m
r) <- BDeque a m -> BDeque a m -> m (BDeque a m, BDeque a m, BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m, BDeque a m, BDeque a m)
share BDeque a m
d1 BDeque a m
d2
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
e <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. MonadInherit m => m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
empty
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
e BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
e BDeque a m
r
concat' (Shallow BDeque a m
d) (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = do
  if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
4 then do
    BDeque a m
df <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
d BDeque a m
f
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
df Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
  else do
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
fa <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
5 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
      CmpdElem a m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
cons (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
f) (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
fa Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
fa Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
d Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
fa BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
concat' (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) (Shallow BDeque a m
d) = do
  if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
d Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
4 then do
    BDeque a m
rd <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
r BDeque a m
d
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
rd
  else do
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
br <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
5 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
      (ImplicitCat (CmpdElem a m) m
-> CmpdElem a m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
`snoc` (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
r)) (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
br Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
br Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
br BDeque a m
d
concat' (Deep BDeque a m
f1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1 BDeque a m
m1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b1 BDeque a m
r1) (Deep BDeque a m
f2 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a2 BDeque a m
m2 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2 BDeque a m
r2) = do
  (BDeque a m
r1', BDeque a m
m, BDeque a m
f2') <- BDeque a m -> BDeque a m -> m (BDeque a m, BDeque a m, BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m, BDeque a m, BDeque a m)
share BDeque a m
r1 BDeque a m
f2
  -- Discharge debits on b1, a2 for compound element
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
f1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3 Bool -> Bool -> Bool
&& BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
r1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
f2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3 Bool -> Bool -> Bool
&& BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
r2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a2 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  CmpdElem a m
c1 <- BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (CmpdElem a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (CmpdElem a m)
cmpd BDeque a m
m1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b1 BDeque a m
r1'
  CmpdElem a m
c2 <- BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (CmpdElem a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (CmpdElem a m)
cmpd BDeque a m
f2' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a2 BDeque a m
m2
  Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f1))
    (ImplicitCat (CmpdElem a m) m
-> CmpdElem a m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
`snoc` CmpdElem a m
c1) (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1
  Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r2))
    CmpdElem a m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
cons CmpdElem a m
c2 (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2
  -- Discharge debits for snoc/cons onto a1/b2
  Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  -- Discharge the debit from swapping f/r
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
f1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 Bool -> Bool -> Bool
&& BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
f2 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
r2 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
3 Bool -> Bool -> Bool
&& BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
r1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
3) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
  -- Notice that only two of the when-statements
  -- can be true at the same time.
  -- So we only discharge 4 debits.
  BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f1 Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a1' BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b2' BDeque a m
r2

replaceHead :: MonadInherit m => a -> ImplicitCat a m -> m (ImplicitCat a m)
replaceHead :: forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
replaceHead a
x (Shallow BDeque a m
d) = do
  Maybe (a, BDeque a m)
d' <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
d
  case Maybe (a, BDeque a m)
d' of
    Maybe (a, BDeque a m)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"replaceHead: empty deque"
    Just (a
_, BDeque a m
d') -> BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
x BDeque a m
d'
replaceHead a
x (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = do
  Maybe (a, BDeque a m)
f' <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
f
  case Maybe (a, BDeque a m)
f' of
    Maybe (a, BDeque a m)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"replaceHead: empty deque"
    Just (a
_, BDeque a m
f') -> do
      BDeque a m
f' <- a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
x BDeque a m
f'
      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r

-- 6 * cost + 1 tick
-- TODO: is there an off-by-one error here?
-- We assign 5 * cost to other thunks and also perform 1 * cost of work.
-- So the cost of the thunk is 6 * cost, not 5 * cost as claimed by Okasaki.
-- In particular consider the case where a = empty and uncons b returns a compound element.
-- Here we need to assign an extra 1 * cost to the bt thunk, but we can't possibly pay for that.
-- Does that mean that this function is not amortized O(1)?
-- This doesn't show up in the testsuite, because we never concat two deep deques
-- and so we never generate a deque with a compound element.
uncons' :: MonadInherit m => ImplicitCat a m -> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
uncons' :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
uncons' (Shallow BDeque a m
d) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
  Maybe (a, BDeque a m)
m <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
d
  case Maybe (a, BDeque a m)
m of
    Maybe (a, BDeque a m)
Nothing -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall a. Maybe a
Nothing
    Just (a
x, BDeque a m
d') -> (Thunk m (ILazyCon m) (ImplicitCat a m)
 -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a, Thunk m (ILazyCon m) (ImplicitCat a m))
-> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall a. a -> Maybe a
Just ((a, Thunk m (ILazyCon m) (ImplicitCat a m))
 -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> (Thunk m (ILazyCon m) (ImplicitCat a m)
    -> (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> Thunk m (ILazyCon m) (ImplicitCat a m)
-> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) (m (Thunk m (ILazyCon m) (ImplicitCat a m))
 -> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. (a -> b) -> a -> b
$ ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat a m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat a m)))
-> ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m))
-> m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ do
      ImplicitCat a m -> m (ImplicitCat a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImplicitCat a m -> m (ImplicitCat a m))
-> ImplicitCat a m -> m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
d'
uncons' (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
  Maybe (a, BDeque a m)
f' <- BDeque a m -> m (Maybe (a, BDeque a m))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (a, BDeque a m))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (a, q a m))
D.uncons BDeque a m
f
  case Maybe (a, BDeque a m)
f' of
    Maybe (a, BDeque a m)
Nothing -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall a. Maybe a
Nothing
    Just (a
x, BDeque a m
f') -> (Thunk m (ILazyCon m) (ImplicitCat a m)
 -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a, Thunk m (ILazyCon m) (ImplicitCat a m))
-> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall a. a -> Maybe a
Just ((a, Thunk m (ILazyCon m) (ImplicitCat a m))
 -> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> (Thunk m (ILazyCon m) (ImplicitCat a m)
    -> (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
-> Thunk m (ILazyCon m) (ImplicitCat a m)
-> Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,)) (m (Thunk m (ILazyCon m) (ImplicitCat a m))
 -> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall a b. (a -> b) -> a -> b
$ ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat a m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat a m)))
-> ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m))
-> m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ do
      if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
f' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3 -- iff D.size f > 3
        then do
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f')
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f')
          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
        else do -- D.size f' == 2
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
          ImplicitCat (CmpdElem a m) m
a <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a
          if Bool -> Bool
not (ImplicitCat (CmpdElem a m) m -> Bool
forall a (m :: * -> *). ImplicitCat a m -> Bool
isEmpty ImplicitCat (CmpdElem a m) m
a)
            then do
              Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
a' <- ImplicitCat (CmpdElem a m) m
-> m (Maybe
        (CmpdElem a m,
         Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
uncons' ImplicitCat (CmpdElem a m) m
a
              case Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
a' of
                Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"uncons': a cannot be empty"
                Just (CmpdElem a m
ah, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
at) -> do
                  case CmpdElem a m
ah of
                    Simple BDeque a m
d -> do
                      BDeque a m
f'' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
f' BDeque a m
d -- cost: 2 * (cons + unsnoc)
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
at Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
at Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
at BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
                    Cmpd BDeque a m
f'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' BDeque a m
r' -> do
                      BDeque a m
f''' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
f' BDeque a m
f'' -- cost: 2 * (cons + unsnoc)
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                        ImplicitCat (CmpdElem a m) m
c'' <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c'
                        ImplicitCat (CmpdElem a m) m
ra <- CmpdElem a m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
replaceHead (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
r') ImplicitCat (CmpdElem a m) m
a -- cost: uncons + cons
                        ImplicitCat (CmpdElem a m) m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' ImplicitCat (CmpdElem a m) m
c'' ImplicitCat (CmpdElem a m) m
ra
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f''' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
            else do
              Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r))
              ImplicitCat (CmpdElem a m) m
b <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b
              if Bool -> Bool
not (ImplicitCat (CmpdElem a m) m -> Bool
forall a (m :: * -> *). ImplicitCat a m -> Bool
isEmpty ImplicitCat (CmpdElem a m) m
b)
                then do
                  Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
b' <- ImplicitCat (CmpdElem a m) m
-> m (Maybe
        (CmpdElem a m,
         Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
uncons' ImplicitCat (CmpdElem a m) m
b
                  case Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
b' of
                    Maybe
  (CmpdElem a m, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"uncons': b cannot be empty"
                    Just (CmpdElem a m
bh, Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt) -> do
                      case CmpdElem a m
bh of
                        Simple BDeque a m
d -> do
                          BDeque a m
f'' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
f' BDeque a m
m -- cost: 2 * (cons + unsnoc)
                          -- TODO: this is ugly. Since bt has 6 * cost debits
                          -- we need to assign 1 * cost extra credits to it. But we
                          -- can not pay for that. Instead, we redirect credits
                          -- passed to a to be sent to bt. Once r is in deepDanger,
                          -- it will pass one credit to a, which is redirected to bt.
                          -- This ensures that bt receives 6 * cost credits by the
                          -- time it is forced.
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b.
Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m b -> ILazyCon m b
IPay Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                            (BDeque (CmpdElem a m) m -> ImplicitCat (CmpdElem a m) m)
-> m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BDeque (CmpdElem a m) m -> ImplicitCat (CmpdElem a m) m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m))
-> m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ m (BDeque (CmpdElem a m) m)
forall (m :: * -> *) a. MonadInherit m => m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
empty
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
d Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt BDeque a m
r
                        Cmpd BDeque a m
f'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' BDeque a m
r' -> do
                          BDeque a m
f''' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
f' BDeque a m
m -- cost: 2 * (cons + unsnoc)
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                            Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
                            CmpdElem a m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
cons (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
f'') (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c'
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r)
                          -- TODO: Here bt has too many debits: it gets 6 * cost
                          -- debits from uncons', but may only have 5 * cost.
                          -- We have already exhausted the credits on the current
                          -- thunk and cannot pay for the extra 1 * cost.
                          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f''' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a'' BDeque a m
r' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bt BDeque a m
r
                else do -- 1 * cost
                  BDeque a m
fm <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendL BDeque a m
f' BDeque a m
m
                  ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' (BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
fm) (BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
r)

replaceLast :: MonadInherit m => ImplicitCat a m -> a -> m (ImplicitCat a m)
replaceLast :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
replaceLast (Shallow BDeque a m
d) a
x = do
  Maybe (BDeque a m, a)
d' <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
d
  case Maybe (BDeque a m, a)
d' of
    Maybe (BDeque a m, a)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"replaceLast: empty deque"
    Just (BDeque a m
d', a
_) -> BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> a -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> a -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
D.snoc BDeque a m
d' a
x
replaceLast (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) a
x = do
  Maybe (BDeque a m, a)
r' <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
r
  case Maybe (BDeque a m, a)
r' of
    Maybe (BDeque a m, a)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"replaceLast: empty deque"
    Just (BDeque a m
r', a
_) -> do
      BDeque a m
r' <- BDeque a m -> a -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> a -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
D.snoc BDeque a m
r' a
x
      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r'

unsnoc' :: MonadInherit m => ImplicitCat a m -> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
unsnoc' :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
unsnoc' (Shallow BDeque a m
d) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
  Maybe (BDeque a m, a)
m <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
d
  case Maybe (BDeque a m, a)
m of
    Maybe (BDeque a m, a)
Nothing -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall a. Maybe a
Nothing
    Just (BDeque a m
d', a
x) -> (Thunk m (ILazyCon m) (ImplicitCat a m)
 -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Thunk m (ILazyCon m) (ImplicitCat a m), a)
-> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall a. a -> Maybe a
Just ((Thunk m (ILazyCon m) (ImplicitCat a m), a)
 -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> (Thunk m (ILazyCon m) (ImplicitCat a m)
    -> (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> Thunk m (ILazyCon m) (ImplicitCat a m)
-> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,a
x)) (m (Thunk m (ILazyCon m) (ImplicitCat a m))
 -> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. (a -> b) -> a -> b
$ ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat a m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat a m)))
-> ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m))
-> m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ do
      ImplicitCat a m -> m (ImplicitCat a m)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ImplicitCat a m -> m (ImplicitCat a m))
-> ImplicitCat a m -> m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
d'
unsnoc' (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m ()
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> do
  Maybe (BDeque a m, a)
r' <- BDeque a m -> m (Maybe (BDeque a m, a))
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> m (Maybe (BDeque a m, a))
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> m (Maybe (q a m, a))
D.unsnoc BDeque a m
r
  case Maybe (BDeque a m, a)
r' of
    Maybe (BDeque a m, a)
Nothing -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall a. Maybe a
Nothing
    Just (BDeque a m
r', a
x) -> (Thunk m (ILazyCon m) (ImplicitCat a m)
 -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Thunk m (ILazyCon m) (ImplicitCat a m), a)
-> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall a. a -> Maybe a
Just ((Thunk m (ILazyCon m) (ImplicitCat a m), a)
 -> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> (Thunk m (ILazyCon m) (ImplicitCat a m)
    -> (Thunk m (ILazyCon m) (ImplicitCat a m), a))
-> Thunk m (ILazyCon m) (ImplicitCat a m)
-> Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,a
x)) (m (Thunk m (ILazyCon m) (ImplicitCat a m))
 -> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)))
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall a b. (a -> b) -> a -> b
$ ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat a m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat a m)))
-> ILazyCon m (ImplicitCat a m)
-> m (Thunk m (ILazyCon m) (ImplicitCat a m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m))
-> m (ImplicitCat a m) -> ILazyCon m (ImplicitCat a m)
forall a b. (a -> b) -> a -> b
$ do
      if BDeque a m -> Int
forall a (m :: * -> *). BDeque a m -> Int
D.size BDeque a m
r' Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
3 -- iff D.size r > 3
        then do
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r')
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
r')
          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r'
        else do
          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
          ImplicitCat (CmpdElem a m) m
b <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b
          if Bool -> Bool
not (ImplicitCat (CmpdElem a m) m -> Bool
forall a (m :: * -> *). ImplicitCat a m -> Bool
isEmpty ImplicitCat (CmpdElem a m) m
b)
            then do
              Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
b' <- ImplicitCat (CmpdElem a m) m
-> m (Maybe
        (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m),
         CmpdElem a m))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
unsnoc' ImplicitCat (CmpdElem a m) m
b
              case Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
b' of
                Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unsnoc': b cannot be empty"
                Just (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bi, CmpdElem a m
bl) -> do
                  case CmpdElem a m
bl of
                    Simple BDeque a m
d -> do
                      BDeque a m
r'' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
d BDeque a m
r'
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bi Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` Credit
cost
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bi Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
bi BDeque a m
r''
                    Cmpd BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' BDeque a m
r'' -> do
                      BDeque a m
r''' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
r'' BDeque a m
r'
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                        ImplicitCat (CmpdElem a m) m
c'' <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c'
                        ImplicitCat (CmpdElem a m) m
bf <- ImplicitCat (CmpdElem a m) m
-> CmpdElem a m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
replaceLast ImplicitCat (CmpdElem a m) m
b (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
f')
                        ImplicitCat (CmpdElem a m) m
-> ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' ImplicitCat (CmpdElem a m) m
bf ImplicitCat (CmpdElem a m) m
c''
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
                      Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                      BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' BDeque a m
r'''
            else do
              Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* (Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f))
              ImplicitCat (CmpdElem a m) m
a <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a
              if Bool -> Bool
not (ImplicitCat (CmpdElem a m) m -> Bool
forall a (m :: * -> *). ImplicitCat a m -> Bool
isEmpty ImplicitCat (CmpdElem a m) m
a)
                then do
                  Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
a' <- ImplicitCat (CmpdElem a m) m
-> m (Maybe
        (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m),
         CmpdElem a m))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
unsnoc' ImplicitCat (CmpdElem a m) m
a
                  case Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
a' of
                    Maybe
  (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m), CmpdElem a m)
Nothing -> String -> m (ImplicitCat a m)
forall a. String -> m a
forall (m :: * -> *) a. MonadFail m => String -> m a
fail String
"unsnoc': a cannot be empty"
                    Just (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai, CmpdElem a m
al) -> do
                      case CmpdElem a m
al of
                        Simple BDeque a m
d -> do
                          BDeque a m
r'' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
m BDeque a m
r'
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b.
Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m b -> ILazyCon m b
IPay Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                            (BDeque (CmpdElem a m) m -> ImplicitCat (CmpdElem a m) m)
-> m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BDeque (CmpdElem a m) m -> ImplicitCat (CmpdElem a m) m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m))
-> m (BDeque (CmpdElem a m) m) -> m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ m (BDeque (CmpdElem a m) m)
forall (m :: * -> *) a. MonadInherit m => m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
empty
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai BDeque a m
d Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r''
                        Cmpd BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' BDeque a m
r'' -> do
                          BDeque a m
r''' <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
m BDeque a m
r'
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' <- ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall (m :: * -> *) (t :: * -> *) a.
MonadLazy m =>
t a -> m (Thunk m t a)
forall (t :: * -> *) a. t a -> m (Thunk m t a)
delay (ILazyCon m (ImplicitCat (CmpdElem a m) m)
 -> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)))
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
-> m (Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m))
forall a b. (a -> b) -> a -> b
$ m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a. m a -> ILazyCon m a
ILazy (m (ImplicitCat (CmpdElem a m) m)
 -> ILazyCon m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> ILazyCon m (ImplicitCat (CmpdElem a m) m)
forall a b. (a -> b) -> a -> b
$ do
                            Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
                            (ImplicitCat (CmpdElem a m) m
-> CmpdElem a m -> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
`snoc` (BDeque a m -> CmpdElem a m
forall a (m :: * -> *). BDeque a m -> CmpdElem a m
Simple BDeque a m
r'')) (ImplicitCat (CmpdElem a m) m -> m (ImplicitCat (CmpdElem a m) m))
-> m (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> m (ImplicitCat (CmpdElem a m) m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
c'
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                          Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
4 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* BDeque a m -> Credit
forall a (m :: * -> *). BDeque a m -> Credit
deepDanger BDeque a m
f)
                          BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
ai BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b'' BDeque a m
r'''
                else do
                  BDeque a m
mr <- BDeque a m -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> BDeque a m -> m (BDeque a m)
dappendR BDeque a m
m BDeque a m
r'
                  ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' (BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
f) (BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow BDeque a m
mr)

instance Deque ImplicitCat where
  empty :: forall (m :: * -> *) a. MonadInherit m => m (ImplicitCat a m)
empty = BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> m (BDeque a m)
forall (m :: * -> *) a. MonadInherit m => m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
m (q a m)
D.empty
  cons :: forall (m :: * -> *) a.
MonadInherit m =>
a -> ImplicitCat a m -> m (ImplicitCat a m)
cons a
x (Shallow BDeque a m
d) = BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
x BDeque a m
d
  cons a
x (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = do
    BDeque a m
f' <- a -> BDeque a m -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
a -> BDeque a m -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
a -> q a m -> m (q a m)
D.cons a
x BDeque a m
f
    BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadCredit m =>
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> m (ImplicitCat a m)
deep BDeque a m
f' Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r
  snoc :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> a -> m (ImplicitCat a m)
snoc (Shallow BDeque a m
d) a
x = BDeque a m -> ImplicitCat a m
forall a (m :: * -> *). BDeque a m -> ImplicitCat a m
Shallow (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> a -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> a -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
D.snoc BDeque a m
d a
x
  snoc (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) a
x = BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> ImplicitCat a m
forall a (m :: * -> *).
BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
-> BDeque a m
-> ImplicitCat a m
Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b (BDeque a m -> ImplicitCat a m)
-> m (BDeque a m) -> m (ImplicitCat a m)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> BDeque a m -> a -> m (BDeque a m)
forall (m :: * -> *) a.
MonadInherit m =>
BDeque a m -> a -> m (BDeque a m)
forall (q :: * -> (* -> *) -> *) (m :: * -> *) a.
(Deque q, MonadInherit m) =>
q a m -> a -> m (q a m)
D.snoc BDeque a m
r a
x
  uncons :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> m (Maybe (a, ImplicitCat a m))
uncons ImplicitCat a m
d = do
    Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
m <- ImplicitCat a m
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m)))
uncons' ImplicitCat a m
d
    case Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
m of
      Maybe (a, Thunk m (ILazyCon m) (ImplicitCat a m))
Nothing -> Maybe (a, ImplicitCat a m) -> m (Maybe (a, ImplicitCat a m))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (a, ImplicitCat a m)
forall a. Maybe a
Nothing
      Just (a
x, Thunk m (ILazyCon m) (ImplicitCat a m)
t) -> do
        Thunk m (ILazyCon m) (ImplicitCat a m)
t Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
6 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
        (a, ImplicitCat a m) -> Maybe (a, ImplicitCat a m)
forall a. a -> Maybe a
Just ((a, ImplicitCat a m) -> Maybe (a, ImplicitCat a m))
-> (ImplicitCat a m -> (a, ImplicitCat a m))
-> ImplicitCat a m
-> Maybe (a, ImplicitCat a m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (a
x,) (ImplicitCat a m -> Maybe (a, ImplicitCat a m))
-> m (ImplicitCat a m) -> m (Maybe (a, ImplicitCat a m))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Thunk m (ILazyCon m) (ImplicitCat a m) -> m (ImplicitCat a m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat a m)
t
  unsnoc :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> m (Maybe (ImplicitCat a m, a))
unsnoc ImplicitCat a m
d = do
    Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
m <- ImplicitCat a m
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m
-> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))
unsnoc' ImplicitCat a m
d
    case Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
m of
      Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a)
Nothing -> Maybe (ImplicitCat a m, a) -> m (Maybe (ImplicitCat a m, a))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (ImplicitCat a m, a)
forall a. Maybe a
Nothing
      Just (Thunk m (ILazyCon m) (ImplicitCat a m)
t, a
x) -> do
        Thunk m (ILazyCon m) (ImplicitCat a m)
t Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
forall (m :: * -> *) a.
MonadCredit m =>
Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()
`icreditWith` (Credit
6 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost)
        (ImplicitCat a m, a) -> Maybe (ImplicitCat a m, a)
forall a. a -> Maybe a
Just ((ImplicitCat a m, a) -> Maybe (ImplicitCat a m, a))
-> (ImplicitCat a m -> (ImplicitCat a m, a))
-> ImplicitCat a m
-> Maybe (ImplicitCat a m, a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (,a
x) (ImplicitCat a m -> Maybe (ImplicitCat a m, a))
-> m (ImplicitCat a m) -> m (Maybe (ImplicitCat a m, a))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Thunk m (ILazyCon m) (ImplicitCat a m) -> m (ImplicitCat a m)
forall (m :: * -> *) (t :: * -> *) a.
(MonadLazy m, HasStep t m) =>
Thunk m t a -> m a
forall (t :: * -> *) a. HasStep t m => Thunk m t a -> m a
force Thunk m (ILazyCon m) (ImplicitCat a m)
t
  concat :: forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat ImplicitCat a m
xs ImplicitCat a m
ys = m ()
forall (m :: * -> *). MonadCount m => m ()
tick m () -> m (ImplicitCat a m) -> m (ImplicitCat a m)
forall a b. m a -> m b -> m b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
forall (m :: * -> *) a.
MonadInherit m =>
ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)
concat' ImplicitCat a m
xs ImplicitCat a m
ys

instance BoundedDeque ImplicitCat where
  qcost :: forall a. Size -> DequeOp a -> Credit
qcost Size
sz (Cons a
x) = forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
sz (a -> DequeOp a
forall a. a -> DequeOp a
Cons a
x)
  qcost Size
sz (Snoc a
x) = forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
sz (a -> DequeOp a
forall a. a -> DequeOp a
Snoc a
x)
  qcost Size
sz DequeOp a
Uncons = Credit
1 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ Credit
6 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
sz DequeOp Any
forall a. DequeOp a
Uncons
  qcost Size
sz DequeOp a
Unsnoc = Credit
1 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ Credit
6 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ forall (q :: * -> (* -> *) -> *) a.
BoundedDeque q =>
Size -> DequeOp a -> Credit
qcost @(D.BDeque) Size
sz DequeOp Any
forall a. DequeOp a
Unsnoc
  qcost Size
_ DequeOp a
Concat = Credit
1 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
+ Credit
5 Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
* Credit
cost

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where
  prettyCell :: ILazyCon m a -> m Memory
prettyCell ILazyCon m a
_ = Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"<lazy>" []

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CmpdElem a m) where
  prettyCell :: CmpdElem a m -> m Memory
prettyCell (Simple BDeque a m
d) = do
    Memory
d' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
d
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Simple" [Memory
d']
  prettyCell (Cmpd BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
m BDeque a m
r) = do
    Memory
f' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
f
    Memory
m' <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m) -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
m
    Memory
r' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
r
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Cmpd" [Memory
f', Memory
m', Memory
r']

instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ImplicitCat a m) where
  prettyCell :: ImplicitCat a m -> m Memory
prettyCell (Shallow BDeque a m
d) = do
    Memory
d' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
d
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Shallow" [Memory
d']
  prettyCell (Deep BDeque a m
f Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a BDeque a m
m Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b BDeque a m
r) = do
    Memory
f' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
f
    Memory
a' <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m) -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
a
    Memory
m' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
m
    Memory
b' <- Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m) -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell Thunk m (ILazyCon m) (ImplicitCat (CmpdElem a m) m)
b
    Memory
r' <- BDeque a m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell BDeque a m
r
    Memory -> m Memory
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> m Memory) -> Memory -> m Memory
forall a b. (a -> b) -> a -> b
$ String -> [Memory] -> Memory
mkMCell String
"Deep" [Memory
f', Memory
a', Memory
m', Memory
b', Memory
r']

instance Pretty a => MemoryStructure (ImplicitCat (PrettyCell a)) where
  prettyStructure :: forall (m :: * -> *).
MonadMemory m =>
ImplicitCat (PrettyCell a) m -> m Memory
prettyStructure = ImplicitCat (PrettyCell a) m -> m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell