See also: mim::plug::math

Introduces a type constructor math.F for various IEEE-754 floating-point formats and a set of operations to calculate with instances of these types. All operations with the exception of math.conv expect a Nat as their very first argument. Via this mode you can fine-tune how strictly floating-point transformations must obey IEEE semantics. It comes before the implicit pe so that currying it - math.arith.add 0 - still yields a value polymorphic in pe.

Types

F

A floating-point type with p bits of precision and e exponent bits. The sign bit is neither included in p nor in e. Thus, the total number of bits occupied by a value of this type is p + e + 1. Current constant folding only supports IEEE binary16/binary32/binary64 literals, subject to host f16 support.

axm F: «2; Nat» → *;
 
anx let f16     = (10,  5);
anx let f32     = (23,  8);
anx let f64     = (52, 11);
anx let bf16    = ( 7,  8);
anx let nvtf32  = (10,  8);
anx let amdfp24 = (16,  7);
anx let pxr24   = (15,  8);
 
anx let F16     = F f16;
anx let F32     = F f32;
anx let F64     = F f64;
anx let BF16    = F bf16;
anx let NVTF32  = F nvtf32; // actually 19 bits; aligns to 32 bit
anx let AMDFP24 = F amdfp24;
anx let PXR24   = F pxr24;

Mode

mode

Fine-tunes how strictly a floating-point operation must obey IEEE semantics - see mim::plug::math::Mode.

pub mod mode {
    pub anx let none     = 0b0000000; // no optimizations allowed
    pub anx let nnan     = 0b0000001; // no NaNs
    pub anx let ninf     = 0b0000010; // no Infs
    pub anx let nsz      = 0b0000100; // no signed zeros
    pub anx let arcp     = 0b0001000; // allow reciprocal instead of division
    pub anx let contract = 0b0010000; // allow contraction, e.g. fused multiply-add
    pub anx let afn      = 0b0100000; // allow approximate functions
    pub anx let reassoc  = 0b1000000; // allow reassociation
    pub anx let finite   = 0b0000011; // nnan | ninf
    pub anx let unsafe   = 0b1001100; // nsz | arcp | reassoc
    pub anx let fast     = 0b1111111; // everything above
}

Numerical Operations

arith

Arithmetic operations.

axm arith.(add, sub, mul, div, rem):
    Nat → {pe: «2; Nat»} → «2; F pe» → F pe, normalize_arith;
 
anx lam minus (m: Nat) {pe: «2; Nat»} (a: F pe): F pe =
    arith.sub m (0:(F pe), a);

extrema

Minimum and maximum:

min or Max
i: Follows the behavior of libm's fmin/fmax. If either operand is a NaN, returns the other non-NaN operand. Returns NaN only if both operands are NaN; the returned NaN is always quiet. If the operands compare equal, returns a value that compares equal to both operands. This means that fmin(+/-0.0, +/-0.0) could return either -0.0 or 0.0.
I: Follows the semantics of minNum/maxNum specified in the draft of IEEE 754-2018. If either operand is a NaN, returns NaN. Otherwise, returns the lesser of the two arguments. -0.0 is considered to be less than +0.0 for this intrinsic.

Subtag	Alias	I	M
im	fmin	o	o
iM	fmax	o	x
Im	ieee754min	x	o
IM	ieee754max	x	x

axm extrema.(im = fmin,       iM = fmax,
             Im = ieee754min, IM = ieee754max):
    Nat → {pe: «2; Nat»} → «2; F pe» → F pe, normalize_extrema;

tri

Trigonometric and hypberbolic functions.

FF: sine, cosine, tangent, unused
Hyperbolic counterpart
Arcus/Area counterpart (inverse)

Subtag	Alias	A	H	FF	Meaning	Semantics
ahff	sin	o	o	oo	sine	\(\sin x\)
ahfF	cos	o	o	xo	cosine	\(\cos x\)
ahFf	tan	o	o	ox	tangent	\(\tan x\)
ahFF		o	o	xx	unused	-
aHff	sinh, h	o	x	oo	hyperbolic sine	\(\sinh x\)
aHfF	cosh	o	x	xo	hyperbolic cosine	\(\cosh x\)
aHFf	tanh	o	x	ox	hyperbolic tangent	\(\tanh x\)
aHFF		o	x	xx	unused	-
Ahff	asin , a	x	o	oo	arcus sine	\(\textrm{asin}\,x\)
AhfF	acos	x	o	xo	arcus cosine	\(\textrm{acos}\,x\)
AhFf	atan	x	o	ox	arcus tangent	\(\textrm{atan}\,x\)
AhFF		x	o	xx	unused	-
AHff	asinh	x	x	oo	area hyperbolic sine	\(\textrm{asinh}\,x\)
AHfF	acosh	x	x	xo	area hyperbolic cosine	\(\textrm{acosh}\,x\)
AHFf	atanh	x	x	ox	area hyperbolic tangent	\(\textrm{atanh}\,x\)
AHFF		x	x	xx	unused	-

