{-# LANGUAGE OverloadedStrings,
PatternSynonyms,
DerivingStrategies #-}
module Parsley.Internal.Backend.Machine.Instructions (
Instr(..),
Handler(..),
Access(..),
MetaInstr(..),
_App, _Fmap, _Modify, _Make, _Put, _Get, _Jump,
addCoins, refundCoins, drainCoins, giveBursary, blockCoins,
PosSelector(..)
) where
import Data.Kind (Type)
import Data.Void (Void)
import Parsley.Internal.Backend.Machine.Identifiers (MVar, ΦVar, ΣVar)
import Parsley.Internal.Backend.Machine.Types.Coins (Coins(willConsume))
import Parsley.Internal.Common (IFunctor4, Fix4(In4), Const4(..), imap4, cata4, Nat(..), One, intercalateDiff)
import Parsley.Internal.Core.CombinatorAST (PosSelector(..))
import Parsley.Internal.Core.CharPred (CharPred)
import Parsley.Internal.Backend.Machine.Defunc as Machine (Defunc, user)
import Parsley.Internal.Core.Defunc as Core (Defunc(ID), pattern FLIP_H)
import qualified Parsley.Internal.Backend.Machine.Types.Coins as Coins (pattern Zero)
data Instr (o :: Type)
(k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type])
(n :: Nat)
(r :: Type)
(a :: Type)
where
Ret :: Instr o k '[x] n x a
Push :: Machine.Defunc x -> k (x : xs) n r a -> Instr o k xs n r a
Pop :: k xs n r a -> Instr o k (x : xs) n r a
Lift2 :: Machine.Defunc (x -> y -> z)
-> k (z : xs) n r a
-> Instr o k (y : x : xs) n r a
Sat :: CharPred
-> k (Char : xs) (Succ n) r a
-> Instr o k xs (Succ n) r a
Call :: MVar x
-> k (x : xs) (Succ n) r a
-> Instr o k xs (Succ n) r a
Empt :: Instr o k xs (Succ n) r a
Commit :: k xs n r a -> Instr o k xs (Succ n) r a
Catch :: k xs (Succ n) r a
-> Handler o k (o : xs) n r a
-> Instr o k xs n r a
Tell :: k (o : xs) n r a -> Instr o k xs n r a
Seek :: k xs n r a -> Instr o k (o : xs) n r a
Case :: k (x : xs) n r a
-> k (y : xs) n r a
-> Instr o k (Either x y : xs) n r a
Choices :: [Machine.Defunc (x -> Bool)]
-> [k xs n r a]
-> k xs n r a
-> Instr o k (x : xs) n r a
Iter :: MVar Void
-> k '[] One Void a
-> Handler o k (o : xs) n r a
-> Instr o k xs n r a
Join :: ΦVar x -> Instr o k (x : xs) n r a
MkJoin :: ΦVar x
-> k (x : xs) n r a
-> k xs n r a
-> Instr o k xs n r a
Swap :: k (x : y : xs) n r a -> Instr o k (y : x : xs) n r a
Dup :: k (x : x : xs) n r a -> Instr o k (x : xs) n r a
Make :: ΣVar x
-> Access
-> k xs n r a
-> Instr o k (x : xs) n r a
Get :: ΣVar x
-> Access
-> k (x : xs) n r a
-> Instr o k xs n r a
Put :: ΣVar x
-> Access
-> k xs n r a
-> Instr o k (x : xs) n r a
SelectPos :: PosSelector -> k (Int : xs) n r a -> Instr o k xs n r a
LogEnter :: String
-> k xs (Succ (Succ n)) r a
-> Instr o k xs (Succ n) r a
LogExit :: String
-> k xs n r a
-> Instr o k xs n r a
MetaInstr :: MetaInstr n
-> k xs n r a
-> Instr o k xs n r a
data Handler (o :: Type) (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type]) (n :: Nat) (r :: Type) (a :: Type) where
Same :: Bool
-> k xs n r a
-> Bool
-> k (o : xs) n r a
-> Handler o k (o : xs) n r a
Always :: Bool
-> k (o : xs) n r a
-> Handler o k (o : xs) n r a
data Access = Hard
| Soft
deriving stock Int -> Access -> String -> String
[Access] -> String -> String
Access -> String
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Access] -> String -> String
$cshowList :: [Access] -> String -> String
show :: Access -> String
$cshow :: Access -> String
showsPrec :: Int -> Access -> String -> String
$cshowsPrec :: Int -> Access -> String -> String
Show
data MetaInstr (n :: Nat) where
AddCoins :: Coins -> MetaInstr (Succ n)
RefundCoins :: Int -> MetaInstr n
DrainCoins :: Int -> MetaInstr (Succ n)
GiveBursary :: Int -> MetaInstr n
BlockCoins :: Bool -> MetaInstr n
mkCoin :: (Coins -> MetaInstr n) -> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin :: forall (n :: Nat) o (xs :: [Type]) r a.
(Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Coins -> MetaInstr n
_ Coins
Coins.Zero = forall a. a -> a
id
mkCoin Coins -> MetaInstr n
meta Coins
n = forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) r a o.
MetaInstr n -> k xs n r a -> Instr o k xs n r a
MetaInstr (Coins -> MetaInstr n
meta Coins
n)
addCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
addCoins :: forall o (xs :: [Type]) (n :: Nat) r a.
Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
addCoins = forall (n :: Nat) o (xs :: [Type]) r a.
(Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin forall (xs :: Nat). Coins -> MetaInstr ('Succ xs)
AddCoins
refundCoins :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins :: forall o (xs :: [Type]) (n :: Nat) r a.
Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins = forall (n :: Nat) o (xs :: [Type]) r a.
(Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin (forall (n :: Nat). Int -> MetaInstr n
RefundCoins forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coins -> Int
willConsume)
drainCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
drainCoins :: forall o (xs :: [Type]) (n :: Nat) r a.
Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
drainCoins = forall (n :: Nat) o (xs :: [Type]) r a.
(Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin (forall (xs :: Nat). Int -> MetaInstr ('Succ xs)
DrainCoins forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coins -> Int
willConsume)
giveBursary :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
giveBursary :: forall o (xs :: [Type]) (n :: Nat) r a.
Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
giveBursary = forall (n :: Nat) o (xs :: [Type]) r a.
(Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin (forall (n :: Nat). Int -> MetaInstr n
GiveBursary forall b c a. (b -> c) -> (a -> b) -> a -> c
. Coins -> Int
willConsume)
blockCoins :: Bool -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
blockCoins :: forall o (xs :: [Type]) (n :: Nat) r a.
Bool
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
blockCoins Bool
strong = forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (n :: Nat) (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) r a o.
MetaInstr n -> k xs n r a -> Instr o k xs n r a
MetaInstr (forall (n :: Nat). Bool -> MetaInstr n
BlockCoins Bool
strong)
_App :: Fix4 (Instr o) (y : xs) n r a -> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
_App :: forall o y (xs :: [Type]) (n :: Nat) r a x.
Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
_App = forall xs xs xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
Defunc (xs -> xs -> xs)
-> k (xs : xs) n r a -> Instr o k (xs : xs : xs) n r a
Lift2 (forall a. Defunc a -> Defunc a
user forall a1. Defunc (a1 -> a1)
ID)
_Fmap :: Machine.Defunc (x -> y) -> Fix4 (Instr o) (y : xs) n r a -> Instr o (Fix4 (Instr o)) (x : xs) n r a
_Fmap :: forall x y o (xs :: [Type]) (n :: Nat) r a.
Defunc (x -> y)
-> Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
_Fmap Defunc (x -> y)
f Fix4 (Instr o) (y : xs) n r a
k = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
Defunc xs -> k (xs : xs) n r a -> Instr o k xs n r a
Push Defunc (x -> y)
f (forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 (forall xs xs xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
Defunc (xs -> xs -> xs)
-> k (xs : xs) n r a -> Instr o k (xs : xs : xs) n r a
Lift2 (forall a. Defunc a -> Defunc a
user (forall y x a b c.
((x -> y) ~ ((a -> b -> c) -> b -> a -> c)) =>
Defunc x -> Defunc y
FLIP_H forall a1. Defunc (a1 -> a1)
ID)) Fix4 (Instr o) (y : xs) n r a
k))
_Modify :: ΣVar x -> Fix4 (Instr o) xs n r a -> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a
_Modify :: forall x o (xs :: [Type]) (n :: Nat) r a.
ΣVar x
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a
_Modify ΣVar x
σ = forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> k (x : xs) n r a -> Instr o k xs n r a
_Get ΣVar x
σ forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o y (xs :: [Type]) (n :: Nat) r a x.
Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
_App forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Put ΣVar x
σ
_Make :: ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Make :: forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Make ΣVar x
σ = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k xs n r a -> Instr o k (xs : xs) n r a
Make ΣVar x
σ Access
Hard
_Put :: ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Put :: forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Put ΣVar x
σ = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k xs n r a -> Instr o k (xs : xs) n r a
Put ΣVar x
σ Access
Hard
_Get :: ΣVar x -> k (x : xs) n r a -> Instr o k xs n r a
_Get :: forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> k (x : xs) n r a -> Instr o k xs n r a
_Get ΣVar x
σ = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k (xs : xs) n r a -> Instr o k xs n r a
Get ΣVar x
σ Access
Hard
_Jump :: MVar x -> Instr o (Fix4 (Instr o)) '[] (Succ n) x a
_Jump :: forall x o (n :: Nat) a.
MVar x -> Instr o (Fix4 (Instr o)) '[] ('Succ n) x a
_Jump = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (xs :: Nat) r a o.
MVar xs
-> k (xs : xs) ('Succ xs) r a -> Instr o k xs ('Succ xs) r a
Call (forall {k} {k1} {k2} {k3}
(f :: (k -> k1 -> k2 -> k3 -> Type) -> k -> k1 -> k2 -> k3 -> Type)
(i :: k) (j :: k1) (k4 :: k2) (l :: k3).
f (Fix4 f) i j k4 l -> Fix4 f i j k4 l
In4 forall o (k :: [Type] -> Nat -> Type -> Type -> Type) x (n :: Nat)
a.
Instr o k '[x] n x a
Ret)
instance IFunctor4 (Instr o) where
imap4 :: forall (a :: [Type] -> Nat -> Type -> Type -> Type) x
(b :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
(j :: Nat) k.
(forall (i' :: [Type]) (j' :: Nat) k'.
a i' j' k' x -> b i' j' k' x)
-> Instr o a i j k x -> Instr o b i j k x
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
_ Instr o a i j k x
Ret = forall o (k :: [Type] -> Nat -> Type -> Type -> Type) x (n :: Nat)
a.
Instr o k '[x] n x a
Ret
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Push Defunc x
x a (x : i) j k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
Defunc xs -> k (xs : xs) n r a -> Instr o k xs n r a
Push Defunc x
x (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : i) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Pop a xs j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o xs.
k xs n r a -> Instr o k (xs : xs) n r a
Pop (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Lift2 Defunc (x -> y -> z)
g a (z : xs) j k x
k) = forall xs xs xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
Defunc (xs -> xs -> xs)
-> k (xs : xs) n r a -> Instr o k (xs : xs : xs) n r a
Lift2 Defunc (x -> y -> z)
g (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (z : xs) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Sat CharPred
g a (Char : i) ('Succ n) k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(xs :: Nat) r a o.
CharPred
-> k (Char : xs) ('Succ xs) r a -> Instr o k xs ('Succ xs) r a
Sat CharPred
g (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (Char : i) ('Succ n) k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Call MVar x
μ a (x : i) ('Succ n) k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (xs :: Nat) r a o.
MVar xs
-> k (xs : xs) ('Succ xs) r a -> Instr o k xs ('Succ xs) r a
Call MVar x
μ (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : i) ('Succ n) k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
_ Instr o a i j k x
Empt = forall o (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (xs :: Nat) r a.
Instr o k xs ('Succ xs) r a
Empt
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Commit a i n k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(xs :: Nat) r a o.
k xs xs r a -> Instr o k xs ('Succ xs) r a
Commit (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i n k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Catch a i ('Succ j) k x
p Handler o a (o : i) j k x
h) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o.
k xs ('Succ n) r a
-> Handler o k (o : xs) n r a -> Instr o k xs n r a
Catch (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i ('Succ j) k x
p) (forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
-> [Type] -> Nat -> Type -> Type -> Type)
(a :: [Type] -> Nat -> Type -> Type -> Type) x
(b :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
(j :: Nat) k.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
a i' j' k' x -> b i' j' k' x)
-> f a i j k x -> f b i j k x
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f Handler o a (o : i) j k x
h)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Tell a (o : i) j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) o
(xs :: [Type]) (n :: Nat) r a.
k (o : xs) n r a -> Instr o k xs n r a
Tell (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (o : i) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Seek a xs j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o.
k xs n r a -> Instr o k (o : xs) n r a
Seek (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Case a (x : xs) j k x
p a (y : xs) j k x
q) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) xs
(xs :: [Type]) (n :: Nat) r a xs o.
k (xs : xs) n r a
-> k (xs : xs) n r a -> Instr o k (Either xs xs : xs) n r a
Case (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : xs) j k x
p) (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (y : xs) j k x
q)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Choices [Defunc (x -> Bool)]
fs [a xs j k x]
ks a xs j k x
def) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
[Defunc (xs -> Bool)]
-> [k xs n r a] -> k xs n r a -> Instr o k (xs : xs) n r a
Choices [Defunc (x -> Bool)]
fs (forall a b. (a -> b) -> [a] -> [b]
map forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f [a xs j k x]
ks) (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
def)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Iter MVar Void
μ a '[] One Void x
l Handler o a (o : i) j k x
h) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) a o
(xs :: [Type]) (n :: Nat) r.
MVar Void
-> k '[] One Void a
-> Handler o k (o : xs) n r a
-> Instr o k xs n r a
Iter MVar Void
μ (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a '[] One Void x
l) (forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
-> [Type] -> Nat -> Type -> Type -> Type)
(a :: [Type] -> Nat -> Type -> Type -> Type) x
(b :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
(j :: Nat) k.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
a i' j' k' x -> b i' j' k' x)
-> f a i j k x -> f b i j k x
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f Handler o a (o : i) j k x
h)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
_ (Join ΦVar x
φ) = forall xs o (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a.
ΦVar xs -> Instr o k (xs : xs) n r a
Join ΦVar x
φ
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (MkJoin ΦVar x
φ a (x : i) j k x
p a i j k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΦVar xs -> k (xs : xs) n r a -> k xs n r a -> Instr o k xs n r a
MkJoin ΦVar x
φ (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : i) j k x
p) (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Swap a (x : y : xs) j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) xs xs
(xs :: [Type]) (n :: Nat) r a o.
k (xs : xs : xs) n r a -> Instr o k (xs : xs : xs) n r a
Swap (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : y : xs) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Dup a (x : x : xs) j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) xs
(xs :: [Type]) (n :: Nat) r a o.
k (xs : xs : xs) n r a -> Instr o k (xs : xs) n r a
Dup (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : x : xs) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Make ΣVar x
σ Access
a a xs j k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k xs n r a -> Instr o k (xs : xs) n r a
Make ΣVar x
σ Access
a (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Get ΣVar x
σ Access
a a (x : i) j k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k (xs : xs) n r a -> Instr o k xs n r a
Get ΣVar x
σ Access
a (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : i) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Put ΣVar x
σ Access
a a xs j k x
k) = forall xs (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) (n :: Nat) r a o.
ΣVar xs -> Access -> k xs n r a -> Instr o k (xs : xs) n r a
Put ΣVar x
σ Access
a (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (SelectPos PosSelector
sel a (Int : i) j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o.
PosSelector -> k (Int : xs) n r a -> Instr o k xs n r a
SelectPos PosSelector
sel (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (Int : i) j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (LogEnter String
name a i ('Succ ('Succ n)) k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(xs :: Nat) r a o.
String
-> k xs ('Succ ('Succ xs)) r a -> Instr o k xs ('Succ xs) r a
LogEnter String
name (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i ('Succ ('Succ n)) k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (LogExit String
name a i j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o.
String -> k xs n r a -> Instr o k xs n r a
LogExit String
name (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i j k x
k)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (MetaInstr MetaInstr j
m a i j k x
k) = forall (n :: Nat) (k :: [Type] -> Nat -> Type -> Type -> Type)
(xs :: [Type]) r a o.
MetaInstr n -> k xs n r a -> Instr o k xs n r a
MetaInstr MetaInstr j
m (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i j k x
k)
instance IFunctor4 (Handler o) where
imap4 :: forall (a :: [Type] -> Nat -> Type -> Type -> Type) x
(b :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
(j :: Nat) k.
(forall (i' :: [Type]) (j' :: Nat) k'.
a i' j' k' x -> b i' j' k' x)
-> Handler o a i j k x -> Handler o b i j k x
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Same Bool
gyes a xs j k x
yes Bool
gno a (o : xs) j k x
no) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
(n :: Nat) r a o.
Bool
-> k xs n r a
-> Bool
-> k (o : xs) n r a
-> Handler o k (o : xs) n r a
Same Bool
gyes (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a xs j k x
yes) Bool
gno (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (o : xs) j k x
no)
imap4 forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f (Always Bool
gk a (o : xs) j k x
k) = forall (k :: [Type] -> Nat -> Type -> Type -> Type) o
(xs :: [Type]) (n :: Nat) r a.
Bool -> k (o : xs) n r a -> Handler o k (o : xs) n r a
Always Bool
gk (forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (o : xs) j k x
k)
instance Show (Fix4 (Instr o) xs n r a) where
show :: Fix4 (Instr o) xs n r a -> String
show = (forall a b. (a -> b) -> a -> b
$ String
"") forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 {k} {k1} {k2} {k3} a (i :: k) (j :: k1) (k4 :: k2)
(l :: k3).
a -> Const4 a i j k4 l
Const4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (xs :: [Type]) (n :: Nat) r a.
Instr o (Const4 (String -> String)) xs n r a -> String -> String
alg)
where
alg :: forall xs n r a. Instr o (Const4 (String -> String)) xs n r a -> String -> String
alg :: forall (xs :: [Type]) (n :: Nat) r a.
Instr o (Const4 (String -> String)) xs n r a -> String -> String
alg Instr o (Const4 (String -> String)) xs n r a
Ret = String -> String
"Ret"
alg (Call MVar x
μ Const4 (String -> String) (x : xs) ('Succ n) r a
k) = String -> String
"(Call " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows MVar x
μ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : xs) ('Succ n) r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Push Defunc x
x Const4 (String -> String) (x : xs) n r a
k) = String -> String
"(Push " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Defunc x
x forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Pop Const4 (String -> String) xs n r a
k) = String -> String
"(Pop " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Lift2 Defunc (x -> y -> z)
f Const4 (String -> String) (z : xs) n r a
k) = String -> String
"(Lift2 " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Defunc (x -> y -> z)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (z : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Sat CharPred
f Const4 (String -> String) (Char : xs) ('Succ n) r a
k) = String -> String
"(Sat " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows CharPred
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (Char : xs) ('Succ n) r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg Instr o (Const4 (String -> String)) xs n r a
Empt = String -> String
"Empt"
alg (Commit Const4 (String -> String) xs n r a
k) = String -> String
"(Commit " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Catch Const4 (String -> String) xs ('Succ n) r a
p Handler o (Const4 (String -> String)) (o : xs) n r a
h) = String -> String
"(Catch " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs ('Succ n) r a
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Handler o (Const4 (String -> String)) (o : xs) n r a
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Tell Const4 (String -> String) (o : xs) n r a
k) = String -> String
"(Tell " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (o : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Seek Const4 (String -> String) xs n r a
k) = String -> String
"(Seek " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Case Const4 (String -> String) (x : xs) n r a
p Const4 (String -> String) (y : xs) n r a
q) = String -> String
"(Case " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : xs) n r a
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (y : xs) n r a
q forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Choices [Defunc (x -> Bool)]
fs [Const4 (String -> String) xs n r a]
ks Const4 (String -> String) xs n r a
def) = String -> String
"(Choices " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows [Defunc (x -> Bool)]
fs forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" [" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. (a -> a) -> [a -> a] -> a -> a
intercalateDiff String -> String
", " (forall a b. (a -> b) -> [a] -> [b]
map forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 [Const4 (String -> String) xs n r a]
ks) forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
"] " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
def forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Iter MVar Void
μ Const4 (String -> String) '[] One Void a
l Handler o (Const4 (String -> String)) (o : xs) n r a
h) = String -> String
"{Iter " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows MVar Void
μ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) '[] One Void a
l forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Handler o (Const4 (String -> String)) (o : xs) n r a
h forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
"}"
alg (Join ΦVar x
φ) = forall a. Show a => a -> String -> String
shows ΦVar x
φ
alg (MkJoin ΦVar x
φ Const4 (String -> String) (x : xs) n r a
p Const4 (String -> String) xs n r a
k) = String -> String
"(let " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows ΦVar x
φ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" = " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : xs) n r a
p forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" in " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Swap Const4 (String -> String) (x : y : xs) n r a
k) = String -> String
"(Swap " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : y : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Dup Const4 (String -> String) (x : x : xs) n r a
k) = String -> String
"(Dup " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : x : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Make ΣVar x
σ Access
a Const4 (String -> String) xs n r a
k) = String -> String
"(Make " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows ΣVar x
σ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Access
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Get ΣVar x
σ Access
a Const4 (String -> String) (x : xs) n r a
k) = String -> String
"(Get " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows ΣVar x
σ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Access
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (x : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (Put ΣVar x
σ Access
a Const4 (String -> String) xs n r a
k) = String -> String
"(Put " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows ΣVar x
σ forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows Access
a forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
" " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (SelectPos PosSelector
Line Const4 (String -> String) (Int : xs) n r a
k) = String -> String
"(Line " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (Int : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (SelectPos PosSelector
Col Const4 (String -> String) (Int : xs) n r a
k) = String -> String
"(Col " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (Int : xs) n r a
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
")"
alg (LogEnter String
_ Const4 (String -> String) xs ('Succ ('Succ n)) r a
k) = forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs ('Succ ('Succ n)) r a
k
alg (LogExit String
_ Const4 (String -> String) xs n r a
k) = forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k
alg (MetaInstr BlockCoins{} Const4 (String -> String) xs n r a
k) = forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k
alg (MetaInstr MetaInstr n
m Const4 (String -> String) xs n r a
k) = String -> String
"[" forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> String -> String
shows MetaInstr n
m forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> String
"] " forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
k
instance Show (Handler o (Const4 (String -> String)) (o : xs) n r a) where
show :: Handler o (Const4 (String -> String)) (o : xs) n r a -> String
show (Same Bool
_ Const4 (String -> String) xs n r a
yes Bool
_ Const4 (String -> String) (o : xs) n r a
no) = String -> String
"(Dup (Tell (Lift2 same (If " (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) xs n r a
yes (String -> String
" " (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (o : xs) n r a
no String
"))))")))
show (Always Bool
_ Const4 (String -> String) (o : xs) n r a
k) = forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
(l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (String -> String) (o : xs) n r a
k String
""
instance Show (MetaInstr n) where
show :: MetaInstr n -> String
show (AddCoins Coins
n) = String
"Add " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Coins
n forall a. [a] -> [a] -> [a]
++ String
" coins"
show (RefundCoins Int
n) = String
"Refund " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" coins"
show (DrainCoins Int
n) = String
"Using " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" coins"
show (GiveBursary Int
n) = String
"Bursary of " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> String
show Int
n forall a. [a] -> [a] -> [a]
++ String
" coins"
show BlockCoins{} = String
""