{-# LANGUAGE OverloadedStrings,
             PatternSynonyms,
             DerivingStrategies #-}
{-|
Module      : Parsley.Internal.Backend.Machine.Instructions
Description : Core instructions that make up a low-level parser.
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

This contains the instructions and satelite datatypes for representing
parsers at the lowest CPS-form level. These are indexed by multiple types,
which are documented in the source (if not on Haddock!).

@since 1.0.0.0
-}
module Parsley.Internal.Backend.Machine.Instructions (
    -- * Main Instructions
    Instr(..),
    -- * Auxilliary Types
    Handler(..),
    Access(..),
    MetaInstr(..),
    -- * Smart Instructions
    _App, _Fmap, _Modify, _Make, _Put, _Get,
    -- * Smart Meta-Instructions
    addCoins, refundCoins, drainCoins, giveBursary, prefetchChar, blockCoins
  ) 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(Coins))
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)

{-|
This represents the instructions of the machine, in CPS form as an indexed functor.

When an instruction has a `Succ` in the type, it indicates that it is capable of failing.

@since 1.4.0.0
-}
data Instr (o :: Type)                                  -- The FIXED input type
           (k :: [Type] -> Nat -> Type -> Type -> Type) -- The FIXED continuation parameter
           (xs :: [Type])                               -- The VARIABLE type defining the required types on the stack on entry
           (n :: Nat)                                   -- The VARIABLE type defining how many handlers are required on entry
           (r :: Type)                                  -- The VARIABLE intermediate type defining what value this parser immediately produces
           (a :: Type)                                  -- The (technically VARIABLE) type specifying the final result of the parser
  where
  {-| This instruction returns from either calls or the entire parser at the top-level.

  @since 1.0.0.0 -}
  Ret       :: Instr o k '[x] n x a {- ^ -}
  {-| Pushes a value onto the stack, which is required by the continuation parameter.

  @since 1.0.0.0 -}
  Push      :: Machine.Defunc x {- ^ Value to push. -} -> k (x : xs) n r a {- ^ Machine requiring value. -} -> Instr o k xs n r a
  {-| Removes a value from the stack, so it is the correct shape for the continuation parameter.

  @since 1.0.0.0 -}
  Pop       :: k xs n r a {- ^ -} -> Instr o k (x : xs) n r a
  {-| Applies a function to the top two elements of the stack, converting them to something else and pushing it back on.

  @since 1.0.0.0 -}
  Lift2     :: Machine.Defunc (x -> y -> z) {- ^ Function to apply. -}
            -> k (z : xs) n r a             {- ^ Machine requiring new value. -}
            -> Instr o k (y : x : xs) n r a
  {-| Reads a character so long as it matches a given predicate. If it does not, or no input is available, this instruction fails.

  @since 1.0.0.0 -}
  Sat       :: Machine.Defunc (Char -> Bool) {- ^ Predicate to apply. -}
            -> k (Char : xs) (Succ n) r a    {- ^ Machine requiring read character. -}
            -> Instr o k xs (Succ n) r a
  {-| Calls another let-bound parser.

  @since 1.0.0.0 -}
  Call      :: MVar x                  {- ^ The binding to invoke. -}
            -> k (x : xs) (Succ n) r a {- ^ Continuation to do after the call. -}
            -> Instr o k xs (Succ n) r a
  {-| Jumps to another let-bound parser tail-recursively.

  @since 1.0.0.0 -}
  Jump      :: MVar x {- ^ The binding to jump to. -} -> Instr o k '[] (Succ n) x a
  {-| Fails unconditionally.

  @since 1.0.0.0 -}
  Empt      :: Instr o k xs (Succ n) r a {- ^ -}
  {-| Discards a failure handler, so that it is no longer in scope.

  @since 1.0.0.0 -}
  Commit    :: k xs n r a {- ^ Next machine, which will /not/ require the discarded handler. -} -> Instr o k xs (Succ n) r a
  {-| Registers a handler to deal with possible failure in the given machine.

  @since 1.4.0.0 -}
  Catch     :: k xs (Succ n) r a          {- ^ Machine where failure is handled by the handler. -}
            -> Handler o k (o : xs) n r a {- ^ The handler to register. -}
            -> Instr o k xs n r a
  {-| Pushes the current input offset onto the stack.

  @since 1.0.0.0 -}
  Tell      :: k (o : xs) n r a {- ^ The machine that accepts the input. -} -> Instr o k xs n r a
  {-| Pops the input offset off of the stack and makes that the current input offset.

  @since 1.0.0.0 -}
  Seek      :: k xs n r a {- ^ Machine to continue with new input. -} -> Instr o k (o : xs) n r a
  {-| Picks one of two continuations based on whether a `Left` or `Right` is on the stack.

  @since 1.0.0.0 -}
  Case      :: k (x : xs) n r a {- ^ Machine to execute if `Left` on stack. -}
            -> k (y : xs) n r a {- ^ Machine to execute if `Right` on stack. -}
            -> Instr o k (Either x y : xs) n r a
  {-| Given a collection of predicates and machines, this instruction will execute the first machine
      for which the corresponding predicate returns true for the value on the top of the stack.

  @since 1.0.0.0 -}
  Choices   :: [Machine.Defunc (x -> Bool)] {- ^ A list of predicates to try. -}
            -> [k xs n r a]                 {- ^ A corresponding list of machines. -}
            -> k xs n r a                   {- ^ A default machine to execute if no predicates match. -}
            -> Instr o k (x : xs) n r a
  {-| Sets up an iteration, where the second argument is executed repeatedly until it fails, which is
      handled by the given handler. The use of `Void` indicates that `Ret` is illegal within the loop.

  @since 1.0.0.0 -}
  Iter      :: MVar Void                  {- ^ The name of the binding. -}
            -> k '[] One Void a           {- ^ The body of the loop: it cannot return "normally". -}
            -> Handler o k (o : xs) n r a {- ^ The handler for the loop's exit. -}
            -> Instr o k xs n r a
  {-| Jumps to a given join point.

  @since 1.0.0.0 -}
  Join      :: ΦVar x {- ^ The join point to jump to. -} -> Instr o k (x : xs) n r a
  {-| Sets up a new join point binding.

  @since 1.0.0.0 -}
  MkJoin    :: ΦVar x           {- ^ The name of the binding that can be referred to later. -}
            -> k (x : xs) n r a {- ^ The body of the join point binding. -}
            -> k xs n r a       {- ^ The scope within which the binding is valid.  -}
            -> Instr o k xs n r a
  {-| Swaps the top two elements on the stack

  @since 1.0.0.0 -}
  Swap      :: k (x : y : xs) n r a {- ^ The machine that requires the reversed stack. -} -> Instr o k (y : x : xs) n r a
  {-| Duplicates the top value on the stack. May produce a let-binding.

  @since 1.0.0.0 -}
  Dup       :: k (x : x : xs) n r a {- ^ Machine that requires doubled element. -} -> Instr o k (x : xs) n r a
  {-| Initialises a new register for use within the continuation. Initial value is on the stack.

  @since 1.0.0.0 -}
  Make      :: ΣVar x     {- ^ The name of the new register. -}
            -> Access     {- ^ Whether or not the register is "concrete". -}
            -> k xs n r a {- ^ The scope within which the register is accessible. -}
            -> Instr o k (x : xs) n r a
  {-| Pushes the value contained within a register onto the stack.

  @since 1.0.0.0 -}
  Get       :: ΣVar x           {- ^ Name of the register to read. -}
            -> Access           {- ^ Whether or not the value is cached. -}
            -> k (x : xs) n r a {- ^ The machine that requires the value. -}
            -> Instr o k xs n r a
  {-| Places the value on the top of the stack into a given register.

  @since 1.0.0.0 -}
  Put       :: ΣVar x     {- ^ Name of the register to update. -}
            -> Access     {- ^ Whether or not the value needs to be stored in a concrete register. -}
            -> k xs n r a
            -> Instr o k (x : xs) n r a
  {-| Begins a debugging scope, the inner scope requires /two/ handlers,
      the first is the log handler itself, and then the second is the
      "real" fail handler for when the log handler is executed.

  @since 1.0.0.0 -}
  LogEnter  :: String                   {- ^ The message to be printed. -}
            -> k xs (Succ (Succ n)) r a {- ^ The machine to be debugged. -}
            -> Instr o k xs (Succ n) r a
  {-| Ends the log scope after a succesful execution.

  @since 1.0.0.0 -}
  LogExit   :: String     {- ^ The message to be printed. -}
            -> k xs n r a {- ^ The machine that follows. -}
            -> Instr o k xs n r a
  {-| Executes a meta-instruction, which is interacting with
      implementation specific static information.

  @since 1.0.0.0 -}
  MetaInstr :: MetaInstr n {- ^ A meta-instruction to perform. -}
            -> k xs n r a  {- ^ The machine that follows. -}
            -> Instr o k xs n r a

{-|
There are two types of organic handlers within parsley, which are
captured by this type, which is also an IFunctor and wraps around
`Instr`.

@since 1.4.0.0
-}
data Handler (o :: Type) (k :: [Type] -> Nat -> Type -> Type -> Type) (xs :: [Type]) (n :: Nat) (r :: Type) (a :: Type) where
  {-| These handlers have two distinct behaviours depending on whether the
      captured offset matches the current offset or not.

  @since 1.4.0.0 -}
  Same :: k xs n r a       -- ^ Execute when the input matches, notice that the captured offset is discarded since it is equal to the current.
       -> k (o : xs) n r a -- ^ Execute when the input does not match, the resulting behaviour could use the captured or current input.
       -> Handler o k (o : xs) n r a
  {-| These handlers are unconditional on the input, and will always do the same
      thing regardless of the input provided.

  @since 1.4.0.0 -}
  Always :: k (o : xs) n r a -> Handler o k (o : xs) n r a

{-|
This determines whether or not an interaction with an register should be materialised
in the generated code or not.

@since 1.0.0.0
-}
data Access = Hard -- ^ Register exists at runtime and this interaction will use it.
            | Soft -- ^ Register may not exist, and the interaction should be with cache regardless.
            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

{-|
These are meta-instructions, which interact with static information to direct the
code-generation process. They are not formally part of parsley's semantics and can
be omitted from an implementation without consequence.

@since 1.0.0.0
-}
data MetaInstr (n :: Nat) where
  {-| Adds coins to the piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information).
      If there are coins already available, add a piggy-bank, otherwise generate a length check and add the coins.

      A handler is required, in case the length check fails.

  @since 1.5.0.0 -}
  AddCoins    :: Coins -> MetaInstr (Succ n)
  {-| Refunds to the piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information).
      This always happens for free, and is added straight to the coins.

  @since 1.5.0.0 -}
  RefundCoins :: Coins -> MetaInstr n
  {-| Remove coins from piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information)
      This is used to pay for more expensive calls to bindings with known required input.

      A handler is required, as there may not be enough coins to pay the cost and a length check causes a failure.

  @since 1.5.0.0 -}
  DrainCoins  :: Coins -> MetaInstr (Succ n)
  {-| Refunds to the piggy-bank system (see "Parsley.Internal.Backend.Machine.Types.Context" for more information).
      This always happens for free, and is added straight to the coins. Unlike `RefundCoins` this cannot reclaim
      input, nor is is subtractive in the analysis.

  @since 1.5.0.0 -}
  GiveBursary :: Coins -> MetaInstr n
  {-| Fetches a character to read in advance. This is used to factor out a common token from alternatives.
      The boolean argument represents whether or not the read is covered by a factored length check, or
      requires its own.

  @since 1.5.0.0 -}
  PrefetchChar :: Bool -> MetaInstr (Succ n)
  {-|
  True meta instruction: does /nothing/ except for reset coin count during coin analysis.

  @since 1.6.0.0
  -}
  BlockCoins :: MetaInstr n

