{-# 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 (Error -> Error -> Bool
(Error -> Error -> Bool) -> (Error -> Error -> Bool) -> Eq Error
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Error -> Error -> Bool
== :: Error -> Error -> Bool
$c/= :: Error -> Error -> Bool
/= :: Error -> Error -> Bool
Eq, Eq Error
Eq Error =>
(Error -> Error -> Ordering)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Bool)
-> (Error -> Error -> Error)
-> (Error -> Error -> Error)
-> Ord Error
Error -> Error -> Bool
Error -> Error -> Ordering
Error -> Error -> Error
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Error -> Error -> Ordering
compare :: Error -> Error -> Ordering
$c< :: Error -> Error -> Bool
< :: Error -> Error -> Bool
$c<= :: Error -> Error -> Bool
<= :: Error -> Error -> Bool
$c> :: Error -> Error -> Bool
> :: Error -> Error -> Bool
$c>= :: Error -> Error -> Bool
>= :: Error -> Error -> Bool
$cmax :: Error -> Error -> Error
max :: Error -> Error -> Error
$cmin :: Error -> Error -> Error
min :: Error -> Error -> Error
Ord, Int -> Error -> ShowS
[Error] -> ShowS
Error -> String
(Int -> Error -> ShowS)
-> (Error -> String) -> ([Error] -> ShowS) -> Show Error
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Error -> ShowS
showsPrec :: Int -> Error -> ShowS
$cshow :: Error -> String
show :: Error -> String
$cshowList :: [Error] -> ShowS
showList :: [Error] -> ShowS
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 (Account -> Account -> Bool
(Account -> Account -> Bool)
-> (Account -> Account -> Bool) -> Eq Account
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Account -> Account -> Bool
== :: Account -> Account -> Bool
$c/= :: Account -> Account -> Bool
/= :: Account -> Account -> Bool
Eq, Eq Account
Eq Account =>
(Account -> Account -> Ordering)
-> (Account -> Account -> Bool)
-> (Account -> Account -> Bool)
-> (Account -> Account -> Bool)
-> (Account -> Account -> Bool)
-> (Account -> Account -> Account)
-> (Account -> Account -> Account)
-> Ord Account
Account -> Account -> Bool
Account -> Account -> Ordering
Account -> Account -> Account
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Account -> Account -> Ordering
compare :: Account -> Account -> Ordering
$c< :: Account -> Account -> Bool
< :: Account -> Account -> Bool
$c<= :: Account -> Account -> Bool
<= :: Account -> Account -> Bool
$c> :: Account -> Account -> Bool
> :: Account -> Account -> Bool
$c>= :: Account -> Account -> Bool
>= :: Account -> Account -> Bool
$cmax :: Account -> Account -> Account
max :: Account -> Account -> Account
$cmin :: Account -> Account -> Account
min :: Account -> Account -> Account
Ord, Int -> Account -> ShowS
[Account] -> ShowS
Account -> String
(Int -> Account -> ShowS)
-> (Account -> String) -> ([Account] -> ShowS) -> Show Account
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Account -> ShowS
showsPrec :: Int -> Account -> ShowS
$cshow :: Account -> String
show :: Account -> String
$cshowList :: [Account] -> ShowS
showList :: [Account] -> ShowS
Show)

newtype Credits = Credits (IntMap Account)
  deriving (Credits -> Credits -> Bool
(Credits -> Credits -> Bool)
-> (Credits -> Credits -> Bool) -> Eq Credits
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Credits -> Credits -> Bool
== :: Credits -> Credits -> Bool
$c/= :: Credits -> Credits -> Bool
/= :: Credits -> Credits -> Bool
Eq, Eq Credits
Eq Credits =>
(Credits -> Credits -> Ordering)
-> (Credits -> Credits -> Bool)
-> (Credits -> Credits -> Bool)
-> (Credits -> Credits -> Bool)
-> (Credits -> Credits -> Bool)
-> (Credits -> Credits -> Credits)
-> (Credits -> Credits -> Credits)
-> Ord Credits
Credits -> Credits -> Bool
Credits -> Credits -> Ordering
Credits -> Credits -> Credits
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Credits -> Credits -> Ordering
compare :: Credits -> Credits -> Ordering
$c< :: Credits -> Credits -> Bool
< :: Credits -> Credits -> Bool
$c<= :: Credits -> Credits -> Bool
<= :: Credits -> Credits -> Bool
$c> :: Credits -> Credits -> Bool
> :: Credits -> Credits -> Bool
$c>= :: Credits -> Credits -> Bool
>= :: Credits -> Credits -> Bool
$cmax :: Credits -> Credits -> Credits
max :: Credits -> Credits -> Credits
$cmin :: Credits -> Credits -> Credits
min :: Credits -> Credits -> Credits
Ord, Int -> Credits -> ShowS
[Credits] -> ShowS
Credits -> String
(Int -> Credits -> ShowS)
-> (Credits -> String) -> ([Credits] -> ShowS) -> Show Credits
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Credits -> ShowS
showsPrec :: Int -> Credits -> ShowS
$cshow :: Credits -> String
show :: Credits -> String
$cshowList :: [Credits] -> ShowS
showList :: [Credits] -> ShowS
Show)

