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

{-# OPTIONS_HADDOCK not-home #-}

-- | 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
forall b.
(Element [Ruleset -> Ruleset] -> b -> b)
-> b -> [Ruleset -> Ruleset] -> b
foldr Element [Ruleset -> Ruleset] -> Ruleset -> Ruleset
(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 out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp inp
Instr inp out
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 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 : c)
Instr (b : a : c) (a : b : c)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP Instr inp (a : b : c) -> Instr (a : b : c) out -> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr (a : b : c) 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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
i
  Seq Instr inp b
i Instr b out
Nop -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  DUPN PeanoNatural n
_             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
SWAP               :# Instr b b
SWAP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  PUSH Value' Instr t
_             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
NONE               :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
UNIT               :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
NIL                :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
EMPTY_SET          :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
EMPTY_MAP          :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
EMPTY_BIG_MAP      :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  LAMBDA IsNotInView => RemFail Instr '[i] '[o]
_           :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  SELF SomeEntrypointCallT arg
_             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
NOW                :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
AMOUNT             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
BALANCE            :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
TOTAL_VOTING_POWER :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
SOURCE             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
SENDER             :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
CHAIN_ID           :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
LEVEL              :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
SELF_ADDRESS       :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c
  Instr inp b
READ_TICKET        :# Instr b b
DROP :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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 c
Instr a c
f Instr inp c -> Instr c out -> Instr inp 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 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
Instr (b : a) a
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp a -> Instr a out -> Instr inp 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 Instr inp out -> Maybe (Instr inp out)
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 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 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 (LazyTake m (Tail inp) ++ s) ++ s')
-> Instr inp out
Instr
  (LazyTake m (Tail inp) ++ s)
  (LazyTake m (LazyTake m (Tail inp) ++ s) ++ s')
-> Instr
     (Head inp : (LazyTake m (Tail inp) ++ s))
     (Head inp : (LazyTake m (LazyTake m (Tail inp) ++ s) ++ 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 (LazyTake m (Tail inp) ++ s) ++ s')
 -> Instr inp out)
-> Maybe
     (Instr
        (LazyTake m (Tail inp) ++ s)
        (LazyTake m (LazyTake m (Tail inp) ++ s) ++ s'))
-> Maybe (Instr inp out)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Instr
  (LazyTake m (Tail inp) ++ s)
  (LazyTake m (LazyTake m (Tail inp) ++ s) ++ s')
-> Maybe
     (Instr
        (LazyTake m (Tail inp) ++ s)
        (LazyTake m (LazyTake m (Tail inp) ++ s) ++ 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 (LazyTake m (Tail inp) ++ s) ++ 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 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
Instr (a : s) b
f 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
RIGHT :# IF_LEFT Instr (a : s) b
_ Instr (b : 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
$ Instr inp b
Instr (b : s) b
f 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
CONS  :# 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
$ Instr inp b
Instr (a : 'TList a : s) b
f 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
NIL   :# IF_CONS Instr (a : 'TList a : s) b
_ Instr 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
$ Instr inp b
Instr s b
f 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
NONE  :# IF_NONE Instr s b
f Instr (a : 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
$ Instr inp b
Instr s b
f 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
SOME  :# 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
$ Instr inp b
Instr (a : s) b
f 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 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 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
Instr s b
f 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 (VOption Maybe (Value' Instr t1)
Nothing)    :# IF_NONE Instr s b
f Instr (a : 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
$ Instr inp b
Instr s b
f 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 (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 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
Instr s b
f 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 (VBool Bool
False)        :# IF Instr s b
_ Instr 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
$ Instr inp b
Instr s b
f 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

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 out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp inp
Instr inp out
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 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 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 inp (b : c) -> Instr (b : c) out -> Instr inp 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 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 s
Instr ('TBool : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp s -> Instr s out -> Instr inp 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 out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp inp
Instr inp out
forall (inp :: [T]). Instr inp inp
Nop
  DIPN PeanoNatural n
_ Instr s s'
Nop -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp inp
Instr inp out
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 (AddPeano n ('S 'Z)) inp ~ b,
      IsLongerOrSameLength inp (AddPeano n ('S 'Z)) ~ '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) :~: AddPeano ('S 'Z) 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 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 ((b ~ b, 'True ~ 'True) => Instr inp out)
-> Dict
     (Drop (AddPeano ('S 'Z) n) (a : b) ~ b,
      IsLongerOrSameLength (a : b) (AddPeano ('S 'Z) 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 ('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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr b out
c

  Instr inp b
UNPAIR :# Instr b b
PAIR :# Instr b out
c -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
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 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
Instr (a : b) b
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP 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
PAIR :# Instr b b
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 (b : s) s -> Instr (a : b : s) (a : s)
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr (b : s) s
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP) Instr inp (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 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 Instr inp out -> Maybe (Instr inp out)
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 out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp inp
Instr inp out
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 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 (Tail inp)
Instr (Head inp : Tail inp) (Tail inp)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (Tail inp) -> Instr (Tail inp) out -> Instr 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 Instr inp out -> Maybe (Instr inp out)
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ (a : b : s), out ~ ('TPair a b : s)) =>
Instr inp out
PAIR ((inp ~ (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) inp)) =>
 Maybe (Instr inp out))
-> (inp :~: (Head inp : Head (Tail inp) : Drop ('S ('S 'Z)) 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 ('S ('S m)) (Tail inp))
pairn <- Instr
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop ('S ('S m)) (Tail inp))
-> Maybe
     (Instr
        (Tail inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
           : Drop ('S ('S m)) (Tail 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 ('S ('S m)) (Tail inp))
 -> Maybe
      (Instr
         (Tail inp)
         (RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
            : Drop ('S ('S m)) (Tail inp))))
-> Instr
     (Tail inp)
     (RightComb
        (Head (Tail inp)
           : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop ('S ('S m)) (Tail inp))
-> Maybe
     (Instr
        (Tail inp)
        (RightComb
           (Head (Tail inp)
              : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
           : Drop ('S ('S m)) (Tail 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 ('S ('S m)) (Tail 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 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
  (Tail inp)
  (RightComb
     (Head (Tail inp)
        : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop ('S ('S m)) (Tail inp))
-> Instr
     (Head inp : Tail inp)
     (Head inp
        : RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop ('S ('S m)) (Tail 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 ('S ('S m)) (Tail inp))
pairn Instr
  inp
  (Head inp
     : RightComb
         (Head (Tail inp)
            : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
     : Drop ('S ('S m)) (Tail inp))
-> Instr
     (Head inp
        : RightComb
            (Head (Tail inp)
               : Head (Tail (Tail inp)) : LazyTake m (Tail (Tail (Tail inp))))
        : Drop ('S ('S m)) (Tail inp))
     out
-> Instr inp out
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 ('S ('S m)) (Tail inp))
  out
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 Instr inp out -> Maybe (Instr inp out)
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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
forall {inp :: [T]} {out :: [T]} (a :: T) (b :: T) (s :: [T]).
(inp ~ ('TPair a b : s), out ~ (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
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s)
        : Head
            (Tail
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s))
        : LazyTake
            m
            (Tail
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s)))))
   ++ s)
unpairn <- Instr
  (RightComb
     (Head
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s)
        : Head
            (Tail
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s))
        : LazyTake
            m
            (Tail
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s)))))
   ++ s)
-> Maybe
     (Instr
        (RightComb
           (Head
              (UnpairN
                 ('S ('S m))
                 (RightComb
                    (Head (Tail out)
                       : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
               ++ s)
              : Head
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))
              : LazyTake
                  m
                  (Tail
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s))))
           : s)
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head
                 (UnpairN
                    ('S ('S m))
                    (RightComb
                       (Head (Tail out)
                          : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                  ++ s)
                 : Head
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s))
                 : LazyTake
                     m
                     (Tail
                        (Tail
                           (UnpairN
                              ('S ('S m))
                              (RightComb
                                 (Head (Tail out)
                                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                            ++ s)))))
         ++ s))
forall (inp :: [T]) (out :: [T]).
Instr inp out -> Maybe (Instr inp out)
go (Instr
   (RightComb
      (Head
         (UnpairN
            ('S ('S m))
            (RightComb
               (Head (Tail out)
                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
          ++ s)
         : Head
             (Tail
                (UnpairN
                   ('S ('S m))
                   (RightComb
                      (Head (Tail out)
                         : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                 ++ s))
         : LazyTake
             m
             (Tail
                (Tail
                   (UnpairN
                      ('S ('S m))
                      (RightComb
                         (Head (Tail out)
                            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                    ++ s))))
      : s)
   (UnpairN
      ('S ('S m))
      (RightComb
         (Head
            (UnpairN
               ('S ('S m))
               (RightComb
                  (Head (Tail out)
                     : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
             ++ s)
            : Head
                (Tail
                   (UnpairN
                      ('S ('S m))
                      (RightComb
                         (Head (Tail out)
                            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                    ++ s))
            : LazyTake
                m
                (Tail
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s)))))
    ++ s)
 -> Maybe
      (Instr
         (RightComb
            (Head
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s)
               : Head
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s))
               : LazyTake
                   m
                   (Tail
                      (Tail
                         (UnpairN
                            ('S ('S m))
                            (RightComb
                               (Head (Tail out)
                                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                          ++ s))))
            : s)
         (UnpairN
            ('S ('S m))
            (RightComb
               (Head
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s)
                  : Head
                      (Tail
                         (UnpairN
                            ('S ('S m))
                            (RightComb
                               (Head (Tail out)
                                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                          ++ s))
                  : LazyTake
                      m
                      (Tail
                         (Tail
                            (UnpairN
                               ('S ('S m))
                               (RightComb
                                  (Head (Tail out)
                                     : Head (Tail (Tail out))
                                     : LazyTake m (Tail (Tail (Tail out)))))
                             ++ s)))))
          ++ s)))
