Optimizer.hs

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

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

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

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

import Prelude hiding (EQ, GT, LT)

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

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

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

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

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

instance Default OptimizerConf where
  def = defaultOptimizerConf

-- | Optimize a typed instruction by replacing some sequences of
-- instructions with smaller equivalent sequences.
-- Applies default set of rewrite rules.
optimize :: Instr inp out -> Instr inp out
optimize = optimizeWithConf def

-- | Optimize a typed instruction using a custom set of rules.
-- The set is divided into several stages, as applying
-- some rules can prevent others to be performed.
optimizeWithConf :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf (OptimizerConf ocGotoValues rules) instr = foldl (flip performOneStage) instrRHS rules
  where
    dfsSettings = def{ dsGoToValues = ocGotoValues }
    performOneStage stageRules =
      dfsModifyInstr dfsSettings $ applyOnce stageRules
    instrRHS = applyOnce (fixpoint flattenSeqLHS) instr

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

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

defaultRules :: [Rule]
defaultRules = map fixpoint
  [ mainStageRules
  , glueAdjacentDropsStageRules
  ]
  where
    glueAdjacentDropsStageRules = flattenSeqLHS `orSimpleRule` adjacentDrops

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

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

flattenSeqLHS :: Rule -> Rule
flattenSeqLHS toplevel = Rule $ \case
  it@(Seq (Seq _ _) _) -> Just $ linearizeAndReapply toplevel it
  _                    -> Nothing

removeNesting :: Rule
removeNesting = Rule $ \case
  Nested i -> Just i
  _        -> Nothing

-- | STACKTYPE is currently a Nop and may safely be removed.
removeExtStackType :: Rule
removeExtStackType = Rule $ \case
  Ext (STACKTYPE{}) -> Just Nop
  _                 -> Nothing

dipDrop2swapDrop :: Rule
dipDrop2swapDrop = Rule $ \case
  DIP DROP -> Just $ SWAP :# DROP
  _        -> Nothing

ifNopNop2Drop :: Rule
ifNopNop2Drop = Rule $ \case
  IF Nop Nop -> Just DROP
  _          -> Nothing

nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq = Rule $ \case
  Nop :# i   -> Just i
  i   :# Nop -> Just i
  _          -> Nothing

variousNops :: Rule
variousNops = Rule $ \case
  DUP                :# DROP :# c -> Just c
  DUPN _             :# DROP :# c -> Just c
  SWAP               :# SWAP :# c -> Just c
  PUSH _             :# DROP :# c -> Just c
  NONE               :# DROP :# c -> Just c
  UNIT               :# DROP :# c -> Just c
  NIL                :# DROP :# c -> Just c
  EMPTY_SET          :# DROP :# c -> Just c
  EMPTY_MAP          :# DROP :# c -> Just c
  EMPTY_BIG_MAP      :# DROP :# c -> Just c
  LAMBDA _           :# DROP :# c -> Just c
  SELF _             :# DROP :# c -> Just c
  NOW                :# DROP :# c -> Just c
  AMOUNT             :# DROP :# c -> Just c
  BALANCE            :# DROP :# c -> Just c
  TOTAL_VOTING_POWER :# DROP :# c -> Just c
  SOURCE             :# DROP :# c -> Just c
  SENDER             :# DROP :# c -> Just c
  CHAIN_ID           :# DROP :# c -> Just c
  LEVEL              :# DROP :# c -> Just c
  SELF_ADDRESS       :# DROP :# c -> Just c
  READ_TICKET        :# DROP :# c -> Just c

  DUP                :# DROP -> Just Nop
  DUPN _             :# DROP -> Just Nop
  SWAP               :# SWAP -> Just Nop
  PUSH _             :# DROP -> Just Nop
  NONE               :# DROP -> Just Nop
  UNIT               :# DROP -> Just Nop
  NIL                :# DROP -> Just Nop
  EMPTY_SET          :# DROP -> Just Nop
  EMPTY_MAP          :# DROP -> Just Nop
  EMPTY_BIG_MAP      :# DROP -> Just Nop
  LAMBDA _           :# DROP -> Just Nop
  SELF _             :# DROP -> Just Nop
  NOW                :# DROP -> Just Nop
  AMOUNT             :# DROP -> Just Nop
  BALANCE            :# DROP -> Just Nop
  TOTAL_VOTING_POWER :# DROP -> Just Nop
  SOURCE             :# DROP -> Just Nop
  SENDER             :# DROP -> Just Nop
  CHAIN_ID           :# DROP -> Just Nop
  LEVEL              :# DROP -> Just Nop
  SELF_ADDRESS       :# DROP -> Just Nop
  READ_TICKET        :# DROP -> Just Nop
  _                          -> Nothing

