diff options
author | 2017-10-13 12:18:37 -0400 | |
---|---|---|
committer | 2017-10-13 12:19:09 -0400 | |
commit | 7ac77b96dda29e3c8e4be4a06ed3ef9c7f94abd8 (patch) | |
tree | d62a3131198003e8ff7498593c7c2a04ab4c5b6c /src | |
parent | 8ee40838bdbeccf31cbd454c10426f12e48eae30 (diff) |
Add comment to Compilers/Z/Bounds/Interpretation.v
Hopefully this will help with extending the framework. Also remove
[t_map4]; it was unused and didn't match the types of the other [t_mapn]s.
Diffstat (limited to 'src')
-rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 23 |
1 files changed, 21 insertions, 2 deletions
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index 25762401d..9de556f74 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -25,6 +25,7 @@ Module Import Bounds. Section with_bitwidth. Context (bit_width : option Z). + (** Generic helper definitions *) Definition two_corners (f : Z -> Z) : t -> t := fun x => let (lx, ux) := x in @@ -63,8 +64,26 @@ Module Import Bounds. := fun x y z => eight_corners f x y z. Definition t_map3 (f : Z -> Z -> Z -> Z) : t -> t -> t -> t := fun x y z => truncation_bounds (eight_corners f x y z). - Definition t_map4 (f : bounds -> bounds -> bounds -> bounds -> bounds) (x y z w : t) - := truncation_bounds (f x y z w). + (** Definitions of the actual bounds propogation *) + (** Rules for adding new operations: + + - Every output must pass through [truncation_bounds] as the + final step. Using [BuildTruncated_bounds] can be more + convienient at times. The reason for [truncation_bounds] is + that we know that every operation is bounded by the bitwidth + of the underlying data type, and maintaining this constraint + is important sometimes. + + - Use [t_mapn] to if the underlying operation on [Z] is + monotonic in all [n] of its arguments ([t_mapn] handles both + monotonic non-increasing and monotonic non-decreasing, and + applies [truncation_bounds]) + + - The [t_mapn'] definitions are for if you need to do further + processing on the bounds before applying + [truncation_bounds]; they handle lifting monotonic [Z] + functions without truncating to the bitwidth. *) + Definition add : t -> t -> t := t_map2 Z.add. Definition sub : t -> t -> t := t_map2 Z.sub. Definition mul : t -> t -> t := t_map2 Z.mul. |