-> Instr
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))))
        : s)
     (UnpairN
        ('S ('S m))
        (RightComb
           (Head
              (UnpairN
                 ('S ('S m))
                 (RightComb
                    (Head (Tail out)
                       : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
               ++ s)
              : Head
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))
              : LazyTake
                  m
                  (Tail
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s)))))
      ++ s)
-> Maybe
     (Instr
        (RightComb
           (Head
              (UnpairN
                 ('S ('S m))
                 (RightComb
                    (Head (Tail out)
                       : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
               ++ s)
              : Head
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))
              : LazyTake
                  m
                  (Tail
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s))))
           : s)
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head
                 (UnpairN
                    ('S ('S m))
                    (RightComb
                       (Head (Tail out)
                          : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                  ++ s)
                 : Head
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s))
                 : LazyTake
                     m
                     (Tail
                        (Tail
                           (UnpairN
                              ('S ('S m))
                              (RightComb
                                 (Head (Tail out)
                                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                            ++ s)))))
         ++ s))
forall a b. (a -> b) -> a -> b
$ PeanoNatural m
-> Instr
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))))
        : s)
     (UnpairN
        m
        (RightComb
           (Head
              (UnpairN
                 ('S ('S m))
                 (RightComb
                    (Head (Tail out)
                       : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
               ++ s)
              : Head
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s))
              : LazyTake
                  m
                  (Tail
                     (Tail
                        (UnpairN
                           ('S ('S m))
                           (RightComb
                              (Head (Tail out)
                                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                         ++ s)))))
      ++ 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 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
  (Head out
     : RightComb
         (Head
            (UnpairN
               ('S ('S m))
               (RightComb
                  (Head (Tail out)
                     : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
             ++ s)
            : Head
                (Tail
                   (UnpairN
                      ('S ('S m))
                      (RightComb
                         (Head (Tail out)
                            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                    ++ s))
            : LazyTake
                m
                (Tail
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s))))
     : 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
  (Head out
     : RightComb
         (Head
            (UnpairN
               ('S ('S m))
               (RightComb
                  (Head (Tail out)
                     : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
             ++ s)
            : Head
                (Tail
                   (UnpairN
                      ('S ('S m))
                      (RightComb
                         (Head (Tail out)
                            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                    ++ s))
            : LazyTake
                m
                (Tail
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s))))
     : s)
-> Instr
     (Head out
        : RightComb
            (Head
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s)
               : Head
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s))
               : LazyTake
                   m
                   (Tail
                      (Tail
                         (UnpairN
                            ('S ('S m))
                            (RightComb
                               (Head (Tail out)
                                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                          ++ s))))
        : s)
     out
