aboutsummaryrefslogtreecommitdiff
path: root/kernel/cbytecodes.ml
diff options
context:
space:
mode:
authorPierre Letouzey2015-12-16 00:59:38 +0100
committerPierre Letouzey2015-12-16 01:07:16 +0100
commit0c60735279301d22ac3e03f862f86997cb85bce0 (patch)
treea5c24cba2804ac4dc632353f7dfb96541e099bd5 /kernel/cbytecodes.ml
parent33742251e62a49c7996b96ca7077cf985627d14b (diff)
Extraction: fixed beta-red with Obj.magic (#2795 again) + other simplifications
Unfortunately, my first attempt at replacing (Obj.magic (fun x -> u) v) by ((fun x -> Obj.magic u) v) was badly typed, as seen in FingerTree: the argument v should also be magic now, otherwise it might not have the same type as x. This optimization is now correctly done, and to mitigate the potential inflation of Obj.magic, I've added a few simplification rules to avoid redundant magics, push them down inside terms, favor the form (Obj.magic f x y z), etc.
Diffstat (limited to 'kernel/cbytecodes.ml')
0 files changed, 0 insertions, 0 deletions