axm tri.(ahff =  sin     , ahfF =  cos , ahFf =  tan , ahFF,
         aHff =  sinh = h, aHfF =  cosh, aHFf =  tanh, aHFF,
         Ahff = asin  = a, AhfF = acos , AhFf = atan , AhFF,
         AHff = asinh    , AHfF = acosh, AHFf = atanh, AHFF):
    Nat → {pe: «2; Nat»} → F pe → F pe, normalize_tri;

pow

Power function: \(x^y\)

axm pow: Nat → {pe: «2; Nat»} → «2; F pe» → F pe, normalize_pow;

rt

Square and cube root:

Name	Meaning	Semantics
math.rt.sq	square root	\(\sqrt{x}\)
math.rt.cb	cube root	\(\sqrt[3]{x}\)

axm rt.(sq, cb): Nat → {pe: «2; Nat»} → F pe → F pe, normalize_rt;

exp

Exponential function and logarithm:

Logarithm
BB: natural, binary, decimal, unused

Subtag	Alias	L	BB	Meaning	Semantics
lbb	exp	o	oo	natural exponential	\(e^x\)
lbB	exp2, bin	o	ox	exponential with base 2	\(2^x\)
lBb	exp10, dec	o	xo	exponential with base 10	\(10^x\)
lBB	unused	o	xx	-	unused
Lbb	log	x	oo	natural logarithm	\(\ln x\)
LbB	log2	x	ox	logarithm with base 2	\(\log_2 x\)
LBb	log10	x	xo	logarithm with base 10	\(\log_{10} x\)
LBB	unused	x	xx	-	unused

axm exp.(lbb = exp, lbB = exp2 = bin, lBb = exp10 = dec, lBB,
         Lbb = log, LbB = log2      , LBb = log10      , LBB):
    Nat → {pe: «2; Nat»} → F pe → F pe, normalize_exp;

er

Error and complementary error function.

Name	Meaning	Semantics
math.er.f	error function	\(\frac{2}{\sqrt\pi}\int_0^x e^{-t^2}\,dt\)
math.er.fc	complementary error function	\(\frac{2}{\sqrt\pi}\int_x^\infty e^{-t^2}\,dt = 1 - \textrm{erf}(x)\)

axm er.(f, fc): Nat → {pe: «2; Nat»} → F pe → F pe, normalize_er;

gamma

Gamma function and its natural logarithm.

Name	Meaning	Semantics
math.gamma.t	gamma function	\(\Gamma(x) = \int_0^\infty t^{x-1} e^{-t}\,dt\)
math.gamma.l	natural logarithm of gamma function	\(\ln \mid \int_0^\infty t^{x-1} e^{-t}\,dt \mid\)

axm gamma.(t, l): Nat → {pe: «2; Nat»} → F pe → F pe, normalize_gamma;

abs

Absolute value of a floating-point number.

axm abs: Nat → {pe: «2; Nat»} → F pe → F pe, normalize_abs;

round

Common rounding operations for floating-point numbers:

floor
ceil
round
truncate

Name	Meaning	Semantics
math.round.f	round down	\(\lfloor x \rfloor \)
math.round.c	round up	\(\lceil x \rceil \)
math.round.r	round to nearest integer	\(round (x)\)
math.round.t	round towards zero	\(trunc (x)\)

axm round.(f,c,r,t): Nat → {pe: «2; Nat»} → F pe → F pe, normalize_round;

Other Operations

cmp

Floating-point comparison is composed of 4 disjoint relations:

Unordered (yields true if either operand is a QNaN)
Greater
Less
Equal

Subtag	Alias	U	G	L	E	Meaning
ugle	f	o	o	o	o	always false
uglE	e	o	o	o	x	ordered and equal
ugLe	l	o	o	x	o	ordered and less
ugLE	le	o	o	x	x	ordered and less or equal
uGle	g	o	x	o	o	ordered and greater
uGlE	ge	o	x	o	x	ordered and greater or equal
uGLe	ne	o	x	x	o	ordered and not equal
uGLE	o	o	x	x	x	ordered (no NaNs)
Ugle	u	x	o	o	o	unordered (either is NaN)
UglE	ue	x	o	o	x	unordered or equal
UgLe	ul	x	o	x	o	unordered or less
UgLE	ule	x	o	x	x	unordered or less or equal
UGle	ug	x	x	o	o	unordered or greater
UGlE	uge	x	x	o	x	unordered or greater or equal
UGLe	une	x	x	x	o	unordered or not equal
UGLE	t	x	x	x	x	always true

axm cmp.(ugle =   f, uglE =   e, ugLe =   l, ugLE =  le,
         uGle =   g, uGlE =  ge, uGLe =  ne, uGLE =   o,
         Ugle =   u, UglE =  ue, UgLe =  ul, UgLE = ule,
         UGle =  ug, UGlE = uge, UGLe = une, UGLE =   t):
    Nat → {pe: «2; Nat»} → «2; F pe» → Bool, normalize_cmp;

is_finite

