Don't linearize and eta in MapCastByDeBruijn

4 files changed, 18 insertions, 33 deletions

diff --git a/src/Reflection/MapCastByDeBruijn.v b/src/Reflection/MapCastByDeBruijn.v
index 7998b0a37..68eb06a54 100644
--- a/src/Reflection/MapCastByDeBruijn.v
+++ b/src/Reflection/MapCastByDeBruijn.v
@@ -5,10 +5,12 @@ Require Import Crypto.Reflection.Named.InterpretToPHOAS.
 Require Import Crypto.Reflection.Named.Compile.
 Require Import Crypto.Reflection.Named.PositiveContext.
 Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
-Require Import Crypto.Reflection.Linearize.
-Require Import Crypto.Reflection.Eta.
 Require Import Crypto.Reflection.Syntax.
 
+(** N.B. This procedure only works when there are no nested lets,
+    i.e., nothing like [let x := let y := z in w] in the PHOAS syntax
+    tree.  This is a limitation of [compile]. *)
+
 Section language.
   Context {base_type_code : Type}
           {op : flat_type base_type_code -> flat_type base_type_code -> Type}
@@ -28,14 +30,11 @@ Section language.
     Context {t} (e : Expr base_type_code op t)
             (input_bounds : interp_flat_type interp_base_type_bounds (domain t)).
 
-    Definition MapCastPreProcess
-      := ExprEta (Linearize e).
-    Definition MapCastCompile (e' : Expr base_type_code op (domain t -> codomain t))
-      := compile (e' _) (DefaultNamesFor e').
-    Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive (domain t -> codomain t)))
+    Definition MapCastCompile
+      := compile (e _) (DefaultNamesFor e).
+    Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive t))
       := option_map
            (fun e'' => map_cast
-                         (t:=Arrow (domain t) (codomain t))
                          interp_op_bounds pick_typeb cast_op
                          (BoundsContext:=PContext _)
                          empty
@@ -51,12 +50,12 @@ Section language.
                                  & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }
       := match e' with
          | Some (Some (existT output_bounds e''))
-           => Some (existT _ output_bounds (Eta.ExprEta (InterpToPHOAS (Context:=fun var => PContext var) failb e'')))
+           => Some (existT _ output_bounds (InterpToPHOAS (Context:=fun var => PContext var) failb e''))
          | Some None | None => None
          end.
     Definition MapCast
       : option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t)
                                  & Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }
-      := MapCastDoInterp (MapCastDoCast (MapCastCompile MapCastPreProcess)).
+      := MapCastDoInterp (MapCastDoCast MapCastCompile).
   End MapCast.
 End language.
diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v
index 7fa043791..74622223e 100644
--- a/src/Reflection/MapCastByDeBruijnInterp.v
+++ b/src/Reflection/MapCastByDeBruijnInterp.v
@@ -11,10 +11,6 @@ Require Import Crypto.Reflection.Named.CompileWf.
 Require Import Crypto.Reflection.Named.PositiveContext.
 Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
 Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties.
-Require Import Crypto.Reflection.EtaInterp.
-Require Import Crypto.Reflection.EtaWf.
-Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.LinearizeWf.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapCastByDeBruijn.
 Require Import Crypto.Util.Decidable.
@@ -83,7 +79,7 @@ Section language.
       /\ @inbounds _ b (Interp interp_op e v)
       /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v).
   Proof.
-    unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'.
+    unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'.
     break_innermost_match; try congruence; intros ? v v'.
     inversion_option; inversion_sigma; subst; simpl in *; intros.
     lazymatch goal with
@@ -103,22 +99,17 @@ Section language.
         end
       |
       | change (interp interp_op (?e ?var) ?v') with (Interp interp_op e v');
-        rewrite InterpExprEta;
         unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen;
         rewrite <- interp_interp_to_phoas; [ reflexivity | ] ].
-    { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _);
-        cbv [Eta.ExprEta Linearize.Linearize];
-        [ rewrite interp_expr_eta, interp_linearize | .. ];
-        [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ];
+    { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _);
+        [ reflexivity | auto | .. | eassumption ];
         auto using name_list_unique_DefaultNamesFor. }
-    { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _);
-        cbv [Eta.ExprEta Linearize.Linearize];
-        [ rewrite interp_expr_eta, interp_linearize | .. ];
-        [ reflexivity | eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ];
+    { erewrite (interp_compile (ContextOk:=PositiveContextOk)) with (e':=e _);
+        [ reflexivity | auto | .. | eassumption ];
         auto using name_list_unique_DefaultNamesFor. }
     { intro; eapply wf_map_cast with (t := Arrow _ _) (fValues := empty); eauto using PositiveContextOk with typeclass_instances.
-      { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _);
-          [ eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ];
+      { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':= e _);
+          [ auto | .. | eassumption ];
           auto using name_list_unique_DefaultNamesFor. }
       { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } }
   Qed.
diff --git a/src/Reflection/MapCastByDeBruijnWf.v b/src/Reflection/MapCastByDeBruijnWf.v
index 2cb7e2f40..7130c00ea 100644
--- a/src/Reflection/MapCastByDeBruijnWf.v
+++ b/src/Reflection/MapCastByDeBruijnWf.v
@@ -9,8 +9,6 @@ Require Import Crypto.Reflection.Named.CompileWf.
 Require Import Crypto.Reflection.Named.PositiveContext.
 Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
 Require Import Crypto.Reflection.Named.PositiveContext.DefaultsProperties.
-Require Import Crypto.Reflection.LinearizeWf.
-Require Import Crypto.Reflection.EtaWf.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.MapCastByDeBruijn.
 Require Import Crypto.Util.Decidable.
@@ -76,12 +74,11 @@ Section language.
     : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')),
       Wf e'.
   Proof.
-    unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'.
+    unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, option_map; intros b e'.
     break_innermost_match; try congruence; intros ? v v'.
     inversion_option; inversion_sigma; subst; simpl in *; intros.
     unfold InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen.
     destruct t as [src dst].
-    apply (proj2 (wf_expr_eta (t:=Arrow _ _))).
     eapply (@wf_interp_to_phoas
               base_type_code op FMapPositive.PositiveMap.key _ _ _ _
               (PositiveContext base_type_code _ base_type_code_beq base_type_code_bl_transparent)
@@ -90,9 +87,7 @@ Section language.
               (failb _) (failb _) _ e1);
       (eapply wf_map_cast with (fValues:=empty); eauto using PositiveContextOk with typeclass_instances);
       try (eapply (wf_compile (ContextOk:=PositiveContextOk));
-           [ eapply (proj2 (wf_expr_eta (t:=Arrow _ _)));
-             [ eapply wf_linearize | .. ];
-             eauto
+           [ eauto
            | ..
            | eassumption ]);
       try solve [ auto using name_list_unique_DefaultNamesFor
diff --git a/src/Reflection/Z/BoundsInterpretations.v b/src/Reflection/Z/Bounds/Interpretation.v
index 8e90213b6..8e90213b6 100644
--- a/src/Reflection/Z/BoundsInterpretations.v
+++ b/src/Reflection/Z/Bounds/Interpretation.v