open :: Cell -> Credits -> Credits
open :: Cell -> Credits -> Credits
open (Cell Int
i) (Credits IntMap Account
cm) = IntMap Account -> Credits
Credits (Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Int# -> Int# -> Account
Balance Int#
0# Int#
0#) IntMap Account
cm)

addCredit :: Cell -> Credit -> Credits -> Credits
addCredit :: Cell -> Credit -> Credits -> Credits
addCredit (Cell Int
i) (Credit (I# Int#
n)) (Credits IntMap Account
cm) = Int -> IntMap Account -> Credits
go Int
i IntMap Account
cm
  where
    go :: Int -> IntMap Account -> Credits
go Int
i IntMap Account
cm =
      case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Account
cm of
        Just (Balance Int#
avail Int#
burnt) -> IntMap Account -> Credits
Credits (Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Int# -> Int# -> Account
Balance (Int#
n Int# -> Int# -> Int#
+# Int#
avail) Int#
burnt) IntMap Account
cm)
        Just (ClosedWithHeir (Cell Int
h) Int#
burnt) ->
          case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
h IntMap Account
cm of
            Just (ClosedWithHeir (Cell Int
h') Int#
burnt') -> -- path halving
              Int -> IntMap Account -> Credits
go Int
h' (Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Cell -> Int# -> Account
ClosedWithHeir (Int -> Cell
Cell Int
h') (Int#
burnt Int# -> Int# -> Int#
+# Int#
burnt')) IntMap Account
cm)
            Maybe Account
_ -> Int -> IntMap Account -> Credits
go Int
h IntMap Account
cm
        Just Account
Closed -> IntMap Account -> Credits
Credits IntMap Account
cm
        Maybe Account
Nothing -> IntMap Account -> Credits
Credits IntMap Account
cm

subCredit :: MonadError Error m => Cell -> Credit -> Credits -> m Credits
subCredit :: forall (m :: * -> *).
MonadError Error m =>
Cell -> Credit -> Credits -> m Credits
subCredit (Cell Int
i) (Credit (I# Int#
n)) (Credits IntMap Account
cm) = Int -> IntMap Account -> m Credits
go Int
i IntMap Account
cm
  where
    go :: Int -> IntMap Account -> m Credits
go Int
i IntMap Account
cm = case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Account
cm of
      Just (Balance Int#
avail Int#
burnt) ->
        if Int# -> Bool
isTrue# (Int# -> Bool) -> Int# -> Bool
forall a b. (a -> b) -> a -> b
$ Int#
avail Int# -> Int# -> Int#
-# Int#
n Int# -> Int# -> Int#
<# Int#
0#
          then Error -> m Credits
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
OutOfCredits (Int -> Cell
Cell Int
i))
          else Credits -> m Credits
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Account -> Credits
Credits (Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Int# -> Int# -> Account
Balance (Int#
avail Int# -> Int# -> Int#
-# Int#
n) (Int#
burnt Int# -> Int# -> Int#
+# Int#
n)) IntMap Account
cm))
      Just (ClosedWithHeir (Cell Int
h) Int#
_) -> Int -> IntMap Account -> m Credits
go Int
h IntMap Account
cm
      Just Account
Closed -> Error -> m Credits
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidTick (Int -> Cell
Cell Int
i))
      Maybe Account
Nothing -> Error -> m Credits
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidTick (Int -> Cell
Cell Int
i))

-- | Close an account
close :: MonadError Error m => Cell -> Credits -> m Credits
close :: forall (m :: * -> *).
MonadError Error m =>
Cell -> Credits -> m Credits
close (Cell Int
i) (Credits IntMap Account
cm) = do
  case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Account
cm of
    Just (Balance Int#
_ Int#
_) -> Credits -> m Credits
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> m Credits) -> Credits -> m Credits
forall a b. (a -> b) -> a -> b
$ IntMap Account -> Credits
Credits (IntMap Account -> Credits) -> IntMap Account -> Credits
forall a b. (a -> b) -> a -> b
$ Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i Account
Closed IntMap Account
cm
    Just Account
Closed -> Credits -> m Credits
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> m Credits) -> Credits -> m Credits
forall a b. (a -> b) -> a -> b
$ IntMap Account -> Credits
Credits IntMap Account
cm
    Just (ClosedWithHeir Cell
_ Int#
_) -> Credits -> m Credits
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> m Credits) -> Credits -> m Credits
forall a b. (a -> b) -> a -> b
$ IntMap Account -> Credits
Credits IntMap Account
cm
    Maybe Account
Nothing -> Error -> m Credits
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidAccount (Int -> Cell
Cell Int
i))

-- | Close an account and transfer its credits to the heir.
closeWithHeir :: MonadError Error m => Cell -> Cell -> Credits -> m Credits
closeWithHeir :: forall (m :: * -> *).
MonadError Error m =>
Cell -> Cell -> Credits -> m Credits
closeWithHeir (Cell Int
i) Cell
h Credits
c = do
  (Credit
n, Int
burnt) <- Credits -> m (Credit, Int)
extractValue Credits
c
  Credits -> m Credits
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> m Credits) -> Credits -> m Credits
forall a b. (a -> b) -> a -> b
$ Int -> Credits -> Credits
closeAccount Int
burnt (Credits -> Credits) -> Credits -> Credits
forall a b. (a -> b) -> a -> b
$ Cell -> Credit -> Credits -> Credits
addCredit Cell
h Credit
n Credits
c
  where
    closeAccount :: Int -> Credits -> Credits
