{-# OPTIONS_HADDOCK not-home #-}
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
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
<$>
[ ([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
]
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
, 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
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
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
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
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
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
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
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
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