#line 6 "/home/ubuntu/felix/src/packages/reals.fdoc"
instance[t in numbers] FloatAddgrp[t] {
fun zero: unit -> t = "(?1)0" ;
fun + : t * t -> t = "$1+$2" ;
fun neg : t -> t = "-$1" ;
fun - : t * t -> t = "$1-$2" ;
proc += : &t * t = "*$1+=$2;";
proc -= : &t * t = "*$1-=$2;";
}
instance[t in numbers] FloatMultSemi1[t] {
fun one: unit -> t = "(?1)1";
fun * : t * t -> t = "$1*$2";
proc *= : &t * t = "*$1*=$2;";
}
instance[t in numbers] FloatRing[t] {}
instance[t in ints \(\cup\) complexes] FloatDring[t] {
fun / : t * t -> t = "$1/$2";
fun % : t * t -> t = "$1%$2";
proc /= : &t * t = "*$1/=$2;";
proc %= : &t * t = "*$1%=$2;";
}
instance[t in floats] FloatDring[t] {
fun / : t * t -> t = "$1/$2";
fun % : t * t -> t = "fmod($1,$2)";
proc /= : &t * t = "*$1/=$2;";
proc %= : &t * t = "*$1=fmod($1,$2);";
}
instance[t in floats] Real[t] {
requires Cxx_headers::cmath;
fun abs: t -> t = "::std::abs($1)";
fun log10: t -> t = "::std::log10($1)";
fun sqrt: t -> t = "::std::sqrt($1)";
fun ceil: t -> t = "::std::ceil($1)";
fun floor: t -> t = "::std::floor($1)";
fun trunc: t -> t = "::std::trunc($1)";
fun embed: int -> t = "(?1)($1)";
fun atan2: t * t -> t = "::std::atan2($1,$2)";
}
#line 49 "/home/ubuntu/felix/src/packages/reals.fdoc"
open class Floatinf
{
const FINFINITY : float = "INFINITY" requires C99_headers::math_h;
}
open class Doubleinf
{
const DINFINITY : double = "(double)INFINITY" requires C99_headers::math_h;
}
open class Ldoubleinf
{
const LINFINITY : ldouble = "(long double)INFINITY" requires C99_headers::math_h;
}
fun isinf[T in reals] : T -> bool = "::std::isinf($1)" requires Cxx_headers::cmath;
fun isfinite[T in reals] : T -> bool = "::std::isfinite($1)" requires Cxx_headers::cmath;
fun isnan[T in reals] : T -> bool = "::std::isnan($1)" requires Cxx_headers::cmath;
ctor[T in ints] float : T = "(float)($1)";
ctor[T in ints] double : T = "(double)($1)";
ctor[T in ints] ldouble : T = "(long double)($1)";
ctor float : double = "(float)($1)";
ctor double: float= "(double)($1)";
ctor float : string = "::std::stof($1)";
ctor double : string = "::std::stod($1)";
ctor ldouble : string = "::std::stold($1)";
open Real[float];
open Real[double];
open Real[ldouble];
#line 90 "/home/ubuntu/felix/src/packages/reals.fdoc"
instance[t in reals] Tord[t] {
fun < : t * t -> bool = "$1<$2";
}