CSE without inlining arithmetic expressions

This takes care of most of #158.  The remaining bits are reworking the
Wf and interpretation lemmas to actually work.  (The former needs a only
bit of rethinking and rephrasing to handle the fact that sometimes we
change the stored symbolic expression from a complicated one to a fresh
variable, while the latter needs major surgery, which Adam tells me is
easy, and this is a note that when I come back to it, I should look at
the email thread with Adam about CSE from last summer.)

1 files changed, 42 insertions, 14 deletions

diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v
index b66db5c33..8d8a5d86f 100644
--- a/src/Compilers/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/CommonSubexpressionEliminationWf.v
@@ -14,6 +14,7 @@ Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.UniquePose.
 Require Import Crypto.Util.Tactics.SplitInContext.
 Require Import Crypto.Util.Decidable.
 
@@ -26,11 +27,11 @@ Section symbolic.
           (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true)
           (op_code_bl : forall x y, op_code_beq x y = true -> x = y)
           (op_code_lb : forall x y, x = y -> op_code_beq x y = true)
-          (interp_base_type : base_type_code -> Type)
           (op : flat_type base_type_code -> flat_type base_type_code -> Type)
           (symbolize_op : forall s d, op s d -> op_code).
   Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
-  Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr).
+  Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr)
+          (inline_symbolic_expr_in_lookup : bool).
 
   Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code op_code base_type_code_beq op_code_beq).
   Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code op_code base_type_code_beq op_code_beq base_type_code_lb op_code_lb).
@@ -38,9 +39,6 @@ Section symbolic.
 
   Local Notation flat_type := (flat_type base_type_code).
   Local Notation type := (type base_type_code).
-  Local Notation interp_type := (interp_type interp_base_type).
-  Local Notation interp_flat_type_gen := interp_flat_type.
-  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
   Local Notation exprf := (@exprf base_type_code op).
   Local Notation expr := (@expr base_type_code op).
   Local Notation Expr := (@Expr base_type_code op).
@@ -48,9 +46,9 @@ Section symbolic.
   Local Notation symbolicify_smart_var := (@symbolicify_smart_var base_type_code op_code).
   Local Notation symbolize_exprf := (@symbolize_exprf base_type_code op_code op symbolize_op).
   Local Notation norm_symbolize_exprf := (@norm_symbolize_exprf base_type_code op_code op symbolize_op normalize_symbolic_op_arguments).
-  Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments).
-  Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments).
-  Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments).
+  Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments inline_symbolic_expr_in_lookup).
+  Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments inline_symbolic_expr_in_lookup).
+  Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op normalize_symbolic_op_arguments inline_symbolic_expr_in_lookup).
   Local Notation SymbolicExprContext := (@SymbolicExprContext base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl).
   Local Notation SymbolicExprContextOk := (@SymbolicExprContextOk base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl base_type_code_lb op_code_bl op_code_lb).
   Local Notation prepend_prefix := (@prepend_prefix base_type_code op).
@@ -82,8 +80,8 @@ Section symbolic.
     Local Arguments lookupb : simpl never.
     Local Arguments extendb : simpl never.
     Lemma wff_csef G G' t e1 e2
-          (m1 : @SymbolicExprContext (interp_flat_type_gen var1))
-          (m2 : @SymbolicExprContext (interp_flat_type_gen var2))
+          (m1 : @SymbolicExprContext (interp_flat_type var1))
+          (m2 : @SymbolicExprContext (interp_flat_type var2))
           (Hlen : length m1 = length m2)
           (Hm1m2None : forall t v, lookupb m1 v t = None <-> lookupb m2 v t = None)
           (Hm1m2Some : forall t v sv1 sv2,
@@ -108,9 +106,13 @@ Section symbolic.
               | [ H : lookupb ?m1 ?x = Some ?k, H' : lookupb ?m2 ?x = None |- _ ]
                 => apply Hm1m2None in H'; congruence
               end;
-          [ | constructor; intros; auto; [].. ];
+          lazymatch goal with
+          | [ |- wff _ (LetIn _ _) (LetIn _ _) ]
+            => constructor; intros; auto; []
+          | _ => idtac
+          end;
           match goal with H : _ |- _ => apply H end;
-          repeat first [ progress unfold symbolize_var
+          try solve [ repeat first [ progress unfold symbolize_var
                        | rewrite Hlen
                        | progress subst
                        | setoid_rewrite length_extendb
@@ -130,8 +132,34 @@ Section symbolic.
                        | break_innermost_match_step
                        | break_innermost_match_hyps_step
                        | progress simpl in *
-                       | solve [ intuition (eauto || congruence) ] ]. }
-    Qed.
+                       | solve [ intuition (eauto || congruence) ]
+                       | match goal with
+                         | [ H : forall t x y, _ |- _ ] => specialize (fun t x0 x1 y0 y1 => H t (x0, x1) (y0, y1)); cbn [fst snd] in H
+                         | [ H : In (existT _ ?t (?x, ?x')) (flatten_binding_list (symbolicify_smart_var _ _) (symbolicify_smart_var _ _)),
+                                 Hm1m2Some : forall t v sv1 sv2, _ -> _ -> forall k', In k' (flatten_binding_list _ _) -> In k' ?G |- _ ]
+                           => is_var x; is_var x';
+                              lazymatch goal with
+                              | [ H : In (existT _ t ((fst x, _), (fst x', _))) G |- _ ] => fail
+                              | _ => let H' := fresh in
+                                     refine (let H' := flatten_binding_list_SmartVarfMap2_pair_in_generalize2 H _ _ in _);
+                                     destruct H' as [? [? H']];
+                                     eapply Hm1m2Some in H'; [ | eassumption.. ]
+                              end
+                         end ] ].
+         repeat first [ progress unfold symbolize_var
+                       | rewrite Hlen
+                       | progress subst
+                       | setoid_rewrite length_extendb
+                       | setoid_rewrite List.in_app_iff
+                       | progress destruct_head' or
+                       | solve [ eauto ]
+                       | progress intros ].
+         (** FIXME: This actually isn't true, because the symbolic
+             expr stored in G might not be the same as the one in the
+             expression tree, when the one in the expression tree is a
+             fresh var *)
+         admit. }
+    Admitted.
 
     Lemma wff_prepend_prefix {var1' var2'} prefix1 prefix2 G t e1 e2
           (Hlen : length prefix1 = length prefix2)