Switch to fully uncurried form for reflection

This will eventually make a number of proofs easier.

Unfortunately, the correctness lemmas for AddCoordinates and LadderStep
no longer work (because of different arities), and there's a proof in
Experiments/Ed25519 that I've admitted.

The correctness lemmas will be easy to re-add when we have a more
general version that handle arbitrary type shapes.

1 files changed, 5 insertions, 13 deletions

diff --git a/src/Reflection/Eta.v b/src/Reflection/Eta.v
index 62e0a525e..6a15ce60e 100644
--- a/src/Reflection/Eta.v
+++ b/src/Reflection/Eta.v
@@ -27,16 +27,8 @@ Section language.
 
       Section gen_type.
         Context (exprf_eta : forall {t} (e : exprf t), exprf t).
-        Fixpoint expr_eta_gen {t} (e : expr t) : expr t
-          := match e with
-             | Return _ v => exprf_eta _ v
-             | Abs src dst f => @Abs
-                                  _ _ _
-                                  src dst
-                                  (interp_flat_type_eta_gen
-                                     (fun x : interp_flat_type var (Tbase src)
-                                      => @expr_eta_gen _ (f x)))
-             end.
+        Definition expr_eta_gen {t} (e : expr t) : expr (Arrow (domain t) (codomain t))
+          := Abs (interp_flat_type_eta_gen (fun x => exprf_eta _ (invert_Abs e x))).
       End gen_type.
 
       Fixpoint exprf_eta_gen {t} (e : exprf t) : exprf t
@@ -64,10 +56,10 @@ Section language.
     Definition expr_eta' {t}
       := @expr_eta_gen (fun _ _ x => (fst x, snd x)) (@exprf_eta') t.
   End with_var.
-  Definition ExprEtaGen eta {t} (e : Expr t) : Expr t
+  Definition ExprEtaGen eta {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t))
     := fun var => expr_eta_gen eta (@exprf_eta_gen var eta) (e var).
-  Definition ExprEta {t} (e : Expr t) : Expr t
+  Definition ExprEta {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t))
     := fun var => expr_eta (e var).
-  Definition ExprEta' {t} (e : Expr t) : Expr t
+  Definition ExprEta' {t} (e : Expr t) : Expr (Arrow (domain t) (codomain t))
     := fun var => expr_eta' (e var).
 End language.