diff options
author | Jason Gross <jgross@mit.edu> | 2017-06-11 20:06:32 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2017-06-11 20:06:32 -0400 |
commit | 079f1813cad0e1d8c62f30895d6d3b3bd5642bd3 (patch) | |
tree | 572ccafb49c51476dfd08d837cf724a7f94b4d48 /src/Compilers/Z | |
parent | c4af7d8327ef91e193856a1173dfa0c6d26d10fe (diff) |
Initial stab at id_with_alt
What remains (beyond the equality-semidecider) is to propogate the side
conditions through the boundedness finder.
Diffstat (limited to 'src/Compilers/Z')
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 13 | ||||
-rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 4 | ||||
-rw-r--r-- | src/Compilers/Z/Syntax/Util.v | 9 |
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 |