{-# LANGUAGE ImplicitParams,
MagicHash,
MultiWayIf,
PatternSynonyms,
RecordWildCards,
TypeApplications,
UnboxedTuples #-}
module Parsley.Internal.Backend.Machine.Eval (eval) where
import Data.Dependent.Map (DMap)
import Data.Functor ((<&>))
import Data.Void (Void)
import Control.Monad (forM, liftM2, liftM3)
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))
eval :: forall o a. (Trace, Ops o, ?ops :: InputOps (StaRep o), ?flags :: Opt.Flags)
=> LetBinding o a a
-> DMap MVar (LetBinding o a)
-> StaRep o
-> Code (Maybe a)
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) 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 ->
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 ->
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
$
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) =
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
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
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
γ
| 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
| 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
γ ->
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)
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
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)