Minor changes to rewriter

These changes make it easier to prove things about the interpretation of
the rewriter.

3 files changed, 103 insertions, 88 deletions

diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 26a833aac..0713ea83a 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -581,19 +581,25 @@ Module Compilers.
              | type.arrow _ _ => fun _ => k None
              end.
 
-        Definition reveal_rawexpr_cps (e : rawexpr) : ~> rawexpr
+        (* Allows assuming that we know the ident that we're revealing; mainly used in proofs *)
+        Definition reveal_rawexpr_cps_gen (assume_known : option bool)
+                   (e : rawexpr) : ~> rawexpr
           := fun T k
-             => match e with
-                | rExpr _ e as r
-                | rValue (type.base _) e as r
+             => match e, assume_known with
+                | rExpr _ e as r, _
+                | rValue (type.base _) e as r, _
                   => match e with
-                     | expr.Ident t idc => k (rIdent false idc e)
+                     | expr.Ident t idc => k (rIdent (match assume_known with Some known => known | _ => false end) idc e)
                      | expr.App s d f x => k (rApp (rExpr f) (rExpr x) e)
                      | _ => k r
                      end
-                | e' => k e'
+                | rIdent _ t idc t' alt, Some known => k (rIdent known idc alt)
+                | e', _ => k e'
                 end.
 
+        Definition reveal_rawexpr_cps (e : rawexpr) : ~> rawexpr
+          := reveal_rawexpr_cps_gen None e.
+
         Fixpoint with_unification_resultT' {t} (p : pattern t) (evm : EvarMap) (K : Type) : Type
           := match p return Type with
              | pattern.Wildcard t => value (pattern.type.subst_default t evm) -> K
@@ -2132,6 +2138,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
                        (*Compile.reflect*)
                        (*Compile.reify*)
                        Compile.reveal_rawexpr_cps
+                       Compile.reveal_rawexpr_cps_gen
                        Compile.rew_should_do_again
                        Compile.rew_with_opt
                        Compile.rew_under_lets
@@ -2228,6 +2235,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
                        (*Compile.reflect*)
                        (*Compile.reify*)
                        Compile.reveal_rawexpr_cps
+                       Compile.reveal_rawexpr_cps_gen
                        Compile.rew_should_do_again
                        Compile.rew_with_opt
                        Compile.rew_under_lets
@@ -2325,6 +2333,7 @@ Z.mul @@ (?x >> 128, ?y >> 128)             --> mulhh @@ (x, y)
                        (*Compile.reflect*)
                        (*Compile.reify*)
                        Compile.reveal_rawexpr_cps
+                       Compile.reveal_rawexpr_cps_gen
                        Compile.rew_should_do_again
                        Compile.rew_with_opt
                        Compile.rew_under_lets
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 4f2017cbf..2537523a4 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -241,7 +241,8 @@ Module Compilers.
         Local Notation reflect := (@reflect ident).
         Local Notation reify_expr := (@reify_expr ident).
         Local Notation rawexpr := (@rawexpr ident).
-        Local Notation eval_decision_tree var := (@eval_decision_tree ident var pident full_types invert_bind_args type_of_raw_pident raw_pident_to_typed).
+        Local Notation eval_decision_tree var := (@eval_decision_tree ident var raw_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
+        Local Notation reveal_rawexpr_gen assume_known e := (@reveal_rawexpr_cps_gen ident _ assume_known e _ id).
         Local Notation reveal_rawexpr e := (@reveal_rawexpr_cps ident _ e _ id).
         Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown).
         Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown type_vars_of_pident).
@@ -615,6 +616,91 @@ Module Compilers.
                            | rewrite Hv; (solve [ auto ] + break_innermost_match_step) ].
             Qed.
           End normalize_deep_rewrite_rule_cps_id.