closeAccount (I# Int#
burnt) (Credits IntMap Account
cm) = IntMap Account -> Credits
Credits (IntMap Account -> Credits) -> IntMap Account -> Credits
forall a b. (a -> b) -> a -> b
$ Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i (Cell -> Int# -> Account
ClosedWithHeir Cell
h Int#
burnt) IntMap Account
cm

    extractValue :: Credits -> m (Credit, Int)
extractValue (Credits IntMap Account
cm) =
      case Account -> Int -> IntMap Account -> Account
forall a. a -> Int -> IntMap a -> a
IntMap.findWithDefault (Int# -> Int# -> Account
Balance Int#
0# Int#
0#) Int
i IntMap Account
cm of
        Balance Int#
a Int#
b -> (Credit, Int) -> m (Credit, Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Credit
Credit (Int# -> Int
I# Int#
a), Int# -> Int
I# Int#
b)
        ClosedWithHeir Cell
_ Int#
_ -> Error -> m (Credit, Int)
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidAccount (Int -> Cell
Cell Int
i))
        Account
Closed -> Error -> m (Credit, Int)
forall a. Error -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidAccount (Int -> Cell
Cell Int
i))

singleton :: Cell -> Credit -> Credits
singleton :: Cell -> Credit -> Credits
singleton (Cell Int
i) (Credit (I# Int#
n)) = IntMap Account -> Credits
Credits (Int -> Account -> IntMap Account
forall a. Int -> a -> IntMap a
IntMap.singleton Int
i (Int# -> Int# -> Account
Balance Int#
n Int#
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 (St -> St -> Bool
(St -> St -> Bool) -> (St -> St -> Bool) -> Eq St
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: St -> St -> Bool
== :: St -> St -> Bool
$c/= :: St -> St -> Bool
/= :: St -> St -> Bool
Eq, Eq St
Eq St =>
(St -> St -> Ordering)
-> (St -> St -> Bool)
-> (St -> St -> Bool)
-> (St -> St -> Bool)
-> (St -> St -> Bool)
-> (St -> St -> St)
-> (St -> St -> St)
-> Ord St
St -> St -> Bool
St -> St -> Ordering
St -> St -> St
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: St -> St -> Ordering
compare :: St -> St -> Ordering
$c< :: St -> St -> Bool
< :: St -> St -> Bool
$c<= :: St -> St -> Bool
<= :: St -> St -> Bool
$c> :: St -> St -> Bool
> :: St -> St -> Bool
$c>= :: St -> St -> Bool
>= :: St -> St -> Bool
$cmax :: St -> St -> St
max :: St -> St -> St
$cmin :: St -> St -> St
min :: St -> St -> St
Ord, Int -> St -> ShowS
[St] -> ShowS
St -> String
(Int -> St -> ShowS)
-> (St -> String) -> ([St] -> ShowS) -> Show St
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> St -> ShowS
showsPrec :: Int -> St -> ShowS
$cshow :: St -> String
show :: St -> String
$cshowList :: [St] -> ShowS
showList :: [St] -> ShowS
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 { forall s (m :: * -> *) a.
CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
runT :: ExceptT Error (StateT St (STT s m)) a }

instance Functor m => Functor (CreditT s m) where
  fmap :: forall a b. (a -> b) -> CreditT s m a -> CreditT s m b
fmap a -> b
f (CreditT ExceptT Error (StateT St (STT s m)) a
m) = ExceptT Error (StateT St (STT s m)) b -> CreditT s m b
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT ((a -> b)
-> ExceptT Error (StateT St (STT s m)) a
-> ExceptT Error (StateT St (STT s m)) b
forall a b.
(a -> b)
-> ExceptT Error (StateT St (STT s m)) a
-> ExceptT Error (StateT St (STT s m)) b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap a -> b
f ExceptT Error (StateT St (STT s m)) a
m)

instance Monad m => Applicative (CreditT s m) where
  pure :: forall a. a -> CreditT s m a
pure = ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) a -> CreditT s m a)
-> (a -> ExceptT Error (StateT St (STT s m)) a)
-> a
-> CreditT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> ExceptT Error (StateT St (STT s m)) a
forall a. a -> ExceptT Error (StateT St (STT s m)) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
  CreditT ExceptT Error (StateT St (STT s m)) (a -> b)
f <*> :: forall a b. CreditT s m (a -> b) -> CreditT s m a -> CreditT s m b
<*> CreditT ExceptT Error (StateT St (STT s m)) a
x = ExceptT Error (StateT St (STT s m)) b -> CreditT s m b
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) (a -> b)
f ExceptT Error (StateT St (STT s m)) (a -> b)
-> ExceptT Error (StateT St (STT s m)) a
-> ExceptT Error (StateT St (STT s m)) b
forall a b.
ExceptT Error (StateT St (STT s m)) (a -> b)
-> ExceptT Error (StateT St (STT s m)) a
-> ExceptT Error (StateT St (STT s m)) b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ExceptT Error (StateT St (STT s m)) a
x)

