{-# 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)
import Control.Monad.Reader                                (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           (InputOps, DynOps)
import Parsley.Internal.Backend.Machine.InputRep           (StaRep)
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, qSubroutine)
import Parsley.Internal.Backend.Machine.PosOps             (initPos)
import Parsley.Internal.Backend.Machine.Types.Context
import Parsley.Internal.Backend.Machine.Types.Coins        (Coins(knownPreds, willConsume, willCache), one, minus)
import Parsley.Internal.Backend.Machine.Types.Input        (Input(off), mkInput, forcePos, updatePos, updateOffset)
import Parsley.Internal.Backend.Machine.Types.Input.Offset (Offset(offset), unsafeDeepestKnown)
import Parsley.Internal.Backend.Machine.Types.State        (Γ(..), OpStack(..))
import Parsley.Internal.Common                             (Fix4, cata4, One, Code, Vec(..), Nat(..))
import Parsley.Internal.Core.CharPred                      (CharPred(UserPred), pattern Item, lamTerm, optimisePredGiven)
import Parsley.Internal.Trace                              (Trace(trace))
import System.Console.Pretty                               (color, Color(Green))

import qualified Debug.Trace (trace)
import qualified Parsley.Internal.Opt   as Opt
import Parsley.Internal.Opt (Flags(leadCharFactoring))

{-|
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, ?ops :: InputOps (StaRep o), ?flags :: Opt.Flags)
     => LetBinding o a a              -- ^ The binding to be generated.
     -> DMap MVar (LetBinding o a)    -- ^ The map of all other required bindings.
     -> StaRep o
     -> Code (Maybe a)                -- ^ The code for this parser.
eval :: forall o a.
(Trace, Ops o, ?ops::InputOps (StaRep o), ?flags::Flags) =>
LetBinding o a a
-> DMap MVar (LetBinding o a) -> StaRep o -> Code (Maybe a)
eval LetBinding o a a
binding DMap MVar (LetBinding o a)
fs StaRep o
offset  = forall a. Trace => String -> a -> a
trace String
"EVALUATING TOP LEVEL" [||
    runST $$(letRec fs
             nameLet
             (\μ exp rs names -> buildRec μ rs (emptyCtx names) (readyMachine exp))
             qSubroutine
             (run (readyMachine (body binding)) (Γ Empty halt (mkInput offset initPos) (VCons fatal VNil)) . nextUnique . emptyCtx))
  ||]
  where
    nameLet :: MVar x -> String
    nameLet :: forall x. MVar x -> String
nameLet (MVar IMVar
i) = String
"sub" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show IMVar
i

readyMachine :: (?ops :: InputOps (StaRep o), Ops o, Trace, ?flags :: Opt.Flags) => Fix4 (Instr o) xs n r a -> Machine s o xs n r a
readyMachine :: forall o (xs :: [Type]) (n :: Nat) r a s.
(?ops::InputOps (StaRep o), Ops o, Trace, ?flags::Flags) =>
Fix4 (Instr o) xs n r a -> Machine s o xs n r a
readyMachine = 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 (forall s o (xs :: [Type]) (n :: Nat) r a.
MachineMonad s o xs n r a -> Machine s o xs n r a
Machine forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), Ops o, ?flags::Flags) =>
Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a
alg)
  where
    alg :: (?ops :: InputOps (StaRep o), Ops o, ?flags :: Opt.Flags) => Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a
    alg :: forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), Ops o, ?flags::Flags) =>
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                 = forall o s x (xs :: [Type]) (n :: Nat) a.
(DynOps o, ?flags::Flags) =>
MachineMonad s o (x : xs) n x a
evalRet
    alg (Call MVar x
μ Machine s o (x : xs) ('Succ n1) r a
k)          = forall s o a x (xs :: [Type]) (n :: Nat) r.
(MarshalOps o, DynOps o, ?flags::Flags) =>
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 n1) r a
k
    alg (Push Defunc x
x Machine s o (x : xs) n r a
k)          = 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 xs1 n r a
k)             = 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 xs1 n r a
k
    alg (Lift2 Defunc (x -> y -> z)
f Machine s o (z : xs1) n r a
k)         = forall x y z s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
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 : xs1) n r a
k
    alg (Sat CharPred
p Machine s o (Char : xs) ('Succ n1) r a
k)           = forall s o (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, Trace, ?flags::Flags) =>
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 n1) r a
k
    alg Instr o (Machine s o) xs n r a
