Add support for cse-modulo-normalization

6 files changed, 96 insertions, 27 deletions

diff --git a/src/Compilers/CommonSubexpressionElimination.v b/src/Compilers/CommonSubexpressionElimination.v
index f1d77a482..e5dd8b9e8 100644
--- a/src/Compilers/CommonSubexpressionElimination.v
+++ b/src/Compilers/CommonSubexpressionElimination.v
@@ -14,7 +14,7 @@ Local Open Scope list_scope.
 
 Inductive symbolic_expr {base_type_code op_code} : Type :=
 | STT
-| SVar  (v : flat_type base_type_code) (n : nat)
+| SVar  (n : nat)
 | SOp   (argT : flat_type base_type_code) (op : op_code) (args : symbolic_expr)
 | SPair (x y : symbolic_expr)
 | SFst  (A B : flat_type base_type_code) (x : symbolic_expr)
@@ -33,7 +33,7 @@ Defined.
 
 Ltac inversion_symbolic_expr_step :=
   match goal with
-  | [ H : SVar _ _ = SVar _ _ |- _ ] => inversion H; clear H
+  | [ H : SVar _ = SVar _ |- _ ] => inversion H; clear H
   | [ H : SOp _ _ _ = SOp _ _ _ |- _ ] => inversion H; clear H
   | [ H : SPair _ _ = SPair _ _ |- _ ] => inversion H; clear H
   | [ H : SFst _ _ _ = SFst _ _ _ |- _ ] => inversion H; clear H
@@ -54,9 +54,11 @@ Section symbolic.
           (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).
-
+          (symbolize_op : forall s d, op s d -> op_code)
+          (op_code_leb : forall (arg1T arg2T : flat_type base_type_code), op_code -> op_code -> bool).
   Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
+  Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr).
+
   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).
   Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
@@ -99,6 +101,61 @@ Section symbolic.
          end.
   End with_var0.
 
+  Local Notation op_code_eqb argT1 argT2 op1 op2
+    := (flat_type_beq _ base_type_code_beq argT1 argT2 && op_code_beq op1 op2).
+  Local Notation ltb_of_leb leb eqb
+    := (leb && negb eqb).
+  Local Notation op_code_ltb argT1 argT2 op1 op2
+    := (ltb_of_leb (op_code_leb argT1 argT2 op1 op2)
+                   (op_code_eqb argT1 argT2 op1 op2)).
+  Local Notation leb_pair leb1 eqb1 leb2
+    := (ltb_of_leb leb1 eqb1 || (eqb1 && leb2)).
+
+  Fixpoint symbolic_expr_leb (x y : symbolic_expr) : bool
+    := match x, y with
+       | STT, _ => true
+       | _, STT => false
+       | SVar n1, SVar n2 => Nat.leb n1 n2
+       | SVar _, _ => true
+       | _, SVar _ => false
+       | SOp argT1 op1 args1, SOp argT2 op2 args2
+         => leb_pair (op_code_leb argT1 argT2 op1 op2)
+                     (op_code_eqb argT1 argT2 op1 op2)
+                     (symbolic_expr_leb args1 args2)
+       | SOp _ _ _, _ => true
+       | _, SOp _ _ _ => false
+       | SPair x1 y1, SPair x2 y2
+         => leb_pair (symbolic_expr_leb x1 x2)
+                     (symbolic_expr_beq x1 x2)
+                     (symbolic_expr_leb y1 y2)
+       | SPair _ _, _ => true
+       | _, SPair _ _ => false
+       | SFst _ _ x, SFst _ _ y
+         => symbolic_expr_leb x y
+       | SFst _ _ _, _ => true
+       | _, SFst _ _ _ => false
+       | SSnd _ _ x, SSnd _ _ y
+         => symbolic_expr_leb x y
+       | SSnd _ _ _, _ => true
+       | _, SSnd _ _ _ => false
+       | SInvalid, _ => true
+       end.
+  Definition symbolic_expr_ltb x y
+    := ltb_of_leb (symbolic_expr_leb x y) (symbolic_expr_beq x y).
+
+  Fixpoint symbolic_expr_normalize (x : symbolic_expr) : symbolic_expr
+    := match x with
+       | STT => STT
+       | SVar n => SVar n
+       | SOp argT op args
+         => SOp argT op (normalize_symbolic_op_arguments op args)
+       | SPair x y
+         => SPair (symbolic_expr_normalize x) (symbolic_expr_normalize y)
+       | SFst A B x => SFst A B (symbolic_expr_normalize x)
+       | SSnd A B x => SFst A B (symbolic_expr_normalize x)
+       | SInvalid => SInvalid
+       end.
+
   Section with_var.
     Context {var : base_type_code -> Type}.
 
@@ -109,7 +166,7 @@ Section symbolic.
     Context (prefix : list (sigT (fun t : flat_type => @exprf fsvar t))).
 
     Definition symbolize_var (xs : mapping) (t : flat_type) : symbolic_expr :=
-      SVar t (length xs).
+      SVar (length xs).
 
     Fixpoint symbolize_exprf
              {t} (v : @exprf fsvar t) {struct v}
@@ -127,6 +184,9 @@ Section symbolic.
                              end
          end.
 
+    Definition norm_symbolize_exprf {t} v : option symbolic_expr
+      := option_map symbolic_expr_normalize (@symbolize_exprf t v).
+
     Definition symbolicify_smart_var {t : flat_type}
                (vs : interp_flat_type_gen var t)
                (ss : symbolic_expr)
