{-# LANGUAGE OverloadedStrings,
             PatternSynonyms,
             DerivingStrategies #-}
module Parsley.Internal.Backend.Machine.Instructions (module Parsley.Internal.Backend.Machine.Instructions) where

import Data.Kind                                    (Type)
import Data.Void                                    (Void)
import Parsley.Internal.Backend.Machine.Identifiers (MVar, ΦVar, ΣVar)
import Parsley.Internal.Common                      (IFunctor4, Fix4(In4), Const4(..), imap4, cata4, Nat(..), One, intercalateDiff)

import Parsley.Internal.Backend.Machine.Defunc as Machine (Defunc, user)
import Parsley.Internal.Core.Defunc            as Core    (Defunc(ID), pattern FLIP_H)

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       :: Machine.Defunc (Char -> Bool) -> 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
  Jump      :: MVar x -> Instr o k '[] (Succ n) x 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 -> 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 -> 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
  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 Access = Hard | Soft deriving stock Int -> Access -> ShowS
[Access] -> ShowS
Access -> String
(Int -> Access -> ShowS)
-> (Access -> String) -> ([Access] -> ShowS) -> Show Access
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Access] -> ShowS
$cshowList :: [Access] -> ShowS
show :: Access -> String
$cshow :: Access -> String
showsPrec :: Int -> Access -> ShowS
$cshowsPrec :: Int -> Access -> ShowS
Show

data MetaInstr (n :: Nat) where
  AddCoins    :: Int -> MetaInstr (Succ n)
  RefundCoins :: Int -> MetaInstr n
  DrainCoins  :: Int -> MetaInstr (Succ n)

mkCoin :: (Int -> MetaInstr n) -> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin :: (Int -> MetaInstr n)
-> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Int -> MetaInstr n
_    Int
0 = Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
forall a. a -> a
id
mkCoin Int -> MetaInstr n
meta Int
n = Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a)
-> (Fix4 (Instr o) xs n r a -> Instr o (Fix4 (Instr o)) xs n r a)
-> Fix4 (Instr o) xs n r a
-> Fix4 (Instr o) xs n r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInstr n
-> Fix4 (Instr o) xs n r a -> Instr o (Fix4 (Instr o)) xs n r a
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 (Int -> MetaInstr n
meta Int
n)

