Skip to content

Encode some info for optimizations

Clarification and motivation

Morley.Michelson.Optimizer has an awful lot of rules for individual operations that could be handled more cleanly/uniformly by encoding and using some stack info about each operation. As just one example, we have

justDrops :: Rule
justDrops = Rule $ \case
  CAR              :# DROP :# c -> Just $ DROP :# c
  CDR              :# DROP :# c -> Just $ DROP :# c
  SOME             :# DROP :# c -> Just $ DROP :# c
  ...

What's this rule really about? In plain language:

If an operation op only changes the element at the top of the stack, then op # drop = drop.

A (useful?) approximation:

Given op :: forall s. A : s -> B : s, op # drop = drop.

More generally, if we have op :: forall s. A1 : ... : Am : s -> B1 : B2 : ... : Bn : s, and k >= n - m, then op # dropN k = drop (k + m - n). We also have to include the special case of drop = dropN 1.

Acceptance criteria

  • Rewrite rules involving drop use information recorded about the stack effects of operations, rather than being custom coded per operation.
  • Rewrite rules for drop work also for dropN.