-- SPDX-FileCopyrightText: 2020 Tocqueville Group
--
-- SPDX-License-Identifier: LicenseRef-MIT-TQ

-- 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 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(..), dfsInstr)
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 :: 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 :: 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 ()
dfsSettings = DfsSettings ()
forall a. Default a => a
def{ dsGoToValues :: Bool
dsGoToValues = Bool
ocGotoValues }
    performOneStage :: Rule -> Instr inp out -> Instr inp out
performOneStage Rule
stageRules = ((Instr inp out, ()) -> Instr inp out
forall a b. (a, b) -> a
fst ((Instr inp out, ()) -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
      ((Instr inp out -> (Instr inp out, ()))
 -> Instr inp out -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall a b. (a -> b) -> a -> b
$ DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings ()
dfsSettings
      ((forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
 -> Instr inp out -> (Instr inp out, ()))
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall a b. (a -> b) -> a -> b
$ (Instr i o -> (Instr i o, ())
forall a. a -> (a, ())
adapter (Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
      ((Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
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
flattenFn
    (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
adjacentDips
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
isSomeOnIf
    (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 (s :: [T]). Instr s s
Nop
  Instr inp out
_                 -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

flattenFn :: Rule
flattenFn :: Rule
flattenFn = (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
  Fn Text
_ StackFn
_ 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

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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 Value' Instr ('TLambda 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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
Nop
  LAMBDA Value' Instr ('TLambda i o)
_           :# Instr b out
DROP -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
DUP Instr (a : s) (a : a : s)
-> Instr (a : a : s) out -> Instr (a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (a : a : s) out
c)
  Instr inp b
DUP :# Instr b out
SWAP      -> Instr (a : s) (a : a : s) -> Maybe (Instr (a : s) (a : a : s))
forall a. a -> Maybe a
Just Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]).
DupableScope a =>
Instr (a : s) (a : a : s)
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 (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x Instr c (t : c) -> Instr (t : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr (t : c) out
c
  PUSH Value' Instr t
x    :# DIP Instr a c
f      -> Instr a (t : c) -> Maybe (Instr a (t : c))
forall a. a -> Maybe a
Just (Instr a (t : c) -> Maybe (Instr a (t : c)))
-> Instr a (t : c) -> Maybe (Instr a (t : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c (t : c) -> Instr a (t : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr c (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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 ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
UNIT Instr c ('TUnit : c) -> Instr ('TUnit : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TUnit : c) out
c
  Instr inp b
UNIT      :# DIP Instr a c
f      -> Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c))
forall a. a -> Maybe a
Just (Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c)))
-> Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TUnit : c) -> Instr a ('TUnit : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
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 ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
NOW Instr c ('TTimestamp : c)
-> Instr ('TTimestamp : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TTimestamp : c) out
c
  Instr inp b
NOW       :# DIP Instr a c
f      -> Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c))
forall a. a -> Maybe a
Just (Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c)))
-> Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TTimestamp : c) -> Instr a ('TTimestamp : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
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 ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
SENDER Instr c ('TAddress : c) -> Instr ('TAddress : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TAddress : c) out
c
  Instr inp b
SENDER    :# DIP Instr a c
f      -> Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c))
forall a. a -> Maybe a
Just (Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c)))
-> Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TAddress : c) -> Instr a ('TAddress : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
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 ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP Instr c ('TMap a b : c) -> Instr ('TMap a b : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TMap a b : c) out
c
  Instr inp b
EMPTY_MAP :# DIP Instr a c
f      -> Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c))
forall a. a -> Maybe a
Just (Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c)))
-> Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TMap a b : c) -> Instr a ('TMap a b : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
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 ('TSet e : c)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
EMPTY_SET Instr c ('TSet e : c) -> Instr ('TSet e : c) out -> Instr c out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr b out
Instr ('TSet e : c) out
c
  Instr inp b
EMPTY_SET :# DIP Instr a c
f      -> Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c))
forall a. a -> Maybe a
Just (Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c)))
-> Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c))
forall a b. (a -> b) -> a -> b
$ Instr a c
f Instr a c -> Instr c ('TSet e : c) -> Instr a ('TSet e : c)
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr c ('TSet e : c)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
      Left Value' Instr l
val -> case CheckScope (ConstantScope l) =>
Either BadTypeForScope (Dict (ConstantScope l))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
        Right Dict (ConstantScope l)
Dict -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr s (l : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr l
val Instr s (l : s) -> Instr (l : s) out -> Instr s 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 CheckScope (ConstantScope r) =>
Either BadTypeForScope (Dict (ConstantScope r))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
        Right Dict (ConstantScope r)
Dict -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr s (r : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr r
val Instr s (r : s) -> Instr (r : s) out -> Instr s 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 t
x : [Value' Instr t]
xs))     :# IF_CONS Instr (a : 'TList a : s) b
f Instr s b
_ :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t) -> Instr s ('TList t : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH ([Value' Instr t] -> Value' Instr ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
xs) Instr s ('TList t : s) -> Instr ('TList t : s) out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr ('TList a : s) (t : 'TList a : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x Instr ('TList a : s) (t : 'TList a : s)
-> Instr (t : 'TList a : s) out -> Instr ('TList a : s) 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 t]
_)            :# 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 t)
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 t
val)) :# IF_NONE Instr s b
_ Instr (a : s) b
f :# Instr b out
c -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr t -> Instr s (t : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
val Instr s (t : s) -> Instr (t : s) out -> Instr s 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)) -> case Either (Value' Instr l) (Value' Instr r)
eitherVal of
      Left Value' Instr l
