-- SPDX-FileCopyrightText: 2021 Oxhead Alpha
-- SPDX-License-Identifier: LicenseRef-MIT-OA

-- NOTE this pragmas.
-- We disable some wargnings for the sake of speed up.
-- Write code with care.
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

-- | Optimizer for typed instructions.
--
-- It's quite experimental and incomplete.

module Morley.Michelson.Optimizer
  ( optimize
  , optimizeWithConf
  , defaultOptimizerConf
  , defaultRules
  , defaultRulesAndPushPack
  , orRule
  , orSimpleRule
  , Rule (..)
  , OptimizerConf (..)
  , ocGotoValuesL
  ) where

import Prelude hiding (EQ, GT, LT)

import Control.Lens (makeLensesFor)
import Data.Constraint (Dict(..))
import Data.Default (Default(def))
import Data.Singletons (sing)
import Data.Type.Equality ((:~:)(Refl))

import Morley.Michelson.Interpret.Pack (packValue')
import Morley.Michelson.Typed.Aliases (Value)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Instr
import Morley.Michelson.Typed.Scope (ConstantScope, PackedValScope, checkScope)
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Util (DfsSettings(..), dfsModifyInstr)
import Morley.Michelson.Typed.Value
import Morley.Util.PeanoNatural

----------------------------------------------------------------------------
-- High level
----------------------------------------------------------------------------

data OptimizerConf = OptimizerConf
  { OptimizerConf -> Bool
ocGotoValues :: Bool
  , OptimizerConf -> [Rule]
ocRuleset    :: [Rule]
  }

-- | Default config - all commonly useful rules will be applied to all the code.
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf :: OptimizerConf
defaultOptimizerConf = OptimizerConf :: Bool -> [Rule] -> OptimizerConf
OptimizerConf
  { ocGotoValues :: Bool
ocGotoValues = Bool
True
  , ocRuleset :: [Rule]
ocRuleset    = [Rule]
defaultRules
  }

instance Default OptimizerConf where
  def :: OptimizerConf
def = OptimizerConf
defaultOptimizerConf

-- | Optimize a typed instruction by replacing some sequences of
-- instructions with smaller equivalent sequences.
-- Applies default set of rewrite rules.
optimize :: Instr inp out -> Instr inp out
optimize :: forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out
optimize = OptimizerConf -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf OptimizerConf
forall a. Default a => a
def

-- | Optimize a typed instruction using a custom set of rules.
-- The set is divided into several stages, as applying
-- some rules can prevent others to be performed.
optimizeWithConf :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf :: forall (inp :: [T]) (out :: [T]).
OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf (OptimizerConf Bool
ocGotoValues [Rule]
rules) Instr inp out
instr = (Instr inp out -> Element [Rule] -> Instr inp out)
-> Instr inp out -> [Rule] -> Instr inp out
forall t b. Container t => (b -> Element t -> b) -> b -> t -> b
foldl ((Rule -> Instr inp out -> Instr inp out)
-> Instr inp out -> Rule -> Instr inp out
forall a b c. (a -> b -> c) -> b -> a -> c
flip Rule -> Instr inp out -> Instr inp out
performOneStage) Instr inp out
instrRHS [Rule]
rules
  where
    dfsSettings :: DfsSettings Identity
dfsSettings = DfsSettings Identity
forall a. Default a => a
def{ dsGoToValues :: Bool
dsGoToValues = Bool
ocGotoValues }
    performOneStage :: Rule -> Instr inp out -> Instr inp out
performOneStage Rule
stageRules =
      DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall (inp :: [T]) (out :: [T]).
DfsSettings Identity
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
dfsModifyInstr DfsSettings Identity
dfsSettings ((forall (inp :: [T]) (out :: [T]). Instr inp out -> Instr inp out)
 -> Instr inp out -> Instr inp out)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Instr inp out)
-> Instr inp out
-> Instr inp out
forall a b. (a -> b) -> a -> b
$ Rule -> Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
stageRules
    instrRHS :: Instr inp out
instrRHS = Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce ((Rule -> Rule) -> Rule
fixpoint Rule -> Rule
flattenSeqLHS) Instr inp out
instr

----------------------------------------------------------------------------
-- Rewrite rules
----------------------------------------------------------------------------

-- Type of a single rewrite rule, wrapped in `newtype`. It takes an instruction
-- and tries to optimize its head (first few instructions). If optimization
-- succeeds, it returns `Just` the optimized instruction, otherwise it returns `Nothing`.
newtype Rule = Rule {Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule :: forall inp out. Instr inp out -> Maybe (Instr inp out)}

defaultRules :: [Rule]
defaultRules :: [Rule]
defaultRules = ((Rule -> Rule) -> Rule) -> [Rule -> Rule] -> [Rule]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
map (Rule -> Rule) -> Rule
fixpoint
  [ Rule -> Rule
mainStageRules
  , Rule -> Rule
glueAdjacentDropsStageRules
  ]
  where
    glueAdjacentDropsStageRules :: Rule -> Rule
glueAdjacentDropsStageRules = Rule -> Rule
flattenSeqLHS (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDrops

-- | We do not enable 'pushPack' rule by default because it is
-- potentially dangerous.
-- There are various code processing functions that may depend on constants,
-- e. g. string transformations.
-- need helper
defaultRulesAndPushPack :: [Rule]
defaultRulesAndPushPack :: [Rule]
defaultRulesAndPushPack =
  case [Rule]
defaultRules of
    -- Perhaps one day main rules will not be performed on the first stage.
    -- We need another way to add `pushPack` to `mainStageRules` in that case.
    Rule
_ : [Rule]
otherStagesRules -> do
      let mainStageRulesAndPushPack :: Rule
mainStageRulesAndPushPack = (Rule -> Rule) -> Rule
fixpoint ((Rule -> Rule) -> Rule) -> (Rule -> Rule) -> Rule
forall a b. (a -> b) -> a -> b
$ Rule -> Rule
mainStageRules (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pushPack
      Rule
mainStageRulesAndPushPack Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: [Rule]
otherStagesRules
    [Rule]
_ -> Text -> [Rule]
forall a. HasCallStack => Text -> a
error Text
"`defaultRules` should not be empty"

mainStageRules :: Rule -> Rule
mainStageRules :: Rule -> Rule
mainStageRules =
  Rule -> Rule
flattenSeqLHS
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
removeNesting
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
removeExtStackType
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dipDrop2swapDrop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
ifNopNop2Drop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
nopIsNeutralForSeq
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
variousNops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dupSwap2dup
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
noDipNeeded
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
branchShortCut
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
compareWithZero
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDrops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
internalNop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDips
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDups
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDips
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
isSomeOnIf
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
redundantIf
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
emptyDip
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
digDug
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
specificPush
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairUnpair
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairMisc
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
unpairMisc
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
swapBeforeCommutative
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
justDrops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
justDoubleDrops

flattenSeqLHS :: Rule -> Rule
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS Rule
toplevel = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  it :: Instr inp out
it@(Seq (Seq Instr inp b
_ Instr b b
_) Instr b out
_) -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
toplevel Instr inp out
it
  Instr inp out
_                    -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

removeNesting :: Rule
removeNesting :: Rule
removeNesting = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Nested Instr inp out
i -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i
  Instr inp out
_        -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

-- | STACKTYPE is currently a Nop and may safely be removed.
removeExtStackType :: Rule
removeExtStackType :: Rule
removeExtStackType = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Ext (STACKTYPE{}) -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp out
_                 -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

dipDrop2swapDrop :: Rule
dipDrop2swapDrop :: Rule
dipDrop2swapDrop = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  DIP Instr a c
DROP -> Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c))
forall a. a -> Maybe a
Just (Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c)))
-> Instr (b : a : c) (b : c) -> Maybe (Instr (b : a : c) (b : c))
forall a b. (a -> b) -> a -> b
$ Instr (b : a : c) (a : b : c)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr (b : a : c) (a : b : c)
-> Instr (a : b : c) (b : c) -> Instr (b : a : c) (b : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : c) (b : c)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp out
_        -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