-> Instr inp out
forall (inp :: [T]) (out :: [T]) (b :: [T]).
Instr inp b -> Instr b out -> Instr inp out
:# Instr
  (RightComb
     (Head
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s)
        : Head
            (Tail
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s))
        : LazyTake
            m
            (Tail
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s)))))
   ++ s)
-> Instr
     (Head out
        : RightComb
            (Head
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s)
               : Head
                   (Tail
                      (UnpairN
                         ('S ('S m))
                         (RightComb
                            (Head (Tail out)
                               : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                       ++ s))
               : LazyTake
                   m
                   (Tail
                      (Tail
                         (UnpairN
                            ('S ('S m))
                            (RightComb
                               (Head (Tail out)
                                  : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                          ++ s))))
        : s)
     (Head out
        : (UnpairN
             ('S ('S m))
             (RightComb
                (Head
                   (UnpairN
                      ('S ('S m))
                      (RightComb
                         (Head (Tail out)
                            : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                    ++ s)
                   : Head
                       (Tail
                          (UnpairN
                             ('S ('S m))
                             (RightComb
                                (Head (Tail out)
                                   : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                           ++ s))
                   : LazyTake
                       m
                       (Tail
                          (Tail
                             (UnpairN
                                ('S ('S m))
                                (RightComb
                                   (Head (Tail out)
                                      : Head (Tail (Tail out))
                                      : LazyTake m (Tail (Tail (Tail out)))))
                              ++ s)))))
           ++ s))
forall (a :: [T]) (c :: [T]) (b :: T).
Instr a c -> Instr (b : a) (b : c)
DIP Instr
  (RightComb
     (Head
        (UnpairN
           ('S ('S m))
           (RightComb
              (Head (Tail out)
                 : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
         ++ s)
        : Head
            (Tail
               (UnpairN
                  ('S ('S m))
                  (RightComb
                     (Head (Tail out)
                        : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                ++ s))
        : LazyTake
            m
            (Tail
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))))
     : s)
  (UnpairN
     ('S ('S m))
     (RightComb
        (Head
           (UnpairN
              ('S ('S m))
              (RightComb
                 (Head (Tail out)
                    : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
            ++ s)
           : Head
               (Tail
                  (UnpairN
                     ('S ('S m))
                     (RightComb
                        (Head (Tail out)
                           : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                   ++ s))
           : LazyTake
               m
               (Tail
                  (Tail
                     (UnpairN
                        ('S ('S m))
                        (RightComb
                           (Head (Tail out)
                              : Head (Tail (Tail out)) : LazyTake m (Tail (Tail (Tail out)))))
                      ++ s)))))
   ++ 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 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 n -> PeanoNatural ('S ('S ('S m)))
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
    ((('TPair b b : s) ~ ('TPair b b : s)) => Instr inp out)
-> (('TPair b b : s) :~: ('TPair b b : s)) -> 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 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
     ('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 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
UNPAIR :# DIP (UNPAIRN n :: PeanoNatural n
n@(Succ Succ{})) :# 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
     ('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 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

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

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 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 : b)
Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (b : b) -> Instr (b : b) out -> Instr inp 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 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 (c : b)
Instr (MemOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (c : b) -> Instr (c : b) out -> Instr inp 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 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 (c : b)
Instr (GetOpKey c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (c : b) -> Instr (c : b) out -> Instr inp 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 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 ('TLambda ('TPair a b) c : 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 inp ('TLambda ('TPair a b) c : b)
-> Instr ('TLambda ('TPair a b) c : b) out -> Instr inp 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 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 (c : b)
Instr (c : c : b) (c : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (c : b) -> Instr (c : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 ('TMutez : b)
Instr ('TMutez : 'TMutez : b) ('TMutez : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp ('TMutez : b) -> Instr ('TMutez : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (m : b)
Instr (n : m : b) (m : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (m : b) -> Instr (m : b) out -> Instr inp 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 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 (n : b)
Instr (n : n : b) (n : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (n : b) -> Instr (n : b) out -> Instr inp 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 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 ('TNat : b)
Instr (a : 'TNat : b) ('TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp ('TNat : b) -> Instr ('TNat : b) out -> Instr inp 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 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 ('TPair 'TNat 'TNat : b)
Instr
  ('TTicket a : 'TPair 'TNat 'TNat : b) ('TPair 'TNat 'TNat : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp ('TPair 'TNat 'TNat : b)
-> Instr ('TPair 'TNat 'TNat : b) out -> Instr inp 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 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 : b)
Instr (a : b : b) (b : b)
forall (a :: T) (out :: [T]). Instr (a : out) out
DROP Instr inp (b : b) -> Instr (b : b) out -> Instr inp 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 inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr
  (a : Head out : Drop ('S ('S 'Z)) out)
  (Head out : a : Drop ('S ('S 'Z)) out)
forall (a :: T) (b :: T) (s :: [T]). Instr (a : b : s) (b : a : s)
SWAP
  DIG PeanoNatural n
One -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just Instr inp out
Instr
  (Head inp : a : Drop ('S ('S 'Z)) inp)
  (a : Head inp : Drop ('S ('S 'Z)) 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 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 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 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

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