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

-- | Optimizer for typed instructions.
--
-- It's quite experimental and incomplete.
-- List of possible improvements:
-- 1. 'pushDrop', 'dupDrop', 'unitDrop' rules are essentially the
-- same. It would be good to generalize them into one rule. The same
-- applies to 'pushDip'.
-- It probably can be done more efficiently.

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

import Prelude hiding (EQ)

import Data.Constraint (Dict(..))
import Data.Default (Default(def))
import Data.Singletons (sing)

import Michelson.Interpret.Pack (packValue')
import Michelson.Typed.Aliases (Value)
import Michelson.Typed.Arith
import Michelson.Typed.Instr
import Michelson.Typed.Scope (PackedValScope)
import Michelson.Typed.Sing
import Michelson.Typed.T
import Michelson.Typed.Util (DfsSettings(..), dfsInstr)
import Michelson.Typed.Value
import Util.Peano (SingNat(..))

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

data OptimizerConf = OptimizerConf
  { OptimizerConf -> Bool
gotoValues :: Bool
  , OptimizerConf -> Rule -> Rule
ruleset    :: Rule -> Rule
  }

instance Default OptimizerConf where
  def :: OptimizerConf
def = $WOptimizerConf :: Bool -> (Rule -> Rule) -> OptimizerConf
OptimizerConf
    { gotoValues :: Bool
gotoValues = Bool
False
    , ruleset :: Rule -> Rule
ruleset    = Rule -> Rule
defaultRules
    }

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

-- | Optimize a typed instruction using a custom set of rules.
optimizeWithConf :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf :: OptimizerConf -> Instr inp out -> Instr inp out
optimizeWithConf (OptimizerConf gotoValues :: Bool
gotoValues rules :: Rule -> Rule
rules)
  = ((Instr inp out, ()) -> Instr inp out
forall a b. (a, b) -> a
fst ((Instr inp out, ()) -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
  ((Instr inp out -> (Instr inp out, ()))
 -> Instr inp out -> Instr inp out)
-> (Instr inp out -> (Instr inp out, ()))
-> Instr inp out
-> Instr inp out
forall a b. (a -> b) -> a -> b
$ DfsSettings ()
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall x (inp :: [T]) (out :: [T]).
Semigroup x =>
DfsSettings x
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, x))
-> Instr inp out
-> (Instr inp out, x)
dfsInstr DfsSettings ()
dfsSettings
  ((forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
 -> Instr inp out -> (Instr inp out, ()))
-> (forall (i :: [T]) (o :: [T]). Instr i o -> (Instr i o, ()))
-> Instr inp out
-> (Instr inp out, ())
forall a b. (a -> b) -> a -> b
$ (Instr i o -> (Instr i o, ())
forall a. a -> (a, ())
adapter (Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
forall b c a. (b -> c) -> (a -> b) -> a -> c
.)
  ((Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ()))
-> (Instr i o -> Instr i o) -> Instr i o -> (Instr i o, ())
forall a b. (a -> b) -> a -> b
$ Rule -> Instr i o -> Instr i o
forall (inp :: [T]) (out :: [T]).
Rule -> Instr inp out -> Instr inp out
applyOnce
  (Rule -> Instr i o -> Instr i o) -> Rule -> Instr i o -> Instr i o
forall a b. (a -> b) -> a -> b
$ (Rule -> Rule) -> Rule
fixpoint Rule -> Rule
rules
  where
    dfsSettings :: DfsSettings ()
dfsSettings = DfsSettings ()
forall a. Default a => a
def{ dsGoToValues :: Bool
dsGoToValues = Bool
gotoValues }

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

-- Type of a single rewrite rule. 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`.
type Rule = forall inp out. Instr inp out -> Maybe (Instr inp out)

defaultRules :: Rule -> Rule
defaultRules :: Rule -> Rule
defaultRules =
  Rule -> Rule
flattenSeqLHS
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
removeNesting
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dipDrop2swapDrop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
ifNopNop2Drop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
nopIsNeutralForSeq
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
variousNops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
dupSwap2dup
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
noDipNeeded
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
branchShortCut
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
compareWithZero
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDrops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
internalNop
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
simpleDips
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDips
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
adjacentDrops
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
specificPush
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pairUnpair
    (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
swapBeforeCommutative

-- | 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 :: Rule -> Rule
defaultRulesAndPushPack :: Rule -> Rule
defaultRulesAndPushPack = Rule -> Rule
defaultRules (Rule -> Rule) -> Rule -> Rule -> Rule
`orSimpleRule` Rule
pushPack

flattenSeqLHS :: Rule -> Rule
flattenSeqLHS :: Rule -> Rule
flattenSeqLHS toplevel :: Rule
toplevel = \case
  it :: Instr inp out
it@(Seq (Seq _ _) _) -> 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
  _                    -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

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

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

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

nopIsNeutralForSeq :: Rule
nopIsNeutralForSeq :: Instr inp out -> Maybe (Instr inp out)
nopIsNeutralForSeq = \case
  Seq Nop i :: Instr b out
i  -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
i
  Seq i :: Instr inp b
i Nop  -> Instr inp b -> Maybe (Instr inp b)
forall a. a -> Maybe a
Just Instr inp b
i
  _          -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

variousNops :: Rule
variousNops :: Instr inp out -> Maybe (Instr inp out)
variousNops = \case
  Seq  SWAP    (Seq SWAP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq (PUSH _) (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  DUP     (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  UNIT    (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  NOW     (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  SENDER  (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  EMPTY_MAP (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  Seq  EMPTY_SET (Seq DROP c :: Instr b out
c) -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c

  Seq  SWAP         SWAP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq (PUSH _)      DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  DUP          DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  UNIT         DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  NOW          DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  SENDER       DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  EMPTY_MAP   DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq  EMPTY_SET   DROP    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  _                         -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

dupSwap2dup :: Rule
dupSwap2dup :: Instr inp out -> Maybe (Instr inp out)
dupSwap2dup = \case
  Seq DUP (Seq SWAP c :: Instr b out
c) -> Instr (a : s) out -> Maybe (Instr (a : s) out)
forall a. a -> Maybe a
Just (Instr (a : s) (a : a : s)
-> Instr (a : a : s) out -> Instr (a : s) out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]). Instr (a : s) (a : a : s)
DUP Instr b out
Instr (a : a : s) out
c)
  Seq DUP      SWAP    -> Instr (a : s) (a : a : s) -> Maybe (Instr (a : s) (a : a : s))
forall a. a -> Maybe a
Just      Instr (a : s) (a : a : s)
forall (a :: T) (s :: [T]). Instr (a : s) (a : a : s)
DUP
  _                    -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

noDipNeeded :: Rule
noDipNeeded :: Instr inp out -> Maybe (Instr inp out)
noDipNeeded = \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.
  Seq (PUSH x :: Value' Instr t
x) (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c (t : c) -> Instr (t : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq (Value' Instr t -> Instr c (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x) Instr b out
Instr (t : c) out
c))
  Seq (PUSH x :: Value' Instr t
x)      (DIP f :: Instr a c
f)    -> Instr a (t : c) -> Maybe (Instr a (t : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c (t : c) -> Instr a (t : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      (Value' Instr t -> Instr c (t : c)
forall (t :: T) (s :: [T]).
ConstantScope t =>
Value' Instr t -> Instr s (t : s)
PUSH Value' Instr t
x))
  Seq UNIT     (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c ('TUnit : c) -> Instr ('TUnit : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr c ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
UNIT Instr b out
Instr ('TUnit : c) out
c))
  Seq UNIT          (DIP f :: Instr a c
f)    -> Instr a ('TUnit : c) -> Maybe (Instr a ('TUnit : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c ('TUnit : c) -> Instr a ('TUnit : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      Instr c ('TUnit : c)
forall (s :: [T]). Instr s ('TUnit : s)
UNIT)
  Seq NOW     (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c ('TTimestamp : c)
-> Instr ('TTimestamp : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr c ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
NOW Instr b out
Instr ('TTimestamp : c) out
c))
  Seq NOW          (DIP f :: Instr a c
f)    -> Instr a ('TTimestamp : c) -> Maybe (Instr a ('TTimestamp : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c ('TTimestamp : c) -> Instr a ('TTimestamp : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      Instr c ('TTimestamp : c)
forall (s :: [T]). Instr s ('TTimestamp : s)
NOW)
  Seq SENDER  (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c ('TAddress : c) -> Instr ('TAddress : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr c ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
SENDER Instr b out
Instr ('TAddress : c) out
c))
  Seq SENDER       (DIP f :: Instr a c
f)    -> Instr a ('TAddress : c) -> Maybe (Instr a ('TAddress : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c ('TAddress : c) -> Instr a ('TAddress : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      Instr c ('TAddress : c)
forall (s :: [T]). Instr s ('TAddress : s)
SENDER)
  Seq EMPTY_MAP     (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c ('TMap a b : c) -> Instr ('TMap a b : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr c ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(KnownT a, KnownT b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP Instr b out
Instr ('TMap a b : c) out
c))
  Seq EMPTY_MAP          (DIP f :: Instr a c
f)    -> Instr a ('TMap a b : c) -> Maybe (Instr a ('TMap a b : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c ('TMap a b : c) -> Instr a ('TMap a b : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      Instr c ('TMap a b : c)
forall (a :: T) (b :: T) (s :: [T]).
(KnownT a, KnownT b, Comparable a) =>
Instr s ('TMap a b : s)
EMPTY_MAP)
  Seq EMPTY_SET     (Seq (DIP f :: Instr a c
f) c :: Instr b out
c) -> Instr a out -> Maybe (Instr a out)
forall a. a -> Maybe a
Just (Instr a c -> Instr c out -> Instr a out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f (Instr c ('TSet e : c) -> Instr ('TSet e : c) out -> Instr c out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr c ('TSet e : c)
forall (e :: T) (s :: [T]).
(KnownT e, Comparable e) =>
Instr s ('TSet e : s)
EMPTY_SET Instr b out
Instr ('TSet e : c) out
c))
  Seq EMPTY_SET          (DIP f :: Instr a c
f)    -> Instr a ('TSet e : c) -> Maybe (Instr a ('TSet e : c))
forall a. a -> Maybe a
Just (Instr a c -> Instr c ('TSet e : c) -> Instr a ('TSet e : c)
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr a c
f      Instr c ('TSet e : c)
forall (e :: T) (s :: [T]).
(KnownT e, Comparable e) =>
Instr s ('TSet e : s)
EMPTY_SET)

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

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

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

  Seq (PUSH (VBool True))  (Seq (IF f :: Instr s b
f _) c :: Instr b out
c) -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr s b
f Instr b out
c)
  Seq (PUSH (VBool False)) (Seq (IF _ f :: Instr s b
f) c :: Instr b out
c) -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just (Instr s b -> Instr b out -> Instr s out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr s b
f Instr b out
c)

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

  Seq (PUSH (VBool True))  (IF f :: Instr s out
f _) -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f
  Seq (PUSH (VBool False)) (IF _ f :: Instr s out
f) -> Instr s out -> Maybe (Instr s out)
forall a. a -> Maybe a
Just Instr s out
f

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

compareWithZero :: Rule
compareWithZero :: Instr inp out -> Maybe (Instr inp out)
compareWithZero = \case
  Seq (PUSH (VInt 0)) (Seq COMPARE (Seq EQ c :: Instr b out
c)) -> Instr ('TInt : s) out -> Maybe (Instr ('TInt : s) out)
forall a. a -> Maybe a
Just          (Instr ('TInt : s) b -> Instr b out -> Instr ('TInt : s) out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ Instr b out
c)
  Seq (PUSH (VNat 0)) (Seq COMPARE (Seq EQ c :: Instr b out
c)) -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr ('TNat : s) ('TInt : s)
forall (s :: [T]). Instr ('TNat : s) ('TInt : s)
INT (Instr ('TInt : s) b -> Instr b out -> Instr ('TInt : s) out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr ('TInt : s) b
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ Instr b out
c))
  Seq (PUSH (VInt 0)) (Seq COMPARE      EQ)    -> Instr inp out -> Maybe (Instr inp out)
forall a. a -> Maybe a
Just               Instr inp out
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ
  Seq (PUSH (VNat 0)) (Seq COMPARE      EQ)    -> Instr ('TNat : s) out -> Maybe (Instr ('TNat : s) out)
forall a. a -> Maybe a
Just (Instr ('TNat : s) ('TInt : s)
-> Instr ('TInt : s) out -> Instr ('TNat : s) out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
Seq Instr ('TNat : s) ('TInt : s)
forall (s :: [T]). Instr ('TNat : s) ('TInt : s)
INT      Instr ('TInt : s) out
forall (n :: T) (s :: [T]).
UnaryArithOp Eq' n =>
Instr (n : s) (UnaryArithRes Eq' n : s)
EQ)
  _                                                  -> Maybe (Instr inp out)
forall a. Maybe a
Nothing

simpleDrops :: Rule
simpleDrops :: Instr inp out -> Maybe (Instr inp out)
simpleDrops = \case
  -- DROP 0 is Nop
  Seq (DROPN SZ) c :: Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c
  DROPN SZ -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop

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

  -- Seq (DROPN (SS SZ)) c -> Just (Seq DROP c)
  -- DROPN (SS SZ) -> Just DROP

  _ -> 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 :: Instr inp out -> Maybe (Instr inp out)
internalNop = \case
  DIP Nop -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop
  Seq (DIP Nop) c :: Instr b out
c -> Instr b out -> Maybe (Instr b out)
forall a. a -> Maybe a
Just Instr b out
c

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

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

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

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

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

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

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

  -- Does not compile, need to do something smart
  -- Seq (DROPN (SS (SS SZ))) DROP -> Just (DROPN (SS $ SS $ SS SZ))

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

specificPush :: Rule
specificPush :: Instr inp out -> Maybe (Instr inp out)
specificPush = \case
  push :: Instr inp out
push@PUSH{} -> Instr inp out -> Maybe (Instr inp out)
Rule
optimizePush Instr inp out
push
  Seq (push :: Instr inp b
push@PUSH{}) c :: Instr b out
c -> (Instr inp b -> Instr b out -> Instr inp out
forall (a :: [T]) (b :: [T]) (c :: [T]).
Instr a b -> Instr b c -> Instr a c
`Seq` Instr 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)
Rule
optimizePush Instr inp b
push

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

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

-- UNPAIR with continuation
pattern UNPAIR_c
  :: ()
  => (i ~ ('TPair a b : s), i' ~ (a : b : s), o' ~ o)
  => Instr i' o' -> Instr i o
pattern $bUNPAIR_c :: Instr i' o' -> Instr i o
$mUNPAIR_c :: forall r (i :: [T]) (o :: [T]).
Instr i o
-> (forall (a :: T) (b :: T) (s :: [T]) (i' :: [T]) (o' :: [T]).
    (i ~ ('TPair a b : s), i' ~ (a : b : s), o' ~ o) =>
    Instr i' o' -> r)
-> (Void# -> r)
-> r
UNPAIR_c c = Seq DUP (Seq CAR (Seq (DIP CDR) c))

pairUnpair :: Rule
pairUnpair :: Instr inp out -> Maybe (Instr inp out)
pairUnpair = \case
  Seq PAIR (UNPAIR_c c :: Instr i' o'
c) -> Instr i' o' -> Maybe (Instr i' o')
forall a. a -> Maybe a
Just Instr i' o'
c
  Seq PAIR UNPAIR       -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop

  UNPAIR_c (Seq PAIR c :: Instr b o'
c) -> Instr b o' -> Maybe (Instr b o')
forall a. a -> Maybe a
Just Instr b o'
c
  UNPAIR_c      PAIR    -> Instr inp inp -> Maybe (Instr inp inp)
forall a. a -> Maybe a
Just Instr inp inp
forall (s :: [T]). Instr s s
Nop

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

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

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

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

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

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

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

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

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

-- | Combine two rule fixpoints.
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> (Rule -> Rule)
orRule :: (Rule -> Rule) -> (Rule -> Rule) -> Rule -> Rule
orRule l :: Rule -> Rule
l r :: Rule -> Rule
r topl :: Rule
topl x :: Instr inp out
x = Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
l Rule
topl Instr inp out
x Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
r Rule
topl Instr inp out
x

-- | Combine a rule fixpoint and a simple rule.
orSimpleRule :: (Rule -> Rule) -> Rule -> (Rule -> Rule)
orSimpleRule :: (Rule -> Rule) -> Rule -> Rule -> Rule
orSimpleRule l :: Rule -> Rule
l r :: Rule
r topl :: Rule
topl x :: Instr inp out
x = Rule -> Instr inp out -> Maybe (Instr inp out)
Rule -> Rule
l Rule
topl Instr inp out
x Maybe (Instr inp out)
-> Maybe (Instr inp out) -> Maybe (Instr inp out)
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Instr inp out -> Maybe (Instr inp out)
Rule
r Instr inp out
x

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

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

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

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