ifNopNop2Drop :: Rule
ifNopNop2Drop :: Rule
ifNopNop2Drop = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  IF Instr s out
Nop Instr s out
Nop -> Instr ('TBool : out) out -> Maybe (Instr ('TBool : out) out)
forall a. a -> Maybe a
Just Instr ('TBool : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp out
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
Nop :# Instr b out
i   -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
i
  Instr inp b
i   :# Instr b out
Nop -> Instr inp b -> Maybe (Instr inp b)
forall a. a -> Maybe a
Just Instr inp b
i
  Instr inp out
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

variousNops :: Rule
variousNops :: Rule
variousNops = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
DUP                :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  DUPN PeanoNatural n
_             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
SWAP               :# Instr b b
SWAP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  PUSH Value' Instr t
_             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
NONE               :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
UNIT               :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
NIL                :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
EMPTY_SET          :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
EMPTY_MAP          :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
EMPTY_BIG_MAP      :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  LAMBDA IsNotInView => RemFail Instr '[i] '[o]
_           :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  SELF SomeEntrypointCallT arg
_             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
NOW                :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
AMOUNT             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
BALANCE            :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
TOTAL_VOTING_POWER :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
SOURCE             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
SENDER             :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
CHAIN_ID           :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
LEVEL              :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
SELF_ADDRESS       :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
READ_TICKET        :# Instr b b
DROP :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c

  Instr inp b
DUP                :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  DUPN PeanoNatural n
_             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
SWAP               :# Instr b out
SWAP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  PUSH Value' Instr t
_             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
NONE               :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
UNIT               :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
NIL                :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
EMPTY_SET          :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
EMPTY_MAP          :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
EMPTY_BIG_MAP      :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  LAMBDA IsNotInView => RemFail Instr '[i] '[o]
_           :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  SELF SomeEntrypointCallT arg
_             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
NOW                :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
AMOUNT             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
BALANCE            :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
TOTAL_VOTING_POWER :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
SOURCE             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
SENDER             :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
CHAIN_ID           :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
LEVEL              :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
SELF_ADDRESS       :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp b
READ_TICKET        :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp out
_                          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

dupSwap2dup :: Rule
dupSwap2dup :: Rule
dupSwap2dup = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
DUP :# Instr b b
SWAP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
DUP :# Instr b out
SWAP      -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP
  Instr inp out
_                -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

noDipNeeded :: Rule
noDipNeeded :: Rule
noDipNeeded = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  -- If we put a constant value on stack and then do something under it,
  -- we can do this "something" on original stack and then put that constant.
  PUSH Value' Instr t
x    :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c b
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t
x Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  PUSH Value' Instr t
x    :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c out
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t
x
  Instr inp b
UNIT      :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
UNIT      :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT
  Instr inp b
NOW       :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
NOW       :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW
  Instr inp b
SENDER    :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SENDER    :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER
  Instr inp b
EMPTY_MAP :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
EMPTY_MAP :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP
  Instr inp b
EMPTY_SET :# DIP Instr a c
f :# Instr b out
c -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c b
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET Instr c b -> Instr b out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
EMPTY_SET :# DIP Instr a c
f      -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a out -> Maybe (Instr a out))
-> Instr a out -> Maybe (Instr a out)
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET

  -- If we do something ignoring top of the stack and then immediately
  -- drop top of the stack, we can drop that item in advance and
  -- not use 'DIP' at all.
  DIP Instr a c
f :# Instr b b
DROP :# Instr b out
c -> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a. a -> Maybe a
Just (Instr (b : a) out -> Maybe (Instr (b : a) out))
-> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a b. (a -> b) -> a -> b
$ Instr (b : a) a
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : a) a -> Instr a out -> Instr (b : a) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr a c
f Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c out
Instr b out
c
  DIP Instr a c
f :# Instr b out
DROP         -> Instr (b : a) c -> Maybe (Instr (b : a) c)
forall a. a -> Maybe a
Just (Instr (b : a) c -> Maybe (Instr (b : a) c))
-> Instr (b : a) c -> Maybe (Instr (b : a) c)
forall a b. (a -> b) -> a -> b
$ Instr (b : a) a
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : a) a -> Instr a c -> Instr (b : a) c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr a c
f

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