@@ -139,7 +199,7 @@ Section symbolic.
       : @exprf var t
       := match v in @Syntax.exprf _ _ _ t return exprf t with
          | LetIn tx ex _ eC
-           => let sx := symbolize_exprf ex in
+           => let sx := norm_symbolize_exprf ex in
               let ex' := @csef _ ex xs in
               let '(sx, sv) := match sx with
                                | Some sx => (sx, lookupb xs sx)
@@ -174,6 +234,6 @@ Section symbolic.
     := fun var => cse (prefix _) (e _) empty.
 End symbolic.
 
-Global Arguments csef {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {var t} _ _.
-Global Arguments cse {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {var} prefix {t} _ _.
-Global Arguments CSE {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op {t} e prefix var.
+Global Arguments csef {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op normalize_symbolic_op_arguments {var t} _ _.
+Global Arguments cse {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op normalize_symbolic_op_arguments {var} prefix {t} _ _.
+Global Arguments CSE {_} op_code base_type_code_beq op_code_beq base_type_code_bl {_} symbolize_op normalize_symbolic_op_arguments {t} e prefix var.
diff --git a/src/Compilers/CommonSubexpressionEliminationDenote.v b/src/Compilers/CommonSubexpressionEliminationDenote.v
index 4d07a9c05..c45fae00e 100644
--- a/src/Compilers/CommonSubexpressionEliminationDenote.v
+++ b/src/Compilers/CommonSubexpressionEliminationDenote.v
@@ -57,13 +57,11 @@ Section symbolic.
       : option (interp_flat_type interp_base_type t)
       := match se, t with
          | STT, Unit => Some tt
-         | SVar t n, t'
-           => if flat_type_beq t t'
-              then match List.nth_error m (length m - n) with
-                   | Some e => @var_cast _ t' (projT2 (snd e))
-                   | None => None
-                   end
-              else None
+         | SVar n, t
+           => match List.nth_error m (length m - n) with
+              | Some e => @var_cast _ t (projT2 (snd e))
+              | None => None
+              end
          | SOp argsT op args, _
            => match denote_op argsT t op, @denote_symbolic_expr argsT args with
               | Some opc, Some eargs => Some (interp_op _ _ opc eargs)
diff --git a/src/Compilers/CommonSubexpressionEliminationInterp.v b/src/Compilers/CommonSubexpressionEliminationInterp.v
index 7126b0c72..2d9115eb6 100644
--- a/src/Compilers/CommonSubexpressionEliminationInterp.v
+++ b/src/Compilers/CommonSubexpressionEliminationInterp.v
@@ -39,8 +39,9 @@ Section symbolic.
           (interp_op : forall s d (opc : op s d), interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d)
           (symbolize_op : forall s d, op s d -> op_code)
           (denote_op : forall s d, op_code -> option (op s d)).
-
   Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
+  Context (normalize_symbolic_op_arguments : op_code -> symbolic_expr -> symbolic_expr).
+
   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).
   Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
@@ -56,9 +57,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 csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
+  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 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).
diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v
index 431978c7b..b66db5c33 100644
--- a/src/Compilers/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/CommonSubexpressionEliminationWf.v
@@ -29,8 +29,9 @@ Section symbolic.
           (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).
+
   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).
   Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
@@ -46,9 +47,10 @@ 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 csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
-  Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl 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 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).
@@ -69,6 +71,14 @@ Section symbolic.
       induction Hwf; simpl; erewrite_hyp ?* by eassumption; reflexivity.
     Qed.
 
+    Lemma wff_norm_symbolize_exprf G t e1 e2
+          (HG : forall t x y, List.In (existT _ t (x, y)) G -> snd x = snd y)
+          (Hwf : wff G e1 e2)
+      : @norm_symbolize_exprf var1 t e1 = @norm_symbolize_exprf var2 t e2.
+    Proof.
+      unfold norm_symbolize_exprf; erewrite wff_symbolize_exprf by eassumption; reflexivity.
+    Qed.
+
     Local Arguments lookupb : simpl never.
     Local Arguments extendb : simpl never.
     Lemma wff_csef G G' t e1 e2
@@ -92,7 +102,7 @@ Section symbolic.
     Proof.
       revert dependent m1; revert m2; revert dependent G'.
       induction Hwf; simpl; intros; try constructor; auto.
-      { erewrite wff_symbolize_exprf by eassumption.
+      { erewrite wff_norm_symbolize_exprf by eassumption.
         break_innermost_match;
           try match goal with
               | [ H : lookupb ?m1 ?x = Some ?k, H' : lookupb ?m2 ?x = None |- _ ]
diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v
index 229e5f869..5240cf9c5 100644
--- a/src/Compilers/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -187,7 +187,7 @@ Section cse.
        | Mul => SMul
        | Sub => SSub
        end.
-  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op t e (fun _ => nil).
+  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op (fun _ x => x) t e (fun _ => nil).
 End cse.
 
 Definition example_expr_simplified := Eval vm_compute in InlineConst is_const (Linearize example_expr).
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index adb29e81f..6fe27b2e4 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -108,7 +108,7 @@ Section reflection.
        | OPaddm => SOPaddm
        end.
 
-  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op t e (fun _ => nil).
+  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op (fun _ x => x) t e (fun _ => nil).
 
   Inductive inline_option := opt_inline | opt_default | opt_noinline.