Split out rewrite_with_rule as a separate definition

2 files changed, 45 insertions, 256 deletions

diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index 313dd62e7..e6982a8a2 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -505,44 +505,50 @@ Module Compilers.
         Definition ERROR_BAD_REWRITE_RULE {t} (pat : pattern) (value : expr t) : expr t := value.
         Global Opaque ERROR_BAD_REWRITE_RULE.
 
-        Definition eval_rewrite_rules
-                   (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t))
-                   (maybe_do_again
-                    := fun (should_do_again : bool) (t : base.type)
-                       => if should_do_again return ((@expr.expr base.type ident (if should_do_again then value else var) t) -> UnderLets (expr t))
-                         then do_again t
-                         else UnderLets.Base)
-                   (d : decision_tree)
-                   (rew : rewrite_rulesT)
-                   (e : rawexpr)
-          : UnderLets (expr (type_of_rawexpr e))
-          := let defaulte := expr_of_rawexpr e in
-             (eval_decision_tree
-                (e::nil) d
-                (fun k ctx
-                 => match ctx return option (UnderLets (expr (type_of_rawexpr e))) with
-                   | e'::nil
-                     => (pf <- nth_error rew k;
-                          let 'existT p f := pf in
-                          bind_data_cps
-                            e' p _
-                            (fun v
-                             => v <- v;
-                                 f v _
-                                   (fun fv
-                                    => fv <- fv;
-                                        let 'existT should_do_again fv := fv in
-                                        Some
-                                          (fv <-- fv;
-                                             fv <-- maybe_do_again should_do_again _ fv;
-                                             type.try_transport_cps
-                                               base.try_make_transport_cps _ _ _ fv _
-                                               (fun fv'
-                                                => UnderLets.Base
-                                                     (fv' ;;; (ERROR_BAD_REWRITE_RULE p defaulte))))%under_lets)))%option
-                   | _ => None
-                   end);;;
-                (UnderLets.Base defaulte))%option.
+        Section eval_rewrite_rules.
+          Context (do_again : forall t : base.type, @expr.expr base.type ident value t -> UnderLets (expr t)).
+
+          Let maybe_do_again
+            := fun (should_do_again : bool) (t : base.type)
+               => if should_do_again return ((@expr.expr base.type ident (if should_do_again then value else var) t) -> UnderLets (expr t))
+                  then do_again t
+                  else UnderLets.Base.
+
+          Definition rewrite_with_rule {t} (defaulte : expr t) e' (pf : rewrite_ruleT)
+            := let 'existT p f := pf in
+               bind_data_cps
+                 e' p _
+                 (fun v
+                  => v <- v;
+                       f v _
+                         (fun fv
+                          => fv <- fv;
+                               let 'existT should_do_again fv := fv in
+                               Some
+                                 (fv <-- fv;
+                                    fv <-- maybe_do_again should_do_again _ fv;
+                                    type.try_transport_cps
+                                      base.try_make_transport_cps _ _ _ fv _
+                                      (fun fv'
+                                       => UnderLets.Base
+                                            (fv' ;;; (ERROR_BAD_REWRITE_RULE p defaulte))))%under_lets))%option.
+
+          Definition eval_rewrite_rules
+                     (d : decision_tree)
+                     (rew : rewrite_rulesT)
+                     (e : rawexpr)
+            : UnderLets (expr (type_of_rawexpr e))
+            := let defaulte := expr_of_rawexpr e in
+               (eval_decision_tree
+                  (e::nil) d
+                  (fun k ctx
+                   => match ctx return option (UnderLets (expr (type_of_rawexpr e))) with
+                      | e'::nil
+                        => (pf <- nth_error rew k; rewrite_with_rule defaulte e' pf)%option
+                      | _ => None
+                      end);;;
+                  (UnderLets.Base defaulte))%option.
+        End eval_rewrite_rules.
 
         Local Notation enumerate ls
           := (List.combine (List.seq 0 (List.length ls)) ls).
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index 5d1bae6e4..fbd8e438d 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -388,58 +388,6 @@ Module Compilers.
           Proof using pident_to_typed_invert_bind_args. intros; eapply wf_eval_decision_tree'; eassumption. Qed.
 
 
-          (*
-        Local Notation opt_anyexprP ivar
-          := (fun should_do_again : bool => UnderLets (@AnyExpr.anyexpr base.type ident (if should_do_again then ivar else var)))
-               (only parsing).
-        Local Notation opt_anyexpr ivar
-          := (option (sigT (opt_anyexprP ivar))) (only parsing).
-
-        Definition rewrite_ruleTP
-          := (fun p : pattern => binding_dataT p -> forall T, (opt_anyexpr value -> T) -> T).
-        Definition rewrite_ruleT := sigT rewrite_ruleTP.
-        Definition rewrite_rulesT
-          := (list rewrite_ruleT).
-
-        Definition ERROR_BAD_REWRITE_RULE {t} (pat : pattern) (value : expr t) : expr t. exact value. Qed.
-           *)
-
-          (*
-          Fixpoint natural_type_of_pattern_binding_data {var} (p : pattern) : @binding_dataT var p -> option { t : type & @expr var t }.
-          Proof.
-            refine match p with
-                   | pattern.Wildcard t => _
-                   | pattern.Ident idc => _
-                   | pattern.App f x => _
-                   end.
-            all: cbn.
-            Focus 2.
-            Fixpoint natural_of_ptype_interp {var} (t : ptype) k (K : forall t, k t -> option { t : type & @expr var t }) {struct t}
-              : @ptype_interp var qexists t k -> option { t : type & @expr var t }.
-              refine match t with
-                     | type.base t => _
-                     | type.arrow s d => _
-                     end.
-              all: cbn.
-              Focus 2.
-              Fixpoint natural_of_pbase_type_interp {var} (t : ptype) k (K : forall t, k t -> option { t : type & @expr var t }) {struct t}
-              : @ptype_interp var qexists t k -> option { t : type & @expr var t }.
-              refine match t with
-                     | type.base t => _
-                     | type.arrow s d => _
-                     end.
-              all: cbn.
-              refine
-          Proof.
-            refine match p with
-                   | pattern.Wildcard t => _
-                   | pattern.Ident idc => _
-                   | pattern.App f x => _
-                   end.
-            cbn.
-
-           *)
-
           Local Ltac do_eq_type_of_rawexpr_of_wf :=
             repeat first [ match goal with
                            | [ |- context[rew [fun t => UnderLets ?var (@?P t)] ?pf in UnderLets.Base ?v] ]
@@ -498,7 +446,7 @@ Module Compilers.
                 (rew [fun t => @UnderLets var1 (expr t)] (proj1 (eq_type_of_rawexpr_of_wf Hwf)) in (eval_rewrite_rules1 do_again1 d rew1 re1))
                 (rew [fun t => @UnderLets var2 (expr t)] (proj2 (eq_type_of_rawexpr_of_wf Hwf)) in (eval_rewrite_rules2 do_again2 d rew2 re2)).
           Proof.
-            cbv [eval_rewrite_rules Option.sequence_return].
+            cbv [eval_rewrite_rules Option.sequence_return rewrite_with_rule].
             cbv [rewrite_rules_goodT] in Hrew.
             eapply wf_eval_decision_tree with (ctxe:=[existT _ t (e1, e2)]);
               cbn [length combine];
@@ -585,171 +533,6 @@ Module Compilers.
                               | progress fold (@reify var1) (@reify var2) (@reflect var1) (@reflect var2) ].
           Qed.
 
-          (*
-        Fixpoint with_bindingsT (p : pattern) (T : Type)
-          := match p return Type with
-             | pattern.Wildcard t => ptype_interp qforall t (fun eT => eT -> T)
-             | pattern.Ident idc
-               => match arg_types idc with
-                 | Some t => t -> T
-                 | None => T
-                 end
-             | pattern.App f x => with_bindingsT f (with_bindingsT x T)
-             end.
-
-        Fixpoint lift_pbase_type_interp_cps {K1 K2} {quant} (F : forall t : base.type, K1 t -> K2 t) {t}
-          : pbase_type_interp_cps quant t K1
-            -> pbase_type_interp_cps quant t K2
-          := match t, quant return pbase_type_interp_cps quant t K1
-                                   -> pbase_type_interp_cps quant t K2 with
-             | pattern.base.type.any, qforall
-               => fun f t => F t (f t)
-             | pattern.base.type.any, qexists
-               => fun tf => existT _ _ (F _ (projT2 tf))
-             | pattern.base.type.type_base t, _
-               => F _
-             | pattern.base.type.prod A B, _
-               => @lift_pbase_type_interp_cps
-                   _ _ quant
-                   (fun A'
-                    => @lift_pbase_type_interp_cps
-                        _ _ quant (fun _ => F _) B)
-                   A
-             | pattern.base.type.list A, _
-               => @lift_pbase_type_interp_cps
-                   _ _ quant (fun _ => F _) A
-             end.
-
-        Fixpoint lift_ptype_interp_cps {K1 K2} {quant} (F : forall t : type.type base.type, K1 t -> K2 t) {t}
-          : ptype_interp_cps quant t K1
-            -> ptype_interp_cps quant t K2
-          := match t return ptype_interp_cps quant t K1
-                                   -> ptype_interp_cps quant t K2 with
-             | type.base t
-               => lift_pbase_type_interp_cps F
-             | type.arrow A B
-               => @lift_ptype_interp_cps
-                   _ _ quant
-                   (fun A'
-                    => @lift_ptype_interp_cps
-                        _ _ quant (fun _ => F _) B)
-                   A
-             end.
-
-        Fixpoint lift_with_bindings {p} {A B : Type} (F : A -> B) {struct p} : with_bindingsT p A -> with_bindingsT p B
-          := match p return with_bindingsT p A -> with_bindingsT p B with
-             | pattern.Wildcard t
-               => lift_ptype_interp_cps
-                   (K1:=fun t => value t -> A)
-                   (K2:=fun t => value t -> B)
-                   (fun _ f v => F (f v))
-             | pattern.Ident idc
-               => match arg_types idc as ty
-                       return match ty with
-                              | Some t => t -> A
-                              | None => A
-                              end -> match ty with
-                                    | Some t => t -> B
-                                    | None => B
-                                    end
-                 with
-                 | Some _ => fun f v => F (f v)
-                 | None => F
-                 end
-             | pattern.App f x
-               => @lift_with_bindings
-                   f _ _
-                   (@lift_with_bindings x _ _ F)
-             end.
-
-        Fixpoint app_pbase_type_interp_cps {T : Type} {K1 K2 : base.type -> Type}
-                 (F : forall t, K1 t -> K2 t -> T)
-                 {t}
-          : pbase_type_interp_cps qforall t K1
-            -> pbase_type_interp_cps qexists t K2 -> T
-          := match t return pbase_type_interp_cps qforall t K1
-                            -> pbase_type_interp_cps qexists t K2 -> T with
-             | pattern.base.type.any
-               => fun f tv => F _ (f _) (projT2 tv)
-             | pattern.base.type.type_base t
-               => fun f v => F _ f v
-             | pattern.base.type.prod A B
-               => @app_pbase_type_interp_cps
-                   _
-                   (fun A' => pbase_type_interp_cps qforall B (fun B' => K1 (A' * B')%etype))
-                   (fun A' => pbase_type_interp_cps qexists B (fun B' => K2 (A' * B')%etype))
-                   (fun A'
-                    => @app_pbase_type_interp_cps
-                        _
-                        (fun B' => K1 (A' * B')%etype)
-                        (fun B' => K2 (A' * B')%etype)
-                        (fun _ => F _)
-                        B)
-                   A
-             | pattern.base.type.list A
-               => @app_pbase_type_interp_cps T (fun A' => K1 (base.type.list A')) (fun A' => K2 (base.type.list A')) (fun _ => F _) A
-             end.
-
-        Fixpoint app_ptype_interp_cps {T : Type} {K1 K2 : type -> Type}
-                 (F : forall t, K1 t -> K2 t -> T)
-                 {t}
-          : ptype_interp_cps qforall t K1
-            -> ptype_interp_cps qexists t K2 -> T
-          := match t return ptype_interp_cps qforall t K1
-                            -> ptype_interp_cps qexists t K2 -> T with
-             | type.base t => app_pbase_type_interp_cps F
-             | type.arrow A B
-               => @app_ptype_interp_cps
-                   _
-                   (fun A' => ptype_interp_cps qforall B (fun B' => K1 (A' -> B')%etype))
-                   (fun A' => ptype_interp_cps qexists B (fun B' => K2 (A' -> B')%etype))
-                   (fun A'
-                    => @app_ptype_interp_cps
-                        _
-                        (fun B' => K1 (A' -> B')%etype)
-                        (fun B' => K2 (A' -> B')%etype)
-                        (fun _ => F _)
-                        B)
-                   A
-             end.
-
-        Fixpoint app_binding_data {T p} : forall (f : with_bindingsT p T) (v : binding_dataT p), T
-          := match p return forall (f : with_bindingsT p T) (v : binding_dataT p), T with
-             | pattern.Wildcard t
-               => app_ptype_interp_cps
-                   (K1:=fun t => value t -> T)
-                   (K2:=fun t => value t)
-                   (fun _ f v => f v)
-             | pattern.Ident idc
-               => match arg_types idc as ty
-                       return match ty with
-                              | Some t => t -> T
-                              | None => T
-                              end -> match ty return Type with
-                                    | Some t => t
-                                    | None => unit
-                                    end -> T
-                 with
-                 | Some t => fun f x => f x
-                 | None => fun v 'tt => v
-                 end
-             | pattern.App f x
-               => fun F '(vf, vx)
-                 => @app_binding_data _ x (@app_binding_data _ f F vf) vx
-             end.
-
-        (** XXX MOVEME? *)
-        Definition mkcast {P : type -> Type} {t1 t2 : type} : ~> (option (P t1 -> P t2))
-          := fun T k => type.try_make_transport_cps base.try_make_transport_cps P t1 t2 _ k.
-        Definition cast {P : type -> Type} {t1 t2 : type} (v : P t1) : ~> (option (P t2))
-          := fun T k => type.try_transport_cps base.try_make_transport_cps P t1 t2 v _ k.
-        Definition castb {P : base.type -> Type} {t1 t2 : base.type} (v : P t1) : ~> (option (P t2))
-          := fun T k => base.try_transport_cps P t1 t2 v _ k.
-        Definition castbe {t1 t2 : base.type} (v : expr t1) : ~> (option (expr t2))
-          := @castb expr t1 t2 v.
-        Definition castv {t1 t2} (v : value t1) : ~> (option (value t2))
-          := fun T k => type.try_transport_cps base.try_make_transport_cps value t1 t2 v _ k.
-           *)
           Section with_do_again.
             Context (dtree : @decision_tree pident)
                     (rew1 : rewrite_rulesT1)