{-# LANGUAGE ImplicitParams, MultiWayIf, RecordWildCards, TypeApplications, UnboxedTuples #-} module Parsley.Internal.Backend.Machine.Eval (eval) where import Data.Dependent.Map (DMap) import Data.Functor ((<&>)) import Data.Void (Void) import Control.Monad (forM, liftM2) import Control.Monad.Reader (ask, asks, local) import Control.Monad.ST (runST) import Parsley.Internal.Backend.Machine.Defunc (Defunc(FREEVAR, OFFSET), genDefunc, genDefunc1, ap2) import Parsley.Internal.Backend.Machine.Identifiers (MVar(..), ΦVar, ΣVar) import Parsley.Internal.Backend.Machine.InputOps (InputDependant, PositionOps, LogOps, InputOps(InputOps)) import Parsley.Internal.Backend.Machine.InputRep (Rep) import Parsley.Internal.Backend.Machine.Instructions (Instr(..), MetaInstr(..), Access(..)) import Parsley.Internal.Backend.Machine.LetBindings (LetBinding(..)) import Parsley.Internal.Backend.Machine.LetRecBuilder import Parsley.Internal.Backend.Machine.Ops import Parsley.Internal.Backend.Machine.State import Parsley.Internal.Common (Fix4, cata4, One, Code, Vec(..), Nat(..)) import Parsley.Internal.Trace (Trace(trace)) import System.Console.Pretty (color, Color(Green)) import qualified Debug.Trace (trace) eval :: forall o a. (Trace, Ops o) => Code (InputDependant (Rep o)) -> LetBinding o a a -> DMap MVar (LetBinding o a) -> Code (Maybe a) eval :: Code (InputDependant (Rep o)) -> LetBinding o a a -> DMap MVar (LetBinding o a) -> Code (Maybe a) eval Code (InputDependant (Rep o)) input (LetBinding !Binding o a a p Regs rs _) DMap MVar (LetBinding o a) fs = String -> Code (Maybe a) -> Code (Maybe a) forall a. Trace => String -> a -> a trace (String "EVALUATING TOP LEVEL") [|| runST $ do let (# next, more, offset #) = $$input $$(let ?ops = InputOps [||more||] [||next||] in letRec fs nameLet (\exp rs names -> buildRec rs (emptyCtx names) (readyMachine exp)) (\names -> run (readyMachine p) (Γ Empty (halt @o) [||offset||] (VCons (fatal @o) VNil)) (emptyCtx names))) ||] where nameLet :: MVar x -> String nameLet :: MVar x -> String nameLet (MVar IMVar i) = String "sub" String -> String -> String forall a. [a] -> [a] -> [a] ++ IMVar -> String forall a. Show a => a -> String show IMVar i readyMachine :: (?ops :: InputOps (Rep o), Ops o, Trace) => Fix4 (Instr o) xs n r a -> Machine s o xs n r a readyMachine :: Fix4 (Instr o) xs n r a -> Machine s o xs n r a readyMachine = (forall (i' :: [Type]) (j' :: Nat) k'. Instr o (Machine s o) i' j' k' a -> Machine s o i' j' k' a) -> Fix4 (Instr o) xs n r a -> Machine s o xs n r a forall (f :: ([Type] -> Nat -> Type -> Type -> Type) -> [Type] -> Nat -> Type -> Type -> Type) (a :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type]) (j :: Nat) k x. IFunctor4 f => (forall (i' :: [Type]) (j' :: Nat) k'. f a i' j' k' x -> a i' j' k' x) -> Fix4 f i j k x -> a i j k x cata4 (MachineMonad s o i' j' k' a -> Machine s o i' j' k' a forall s o (xs :: [Type]) (n :: Nat) r a. MachineMonad s o xs n r a -> Machine s o xs n r a Machine (MachineMonad s o i' j' k' a -> Machine s o i' j' k' a) -> (Instr o (Machine s o) i' j' k' a -> MachineMonad s o i' j' k' a) -> Instr o (Machine s o) i' j' k' a -> Machine s o i' j' k' a forall b c a. (b -> c) -> (a -> b) -> a -> c . Instr o (Machine s o) i' j' k' a -> MachineMonad s o i' j' k' a forall o s (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), Ops o) => Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a alg) where alg :: (?ops :: InputOps (Rep o), Ops o) => Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a alg :: Instr o (Machine s o) xs n r a -> MachineMonad s o xs n r a alg Instr o (Machine s o) xs n r a Ret = MachineMonad s o xs n r a forall s o x (xs :: [Type]) (n :: Nat) a. MachineMonad s o (x : xs) n x a evalRet alg (Call MVar x μ Machine s o (x : xs) ('Succ n) r a k) = MVar x -> Machine s o (x : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall s o a x (xs :: [Type]) (n :: Nat) r. ContOps o => MVar x -> Machine s o (x : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a evalCall MVar x μ Machine s o (x : xs) ('Succ n) r a k alg (Jump MVar r μ) = MVar r -> MachineMonad s o '[] ('Succ n) r a forall s o a x (n :: Nat). MVar x -> MachineMonad s o '[] ('Succ n) x a evalJump MVar r μ alg (Push Defunc x x Machine s o (x : xs) n r a k) = Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a forall x s o (xs :: [Type]) (n :: Nat) r a. Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalPush Defunc x x Machine s o (x : xs) n r a k alg (Pop Machine s o xs n r a k) = Machine s o xs n r a -> MachineMonad s o (x : xs) n r a forall s o (xs :: [Type]) (n :: Nat) r a x. Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPop Machine s o xs n r a k alg (Lift2 Defunc (x -> y -> z) f Machine s o (z : xs) n r a k) = Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a forall x y z s o (xs :: [Type]) (n :: Nat) r a. Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalLift2 Defunc (x -> y -> z) f Machine s o (z : xs) n r a k alg (Sat Defunc (Char -> Bool) p Machine s o (Char : xs) ('Succ n) r a k) = Defunc (Char -> Bool) -> Machine s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall o s (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), PositionOps o, Trace) => Defunc (Char -> Bool) -> Machine s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a evalSat Defunc (Char -> Bool) p Machine s o (Char : xs) ('Succ n) r a k alg Instr o (Machine s o) xs n r a Empt = MachineMonad s o xs n r a forall s o (xs :: [Type]) (n :: Nat) r a. MachineMonad s o xs ('Succ n) r a evalEmpt alg (Commit Machine s o xs n r a k) = Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a evalCommit Machine s o xs n r a k alg (Catch Machine s o xs ('Succ n) r a k Machine s o (o : xs) n r a h) = Machine s o xs ('Succ n) r a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a forall o s (xs :: [Type]) (n :: Nat) r a. HandlerOps o => Machine s o xs ('Succ n) r a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalCatch Machine s o xs ('Succ n) r a k Machine s o (o : xs) n r a Machine s o (o : xs) n r a h alg (Tell Machine s o (o : xs) n r a k) = Machine s o (o : xs) n r a -> MachineMonad s o xs n r a forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalTell Machine s o (o : xs) n r a Machine s o (o : xs) n r a k alg (Seek Machine s o xs n r a k) = Machine s o xs n r a -> MachineMonad s o (o : xs) n r a forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> MachineMonad s o (o : xs) n r a evalSeek Machine s o xs n r a k alg (Case Machine s o (x : xs) n r a p Machine s o (y : xs) n r a q) = Machine s o (x : xs) n r a -> Machine s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a forall s o x (xs :: [Type]) (n :: Nat) r a y. Machine s o (x : xs) n r a -> Machine s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a evalCase Machine s o (x : xs) n r a p Machine s o (y : xs) n r a q alg (Choices [Defunc (x -> Bool)] fs [Machine s o xs n r a] ks Machine s o xs n r a def) = [Defunc (x -> Bool)] -> [Machine s o xs n r a] -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a forall x s o (xs :: [Type]) (n :: Nat) r a. [Defunc (x -> Bool)] -> [Machine s o xs n r a] -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalChoices [Defunc (x -> Bool)] fs [Machine s o xs n r a] ks Machine s o xs n r a def alg (Iter MVar Void μ Machine s o '[] One Void a l Machine s o (o : xs) n r a k) = MVar Void -> Machine s o '[] One Void a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a forall o s a (xs :: [Type]) (n :: Nat) r. (RecBuilder o, ReturnOps o, HandlerOps o) => MVar Void -> Machine s o '[] One Void a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalIter MVar Void μ Machine s o '[] One Void a l Machine s o (o : xs) n r a Machine s o (o : xs) n r a k alg (Join ΦVar x φ) = ΦVar x -> MachineMonad s o (x : xs) n r a forall x s o (xs :: [Type]) (n :: Nat) r a. ΦVar x -> MachineMonad s o (x : xs) n r a evalJoin ΦVar x φ alg (MkJoin ΦVar x φ Machine s o (x : xs) n r a p Machine s o xs n r a k) = ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a forall o x s (xs :: [Type]) (n :: Nat) r a. JoinBuilder o => ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMkJoin ΦVar x φ Machine s o (x : xs) n r a p Machine s o xs n r a k alg (Swap Machine s o (x : y : xs) n r a k) = Machine s o (x : y : xs) n r a -> MachineMonad s o (y : x : xs) n r a forall s o x y (xs :: [Type]) (n :: Nat) r a. Machine s o (x : y : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalSwap Machine s o (x : y : xs) n r a k alg (Dup Machine s o (x : x : xs) n r a k) = Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a forall s o x (xs :: [Type]) (n :: Nat) r a. Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a evalDup Machine s o (x : x : xs) n r a k alg (Make ΣVar x σ Access c Machine s o xs n r a k) = ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a forall x s o (xs :: [Type]) (n :: Nat) r a. ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalMake ΣVar x σ Access c Machine s o xs n r a k alg (Get ΣVar x σ Access c Machine s o (x : xs) n r a k) = ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a forall x s o (xs :: [Type]) (n :: Nat) r a. ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalGet ΣVar x σ Access c Machine s o (x : xs) n r a k alg (Put ΣVar x σ Access c Machine s o xs n r a k) = ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a forall x s o (xs :: [Type]) (n :: Nat) r a. ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPut ΣVar x σ Access c Machine s o xs n r a k alg (LogEnter String name Machine s o xs ('Succ ('Succ n)) r a k) = String -> Machine s o xs ('Succ ('Succ n)) r a -> MachineMonad s o xs ('Succ n) r a forall o s (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), LogHandler o) => String -> Machine s o xs ('Succ ('Succ n)) r a -> MachineMonad s o xs ('Succ n) r a evalLogEnter String name Machine s o xs ('Succ ('Succ n)) r a k alg (LogExit String name Machine s o xs n r a k) = String -> Machine s o xs n r a -> MachineMonad s o xs n r a forall o s (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), PositionOps o, LogOps (Rep o)) => String -> Machine s o xs n r a -> MachineMonad s o xs n r a evalLogExit String name Machine s o xs n r a k alg (MetaInstr MetaInstr n m Machine s o xs n r a k) = MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a forall o (n :: Nat) s (xs :: [Type]) r a. (?ops::InputOps (Rep o), PositionOps o) => MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMeta MetaInstr n m Machine s o xs n r a k evalRet :: MachineMonad s o (x : xs) n x a evalRet :: MachineMonad s o (x : xs) n x a evalRet = (Γ s o (x : xs) n x a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n x a forall (m :: Type -> Type) a. Monad m => a -> m a return ((Γ s o (x : xs) n x a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n x a) -> (Γ s o (x : xs) n x a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n x a forall a b. (a -> b) -> a -> b $! Γ s o (x : xs) n x a -> Code (Cont s o a x) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Cont s o a r) retCont (Γ s o (x : xs) n x a -> Code (Cont s o a x)) -> (Code (Cont s o a x) -> Γ s o (x : xs) n x a -> Code (ST s (Maybe a))) -> Γ s o (x : xs) n x a -> Code (ST s (Maybe a)) forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b >>= Code (Cont s o a x) -> Γ s o (x : xs) n x a -> Code (ST s (Maybe a)) forall s o a x (xs :: [Type]) (n :: Nat) r. Code (Cont s o a x) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)) resume evalCall :: forall s o a x xs n r. ContOps o => MVar x -> Machine s o (x : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a evalCall :: MVar x -> Machine s o (x : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a evalCall MVar x μ (Machine MachineMonad s o (x : xs) ('Succ n) r a k) = ((Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a)) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) ('Succ n) r a -> ReaderT (Ctx s o a) Identity (Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)) mk Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a)) sub γ :: Γ s o xs ('Succ n) r a γ@Γ{Code (Cont s o a r) Code (Rep o) HandlerStack ('Succ n) s o a OpStack xs handlers :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> HandlerStack n s o a input :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Rep o) operands :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs handlers :: HandlerStack ('Succ n) s o a input :: Code (Rep o) retCont :: Code (Cont s o a r) operands :: OpStack xs retCont :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Cont s o a r) ..} -> Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a)) -> Code (x -> Rep o -> ST s (Maybe a)) -> Code (Rep o) -> HandlerStack ('Succ n) s o a -> Code (ST s (Maybe a)) forall o s a x (n :: Nat). Code (SubRoutine s o a x) -> Code (Cont s o a x) -> Code (Rep o) -> Vec ('Succ n) (Code (Handler s o a)) -> Code (ST s (Maybe a)) callWithContinuation @o Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a)) sub ((Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (x -> Rep o -> ST s (Maybe a)) forall o s x (xs :: [Type]) (n :: Nat) r a. ContOps o => (Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o xs n r a -> Code (Cont s o a x) suspend Γ s o (x : xs) ('Succ n) r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ) Code (Rep o) input HandlerStack ('Succ n) s o a handlers) MachineMonad s o (x : xs) ('Succ n) r a k (MVar x -> ReaderT (Ctx s o a) Identity (Code ((x -> Rep o -> ST s (Maybe a)) -> Rep o -> (Rep o -> ST s (Maybe a)) -> ST s (Maybe a))) forall s o a (m :: Type -> Type) x. MonadReader (Ctx s o a) m => MVar x -> m (Code (SubRoutine s o a x)) askSub MVar x μ) evalJump :: forall s o a x n. MVar x -> MachineMonad s o '[] (Succ n) x a evalJump :: MVar x -> MachineMonad s o '[] ('Succ n) x a evalJump MVar x μ = MVar x -> ReaderT (Ctx s o a) Identity (Code (SubRoutine s o a x)) forall s o a (m :: Type -> Type) x. MonadReader (Ctx s o a) m => MVar x -> m (Code (SubRoutine s o a x)) askSub MVar x μ ReaderT (Ctx s o a) Identity (Code (SubRoutine s o a x)) -> (Code (SubRoutine s o a x) -> Γ s o '[] ('Succ n) x a -> Code (ST s (Maybe a))) -> MachineMonad s o '[] ('Succ n) x a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Code (SubRoutine s o a x) sub Γ{Code (Cont s o a x) Code (Rep o) HandlerStack ('Succ n) s o a OpStack '[] handlers :: HandlerStack ('Succ n) s o a input :: Code (Rep o) retCont :: Code (Cont s o a x) operands :: OpStack '[] handlers :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> HandlerStack n s o a input :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Rep o) operands :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs retCont :: forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Cont s o a r) ..} -> Code (SubRoutine s o a x) -> Code (Cont s o a x) -> Code (Rep o) -> HandlerStack ('Succ n) s o a -> Code (ST s (Maybe a)) forall o s a x (n :: Nat). Code (SubRoutine s o a x) -> Code (Cont s o a x) -> Code (Rep o) -> Vec ('Succ n) (Code (Handler s o a)) -> Code (ST s (Maybe a)) callWithContinuation @o Code (SubRoutine s o a x) sub Code (Cont s o a x) retCont Code (Rep o) input HandlerStack ('Succ n) s o a handlers evalPush :: Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalPush :: Defunc x -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalPush Defunc x x (Machine MachineMonad s o (x : xs) n r a k) = MachineMonad s o (x : xs) n r a k MachineMonad s o (x : xs) n r a -> ((Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o (x : xs) n r a -> Code (ST s (Maybe a)) m Γ s o xs n r a γ -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)) m (Γ s o xs n r a γ {operands :: OpStack (x : xs) operands = Defunc x -> OpStack xs -> OpStack (x : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc x x (Γ s o xs n r a -> OpStack xs forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o xs n r a γ)}) evalPop :: Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPop :: Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPop (Machine MachineMonad s o xs n r a k) = MachineMonad s o xs n r a k MachineMonad s o xs n r a -> ((Γ s o xs n r a -> Code (ST s (Maybe a))) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o xs n r a -> Code (ST s (Maybe a)) m Γ s o (x : xs) n r a γ -> Γ s o xs n r a -> Code (ST s (Maybe a)) m (Γ s o (x : xs) n r a γ {operands :: OpStack xs operands = let Op Defunc x _ OpStack xs xs = Γ s o (x : xs) n r a -> OpStack (x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (x : xs) n r a γ in OpStack xs xs}) evalLift2 :: Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalLift2 :: Defunc (x -> y -> z) -> Machine s o (z : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalLift2 Defunc (x -> y -> z) f (Machine MachineMonad s o (z : xs) n r a k) = MachineMonad s o (z : xs) n r a k MachineMonad s o (z : xs) n r a -> ((Γ s o (z : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o (y : x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (y : x : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o (z : xs) n r a -> Code (ST s (Maybe a)) m Γ s o (y : x : xs) n r a γ -> Γ s o (z : xs) n r a -> Code (ST s (Maybe a)) m (Γ s o (y : x : xs) n r a γ {operands :: OpStack (z : xs) operands = let Op Defunc x y (Op Defunc x x OpStack xs xs) = Γ s o (y : x : xs) n r a -> OpStack (y : x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (y : x : xs) n r a γ in Defunc z -> OpStack xs -> OpStack (z : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op (Defunc (x -> y -> z) -> Defunc x -> Defunc y -> Defunc z forall a b c. Defunc (a -> b -> c) -> Defunc a -> Defunc b -> Defunc c ap2 Defunc (x -> y -> z) f Defunc x x Defunc y y) OpStack xs xs}) evalSat :: (?ops :: InputOps (Rep o), PositionOps o, Trace) => Defunc (Char -> Bool) -> Machine s o (Char : xs) (Succ n) r a -> MachineMonad s o xs (Succ n) r a evalSat :: Defunc (Char -> Bool) -> Machine s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a evalSat Defunc (Char -> Bool) p (Machine MachineMonad s o (Char : xs) ('Succ n) r a k) = do Bool bankrupt <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks Ctx s o a -> Bool forall s o a. Ctx s o a -> Bool isBankrupt Bool hasChange <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks Ctx s o a -> Bool forall s o a. Ctx s o a -> Bool hasCoin if | Bool bankrupt -> Maybe Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) maybeEmitCheck (Int -> Maybe Int forall a. a -> Maybe a Just Int 1) ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> MachineMonad s o (Char : xs) ('Succ n) r a k | Bool hasChange -> Maybe Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) maybeEmitCheck Maybe Int forall a. Maybe a Nothing ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> (Ctx s o a -> Ctx s o a) -> MachineMonad s o (Char : xs) ('Succ n) r a -> MachineMonad s o (Char : xs) ('Succ n) r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local Ctx s o a -> Ctx s o a forall s o a. Ctx s o a -> Ctx s o a spendCoin MachineMonad s o (Char : xs) ('Succ n) r a k | Bool otherwise -> String -> MachineMonad s o xs ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall a. Trace => String -> a -> a trace String "I have a piggy :)" (MachineMonad s o xs ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a) -> MachineMonad s o xs ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall a b. (a -> b) -> a -> b $ (Ctx s o a -> Ctx s o a) -> MachineMonad s o xs ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local Ctx s o a -> Ctx s o a forall s o a. Ctx s o a -> Ctx s o a breakPiggy (Maybe Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) maybeEmitCheck (Maybe Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> (Int -> Maybe Int) -> Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall b c a. (b -> c) -> (a -> b) -> a -> c . Int -> Maybe Int forall a. a -> Maybe a Just (Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> ReaderT (Ctx s o a) Identity Int -> ReaderT (Ctx s o a) Identity ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b <$> (Ctx s o a -> Int) -> ReaderT (Ctx s o a) Identity Int forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks Ctx s o a -> Int forall s o a. Ctx s o a -> Int coins ReaderT (Ctx s o a) Identity ((Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o (Char : xs) ('Succ n) r a -> MachineMonad s o xs ('Succ n) r a forall (f :: Type -> Type) a b. Applicative f => f (a -> b) -> f a -> f b <*> (Ctx s o a -> Ctx s o a) -> MachineMonad s o (Char : xs) ('Succ n) r a -> MachineMonad s o (Char : xs) ('Succ n) r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local Ctx s o a -> Ctx s o a forall s o a. Ctx s o a -> Ctx s o a spendCoin MachineMonad s o (Char : xs) ('Succ n) r a k) where maybeEmitCheck :: Maybe Int -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) maybeEmitCheck Maybe Int Nothing Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ = (Code Char -> Code Bool) -> (Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall o s (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o)) => (Code Char -> Code Bool) -> (Γ s o (Char : xs) n r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs n r a -> Code (ST s (Maybe a)) sat (Defunc (Char -> Bool) -> Code Char -> Code Bool forall a b. Defunc (a -> b) -> Code a -> Code b genDefunc1 Defunc (Char -> Bool) p) Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)) mk (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) raise Γ s o xs ('Succ n) r a γ) Γ s o xs ('Succ n) r a γ maybeEmitCheck (Just Int n) Γ s o (Char : xs) ('Succ n) r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ = [|| let bad = $$(raise γ) in $$(emitLengthCheck n (sat (genDefunc1 p) mk [||bad||]) [||bad||] γ)||] evalEmpt :: MachineMonad s o xs (Succ n) r a evalEmpt :: MachineMonad s o xs ('Succ n) r a evalEmpt = (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a forall (m :: Type -> Type) a. Monad m => a -> m a return ((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a) -> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a forall a b. (a -> b) -> a -> b $! Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) raise evalCommit :: Machine s o xs n r a -> MachineMonad s o xs (Succ n) r a evalCommit :: Machine s o xs n r a -> MachineMonad s o xs ('Succ n) r a evalCommit (Machine MachineMonad s o xs n r a k) = MachineMonad s o xs n r a k MachineMonad s o xs n r a -> ((Γ s o xs n r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o xs n r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ -> let VCons Code (Rep o -> ST s (Maybe a)) _ Vec n (Code (Rep o -> ST s (Maybe a))) hs = Γ s o xs ('Succ n) r a -> Vec ('Succ n) (Code (Rep o -> ST s (Maybe a))) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> HandlerStack n s o a handlers Γ s o xs ('Succ n) r a γ in Γ s o xs n r a -> Code (ST s (Maybe a)) mk (Γ s o xs ('Succ n) r a γ {handlers :: HandlerStack n s o a handlers = HandlerStack n s o a hs}) evalCatch :: HandlerOps o => Machine s o xs (Succ n) r a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalCatch :: Machine s o xs ('Succ n) r a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalCatch (Machine MachineMonad s o xs ('Succ n) r a k) (Machine MachineMonad s o (o : xs) n r a h) = ((Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ n) r a -> MachineMonad s o (o : xs) n r a -> MachineMonad s o xs n r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) mk Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mh Γ s o xs n r a γ -> Γ s o xs n r a -> (Code (Rep o) -> Code (Handler s o a)) -> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> (Code (Rep o) -> Code (Handler s o a)) -> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) setupHandler Γ s o xs n r a γ (Γ s o xs n r a -> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Code (Rep o) -> Code (Handler s o a) forall o s (xs :: [Type]) (n :: Nat) r a. HandlerOps o => Γ s o xs n r a -> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Code (Rep o) -> Code (Handler s o a) buildHandler Γ s o xs n r a γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mh) Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) mk) MachineMonad s o xs ('Succ n) r a k MachineMonad s o (o : xs) n r a h evalTell :: Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalTell :: Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalTell (Machine MachineMonad s o (o : xs) n r a k) = MachineMonad s o (o : xs) n r a k MachineMonad s o (o : xs) n r a -> ((Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mk Γ s o xs n r a γ -> Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mk (Γ s o xs n r a γ {operands :: OpStack (o : xs) operands = Defunc o -> OpStack xs -> OpStack (o : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op (Code (Rep o) -> Defunc o forall o. Code (Rep o) -> Defunc o OFFSET (Γ s o xs n r a -> Code (Rep o) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Rep o) input Γ s o xs n r a γ)) (Γ s o xs n r a -> OpStack xs forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o xs n r a γ)}) evalSeek :: Machine s o xs n r a -> MachineMonad s o (o : xs) n r a evalSeek :: Machine s o xs n r a -> MachineMonad s o (o : xs) n r a evalSeek (Machine MachineMonad s o xs n r a k) = MachineMonad s o xs n r a k MachineMonad s o xs n r a -> ((Γ s o xs n r a -> Code (ST s (Maybe a))) -> Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (o : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o xs n r a -> Code (ST s (Maybe a)) mk Γ s o (o : xs) n r a γ -> let Op (OFFSET Code (Rep x) input) OpStack xs xs = Γ s o (o : xs) n r a -> OpStack (o : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (o : xs) n r a γ in Γ s o xs n r a -> Code (ST s (Maybe a)) mk (Γ s o (o : xs) n r a γ {operands :: OpStack xs operands = OpStack xs xs, input :: Code (Rep o) input = Code (Rep o) input}) evalCase :: Machine s o (x : xs) n r a -> Machine s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a evalCase :: Machine s o (x : xs) n r a -> Machine s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a evalCase (Machine MachineMonad s o (x : xs) n r a p) (Machine MachineMonad s o (y : xs) n r a q) = ((Γ s o (x : xs) n r a -> Q (TExp (ST s (Maybe a)))) -> (Γ s o (y : xs) n r a -> Q (TExp (ST s (Maybe a)))) -> Γ s o (Either x y : xs) n r a -> Q (TExp (ST s (Maybe a)))) -> MachineMonad s o (x : xs) n r a -> MachineMonad s o (y : xs) n r a -> MachineMonad s o (Either x y : xs) n r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o (x : xs) n r a -> Q (TExp (ST s (Maybe a))) mp Γ s o (y : xs) n r a -> Q (TExp (ST s (Maybe a))) mq Γ s o (Either x y : xs) n r a γ -> let Op Defunc x e OpStack xs xs = Γ s o (Either x y : xs) n r a -> OpStack (Either x y : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (Either x y : xs) n r a γ in [||case $$(genDefunc e) of Left x -> $$(mp (γ {operands = Op (FREEVAR [||x||]) xs})) Right y -> $$(mq (γ {operands = Op (FREEVAR [||y||]) xs}))||]) MachineMonad s o (x : xs) n r a p MachineMonad s o (y : xs) n r a q evalChoices :: [Defunc (x -> Bool)] -> [Machine s o xs n r a] -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalChoices :: [Defunc (x -> Bool)] -> [Machine s o xs n r a] -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalChoices [Defunc (x -> Bool)] fs [Machine s o xs n r a] ks (Machine MachineMonad s o xs n r a def) = ((Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))) -> [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] -> Γ s o (x : xs) n r a -> Q (TExp (ST s (Maybe a)))) -> MachineMonad s o xs n r a -> ReaderT (Ctx s o a) Identity [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] -> MachineMonad s o (x : xs) n r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o xs n r a -> Q (TExp (ST s (Maybe a))) mdef [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] mks Γ s o (x : xs) n r a γ -> let Op Defunc x x OpStack xs xs = Γ s o (x : xs) n r a -> OpStack (x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (x : xs) n r a γ in Defunc x -> [Defunc (x -> Bool)] -> [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] -> (Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))) -> Γ s o xs n r a -> Q (TExp (ST s (Maybe a))) forall a t p. Defunc a -> [Defunc (a -> Bool)] -> [t -> Q (TExp p)] -> (t -> Q (TExp p)) -> t -> Q (TExp p) go Defunc x x [Defunc (x -> Bool)] fs [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] mks Γ s o xs n r a -> Q (TExp (ST s (Maybe a))) mdef (Γ s o (x : xs) n r a γ {operands :: OpStack xs operands = OpStack xs xs})) MachineMonad s o xs n r a def ([Machine s o xs n r a] -> (Machine s o xs n r a -> MachineMonad s o xs n r a) -> ReaderT (Ctx s o a) Identity [Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))] forall (t :: Type -> Type) (m :: Type -> Type) a b. (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b) forM [Machine s o xs n r a] ks Machine s o xs n r a -> MachineMonad s o xs n r a forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> MachineMonad s o xs n r a getMachine) where go :: Defunc a -> [Defunc (a -> Bool)] -> [t -> Q (TExp p)] -> (t -> Q (TExp p)) -> t -> Q (TExp p) go Defunc a x (Defunc (a -> Bool) f:[Defunc (a -> Bool)] fs) (t -> Q (TExp p) mk:[t -> Q (TExp p)] mks) t -> Q (TExp p) def t γ = [|| if $$(genDefunc1 f (genDefunc x)) then $$(mk γ) else $$(go x fs mks def γ) ||] go Defunc a _ [Defunc (a -> Bool)] _ [t -> Q (TExp p)] _ t -> Q (TExp p) def t γ = t -> Q (TExp p) def t γ evalIter :: (RecBuilder o, ReturnOps o, HandlerOps o) => MVar Void -> Machine s o '[] One Void a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalIter :: MVar Void -> Machine s o '[] One Void a -> Machine s o (o : xs) n r a -> MachineMonad s o xs n r a evalIter MVar Void μ Machine s o '[] One Void a l (Machine MachineMonad s o (o : xs) n r a h) = ((Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (o : xs) n r a -> ReaderT (Ctx s o a) Identity (Ctx s o a) -> MachineMonad s o xs n r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mh Ctx s o a ctx Γ s o xs n r a γ -> Ctx s o a -> MVar Void -> Machine s o '[] One Void a -> (Code (Rep o) -> Code (Handler s o a)) -> Code (Rep o) -> Code (ST s (Maybe a)) forall o s a. (RecBuilder o, ReturnOps o) => Ctx s o a -> MVar Void -> Machine s o '[] One Void a -> (Code (Rep o) -> Code (Handler s o a)) -> Code (Rep o) -> Code (ST s (Maybe a)) buildIter Ctx s o a ctx MVar Void μ Machine s o '[] One Void a l (Γ s o xs n r a -> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Code (Rep o) -> Code (Handler s o a) forall o s (xs :: [Type]) (n :: Nat) r a. HandlerOps o => Γ s o xs n r a -> (Γ s o (o : xs) n r a -> Code (ST s (Maybe a))) -> Code (Rep o) -> Code (Handler s o a) buildHandler Γ s o xs n r a γ Γ s o (o : xs) n r a -> Code (ST s (Maybe a)) mh) (Γ s o xs n r a -> Code (Rep o) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> Code (Rep o) input Γ s o xs n r a γ)) MachineMonad s o (o : xs) n r a h ReaderT (Ctx s o a) Identity (Ctx s o a) forall r (m :: Type -> Type). MonadReader r m => m r ask evalJoin :: ΦVar x -> MachineMonad s o (x : xs) n r a evalJoin :: ΦVar x -> MachineMonad s o (x : xs) n r a evalJoin ΦVar x φ = ΦVar x -> ReaderT (Ctx s o a) Identity (Code (Cont s o a x)) forall s o a (m :: Type -> Type) x. MonadReader (Ctx s o a) m => ΦVar x -> m (Code (Cont s o a x)) askΦ ΦVar x φ ReaderT (Ctx s o a) Identity (Code (Cont s o a x)) -> (Code (Cont s o a x) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> Code (Cont s o a x) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)) forall s o a x (xs :: [Type]) (n :: Nat) r. Code (Cont s o a x) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a)) resume evalMkJoin :: JoinBuilder o => ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMkJoin :: ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMkJoin = ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a forall o x s (xs :: [Type]) (n :: Nat) r a. JoinBuilder o => ΦVar x -> Machine s o (x : xs) n r a -> Machine s o xs n r a -> MachineMonad s o xs n r a setupJoinPoint evalSwap :: Machine s o (x : y : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalSwap :: Machine s o (x : y : xs) n r a -> MachineMonad s o (y : x : xs) n r a evalSwap (Machine MachineMonad s o (x : y : xs) n r a k) = MachineMonad s o (x : y : xs) n r a k MachineMonad s o (x : y : xs) n r a -> ((Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o (y : x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (y : x : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a)) mk Γ s o (y : x : xs) n r a γ -> Γ s o (x : y : xs) n r a -> Code (ST s (Maybe a)) mk (Γ s o (y : x : xs) n r a γ {operands :: OpStack (x : y : xs) operands = let Op Defunc x y (Op Defunc x x OpStack xs xs) = Γ s o (y : x : xs) n r a -> OpStack (y : x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (y : x : xs) n r a γ in Defunc x -> OpStack (y : xs) -> OpStack (x : y : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc x x (Defunc y -> OpStack xs -> OpStack (y : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc y y OpStack xs xs)}) evalDup :: Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a evalDup :: Machine s o (x : x : xs) n r a -> MachineMonad s o (x : xs) n r a evalDup (Machine MachineMonad s o (x : x : xs) n r a k) = MachineMonad s o (x : x : xs) n r a k MachineMonad s o (x : x : xs) n r a -> ((Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a))) -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a)) mk Γ s o (x : xs) n r a γ -> let Op Defunc x x OpStack xs xs = Γ s o (x : xs) n r a -> OpStack (x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (x : xs) n r a γ in Defunc x -> (Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) forall x r. Defunc x -> (Defunc x -> Code r) -> Code r dup Defunc x x ((Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a))) -> (Defunc x -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) forall a b. (a -> b) -> a -> b $ \Defunc x dupx -> Γ s o (x : x : xs) n r a -> Code (ST s (Maybe a)) mk (Γ s o (x : xs) n r a γ {operands :: OpStack (x : x : xs) operands = Defunc x -> OpStack (x : xs) -> OpStack (x : x : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc x dupx (Defunc x -> OpStack xs -> OpStack (x : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc x dupx OpStack xs xs)}) evalMake :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalMake :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalMake ΣVar x σ Access a Machine s o xs n r a k = (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks ((Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a) -> (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall a b. (a -> b) -> a -> b $! \Ctx s o a ctx Γ s o (x : xs) n r a γ -> let Op Defunc x x OpStack xs xs = Γ s o (x : xs) n r a -> OpStack (x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (x : xs) n r a γ in ΣVar x -> Access -> Defunc x -> (Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) forall x s o a. ΣVar x -> Access -> Defunc x -> (Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) newΣ ΣVar x σ Access a Defunc x x (Machine s o xs n r a -> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a)) run Machine s o xs n r a k (Γ s o (x : xs) n r a γ {operands :: OpStack xs operands = OpStack xs xs})) Ctx s o a ctx evalGet :: ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalGet :: ΣVar x -> Access -> Machine s o (x : xs) n r a -> MachineMonad s o xs n r a evalGet ΣVar x σ Access a Machine s o (x : xs) n r a k = (Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks ((Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs n r a) -> (Ctx s o a -> Γ s o xs n r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs n r a forall a b. (a -> b) -> a -> b $! \Ctx s o a ctx Γ s o xs n r a γ -> ΣVar x -> Access -> (Defunc x -> Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) forall x s o a. ΣVar x -> Access -> (Defunc x -> Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) readΣ ΣVar x σ Access a (\Defunc x x -> Machine s o (x : xs) n r a -> Γ s o (x : xs) n r a -> Ctx s o a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a)) run Machine s o (x : xs) n r a k (Γ s o xs n r a γ {operands :: OpStack (x : xs) operands = Defunc x -> OpStack xs -> OpStack (x : xs) forall x (xs :: [Type]). Defunc x -> OpStack xs -> OpStack (x : xs) Op Defunc x x (Γ s o xs n r a -> OpStack xs forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o xs n r a γ)})) Ctx s o a ctx evalPut :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPut :: ΣVar x -> Access -> Machine s o xs n r a -> MachineMonad s o (x : xs) n r a evalPut ΣVar x σ Access a Machine s o xs n r a k = (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks ((Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a) -> (Ctx s o a -> Γ s o (x : xs) n r a -> Code (ST s (Maybe a))) -> MachineMonad s o (x : xs) n r a forall a b. (a -> b) -> a -> b $! \Ctx s o a ctx Γ s o (x : xs) n r a γ -> let Op Defunc x x OpStack xs xs = Γ s o (x : xs) n r a -> OpStack (x : xs) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs n r a -> OpStack xs operands Γ s o (x : xs) n r a γ in ΣVar x -> Access -> Defunc x -> (Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) forall x s o a. ΣVar x -> Access -> Defunc x -> (Ctx s o a -> Code (ST s (Maybe a))) -> Ctx s o a -> Code (ST s (Maybe a)) writeΣ ΣVar x σ Access a Defunc x x (Machine s o xs n r a -> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Machine s o xs n r a -> Γ s o xs n r a -> Ctx s o a -> Code (ST s (Maybe a)) run Machine s o xs n r a k (Γ s o (x : xs) n r a γ {operands :: OpStack xs operands = OpStack xs xs})) Ctx s o a ctx evalLogEnter :: (?ops :: InputOps (Rep o), LogHandler o) => String -> Machine s o xs (Succ (Succ n)) r a -> MachineMonad s o xs (Succ n) r a evalLogEnter :: String -> Machine s o xs ('Succ ('Succ n)) r a -> MachineMonad s o xs ('Succ n) r a evalLogEnter String name (Machine MachineMonad s o xs ('Succ ('Succ n)) r a mk) = ((Γ s o xs ('Succ ('Succ n)) r a -> Code (ST s (Maybe a))) -> Ctx s o a -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> MachineMonad s o xs ('Succ ('Succ n)) r a -> ReaderT (Ctx s o a) Identity (Ctx s o a) -> MachineMonad s o xs ('Succ n) r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o xs ('Succ ('Succ n)) r a -> Code (ST s (Maybe a)) k Ctx s o a ctx Γ s o xs ('Succ n) r a γ -> [|| Debug.Trace.trace $$(preludeString name '>' γ ctx "") $$(setupHandler γ (logHandler name ctx γ) k)||]) ((Ctx s o a -> Ctx s o a) -> MachineMonad s o xs ('Succ ('Succ n)) r a -> MachineMonad s o xs ('Succ ('Succ n)) r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local Ctx s o a -> Ctx s o a forall s o a. Ctx s o a -> Ctx s o a debugUp MachineMonad s o xs ('Succ ('Succ n)) r a mk) ReaderT (Ctx s o a) Identity (Ctx s o a) forall r (m :: Type -> Type). MonadReader r m => m r ask evalLogExit :: (?ops :: InputOps (Rep o), PositionOps o, LogOps (Rep o)) => String -> Machine s o xs n r a -> MachineMonad s o xs n r a evalLogExit :: String -> Machine s o xs n r a -> MachineMonad s o xs n r a evalLogExit String name (Machine MachineMonad s o xs n r a mk) = ((Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))) -> Ctx s o a -> Γ s o xs n r a -> Q (TExp (ST s (Maybe a)))) -> MachineMonad s o xs n r a -> ReaderT (Ctx s o a) Identity (Ctx s o a) -> MachineMonad s o xs n r a forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Γ s o xs n r a -> Q (TExp (ST s (Maybe a))) k Ctx s o a ctx Γ s o xs n r a γ -> [|| Debug.Trace.trace $$(preludeString name '<' γ (debugDown ctx) (color Green " Good")) $$(k γ) ||]) ((Ctx s o a -> Ctx s o a) -> MachineMonad s o xs n r a -> MachineMonad s o xs n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local Ctx s o a -> Ctx s o a forall s o a. Ctx s o a -> Ctx s o a debugDown MachineMonad s o xs n r a mk) ReaderT (Ctx s o a) Identity (Ctx s o a) forall r (m :: Type -> Type). MonadReader r m => m r ask evalMeta :: (?ops :: InputOps (Rep o), PositionOps o) => MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMeta :: MetaInstr n -> Machine s o xs n r a -> MachineMonad s o xs n r a evalMeta (AddCoins Int coins) (Machine MachineMonad s o xs n r a k) = do Bool requiresPiggy <- (Ctx s o a -> Bool) -> ReaderT (Ctx s o a) Identity Bool forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks Ctx s o a -> Bool forall s o a. Ctx s o a -> Bool hasCoin if Bool requiresPiggy then (Ctx s o a -> Ctx s o a) -> MachineMonad s o xs n r a -> MachineMonad s o xs n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local (Int -> Ctx s o a -> Ctx s o a forall s o a. Int -> Ctx s o a -> Ctx s o a storePiggy Int coins) MachineMonad s o xs n r a k else (Ctx s o a -> Ctx s o a) -> MachineMonad s o xs n r a -> MachineMonad s o xs n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local (Int -> Ctx s o a -> Ctx s o a forall s o a. Int -> Ctx s o a -> Ctx s o a giveCoins Int coins) MachineMonad s o xs n r a k MachineMonad s o xs n r a -> ((Γ s o xs n r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> ReaderT (Ctx s o a) Identity (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b <&> \Γ s o xs n r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ -> Int -> (Γ s o xs n r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs n r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), PositionOps o) => Int -> (Γ s o xs n r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs n r a -> Code (ST s (Maybe a)) emitLengthCheck Int coins Γ s o xs n r a -> Code (ST s (Maybe a)) mk (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) raise Γ s o xs ('Succ n) r a γ) Γ s o xs n r a Γ s o xs ('Succ n) r a γ evalMeta (RefundCoins Int coins) (Machine MachineMonad s o xs n r a k) = (Ctx s o a -> Ctx s o a) -> MachineMonad s o xs n r a -> MachineMonad s o xs n r a forall r (m :: Type -> Type) a. MonadReader r m => (r -> r) -> m a -> m a local (Int -> Ctx s o a -> Ctx s o a forall s o a. Int -> Ctx s o a -> Ctx s o a giveCoins Int coins) MachineMonad s o xs n r a k evalMeta (DrainCoins Int coins) (Machine MachineMonad s o xs n r a k) = (Int -> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> ReaderT (Ctx s o a) Identity Int -> ReaderT (Ctx s o a) Identity (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> ReaderT (Ctx s o a) Identity (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) forall (m :: Type -> Type) a1 a2 r. Monad m => (a1 -> a2 -> r) -> m a1 -> m a2 -> m r liftM2 (\Int n Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) mk Γ s o xs ('Succ n) r a γ -> Int -> (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. (?ops::InputOps (Rep o), PositionOps o) => Int -> (Γ s o xs n r a -> Code (ST s (Maybe a))) -> Code (ST s (Maybe a)) -> Γ s o xs n r a -> Code (ST s (Maybe a)) emitLengthCheck Int n Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) mk (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) forall s o (xs :: [Type]) (n :: Nat) r a. Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a)) raise Γ s o xs ('Succ n) r a γ) Γ s o xs ('Succ n) r a γ) ((Ctx s o a -> Int) -> ReaderT (Ctx s o a) Identity Int forall r (m :: Type -> Type) a. MonadReader r m => (r -> a) -> m a asks ((Int coins Int -> Int -> Int forall a. Num a => a -> a -> a -) (Int -> Int) -> (Ctx s o a -> Int) -> Ctx s o a -> Int forall b c a. (b -> c) -> (a -> b) -> a -> c . Ctx s o a -> Int forall s o a. Ctx s o a -> Int liquidate)) MachineMonad s o xs n r a ReaderT (Ctx s o a) Identity (Γ s o xs ('Succ n) r a -> Code (ST s (Maybe a))) k