val -> case CheckScope (ConstantScope l) =>
Either BadTypeForScope (Dict (ConstantScope l))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope l) of
        Right Dict (ConstantScope l)
Dict -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr l -> Instr s (l : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr l
val Instr s (l : s) -> Instr (l : s) out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (l : s) out
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 CheckScope (ConstantScope r) =>
Either BadTypeForScope (Dict (ConstantScope r))
forall (c :: Constraint).
CheckScope c =>
Either BadTypeForScope (Dict c)
checkScope @(ConstantScope r) of
        Right Dict (ConstantScope r)
Dict -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr r -> Instr s (r : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr r
val Instr s (r : s) -> Instr (r : s) out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (r : s) out
Instr (b : s) out
g)
        Either BadTypeForScope (Dict (ConstantScope r))
_          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing
  PUSH (VList (Value' Instr t
x : [Value' Instr t]
xs))     :# IF_CONS Instr (a : 'TList a : s) out
f Instr s out
_ -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr ('TList t) -> Instr s ('TList t : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH ([Value' Instr t] -> Value' Instr ('TList t)
forall (t :: T) (instr :: [T] -> [T] -> *).
SingI t =>
[Value' instr t] -> Value' instr ('TList t)
VList [Value' Instr t]
xs) Instr s ('TList t : s) -> Instr ('TList t : s) out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Value' Instr t -> Instr ('TList a : s) (t : 'TList a : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x Instr ('TList a : s) (t : 'TList a : s)
-> Instr (t : 'TList a : s) out -> Instr ('TList a : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (t : 'TList a : s) out
Instr (a : 'TList a : s) out
f)
  PUSH (VList [Value' Instr t]
_)            :# 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 t)
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 t
val)) :# IF_NONE Instr s out
_ Instr (a : s) out
f -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Value' Instr t -> Instr s (t : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
val Instr s (t : s) -> Instr (t : s) out -> Instr s out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr (t : s) out
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 ('TInt : s) out -> Maybe (Instr ('TInt : s) out)
forall a. a -> Maybe a
Just (Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out))
-> Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
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 (VNat Natural
0) :# Instr b b
COMPARE :# Instr b b
EQ :# Instr b out
c -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out))
-> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TNat : s) ('TInt : s)
forall (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
INT Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
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 (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ
  PUSH (VNat Natural
0) :# Instr b b
COMPARE :# Instr b out
EQ      -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out))
-> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a b. (a -> b) -> a -> b
$ Instr ('TNat : s) ('TInt : s)
forall (n :: T) (s :: [T]).
ToIntArithOp n =>
Instr (n : s) ('TInt : s)
INT Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (c :: [T]) (b :: [T]).
Instr a b -> Instr b c -> Instr a c
:# Instr ('TInt : s) out
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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

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

-- 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 :: Peano) (s :: [T]).
RequireLongerOrSameLength s n =>
PeanoNatural n -> Instr s (Drop n s)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Peano). (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 :: Peano) (s :: [T]).
RequireLongerOrSameLength s n =>
PeanoNatural n -> Instr s (Drop n s)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Peano). (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 :: 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 ('TUnit : inp) -> Maybe (Instr inp ('TUnit : inp))
forall a. a -> Maybe a
Just Instr inp ('TUnit : inp)
forall (s :: [T]). Instr s ('TUnit : s)
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 SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @v of STMap{} -> Instr inp ('TMap k v : inp) -> Maybe (Instr inp ('TMap k v : inp))
forall a. a -> Maybe a
Just Instr inp ('TMap k v : inp)
forall (a :: T) (b :: T) (s :: [T]).
(SingI a, SingI b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP
        VSet Set (Value' Instr t)
m
          | Set (Value' Instr t) -> Bool
forall t. Container t => t -> Bool
null Set (Value' Instr t)
m -> case SingI t => Sing t
forall k (a :: k). SingI a => Sing a
sing @v of STSet{} -> Instr inp ('TSet t : inp) -> Maybe (Instr inp ('TSet t : inp))
forall a. a -> Maybe a
Just Instr inp ('TSet t : inp)
forall (e :: T) (s :: [T]).
(SingI e, Comparable e) =>
Instr s ('TSet e : s)
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 t)
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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 (s :: [T]). Instr s s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (a : b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
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 (i :: [T]) (o :: [T]) (a :: T) (b :: T) (s :: [T]).
(i ~ ('TPair a b : s), o ~ (b : s)) =>
Instr i o
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 :: 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 <- ArithOp Add n m =>
Maybe (Dict (ArithRes Add n m ~ ArithRes Add m n, ArithOp Add m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Add n m =>
Instr (n : m : s) (ArithRes Add n m : s)
ADD
  Instr (n : m : s) out
MUL -> do Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n)
Dict <- ArithOp Mul n m =>
Maybe (Dict (ArithRes Mul n m ~ ArithRes Mul m n, ArithOp Mul m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Mul n m =>
Instr (n : m : s) (ArithRes Mul n m : s)
MUL
  Instr (n : m : s) out
OR -> do Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n)
Dict <- ArithOp Or n m =>
Maybe (Dict (ArithRes Or n m ~ ArithRes Or m n, ArithOp Or m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Or n m =>
Instr (n : m : s) (ArithRes Or n m : s)
OR
  Instr (n : m : s) out
AND -> do Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n)
Dict <- ArithOp And n m =>
Maybe (Dict (ArithRes And n m ~ ArithRes And m n, ArithOp And m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp And n m =>
Instr (n : m : s) (ArithRes And n m : s)
AND
  Instr (n : m : s) out
XOR -> do Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n)
Dict <- ArithOp Xor n m =>
Maybe (Dict (ArithRes Xor n m ~ ArithRes Xor m n, ArithOp Xor m n))
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)
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 (n :: T) (m :: T) (s :: [T]).
ArithOp Xor n m =>
Instr (n : m : s) (ArithRes Xor n m : s)
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 :: Value t -> Instr s ('TBytes : s)
pushPacked = Value' Instr 'TBytes -> Instr s ('TBytes : s)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 Notes p
_ 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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
DROP
  CONTRACT Notes p
_ 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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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) (s :: [T]). Instr (a : s) s
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 :: 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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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 (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
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 :: 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)

-- | An adapter for `dfsInstr`.
adapter :: a -> (a, ())
adapter :: a -> (a, ())
adapter a
a = (a
a, ())

-- | 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 :: 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