Don't introduce extra lambdas and apps in uncurry

Previously I was trying to make the proof easier by using the same var
type for input and output (which would allow a
correctness-of-interpretation proof which doesn't depend on
well-formedness).  We now no longer do that, and instead go from `@expr
(@expr var)` to `@expr var`, and avoid introducing useless `Abs` and
`App` nodes.

1 files changed, 15 insertions, 13 deletions

diff --git a/src/Experiments/SimplyTypedArithmetic.v b/src/Experiments/SimplyTypedArithmetic.v
index 95b7d2c2c..79bedd94b 100644
--- a/src/Experiments/SimplyTypedArithmetic.v
+++ b/src/Experiments/SimplyTypedArithmetic.v
@@ -3607,32 +3607,34 @@ Module Compilers.
       Section with_var.
         Context {var : type -> Type}.
 
-        Fixpoint uncurry {t}
-          : @expr var t -> @expr var (type.uncurry t)
-          := match t return expr t -> expr (type.uncurry t) with
+        Fixpoint uncurry' {t}
+          : @expr (@expr var) t -> @expr var (type.uncurried_domain t) -> @expr var (type.final_codomain t)
+          := match t return expr t -> expr (type.uncurried_domain t) -> expr (type.final_codomain t) with
              | type.arrow s d
                => fun e
                   => let f := fun v
-                              => @uncurry
+                              => @uncurry'
                                    d
                                    match invert_Abs e with
                                    | Some f => f v
                                    | None => e @ Var v
                                    end%expr in
-                     match d return (var s -> expr (type.uncurry d)) -> expr (type.uncurry (s -> d)) with
+                     match d return (expr s -> expr (type.uncurried_domain d) -> expr (type.final_codomain d)) -> expr (type.uncurried_domain (s -> d)) -> expr (type.final_codomain d) with
                      | type.arrow _ _ as d
-                       => fun f
-                          => Abs (fun sdv
-                                  => Abs f @ (ident.fst @@ Var sdv) @ (ident.snd @@ Var sdv))
+                       => fun f sdv
+                          => f (ident.fst @@ sdv) (ident.snd @@ sdv)
                      | _
-                       => fun f
-                          => Abs (fun sv => f sv @ TT)
+                       => fun f sv => f sv TT
                      end f
              | type.type_primitive _
              | type.prod _ _
              | type.list _
-               => fun e => Abs (fun _ => e)
+               => fun e _ => unexpr e
              end%expr.
+
+        Definition uncurry {t} (e : @expr (@expr var) t)
+          : @expr var (type.uncurry t)
+          := Abs (fun v => @uncurry' t e (Var v)).
       End with_var.
 
       Definition Uncurry {t} (e : Expr t) : Expr (type.uncurry t)
@@ -6456,7 +6458,7 @@ Module test10.
     let v := Reify (fun (f : Z -> Z -> Z) x y => f (x + y) (x * y))%Z in
     pose v as E.
     vm_compute in E.
-    pose (PartialEvaluate true (Uncurry.expr.Uncurry (PartialEvaluate true (canonicalize_list_recursion E)))) as E'.
+    pose (Uncurry.expr.Uncurry (PartialEvaluate true (canonicalize_list_recursion E))) as E'.
     lazy in E'.
     clear E.
     lazymatch (eval cbv delta [E'] in E') with
@@ -6476,7 +6478,7 @@ Module test11.
     let v := Reify (fun x y => (fun f a b => f a b) (fun a b => a + b) (x + y) (x * y))%Z in
     pose v as E.
     vm_compute in E.
-    pose (PartialEvaluate true (Uncurry.expr.Uncurry (canonicalize_list_recursion E))) as E'.
+    pose (Uncurry.expr.Uncurry (PartialEvaluate true (canonicalize_list_recursion E))) as E'.
     lazy in E'.
     clear E.
     lazymatch (eval cbv delta [E'] in E') with