From fcb66475517e2e703e037eaa66218331170d764a Mon Sep 17 00:00:00 2001
From: Tom Jack <tom@tomjack.co>
Date: Sat, 4 Jul 2020 16:16:54 -0500
Subject: [PATCH 1/3] Strip annots in PUSH type

---
 src/passes/14-self_michelson/self_michelson.ml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/passes/14-self_michelson/self_michelson.ml b/src/passes/14-self_michelson/self_michelson.ml
index 8af08fb6a..ce11403a6 100644
--- a/src/passes/14-self_michelson/self_michelson.ml
+++ b/src/passes/14-self_michelson/self_michelson.ml
@@ -431,6 +431,7 @@ let prim_type_args : prim -> int option = function
   | I_EMPTY_MAP -> Some 2
   | I_EMPTY_BIG_MAP -> Some 2
   | I_LAMBDA -> Some 2
+  | I_PUSH -> Some 1
   (* _not_ I_CONTRACT! annot is important there *)
   (* but could include I_SELF, maybe? *)
   | _ -> None

From b905c495791320b7448b10988efce922392eee8a Mon Sep 17 00:00:00 2001
From: Tom Jack <tom@tomjack.co>
Date: Sat, 4 Jul 2020 16:26:33 -0500
Subject: [PATCH 2/3] Beta-reduce "inserted" Michelson lambdas

---
 .../14-self_michelson/self_michelson.ml       | 44 +++++++++++++++++++
 1 file changed, 44 insertions(+)

diff --git a/src/passes/14-self_michelson/self_michelson.ml b/src/passes/14-self_michelson/self_michelson.ml
index ce11403a6..0b88100b7 100644
--- a/src/passes/14-self_michelson/self_michelson.ml
+++ b/src/passes/14-self_michelson/self_michelson.ml
@@ -199,6 +199,7 @@ type peep1 = michelson -> michelson list option
 type peep2 = michelson * michelson -> michelson list option
 type peep3 = michelson * michelson * michelson -> michelson list option
 type peep4 = michelson * michelson * michelson * michelson -> michelson list option
+type peep5 = michelson * michelson * michelson * michelson * michelson -> michelson list option
 
 let rec peep1 (f : peep1) : michelson list -> bool * michelson list = function
   | [] -> (false, [])
@@ -242,6 +243,19 @@ let rec peep4 (f : peep4) : michelson list -> bool * michelson list = function
      | None -> let (changed, xs') = peep4 f (x2 :: x3 :: x4 :: xs) in
                (changed, x1 :: xs')
 
+let rec peep5 (f : peep5) : michelson list -> bool * michelson list = function
+  | [] -> (false, [])
+  | [x] -> (false, [x])
+  | [x ; y] -> (false, [x ; y])
+  | [x ; y ; z] -> (false, [x ; y ; z])
+  | [x ; y ; z ; w] -> (false, [x ; y ; z ; w])
+  | x1 :: x2 :: x3 :: x4 :: x5 :: xs ->
+     match f (x1, x2, x3, x4, x5) with
+     | Some xs' -> let (_, xs') = peep5 f (xs' @ xs) in
+                   (true, xs')
+     | None -> let (changed, xs') = peep5 f (x2 :: x3 :: x4 :: x5 :: xs) in
+               (changed, x1 :: xs')
+
 (* apply f to all seqs *)
 let rec peephole (f : michelson list -> bool * michelson list) : michelson -> bool * michelson =
   let peep_args ~seq args =
@@ -354,6 +368,34 @@ let opt_swap2 : peep2 = function
      Some [comm_op]
   | _ -> None
 
+(* for inserted Michelson lambdas *)
+let opt_beta3 : peep3 = function
+  (* PUSH (lambda ...) code ; SWAP ; EXEC  ↦  f *)
+  | Prim (_, I_PUSH, [Prim(_, T_lambda, _, _); code], _),
+    Prim (_, I_SWAP, _, _),
+    Prim (_, I_EXEC, _, _) ->
+      (match flatten_seqs code with
+       | Seq (_, code) -> Some code
+       | _ -> None)
+  | _ -> None
+
+let opt_beta5 : peep5 = function
+  (* PAIR ; DUP ; CDR ; SWAP ; CAR  ↦  *)
+  | Prim (_, I_PAIR, _, _),
+    Prim (_, I_DUP, _, _),
+    Prim (_, I_CDR, _, _),
+    Prim (_, I_SWAP, _, _),
+    Prim (_, I_CAR, _, _) ->
+    Some []
+  (* PAIR ; DUP ; CAR ; SWAP ; CDR  ↦  SWAP *)
+  | Prim (_, I_PAIR, _, _),
+    Prim (_, I_DUP, _, _),
+    Prim (_, I_CAR, _, _),
+    Prim (_, I_SWAP, _, _),
+    Prim (_, I_CDR, _, _) ->
+    Some [Prim(-1, I_SWAP, [], [])]
+  | _ -> None
+
 (* This "optimization" deletes dead code produced by the compiler
    after a FAILWITH, which is illegal in Michelson. This means we are
    thwarting the intent of the Michelson tail fail restriction -- the
@@ -483,6 +525,8 @@ let optimize : michelson -> michelson =
                      peephole @@ peep2 opt_dip2 ;
                      peephole @@ peep1 opt_dip1 ;
                      peephole @@ peep2 opt_swap2 ;
+                     peephole @@ peep3 opt_beta3 ;
+                     peephole @@ peep5 opt_beta5 ;
                    ] in
   let x = iterate_optimizer (sequence_optimizers optimizers) x in
   let x = opt_combine_drops x in

From 9b4e881827bb418e838ae7be03264f80c83ecd1c Mon Sep 17 00:00:00 2001
From: Tom Jack <tom@tomjack.co>
Date: Sat, 4 Jul 2020 23:16:42 -0500
Subject: [PATCH 3/3] fix expect test

---
 src/bin/expect_tests/code_insertion.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/src/bin/expect_tests/code_insertion.ml b/src/bin/expect_tests/code_insertion.ml
index 78a27def7..fa07169bb 100644
--- a/src/bin/expect_tests/code_insertion.ml
+++ b/src/bin/expect_tests/code_insertion.ml
@@ -51,9 +51,11 @@ let%expect_test _ =
     { parameter nat ;
       storage nat ;
       code { DUP ;
-             LAMBDA (pair nat nat) nat { { { DUP ; CDR ; SWAP ; CAR } } ; ADD } ;
+             DUP ;
+             CDR ;
              SWAP ;
-             EXEC ;
+             CAR ;
+             ADD ;
              NIL operation ;
              PAIR ;
              DIP { DROP } } } |}]