Generalize expr.interp_related

This is needed to handle exprs whose var types are value

5 files changed, 85 insertions, 57 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index c129675c9..eba5cf85a 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -458,31 +458,38 @@ Module Compilers.
               {interp_base_type : base_type -> Type}
               (interp_ident : forall t, ident t -> type.interp interp_base_type t).
 
-      Fixpoint interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop
+      Fixpoint interp_related_gen
+               {var : type base_type -> Type}
+               (R : forall t, var t -> type.interp interp_base_type t -> Prop)
+               {t} (e : @expr base_type ident var t)
+        : type.interp interp_base_type t -> Prop
         := match e in expr t return type.interp interp_base_type t -> Prop with
-           | expr.Var t v1 => fun v2 => v1 == v2
+           | expr.Var t v1 => R t v1
            | expr.App s d f x
              => fun v2
                 => exists fv xv,
-                    @interp_related _ f fv
-                    /\ @interp_related _ x xv
+                    @interp_related_gen var R _ f fv
+                    /\ @interp_related_gen var R _ x xv
                     /\ fv xv = v2
            | expr.Ident t idc
              => fun v2 => interp_ident _ idc == v2
            | expr.Abs s d f1
              => fun f2
                 => forall x1 x2,
-                    x1 == x2
-                    -> @interp_related d (f1 x1) (f2 x2)
+                    R _ x1 x2
+                    -> @interp_related_gen var R d (f1 x1) (f2 x2)
            | expr.LetIn s d x f (* combine the App rule with the Abs rule *)
              => fun v2
                 => exists fv xv,
-                    @interp_related _ x xv
+                    @interp_related_gen var R _ x xv
                     /\ (forall x1 x2,
-                           x1 == x2
-                           -> @interp_related d (f x1) (fv x2))
+                           R _ x1 x2
+                           -> @interp_related_gen var R d (f x1) (fv x2))
                     /\ fv xv = v2
            end.
+
+      Definition interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop
+        := @interp_related_gen (type.interp interp_base_type) (@type.eqv) t e.
     End with_interp.
 
     Definition Expr {base_type ident} t := forall var, @expr base_type ident var t.
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index f5cc89b4f..bc9ad60be 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -603,14 +603,14 @@ Module Compilers.
       Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}.
       Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
 
-      Lemma reify_list_interp_related_iff {t ls v}
-        : expr.interp_related (@ident_interp) (reify_list (t:=t) ls) v
-          <-> List.Forall2 (expr.interp_related (@ident_interp)) ls v.
+      Lemma reify_list_interp_related_gen_iff {var R t ls v}
+        : expr.interp_related_gen (var:=var) (@ident_interp) R (reify_list (t:=t) ls) v
+          <-> List.Forall2 (expr.interp_related_gen (@ident_interp) R) ls v.
       Proof using Type.
         revert v; induction ls as [|l ls IHls], v as [|v vs].
         all: repeat first [ rewrite expr.reify_list_nil
                           | rewrite expr.reify_list_cons
-                          | progress cbn [expr.interp_related ident.gen_interp type.related] in *
+                          | progress cbn [expr.interp_related_gen ident.gen_interp type.related] in *
                           | progress cbv [Morphisms.respectful] in *
                           | progress destruct_head'_ex
                           | progress destruct_head'_and
@@ -634,14 +634,25 @@ Module Compilers.
                             end ].
       Qed.
 