addCoins :: Int -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
addCoins :: Int
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
addCoins = (Int -> MetaInstr ('Succ n))
-> Int
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
forall (n :: Nat) o (xs :: [Type]) r a.
(Int -> MetaInstr n)
-> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Int -> MetaInstr ('Succ n)
forall (n :: Nat). Int -> MetaInstr ('Succ n)
AddCoins
refundCoins :: Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins :: Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins = (Int -> MetaInstr n)
-> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
forall (n :: Nat) o (xs :: [Type]) r a.
(Int -> MetaInstr n)
-> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Int -> MetaInstr n
forall (n :: Nat). Int -> MetaInstr n
RefundCoins
drainCoins :: Int -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
drainCoins :: Int
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
drainCoins = (Int -> MetaInstr ('Succ n))
-> Int
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
forall (n :: Nat) o (xs :: [Type]) r a.
(Int -> MetaInstr n)
-> Int -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Int -> MetaInstr ('Succ n)
forall (n :: Nat). Int -> MetaInstr ('Succ n)
DrainCoins

_App :: Fix4 (Instr o) (y : xs) n r a -> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
_App :: Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
_App Fix4 (Instr o) (y : xs) n r a
k = Defunc ((x -> y) -> x -> y)
-> Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> y) : xs) n r a
forall x y z (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
Defunc (x -> y -> z)
-> k (z : xs) n r a -> Instr o k (y : x : xs) n r a
Lift2 (Defunc ((x -> y) -> x -> y) -> Defunc ((x -> y) -> x -> y)
forall a. Defunc a -> Defunc a
user Defunc ((x -> y) -> x -> y)
forall a. Defunc (a -> a)
ID) Fix4 (Instr o) (y : xs) n r a
k

_Fmap :: Machine.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)
-> 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 = Defunc (x -> y)
-> Fix4 (Instr o) ((x -> y) : x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
Defunc x -> k (x : xs) n r a -> Instr o k xs n r a
Push Defunc (x -> y)
f (Instr o (Fix4 (Instr o)) ((x -> y) : x : xs) n r a
-> Fix4 (Instr o) ((x -> y) : x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Defunc (x -> (x -> y) -> y)
-> Fix4 (Instr o) (y : xs) n r a
-> Instr o (Fix4 (Instr o)) ((x -> y) : x : xs) n r a
forall x y z (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
Defunc (x -> y -> z)
-> k (z : xs) n r a -> Instr o k (y : x : xs) n r a
Lift2 (Defunc (x -> (x -> y) -> y) -> Defunc (x -> (x -> y) -> y)
forall a. Defunc a -> Defunc a
user (Defunc ((x -> y) -> x -> y) -> Defunc (x -> (x -> y) -> y)
forall y x a b c.
((x -> y) ~ ((a -> b -> c) -> b -> a -> c)) =>
Defunc x -> Defunc y
FLIP_H Defunc ((x -> y) -> x -> y)
forall a. Defunc (a -> a)
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 :: ΣVar x
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a
_Modify ΣVar x
σ  = ΣVar x
-> Fix4 (Instr o) (x : (x -> x) : xs) n r a
-> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a
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
σ (Fix4 (Instr o) (x : (x -> x) : xs) n r a
 -> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a)
-> (Fix4 (Instr o) xs n r a
    -> Fix4 (Instr o) (x : (x -> x) : xs) n r a)
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) ((x -> x) : xs) n r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a
-> Fix4 (Instr o) (x : (x -> x) : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a
 -> Fix4 (Instr o) (x : (x -> x) : xs) n r a)
-> (Fix4 (Instr o) xs n r a
    -> Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a)
-> Fix4 (Instr o) xs n r a
-> Fix4 (Instr o) (x : (x -> x) : xs) n r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Fix4 (Instr o) (x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a
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 (Fix4 (Instr o) (x : xs) n r a
 -> Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a)
-> (Fix4 (Instr o) xs n r a -> Fix4 (Instr o) (x : xs) n r a)
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) (x : (x -> x) : xs) n r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o (Fix4 (Instr o)) (x : xs) n r a
-> Fix4 (Instr o) (x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Instr o (Fix4 (Instr o)) (x : xs) n r a
 -> Fix4 (Instr o) (x : xs) n r a)
-> (Fix4 (Instr o) xs n r a
    -> Instr o (Fix4 (Instr o)) (x : xs) n r a)
-> Fix4 (Instr o) xs n r a
-> Fix4 (Instr o) (x : xs) n r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ΣVar x
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
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 :: ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Make ΣVar x
σ = ΣVar x -> Access -> k xs n r a -> Instr o k (x : xs) n r a
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k xs n r a -> Instr o k (x : 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 :: ΣVar x -> k xs n r a -> Instr o k (x : xs) n r a
_Put ΣVar x
σ = ΣVar x -> Access -> k xs n r a -> Instr o k (x : xs) n r a
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k xs n r a -> Instr o k (x : 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 :: ΣVar x -> k (x : xs) n r a -> Instr o k xs n r a
_Get ΣVar x
σ = ΣVar x -> Access -> k (x : xs) n r a -> Instr o k xs n r a
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k (x : xs) n r a -> Instr o k xs n r a
Get ΣVar x
σ Access
Hard

-- This this is a nice little trick to get this instruction to generate optimised code
_If :: Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a -> Instr o (Fix4 (Instr o)) (Bool : xs) n r a
_If :: Fix4 (Instr o) xs n r a
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) (Bool : xs) n r a
_If Fix4 (Instr o) xs n r a
t Fix4 (Instr o) xs n r a
e = [Defunc (Bool -> Bool)]
-> [Fix4 (Instr o) xs n r a]
-> Fix4 (Instr o) xs n r a
-> Instr o (Fix4 (Instr o)) (Bool : xs) n r a
forall y (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
[Defunc (y -> Bool)]
-> [k xs n r a] -> k xs n r a -> Instr o k (y : xs) n r a
Choices [Defunc (Bool -> Bool) -> Defunc (Bool -> Bool)
forall a. Defunc a -> Defunc a
user Defunc (Bool -> Bool)
forall a. Defunc (a -> a)
ID] [Fix4 (Instr o) xs n r a
t] Fix4 (Instr o) xs n r a
e

instance IFunctor4 (Instr o) where
  imap4 :: (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                 = Instr o b i j k x
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)          = Defunc x -> b (x : i) j k x -> Instr o b i j k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
Defunc x -> k (x : xs) n r a -> Instr o k xs n r a
Push Defunc x
x (a (x : i) j k x -> b (x : i) j k 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)             = b xs j k x -> Instr o b (x : xs) j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
       (n :: Nat) r a o x.
k xs n r a -> Instr o k (x : xs) n r a
Pop (a xs j k x -> b xs j k x
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)         = Defunc (x -> y -> z)
-> b (z : xs) j k x -> Instr o b (y : x : xs) j k x
forall x y z (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
Defunc (x -> y -> z)
-> k (z : xs) n r a -> Instr o k (y : x : xs) n r a
Lift2 Defunc (x -> y -> z)
g (a (z : xs) j k x -> b (z : xs) j k x
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 Defunc (Char -> Bool)
g a (Char : i) ('Succ n) k x
k)           = Defunc (Char -> Bool)
-> b (Char : i) ('Succ n) k x -> Instr o b i ('Succ n) k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
       (n :: Nat) r a o.
Defunc (Char -> Bool)
-> k (Char : xs) ('Succ n) r a -> Instr o k xs ('Succ n) r a
Sat Defunc (Char -> Bool)
g (a (Char : i) ('Succ n) k x -> b (Char : i) ('Succ n) k x
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)          = MVar x -> b (x : i) ('Succ n) k x -> Instr o b i ('Succ n) k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
MVar x -> k (x : xs) ('Succ n) r a -> Instr o k xs ('Succ n) r a
Call MVar x
μ (a (x : i) ('Succ n) k x -> b (x : i) ('Succ n) k 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
_ (Jump MVar k
μ)            = MVar k -> Instr o b '[] ('Succ n) k x
forall x o (k :: [Type] -> Nat -> Type -> Type -> Type) (n :: Nat)
       a.
MVar x -> Instr o k '[] ('Succ n) x a
Jump MVar 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                = Instr o b i j k x
forall o (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a.
Instr o k xs ('Succ n) 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)          = b i n k x -> Instr o b i ('Succ n) k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
       (n :: Nat) r a o.
k xs n r a -> Instr o k xs ('Succ n) r a
Commit (a i n k x -> b i n k x
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 a (o : i) j k x
h)         = b i ('Succ j) k x -> b (o : i) j k x -> Instr o b i j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
       (n :: Nat) r a o.
k xs ('Succ n) r a -> k (o : xs) n r a -> Instr o k xs n r a
Catch (a i ('Succ j) k x -> b i ('Succ j) k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i ('Succ j) k x
p) (a (o : i) j k x -> b (o : i) j k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f 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)            = b (o : i) j k x -> Instr o b i j k x
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 (a (o : i) j k x -> b (o : i) j k x
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)            = b xs j k x -> Instr o b (o : xs) j k x
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 (a xs j k x -> b xs j k x
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)          = b (x : xs) j k x
-> b (y : xs) j k x -> Instr o b (Either x y : xs) j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) x
       (xs :: [Type]) (n :: Nat) r a y o.
k (x : xs) n r a
-> k (y : xs) n r a -> Instr o k (Either x y : xs) n r a
Case (a (x : xs) j k x -> b (x : xs) j k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a (x : xs) j k x
p) (a (y : xs) j k x -> b (y : xs) j k x
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) = [Defunc (x -> Bool)]
-> [b xs j k x] -> b xs j k x -> Instr o b (x : xs) j k x
forall y (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
[Defunc (y -> Bool)]
-> [k xs n r a] -> k xs n r a -> Instr o k (y : xs) n r a
Choices [Defunc (x -> Bool)]
fs ((a xs j k x -> b xs j k x) -> [a xs j k x] -> [b xs j k x]
forall a b. (a -> b) -> [a] -> [b]
map a xs j k x -> b xs j k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f [a xs j k x]
ks) (a xs j k x -> b xs j k x
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 a (o : i) j k x
h)        = MVar Void
-> b '[] One Void x -> b (o : i) j k x -> Instr o b i j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) a o
       (xs :: [Type]) (n :: Nat) r.
MVar Void
-> k '[] One Void a -> k (o : xs) n r a -> Instr o k xs n r a
Iter MVar Void
μ (a '[] One Void x -> b '[] One Void x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a '[] One Void x
l) (a (o : i) j k x -> b (o : i) j k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f 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
φ)            = ΦVar x -> Instr o b (x : xs) j k x
forall x o (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a.
ΦVar x -> Instr o k (x : 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)      = ΦVar x -> b (x : i) j k x -> b i j k x -> Instr o b i j k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΦVar x -> k (x : xs) n r a -> k xs n r a -> Instr o k xs n r a
MkJoin ΦVar x
φ (a (x : i) j k x -> b (x : i) j k 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) (a i j k x -> b i j k x
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)            = b (x : y : xs) j k x -> Instr o b (y : x : xs) j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) x y
       (xs :: [Type]) (n :: Nat) r a o.
k (x : y : xs) n r a -> Instr o k (y : x : xs) n r a
Swap (a (x : y : xs) j k x -> b (x : y : xs) j k x
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)             = b (x : x : xs) j k x -> Instr o b (x : xs) j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) x
       (xs :: [Type]) (n :: Nat) r a o.
k (x : x : xs) n r a -> Instr o k (x : xs) n r a
Dup (a (x : x : xs) j k x -> b (x : x : xs) j k x
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)        = ΣVar x -> Access -> b xs j k x -> Instr o b (x : xs) j k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k xs n r a -> Instr o k (x : xs) n r a
Make ΣVar x
σ Access
a (a xs j k x -> b xs j k x
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)         = ΣVar x -> Access -> b (x : i) j k x -> Instr o b i j k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k (x : xs) n r a -> Instr o k xs n r a
Get ΣVar x
σ Access
a (a (x : i) j k x -> b (x : i) j k 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 (Put ΣVar x
σ Access
a a xs j k x
k)         = ΣVar x -> Access -> b xs j k x -> Instr o b (x : xs) j k x
forall x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
ΣVar x -> Access -> k xs n r a -> Instr o k (x : xs) n r a
Put ΣVar x
σ Access
a (a xs j k x -> b xs j k x
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 (LogEnter String
name a i ('Succ ('Succ n)) k x
k)   = String -> b i ('Succ ('Succ n)) k x -> Instr o b i ('Succ n) k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type])
       (n :: Nat) r a o.
String -> k xs ('Succ ('Succ n)) r a -> Instr o k xs ('Succ n) r a
LogEnter String
name (a i ('Succ ('Succ n)) k x -> b i ('Succ ('Succ n)) k x
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)    = String -> b i j k x -> Instr o b i j k x
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 (a i j k x -> b i j k x
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)     = MetaInstr j -> b i j k x -> Instr o b i j k x
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 (a i j k x -> b i j k x
forall (i' :: [Type]) (j' :: Nat) k'. a i' j' k' x -> b i' j' k' x
f a i j k x
k)

instance Show (Fix4 (Instr o) xs n r a) where
  show :: Fix4 (Instr o) xs n r a -> String
show = (ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ String
"") (ShowS -> String)
-> (Fix4 (Instr o) xs n r a -> ShowS)
-> Fix4 (Instr o) xs n r a
-> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 (Const4 ShowS xs n r a -> ShowS)
-> (Fix4 (Instr o) xs n r a -> Const4 ShowS xs n r a)
-> Fix4 (Instr o) xs n r a
-> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (i' :: [Type]) (j' :: Nat) k'.
 Instr o (Const4 ShowS) i' j' k' a -> Const4 ShowS i' j' k' a)
-> Fix4 (Instr o) xs n r a -> Const4 ShowS 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 (ShowS -> Const4 ShowS i' j' k' a
forall k1 k2 k3 k5 a (i :: k1) (j :: k2) (k4 :: k3) (l :: k5).
a -> Const4 a i j k4 l
Const4 (ShowS -> Const4 ShowS i' j' k' a)
-> (Instr o (Const4 ShowS) i' j' k' a -> ShowS)
-> Instr o (Const4 ShowS) i' j' k' a
-> Const4 ShowS i' j' k' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o (Const4 ShowS) i' j' k' a -> ShowS
forall (xs :: [Type]) (n :: Nat) r a.
Instr o (Const4 ShowS) xs n r a -> ShowS
alg)
    where
      alg :: forall xs n r a. Instr o (Const4 (String -> String)) xs n r a -> String -> String
      alg :: Instr o (Const4 ShowS) xs n r a -> ShowS
alg Instr o (Const4 ShowS) xs n r a
Ret                 = ShowS
"Ret"
      alg (Call MVar x
μ Const4 ShowS (x : xs) ('Succ n) r a
k)          = ShowS
"(Call " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MVar x -> ShowS
forall a. Show a => a -> ShowS
shows MVar x
μ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : xs) ('Succ n) r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : xs) ('Succ n) r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Jump MVar r
μ)            = ShowS
"(Jump " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MVar r -> ShowS
forall a. Show a => a -> ShowS
shows MVar r
μ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Push Defunc x
x Const4 ShowS (x : xs) n r a
k)          = ShowS
"(Push " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defunc x -> ShowS
forall a. Show a => a -> ShowS
shows Defunc x
x ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Pop Const4 ShowS xs n r a
k)             = ShowS
"(Pop " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Lift2 Defunc (x -> y -> z)
f Const4 ShowS (z : xs) n r a
k)         = ShowS
"(Lift2 " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defunc (x -> y -> z) -> ShowS
forall a. Show a => a -> ShowS
shows Defunc (x -> y -> z)
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (z : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (z : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Sat Defunc (Char -> Bool)
f Const4 ShowS (Char : xs) ('Succ n) r a
k)           = ShowS
"(Sat " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Defunc (Char -> Bool) -> ShowS
forall a. Show a => a -> ShowS
shows Defunc (Char -> Bool)
f ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (Char : xs) ('Succ n) r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (Char : xs) ('Succ n) r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg Instr o (Const4 ShowS) xs n r a
Empt                = ShowS
"Empt"
      alg (Commit Const4 ShowS xs n r a
k)          = ShowS
"(Commit " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Catch Const4 ShowS xs ('Succ n) r a
p Const4 ShowS (o : xs) n r a
h)         = ShowS
"(Catch " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs ('Succ n) r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs ('Succ n) r a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (o : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (o : xs) n r a
h ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Tell Const4 ShowS (o : xs) n r a
k)            = ShowS
"(Tell " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (o : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (o : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Seek Const4 ShowS xs n r a
k)            = ShowS
"(Seek " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Case Const4 ShowS (x : xs) n r a
p Const4 ShowS (y : xs) n r a
q)          = ShowS
"(Case " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : xs) n r a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (y : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (y : xs) n r a
q ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Choices [Defunc (x -> Bool)]
fs [Const4 ShowS xs n r a]
ks Const4 ShowS xs n r a
def) = ShowS
"(Choices " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Defunc (x -> Bool)] -> ShowS
forall a. Show a => a -> ShowS
shows [Defunc (x -> Bool)]
fs ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" [" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [ShowS] -> ShowS
forall a. (a -> a) -> [a -> a] -> a -> a
intercalateDiff ShowS
", " ((Const4 ShowS xs n r a -> ShowS)
-> [Const4 ShowS xs n r a] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 [Const4 ShowS xs n r a]
ks) ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
"] " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
def ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Iter MVar Void
μ Const4 ShowS '[] One Void a
l Const4 ShowS (o : xs) n r a
h)        = ShowS
"{Iter " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MVar Void -> ShowS
forall a. Show a => a -> ShowS
shows MVar Void
μ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS '[] One Void a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS '[] One Void a
l ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (o : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (o : xs) n r a
h ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
"}"
      alg (Join ΦVar x
φ)            = ΦVar x -> ShowS
forall a. Show a => a -> ShowS
shows ΦVar x
φ
      alg (MkJoin ΦVar x
φ Const4 ShowS (x : xs) n r a
p Const4 ShowS xs n r a
k)      = ShowS
"(let " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ΦVar x -> ShowS
forall a. Show a => a -> ShowS
shows ΦVar x
φ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" = " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : xs) n r a
p ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" in " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Swap Const4 ShowS (x : y : xs) n r a
k)            = ShowS
"(Swap " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : y : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : y : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Dup Const4 ShowS (x : x : xs) n r a
k)             = ShowS
"(Dup " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : x : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : x : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Make ΣVar x
σ Access
a Const4 ShowS xs n r a
k)        = ShowS
"(Make " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ΣVar x -> ShowS
forall a. Show a => a -> ShowS
shows ΣVar x
σ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> ShowS
forall a. Show a => a -> ShowS
shows Access
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Get ΣVar x
σ Access
a Const4 ShowS (x : xs) n r a
k)         = ShowS
"(Get " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ΣVar x -> ShowS
forall a. Show a => a -> ShowS
shows ΣVar x
σ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> ShowS
forall a. Show a => a -> ShowS
shows Access
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS (x : xs) n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS (x : xs) n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (Put ΣVar x
σ Access
a Const4 ShowS xs n r a
k)         = ShowS
"(Put " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ΣVar x -> ShowS
forall a. Show a => a -> ShowS
shows ΣVar x
σ ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Access -> ShowS
forall a. Show a => a -> ShowS
shows Access
a ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
" " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
")"
      alg (LogEnter String
_ Const4 ShowS xs ('Succ ('Succ n)) r a
k)      = Const4 ShowS xs ('Succ ('Succ n)) r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs ('Succ ('Succ n)) r a
k
      alg (LogExit String
_ Const4 ShowS xs n r a
k)       = Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k
      alg (MetaInstr MetaInstr n
m Const4 ShowS xs n r a
k)     = ShowS
"[" ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInstr n -> ShowS
forall a. Show a => a -> ShowS
shows MetaInstr n
m ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS
"] " ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 ShowS xs n r a -> ShowS
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 ShowS xs n r a
k

instance Show (MetaInstr n) where
  show :: MetaInstr n -> String
show (AddCoins Int
n)    = String
"Add " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (RefundCoins Int
n) = String
"Refund " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (DrainCoins Int
n)  = String
"Using " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"