instance Monad m => Monad (CreditT s m) where
  CreditT ExceptT Error (StateT St (STT s m)) a
m >>= :: forall a b. CreditT s m a -> (a -> CreditT s m b) -> CreditT s m b
>>= a -> CreditT s m b
f = ExceptT Error (StateT St (STT s m)) b -> CreditT s m b
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) a
m ExceptT Error (StateT St (STT s m)) a
-> (a -> ExceptT Error (StateT St (STT s m)) b)
-> ExceptT Error (StateT St (STT s m)) b
forall a b.
ExceptT Error (StateT St (STT s m)) a
-> (a -> ExceptT Error (StateT St (STT s m)) b)
-> ExceptT Error (StateT St (STT s m)) b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= CreditT s m b -> ExceptT Error (StateT St (STT s m)) b
forall s (m :: * -> *) a.
CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
runT (CreditT s m b -> ExceptT Error (StateT St (STT s m)) b)
-> (a -> CreditT s m b)
-> a
-> ExceptT Error (StateT St (STT s m)) b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> CreditT s m b
f)

instance Monad m => MonadError Error (CreditT s m) where
  throwError :: forall a. Error -> CreditT s m a
throwError Error
e = ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (Error -> ExceptT Error (StateT St (STT s m)) a
forall a. Error -> ExceptT Error (StateT St (STT s m)) a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError Error
e)
  catchError :: forall a.
