#include "prelude/params.hats"
#if VERBOSE_PRELUDE #then
#print "Loading [float.sats] starts!\n"
#endif
typedef lint = int_long_t0ype
typedef ulint = uint_long_t0ype
typedef llint = int_long_long_t0ype
typedef ullint = uint_long_long_t0ype
abst@ype float_t0ype = $extype "ats_float_type"
stadef float = float_t0ype
abst@ype double_long_t0ype = $extype "ats_ldouble_type"
stadef ldouble = double_long_t0ype
fun int_of_float
(f: float):<> int = "atspre_int_of_float"
overload int_of with int_of_float
fun lint_of_float
(f: float):<> lint = "atspre_lint_of_float"
overload lint_of with lint_of_float
fun llint_of_float
(f: float):<> llint = "atspre_llint_of_float"
overload llint_of with llint_of_float
fun float_of_int
(i: int):<> float = "atspre_float_of_int"
overload float_of with float_of_int
fun float_of_uint
(u: uint):<> float = "atspre_float_of_uint"
overload float_of with float_of_uint
fun float_of_lint
(i: lint):<> float = "atspre_float_of_lint"
overload float_of with float_of_lint
fun float_of_ulint
(u: ulint):<> float = "atspre_float_of_ulint"
overload float_of with float_of_ulint
fun float_of_llint
(i: llint):<> float = "atspre_float_of_llint"
overload float_of with float_of_llint
fun float_of_ullint
(u: ullint):<> float = "atspre_float_of_ullint"
overload float_of with float_of_ullint
fun float_of_size
(sz: size_t):<> float = "atspre_float_of_size"
overload float_of with float_of_size
fun float_of_double
(d: double):<> float = "atspre_float_of_double"
overload float_of with float_of_double
fun float_of_string
(s: string):<> float = "atspre_float_of_string"
overload float_of with float_of_string
fun abs_float (f: float):<> float = "atspre_abs_float"
overload abs with abs_float
fun neg_float (f: float):<> float = "atspre_neg_float"
overload ~ with neg_float
fun succ_float (f: float):<> float = "atspre_succ_float"
and pred_float (f: float):<> float = "atspre_pred_float"
overload succ with succ_float
overload pred with pred_float
fun add_float_float (f1: float, f2: float):<> float
= "atspre_add_float_float"
and sub_float_float (f1: float, f2: float):<> float
= "atspre_sub_float_float"
overload + with add_float_float
overload - with sub_float_float
fun mul_float_float
(f1: float, f2: float):<> float = "atspre_mul_float_float"
and mul_int_float (i1: int, f2: float):<> float = "atspre_mul_int_float"
and mul_float_int (f1: float, i2: int):<> float = "atspre_mul_float_int"
overload * with mul_float_float
overload * with mul_int_float
overload * with mul_float_int
fun div_float_float
(f1: float, f2: float):<> float = "atspre_div_float_float"
and div_float_int (f1: float, i2: int):<> float = "atspre_div_float_int"
overload / with div_float_float
overload / with div_float_int
fun lt_float_float (f1: float, f2: float):<> bool
= "atspre_lt_float_float"
and lte_float_float (f1: float, f2: float):<> bool
= "atspre_lte_float_float"
overload < with lt_float_float
overload <= with lte_float_float
fun gt_float_float (f1: float, f2: float):<> bool
= "atspre_gt_float_float"
and gte_float_float (f1: float, f2: float):<> bool
= "atspre_gte_float_float"
overload > with gt_float_float
overload >= with gte_float_float
fun eq_float_float (f1: float, f2: float):<> bool
= "atspre_eq_float_float"
and neq_float_float (f1: float, f2: float):<> bool
= "atspre_neq_float_float"
overload = with eq_float_float
overload <> with neq_float_float
fun compare_float_float (f1: float, f2: float):<> Sgn
= "atspre_compare_float_float"
overload compare with compare_float_float
fun max_float_float (f1: float, f2: float):<> float
= "atspre_max_float_float"
and min_float_float (f1: float, f2: float):<> float
= "atspre_min_float_float"
overload max with max_float_float
overload min with min_float_float
fun square_float
(f: float):<> float = "atspre_square_float"
overload square with square_float
fun pow_float_int1 (f: float, n: Nat):<> float
overload pow with pow_float_int1
symintr fprint_float
fun fprint0_float (out: FILEref, x: float):<!exnref> void
= "atspre_fprint_float"
overload fprint_float with fprint0_float
fun fprint1_float {m:file_mode}
(pf: file_mode_lte (m, w) | out: &FILE m, x: float):<!exnref> void
= "atspre_fprint_float"
overload fprint_float with fprint1_float
overload fprint with fprint_float
fun print_float (f: float):<!ref> void = "atspre_print_float"
and prerr_float (f: float):<!ref> void = "atspre_prerr_float"
overload print with print_float
overload prerr with prerr_float
fun tostrptr_float
(f: float):<> strptr1 = "atspre_tostrptr_float"
overload tostrptr with tostrptr_float
fun tostring_float (f: float):<> string = "atspre_tostrptr_float"
overload tostring with tostring_float
fun int_of_double
(d: double):<> int = "atspre_int_of_double"
overload int_of with int_of_double
fun lint_of_double
(d: double):<> lint = "atspre_lint_of_double"
overload lint_of with lint_of_double
fun llint_of_double
(d: double):<> llint = "atspre_llint_of_double"
overload llint_of with llint_of_double
fun double_of_int
(i: int):<> double = "atspre_double_of_int"
overload double_of with double_of_int
fun double_of_uint
(u: uint):<> double = "atspre_double_of_uint"
overload double_of with double_of_uint
fun double_of_lint
(i: lint):<> double = "atspre_double_of_lint"
overload double_of with double_of_lint
fun double_of_ulint
(u: ulint):<> double = "atspre_double_of_ulint"
overload double_of with double_of_ulint
fun double_of_llint
(i: llint):<> double = "atspre_double_of_llint"
overload double_of with double_of_llint
fun double_of_ullint
(u: ullint):<> double = "atspre_double_of_ullint"
overload double_of with double_of_ullint
fun double_of_size
(sz: size_t):<> double = "atspre_double_of_size"
overload double_of with double_of_size
fun double_of_float (f: float):<> double
= "atspre_double_of_float"
overload double_of with double_of_float
fun double_of_string
(s: string):<> double = "atspre_double_of_string"
overload double_of with double_of_string
fun abs_double (d: double):<> double = "atspre_abs_double"
overload abs with abs_double
fun neg_double (d: double):<> double = "atspre_neg_double"
overload ~ with neg_double
fun succ_double (d: double):<> double = "atspre_succ_double"
and pred_double (d: double):<> double = "atspre_pred_double"
overload succ with succ_double
overload pred with pred_double
fun add_double_double
(d1: double, d2: double):<> double = "atspre_add_double_double"
and add_double_int (d1: double, i2: int):<> double = "atspre_add_double_int"
and add_int_double (i1: int, d2: double):<> double = "atspre_add_int_double"
overload + with add_double_double
overload + with add_double_int
overload + with add_int_double
fun sub_double_double
(d1: double, d2: double):<> double = "atspre_sub_double_double"
and sub_double_int (d1: double, i2: int):<> double = "atspre_sub_double_int"
and sub_int_double (i1: int, d2: double):<> double = "atspre_sub_int_double"
overload - with sub_double_double
overload - with sub_double_int
overload - with sub_int_double
fun mul_double_double
(d1: double, d2: double):<> double = "atspre_mul_double_double"
and mul_double_int (d1: double, i2: int):<> double = "atspre_mul_double_int"
and mul_int_double (i1: int, d2: double):<> double = "atspre_mul_int_double"
overload * with mul_double_double
overload * with mul_double_int
overload * with mul_int_double
fun div_double_double
(d1: double, d2: double):<> double = "atspre_div_double_double"
and div_double_int
(d1: double, i2: int):<> double = "atspre_div_double_int"
and div_int_double
(i1: int, d2: double):<> double = "atspre_div_int_double"
overload / with div_double_double
overload / with div_double_int
overload / with div_int_double
fun lt_double_double (d1: double, d2: double):<> bool
= "atspre_lt_double_double"
and lte_double_double (d1: double, d2: double):<> bool
= "atspre_lte_double_double"
overload < with lt_double_double
overload <= with lte_double_double
fun gt_double_double (d1: double, d2: double):<> bool
= "atspre_gt_double_double"
and gte_double_double (d1: double, d2: double):<> bool
= "atspre_gte_double_double"
overload > with gt_double_double
overload >= with gte_double_double
fun eq_double_double (d1: double, d2: double):<> bool
= "atspre_eq_double_double"
and neq_double_double (d1: double, d2: double):<> bool
= "atspre_neq_double_double"
overload = with eq_double_double
overload <> with neq_double_double
fun compare_double_double (d1: double, d2: double):<> Sgn
= "atspre_compare_double_double"
overload compare with compare_double_double
fun max_double_double (d1: double, d2: double):<> double
= "atspre_max_double_double"
and min_double_double (d1: double, d2: double):<> double
= "atspre_min_double_double"
overload max with max_double_double
overload min with min_double_double
fun square_double
(d: double):<> double = "atspre_square_double"
overload square with square_double
fun pow_double_int1 (d: double, n: Nat):<> double
overload pow with pow_double_int1
symintr fprint_double
fun fprint0_double (out: FILEref, x: double):<!exnref> void
= "atspre_fprint_double"
overload fprint_double with fprint0_double
fun fprint1_double {m:file_mode}
(pf: file_mode_lte (m, w) | out: &FILE m, x: double):<!exnref> void
= "atspre_fprint_double"
overload fprint_double with fprint1_double
overload fprint with fprint_double
fun print_double (f: double):<!ref> void = "atspre_print_double"
and prerr_double (f: double):<!ref> void = "atspre_prerr_double"
overload print with print_double
overload prerr with prerr_double
fun tostrptr_double
(d: double):<> strptr1 = "atspre_tostrptr_double"
overload tostrptr with tostrptr_double
fun tostring_double (d: double):<> string = "atspre_tostrptr_double"
overload tostring with tostring_double
fun int_of_ldouble
(ld: ldouble):<> int = "atspre_int_of_ldouble"
overload int_of with int_of_ldouble
fun lint_of_ldouble
(ld: ldouble):<> lint = "atspre_lint_of_ldouble"
overload lint_of with lint_of_ldouble
fun llint_of_ldouble
(ld: ldouble):<> llint = "atspre_llint_of_ldouble"
overload llint_of with llint_of_ldouble
fun ldouble_of_int
(i: int):<> ldouble = "atspre_ldouble_of_int"
overload ldouble_of with ldouble_of_int
fun ldouble_of_lint
(li: lint):<> ldouble = "atspre_ldouble_of_lint"
overload ldouble_of with ldouble_of_lint
fun ldouble_of_llint
(lli: llint):<> ldouble = "atspre_ldouble_of_llint"
overload ldouble_of with ldouble_of_llint
fun ldouble_of_float
(f: float):<> ldouble = "atspre_ldouble_of_float"
overload ldouble_of with ldouble_of_float
fun ldouble_of_double
(d: double):<> ldouble = "atspre_ldouble_of_double"
overload ldouble_of with ldouble_of_double
fun abs_ldouble
(ld: ldouble):<> ldouble = "atspre_abs_ldouble"
overload abs with abs_ldouble
fun neg_ldouble
(ld: ldouble):<> ldouble = "atspre_neg_ldouble"
overload ~ with neg_ldouble
fun succ_ldouble
(ld: ldouble):<> ldouble = "atspre_succ_ldouble"
and pred_ldouble
(ld: ldouble):<> ldouble = "atspre_pred_ldouble"
overload succ with succ_ldouble
overload pred with pred_ldouble
fun add_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_add_ldouble_ldouble"
and sub_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_sub_ldouble_ldouble"
overload + with add_ldouble_ldouble
overload - with sub_ldouble_ldouble
fun mul_ldouble_ldouble
(ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_mul_ldouble_ldouble"
and mul_int_ldouble (i1: int, ld2: ldouble):<> ldouble
= "atspre_mul_int_ldouble"
and mul_ldouble_int (ld1: ldouble, i2: int):<> ldouble
= "atspre_mul_ldouble_int"
overload * with mul_ldouble_ldouble
overload * with mul_int_ldouble
overload * with mul_ldouble_int
fun div_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_div_ldouble_ldouble"
and div_ldouble_int (ld1: ldouble, i2: int):<> ldouble
= "atspre_div_ldouble_int"
overload / with div_ldouble_ldouble
overload / with div_ldouble_int
fun lt_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_lt_ldouble_ldouble"
and lte_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_lte_ldouble_ldouble"
overload < with lt_ldouble_ldouble
overload <= with lte_ldouble_ldouble
fun gt_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_gt_ldouble_ldouble"
and gte_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_gte_ldouble_ldouble"
overload > with gt_ldouble_ldouble
overload >= with gte_ldouble_ldouble
fun eq_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_eq_ldouble_ldouble"
and neq_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> bool
= "atspre_neq_ldouble_ldouble"
overload = with eq_ldouble_ldouble
overload <> with neq_ldouble_ldouble
fun compare_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> Sgn
= "atspre_compare_ldouble_ldouble"
overload compare with compare_ldouble_ldouble
fun max_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_max_ldouble_ldouble"
and min_ldouble_ldouble (ld1: ldouble, ld2: ldouble):<> ldouble
= "atspre_min_ldouble_ldouble"
overload max with max_ldouble_ldouble
overload min with min_ldouble_ldouble
fun square_ldouble
(ld: ldouble):<> ldouble = "atspre_square_ldouble"
overload square with square_ldouble
fun pow_ldouble_int1 (ld: ldouble, n: Nat):<> ldouble
overload pow with pow_ldouble_int1
symintr fprint_ldouble
fun fprint0_ldouble (out: FILEref, x: ldouble):<!exnref> void
= "atspre_fprint_ldouble"
overload fprint_ldouble with fprint0_ldouble
fun fprint1_ldouble {m:file_mode}
(pf: file_mode_lte (m, w) | out: &FILE m, x: ldouble):<!exnref> void
= "atspre_fprint_ldouble"
overload fprint_ldouble with fprint1_ldouble
overload fprint with fprint_ldouble
fun print_ldouble (ld: ldouble):<!ref> void = "atspre_print_ldouble"
and prerr_ldouble (ld: ldouble):<!ref> void = "atspre_prerr_ldouble"
overload print with print_ldouble
overload prerr with prerr_ldouble
fun tostrptr_ldouble
(ld: ldouble):<> strptr1 = "atspre_tostrptr_ldouble"
overload tostrptr with tostrptr_ldouble
fun tostring_ldouble (ld: ldouble):<> string = "atspre_tostrptr_ldouble"
overload tostring with tostring_ldouble
#if VERBOSE_PRELUDE #then
#print "Loading [float.sats] finishes!\n"
#endif