branchShortCut :: Rule
branchShortCut :: Rule
branchShortCut = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
LEFT  :# IF_LEFT Instr (a : s) b
f Instr (b : s) b
_ :# Instr b out
c -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
RIGHT :# IF_LEFT Instr (a : s) b
_ Instr (b : s) b
f :# Instr b out
c -> Instr (b : s) out -> Maybe (Instr (b : s) out)
forall a. a -> Maybe a
Just (Instr (b : s) b
f Instr (b : s) b -> Instr b out -> Instr (b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
CONS  :# IF_CONS Instr (a : 'TList a : s) b
f Instr s b
_ :# Instr b out
c -> Instr (a : 'TList a : s) out
-> Maybe (Instr (a : 'TList a : s) out)
forall a. a -> Maybe a
Just (Instr (a : 'TList a : s) b
f Instr (a : 'TList a : s) b
-> Instr b out -> Instr (a : 'TList a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
NIL   :# IF_CONS Instr (a : 'TList a : s) b
_ Instr s b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
NONE  :# IF_NONE Instr s b
f Instr (a : s) b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  Instr inp b
SOME  :# IF_NONE Instr s b
_ Instr (a : s) b
f :# Instr b out
c -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)

  PUSH vOr :: Value' Instr t
vOr@(VOr Either (Value' Instr l) (Value' Instr r)
eitherVal) :# IF_LEFT Instr (a : s) b
f Instr (b : s) b
g :# Instr b out
c -> case Value' Instr t
vOr of
    (Value ('TOr l r)
_ :: Value ('TOr l r)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
      Left Value' Instr l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
        Right Dict (ConstantScope l)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr inp (a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr l
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
        Either BadTypeForScope (Dict (ConstantScope l))
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
      Right Value' Instr r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
        Right Dict (ConstantScope r)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr inp (b : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr r
val Instr inp (b : s) -> Instr (b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : s) b
g Instr (b : s) b -> Instr b out -> Instr (b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
        Either BadTypeForScope (Dict (ConstantScope r))
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  PUSH (VList (Value' Instr t1
x : [Value' Instr t1]
xs))     :# IF_CONS Instr (a : 'TList a : s) b
f Instr s b
_ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t1) -> Instr inp ('TList t1 : inp)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH ([Value' Instr t1] -> Value' Instr ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
xs) Instr inp ('TList t1 : inp)
-> Instr ('TList t1 : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t1 -> Instr ('TList t1 : inp) (a : 'TList a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t1
x Instr ('TList t1 : inp) (a : 'TList a : s)
-> Instr (a : 'TList a : s) out -> Instr ('TList t1 : inp) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : 'TList a : s) b
f Instr (a : 'TList a : s) b
-> Instr b out -> Instr (a : 'TList a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  PUSH (VList [Value' Instr t1]
_)            :# IF_CONS Instr (a : 'TList a : s) b
_ Instr s b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  PUSH (VOption Maybe (Value' Instr t1)
Nothing)    :# IF_NONE Instr s b
f Instr (a : s) b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  PUSH (VOption (Just Value' Instr t1
val)) :# IF_NONE Instr s b
_ Instr (a : s) b
f :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t1 -> Instr inp (a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t1
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  PUSH (VBool Bool
True)         :# IF Instr s b
f Instr s b
_      :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)
  PUSH (VBool Bool
False)        :# IF Instr s b
_ Instr s b
f      :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)

  Instr inp b
LEFT  :# IF_LEFT Instr (a : s) out
f Instr (b : s) out
_ -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just Instr (a : s) out
f
  Instr inp b
RIGHT :# IF_LEFT Instr (a : s) out
_ Instr (b : s) out
f -> Instr (b : s) out -> Maybe (Instr (b : s) out)
forall a. a -> Maybe a
Just Instr (b : s) out
f
  Instr inp b
CONS  :# IF_CONS Instr (a : 'TList a : s) out
f Instr s out
_ -> Instr (a : 'TList a : s) out
-> Maybe (Instr (a : 'TList a : s) out)
forall a. a -> Maybe a
Just Instr (a : 'TList a : s) out
f
  Instr inp b
NIL   :# IF_CONS Instr (a : 'TList a : s) out
_ Instr s out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  Instr inp b
NONE  :# IF_NONE Instr s out
f Instr (a : s) out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  Instr inp b
SOME  :# IF_NONE Instr s out
_ Instr (a : s) out
f -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just Instr (a : s) out
f

  PUSH vOr :: Value' Instr t
vOr@(VOr Either (Value' Instr l) (Value' Instr r)
eitherVal) :# IF_LEFT Instr (a : s) out
f Instr (b : s) out
g -> case Value' Instr t
vOr of
    (Value ('TOr l r)
_ :: Value ('TOr l r)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
      Left Value' Instr l
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
        Right Dict (ConstantScope l)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr inp (a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr l
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) out
f)
        Either BadTypeForScope (Dict (ConstantScope l))
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
      Right Value' Instr r
val -> case forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
        Right Dict (ConstantScope r)
Dict -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr inp (b : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr r
val Instr inp (b : s) -> Instr (b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : s) out
g)
        Either BadTypeForScope (Dict (ConstantScope r))
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  PUSH (VList (Value' Instr t1
x : [Value' Instr t1]
xs))     :# IF_CONS Instr (a : 'TList a : s) out
f Instr s out
_ -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t1) -> Instr inp ('TList t1 : inp)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH ([Value' Instr t1] -> Value' Instr ('TList t1)
forall (t1 :: T) (instr :: [T] -> [T] -> *).
SingI t1 =>
[Value' instr t1] -> Value' instr ('TList t1)
VList [Value' Instr t1]
xs) Instr inp ('TList t1 : inp)
-> Instr ('TList t1 : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t1 -> Instr ('TList t1 : inp) (a : 'TList a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t1
x Instr ('TList t1 : inp) (a : 'TList a : s)
-> Instr (a : 'TList a : s) out -> Instr ('TList t1 : inp) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : 'TList a : s) out
f)
  PUSH (VList [Value' Instr t1]
_)            :# IF_CONS Instr (a : 'TList a : s) out
_ Instr s out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  PUSH (VOption Maybe (Value' Instr t1)
Nothing)    :# IF_NONE Instr s out
f Instr (a : s) out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  PUSH (VOption (Just Value' Instr t1
val)) :# IF_NONE Instr s out
_ Instr (a : s) out
f -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t1 -> Instr inp (a : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t1
val Instr inp (a : s) -> Instr (a : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : s) out
f)
  PUSH (VBool Bool
True)         :# IF Instr s out
f Instr s out
_      -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  PUSH (VBool Bool
False)        :# IF Instr s out
_ Instr s out
f      -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

compareWithZero :: Rule
compareWithZero :: Rule
compareWithZero = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  PUSH (VInt Integer
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
 UnaryArithOp Eq' n) =>
Instr inp out
EQ Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp ('TInt : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TInt : s), ToIntArithOp n) =>
Instr inp out
INT Instr inp ('TInt : s) -> Instr ('TInt : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) b
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
 UnaryArithOp Eq' n) =>
Instr inp out
EQ Instr ('TInt : s) b -> Instr b out -> Instr ('TInt : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  PUSH (VInt Integer
0) :# Instr b b
COMPARE :# Instr b out
EQ      -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
 UnaryArithOp Eq' n) =>
Instr inp out
EQ
  PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b out
EQ      -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp ('TInt : s)
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ ('TInt : s), ToIntArithOp n) =>
Instr inp out
INT Instr inp ('TInt : s) -> Instr ('TInt : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (s :: [T]).
(inp ~ (n : s), out ~ (UnaryArithRes Eq' n : s),
 UnaryArithOp Eq' n) =>
Instr inp out
EQ
  Instr inp out
_                                   -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

simpleDrops :: Rule
simpleDrops :: Rule
simpleDrops = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  -- DROP 0 is Nop
  DROPN PeanoNatural n
Zero :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  DROPN PeanoNatural n
Zero -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop

  -- DROP 1 is DROP.
  -- @gromak: DROP seems to be cheaper (in my experiments it consumed 3 less gas).
  -- It is packed more efficiently.
  -- Unfortunately I do not know how to convince GHC that types match here.
  -- Specifically, it can not deduce that `inp` is not empty
  -- (`DROP` expects non-empty input).
  -- We have `LongerOrSameLength inp (S Z)` here, but that is not enough to
  -- convince GHC.
  -- I will leave this note and rule here in hope that someone will manage to
  -- deal with this problem one day.

  -- DROPN One :# c -> Just (DROP :# c)
  -- DROPN One -> Just DROP

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

-- If an instruction takes another instruction as an argument and that
-- internal instruction is 'Nop', sometimes the whole instruction is
-- 'Nop'.
-- For now we do it only for 'DIP', but ideally we should do it for
-- 'MAP' as well (which is harder).
internalNop :: Rule
internalNop :: Rule
internalNop = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  DIP Instr a c
Nop      -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  DIP Instr a c
Nop :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

simpleDips :: Rule
simpleDips :: Rule
simpleDips = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  -- DIP 0 is redundant
  DIPN PeanoNatural n
Zero Instr s s'
i :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s s'
i Instr s s' -> Instr s' out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr s' out
c)
  DIPN PeanoNatural n
Zero Instr s s'
i -> Instr s s' -> Maybe (Instr s s')
forall a. a -> Maybe a
Just Instr s s'
i

  -- @gromak: same situation as with `DROP 1` (see above).
  -- DIPN One i :# c -> Just (DIP i :# c)
  -- DIPN One i -> Just (DIP i)

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

simpleDups :: Rule
simpleDups :: Rule
simpleDups = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  -- DUP 1 is just DUP
  DUPN PeanoNatural n
One :# Instr b out
xs -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
xs
  DUPN PeanoNatural n
One -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

adjacentDips :: Rule
adjacentDips :: Rule
adjacentDips = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  DIP Instr a c
f :# DIP Instr a c
g -> Instr (b : a) (b : c) -> Maybe (Instr (b : a) (b : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr a c
f Instr a c -> Instr c c -> Instr a c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c c
Instr a c
g))
  DIP Instr a c
f :# DIP Instr a c
g :# Instr b out
c -> Instr (b : a) out -> Maybe (Instr (b : a) out)
forall a. a -> Maybe a
Just (Instr a c -> Instr (b : a) (b : c)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr a c
f Instr a c -> Instr c c -> Instr a c
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c c
Instr a c
g) Instr (b : a) (b : c) -> Instr (b : c) out -> Instr (b : a) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (b : c) out
c)

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

redundantIf :: Rule
redundantIf :: Rule
redundantIf = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  IF Instr s b
x Instr s b
y :# Instr b out
xs
    | Instr s b
x Instr s b -> Instr s b -> Bool
forall a. Eq a => a -> a -> Bool
== Instr s b
y
    -> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a. a -> Maybe a
Just (Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out))
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBool : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBool : s) s -> Instr s out -> Instr ('TBool : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr s b
x Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
xs
  IF Instr s out
x Instr s out
y
    | Instr s out
x Instr s out -> Instr s out -> Bool
forall a. Eq a => a -> a -> Bool
== Instr s out
y
    -> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a. a -> Maybe a
Just (Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out))
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBool : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBool : s) s -> Instr s out -> Instr ('TBool : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr s out
x
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

emptyDip :: Rule
emptyDip :: Rule
emptyDip = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  DIP Instr a c
Nop :# Instr b out
xs -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
  DIP Instr a c
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  DIPN PeanoNatural n
_ Instr s s'
Nop :# Instr b out
xs -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
  DIPN PeanoNatural n
_ Instr s s'
Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

digDug :: Rule
digDug :: Rule
digDug = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  (DIG (PeanoNatural n
x :: PeanoNatural n) :: Instr inp t) :# (DUG PeanoNatural n
y :: Instr t out) :# Instr b out
xs
    | Just n :~: n
Refl <- PeanoNatural n -> PeanoNatural n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat PeanoNatural n
x PeanoNatural n
y
    -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
xs
  (DIG (PeanoNatural n
x :: PeanoNatural n) :: Instr inp t) :# (DUG PeanoNatural n
y :: Instr t out)
    | Just n :~: n
Refl <- PeanoNatural n -> PeanoNatural n -> Maybe (n :~: n)
forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> Maybe (a :~: b)
eqPeanoNat PeanoNatural n
x PeanoNatural n
y
    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

-- TODO [#299]: optimize sequences of more than 2 DROPs.
-- | Sequences of @DROP@s can be turned into single @DROP n@.
-- When @n@ is greater than 2 it saves size and gas.
-- When @n@ is 2 it saves gas only.
adjacentDrops :: Rule
adjacentDrops :: Rule
adjacentDrops = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
DROP :# Instr b out
DROP -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (PeanoNatural ('S ('S 'Z))
-> Instr (a : a : out) (Drop ('S ('S 'Z)) (a : a : out))
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two)
  Instr inp b
DROP :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (PeanoNatural ('S ('S 'Z)) -> Instr inp (Drop ('S ('S 'Z)) inp)
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c)

  -- Does not compile, need to do something smart
  -- DROPN Two :# DROP -> Just (DROPN (Succ Two))

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

specificPush :: Rule
specificPush :: Rule
specificPush = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  push :: Instr inp out
push@PUSH{}         -> Instr inp out -> Maybe (Instr inp out)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush Instr inp out
push
  push :: Instr inp b
push@PUSH{} :# Instr b out
c -> (Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c) (Instr inp b -> Instr inp out)
-> Maybe (Instr inp b) -> Maybe (Instr inp out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr inp b -> Maybe (Instr inp b)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush Instr inp b
push

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  where
    optimizePush :: Instr inp out -> Maybe (Instr inp out)
    optimizePush :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush = \case
      PUSH Value' Instr t
v | Value' Instr t
_ :: Value v <- Value' Instr t
v -> case Value' Instr t
v of
        Value' Instr t
VUnit -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT
        VMap Map (Value' Instr k) (Value' Instr v)
m
          | Map (Value' Instr k) (Value' Instr v) -> Bool
forall t. Container t => t -> Bool
null Map (Value' Instr k) (Value' Instr v)
m -> case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @v of STMap{} -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI a, SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP
        VSet Set (Value' Instr t1)
m
          | Set (Value' Instr t1) -> Bool
forall t. Container t => t -> Bool
null Set (Value' Instr t1)
m -> case forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @v of STSet{} -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), SingI e, Comparable e) =>
Instr inp out
EMPTY_SET
        Value' Instr t
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

      Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing


isSomeOnIf :: Rule
isSomeOnIf :: Rule
isSomeOnIf = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  IF (PUSH (VOption Just{})) (PUSH (VOption Maybe (Value' Instr t1)
Nothing)) :# Instr b out
c -> case Instr b out
c of
    IF_NONE (PUSH (VBool Bool
False)) (Instr (a : s) b
DROP :# PUSH (VBool Bool
True)) :# Instr b out
s -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
s
    IF_NONE (PUSH (VBool Bool
False)) (Instr (a : s) b
DROP :# PUSH (VBool Bool
True))      -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
    Instr b out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

pairUnpair :: Rule
pairUnpair :: Rule
pairUnpair = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
PAIR :# Instr b b
UNPAIR :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
PAIR :# Instr b out
UNPAIR      -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop

  Instr inp b
UNPAIR :# Instr b b
PAIR :# Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Instr inp b
UNPAIR :# Instr b out
PAIR      -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

pairMisc :: Rule
pairMisc :: Rule
pairMisc = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
PAIR :# Instr b b
CDR :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
PAIR :# Instr b out
CDR      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP

  Instr inp b
PAIR :# Instr b b
CAR :# Instr b out
c -> Instr (a : b : s) out -> Maybe (Instr (a : b : s) out)
forall a. a -> Maybe a
Just (Instr (a : b : s) out -> Maybe (Instr (a : b : s) out))
-> Instr (a : b : s) out -> Maybe (Instr (a : b : s) out)
forall a b. (a -> b) -> a -> b
$ (Instr (b : s) s -> Instr (a : b : s) (a : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP) Instr (a : b : s) (a : s)
-> Instr (a : s) out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (a : s) out
c
  Instr inp b
PAIR :# Instr b out
CAR      -> Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s))
forall a. a -> Maybe a
Just (Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s)))
-> Instr (a : b : s) (a : s) -> Maybe (Instr (a : b : s) (a : s))
forall a b. (a -> b) -> a -> b
$ Instr (b : s) s -> Instr (a : b : s) (a : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

unpairMisc :: Rule
unpairMisc :: Rule
unpairMisc = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
DUP :# Instr b b
CAR :# DIP Instr a c
CDR      -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR
  Instr inp b
DUP :# Instr b b
CAR :# DIP Instr a c
CDR :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c

  Instr inp b
DUP :# Instr b b
CDR :# DIP Instr a c
CAR      -> Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s))
forall a. a -> Maybe a
Just (Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s)))
-> Instr inp (b : a : s) -> Maybe (Instr inp (b : a : s))
forall a b. (a -> b) -> a -> b
$ Instr inp (a : b : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr inp (a : b : s)
-> Instr (a : b : s) (b : a : s) -> Instr inp (b : a : s)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : s) (b : a : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
  Instr inp b
DUP :# Instr b b
CDR :# DIP Instr a c
CAR :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp (a : b : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr inp (a : b : s) -> Instr (a : b : s) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (a : b : s) (b : a : s)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr (a : b : s) (b : a : s)
-> Instr (b : a : s) out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (b : a : s) out
c

  Instr inp b
UNPAIR :# Instr b out
DROP             -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR
  Instr inp b
UNPAIR :# Instr b b
DROP :# Instr b out
c        -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (b : s)) =>
Instr inp out
CDR Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

commuteArith ::
  forall n m s out. Instr (n ': m ': s) out -> Maybe (Instr (m ': n ': s) out)
commuteArith :: forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith = \case
  Instr (n : m : s) out
ADD -> do Dict (ArithRes Add n m ~ ArithRes Add m n, ArithOp Add m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Add @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Add n m : s),
 ArithOp Add n m) =>
Instr inp out
ADD
  Instr (n : m : s) out
MUL -> do Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Mul @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Mul n m : s),
 ArithOp Mul n m) =>
Instr inp out
MUL
  Instr (n : m : s) out
OR -> do Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Or @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Or n m : s), ArithOp Or n m) =>
Instr inp out
OR
  Instr (n : m : s) out
AND -> do Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @And @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes And n m : s),
 ArithOp And n m) =>
Instr inp out
AND
  Instr (n : m : s) out
XOR -> do Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n)
Dict <- forall {k} (aop :: k) (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
forall aop (n :: T) (m :: T).
ArithOp aop n m =>
Maybe $ Dict (ArithRes aop n m ~ ArithRes aop m n, ArithOp aop m n)
commutativityProof @Xor @n @m; Instr (m : n : s) out -> Maybe (Instr (m : n : s) out)
forall a. a -> Maybe a
Just Instr (m : n : s) out
forall {inp :: [T]} {out :: [T]} (n :: T) (m :: T) (s :: [T]).
(inp ~ (n : m : s), out ~ (ArithRes Xor n m : s),
 ArithOp Xor n m) =>
Instr inp out
XOR
  Instr (n : m : s) out
_ -> Maybe (Instr (m : n : s) out)
forall a. Maybe a
Nothing

swapBeforeCommutative :: Rule
swapBeforeCommutative :: Rule
swapBeforeCommutative = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
SWAP :# Instr b b
i :# Instr b out
c -> (Instr (a : b : s) b -> Instr b out -> Instr (a : b : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c) (Instr (a : b : s) b -> Instr (a : b : s) out)
-> Maybe (Instr (a : b : s) b) -> Maybe (Instr (a : b : s) out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr (b : a : s) b -> Maybe (Instr (a : b : s) b)
forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith Instr b b
Instr (b : a : s) b
i
  Instr inp b
SWAP :# Instr b out
i -> Instr (b : a : s) out -> Maybe (Instr (a : b : s) out)
forall (n :: T) (m :: T) (s :: [T]) (out :: [T]).
Instr (n : m : s) out -> Maybe (Instr (m : n : s) out)
commuteArith Instr b out
Instr (b : a : s) out
i

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

pushPack :: Rule
pushPack :: Rule
pushPack = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  PUSH Value' Instr t
x :# Instr b out
PACK -> Instr inp ('TBytes : inp) -> Maybe (Instr inp ('TBytes : inp))
forall a. a -> Maybe a
Just (Value' Instr t -> Instr inp ('TBytes : inp)
forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked Value' Instr t
x)
  PUSH Value' Instr t
x :# Instr b b
PACK :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Value' Instr t -> Instr inp ('TBytes : inp)
forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked Value' Instr t
x Instr inp ('TBytes : inp)
-> Instr ('TBytes : inp) out -> Instr inp out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TBytes : inp) out
c)

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  where
    pushPacked :: PackedValScope t => Value t -> Instr s ('TBytes ': s)
    pushPacked :: forall (t :: T) (s :: [T]).
PackedValScope t =>
Value t -> Instr s ('TBytes : s)
pushPacked = Value' Instr 'TBytes -> Instr s ('TBytes : s)
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH (Value' Instr 'TBytes -> Instr s ('TBytes : s))
-> (Value t -> Value' Instr 'TBytes)
-> Value t
-> Instr s ('TBytes : s)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Value' Instr 'TBytes
forall (instr :: [T] -> [T] -> *).
ByteString -> Value' instr 'TBytes
VBytes (ByteString -> Value' Instr 'TBytes)
-> (Value t -> ByteString) -> Value t -> Value' Instr 'TBytes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Value t -> ByteString
forall (t :: T). PackedValScope t => Value t -> ByteString
packValue'

justDrops :: Rule
justDrops :: Rule
justDrops = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
CAR              :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out))
-> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair a b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair a b : b) b
-> Instr b out -> Instr ('TPair a b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
CDR              :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out))
-> Instr ('TPair a b : b) out -> Maybe (Instr ('TPair a b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair a b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair a b : b) b
-> Instr b out -> Instr ('TPair a b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SOME             :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
LEFT             :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
RIGHT            :# Instr b b
DROP :# Instr b out
c -> Instr (b : b) out -> Maybe (Instr (b : b) out)
forall a. a -> Maybe a
Just (Instr (b : b) out -> Maybe (Instr (b : b) out))
-> Instr (b : b) out -> Maybe (Instr (b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SIZE             :# Instr b b
DROP :# Instr b out
c -> Instr (c : b) out -> Maybe (Instr (c : b) out)
forall a. a -> Maybe a
Just (Instr (c : b) out -> Maybe (Instr (c : b) out))
-> Instr (c : b) out -> Maybe (Instr (c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  GETN PeanoNatural ix
_           :# Instr b b
DROP :# Instr b out
c -> Instr (pair : b) out -> Maybe (Instr (pair : b) out)
forall a. a -> Maybe a
Just (Instr (pair : b) out -> Maybe (Instr (pair : b) out))
-> Instr (pair : b) out -> Maybe (Instr (pair : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (pair : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (pair : b) b -> Instr b out -> Instr (pair : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
CAST             :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
RENAME           :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
PACK             :# Instr b b
DROP :# Instr b out
c -> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a. a -> Maybe a
Just (Instr (a : b) out -> Maybe (Instr (a : b) out))
-> Instr (a : b) out -> Maybe (Instr (a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
UNPACK           :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
CONCAT'          :# Instr b b
DROP :# Instr b out
c -> Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out)
forall a. a -> Maybe a
Just (Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out))
-> Instr ('TList c : b) out -> Maybe (Instr ('TList c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TList c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TList c : b) b -> Instr b out -> Instr ('TList c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
ISNAT            :# Instr b b
DROP :# Instr b out
c -> Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out)
forall a. a -> Maybe a
Just (Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out))
-> Instr ('TInt : b) out -> Maybe (Instr ('TInt : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TInt : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TInt : b) b -> Instr b out -> Instr ('TInt : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
ABS              :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
NEG              :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
NOT              :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
EQ               :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
NEQ              :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
LT               :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
GT               :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
LE               :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
GE               :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
INT              :# Instr b b
DROP :# Instr b out
c -> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a. a -> Maybe a
Just (Instr (n : b) out -> Maybe (Instr (n : b) out))
-> Instr (n : b) out -> Maybe (Instr (n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  CONTRACT EpName
_       :# Instr b b
DROP :# Instr b out
c -> Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out)
forall a. a -> Maybe a
Just (Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out))
-> Instr ('TAddress : b) out -> Maybe (Instr ('TAddress : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TAddress : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TAddress : b) b -> Instr b out -> Instr ('TAddress : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SET_DELEGATE     :# Instr b b
DROP :# Instr b out
c -> Instr ('TOption 'TKeyHash : b) out
-> Maybe (Instr ('TOption 'TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TOption 'TKeyHash : b) out
 -> Maybe (Instr ('TOption 'TKeyHash : b) out))
-> Instr ('TOption 'TKeyHash : b) out
-> Maybe (Instr ('TOption 'TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TOption 'TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TOption 'TKeyHash : b) b
-> Instr b out -> Instr ('TOption 'TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
IMPLICIT_ACCOUNT :# Instr b b
DROP :# Instr b out
c -> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out))
-> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKeyHash : b) b -> Instr b out -> Instr ('TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
VOTING_POWER     :# Instr b b
DROP :# Instr b out
c -> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a. a -> Maybe a
Just (Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out))
-> Instr ('TKeyHash : b) out -> Maybe (Instr ('TKeyHash : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKeyHash : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKeyHash : b) b -> Instr b out -> Instr ('TKeyHash : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SHA256           :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SHA512           :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
BLAKE2B          :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SHA3             :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
KECCAK           :# Instr b b
DROP :# Instr b out
c -> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a. a -> Maybe a
Just (Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out))
-> Instr ('TBytes : b) out -> Maybe (Instr ('TBytes : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TBytes : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TBytes : b) b -> Instr b out -> Instr ('TBytes : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
HASH_KEY         :# Instr b b
DROP :# Instr b out
c -> Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out)
forall a. a -> Maybe a
Just (Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out))
-> Instr ('TKey : b) out -> Maybe (Instr ('TKey : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TKey : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TKey : b) b -> Instr b out -> Instr ('TKey : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
PAIRING_CHECK    :# Instr b b
DROP :# Instr b out
c -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
-> Maybe
     (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out)
forall a. a -> Maybe a
Just (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
 -> Maybe
      (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out))
-> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
-> Maybe
     (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) b
-> Instr b out
-> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
ADDRESS          :# Instr b b
DROP :# Instr b out
c -> Instr ('TContract a : b) out
-> Maybe (Instr ('TContract a : b) out)
forall a. a -> Maybe a
Just (Instr ('TContract a : b) out
 -> Maybe (Instr ('TContract a : b) out))
-> Instr ('TContract a : b) out
-> Maybe (Instr ('TContract a : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TContract a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TContract a : b) b
-> Instr b out -> Instr ('TContract a : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
JOIN_TICKETS     :# Instr b b
DROP :# Instr b out
c -> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out)
forall a. a -> Maybe a
Just (Instr ('TPair ('TTicket a) ('TTicket a) : b) out
 -> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out))
-> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TPair ('TTicket a) ('TTicket a) : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair ('TTicket a) ('TTicket a) : b) b
-> Instr b out -> Instr ('TPair ('TTicket a) ('TTicket a) : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c

  Instr inp b
CAR              :# Instr b out
DROP      -> Instr ('TPair a b : out) out
-> Maybe (Instr ('TPair a b : out) out)
forall a. a -> Maybe a
Just Instr ('TPair a b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
CDR              :# Instr b out
DROP      -> Instr ('TPair a b : out) out
-> Maybe (Instr ('TPair a b : out) out)
forall a. a -> Maybe a
Just Instr ('TPair a b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SOME             :# Instr b out
DROP      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
LEFT             :# Instr b out
DROP      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
RIGHT            :# Instr b out
DROP      -> Instr (b : out) out -> Maybe (Instr (b : out) out)
forall a. a -> Maybe a
Just Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SIZE             :# Instr b out
DROP      -> Instr (c : out) out -> Maybe (Instr (c : out) out)
forall a. a -> Maybe a
Just Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  GETN PeanoNatural ix
_           :# Instr b out
DROP      -> Instr (pair : out) out -> Maybe (Instr (pair : out) out)
forall a. a -> Maybe a
Just Instr (pair : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
CAST             :# Instr b out
DROP      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
RENAME           :# Instr b out
DROP      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
PACK             :# Instr b out
DROP      -> Instr (a : out) out -> Maybe (Instr (a : out) out)
forall a. a -> Maybe a
Just Instr (a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
UNPACK           :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
CONCAT'          :# Instr b out
DROP      -> Instr ('TList c : out) out -> Maybe (Instr ('TList c : out) out)
forall a. a -> Maybe a
Just Instr ('TList c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
ISNAT            :# Instr b out
DROP      -> Instr ('TInt : out) out -> Maybe (Instr ('TInt : out) out)
forall a. a -> Maybe a
Just Instr ('TInt : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
ABS              :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
NEG              :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
NOT              :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
EQ               :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
NEQ              :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
LT               :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
GT               :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
LE               :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
GE               :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
INT              :# Instr b out
DROP      -> Instr (n : out) out -> Maybe (Instr (n : out) out)
forall a. a -> Maybe a
Just Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  CONTRACT EpName
_       :# Instr b out
DROP      -> Instr ('TAddress : out) out -> Maybe (Instr ('TAddress : out) out)
forall a. a -> Maybe a
Just Instr ('TAddress : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SET_DELEGATE     :# Instr b out
DROP      -> Instr ('TOption 'TKeyHash : out) out
-> Maybe (Instr ('TOption 'TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TOption 'TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
IMPLICIT_ACCOUNT :# Instr b out
DROP      -> Instr ('TKeyHash : out) out -> Maybe (Instr ('TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
VOTING_POWER     :# Instr b out
DROP      -> Instr ('TKeyHash : out) out -> Maybe (Instr ('TKeyHash : out) out)
forall a. a -> Maybe a
Just Instr ('TKeyHash : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SHA256           :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SHA512           :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
BLAKE2B          :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SHA3             :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
KECCAK           :# Instr b out
DROP      -> Instr ('TBytes : out) out -> Maybe (Instr ('TBytes : out) out)
forall a. a -> Maybe a
Just Instr ('TBytes : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
HASH_KEY         :# Instr b out
DROP      -> Instr ('TKey : out) out -> Maybe (Instr ('TKey : out) out)
forall a. a -> Maybe a
Just Instr ('TKey : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
PAIRING_CHECK    :# Instr b out
DROP      -> Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out
-> Maybe
     (Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out)
forall a. a -> Maybe a
Just Instr ('TList ('TPair 'TBls12381G1 'TBls12381G2) : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
ADDRESS          :# Instr b out
DROP      -> Instr ('TContract a : out) out
-> Maybe (Instr ('TContract a : out) out)
forall a. a -> Maybe a
Just Instr ('TContract a : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
JOIN_TICKETS     :# Instr b out
DROP      -> Instr ('TPair ('TTicket a) ('TTicket a) : out) out
-> Maybe (Instr ('TPair ('TTicket a) ('TTicket a) : out) out)
forall a. a -> Maybe a
Just Instr ('TPair ('TTicket a) ('TTicket a) : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp out
_                             -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

justDoubleDrops :: Rule
justDoubleDrops :: Rule
justDoubleDrops = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
PAIR         :# Instr b b
DROP :# Instr b out
c -> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a. a -> Maybe a
Just (Instr (a : b : b) out -> Maybe (Instr (a : b : b) out))
-> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : b) (b : b)
-> Instr (b : b) out -> Instr (a : b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
MEM          :# Instr b b
DROP :# Instr b out
c -> Instr (MemOpKey c : c : b) out
-> Maybe (Instr (MemOpKey c : c : b) out)
forall a. a -> Maybe a
Just (Instr (MemOpKey c : c : b) out
 -> Maybe (Instr (MemOpKey c : c : b) out))
-> Instr (MemOpKey c : c : b) out
-> Maybe (Instr (MemOpKey c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (MemOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (MemOpKey c : c : b) (c : b)
-> Instr (c : b) out -> Instr (MemOpKey c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
GET          :# Instr b b
DROP :# Instr b out
c -> Instr (GetOpKey c : c : b) out
-> Maybe (Instr (GetOpKey c : c : b) out)
forall a. a -> Maybe a
Just (Instr (GetOpKey c : c : b) out
 -> Maybe (Instr (GetOpKey c : c : b) out))
-> Instr (GetOpKey c : c : b) out
-> Maybe (Instr (GetOpKey c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (GetOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (GetOpKey c : c : b) (c : b)
-> Instr (c : b) out -> Instr (GetOpKey c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
APPLY        :# Instr b b
DROP :# Instr b out
c -> Instr (a : 'TLambda ('TPair a b) c : b) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out)
forall a. a -> Maybe a
Just (Instr (a : 'TLambda ('TPair a b) c : b) out
 -> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out))
-> Instr (a : 'TLambda ('TPair a b) c : b) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr
  (a : 'TLambda ('TPair a b) c : b) ('TLambda ('TPair a b) c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
  (a : 'TLambda ('TPair a b) c : b) ('TLambda ('TPair a b) c : b)
-> Instr ('TLambda ('TPair a b) c : b) out
-> Instr (a : 'TLambda ('TPair a b) c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TLambda ('TPair a b) c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TLambda ('TPair a b) c : b) b
-> Instr b out -> Instr ('TLambda ('TPair a b) c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
CONCAT       :# Instr b b
DROP :# Instr b out
c -> Instr (c : c : b) out -> Maybe (Instr (c : c : b) out)
forall a. a -> Maybe a
Just (Instr (c : c : b) out -> Maybe (Instr (c : c : b) out))
-> Instr (c : c : b) out -> Maybe (Instr (c : c : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : c : b) (c : b)
-> Instr (c : b) out -> Instr (c : c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : b) b -> Instr b out -> Instr (c : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
ADD          :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SUB          :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SUB_MUTEZ    :# Instr b b
DROP :# Instr b out
c -> Instr ('TMutez : 'TMutez : b) out
-> Maybe (Instr ('TMutez : 'TMutez : b) out)
forall a. a -> Maybe a
Just (Instr ('TMutez : 'TMutez : b) out
 -> Maybe (Instr ('TMutez : 'TMutez : b) out))
-> Instr ('TMutez : 'TMutez : b) out
-> Maybe (Instr ('TMutez : 'TMutez : b) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TMutez : 'TMutez : b) ('TMutez : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : 'TMutez : b) ('TMutez : b)
-> Instr ('TMutez : b) out -> Instr ('TMutez : 'TMutez : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TMutez : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : b) b -> Instr b out -> Instr ('TMutez : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
MUL          :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
EDIV         :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
OR           :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
AND          :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
XOR          :# Instr b b
DROP :# Instr b out
c -> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a. a -> Maybe a
Just (Instr (n : m : b) out -> Maybe (Instr (n : m : b) out))
-> Instr (n : m : b) out -> Maybe (Instr (n : m : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : b) (m : b)
-> Instr (m : b) out -> Instr (n : m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (m : b) b -> Instr b out -> Instr (m : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
COMPARE      :# Instr b b
DROP :# Instr b out
c -> Instr (n : n : b) out -> Maybe (Instr (n : n : b) out)
forall a. a -> Maybe a
Just (Instr (n : n : b) out -> Maybe (Instr (n : n : b) out))
-> Instr (n : n : b) out -> Maybe (Instr (n : n : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : n : b) (n : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : n : b) (n : b)
-> Instr (n : b) out -> Instr (n : n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (n : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : b) b -> Instr b out -> Instr (n : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
TICKET       :# Instr b b
DROP :# Instr b out
c -> Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out)
forall a. a -> Maybe a
Just (Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out))
-> Instr (a : 'TNat : b) out -> Maybe (Instr (a : 'TNat : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : 'TNat : b) ('TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : 'TNat : b) ('TNat : b)
-> Instr ('TNat : b) out -> Instr (a : 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TNat : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TNat : b) b -> Instr b out -> Instr ('TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SPLIT_TICKET :# Instr b b
DROP :# Instr b out
c -> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out)
forall a. a -> Maybe a
Just (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
 -> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out))
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out)
forall a b. (a -> b) -> a -> b
$ Instr
  ('TTicket a : 'TPair 'TNat 'TNat : b) ('TPair 'TNat 'TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
  ('TTicket a : 'TPair 'TNat 'TNat : b) ('TPair 'TNat 'TNat : b)
-> Instr ('TPair 'TNat 'TNat : b) out
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TPair 'TNat 'TNat : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TPair 'TNat 'TNat : b) b
-> Instr b out -> Instr ('TPair 'TNat 'TNat : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c
  Instr inp b
SWAP :# Instr b b
DROP :# Instr b b
DROP :# Instr b out
c -> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a. a -> Maybe a
Just (Instr (a : b : b) out -> Maybe (Instr (a : b : b) out))
-> Instr (a : b : b) out -> Maybe (Instr (a : b : b) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : b) (b : b)
-> Instr (b : b) out -> Instr (a : b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (b : b) b -> Instr b out -> Instr (b : b) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
c

  Instr inp b
PAIR         :# Instr b out
DROP      -> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a. a -> Maybe a
Just (Instr (a : b : out) out -> Maybe (Instr (a : b : out) out))
-> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : out) (b : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : out) (b : out)
-> Instr (b : out) out -> Instr (a : b : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
MEM          :# Instr b out
DROP      -> Instr (MemOpKey c : c : out) out
-> Maybe (Instr (MemOpKey c : c : out) out)
forall a. a -> Maybe a
Just (Instr (MemOpKey c : c : out) out
 -> Maybe (Instr (MemOpKey c : c : out) out))
-> Instr (MemOpKey c : c : out) out
-> Maybe (Instr (MemOpKey c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (MemOpKey c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (MemOpKey c : c : out) (c : out)
-> Instr (c : out) out -> Instr (MemOpKey c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
GET          :# Instr b out
DROP      -> Instr (GetOpKey c : c : out) out
-> Maybe (Instr (GetOpKey c : c : out) out)
forall a. a -> Maybe a
Just (Instr (GetOpKey c : c : out) out
 -> Maybe (Instr (GetOpKey c : c : out) out))
-> Instr (GetOpKey c : c : out) out
-> Maybe (Instr (GetOpKey c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (GetOpKey c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (GetOpKey c : c : out) (c : out)
-> Instr (c : out) out -> Instr (GetOpKey c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
APPLY        :# Instr b out
DROP      -> Instr (a : 'TLambda ('TPair a b) c : out) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out)
forall a. a -> Maybe a
Just (Instr (a : 'TLambda ('TPair a b) c : out) out
 -> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out))
-> Instr (a : 'TLambda ('TPair a b) c : out) out
-> Maybe (Instr (a : 'TLambda ('TPair a b) c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr
  (a : 'TLambda ('TPair a b) c : out) ('TLambda ('TPair a b) c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
  (a : 'TLambda ('TPair a b) c : out) ('TLambda ('TPair a b) c : out)
-> Instr ('TLambda ('TPair a b) c : out) out
-> Instr (a : 'TLambda ('TPair a b) c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TLambda ('TPair a b) c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
CONCAT       :# Instr b out
DROP      -> Instr (c : c : out) out -> Maybe (Instr (c : c : out) out)
forall a. a -> Maybe a
Just (Instr (c : c : out) out -> Maybe (Instr (c : c : out) out))
-> Instr (c : c : out) out -> Maybe (Instr (c : c : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (c : c : out) (c : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (c : c : out) (c : out)
-> Instr (c : out) out -> Instr (c : c : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (c : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
ADD          :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SUB          :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SUB_MUTEZ    :# Instr b out
DROP      -> Instr ('TMutez : 'TMutez : out) out
-> Maybe (Instr ('TMutez : 'TMutez : out) out)
forall a. a -> Maybe a
Just (Instr ('TMutez : 'TMutez : out) out
 -> Maybe (Instr ('TMutez : 'TMutez : out) out))
-> Instr ('TMutez : 'TMutez : out) out
-> Maybe (Instr ('TMutez : 'TMutez : out) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TMutez : 'TMutez : out) ('TMutez : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr ('TMutez : 'TMutez : out) ('TMutez : out)
-> Instr ('TMutez : out) out -> Instr ('TMutez : 'TMutez : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TMutez : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
MUL          :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
EDIV         :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
OR           :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
AND          :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
XOR          :# Instr b out
DROP      -> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a. a -> Maybe a
Just (Instr (n : m : out) out -> Maybe (Instr (n : m : out) out))
-> Instr (n : m : out) out -> Maybe (Instr (n : m : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : m : out) (m : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : m : out) (m : out)
-> Instr (m : out) out -> Instr (n : m : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (m : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
COMPARE      :# Instr b out
DROP      -> Instr (n : n : out) out -> Maybe (Instr (n : n : out) out)
forall a. a -> Maybe a
Just (Instr (n : n : out) out -> Maybe (Instr (n : n : out) out))
-> Instr (n : n : out) out -> Maybe (Instr (n : n : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (n : n : out) (n : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (n : n : out) (n : out)
-> Instr (n : out) out -> Instr (n : n : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (n : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
TICKET       :# Instr b out
DROP      -> Instr (a : 'TNat : out) out -> Maybe (Instr (a : 'TNat : out) out)
forall a. a -> Maybe a
Just (Instr (a : 'TNat : out) out
 -> Maybe (Instr (a : 'TNat : out) out))
-> Instr (a : 'TNat : out) out
-> Maybe (Instr (a : 'TNat : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : 'TNat : out) ('TNat : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : 'TNat : out) ('TNat : out)
-> Instr ('TNat : out) out -> Instr (a : 'TNat : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TNat : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SPLIT_TICKET :# Instr b out
DROP      -> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out)
forall a. a -> Maybe a
Just (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
 -> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out))
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
-> Maybe (Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out)
forall a b. (a -> b) -> a -> b
$ Instr
  ('TTicket a : 'TPair 'TNat 'TNat : out) ('TPair 'TNat 'TNat : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr
  ('TTicket a : 'TPair 'TNat 'TNat : out) ('TPair 'TNat 'TNat : out)
-> Instr ('TPair 'TNat 'TNat : out) out
-> Instr ('TTicket a : 'TPair 'TNat 'TNat : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TPair 'TNat 'TNat : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp b
SWAP :# Instr b b
DROP :# Instr b out
DROP      -> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a. a -> Maybe a
Just (Instr (a : b : out) out -> Maybe (Instr (a : b : out) out))
-> Instr (a : b : out) out -> Maybe (Instr (a : b : out) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : b : out) (b : out)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (a : b : out) (b : out)
-> Instr (b : out) out -> Instr (a : b : out) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (b : out) out
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP

  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

-- | Append LHS of v'Seq' to RHS and re-run pointwise ocRuleset at each point.
--   That might cause reinvocation of this function (see 'defaultRules'),
--   but effectively this ensures it will flatten any v'Seq'-tree right-to-left,
--   while evaling no more than once on each node.
--
--   The reason this function invokes ocRuleset is when you append an instr
--   to already-optimised RHS of v'Seq', you might get an optimisable tree.
--
--   The argument is a local, non-structurally-recursive ocRuleset.
linearizeAndReapply :: Rule -> Instr inp out -> Instr inp out
linearizeAndReapply :: forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
restart = \case
  Seq (Seq Instr inp b
a Instr b b
b) Instr b out
c ->
    Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
restart (Instr inp out -> Instr inp out) -> Instr inp out -> Instr inp out
forall a b. (a -> b) -> a -> b
$ Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr inp b
a (Rule -> Instr b out -> Instr b out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
linearizeAndReapply Rule
restart (Instr b b -> Instr b out -> Instr b out
forall (inp :: [T]) (b :: [T]) (out :: [T]).
Instr inp b -> Instr b out -> Instr inp out
Seq Instr b b
b Instr b out
c))

  Instr inp out
other -> Rule -> Instr inp out -> Instr inp out
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
restart Instr inp out
other

----------------------------------------------------------------------------
-- Generic functions working with rules
----------------------------------------------------------------------------

-- | Combine two rule fixpoints.
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> (Rule -> Rule)
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
orRule Rule -> Rule
l Rule -> Rule
r Rule
topl = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \Instr inp out
instr ->
  (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
l Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr) Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
r Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr)

-- | Combine a rule fixpoint and a simple rule.
orSimpleRule :: (Rule -> Rule) -> Rule -> (Rule -> Rule)
orSimpleRule :: (Rule -> Rule) -> Rule -> Rule -> Rule
orSimpleRule Rule -> Rule
l Rule
r Rule
topl = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \Instr inp out
instr ->
  (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule (Rule -> Rule
l Rule
topl) (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr) Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
instr)

-- | Turn rule fixpoint into rule.
fixpoint :: (Rule -> Rule) -> Rule
fixpoint :: (Rule -> Rule) -> Rule
fixpoint Rule -> Rule
r = Rule
go
  where
    go :: Rule
    go :: Rule
go = Rule -> Rule
whileApplies (Rule -> Rule
r Rule
go)

-- | Apply the rule once, if it fails, return the instruction unmodified.
applyOnce :: Rule -> Instr inp out -> Instr inp out
applyOnce :: forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce Rule
r Instr inp out
i = Instr inp out
-> (Instr inp out -> Instr inp out)
-> Maybe (Instr inp out)
-> Instr inp out
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Instr inp out
i Instr inp out -> Instr inp out
forall a. a -> a
id (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
i)

-- | Apply a rule to the same code, until it fails.
whileApplies :: Rule -> Rule
whileApplies :: Rule -> Rule
whileApplies Rule
r = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go
  where
    go :: Instr inp out -> Maybe (Instr inp out)
    go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go Instr inp out
i = Maybe (Instr inp out)
-> (Instr inp out -> Maybe (Instr inp out))
-> Maybe (Instr inp out)
-> Maybe (Instr inp out)
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i) Instr inp out -> Maybe (Instr inp out)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Rule
-> forall (inp :: [T]) (out :: [T]).
   Instr inp out -> Maybe (Instr inp out)
unRule Rule
r (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp out
i)

----------------------------------------------------------------------------
-- TH
----------------------------------------------------------------------------

makeLensesFor [("ocGotoValues", "ocGotoValuesL")] ''OptimizerConf