Break up MapCast into separate pieces for easier debugging

1 files changed, 20 insertions, 10 deletions

diff --git a/src/Reflection/MapCastByDeBruijnInterp.v b/src/Reflection/MapCastByDeBruijnInterp.v
index 0e425886b..7fa043791 100644
--- a/src/Reflection/MapCastByDeBruijnInterp.v
+++ b/src/Reflection/MapCastByDeBruijnInterp.v
@@ -11,6 +11,8 @@ 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.
@@ -70,6 +72,7 @@ Section language.
       abstract (intro; erewrite base_type_code_lb in pf by eassumption; congruence). }
   Defined.
 
+  Local Arguments Compile.compile : simpl never.
   Lemma MapCastCorrect
         {t} (e : Expr base_type_code op t)
         (Hwf : Wf e)
@@ -80,7 +83,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, option_map; intros b e'.
+    unfold MapCastByDeBruijn.MapCast, MapCastCompile, MapCastDoCast, MapCastDoInterp, MapCastPreProcess, option_map; intros b e'.
     break_innermost_match; try congruence; intros ? v v'.
     inversion_option; inversion_sigma; subst; simpl in *; intros.
     lazymatch goal with
@@ -93,23 +96,30 @@ Section language.
                 | repeat first [ rewrite !lookupb_empty by (apply PositiveContextOk; assumption)
                                | intro
                                | congruence ] ];
-      unfold Interp, InterpretToPHOAS.Named.InterpToPHOAS, InterpretToPHOAS.Named.InterpToPHOAS_gen;
+      unfold Interp;
       [ match goal with
         | [ H : ?y = Some ?b |- ?x = ?b ]
           => cut (y = Some x); [ congruence | ]
         end
       |
-      | rewrite <- interp_interp_to_phoas; [ reflexivity | ] ].
-    { erewrite (interp_compile (ContextOk:=PositiveContextOk)), interp_linearize;
-        [ reflexivity | apply wf_linearize; auto | .. | eassumption ];
+      | 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 ];
         auto using name_list_unique_DefaultNamesFor. }
-    { erewrite (interp_compile (ContextOk:=PositiveContextOk)), interp_linearize;
-        [ reflexivity | apply wf_linearize; auto | .. | eassumption ];
+    { 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 ];
         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));
-          [ apply wf_linearize; auto | .. | eassumption ].
-        auto using name_list_unique_DefaultNamesFor. }
+      { eapply (wf_compile (ContextOk:=PositiveContextOk)) with (e':=Eta.ExprEta (Linearize.Linearize e) _);
+          [ eapply wf_expr_eta, wf_linearize; auto | .. | eassumption ];
+          auto using name_list_unique_DefaultNamesFor. }
       { intros ???; rewrite lookupb_empty by apply PositiveContextOk; congruence. } }
   Qed.
 End language.