Empt                = forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
MachineMonad s o xs ('Succ n) r a
evalEmpt
    alg (Commit Machine s o xs n1 r a
k)          = 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 n1 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)         = forall o s (xs :: [Type]) (n :: Nat) r a.
(PositionOps (StaRep o), HandlerOps o, DynOps 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)            = 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 xs1 n r a
k)            = 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 xs1 n r a
k
    alg (Case Machine s o (x : xs1) n r a
p Machine s o (y : xs1) n r a
q)          = forall s o x (xs :: [Type]) (n :: Nat) r a y.
(?flags::Flags) =>
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 : xs1) n r a
p Machine s o (y : xs1) n r a
q
    alg (Choices [Defunc (x -> Bool)]
fs [Machine s o xs1 n r a]
ks Machine s o xs1 n r a
def) = forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
[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 xs1 n r a]
ks Machine s o xs1 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)        = forall o s a (xs :: [Type]) (n :: Nat) r.
(RecBuilder o, PositionOps (StaRep o), HandlerOps o, DynOps 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
φ)            = forall o x s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Φ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)      = forall o x s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags, 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 : xs1) n r a
k)            = 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 : xs1) n r a
k
    alg (Dup Machine s o (x : x : xs1) n r a
k)             = forall s o x (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
evalDup Machine s o (x : x : xs1) n r a
k
    alg (Make ΣVar x
σ Access
c Machine s o xs1 n r a
k)        = forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 xs1 n r a
k
    alg (Get ΣVar x
σ Access
c Machine s o (x : xs) n r a
k)         = forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 xs1 n r a
k)         = forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 xs1 n r a
k
    alg (SelectPos PosSelector
sel Machine s o (Int : xs) n r a
k)   = forall s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
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 n1)) r a
k)   = forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), LogHandler o, HandlerOps o,
 ?flags::Flags) =>
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 n1)) r a
k
    alg (LogExit String
name Machine s o xs n r a
k)    = forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), PositionOps (StaRep o),
 LogOps (StaRep o), DynOps 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)     = forall o (n :: Nat) s (xs :: [Type]) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
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 :: (DynOps o, ?flags :: Opt.Flags) => MachineMonad s o (x : xs) n x a
evalRet :: forall o s x (xs :: [Type]) (n :: Nat) a.
(DynOps o, ?flags::Flags) =>
MachineMonad s o (x : xs) n x a
evalRet = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> StaCont s o a r
retCont forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall o s a x (xs :: [Type]) (n :: Nat) r.
(DynOps o, ?flags::Flags) =>
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, DynOps o, ?flags :: Opt.Flags) => MVar x -> Machine s o (x : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
evalCall :: forall s o a x (xs :: [Type]) (n :: Nat) r.
(MarshalOps o, DynOps o, ?flags::Flags) =>
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) = forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique forall a b. (a -> b) -> a -> b
$ \Word
u -> forall (m :: Type -> Type) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (forall s o (xs :: [Type]) (n :: Nat) r a x.
(MarshalOps o, DynOps o, ?flags::Flags) =>
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) (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

evalPush :: Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalPush :: 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 MachineMonad s o (x : xs) n r a
k) = MachineMonad s o (x : xs) n r a
k 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 = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
x (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 :: 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 MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k 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
OpStack xs1
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 :: (?flags :: Opt.Flags) => Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a
evalLift2 :: forall x y z s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
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 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 y
Defunc x
y (Op Defunc x
Defunc x
x OpStack xs
OpStack xs1
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 forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op (forall a b c.
(?flags::Flags) =>
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 (StaRep o), DynOps o, Trace, ?flags :: Opt.Flags) => CharPred -> Machine s o (Char : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a
evalSat :: forall s o (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, Trace, ?flags::Flags) =>
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
mk = do
  Bool
bankrupt <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks forall s o a. Ctx s o a -> Bool
isBankrupt
  Bool
hasChange <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks forall s o a. Ctx s o a -> Bool
hasCoin
  if | Bool
bankrupt -> forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
Coins
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
withLengthCheckAndCoins (CharPred -> Coins
one CharPred
p) MachineMonad s o xs ('Succ n) r a
satFetch
     | Bool
hasChange -> MachineMonad s o xs ('Succ n) r a
satFetch
     | Bool
otherwise -> forall a. Trace => String -> a -> a
trace String
"I have a piggy :)" forall a b. (a -> b) -> a -> b
$ forall r a b. (r -> (a, r)) -> (a -> Reader r b) -> Reader r b
state forall s o a. Ctx s o a -> (Coins, Ctx s o a)
breakPiggy forall a b. (a -> b) -> a -> b
$ \Coins
coins -> forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
Coins
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
withLengthCheckAndCoins Coins
coins MachineMonad s o xs ('Succ n) r a
satFetch
  where
    satFetch :: MachineMonad s o xs (Succ n) r a
    satFetch :: MachineMonad s o xs ('Succ n) r a
satFetch = forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs ('Succ n) r a
γ ->
      forall s o a b.
Ctx s o a
-> CharPred
-> ((Code Char -> Offset o -> Code b) -> Code b)
-> (Code Char
    -> CharPred -> CharPred -> Offset o -> Ctx s o a -> Code b)
-> Code b
readChar (forall s o a. Ctx s o a -> Ctx s o a
spendCoin Ctx s o a
ctx) CharPred
p (forall o b.
(?ops::InputOps (StaRep o)) =>
Offset o -> (Code Char -> Offset o -> Code b) -> Code b
fetch (forall o. Input o -> Offset o
off (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
γ))) forall a b. (a -> b) -> a -> b
$ \Code Char
c CharPred
staOldPred CharPred
staPosPred Offset o
offset' Ctx s o a
ctx' ->
        let staPredC' :: CharPred
staPredC' = CharPred -> CharPred -> CharPred
optimisePredGiven CharPred
p CharPred
staOldPred
        in forall b.
(?flags::Flags) =>
(Defunc Char -> Defunc Bool)
-> Code Char -> (Defunc Char -> Code b) -> Code b -> Code b
sat (forall a b.
(?flags::Flags) =>
Defunc (a -> b) -> Defunc a -> Defunc b
ap (forall a. Lam a -> Defunc a
LAM (CharPred -> Lam (Char -> Bool)
lamTerm CharPred
staPredC'))) Code Char
c (forall {s} {o} {x} {xs1 :: [Type]} {n :: Nat} {r} {a}.
Machine s o (x : xs1) n r a
-> Γ s o xs1 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
γ (forall o. Input o -> Code Char -> CharPred -> Input o
updatePos (forall o. Offset o -> Input o -> Input o
updateOffset Offset o
offset' (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
c CharPred
staPosPred) Ctx s o a
ctx')
                                                (forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ)

    continue :: Machine s o (x : xs1) n r a
-> Γ s o xs1 n r a
-> Input o
-> Ctx s o a
-> Defunc x
-> Code (ST s (Maybe a))
continue Machine s o (x : xs1) n r a
mk Γ s o xs1 n r a
γ Input o
input' Ctx s o a
ctx Defunc x
v = 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 : xs1) n r a
mk (Γ s o xs1 n r a
γ {input :: Input o
input = Input o
input', operands :: OpStack (x : xs1)
operands = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
v (forall s o (xs :: [Type]) (n :: Nat) r a.
Γ s o xs n r a -> OpStack xs
operands Γ s o xs1 n r a
γ)}) Ctx s o a
ctx

evalEmpt :: (DynOps o, ?flags :: Opt.Flags) => MachineMonad s o xs (Succ n) r a
evalEmpt :: forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
MachineMonad s o xs ('Succ n) r a
evalEmpt = forall (m :: Type -> Type) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$! forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ 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 :: 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 MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k 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)
Vec n1 (AugmentedStaHandler s o a)
hs = 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 (StaRep o), HandlerOps o, DynOps 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 :: forall o s (xs :: [Type]) (n :: Nat) r a.
(PositionOps (StaRep o), HandlerOps o, DynOps 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 MachineMonad s o xs ('Succ n) r a
k) Handler o (Machine s o) (o : xs) n r a
h = forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique 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 : xs1) n r a
h) ->
    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
γ -> 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 (forall o s (xs :: [Type]) (n :: Nat) r a.
DynOps o =>
Γ 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 MachineMonad s o (o : xs1) n r a
h
  Same Bool
gyes (Machine MachineMonad s o xs1 n r a
yes) Bool
gno (Machine MachineMonad s o (o : xs1) n r a
no) ->
    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
γ -> forall s o (xs :: [Type]) (n :: Nat) r a b.
(HandlerOps o, PositionOps (StaRep o), DynOps 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 (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 (forall o s (xs :: [Type]) (n :: Nat) r a.
DynOps o =>
Γ 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 xs1 n r a
yes MachineMonad s o (o : xs1) n r a
no

evalTell :: Machine s o (o : xs) n r a -> MachineMonad s o xs n r a
evalTell :: 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 MachineMonad s o (o : xs) n r a
k) = MachineMonad s o (o : xs) n r a
k 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 = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op (forall a. Input a -> Defunc a
INPUT (forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs n r a
γ)) (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 :: 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 MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k 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 o
Input x
input) OpStack xs
OpStack xs1
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 :: (?flags :: Opt.Flags) => 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 :: forall s o x (xs :: [Type]) (n :: Nat) r a y.
(?flags::Flags) =>
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) = 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 -> Code Q (ST s (Maybe a))
mp Γ s o (y : xs) n r a -> Code Q (ST s (Maybe a))
mq Γ s o (Either x y : xs) n r a
γ ->
  let Op Defunc x
Defunc (Either x y)
e OpStack xs
OpStack xs1
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 :: (?flags :: Opt.Flags) => [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 :: forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
[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) = 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
Defunc x
x OpStack xs
OpStack xs1
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 forall {a} {t} {a}.
(?flags::Flags) =>
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
  (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 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
γ = forall a.
(?flags::Flags) =>
Defunc Bool -> Code a -> Code a -> Code a
_if (forall a b.
(?flags::Flags) =>
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 (StaRep o), HandlerOps o, DynOps 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 :: forall o s a (xs :: [Type]) (n :: Nat) r.
(RecBuilder o, PositionOps (StaRep o), HandlerOps o, DynOps 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
h =
  forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique forall a b. (a -> b) -> a -> b
$ \Word
u1 ->   -- This one is used for the handler's offset from point of failure
    forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique forall a b. (a -> b) -> a -> b
$ \Word
u2 -> -- This one is used for the handler's check and loop offset
      forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local forall s o a. Ctx s o a -> Ctx s o a
voidCoins forall a b. (a -> b) -> a -> b
$  -- We must not allow factored input to pass through to iterative handlers, they have rolling inputs
        case Handler o (Machine s o) (o : xs) n r a
h of
          Always Bool
gh (Machine MachineMonad s o (o : xs1) n r a
h) ->
            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
γ -> forall s o a.
(RecBuilder o, DynOps 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 (forall o s (xs :: [Type]) (n :: Nat) r a.
DynOps o =>
Γ 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) (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 : xs1) n r a
h forall r (m :: Type -> Type). MonadReader r m => m r
ask
          Same Bool
gyes (Machine MachineMonad s o xs1 n r a
yes) Bool
gno (Machine MachineMonad s o (o : xs1) n r a
no) ->
            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
γ -> forall s o a.
(RecBuilder o, HandlerOps o, PositionOps (StaRep o), DynOps 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 (forall o s (xs :: [Type]) (n :: Nat) r a.
DynOps o =>
Γ 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 (forall o s (xs :: [Type]) (n :: Nat) r a.
DynOps o =>
Γ 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) (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 xs1 n r a
yes MachineMonad s o (o : xs1) n r a
no forall r (m :: Type -> Type). MonadReader r m => m r
ask

evalJoin :: (DynOps o, ?flags :: Opt.Flags) => ΦVar x -> MachineMonad s o (x : xs) n r a
evalJoin :: forall o x s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
ΦVar x -> MachineMonad s o (x : xs) n r a
evalJoin ΦVar 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
φ forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> forall o s a x (xs :: [Type]) (n :: Nat) r.
(DynOps o, ?flags::Flags) =>
StaCont s o a x -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))
resume

evalMkJoin :: (DynOps o, ?flags :: Opt.Flags) => 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 :: forall o x s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags, 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 = forall s o (xs :: [Type]) (n :: Nat) r a x.
(JoinBuilder o, DynOps o, ?flags::Flags) =>
Φ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 :: 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 MachineMonad s o (x : y : xs) n r a
k) = MachineMonad s o (x : y : xs) n r a
k 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 y
Defunc x
y (Op Defunc x
Defunc x
x OpStack xs
OpStack xs1
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 forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
x (forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc y
y OpStack xs
xs)})

evalDup :: (?flags :: Opt.Flags) => Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a
evalDup :: forall s o x (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
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 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
Defunc x
x OpStack xs
OpStack xs1
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 forall x r.
(?flags::Flags) =>
Defunc x -> (Defunc x -> Code r) -> Code r
dup Defunc x
x 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 = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
dupx (forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
dupx OpStack xs
xs)})

evalMake :: (?flags :: Opt.Flags) => ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalMake :: forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 = forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o (x : xs) n r a
γ ->
  let Op Defunc x
Defunc x
x OpStack xs
OpStack xs1
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 forall x s o a r.
(?flags::Flags) =>
Σ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 (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 :: (?flags :: Opt.Flags) => ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a
evalGet :: forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 = forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs n r a
γ -> forall x s o a r.
(?flags::Flags) =>
Σ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 -> 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 = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op Defunc x
x (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 :: (?flags :: Opt.Flags) => ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a
evalPut :: forall x s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
Σ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 = forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o (x : xs) n r a
γ ->
  let Op Defunc x
Defunc x
x OpStack xs
OpStack xs1
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 forall x s o a r.
(?flags::Flags) =>
Σ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 (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 :: (?flags :: Opt.Flags) => PosSelector -> Machine s o (Int : xs) n r a -> MachineMonad s o xs n r a
evalSelectPos :: forall s o (xs :: [Type]) (n :: Nat) r a.
(?flags::Flags) =>
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 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
γ -> forall o r.
Input o -> PosSelector -> (Code Int -> Input o -> Code r) -> Code r
forcePos (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 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 = forall x (xs1 :: [Type]).
Defunc x -> OpStack xs1 -> OpStack (x : xs1)
Op (forall a. (?flags::Flags) => Code a -> Defunc a
FREEVAR Code Int
component) (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 (StaRep o), LogHandler o, HandlerOps o, ?flags :: Opt.Flags)
             => String -> Machine s o xs (Succ (Succ n)) r a -> MachineMonad s o xs (Succ n) r a
evalLogEnter :: forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), LogHandler o, HandlerOps o,
 ?flags::Flags) =>
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) = forall s o a (m :: Type -> Type) b.
MonadReader (Ctx s o a) m =>
(Word -> m b) -> m b
freshUnique forall a b. (a -> b) -> a -> b
$ \Word
u ->
  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)||])
    (forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local forall s o a. Ctx s o a -> Ctx s o a
debugUp MachineMonad s o xs ('Succ ('Succ n)) r a
mk)
    forall r (m :: Type -> Type). MonadReader r m => m r
ask

evalLogExit :: (?ops :: InputOps (StaRep o), PositionOps (StaRep o), LogOps (StaRep o), DynOps o) => String -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalLogExit :: forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), PositionOps (StaRep o),
 LogOps (StaRep o), DynOps o) =>
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) =
  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 Q (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 γ) ||])
    (forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local forall s o a. Ctx s o a -> Ctx s o a
debugDown MachineMonad s o xs n r a
mk)
    forall r (m :: Type -> Type). MonadReader r m => m r
ask

evalMeta :: (?ops :: InputOps (StaRep o), DynOps o, ?flags :: Opt.Flags) => MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMeta :: forall o (n :: Nat) s (xs :: [Type]) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a
evalMeta MetaInstr n
_ (Machine MachineMonad s o xs n r a
k) | Bool -> Bool
not (Flags -> Bool
Opt.lengthCheckFactoring ?flags::Flags
?flags) = MachineMonad s o xs n r a
k
evalMeta (AddCoins Coins
coins) (Machine MachineMonad s o xs n r a
k) =
  -- when there are coins available, this cannot be discharged, and will wait until the current amounts
  -- are exhausted. Because it might have been the case that lookahead was performed to refund, the
  -- over-imbursement cannot be done in advance, and is instead done here, deducting the net-worth
  -- of the coin count to ensure that only enough to make up the change is put in the piggy-banks
  do Int
net <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks forall s o a. Ctx s o a -> Int
netWorth
     let requiresPiggy :: Bool
requiresPiggy = Int
net forall a. Eq a => a -> a -> Bool
/= Int
0
     if Bool
requiresPiggy then forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (forall s o a. Coins -> Ctx s o a -> Ctx s o a
storePiggy (Coins
coins Coins -> Int -> Coins
`minus` Int
net)) MachineMonad s o xs n r a
k
     else forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
Coins
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
withLengthCheckAndCoins Coins
coins MachineMonad s o xs n r a
k
evalMeta (RefundCoins Int
coins) (Machine MachineMonad s o xs n r a
k)
  | Flags -> Bool
Opt.reclaimInput ?flags::Flags
?flags = forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (forall s o a. Int -> Ctx s o a -> Ctx s o a
refundCoins Int
coins) MachineMonad s o xs n r a
k
  | Bool
otherwise               = forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (forall s o a. Int -> Ctx s o a -> Ctx s o a
giveCoins Int
coins) MachineMonad s o xs n r a
k
-- No interaction with input reclamation here!
evalMeta (DrainCoins Int
coins) (Machine MachineMonad s o xs n r a
k) =
  forall (m :: Type -> Type) a1 a2 a3 r.
Monad m =>
(a1 -> a2 -> a3 -> r) -> m a1 -> m a2 -> m a3 -> m r
liftM3 Bool
-> Maybe Int
-> (Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n1) r a
-> Code (ST s (Maybe a))
drain
         (forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks forall s o a. Ctx s o a -> Bool
isBankrupt)
         (forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks (forall s o a. Int -> Ctx s o a -> Maybe Int
canAfford Int
coins))
         MachineMonad s o xs n r a
k
  where
    -- there are enough coins to pay in full
    drain :: Bool
-> Maybe Int
-> (Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a)))
-> Γ s o xs ('Succ n1) r a
-> Code (ST s (Maybe a))
drain Bool
_ Maybe Int
Nothing Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n1) r a
γ = Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n1) r a
γ
    drain Bool
bankrupt ~(Just Int
m) Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n1) r a
γ
      -- full length check required
      | Bool
bankrupt = forall o a.
(?ops::InputOps (StaRep o)) =>
Int
-> Int
-> Maybe (Code Char -> Code a -> Code a)
-> (Offset o -> [(Code Char, Offset o)] -> Code a)
-> Code a
-> Offset o
-> (Offset o -> StaRep o)
-> Code a
emitLengthCheck Int
coins Int
0 forall a. Maybe a
Nothing (\Offset o
off [(Code Char, Offset o)]
_ -> forall s o (xs :: [Type]) (n :: Nat) r a t.
(Γ s o xs n r a -> t) -> Γ s o xs n r a -> Offset o -> t
withUpdatedOffset Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n1) r a
γ Offset o
off) (forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n1) r a
γ) (forall o. Input o -> Offset o
off (forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs ('Succ n1) r a
γ)) forall o. Offset o -> StaRep o
offset
      -- can be partially paid from last known deepest offset
      | Bool
otherwise = forall o a.
(?ops::InputOps (StaRep o)) =>
Int
-> Int
-> Maybe (Code Char -> Code a -> Code a)
-> (Offset o -> [(Code Char, Offset o)] -> Code a)
-> Code a
-> Offset o
-> (Offset o -> StaRep o)
-> Code a
emitLengthCheck (Int
m forall a. Num a => a -> a -> a
+ Int
1) Int
0 forall a. Maybe a
Nothing (\Offset o
off [(Code Char, Offset o)]
_ -> forall s o (xs :: [Type]) (n :: Nat) r a t.
(Γ s o xs n r a -> t) -> Γ s o xs n r a -> Offset o -> t
withUpdatedOffset Γ s o xs ('Succ n1) r a -> Code (ST s (Maybe a))
mk Γ s o xs ('Succ n1) r a
γ Offset o
off) (forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n1) r a
γ) (forall o. Input o -> Offset o
off (forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs ('Succ n1) r a
γ)) forall o. Offset o -> StaRep o
unsafeDeepestKnown
evalMeta (GiveBursary Int
coins) (Machine MachineMonad s o xs n r a
k) = forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (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 BlockCoins{} (Machine MachineMonad s o xs n r a
k) = MachineMonad s o xs n r a
k

withUpdatedOffset :: (Γ s o xs n r a -> t) -> Γ s o xs n r a -> Offset o -> t
withUpdatedOffset :: forall s o (xs :: [Type]) (n :: Nat) r a t.
(Γ s o xs n r a -> t) -> Γ s o xs n r a -> Offset o -> t
withUpdatedOffset Γ s o xs n r a -> t
k Γ s o xs n r a
γ Offset o
off = Γ s o xs n r a -> t
k (Γ s o xs n r a
γ { input :: Input o
input = forall o. Offset o -> Input o -> Input o
updateOffset Offset o
off (forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Input o
input Γ s o xs n r a
γ)})

withLengthCheckAndCoins :: (?ops::InputOps (StaRep o), DynOps o, ?flags :: Opt.Flags) => Coins -> MachineMonad s o xs (Succ n) r a -> MachineMonad s o xs (Succ n) r a
withLengthCheckAndCoins :: forall o s (xs :: [Type]) (n :: Nat) r a.
(?ops::InputOps (StaRep o), DynOps o, ?flags::Flags) =>
Coins
-> MachineMonad s o xs ('Succ n) r a
-> MachineMonad s o xs ('Succ n) r a
withLengthCheckAndCoins Coins
coins MachineMonad s o xs ('Succ n) r a
k = forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
reader forall a b. (a -> b) -> a -> b
$ \Ctx s o a
ctx Γ s o xs ('Succ n) r a
γ ->
    -- it seems like _specific_ prefetching must not move out of the scope of a handler that rolls back (like try)
    -- It does work, however, if exactly one character is considered (see take 1 below) and then n-1 Items, which cannot fail
    let prefetch :: ((Code Char, Offset o), CharPred)
-> (Ctx s o a -> c) -> Ctx s o a -> c
prefetch ((Code Char
c, Offset o
offset'), CharPred
pred) Ctx s o a -> c
k = Ctx s o a -> c
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o s a.
CharPred -> Code Char -> Offset o -> Ctx s o a -> Ctx s o a
addChar CharPred
pred Code Char
c Offset o
offset'
        remainder :: Offset o -> Ctx s o a -> Code (ST s (Maybe a))
remainder Offset o
deepest Ctx s o a
ctx = forall s o (xs :: [Type]) (n :: Nat) r a t.
(Γ s o xs n r a -> t) -> Γ s o xs n r a -> Offset o -> t
withUpdatedOffset (forall a b c. (a -> b -> c) -> b -> a -> c
flip (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 (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 xs ('Succ n) r a
k)) (forall s o a. Int -> Ctx s o a -> Ctx s o a
giveCoins (Coins -> Int
willConsume Coins
coins) Ctx s o a
ctx)) Γ s o xs ('Succ n) r a
γ Offset o
deepest
        staPred :: Maybe CharPred
staPred = Coins -> Maybe CharPred
knownPreds Coins
coins forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= (?flags::Flags) => CharPred -> Maybe CharPred
onlyStatic
        preds :: [CharPred]
preds = forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. a -> a
id (:) Maybe CharPred
staPred (forall a. a -> [a]
repeat CharPred
Item) -- these are fed in to ensure the right checked pred is accounted for
        headCheck :: Maybe (Code Char -> Code (ST s (Maybe a)) -> Code (ST s (Maybe a)))
headCheck = Maybe CharPred
staPred forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> \CharPred
pred Code Char
c Code (ST s (Maybe a))
good -> forall b.
(?flags::Flags) =>
(Defunc Char -> Defunc Bool)
-> Code Char -> (Defunc Char -> Code b) -> Code b -> Code b
sat (forall a b.
(?flags::Flags) =>
Defunc (a -> b) -> Defunc a -> Defunc b
ap (forall a. Lam a -> Defunc a
LAM (CharPred -> Lam (Char -> Bool)
lamTerm CharPred
pred))) Code Char
c (forall a b. a -> b -> a
const Code (ST s (Maybe a))
good) (forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ)
        good :: Offset o -> [(Code Char, Offset o)] -> Code (ST s (Maybe a))
good Offset o
deepest [(Code Char, Offset o)]
cached = forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr forall {o} {s} {a} {c}.
((Code Char, Offset o), CharPred)
-> (Ctx s o a -> c) -> Ctx s o a -> c
prefetch (Offset o -> Ctx s o a -> Code (ST s (Maybe a))
remainder Offset o
deepest) (forall a b. [a] -> [b] -> [(a, b)]
zip [(Code Char, Offset o)]
cached [CharPred]
preds) Ctx s o a
ctx
    in forall o a.
(?ops::InputOps (StaRep o)) =>
Int
-> Int
-> Maybe (Code Char -> Code a -> Code a)
-> (Offset o -> [(Code Char, Offset o)] -> Code a)
-> Code a
-> Offset o
-> (Offset o -> StaRep o)
-> Code a
emitLengthCheck (Coins -> Int
willConsume Coins
coins) (Coins -> Int
willCache Coins
coins) Maybe (Code Char -> Code (ST s (Maybe a)) -> Code (ST s (Maybe a)))
headCheck Offset o -> [(Code Char, Offset o)] -> Code (ST s (Maybe a))
good (forall o s (xs :: [Type]) (n :: Nat) r a.
(DynOps o, ?flags::Flags) =>
Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))
raise Γ s o xs ('Succ n) r a
γ) (forall o. Input o -> Offset o
off (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
γ)) forall o. Offset o -> StaRep o
offset
        -- this is needed because a cached predicate cannot be compared for equality if it's user-pred, and it'll duplicate!
  where onlyStatic :: CharPred -> Maybe CharPred
onlyStatic UserPred{}                   = forall a. Maybe a
Nothing
        onlyStatic CharPred
p | Flags -> Bool
leadCharFactoring ?flags::Flags
?flags = forall a. a -> Maybe a
Just CharPred
p
        onlyStatic CharPred
_                            = forall a. Maybe a
Nothing

state :: (r -> (a, r)) -> (a -> Reader r b) -> Reader r b
state :: forall r a b. (r -> (a, r)) -> (a -> Reader r b) -> Reader r b
state r -> (a, r)
f a -> Reader r b
k = do
  (a
x, r
r) <- forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a
asks r -> (a, r)
f
  forall r (m :: Type -> Type) a.
MonadReader r m =>
(r -> r) -> m a -> m a
local (forall a b. a -> b -> a
const r
r) (a -> Reader r b
k a
x)