cakeml icon indicating copy to clipboard operation
cakeml copied to clipboard

Add optimizations for case when result is equal

Open ordinarymath opened this issue 1 year ago • 0 comments

when cakeml is given

fun evaluated_case_elim x =
  case x of
    A a => A a
  | B a b => B a b
  | C a b c => C a b c;

it results in cakeml doing a heap allocation to deconstruct and reconstruct the result. there should be an optimization that makes it rewritten to a form like

fun evaluated_case_elim x =
case x of
  A a => x
| B a b => x
| C a b c => x;

and it should be done such that when #1106 is done it is simplified into an identity function

ordinarymath avatar Dec 08 '24 08:12 ordinarymath