Revert "Remove the series of Let statements in favor of a fixpoint"

This reverts commit 0687a75d075d37ab36ef06b5f3228df801bd80e7.

1 files changed, 302 insertions, 236 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 8b04b566c..383da3310 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -687,19 +687,17 @@ Module Compilers.
     (** TODO: pick a better name for this (partial_expr?) *)
     Section interp.
       Context (var : type -> Type).
-      Definition interp_prestep_gen (interp_dom interp_cod : type -> Type) (t : type)
+      Definition interp_prestep (interp : type -> Type) (t : type)
         := match t return Type with
-           | type.prod A B as t => interp_cod A * interp_cod B
-           | type.arrow s d => interp_dom s -> interp_cod d
-           | type.list A => list (interp_cod A)
+           | type.prod A B as t => interp A * interp B
+           | type.arrow s d => interp s -> interp d
+           | type.list A => list (interp A)
            | type.unit as t
            | type.Z as t
            | type.nat as t
            | type.bool as t
              => type.interp t
            end%type.
-      Definition interp_prestep (interp : type -> Type) (t : type)
-        := interp_prestep_gen interp interp t.
       Definition interp_step (interp : type -> Type) (t : type)
         := match t return Type with
            | type.unit as t
@@ -715,75 +713,47 @@ Module Compilers.
       Fixpoint interp (t : type)
         := interp_step interp t.
 
