diff options
| author |  Robert Sloan <varomodt@gmail.com> | 2016-04-29 16:24:14 -0400 |
|---|---|---|
| committer | Robert Sloan <varomodt@gmail.com> | 2016-06-22 13:43:22 -0400 |
| commit | 49ed9cfaa635bfa0a12bfe1231b103f247ffc141 (patch) | |
| tree | 4a1077faa94302ea436333a6efac8f2bd0ff2ebe /src/Assembly/QhasmUtil.v | |
| parent | 3cc7ed63dc1b3f26b6c64ebc46e526abdcb71071 (diff) | |
removed float operations + improved pseudo somewhat
Diffstat (limited to 'src/Assembly/QhasmUtil.v')
| -rw-r--r-- | src/Assembly/QhasmUtil.v | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v index 70c3e4218..dea937ac1 100644 --- a/src/Assembly/QhasmUtil.v +++ b/src/Assembly/QhasmUtil.v @@ -10,19 +10,6 @@ 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 *) |