+
+          Lemma reveal_rawexpr_cps_gen_id assume_known e T k
+            : @reveal_rawexpr_cps_gen ident var assume_known e T k = k (reveal_rawexpr_gen assume_known e).
+          Proof.
+            cbv [reveal_rawexpr_cps_gen]; break_innermost_match; try reflexivity.
+            all: cbv [value value'] in *; expr.invert_match; try reflexivity.
+          Qed.
+
+          Lemma reveal_rawexpr_cps_id e T k
+            : @reveal_rawexpr_cps ident var e T k = k (reveal_rawexpr e).
+          Proof. apply reveal_rawexpr_cps_gen_id. Qed.
+
+          Fixpoint eval_decision_tree_cont_None_ext
+                   {T ctx d cont}
+                   (Hcont : forall x y, cont x y = None)
+                   {struct d}
+            : @eval_decision_tree var T ctx d cont = None.
+          Proof using Type.
+            clear -Hcont eval_decision_tree_cont_None_ext.
+            specialize (fun d ctx => @eval_decision_tree_cont_None_ext T ctx d).
+            destruct d; cbn [eval_decision_tree]; intros; try (clear eval_decision_tree_cont_None_ext; tauto).
+            { let d := match goal with d : decision_tree |- _ => d end in
+              specialize (eval_decision_tree_cont_None_ext d).
+              rewrite !Hcont, !eval_decision_tree_cont_None_ext by assumption.
+              break_innermost_match; reflexivity. }
+            { let d := match goal with d : decision_tree |- _ => d end in
+              pose proof (eval_decision_tree_cont_None_ext d) as IHd.
+              let d := match goal with d : option decision_tree |- _ => d end in
+              pose proof (match d as d' return match d' with Some _ => _ | None => True end with
+                          | Some d => eval_decision_tree_cont_None_ext d
+                          | None => I
+                          end) as IHapp_case.
+              all: destruct ctx; try (clear eval_decision_tree_cont_None_ext; (tauto || congruence)); [].
+              all: lazymatch goal with
+                   | [ |- match ?d with
+                          | TryLeaf _ _ => (?res ;; ?ev)%option
+                          | _ => _
+                          end = None ]
+                     => cut (res = None /\ ev = None);
+                          [ clear eval_decision_tree_cont_None_ext;
+                            let H1 := fresh in
+                            let H2 := fresh in
+                            intros [H1 H2]; rewrite H1, H2; destruct d; reflexivity
+                          | ]
+                   end.
+              all: split; [ | clear eval_decision_tree_cont_None_ext; eapply IHd; eassumption ].
+              (** We use the trick that [induction] inside [Fixpoint]
+                  gives us nested [fix]es that pass the guarded
+                  checker, as long as we're careful about how we do
+                  things *)
+              let icases := match goal with d : list (_ * decision_tree) |- _ => d end in
+              induction icases as [|icase icases IHicases];
+                [ | pose proof (eval_decision_tree_cont_None_ext (snd icase)) as IHicase ];
+                clear eval_decision_tree_cont_None_ext.
+              (** now we can stop being super-careful about [destruct]
+                  ordering because, if we're [Guarded] here (which we
+                  are), then we cannot break guardedness from this
+                  point on, because we've cleared the bare fixpoint
+                  after specializing it to valid arguments *)
+              2: revert IHicases.
+              rewrite reveal_rawexpr_cps_id.
+              all: repeat (rewrite reveal_rawexpr_cps_id; set (reveal_rawexpr_cps _ _ id)).
+              all: repeat match goal with H := reveal_rawexpr _ |- _ => subst H end.
+              all: repeat first [ progress cbn [fold_right Option.sequence Option.sequence_return fst snd] in *
+                                | progress subst
+                                | reflexivity
+                                | rewrite IHd
+                                | rewrite IHapp_case
+                                | rewrite IHicase
+                                | break_innermost_match_step
+                                | progress intros
+                                | solve [ auto ]
+                                | progress break_match
+                                | progress cbv [Option.bind option_bind'] in * ]. }
+            { let d := match goal with d : decision_tree |- _ => d end in
+              specialize (eval_decision_tree_cont_None_ext d); rename eval_decision_tree_cont_None_ext into IHd.
+              repeat first [ break_innermost_match_step
+                           | rewrite IHd
+                           | solve [ auto ]
+                           | progress intros ]. }
+          Qed.
+
+          Lemma eval_decision_tree_cont_None {T ctx d}
+            : @eval_decision_tree var T ctx d (fun _ _ => None) = None.
+          Proof using Type. apply eval_decision_tree_cont_None_ext; reflexivity. Qed.
         End with_var1.
 
         Section with_var2.
@@ -798,18 +884,11 @@ Module Compilers.
               destruct (eq_type_of_rawexpr_of_wf Hwf); generalize dependent (type_of_rawexpr re1); generalize dependent (type_of_rawexpr re2); intros; subst; clear; eliminate_hprop_eq; reflexivity.
           Qed.
 
-          Lemma reveal_rawexpr_cps_id {var} e T k
-            : @reveal_rawexpr_cps ident var e T k = k (reveal_rawexpr e).
-          Proof.
-            cbv [reveal_rawexpr_cps]; break_innermost_match; try reflexivity.
-            cbv [value value'] in *; expr.invert_match; try reflexivity.
-          Qed.
-
           Lemma wf_reveal_rawexpr t G re1 e1 re2 e2 (Hwf : @wf_rawexpr G t re1 e1 re2 e2)
             : @wf_rawexpr G t (reveal_rawexpr re1) e1 (reveal_rawexpr re2) e2.
           Proof.
             pose proof (wf_expr_of_wf_rawexpr Hwf).
-            destruct Hwf; cbv [reveal_rawexpr_cps id];
+            destruct Hwf; cbv [reveal_rawexpr_cps reveal_rawexpr_cps_gen id];
               repeat first [ assumption
                            | constructor
                            | progress subst
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index de17f2896..feb5b98f9 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -378,79 +378,6 @@ Module Compilers.
                    end;
             fin_handle_list.
 
-          Fixpoint eval_decision_tree_cont_None_ext
-                {var} {T ctx d cont}
-                (Hcont : forall x y, cont x y = None)
-                {struct d}
-            : @eval_decision_tree var T ctx d cont = None.
-          Proof using Type.
-            clear -Hcont eval_decision_tree_cont_None_ext.
-            specialize (fun d ctx => @eval_decision_tree_cont_None_ext var T ctx d).
-            destruct d; cbn [eval_decision_tree]; intros; try (clear eval_decision_tree_cont_None_ext; tauto).
-            { let d := match goal with d : decision_tree |- _ => d end in
-              specialize (eval_decision_tree_cont_None_ext d).
-              rewrite !Hcont, !eval_decision_tree_cont_None_ext by assumption.
-              break_innermost_match; reflexivity. }
-            { let d := match goal with d : decision_tree |- _ => d end in
-              pose proof (eval_decision_tree_cont_None_ext d) as IHd.
-              let d := match goal with d : option decision_tree |- _ => d end in
-              pose proof (match d as d' return match d' with Some _ => _ | None => True end with
-                          | Some d => eval_decision_tree_cont_None_ext d
-                          | None => I
-                          end) as IHapp_case.
-              all: destruct ctx; try (clear eval_decision_tree_cont_None_ext; (tauto || congruence)); [].
-              all: lazymatch goal with
-                   | [ |- match ?d with
-                          | TryLeaf _ _ => (?res ;; ?ev)%option
-                          | _ => _
-                          end = None ]
-                     => cut (res = None /\ ev = None);
-                          [ clear eval_decision_tree_cont_None_ext;
-                            let H1 := fresh in
-                            let H2 := fresh in
-                            intros [H1 H2]; rewrite H1, H2; destruct d; reflexivity
-                          | ]
-                   end.
-              all: split; [ | clear eval_decision_tree_cont_None_ext; eapply IHd; eassumption ].
-              (** We use the trick that [induction] inside [Fixpoint]
-                  gives us nested [fix]es that pass the guarded
-                  checker, as long as we're careful about how we do
-                  things *)
-              let icases := match goal with d : list (_ * decision_tree) |- _ => d end in
-              induction icases as [|icase icases IHicases];
-                [ | pose proof (eval_decision_tree_cont_None_ext (snd icase)) as IHicase ];
-                clear eval_decision_tree_cont_None_ext.
-              (** now we can stop being super-careful about [destruct]
-                  ordering because, if we're [Guarded] here (which we
-                  are), then we cannot break guardedness from this
-                  point on, because we've cleared the bare fixpoint
-                  after specializing it to valid arguments *)
-              2: revert IHicases.
-              all: repeat (rewrite reveal_rawexpr_cps_id; set (reveal_rawexpr _)).
-              all: repeat match goal with H := reveal_rawexpr _ |- _ => subst H end.
-              all: repeat first [ progress cbn [fold_right Option.sequence Option.sequence_return fst snd] in *
-                                | progress subst
-                                | reflexivity
-                                | rewrite IHd
-                                | rewrite IHapp_case
-                                | rewrite IHicase
-                                | break_innermost_match_step
-                                | progress intros
-                                | solve [ auto ]
-                                | progress break_match
-                                | progress cbv [Option.bind option_bind'] in * ]. }
-            { let d := match goal with d : decision_tree |- _ => d end in
-              specialize (eval_decision_tree_cont_None_ext d); rename eval_decision_tree_cont_None_ext into IHd.
-              repeat first [ break_innermost_match_step
-                           | rewrite IHd
-                           | solve [ auto ]
-                           | progress intros ]. }
-          Qed.
-
-          Lemma eval_decision_tree_cont_None {var} {T ctx d}
-            : @eval_decision_tree var T ctx d (fun _ _ => None) = None.
-          Proof using Type. apply eval_decision_tree_cont_None_ext; reflexivity. Qed.
-
           Fixpoint wf_eval_decision_tree' {T1 T2} G d (P : option T1 -> option T2 -> Prop) (HPNone : P None None) {struct d}
             : forall (ctx1 : list (@rawexpr var1))
                      (ctx2 : list (@rawexpr var2))