CreditT s m a -> (Error -> CreditT s m a) -> CreditT s m a
catchError (CreditT ExceptT Error (StateT St (STT s m)) a
m) Error -> CreditT s m a
h = ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) a
-> (Error -> ExceptT Error (StateT St (STT s m)) a)
-> ExceptT Error (StateT St (STT s m)) a
forall a.
ExceptT Error (StateT St (STT s m)) a
-> (Error -> ExceptT Error (StateT St (STT s m)) a)
-> ExceptT Error (StateT St (STT s m)) a
forall e (m :: * -> *) a.
MonadError e m =>
m a -> (e -> m a) -> m a
catchError ExceptT Error (StateT St (STT s m)) a
m (CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
forall s (m :: * -> *) a.
CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
runT (CreditT s m a -> ExceptT Error (StateT St (STT s m)) a)
-> (Error -> CreditT s m a)
-> Error
-> ExceptT Error (StateT St (STT s m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Error -> CreditT s m a
h))

instance Monad m => MonadState St (CreditT s m) where
  get :: CreditT s m St
get = ExceptT Error (StateT St (STT s m)) St -> CreditT s m St
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT ExceptT Error (StateT St (STT s m)) St
forall s (m :: * -> *). MonadState s m => m s
get
  put :: St -> CreditT s m ()
put St
s = ExceptT Error (StateT St (STT s m)) () -> CreditT s m ()
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (St -> ExceptT Error (StateT St (STT s m)) ()
forall s (m :: * -> *). MonadState s m => s -> m ()
put St
s)

instance MonadTrans (CreditT s) where
  lift :: forall (m :: * -> *) a. Monad m => m a -> CreditT s m a
lift = ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) a -> CreditT s m a)
-> (m a -> ExceptT Error (StateT St (STT s m)) a)
-> m a
-> CreditT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT St (STT s m) a -> ExceptT Error (StateT St (STT s m)) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT Error m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT St (STT s m) a -> ExceptT Error (StateT St (STT s m)) a)
-> (m a -> StateT St (STT s m) a)
-> m a
-> ExceptT Error (StateT St (STT s m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STT s m a -> StateT St (STT s m) a
forall (m :: * -> *) a. Monad m => m a -> StateT St m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (STT s m a -> StateT St (STT s m) a)
-> (m a -> STT s m a) -> m a -> StateT St (STT s m) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m a -> STT s m a
forall (m :: * -> *) a. Monad m => m a -> STT s m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

liftST :: Monad m => STT s m a -> CreditT s m a
liftST :: forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST = ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
forall s (m :: * -> *) a.
ExceptT Error (StateT St (STT s m)) a -> CreditT s m a
CreditT (ExceptT Error (StateT St (STT s m)) a -> CreditT s m a)
-> (STT s m a -> ExceptT Error (StateT St (STT s m)) a)
-> STT s m a
-> CreditT s m a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. StateT St (STT s m) a -> ExceptT Error (StateT St (STT s m)) a
forall (m :: * -> *) a. Monad m => m a -> ExceptT Error m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift (StateT St (STT s m) a -> ExceptT Error (StateT St (STT s m)) a)
-> (STT s m a -> StateT St (STT s m) a)
-> STT s m a
-> ExceptT Error (StateT St (STT s m)) a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. STT s m a -> StateT St (STT s m) a
forall (m :: * -> *) a. Monad m => m a -> StateT St m a
forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
(MonadTrans t, Monad m) =>
m a -> t m a
lift

getMe :: Monad m => CreditT s m Cell
getMe :: forall (m :: * -> *) s. Monad m => CreditT s m Cell
getMe = do
  St Cell
me Credits
_ Int
_ <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
  Cell -> CreditT s m Cell
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Cell
me

getNext :: Monad m => CreditT s m Cell
getNext :: forall (m :: * -> *) s. Monad m => CreditT s m Cell
getNext = do
  St Cell
_ Credits
_ Int
nxt <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
  (St -> St) -> CreditT s m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((St -> St) -> CreditT s m ()) -> (St -> St) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ \(St Cell
me Credits
c Int
_) -> Cell -> Credits -> Int -> St
St Cell
me Credits
c (Int
nxt Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  Cell -> CreditT s m Cell
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cell -> CreditT s m Cell) -> Cell -> CreditT s m Cell
forall a b. (a -> b) -> a -> b
$ Int -> Cell
Cell Int
nxt

withCredits :: Monad m => (Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits :: forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits Credits -> CreditT s m Credits
f = do
  St Cell
_ Credits
c Int
_ <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
  Credits
c' <- Credits -> CreditT s m Credits
f Credits
c
  (St -> St) -> CreditT s m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((St -> St) -> CreditT s m ()) -> (St -> St) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ \(St Cell
me Credits
_ Int
nxt) -> Cell -> Credits -> Int -> St
St Cell
me Credits
c' Int
nxt

instance Monad m => MonadFail (CreditT s m) where
  fail :: forall a. String -> CreditT s m a
fail String
e = Error -> CreditT s m a
forall a. Error -> CreditT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Error
UserError String
e)

instance Monad m => MonadCount (CreditT s m) where
  tick :: CreditT s m ()
tick = do
    Cell
me <- CreditT s m Cell
forall (m :: * -> *) s. Monad m => CreditT s m Cell
getMe
    (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ Cell -> Credit -> Credits -> CreditT s m Credits
forall (m :: * -> *).
MonadError Error m =>
Cell -> Credit -> Credits -> m Credits
subCredit Cell
me Credit
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 :: forall (t :: * -> *) a.
t a -> CreditT s m (Thunk (CreditT s m) t a)
delay t a
a = do
    Cell
i <- CreditT s m Cell
forall (m :: * -> *) s. Monad m => CreditT s m Cell
getNext
    (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ Credits -> CreditT s m Credits
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> CreditT s m Credits)
-> (Credits -> Credits) -> Credits -> CreditT s m Credits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell -> Credits -> Credits
open Cell
i
    STRef s (Either (t a) a)
s <- STT s m (STRef s (Either (t a) a))
-> CreditT s m (STRef s (Either (t a) a))
forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST (STT s m (STRef s (Either (t a) a))
 -> CreditT s m (STRef s (Either (t a) a)))
-> STT s m (STRef s (Either (t a) a))
-> CreditT s m (STRef s (Either (t a) a))
forall a b. (a -> b) -> a -> b
$ Either (t a) a -> STT s m (STRef s (Either (t a) a))
forall (m :: * -> *) a s. Applicative m => a -> STT s m (STRef s a)
newSTRef (t a -> Either (t a) a
forall a b. a -> Either a b
Left t a
a)
    Thunk (CreditT s m) t a -> CreditT s m (Thunk (CreditT s m) t a)
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Cell -> STRef s (Either (t a) a) -> Thunk (CreditT s m) t a
forall s (m :: * -> *) (t :: * -> *) b.
Cell -> STRef s (Either (t b) b) -> Thunk (CreditT s m) t b
Thunk Cell
i STRef s (Either (t a) a)
s)
  force :: forall (t :: * -> *) a.
HasStep t (CreditT s m) =>
Thunk (CreditT s m) t a -> CreditT s m a
force (Thunk Cell
i STRef s (Either (t a) a)
t) = do
    Either (t a) a
t' <- STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST (STT s m (Either (t a) a) -> CreditT s m (Either (t a) a))
-> STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall a b. (a -> b) -> a -> b
$ STRef s (Either (t a) a) -> STT s m (Either (t a) a)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s (Either (t a) a)
t
    case Either (t a) a
t' of
      Left t a
a -> do  -- [step] rule in the big-step semantics of the paper
        St Cell
me Credits
_ Int
_ <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
        (St -> St) -> CreditT s m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((St -> St) -> CreditT s m ()) -> (St -> St) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ \(St Cell
_ Credits
c Int
nxt) -> Cell -> Credits -> Int -> St
St Cell
i Credits
c Int
nxt
        a
b <- t a -> CreditT s m a
forall a. t a -> CreditT s m a
forall {k} (t :: k -> *) (m :: k -> *) (a :: k).
HasStep t m =>
t a -> m a
step t a
a
        (St -> St) -> CreditT s m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify' ((St -> St) -> CreditT s m ()) -> (St -> St) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ \(St Cell
_ Credits
c Int
nxt) -> Cell -> Credits -> Int -> St
St Cell
me Credits
c Int
nxt
        STT s m () -> CreditT s m ()
forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST (STT s m () -> CreditT s m ()) -> STT s m () -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ STRef s (Either (t a) a) -> Either (t a) a -> STT s m ()
forall (m :: * -> *) s a.
Applicative m =>
STRef s a -> a -> STT s m ()
writeSTRef STRef s (Either (t a) a)
t (a -> Either (t a) a
forall a b. b -> Either a b
Right a
b)
        (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ Cell -> Credits -> CreditT s m Credits
forall (m :: * -> *).
MonadError Error m =>
Cell -> Credits -> m Credits
close Cell
i
        a -> CreditT s m a
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
b
      Right a
b -> a -> CreditT s m a
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure a
b
  lazymatch :: forall (t :: * -> *) a b.
Thunk (CreditT s m) t a
-> (a -> CreditT s m b) -> (t a -> CreditT s m b) -> CreditT s m b
lazymatch (Thunk Cell
_ STRef s (Either (t a) a)
t) a -> CreditT s m b
f t a -> CreditT s m b
g = do
    Either (t a) a
t' <- STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST (STT s m (Either (t a) a) -> CreditT s m (Either (t a) a))
-> STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall a b. (a -> b) -> a -> b
$ STRef s (Either (t a) a) -> STT s m (Either (t a) a)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s (Either (t a) a)
t
    case Either (t a) a
t' of
      Right a
b -> a -> CreditT s m b
f a
b
      Left t a
a -> t a -> CreditT s m b
g t a
a

assertAtLeast :: Monad m => Cell -> Credit -> CreditT s m ()
assertAtLeast :: forall (m :: * -> *) s. Monad m => Cell -> Credit -> CreditT s m ()
assertAtLeast (Cell Int
i) Credit
n = do
  St Cell
_ (Credits IntMap Account
cm) Int
_ <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
  case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Account
cm of
    Just (Balance Int#
m' Int#
_) -> do
      let m :: Credit
m = Int -> Credit
Credit (Int# -> Int
I# Int#
m')
      if Credit
m Credit -> Credit -> Bool
forall a. Ord a => a -> a -> Bool
>= Credit
n
        then () -> CreditT s m ()
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        else Error -> CreditT s m ()
forall a. Error -> CreditT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Credit -> Credit -> Error
AssertionFailed (Int -> Cell
Cell Int
i) Credit
n Credit
m)
    Just Account
Closed -> () -> CreditT s m ()
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just (ClosedWithHeir Cell
i Int#
burnt) ->
      Cell -> Credit -> CreditT s m ()
forall (m :: * -> *) s. Monad m => Cell -> Credit -> CreditT s m ()
assertAtLeast Cell
i (Credit
n Credit -> Credit -> Credit
forall a. Num a => a -> a -> a
- Int -> Credit
Credit (Int# -> Int
I# Int#
burnt))
    Maybe Account
Nothing -> Error -> CreditT s m ()
forall a. Error -> CreditT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Cell -> Error
InvalidAccount (Int -> Cell
Cell Int
i))

instance Monad m => MonadCredit (CreditT s m) where
  {-# SPECIALIZE instance MonadCredit (CreditT s Identity) #-}
  {-# SPECIALIZE instance MonadCredit (CreditT s (State st)) #-}
  creditWith :: forall (t :: * -> *) a.
Thunk (CreditT s m) t a -> Credit -> CreditT s m ()
creditWith (Thunk Cell
i STRef s (Either (t a) a)
_) Credit
n =
    if Credit
n Credit -> Credit -> Bool
forall a. Ord a => a -> a -> Bool
> Credit
0 then do
      Cell
me <- CreditT s m Cell
forall (m :: * -> *) s. Monad m => CreditT s m Cell
getMe
      (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ Cell -> Credit -> Credits -> CreditT s m Credits
forall (m :: * -> *).
MonadError Error m =>
Cell -> Credit -> Credits -> m Credits
subCredit Cell
me Credit
n (Credits -> CreditT s m Credits)
-> (Credits -> Credits) -> Credits -> CreditT s m Credits
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Cell -> Credit -> Credits -> Credits
addCredit Cell
i Credit
n
    else () -> CreditT s m ()
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  hasAtLeast :: forall (t :: * -> *) a.
Thunk (CreditT s m) t a -> Credit -> CreditT s m ()
hasAtLeast (Thunk Cell
i STRef s (Either (t a) a)
_) Credit
n =
    Cell -> Credit -> CreditT s m ()
forall (m :: * -> *) s. Monad m => Cell -> Credit -> CreditT s m ()
assertAtLeast Cell
i Credit
n

instance Monad m => MonadInherit (CreditT s m) where
  {-# SPECIALIZE instance MonadInherit (CreditT s Identity) #-}
  {-# SPECIALIZE instance MonadInherit (CreditT s (State st)) #-}
  creditAllTo :: forall (t :: * -> *) a. Thunk (CreditT s m) t a -> CreditT s m ()
creditAllTo (Thunk Cell
i STRef s (Either (t a) a)
_) = do
    Cell
me <- CreditT s m Cell
forall (m :: * -> *) s. Monad m => CreditT s m Cell
getMe
    (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ Cell
me Cell -> Cell -> Credits -> CreditT s m Credits
forall (m :: * -> *).
MonadError Error m =>
Cell -> Cell -> Credits -> m Credits
`closeWithHeir` Cell
i

emptyState :: Credit -> St
emptyState :: Credit -> St
emptyState Credit
n = Cell -> Credits -> Int -> St
St (Int -> Cell
Cell Int
0) (Cell -> Credit -> Credits
singleton (Int -> Cell
Cell Int
0) Credit
n) Int
1

runCreditT :: Monad m => Credit -> (forall s. CreditT s m a) -> m (Either Error a)
runCreditT :: forall (m :: * -> *) a.
Monad m =>
Credit -> (forall s. CreditT s m a) -> m (Either Error a)
runCreditT Credit
n forall s. CreditT s m a
m = (forall s. STT s m (Either Error a)) -> m (Either Error a)
forall (m :: * -> *) a. Monad m => (forall s. STT s m a) -> m a
runSTT ((forall s. STT s m (Either Error a)) -> m (Either Error a))
-> (forall s. STT s m (Either Error a)) -> m (Either Error a)
forall a b. (a -> b) -> a -> b
$ StateT St (STT s m) (Either Error a)
-> St -> STT s m (Either Error a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ExceptT Error (StateT St (STT s m)) a
-> StateT St (STT s m) (Either Error a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
forall s (m :: * -> *) a.
CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
runT CreditT s m a
forall s. CreditT s m a
m)) (Credit -> St
emptyState Credit
n)

runCreditM :: Credit -> (forall s. CreditM s a) -> Either Error a
runCreditM :: forall a. Credit -> (forall s. CreditM s a) -> Either Error a
runCreditM Credit
n forall s. CreditM s a
m = Identity (Either Error a) -> Either Error a
forall a. Identity a -> a
runIdentity (Identity (Either Error a) -> Either Error a)
-> Identity (Either Error a) -> Either Error a
forall a b. (a -> b) -> a -> b
$ (forall s. STT s Identity (Either Error a))
-> Identity (Either Error a)
forall (m :: * -> *) a. Monad m => (forall s. STT s m a) -> m a
runSTT ((forall s. STT s Identity (Either Error a))
 -> Identity (Either Error a))
-> (forall s. STT s Identity (Either Error a))
-> Identity (Either Error a)
forall a b. (a -> b) -> a -> b
$ StateT St (STT s Identity) (Either Error a)
-> St -> STT s Identity (Either Error a)
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT (ExceptT Error (StateT St (STT s Identity)) a
-> StateT St (STT s Identity) (Either Error a)
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (CreditT s Identity a
-> ExceptT Error (StateT St (STT s Identity)) a
forall s (m :: * -> *) a.
CreditT s m a -> ExceptT Error (StateT St (STT s m)) a
runT CreditT s Identity a
forall s. CreditM s a
m)) (Credit -> St
emptyState Credit
n)

{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s Identity () #-}
{-# SPECIALIZE resetCurrentThunk :: Credit -> CreditT s (State st) () #-}
resetCurrentThunk :: Monad m => Credit -> CreditT s m ()
resetCurrentThunk :: forall (m :: * -> *) s. Monad m => Credit -> CreditT s m ()
resetCurrentThunk (Credit (I# Int#
n)) = do
  (Cell Int
me) <- CreditT s m Cell
forall (m :: * -> *) s. Monad m => CreditT s m Cell
getMe
  (Credits -> CreditT s m Credits) -> CreditT s m ()
forall (m :: * -> *) s.
Monad m =>
(Credits -> CreditT s m Credits) -> CreditT s m ()
withCredits ((Credits -> CreditT s m Credits) -> CreditT s m ())
-> (Credits -> CreditT s m Credits) -> CreditT s m ()
forall a b. (a -> b) -> a -> b
$ \(Credits IntMap Account
c) -> do
    case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
me IntMap Account
c of
      Just (Balance Int#
m Int#
b) -> Credits -> CreditT s m Credits
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credits -> CreditT s m Credits) -> Credits -> CreditT s m Credits
forall a b. (a -> b) -> a -> b
$ IntMap Account -> Credits
Credits (IntMap Account -> Credits) -> IntMap Account -> Credits
forall a b. (a -> b) -> a -> b
$ Int -> Account -> IntMap Account -> IntMap Account
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
me (Int# -> Int# -> Account
Balance (Int#
n Int# -> Int# -> Int#
+# Int#
m) Int#
b) IntMap Account
c
      Maybe Account
_ -> Error -> CreditT s m Credits
forall a. Error -> CreditT s m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (Error -> CreditT s m Credits) -> Error -> CreditT s m Credits
forall a b. (a -> b) -> a -> b
$ Cell -> Error
ClosedCurrent (Int -> Cell
Cell Int
me)

-- Pretty Printing

getCredit :: Monad m => Cell -> CreditT s m Credit
getCredit :: forall (m :: * -> *) s. Monad m => Cell -> CreditT s m Credit
getCredit (Cell Int
i) = do
  St Cell
_ (Credits IntMap Account
cm) Int
_ <- CreditT s m St
forall s (m :: * -> *). MonadState s m => m s
get
  case Int -> IntMap Account -> Maybe Account
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap Account
cm of
    Just (Balance Int#
n Int#
_) -> Credit -> CreditT s m Credit
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Credit -> CreditT s m Credit) -> Credit -> CreditT s m Credit
forall a b. (a -> b) -> a -> b
$ Int -> Credit
Credit (Int# -> Int
I# Int#
n)
    Maybe Account
_ -> Credit -> CreditT s m Credit
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Credit
0

instance (Monad m) => MonadMemory (CreditT s m) where
  {-# SPECIALIZE instance MonadMemory (CreditT s Identity) #-}
  {-# SPECIALIZE instance MonadMemory (CreditT s (State st)) #-}
  prettyThunk :: forall a (t :: * -> *).
(MemoryCell (CreditT s m) a, MemoryCell (CreditT s m) (t a)) =>
Thunk (CreditT s m) t a -> CreditT s m Memory
prettyThunk (Thunk Cell
c STRef s (Either (t a) a)
s) = do
    Either (t a) a
e <- STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall (m :: * -> *) s a. Monad m => STT s m a -> CreditT s m a
liftST (STT s m (Either (t a) a) -> CreditT s m (Either (t a) a))
-> STT s m (Either (t a) a) -> CreditT s m (Either (t a) a)
forall a b. (a -> b) -> a -> b
$ STRef s (Either (t a) a) -> STT s m (Either (t a) a)
forall (m :: * -> *) s a. Applicative m => STRef s a -> STT s m a
readSTRef STRef s (Either (t a) a)
s
    (Memory MTree
mtree Map Cell (MTree, Credit)
mstore) <- case Either (t a) a
e of
      Left t a
a -> t a -> CreditT s m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell t a
a
      Right a
b -> a -> CreditT s m Memory
forall (m :: * -> *) a. MemoryCell m a => a -> m Memory
prettyCell a
b
    Credit
cr <- Cell -> CreditT s m Credit
forall (m :: * -> *) s. Monad m => Cell -> CreditT s m Credit
getCredit Cell
c
    Memory -> CreditT s m Memory
forall a. a -> CreditT s m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Memory -> CreditT s m Memory) -> Memory -> CreditT s m Memory
forall a b. (a -> b) -> a -> b
$ MTree -> Map Cell (MTree, Credit) -> Memory
Memory (Cell -> MTree
Indirection Cell
c) (Cell
-> (MTree, Credit)
-> Map Cell (MTree, Credit)
-> Map Cell (MTree, Credit)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Cell
c (MTree
mtree, Credit
cr) Map Cell (MTree, Credit)
mstore)

instance Pretty Error where
  pretty :: forall ann. Error -> Doc ann
pretty (OutOfCredits Cell
i) = Doc ann
"Out of credits for" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
i
  pretty (InvalidAccount Cell
i) = Doc ann
"Invalid account for" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
i
  pretty (InvalidTick Cell
i) = Doc ann
"Invalid tick for" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
i
  pretty (ClosedCurrent (Cell Int
0)) = Doc ann
"Closed maint thread account. Never invoke creditAllTo on main thread."
  pretty (ClosedCurrent Cell
i) = Doc ann
"Closed current account" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
i
  pretty (UserError String
e) = Doc ann
"User error:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
e
  pretty (AssertionFailed Cell
i Credit
n Credit
m) = Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
i Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"should have" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Credit -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Credit -> Doc ann
pretty Credit
n Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"credits but only has" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Credit -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Credit -> Doc ann
pretty Credit
m

instance Pretty a => Pretty (Either Error a) where
  pretty :: forall ann. Either Error a -> Doc ann
pretty (Left Error
e) = Error -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Error -> Doc ann
pretty Error
e
  pretty (Right a
a) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a

instance Pretty Account where
  pretty :: forall ann. Account -> Doc ann
pretty (Balance Int#
n Int#
_) = Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (Int# -> Int
I# Int#
n)
  pretty Account
Closed = Doc ann
"closed"
  pretty (ClosedWithHeir Cell
h Int#
_) = Doc ann
"closed with heir" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
h

instance Pretty Credits where
  pretty :: forall ann. Credits -> Doc ann
pretty (Credits IntMap Account
cm) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
forall a b. (a -> b) -> a -> b
$ ((Int, Account) -> Doc ann) -> [(Int, Account)] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Account) -> Doc ann
forall {a} {a} {ann}. (Pretty a, Pretty a) => (a, a) -> Doc ann
prettyPair (IntMap Account -> [(Int, Account)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Account
cm)
    where
      prettyPair :: (a, a) -> Doc ann
prettyPair (a
i, a
a) = a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
i Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"->" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> a -> Doc ann
forall ann. a -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty a
a

instance Pretty St where
  pretty :: forall ann. St -> Doc ann
pretty (St Cell
me Credits
c Int
nxt) = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
vsep
    [ Doc ann
"me:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Cell -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Cell -> Doc ann
pretty Cell
me
    , Doc ann
"credits:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Credits -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Credits -> Doc ann
pretty Credits
c
    , Doc ann
"next:" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Int -> Doc ann
forall ann. Int -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty Int
nxt
    ]