{-# LANGUAGE ImplicitParams,
             MultiWayIf,
             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)
import Control.Monad.Reader                           (ask, asks, local)
import Control.Monad.ST                               (runST)
import Parsley.Internal.Backend.Machine.Defunc        (Defunc(FREEVAR, OFFSET), genDefunc, genDefunc1, ap2)
import Parsley.Internal.Backend.Machine.Identifiers   (MVar(..), ΦVar, ΣVar)
import Parsley.Internal.Backend.Machine.InputOps      (InputDependant, PositionOps, LogOps, InputOps(InputOps))
import Parsley.Internal.Backend.Machine.InputRep      (Rep)
import Parsley.Internal.Backend.Machine.Instructions  (Instr(..), MetaInstr(..), Access(..))
import Parsley.Internal.Backend.Machine.LetBindings   (LetBinding(..))
import Parsley.Internal.Backend.Machine.LetRecBuilder
import Parsley.Internal.Backend.Machine.Ops
import Parsley.Internal.Backend.Machine.State
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 !Binding o a a
p Regs rs
_) 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))
             (\names -> run (readyMachine p) (Γ Empty (halt @o) [||offset||] (VCons (fatal @o) VNil)) (emptyCtx names)))
  ||]
  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.
ContOps 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).
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 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 Machine s o (o : xs) n r a
h)         = Machine s o xs ('Succ n) r a
-> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
forall o s (xs :: [Type]) (n :: Nat) r a.
HandlerOps o =>
Machine s o xs ('Succ n) r a
-> 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 Machine s o (o : xs) n r a
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
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 Machine s o (o : xs) n r a
k)        = MVar Void
-> Machine s o '[] One Void a
-> 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, ReturnOps o, HandlerOps o) =>
MVar Void
-> Machine s o '[] One Void a
-> 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 Machine s o (o : xs) n r a
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) =>
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 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 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 -> Code (Cont s o a x)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Cont s o a r)
retCont (Γ s o (x : xs) n x a -> Code (Cont s o a x))
-> (Code (Cont 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
>>= Code (Cont 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.
Code (Cont 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. ContOps 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) = ((Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
 -> Code
      ((x -> Rep o -> ST s (Maybe a))
       -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))
 -> Γ s o xs ('Succ n) r a
 -> Code (ST s (Maybe a)))
-> MachineMonad s o (x : xs) ('Succ n) r a
-> ReaderT
     (Ctx s o a)
     Identity
     (Code
        ((x -> Rep o -> ST s (Maybe a))
         -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe 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 (x : xs) ('Succ n) r a -> Code (ST s (Maybe a))
mk Code
  ((x -> Rep o -> ST s (Maybe a))
   -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))
sub γ :: Γ s o xs ('Succ n) r a
γ@Γ{Code (Cont s o a r)
Code (Rep o)
HandlerStack ('Succ n) s o a
OpStack xs
handlers :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> HandlerStack n s o a
input :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Rep o)
operands :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
handlers :: HandlerStack ('Succ n) s o a
input :: Code (Rep o)
retCont :: Code (Cont s o a r)
operands :: OpStack xs
retCont :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Cont s o a r)
..} -> Code
  ((x -> Rep o -> ST s (Maybe a))
   -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))
-> Code (x -> Rep o -> ST s (Maybe a))
-> Code (Rep o)
-> HandlerStack ('Succ n) s o a
-> Code (ST s (Maybe a))
forall o s a x (n :: Nat).
Code (SubRoutine s o a x)
-> Code (Cont s o a x)
-> Code (Rep o)
-> Vec ('Succ n) (Code (Handler s o a))
-> Code (ST s (Maybe a))
callWithContinuation @o Code
  ((x -> Rep o -> ST s (Maybe a))
   -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))
sub ((Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a -> Code (x -> Rep o -> ST s (Maybe a))
forall o s x (xs :: [Type]) (n :: Nat) r a.
ContOps o =>
(Γ s o (x : xs) n r a -> Code (ST s (Maybe a)))
-> Γ s o xs n r a -> Code (Cont s o a x)
suspend Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ) Code (Rep o)
input HandlerStack ('Succ n) s o a
handlers) MachineMonad s o (x : xs) ('Succ n) r a
k (MVar x
-> ReaderT
     (Ctx s o a)
     Identity
     (Code
        ((x -> Rep o -> ST s (Maybe a))
         -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a)))
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
MVar x -> m (Code (SubRoutine s o a x))
askSub MVar x
μ)

evalJump :: forall s o a x n. 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 (Code (SubRoutine s o a x))
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
MVar x -> m (Code (SubRoutine s o a x))
askSub MVar x
μ ReaderT (Ctx s o a) Identity (Code (SubRoutine s o a x))
-> (Code (SubRoutine 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
<&> \Code (SubRoutine s o a x)
sub Γ{Code (Cont s o a x)
Code (Rep o)
HandlerStack ('Succ n) s o a
OpStack '[]
handlers :: HandlerStack ('Succ n) s o a
input :: Code (Rep o)
retCont :: Code (Cont s o a x)
operands :: OpStack '[]
handlers :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> HandlerStack n s o a
input :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Rep o)
operands :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
retCont :: forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Cont s o a r)
..} -> Code (SubRoutine s o a x)
-> Code (Cont s o a x)
-> Code (Rep o)
-> HandlerStack ('Succ n) s o a
-> Code (ST s (Maybe a))
forall o s a x (n :: Nat).
Code (SubRoutine s o a x)
-> Code (Cont s o a x)
-> Code (Rep o)
-> Vec ('Succ n) (Code (Handler s o a))
-> Code (ST s (Maybe a))
callWithContinuation @o Code (SubRoutine s o a x)
sub Code (Cont s o a x)
retCont Code (Rep o)
input HandlerStack ('Succ n) 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 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 (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 -> Maybe Int
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
maybeEmitCheck (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1) ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
 -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> MachineMonad s o (Char : xs) ('Succ n) r a
k
     | Bool
hasChange -> Maybe Int
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
maybeEmitCheck Maybe Int
forall a. Maybe a
Nothing ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
 -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (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
     | 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 (Maybe Int
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
maybeEmitCheck (Maybe Int
 -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
 -> Γ s o xs ('Succ n) r a
 -> Code (ST s (Maybe a)))
-> (Int -> Maybe Int)
-> Int
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
 -> (Γ s o (Char : 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 Int
-> ReaderT
     (Ctx s o a)
     Identity
     ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
      -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> (Ctx s o a -> Int) -> ReaderT (Ctx s o a) Identity Int
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks Ctx s o a -> Int
forall s o a. Ctx s o a -> Int
coins ReaderT
  (Ctx s o a)
  Identity
  ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
   -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> MachineMonad s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> (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
    maybeEmitCheck :: Maybe Int
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
maybeEmitCheck Maybe Int
Nothing Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ = (Code Char -> Code Bool)
-> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Γ s o xs ('Succ n) r a
-> Code (ST s (Maybe a))
forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o)) =>
(Code Char -> Code Bool)
-> (Γ s o (Char : xs) n r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Γ s o xs n r a
-> Code (ST s (Maybe a))
sat (Defunc (Char -> Bool) -> Code Char -> Code Bool
forall a b. Defunc (a -> b) -> Code a -> Code b
genDefunc1 Defunc (Char -> Bool)
p) Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))
mk (Γ 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
γ
    maybeEmitCheck (Just Int
n) Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ =
      [|| let bad = $$(raise γ) in $$(emitLengthCheck n (sat (genDefunc1 p) mk [||bad||]) [||bad||] γ)||]

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 Code (Rep o -> ST s (Maybe a))
_ Vec n (Code (Rep o -> ST s (Maybe a)))
hs = Γ s o xs ('Succ n) r a
-> Vec ('Succ n) (Code (Rep o -> ST s (Maybe a)))
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> HandlerStack n 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 :: HandlerStack n s o a
handlers = HandlerStack n s o a
hs})

evalCatch :: HandlerOps o => Machine s o xs (Succ n) r a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
evalCatch :: Machine s o xs ('Succ n) r a
-> 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) (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
-> MachineMonad s o (o : xs) n r 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
-> (Code (Rep o) -> Code (Handler 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.
Γ s o xs n r a
-> (Code (Rep o) -> Code (Handler s o a))
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
setupHandler Γ s o xs n r a
γ (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Code (Rep o)
-> Code (Handler s o a)
forall o s (xs :: [Type]) (n :: Nat) r a.
HandlerOps o =>
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Code (Rep o)
-> Code (Handler s o a)
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh) Γ 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 (o : xs) n r a
h

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 (Code (Rep o) -> Defunc o
forall o. Code (Rep o) -> Defunc o
OFFSET (Γ s o xs n r a -> Code (Rep o)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Rep 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 Code (Rep 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 :: Code (Rep o)
input = Code (Rep 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 -> Q (TExp (ST s (Maybe a))))
 -> [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))]
 -> Γ s o (x : xs) n r a
 -> Q (TExp (ST s (Maybe a))))
-> MachineMonad s o xs n r a
-> ReaderT
     (Ctx s o a) Identity [Γ s o xs n r a -> Q (TExp (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 -> Q (TExp (ST s (Maybe a)))
mdef [Γ s o xs n r a -> Q (TExp (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 -> Q (TExp (ST s (Maybe a)))]
-> (Γ s o xs n r a -> Q (TExp (ST s (Maybe a))))
-> Γ s o xs n r a
-> Q (TExp (ST s (Maybe a)))
forall a t p.
Defunc a
-> [Defunc (a -> Bool)]
-> [t -> Q (TExp p)]
-> (t -> Q (TExp p))
-> t
-> Q (TExp p)
go Defunc x
x [Defunc (x -> Bool)]
fs [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))]
mks Γ s o xs n r a -> Q (TExp (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 -> Q (TExp (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 -> Q (TExp p)]
-> (t -> Q (TExp p))
-> t
-> Q (TExp p)
go Defunc a
x (Defunc (a -> Bool)
f:[Defunc (a -> Bool)]
fs) (t -> Q (TExp p)
mk:[t -> Q (TExp p)]
mks) t -> Q (TExp p)
def t
γ = [||
        if $$(genDefunc1 f (genDefunc x)) then $$(mk γ)
        else $$(go x fs mks def γ)
      ||]
    go Defunc a
_ [Defunc (a -> Bool)]
_ [t -> Q (TExp p)]
_ t -> Q (TExp p)
def t
γ = t -> Q (TExp p)
def t
γ

evalIter :: (RecBuilder o, ReturnOps o, HandlerOps o)
         => MVar Void -> Machine s o '[] One Void a -> Machine s o (o : xs) n r a
         -> MachineMonad s o xs n r a
evalIter :: MVar Void
-> Machine s o '[] One Void a
-> 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 (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)
-> 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 (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
-> (Code (Rep o) -> Code (Handler s o a))
-> Code (Rep o)
-> Code (ST s (Maybe a))
forall o s a.
(RecBuilder o, ReturnOps o) =>
Ctx s o a
-> MVar Void
-> Machine s o '[] One Void a
-> (Code (Rep o) -> Code (Handler s o a))
-> Code (Rep o)
-> Code (ST s (Maybe a))
buildIter Ctx s o a
ctx MVar Void
μ Machine s o '[] One Void a
l (Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Code (Rep o)
-> Code (Handler s o a)
forall o s (xs :: [Type]) (n :: Nat) r a.
HandlerOps o =>
Γ s o xs n r a
-> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a)))
-> Code (Rep o)
-> Code (Handler s o a)
buildHandler Γ s o xs n r a
γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a))
mh) (Γ s o xs n r a -> Code (Rep o)
forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> Code (Rep o)
input Γ s o xs n r a
γ)) 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

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 (Code (Cont s o a x))
forall s o a (m :: Type -> Type) x.
MonadReader (Ctx s o a) m =>
ΦVar x -> m (Code (Cont s o a x))
askΦ ΦVar x
φ ReaderT (Ctx s o a) Identity (Code (Cont s o a x))
-> (Code (Cont 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
<&> Code (Cont 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.
Code (Cont 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 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
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
asks ((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.
ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
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
asks ((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.
ΣVar x
-> Access
-> (Defunc x -> Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
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
asks ((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.
ΣVar x
-> Access
-> Defunc x
-> (Ctx s o a -> Code (ST s (Maybe a)))
-> Ctx s o a
-> Code (ST s (Maybe a))
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) => 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) =
  ((Γ 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 "") $$(setupHandler γ (logHandler name ctx γ) 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 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 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 Int
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 (Int -> Ctx s o a -> Ctx s o a
forall s o a. Int -> Ctx s o a -> Ctx s o a
storePiggy Int
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 (Int -> Ctx s o a -> Ctx s o a
forall s o a. Int -> Ctx s o a -> Ctx s o a
giveCoins Int
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 ('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) 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
γ -> Int
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Γ s o xs n r a
-> Code (ST s (Maybe a))
forall s o (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps o) =>
Int
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Γ s o xs n r a
-> Code (ST s (Maybe a))
emitLengthCheck Int
coins Γ s o xs n r a -> Code (ST s (Maybe a))
mk (Γ 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 n r a
Γ s o xs ('Succ n) r a
γ
evalMeta (RefundCoins Int
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 (Int -> Ctx s o a -> Ctx s o a
forall s o a. Int -> Ctx s o a -> Ctx s o a
giveCoins Int
coins) MachineMonad s o xs n r a
k
evalMeta (DrainCoins Int
coins) (Machine MachineMonad s o xs n r a
k) = (Int
 -> (Γ 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 Int
-> 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 (\Int
n Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n) r a
γ -> Int
-> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe 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.
(?ops::InputOps (Rep o), PositionOps o) =>
Int
-> (Γ s o xs n r a -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Γ s o xs n r a
-> Code (ST s (Maybe a))
emitLengthCheck Int
n Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
mk (Γ 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
γ) ((Ctx s o a -> Int) -> ReaderT (Ctx s o a) Identity Int
forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks ((Int
coins Int -> Int -> Int
forall a. Num a => a -> a -> a
-) (Int -> Int) -> (Ctx s o a -> Int) -> Ctx s o a -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ctx s o a -> Int
forall s o a. Ctx s o a -> Int
liquidate)) 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