Use to_expr_App instead of to_expr so that reduction works correctly (#…

…79)

src/Rewriter/Language/UnderLets.v

@@ -107,6 +107,12 @@ Module Compilers.
            | UnderLet A x f
              => expr.LetIn x (fun v => @to_expr _ (f v))
            end.
+      Fixpoint to_expr_App {t} (x : @UnderLets (expr t)) : expr t
+        := match x with
+           | Base v => v
+           | UnderLet A x f
+             => expr.App (expr.Abs (fun v => @to_expr_App _ (f v))) x
+           end.
       Fixpoint of_expr {t} (x : expr t) : @UnderLets (expr t)
         := match x in expr.expr t return @UnderLets (expr t) with
            | expr.LetIn A B x f
@@ -263,5 +269,5 @@ Module Compilers.
     End reify.
   End UnderLets.
   Export UnderLets.Notations.
-  Global Strategy -1000 [UnderLets.to_expr].
+  Global Strategy -1000 [UnderLets.to_expr UnderLets.to_expr_App].
 End Compilers.

src/Rewriter/Language/UnderLetsCacheProofs.v

@@ -43,7 +43,7 @@ Module Compilers.
                  (fun t e v => expr.interp ident_interp e = v)
                  (fun e v => expr.interp ident_interp e = v)
                  v
-                 (expr.interp ident_interp (UnderLets.to_expr e) = v)
+                 (expr.interp ident_interp (UnderLets.to_expr_App e) = v)
                  e.
 
           Lemma cached_interp_related_impl {t} e v