dupSwap2dup :: Rule
dupSwap2dup = Rule $ \case
  DUP :# SWAP :# c -> Just (DUP :# c)
  DUP :# SWAP      -> Just DUP
  _                -> Nothing

noDipNeeded :: Rule
noDipNeeded = Rule $ \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 x    :# DIP f :# c -> Just $ f :# PUSH x :# c
  PUSH x    :# DIP f      -> Just $ f :# PUSH x
  UNIT      :# DIP f :# c -> Just $ f :# UNIT :# c
  UNIT      :# DIP f      -> Just $ f :# UNIT
  NOW       :# DIP f :# c -> Just $ f :# NOW :# c
  NOW       :# DIP f      -> Just $ f :# NOW
  SENDER    :# DIP f :# c -> Just $ f :# SENDER :# c
  SENDER    :# DIP f      -> Just $ f :# SENDER
  EMPTY_MAP :# DIP f :# c -> Just $ f :# EMPTY_MAP :# c
  EMPTY_MAP :# DIP f      -> Just $ f :# EMPTY_MAP
  EMPTY_SET :# DIP f :# c -> Just $ f :# EMPTY_SET :# c
  EMPTY_SET :# DIP f      -> Just $ f :# EMPTY_SET

  -- If we do something ignoring top of the stack and then immediately
  -- drop top of the stack, we can drop that item in advance and
  -- not use 'DIP' at all.
  DIP f :# DROP :# c -> Just $ DROP :# f :# c
  DIP f :# DROP         -> Just $ DROP :# f

  _ -> Nothing

