61 lines
1.6 KiB
Text
61 lines
1.6 KiB
Text
export {
|
||
/* Platform Specific Types */
|
||
type machine.Float16 = IEEE-754.half ~ <machine.Bits 16>;
|
||
type machine.Float32 = IEEE-754.single ~ <machine.Bits 32>;
|
||
type machine.Float64 = IEEE-754.double ~ <machine.Bits 64>;
|
||
|
||
overload + = λ{
|
||
a:ℝ ~ machine.Float16 ;
|
||
b:ℝ ~ machine.Float16 ;
|
||
} -> ℝ ~ machine.Float16 ↦ {
|
||
machine.Float16.add a b;
|
||
};
|
||
|
||
overload * = λ{
|
||
a:ℝ ~ machine.Float16 ;
|
||
b:ℝ ~ machine.Float16 ;
|
||
} -> ℝ ~ machine.Float16 ↦ {
|
||
machine.Float16.mul a b;
|
||
};
|
||
|
||
let Sign = enum { Positive; Negative; };
|
||
let Sign.Positive : <machine.Bits 1> = 0;
|
||
let Sign.Negative : <machine.Bits 1> = 1;
|
||
|
||
let softfloat16-mul = λ{
|
||
{
|
||
a.sign: Sign
|
||
~ <machine.Bits 1>
|
||
;
|
||
a.exponent: ℤ_[-14,15]
|
||
~ <BiasedInt -14>
|
||
~ ℤ_32
|
||
~ <PosInt 2 BigEndian>
|
||
~ <Seq <Digit 2>~Bit >
|
||
~ <machine.Bits 5>
|
||
;
|
||
a.significand: ℤ_2048
|
||
~ <PosInt 2 BigEndian>
|
||
~ <Seq <Digit2> ~ Bit>
|
||
~ <machine.Bits 11>
|
||
;
|
||
} : ℝ
|
||
~ IEEE-754.Half
|
||
~ <machine.Bits 16>
|
||
;
|
||
{
|
||
b.sign: <machine.Bits 1>;
|
||
} : ℝ ~ IEEE-754.Half ~ <machine.Bits 16> ;
|
||
} -> result: ℝ ~ IEEE~754.Half ~ <machine.Bits 16> ↦ {
|
||
|
||
/* 1. unify */
|
||
|
||
/* 2. add exponent */
|
||
+ a.exponent b.exponent;
|
||
|
||
/* 3. normaize */
|
||
|
||
result.sign = bit-xor a.sign b.sign ;
|
||
}
|
||
}
|
||
|