{-# LANGUAGE ImplicitParams,
MultiWayIf,
PatternSynonyms,
RecordWildCards,
TypeApplications,
UnboxedTuples #-}
module Parsley.Internal.Backend.Machine.Eval (eval) where
import Data.Dependent.Map (DMap)
import Data.Functor ((<&>))
import Data.Void (Void)
import Control.Monad (forM, liftM2, liftM3, when)
import Control.Monad.Reader (ask, asks, reader, local)
import Control.Monad.ST (runST)
import Parsley.Internal.Backend.Machine.Defunc (Defunc(OFFSET), pattern FREEVAR, genDefunc, ap, ap2, _if)
import Parsley.Internal.Backend.Machine.Identifiers (MVar(..), ΦVar, ΣVar)
import Parsley.Internal.Backend.Machine.InputOps (InputDependant, InputOps(InputOps))
import Parsley.Internal.Backend.Machine.InputRep (Rep)
import Parsley.Internal.Backend.Machine.Instructions (Instr(..), MetaInstr(..), Access(..), Handler(..))
import Parsley.Internal.Backend.Machine.LetBindings (LetBinding(body))
import Parsley.Internal.Backend.Machine.LetRecBuilder (letRec)
import Parsley.Internal.Backend.Machine.Ops
import Parsley.Internal.Backend.Machine.Types (MachineMonad, Machine(..), run)
import Parsley.Internal.Backend.Machine.Types.Context
import Parsley.Internal.Backend.Machine.Types.Coins (willConsume, int)
import Parsley.Internal.Backend.Machine.Types.Offset (mkOffset, offset)
import Parsley.Internal.Backend.Machine.Types.State (Γ(..), OpStack(..))
import Parsley.Internal.Common (Fix4, cata4, One, Code, Vec(..), Nat(..))
import Parsley.Internal.Trace (Trace(trace))
import System.Console.Pretty (color, Color(Green))
import qualified Debug.Trace (trace)
eval :: forall o a. (Trace, Ops o)
=> Code (InputDependant (Rep o))
-> LetBinding o a a
-> DMap MVar (LetBinding o a)
-> Code (Maybe a)
eval :: Code (InputDependant (Rep o))
-> LetBinding o a a -> DMap MVar (LetBinding o a) -> Code (Maybe a)
eval Code (InputDependant (Rep o))
input LetBinding o a a
binding DMap MVar (LetBinding o a)
fs = String -> Code (Maybe a) -> Code (Maybe a)
forall a. Trace => String -> a -> a
trace String
"EVALUATING TOP LEVEL" [|| runST $
do let !(# next, more, offset #) = $$input
$$(let ?ops = InputOps [||more||] [||next||]
in letRec fs
nameLet
(\μ exp rs names -> buildRec μ rs (emptyCtx names) (readyMachine exp))
(run (readyMachine (body binding)) (Γ Empty halt (mkOffset [||offset||] 0) (VCons fatal VNil)) . nextUnique . emptyCtx))
||]
where
nameLet :: MVar x -> String
nameLet :: MVar x -> String
nameLet (MVar IMVar
i) = String
"sub" String -> String -> String
forall a. [a] -> [a] -> [a]
++ IMVar -> String
forall a. Show a => a -> String
show IMVar
i
readyMachine :: (?ops :: InputOps (Rep o), Ops o, Trace) => Fix4 (Instr o) xs n r a -> Machine s o xs n r a
readyMachine :: Fix4 (Instr o) xs n r a -> Machine s o xs n r a
readyMachine = (forall (i' :: [Type]) (j' :: Nat) k'.
Instr o (Machine s o) i' j' k' a -> Machine s o i' j' k' a)
-> Fix4 (Instr o) xs n r a -> Machine s o xs n r a
forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
-> [Type] -> Nat -> Type -> Type -> Type)
(a :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
(j :: Nat) k x.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
f a i' j' k' x -> a i' j' k' x)
-> Fix4 f i j k x -> a i j k x
cata4 (MachineMonad s o i' j' k' a -> Machine s o i' j' k' a
forall s o (xs :: [Type]) (n :: Nat) r a.
MachineMonad s o xs n r a -> Machine s o xs n r a
Machine (MachineMonad s o i' j' k' a -> Machine s o i' j' k' a)
-> (Instr o (Machine s o) i' j' k' a
-> MachineMonad s o i' j' k' a)
-> Instr o (Machine s o) i' j' k' a
-> Machine s o i' j' k' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o (Machine s o) i' j' k' a -> MachineMonad s o i' j' k' a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), Ops o) =>
Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a
alg)
where
alg :: (?ops :: InputOps (Rep o), Ops o) => Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a
alg :: Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a
alg Instr o (Machine s o) xs n r a
Ret = MachineMonad s o xs n r a
forall s o x (xs :: [Type]) (n :: Nat) a.
MachineMonad s o (x : xs) n x a
evalRet
alg (Call MVar x
μ Machine s o (x : xs) ('Succ n) r a
k) = MVar x
-> Machine s o (x : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall s o a x (xs :: [Type]) (n :: Nat) r.
MarshalOps o =>
MVar x
-> Machine s o (x : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalCall MVar x
μ Machine s o (x : xs) ('Succ n) r a
k
alg (Jump MVar r
μ) = MVar r -> MachineMonad s o '[] ('Succ n) r a
forall s o a x (n :: Nat).
MarshalOps o =>
MVar x -> MachineMonad s o '[] ('Succ n) x a
evalJump MVar r
μ
alg (Push Defunc x
x Machine s o (x : xs) n r a
k) = Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalPush Defunc x
x Machine s o (x : xs) n r a
k
alg (Pop Machine s o xs n r a
k) = Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
forall s o (xs :: [Type]) (n :: Nat) r a x.
Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalPop Machine s o xs n r a
k
alg (Lift2 Defunc (x -> y -> z)
f Machine s o (z : xs) n r a
k) = Defunc (x -> y -> z)
-> Machine s o (z : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
forall x y z s o (xs :: [Type]) (n :: Nat) r a.
Defunc (x -> y -> z)
-> Machine s o (z : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
evalLift2 Defunc (x -> y -> z)
f Machine s o (z : xs) n r a
k
alg (Sat Defunc (Char -> Bool)
p Machine s o (Char : xs) ('Succ n) r a
k) = Defunc (Char -> Bool)
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o), Trace) =>
Defunc (Char -> Bool)
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalSat Defunc (Char -> Bool)
p Machine s o (Char : xs) ('Succ n) r a
k
alg Instr o (Machine s o) xs n r a
Empt = MachineMonad s o xs n r a
forall s o (xs :: [Type]) (n :: Nat) r a.
MachineMonad s o xs ('Succ n) r a
evalEmpt
alg (Commit Machine s o xs n r a
k) = Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a
evalCommit Machine s o xs n r a
k
alg (Catch Machine s o xs ('Succ n) r a
k Handler o (Machine s o) (o : xs) n r a
h) = Machine s o xs ('Succ n) r a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(PositionOps (Rep o), HandlerOps o) =>
Machine s o xs ('Succ n) r a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
evalCatch Machine s o xs ('Succ n) r a
k Handler o (Machine s o) (o : xs) n r a
h
alg (Tell Machine s o (o : xs) n r a
k) = Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
evalTell Machine s o (o : xs) n r a
k
alg (Seek Machine s o xs n r a
k) = Machine s o xs n r a -> MachineMonad s o (o : xs) n r a
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a -> MachineMonad s o (o : xs) n r a
evalSeek Machine s o xs n r a
k
alg (Case Machine s o (x : xs) n r a
p Machine s o (y : xs) n r a
q) = Machine s o (x : xs) n r a
-> Machine s o (y : xs) n r a
-> MachineMonad s o (Either x y : xs) n r a
forall s o x (xs :: [Type]) (n :: Nat) r a y.
Machine s o (x : xs) n r a
-> Machine s o (y : xs) n r a
-> MachineMonad s o (Either x y : xs) n r a
evalCase Machine s o (x : xs) n r a
p Machine s o (y : xs) n r a
q
alg (Choices [Defunc (x -> Bool)]
fs [Machine s o xs n r a]
ks Machine s o xs n r a
def) = [Defunc (x -> Bool)]
-> [Machine s o xs n r a]
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
[Defunc (x -> Bool)]
-> [Machine s o xs n r a]
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalChoices [Defunc (x -> Bool)]
fs [Machine s o xs n r a]
ks Machine s o xs n r a
def
alg (Iter MVar Void
μ Machine s o '[] One Void a
l Handler o (Machine s o) (o : xs) n r a
k) = MVar Void
-> Machine s o '[] One Void a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
forall o s a (xs :: [Type]) (n :: Nat) r.
(RecBuilder o, PositionOps (Rep o), HandlerOps o) =>
MVar Void
-> Machine s o '[] One Void a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
evalIter MVar Void
μ Machine s o '[] One Void a
l Handler o (Machine s o) (o : xs) n r a
k
alg (Join ΦVar x
φ) = ΦVar x -> MachineMonad s o (x : xs) n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
ΦVar x -> MachineMonad s o (x : xs) n r a
evalJoin ΦVar x
φ
alg (MkJoin ΦVar x
φ Machine s o (x : xs) n r a
p Machine s o xs n r a
k) = ΦVar x
-> Machine s o (x : xs) n r a
-> Machine s o xs n r a
-> MachineMonad s o xs n r a
forall o x s (xs :: [Type]) (n :: Nat) r a.
JoinBuilder o =>
ΦVar x
-> Machine s o (x : xs) n r a
-> Machine s o xs n r a
-> MachineMonad s o xs n r a
evalMkJoin ΦVar x
φ Machine s o (x : xs) n r a
p Machine s o xs n r a
k
alg (Swap Machine s o (x : y : xs) n r a
k) = Machine s o (x : y : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
forall s o x y (xs :: [Type]) (n :: Nat) r a.
Machine s o (x : y : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
evalSwap Machine s o (x : y : xs) n r a
k
alg (Dup Machine s o (x : x : xs) n r a
k) = Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
forall s o x (xs :: [Type]) (n :: Nat) r a.
Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
evalDup Machine s o (x : x : xs) n r a
k
alg (Make ΣVar x
σ Access
c Machine s o xs n r a
k) = ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalMake ΣVar x
σ Access
c Machine s o xs n r a
k
alg (Get ΣVar x
σ Access
c Machine s o (x : xs) n r a
k) = ΣVar x
-> Access
-> Machine s o (x : xs) n r a
-> MachineMonad s o xs n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
ΣVar x
-> Access
-> Machine s o (x : xs) n r a
-> MachineMonad s o xs n r a
evalGet ΣVar x
σ Access
c Machine s o (x : xs) n r a
k
alg (Put ΣVar x
σ Access
c Machine s o xs n r a
k) = ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
forall x s o (xs :: [Type]) (n :: Nat) r a.
ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalPut ΣVar x
σ Access
c Machine s o xs n r a
k
alg (LogEnter String
name Machine s o xs ('Succ ('Succ n)) r a
k) = String
-> Machine s o xs ('Succ ('Succ n)) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), LogHandler o, HandlerOps o) =>
String
-> Machine s o xs ('Succ ('Succ n)) r a
-> MachineMonad s o xs ('Succ n) r a
evalLogEnter String
name Machine s o xs ('Succ ('Succ n)) r a
k
alg (LogExit String
name Machine s o xs n r a
k) = String -> Machine s o xs n r a -> MachineMonad s o xs n r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o), LogOps (Rep o)) =>
String -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalLogExit String
name Machine s o xs n r a
k
alg (MetaInstr MetaInstr n
m Machine s o xs n r a
k) = MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
forall o (n :: Nat) s (xs :: [Type]) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMeta MetaInstr n
m Machine s o xs n r a
k
evalRet :: MachineMonad s o (x : xs) n x a
evalRet :: MachineMonad s o (x : xs) n x a
evalRet = (Γ s o (x : xs) n x a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n x a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Γ s o (x : xs) n x a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n x a)
-> (Γ s o (x : xs) n x a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n x a
forall a b. (a -> b) -> a -> b
$! Γ s o (x : xs) n x a -> StaCont s o a x
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> StaCont s o a r
retCont (Γ s o (x : xs) n x a -> StaCont s o a x)
-> (StaCont s o a x
-> Γ s o (x : xs) n x a -> Code (ST s (Maybe a)))
-> Γ s o (x : xs) n x a
-> Code (ST s (Maybe a))
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= StaCont s o a x -> Γ s o (x : xs) n x a -> Code (ST s (Maybe a))
forall s o a x (xs :: [Type]) (n :: Nat) r.
StaCont s o a x -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
resume
evalCall :: forall s o a x xs n r. MarshalOps o => MVar x -> Machine s o (x : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
evalCall :: MVar x
-> Machine s o (x : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalCall MVar x
μ (Machine MachineMonad s o (x : xs) ('Succ n) r a
k) = (Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique ((Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a)
-> (Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$ \Word
u -> (StaSubroutine s o a x
-> (Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a)))
-> ReaderT (Ctx s o a) Identity (StaSubroutine s o a x)
-> MachineMonad s o (x : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (Word
-> StaSubroutine s o a x
-> (Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a x.
MarshalOps o =>
Word
-> StaSubroutine s o a x
-> (Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
callCC Word
u) (MVar x -> ReaderT (Ctx s o a) Identity (StaSubroutine s o a x)
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
MVar x -> m (StaSubroutine s o a x)
askSub MVar x
μ) MachineMonad s o (x : xs) ('Succ n) r a
k
evalJump :: forall s o a x n. MarshalOps o => MVar x -> MachineMonad s o '[] (Succ n) x a
evalJump :: MVar x -> MachineMonad s o '[] ('Succ n) x a
evalJump MVar x
μ = MVar x -> ReaderT (Ctx s o a) Identity (StaSubroutine s o a x)
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
MVar x -> m (StaSubroutine s o a x)
askSub MVar x
μ ReaderT (Ctx s o a) Identity (StaSubroutine s o a x)
-> (StaSubroutine s o a x
-> Γ s o '[] ('Succ n) x a -> Code (ST s (Maybe a)))
-> MachineMonad s o '[] ('Succ n) x a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \StaSubroutine s o a x
sub Γ{Vec ('Succ n) (AugmentedStaHandler s o a)
Offset o
StaCont s o a x
OpStack '[]
handlers :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Vec n (AugmentedStaHandler s o a)
input :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
operands :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
handlers :: Vec ('Succ n) (AugmentedStaHandler s o a)
input :: Offset o
retCont :: StaCont s o a x
operands :: OpStack '[]
retCont :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> StaCont s o a r
..} -> StaSubroutine s o a x
-> StaCont s o a x
-> Code (Rep o)
-> Vec ('Succ n) (AugmentedStaHandler s o a)
-> Code (ST s (Maybe a))
forall o s a x (n :: Nat).
MarshalOps o =>
StaSubroutine s o a x
-> StaCont s o a x
-> Code (Rep o)
-> Vec ('Succ n) (AugmentedStaHandler s o a)
-> Code (ST s (Maybe a))
callWithContinuation @o StaSubroutine s o a x
sub StaCont s o a x
retCont (Offset o -> Code (Rep o)
forall o. Offset o -> Code (Rep o)
offset Offset o
input) Vec ('Succ n) (AugmentedStaHandler s o a)
handlers
evalPush :: Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalPush :: Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalPush Defunc x
x (Machine MachineMonad s o (x : xs) n r a
k) = MachineMonad s o (x : xs) n r a
k MachineMonad s o (x : xs) n r a
-> ((Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
m Γ s o xs n r a
γ -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
m (Γ s o xs n r a
γ {operands :: OpStack (x : xs)
operands = Defunc x -> OpStack xs -> OpStack (x : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
x (Γ s o xs n r a -> OpStack xs
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o xs n r a
γ)})
evalPop :: Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalPop :: Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalPop (Machine MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k MachineMonad s o xs n r a
-> ((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o xs n r a -> Code (ST s (Maybe a))
m Γ s o (x : xs) n r a
γ -> Γ s o xs n r a -> Code (ST s (Maybe a))
m (Γ s o (x : xs) n r a
γ {operands :: OpStack xs
operands = let Op Defunc x
_ OpStack xs
xs = Γ s o (x : xs) n r a -> OpStack (x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (x : xs) n r a
γ in OpStack xs
xs})
evalLift2 :: Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a
evalLift2 :: Defunc (x -> y -> z)
-> Machine s o (z : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
evalLift2 Defunc (x -> y -> z)
f (Machine MachineMonad s o (z : xs) n r a
k) = MachineMonad s o (z : xs) n r a
k MachineMonad s o (z : xs) n r a
-> ((Γ s o (z : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o (y : x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (y : x : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o (z : xs) n r a -> Code (ST s (Maybe a))
m Γ s o (y : x : xs) n r a
γ -> Γ s o (z : xs) n r a -> Code (ST s (Maybe a))
m (Γ s o (y : x : xs) n r a
γ {operands :: OpStack (z : xs)
operands = let Op Defunc x
y (Op Defunc x
x OpStack xs
xs) = Γ s o (y : x : xs) n r a -> OpStack (y : x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (y : x : xs) n r a
γ in Defunc z -> OpStack xs -> OpStack (z : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op (Defunc (x -> y -> z) -> Defunc x -> Defunc y -> Defunc z
forall a b c.
Defunc (a -> b -> c) -> Defunc a -> Defunc b -> Defunc c
ap2 Defunc (x -> y -> z)
f Defunc x
x Defunc y
y) OpStack xs
xs})
evalSat :: (?ops :: InputOps (Rep o), PositionOps (Rep o), Trace) => Defunc (Char -> Bool) -> Machine s o (Char : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
evalSat :: Defunc (Char -> Bool)
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalSat Defunc (Char -> Bool)
p k :: Machine s o (Char : xs) ('Succ n) r a
k@(Machine MachineMonad s o (Char : xs) ('Succ n) r a
k') = do
Bool
bankrupt <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks Ctx s o a -> Bool
forall s o a. Ctx s o a -> Bool
isBankrupt
Bool
hasChange <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks Ctx s o a -> Bool
forall s o a. Ctx s o a -> Bool
hasCoin
if | Bool
bankrupt -> Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
emitCheckAndFetch Int
1 Machine s o (Char : xs) ('Succ n) r a
k
| Bool
hasChange -> (Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local Ctx s o a -> Ctx s o a
forall s o a. Ctx s o a -> Ctx s o a
spendCoin (Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o)) =>
Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
satFetch Machine s o (Char : xs) ('Succ n) r a
k)
| Bool
otherwise -> String
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall a. Trace => String -> a -> a
trace String
"I have a piggy :)" (MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$
(Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local Ctx s o a -> Ctx s o a
forall s o a. Ctx s o a -> Ctx s o a
breakPiggy (MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$
do Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
check <- (Ctx s o a
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a)
-> ReaderT
(Ctx s o a)
Identity
(Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a)
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
emitCheckAndFetch (Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a)
-> (Ctx s o a -> Int)
-> Ctx s o a
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx s o a -> Int
forall s o a. Ctx s o a -> Int
coins)
Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
check (MachineMonad s o (Char : xs) ('Succ n) r a
-> Machine s o (Char : xs) ('Succ n) r a
forall s o (xs :: [Type]) (n :: Nat) r a.
MachineMonad s o xs n r a -> Machine s o xs n r a
Machine ((Ctx s o a -> Ctx s o a)
-> MachineMonad s o (Char : xs) ('Succ n) r a
-> MachineMonad s o (Char : xs) ('Succ n) r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local Ctx s o a -> Ctx s o a
forall s o a. Ctx s o a -> Ctx s o a
spendCoin MachineMonad s o (Char : xs) ('Succ n) r a
k'))
where
satFetch :: (?ops :: InputOps (Rep o))
=> Machine s o (Char : xs) (Succ n) r a
-> MachineMonad s o xs (Succ n) r a
satFetch :: Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
satFetch Machine s o (Char : xs) ('Succ n) r a
mk = (Ctx s o a -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader ((Ctx s o a -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a)
-> (Ctx s o a -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs ('Succ n) r a
γ ->
(Defunc Char -> Defunc Bool)
-> ((Code Char -> Offset o -> Ctx s o a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a)))
-> (Defunc Char -> Offset o -> Ctx s o a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
forall o aux b.
(Defunc Char -> Defunc Bool)
-> ((Code Char -> Offset o -> aux -> Code b) -> Code b)
-> (Defunc Char -> Offset o -> aux -> Code b)
-> Code b
-> Code b
sat (Defunc (Char -> Bool) -> Defunc Char -> Defunc Bool
forall a b. Defunc (a -> b) -> Defunc a -> Defunc b
ap Defunc (Char -> Bool)
p) (Ctx s o a
-> ((Code Char -> Offset o -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a)))
-> (Code Char -> Offset o -> Ctx s o a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall s o a b.
Ctx s o a
-> ((Code Char -> Offset o -> Code b) -> Code b)
-> (Code Char -> Offset o -> Ctx s o a -> Code b)
-> Code b
readChar Ctx s o a
ctx (Offset o
-> (Code Char -> Offset o -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall o b.
(?ops::InputOps (Rep o)) =>
Offset o -> (Code Char -> Offset o -> Code b) -> Code b
fetch (Γ s o xs ('Succ n) r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs ('Succ n) r a
γ)))
(Machine s o (Char : xs) ('Succ n) r a
-> Γ s o xs ('Succ n) r a
-> Defunc Char
-> Offset o
-> Ctx s o a
-> Code (ST s (Maybe a))
forall s o x (xs :: [Type]) (n :: Nat) r a.
Machine s o (x : xs) n r a
-> Γ s o xs n r a
-> Defunc x
-> Offset o
-> Ctx s o a
-> Code (ST s (Maybe a))
continue Machine s o (Char : xs) ('Succ n) r a
mk Γ s o xs ('Succ n) r a
γ)
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ)
emitCheckAndFetch :: (?ops :: InputOps (Rep o), PositionOps (Rep o))
=> Int
-> Machine s o (Char : xs) (Succ n) r a
-> MachineMonad s o xs (Succ n) r a
emitCheckAndFetch :: Int
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
emitCheckAndFetch Int
n Machine s o (Char : xs) ('Succ n) r a
mk = do
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
sat <- Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o)) =>
Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
satFetch Machine s o (Char : xs) ('Succ n) r a
mk
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a)
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$ \Γ s o xs ('Succ n) r a
γ -> Int
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
-> Offset o
-> Code (ST s (Maybe a))
forall o a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int -> Code a -> Code a -> Offset o -> Code a
emitLengthCheck Int
n (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
sat Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs ('Succ n) r a
γ)
continue :: Machine s o (x : xs) n r a
-> Γ s o xs n r a
-> Defunc x
-> Offset o
-> Ctx s o a
-> Code (ST s (Maybe a))
continue Machine s o (x : xs) n r a
mk Γ s o xs n r a
γ Defunc x
c Offset o
input' = Machine s o (x : xs) n r a
-> Γ s o (x : xs) n r a -> Ctx s o a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
run Machine s o (x : xs) n r a
mk (Γ s o xs n r a
γ {input :: Offset o
input = Offset o
input', operands :: OpStack (x : xs)
operands = Defunc x -> OpStack xs -> OpStack (x : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
c (Γ s o xs n r a -> OpStack xs
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o xs n r a
γ)})
evalEmpt :: MachineMonad s o xs (Succ n) r a
evalEmpt :: MachineMonad s o xs ('Succ n) r a
evalEmpt = (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a)
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$! Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise
evalCommit :: Machine s o xs n r a -> MachineMonad s o xs (Succ n) r a
evalCommit :: Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a
evalCommit (Machine MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k MachineMonad s o xs n r a
-> ((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o xs n r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ -> let VCons AugmentedStaHandler s o a
_ Vec n (AugmentedStaHandler s o a)
hs = Γ s o xs ('Succ n) r a -> Vec ('Succ n) (AugmentedStaHandler s o a)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Vec n (AugmentedStaHandler s o a)
handlers Γ s o xs ('Succ n) r a
γ in Γ s o xs n r a -> Code (ST s (Maybe a))
mk (Γ s o xs ('Succ n) r a
γ {handlers :: Vec n (AugmentedStaHandler s o a)
handlers = Vec n (AugmentedStaHandler s o a)
hs})
evalCatch :: (PositionOps (Rep o), HandlerOps o) => Machine s o xs (Succ n) r a -> Handler o (Machine s o) (o : xs) n r a -> MachineMonad s o xs n r a
evalCatch :: Machine s o xs ('Succ n) r a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
evalCatch (Machine MachineMonad s o xs ('Succ n) r a
k) Handler o (Machine s o) (o : xs) n r a
h = (Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique ((Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a)
-> (Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall a b. (a -> b) -> a -> b
$ \Word
u -> case Handler o (Machine s o) (o : xs) n r a
h of
Always Bool
gh (Machine MachineMonad s o (o : xs) n r a
h) ->
((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a
-> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
-> ReaderT
(Ctx s o a)
Identity
(Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh Γ s o xs n r a
γ -> Γ s o xs n r a
-> Bool
-> StaHandlerBuilder s o a
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a b.
HandlerOps o =>
Γ s o xs n r a
-> Bool
-> StaHandlerBuilder s o a
-> (Γ s o xs ('Succ n) r a -> Code b)
-> Code b
bindAlwaysHandler Γ s o xs n r a
γ Bool
gh (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh Word
u) Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk) MachineMonad s o xs ('Succ n) r a
k ReaderT
(Ctx s o a)
Identity
(Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
MachineMonad s o (o : xs) n r a
h
Same Bool
gyes (Machine MachineMonad s o xs n r a
yes) Bool
gno (Machine MachineMonad s o (o : xs) n r a
no) ->
((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a
-> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs n r a
-> ReaderT
(Ctx s o a)
Identity
(Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall (m :: Type -> Type) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (\Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs n r a -> Code (ST s (Maybe a))
myes Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mno Γ s o xs n r a
γ -> Γ s o xs n r a
-> Bool
-> StaHandler s o a
-> Bool
-> StaHandlerBuilder s o a
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a b.
(HandlerOps o, PositionOps (Rep o)) =>
Γ s o xs n r a
-> Bool
-> StaHandler s o a
-> Bool
-> StaHandlerBuilder s o a
-> (Γ s o xs ('Succ n) r a -> Code b)
-> Code b
bindSameHandler Γ s o xs n r a
γ Bool
gyes (Γ s o xs n r a
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandler s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandler s o a
buildYesHandler Γ s o xs n r a
γ Γ s o xs n r a -> Code (ST s (Maybe a))
myes Word
u) Bool
gno (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mno Word
u) Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk) MachineMonad s o xs ('Succ n) r a
k MachineMonad s o xs n r a
MachineMonad s o xs n r a
yes ReaderT
(Ctx s o a)
Identity
(Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
MachineMonad s o (o : xs) n r a
no
evalTell :: Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
evalTell :: Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
evalTell (Machine MachineMonad s o (o : xs) n r a
k) = MachineMonad s o (o : xs) n r a
k MachineMonad s o (o : xs) n r a
-> ((Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mk Γ s o xs n r a
γ -> Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mk (Γ s o xs n r a
γ {operands :: OpStack (o : xs)
operands = Defunc o -> OpStack xs -> OpStack (o : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op (Offset o -> Defunc o
forall o. Offset o -> Defunc o
OFFSET (Γ s o xs n r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs n r a
γ)) (Γ s o xs n r a -> OpStack xs
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o xs n r a
γ)})
evalSeek :: Machine s o xs n r a -> MachineMonad s o (o : xs) n r a
evalSeek :: Machine s o xs n r a -> MachineMonad s o (o : xs) n r a
evalSeek (Machine MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k MachineMonad s o xs n r a
-> ((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (o : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o xs n r a -> Code (ST s (Maybe a))
mk Γ s o (o : xs) n r a
γ -> let Op (OFFSET Offset x
input) OpStack xs
xs = Γ s o (o : xs) n r a -> OpStack (o : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (o : xs) n r a
γ in Γ s o xs n r a -> Code (ST s (Maybe a))
mk (Γ s o (o : xs) n r a
γ {operands :: OpStack xs
operands = OpStack xs
xs, input :: Offset o
input = Offset o
input})
evalCase :: Machine s o (x : xs) n r a -> Machine s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a
evalCase :: Machine s o (x : xs) n r a
-> Machine s o (y : xs) n r a
-> MachineMonad s o (Either x y : xs) n r a
evalCase (Machine MachineMonad s o (x : xs) n r a
p) (Machine MachineMonad s o (y : xs) n r a
q) = ((Γ s o (x : xs) n r a -> Q (TExp (ST s (Maybe a))))
-> (Γ s o (y : xs) n r a -> Q (TExp (ST s (Maybe a))))
-> Γ s o (Either x y : xs) n r a
-> Q (TExp (ST s (Maybe a))))
-> MachineMonad s o (x : xs) n r a
-> MachineMonad s o (y : xs) n r a
-> MachineMonad s o (Either x y : xs) n r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o (x : xs) n r a -> Q (TExp (ST s (Maybe a)))
mp Γ s o (y : xs) n r a -> Q (TExp (ST s (Maybe a)))
mq Γ s o (Either x y : xs) n r a
γ ->
let Op Defunc x
e OpStack xs
xs = Γ s o (Either x y : xs) n r a -> OpStack (Either x y : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (Either x y : xs) n r a
γ
in [||case $$(genDefunc e) of
Left x -> $$(mp (γ {operands = Op (FREEVAR [||x||]) xs}))
Right y -> $$(mq (γ {operands = Op (FREEVAR [||y||]) xs}))||]) MachineMonad s o (x : xs) n r a
p MachineMonad s o (y : xs) n r a
q
evalChoices :: [Defunc (x -> Bool)] -> [Machine s o xs n r a] -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalChoices :: [Defunc (x -> Bool)]
-> [Machine s o xs n r a]
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalChoices [Defunc (x -> Bool)]
fs [Machine s o xs n r a]
ks (Machine MachineMonad s o xs n r a
def) = ((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> [Γ s o xs n r a -> Code (ST s (Maybe a))]
-> Γ s o (x : xs) n r a
-> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
-> ReaderT
(Ctx s o a) Identity [Γ s o xs n r a -> Code (ST s (Maybe a))]
-> MachineMonad s o (x : xs) n r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o xs n r a -> Code (ST s (Maybe a))
mdef [Γ s o xs n r a -> Code (ST s (Maybe a))]
mks Γ s o (x : xs) n r a
γ -> let Op Defunc x
x OpStack xs
xs = Γ s o (x : xs) n r a -> OpStack (x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (x : xs) n r a
γ in Defunc x
-> [Defunc (x -> Bool)]
-> [Γ s o xs n r a -> Code (ST s (Maybe a))]
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a
-> Code (ST s (Maybe a))
forall a t a.
Defunc a
-> [Defunc (a -> Bool)]
-> [t -> Code a]
-> (t -> Code a)
-> t
-> Code a
go Defunc x
x [Defunc (x -> Bool)]
fs [Γ s o xs n r a -> Code (ST s (Maybe a))]
mks Γ s o xs n r a -> Code (ST s (Maybe a))
mdef (Γ s o (x : xs) n r a
γ {operands :: OpStack xs
operands = OpStack xs
xs}))
MachineMonad s o xs n r a
def
([Machine s o xs n r a]
-> (Machine s o xs n r a -> MachineMonad s o xs n r a)
-> ReaderT
(Ctx s o a) Identity [Γ s o xs n r a -> Code (ST s (Maybe a))]
forall (t :: Type -> Type) (m :: Type -> Type) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Machine s o xs n r a]
ks Machine s o xs n r a -> MachineMonad s o xs n r a
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a -> MachineMonad s o xs n r a
getMachine)
where
go :: Defunc a
-> [Defunc (a -> Bool)]
-> [t -> Code a]
-> (t -> Code a)
-> t
-> Code a
go Defunc a
x (Defunc (a -> Bool)
f:[Defunc (a -> Bool)]
fs) (t -> Code a
mk:[t -> Code a]
mks) t -> Code a
def t
γ = Defunc Bool -> Code a -> Code a -> Code a
forall a. Defunc Bool -> Code a -> Code a -> Code a
_if (Defunc (a -> Bool) -> Defunc a -> Defunc Bool
forall a b. Defunc (a -> b) -> Defunc a -> Defunc b
ap Defunc (a -> Bool)
f Defunc a
x) (t -> Code a
mk t
γ) (Defunc a
-> [Defunc (a -> Bool)]
-> [t -> Code a]
-> (t -> Code a)
-> t
-> Code a
go Defunc a
x [Defunc (a -> Bool)]
fs [t -> Code a]
mks t -> Code a
def t
γ)
go Defunc a
_ [Defunc (a -> Bool)]
_ [t -> Code a]
_ t -> Code a
def t
γ = t -> Code a
def t
γ
evalIter :: (RecBuilder o, PositionOps (Rep o), HandlerOps o)
=> MVar Void -> Machine s o '[] One Void a -> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
evalIter :: MVar Void
-> Machine s o '[] One Void a
-> Handler o (Machine s o) (o : xs) n r a
-> MachineMonad s o xs n r a
evalIter MVar Void
μ Machine s o '[] One Void a
l Handler o (Machine s o) (o : xs) n r a
h =
(Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique ((Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a)
-> (Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall a b. (a -> b) -> a -> b
$ \Word
u1 ->
(Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique ((Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a)
-> (Word -> MachineMonad s o xs n r a) -> MachineMonad s o xs n r a
forall a b. (a -> b) -> a -> b
$ \Word
u2 ->
case Handler o (Machine s o) (o : xs) n r a
h of
Always Bool
gh (Machine MachineMonad s o (o : xs) n r a
h) ->
((Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (o : xs) n r a
-> ReaderT (Ctx s o a) Identity (Ctx s o a)
-> ReaderT
(Ctx s o a) Identity (Γ s o xs n r a -> Code (ST s (Maybe a)))
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh Ctx s o a
ctx Γ s o xs n r a
γ -> Ctx s o a
-> MVar Void
-> Machine s o '[] One Void a
-> Bool
-> StaHandlerBuilder s o a
-> Offset o
-> Word
-> Code (ST s (Maybe a))
forall s o a.
RecBuilder o =>
Ctx s o a
-> MVar Void
-> Machine s o '[] One Void a
-> Bool
-> StaHandlerBuilder s o a
-> Offset o
-> Word
-> Code (ST s (Maybe a))
bindIterAlways Ctx s o a
ctx MVar Void
μ Machine s o '[] One Void a
l Bool
gh (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh Word
u1) (Γ s o xs n r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs n r a
γ) Word
u2) MachineMonad s o (o : xs) n r a
h ReaderT (Ctx s o a) Identity (Ctx s o a)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
Same Bool
gyes (Machine MachineMonad s o xs n r a
yes) Bool
gno (Machine MachineMonad s o (o : xs) n r a
no) ->
((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Γ s o xs n r a
-> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
-> MachineMonad s o (o : xs) n r a
-> ReaderT (Ctx s o a) Identity (Ctx s o a)
-> MachineMonad s o xs n r a
forall (m :: Type -> Type) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 (\Γ s o xs n r a -> Code (ST s (Maybe a))
myes Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mno Ctx s o a
ctx Γ s o xs n r a
γ -> Ctx s o a
-> MVar Void
-> Machine s o '[] One Void a
-> Bool
-> StaHandler s o a
-> Bool
-> StaHandlerBuilder s o a
-> Offset o
-> Word
-> Code (ST s (Maybe a))
forall s o a.
(RecBuilder o, HandlerOps o, PositionOps (Rep o)) =>
Ctx s o a
-> MVar Void
-> Machine s o '[] One Void a
-> Bool
-> StaHandler s o a
-> Bool
-> StaHandlerBuilder s o a
-> Offset o
-> Word
-> Code (ST s (Maybe a))
bindIterSame Ctx s o a
ctx MVar Void
μ Machine s o '[] One Void a
l Bool
gyes (Γ s o xs n r a
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandler s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandler s o a
buildYesHandler Γ s o xs n r a
γ Γ s o xs n r a -> Code (ST s (Maybe a))
myes Word
u1) Bool
gno (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Word
-> StaHandlerBuilder s o a
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mno Word
u1) (Γ s o xs n r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs n r a
γ) Word
u2) MachineMonad s o xs n r a
yes MachineMonad s o (o : xs) n r a
no ReaderT (Ctx s o a) Identity (Ctx s o a)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
evalJoin :: ΦVar x -> MachineMonad s o (x : xs) n r a
evalJoin :: ΦVar x -> MachineMonad s o (x : xs) n r a
evalJoin ΦVar x
φ = ΦVar x -> ReaderT (Ctx s o a) Identity (StaCont s o a x)
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
ΦVar x -> m (StaCont s o a x)
askΦ ΦVar x
φ ReaderT (Ctx s o a) Identity (StaCont s o a x)
-> (StaCont s o a x
-> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> StaCont s o a x -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
forall s o a x (xs :: [Type]) (n :: Nat) r.
StaCont s o a x -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
resume
evalMkJoin :: JoinBuilder o => ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMkJoin :: ΦVar x
-> Machine s o (x : xs) n r a
-> Machine s o xs n r a
-> MachineMonad s o xs n r a
evalMkJoin = ΦVar x
-> Machine s o (x : xs) n r a
-> Machine s o xs n r a
-> MachineMonad s o xs n r a
forall s o (xs :: [Type]) (n :: Nat) r a x.
JoinBuilder o =>
ΦVar x
-> Machine s o (x : xs) n r a
-> Machine s o xs n r a
-> MachineMonad s o xs n r a
setupJoinPoint
evalSwap :: Machine s o (x : y : xs) n r a -> MachineMonad s o (y : x : xs) n r a
evalSwap :: Machine s o (x : y : xs) n r a
-> MachineMonad s o (y : x : xs) n r a
evalSwap (Machine MachineMonad s o (x : y : xs) n r a
k) = MachineMonad s o (x : y : xs) n r a
k MachineMonad s o (x : y : xs) n r a
-> ((Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o (y : x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (y : x : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a))
mk Γ s o (y : x : xs) n r a
γ -> Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a))
mk (Γ s o (y : x : xs) n r a
γ {operands :: OpStack (x : y : xs)
operands = let Op Defunc x
y (Op Defunc x
x OpStack xs
xs) = Γ s o (y : x : xs) n r a -> OpStack (y : x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (y : x : xs) n r a
γ in Defunc x -> OpStack (y : xs) -> OpStack (x : y : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
x (Defunc y -> OpStack xs -> OpStack (y : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc y
y OpStack xs
xs)})
evalDup :: Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
evalDup :: Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
evalDup (Machine MachineMonad s o (x : x : xs) n r a
k) = MachineMonad s o (x : x : xs) n r a
k MachineMonad s o (x : x : xs) n r a
-> ((Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a))
mk Γ s o (x : xs) n r a
γ ->
let Op Defunc x
x OpStack xs
xs = Γ s o (x : xs) n r a -> OpStack (x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (x : xs) n r a
γ
in Defunc x
-> (Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a))
forall x r. Defunc x -> (Defunc x -> Code r) -> Code r
dup Defunc x
x ((Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)))
-> (Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a))
forall a b. (a -> b) -> a -> b
$ \Defunc x
dupx -> Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a))
mk (Γ s o (x : xs) n r a
γ {operands :: OpStack (x : x : xs)
operands = Defunc x -> OpStack (x : xs) -> OpStack (x : x : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
dupx (Defunc x -> OpStack xs -> OpStack (x : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
dupx OpStack xs
xs)})
evalMake :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalMake :: ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalMake ΣVar x
σ Access
a Machine s o xs n r a
k = (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader ((Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a)
-> (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o (x : xs) n r a
γ ->
let Op Defunc x
x OpStack xs
xs = Γ s o (x : xs) n r a -> OpStack (x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (x : xs) n r a
γ
in ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
forall x s o a r.
ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s r))
-> Ctx s o a
-> Code (ST s r)
newΣ ΣVar x
σ Access
a Defunc x
x (Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
run Machine s o xs n r a
k (Γ s o (x : xs) n r a
γ {operands :: OpStack xs
operands = OpStack xs
xs})) Ctx s o a
ctx
evalGet :: ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalGet :: ΣVar x
-> Access
-> Machine s o (x : xs) n r a
-> MachineMonad s o xs n r a
evalGet ΣVar x
σ Access
a Machine s o (x : xs) n r a
k = (Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader ((Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a)
-> (Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs n r a
γ -> ΣVar x
-> Access
-> (Defunc x -> Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
forall x s o a r.
ΣVar x
-> Access
-> (Defunc x -> Ctx s o a -> Code (ST s r))
-> Ctx s o a
-> Code (ST s r)
readΣ ΣVar x
σ Access
a (\Defunc x
x -> Machine s o (x : xs) n r a
-> Γ s o (x : xs) n r a -> Ctx s o a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
run Machine s o (x : xs) n r a
k (Γ s o xs n r a
γ {operands :: OpStack (x : xs)
operands = Defunc x -> OpStack xs -> OpStack (x : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op Defunc x
x (Γ s o xs n r a -> OpStack xs
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o xs n r a
γ)})) Ctx s o a
ctx
evalPut :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalPut :: ΣVar x
-> Access
-> Machine s o xs n r a
-> MachineMonad s o (x : xs) n r a
evalPut ΣVar x
σ Access
a Machine s o xs n r a
k = (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader ((Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a)
-> (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) n r a
forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o (x : xs) n r a
γ ->
let Op Defunc x
x OpStack xs
xs = Γ s o (x : xs) n r a -> OpStack (x : xs)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o (x : xs) n r a
γ
in ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
forall x s o a r.
ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s r))
-> Ctx s o a
-> Code (ST s r)
writeΣ ΣVar x
σ Access
a Defunc x
x (Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
run Machine s o xs n r a
k (Γ s o (x : xs) n r a
γ {operands :: OpStack xs
operands = OpStack xs
xs})) Ctx s o a
ctx
evalLogEnter :: (?ops :: InputOps (Rep o), LogHandler o, HandlerOps o)
=> String -> Machine s o xs (Succ (Succ n)) r a -> MachineMonad s o xs (Succ n) r a
evalLogEnter :: String
-> Machine s o xs ('Succ ('Succ n)) r a
-> MachineMonad s o xs ('Succ n) r a
evalLogEnter String
name (Machine MachineMonad s o xs ('Succ ('Succ n)) r a
mk) = (Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique ((Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a)
-> (Word -> MachineMonad s o xs ('Succ n) r a)
-> MachineMonad s o xs ('Succ n) r a
forall a b. (a -> b) -> a -> b
$ \Word
u ->
((Γ s o xs ('Succ ('Succ n)) r a -> Code (ST s (Maybe a)))
-> Ctx s o a -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs ('Succ ('Succ n)) r a
-> ReaderT (Ctx s o a) Identity (Ctx s o a)
-> MachineMonad s o xs ('Succ n) r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o xs ('Succ ('Succ n)) r a -> Code (ST s (Maybe a))
k Ctx s o a
ctx Γ s o xs ('Succ n) r a
γ -> [|| Debug.Trace.trace $$(preludeString name '>' γ ctx "") $$(bindAlwaysHandler γ True (logHandler name ctx γ u) k)||])
((Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs ('Succ ('Succ n)) r a
-> MachineMonad s o xs ('Succ ('Succ n)) r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local Ctx s o a -> Ctx s o a
forall s o a. Ctx s o a -> Ctx s o a
debugUp MachineMonad s o xs ('Succ ('Succ n)) r a
mk)
ReaderT (Ctx s o a) Identity (Ctx s o a)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
evalLogExit :: (?ops :: InputOps (Rep o), PositionOps (Rep o), LogOps (Rep o)) => String -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalLogExit :: String -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalLogExit String
name (Machine MachineMonad s o xs n r a
mk) =
((Γ s o xs n r a -> Q (TExp (ST s (Maybe a))))
-> Ctx s o a -> Γ s o xs n r a -> Q (TExp (ST s (Maybe a))))
-> MachineMonad s o xs n r a
-> ReaderT (Ctx s o a) Identity (Ctx s o a)
-> MachineMonad s o xs n r a
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))
k Ctx s o a
ctx Γ s o xs n r a
γ -> [|| Debug.Trace.trace $$(preludeString name '<' γ (debugDown ctx) (color Green " Good")) $$(k γ) ||])
((Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs n r a -> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local Ctx s o a -> Ctx s o a
forall s o a. Ctx s o a -> Ctx s o a
debugDown MachineMonad s o xs n r a
mk)
ReaderT (Ctx s o a) Identity (Ctx s o a)
forall r (m :: Type -> Type). MonadReader r m => m r
ask
evalMeta :: (?ops :: InputOps (Rep o), PositionOps (Rep o)) => MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMeta :: MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMeta (AddCoins Coins
coins) (Machine MachineMonad s o xs n r a
k) =
do Bool
requiresPiggy <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks Ctx s o a -> Bool
forall s o a. Ctx s o a -> Bool
hasCoin
if Bool
requiresPiggy then (Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs n r a -> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Coins -> Ctx s o a -> Ctx s o a
forall s o a. Coins -> Ctx s o a -> Ctx s o a
storePiggy Coins
coins) MachineMonad s o xs n r a
k
else (Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs n r a -> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Coins -> Ctx s o a -> Ctx s o a
forall s o a. Coins -> Ctx s o a -> Ctx s o a
giveCoins Coins
coins) MachineMonad s o xs n r a
k MachineMonad s o xs n r a
-> ((Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o xs n r a -> Code (ST s (Maybe a))
mk Γ s o xs n r a
γ -> Int
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
-> Offset o
-> Code (ST s (Maybe a))
forall o a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int -> Code a -> Code a -> Offset o -> Code a
emitLengthCheck (Coins -> Int
willConsume Coins
coins) (Γ s o xs n r a -> Code (ST s (Maybe a))
mk Γ s o xs n r a
γ) (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs n r a
Γ s o xs ('Succ n) r a
γ) (Γ s o xs n r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs n r a
γ)
evalMeta (RefundCoins Coins
coins) (Machine MachineMonad s o xs n r a
k) = (Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs n r a -> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Coins -> Ctx s o a -> Ctx s o a
forall s o a. Coins -> Ctx s o a -> Ctx s o a
refundCoins Coins
coins) MachineMonad s o xs n r a
k
evalMeta (DrainCoins Coins
coins) (Machine MachineMonad s o xs n r a
k) =
(Bool
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a)))
-> ReaderT (Ctx s o a) Identity Bool
-> ReaderT
(Ctx s o a)
Identity
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> ReaderT
(Ctx s o a)
Identity
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\Bool
canAfford Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ -> if Bool
canAfford then Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ else Int
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
-> Offset o
-> Code (ST s (Maybe a))
forall o a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int -> Code a -> Code a -> Offset o -> Code a
emitLengthCheck (Coins -> Int
willConsume Coins
coins) (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs ('Succ n) r a
γ))
((Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (Int -> Ctx s o a -> Bool
forall s o a. Int -> Ctx s o a -> Bool
canAfford (Coins -> Int
willConsume Coins
coins)))
MachineMonad s o xs n r a
ReaderT
(Ctx s o a)
Identity
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
k
evalMeta (GiveBursary Coins
coins) (Machine MachineMonad s o xs n r a
k) = (Ctx s o a -> Ctx s o a)
-> MachineMonad s o xs n r a -> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Coins -> Ctx s o a -> Ctx s o a
forall s o a. Coins -> Ctx s o a -> Ctx s o a
giveCoins Coins
coins) MachineMonad s o xs n r a
k
evalMeta (PrefetchChar Bool
check) Machine s o xs n r a
k =
do Bool
bankrupt <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks Ctx s o a -> Bool
forall s o a. Ctx s o a -> Bool
isBankrupt
Bool
-> ReaderT (Ctx s o a) Identity ()
-> ReaderT (Ctx s o a) Identity ()
forall (f :: Type -> Type). Applicative f => Bool -> f () -> f ()
when (Bool -> Bool
not Bool
bankrupt Bool -> Bool -> Bool
&& Bool
check) (String -> ReaderT (Ctx s o a) Identity ()
forall a. HasCallStack => String -> a
error String
"must be bankrupt to generate a prefetch check")
Bool
-> ReaderT
(Ctx s o a)
Identity
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> ReaderT
(Ctx s o a)
Identity
(Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
forall (f :: Type -> Type) s o a o s (xs :: [Type]) (n :: Nat) r a.
(MonadReader (Ctx s o a) f, ?ops::InputOps (Rep o),
PositionOps (Rep o)) =>
Bool
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
mkCheck Bool
check ((Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader ((Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a)
-> (Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a)))
-> MachineMonad s o xs n r a
forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs n r a
γ -> Offset o
-> Ctx s o a
-> (Ctx s o a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall o s a b.
(?ops::InputOps (Rep o)) =>
Offset o -> Ctx s o a -> (Ctx s o a -> Code b) -> Code b
prefetch (Γ s o xs n r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs n r a
γ) Ctx s o a
ctx (Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Machine s o xs n r a
-> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a))
run Machine s o xs n r a
k Γ s o xs n r a
γ))
where
mkCheck :: Bool
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
mkCheck Bool
True f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
k = (Ctx s o a -> Ctx s o a)
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (Coins -> Ctx s o a -> Ctx s o a
forall s o a. Coins -> Ctx s o a -> Ctx s o a
giveCoins (Int -> Coins
int Int
1)) f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
k f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> ((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ -> Int
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
-> Offset o
-> Code (ST s (Maybe a))
forall o a.
(?ops::InputOps (Rep o), PositionOps (Rep o)) =>
Int -> Code a -> Code a -> Offset o -> Code a
emitLengthCheck Int
1 (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ) (Γ s o xs ('Succ n) r a -> Offset o
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Offset o
input Γ s o xs ('Succ n) r a
γ)
mkCheck Bool
False f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
k = f (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
k
prefetch :: Offset o -> Ctx s o a -> (Ctx s o a -> Code b) -> Code b
prefetch Offset o
o Ctx s o a
ctx Ctx s o a -> Code b
k = Offset o -> (Code Char -> Offset o -> Code b) -> Code b
forall o b.
(?ops::InputOps (Rep o)) =>
Offset o -> (Code Char -> Offset o -> Code b) -> Code b
fetch Offset o
o (\Code Char
c Offset o
o' -> Ctx s o a -> Code b
k (Code Char -> Offset o -> Ctx s o a -> Ctx s o a
forall o s a. Code Char -> Offset o -> Ctx s o a -> Ctx s o a
addChar Code Char
c Offset o
o' Ctx s o a
ctx))
evalMeta MetaInstr n
BlockCoins (Machine MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k