mkCoin :: (Coins -> MetaInstr n) -> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin :: (Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
mkCoin Coins -> MetaInstr n
_    (Coins Int
0 Int
0) = Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
forall a. a -> a
id
mkCoin Coins -> MetaInstr n
meta Coins
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 (Coins -> MetaInstr n
meta Coins
n)

{-|
Smart-constuctor around `AddCoins`.

@since 1.5.0.0
-}
addCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
addCoins :: Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
addCoins (Coins Int
1 Int
1) = Fix4 (Instr o) xs ('Succ n) r a -> Fix4 (Instr o) xs ('Succ n) r a
forall a. a -> a
id
addCoins Coins
coins       = (Coins -> MetaInstr ('Succ n))
-> Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
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 ('Succ n)
forall (n :: Nat). Coins -> MetaInstr ('Succ n)
AddCoins Coins
coins

{-|
Smart-constuctor around `RefundCoins`.

@since 1.5.0.0
-}
refundCoins :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
refundCoins = (Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
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
forall (n :: Nat). Coins -> MetaInstr n
RefundCoins

{-|
Smart-constuctor around `DrainCoins`.

@since 1.5.0.0
-}
drainCoins :: Coins -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
drainCoins :: Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
drainCoins = (Coins -> MetaInstr ('Succ n))
-> Coins
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
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 ('Succ n)
forall (n :: Nat). Coins -> MetaInstr ('Succ n)
DrainCoins

{-|
Smart-constuctor around `RefundCoins`.

@since 1.5.0.0
-}
giveBursary :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
giveBursary :: Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
giveBursary = (Coins -> MetaInstr n)
-> Coins -> Fix4 (Instr o) xs n r a -> Fix4 (Instr o) xs n r a
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
forall (n :: Nat). Coins -> MetaInstr n
GiveBursary

{-|
Smart-constructor around `PrefetchChar`.

@since 1.5.0.0
-}
prefetchChar :: Bool -> Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
prefetchChar :: Bool
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
prefetchChar Bool
check = Instr o (Fix4 (Instr o)) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ 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 ('Succ n) r a
 -> Fix4 (Instr o) xs ('Succ n) r a)
-> (Fix4 (Instr o) xs ('Succ n) r a
    -> Instr o (Fix4 (Instr o)) xs ('Succ n) r a)
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInstr ('Succ n)
-> Fix4 (Instr o) xs ('Succ n) r a
-> Instr o (Fix4 (Instr o)) xs ('Succ 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 (Bool -> MetaInstr ('Succ n)
forall (n :: Nat). Bool -> MetaInstr ('Succ n)
PrefetchChar Bool
check)

{-|
Smart-constructor around `PrefetchChar`.

@since 1.6.0.0
-}
blockCoins :: Fix4 (Instr o) xs (Succ n) r a -> Fix4 (Instr o) xs (Succ n) r a
blockCoins :: Fix4 (Instr o) xs ('Succ n) r a -> Fix4 (Instr o) xs ('Succ n) r a
blockCoins = Instr o (Fix4 (Instr o)) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ 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 ('Succ n) r a
 -> Fix4 (Instr o) xs ('Succ n) r a)
-> (Fix4 (Instr o) xs ('Succ n) r a
    -> Instr o (Fix4 (Instr o)) xs ('Succ n) r a)
-> Fix4 (Instr o) xs ('Succ n) r a
-> Fix4 (Instr o) xs ('Succ n) r a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MetaInstr ('Succ n)
-> Fix4 (Instr o) xs ('Succ n) r a
-> Instr o (Fix4 (Instr o)) xs ('Succ 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 MetaInstr ('Succ n)
forall (n :: Nat). MetaInstr n
BlockCoins

{-|
Applies a value on the top of the stack to a function on the second-most top of the stack.

@since 1.0.0.0
-}
_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 = 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)

{-|
Adjusts the value on the top of the stack with the given function.

@since 1.0.0.0
-}
_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))

{-|
Updates the value in a given register using the function on the top of the stack.

@since 1.0.0.0
-}
_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
σ

{-|
Smart-instruction for `Make` that uses a `Hard` access.

@since 1.0.0.0
-}
_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

{-|
Smart-instruction for `Put` that uses a `Hard` access.

@since 1.0.0.0
-}
_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

{-|
Smart-instruction for `Get` that uses a `Hard` access.

@since 1.0.0.0
-}
_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

-- Instances
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 Handler o a (o : i) j k x
h)         = b i ('Succ j) k x -> Handler o 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
-> Handler o 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) ((forall (i' :: [Type]) (j' :: Nat) k'.
 a i' j' k' x -> b i' j' k' x)
-> Handler o a (o : i) j k x -> Handler o b (o : i) j k x
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)            = 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 x o.
k (x : xs) n r a
-> k (x : xs) n r a -> Instr o k (Either x x : 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 x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a o.
[Defunc (x -> Bool)]
-> [k xs n r a] -> k xs n r a -> Instr o k (x : 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 Handler o a (o : i) j k x
h)        = MVar Void
-> b '[] One Void x
-> Handler o 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
-> Handler o 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) ((forall (i' :: [Type]) (j' :: Nat) k'.
 a i' j' k' x -> b i' j' k' x)
-> Handler o a (o : i) j k x -> Handler o b (o : i) j k x
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
φ)            = Φ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 IFunctor4 (Handler o) where
  imap4 :: (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 a xs j k x
yes a (o : xs) j k x
no) = b xs j k x -> b (o : xs) j k x -> Handler 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 -> k (o : xs) n r a -> Handler o k (o : xs) n r a
Same (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
yes) (a (o : xs) j k x -> b (o : xs) j k x
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 a (o : xs) j k x
k)    = b (o : xs) j k x -> Handler o b (o : xs) j k x
forall (k :: [Type] -> Nat -> Type -> Type -> Type) o
       (xs :: [Type]) (n :: Nat) r a.
k (o : xs) n r a -> Handler o k (o : xs) n r a
Always (a (o : xs) j k x -> b (o : xs) j k x
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 = (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 Handler o (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
. Handler o (Const4 ShowS) (o : xs) n r a -> ShowS
forall a. Show a => a -> ShowS
shows Handler o (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 Handler o (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
. Handler o (Const4 ShowS) (o : xs) n r a -> ShowS
forall a. Show a => a -> ShowS
shows Handler o (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
BlockCoins 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 (Handler o (Const4 (String -> String)) (o : xs) n r a) where
  show :: Handler o (Const4 ShowS) (o : xs) n r a -> String
show (Same Const4 ShowS xs n r a
yes Const4 ShowS (o : xs) n r a
no) = ShowS
"(Dup (Tell (Lift2 same (If " (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
yes (ShowS
" " (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
no String
"))))")))
  show (Always Const4 ShowS (o : xs) n r a
k)    = 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 String
""

instance Show (MetaInstr n) where
  show :: MetaInstr n -> String
show (AddCoins Coins
n)     = String
"Add " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Coins -> String
forall a. Show a => a -> String
show Coins
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (RefundCoins Coins
n)  = String
"Refund " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Coins -> String
forall a. Show a => a -> String
show Coins
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (DrainCoins Coins
n)   = String
"Using " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Coins -> String
forall a. Show a => a -> String
show Coins
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (GiveBursary Coins
n)  = String
"Bursary of " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Coins -> String
forall a. Show a => a -> String
show Coins
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" coins"
  show (PrefetchChar Bool
b) = String
"Prefetch character " String -> ShowS
forall a. [a] -> [a] -> [a]
++ (if Bool
b then String
"with" else String
"without") String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" length-check"
  show MetaInstr n
BlockCoins       = String
""