-      Lemma reflect_list_interp_related_iff {t ls ls' v}
+      Lemma reify_list_interp_related_iff {t ls v}
+        : expr.interp_related (@ident_interp) (reify_list (t:=t) ls) v
+          <-> List.Forall2 (expr.interp_related (@ident_interp)) ls v.
+      Proof using Type. apply reify_list_interp_related_gen_iff. Qed.
+
+      Lemma reflect_list_interp_related_gen_iff {var R t ls ls' v}
             (Hls : invert_expr.reflect_list (t:=t) ls = Some ls')
-        : List.Forall2 (expr.interp_related (@ident_interp)) ls' v
-          <-> expr.interp_related (@ident_interp) ls v.
+        : List.Forall2 (expr.interp_related_gen (var:=var) (@ident_interp) R) ls' v
+          <-> expr.interp_related_gen (@ident_interp) R ls v.
       Proof using Type.
         apply reflect_list_Some in Hls; subst.
-        rewrite reify_list_interp_related_iff; reflexivity.
+        rewrite reify_list_interp_related_gen_iff; reflexivity.
       Qed.
+
+      Lemma reflect_list_interp_related_iff {t ls ls' v}
+            (Hls : invert_expr.reflect_list (t:=t) ls = Some ls')
+        : List.Forall2 (expr.interp_related (@ident_interp)) ls' v
+          <-> expr.interp_related (@ident_interp) ls v.
+      Proof using Type. now apply reflect_list_interp_related_gen_iff. Qed.
     End with_interp.
 
     Ltac invert_subst_step_helper guard_tac :=
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index a459df399..3919287d4 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -586,7 +586,7 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
           : expr.interp_related interp_ident e v
             -> @type.eqv t (expr.interp interp_ident e) v.
         Proof using Type.
-          induction e; cbn [expr.interp_related expr.interp type.related]; cbv [respectful LetIn.Let_In].
+          cbv [expr.interp_related]; induction e; cbn [expr.interp_related_gen expr.interp type.related]; cbv [respectful LetIn.Let_In].
           all: repeat first [ progress intros
                             | assumption
                             | solve [ eauto ]
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index 962161102..872cc2be0 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -150,10 +150,11 @@ Module Compilers.
              let v'' := fresh in
              cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in
         match goal with
+        | _ => progress cbv [expr.interp_related] in *
         | _ => progress cbn [Compile.reify_expr]
         | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
         | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
-        | [ |- expr.interp_related ?ident_interp ?f ?v ]
+        | [ |- expr.interp_related_gen ?ident_interp ?R ?f ?v ]
           => do_replace v
         | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1),
               _ /\ _ /\ fv ev = ?x ]
@@ -162,18 +163,18 @@ Module Compilers.
              first [ do_replace x
                    | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ]
         | _ => progress intros
-        | [ |- expr.interp_related _ _ ?ev ] => is_evar ev; eassumption
-        | [ |- expr.interp_related _ (?f @ ?x) ?ev ]
+        | [ |- expr.interp_related_gen _ _ _ ?ev ] => is_evar ev; eassumption
+        | [ |- expr.interp_related_gen _ _ (?f @ ?x) ?ev ]
           => is_evar ev;
              let fh := fresh in
              let xh := fresh in
-             set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh;
+             set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh;
              do 2 eexists; repeat apply conj; [ | | reflexivity ]
-        | [ |- expr.interp_related _ (expr.Abs ?f) _ ]
-          => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh
-        | [ |- expr.interp_related _ (expr.Ident ?idc) ?ev ]
+        | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ]
+          => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh
+        | [ |- expr.interp_related_gen _ _ (expr.Ident ?idc) ?ev ]
           => is_evar ev;
-             cbn [expr.interp_related]; apply ident.gen_interp_Proper; reflexivity
+             cbn [expr.interp_related_gen]; apply ident.gen_interp_Proper; reflexivity
         | [ |- _ = _ :> ?T ]
           => lazymatch T with
              | BinInt.Z => idtac
@@ -192,13 +193,13 @@ Module Compilers.
                 | [ |- True ] => exact I
                 | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence
                 | [ |- ?G ] => has_evar G; reflexivity
-                | [ |- context[expr.interp_related _ _ _] ] => reflexivity
+                | [ |- context[expr.interp_related_gen _ _ _ _] ] => reflexivity
                 | [ |- context[_ == _] ] => reflexivity
                 (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
                 | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*)
                 end
               | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in *
-              | progress cbv [Compile.option_bind' respectful] in *
+              | progress cbv [Compile.option_bind' respectful expr.interp_related] in *
               | progress fold (@type.interp _ base.interp)
               | progress fold (@base.interp)
               | match goal with
@@ -228,10 +229,10 @@ Module Compilers.
                   => rewrite (@eq_map_list_rect A B f ls)
                 | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ]
                   =>  rewrite (@eq_fold_right_list_rect A B f v ls)
-                | [ |- context[expr.interp_related _ (reify_list _)] ]
-                  => rewrite expr.reify_list_interp_related_iff
-                | [ H : context[expr.interp_related _ (reify_list _)] |- _ ]
-                  => rewrite expr.reify_list_interp_related_iff in H
+                | [ |- context[expr.interp_related_gen _ _ (reify_list _)] ]
+                  => rewrite expr.reify_list_interp_related_gen_iff
+                | [ H : context[expr.interp_related_gen _ _ (reify_list _)] |- _ ]
+                  => rewrite expr.reify_list_interp_related_gen_iff in H
                 | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff
                 | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff
                 | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff
@@ -281,27 +282,27 @@ Module Compilers.
                        => let f := match (eval pattern (v1 yv) in f) with ?f _ => f end in
                           eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ (e xv) (v1 yv) f); [ | eapply H; assumption ]
                      end
-                | [ |- expr.interp_related
-                         _
+                | [ |- expr.interp_related_gen
+                         _ _
                          (#(ident.prod_rect) @ ?f @ ?e)%expr
                          match ?e' with pair a b => @?f' a b end ]
                   => let fh := fresh in
                      let eh := fresh in
-                     set (fh := f); set (eh := e); cbn [expr.interp_related]; subst fh eh;
+                     set (fh := f); set (eh := e); cbn [expr.interp_related_gen]; subst fh eh;
                      exists (fun ev => match ev with pair a b => f' a b end), e';
                      repeat apply conj;
                      [ | assumption | reflexivity ];
                      exists (fun fv ev => match ev with pair a b => fv a b end), f';
                      repeat apply conj;
                      [ cbn [type.interp type.related ident_interp]; cbv [respectful]; intros; subst; eta_expand; auto | | reflexivity ]
-                | [ |- expr.interp_related
-                         _
+                | [ |- expr.interp_related_gen
+                         _ _
                          (#(ident.bool_rect) @ ?t @ ?f @ ?b)%expr
                          (bool_rect ?P ?t' ?f' ?b') ]
                   => let th := fresh in
                      let fh := fresh in
                      let bh := fresh in
-                     set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related]; subst th fh bh;
+                     set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related_gen]; subst th fh bh;
                      unshelve
                        ((exists (bool_rect P t' f'), b'); repeat apply conj;
                         [ | shelve | reflexivity ];
@@ -309,7 +310,7 @@ Module Compilers.
                         [ | shelve | reflexivity ];
                         (exists (fun tv fv => bool_rect P (tv tt) (fv tt)), (fun _ => t')); repeat apply conj;
                         [ | shelve | reflexivity ])
-                | [ |- @expr.interp_related _ _ _ _ (type.base ?t) _ _ ]
+                | [ |- @expr.interp_related_gen _ _ _ _ _ _ (type.base ?t) _ _ ]
                   => lazymatch t with
                      | base.type.type_base base.type.Z => idtac
                      | base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z) => idtac
@@ -320,12 +321,12 @@ Module Compilers.
                   => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end;
                      lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end;
                      progress repeat recurse_interp_related_step
-                | [ |- expr.interp_related _ (expr.Abs ?f) _ ]
-                  => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh
-                | [ H : expr.interp_related _ ?x ?x' |- expr.interp_related _ (?f @ ?x) (?f' ?x') ]
+                | [ |- expr.interp_related_gen _ _ (expr.Abs ?f) _ ]
+                  => let fh := fresh in set (fh := f); cbn [expr.interp_related_gen]; subst fh
+                | [ H : expr.interp_related_gen _ _ ?x ?x' |- expr.interp_related_gen _ _ (?f @ ?x) (?f' ?x') ]
                   => let fh := fresh in
                      let xh := fresh in
-                     set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh;
+                     set (fh := f); set (xh := x); cbn [expr.interp_related_gen]; subst fh xh;
                      exists f', x'; repeat apply conj;
                      [ | exact H | reflexivity ]
                 | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] => apply Forall2_update_nth
@@ -451,7 +452,7 @@ Module Compilers.
               | break_innermost_match_step
               | break_innermost_match_hyps_step
               | progress destruct_head'_or
-              | progress cbn [expr.interp_related] in *
+              | progress cbn [expr.interp_related_gen] in *
               | match goal with
                 | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
                     |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
@@ -465,7 +466,7 @@ Module Compilers.
                 end
               | progress cbv [Option.bind] in *
               | match goal with
-                | [ H : expr.interp_related _ ?e ?v |- _ ] => is_var e; clear H e
+                | [ H : expr.interp_related_gen _ _ ?e ?v |- _ ] => is_var e; clear H e
                 end ].
 
       Local Ltac interp_good_t_step_arith :=
@@ -541,6 +542,7 @@ Module Compilers.
                      [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia..
                      | ]
                 end
+              | progress cbn [expr.interp_related_gen] in *
               | match goal with
                 | [ |- context[Z.shiftl] ] => rewrite Z.shiftl_mul_pow2 by auto with zarith
                 | [ |- context[Z.shiftr] ] => rewrite Z.shiftr_div_pow2 by auto with zarith
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index 3a682e2e9..a290c8d95 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -2196,8 +2196,15 @@ Module Compilers.
                 clear reify_interp_related reflect_interp_related ].
             all: repeat first [ progress cbn [reify reflect] in *
                               | progress fold (@reify) (@reflect) in *
-                              | progress cbn [expr_interp_related value_interp_related] in *
+                              | progress cbv [expr.interp_related] in *
+                              | progress cbn [expr.interp_related_gen value_interp_related] in *
                               | break_innermost_match_step
+                              | match goal with
+                                | [ |- context G[expr.interp_related_gen ?ii (@type.eqv) (UnderLets.to_expr ?v)] ]
+                                  => let G' := context G[expr_interp_related (UnderLets.to_expr v)] in
+                                     change G';
+                                     rewrite <- UnderLets.to_expr_interp_related_iff
+                                end
                               | rewrite <- UnderLets.to_expr_interp_related_iff
                               | exact id
                               | assumption
@@ -2211,12 +2218,12 @@ Module Compilers.
             : rawexpr_interp_related r v
               -> expr_interp_related (expr_of_rawexpr r) v.
           Proof using Type.
-            revert v; induction r; cbn [expr_of_rawexpr expr_interp_related rawexpr_interp_related]; intros.
+            cbv [expr.interp_related]; revert v; induction r; cbn [expr_of_rawexpr expr.interp_related_gen rawexpr_interp_related]; intros.
             all: repeat first [ progress destruct_head'_and
                               | progress destruct_head'_ex
                               | progress subst
                               | progress inversion_sigma
-                              | progress cbn [eq_rect type_of_rawexpr expr.interp expr_interp_related type_of_rawexpr] in *
+                              | progress cbn [eq_rect type_of_rawexpr expr.interp expr.interp_related_gen type_of_rawexpr] in *
                               | assumption
                               | exfalso; assumption
                               | apply conj
@@ -2238,7 +2245,8 @@ Module Compilers.
                               | progress destruct_head'_and
                               | assumption
                               | apply reflect_interp_related
-                              | progress cbn [expr_interp_related]
+                              | progress cbn [expr.interp_related_gen]
+                              | progress cbv [expr.interp_related]
                               | solve [ eauto ] ].
           Qed.
 
@@ -2249,7 +2257,8 @@ Module Compilers.
           Proof using Type.
             revert t e H v; induction re.
             all: repeat first [ progress intros
-                              | progress cbn [rawexpr_equiv_expr eq_rect rawexpr_interp_related type_of_rawexpr expr_interp_related] in *
+                              | progress cbn [rawexpr_equiv_expr eq_rect rawexpr_interp_related type_of_rawexpr expr.interp_related_gen] in *
+                              | progress cbv [expr.interp_related] in *
                               | progress subst
                               | progress destruct_head'_and
                               | progress destruct_head'_ex
@@ -2302,7 +2311,8 @@ Module Compilers.
               -> rawexpr_interp_related re2 (rew [type.interp base.interp] eq_type_of_rawexpr_equiv H in v).
           Proof using Type.
             revert re2 H; induction re1, re2; intros H H'.
-            all: repeat first [ progress cbn [rawexpr_equiv rawexpr_interp_related eq_rect type_of_rawexpr projT1 projT2 rawexpr_equiv_expr expr_interp_related] in *
+            all: repeat first [ progress cbn [rawexpr_equiv rawexpr_interp_related eq_rect type_of_rawexpr projT1 projT2 rawexpr_equiv_expr expr.interp_related_gen] in *
+                              | progress cbv [expr.interp_related] in *
                               | eassumption
                               | reflexivity
                               | progress intros
@@ -2419,12 +2429,10 @@ Module Compilers.
                | None => True
                | Some v1 => UnderLets.interp_related
                               ident_interp
-                              (fun e
-                               => expr_interp_related
-                                    ((if should_do_again
-                                         return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> _
-                                      then reify_expr
-                                      else fun v1 => v1) e))
+                              (if should_do_again
+                                  return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> _
+                               then expr.interp_related_gen ident_interp (fun t => value_interp_related)
+                               else expr_interp_related)
                               v1
                               v2
                end.