diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-04-15 14:05:03 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:16 -0400 |
| commit | 0e873baff11d8abbe9696d2bb137e73576d3857d (patch) | |
| tree | 0a3f126b743a32777f2854fa7f4e170166cb3cc2 /src/Assembly/QhasmUtil.v | |
| parent | e47ac2cea2614da8918861607fc0c74d30ebb7fa (diff) | |
Simpler QhasmCommon grammar
updating QhasmCommon
Pushing through changes
Pushing through changes
Pushing through changes
Pushing through changes
Pushing through changes
Pushing through changes
Diffstat (limited to 'src/Assembly/QhasmUtil.v')
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index 774dc50b8..70c3e4218 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -10,11 +10,24 @@ Module Util. Definition indexToNat {lim: nat} (i: Index lim): nat := proj1_sig i. Coercion indexToNat : Index >-> nat. + (* Float Manipulations *) + + Definition getFractionalBits {n} (reg: FReg n): nat := + if (Nat.eq_dec n 32) then 23 else + if (Nat.eq_dec n 64) then 52 else 0. + + Definition getFloatInstance {n} (reg: FReg n): Float n (getFractionalBits reg). + refine match reg with + | regFloat32 _ => (eq_rect _ id Float32 _ _) + | regFloat64 _ => (eq_rect _ id Float64 _ _) + end; abstract intuition. + Defined. + (* Magical Bitwise Manipulations *) (* Force w to be m bits long, by truncation or zero-extension *) Definition trunc {n} (m: nat) (w: word n): word m. - destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. + destruct (lt_eq_lt_dec n m) as [s|s]; try destruct s as [s|s]. - replace m with (n + (m - n)) by abstract intuition. refine (zext w (m - n)). @@ -49,11 +62,11 @@ Module Util. Proof. intros; destruct x; simpl; intuition. Qed. Definition segmentStackWord {n} (x: Stack n) (w: word n): word (32 * (getStackWords x)). - intros; destruct x; simpl; intuition. + intros; destruct x; simpl; intuition. Defined. Definition desegmentStackWord {n} (x: Stack n) (w: word (32 * (getStackWords x))): word n. - intros; destruct x; simpl; intuition. + intros; destruct x; simpl; intuition. Defined. End Util. |