File: fpthreesimp.sail

package info (click to toggle)
sail-ocaml 0.19.1%2Bdfsg5-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 18,008 kB
  • sloc: ml: 75,941; ansic: 8,848; python: 1,342; exp: 560; sh: 474; makefile: 218; cpp: 36
file content (14 lines) | stat: -rw-r--r-- 456 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
 
default Order dec

$include <prelude.sail>

val Zeros : forall 'N, 'N >= 0. int('N) -> bits('N)

type FPExponent ('N : Int) = {'E, ('N == 16 & 'E == 5) | ('N == 32 & 'E == 8) | ('N == 64 & 'E == 11). int('E)}

val FPThree : forall 'N, 'N in {16, 32, 64}. (implicit('N), bits(1)) -> bits('N)

function FPThree(N, sign) = {
  let E : FPExponent('N) = if 'N == 16 then 5 else if 'N == 32 then 8 else 11;
  sign @ 0b1 @ Zeros(E - 1) @ 0b1 @ Zeros('N - E - 2)
}