-      Fixpoint interp_prestepn (n : nat) : type -> Type
-        := match n with
-           | O => interp
-           | S n' => interp_prestep_gen
-                       interp
-                       (interp_prestepn n')
-           end.
-
-      Definition lift_interp_prestep_gen
-                 {interp_dom1 interp_dom2 interp_cod1 interp_cod2 : type -> Type}
-                 (f_dom : forall A, interp_dom2 A -> interp_dom1 A)
-                 (f_cod : forall A, interp_cod1 A -> interp_cod2 A)
-                 {t : type}
-        : interp_prestep_gen interp_dom1 interp_cod1 t
-          -> interp_prestep_gen interp_dom2 interp_cod2 t
-        := match t return interp_prestep_gen interp_dom1 interp_cod1 t
-                          -> interp_prestep_gen interp_dom2 interp_cod2 t with
-           | type.prod A B
-             => fun '((a, b) : interp_cod1 A * interp_cod1 B)
-                => (f_cod A a, f_cod B b)
-           | type.arrow s d => fun f x => f_cod d (f (f_dom s x))
-           | type.list A
-             => List.map (f_cod A)
-           | type.unit
-           | type.nat
-           | type.Z
-           | type.bool
-             => id
-           end.
-
-      Definition uninterp_prestep_gen
-                 {interp_dom1 interp_cod1 : type -> Type}
-                 (f_dom : forall A, interp A -> interp_dom1 A)
-                 (f_cod : forall A, interp_cod1 A -> interp A)
-                 {t : type}
-        : interp_prestep_gen interp_dom1 interp_cod1 t
-          -> interp t
-        := match t return interp_prestep_gen interp_dom1 interp_cod1 t
-                          -> interp t with
-           | type.arrow s d
-             => fun f (x : interp s)
-                => f_cod d (f (f_dom s x))
-           | type.unit
+      Definition unprestep {t : type} : interp_prestep interp t -> interp t
+        := match t return interp_prestep interp t -> interp t with
+           | type.unit as t
+           | type.arrow _ _ as t
              => id
            | type.prod _ _ as t
            | type.list _ as t
-           | type.nat as t
            | type.Z as t
+           | type.nat as t
            | type.bool as t
-             => fun x => @inr (expr t) (interp_prestep interp t)
-                              (lift_interp_prestep_gen f_dom f_cod x)
-           end.
-
-        Fixpoint unprestepn {n : nat} : forall {t : type}, interp_prestepn n t -> interp t
-          := match n return forall t, interp_prestepn n t -> interp t with
-             | O => fun t v => v
-             | S n'
-               => @uninterp_prestep_gen
-                    interp (@interp_prestepn n')
-                    (fun _ => id)
-                    (@unprestepn n')
-             end.
+             => @inr _ (interp_prestep interp t)
+           end%type.
 
-        Definition unprestep {t : type} : interp_prestep interp t -> interp t
-          := @unprestepn 1 t.
+      Definition unprestep2 {t : type}
+        : interp_prestep (interp_prestep interp) t
+          -> match t with
+             | type.arrow _ _ => interp_prestep (interp_prestep interp) t
+             | t => interp_prestep interp t
+             end
+        := match t
+                 return (interp_prestep (interp_prestep interp) t
+                         -> match t with
+                            | type.arrow _ _ => interp_prestep (interp_prestep interp) t
+                            | t => interp_prestep interp t
+                            end)
+           with
+           | type.prod A B
+             => fun '((a, b) : interp_prestep interp A * interp_prestep interp B)
+                => (@unprestep A a, @unprestep B b)
+           | type.list A as t
+             => List.map (@unprestep A)
+           | type.arrow _ _ as t
+           | type.unit as t
+           | type.Z as t
+           | type.nat as t
+           | type.bool as t
+             => id
+           end%type.
     End interp.
     Arguments unprestep {var t} _.
-    Arguments uninterp_prestep_gen {var _ _} _ _ {t} _.
-    Arguments unprestepn {var n t} _.
+    Arguments unprestep2 {var t} _.
 
     Notation expr_const := const.
 
@@ -895,100 +865,6 @@ Module Compilers.
       End SmartLetIn.
     End expr.
 
-    Module Controlled.
-      Inductive arguments : type -> Set :=
-      | evaluated {T} (n : nat) : arguments T
-      | optionally {T} (a : arguments T) : arguments T
-      | arrow {s d} (sn : nat) (da : arguments d) : arguments (type.arrow s d).
-
-      Module Export Notations.
-        Bind Scope arguments_scope with arguments.
-        Delimit Scope arguments_scope with arguments.
-        Notation "!" := (@evaluated _) : arguments_scope.
-        Notation "a -> b" := (@arrow _ _ a%nat b%arguments) : arguments_scope.
-      End Notations.
-
-      Section with_var.
-        Context (var : type -> Type).
-
-        Fixpoint preinterp_in {t : type} (a : arguments t) : Type
-          := match a return Type with
-             | evaluated T n
-               => interp_prestepn var n T
-             | optionally T a
-               => option (@preinterp_in T a)
-             | arrow s d n da
-               => interp_prestepn var n s -> @preinterp_in d da
-             end.
-
-        Fixpoint preinterp_out {t : type} (a : arguments t) : Type
-          := match a return Type with
-             | evaluated T O
-               => interp var T
-             | evaluated T n
-               => @expr var T + interp_prestep (interp var) T
-             | optionally T a
-               => @preinterp_out T a
-             | arrow s d O da
-               => interp var s
-                  -> @preinterp_out d da
-             | arrow s d n da
-               => (@expr var s + interp_prestepn var n s)
-                  -> @preinterp_out d da
-             end.
-
-        Fixpoint out_expr {t} {a : arguments t} : @expr var t -> preinterp_out a
-          := match a in arguments t return expr t -> preinterp_out a with
-             | evaluated T O
-               => expr.reflect
-             | evaluated T n
-               => inl
-             | optionally T a
-               => @out_expr T a
-             | arrow s d O da
-               => fun e x
-                  => @out_expr d da (App e (expr.reify x))
-             | arrow s d sa da
-               => fun e x
-                  => @out_expr
-                       d da (App e match x with
-                                   | inl xe => xe
-                                   | inr xi => expr.reify (unprestepn xi)
-                                   end)
-             end.
-
-        Fixpoint defaulted_App {t} (default : @expr var t) (a : arguments t)
-          : preinterp_in a -> preinterp_out a
-          := match a in arguments t return expr t -> preinterp_in a -> preinterp_out a with
-             | evaluated T O => fun _ => id
-             | evaluated T n
-               => fun _ x => inr (@lift_interp_prestep_gen
-                                    (interp var) (interp var) (interp_prestepn var _) (interp var)
-                                    (fun _ => id)
-                                    (@unprestepn _ _)
-                                    _
-                                    x)
-             | optionally T a
-               => fun default (v : option (preinterp_in a))
-                  => match v with
-                     | Some v => @defaulted_App T default a v
-                     | None => out_expr default
-                     end
-             | arrow s d O da
-               => fun e F x
-                  => @defaulted_App d (App e (expr.reify x)) da (F x)
-             | arrow s d sa da
-               => fun e F x
-                  => match x return preinterp_out da with
-                     | inl xe => out_expr (App e xe)
-                     | inr xi => @defaulted_App d (App e (expr.reify (unprestepn xi))) da (F xi)
-                     end
-             end default.
-      End with_var.
-      Arguments defaulted_App {var t} _ _ _.
-    End Controlled.
-    Export Controlled.Notations.
-
     Definition sum_arrow {A A' B B'} (f : A -> A') (g : B -> B')
                (v : A + B)
       : A' + B'
@@ -1001,9 +877,214 @@ Module Compilers.
     Module ident.
       Section interp.
         Context {var : type -> Type}.
+        Let defaulted_App_p_e {A B} (idc : ident (A -> B))
+            (F : interp_prestep (interp var) A
+                 -> interp var B)
+          : @expr var A + interp_prestep (interp var) A
+            -> interp var B
+          := fun x
+             => match x with
+                | inl e => expr.reflect (App (Ident idc) e)
+                | inr x => F x
+                end.
+        Let defaulted_App_p_p {A B} (idc : ident (A -> B))
+            (F : interp_prestep (interp var) A
+                 -> interp_prestep (interp var) B)
+          : @expr var A + interp_prestep (interp var) A
+            -> @expr var B + interp_prestep (interp var) B
+          := (App (Ident idc) + F)%function.
+        Let defaulted_App_ep_p {A B C} (idc : ident (A -> B -> C))
+            (F : interp var A
+                 -> interp_prestep (interp var) B
+                 -> interp_prestep (interp var) C)
+          : interp var A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + interp_prestep (interp var) C
+          := fun x
+             => (App (App (Ident idc) (expr.reify x))
+                 + (F x))%function.
+        Let defaulted_App_eep_e {A B C D} (idc : ident (A -> B -> C -> D))
+            (F : interp var A
+                 -> interp var B
+                 -> interp_prestep (interp var) C
+                 -> interp var D)
+          : interp var A
+            -> interp var B
+            -> @expr var C + interp_prestep (interp var) C
+            -> interp var D
+          := fun x y z
+             => match z with
+                | inl z => expr.reflect (App (App (App (Ident idc) (expr.reify x)) (expr.reify y)) z)
+                | inr z => F x y z
+                end.
+        Let defaulted_App_pe_p {A B C} (idc : ident (A -> B -> C))
+            (F : interp_prestep (interp var) A
+                 -> interp var B
+                 -> interp_prestep (interp var) C)
+          : @expr var A + interp_prestep (interp var) A
+            -> interp var B
+            -> @expr var C + interp_prestep (interp var) C
+          := fun x y
+             => match x with
+                | inl x => inl (App (App (Ident idc) x) (expr.reify y))
+                | inr x => inr (F x y)
+                end.
+        Let defaulted_App_pep_p {A B C D} (idc : ident (A -> B -> C -> D))
+            (F : interp_prestep (interp var) A
+                 -> interp var B
+                 -> interp_prestep (interp var) C
+                 -> interp_prestep (interp var) D)
+          : @expr var A + interp_prestep (interp var) A
+            -> interp var B
+            -> @expr var C + interp_prestep (interp var) C
+            -> @expr var D + interp_prestep (interp var) D
+          := fun x y z
+             => let xz
+                    := match x, z with
+                       | inl x, inl z => inl (x, z)
+                       | inr x, inl z => inl (expr.reify (unprestep x), z)
+                       | inl x, inr z => inl (x, expr.reify (unprestep z))
+                       | inr x, inr z => inr (x, z)
+                       end in
+                match xz with
+                | inl (x, z) => inl (App (App (App (Ident idc) x) (expr.reify y)) z)
+                | inr (x, z) => inr (F x y z)
+                end.
+        Let defaulted_App_pp_p {A B C} (idc : ident (A -> B -> C))
+            (F : interp_prestep (interp var) A
+                 -> interp_prestep (interp var) B
+                 -> interp_prestep (interp var) C)
+          : @expr var A + interp_prestep (interp var) A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + interp_prestep (interp var) C
+          := fun x y
+             => let xy
+                    := match x, y with
+                       | inl x, inl y => inl (x, y)
+                       | inr x, inl y => inl (expr.reify (unprestep x), y)
+                       | inl x, inr y => inl (x, expr.reify (unprestep y))
+                       | inr x, inr y => inr (x, y)
+                       end in
+                match xy with
+                | inl (x, y) => inl (App (App (Ident idc) x) y)
+                | inr (x, y) => inr (F x y)
+                end.
+        Let defaulted_App_pp_p_or_pe_e_or_ep_e {A B C} (idc : ident (A -> B -> C))
+            (F : interp_prestep (interp var) A
+                 -> interp_prestep (interp var) B
+                 -> interp_prestep (interp var) C)
+            (F1 : interp_prestep (interp var) A
+                 -> @expr var B
+                 -> option (@expr var C + interp_prestep (interp var) C))
+            (F2 : @expr var A
+                 -> interp_prestep (interp var) B
+                 -> option (@expr var C + interp_prestep (interp var) C))
+          : @expr var A + interp_prestep (interp var) A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + interp_prestep (interp var) C
+          := fun x y
+             => let default := defaulted_App_pp_p idc F x y in
+                match x, y with
+                | inl x, inl y => inl (App (App (Ident idc) x) y)
+                | inl x, inr y => match F2 x y with
+                                  | Some Fxy => Fxy
+                                  | None => default
+                                  end
+                | inr x, inl y => match F1 x y with
+                                  | Some Fxy => Fxy
+                                  | None => default
+                                  end
+                | inr x, inr y => inr (F x y)
+                end.
+        Let defaulted_App_pp_p_or_pe_e_comm {A C} (idc : ident (A -> A -> C))
+            (F : interp_prestep (interp var) A
+                 -> interp_prestep (interp var) A
+                 -> interp_prestep (interp var) C)
+            (F1 : interp_prestep (interp var) A
+                 -> @expr var A
+                 -> option (@expr var C + interp_prestep (interp var) C))
+          : @expr var A + interp_prestep (interp var) A
+            -> @expr var A + interp_prestep (interp var) A
+            -> @expr var C + interp_prestep (interp var) C
+          := defaulted_App_pp_p_or_pe_e_or_ep_e
+               idc
+               F
+               F1
+               (fun x y => F1 y x).
+        Let defaulted_App_epp_e {A B C D} (idc : ident (A -> B -> C -> D))
+            (F : interp var A
+                 -> interp_prestep (interp var) B
+                 -> interp_prestep (interp var) C
+                 -> interp var D)
+          : interp var A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + interp_prestep (interp var) C
+            -> interp var D
+          := fun x y z
+             => let yz
+                    := match y, z with
+                       | inl y, inl z => inl (y, z)
+                       | inr y, inl z => inl (expr.reify (unprestep y), z)
+                       | inl y, inr z => inl (y, expr.reify (unprestep z))
+                       | inr y, inr z => inr (y, z)
+                       end in
+                match yz with
+                | inl (y, z) => expr.reflect (App (App (App (Ident idc) (expr.reify x)) y) z)
+                | inr (y, z) => F x y z
+                end.
+        Let defaulted_App_pp_p2 {A B C} (idc : ident (A -> B -> C))
+            (F : interp_prestep (interp var) A
+                 -> interp_prestep (interp var) B
+                 -> interp_prestep (interp_prestep (interp var)) C)
+          : @expr var A + interp_prestep (interp var) A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + match C with
+                             | type.arrow s d => interp_prestep (interp_prestep (interp var)) C
+                             | C => interp_prestep (interp var) C
+                             end
+          := fun x y
+             => let xy
+                    := match x, y with
+                       | inl x, inl y => inl (x, y)
+                       | inr x, inl y => inl (expr.reify (unprestep x), y)
+                       | inl x, inr y => inl (x, expr.reify (unprestep y))
+                       | inr x, inr y => inr (x, y)
+                       end in
+                match xy with
+                | inl (x, y) => inl (App (App (Ident idc) x) y)
+                | inr (x, y) => inr (unprestep2 (F x y))
+                end.
+        Let defaulted_App_ep_p2o {A B C} (idc : ident (A -> B -> C))
+            (F : interp var A
+                 -> interp_prestep (interp var) B
+                 -> option (interp_prestep (interp_prestep (interp var)) C))
+          : interp var A
+            -> @expr var B + interp_prestep (interp var) B
+            -> @expr var C + match C with
+                             | type.arrow s d => interp_prestep (interp_prestep (interp var)) C
+                             | C => interp_prestep (interp var) C
+                             end
+          := fun x y
+             => match y with
+                | inl y => inl (App (App (Ident idc) (expr.reify x)) y)
+                | inr y
+                  => match F x y with
+                     | Some Fxy => inr (unprestep2 Fxy)
+                     | None
+                       => inl (App (App (Ident idc) (expr.reify x)) (expr.reify (unprestep y)))
+                     end
+                end.
+
 
-        Local Notation defaulted_App idc args F
-          := (Controlled.defaulted_App (Ident idc) args F).
+
+        Let defaulted_App_ee_p {A B C} (idc : ident (A -> B -> C))
+            (F : interp var A
+                 -> interp var B
+                 -> interp_prestep (interp var) C)
+          : interp var A
+            -> interp var B
+            -> @expr var C + interp_prestep (interp var) C
+          := fun x y => inr (F x y).
 
         Definition interp {t} (idc : ident t) : interp var t
           := match idc in ident t return interp var t with
@@ -1014,19 +1095,18 @@ Module Compilers.
              | ident.nil t
                => inr (@nil (interp var t))
              | ident.cons t as idc
-               => defaulted_App idc (0->1->!1) (@cons (interp var t))
+               => defaulted_App_ep_p idc (@cons (interp var t))
              | ident.pair A B as idc
-               => defaulted_App idc (0->0->!1) (@pair (interp var A) (interp var B))
+               => defaulted_App_ee_p idc (@pair (interp var A) (interp var B))
              | ident.fst A B as idc
-               => defaulted_App idc (1->!0) (@fst (interp var A) (interp var B))
+               => defaulted_App_p_e idc (@fst (interp var A) (interp var B))
              | ident.snd A B as idc
-               => defaulted_App idc (1->!0) (@snd (interp var A) (interp var B))
+               => defaulted_App_p_e idc (@snd (interp var A) (interp var B))
              | ident.bool_rect T as idc
-               => defaulted_App idc (0->0->1->!0) (@bool_rect (fun _ => interp var T))
+               => defaulted_App_eep_e idc (@bool_rect (fun _ => interp var T))
              | ident.nat_rect P as idc
-               => defaulted_App
+               => defaulted_App_eep_e
                     idc
-                    (0->0->1->!0)
                     (fun O_case S_case n
                      => @nat_rect
                           (fun _ => interp var P)
@@ -1034,91 +1114,77 @@ Module Compilers.
                           (fun n' => S_case (inr n'))
                           n)
              | ident.List_seq as idc
-               => defaulted_App idc (1->1->!2) List.seq
+               => defaulted_App_pp_p2 idc List.seq
              | ident.List_repeat A as idc
-               => defaulted_App idc (0->1->!1) (@List.repeat (interp var A))
+               => defaulted_App_ep_p idc (@List.repeat (interp var A))
              | ident.List_combine A B as idc
-               => defaulted_App idc (1->1->!2) (@List.combine (interp var A) (interp var B))
+               => defaulted_App_pp_p2 idc (@List.combine (interp var A) (interp var B))
              | ident.List_map A B as idc
-               => defaulted_App idc (0->1->!1) (@List.map (interp var A) (interp var B))
+               => defaulted_App_ep_p idc (@List.map (interp var A) (interp var B))
              | ident.List_flat_map A B as idc
-               => defaulted_App
-                    idc (0->1->!0)
-                    (fun (f : interp var A -> expr (type.list B) + list (interp var B))
-                         (ls : list (interp var A))
-                     => match option_flat_map
-                                (fun x => match f x with
-                                          | inl _ => None
-                                          | inr v => Some v
-                                          end)
-                                ls
-                              return expr (type.list B) + list (interp var B)
-                        with
-                        | Some res => inr res
-                        | None
-                          => let ls'
-                                 := List.map
-                                      (fun x => match f x with
-                                                | inl e => e
-                                                | inr v => reify_list (List.map expr.reify v)
-                                                end)
-                                      ls in
-                             inl (reify_list_by_app ls')
-                        end)
+               => fun (f : interp var A -> expr (type.list B) + list (interp var B))
+                      (ls : expr (type.list A) + list (interp var A))
+                  => match ls return expr (type.list B) + list (interp var B) with
+                     | inl lse
+                       => inl (App (App (Ident idc) (expr.reify (t:=A->type.list B) f)) lse)
+                     | inr ls
+                       => match option_flat_map
+                                  (fun x => match f x with
+                                            | inl _ => None
+                                            | inr v => Some v
+                                            end)
+                                  ls
+                          with
+                          | Some res => inr res
+                          | None
+                            => let ls'
+                                   := List.map
+                                        (fun x => match f x with
+                                                  | inl e => e
+                                                  | inr v => reify_list (List.map expr.reify v)
+                                                  end)
+                                        ls in
+                               inl (reify_list_by_app ls')
+                          end
+                     end
              | ident.List_partition A as idc
-               => defaulted_App
-                    idc (0->1->Controlled.optionally (!2))
+               => defaulted_App_ep_p2o
+                    idc
                     (fun f => option_partition (fun x => match f x with
                                                          | inl _ => None
                                                          | inr b => Some b
                                                          end))
              | ident.List_app A as idc
-               => defaulted_App idc (1->1->!1) (@List.app (interp var A))
+               => defaulted_App_pp_p idc (@List.app (interp var A))
              | ident.List_rev A as idc
-               => defaulted_App idc (1->!1) (@List.rev (interp var A))
+               => defaulted_App_p_p idc (@List.rev (interp var A))
              | ident.List_fold_right A B as idc
-               => defaulted_App idc (0->0->1->!0) (@List.fold_right (interp var A) (interp var B))
+               => defaulted_App_eep_e idc (@List.fold_right (interp var A) (interp var B))
              | ident.List_update_nth T as idc
-               => defaulted_App idc (1->0->1->!1) (@update_nth (interp var T))
+               => defaulted_App_pep_p idc (@update_nth (interp var T))
              | ident.List_nth_default T as idc
-               => defaulted_App idc (0->1->1->!0) (@List.nth_default (interp var T))
+               => defaulted_App_epp_e idc (@List.nth_default (interp var T))
              | ident.pred as idc
              | ident.S as idc
              | ident.Z_of_nat as idc
              | ident.Z_opp as idc
-               => defaulted_App idc (1->!1) (ident.interp idc)
+               => defaulted_App_p_p idc (ident.interp idc)
              | ident.Z_runtime_mul as idc
-               => defaulted_App
-                    idc
-                    (0 -> 0 -> Controlled.optionally (!0))
-                    (fun x y
-                     => match x, y with
-                        | inr x, inr y
-                          => Some (inr (ident.interp idc x y))
-                        | inr x, inl y
-                        | inl y, inr x
-                          => if Z.eqb x 0
-                             then Some (inr 0%Z)
-                             else if Z.eqb x 1
-                                  then Some (inl y)
-                                  else None
-                        | inl x, inl y => None
-                        end)
+               => defaulted_App_pp_p_or_pe_e_comm
+                    idc (ident.interp idc)
+                    (fun x e
+                     => if Z.eqb x 0
+                        then Some (inr 0%Z)
+                        else if Z.eqb x 1
+                             then Some (inl e)
+                             else None)
              | ident.Z_runtime_add as idc
-               => defaulted_App
-                    idc
-                    (0 -> 0 -> Controlled.optionally (!0))
-                    (fun x y
-                     => match x, y with
-                        | inr x, inr y
-                          => Some (inr (ident.interp idc x y))
-                        | inr x, inl y
-                        | inl y, inr x
-                          => if Z.eqb x 0
-                             then Some (inl y)
-                             else None
-                        | inl x, inl y => None
-                        end)
+               => defaulted_App_pp_p_or_pe_e_comm
+                    idc (ident.interp idc)
+                    (fun x e
+                     => if Z.eqb x 0
+                        then Some (inl e)
+                        else None)
              | ident.Z_add as idc
              | ident.Z_mul as idc
              | ident.Z_pow as idc
@@ -1126,7 +1192,7 @@ Module Compilers.
              | ident.Z_modulo as idc
              | ident.Z_eqb as idc
              | ident.Nat_sub as idc
-               => defaulted_App idc (1->1->!1) (ident.interp idc)
+               => defaulted_App_pp_p idc (ident.interp idc)
              end.
       End interp.
     End ident.