{-# LANGUAGE ImplicitParams,
             MagicHash,
             MultiWayIf,
             PatternSynonyms,
             RecordWildCards,
             TypeApplications,
             UnboxedTuples #-}
{-|
Module      : Parsley.Internal.Backend.Machine.Eval
Description : Entry point for the evaluator
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

This module exports the `eval` functions used to convert a machine into code.

@since 1.0.0.0
-}
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(INPUT, LAM), 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(..), PosSelector(..))
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.PosOps             (initPos)
import Parsley.Internal.Backend.Machine.Types.Context
import Parsley.Internal.Backend.Machine.Types.Coins        (willConsume, int)
import Parsley.Internal.Backend.Machine.Types.Input        (Input(off), mkInput, forcePos, updatePos)
import Parsley.Internal.Backend.Machine.Types.State        (Γ(..), OpStack(..))
import Parsley.Internal.Common                             (Fix4, cata4, One, Code, Vec(..), Nat(..))
import Parsley.Internal.Core.CharPred                      (CharPred, lamTerm, optimisePredGiven)
import Parsley.Internal.Trace                              (Trace(trace))
import System.Console.Pretty                               (color, Color(Green))

import qualified Debug.Trace (trace)

{-|
This function performs the evaluation on the top-level let-bound parser to convert it into code.

@since 1.0.0.0
-}
eval :: forall o a. (Trace, Ops o)
     => Code (InputDependant (Rep o)) -- ^ The input as provided by the user.
     -> LetBinding o a a              -- ^ The binding to be generated.
     -> DMap MVar (LetBinding o a)    -- ^ The map of all other required bindings.
     -> Code (Maybe a)                -- ^ The code for this parser.
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 (mkInput [||offset||] initPos) (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 CharPred
p Machine s o (Char : xs) ('Succ n) r a
k)           = CharPred
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
forall s o (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (Rep o), PositionOps (Rep o), Trace) =>
CharPred
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalSat CharPred
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 (SelectPos PosSelector
sel Machine s o (Int : xs) n r a
k)   = PosSelector
-> Machine s o (Int : xs) n r a -> MachineMonad s o xs n r a
forall s o (xs :: [Type]) (n :: Nat) r a.
PosSelector
-> Machine s o (Int : xs) n r a -> MachineMonad s o xs n r a
evalSelectPos PosSelector
sel Machine s o (Int : 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)
Input 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 -> Input 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 :: Input 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
-> Input 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
-> Input 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 Input 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 :: forall s o xs n r a. (?ops :: InputOps (Rep o), PositionOps (Rep o), Trace) => CharPred -> Machine s o (Char : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
evalSat :: CharPred
-> Machine s o (Char : xs) ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
evalSat CharPred
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
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
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
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 :: 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
γ ->
      Ctx s o a
-> CharPred
-> ((Code Char -> Input o -> Code (ST s (Maybe a)))
    -> Code (ST s (Maybe a)))
-> (Code Char
    -> CharPred
    -> CharPred
    -> Input o
    -> Ctx s o a
    -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall s o a b.
Ctx s o a
-> CharPred
-> ((Code Char -> Input o -> Code b) -> Code b)
-> (Code Char
    -> CharPred -> CharPred -> Input o -> Ctx s o a -> Code b)
-> Code b
readChar Ctx s o a
ctx CharPred
p (Input o
-> (Code Char -> Input o -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall o b.
(?ops::InputOps (Rep o)) =>
Input o -> (Code Char -> Input o -> Code b) -> Code b
fetch (Γ s o xs ('Succ n) r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs ('Succ n) r a
γ)) ((Code Char
  -> CharPred
  -> CharPred
  -> Input o
  -> Ctx s o a
  -> Code (ST s (Maybe a)))
 -> Code (ST s (Maybe a)))
-> (Code Char
    -> CharPred
    -> CharPred
    -> Input o
    -> Ctx s o a
    -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall a b. (a -> b) -> a -> b
$ \Code Char
c CharPred
staOldPred CharPred
staPosPred Input o
input' Ctx s o a
ctx' ->
        let staPredC' :: CharPred
staPredC' = CharPred -> CharPred -> CharPred
optimisePredGiven CharPred
p CharPred
staOldPred
        in (Defunc Char -> Defunc Bool)
-> Code Char
-> (Defunc Char -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
-> Code (ST s (Maybe a))
forall b.
(Defunc Char -> Defunc Bool)
-> Code Char -> (Defunc Char -> 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 (Lam (Char -> Bool) -> Defunc (Char -> Bool)
forall a. Lam a -> Defunc a
LAM (CharPred -> Lam (Char -> Bool)
lamTerm CharPred
staPredC'))) Code Char
c (Machine s o (Char : xs) ('Succ n) r a
-> Γ s o xs ('Succ n) r a
-> Input o
-> Ctx s o a
-> Defunc Char
-> 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
-> Input o
-> Ctx s o a
-> Defunc x
-> Code (ST s (Maybe a))
continue Machine s o (Char : xs) ('Succ n) r a
mk Γ s o xs ('Succ n) r a
γ (Input o -> Code Char -> CharPred -> Input o
forall o. Input o -> Code Char -> CharPred -> Input o
updatePos Input o
input' Code Char
c CharPred
staPosPred) Ctx s o a
ctx')
                                                (Γ 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 :: 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
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
γ) (Input o -> Offset o
forall o. Input o -> Offset o
off (Γ s o xs ('Succ n) r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs ('Succ n) r a
γ))

    continue :: Machine s o (x : xs) n r a
-> Γ s o xs n r a
-> Input o
-> Ctx s o a
-> Defunc x
-> Code (ST s (Maybe a))
continue Machine s o (x : xs) n r a
mk Γ s o xs n r a
γ Input o
input' Ctx s o a
ctx Defunc x
v = 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 :: Input o
input = Input 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
v (Γ 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

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
-> StaYesHandler 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
-> StaYesHandler 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))) -> StaYesHandler 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))) -> StaYesHandler s o a
buildYesHandler Γ s o xs n r a
γ Γ s o xs n r a -> Code (ST s (Maybe a))
myes{- 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 (Input o -> Defunc o
forall o. Input o -> Defunc o
INPUT (Γ s o xs n r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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 (INPUT Input 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 :: Input o
input = Input 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 ->   -- This one is used for the handler's offset from point of failure
    (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 -> -- This one is used for the handler's check and loop offset
      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
-> Input 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
-> Input 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 -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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
-> Input 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
-> Input 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
buildIterYesHandler Γ 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 -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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

evalSelectPos :: PosSelector -> Machine s o (Int : xs) n r a -> MachineMonad s o xs n r a
evalSelectPos :: PosSelector
-> Machine s o (Int : xs) n r a -> MachineMonad s o xs n r a
evalSelectPos PosSelector
sel (Machine MachineMonad s o (Int : xs) n r a
k) = MachineMonad s o (Int : xs) n r a
k MachineMonad s o (Int : xs) n r a
-> ((Γ s o (Int : 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 (Int : xs) n r a -> Code (ST s (Maybe a))
m Γ s o xs n r a
γ -> Input o
-> PosSelector
-> (Code Int -> Input o -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall o r.
Input o -> PosSelector -> (Code Int -> Input o -> Code r) -> Code r
forcePos (Γ s o xs n r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs n r a
γ) PosSelector
sel ((Code Int -> Input o -> Code (ST s (Maybe a)))
 -> Code (ST s (Maybe a)))
-> (Code Int -> Input o -> Code (ST s (Maybe a)))
-> Code (ST s (Maybe a))
forall a b. (a -> b) -> a -> b
$ \Code Int
component Input o
input' ->
  Γ s o (Int : xs) n r a -> Code (ST s (Maybe a))
m (Γ s o xs n r a
γ {operands :: OpStack (Int : xs)
operands = Defunc Int -> OpStack xs -> OpStack (Int : xs)
forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs)
Op (Code Int -> Defunc Int
forall a. Code a -> Defunc a
FREEVAR Code Int
component) (Γ 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
γ), input :: Input o
input = Input o
input'})

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
γ) (Input o -> Offset o
forall o. Input o -> Offset o
off (Γ s o xs n r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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
-- No interaction with input reclamation here!
evalMeta (DrainCoins Coins
coins) (Machine MachineMonad s o xs n r a
k) =
  -- If there are enough coins left to cover the cost, no length check is required
  -- Otherwise, the full length check is required (partial doesn't work until the right offset is reached)
  (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
γ) (Input o -> Offset o
forall o. Input o -> Offset o
off (Γ s o xs ('Succ n) r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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
γ -> Input 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)) =>
Input o -> Ctx s o a -> (Ctx s o a -> Code b) -> Code b
prefetch (Γ s o xs n r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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
γ) (Input o -> Offset o
forall o. Input o -> Offset o
off (Γ s o xs ('Succ n) r a -> Input o
forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input 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 :: Input o -> Ctx s o a -> (Ctx s o a -> Code b) -> Code b
prefetch Input o
o Ctx s o a
ctx Ctx s o a -> Code b
k = Input o -> (Code Char -> Input o -> Code b) -> Code b
forall o b.
(?ops::InputOps (Rep o)) =>
Input o -> (Code Char -> Input o -> Code b) -> Code b
fetch Input o
o (\Code Char
c Input o
o' -> Ctx s o a -> Code b
k (Code Char -> Input o -> Ctx s o a -> Ctx s o a
forall o s a. Code Char -> Input o -> Ctx s o a -> Ctx s o a
addChar Code Char
c Input 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