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

{-# OPTIONS_HADDOCK not-home #-}

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

-- | Optimizer rewrite rules
module Morley.Michelson.Optimizer.Internal.Rules
  ( module Morley.Michelson.Optimizer.Internal.Rules
  ) where

import Prelude hiding (EQ, GT, LT)

import Data.Constraint (Dict(..), (\\))
import Data.Default (Default(def))
import Data.Singletons (sing)
import Data.Type.Equality ((:~:)(Refl))

import Morley.Michelson.Interpret.Pack (packValue')
import Morley.Michelson.Optimizer.Internal.Proofs
import Morley.Michelson.Optimizer.Internal.Ruleset
import Morley.Michelson.Optimizer.Utils
import Morley.Michelson.Typed.Aliases (Value)
import Morley.Michelson.Typed.Arith
import Morley.Michelson.Typed.Instr hiding ((:#))
import Morley.Michelson.Typed.Scope (ConstantScope, PackedValScope, checkScope)
import Morley.Michelson.Typed.Sing
import Morley.Michelson.Typed.T
import Morley.Michelson.Typed.Value
import Morley.Util.Peano
import Morley.Util.PeanoNatural

{-
Note [Writing optimizer rules]
------------------------------

We locally redefine (:#) to simplify handling instruction sequence tails.
Consider that a given instruction sequence can appear in the middle, and then @a
:# b :# tail@ will match, or at the end of the sequence, and then @a :# b@ will
match.

Local definition of (:#) makes it so we can always assume there's a tail.
However, we don't need it when matching on single instructions.

Thus, the rule of thumb is this: if you're matching on a single instruction,
everything is fine. If you're matching on a sequence, i.e. using (:#), then
always match on tail.
-}

-- | Default optimization rules.
defaultRules :: Ruleset
defaultRules :: Ruleset
defaultRules = (Element [Ruleset -> Ruleset] -> Ruleset -> Ruleset)
-> Ruleset -> [Ruleset -> Ruleset] -> Ruleset
forall t b. Container t => (Element t -> b -> b) -> b -> t -> b
foldr Element [Ruleset -> Ruleset] -> Ruleset -> Ruleset
forall a b. (a -> b) -> a -> b
($) Ruleset
forall a. Default a => a
def ([Ruleset -> Ruleset] -> Ruleset)
-> [Ruleset -> Ruleset] -> Ruleset
forall a b. (a -> b) -> a -> b
$ ([Rule] -> OptimizationStage -> Ruleset -> Ruleset)
-> ([Rule], OptimizationStage) -> Ruleset -> Ruleset
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (([Rule] -> [Rule]) -> OptimizationStage -> Ruleset -> Ruleset
alterRulesAtPrio (([Rule] -> [Rule]) -> OptimizationStage -> Ruleset -> Ruleset)
-> ([Rule] -> [Rule] -> [Rule])
-> [Rule]
-> OptimizationStage
-> Ruleset
-> Ruleset
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Rule] -> [Rule] -> [Rule]
forall a b. a -> b -> a
const) (([Rule], OptimizationStage) -> Ruleset -> Ruleset)
-> [([Rule], OptimizationStage)] -> [Ruleset -> Ruleset]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>
  -- NB: if adding more main stages, remember to check if
  -- 'defaultRulesAndPushPack' needs updating.
  [ ([Rule]
mainStageRules              , Int -> OptimizationStage
OptimizationStageMain Int
0)
  , ([Rule]
dipDrop2swapDropStageRules  , Int -> OptimizationStage
OptimizationStageMainExtended Int
0)
  , ([Rule]
fixupStageRules             , Int -> OptimizationStage
OptimizationStageFixup Int
0)
  , ([Rule]
glueAdjacentInstrsStageRules, Int -> OptimizationStage
OptimizationStageRollAdjacent Int
0)
  ]
  where
    dipDrop2swapDropStageRules :: [Rule]
dipDrop2swapDropStageRules = Rule
dipDrop2swapDrop Rule -> [Rule] -> [Rule]
forall a. a -> [a] -> [a]
: [Rule]
mainStageRules
    fixupStageRules :: [Rule]
fixupStageRules = [Rule
dipSwapDrop]
    glueAdjacentInstrsStageRules :: [Rule]
glueAdjacentInstrsStageRules =
      [ Rule
adjacentDrops
      , Rule
rollPairN
      , Rule
rollUnpairN
      , Rule
rollDips
      ]

-- | 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.
defaultRulesAndPushPack :: Ruleset
defaultRulesAndPushPack :: Ruleset
defaultRulesAndPushPack = Ruleset
defaultRules
  Ruleset -> (Ruleset -> Ruleset) -> Ruleset
forall a b. a -> (a -> b) -> b
& OptimizationStage -> Rule -> Ruleset -> Ruleset
insertRuleAtPrio (Int -> OptimizationStage
OptimizationStageMainExtended Int
0) Rule
pushPack

mainStageRules :: [Rule]
mainStageRules :: [Rule]
mainStageRules =
  [ Rule
removeNesting
  , Rule
removeExtStackType
  , Rule
ifNopNop2Drop
  , Rule
nopIsNeutralForSeq
  , Rule
variousNops
  , Rule
dupSwap2dup
  , Rule
noDipNeeded
  , Rule
branchShortCut
  , Rule
compareWithZero
  , Rule
internalNop
  , Rule
simpleDups
  , Rule
adjacentDips
  , Rule
isSomeOnIf
  , Rule
redundantIf
  , Rule
emptyDip
  , Rule
digDug
  , Rule
specificPush
  , Rule
pairUnpair
  , Rule
pairMisc
  , Rule
unpairMisc
  , Rule
swapBeforeCommutative
  , Rule
justDrops
  , Rule
justDoubleDrops
  , Rule
dig1AndDug1AreSwap
  , Rule
notIf
  , Rule
dropMeta
  , Rule
dupDugDrop
  -- strictly speaking, these rules below are de-optimisations, but they
  -- expose opportunities for other optimisations, and they are undone in the
  -- last stage.
  , Rule
unrollPairN
  , Rule
unrollUnpairN
  , Rule
unrollDropN
  , Rule
unrollDips
  ]

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

dropMeta :: Rule
dropMeta :: Rule
dropMeta = (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
  Meta SomeMeta
_ Instr inp out
i -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
i
  WithLoc ErrorSrcPos
_ 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

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

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

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

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

nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  -- NB: we're not using (:#) here because it'll always match when rhs is Nop
  Seq 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
  Seq Instr inp b
i Instr b out
Nop -> Instr inp b -> Maybe (Instr inp b)
forall a. a -> Maybe a
Just Instr inp b
i
  Instr inp out
_         -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

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

dupSwap2dup :: Rule
dupSwap2dup :: Rule
dupSwap2dup = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
DUP :# Instr b b
SWAP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (s :: [T]).
(inp ~ (a : s), out ~ (a : a : s), DupableScope a) =>
Instr inp out
DUP Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Value' Instr t -> Instr c b
forall {inp :: [T]} {out :: [T]} (t :: T) (s :: [T]).
(inp ~ s, out ~ (t : s), ConstantScope t) =>
Value' Instr t -> Instr inp out
PUSH Value' Instr t
x Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TUnit : s)) =>
Instr inp out
UNIT Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TTimestamp : s)) =>
Instr inp out
NOW Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c b
forall {inp :: [T]} {out :: [T]} (s :: [T]).
(inp ~ s, out ~ ('TAddress : s)) =>
Instr inp out
SENDER Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c b
forall {inp :: [T]} {out :: [T]} (b :: T) (a :: T) (s :: [T]).
(inp ~ s, out ~ ('TMap a b : s), SingI b, Comparable a) =>
Instr inp out
EMPTY_MAP Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c b
forall {inp :: [T]} {out :: [T]} (e :: T) (s :: [T]).
(inp ~ s, out ~ ('TSet e : s), Comparable e) =>
Instr inp out
EMPTY_SET Instr c b -> Instr b out -> Instr c out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c

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

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

unrollDips :: Rule
unrollDips :: Rule
unrollDips = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go
  where
    go :: Instr inp out -> Maybe (Instr inp out)
    go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go = \case
      DIPN PeanoNatural n
Zero Instr s s'
c -> Instr s s' -> Maybe (Instr s s')
forall a. a -> Maybe a
Just (Instr s s' -> Maybe (Instr s s'))
-> Instr s s' -> Maybe (Instr s s')
forall a b. (a -> b) -> a -> b
$ Instr s s'
c
      DIPN PeanoNatural n
One Instr s s'
c -> Instr (Head inp : s) (Head inp : s')
-> Maybe (Instr (Head inp : s) (Head inp : s'))
forall a. a -> Maybe a
Just (Instr (Head inp : s) (Head inp : s')
 -> Maybe (Instr (Head inp : s) (Head inp : s')))
-> Instr (Head inp : s) (Head inp : s')
-> Maybe (Instr (Head inp : s) (Head inp : s'))
forall a b. (a -> b) -> a -> b
$ Instr s s' -> Instr (Head inp : s) (Head inp : s')
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr s s'
c
      DIPN (Succ PeanoNatural m
n) Instr s s'
c -> Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s')
-> Instr
     (Head inp : (LazyTake m (Tail inp) ++ s))
     (Head inp : (LazyTake m (Tail inp) ++ s'))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP (Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s')
 -> Instr
      (Head inp : (LazyTake m (Tail inp) ++ s))
      (Head inp : (LazyTake m (Tail inp) ++ s')))
-> Maybe
     (Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s'))
-> Maybe
     (Instr
        (Head inp : (LazyTake m (Tail inp) ++ s))
        (Head inp : (LazyTake m (Tail inp) ++ s')))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s')
-> Maybe
     (Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s'))
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (PeanoNatural m
-> Instr s s'
-> Instr (LazyTake m (Tail inp) ++ s) (LazyTake m (Tail inp) ++ s')
forall (n :: Nat) (inp :: [T]) (out :: [T]) (s :: [T]) (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural m
n Instr s s'
c)
      Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

rollDips :: Rule
rollDips :: Rule
rollDips = (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 (DIP Instr a c
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
$ PeanoNatural ('S ('S 'Z)) -> Instr a c -> Instr inp out
forall (n :: Nat) (inp :: [T]) (out :: [T]) (s :: [T]) (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two Instr a c
c
  DIP (DIPN PeanoNatural n
n Instr s s'
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
$ PeanoNatural ('S n) -> Instr s s' -> Instr inp out
forall (n :: Nat) (inp :: [T]) (out :: [T]) (s :: [T]) (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n) Instr s s'
c
  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) out -> Maybe (Instr (a : s) out))
-> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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) out -> Maybe (Instr (b : s) out))
-> Instr (b : s) out -> Maybe (Instr (b : s) out)
forall a b. (a -> b) -> a -> b
$ Instr (b : s) b
f Instr (b : s) b -> Instr b out -> Instr (b : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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) out
 -> Maybe (Instr (a : 'TList a : s) out))
-> Instr (a : 'TList a : s) out
-> Maybe (Instr (a : 'TList a : s) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : 'TList a : s) b
f Instr (a : 'TList a : s) b
-> Instr b out -> Instr (a : 'TList a : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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 out -> Maybe (Instr s out))
-> Instr s out -> Maybe (Instr s out)
forall a b. (a -> b) -> a -> b
$ Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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 out -> Maybe (Instr s out))
-> Instr s out -> Maybe (Instr s out)
forall a b. (a -> b) -> a -> b
$ Instr s b
f Instr s b -> Instr b out -> Instr s out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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) out -> Maybe (Instr (a : s) out))
-> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a b. (a -> b) -> a -> b
$ Instr (a : s) b
f Instr (a : s) b -> Instr b out -> Instr (a : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c

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

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

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

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

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

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

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 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 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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr c c
Instr a c
g) Instr (b : a) (b : c) -> Instr (b : c) out -> Instr (b : a) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
Instr (b : c) out
c

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

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

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

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

-- | 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 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
$ PeanoNatural ('S ('S 'Z)) -> Instr inp (Drop ('S ('S 'Z)) inp)
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c

  (DROPN PeanoNatural n
n :: Instr inp out) :# (Instr b b
DROP :: Instr inp' out') :# 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
$ PeanoNatural ('S n) -> Instr inp (Drop ('S n) inp)
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n) Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c ((Drop ('S n) inp ~ b, IsLongerOrSameLength inp ('S n) ~ 'True) =>
 Instr inp out)
-> Dict
     (Drop ('S n) inp ~ b, IsLongerOrSameLength inp ('S n) ~ 'True)
-> Instr inp out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (out' :: [T]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof @inp @out @out' PeanoNatural n
n PeanoNatural ('S 'Z)
forall (n :: Nat). (n ~ 'S 'Z) => PeanoNatural n
One
                                   ((AddPeano n ('S 'Z) ~ 'S n) => Instr inp out)
-> (AddPeano n ('S 'Z) :~: 'S n) -> Instr inp out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ SingNat n
-> SingNat ('S 'Z) -> AddPeano n ('S 'Z) :~: AddPeano ('S 'Z) n
forall (x :: Nat) (y :: Nat).
SingNat x -> SingNat y -> AddPeano x y :~: AddPeano y x
commutativity (PeanoNatural n -> SingNat n
forall (a :: Nat). PeanoNatural a -> SingNat a
singPeanoNat PeanoNatural n
n) (PeanoNatural ('S 'Z) -> SingNat ('S 'Z)
forall (a :: Nat). PeanoNatural a -> SingNat a
singPeanoNat PeanoNatural ('S 'Z)
forall (n :: Nat). (n ~ 'S 'Z) => PeanoNatural n
One)

  (Instr inp b
DROP :: Instr inp out) :# (DROPN PeanoNatural n
n :: Instr inp' out') :# 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
$ PeanoNatural ('S n) -> Instr (a : b) (Drop ('S n) (a : b))
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN (PeanoNatural n -> PeanoNatural ('S n)
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n) Instr (a : b) b -> Instr b out -> Instr (a : b) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c ((b ~ b, 'True ~ 'True) => Instr inp out)
-> Dict (b ~ b, 'True ~ 'True) -> Instr inp out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (out' :: [T]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof @inp @out @out' PeanoNatural ('S 'Z)
forall (n :: Nat). (n ~ 'S 'Z) => PeanoNatural n
One PeanoNatural n
n

  (DROPN PeanoNatural n
n :: Instr inp out) :# (DROPN PeanoNatural n
m :: Instr inp' out') :# 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
$ PeanoNatural (AddPeano n n) -> Instr inp (Drop (AddPeano n n) inp)
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN (PeanoNatural n -> PeanoNatural n -> PeanoNatural (AddPeano n n)
forall (a :: Nat) (b :: Nat).
PeanoNatural a -> PeanoNatural b -> PeanoNatural (AddPeano a b)
addPeanoNat PeanoNatural n
n PeanoNatural n
m) Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c ((Drop (AddPeano n n) inp ~ b,
  IsLongerOrSameLength inp (AddPeano n n) ~ 'True) =>
 Instr inp out)
-> Dict
     (Drop (AddPeano n n) inp ~ b,
      IsLongerOrSameLength inp (AddPeano n n) ~ 'True)
-> Instr inp out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (out' :: [T]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
forall {k} (inp :: [k]) (out :: [k]) (out' :: [k]) (n :: Nat)
       (m :: Nat).
(out ~ Drop n inp, IsLongerOrSameLength inp n ~ 'True,
 out' ~ Drop m out, IsLongerOrSameLength out m ~ 'True) =>
PeanoNatural n
-> PeanoNatural m
-> Dict
     (Drop (AddPeano n m) inp ~ out',
      IsLongerOrSameLength inp (AddPeano n m) ~ 'True)
dropNDropNProof @inp @out @out' PeanoNatural n
n PeanoNatural n
m

  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 b
push@PUSH{} :# Instr b out
c -> (Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c) (Instr inp b -> Instr inp out)
-> Maybe (Instr inp b) -> Maybe (Instr inp out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr inp b -> Maybe (Instr inp b)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
optimizePush Instr inp b
push

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

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


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

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
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 out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

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

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

  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 b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ Instr inp b
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c

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

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

unrollDropN :: Rule
unrollDropN :: Rule
unrollDropN = (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 :: forall inp out. Instr inp out -> Maybe (Instr inp out)
    go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go = \case
      DROPN PeanoNatural n
Zero -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (inp :: [T]). Instr inp inp
Nop
      DROPN (Succ PeanoNatural m
n) -> do
        Instr (Tail inp) out
dropn <- Instr (Tail inp) out -> Maybe (Instr (Tail inp) out)
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Instr (Tail inp) out -> Maybe (Instr (Tail inp) out))
-> Instr (Tail inp) out -> Maybe (Instr (Tail inp) out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural m -> Instr (Tail inp) (Drop m (Tail inp))
forall (n :: Nat) (inp :: [T]).
RequireLongerOrSameLength inp n =>
PeanoNatural n -> Instr inp (Drop n inp)
DROPN PeanoNatural m
n
        Instr (Head inp : Tail inp) out
-> Maybe (Instr (Head inp : Tail inp) out)
forall a. a -> Maybe a
Just (Instr (Head inp : Tail inp) out
 -> Maybe (Instr (Head inp : Tail inp) out))
-> Instr (Head inp : Tail inp) out
-> Maybe (Instr (Head inp : Tail inp) out)
forall a b. (a -> b) -> a -> b
$ Instr (Head inp : Tail inp) (Tail inp)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr (Head inp : Tail inp) (Tail inp)
-> Instr (Tail inp) out -> Instr (Head inp : Tail inp) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr (Tail inp) out
dropn
        ((inp ~ (Head inp : Tail inp)) => Maybe (Instr inp out))
-> (inp :~: (Head inp : Tail inp)) -> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (n :: Nat).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
forall {a} (inp :: [a]) (n :: Nat).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
unconsListProof @inp PeanoNatural m
n
      Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

unrollPairN :: Rule
unrollPairN :: Rule
unrollPairN = (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 :: forall inp out. Instr inp out -> Maybe (Instr inp out)
    go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go = \case
      PAIRN PeanoNatural n
Two -> Instr
  (Head inp : Head (Tail inp) : Drop n inp)
  ('TPair (Head inp) (Head (Tail inp)) : Drop n inp)
-> Maybe
     (Instr
        (Head inp : Head (Tail inp) : Drop n inp)
        ('TPair (Head inp) (Head (Tail inp)) : Drop n inp))
forall a. a -> Maybe a
Just Instr
  (Head inp : Head (Tail inp) : Drop n inp)
  ('TPair (Head inp) (Head (Tail inp)) : Drop n inp)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR ((inp ~ (Head inp : Head (Tail inp) : Drop n inp)) =>
 Maybe (Instr inp out))
-> (inp :~: (Head inp : Head (Tail inp) : Drop n inp))
-> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]).
(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True) =>
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
forall {k} (inp :: [k]).
(IsLongerOrSameLength inp ('S ('S 'Z)) ~ 'True) =>
inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)
pairN2isPairProof @inp
      PAIRN (Succ n :: PeanoNatural m
n@(Succ Succ{}) ) -> do
        Instr
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
pairn <- Instr
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
-> Maybe
     (Instr
        (Tail inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
           : Drop n inp))
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Instr
   (Tail inp)
   (RightComb
      (Head (Tail inp)
         : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
      : Drop n inp)
 -> Maybe
      (Instr
         (Tail inp)
         (RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
            : Drop n inp)))
-> Instr
     (Tail inp)
     (RightComb
        (Head (Tail inp)
           : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop n inp)
-> Maybe
     (Instr
        (Tail inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
           : Drop n inp))
forall a b. (a -> b) -> a -> b
$ PeanoNatural m
-> Instr
     (Tail inp)
     (RightComb
        (Head (Tail inp)
           : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop n inp)
forall {inp :: [T]} {out :: [T]} (n :: Nat) (inp1 :: [T]).
(inp ~ inp1, out ~ PairN n inp1, ConstraintPairN n inp1) =>
PeanoNatural n -> Instr inp out
PAIRN PeanoNatural m
n
        Instr
  (Head inp : Tail inp)
  ('TPair
     (Head inp)
     (RightComb
        (Head (Tail inp)
           : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
     : Drop n inp)
-> Maybe
     (Instr
        (Head inp : Tail inp)
        ('TPair
           (Head inp)
           (RightComb
              (Head (Tail inp)
                 : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
           : Drop n inp))
forall a. a -> Maybe a
Just (Instr
   (Head inp : Tail inp)
   ('TPair
      (Head inp)
      (RightComb
         (Head (Tail inp)
            : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
      : Drop n inp)
 -> Maybe
      (Instr
         (Head inp : Tail inp)
         ('TPair
            (Head inp)
            (RightComb
               (Head (Tail inp)
                  : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
            : Drop n inp)))
-> Instr
     (Head inp : Tail inp)
     ('TPair
        (Head inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
        : Drop n inp)
-> Maybe
     (Instr
        (Head inp : Tail inp)
        ('TPair
           (Head inp)
           (RightComb
              (Head (Tail inp)
                 : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
           : Drop n inp))
forall a b. (a -> b) -> a -> b
$ Instr
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
-> Instr
     (Head inp : Tail inp)
     (Head inp
        : RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop n inp)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
pairn Instr
  (Head inp : Tail inp)
  (Head inp
     : RightComb
         (Head (Tail inp)
            : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
-> Instr
     (Head inp
        : RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop n inp)
     ('TPair
        (Head inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
        : Drop n inp)
-> Instr
     (Head inp : Tail inp)
     ('TPair
        (Head inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
        : Drop n inp)
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr
  (Head inp
     : RightComb
         (Head (Tail inp)
            : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop n inp)
  ('TPair
     (Head inp)
     (RightComb
        (Head (Tail inp)
           : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp)))))
     : Drop n inp)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR
        ((inp ~ (Head inp : Tail inp)) => Maybe (Instr inp out))
-> (inp :~: (Head inp : Tail inp)) -> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (n :: Nat).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
forall {a} (inp :: [a]) (n :: Nat).
(IsLongerOrSameLength inp ('S n) ~ 'True) =>
PeanoNatural n -> inp :~: (Head inp : Tail inp)
unconsListProof @inp PeanoNatural m
n
      Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

unrollUnpairN :: Rule
unrollUnpairN :: Rule
unrollUnpairN = (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 :: forall inp out. Instr inp out -> Maybe (Instr inp out)
    go :: forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go = \case
      UNPAIRN PeanoNatural n
Two -> Instr
  ('TPair (Head out) (Head (Tail out)) : s)
  (Head out : Head (Tail out) : s)
-> Maybe
     (Instr
        ('TPair (Head out) (Head (Tail out)) : s)
        (Head out : Head (Tail out) : s))
forall a. a -> Maybe a
Just Instr
  ('TPair (Head out) (Head (Tail out)) : s)
  (Head out : Head (Tail out) : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR (((pair : s)
  ~ ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out)) =>
 Maybe (Instr inp out))
-> ((pair : s)
    :~: ('TPair (Head out) (Head (Tail out)) : Drop ('S ('S 'Z)) out))
-> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T]).
(inp ~ (pair : s), out ~ (UnpairN ('S ('S 'Z)) pair ++ s),
 ConstraintUnpairN (ToPeano 2) pair) =>
inp :~: PairN (ToPeano 2) out
unpairN2isUnpairProof @inp @out
      UNPAIRN (Succ n :: PeanoNatural m
n@(Succ Succ{})) -> do
        Instr
  (RightComb
     (Head (Tail out)
        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
   ++ s)
unpairn <- Instr
  (RightComb
     (Head (Tail out)
        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
   ++ s)
-> Maybe
     (Instr
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
           : s)
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s))
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Instr
   (RightComb
      (Head (Tail out)
         : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
      : s)
   (UnpairN
      ('S ('S m))
      (RightComb
         (Head (Tail out)
            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
    ++ s)
 -> Maybe
      (Instr
         (RightComb
            (Head (Tail out)
               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
            : s)
         (UnpairN
            ('S ('S m))
            (RightComb
               (Head (Tail out)
                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
          ++ s)))
-> Instr
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
        : s)
     (UnpairN
        ('S ('S m))
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
      ++ s)
-> Maybe
     (Instr
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
           : s)
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s))
forall a b. (a -> b) -> a -> b
$ PeanoNatural m
-> Instr
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
        : s)
     (UnpairN
        m
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
      ++ s)
forall (n :: Nat) (pair :: T) (s :: [T]).
ConstraintUnpairN n pair =>
PeanoNatural n -> Instr (pair : s) (UnpairN n pair ++ s)
UNPAIRN PeanoNatural m
n
        Instr
  ('TPair
     (Head out)
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
     : s)
  (Head out
     : (UnpairN
          ('S ('S m))
          (RightComb
             (Head (Tail out)
                : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
        ++ s))
-> Maybe
     (Instr
        ('TPair
           (Head out)
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           : s)
        (Head out
           : (UnpairN
                ('S ('S m))
                (RightComb
                   (Head (Tail out)
                      : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
              ++ s)))
forall a. a -> Maybe a
Just (Instr
   ('TPair
      (Head out)
      (RightComb
         (Head (Tail out)
            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
      : s)
   (Head out
      : (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s))
 -> Maybe
      (Instr
         ('TPair
            (Head out)
            (RightComb
               (Head (Tail out)
                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            : s)
         (Head out
            : (UnpairN
                 ('S ('S m))
                 (RightComb
                    (Head (Tail out)
                       : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
               ++ s))))
-> Instr
     ('TPair
        (Head out)
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
        : s)
     (Head out
        : (UnpairN
             ('S ('S m))
             (RightComb
                (Head (Tail out)
                   : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           ++ s))
-> Maybe
     (Instr
        ('TPair
           (Head out)
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           : s)
        (Head out
           : (UnpairN
                ('S ('S m))
                (RightComb
                   (Head (Tail out)
                      : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
              ++ s)))
forall a b. (a -> b) -> a -> b
$ Instr
  ('TPair
     (Head out)
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
     : s)
  (Head out
     : RightComb
         (Head (Tail out)
            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (a : b : s)) =>
Instr inp out
UNPAIR Instr
  ('TPair
     (Head out)
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
     : s)
  (Head out
     : RightComb
         (Head (Tail out)
            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
-> Instr
     (Head out
        : RightComb
            (Head (Tail out)
               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
        : s)
     (Head out
        : (UnpairN
             ('S ('S m))
             (RightComb
                (Head (Tail out)
                   : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           ++ s))
-> Instr
     ('TPair
        (Head out)
        (RightComb
           (Head (Tail out)
              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
        : s)
     (Head out
        : (UnpairN
             ('S ('S m))
             (RightComb
                (Head (Tail out)
                   : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           ++ s))
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr
  (RightComb
     (Head (Tail out)
        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
   ++ s)
-> Instr
     (Head out
        : RightComb
            (Head (Tail out)
               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
        : s)
     (Head out
        : (UnpairN
             ('S ('S m))
             (RightComb
                (Head (Tail out)
                   : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
           ++ s))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
  (RightComb
     (Head (Tail out)
        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head (Tail out)
           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
   ++ s)
unpairn
        ((pair
  ~ 'TPair
      (Head out)
      (RightComb
         (Head (Tail out)
            : Head (Tail (Tail out))
            : LazyTake m (Tail (Tail (Tail out)))))) =>
 Maybe (Instr inp out))
-> (pair
    :~: 'TPair
          (Head out)
          (RightComb
             (Head (Tail out)
                : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out))))))
-> Maybe (Instr inp out)
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (out :: [T]) (pair :: T) (s :: [T]) (n :: Nat).
(inp ~ (pair : s), out ~ (UnpairN ('S n) pair ++ s),
 ConstraintUnpairN ('S n) pair) =>
PeanoNatural n -> pair :~: RightComb (LazyTake ('S n) out)
unpairNisUnpairDipUnpairNProof @inp @out PeanoNatural m
n
      Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

rollPairN :: Rule
rollPairN :: Rule
rollPairN = (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
PAIR :# Instr b b
PAIR :# 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
$ PeanoNatural ('S ('S ('S 'Z))) -> Instr inp b
forall {inp :: [T]} {out :: [T]} (n :: Nat) (inp1 :: [T]).
(inp ~ inp1, out ~ PairN n inp1, ConstraintPairN n inp1) =>
PeanoNatural n -> Instr inp out
PAIRN (PeanoNatural ('S ('S 'Z)) -> PeanoNatural ('S ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two) Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c

  (DIP (PAIRN n :: PeanoNatural n
n@(Succ Succ{})) :: Instr inp out) :# Instr b b
PAIR :# 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
$ PeanoNatural ('S ('S ('S m))) -> Instr (b : a) b
forall {inp :: [T]} {out :: [T]} (n :: Nat) (inp1 :: [T]).
(inp ~ inp1, out ~ PairN n inp1, ConstraintPairN n inp1) =>
PeanoNatural n -> Instr inp out
PAIRN (PeanoNatural n -> PeanoNatural ('S ('S ('S m)))
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n) Instr (b : a) b -> Instr b out -> Instr (b : a) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
    ((('TPair b (RightComb (LazyTake n a)) : Drop n a)
  ~ ('TPair b (RightComb (LazyTake n a)) : Drop n a)) =>
 Instr inp out)
-> (('TPair b (RightComb (LazyTake n a)) : Drop n a)
    :~: ('TPair b (RightComb (LazyTake n a)) : Drop n a))
-> Instr inp out
forall (c :: Constraint) e r. HasDict c e => (c => r) -> e -> r
\\ forall (inp :: [T]) (n :: Nat).
((n >= ToPeano 2) ~ 'True,
 IsLongerOrSameLength (Tail inp) n ~ 'True,
 inp ~ (Head inp : Tail inp)) =>
PeanoNatural n
-> PairN ('S n) inp
   :~: ('TPair (Head inp) (RightComb (LazyTake n (Tail inp)))
          : Drop n (Tail inp))
dipPairNPairIsPairNProof @inp PeanoNatural n
n

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

rollUnpairN :: Rule
rollUnpairN :: Rule
rollUnpairN = (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
UNPAIR :# DIP Instr a c
UNPAIR :# Instr b out
c -> Instr ('TPair a ('TPair a b) : s) out
-> Maybe (Instr ('TPair a ('TPair a b) : s) out)
forall a. a -> Maybe a
Just (Instr ('TPair a ('TPair a b) : s) out
 -> Maybe (Instr ('TPair a ('TPair a b) : s) out))
-> Instr ('TPair a ('TPair a b) : s) out
-> Maybe (Instr ('TPair a ('TPair a b) : s) out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural ('S ('S ('S 'Z)))
-> Instr
     ('TPair a ('TPair a b) : s)
     (UnpairN ('S ('S ('S 'Z))) ('TPair a ('TPair a b)) ++ s)
forall (n :: Nat) (pair :: T) (s :: [T]).
ConstraintUnpairN n pair =>
PeanoNatural n -> Instr (pair : s) (UnpairN n pair ++ s)
UNPAIRN (PeanoNatural ('S ('S 'Z)) -> PeanoNatural ('S ('S ('S 'Z)))
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two) Instr ('TPair a ('TPair a b) : s) b
-> Instr b out -> Instr ('TPair a ('TPair a b) : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  Instr inp b
UNPAIR :# DIP (UNPAIRN n :: PeanoNatural n
n@(Succ Succ{})) :# Instr b out
c -> Instr ('TPair a b : s) out -> Maybe (Instr ('TPair a b : s) out)
forall a. a -> Maybe a
Just (Instr ('TPair a b : s) out -> Maybe (Instr ('TPair a b : s) out))
-> Instr ('TPair a b : s) out -> Maybe (Instr ('TPair a b : s) out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural ('S ('S ('S m)))
-> Instr
     ('TPair a b : s) (UnpairN ('S ('S ('S m))) ('TPair a b) ++ s)
forall (n :: Nat) (pair :: T) (s :: [T]).
ConstraintUnpairN n pair =>
PeanoNatural n -> Instr (pair : s) (UnpairN n pair ++ s)
UNPAIRN (PeanoNatural n -> PeanoNatural ('S ('S ('S m)))
forall (n :: Nat) (m :: Nat).
(n ~ 'S m) =>
PeanoNatural m -> PeanoNatural n
Succ PeanoNatural n
n) Instr ('TPair a b : s) b
-> Instr b out -> Instr ('TPair a b : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

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

swapBeforeCommutative :: Rule
swapBeforeCommutative :: Rule
swapBeforeCommutative = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule ((forall (inp :: [T]) (out :: [T]).
  Instr inp out -> Maybe (Instr inp out))
 -> Rule)
-> (forall (inp :: [T]) (out :: [T]).
    Instr inp out -> Maybe (Instr inp out))
-> Rule
forall a b. (a -> b) -> a -> b
$ \case
  Instr inp b
SWAP :# Instr b b
i :# Instr b out
c -> (Instr (a : b : s) b -> Instr b out -> Instr (a : b : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# 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 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 b
PACK :# 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
$ 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 (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
Instr ('TBytes : inp) out
c

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

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

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

dig1AndDug1AreSwap :: Rule
dig1AndDug1AreSwap :: Rule
dig1AndDug1AreSwap = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  DUG PeanoNatural n
One -> Instr
  (a : Head (LazyTake n out ++ Drop ('S n) out) : Drop ('S n) out)
  (Head (LazyTake n out ++ Drop ('S n) out) : a : Drop ('S n) out)
-> Maybe
     (Instr
        (a : Head (LazyTake n out ++ Drop ('S n) out) : Drop ('S n) out)
        (Head (LazyTake n out ++ Drop ('S n) out) : a : Drop ('S n) out))
forall a. a -> Maybe a
Just Instr
  (a : Head (LazyTake n out ++ Drop ('S n) out) : Drop ('S n) out)
  (Head (LazyTake n out ++ Drop ('S n) out) : a : Drop ('S n) out)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
  DIG PeanoNatural n
One -> Instr
  (Head (LazyTake n inp ++ Drop ('S n) inp) : a : Drop ('S n) inp)
  (a : Head (LazyTake n inp ++ Drop ('S n) inp) : Drop ('S n) inp)
-> Maybe
     (Instr
        (Head (LazyTake n inp ++ Drop ('S n) inp) : a : Drop ('S n) inp)
        (a : Head (LazyTake n inp ++ Drop ('S n) inp) : Drop ('S n) inp))
forall a. a -> Maybe a
Just Instr
  (Head (LazyTake n inp ++ Drop ('S n) inp) : a : Drop ('S n) inp)
  (a : Head (LazyTake n inp ++ Drop ('S n) inp) : Drop ('S n) inp)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

notIf :: Rule
notIf :: Rule
notIf = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  (Instr inp b
NOT :: Instr inp out) :# IF Instr s b
a Instr s b
b :# Instr b out
c | Sing (Head inp)
SingT n
STBool <- forall {k} (a :: k). SingI a => Sing a
forall (a :: T). SingI a => Sing a
sing @(Head inp) -> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a. a -> Maybe a
Just (Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out))
-> Instr ('TBool : s) out -> Maybe (Instr ('TBool : s) out)
forall a b. (a -> b) -> a -> b
$ Instr s b -> Instr s b -> Instr ('TBool : s) b
forall (s :: [T]) (out :: [T]).
Instr s out -> Instr s out -> Instr ('TBool : s) out
IF Instr s b
b Instr s b
a Instr ('TBool : s) b -> Instr b out -> Instr ('TBool : s) out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
c
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

-- | NB: This rule MUST be applied AFTER all main stages, but BEFORE nested dips
-- are rolled up
dipSwapDrop :: Rule
dipSwapDrop :: Rule
dipSwapDrop = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  DIP (Instr a b
SWAP :# Instr b c
DROP) -> 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
$ PeanoNatural ('S ('S 'Z)) -> Instr (b : s) s -> Instr inp out
forall (n :: Nat) (inp :: [T]) (out :: [T]) (s :: [T]) (s' :: [T]).
ConstraintDIPN n inp out s s' =>
PeanoNatural n -> Instr s s' -> Instr inp out
DIPN PeanoNatural ('S ('S 'Z))
forall (n :: Nat). (n ~ 'S ('S 'Z)) => PeanoNatural n
Two Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

dupDugDrop :: Rule
dupDugDrop :: Rule
dupDugDrop = (forall (inp :: [T]) (out :: [T]).
 Instr inp out -> Maybe (Instr inp out))
-> Rule
Rule \case
  Instr inp b
DUP :# DUG (Succ PeanoNatural m
m) :# Instr b b
DROP :# Instr b out
xs -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just (Instr inp out -> Maybe (Instr inp out))
-> Instr inp out -> Maybe (Instr inp out)
forall a b. (a -> b) -> a -> b
$ PeanoNatural m -> Instr inp b
forall (n :: Nat) (inp :: [T]) (out :: [T]) (a :: T).
ConstraintDUG n inp out a =>
PeanoNatural n -> Instr inp out
DUG PeanoNatural m
m Instr inp b -> Instr b out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr b out
xs
  Instr inp out
_ -> Maybe (Instr inp out)
forall a. Maybe a
Nothing