62 lines
1.6 KiB
Text
62 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 ;
|
|||
|
|
}
|
|||
|
|
}
|
|||
|
|
|