Initial stab at id_with_alt

What remains (beyond the equality-semidecider) is to propogate the side
conditions through the boundedness finder.

3 files changed, 20 insertions, 6 deletions

diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v
index c574d3fb1..7b1254138 100644
--- a/src/Compilers/Z/Bounds/Interpretation.v
+++ b/src/Compilers/Z/Bounds/Interpretation.v
@@ -21,6 +21,8 @@ Module Import Bounds.
   Definition t := bounds.
   Bind Scope bounds_scope with t.
   Local Coercion Z.of_nat : nat >-> Z.
+  Definition interp_base_type (ty : base_type) : Set := t.
+
   Section with_bitwidth.
     Context (bit_width : option Z).
     Definition two_corners (f : Z -> Z) : t -> t
@@ -151,9 +153,12 @@ Module Import Bounds.
     Definition cmovle (x y r1 r2 : t) : t
       := truncation_bounds (cmovle' r1 r2).
 
-    (** TODO(jgross): swap to other bounds here *)
-    Definition id_with_alt (x y : t) : t
-      := truncation_bounds x.
+    Definition id_with_alt {T1 T2 Tout} (x : interp_base_type T1) (y : interp_base_type T2)
+      : interp_base_type Tout
+      := truncation_bounds match T1, T2, Tout with
+                           | TZ, TZ, TZ => (*y*)x
+                           | _, _, _ => x
+                           end.
   End with_bitwidth.
   Section with_bitwidth2.
     Context (bit_width1 bit_width2 : option Z)
@@ -185,8 +190,6 @@ Module Import Bounds.
     Notation "- x" := (opp _ x) : bounds_scope.
   End Notations.
 
-  Definition interp_base_type (ty : base_type) : Set := t.
-
   Definition log_bit_width_of_base_type ty : option nat
     := match ty with
        | TZ => None
diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
index 169c59d96..c0172c67a 100644
--- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
+++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v
@@ -332,6 +332,7 @@ Lemma is_bounded_by_interp_op t tR (opc : op t tR)
       (bs : interp_flat_type Bounds.interp_base_type _)
       (v : interp_flat_type interp_base_type _)
       (H : Bounds.is_bounded_by bs v)
+      (*H_side : interped_op_side_conditions opc v = true*)
   : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v).
 Proof.
   destruct opc;
@@ -390,7 +391,8 @@ Proof.
                  | progress simpl in *
                  | progress split_min_max
                  | omega ]. }
-  { split; assumption. }
+  { break_innermost_match; simpl in *; Z.ltb_to_lt; subst;
+      split; assumption. }
   { destruct_head Bounds.t; cbv [Bounds.zselect' Z.zselect].
     break_innermost_match; split_min_max; omega. }
   { apply (@monotone_eight_corners true true true _ _ _); split; auto. }
diff --git a/src/Compilers/Z/Syntax/Util.v b/src/Compilers/Z/Syntax/Util.v
index d85226c98..c50ac7bb2 100644
--- a/src/Compilers/Z/Syntax/Util.v
+++ b/src/Compilers/Z/Syntax/Util.v
@@ -26,6 +26,15 @@ Definition is_const_or_opp s d (v : op s d) : bool
 Arguments is_const_or_opp [s d] v.
 
 
+Definition interped_op_side_conditions {s d} (opc : op s d)
+  : interp_flat_type interp_base_type s -> bool
+  := match opc in op s d return interp_flat_type _ s -> _ with
+     | IdWithAlt TZ TZ TZ
+       => fun v1v2 : Z * Z
+          => Z.eqb (fst v1v2) (snd v1v2)
+     | _ => fun _ => true
+     end.
+
 Definition cast_back_flat_const {var t f V}
            (v : interp_flat_type interp_base_type (@SmartFlatTypeMap base_type var f t V))
   : interp_flat_type interp_base_type t