branchShortCut :: Rule
branchShortCut = Rule $ \case
  LEFT  :# IF_LEFT f _ :# c -> Just (f :# c)
  RIGHT :# IF_LEFT _ f :# c -> Just (f :# c)
  CONS  :# IF_CONS f _ :# c -> Just (f :# c)
  NIL   :# IF_CONS _ f :# c -> Just (f :# c)
  NONE  :# IF_NONE f _ :# c -> Just (f :# c)
  SOME  :# IF_NONE _ f :# c -> Just (f :# c)

  PUSH vOr@(VOr eitherVal) :# IF_LEFT f g :# c -> case vOr of
    (_ :: Value ('TOr l r)) -> case eitherVal of
      Left val -> case checkScope @(ConstantScope l) of
        Right Dict -> Just (PUSH val :# f :# c)
        _          -> Nothing
      Right val -> case checkScope @(ConstantScope r) of
        Right Dict -> Just (PUSH val :# g :# c)
        _          -> Nothing
  PUSH (VList (x : xs))     :# IF_CONS f _ :# c -> Just (PUSH (VList xs) :# PUSH x :# f :# c)
  PUSH (VList _)            :# IF_CONS _ f :# c -> Just (f :# c)
  PUSH (VOption Nothing)    :# IF_NONE f _ :# c -> Just (f :# c)
  PUSH (VOption (Just val)) :# IF_NONE _ f :# c -> Just (PUSH val :# f :# c)
  PUSH (VBool True)         :# IF f _      :# c -> Just (f :# c)
  PUSH (VBool False)        :# IF _ f      :# c -> Just (f :# c)

  LEFT  :# IF_LEFT f _ -> Just f
  RIGHT :# IF_LEFT _ f -> Just f
  CONS  :# IF_CONS f _ -> Just f
  NIL   :# IF_CONS _ f -> Just f
  NONE  :# IF_NONE f _ -> Just f
  SOME  :# IF_NONE _ f -> Just f

  PUSH vOr@(VOr eitherVal) :# IF_LEFT f g -> case vOr of
    (_ :: Value ('TOr l r)) -> case eitherVal of
      Left val -> case checkScope @(ConstantScope l) of
        Right Dict -> Just (PUSH val :# f)
        _          -> Nothing
      Right val -> case checkScope @(ConstantScope r) of
        Right Dict -> Just (PUSH val :# g)
        _          -> Nothing
  PUSH (VList (x : xs))     :# IF_CONS f _ -> Just (PUSH (VList xs) :# PUSH x :# f)
  PUSH (VList _)            :# IF_CONS _ f -> Just f
  PUSH (VOption Nothing)    :# IF_NONE f _ -> Just f
  PUSH (VOption (Just val)) :# IF_NONE _ f -> Just (PUSH val :# f)
  PUSH (VBool True)         :# IF f _      -> Just f
  PUSH (VBool False)        :# IF _ f      -> Just f

  _ -> Nothing

compareWithZero :: Rule
compareWithZero = Rule $ \case
  PUSH (VInt 0) :# COMPARE :# EQ :# c -> Just $ EQ :# c
  PUSH (VNat 0) :# COMPARE :# EQ :# c -> Just $ INT :# EQ :# c
  PUSH (VInt 0) :# COMPARE :# EQ      -> Just $ EQ
  PUSH (VNat 0) :# COMPARE :# EQ      -> Just $ INT :# EQ
  _                                   -> Nothing

simpleDrops :: Rule
simpleDrops = Rule $ \case
  -- DROP 0 is Nop
  DROPN Zero :# c -> Just c
  DROPN Zero -> Just Nop

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

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

  _ -> 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 $ \case
  DIP Nop      -> Just Nop
  DIP Nop :# c -> Just c

  _ -> Nothing

simpleDips :: Rule
simpleDips = Rule $ \case
  -- DIP 0 is redundant
  DIPN Zero i :# c -> Just (i :# c)
  DIPN Zero i -> Just i

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

  _ -> Nothing

simpleDups :: Rule
simpleDups = Rule $ \case
  -- DUP 1 is just DUP
  DUPN One :# xs -> Just $ DUP :# xs
  DUPN One -> Just $ DUP

  _ -> Nothing

adjacentDips :: Rule
adjacentDips = Rule $ \case
  DIP f :# DIP g -> Just (DIP (f :# g))
  DIP f :# DIP g :# c -> Just (DIP (f :# g) :# c)

  _ -> Nothing

redundantIf :: Rule
redundantIf = Rule \case
  IF x y :# xs
    | x == y
    -> Just $ DROP :# x :# xs
  IF x y
    | x == y
    -> Just $ DROP :# x
  _ -> Nothing

emptyDip :: Rule
emptyDip = Rule \case
  DIP Nop :# xs -> Just xs
  DIP Nop -> Just Nop
  DIPN _ Nop :# xs -> Just xs
  DIPN _ Nop -> Just Nop
  _ -> Nothing

digDug :: Rule
digDug = Rule \case
  (DIG (x :: PeanoNatural n) :: Instr inp t) :# (DUG y :: Instr t out) :# xs
    | Just Refl <- eqPeanoNat x y
    -> Just xs
  (DIG (x :: PeanoNatural n) :: Instr inp t) :# (DUG y :: Instr t out)
    | Just Refl <- eqPeanoNat x y
    -> Just Nop
  _ -> Nothing

-- TODO [#299]: optimize sequences of more than 2 DROPs.
-- | Sequences of @DROP@s can be turned into single @DROP n@.
-- When @n@ is greater than 2 it saves size and gas.
-- When @n@ is 2 it saves gas only.
adjacentDrops :: Rule
adjacentDrops = Rule $ \case
  DROP :# DROP -> Just (DROPN Two)
  DROP :# DROP :# c -> Just (DROPN Two :# c)

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

  _ -> Nothing

specificPush :: Rule
specificPush = Rule $ \case
  push@PUSH{}         -> optimizePush push
  push@PUSH{} :# c -> (:# c) <$> optimizePush push

  _ -> Nothing
  where
    optimizePush :: Instr inp out -> Maybe (Instr inp out)
    optimizePush = \case
      PUSH v | _ :: Value v <- v -> case v of
        VUnit -> Just UNIT
        VMap m
          | null m -> case sing @v of STMap{} -> Just EMPTY_MAP
        VSet m
          | null m -> case sing @v of STSet{} -> Just EMPTY_SET
        _ -> Nothing

      _ -> Nothing


isSomeOnIf :: Rule
isSomeOnIf = Rule $ \case
  IF (PUSH (VOption Just{})) (PUSH (VOption Nothing)) :# c -> case c of
    IF_NONE (PUSH (VBool False)) (DROP :# PUSH (VBool True)) :# s -> Just s
    IF_NONE (PUSH (VBool False)) (DROP :# PUSH (VBool True))      -> Just Nop
    _ -> Nothing
  _ -> Nothing

pairUnpair :: Rule
pairUnpair = Rule $ \case
  PAIR :# UNPAIR :# c -> Just c
  PAIR :# UNPAIR      -> Just Nop

  UNPAIR :# PAIR :# c -> Just c
  UNPAIR :# PAIR      -> Just Nop

  _ -> Nothing

pairMisc :: Rule
pairMisc = Rule $ \case
  PAIR :# CDR :# c -> Just $ DROP :# c
  PAIR :# CDR      -> Just DROP

  PAIR :# CAR :# c -> Just $ (DIP DROP) :# c
  PAIR :# CAR      -> Just $ DIP DROP

  _ -> Nothing

unpairMisc :: Rule
unpairMisc = Rule $ \case
  DUP :# CAR :# DIP CDR      -> Just $ UNPAIR
  DUP :# CAR :# DIP CDR :# c -> Just $ UNPAIR :# c

  DUP :# CDR :# DIP CAR      -> Just $ UNPAIR :# SWAP
  DUP :# CDR :# DIP CAR :# c -> Just $ UNPAIR :# SWAP :# c

  UNPAIR :# DROP             -> Just CDR
  UNPAIR :# DROP :# c        -> Just $ CDR :# c
  _ -> Nothing

commuteArith ::
  forall n m s out. Instr (n ': m ': s) out -> Maybe (Instr (m ': n ': s) out)
commuteArith = \case
  ADD -> do Dict <- commutativityProof @Add @n @m; Just ADD
  MUL -> do Dict <- commutativityProof @Mul @n @m; Just MUL
  OR -> do Dict <- commutativityProof @Or @n @m; Just OR
  AND -> do Dict <- commutativityProof @And @n @m; Just AND
  XOR -> do Dict <- commutativityProof @Xor @n @m; Just XOR
  _ -> Nothing

swapBeforeCommutative :: Rule
swapBeforeCommutative = Rule $ \case
  SWAP :# i :# c -> (:# c) <$> commuteArith i
  SWAP :# i -> commuteArith i

  _ -> Nothing

pushPack :: Rule
pushPack = Rule $ \case
  PUSH x :# PACK -> Just (pushPacked x)
  PUSH x :# PACK :# c -> Just (pushPacked x :# c)

  _ -> Nothing
  where
    pushPacked :: PackedValScope t => Value t -> Instr s ('TBytes ': s)
    pushPacked = PUSH . VBytes . packValue'

justDrops :: Rule
justDrops = Rule $ \case
  CAR              :# DROP :# c -> Just $ DROP :# c
  CDR              :# DROP :# c -> Just $ DROP :# c
  SOME             :# DROP :# c -> Just $ DROP :# c
  LEFT             :# DROP :# c -> Just $ DROP :# c
  RIGHT            :# DROP :# c -> Just $ DROP :# c
  SIZE             :# DROP :# c -> Just $ DROP :# c
  GETN _           :# DROP :# c -> Just $ DROP :# c
  CAST             :# DROP :# c -> Just $ DROP :# c
  RENAME           :# DROP :# c -> Just $ DROP :# c
  PACK             :# DROP :# c -> Just $ DROP :# c
  UNPACK           :# DROP :# c -> Just $ DROP :# c
  CONCAT'          :# DROP :# c -> Just $ DROP :# c
  ISNAT            :# DROP :# c -> Just $ DROP :# c
  ABS              :# DROP :# c -> Just $ DROP :# c
  NEG              :# DROP :# c -> Just $ DROP :# c
  NOT              :# DROP :# c -> Just $ DROP :# c
  EQ               :# DROP :# c -> Just $ DROP :# c
  NEQ              :# DROP :# c -> Just $ DROP :# c
  LT               :# DROP :# c -> Just $ DROP :# c
  GT               :# DROP :# c -> Just $ DROP :# c
  LE               :# DROP :# c -> Just $ DROP :# c
  GE               :# DROP :# c -> Just $ DROP :# c
  INT              :# DROP :# c -> Just $ DROP :# c
  CONTRACT _       :# DROP :# c -> Just $ DROP :# c
  SET_DELEGATE     :# DROP :# c -> Just $ DROP :# c
  IMPLICIT_ACCOUNT :# DROP :# c -> Just $ DROP :# c
  VOTING_POWER     :# DROP :# c -> Just $ DROP :# c
  SHA256           :# DROP :# c -> Just $ DROP :# c
  SHA512           :# DROP :# c -> Just $ DROP :# c
  BLAKE2B          :# DROP :# c -> Just $ DROP :# c
  SHA3             :# DROP :# c -> Just $ DROP :# c
  KECCAK           :# DROP :# c -> Just $ DROP :# c
  HASH_KEY         :# DROP :# c -> Just $ DROP :# c
  PAIRING_CHECK    :# DROP :# c -> Just $ DROP :# c
  ADDRESS          :# DROP :# c -> Just $ DROP :# c
  JOIN_TICKETS     :# DROP :# c -> Just $ DROP :# c

  CAR              :# DROP      -> Just DROP
  CDR              :# DROP      -> Just DROP
  SOME             :# DROP      -> Just DROP
  LEFT             :# DROP      -> Just DROP
  RIGHT            :# DROP      -> Just DROP
  SIZE             :# DROP      -> Just DROP
  GETN _           :# DROP      -> Just DROP
  CAST             :# DROP      -> Just DROP
  RENAME           :# DROP      -> Just DROP
  PACK             :# DROP      -> Just DROP
  UNPACK           :# DROP      -> Just DROP
  CONCAT'          :# DROP      -> Just DROP
  ISNAT            :# DROP      -> Just DROP
  ABS              :# DROP      -> Just DROP
  NEG              :# DROP      -> Just DROP
  NOT              :# DROP      -> Just DROP
  EQ               :# DROP      -> Just DROP
  NEQ              :# DROP      -> Just DROP
  LT               :# DROP      -> Just DROP
  GT               :# DROP      -> Just DROP
  LE               :# DROP      -> Just DROP
  GE               :# DROP      -> Just DROP
  INT              :# DROP      -> Just DROP
  CONTRACT _       :# DROP      -> Just DROP
  SET_DELEGATE     :# DROP      -> Just DROP
  IMPLICIT_ACCOUNT :# DROP      -> Just DROP
  VOTING_POWER     :# DROP      -> Just DROP
  SHA256           :# DROP      -> Just DROP
  SHA512           :# DROP      -> Just DROP
  BLAKE2B          :# DROP      -> Just DROP
  SHA3             :# DROP      -> Just DROP
  KECCAK           :# DROP      -> Just DROP
  HASH_KEY         :# DROP      -> Just DROP
  PAIRING_CHECK    :# DROP      -> Just DROP
  ADDRESS          :# DROP      -> Just DROP
  JOIN_TICKETS     :# DROP      -> Just DROP
  _                             -> Nothing

justDoubleDrops :: Rule
justDoubleDrops = Rule $ \case
  PAIR         :# DROP :# c -> Just $ DROP :# DROP :# c
  MEM          :# DROP :# c -> Just $ DROP :# DROP :# c
  GET          :# DROP :# c -> Just $ DROP :# DROP :# c
  APPLY        :# DROP :# c -> Just $ DROP :# DROP :# c
  CONCAT       :# DROP :# c -> Just $ DROP :# DROP :# c
  ADD          :# DROP :# c -> Just $ DROP :# DROP :# c
  SUB          :# DROP :# c -> Just $ DROP :# DROP :# c
  SUB_MUTEZ    :# DROP :# c -> Just $ DROP :# DROP :# c
  MUL          :# DROP :# c -> Just $ DROP :# DROP :# c
  EDIV         :# DROP :# c -> Just $ DROP :# DROP :# c
  OR           :# DROP :# c -> Just $ DROP :# DROP :# c
  AND          :# DROP :# c -> Just $ DROP :# DROP :# c
  XOR          :# DROP :# c -> Just $ DROP :# DROP :# c
  COMPARE      :# DROP :# c -> Just $ DROP :# DROP :# c
  TICKET       :# DROP :# c -> Just $ DROP :# DROP :# c
  SPLIT_TICKET :# DROP :# c -> Just $ DROP :# DROP :# c
  SWAP :# DROP :# DROP :# c -> Just $ DROP :# DROP :# c

  PAIR         :# DROP      -> Just $ DROP :# DROP
  MEM          :# DROP      -> Just $ DROP :# DROP
  GET          :# DROP      -> Just $ DROP :# DROP
  APPLY        :# DROP      -> Just $ DROP :# DROP
  CONCAT       :# DROP      -> Just $ DROP :# DROP
  ADD          :# DROP      -> Just $ DROP :# DROP
  SUB          :# DROP      -> Just $ DROP :# DROP
  SUB_MUTEZ    :# DROP      -> Just $ DROP :# DROP
  MUL          :# DROP      -> Just $ DROP :# DROP
  EDIV         :# DROP      -> Just $ DROP :# DROP
  OR           :# DROP      -> Just $ DROP :# DROP
  AND          :# DROP      -> Just $ DROP :# DROP
  XOR          :# DROP      -> Just $ DROP :# DROP
  COMPARE      :# DROP      -> Just $ DROP :# DROP
  TICKET       :# DROP      -> Just $ DROP :# DROP
  SPLIT_TICKET :# DROP      -> Just $ DROP :# DROP
  SWAP :# DROP :# DROP      -> Just $ DROP :# DROP

  _ -> Nothing

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

  other -> applyOnce restart other

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

-- | Combine two rule fixpoints.
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> (Rule -> Rule)
orRule l r topl = Rule $ \instr ->
  (unRule (l topl) $ instr) <|> (unRule (r topl) $ instr)

-- | Combine a rule fixpoint and a simple rule.
orSimpleRule :: (Rule -> Rule) -> Rule -> (Rule -> Rule)
orSimpleRule l r topl = Rule $ \instr ->
  (unRule (l topl) $ instr) <|> (unRule r $ instr)

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

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

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

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

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