Returns tt if the float is finite and ff if not (i.e. if it is ±∞ or NaN).

axm is_finite: Nat → {pe: «2; Nat»} → F pe → Bool;

conv

Conversion between floating-point and index types - both signed and unsigned - of different sizes.

pub mod conv {
    axm s2f: { ss:     Nat } → [dpe: «2; Nat»] →   Idx  ss → F dpe, normalize_conv;
    axm u2f: { ss:     Nat } → [dpe: «2; Nat»] →   Idx  ss → F dpe, normalize_conv;
    axm f2s: {spe: «2; Nat»} → [ ds:     Nat ] → F spe →   Idx  ds, normalize_conv;
    axm f2u: {spe: «2; Nat»} → [ ds:     Nat ] → F spe →   Idx  ds, normalize_conv;
    axm f2f: {spe: «2; Nat»} → [dpe: «2; Nat»] → F spe → F dpe,     normalize_conv;
}

slf

Standard logistic function of a floating-point number ( \(\textrm{slf}(x) = \frac{1}{1+e^{-x}}\))

anx lam slf (m: Nat) {pe: «2; Nat»} (x: F pe): F pe =

arith.div m ((conv.f2f pe 1.0:(F64)), arith.add m ((conv.f2f pe 1.0:(F64)), exp.exp m (minus m x)));

sgn

Sign function

anx lam sgn (m: Nat) {pe: «2; Nat»} (x: F pe): F pe =

((conv.f2f pe (-1.0:(F64))), ((conv.f2f pe 0.0:(F64)), (conv.f2f pe 1.0:(F64)))#(cmp.g m (x,(conv.f2f pe 0.0:(F64)))))#(cmp.ge m (x, (conv.f2f pe 0.0:(F64))));

rrt

Reciprocal of the square root ( \(\textrm{rrt}(x) = \frac{1}{\sqrt{x}}\))

anx lam rrt (m: Nat) {pe: «2; Nat»} (x: F pe): F pe =

arith.div m (conv.f2f pe 1.0:(F64), rt.sq m x);

Operators

Bindings for the infix operators, which are sugar for an application of the escaped name. use the module whose math.mode matches the accuracy you are willing to trade:

Module	Mode
math.ops.none	math.mode.none
math.ops.finite	math.mode.finite
math.ops.unsafe	math.mode.unsafe
math.ops.fast	math.mode.fast

!= is math.cmp.une - the exact complement of == - and hence tt if an operand is a NaN.
All other comparisons are ordered and thus ff in that case.

pub mod ops {
    pub mod none {
        pub let `+  = arith.add mode.none;
        pub let `-  = arith.sub mode.none;
        pub let `*  = arith.mul mode.none;
        pub let `/  = arith.div mode.none;
        pub let `%  = arith.rem mode.none;
        pub let `== =   cmp.e   mode.none;
        pub let `!= =   cmp.une mode.none;
        pub let `<  =   cmp.l   mode.none;
        pub let `<= =   cmp.le  mode.none;
        pub let `>  =   cmp.g   mode.none;
        pub let `>= =   cmp.ge  mode.none;
    }
 
    pub mod finite {
        pub let `+  = arith.add mode.finite;
        pub let `-  = arith.sub mode.finite;
        pub let `*  = arith.mul mode.finite;
        pub let `/  = arith.div mode.finite;
        pub let `%  = arith.rem mode.finite;
        pub let `== =   cmp.e   mode.finite;
        pub let `!= =   cmp.une mode.finite;
        pub let `<  =   cmp.l   mode.finite;
        pub let `<= =   cmp.le  mode.finite;
        pub let `>  =   cmp.g   mode.finite;
        pub let `>= =   cmp.ge  mode.finite;
    }
 
    pub mod unsafe {
        pub let `+  = arith.add mode.unsafe;
        pub let `-  = arith.sub mode.unsafe;
        pub let `*  = arith.mul mode.unsafe;
        pub let `/  = arith.div mode.unsafe;
        pub let `%  = arith.rem mode.unsafe;
        pub let `== =   cmp.e   mode.unsafe;
        pub let `!= =   cmp.une mode.unsafe;
        pub let `<  =   cmp.l   mode.unsafe;
        pub let `<= =   cmp.le  mode.unsafe;
        pub let `>  =   cmp.g   mode.unsafe;
        pub let `>= =   cmp.ge  mode.unsafe;
    }
 
    pub mod fast {
        pub let `+  = arith.add mode.fast;
        pub let `-  = arith.sub mode.fast;
        pub let `*  = arith.mul mode.fast;
        pub let `/  = arith.div mode.fast;
        pub let `%  = arith.rem mode.fast;
        pub let `== =   cmp.e   mode.fast;
        pub let `!= =   cmp.une mode.fast;
        pub let `<  =   cmp.l   mode.fast;
        pub let `<= =   cmp.le  mode.fast;
        pub let `>  =   cmp.g   mode.fast;
        pub let `>= =   cmp.ge  mode.fast;
    }
}