packages feed

creditmonad (empty) → 1.0.0

raw patch · 38 files changed

+4757/−0 lines, 38 filesdep +QuickCheckdep +STMonadTransdep +base

Dependencies added: QuickCheck, STMonadTrans, base, containers, creditmonad, mtl, prettyprinter, unliftio

Files

+ CHANGELOG.md view
+ app/Implicit.hs view
@@ -0,0 +1,14 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, ImpredicativeTypes #-}++-- | Testing the code about printing implicit queues.+module Implicit where++import Control.Monad.Credit+import Test.Credit.Queue.Base+import Test.Credit.Queue.Implicit++testImplicit :: Either String (Maybe (Int, String), Ticks)+testImplicit =+  runCounterM $ (=<<) (traverse (traverse showImplicit)) $+    empty >>= (`snoc` 1) >>= (`snoc` 2) >>= (`snoc` 3)+          >>= (`snoc` 4) >>= (`snoc` 5) >>= uncons
+ app/Intro.hs view
@@ -0,0 +1,47 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}++-- | Testing the code in the introduction of the paper.+module Intro where++import Control.Monad+import System.Environment (getArgs)+import Test.QuickCheck++import Control.Monad.Credit++data Batched a = Batched [a] [a]+  deriving (Eq, Ord, Show)++rev :: MonadCount m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc)++batched :: MonadCount m => [a] -> [a] -> m (Batched a)+batched [] rear = do+  front <- rev rear []+  pure $ Batched front []+batched front rear = pure $ Batched front rear++empty :: MonadCount m => m (Batched a)+empty = pure $ Batched [] []++snoc :: MonadCount m => Batched a -> a -> m (Batched a)+snoc   (Batched front rear) x = batched front (x : rear)++uncons :: MonadCount m => Batched a -> m (Maybe (a, Batched a))+uncons (Batched [] []) = pure Nothing+uncons (Batched (x:front) rear) = do+  q' <- batched front rear+  pure $ Just (x, q')++unfoldM :: Monad m => (b -> m (Maybe (a, b))) -> b -> m [a] +unfoldM f b = do+  mb <- f b+  case mb of+    Nothing -> pure []+    Just (x, b') -> (x :) <$> unfoldM f b'++testBatched :: Either String ([Int], Ticks)+testBatched =+  runCounterM $ empty >>= flip (foldM snoc) [1..10]+                      >>= unfoldM uncons
+ app/Main.hs view
@@ -0,0 +1,137 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, DerivingStrategies #-}++module Main where++import UnliftIO.Internals.Async+import System.Environment (getArgs)+import Test.QuickCheck+import Prettyprinter++import Control.Monad.Credit+import Test.Credit+import Test.Credit.Queue.Base+import Test.Credit.Queue.Batched+import Test.Credit.Queue.Bankers+import Test.Credit.Queue.Physicists+import Test.Credit.Queue.Realtime+import Test.Credit.Queue.Bootstrapped+import Test.Credit.Queue.Implicit+import Test.Credit.Deque.Base+import Test.Credit.Deque.Bankers+import Test.Credit.Deque.Realtime+import Test.Credit.Deque.Catenable+import Test.Credit.Deque.SimpleCat+import Test.Credit.Deque.ImplicitCat+import Test.Credit.Finger+import Test.Credit.Heap.Base+import Test.Credit.Heap.Binomial+import Test.Credit.Heap.LazyPairing+import Test.Credit.Heap.Scheduled+import Test.Credit.Sortable.Base+import Test.Credit.Sortable.MergeSort+import Test.Credit.Sortable.Scheduled+import Test.Credit.RandomAccess.Base+import Test.Credit.RandomAccess.Binary+import Test.Credit.RandomAccess.Zeroless++run :: forall t op. (MemoryStructure t, DataStructure t op) => Args -> Strategy -> IO Result+run args strat = quickCheckWithResult args $ checkCreditsMemory @t strat++newtype Alpha = Alpha Char+  deriving (Eq, Ord)+  deriving newtype (Pretty)++instance Show Alpha where+  show (Alpha c) = [c]++instance Arbitrary Alpha where+  arbitrary = Alpha <$> frequency+    [ (1, choose ('a', 'z')), (1, choose ('A', 'Z')) ]++benchmarks :: Args -> [(String, IO Result)]+benchmarks args =+  [ (benchs ++ strats ++ ":", runB args strat)+  | (strats, strat) <-+      [ (" (path)", Path)+      , (" (bloom)", Bloom)+      , (" (pennant)", Pennant)+      , (" (random)", Random)+      ]+  , (benchs, runB) <- reverse+      [ ("Batched Queue", run @(Q Batched Alpha))+      , ("Bankers Queue", run @(Q BQueue Alpha))+      , ("Physicists Queue", run @(Q Physicists Alpha))+      , ("Realtime Queue", run @(Q RQueue Alpha))+      , ("Bootstrapped Queue", run @(Q Bootstrapped Alpha))+      , ("Implicit Queue", run @(Q Implicit Alpha))+      , ("Bankers Deque", run @(D BDeque Alpha))+      , ("Realtime Deque", run @(D RDeque Alpha))+      , ("Catenable List", run @(D CatDeque Alpha))+      , ("Simple Catenable Deque", run @(D SimpleCat Alpha))+      , ("Implicit Catenable Deque", run @(D ImplicitCat Alpha))+      , ("Catenable List (Concat)", run @(BD CatDeque Alpha))+      , ("Simple Catenable Deque (Concat)", run @(BD SimpleCat Alpha))+      , ("Implicit Catenable Deque (Concat)", run @(BD ImplicitCat Alpha))+      , ("Binomial Heap", run @(H Binomial Alpha))+      , ("Lazy Pairing Heap", run @(H LazyPairing Alpha))+      , ("Scheduled Binomial Heap", run @(H Scheduled Alpha))+      , ("Binomial Heap (Merge)", run @(BH Binomial Alpha))+      , ("Lazy Pairing Heap (Merge)", run @(BH LazyPairing Alpha))+      , ("Scheduled Binomial Heap (Merge)", run @(BH Scheduled Alpha))+      , ("Mergesort", run @(S MergeSort Alpha))+      , ("Scheduled Mergesort", run @(S SMergeSort Alpha))+      , ("Binary Random Access List", run @(RA BinaryRA Alpha))+      , ("Zeroless Random Access List", run @(RA ZerolessRA Alpha))+      , ("Finger Tree (Deque)", run @(D FingerDeque Alpha))+      , ("Finger Tree (Concat)", run @(BD FingerDeque Alpha))+      , ("Finger Tree (Heap)", run @(H FingerHeap Alpha))+      , ("Finger Tree (Merge)", run @(BH FingerHeap Alpha))+      , ("Finger Tree (Random Access)", run @(RA FingerRA Alpha))+      , ("Finger Tree (Sortable)", run @(S FingerSort Alpha))+      ]+  ]++main :: IO ()+main = do+  (maxSuccess, maxSize) <- do+    args <- getArgs+    case args of+      [n, s]    -> pure (read n, read s)+      [n]       -> pure (read n, 1000)+      _         -> pure (1000,   1000)+  let args = stdArgs { maxSuccess, maxSize, maxShrinks = maxBound, chatty = False }+  pooledForConcurrently_ (benchmarks args) $ \(s,r) -> do+    res <- r+    putStrLn $ s ++ "\n" ++ output res++-- Categorization of implementations:++-- Passing static credits to static reference:+--  - Realtime Queue (Section 7.2)+--  - Realtime Deque (Section 8.4.3)+--  - Scheduled Binomial Heaps (Section 7.3)+--  - Scheduled Mergesort (Section 7.4)++-- Passing static credits to dynamic reference:+--  - Implicit Queue (Section 11.1)+--  - Binary Random Access List (Section 9.2.3)+--  - Zeroless Random Access List (Section 9.2.3)+--  - Finger Tree+--  - Simple Catenable Deque (Section 11.2)+--  - Implicit Catenable Deque (Section 11.2)++-- Passing dynamic credits to static reference:+--  - Binomial Heaps (Section 6.4.1)+--  - Lazy Pairing Heaps (Section 6.5)+--  - Bottom-up Mergesort (Section 6.4.3)++-- Passing static credits to ghost reference:+--  - Bootstrapped Queue (Section 10.1.3)+--  - Physicists Queue (Section 6.4.2)++-- Requires extra traversal:+--  - Catenable List (Section 10.2.1)++-- Needs Credit Inheritance:+--  - Bankers Queue (Section 6.3.2)+--  - Bankers Deque (Section 8.4.2)
+ app/Stack.hs view
@@ -0,0 +1,61 @@+module Stack where++fn :: Int -> (a -> a) -> a -> a+fn 0 f x = x+fn n f x = fn (n - 1) f (f x)++suc :: Int -> Int+suc n = n + 1++exp1 :: Int -> Int -> Int+exp1 m n = fn m (fn n) suc 0++--++data Fun b = Unit (b -> b) | Rec (Fun b) (Fun b -> b -> b)++call :: Fun b -> b -> b+call (Unit f) x = f x+call (Rec env f) x = f env x++fn' :: Int -> Fun b -> b -> b+fn' 0 f x = x+fn' n f x = fn' (n - 1) f (call f x)++fn1 :: Int -> Fun b -> Fun b+fn1 n f = Rec f (fn' n)++exp2 :: Int -> Int -> Int+exp2 m n = call (fn' m (Unit (fn1 n)) (Unit suc)) 0++--++data Closure b where+  Exists :: a -> (a -> b -> b) -> Closure b++callC :: Closure b -> b -> b+callC (Exists x f) y = f x y++fnC :: Int -> Closure b -> b -> b+fnC 0 c x = x+fnC n c x = fnC (n - 1) c (callC c x)++fnC1 :: Int -> Closure b -> Closure b+fnC1 n c = Exists c (fnC n)++fnC1' :: Int -> () -> Closure b -> Closure b+fnC1' n () c = fnC1 n c++sucC :: () -> Int -> Int+sucC () n = n + 1++exp3 :: Int -> Int -> Int+exp3 m n = callC (fnC m (Exists () (fnC1' n)) (Exists () sucC)) 0++--++-- type Closure b c = ... | Fn (type of env) (type of env -> b -> c) | ...+-- [[\x.^n e]] = (fn, env) where+--   fn env x = [[e]]+--   env = "free vars in [[e]]"+
+ creditmonad.cabal view
@@ -0,0 +1,103 @@+cabal-version: 2.2++-- This file has been generated from package.yaml by hpack version 0.38.1.+--+-- see: https://github.com/sol/hpack++name:           creditmonad+version:        1.0.0+synopsis:       Reasoning about amortized time complexity+description:    Persistent data structures are ubiquitous in functional+                programming languages and their designers frequently have to+                reason about amortized time complexity. But proving amortized+                bounds is difficult in a persistent setting, and pen-and-paper+                proofs give little assurance of correctness, while a full+                mechanization in a proof assistant can be too involved for the+                casual user. This package defines a domain specific+                language for testing the amortized time complexity of+                persistent data structures using QuickCheck. The DSL can+                give strong evidence of correctness, while imposing low+                overhead on the user. The package includes implementations+                and tests of all lazy data structures given in Okasaki's book.+                See the paper "Lightweight Testing of Persistent Amortized Time+                Complexity in the Credit Monad" (2025) for a detailed description.+category:       Development+homepage:       https://github.com/anfelor/creditmonad#readme+bug-reports:    https://github.com/anfelor/creditmonad/issues+author:         Anton Lorenzen <anton.lorenzen@ed.ac.uk>+maintainer:     Anton Lorenzen <anton.lorenzen@ed.ac.uk>+license:        BSD-3-Clause+build-type:     Simple+extra-doc-files:+    CHANGELOG.md++source-repository head+  type: git+  location: https://github.com/anfelor/creditmonad++library+  exposed-modules:+      Control.Monad.Credit+      Test.Credit+      Test.Credit.Deque.Bankers+      Test.Credit.Deque.Base+      Test.Credit.Deque.Catenable+      Test.Credit.Deque.ImplicitCat+      Test.Credit.Deque.Realtime+      Test.Credit.Deque.SimpleCat+      Test.Credit.Deque.Streams+      Test.Credit.Finger+      Test.Credit.Heap.Base+      Test.Credit.Heap.Binomial+      Test.Credit.Heap.LazyPairing+      Test.Credit.Heap.Pairing+      Test.Credit.Heap.Scheduled+      Test.Credit.Queue.Bankers+      Test.Credit.Queue.Base+      Test.Credit.Queue.Batched+      Test.Credit.Queue.Bootstrapped+      Test.Credit.Queue.Implicit+      Test.Credit.Queue.Physicists+      Test.Credit.Queue.Realtime+      Test.Credit.Queue.Streams+      Test.Credit.RandomAccess.Base+      Test.Credit.RandomAccess.Binary+      Test.Credit.RandomAccess.Zeroless+      Test.Credit.Sortable.Base+      Test.Credit.Sortable.MergeSort+      Test.Credit.Sortable.Scheduled+  other-modules:+      Control.Monad.Credit.Base+      Control.Monad.Credit.CreditM+      Control.Monad.Credit.CounterM+  hs-source-dirs:+      src+  ghc-options: -Wall -Wno-name-shadowing+  build-depends:+      QuickCheck >=2.14 && <3+    , STMonadTrans ==0.4.*+    , base >=4.13 && <5+    , containers >=0.6 && <1.7+    , mtl ==2.3.*+    , prettyprinter ==1.7.*+  default-language: GHC2021++executable creditmonad+  main-is: Main.hs+  other-modules:+      Implicit+      Intro+      Stack+  hs-source-dirs:+      app+  ghc-options: -Wall -Wno-name-shadowing -O2 -fworker-wrapper-cbv -threaded -rtsopts+  build-depends:+      QuickCheck >=2.14 && <3+    , STMonadTrans ==0.4.*+    , base >=4.13 && <5+    , containers >=0.6 && <1.7+    , creditmonad+    , mtl ==2.3.*+    , prettyprinter ==1.7.*+    , unliftio ==0.2.*+  default-language: GHC2021
+ src/Control/Monad/Credit.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE GADTs #-}++module Control.Monad.Credit +  (+  -- * Computations with credits+    Control.Monad.Credit.Base.MonadCount(..), Control.Monad.Credit.Base.MonadLazy (..), Control.Monad.Credit.Base.HasStep(..), Control.Monad.Credit.Base.Lazy(..)+  , Control.Monad.Credit.Base.Ticks, Control.Monad.Credit.Base.Credit, Control.Monad.Credit.Base.MonadCredit(..), Control.Monad.Credit.Base.MonadInherit(..)+  -- * Counter Monad+  , Control.Monad.Credit.CounterM.CounterM, Control.Monad.Credit.CounterM.runCounterM, Control.Monad.Credit.CounterM.CounterT, Control.Monad.Credit.CounterM.runCounterT+  -- * Credit Monad+  , Control.Monad.Credit.CreditM.CreditM, Control.Monad.Credit.CreditM.runCreditM, Control.Monad.Credit.CreditM.CreditT, Control.Monad.Credit.CreditM.runCreditT+  , Control.Monad.Credit.CreditM.Error(..), Control.Monad.Credit.Base.Cell+  -- * Pretty-printing memory cells+  , Control.Monad.Credit.Base.Memory, Control.Monad.Credit.Base.mkMCell, Control.Monad.Credit.Base.mkMList, linearize+  , Control.Monad.Credit.Base.MemoryCell(..), Control.Monad.Credit.Base.MonadMemory(..), Control.Monad.Credit.Base.PrettyCell(..), Control.Monad.Credit.Base.MemoryStructure(..)+  ) where++import Control.Monad.Credit.Base+import Control.Monad.Credit.CreditM+import Control.Monad.Credit.CounterM
+ src/Control/Monad/Credit/Base.hs view
@@ -0,0 +1,202 @@+{-# LANGUAGE DerivingStrategies, TypeFamilies #-}++module Control.Monad.Credit.Base+  ( Cell(..), Credit(..), Ticks(..)+  , MonadCount(..), MonadLazy(..), MonadCredit(..), HasStep(..), Lazy(..), MonadInherit(..)+  , MTree(..), Memory(..), MemoryCell(..), MonadMemory(..), linearize, mkMCell, mkMList+  , MemoryStructure(..), PrettyCell(..)+  ) where++import Prettyprinter+import Control.Monad+import Control.Monad.State+import Data.Char+import Data.Maybe+import Data.Map (Map)+import Data.Kind (Type)+import qualified Data.Map as Map++newtype Credit = Credit Int+  deriving (Eq, Ord, Show)+  deriving newtype (Num, Enum, Real, Integral, Pretty)++newtype Cell = Cell Int+  deriving (Eq, Ord, Show)++instance Pretty Cell where+  pretty (Cell 0) = pretty "main thread"+  pretty (Cell i) = pretty "thunk" <+> pretty i++newtype Ticks = Ticks Int+  deriving (Eq, Ord, Show)+  deriving newtype (Num, Enum, Real, Integral, Pretty)++class Monad m => MonadCount m where+  tick :: m ()+  -- ^ tick consumes one credit of the current cell++class Monad m => MonadLazy m where+  data Thunk m :: (Type -> Type) -> Type -> Type+  delay :: t a -> m (Thunk m t a)+  -- ^ delay creates a new cell with the given thunk+  force :: HasStep t m => Thunk m t a -> m a+  -- ^ force retrieves and evaluates the thunk of a cell+  lazymatch :: Thunk m t a -> (a -> m b) -> (t a -> m b) -> m b+  -- ^ lazymatch can inspect the unevaluated thunk and allows us to+  -- perform an action like forcing or assigning credits.++-- | Thunks can take a step to yield a computation that evaluates to their result.+class HasStep t m where+  step :: t a -> m a++-- | A basic thunk that contains the computation to be evaluated.+-- This type can be used to express any thunk but its disadvantage is that+-- it will be printed merely as "<lazy>".+newtype Lazy m a = Lazy (m a)++instance HasStep (Lazy m) m where+  step (Lazy f) = f++-- | A computation in the credit monad has a given amounts of credits,+-- which it can spend on computation or transfer to other cells.+class (MonadCount m, MonadLazy m, MonadFail m) => MonadCredit m where+  creditWith :: Thunk m t a -> Credit -> m ()+  -- ^ creditWith transfers a given amount of credits to a cell+  hasAtLeast :: Thunk m t a -> Credit -> m ()+  -- ^ assert that a cell has at least a given amount of credits++class MonadCredit m => MonadInherit m where+  creditAllTo :: Thunk m t a -> m ()+  -- ^ creditAllTo transfers all credits to a cell and assigns it as heir++data MTree = MCell String [MTree] | MList [MTree] (Maybe MTree) | Indirection Cell++-- | A view of memory that can be pretty-printed.+data Memory = Memory+  { memoryTree :: MTree+  , memoryStore :: Map Cell (MTree, Credit)+  }++-- | Make memory cell with a given tag and a list of children.+mkMCell :: String -> [Memory] -> Memory+mkMCell d ms = Memory (MCell d (map memoryTree ms)) (Map.unions (map memoryStore ms))++-- | A special case for nicer printing of list-like datatypes.+-- ''mkMList [m1,...,mn] Nothing'' renders as ''[m1, .., mn]'', while+-- ''mkMList [m1,...,mn] (Just m)'' renders as ''[m1, .., mn] ++ m''.+mkMList :: [Memory] -> Maybe Memory -> Memory+mkMList ms mm =+  let ms' = case mm of Nothing -> ms; Just m -> ms ++ [m] in+  Memory (MList (map memoryTree ms) (fmap memoryTree mm)) (Map.unions (map memoryStore ms'))++-- | A class for pretty-printing memory cells.+class Monad m => MemoryCell m a where+  prettyCell :: a -> m Memory++instance Monad m => MemoryCell m Int where+  prettyCell i = pure $ mkMCell (show i) []++instance MemoryCell m a => MemoryCell m [a] where+  prettyCell xs = flip mkMList Nothing <$> mapM prettyCell xs++instance (MemoryCell m a, MemoryCell m b) => MemoryCell m (a, b) where+  prettyCell (a, b) = mkMCell "" <$> sequence [prettyCell a, prettyCell b]++instance (MemoryCell m a, MemoryCell m b, MemoryCell m c) => MemoryCell m (a, b, c) where+  prettyCell (a, b, c) = mkMCell "" <$> sequence [prettyCell a, prettyCell b, prettyCell c]++instance Monad m => MemoryCell m (Lazy m a) where+  prettyCell (Lazy _) = pure $ mkMCell "<lazy>" []++class Monad m => MonadMemory m where+  prettyThunk :: (MemoryCell m a, MemoryCell m (t a)) => Thunk m t a -> m Memory++instance (MonadMemory m, MemoryCell m a, MemoryCell m (t a)) => MemoryCell m (Thunk m t a) where+  prettyCell t = prettyThunk t++newtype PrettyCell a = PrettyCell a+  deriving (Eq, Ord, Show)++instance (Monad m, Pretty a) => MemoryCell m (PrettyCell a) where+  prettyCell (PrettyCell a) = pure $ mkMCell (show $ pretty a) []++class MemoryStructure t where+  prettyStructure :: MonadMemory m => t m -> m Memory++showCredit :: Credit -> String+showCredit (Credit c) = map (chr . (\n -> n - 48 + 8320) . ord) $ show c++annCredit :: Credit -> MTree -> MTree+annCredit c (MCell d ms) = MCell (d ++ showCredit c) ms+annCredit c m = m++-- | Inline memory cells that are only used once and remove them from the store +linearize :: Memory -> Memory+linearize mem = linearize' mem $ countUsages mem+  where+    countUsage :: MTree -> Map Cell Int+    countUsage (MCell _ ms) = Map.unionsWith (+) (map countUsage ms)+    countUsage (MList ms mm) =+      Map.unionsWith (+) (countUsage <$> ms ++ maybeToList mm)+    countUsage (Indirection c) = Map.singleton c 1++    countUsages :: Memory -> Map Cell Int+    countUsages (Memory mtree mstore) = Map.unionsWith (+) (countUsage mtree : map (countUsage . fst) (Map.elems mstore))++    lin :: Map Cell Int -> Map Cell (MTree, Credit) -> Cell -> State (Map Cell (MTree, Credit)) ()+    lin usages mstore c = do+      mstore' <- get+      when (Map.notMember c mstore') $+        case Map.lookup c mstore of+          Just (mtree, credit) -> do+            mtree' <- linearizeTree usages mstore mtree+            case Map.lookup c usages of+              Just 1 -> modify' $ Map.insert c (annCredit credit mtree', credit)+              _ -> modify' $ Map.insert c (mtree', credit)+          Nothing -> pure ()++    linearizeTree :: Map Cell Int -> Map Cell (MTree, Credit) -> MTree -> State (Map Cell (MTree, Credit)) MTree+    linearizeTree usages mstore (MCell d ms) = do+      ms' <- mapM (linearizeTree usages mstore) ms+      pure $ MCell d ms'+    linearizeTree usages mstore (MList ms mm) = do+      ms' <- mapM (linearizeTree usages mstore) ms+      mm' <- mapM (linearizeTree usages mstore) mm+      pure $ MList ms' mm'+    linearizeTree usages mstore (Indirection c) =+      case Map.lookup c usages of+        Just 1 -> do+          lin usages mstore c+          mstore' <- get+          pure $ case Map.lookup c mstore' of+            Just (mtree, _) -> mtree+            Nothing -> Indirection c+        _ -> pure $ Indirection c++    linearizeAll :: Map Cell Int -> Map Cell (MTree, Credit) -> Map Cell (MTree, Credit)+    linearizeAll usages mstore = Map.foldrWithKey (\k _ -> execState (lin usages mstore k)) Map.empty mstore++    removeUniques :: Map Cell Int -> Map Cell (MTree, Credit) -> Map Cell (MTree, Credit)+    removeUniques usages mstore = Map.filterWithKey (\c _ -> Map.findWithDefault 0 c usages > 1) mstore++    linearize' :: Memory -> Map Cell Int -> Memory+    linearize' (Memory mtree mstore) usages =+      let mstore' = linearizeAll usages mstore+          mtree' = evalState (linearizeTree usages mstore' mtree) mstore'+      in Memory mtree' (removeUniques usages mstore')++instance Pretty MTree where+  pretty (MCell d []) = pretty d +  pretty (MCell d ms) = pretty d <> tupled (map pretty ms)+  pretty (MList [] Nothing) = pretty "[]"+  pretty (MList [] (Just m)) = pretty m+  pretty (MList ms Nothing) = list (map pretty ms)+  pretty (MList ms (Just m)) = tupled [list (map pretty ms) <+> pretty "++" <+> pretty m]+  pretty (Indirection (Cell c)) = pretty "<" <> pretty c <> pretty ">"++instance Pretty Memory where+  pretty (Memory mtree mstore) =+    let prettyStore = case Map.toList mstore of+          [] -> mempty+          _ -> pretty "where:" <+> align (vsep (map (\((Cell c), (m, cr)) -> pretty "<" <> pretty c <> pretty "> =>" <> pretty (showCredit cr) <+> pretty m) (Map.toList mstore)))+    in pretty mtree <> line <> prettyStore
+ src/Control/Monad/Credit/CounterM.hs view
@@ -0,0 +1,103 @@+{-# LANGUAGE TypeFamilies, StandaloneDeriving, UndecidableInstances, OverloadedStrings, DerivingStrategies, MagicHash #-}++module Control.Monad.Credit.CounterM (CounterM, runCounterM, CounterT, runCounterT) where++import Prelude hiding (lookup)+import Control.Monad.Except+import Control.Monad.Identity+import Control.Monad.State.Lazy+import Control.Monad.ST.Trans++import Control.Monad.Credit.Base++-- Run computation in a state monad++-- State of the computation+-- credits: The total credits consumed so far+newtype St = St Ticks+  deriving (Eq, Ord, Show)++-- | An instance of the counter monad using ST to memoize thunks.+type CounterM s = CounterT s Identity++-- | A monad transformer on the counter monad.+-- Warning! This monad transformer includes the ST monad transformer and+-- should not be used with monads that can contain multiple answers,+-- like the list monad. Safe monads include the monads State, Reader, Writer,+-- Maybe and combinations of their corresponding monad transformers.+newtype CounterT s m a = CounterT { runT :: StateT St (ExceptT String (STT s m)) a }++instance Functor m => Functor (CounterT s m) where+  fmap f (CounterT m) = CounterT (fmap f m)++instance Monad m => Applicative (CounterT s m) where+  pure = CounterT . pure+  CounterT f <*> CounterT x = CounterT (f <*> x)++instance Monad m => Monad (CounterT s m) where+  CounterT m >>= f = CounterT (m >>= runT . f)++instance Monad m => MonadError String (CounterT s m) where+  throwError e = CounterT (throwError e)+  catchError (CounterT m) h = CounterT (catchError m (runT . h))++instance Monad m => MonadState St (CounterT s m) where+  get = CounterT get+  put s = CounterT (put s)++instance MonadTrans (CounterT s) where+  lift = CounterT . lift . lift . lift++liftST :: Monad m => STT s m a -> CounterT s m a+liftST = CounterT . lift . lift++instance Monad m => MonadFail (CounterT s m) where+  fail e = throwError e++instance Monad m => MonadCount (CounterT s m) where+  tick = do+    (St c) <- get+    put (St (c + 1))++instance Monad m => MonadLazy (CounterT s m) where+  {-# SPECIALIZE instance MonadLazy (CounterT s Identity) #-}+  {-# SPECIALIZE instance MonadLazy (CounterT s (State st)) #-}+  data Thunk (CounterT s m) t b = Thunk !(STRef s (Either (t b) b))+  delay a = do+    s <- liftST $ newSTRef (Left a)+    pure (Thunk s)+  force (Thunk t) = do+    t' <- liftST $ readSTRef t+    case t' of+      Left a -> do+        b <- step a+        liftST $ writeSTRef t (Right b)+        pure b+      Right b -> pure b+  lazymatch (Thunk t) f g = do+    t' <- liftST $ readSTRef t+    case t' of+      Right b -> f b+      Left a -> g a++instance Monad m => MonadCredit (CounterT s m) where+  {-# SPECIALIZE instance MonadCredit (CounterT s Identity) #-}+  {-# SPECIALIZE instance MonadCredit (CounterT s (State st)) #-}+  creditWith _ _ = pure ()+  hasAtLeast _ _ = pure ()++instance Monad m => MonadInherit (CounterT s m) where+  {-# SPECIALIZE instance MonadInherit (CounterT s Identity) #-}+  {-# SPECIALIZE instance MonadInherit (CounterT s (State st)) #-}+  creditAllTo _ = pure ()++runStateT' :: Monad m => StateT St m a -> m (a, Ticks)+runStateT' m = do+  (a, St c) <- runStateT m $ St 0+  pure (a, c)++runCounterT :: Monad m => (forall s. CounterT s m a) -> m (Either String (a, Ticks))+runCounterT m = runSTT $ runExceptT $ runStateT' $ runT m++runCounterM :: (forall s. CounterM s a) -> Either String (a, Ticks)+runCounterM m = runIdentity $ runSTT $ runExceptT $ runStateT' $ runT m
+ src/Control/Monad/Credit/CreditM.hs view
@@ -0,0 +1,292 @@+{-# LANGUAGE TypeFamilies, StandaloneDeriving, UndecidableInstances, OverloadedStrings, DerivingStrategies, MagicHash #-}++module Control.Monad.Credit.CreditM (CreditM, Error(..), runCreditM, CreditT, runCreditT, resetCurrentThunk) where++import Prelude hiding (lookup)+import Control.Monad.Except+import Control.Monad.Identity+import Control.Monad.State.Lazy+import Control.Monad.ST.Trans+import Data.Map (Map)+import qualified Data.Map as Map+import Data.IntMap (IntMap)+import qualified Data.IntMap as IntMap+import GHC.Exts+import Prettyprinter++import Control.Monad.Credit.Base++-- Errors++data Error+  = OutOfCredits Cell+  | InvalidAccount Cell+  | InvalidTick Cell+  | ClosedCurrent Cell+  | UserError String+  | AssertionFailed Cell Credit Credit+  deriving (Eq, Ord, Show)++-- Each memory cell has an associated amount of credits+-- Once it is evaluated, it chooses an heir to pass its credits on to++data Account = Balance+                 Int# -- ^ The amount of credits in the account+                 Int# -- ^ The number of credits consumed so far+             | Closed+             | ClosedWithHeir {-# UNPACK #-} !Cell Int#+  deriving (Eq, Ord, Show)++newtype Credits = Credits (IntMap Account)+  deriving (Eq, Ord, Show)++open :: Cell -> Credits -> Credits+open (Cell i) (Credits cm) = Credits (IntMap.insert i (Balance 0# 0#) cm)++addCredit :: Cell -> Credit -> Credits -> Credits+addCredit (Cell i) (Credit (I# n)) (Credits cm) = go i cm+  where+    go i cm =+      case IntMap.lookup i cm of+        Just (Balance avail burnt) -> Credits (IntMap.insert i (Balance (n +# avail) burnt) cm)+        Just (ClosedWithHeir (Cell h) burnt) ->+          case IntMap.lookup h cm of+            Just (ClosedWithHeir (Cell h') burnt') -> -- path halving+              go h' (IntMap.insert i (ClosedWithHeir (Cell h') (burnt +# burnt')) cm)+            _ -> go h cm+        Just Closed -> Credits cm+        Nothing -> Credits cm++subCredit :: MonadError Error m => Cell -> Credit -> Credits -> m Credits+subCredit (Cell i) (Credit (I# n)) (Credits cm) = go i cm+  where+    go i cm = case IntMap.lookup i cm of+      Just (Balance avail burnt) ->+        if isTrue# $ avail -# n <# 0#+          then throwError (OutOfCredits (Cell i))+          else pure (Credits (IntMap.insert i (Balance (avail -# n) (burnt +# n)) cm))+      Just (ClosedWithHeir (Cell h) _) -> go h cm+      Just Closed -> throwError (InvalidTick (Cell i))+      Nothing -> throwError (InvalidTick (Cell i))++-- | Close an account+close :: MonadError Error m => Cell -> Credits -> m Credits+close (Cell i) (Credits cm) = do+  case IntMap.lookup i cm of+    Just (Balance _ _) -> pure $ Credits $ IntMap.insert i Closed cm+    Just Closed -> pure $ Credits cm+    Just (ClosedWithHeir _ _) -> pure $ Credits cm+    Nothing -> throwError (InvalidAccount (Cell i))++-- | Close an account and transfer its credits to the heir.+closeWithHeir :: MonadError Error m => Cell -> Cell -> Credits -> m Credits+closeWithHeir (Cell i) h c = do+  (n, burnt) <- extractValue c+  pure $ closeAccount burnt $ addCredit h n c+  where+    closeAccount (I# burnt) (Credits cm) = Credits $ IntMap.insert i (ClosedWithHeir h burnt) cm++    extractValue (Credits cm) =+      case IntMap.findWithDefault (Balance 0# 0#) i cm of+        Balance a b -> pure (Credit (I# a), I# b)+        ClosedWithHeir _ _ -> throwError (InvalidAccount (Cell i))+        Closed -> throwError (InvalidAccount (Cell i))++singleton :: Cell -> Credit -> Credits+singleton (Cell i) (Credit (I# n)) = Credits (IntMap.singleton i (Balance n 0#))++-- Run computation in a state monad++-- State of the computation+-- me: The currently evaluated cell+-- credits: The credits of each cell+-- next: The next free cell to be allocated+data St = St {-# UNPACK #-} !Cell !Credits {-# UNPACK #-} !Int +  deriving (Eq, Ord, Show)++-- | An instance of the credit monad using ST to memoize thunks.+type CreditM s = CreditT s Identity++-- | A monad transformer on the credit monad.+-- Warning! This monad transformer includes the ST monad transformer and+-- should not be used with monads that can contain multiple answers,+-- like the list monad. Safe monads include the monads State, Reader, Writer,+-- Maybe and combinations of their corresponding monad transformers.+newtype CreditT s m a = CreditT { runT :: ExceptT Error (StateT St (STT s m)) a }++instance Functor m => Functor (CreditT s m) where+  fmap f (CreditT m) = CreditT (fmap f m)++instance Monad m => Applicative (CreditT s m) where+  pure = CreditT . pure+  CreditT f <*> CreditT x = CreditT (f <*> x)++instance Monad m => Monad (CreditT s m) where+  CreditT m >>= f = CreditT (m >>= runT . f)++instance Monad m => MonadError Error (CreditT s m) where+  throwError e = CreditT (throwError e)+  catchError (CreditT m) h = CreditT (catchError m (runT . h))++instance Monad m => MonadState St (CreditT s m) where+  get = CreditT get+  put s = CreditT (put s)++instance MonadTrans (CreditT s) where+  lift = CreditT . lift . lift . lift++liftST :: Monad m => STT s m a -> CreditT s m a+liftST = CreditT . lift . lift++getMe :: Monad m => CreditT s m Cell+getMe = do+  St me _ _ <- get+  pure me++getNext :: Monad m => CreditT s m Cell+getNext = do+  St _ _ nxt <- get+  modify' $ \(St me c _) -> St me c (nxt + 1)+  pure $ Cell nxt++withCredits :: Monad m => (Credits -> CreditT s m Credits) -> CreditT s m ()+withCredits f = do+  St _ c _ <- get+  c' <- f c+  modify' $ \(St me _ nxt) -> St me c' nxt++instance Monad m => MonadFail (CreditT s m) where+  fail e = throwError (UserError e)++instance Monad m => MonadCount (CreditT s m) where+  tick = do+    me <- getMe+    withCredits $ subCredit me 1++instance Monad m => MonadLazy (CreditT s m) where+  {-# SPECIALIZE instance MonadLazy (CreditT s Identity) #-}+  {-# SPECIALIZE instance MonadLazy (CreditT s (State st)) #-}+  data Thunk (CreditT s m) t b = Thunk !Cell !(STRef s (Either (t b) b))+  delay a = do+    i <- getNext+    withCredits $ pure . open i+    s <- liftST $ newSTRef (Left a)+    pure (Thunk i s)+  force (Thunk i t) = do+    t' <- liftST $ readSTRef t+    case t' of+      Left a -> do  -- [step] rule in the big-step semantics of the paper+        St me _ _ <- get+        modify' $ \(St _ c nxt) -> St i c nxt+        b <- step a+        modify' $ \(St _ c nxt) -> St me c nxt+        liftST $ writeSTRef t (Right b)+        withCredits $ close i+        pure b+      Right b -> pure b+  lazymatch (Thunk _ t) f g = do+    t' <- liftST $ readSTRef t+    case t' of+      Right b -> f b+      Left a -> g a++assertAtLeast :: Monad m => Cell -> Credit -> CreditT s m ()+assertAtLeast (Cell i) n = do+  St _ (Credits cm) _ <- get+  case IntMap.lookup i cm of+    Just (Balance m' _) -> do+      let m = Credit (I# m')+      if m >= n+        then pure ()+        else throwError (AssertionFailed (Cell i) n m)+    Just Closed -> pure ()+    Just (ClosedWithHeir i burnt) ->+      assertAtLeast i (n - Credit (I# burnt))+    Nothing -> throwError (InvalidAccount (Cell i))++instance Monad m => MonadCredit (CreditT s m) where+  {-# SPECIALIZE instance MonadCredit (CreditT s Identity) #-}+  {-# SPECIALIZE instance MonadCredit (CreditT s (State st)) #-}+  creditWith (Thunk i _) n =+    if n > 0 then do+      me <- getMe+      withCredits $ subCredit me n . addCredit i n+    else pure ()+  hasAtLeast (Thunk i _) n =+    assertAtLeast i n++instance Monad m => MonadInherit (CreditT s m) where+  {-# SPECIALIZE instance MonadInherit (CreditT s Identity) #-}+  {-# SPECIALIZE instance MonadInherit (CreditT s (State st)) #-}+  creditAllTo (Thunk i _) = do+    me <- getMe+    withCredits $ me `closeWithHeir` i++emptyState :: Credit -> St+emptyState n = St (Cell 0) (singleton (Cell 0) n) 1++runCreditT :: Monad m => Credit -> (forall s. CreditT s m a) -> m (Either Error a)+runCreditT n m = runSTT $ evalStateT (runExceptT (runT m)) (emptyState n)++runCreditM :: Credit -> (forall s. CreditM s a) -> Either Error a+runCreditM n m = runIdentity $ runSTT $ evalStateT (runExceptT (runT m)) (emptyState n)++{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s Identity () #-}+{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s (State st) () #-}+resetCurrentThunk :: Monad m => Credit -> CreditT s m ()+resetCurrentThunk (Credit (I# n)) = do+  (Cell me) <- getMe+  withCredits $ \(Credits c) -> do+    case IntMap.lookup me c of+      Just (Balance m b) -> pure $ Credits $ IntMap.insert me (Balance (n +# m) b) c+      _ -> throwError $ ClosedCurrent (Cell me)++-- Pretty Printing++getCredit :: Monad m => Cell -> CreditT s m Credit+getCredit (Cell i) = do+  St _ (Credits cm) _ <- get+  case IntMap.lookup i cm of+    Just (Balance n _) -> pure $ Credit (I# n)+    _ -> pure 0++instance (Monad m) => MonadMemory (CreditT s m) where+  {-# SPECIALIZE instance MonadMemory (CreditT s Identity) #-}+  {-# SPECIALIZE instance MonadMemory (CreditT s (State st)) #-}+  prettyThunk (Thunk c s) = do+    e <- liftST $ readSTRef s+    (Memory mtree mstore) <- case e of+      Left a -> prettyCell a+      Right b -> prettyCell b+    cr <- getCredit c+    pure $ Memory (Indirection c) (Map.insert c (mtree, cr) mstore)++instance Pretty Error where+  pretty (OutOfCredits i) = "Out of credits for" <+> pretty i+  pretty (InvalidAccount i) = "Invalid account for" <+> pretty i+  pretty (InvalidTick i) = "Invalid tick for" <+> pretty i+  pretty (ClosedCurrent (Cell 0)) = "Closed maint thread account. Never invoke creditAllTo on main thread."+  pretty (ClosedCurrent i) = "Closed current account" <+> pretty i+  pretty (UserError e) = "User error:" <+> pretty e+  pretty (AssertionFailed i n m) = pretty i <+> "should have" <+> pretty n <+> "credits but only has" <+> pretty m++instance Pretty a => Pretty (Either Error a) where+  pretty (Left e) = pretty e+  pretty (Right a) = pretty a++instance Pretty Account where+  pretty (Balance n _) = pretty (I# n)+  pretty Closed = "closed"+  pretty (ClosedWithHeir h _) = "closed with heir" <+> pretty h++instance Pretty Credits where+  pretty (Credits cm) = vsep $ map prettyPair (IntMap.toList cm)+    where+      prettyPair (i, a) = pretty i <+> "->" <+> pretty a++instance Pretty St where+  pretty (St me c nxt) = vsep+    [ "me:" <+> pretty me+    , "credits:" <+> pretty c+    , "next:" <+> pretty nxt+    ]
+ src/Test/Credit.hs view
@@ -0,0 +1,180 @@+{-# LANGUAGE DerivingStrategies, FunctionalDependencies, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables #-}++module Test.Credit+  (+  -- * Common time-complexity functions+    Size, logstar, log2, linear+  -- * Tree shapes for testing+  , Strategy(..), genTree+  -- * Testing data structures on trees of operations+  , DataStructure(..), runTree, checkCredits, runTreeMemory, checkCreditsMemory+  ) where++import Data.Either+import Control.Monad.State+import Data.Tree+import Test.QuickCheck+import Prettyprinter+import Prettyprinter.Render.String++import Control.Monad.Credit.Base+import Control.Monad.Credit.CreditM++path :: Arbitrary a => Int -> Tree a -> Gen (Tree a)+path 0 end = pure end+path n end = Node <$> arbitrary <*> ((:[]) <$> path (n-1) end)++path' :: Arbitrary a => Int -> Gen (Tree a)+path' n = path n =<< Node <$> arbitrary <*> pure []++bloom :: Arbitrary a => Gen (Tree a)+bloom = sized $ \n -> do+  m <- chooseInt (0, n)+  k <- chooseInt (0, m `div` 2)+  ts <- mapM (\_ -> path' (m `div` k)) [1..k]+  path (n - m) =<< Node <$> arbitrary <*> pure ts++pennant :: Arbitrary a => Gen (Tree a)+pennant = sized go+  where+    go n | n <= 1 = path' 0+    go n = do+      k <- chooseInt (n `div` 3, 2 * (n `div` 3))+      ts <- mapM (\_ -> go ((n - k - 1) `div` 2)) [1..2]+      path k =<< Node <$> arbitrary <*> pure ts++newtype SeqTree a = SeqTree { fromSeqTree :: Tree a }+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (SeqTree a) where+  arbitrary = sized $ \n -> SeqTree <$> path' n++newtype BloomTree a = BloomTree { fromBloomTree :: Tree a }+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (BloomTree a) where+  arbitrary = BloomTree <$> bloom++newtype PennantTree a = PennantTree { fromPennantTree :: Tree a }+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (PennantTree a) where+  arbitrary = PennantTree <$> pennant++newtype PrsTree a = PrsTree { fromPrsTree :: Tree a }+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (PrsTree a) where+  arbitrary = PrsTree <$> arbitrary++data Strategy = Path | Bloom | Pennant | Random+  deriving (Eq, Ord, Show)++genTree :: Arbitrary op => Strategy -> Gen (Tree op)+genTree Path = fromSeqTree <$> arbitrary+genTree Bloom = fromBloomTree <$> arbitrary+genTree Pennant = fromPennantTree <$> arbitrary+genTree Random = fromPrsTree <$> arbitrary++newtype Size = Size Int+  deriving (Eq, Ord, Show)+  deriving newtype (Num, Enum, Real, Integral, Pretty)++instance Monad m => MemoryCell m Size where+  prettyCell (Size i) = pure $ mkMCell (show i) []++logstar :: Size -> Credit+logstar (Size n) = fromInteger $ go n 0+  where+    go n acc | n < 2 = acc+    go n acc = go (log2 n 0) (acc + 1)++    log2 n acc | n < 2 = acc+    log2 n acc = log2 (n `div` 2) (acc + 1)++log2 :: Size -> Credit+log2 (Size n) = fromInteger $ go n 0+  where+    go n acc | n < 2 = acc+    go n acc = go (n `div` 2) (acc + 1)++linear :: Size -> Credit+linear (Size n) = fromInteger $ toInteger n++class (Arbitrary op, Show op) => DataStructure t op | t -> op where+  create :: forall m. MonadInherit m => t m+  action :: forall m. MonadInherit m => t m -> op -> (Credit, m (t m))++runTree :: forall t op. DataStructure t op => Tree op -> Either Error ()+runTree tree = runCreditM 0 (go (create @t) tree)+  where+    go :: forall s t op. DataStructure t op => t (CreditM s) -> Tree op -> CreditM s ()+    go a (Node op ts) = do+      let (cr, f) = action a op+      resetCurrentThunk cr+      a' <- f+      mapM_ (go a') ts++isPersistent :: Tree a -> Bool+isPersistent (Node _ ts) = length ts > 1 || any isPersistent ts++-- | Evaluate the queue operations using the given strategy on the given queue+-- Reports only if evaluation succeeded.+checkCredits :: forall t op. DataStructure t op => Strategy -> Property+checkCredits strat =+  forAllShrink (genTree strat) shrink $ \t ->+    classify (isPersistent t) "persistent" $+      isRight $ runTree @t t++data RoseZipper a = Root | Branch a [Tree a] (RoseZipper a)+  deriving (Eq, Ord, Show)++up :: RoseZipper a -> RoseZipper a+up (Branch x ls (Branch y rs z)) = Branch y (Node x (reverse ls) : rs) z+up z = z++extend :: String -> RoseZipper String -> RoseZipper String+extend s (Branch x ls z) = Branch (x ++ s) ls z+extend _ Root = Root++extract :: RoseZipper a -> Tree a+extract (Branch x ls Root) = Node x (reverse ls)+extract z = extract (up z)++flattenTree :: Tree a -> Tree a+flattenTree t = case go t of+  Just (x:xs) -> Node x (map (\x -> Node x []) xs)+  _ -> t+  where+    go (Node x []) = Just [x]+    go (Node x [t]) = (x :) <$> go t+    go (Node _ _) = Nothing++showState :: (Either Error (), RoseZipper String) -> String+showState (Left e, t) = drawTree $ flattenTree $ extract $ extend (show $ pretty e) t+showState (Right (), t) = drawTree $ flattenTree $ extract t++type M s = CreditT s (State (RoseZipper String))++runTreeMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Tree op -> String+runTreeMemory tree = showState $ runState (runCreditT 0 (go (create @t) tree)) Root+  where+    go :: forall s t op. (MemoryStructure t, DataStructure t op) => t (M s) -> Tree op -> M s ()+    go a (Node op ts) = do+      let (cr, f) = action a op+      resetCurrentThunk cr+      lift $ modify' (Branch (show op ++ ": ") []) +      a' <- f+      mem <- prettyStructure a'+      let s = renderString $ layoutSmart (defaultLayoutOptions { layoutPageWidth = Unbounded }) $ nest 2 $ pretty $ mem+      lift $ modify' (extend s)+      mapM_ (go a') ts+      lift $ modify' up++-- | Evaluate the queue operations using the given strategy on the given queue+-- Reports only if evaluation succeeded.+checkCreditsMemory :: forall t op. (MemoryStructure t, DataStructure t op) => Strategy -> Property+checkCreditsMemory strat =+  forAllShrinkShow (genTree strat) shrink (\t -> runTreeMemory @t t) $ \t ->+    classify (isPersistent t) "persistent" $+      isRight $ runTree @t t
+ src/Test/Credit/Deque/Bankers.hs view
@@ -0,0 +1,95 @@+module Test.Credit.Deque.Bankers where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Deque.Base+import Test.Credit.Deque.Streams++-- | Delay a computation, but do not consume any credits+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)+indirect t = delay t >>= pure . SIndirect++data BDeque a m = BDeque+  { front :: Stream m a+  , lenf :: !Int+  , ghostf :: Stream m a+  , rear :: Stream m a+  , lenr :: !Int+  , ghostr :: Stream m a+  }++isEmpty :: BDeque a m -> Bool+isEmpty (BDeque _ 0 _ _ 0 _) = True+isEmpty (BDeque _ _ _ _ _ _) = False++size :: BDeque a m -> Int+size (BDeque _ lenf _ _ lenr _) = lenf + lenr++-- Rough proof sketch:+-- After rebalancing, the front and rear streams have at most lenf + lenr debits.+-- Need (c - 1) * n/2 cons operations before rebalance, which means we have to+-- pay off 2 / (c - 1) debits on each stream per cons operation.+-- Need (c - 1) / c * n/2 uncons operations before rebalance, which means we have to+-- pay off at least 2*c / (c - 1) debits on each stream per uncons operation+-- (but also at least (c + 1) debits to be able to force on element).+-- Not sure if the analysis above works for c < 3++bdeque :: MonadInherit m => BDeque a m -> m (BDeque a m)+bdeque (BDeque f lenf gf r lenr gr)+  | lenf > c * lenr + 1 = do+    let i = (lenf + lenr) `div` 2+    let j = lenf + lenr - i+    f' <- indirect (STake i f)+    f'' <- indirect (SRevDrop i f SNil)+    credit (fromIntegral c) f'' >> eval (fromIntegral c) f''+    r' <- indirect (SAppend r f'')+    credit 1 r'+    pure $ BDeque f' i f' r' j r'+  | lenr > c * lenf + 1 = do+    let j = (lenf + lenr) `div` 2+    let i = lenf + lenr - j+    r' <- indirect (STake j r)+    r'' <- indirect (SRevDrop j r SNil)+    credit (fromIntegral c) r'' >> eval (fromIntegral c) r''+    f' <- indirect (SAppend f r'')+    credit 1 f'+    pure $ BDeque f' i f' r' j r'+  | otherwise =+    pure $ BDeque f lenf gf r lenr gr++instance Deque BDeque where+  empty = pure $ BDeque SNil 0 SNil SNil 0 SNil+  cons x (BDeque f fl gf r rl gr) = credit 1 gf >> credit 1 gr >>+    bdeque (BDeque (SCons x f) (fl + 1) gf r rl gr)+  snoc (BDeque f fl gf r rl gr) x = credit 1 gf >> credit 1 gr >>+    bdeque (BDeque f fl gf (SCons x r) (rl + 1) gr)+  uncons (BDeque f fl gf r rl gr) = credit (fromIntegral c + 1) gf >> credit (fromIntegral c + 1) gr >> smatch f+    (\x f -> bdeque (BDeque f (fl - 1) gf r rl gr) >>= \q -> pure $ Just (x, q))+    (smatch r+      (\x _ -> empty >>= \q -> pure $ Just (x, q))+      (pure Nothing))+  unsnoc (BDeque f fl gf r rl gr) = credit (fromIntegral c + 1) gr >> credit (fromIntegral c + 1) gf >> smatch r+    (\x r -> bdeque (BDeque f fl gf r (rl - 1) gr) >>= \q -> pure $ Just (q, x))+    (smatch f+      (\x _ -> empty >>= \q -> pure $ Just (q, x))+      (pure Nothing))+  concat = undefined++instance BoundedDeque BDeque where+  qcost _ (Cons _) = fromIntegral c + 3+  qcost _ (Snoc _) = fromIntegral c + 3+  qcost _ Uncons = 3 * fromIntegral c + 4+  qcost _ Unsnoc = 3 * fromIntegral c + 4+  qcost _ Concat = 0++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BDeque a m) where+  prettyCell (BDeque f fl _ r rl _) = do+    f' <- prettyCell f+    fl' <- prettyCell fl+    r' <- prettyCell r+    rl' <- prettyCell rl+    pure $ mkMCell "BDeque" [f', fl', r', rl']++instance Pretty a => MemoryStructure (BDeque (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Deque/Base.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}++module Test.Credit.Deque.Base (DequeOp(..), Deque(..), BoundedDeque(..), D, BD) where++import Prelude hiding (concat)+import Control.Monad.Credit+import Test.Credit+import Test.QuickCheck++data DequeOp a = Cons a | Snoc a | Uncons | Unsnoc | Concat+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (DequeOp a) where+  arbitrary = frequency+    [ (7, Cons <$> arbitrary)+    , (4, Snoc <$> arbitrary)+    , (2, pure Uncons)+    , (6, pure Unsnoc)+    , (1, pure Concat)+    ]++class Deque q where+  empty :: MonadInherit m => m (q a m)+  cons :: MonadInherit m => a -> q a m -> m (q a m)+  snoc :: MonadInherit m => q a m -> a -> m (q a m)+  uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))+  unsnoc :: MonadInherit m => q a m -> m (Maybe (q a m, a))+  concat :: MonadInherit m => q a m -> q a m -> m (q a m)++class Deque q => BoundedDeque q where+  qcost :: Size -> DequeOp a -> Credit++data D q a m = E | D Size (q (PrettyCell a) m)++instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (D q a m) where+  prettyCell E = pure $ mkMCell "" []+  prettyCell (D _ q) = prettyCell q++instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (D q a) where+  prettyStructure E = pure $ mkMCell "" []+  prettyStructure (D _ q) = prettyStructure q++act :: (MonadInherit m, Deque q) => Size -> q (PrettyCell a) m -> DequeOp a -> m (D q a m)+act sz q (Cons x) = D (sz + 1) <$> cons (PrettyCell x) q+act sz q (Snoc x) = D (sz + 1) <$> snoc q (PrettyCell x)+act sz q Uncons = do+  m <- uncons q+  case m of+    Nothing -> pure E+    Just (_, q') -> pure $ D (max 0 (sz - 1)) q'+act sz q Unsnoc = do+  m <- unsnoc q+  case m of+    Nothing -> pure E+    Just (q', _) -> pure $ D (max 0 (sz - 1)) q'+act sz q Concat = pure $ D sz q++instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (D q a) (DequeOp a) where+  create = E+  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)+  action (D sz q) op = (qcost @q sz op, act sz q op)++size :: D q a m -> Size+size E = 0+size (D sz _) = sz++data BD q a m = BD (D q a m) (D q a m)++instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (BD q a m) where+  prettyCell (BD q1 q2) = do+    q1' <- prettyCell q1+    q2' <- prettyCell q2+    pure $ mkMCell "Concat" [q1', q2']++instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (BD q a) where+  prettyStructure (BD q1 q2) = do+    q1' <- prettyStructure q1+    q2' <- prettyStructure q2+    pure $ mkMCell "Concat" [q1', q2']++act1 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)+act1 op (BD q1 q2) = do+  q1' <- case q1 of+    E -> empty+    D _ q -> pure q+  q1'' <- act (size q1) q1' op +  pure $ BD q1'' q2++act2 :: (MonadInherit m, Deque q) => DequeOp a -> BD q a m -> m (BD q a m)+act2 op (BD q1 q2) = do+  let sz = size q2+  q2' <- case q2 of+    E -> empty+    D _ q -> pure q+  q2'' <- act (size q2) q2' op +  pure $ BD q1 q2''++concatenate :: (MonadInherit m, Deque q) => D q a m -> D q a m -> m (D q a m)+concatenate E E = pure E+concatenate (D sz1 q1) E = pure $ D sz1 q1+concatenate E (D sz2 q2) = pure $ D sz2 q2+concatenate (D sz1 q1) (D sz2 q2) = D (sz1 + sz2) <$> concat q1 q2++instance (Arbitrary a, BoundedDeque q, Show a) => DataStructure (BD q a) (DequeOp a) where+  create = BD E E+  action (BD q1 q2) (Cons x) = (qcost @q (size q1) (Cons x), act1 (Cons x) (BD q1 q2))+  action (BD q1 q2) (Snoc x) = (qcost @q (size q2) (Snoc x), act2 (Snoc x) (BD q1 q2))+  action (BD q1 q2) Uncons = (qcost @q (size q1) Uncons, act1 Uncons (BD q1 q2))+  action (BD q1 q2) Unsnoc = (qcost @q (size q2) Unsnoc, act2 Unsnoc (BD q1 q2))+  action (BD q1 q2) Concat = (qcost @q (size q1 + size q2) Concat, BD E <$> concatenate q1 q2)
+ src/Test/Credit/Deque/Catenable.hs view
@@ -0,0 +1,135 @@+{-# LANGUAGE GADTs, LambdaCase #-}++module Test.Credit.Deque.Catenable where++import Prelude hiding (concat)+import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit.Deque.Base+import qualified Test.Credit.Queue.Base as Q+import qualified Test.Credit.Queue.Bankers as Q++-- | A rose tree where the elements are pre-ordered+data CatDeque a m+  = E+  | C a -- ^ head+      (Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m) -- ^ tail++data CLazyCon m a where+  Pure :: a -> CLazyCon m a+  LinkAll :: Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> CLazyCon m (CatDeque a m)++instance MonadInherit m => HasStep (CLazyCon m) m where+  step (Pure xs) = pure xs+  step (LinkAll q) = linkAll q++costSnoc :: Credit+costSnoc = Q.qcost @(Q.BQueue) undefined (Q.Snoc undefined)++costUncons :: Credit+costUncons = Q.qcost @(Q.BQueue) undefined (Q.Uncons)++link :: MonadInherit m => CatDeque a m -> Thunk m (CLazyCon m) (CatDeque a m) -> m (CatDeque a m)+link (C x q) s = C x <$> Q.snoc q s++linkAll :: MonadInherit m => Q.BQueue (Thunk m (CLazyCon m) (CatDeque a m)) m -> m (CatDeque a m)+linkAll q = do+  m <- Q.uncons q+  case m of+    Nothing -> fail "linkAll: empty queue"+    Just (t, q') -> do+      t <- force t+      if Q.isEmpty q' then pure t+      else do+        s <- delay $ LinkAll q'+        creditWith s costUncons -- for the last uncons+        link t s++concat' :: MonadInherit m => CatDeque a m -> CatDeque a m -> m (CatDeque a m)+concat' E xs = pure xs+concat' xs E = pure xs+concat' xs ys = do+  ys <- delay $ Pure ys+  link xs ys++-- | Assign credits to the thunk and force it+-- unless it is a `LinkAll(t:_)` where `t` requires credits.+-- In the latter case, recursive until we can force a thunk.+dischargeThunk :: MonadInherit m => Thunk m (CLazyCon m) (CatDeque a m) -> m ()+dischargeThunk s = do+  let assign = creditWith s (costSnoc + costUncons) >> force s >> pure ()+  lazymatch s (\_ -> assign) $ \case+    Pure _ -> assign+    LinkAll q -> do+      q' <- Q.lazyqueue q+      case q' of+        [] -> assign+        t' : _ -> do+          lazymatch t' (\_ -> assign) $ \case+            Pure _ -> assign+            LinkAll _ -> dischargeThunk t'++findFirstThunk :: MonadInherit m => CatDeque a m -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))+findFirstThunk (C _ q) = do+  q' <- Q.lazyqueue q+  seekFirstThunk q'+findFirstThunk _ = pure Nothing++seekFirstThunk :: MonadInherit m => [Thunk m (CLazyCon m) (CatDeque a m)] -> m (Maybe (Thunk m (CLazyCon m) (CatDeque a m)))+seekFirstThunk [] = pure Nothing+seekFirstThunk (t : q) = do+  mt <- lazymatch t findFirstThunk $ \case+    Pure q' -> findFirstThunk q'+    LinkAll _ -> pure $ Just t+  case mt of+    Nothing -> seekFirstThunk q+    Just t' -> pure $ Just t'++dischargeFirst :: MonadInherit m => CatDeque a m -> m ()+dischargeFirst q = do+  mt <- findFirstThunk q+  case mt of+    Nothing -> pure ()+    Just t -> dischargeThunk t++instance Deque CatDeque where+  empty = pure E+  cons x q = do+    e <- Q.empty+    concat (C x e) q+  snoc q x = do+    e <- Q.empty+    concat q (C x e)+  uncons E = pure Nothing+  uncons (C x q) = do+    q' <- if Q.isEmpty q then pure E else linkAll q+    dischargeFirst q'+    dischargeFirst q'+    pure $ Just (x, q')+  unsnoc q = pure $ Just (q, undefined)+  concat = concat'++instance BoundedDeque CatDeque where+  qcost _ (Cons _) = costSnoc+  qcost _ (Snoc _) = costSnoc+  qcost _ Uncons = 4 * costUncons + 3 * costSnoc+  qcost _ Unsnoc = 0+  qcost _ Concat = 0++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CLazyCon m a) where+  prettyCell (Pure x) = do+    x' <- prettyCell x+    pure $ mkMCell "Pure" [x']+  prettyCell (LinkAll q) = do+    q' <- prettyCell q+    pure $ mkMCell "LinkAll" [q']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CatDeque a m) where+  prettyCell E = pure $ mkMCell "E" []+  prettyCell (C x q) = do+    x' <- prettyCell x+    q' <- prettyCell q+    pure $ mkMCell "C" [x', q']++instance Pretty a => MemoryStructure (CatDeque (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Deque/ImplicitCat.hs view
@@ -0,0 +1,404 @@+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 (IPay _ m) = m+  step (ILazy m) = 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 = 3 * (qcost @(D.BDeque) undefined (Cons undefined) + qcost @(D.BDeque) undefined Uncons)++deepDanger :: D.BDeque a m -> Credit+deepDanger d = if D.size d == 3 then cost else 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 f a m b r = do+  -- a `hasAtLeast` (4 * deepDanger f + deepDanger r)+  -- b `hasAtLeast` (deepDanger f + 4 * deepDanger r)+  pure $ Deep f a m b r++icreditWith :: MonadCredit m => Thunk m (ILazyCon m) (ImplicitCat a m) -> Credit -> m ()+icreditWith t c = do+  lazymatch t (\_ -> pure ()) $ \t'' -> case t'' of+    ILazy _ ->   t  `creditWith` c+    IPay t' _ -> t' `creditWith` c++cmpdDanger :: D.BDeque a m -> Credit+cmpdDanger d = if D.size d == 2 then cost else 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 f c r = pure $ Cmpd f c r++isEmpty :: ImplicitCat a m -> Bool+isEmpty (Shallow d) = D.isEmpty d+isEmpty (Deep _ _ _ _ _) = 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 f r = do+  fu <- D.unsnoc f+  ru <- D.uncons r+  case (fu, ru) of+    (Just (fi, fl), Just (rh, rt)) -> do+      m <- D.cons fl =<< D.cons rh =<< D.empty+      pure $ (fi, m, rt)+    _ -> fail "share: empty deque"++dappendL :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)+dappendL d1 d2 = do+  d1' <- D.unsnoc d1+  case d1' of+    Nothing -> pure d2+    Just (d1i, d1l) -> dappendL d1i =<< D.cons d1l d2++dappendR :: MonadInherit m => D.BDeque a m -> D.BDeque a m -> m (D.BDeque a m)+dappendR d1 d2 = do+  d2' <- D.uncons d2+  case d2' of+    Nothing -> pure d1+    Just (d2h, d2t) -> join $ dappendR <$> D.snoc d1 d2h <*> pure d2t++-- 5 * cost+concat' :: MonadInherit m => ImplicitCat a m -> ImplicitCat a m -> m (ImplicitCat a m)+concat' (Shallow d1) (Shallow d2) = do+  if D.size d1 < 4 then Shallow <$> dappendL d1 d2+  else if D.size d2 < 4 then Shallow <$> dappendR d1 d2+  else do+    (f, m, r) <- share d1 d2+    e <- delay $ ILazy $ empty+    deep f e m e r+concat' (Shallow d) (Deep f a m b r) = do+  if D.size d < 4 then do+    df <- dappendL d f+    deep df a m b r+  else do+    fa <- delay $ ILazy $ do+      a `icreditWith` (5 * cost)+      cons (Simple f) =<< force a+    fa `icreditWith` cost+    fa `icreditWith` (deepDanger r)+    deep d fa m b r+concat' (Deep f a m b r) (Shallow d) = do+  if D.size d < 4 then do+    rd <- dappendR r d+    deep f a m b rd+  else do+    br <- delay $ ILazy $ do+      b `icreditWith` (5 * cost)+      (`snoc` (Simple r)) =<< force b+    br `icreditWith` cost+    br `icreditWith` (deepDanger f)+    deep f a m br d+concat' (Deep f1 a1 m1 b1 r1) (Deep f2 a2 m2 b2 r2) = do+  (r1', m, f2') <- share r1 f2+  -- Discharge debits on b1, a2 for compound element+  when (D.size f1 > 3 && D.size r1 > 3) $+    b1 `icreditWith` cost+  when (D.size f2 > 3 && D.size r2 > 3) $+    a2 `icreditWith` cost+  c1 <- cmpd m1 b1 r1'+  c2 <- cmpd f2' a2 m2+  a1' <- delay $ ILazy $ do+    a1 `icreditWith` (4 * (cost - deepDanger f1))+    (`snoc` c1) =<< force a1+  b2' <- delay $ ILazy $ do+    b2 `icreditWith` (4 * (cost - deepDanger r2))+    cons c2 =<< force b2+  -- Discharge debits for snoc/cons onto a1/b2+  a1' `icreditWith` cost+  b2' `icreditWith` cost+  -- Discharge the debit from swapping f/r+  when (D.size f1 == 3 && D.size f2 > 3) $+    b2 `icreditWith` cost+  when (D.size r2 == 3 && D.size r1 > 3) $+    a1 `icreditWith` cost+  -- Notice that only two of the when-statements+  -- can be true at the same time.+  -- So we only discharge 4 debits.+  deep f1 a1' m b2' r2++replaceHead :: MonadInherit m => a -> ImplicitCat a m -> m (ImplicitCat a m)+replaceHead x (Shallow d) = do+  d' <- D.uncons d+  case d' of+    Nothing -> fail "replaceHead: empty deque"+    Just (_, d') -> Shallow <$> D.cons x d'+replaceHead x (Deep f a m b r) = do+  f' <- D.uncons f+  case f' of+    Nothing -> fail "replaceHead: empty deque"+    Just (_, f') -> do+      f' <- D.cons x f'+      deep f' a m b 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' (Shallow d) = tick >> do+  m <- D.uncons d+  case m of+    Nothing -> pure Nothing+    Just (x, d') -> fmap (Just . (x,)) $ delay $ ILazy $ do+      pure $ Shallow d'+uncons' (Deep f a m b r) = tick >> do+  f' <- D.uncons f+  case f' of+    Nothing -> pure Nothing+    Just (x, f') -> fmap (Just . (x,)) $ delay $ ILazy $ do+      if D.size f' >= 3 -- iff D.size f > 3+        then do+          a `icreditWith` (4 * deepDanger f')+          b `icreditWith` (deepDanger f')+          deep f' a m b r+        else do -- D.size f' == 2+          a `icreditWith` (cost - deepDanger r)+          a <- force a+          if not (isEmpty a)+            then do+              a' <- uncons' a+              case a' of+                Nothing -> fail "uncons': a cannot be empty"+                Just (ah, at) -> do+                  case ah of+                    Simple d -> do+                      f'' <- dappendL f' d -- cost: 2 * (cons + unsnoc)+                      at `icreditWith` cost+                      at `icreditWith` (deepDanger r)+                      deep f'' at m b r+                    Cmpd f'' c' r' -> do+                      f''' <- dappendL f' f'' -- cost: 2 * (cons + unsnoc)+                      a'' <- delay $ ILazy $ do+                        c'' <- force c'+                        ra <- replaceHead (Simple r') a -- cost: uncons + cons+                        concat' c'' ra+                      c' `icreditWith` (4 * cost)+                      a'' `icreditWith` (deepDanger r)+                      deep f''' a'' m b r+            else do+              b `icreditWith` (4 * (cost - deepDanger r))+              b <- force b+              if not (isEmpty b)+                then do+                  b' <- uncons' b+                  case b' of+                    Nothing -> fail "uncons': b cannot be empty"+                    Just (bh, bt) -> do+                      case bh of+                        Simple d -> do+                          f'' <- dappendL f' 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.+                          a <- delay $ IPay bt $ do+                            fmap Shallow $ empty+                          a `icreditWith` (deepDanger r)+                          bt `icreditWith` (4 * deepDanger r)+                          deep f'' a d bt r+                        Cmpd f'' c' r' -> do+                          f''' <- dappendL f' m -- cost: 2 * (cons + unsnoc)+                          a'' <- delay $ ILazy $ do+                            c' `icreditWith` (4 * cost)+                            cons (Simple f'') =<< force c'+                          a'' `icreditWith` (deepDanger r)+                          bt `icreditWith` (4 * deepDanger 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.+                          deep f''' a'' r' bt r+                else do -- 1 * cost+                  fm <- dappendL f' m+                  concat' (Shallow fm) (Shallow r)++replaceLast :: MonadInherit m => ImplicitCat a m -> a -> m (ImplicitCat a m)+replaceLast (Shallow d) x = do+  d' <- D.unsnoc d+  case d' of+    Nothing -> fail "replaceLast: empty deque"+    Just (d', _) -> Shallow <$> D.snoc d' x+replaceLast (Deep f a m b r) x = do+  r' <- D.unsnoc r+  case r' of+    Nothing -> fail "replaceLast: empty deque"+    Just (r', _) -> do+      r' <- D.snoc r' x+      deep f a m b r'++unsnoc' :: MonadInherit m => ImplicitCat a m -> m (Maybe (Thunk m (ILazyCon m) (ImplicitCat a m), a))+unsnoc' (Shallow d) = tick >> do+  m <- D.unsnoc d+  case m of+    Nothing -> pure Nothing+    Just (d', x) -> fmap (Just . (,x)) $ delay $ ILazy $ do+      pure $ Shallow d'+unsnoc' (Deep f a m b r) = tick >> do+  r' <- D.unsnoc r+  case r' of+    Nothing -> pure Nothing+    Just (r', x) -> fmap (Just . (,x)) $ delay $ ILazy $ do+      if D.size r' >= 3 -- iff D.size r > 3+        then do+          a `icreditWith` (deepDanger r')+          b `icreditWith` (4 * deepDanger r')+          deep f a m b r'+        else do+          b `icreditWith` (cost - deepDanger f)+          b <- force b+          if not (isEmpty b)+            then do+              b' <- unsnoc' b+              case b' of+                Nothing -> fail "unsnoc': b cannot be empty"+                Just (bi, bl) -> do+                  case bl of+                    Simple d -> do+                      r'' <- dappendR d r'+                      bi `icreditWith` cost+                      bi `icreditWith` (deepDanger f)+                      deep f a m bi r''+                    Cmpd f' c' r'' -> do+                      r''' <- dappendR r'' r'+                      b'' <- delay $ ILazy $ do+                        c'' <- force c'+                        bf <- replaceLast b (Simple f')+                        concat' bf c''+                      c' `icreditWith` (4 * cost)+                      b'' `icreditWith` (deepDanger f)+                      deep f a m b'' r'''+            else do+              a `icreditWith` (4 * (cost - deepDanger f))+              a <- force a+              if not (isEmpty a)+                then do+                  a' <- unsnoc' a+                  case a' of+                    Nothing -> fail "unsnoc': a cannot be empty"+                    Just (ai, al) -> do+                      case al of+                        Simple d -> do+                          r'' <- dappendR m r'+                          b <- delay $ IPay ai $ do+                            fmap Shallow $ empty+                          b `icreditWith` (deepDanger f)+                          ai `icreditWith` (4 * deepDanger f)+                          deep f ai d b r''+                        Cmpd f' c' r'' -> do+                          r''' <- dappendR m r'+                          b'' <- delay $ ILazy $ do+                            c' `icreditWith` (4 * cost)+                            (`snoc` (Simple r'')) =<< force c'+                          b'' `icreditWith` (deepDanger f)+                          ai `icreditWith` (4 * deepDanger f)+                          deep f ai f' b'' r'''+                else do+                  mr <- dappendR m r'+                  concat' (Shallow f) (Shallow mr)++instance Deque ImplicitCat where+  empty = Shallow <$> D.empty+  cons x (Shallow d) = Shallow <$> D.cons x d+  cons x (Deep f a m b r) = do+    f' <- D.cons x f+    deep f' a m b r+  snoc (Shallow d) x = Shallow <$> D.snoc d x+  snoc (Deep f a m b r) x = Deep f a m b <$> D.snoc r x+  uncons d = do+    m <- uncons' d+    case m of+      Nothing -> pure Nothing+      Just (x, t) -> do+        t `icreditWith` (6 * cost)+        Just . (x,) <$> force t+  unsnoc d = do+    m <- unsnoc' d+    case m of+      Nothing -> pure Nothing+      Just (t, x) -> do+        t `icreditWith` (6 * cost)+        Just . (,x) <$> force t+  concat xs ys = tick >> concat' xs ys++instance BoundedDeque ImplicitCat where+  qcost sz (Cons x) = qcost @(D.BDeque) sz (Cons x)+  qcost sz (Snoc x) = qcost @(D.BDeque) sz (Snoc x)+  qcost sz Uncons = 1 + 6 * cost + qcost @(D.BDeque) sz Uncons+  qcost sz Unsnoc = 1 + 6 * cost + qcost @(D.BDeque) sz Unsnoc+  qcost _ Concat = 1 + 5 * cost++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where+  prettyCell _ = pure $ mkMCell "<lazy>" []++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (CmpdElem a m) where+  prettyCell (Simple d) = do+    d' <- prettyCell d+    pure $ mkMCell "Simple" [d']+  prettyCell (Cmpd f m r) = do+    f' <- prettyCell f+    m' <- prettyCell m+    r' <- prettyCell r+    pure $ mkMCell "Cmpd" [f', m', r']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ImplicitCat a m) where+  prettyCell (Shallow d) = do+    d' <- prettyCell d+    pure $ mkMCell "Shallow" [d']+  prettyCell (Deep f a m b r) = do+    f' <- prettyCell f+    a' <- prettyCell a+    m' <- prettyCell m+    b' <- prettyCell b+    r' <- prettyCell r+    pure $ mkMCell "Deep" [f', a', m', b', r']++instance Pretty a => MemoryStructure (ImplicitCat (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Deque/Realtime.hs view
@@ -0,0 +1,84 @@+module Test.Credit.Deque.Realtime where++import Prelude hiding (lookup, reverse)++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit.Deque.Base+import Test.Credit.Deque.Streams++-- | Delay a computation, but do not consume any credits+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)+indirect t = delay t >>= pure . SIndirect++data RDeque a m = RDeque+  { lenf :: !Int+  , front :: Stream m a+  , sf :: Stream m a+  , lenr :: !Int+  , rear :: Stream m a+  , sr :: Stream m a+  }++exec1 :: MonadInherit m => Stream m a -> m (Stream m a)+exec1 xs = credit (fromIntegral c + 1) xs >> smatch xs+  (\_ xs -> pure xs)+  (pure SNil)++exec2 :: MonadInherit m => Stream m a -> m (Stream m a)+exec2 xs = exec1 xs >>= exec1++rdeque :: MonadInherit m => RDeque a m -> m (RDeque a m)+rdeque (RDeque lenf f sf lenr r sr)+  | lenf > c * lenr + 1 = do+    let i = (lenf + lenr) `div` 2+    let j = lenf + lenr - i+    f' <- indirect (STake i f)+    f'' <- indirect (SRevDrop i f SNil)+    r' <- indirect (SAppend r f'')+    credit (fromIntegral c) f'' >> eval (fromIntegral c) f''+    pure $ RDeque i f' f' j r' r'+  | lenr > c * lenf + 1 = do+    let j = (lenf + lenr) `div` 2+    let i = lenf + lenr - j+    r' <- indirect (STake j r)+    r'' <- indirect (SRevDrop j r SNil)+    f' <- indirect (SAppend f r'')+    credit (fromIntegral c) r'' >> eval (fromIntegral c) r''+    pure $ RDeque i f' f' j r' r'+  | otherwise =+    pure $ RDeque lenf f sf lenr r sr++instance Deque RDeque where+  empty = pure $ RDeque 0 SNil SNil 0 SNil SNil+  cons x (RDeque lenf f sf lenr r sr) = exec1 sf >>= \sf -> exec1 sr >>= \sr ->+    rdeque (RDeque (lenf + 1) (SCons x f) sf lenr r sr)+  snoc (RDeque lenf f sf lenr r sr) x = exec1 sf >>= \sf -> exec1 sr >>= \sr ->+    rdeque (RDeque lenf f sf (lenr + 1) (SCons x r) sr)+  uncons (RDeque lenf f sf lenr r sr) = exec2 sf >>= \sf -> exec2 sr >>= \sr -> smatch f+    (\x f -> rdeque (RDeque (lenf - 1) f sf lenr r sr) >>= \q -> pure $ Just (x, q))+    (pure Nothing)+  unsnoc (RDeque lenf f sf lenr r sr) = exec2 sf >>= \sf -> exec2 sr >>= \sr -> smatch r+    (\x r -> rdeque (RDeque lenf f sf (lenr - 1) r sr) >>= \q -> pure $ Just (q, x))+    (pure Nothing)+  concat = undefined++instance BoundedDeque RDeque where+  qcost _ (Cons _) = 3 * fromIntegral c + 4+  qcost _ (Snoc _) = 3 * fromIntegral c + 4+  qcost _ Uncons = 5 * fromIntegral c + 8+  qcost _ Unsnoc = 5 * fromIntegral c + 8+  qcost _ Concat = 0++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (RDeque a m) where+  prettyCell (RDeque lenf f sf lenr r sr) = do+    lenf' <- prettyCell lenf+    f' <- prettyCell f+    sf' <- prettyCell sf+    lenr' <- prettyCell lenr+    r' <- prettyCell r+    sr' <- prettyCell sr+    pure $ mkMCell "Deque" [lenf', f', sf', lenr', r', sr']++instance Pretty a => MemoryStructure (RDeque (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Deque/SimpleCat.hs view
@@ -0,0 +1,200 @@+module Test.Credit.Deque.SimpleCat where++import Prelude hiding (head, tail, concat)+import Prettyprinter (Pretty)+import Control.Monad+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++-- | "simple"+data SimpleCat a m+  = Shallow (D.BDeque a m)+  | Deep (D.BDeque a m) -- ^ (>= 2 elements)+         (Thunk m (Lazy m) (SimpleCat (D.BDeque a m) m))+         (D.BDeque a m) -- ^ (>= 2 elements)++dangerous :: D.BDeque a m -> Bool+dangerous d = D.size d == 2++cost :: Credit+cost = qcost @(D.BDeque) undefined (Cons undefined) + 3 * qcost @(D.BDeque) undefined Uncons++danger :: D.BDeque a m -> Credit+danger d = if D.size d == 2 then cost else 0++deep :: MonadInherit m => D.BDeque a m -> Thunk m (Lazy m) (SimpleCat (D.BDeque a m) m) -> D.BDeque a m -> m (SimpleCat a m)+deep f m r = do+  m `hasAtLeast` (danger f + danger r)+  pure $ Deep f m r++isEmpty :: SimpleCat a m -> Bool+isEmpty (Shallow d) = D.isEmpty d+isEmpty (Deep _ _ _) = False++data DequeIs a m+  = Small (Maybe a)+  | Big (D.BDeque a m)++tooSmall :: MonadInherit m => D.BDeque a m -> m (DequeIs a m)+tooSmall d = do+  m1 <- D.uncons d+  case m1 of+    Nothing -> pure $ Small Nothing+    Just (x, d') -> do+      m2 <- D.uncons d'+      case m2 of+        Nothing -> pure $ Small (Just x)+        Just _ -> pure $ Big d++dappendL :: MonadInherit m => Maybe a -> D.BDeque a m -> m (D.BDeque a m)+dappendL Nothing d2 = pure d2+dappendL (Just x) d2 = D.cons x d2++dappendR :: MonadInherit m => D.BDeque a m -> Maybe a -> m (D.BDeque a m)+dappendR d1 Nothing = pure d1+dappendR d1 (Just x) = D.snoc d1 x++uncons' :: MonadInherit m => SimpleCat a m -> m (Maybe (a, Thunk m (Lazy m) (SimpleCat a m)))+uncons' (Shallow d) = tick >> do+  m <- D.uncons d+  case m of+    Nothing -> pure Nothing+    Just (x, d') -> fmap (Just . (x,)) $ delay $ Lazy $ do+      pure $ Shallow d'+uncons' (Deep f m r) = tick >> do+  f' <- D.uncons f+  case f' of+    Nothing -> pure Nothing+    Just (x, f') -> fmap (Just . (x,)) $ delay $ Lazy $ do+      dis <- tooSmall f'+      case dis of+        Big f' -> do+          when (dangerous f') $ m `creditWith` cost+          deep f' m r+        Small y -> do+          unless (dangerous r) $ m `creditWith` cost+          m' <- uncons' =<< force m+          case m' of+            Nothing -> Shallow <$> dappendL y r+            Just (h, t) -> do+              when (dangerous r) $ t `creditWith` cost+              dappendL y h >>= \h -> deep h t r++unsnoc' :: MonadInherit m => SimpleCat a m -> m (Maybe (Thunk m (Lazy m) (SimpleCat a m), a))+unsnoc' (Shallow d) = tick >> do+  m <- D.unsnoc d+  case m of+    Nothing -> pure Nothing+    Just (d', x) -> fmap (Just . (,x)) $ delay $ Lazy $ do+      pure $ Shallow d'+unsnoc' (Deep f m r) = tick >> do+  r' <- D.unsnoc r+  case r' of+    Nothing -> pure Nothing+    Just (r', x) -> fmap (Just . (,x)) $ delay $ Lazy $ do+      dis <- tooSmall r'+      case dis of+        Big r' -> do+          when (dangerous r') $ m `creditWith` cost+          deep f m r'+        Small y -> do+          unless (dangerous f) $ m `creditWith` cost+          m' <- unsnoc' =<< force m+          case m' of+            Nothing -> Shallow <$> dappendR f y+            Just (t, h) -> do+              when (dangerous f) $ t `creditWith` cost+              deep f t =<< dappendR h y++concat' :: MonadInherit m => SimpleCat a m -> SimpleCat a m -> m (SimpleCat a m)+concat' (Shallow d1) (Shallow d2) = tick >> do+  dis1 <- tooSmall d1+  case dis1 of+    Small y -> Shallow <$> dappendL y d2+    Big d1 -> do+      dis2 <- tooSmall d2+      case dis2 of+        Small y -> Shallow <$> dappendR d1 y+        Big d2 -> do+          m <- delay $ Lazy empty+          when (dangerous d1) $ m `creditWith` cost+          when (dangerous d2) $ m `creditWith` cost+          deep d1 m d2+concat' (Shallow d1) (Deep f m r) = tick >> do+  dis1 <- tooSmall d1+  case dis1 of+    Small y -> dappendL y f >>= \f -> deep f m r+    Big d -> do+      m `creditWith` cost+      unless (dangerous r) $ m `creditWith` cost+      m' <- delay $ Lazy $ cons f =<< force m+      when (dangerous d) $ m' `creditWith` cost+      when (dangerous r) $ m' `creditWith` cost+      deep d m' r+concat' (Deep f m r) (Shallow d2) = tick >> do+  dis2 <- tooSmall d2+  case dis2 of+    Small y -> deep f m =<< dappendR r y+    Big d -> do+      m `creditWith` cost+      unless (dangerous f) $ m `creditWith` cost+      m' <- delay $ Lazy $ flip snoc r =<< force m+      when (dangerous d) $ m' `creditWith` cost+      when (dangerous f) $ m' `creditWith` cost+      deep f m' d+concat' (Deep f1 m1 r1) (Deep f2 m2 r2) = tick >> do+  m <- delay $ Lazy $ do+    m1 `creditWith` (2 * cost)+    m1' <- flip snoc r1 =<< force m1+    m2 `creditWith` (2 * cost)+    m2' <- cons f2 =<< force m2+    concat' m1' m2'+  creditAllTo m+  deep f1 m r2++instance Deque SimpleCat where+  empty = Shallow <$> D.empty+  cons x (Shallow d) = Shallow <$> D.cons x d+  cons x (Deep f m r) = do+    f' <- D.cons x f+    deep f' m r+  snoc (Shallow d) x = Shallow <$> D.snoc d x+  snoc (Deep f m r) x = deep f m =<< D.snoc r x+  uncons d = do+    m <- uncons' d+    case m of+      Nothing -> pure Nothing+      Just (x, t) -> do+        t `creditWith` (2 * cost)+        Just . (x,) <$> force t+  unsnoc d = do+    m <- unsnoc' d+    case m of+      Nothing -> pure Nothing+      Just (t, x) -> do+        t `creditWith` (2 * cost)+        Just . (,x) <$> force t+  concat = concat'++instance BoundedDeque SimpleCat where+  qcost n (Cons x) = qcost @(D.BDeque) n (Cons x)+  qcost n (Snoc x) = qcost @(D.BDeque) n (Snoc x)+  qcost n Uncons = 1 + qcost @(D.BDeque) n Uncons + 2 * cost+  qcost n Unsnoc = 1 + qcost @(D.BDeque) n Unsnoc + 2 * cost+  qcost n Concat = (1 + 6 * cost) * log2 n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SimpleCat a m) where+  prettyCell (Shallow d) = do+    d' <- prettyCell d+    pure $ mkMCell "Shallow" [d']+  prettyCell (Deep f m r) = do+    f' <- prettyCell f+    m' <- prettyCell m+    r' <- prettyCell r+    pure $ mkMCell "Deep" [f', m', r']++instance Pretty a => MemoryStructure (SimpleCat (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Deque/Streams.hs view
@@ -0,0 +1,99 @@+{-# LANGUAGE GADTs #-}++module Test.Credit.Deque.Streams (Stream(..), SLazyCon(..), smatch, credit, eval, c) where++import Prelude hiding (lookup, reverse)+import Control.Monad.Credit++c :: Int+c = 5++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (SThunk m (Stream m a))++type SThunk m = Thunk m (SLazyCon m)++data SLazyCon m a where+  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)+  SRevDrop :: Int -> Stream m a -> Stream m a -> SLazyCon m (Stream m a)+  STake :: Int -> Stream m a -> SLazyCon m (Stream m a)++instance MonadInherit m => HasStep (SLazyCon m) m where+  step (SAppend xs ys) = sappend xs ys+  step (SRevDrop n xs ys) = srevdrop n xs ys+  step (STake n xs) = stake n xs++-- | Smart destructor for streams, consuming one credit+smatch :: MonadInherit m => Stream m a -- ^ Scrutinee+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b -- ^ Nil case+       -> m b+smatch x cons nil = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++-- | delay a computation, consuming all credits+taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)+taildelay t = delay t >>= \x -> creditAllTo x >> pure (SIndirect x)++stake :: MonadInherit m => Int -> Stream m a -> m (Stream m a)+stake 0 xs = pure SNil+stake n xs = smatch xs+  (\x xs -> SCons x <$> taildelay (STake (n - 1) xs))+  (pure SNil)++srevdrop :: MonadInherit m => Int -> Stream m a -> Stream m a -> m (Stream m a)+srevdrop 0 xs ys = smatch xs+  (\x xs -> taildelay (SRevDrop 0 xs (SCons x ys)))+  (pure ys)+srevdrop n xs ys = smatch xs+  (\x xs -> taildelay (SRevDrop (n - 1) xs ys))+  (fail "drop: empty stream")++credit :: MonadInherit m => Credit -> Stream m a -> m ()+credit n (SIndirect i) = creditWith i n+credit _ _ = pure ()++evalone :: MonadInherit m => Stream m a -> m ()+evalone (SIndirect i) = force i >> pure ()+evalone _ = pure ()++eval :: MonadInherit m => Int -> Stream m a -> m ()+eval 0 s = pure ()+eval n s = evalone s >> eval (n - 1) s++sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)+sappend xs ys = credit (fromIntegral c) ys >> eval c ys >> smatch xs+  (\x xs -> SCons x <$> taildelay (SAppend xs ys))+  (pure ys)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where+  prettyCell (SAppend xs ys) = do+    xs' <- prettyCell xs+    ys' <- prettyCell ys+    pure $ mkMCell "SAppend" [xs', ys']+  prettyCell (SRevDrop n xs ys) = do+    n' <- prettyCell n+    xs' <- prettyCell xs+    ys' <- prettyCell ys+    pure $ mkMCell "SRevDrop" [n', xs', ys']+  prettyCell (STake n xs) = do+    n' <- prettyCell n+    xs' <- prettyCell xs+    pure $ mkMCell "STake" [n', xs']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t
+ src/Test/Credit/Finger.hs view
@@ -0,0 +1,618 @@+{-# LANGUAGE GADTs, OverloadedLists, LambdaCase #-}++module Test.Credit.Finger where++import Prelude hiding (head, tail, last, init)+import Data.List.NonEmpty (NonEmpty(..), (<|))+import qualified Data.List.NonEmpty as NE+import Control.Monad (when, unless)+import Data.Foldable (foldlM, foldrM)+import Prettyprinter (Pretty)++import Control.Monad.Credit+import Test.Credit (linear, log2)+import qualified Test.Credit.Deque.Base as D+import qualified Test.Credit.Heap.Base as H+import qualified Test.Credit.RandomAccess.Base as RA+import qualified Test.Credit.Sortable.Base as S++data Digit a = One a | Two a a | Three a a a+  deriving (Eq, Ord, Show)++data Tuple v a = Pair v a a | Triple v a a a+  deriving (Eq, Ord, Show)++data FingerTree v a m+  = Empty+  | Single a+  | Deep (Thunk m (Lazy m) v) (Digit a) (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) (Digit a)++data FLazyCon m a where+  FPure :: a -> FLazyCon m a+  FCons :: Measured a v => a -> Thunk m (FLazyCon m) (FingerTree v a m) -> FLazyCon m (FingerTree v a m)+  FSnoc :: Measured a v => Thunk m (FLazyCon m) (FingerTree v a m) -> a -> FLazyCon m (FingerTree v a m)+  FTail :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)+  FInit :: Measured a v => FingerTree v a m -> FLazyCon m (FingerTree v a m)++instance MonadCredit m => HasStep (FLazyCon m) m where+  step (FPure xs) = pure xs+  step (FCons x m) = cons x =<< force m+  step (FSnoc m x) = flip snoc x =<< force m+  step (FTail q) = tail q+  step (FInit q) = init q++-- Main idea:+--  - cons, snoc, tail and init all cost two credits+--  - the first credit is used to tick+--  - We maintain the invariant: In each queue Deep(f, m, r), m has ||f| - 2| + ||r| - 2| credits.+--  - The m thunk requires two credits to force.+--  - snoc and tail spend their second credit on either the old m to be able to force it,+--    or on the new m to maintain the invariant.++class Monoid v => Measured a v where+  measure :: a -> v++instance Measured a v => Measured [a] v where+  measure = mconcat . map measure++instance Measured a v => Measured (Digit a) v where+  measure = measure . toList++instance Monoid v => Measured (Tuple v a) v where+  measure (Pair v _ _) = v+  measure (Triple v _ _ _) = v++measurement :: (MonadCredit m, Measured a v) => FingerTree v a m -> m v+measurement Empty = pure $ mempty+measurement (Single x) = pure $ measure x+measurement (Deep vm f m r) = do+  vm' <- force vm+  pure $ measure f <> vm' <> measure r++forceAll :: (MonadCredit m, Measured a v) => FingerTree v a m -> m ()+forceAll Empty = pure ()+forceAll (Single _) = pure ()+forceAll (Deep _ _ m _) = do+  creditWith m 2+  forceAll =<< force m++isTwo :: Digit a -> Bool+isTwo (Two _ _) = True+isTwo _ = False++empty :: MonadCredit m => m (Thunk m (FLazyCon m) (FingerTree v a m))+empty = delay $ FPure Empty++pair :: Measured a v => a -> a -> Tuple v a+pair x y = Pair (measure x <> measure y) x y++triple :: Measured a v => a -> a -> a -> Tuple v a+triple x y z = Triple (measure x <> measure y <> measure z) x y z++deep :: (MonadCredit m, Measured a v) => Thunk m (Lazy m) v -> Digit a -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)+deep v f m r = do+  let oneIfDangerous d = if isTwo d then 0 else 1+  mIsPure <- lazymatch m (\_ -> pure True) $ \case+    FPure _ -> pure True+    _ -> pure False+  unless mIsPure $+    m `hasAtLeast` (oneIfDangerous f + oneIfDangerous r)+  pure $ Deep v f m r++deep' :: (MonadCredit m, Measured a v) => Digit a -> m (Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m)) -> Digit a -> m (FingerTree v a m)+deep' f mkM r = do+  m <- mkM+  vm <- delay $ Lazy $ measurement =<< force m+  deep vm f m r++isEmpty :: FingerTree v a m -> Bool+isEmpty Empty = True+isEmpty _ = False++toList :: Digit a -> [a]+toList (One x) = [x]+toList (Two x y) = [x, y]+toList (Three x y z) = [x, y, z]++toTree :: (MonadCredit m, Measured a v) => [a] -> m (FingerTree v a m)+toTree [] = pure Empty+toTree [x] = pure $ Single x+toTree [x,y] = deep' (One x) empty (One y)+toTree [x,y,z] = deep' (Two x y) empty (One z)++toDigit :: Tuple v a -> Digit a+toDigit (Pair _ x y) = Two x y+toDigit (Triple _ x y z) = Three x y z++cons :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)+cons x q = tick >> cons' x q++cons' :: (MonadCredit m, Measured a v) => a -> FingerTree v a m -> m (FingerTree v a m)+cons' x Empty = pure $ Single x+cons' x (Single y) = do+  deep' (One x) empty (One y)+cons' x (Deep vq pr q u) = case pr of+  One y       -> deep vq (Two x y) q u+  Two y z     -> creditWith q 1 >> pure (Deep vq (Three x y z) q u)+  Three y z w -> do+    q' <- delay $ FCons (pair z w) q+    if isTwo u+      then creditWith q 1+      else creditWith q' 1+    vq' <- delay $ Lazy $ measurement =<< force q'+    deep vq' (Two x y) q' u++head :: MonadCredit m => FingerTree v a m -> m a+head Empty = fail "head: empty queue"+head (Single x) = pure x+head (Deep _ s _ _) = pure $ let (h:_) = toList s in h++tail :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)+tail Empty = tick >> pure Empty+tail (Single _) = tick >> pure Empty+tail (Deep vq (Three _ x y) q u) = tick >> pure (Deep vq (Two x y) q u)+tail (Deep vq (Two _ x) q u) = tick >> creditWith q 1 >> pure (Deep vq (One x) q u)+tail (Deep _ (One _) q u) = tick >> do+  when (isTwo u) $ creditWith q 1+  q' <- force q+  deep0 q' u++deep0 :: (MonadCredit m, Measured a v) => FingerTree v (Tuple v a) m -> Digit a -> m (FingerTree v a m)+deep0 Empty s = toTree $ toList s+deep0 q u = do+  h <- head q+  case h of+    Pair _ x y -> do+      t <- delay $ FTail q+      unless (isTwo u) $ creditWith t 1+      vt <- delay $ Lazy $ measurement =<< force t+      deep vt (Two x y) t u+    Triple _ x _ _ -> do+      q' <- map1 chop q+      deep' (One x) (delay $ FPure q') u+      where chop (Triple _ _ y z) = pair y z++map1 :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)+map1 _ Empty = pure Empty+map1 f (Single x) = pure $ Single (f x)+map1 f (Deep vq (One x) q u) = deep vq (One (f x)) q u+map1 f (Deep vq (Two x y) q u) = deep vq (Two (f x) y) q u+map1 f (Deep vq (Three x y z) q u) = deep vq (Three (f x) y z) q u++uncons :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (a, FingerTree v a m))+uncons q =+  if isEmpty q+    then pure Nothing+    else do+      h <- head q+      t <- tail q+      pure $ Just (h, t)++deepL :: (MonadCredit m, Measured a v) => [a] -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> Digit a -> m (FingerTree v a m)+deepL [] _ m sf = do+  m' <- uncons =<< force m+  case m' of+    Nothing -> toTree $ toList sf+    Just (Pair _ x y, m'') -> do+      deep' (Two x y) (delay $ FPure m'') sf+    Just (Triple _ x y z, m'') -> do+      deep' (Three x y z) (delay $ FPure m'') sf+deepL [x] vm m sf = deep vm (One x) m sf+deepL [x,y] vm m sf = deep vm (Two x y) m sf+deepL [x,y,z] vm m sf = deep vm (Three x y z) m sf++last :: (MonadCredit m, Measured a v) => FingerTree v a m -> m a+last Empty = fail "last: empty queue"+last (Single x) = pure x+last (Deep _ _ _ s) = pure $ let (h:_) = reverse $ toList s in h++snoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)+snoc q y = tick >> snoc' q y++snoc' :: (MonadCredit m, Measured a v) => FingerTree v a m -> a -> m (FingerTree v a m)+snoc' Empty y = pure $ Single y+snoc' (Single x) y = deep' (One x) empty (One y)+snoc' (Deep vq u q (One x)) y = deep vq u q (Two x y)+snoc' (Deep vq u q (Two x y)) z = creditWith q 1 >> pure (Deep vq u q (Three x y z))+snoc' (Deep _ u q (Three x y z)) w = do+  q' <- delay $ FSnoc q (pair x y)+  if isTwo u+    then creditWith q 1+    else creditWith q' 1+  vq' <- delay $ Lazy $ measurement =<< force q'+  deep vq' u q' (Two z w)++init :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (FingerTree v a m)+init Empty = tick >> pure Empty+init (Single _) = tick >> pure Empty+init (Deep vq u q (Three x y _)) = tick >> pure (Deep vq u q (Two x y))+init (Deep vq u q (Two x _)) = tick >> creditWith q 1 >> pure (Deep vq u q (One x))+init (Deep _ u q (One _)) = tick >> when (isTwo u) (creditWith q 1) >> force q >>= deepN u++deepN :: (MonadCredit m, Measured a v) => Digit a -> FingerTree v (Tuple v a) m -> m (FingerTree v a m)+deepN s Empty = toTree $ toList s+deepN u q = do+  l <- last q+  case l of+    Pair _ x y -> do+      t <- delay $ FInit q+      unless (isTwo u) $ creditWith t 1+      vt <- delay $ Lazy $ measurement =<< force t+      deep vt u t (Two x y)+    Triple _ _ _ z -> do+      q' <- mapN chop q+      deep' u (delay $ FPure q') (One z)+      where chop (Triple _ x y _) = pair x y++mapN :: (MonadCredit m, Measured a v) => (a -> a) -> FingerTree v a m -> m (FingerTree v a m)+mapN _ Empty = pure $ Empty+mapN f (Single x) = pure $ Single (f x)+mapN f (Deep vq u q (One x)) = deep vq u q (One (f x))+mapN f (Deep vq u q (Two x y)) = deep vq u q (Two x (f y))+mapN f (Deep vq u q (Three x y z)) = deep vq u q (Three x y (f z))++unsnoc :: (MonadCredit m, Measured a v) => FingerTree v a m -> m (Maybe (FingerTree v a m, a))+unsnoc q =+  if isEmpty q+    then pure Nothing+    else do+      h <- last q+      t <- init q+      pure $ Just (t, h)++deepR :: (MonadCredit m, Measured a v) => Digit a -> Thunk m (Lazy m) v -> Thunk m (FLazyCon m) (FingerTree v (Tuple v a) m) -> [a] -> m (FingerTree v a m)+deepR s _ m [] = do+  m' <- unsnoc =<< force m+  case m' of+    Nothing -> toTree $ toList s+    Just (m'', Pair _ x y) -> do+      deep' s (delay $ FPure m'') (Two x y)+    Just (m'', Triple _ x y z) -> do+      deep' s (delay $ FPure m'') (Three x y z)+deepR s vm m [x] = deep vm s m (One x)+deepR s vm m [x, y] = deep vm s m (Two x y)+deepR s vm m [x, y, z] = deep vm s m (Three x y z)++toTuples :: Measured a v => [a] -> [Tuple v a]+toTuples [] = []+toTuples [x, y] = [pair x y]+toTuples [x, y, z, w] = [pair x y, pair z w]+toTuples (x : y : z : xs) = triple x y z : toTuples xs++glue :: (MonadCredit m, Measured a v) => FingerTree v a m -> [a] -> FingerTree v a m -> m (FingerTree v a m)+glue Empty as q2 = foldrM cons q2 as+glue q1 as Empty = foldlM snoc q1 as+glue (Single x) as q2 = foldrM cons q2 (x : as)+glue q1 as (Single y) = foldlM snoc q1 (as ++ [y])+glue (Deep _ u1 q1 v1) as (Deep _ u2 q2 v2) = tick >> do+  creditWith q1 2+  q1 <- force q1+  creditWith q2 2+  q2 <- force q2+  q <- glue q1 (toTuples (toList v1 ++ as ++ toList u2)) q2+  deep' u1 (delay $ FPure q) v2++concat' :: (MonadCredit m, Measured a v) => FingerTree v a m -> FingerTree v a m -> m (FingerTree v a m)+concat' q1 q2 = glue q1 [] q2++data Split v a m = Split+  { measureOfSmaller :: v+  , smaller :: FingerTree v a m+  , found   :: a+  , bigger  :: FingerTree v a m+  }++splitDigit :: Measured a v => (v -> Bool) -> v -> Digit a -> ([a], a, [a])+splitDigit p i (One x) = ([], x, [])+splitDigit p i (Two x y)+  | p (i <> measure x) = ([], x, [y])+  | otherwise = ([x], y, [])+splitDigit p i (Three x y z)+  | p (i <> measure x) = ([], x, [y, z])+  | p (i <> measure x <> measure y) = ([x], y, [z])+  | otherwise = ([x, y], z, [])++-- For '(Split vml ml xs mr) <- splitTree p i m', we have 'vml = measurement ml'.+splitTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Split v a m)+splitTree p i Empty = fail "splitTree: empty tree"+splitTree p i (Single x) = pure $ Split mempty Empty x Empty+splitTree p i (Deep vm pr m sf) = tick >> do+  vm' <- force vm+  let vpr = i <> measure pr+  let vprm = vpr <> vm'+  if p vpr then do+    let (l, x, r) = splitDigit p i pr+    Split (measure l) <$> toTree l <*> pure x <*> deepL r vm m sf+  else if p vprm then do+    Split vml ml xs mr <- splitTree p vpr =<< force m+    let (l, x, r) = splitDigit p (vpr <> vml) (toDigit xs)+    -- [ml', mr', vmr', vml'] <- mapM (delay . Lazy)+      -- [pure ml, pure mr, measurement mr, pure vml]+    ml' <- delay $ FPure ml+    mr' <- delay $ FPure mr+    vmr' <- delay $ Lazy $ measurement mr+    vml' <- delay $ Lazy $ pure vml+    Split (measure pr <> vml <> measure l) <$> deepR pr vml' ml' l <*> pure x <*> deepL r vmr' mr' sf+  else do+    let (l, x, r) = splitDigit p vprm sf+    Split (measure pr <> vm' <> measure l) <$> deepR pr vm m l <*> pure x <*> toTree r++split :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m, FingerTree v a m)+split p Empty = pure (Empty, Empty)+split p xs = do+  forceAll xs+  mxs <- measurement xs+  if p mxs+    then do (Split _ l x r) <- splitTree p mempty xs+            (l,) <$> cons x r+    else pure (xs, Empty)++takeUntil :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m)+takeUntil p m = fst <$> split p m++dropUntil :: (MonadCredit m, Measured a v) => (v -> Bool) -> FingerTree v a m -> m (FingerTree v a m)+dropUntil p m = snd <$> split p m++lookupTree :: (MonadCredit m, Measured a v) => (v -> Bool) -> v -> FingerTree v a m -> m (Maybe (v, a))+lookupTree p i Empty = pure Nothing+lookupTree p i t = do+  forceAll t+  (Split ml _ x _) <- splitTree p i t+  pure $ Just (i <> ml, x)++instance MemoryCell m a => MemoryCell m (Digit a) where+  prettyCell (One a) = do+    a' <- prettyCell a+    pure $ mkMCell "One" [a']+  prettyCell (Two a b) = do+    a' <- prettyCell a+    b' <- prettyCell b+    pure $ mkMCell "Two" [a', b']+  prettyCell (Three a b c) = do+    a' <- prettyCell a+    b' <- prettyCell b+    c' <- prettyCell c+    pure $ mkMCell "Three" [a', b', c']++instance MemoryCell m a => MemoryCell m (Tuple v a) where+  prettyCell (Pair _ a b) = do+    a' <- prettyCell a+    b' <- prettyCell b+    pure $ mkMCell "Pair" [a', b']+  prettyCell (Triple _ a b c) = do+    a' <- prettyCell a+    b' <- prettyCell b+    c' <- prettyCell c+    pure $ mkMCell "Triple" [a', b', c']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FLazyCon m a) where+  prettyCell (FPure x) = do+    x' <- prettyCell x+    pure $ mkMCell "FPure" [x']+  prettyCell (FCons x m) = do+    -- x' <- prettyCell x+    m' <- prettyCell m+    pure $ mkMCell "FCons" [m']+  prettyCell (FSnoc m x) = do+    m' <- prettyCell m+    -- x' <- prettyCell x+    pure $ mkMCell "FSnoc" [m']+  prettyCell (FTail q) = do+    q' <- prettyCell q+    pure $ mkMCell "FTail" [q']+  prettyCell (FInit q) = do+    q' <- prettyCell q+    pure $ mkMCell "FInit" [q']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerTree v a m) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (Single a) = do+    a' <- prettyCell a+    pure $ mkMCell "Single" [a']+  prettyCell (Deep _ s q u) = do+    s' <- prettyCell s+    q' <- prettyCell q+    u' <- prettyCell u+    pure $ mkMCell "Deep" [s', q', u']++instance Pretty a => MemoryStructure (FingerTree v (PrettyCell a)) where+  prettyStructure = prettyCell++newtype Elem a = Elem a+  deriving (Eq, Ord, Show)++instance (MemoryCell m a) => MemoryCell m (Elem a) where+  prettyCell (Elem x) = prettyCell x++-- Deque++instance Measured (Elem a) () where+  measure (Elem x) = ()++newtype FingerDeque a m = FingerDeque (FingerTree () (Elem a) m)++instance D.Deque FingerDeque where+  empty = pure $ FingerDeque Empty+  cons x (FingerDeque q) = FingerDeque <$> cons (Elem x) q+  snoc (FingerDeque q) x = FingerDeque <$> snoc q (Elem x)+  uncons (FingerDeque q) = do+    m <- uncons q+    case m of+      Nothing -> pure Nothing+      Just (Elem x, q') -> pure $ Just (x, FingerDeque q')+  unsnoc (FingerDeque q) = do+    m <- unsnoc q+    case m of+      Nothing -> pure Nothing+      Just (q', Elem x) -> pure $ Just (FingerDeque q', x)+  concat (FingerDeque q1) (FingerDeque q2) = FingerDeque <$> concat' q1 q2++instance D.BoundedDeque FingerDeque where+  qcost _ (D.Cons _) = 2+  qcost _ (D.Snoc _) = 2+  qcost _ D.Uncons = 4+  qcost _ D.Unsnoc = 2+  qcost n D.Concat = 5 * log2 n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerDeque a m) where+  prettyCell (FingerDeque q) = prettyCell q++instance Pretty a => MemoryStructure (FingerDeque (PrettyCell a)) where+  prettyStructure = prettyCell++-- Random Access++newtype Size = Size Int+  deriving (Eq, Ord, Show, Num)++instance Semigroup Size where+  x <> y = x + y++instance Monoid Size where+  mempty = 0++instance Measured (Elem a) Size where+  measure (Elem x) = 1++newtype FingerRA a m = FingerRA (FingerTree Size (Elem a) m)++-- Contrary to Hinze and Paterson, this is not O(1) but O(log n)+-- because we need to force all thunks in the tree to get the size.+length :: MonadCredit m => FingerRA a m -> m Size+length (FingerRA t) = measurement t++splitAt :: MonadCredit m => Int -> FingerRA a m -> m (FingerRA a m, FingerRA a m)+splitAt i (FingerRA xs) = do+   (l, r) <- split (fromIntegral i <) xs+   pure $ (FingerRA l, FingerRA r)++instance RA.RandomAccess FingerRA where+  empty = pure $ FingerRA Empty+  cons x (FingerRA q) = FingerRA <$> cons (Elem x) q+  uncons (FingerRA q) = do+    m <- uncons q+    case m of+      Nothing -> pure Nothing+      Just (Elem x, m') -> do+        pure $ Just (x, FingerRA m')+  lookup i (FingerRA Empty) = pure Nothing+  lookup i (FingerRA xs) = do+    forceAll xs+    (Split _ _ (Elem x) _) <- splitTree (fromIntegral i <) 0 xs+    pure $ Just x+  update i a (FingerRA Empty) = pure $ FingerRA Empty+  update i a (FingerRA xs) = do+    forceAll xs+    (Split ml l (Elem x) r) <- splitTree (fromIntegral i <) 0 xs+    if fromIntegral i > ml+      then FingerRA <$> snoc l (Elem x)+      else FingerRA <$> (concat' l =<< cons (Elem a) r)++instance RA.BoundedRandomAccess FingerRA where+  qcost n (RA.Cons _) = 2+  qcost n RA.Uncons = 2+  qcost n (RA.Lookup i) = 5 * log2 n+  qcost n (RA.Update i _) = 2 + 10 * log2 n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerRA a m) where+  prettyCell (FingerRA q) = prettyCell q++instance Pretty a => MemoryStructure (FingerRA (PrettyCell a)) where+  prettyStructure = prettyCell++-- Heap++data Prio a = MInfty | Prio a+  deriving (Eq, Ord, Show)++instance Ord a => Semigroup (Prio a) where+  MInfty <> p = p+  p <> MInfty = p+  Prio x <> Prio y = Prio (min x y)++instance Ord a => Monoid (Prio a) where+  mempty = MInfty++instance Ord a => Measured (Elem a) (Prio a) where+  measure (Elem x) = Prio x++newtype FingerHeap a m = FingerHeap (FingerTree (Prio a) (Elem a) m)++instance H.Heap FingerHeap where+  empty = pure $ FingerHeap Empty+  insert x (FingerHeap xs) = FingerHeap <$> cons (Elem x) xs+  merge (FingerHeap a) (FingerHeap b) = FingerHeap <$> concat' a b+  splitMin (FingerHeap Empty) = pure Nothing+  splitMin (FingerHeap xs) = do+    forceAll xs -- 2 * log n+    k <- measurement xs+    (Split _ l (Elem x) r) <- splitTree (k >=) mempty xs -- 3 * log n+    lr <- concat' l r -- 5 log n+    pure $ Just (x, FingerHeap lr)++instance H.BoundedHeap FingerHeap where+  hcost n (H.Insert _) = 2+  hcost n H.Merge = 5 * log2 n+  hcost n H.SplitMin = 1 + 10 * log2 (n + 1)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerHeap a m) where+  prettyCell (FingerHeap q) = prettyCell q++instance Pretty a => MemoryStructure (FingerHeap (PrettyCell a)) where+  prettyStructure = prettyCell++-- Sortable Collection++data Key a = NoKey | Key a+  deriving (Eq, Ord, Show)++instance Semigroup (Key a) where+  k <> NoKey = k+  _ <> k = k++instance Monoid (Key a) where+  mempty = NoKey++instance Measured (Elem a) (Key a) where+  measure (Elem x) = Key x++newtype FingerSort a m = FingerSort (FingerTree (Key a) (Elem a) m)++rev :: MonadCredit m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc) ++append :: MonadCredit m => [a] -> [a] -> m [a]+append [] ys = pure ys+append (x : xs) ys = tick >> fmap (x:) (append xs ys)++treeToList :: MonadCredit m => [b] -> (a -> m [b]) -> FingerTree v a m -> m [b]+treeToList acc f Empty = rev acc []+treeToList acc f (Single x) = do+  fx <- f x+  flip rev [] =<< append fx acc+treeToList acc f (Deep _ s q u) = do+  s' <- fmap (concatMap id) $ traverse f $ toList s+  u' <- fmap (concatMap id) $ traverse f $ toList u+  creditWith q 2+  q' <- treeToList (u' ++ acc) (fmap (concatMap id) . traverse f . toList . toDigit) =<< force q+  append s' q'++instance S.Sortable FingerSort where+  empty = pure $ FingerSort Empty+  add x (FingerSort xs) = do+    (l, r) <- split (>= Key x) xs+    lxr <- concat' l =<< cons (Elem x) r+    pure $ FingerSort lxr+  sort (FingerSort xs) = do+    treeToList [] (\(Elem x) -> tick >> pure [x]) xs++instance S.BoundedSortable FingerSort where+  scost n (S.Add _) = 1 + 10 * log2 (n + 1)+  scost n S.Sort = 2 * log2 n + 3 * linear n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (FingerSort a m) where+  prettyCell (FingerSort q) = prettyCell q++instance Pretty a => MemoryStructure (FingerSort (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Heap/Base.hs view
@@ -0,0 +1,96 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}++module Test.Credit.Heap.Base (HeapOp(..), Heap(..), BoundedHeap(..), H, BH) where++import Control.Monad.Credit+import Test.Credit+import Test.QuickCheck++data HeapOp a = Insert a | Merge | SplitMin+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (HeapOp a) where+  arbitrary = frequency+    [ (6, Insert <$> arbitrary)+    , (3, pure SplitMin)+    , (1, pure Merge)+    ]++class Heap h where+  empty :: MonadCredit m => m (h a m)+  insert :: MonadCredit m => Ord a => a -> h a m -> m (h a m)+  merge :: MonadCredit m => Ord a => h a m -> h a m -> m (h a m)+  splitMin :: MonadCredit m => Ord a => h a m -> m (Maybe (a, h a m))++class Heap h => BoundedHeap h where+  hcost :: Size -> HeapOp a -> Credit++data H h a m = E | H Size (h (PrettyCell a) m)++instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (H h a m) where+  prettyCell E = pure $ mkMCell "" []+  prettyCell (H _ h) = prettyCell h++instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (H h a) where+  prettyStructure E = pure $ mkMCell "" []+  prettyStructure (H _ h) = prettyStructure h++act :: (MonadCredit m, Heap h, Ord a) => Size -> h (PrettyCell a) m -> HeapOp a -> m (H h a m)+act sz h (Insert x) = H (sz + 1) <$> insert (PrettyCell x) h+act sz h Merge = pure $ H sz h+act sz h SplitMin = do+  m <- splitMin h+  case m of+    Nothing -> pure E+    Just (_, h') -> pure $ H (max 0 (sz - 1)) h'++instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (H h a) (HeapOp a) where+  create = E+  action E op = (hcost @h 0 op, empty >>= flip (act 0) op)+  action (H sz h) op = (hcost @h sz op, act sz h op)++size :: H h a m -> Size+size E = 0+size (H sz _) = sz++data BH h a m = BH (H h a m) (H h a m)++instance (MemoryCell m (h (PrettyCell a) m)) => MemoryCell m (BH h a m) where+  prettyCell (BH h1 h2) = do+    h1' <- prettyCell h1+    h2' <- prettyCell h2+    pure $ mkMCell "Merge" [h1', h2']++instance (MemoryStructure (h (PrettyCell a))) => MemoryStructure (BH h a) where+  prettyStructure (BH h1 h2) = do+    h1' <- prettyStructure h1+    h2' <- prettyStructure h2+    pure $ mkMCell "Merge" [h1', h2']++act1 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)+act1 op (BH h1 h2) = do+  h1' <- case h1 of+    E -> empty+    H _ h -> pure h+  h1'' <- act (size h1) h1' op +  pure $ BH h1'' h2++act2 :: (MonadInherit m, Heap h, Ord a) => HeapOp a -> BH h a m -> m (BH h a m)+act2 op (BH h1 h2) = do+  h2' <- case h2 of+    E -> empty+    H _ h -> pure h+  h2'' <- act (size h2) h2' op +  pure $ BH h1 h2''++mergeH :: (MonadInherit m, Heap h, Ord a) => H h a m -> H h a m -> m (H h a m)+mergeH E E = pure E+mergeH (H sz1 h1) E = pure $ H sz1 h1+mergeH E (H sz2 h2) = pure $ H sz2 h2+mergeH (H sz1 h1) (H sz2 h2) = H (sz1 + sz2) <$> merge h1 h2++instance (Arbitrary a, Ord a, BoundedHeap h, Show a) => DataStructure (BH h a) (HeapOp a) where+  create = BH E E+  action (BH h1 h2) (Insert a) = (hcost @h (size h1) (Insert a),      act1 (Insert a) (BH h1 h2))+  action (BH h1 h2) SplitMin   = (hcost @h (size h2) SplitMin,        act2 SplitMin (BH h1 h2))+  action (BH h1 h2) Merge      = (hcost @h (size h1 + size h2) Merge, BH E <$> mergeH h1 h2)
+ src/Test/Credit/Heap/Binomial.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE TypeFamilies #-}++module Test.Credit.Heap.Binomial where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Heap.Base++data Tree a = Node Int a [Tree a]+  deriving (Eq, Ord, Show)++rank :: Tree a -> Int+rank (Node r _ _) = r++root :: Tree a -> a+root (Node _ x _) = x++rev :: MonadCredit m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc)++link :: Ord a => Tree a -> Tree a -> Tree a+link t1@(Node r x1 c1) t2@(Node _ x2 c2)+  | x1 <= x2 = Node (r+1) x1 (t2:c1)+  | otherwise = Node (r+1) x2 (t1:c2)++insTree :: MonadCredit m => Ord a => Tree a -> [Tree a] -> m [Tree a]+insTree t [] = pure [t]+insTree t ts@(t':ts')+  | rank t < rank t' = pure $ t:ts+  | otherwise = tick >> insTree (link t t') ts'++mrg :: MonadCredit m => Ord a => [Tree a] -> [Tree a] -> m [Tree a]+mrg ts1 [] = pure ts1+mrg [] ts2 = pure ts2+mrg ts1@(t1:ts1') ts2@(t2:ts2')+  | rank t1 < rank t2 = tick >> (t1 :) <$> mrg ts1' ts2+  | rank t2 < rank t1 = tick >> (t2 :) <$> mrg ts1 ts2'+  | otherwise = tick >> do+    insTree (link t1 t2) =<< mrg ts1' ts2'++removeMinTree :: MonadCredit m => Ord a => [Tree a] -> m (Tree a, [Tree a])+removeMinTree [] = error "removeMinTree"+removeMinTree [t] = pure (t, [])+removeMinTree (t:ts) = tick >> do+  (t', ts') <- removeMinTree ts+  pure $ if root t <= root t' then (t, ts) else (t', t:ts')++data Binomial a m = Binomial Size (Thunk m (Lazy m) [Tree a])++allZeros :: Size -> Credit+allZeros 0 = 0+allZeros n = (fromIntegral $ (n + 1) `mod` 2) + allZeros (n `div` 2)++instance Heap Binomial where+  empty = do+    t <- delay $ Lazy $ pure []+    pure $ Binomial 0 t+  insert x (Binomial n h) = do+    ts <- delay $ Lazy $ do +      creditWith h (allZeros n)+      h' <- force h+      insTree (Node 0 x []) h'+    creditWith ts 2+    pure $ Binomial (n + 1) ts+  merge (Binomial n1 t1) (Binomial n2 t2) = do+    t1 `creditWith` (allZeros n1)+    ts1 <- force t1+    t2 `creditWith` (allZeros n2)+    ts2 <- force t2+    ts <- delay $ Lazy $ mrg ts1 ts2+    ts `creditWith` (log2 (n1 + n2))+    pure $ Binomial (n1 + n2) ts+  splitMin (Binomial n t) = do+    creditWith t (log2 n)+    ts <- force t+    case ts of+      [] -> pure Nothing+      _ -> do+        (Node _ x ts1, ts2) <- removeMinTree ts+        t' <- delay $ Lazy $ do+          rts1 <- rev ts1 []+          mrg rts1 ts2+        creditWith t' (2 * log2 n)+        pure $ Just (x, Binomial (max 0 (n - 1)) t')++instance BoundedHeap Binomial where+  hcost _ (Insert _) = 2+  hcost n Merge = 3 * log2 n+  hcost n SplitMin = 4 * log2 n++instance MemoryCell m a => MemoryCell m (Tree a) where+  prettyCell (Node r x c) = do+    r' <- prettyCell r+    x' <- prettyCell x+    c' <- mapM prettyCell c+    pure $ mkMCell "Node" [r', x', mkMList c' Nothing]++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Binomial a m) where+  prettyCell (Binomial _ t) = do+    t' <- prettyCell t+    pure $ mkMCell "Binomial" [t']++instance Pretty a => MemoryStructure (Binomial (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Heap/LazyPairing.hs view
@@ -0,0 +1,106 @@+{-# LANGUAGE GADTs #-}++module Test.Credit.Heap.LazyPairing where++import Prettyprinter (Pretty)++import Control.Monad.Credit+import Test.Credit+import Test.Credit.Heap.Base++-- Okasaki does not present an amortized analysis and instead merely conjectures+-- that they have O(log n) amortized cost for insert and splitMin (Section 6.5).+-- An amortized analysis in a sequential setting is given by Nipkow and Brinkop+-- in 'Amortized Complexity Verified' (2019), Section 8.+-- Below we generalize it to the persistent setting.++data LazyPairing a s+  = Empty+  | Heap Size a (LazyPairing a s) (PThunk s (LazyPairing a s))+  -- ^ Changed from Okasaki is that we annotate the size of the thunk.+  --   Invariant: For 'Heap sm x a m', we have either:+  --   - 'a' is Empty and 'm' has (log2 sm) credits+  --   - 'a' is not Empty and 'm' has (2 * log2 sm) credits+  --   - Right before forcing, 'm' has (3 * log2 sm) credits++size :: LazyPairing a s -> Size+size Empty = 0+size (Heap sm _ a _) = 1 + sm + size a++data PLazyCon m a where+  Em :: PLazyCon m (LazyPairing a m)+  Link :: Ord a => Size -> LazyPairing a m -> LazyPairing a m -> Thunk m (PLazyCon m) (LazyPairing a m) -> PLazyCon m (LazyPairing a m)+  -- ^ Merging 'h = Link(a, b, m)' costs one tick and performs two links, and assigns some credits to 'm'.+  --   Because 'link a b' costs 'log2 (sa + sb)' credits, we have total costs of:+  --     2 + 2*log2 (sa + sb + sm) + 2*log2 (sa + sb) + 2*log2 sm+  --     <= 6 * log2 sh (since sa + sb + sm <= sh)++instance MonadCredit m => HasStep (PLazyCon m) m where+  step Em = pure Empty+  step (Link sm a b m) = tick >> do -- 1+    creditWith m (log2 sm) -- log2 sm+    m <- force m -- free+    ab <- link a b -- log2 (sa + sb)+    link ab m -- log2 (sa + sb + sm)++type PThunk s = Thunk s (PLazyCon s)++data NEHeap s a = NEHeap Size a (LazyPairing a s) (PThunk s (LazyPairing a s))++-- | 'mergePairs' costs up to 'log2 (sz + sa)' credits+mergePairs :: MonadCredit m => Ord a => NEHeap m a -> LazyPairing a m -> m (LazyPairing a m)+mergePairs (NEHeap sm x Empty m) a = do+  creditWith m (log2 sm)+  pure $ Heap sm x a m+mergePairs (NEHeap sm x b m) a = do+  t <- delay $ Link sm a b m+  let sz = size a + size b + sm+  creditWith t (log2 sz)+  pure $ Heap sz x Empty t++-- | 'link' costs up to 'log2 (sz + sa) + 1' credits+link :: MonadCredit m => Ord a => LazyPairing a m -> LazyPairing a m -> m (LazyPairing a m)+link a Empty = pure a+link Empty b = pure b+link a@(Heap sa x a1 a2) b@(Heap sb y b1 b2)+  | x <= y    = mergePairs (NEHeap sa x a1 a2) b+  | otherwise = mergePairs (NEHeap sb y b1 b2) a ++instance Heap LazyPairing where+  empty = pure Empty+  insert x a = do+    t <- delay $ Em+    merge (Heap 0 x Empty t) a+  -- | 'merge' costs '1 + log2 (sa + sb)' credits+  merge a b = tick >> link a b+  splitMin Empty = pure Nothing+  splitMin (Heap sm x a m) = do+    creditWith m (2 * log2 sm) -- in case 'a' is Empty+    m <- force m+    am <- merge a m+    pure $ Just (x, am)++instance BoundedHeap LazyPairing where+  hcost n (Insert _) = 1 + log2 (n + 1)+  hcost n Merge = 1 + log2 (n + 1)+  hcost n SplitMin = 1 + 3 * log2 (n + 1)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PLazyCon m a) where+  prettyCell Em = pure $ mkMCell "Empty" []+  prettyCell (Link _ a b m) = do+    a' <- prettyCell a+    b' <- prettyCell b+    m' <- prettyCell m+    pure $ mkMCell "Link" [a', b', m']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (LazyPairing a m) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (Heap sz x a m) = do+    sz' <- prettyCell sz+    x' <- prettyCell x+    a' <- prettyCell a+    m' <- prettyCell m+    pure $ mkMCell "Heap" [sz', x', a', m']++instance Pretty a => MemoryStructure (LazyPairing (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Heap/Pairing.hs view
@@ -0,0 +1,59 @@+module Test.Credit.Heap.Pairing where++import Prettyprinter (Pretty)++import Control.Monad.Credit+import Test.Credit+import Test.Credit.Heap.Base++-- Binary pairing heaps as in Exercise 5.8 of Okasaki's book.++data PairingHeap a m+  = Nil+  | Heap a (PairingHeap a m) (PairingHeap a m)++-- | At the root, the right child is Empty.+data Pairing a m = Empty | Root a (PairingHeap a m)++link :: Ord a => Pairing a m -> Pairing a m -> Pairing a m+link Empty b = b+link a Empty = a+link (Root x a) (Root y b)+  | x <= y    = Root x (Heap y b a)+  | otherwise = Root y (Heap x a b)++mergePairs :: (MonadCredit m, Ord a) => PairingHeap a m -> m (Pairing a m)+mergePairs Nil = pure $ Empty+mergePairs (Heap x a1 Nil) = pure $ Root x a1+mergePairs (Heap x a1 (Heap y a2 a3)) = tick >> link ((link (Root x a1) (Root y a2))) <$> mergePairs a3++instance Heap Pairing where+  empty = pure Empty+  insert x h = merge (Root x Nil) h+  merge a b = tick >> pure (link a b)+  splitMin Empty = pure Nothing+  splitMin (Root x h) = Just . (x,) <$> mergePairs h++-- We can only prove a log(n) bound for insert, but this seems to work (as conjectured by Okasaki and others).+instance BoundedHeap Pairing where+  hcost n (Insert _) = 1+  hcost n Merge = 1+  hcost n SplitMin = 5 * log2 (n + 1)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PairingHeap a m) where+  prettyCell Nil = pure $ mkMCell "Nil" []+  prettyCell (Heap a l r) = do+    a' <- prettyCell a+    l' <- prettyCell l+    r' <- prettyCell r+    pure $ mkMCell "Heap" [a', l', r']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Pairing a m) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (Root a l) = do+    a' <- prettyCell a+    l' <- prettyCell l+    pure $ mkMCell "Root" [a', l']++instance Pretty a => MemoryStructure (Pairing (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Heap/Scheduled.hs view
@@ -0,0 +1,153 @@+{-# LANGUAGE TypeFamilies #-}++module Test.Credit.Heap.Scheduled where++import Prettyprinter (Pretty)+import Control.Monad.Credit hiding (exec)+import Test.Credit+import Test.Credit.Heap.Base++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (Thunk m (Lazy m) (Stream m a))++indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)+indirect = fmap SIndirect . delay . Lazy++credit :: MonadCredit m => Credit -> Stream m a -> m ()+credit cr (SIndirect i) = creditWith i cr+credit _ _ = pure ()++-- | Smart destructor for streams, consuming one credit+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee+       -> m b -- ^ Nil case+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b+smatch x nil cons = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++data Tree a = Node a [Tree a]+  deriving (Eq, Ord, Show)++data Digit a = Zero | One (Tree a)+  deriving (Eq, Ord, Show)++type Schedule m a = [Stream m (Digit a)]++data Scheduled a m = Scheduled (Stream m (Digit a)) (Schedule m a)++link :: Ord a => Tree a -> Tree a -> Tree a+link t1@(Node x1 c1) t2@(Node x2 c2)+  | x1 <= x2 = Node x1 (t2:c1)+  | otherwise = Node x2 (t1:c2)++insTree :: MonadCredit m => Ord a => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))+insTree t s = smatch s+  (pure $ SCons (One t) SNil)+  (\d ds -> case d of+    Zero -> pure $ SCons (One t) ds+    One t' -> indirect $ do+      SCons Zero <$> insTree (link t t') ds)++mrg :: MonadCredit m => Ord a => Stream m (Digit a) -> Stream m (Digit a) -> m (Stream m (Digit a))+mrg ds1 ds2 = credit 1 ds1 >> smatch ds1+  (pure ds2)+  (\d1 ds1 -> credit 1 ds1 >> smatch ds2+    (pure $ SCons d1 ds1)+    (\d2 ds2 -> case (d1, d2) of+      (Zero, _) -> SCons d2 <$> mrg ds1 ds2+      (_, Zero) -> SCons d1 <$> mrg ds1 ds2+      (One t1, One t2) -> SCons Zero <$> (insTree (link t1 t2) =<< mrg ds1 ds2)))++normalize :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Stream m (Digit a))+normalize ds = credit 1 ds >> smatch ds+    (pure SNil)+    (\d ds -> SCons d <$> normalize ds)++exec :: MonadCredit m => Schedule m a -> m (Schedule m a)+exec [] = pure []+exec (ds:dss) = credit 1 ds >> smatch ds+  (pure dss)+  (\d job -> case d of+    Zero -> pure $ job:dss+    One _ -> pure dss)++removeMinTree :: MonadCredit m => Ord a => Stream m (Digit a) -> m (Tree a, Stream m (Digit a))+removeMinTree ds = credit 1 ds >> smatch ds+  (fail "removeMinTree: empty stream")+  (\d ds -> case d of+      Zero -> do +        (t', ds') <- removeMinTree ds+        pure (t', SCons Zero ds')+      One (t@(Node x _)) -> credit 1 ds >> smatch ds+        (pure (t, SNil))+        (\_ _ -> do+          (t'@(Node x' _), ds') <- removeMinTree ds+          if x <= x'+            then pure (t, SCons Zero ds)+            else pure (t', SCons (One t) ds')))++revOneStream :: MonadCredit m => [Tree a] -> Stream m (Digit a) -> m (Stream m (Digit a))+revOneStream [] acc = pure acc+revOneStream (t:ts) acc = tick >> revOneStream ts (SCons (One t) acc)++instance Heap Scheduled where+  empty = pure $ Scheduled SNil []+  insert x (Scheduled ds sched) = do+    ds' <- insTree (Node x []) ds -- 1+    sched' <- exec =<< exec (ds':sched) -- 2 + 2+    pure $ Scheduled ds' sched'+  merge (Scheduled ds1 _) (Scheduled ds2 _) = do+    normalize ds1 -- log2 n1+    normalize ds2 -- log2 n2+    ds <- mrg ds1 ds2 -- 5 * log2 (n1 + n2)+    normalize ds -- log2 (n1 + n2)+    pure $ Scheduled ds []+  splitMin (Scheduled ds sched) = smatch ds+    (pure Nothing)+    (\_ _ -> do+      (Node x c, ds') <- removeMinTree ds -- 4 * log2 n+      c' <- revOneStream c SNil -- log2 n+      ds'' <- mrg c' ds' -- 5 * log2 (n1 + n2)+      normalize ds'' -- log2 (n1 + n2)+      pure (Just (x, Scheduled ds'' [])))++instance BoundedHeap Scheduled where+  hcost _ (Insert _) = 5+  hcost n Merge = 4 + 8 * log2 n+  hcost n SplitMin = 1 + 5 * log2 n + 6 * log2 (2 * n)++instance MemoryCell m a => MemoryCell m (Tree a) where+  prettyCell (Node x c) = do+    x' <- prettyCell x+    c' <- mapM prettyCell c+    pure $ mkMCell "Node" [x', mkMList c' Nothing]++instance MemoryCell m a => MemoryCell m (Digit a) where+  prettyCell Zero = pure $ mkMCell "Zero" []+  prettyCell (One t) = mkMCell "One" . (:[]) <$> prettyCell t++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Scheduled a m) where+  prettyCell (Scheduled ds sched) = do+    ds' <- prettyCell ds+    sched' <- mapM prettyCell sched+    pure $ mkMCell "Scheduled" [ds', mkMList sched' Nothing]++instance Pretty a => MemoryStructure (Scheduled (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Bankers.hs view
@@ -0,0 +1,62 @@+module Test.Credit.Queue.Bankers where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Queue.Base+import Test.Credit.Queue.Streams++data BQueue a m = BQueue+  { front :: Stream m a+  , flen :: !Int+  , rear :: Stream m a+  , rlen :: !Int+  }++bqueue :: MonadInherit m => BQueue a m -> m (BQueue a m)+bqueue (BQueue f fl r rl) = do+  ifIndirect f (`hasAtLeast` fromIntegral rl)+  if fl >= rl +    then pure $ BQueue f fl r rl+    else do+      r' <- delay (SReverse r SNil)+      r' `creditWith` 1+      f' <- delay (SAppend f (SIndirect r'))+      pure $ BQueue (SIndirect f') (fl + rl) SNil 0++instance Queue BQueue where+  empty = pure $ BQueue SNil 0 SNil 0+  snoc (BQueue f fl r rl) x = do+    credit f+    bqueue (BQueue f fl (SCons x r) (rl + 1))+  uncons (BQueue f fl r rl) = do+    credit f >> credit f+    smatch f+      (\x f -> do+        q <- bqueue (BQueue f (fl - 1) r rl)+        pure $ Just (x, q))+      (pure Nothing)++isEmpty :: BQueue a m -> Bool+isEmpty (BQueue _ flen _ rlen) = flen == 0 && rlen == 0++lazyqueue :: MonadInherit m => BQueue a m -> m [a]+lazyqueue (BQueue f fl r rl) = do+  f' <- toList f+  r' <- toList r+  pure $ f' ++ reverse r'++instance BoundedQueue BQueue where+  qcost _ (Snoc _) = 2+  qcost _ Uncons = 4++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BQueue a m) where+  prettyCell (BQueue f fl r rl) = do+    f' <- prettyCell f+    fl' <- prettyCell fl+    r' <- prettyCell r+    rl' <- prettyCell rl+    pure $ mkMCell "Queue" [f', fl', r', rl']++instance Pretty a => MemoryStructure (BQueue (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Base.hs view
@@ -0,0 +1,44 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, UndecidableInstances #-}++module Test.Credit.Queue.Base where++import Control.Monad.Credit+import Prettyprinter+import Test.Credit+import Test.QuickCheck++data QueueOp a = Snoc a | Uncons+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (QueueOp a) where+  arbitrary = frequency+    [ (7, Snoc <$> arbitrary)+    , (3, pure Uncons)+    ]++class Queue q where+  empty :: MonadInherit m => m (q a m)+  snoc :: MonadInherit m => q a m -> a -> m (q a m)+  uncons :: MonadInherit m => q a m -> m (Maybe (a, q a m))++class Queue q => BoundedQueue q where+  qcost :: Size -> QueueOp a -> Credit++data Q q a m = E | Q Size (q (PrettyCell a) m)++instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (Q q a) where+  prettyStructure E = pure $ mkMCell "" []+  prettyStructure (Q _ q) = prettyStructure q++act :: (MonadInherit m, Queue q) => Size -> q (PrettyCell a) m -> QueueOp a -> m (Q q a m)+act sz q (Snoc x) = Q (sz + 1) <$> snoc q (PrettyCell x)+act sz q Uncons = do+  m <- uncons q+  case m of+    Nothing -> pure E+    Just (_, q') -> pure $ Q (max 0 (sz - 1)) q'++instance (Arbitrary a, BoundedQueue q, Show a) => DataStructure (Q q a) (QueueOp a) where+  create = E+  action E op = (qcost @q 0 op, empty >>= flip (act 0) op)+  action (Q sz q) op = (qcost @q sz op, act sz q op)
+ src/Test/Credit/Queue/Batched.hs view
@@ -0,0 +1,35 @@+module Test.Credit.Queue.Batched where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Queue.Base++data Batched a m = Batched [a] [a]++rev :: MonadCount m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc)++bqueue :: MonadCount m => Batched a m -> m (Batched a m)+bqueue (Batched [] rear) = rev rear [] >>= \f -> pure $ Batched f []+bqueue (Batched front rear) = pure $ Batched front rear++instance Queue Batched where+  empty = pure $ Batched [] []+  snoc (Batched front rear) x = bqueue (Batched front (x : rear))+  uncons (Batched [] rear) = pure Nothing+  uncons (Batched (x:front) rear) = Just . (x,) <$> bqueue (Batched front rear)++instance BoundedQueue Batched where+  qcost n (Snoc _) = 1+  qcost n Uncons = linear n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Batched a m) where+  prettyCell (Batched f r) = do+    f' <- prettyCell f+    r' <- prettyCell r+    pure $ mkMCell "Queue" [f', r']++instance Pretty a => MemoryStructure (Batched (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Bootstrapped.hs view
@@ -0,0 +1,93 @@+{-# LANGUAGE GADTs #-}++module Test.Credit.Queue.Bootstrapped where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Queue.Base++rev :: MonadCredit m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc) ++data BLazyCon m a where+  Rev :: [a] -> BLazyCon m [a]++instance MonadCredit m => HasStep (BLazyCon m) m where+  step (Rev xs) = rev xs []++type BThunk m = Thunk m (BLazyCon m)++data NEQueue a m = NEQueue+  { lenfm :: !Int+  , f :: [a]+  , m :: Bootstrapped (BThunk m [a]) m+  , ghost :: BThunk m [a]+  , lenr :: !Int+  , r :: [a]+  }++data Bootstrapped a m = Empty | BQueue (NEQueue a m)++checkQ :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)+checkQ q@(NEQueue lenfm f m _ lenr r)+  | lenr <= lenfm = checkF q+  | otherwise = do+    r' <- delay $ Rev r+    creditWith r' 2+    m' <- snoc' m r'+    checkF (NEQueue (lenfm + lenr) f m' r' 0 [])++checkF :: MonadCredit m => NEQueue a m -> m (Bootstrapped a m)+checkF (NEQueue lenfm [] Empty _ lenr r) = pure Empty+checkF (NEQueue lenfm [] (BQueue m) ghost lenr r) = do+  (f, m') <- uncons'' m+  f' <- force f+  pure $ BQueue (NEQueue lenfm f' m' ghost lenr r)+checkF q = pure $ BQueue q++snoc' :: MonadCredit m => Bootstrapped a m -> a -> m (Bootstrapped a m)  +snoc' Empty x = do+  ghost <- delay $ Rev undefined -- never forced+  pure $ BQueue (NEQueue 1 [x] Empty ghost 0 [])+snoc' (BQueue (NEQueue lenfm f m g lenr r)) x = do+  creditWith g 1+  checkQ (NEQueue lenfm f m g (lenr + 1) (x : r))++uncons'' :: MonadCredit m => NEQueue a m -> m (a, Bootstrapped a m)+uncons'' (NEQueue lenfm (x : f') m g lenr r) = tick >> do+  creditWith g 1+  q <- checkQ (NEQueue (lenfm - 1) f' m g lenr r)+  pure (x, q)++uncons' :: MonadCredit m => Bootstrapped a m -> m (Maybe (a, Bootstrapped a m))+uncons' Empty = pure Nothing+uncons' (BQueue ne) = Just <$> uncons'' ne++instance Queue Bootstrapped where+  empty = pure Empty+  snoc q x = snoc' q x+  uncons q = uncons' q++instance BoundedQueue Bootstrapped where+  qcost n (Snoc _) = 3 * (max 1 (logstar n))+  qcost n Uncons = 6 * (max 1 (logstar n))++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BLazyCon m a) where+  prettyCell (Rev xs) = do+    xs' <- prettyCell xs+    pure $ mkMCell "Rev" [xs']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Bootstrapped a m) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (BQueue (NEQueue lenfm f m _ lenr r)) = do+    lenfm' <- prettyCell lenfm+    f' <- prettyCell f+    m' <- prettyCell m+    lenr' <- prettyCell lenr+    r' <- prettyCell r+    pure $ mkMCell "Queue" [lenfm', f', m', lenr', r']++instance Pretty a => MemoryStructure (Bootstrapped (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Implicit.hs view
@@ -0,0 +1,167 @@+{-# LANGUAGE GADTs, LambdaCase #-}++module Test.Credit.Queue.Implicit where++import Prelude hiding (head, tail)+import Control.Monad (when, unless)+import Control.Monad.Credit+import Prettyprinter (Pretty)+import Test.Credit.Queue.Base++-- Main idea:+--  - snoc and tail both cost two credits+--  - the first credit is used to tick+--  - We maintain the invariant: In each queue Deep(f, m, r), m has 2 - (|f| - |r|) credits.+--  - The m thunk represents either a snoc or a tail, and thus requires two credits to force.+--  - snoc and tail spend their second credit on either the old m to be able to force it,+--    or on the new m to maintain the invariant.++data Digit a = Zero | One a | Two a a+  deriving (Eq, Ord)++data Implicit a m+  = Shallow (Digit a)+  | Deep (Digit a) (Thunk m (ILazyCon m) (Implicit (a, a) m)) (Digit a)++data ILazyCon m a where+  IPure :: a -> ILazyCon m a+  ISnoc :: Thunk m (ILazyCon m) (Implicit a m) -> a -> ILazyCon m (Implicit a m)+  ITail :: Implicit a m -> ILazyCon m (Implicit a m)++instance MonadCredit m => HasStep (ILazyCon m) m where+  step (IPure x) = pure x+  step (ISnoc t p) = do+    q <- force t+    snoc' q p+  step (ITail q) = tail q++isEmpty :: Implicit a m -> Bool+isEmpty (Shallow Zero) = True+isEmpty _ = False++head :: MonadCredit m => Implicit a m -> m a+head q = case q of+  Shallow (One x) -> pure x+  Deep (Two x _) _ _ -> pure x+  Deep (One x) _ _ -> pure x+  _ -> fail "head: empty queue"++size :: Digit a -> Credit+size = \case { Zero -> 0; One _ -> 1; Two _ _ -> 2 }++deep :: MonadCredit m => Digit a -> Thunk m (ILazyCon m) (Implicit (a, a) m) -> Digit a -> m (Implicit a m)+deep f m r = do+  m `hasAtLeast` (2 - size f + size r)+  pure $ Deep f m r++snoc' :: MonadCredit m => Implicit a m -> a -> m (Implicit a m)+snoc' q y = do+  tick+  case q of+    Shallow Zero -> pure $ Shallow (One y)+    Shallow (One x) -> do+      middle <- delay $ IPure $ Shallow Zero+      deep (Two x y) middle Zero+    Deep front middle Zero -> do+      middle `creditWith` 1+      deep front middle (One y)+    Deep front middle (One x) -> do+      middle `hasAtLeast` (2 - size front + 1)+      t <- delay $ ISnoc middle (x, y)+      if size front == 1+        then t      `creditWith` 1+        else middle `creditWith` 1+      deep front t Zero+    _ -> fail "snoc: malformed queue"++tail :: MonadCredit m => Implicit a m -> m (Implicit a m)+tail q = tick >> case q of+  Shallow (One _) -> pure $ Shallow Zero+  Deep (Two _ y) m rear -> do+    creditWith m 1+    deep (One y) m rear+  Deep (One _) m rear -> do+    unless (size rear == 1) $ creditWith m 1+    m' <- force m+    if isEmpty m'+      then pure $ Shallow rear+      else do+        (y, z) <- head m'+        t <- delay $ ITail m'+        when (size rear == 1) $ creditWith t 1+        deep (Two y z) t rear+  _ -> fail "tail: empty queue"++instance Show a => Show (Digit a) where+  show Zero = "Zero"+  show (One a) = "(One " ++ show a ++ ")"+  show (Two a b) = "(Two " ++ show a ++ " " ++ show b ++ ")"++showThunk :: (MonadLazy m, Show a)+          => Thunk m (ILazyCon m) (Implicit a m) -> m String+showThunk t = lazymatch t showImplicit $ \case+    IPure a -> showImplicit a+    ISnoc middle xy -> do+      m <- showThunk middle+      pure $ "(snoc " ++ m ++ " " ++ show xy ++ ")"+    ITail q -> do+      m <- showImplicit q+      pure $ "(tail " ++ m ++ ")"++showImplicit :: (MonadLazy m, Show a)+             => Implicit a m -> m String+showImplicit (Shallow d) = do+  pure $ "(Shallow " ++ show d ++ ")"+showImplicit (Deep f m r) = do+  m' <- showThunk m+  pure $ "(Deep " ++ show f ++ " " ++ m' ++ " "+                  ++ show r ++ ")"++instance Queue Implicit where+  empty = pure $ Shallow Zero+  snoc q y = snoc' q y+  uncons q =+    if isEmpty q+      then pure Nothing+      else do+        h <- head q+        t <- tail q+        pure $ Just (h, t)++instance BoundedQueue Implicit where+  qcost _ (Snoc _) = 2+  qcost _ Uncons = 2++instance MemoryCell m a => MemoryCell m (Digit a) where+  prettyCell Zero = pure $ mkMCell "Zero" []+  prettyCell (One a) = do+    a' <- prettyCell a+    pure $ mkMCell "One" [a']+  prettyCell (Two a b) = do+    a' <- prettyCell a+    b' <- prettyCell b+    pure $ mkMCell "Two" [a', b']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ILazyCon m a) where+  prettyCell (IPure x) = do+    x' <- prettyCell x+    pure $ mkMCell "IPure" [x']+  prettyCell (ISnoc t _) = do+    t' <- prettyCell t+    pure $ mkMCell "ISnoc" [t']+  prettyCell (ITail q) = do+    q' <- prettyCell q+    pure $ mkMCell "ITail" [q']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Implicit a m) where+  prettyCell (Shallow d) = do+    d' <- prettyCell d+    pure $ mkMCell "Shallow" [d']+  prettyCell (Deep f m r) = do+    f' <- prettyCell f+    m' <- prettyCell m+    r' <- prettyCell r+    pure $ mkMCell "Deep" [f', m', r']++instance Pretty a => MemoryStructure (Implicit (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Physicists.hs view
@@ -0,0 +1,90 @@+{-# LANGUAGE TypeFamilies #-}++module Test.Credit.Queue.Physicists where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Queue.Base++app :: MonadCredit m => [a] -> [a] -> m [a]+app [] ys = pure ys+app (x : xs) ys = tick >> app xs (x : ys)++rev :: MonadCredit m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc)++data PLazyCon m a where+  Empty :: PLazyCon m [a]+  AppRev :: [a] -> [a] -> PLazyCon m [a]+  Tail :: Thunk m (PLazyCon m) [a] -> PLazyCon m [a]++instance MonadCredit m => HasStep (PLazyCon m) m where+  step Empty = pure []+  step (AppRev xs ys) = app xs =<< rev ys []+  step (Tail xs) = tick >> drop 1 <$> force xs++type PThunk m = Thunk m (PLazyCon m)++data Physicists a m = Queue [a] Int (PThunk m [a]) (PThunk m [a]) Int [a]++checkw :: MonadCredit m => Physicists a m -> m (Physicists a m)+checkw (Queue working lenf front ghost lenr rear) = case working of+  [] -> do+    front' <- force front+    pure $ Queue front' lenf front ghost lenr rear+  _ -> pure $ Queue working lenf front ghost lenr rear++check :: MonadCredit m => Physicists a m -> m (Physicists a m)+check q@(Queue _ lenf front ghost lenr rear) =+  if lenr <= lenf+    then do+      creditWith ghost 1+      checkw q+    else do+      working <- force front+      front' <- delay $ AppRev working rear+      creditWith front' 1+      checkw $ Queue working (lenf + lenr) front' front' 0 []++instance Queue Physicists where+  empty = do+    front <- delay Empty+    pure $ Queue [] 0 front front 0 []+  snoc (Queue working lenf front ghost lenr rear) x = tick >> do+    creditWith ghost 1+    check (Queue working lenf front ghost (lenr + 1) (x : rear))+  uncons (Queue [] lenf front ghost lenr rear) = tick >> pure Nothing+  uncons (Queue (x : working) lenf front ghost lenr rear) = tick >> do+    front' <- delay $ Tail front+    creditWith front' 1+    creditWith ghost 1+    q' <- check $ Queue working (lenf - 1) front' ghost lenr rear+    pure $ Just (x, q')++instance BoundedQueue Physicists where+  qcost _ (Snoc _) = 3+  qcost _ Uncons = 4++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (PLazyCon m a) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (AppRev xs ys) = do+    xs' <- prettyCell xs+    ys' <- prettyCell ys+    pure $ mkMCell "AppRev" [xs', ys']+  prettyCell (Tail xs) = do+    xs' <- prettyCell xs+    pure $ mkMCell "Tail" [xs']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Physicists a m) where+  prettyCell (Queue working lenf front _ lenr rear) = do+    working' <- prettyCell working+    lenf' <- prettyCell lenf+    front' <- prettyCell front+    lenr' <- prettyCell lenr+    rear' <- prettyCell rear+    pure $ mkMCell "Queue" [working', lenf', front', lenr', rear']++instance Pretty a => MemoryStructure (Physicists (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Realtime.hs view
@@ -0,0 +1,48 @@+module Test.Credit.Queue.Realtime where++import Prelude hiding (lookup, reverse)++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit.Queue.Base+import Test.Credit.Queue.Streams++-- | Delay a computation, but do not consume any credits+indirect :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)+indirect t = delay t >>= pure . SIndirect++data RQueue a m = RQueue+  { front :: Stream m a+  , rear :: Stream m a+  , schedule :: Stream m a+  }++rqueue :: MonadInherit m => RQueue a m -> m (RQueue a m)+rqueue (RQueue f r s) = credit s >> credit s >> smatch s+  (\x s -> pure $ RQueue f r s)+  (do+    r' <- indirect (SReverse r SNil)+    f' <- indirect (SAppend f r')+    credit r' >> evalone r'+    pure $ RQueue f' SNil f')++instance Queue RQueue where+  empty = pure $ RQueue SNil SNil SNil+  snoc (RQueue f r s) x = rqueue (RQueue f (SCons x r) s)+  uncons (RQueue f r s) = credit f >> credit f >> smatch f+    (\x f -> rqueue (RQueue f r s) >>= \q -> pure $ Just (x, q))+    (pure Nothing)++instance BoundedQueue RQueue where+  qcost _ (Snoc _) = 4+  qcost _ Uncons = 7++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (RQueue a m) where+  prettyCell (RQueue f r s) = do+    f' <- prettyCell f+    r' <- prettyCell r+    s' <- prettyCell s+    pure $ mkMCell "Queue" [f', r', s']++instance Pretty a => MemoryStructure (RQueue (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Queue/Streams.hs view
@@ -0,0 +1,110 @@+{-# LANGUAGE GADTs, LambdaCase #-}++module Test.Credit.Queue.Streams (Stream(..), SThunk, SLazyCon(..), smatch, credit, evalone, toList, ifIndirect, test) where++import Control.Monad+import Control.Monad.Credit++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (SThunk m (Stream m a))++type SThunk m = Thunk m (SLazyCon m)++data SLazyCon m a where+  SAppend :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)+  SReverse :: Stream m a -> Stream m a -> SLazyCon m (Stream m a)++instance MonadInherit m => HasStep (SLazyCon m) m where+  step (SAppend xs ys) = sappend xs ys+  step (SReverse xs ys) = sreverse xs ys++-- | Smart destructor for streams, consuming one credit+smatch :: MonadInherit m => Stream m a -- ^ Scrutinee+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b -- ^ Nil case+       -> m b+smatch x cons nil = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++-- | delay a computation, consuming all credits+taildelay :: MonadInherit m => SLazyCon m (Stream m a) -> m (Stream m a)+taildelay t = do+  x <- delay t+  creditAllTo x+  pure (SIndirect x)++sreverse :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)+sreverse xs ys = smatch xs+  (\x xs -> taildelay (SReverse xs (SCons x ys)))+  (pure ys)++ifIndirect :: Monad m => Stream m a -> (SThunk m (Stream m a) -> m ()) -> m ()+ifIndirect (SIndirect i) f = f i+ifIndirect _ _ = pure ()++credit :: MonadInherit m => Stream m a -> m ()+credit s = ifIndirect s (`creditWith` 1)++evalone :: MonadInherit m => Stream m a -> m ()+evalone s = ifIndirect s (void . force)++sappend :: MonadInherit m => Stream m a -> Stream m a -> m (Stream m a)+sappend xs ys = credit ys >> evalone ys >> smatch xs+  (\x xs -> SCons x <$> taildelay (SAppend xs ys))+  (pure ys)++walk s = smatch s (\_ xs -> walk xs) (pure ())++foo :: MonadInherit m => Stream m a -> m ()+foo s = smatch s (\_ _ -> pure ()) (pure ())++test :: MonadInherit m => m ()+test = do+  s <- sappend (SCons 1 SNil) (SCons 2 SNil)+  credit s >> credit s+  foo s+  credit s+  walk s++toList :: MonadLazy m => Stream m a -> m [a]+toList SNil = pure []+toList (SCons x xs) = do+  xs' <- toList xs+  pure $ x : xs'+toList (SIndirect t) = do+  lazymatch t toList $ \case+      SAppend xs ys -> do+        xs' <- toList xs+        ys' <- toList ys+        pure $ xs' ++ ys'+      SReverse xs ys -> do+        xs' <- toList xs+        ys' <- toList ys+        pure $ reverse xs' ++ ys'++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SLazyCon m a) where+  prettyCell (SAppend xs ys) = do+    xs' <- prettyCell xs+    ys' <- prettyCell ys+    pure $ mkMCell "SAppend" [xs', ys']+  prettyCell (SReverse xs ys) = do+    xs' <- prettyCell xs+    ys' <- prettyCell ys+    pure $ mkMCell "SReverse" [xs', ys']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t
+ src/Test/Credit/RandomAccess/Base.hs view
@@ -0,0 +1,64 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}++module Test.Credit.RandomAccess.Base where++import Prelude hiding (lookup)+import Control.Monad.Credit+import Test.Credit+import Test.QuickCheck++data RandomAccessOp a = Cons a | Uncons | Lookup Int | Update Int a+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (RandomAccessOp a) where+  arbitrary = frequency+    [ (13, Cons <$> arbitrary)+    , (6, pure Uncons)+    , (1, Lookup <$> arbitrary)+    , (1, Update <$> arbitrary <*> arbitrary)+    ]++class RandomAccess q where+  empty :: MonadCredit m => m (q a m)+  cons :: MonadCredit m => a -> q a m  -> m (q a m)+  uncons :: MonadCredit m => q a m -> m (Maybe (a, q a m))+  lookup :: MonadCredit m => Int -> q a m -> m (Maybe a)+  update :: MonadCredit m => Int -> a -> q a m -> m (q a m)++class RandomAccess q => BoundedRandomAccess q where+  qcost :: Size -> RandomAccessOp a -> Credit++data RA q a m = E | RA Size (q (PrettyCell a) m)++instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (RA q a m) where+  prettyCell E = pure $ mkMCell "" []+  prettyCell (RA _ q) = prettyCell q++instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (RA q a) where+  prettyStructure E = pure $ mkMCell "" []+  prettyStructure (RA _ q) = prettyStructure q++idx :: Int -> Size -> Int+idx i sz = if sz <= 0 then 0 else abs (i `mod` fromIntegral sz)++norm :: Size -> RandomAccessOp a -> RandomAccessOp a+norm sz (Lookup i) = Lookup (idx i sz)+norm sz (Update i a) = Update (idx i sz) a+norm _ op = op++act :: (MonadCredit m, RandomAccess q) => Size -> q (PrettyCell a) m -> RandomAccessOp a -> m (RA q a m)+act sz q (Cons x) = RA (sz + 1) <$> cons (PrettyCell x) q+act sz q Uncons = do+  m <- uncons q+  case m of+    Nothing -> pure E+    Just (_, q') -> pure $ RA (max 0 (sz - 1)) q'+act sz q (Lookup i) = do+  _ <- lookup i q+  pure $ RA sz q+act sz q (Update i a) = RA sz <$> update i (PrettyCell a) q++instance (Arbitrary a, BoundedRandomAccess q, Show a) => DataStructure (RA q a) (RandomAccessOp a) where+  create = E+  action E op = (qcost @q 0 (norm 0 op), empty >>= flip (act 0) (norm 0 op))+  action (RA sz q) op = (qcost @q sz (norm sz op), act sz q (norm sz op))
+ src/Test/Credit/RandomAccess/Binary.hs view
@@ -0,0 +1,174 @@+{-# LANGUAGE TypeFamilies #-}++module Test.Credit.RandomAccess.Binary where++import Prelude hiding (lookup)+import Prettyprinter (Pretty)+import Control.Monad.Credit hiding (exec)+import Test.Credit+import Test.Credit.RandomAccess.Base++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (Thunk m (Lazy m) (Stream m a))++indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)+indirect = fmap SIndirect . delay . Lazy++credit :: MonadCredit m => Credit -> Stream m a -> m ()+credit cr (SIndirect i) = creditWith i cr+credit _ _ = pure ()++-- | Smart destructor for streams, consuming one credit+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee+       -> m b -- ^ Nil case+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b+smatch x nil cons = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++data Tree a = Leaf a | Node Int (Tree a) (Tree a)+  deriving (Eq, Ord, Show)++data Digit a = Zero | One (Tree a) | Two (Tree a) (Tree a)+  deriving (Eq, Ord, Show)++size :: Tree a -> Int+size (Leaf _) = 1+size (Node w _ _) = w++link :: Tree a -> Tree a -> Tree a+link t1 t2 = Node (size t1 + size t2) t1 t2++consTree :: MonadCredit m => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))+consTree t ts = smatch ts+  (pure $ SCons (One t) SNil)+  (\d ds -> case d of+    Zero -> pure $ SCons (One t) ds+    One t' -> credit 1 ds >> pure (SCons (Two t t') ds)+    Two t2 t3 -> do+      ds' <- indirect $ consTree (link t2 t3) ds+      credit 1 ds'+      pure $ SCons (One t) ds')++unconsTree :: MonadCredit m => Stream m (Digit a) -> m (Maybe (Tree a, Stream m (Digit a)))+unconsTree ts = smatch ts+  (pure Nothing)+  (\d ds -> case d of+    One t -> credit 1 ds >> smatch ds+      (pure $ Just (t, SNil))+      (\_ _ -> pure $ Just (t, SCons Zero ds))+    Two t t' -> pure $ Just (t, SCons (One t') ds)+    Zero -> do+      ds' <- unconsTree ds+      case ds' of+        Just (Node _ t1 t2, ds'') -> pure $ Just (t1, SCons (One t2) ds'')+        _ -> pure Nothing)++lookupTree :: MonadCredit m => Int -> Tree a -> m (Maybe a)+lookupTree 0 (Leaf x) = pure $ Just x+lookupTree i (Leaf _) = pure Nothing+lookupTree i (Node w t1 t2)+  | i < w `div` 2 = tick >> lookupTree i t1+  | otherwise = tick >> lookupTree (i - w `div` 2) t2++updateTree :: MonadCredit m => Int -> a -> Tree a -> m (Tree a)+updateTree 0 y (Leaf _) = pure $ Leaf y+updateTree i _ (Leaf x) = pure $ Leaf x+updateTree i y (Node w t1 t2)+  | i < w `div` 2 = tick >> do+      t1' <- updateTree i y t1+      pure $ Node w t1' t2+  | otherwise = tick >> do+      t2' <- updateTree (i - w `div` 2) y t2+      pure $ Node w t1 t2'++newtype BinaryRA a m = BinaryRA { unBinaryRA :: Stream m (Digit a) }++instance RandomAccess BinaryRA where+  empty = pure $ BinaryRA SNil+  cons x (BinaryRA ts) = BinaryRA <$> consTree (Leaf x) ts+  uncons (BinaryRA ts) = do+    m <- unconsTree ts+    case m of+      Just (Leaf x, ts') -> pure $ Just (x, BinaryRA ts')+      _ -> pure Nothing+  lookup i (BinaryRA ts) = smatch ts+    (pure Nothing)+    (\d ds -> case d of+      Zero -> lookup i (BinaryRA ds)+      One t ->+        if i < size t+          then lookupTree i t+          else credit 1 ds >> lookup (i - size t) (BinaryRA ds)+      Two t1 t2 ->+        if i < size t1+          then lookupTree i t1+          else let j = i - size t1 in+            if j < size t2+              then lookupTree j t2+              else lookup (j - size t2) (BinaryRA ds))+  update i y (BinaryRA ts) = smatch ts+    (pure $ BinaryRA SNil)+    (\d ds -> case d of+      Zero -> BinaryRA . (SCons Zero) . unBinaryRA <$> update i y (BinaryRA ds)+      One t ->+        if i < size t+          then BinaryRA . (flip SCons ds) . One <$> updateTree i y t+          else credit 1 ds >> BinaryRA . (SCons (One t)) . unBinaryRA <$> update (i - size t) y (BinaryRA ds)+      Two t1 t2 ->+        if i < size t1+          then BinaryRA . (flip SCons ds) . flip Two t2 <$> updateTree i y t1+          else let j = i - size t1 in+            if j < size t2+              then BinaryRA . (flip SCons ds) . Two t1 <$> updateTree j y t2+              else BinaryRA . (SCons (Two t1 t2)) . unBinaryRA <$> update (j - size t2) y (BinaryRA ds))++instance BoundedRandomAccess BinaryRA where+  qcost n (Cons _) = 2+  qcost n Uncons = 3 + log2 n+  qcost n (Lookup _) = 1 + 3 * log2 n+  qcost n (Update _ _) = 1 + 3 * log2 n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t++instance MemoryCell m a => MemoryCell m (Tree a) where+  prettyCell (Leaf x) = do+    x' <- prettyCell x+    pure $ mkMCell "Leaf" [x']+  prettyCell (Node w t1 t2) = do+    t1' <- prettyCell t1+    t2' <- prettyCell t2+    pure $ mkMCell "Node" [t1', t2']++instance MemoryCell m a => MemoryCell m (Digit a) where+  prettyCell Zero = pure $ mkMCell "Zero" []+  prettyCell (One t) = do+    t' <- prettyCell t+    pure $ mkMCell "One" [t']+  prettyCell (Two t1 t2) = do+    t1' <- prettyCell t1+    t2' <- prettyCell t2+    pure $ mkMCell "Two" [t1', t2']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (BinaryRA a m) where+  prettyCell (BinaryRA ts) = do+    ts' <- prettyCell ts+    pure $ mkMCell "BinaryRA" [ts']++instance Pretty a => MemoryStructure (BinaryRA (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/RandomAccess/Zeroless.hs view
@@ -0,0 +1,200 @@+{-# LANGUAGE TypeFamilies #-}++module Test.Credit.RandomAccess.Zeroless where++import Prelude hiding (lookup)+import Prettyprinter (Pretty)+import Control.Monad.Credit hiding (exec)+import Test.Credit+import Test.Credit.RandomAccess.Base++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (Thunk m (Lazy m) (Stream m a))++indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)+indirect = fmap SIndirect . delay . Lazy++credit :: MonadCredit m => Credit -> Stream m a -> m ()+credit cr (SIndirect i) = creditWith i cr+credit _ _ = pure ()++-- | Smart destructor for streams, consuming one credit+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee+       -> m b -- ^ Nil case+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b+smatch x nil cons = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++data Tree a = Leaf a | Node Int (Tree a) (Tree a)+  deriving (Eq, Ord, Show)++data Digit a = One (Tree a) | Two (Tree a) (Tree a) | Three (Tree a) (Tree a) (Tree a)+  deriving (Eq, Ord, Show)++size :: Tree a -> Int+size (Leaf _) = 1+size (Node w _ _) = w++link :: Tree a -> Tree a -> Tree a+link t1 t2 = Node (size t1 + size t2) t1 t2++consTree :: MonadCredit m => Tree a -> Stream m (Digit a) -> m (Stream m (Digit a))+consTree t1 ts = smatch ts+  (pure $ SCons (One t1) SNil)+  (\d ds -> case d of+    One t2 -> pure $ SCons (Two t1 t2) ds+    Two t2 t3 -> credit 2 ds >> pure (SCons (Three t1 t2 t3) ds)+    Three t2 t3 t4 -> do+      ds' <- indirect $ consTree (link t3 t4) ds+      credit 2 ds'+      pure $ SCons (Two t1 t2) ds')++unconsTree :: MonadCredit m => Stream m (Digit a) -> m (Maybe (Tree a, Stream m (Digit a)))+unconsTree ts = smatch ts+  (pure Nothing)+  (\d ds -> case d of+      One t -> smatch ds+        (pure $ Just (t, SNil))+        (\_ _ -> do+          ds' <- indirect $ do+            ds' <- unconsTree ds+            case ds' of+              Just (Node _ t1 t2, ds'') -> do+                pure $ SCons (Two t1 t2) ds''+              Nothing -> fail "unconsTree: malformed tree"+          credit 2 ds'+          pure $ Just (t, ds'))+      Two t1 t2 -> credit 2 ds >> pure (Just (t1, SCons (One t2) ds))+      Three t1 t2 t3 -> pure $ Just (t1, SCons (Two t2 t3) ds))++lookupTree :: MonadCredit m => Int -> Tree a -> m (Maybe a)+lookupTree 0 (Leaf x) = pure $ Just x+lookupTree i (Leaf _) = pure Nothing+lookupTree i (Node w t1 t2)+  | i < w `div` 2 = tick >> lookupTree i t1+  | otherwise = tick >> lookupTree (i - w `div` 2) t2++updateTree :: MonadCredit m => Int -> a -> Tree a -> m (Tree a)+updateTree 0 y (Leaf _) = pure $ Leaf y+updateTree i _ (Leaf x) = pure $ Leaf x+updateTree i y (Node w t1 t2)+  | i < w `div` 2 = tick >> do+      t1' <- updateTree i y t1+      pure $ Node w t1' t2+  | otherwise = tick >> do+      t2' <- updateTree (i - w `div` 2) y t2+      pure $ Node w t1 t2'++newtype ZerolessRA a m = ZerolessRA { unZerolessRA :: Stream m (Digit a) }++instance RandomAccess ZerolessRA where+  empty = pure $ ZerolessRA SNil+  cons x (ZerolessRA ts) = credit 2 ts >> ZerolessRA <$> consTree (Leaf x) ts+  uncons (ZerolessRA ts) = credit 2 ts >> do+    m <- unconsTree ts+    case m of+      Just (Leaf x, ts') -> pure $ Just (x, ZerolessRA ts')+      _ -> pure Nothing+  lookup i (ZerolessRA ts) = credit 2 ts >> smatch ts+    (pure Nothing)+    (\d ds -> case d of+      One t -> do+        if i < size t+          then lookupTree i t+          else lookup (i - size t) (ZerolessRA ds)+      Two t1 t2 -> do+        if i < size t1+          then lookupTree i t1+          else let j = i - size t1 in+            if j < size t2+              then lookupTree j t2+              else credit 2 ds >> lookup (j - size t2) (ZerolessRA ds)+      Three t1 t2 t3 -> do+        if i < size t1+          then lookupTree i t1+          else let j = i - size t1 in+            if j < size t2+              then lookupTree j t2+              else let k = j - size t2 in+                if k < size t3+                  then lookupTree k t3+                  else lookup (k - size t3) (ZerolessRA ds))+  update i y (ZerolessRA ts) = credit 2 ts >> smatch ts+    (pure $ ZerolessRA SNil)+    (\d ds -> case d of+        One t -> do+            if i < size t+              then ZerolessRA . (flip SCons ds) . One <$> updateTree i y t+              else ZerolessRA . (SCons (One t)) . unZerolessRA <$> update (i - size t) y (ZerolessRA ds)+        Two t1 t2 -> do+            if i < size t1+              then ZerolessRA . (flip SCons ds) . flip Two t2 <$> updateTree i y t1+              else let j = i - size t1 in+                if j < size t2+                  then ZerolessRA . (flip SCons ds) . Two t1 <$> updateTree j y t2+                  else credit 2 ds >> ZerolessRA . (SCons (Two t1 t2)) . unZerolessRA <$> update (j - size t2) y (ZerolessRA ds)+        Three t1 t2 t3 -> do+            if i < size t1+              then ZerolessRA . (flip SCons ds) . (\t1' -> Three t1' t2 t3) <$> updateTree i y t1+              else let j = i - size t1 in+                if j < size t2+                  then ZerolessRA . (flip SCons ds) . (\t2' -> Three t1 t2' t3) <$> updateTree j y t2+                  else let k = j - size t2 in+                    if k < size t3+                      then ZerolessRA . (flip SCons ds) . Three t1 t2 <$> updateTree k y t3+                      else ZerolessRA . (SCons (Three t1 t2 t3)) . unZerolessRA <$> update (k - size t3) y (ZerolessRA ds))++instance BoundedRandomAccess ZerolessRA where+  qcost n (Cons _) = 5+  qcost n Uncons = 6+  qcost _ (Lookup i) = 3 + 5 * log2 (fromIntegral i * 2)+  qcost _ (Update i _) = 3 + 5 * log2 (fromIntegral i * 2)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t++instance MemoryCell m a => MemoryCell m (Tree a) where+  prettyCell (Leaf x) = do+    x' <- prettyCell x+    pure $ mkMCell "Leaf" [x']+  prettyCell (Node w t1 t2) = do+    t1' <- prettyCell t1+    t2' <- prettyCell t2+    pure $ mkMCell "Node" [t1', t2']++instance MemoryCell m a => MemoryCell m (Digit a) where+  prettyCell (One t) = do+    t' <- prettyCell t+    pure $ mkMCell "One" [t']+  prettyCell (Two t1 t2) = do+    t1' <- prettyCell t1+    t2' <- prettyCell t2+    pure $ mkMCell "Two" [t1', t2']+  prettyCell (Three t1 t2 t3) = do+    t1' <- prettyCell t1+    t2' <- prettyCell t2+    t3' <- prettyCell t3+    pure $ mkMCell "Three" [t1', t2', t3']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (ZerolessRA a m) where+  prettyCell (ZerolessRA ts) = do+    ts' <- prettyCell ts+    pure $ mkMCell "ZerolessRA" [ts']++instance Pretty a => MemoryStructure (ZerolessRA (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Sortable/Base.hs view
@@ -0,0 +1,45 @@+{-# LANGUAGE AllowAmbiguousTypes, TypeApplications #-}++module Test.Credit.Sortable.Base where++import Control.Monad.Credit+import Test.Credit+import Test.QuickCheck++data SortableOp a = Add a | Sort+  deriving (Eq, Ord, Show)++instance Arbitrary a => Arbitrary (SortableOp a) where+  arbitrary = frequency+    [ (9, Add <$> arbitrary)+    , (1, pure Sort)+    ]++class Sortable q where+  empty :: MonadCredit m => m (q a m)+  add :: MonadCredit m => Ord a => a -> q a m -> m (q a m)+  sort :: MonadCredit m => Ord a => q a m -> m [a] ++class Sortable q => BoundedSortable q where+  scost :: Size -> SortableOp a -> Credit++data S q a m = E | S Size (q (PrettyCell a) m)++instance (MemoryCell m (q (PrettyCell a) m)) => MemoryCell m (S q a m) where+  prettyCell E = pure $ mkMCell "" []+  prettyCell (S _ q) = prettyCell q++instance (MemoryStructure (q (PrettyCell a))) => MemoryStructure (S q a) where+  prettyStructure E = pure $ mkMCell "" []+  prettyStructure (S sz q) = prettyStructure q++act :: (MonadCredit m, Sortable q, Ord a) => Size -> q (PrettyCell a) m -> SortableOp a -> m (S q a m)+act sz q (Add x) = S (sz + 1) <$> add (PrettyCell x) q+act sz q Sort = do+  xs <- sort q+  pure $ S sz q++instance (Arbitrary a, Ord a, BoundedSortable q, Show a) => DataStructure (S q a) (SortableOp a) where+  create = E+  action E op = (scost @q 0 op, empty >>= flip (act 0) op)+  action (S sz q) op = (scost @q sz op, act sz q op)
+ src/Test/Credit/Sortable/MergeSort.hs view
@@ -0,0 +1,82 @@+{-# LANGUAGE GADTs #-}++module Test.Credit.Sortable.MergeSort where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Sortable.Base++data MergeSort a m = MergeSort Size (Thunk m (MLazyCon m) [[a]])++mrg :: MonadCredit m => Ord a => [a] -> [a] -> m [a]+mrg [] ys = pure ys+mrg xs [] = pure xs+mrg (x:xs) (y:ys) = tick >>+  if x <= y+    then (x:) <$> mrg xs (y:ys)+    else (y:) <$> mrg (x:xs) ys++addSeg :: MonadCredit m => Ord a => [a] -> [[a]] -> Size -> m [[a]]+addSeg seg segs size =+  if size `mod` 2 == 0 then pure $ seg : segs+  else do -- technically we should have a tick here, but Okasaki doesn't and we follow his presentation+    let (seg1:segs') = segs+    seg' <- mrg seg seg1 +    addSeg seg' segs' (size `div` 2)++psi :: Size -> Credit+psi n = 2 * linear n - 2 * sum [ linear $ b i * (n `mod` 2^i + 1) | i <- [0..(log2 n + 1)] ]+  where+    b i = (n `div` 2^i) `mod` 2++data MLazyCon m a where+  Empty :: MLazyCon m [[a]]+  AddSeg :: Ord a => [a] -> Thunk m (MLazyCon m) [[a]] -> Size -> MLazyCon m [[a]]++instance MonadCredit m => HasStep (MLazyCon m) m where+  step Empty = pure []+  step (AddSeg seg segs size) = do+    creditWith segs (psi size)+    segs' <- force segs+    addSeg seg segs' size++mrgAll :: MonadCredit m => Ord a => [a] -> [[a]] -> m [a]+mrgAll xs [] = pure xs+mrgAll xs (seg:segs) = tick >> do+  seg' <- mrg xs seg+  mrgAll seg' segs++instance Sortable MergeSort where+  empty = do+    segs <- delay Empty+    pure $ MergeSort 0 segs+  add x (MergeSort size segs) = do+    segs' <- delay $ AddSeg [x] segs size+    creditWith segs' (2 * log2 size + 1)+    pure $ MergeSort (size + 1) segs'+  sort (MergeSort size segs) = do+    creditWith segs (psi size)+    segs' <- force segs+    mrgAll [] segs'++instance BoundedSortable MergeSort where+  scost n (Add _) = 2 * log2 n + 1+  scost n Sort = psi n +  2 * linear n++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (MLazyCon m a) where+  prettyCell Empty = pure $ mkMCell "Empty" []+  prettyCell (AddSeg seg segs size) = do+    -- seg' <- prettyCell seg+    segs' <- prettyCell segs+    size' <- prettyCell size+    pure $ mkMCell "AddSeg" [segs', size']++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (MergeSort a m) where+  prettyCell (MergeSort size segs) = do+    size' <- prettyCell size+    segs' <- prettyCell segs+    pure $ mkMCell "MergeSort" [size', segs']++instance Pretty a => MemoryStructure (MergeSort (PrettyCell a)) where+  prettyStructure = prettyCell
+ src/Test/Credit/Sortable/Scheduled.hs view
@@ -0,0 +1,119 @@+{-# LANGUAGE GADTs #-}++module Test.Credit.Sortable.Scheduled where++import Prettyprinter (Pretty)+import Control.Monad.Credit+import Test.Credit+import Test.Credit.Sortable.Base++rev :: MonadCredit m => [a] -> [a] -> m [a]+rev [] acc = pure acc+rev (x : xs) acc = tick >> rev xs (x : acc)++data Stream m a+  = SCons a (Stream m a)+  | SNil+  | SIndirect (Thunk m (Lazy m) (Stream m a))++indirect :: MonadCredit m => m (Stream m a) -> m (Stream m a)+indirect = fmap SIndirect . delay . Lazy++credit :: MonadCredit m => Credit -> Stream m a -> m ()+credit cr (SIndirect i) = creditWith i cr+credit _ _ = pure ()++-- | Smart destructor for streams, consuming one credit+smatch :: MonadCredit m => Stream m a -- ^ Scrutinee+       -> m b -- ^ Nil case+       -> (a -> Stream m a -> m b) -- ^ Cons case+       -> m b+smatch x nil cons = tick >> eval x+  where+    eval x = case x of+      SCons a as -> cons a as+      SNil -> nil+      SIndirect i -> force i >>= eval++streamToList :: MonadCredit m => Stream m a -> m [a]+streamToList xs = smatch xs+  (pure [])+  (\x xs' -> (x:) <$> streamToList xs')++type Schedule m a = [Stream m a]++data SMergeSort a m = SMergeSort Size [(Stream m a, Schedule m a)]++mrg :: MonadCredit m => Ord a => Stream m a -> Stream m a -> m (Stream m a)+mrg xs ys = indirect $ do+  smatch xs (pure ys) $ \x xs' ->+    smatch ys (pure xs) $ \y ys' -> do+      if x <= y+        then (SCons x) <$> mrg xs' ys+        else (SCons y) <$> mrg xs ys'++exec1 :: MonadCredit m => Schedule m a -> m (Schedule m a)+exec1 [] = pure []+exec1 (ds:sched) = credit 2 ds >> smatch ds+  (exec1 sched)+  (\_ xs -> pure $ xs : sched)++exec2 :: MonadCredit m => (Stream m a, Schedule m a) -> m (Stream m a, Schedule m a)+exec2 (xs, sched) = exec1 sched >>= exec1 >>= pure . (xs,)++execAll :: MonadCredit m => Schedule m a -> m ()+execAll [] = pure ()+execAll sched = exec1 sched >>= execAll++addSeg :: MonadCredit m => Ord a => Stream m a -> [(Stream m a, Schedule m a)] -> Size -> Schedule m a -> m [(Stream m a, Schedule m a)]+addSeg xs segs size rsched =+  if size `mod` 2 == 0+    then do+      sched <- rev rsched [] -- log2 size+      pure $ (xs, sched) : segs+    else do+      let ((xs', []) : segs') = segs+      xs'' <- mrg xs xs'+      addSeg xs'' segs' (size `div` 2) (xs'' : rsched)++mrgAll :: MonadCredit m => Ord a => Stream m a -> [(Stream m a, Schedule m a)] -> m (Stream m a)+mrgAll xs [] = pure xs+mrgAll xs ((xs', sched):segs) = do+  execAll sched -- total cost: 3 * linear size+  seg <- mrg xs xs'+  execAll [seg] -- total cost: 6 * linear size+  mrgAll seg segs++instance Sortable SMergeSort where+  empty = pure $ SMergeSort 0 []+  add x (SMergeSort size segs) = do+    segs' <- addSeg (SCons x SNil) segs size [] -- 1 * (log2 size + 1)+    segs'' <- mapM exec2 segs' -- 6 * (log2 size + 1)+    pure $ SMergeSort (size + 1) segs''+  sort (SMergeSort size segs) = do+    s <- mrgAll SNil segs -- 9 * (log2 size + 1)+    streamToList s -- linear size++instance BoundedSortable SMergeSort where+  scost n (Add _) = 7 * (log2 n + 1)+  scost n Sort = 10 * (linear n + 1)++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (Stream m a) where+  prettyCell xs = mkMList <$> toList xs <*> toHole xs+    where+      toList SNil = pure $ []+      toList (SCons x xs) = (:) <$> prettyCell x <*> toList xs+      toList (SIndirect t) = pure $ []++      toHole SNil = pure $ Nothing+      toHole (SCons x xs) = toHole xs+      toHole (SIndirect t) = Just <$> prettyCell t++instance (MonadMemory m, MemoryCell m a) => MemoryCell m (SMergeSort a m) where+  prettyCell (SMergeSort size segs) = do+    size' <- prettyCell size+    segs' <- prettyCell segs+    pure $ mkMCell "SMergeSort" [size', segs']++instance Pretty a => MemoryStructure (SMergeSort (PrettyCell a)) where+  prettyStructure = prettyCell