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.

4 files changed, 19 insertions, 27 deletions

diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v
index 7ffc5fded..55f4aba70 100644
--- a/src/Reflection/Named/Compile.v
+++ b/src/Reflection/Named/Compile.v
@@ -38,14 +38,13 @@ Section language.
                            end
        end.
 
-  Fixpoint ocompile {t} (e : expr t) (ls : list (option Name)) {struct e}
+  Definition ocompile {t} (e : expr t) (ls : list (option Name))
     : option (nexpr t)
     := match e in @Syntax.expr _ _ _ t return option (nexpr t) with
-       | Return _ x => option_map Named.Return (ocompilef x ls)
-       | Abs _ _ f
-         => match ls with
-            | cons (Some n) ls'
-              => option_map (Named.Abs n) (@ocompile _ (f n) ls')
+       | Abs src _ f
+         => match split_onames src ls with
+            | (Some n, ls')%core
+              => option_map (Named.Abs n) (@ocompilef _ (f n) ls')
             | _ => None
             end
        end.
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index bd9a46b9a..7509d5f7a 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -68,15 +68,14 @@ Section language.
     Fixpoint compute_livenessf ctx {t} e prefix
       := @compute_livenessf_step (@compute_livenessf) ctx t e prefix.
 
-    Fixpoint compute_liveness (ctx : Context)
+    Definition compute_liveness (ctx : Context)
              {t} (e : expr Name t) (prefix : list liveness)
       : list liveness
       := match e with
-         | Return _ x => compute_livenessf ctx x prefix
          | Abs src _ n f
-           => let prefix := prefix ++ repeat live (count_pairs (Tbase src)) in
-              let ctx := extend (t:=Tbase src) ctx n (SmartValf _ (fun _ => prefix) (Tbase src)) in
-              @compute_liveness ctx _ f prefix
+           => let prefix := prefix ++ repeat live (count_pairs src) in
+              let ctx := extend (t:=src) ctx n (SmartValf _ (fun _ => prefix) src) in
+              compute_livenessf ctx f prefix
          end.
 
     Section insert_dead.
diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Reflection/Named/RegisterAssign.v
index ce8188ee5..70ee5a203 100644
--- a/src/Reflection/Named/RegisterAssign.v
+++ b/src/Reflection/Named/RegisterAssign.v
@@ -67,18 +67,17 @@ Section language.
     Fixpoint register_reassignf ctxi ctxr {t} e new_names
       := @register_reassignf_step (@register_reassignf) ctxi ctxr t e new_names.
 
-    Fixpoint register_reassign (ctxi : InContext) (ctxr : ReverseContext)
+    Definition register_reassign (ctxi : InContext) (ctxr : ReverseContext)
              {t} (e : expr InName t) (new_names : list (option OutName))
       : option (expr OutName t)
       := match e in Named.expr _ _ _ t return option (expr _ t) with
-         | Return _ x => option_map Return (register_reassignf ctxi ctxr x new_names)
          | Abs src _ n f
-           => let '(n', new_names') := eta (split_onames (Tbase src) new_names) in
+           => let '(n', new_names') := eta (split_onames src new_names) in
               match n' with
               | Some n'
-                => let ctxi := extendb (t:=src) ctxi n n' in
-                   let ctxr := extendb (t:=src) ctxr n' n in
-                   option_map (Abs n') (@register_reassign ctxi ctxr _ f new_names')
+                => let ctxi := extend (t:=src) ctxi n n' in
+                   let ctxr := extend (t:=src) ctxr n' n in
+                   option_map (Abs n') (register_reassignf ctxi ctxr f new_names')
               | None => None
               end
          end.
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index 2c1f3bd23..996d707a3 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -47,10 +47,8 @@ Module Export Named.
         | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2).
         Bind Scope nexpr_scope with exprf.
         Inductive expr : type -> Type :=
-        | Return {t} : exprf t -> expr t
-        | Abs {src dst} : Name -> expr dst -> expr (Arrow src dst).
+        | Abs {src dst} : interp_flat_type_gen (fun _ => Name) src -> exprf dst -> expr (Arrow src dst).
         Bind Scope nexpr_scope with expr.
-        Global Coercion Return : exprf >-> expr.
         (** [SmartVar] is like [Var], except that it inserts
           pair-projections and [Pair] as necessary to handle
           [flat_type], and not just [base_type_code] *)
@@ -110,10 +108,9 @@ Module Export Named.
                | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey
                end%option_pointed_prop.
 
-          Fixpoint wf (ctx : Context) {t} (e : expr t) : Prop
+          Definition wf (ctx : Context) {t} (e : expr t) : Prop
             := match e with
-               | Return _ x => prop_of_option (wff ctx x)
-               | Abs src _ n f => forall v, @wf (extend ctx (t:=Tbase src) n v) _ f
+               | Abs src _ n f => forall v, prop_of_option (@wff (extend ctx (t:=src) n v) _ f)
                end.
         End wf.
 
@@ -166,11 +163,10 @@ Module Export Named.
                tt (fun _ x => x) interp_op (fun _ y _ f => let x := y in f x)
                (fun _ x _ y => (x, y)%core).
 
-        Fixpoint interp (ctx : Context) {t} (e : expr t)
+        Definition interp (ctx : Context) {t} (e : expr t)
           : wf ctx e -> interp_type t
           := match e in expr t return wf ctx e -> interp_type t with
-             | Return _ x => interpf ctx x
-             | Abs _ _ n f => fun good v => @interp _ _ f (good v)
+             | Abs _ _ n f => fun good v => @interpf _ _ f (good v)
              end.
       End with_val_context.
     End expr_param.
@@ -183,7 +179,6 @@ Global Arguments SmartVar {_ _ _ _} _.
 Global Arguments Op {_ _ _ _ _} _ _.
 Global Arguments LetIn {_ _ _} _ _ _ {_} _.
 Global Arguments Pair {_ _ _ _} _ {_} _.
-Global Arguments Return {_ _ _ _} _.
 Global Arguments Abs {_ _ _ _ _} _ _.
 Global Arguments extend {_ _ _ _} ctx {_} _ _.
 Global Arguments remove {_ _ _ _} ctx {_} _.