(***********************************************************************) (* *) (* Applied Type System *) (* *) (* Hongwei Xi *) (* *) (***********************************************************************) (* ** ATS - Unleashing the Potential of Types! ** ** Copyright (C) 2002-2008 Hongwei Xi, Boston University ** ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU LESSER GENERAL PUBLIC LICENSE as published by the ** Free Software Foundation; either version 2.1, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* author: Hongwei Xi (hwxi AT cs DOT bu DOT edu) *) (* ****** ****** *) #include "prelude/params.hats" (* ****** ****** *) #if VERBOSE_PRELUDE #then #print "Loading [integer_fixed.sats] starts!\n" #endif // end of [VERBOSE_PRELUDE] (* ****** ****** *) // signed and unsigned integers with fixed size (* ****** ****** *) typedef int8 = int8_t0ype fun int8_of_int (i: int):<> int8 = "atspre_int8_of_int" fun int_of_int8 (i: int8):<> int = "atspre_int_of_int8" // ------ ------ fun abs_int8 (i: int8):<> int8 = "atspre_abs_int8" overload abs with abs_int8 fun neg_int8 (i: int8):<> int8 = "atspre_neg_int8" overload ~ with neg_int8 fun succ_int8 (i: int8):<> int8 = "atspre_succ_int8" and pred_int8 (i: int8):<> int8 = "atspre_pred_int8" overload succ with succ_int8 overload pred with pred_int8 fun add_int8_int8 (i: int8, j: int8):<> int8 = "atspre_add_int8_int8" and sub_int8_int8 (i: int8, j: int8):<> int8 = "atspre_sub_int8_int8" and mul_int8_int8 (i: int8, j: int8):<> int8 = "atspre_mul_int8_int8" and div_int8_int8 (i: int8, j: int8):<> int8 = "atspre_div_int8_int8" and mod_int8_int8 (i: int8, j: int8):<> int8 = "atspre_mod_int8_int8" overload + with add_int8_int8 overload - with sub_int8_int8 overload * with mul_int8_int8 overload / with div_int8_int8 overload mod with mod_int8_int8 fun lt_int8_int8 (i: int8, j: int8):<> bool = "atspre_lt_int8_int8" and lte_int8_int8 (i: int8, j: int8):<> bool = "atspre_lte_int8_int8" fun gt_int8_int8 (i: int8, j: int8):<> bool = "atspre_gt_int8_int8" and gte_int8_int8 (i: int8, j: int8):<> bool = "atspre_gte_int8_int8" fun eq_int8_int8 (i: int8, j: int8):<> bool = "atspre_eq_int8_int8" and neq_int8_int8 (i: int8, j: int8):<> bool = "atspre_neq_int8_int8" overload < with lt_int8_int8 overload <= with lte_int8_int8 overload > with gt_int8_int8 overload >= with gte_int8_int8 overload = with eq_int8_int8 overload <> with neq_int8_int8 fun max_int8_int8 (i: int8, j: int8):<> int8 = "atspre_max_int8_int8" and min_int8_int8 (i: int8, j: int8):<> int8 = "atspre_min_int8_int8" overload max with max_int8_int8 overload min with min_int8_int8 (* ****** ****** *) symintr fprint_int8 fun fprint0_int8 (out: FILEref, x: int8): void = "atspre_fprint_int8" overload fprint_int8 with fprint0_int8 fun fprint1_int8 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: int8): void = "atspre_fprint_int8" overload fprint_int8 with fprint1_int8 overload fprint with fprint_int8 fun print_int8 (i: int8): void = "atspre_print_int8" and prerr_int8 (i: int8): void = "atspre_prerr_int8" overload print with print_int8 overload prerr with prerr_int8 (* ****** ****** *) typedef uint8 = uint8_t0ype fun uint8_of_uint (i: uint):<> uint8 = "atspre_uint8_of_uint" fun uint_of_uint8 (i: uint8):<> uint = "atspre_uint_of_uint8" // ------ ------ fun succ_uint8 (i: uint8):<> uint8 = "atspre_succ_uint8" and pred_uint8 (i: uint8):<> uint8 = "atspre_pred_uint8" overload succ with succ_uint8 overload pred with pred_uint8 fun add_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_add_uint8_uint8" and sub_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_sub_uint8_uint8" and mul_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_mul_uint8_uint8" and div_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_div_uint8_uint8" and mod_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_mod_uint8_uint8" overload + with add_uint8_uint8 overload - with sub_uint8_uint8 overload * with mul_uint8_uint8 overload / with div_uint8_uint8 overload mod with mod_uint8_uint8 fun lt_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_lt_uint8_uint8" and lte_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_lte_uint8_uint8" fun gt_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_gt_uint8_uint8" and gte_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_gte_uint8_uint8" fun eq_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_eq_uint8_uint8" and neq_uint8_uint8 (i: uint8, j: uint8):<> bool = "atspre_neq_uint8_uint8" overload < with lt_uint8_uint8 overload <= with lte_uint8_uint8 overload > with gt_uint8_uint8 overload >= with gte_uint8_uint8 overload = with eq_uint8_uint8 overload <> with neq_uint8_uint8 fun max_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_max_uint8_uint8" and min_uint8_uint8 (i: uint8, j: uint8):<> uint8 = "atspre_min_uint8_uint8" overload max with max_uint8_uint8 overload min with min_uint8_uint8 (* ****** ****** *) symintr fprint_uint8 fun fprint0_uint8 (out: FILEref, x: uint8): void = "atspre_fprint_uint8" overload fprint_uint8 with fprint0_uint8 fun fprint1_uint8 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: uint8): void = "atspre_fprint_uint8" overload fprint_uint8 with fprint1_uint8 overload fprint with fprint_uint8 fun print_uint8 (i: uint8): void = "atspre_print_uint8" and prerr_uint8 (i: uint8): void = "atspre_prerr_uint8" overload print with print_uint8 overload prerr with prerr_uint8 (* ****** ****** *) // signed integer of size 16bit typedef int16 = int16_t0ype fun int16_of_int (i: int):<> int16 = "atspre_int16_of_int" fun int_of_int16 (i: int16):<> int = "atspre_int_of_int16" // ------ ------ fun abs_int16 (i: int16):<> int16 = "atspre_abs_int16" overload abs with abs_int16 fun neg_int16 (i: int16):<> int16 = "atspre_neg_int16" overload ~ with neg_int16 fun succ_int16 (i: int16):<> int16 = "atspre_succ_int16" and pred_int16 (i: int16):<> int16 = "atspre_pred_int16" overload succ with succ_int16 overload pred with pred_int16 fun add_int16_int16 (i: int16, j: int16):<> int16 = "atspre_add_int16_int16" and sub_int16_int16 (i: int16, j: int16):<> int16 = "atspre_sub_int16_int16" and mul_int16_int16 (i: int16, j: int16):<> int16 = "atspre_mul_int16_int16" and div_int16_int16 (i: int16, j: int16):<> int16 = "atspre_div_int16_int16" and mod_int16_int16 (i: int16, j: int16):<> int16 = "atspre_mod_int16_int16" overload + with add_int16_int16 overload - with sub_int16_int16 overload * with mul_int16_int16 overload / with div_int16_int16 overload mod with mod_int16_int16 fun lt_int16_int16 (i: int16, j: int16):<> bool = "atspre_lt_int16_int16" and lte_int16_int16 (i: int16, j: int16):<> bool = "atspre_lte_int16_int16" fun gt_int16_int16 (i: int16, j: int16):<> bool = "atspre_gt_int16_int16" and gte_int16_int16 (i: int16, j: int16):<> bool = "atspre_gte_int16_int16" fun eq_int16_int16 (i: int16, j: int16):<> bool = "atspre_eq_int16_int16" and neq_int16_int16 (i: int16, j: int16):<> bool = "atspre_neq_int16_int16" overload < with lt_int16_int16 overload <= with lte_int16_int16 overload > with gt_int16_int16 overload >= with gte_int16_int16 overload = with eq_int16_int16 overload <> with neq_int16_int16 fun max_int16_int16 (i: int16, j: int16):<> int16 = "atspre_max_int16_int16" and min_int16_int16 (i: int16, j: int16):<> int16 = "atspre_min_int16_int16" overload max with max_int16_int16 overload min with min_int16_int16 (* ****** ****** *) symintr fprint_int16 fun fprint0_int16 (out: FILEref, x: int16): void = "atspre_fprint_int16" overload fprint_int16 with fprint0_int16 fun fprint1_int16 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: int16): void = "atspre_fprint_int16" overload fprint_int16 with fprint1_int16 overload fprint with fprint_int16 fun print_int16 (i: int16): void = "atspre_print_int16" and prerr_int16 (i: int16): void = "atspre_prerr_int16" overload print with print_int16 overload prerr with prerr_int16 (* ****** ****** *) // unsigned integer of size 16bit typedef uint16 = uint16_t0ype fun uint16_of_int (i: int):<> uint16 = "atspre_uint16_of_int" fun int_of_uint16 (u: uint16):<> int = "atspre_int_of_uint16" fun uint16_of_uint (i: uint):<> uint16 = "atspre_uint16_of_uint" fun uint_of_uint16 (i: uint16):<> uint = "atspre_uint_of_uint16" // ------ ------ fun succ_uint16 (i: uint16):<> uint16 = "atspre_succ_uint16" and pred_uint16 (i: uint16):<> uint16 = "atspre_pred_uint16" overload succ with succ_uint16 overload pred with pred_uint16 fun add_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_add_uint16_uint16" and sub_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_sub_uint16_uint16" and mul_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_mul_uint16_uint16" and div_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_div_uint16_uint16" and mod_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_mod_uint16_uint16" overload + with add_uint16_uint16 overload - with sub_uint16_uint16 overload * with mul_uint16_uint16 overload / with div_uint16_uint16 overload mod with mod_uint16_uint16 fun lt_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_lt_uint16_uint16" and lte_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_lte_uint16_uint16" fun gt_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_gt_uint16_uint16" and gte_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_gte_uint16_uint16" fun eq_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_eq_uint16_uint16" and neq_uint16_uint16 (i: uint16, j: uint16):<> bool = "atspre_neq_uint16_uint16" overload < with lt_uint16_uint16 overload <= with lte_uint16_uint16 overload > with gt_uint16_uint16 overload >= with gte_uint16_uint16 overload = with eq_uint16_uint16 overload <> with neq_uint16_uint16 fun max_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_max_uint16_uint16" and min_uint16_uint16 (i: uint16, j: uint16):<> uint16 = "atspre_min_uint16_uint16" overload max with max_uint16_uint16 overload min with min_uint16_uint16 (* ****** ****** *) symintr fprint_uint16 fun fprint0_uint16 (out: FILEref, x: uint16): void = "atspre_fprint_uint16" overload fprint_uint16 with fprint0_uint16 fun fprint1_uint16 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: uint16): void = "atspre_fprint_uint16" overload fprint_uint16 with fprint1_uint16 overload fprint with fprint_uint16 fun print_uint16 (i: uint16): void = "atspre_print_uint16" and prerr_uint16 (i: uint16): void = "atspre_prerr_uint16" overload print with print_uint16 overload prerr with prerr_uint16 (* ****** ****** *) // signed integer of size 32bit typedef int32 = int32_t0ype fun int32_of_int (i: int):<> int32 = "atspre_int32_of_int" fun int_of_int32 (i: int32):<> int = "atspre_int_of_int32" // ------ ------ fun abs_int32 (i: int32):<> int32 = "atspre_abs_int32" overload abs with abs_int32 fun neg_int32 (i: int32):<> int32 = "atspre_neg_int32" overload ~ with neg_int32 fun succ_int32 (i: int32):<> int32 = "atspre_succ_int32" and pred_int32 (i: int32):<> int32 = "atspre_pred_int32" overload succ with succ_int32 overload pred with pred_int32 fun add_int32_int32 (i: int32, j: int32):<> int32 = "atspre_add_int32_int32" and sub_int32_int32 (i: int32, j: int32):<> int32 = "atspre_sub_int32_int32" and mul_int32_int32 (i: int32, j: int32):<> int32 = "atspre_mul_int32_int32" and div_int32_int32 (i: int32, j: int32):<> int32 = "atspre_div_int32_int32" and mod_int32_int32 (i: int32, j: int32):<> int32 = "atspre_mod_int32_int32" overload + with add_int32_int32 overload - with sub_int32_int32 overload * with mul_int32_int32 overload / with div_int32_int32 overload mod with mod_int32_int32 fun lt_int32_int32 (i: int32, j: int32):<> bool = "atspre_lt_int32_int32" and lte_int32_int32 (i: int32, j: int32):<> bool = "atspre_lte_int32_int32" fun gt_int32_int32 (i: int32, j: int32):<> bool = "atspre_gt_int32_int32" and gte_int32_int32 (i: int32, j: int32):<> bool = "atspre_gte_int32_int32" fun eq_int32_int32 (i: int32, j: int32):<> bool = "atspre_eq_int32_int32" and neq_int32_int32 (i: int32, j: int32):<> bool = "atspre_neq_int32_int32" overload < with lt_int32_int32 overload <= with lte_int32_int32 overload > with gt_int32_int32 overload >= with gte_int32_int32 overload = with eq_int32_int32 overload <> with neq_int32_int32 fun compare_int32_int32 (i1: int32, i2: int32):<> Sgn = "atspre_compare_int32_int32" overload compare with compare_int32_int32 fun max_int32_int32 (i: int32, j: int32):<> int32 = "atspre_max_int32_int32" and min_int32_int32 (i: int32, j: int32):<> int32 = "atspre_min_int32_int32" overload max with max_int32_int32 overload min with min_int32_int32 (* ****** ****** *) symintr fprint_int32 fun fprint0_int32 (out: FILEref, x: int32): void = "atspre_fprint_int32" overload fprint_int32 with fprint0_int32 fun fprint1_int32 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: int32): void = "atspre_fprint_int32" overload fprint_int32 with fprint1_int32 overload fprint with fprint_int32 fun print_int32 (i: int32): void = "atspre_print_int32" and prerr_int32 (i: int32): void = "atspre_prerr_int32" overload print with print_int32 overload prerr with prerr_int32 (* ****** ****** *) // // stringization // fun tostrptr_int32 (i: int32):<> strptr1 = "atspre_tostrptr_int32" overload tostrptr with tostrptr_int32 fun tostring_int32 (i: int32):<> string = "atspre_tostrptr_int32" overload tostring with tostring_int32 (* ****** ****** *) // unsigned integer of size 32bit typedef uint32 = uint32_t0ype fun uint32_of_uint (i: uint):<> uint32 = "atspre_uint32_of_uint" fun uint_of_uint32 (i: uint32):<> uint = "atspre_uint_of_uint32" // ------ ------ fun succ_uint32 (i: uint32):<> uint32 = "atspre_succ_uint32" and pred_uint32 (i: uint32):<> uint32 = "atspre_pred_uint32" overload succ with succ_uint32 overload pred with pred_uint32 fun add_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_add_uint32_uint32" and sub_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_sub_uint32_uint32" and mul_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_mul_uint32_uint32" and div_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_div_uint32_uint32" and mod_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_mod_uint32_uint32" overload + with add_uint32_uint32 overload - with sub_uint32_uint32 overload * with mul_uint32_uint32 overload / with div_uint32_uint32 overload mod with mod_uint32_uint32 fun lt_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_lt_uint32_uint32" and lte_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_lte_uint32_uint32" fun gt_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_gt_uint32_uint32" and gte_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_gte_uint32_uint32" fun eq_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_eq_uint32_uint32" and neq_uint32_uint32 (i: uint32, j: uint32):<> bool = "atspre_neq_uint32_uint32" overload < with lt_uint32_uint32 overload <= with lte_uint32_uint32 overload > with gt_uint32_uint32 overload >= with gte_uint32_uint32 overload = with eq_uint32_uint32 overload <> with neq_uint32_uint32 fun max_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_max_uint32_uint32" and min_uint32_uint32 (i: uint32, j: uint32):<> uint32 = "atspre_min_uint32_uint32" overload max with max_uint32_uint32 overload min with min_uint32_uint32 (* ****** ****** *) symintr fprint_uint32 fun fprint0_uint32 (out: FILEref, x: uint32): void = "atspre_fprint_uint32" overload fprint_uint32 with fprint0_uint32 fun fprint1_uint32 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: uint32): void = "atspre_fprint_uint32" overload fprint_uint32 with fprint1_uint32 overload fprint with fprint_uint32 fun print_uint32 (i: uint32): void = "atspre_print_uint32" and prerr_uint32 (i: uint32): void = "atspre_prerr_uint32" overload print with print_uint32 overload prerr with prerr_uint32 (* ****** ****** *) // signed integer of size 64bit typedef int64 = int64_t0ype symintr int64_of fun int64_of_int (i: int):<> int64 = "atspre_int64_of_int" overload int64_of with int64_of_int fun int64_of_lint (i: lint):<> int64 = "atspre_int64_of_lint" overload int64_of with int64_of_lint fun int64_of_llint (i: llint):<> int64 = "atspre_int64_of_llint" overload int64_of with int64_of_llint fun int_of_int64 (i: int64):<> int = "atspre_int_of_int64" // ------ ------ fun abs_int64 (i: int64):<> int64 = "atspre_abs_int64" overload abs with abs_int64 fun neg_int64 (i: int64):<> int64 = "atspre_neg_int64" overload ~ with neg_int64 fun succ_int64 (i: int64):<> int64 = "atspre_succ_int64" and pred_int64 (i: int64):<> int64 = "atspre_pred_int64" overload succ with succ_int64 overload pred with pred_int64 fun add_int64_int64 (i: int64, j: int64):<> int64 = "atspre_add_int64_int64" and sub_int64_int64 (i: int64, j: int64):<> int64 = "atspre_sub_int64_int64" and mul_int64_int64 (i: int64, j: int64):<> int64 = "atspre_mul_int64_int64" and div_int64_int64 (i: int64, j: int64):<> int64 = "atspre_div_int64_int64" and mod_int64_int64 (i: int64, j: int64):<> int64 = "atspre_mod_int64_int64" overload + with add_int64_int64 overload - with sub_int64_int64 overload * with mul_int64_int64 overload / with div_int64_int64 overload mod with mod_int64_int64 fun lt_int64_int64 (i: int64, j: int64):<> bool = "atspre_lt_int64_int64" and lte_int64_int64 (i: int64, j: int64):<> bool = "atspre_lte_int64_int64" fun gt_int64_int64 (i: int64, j: int64):<> bool = "atspre_gt_int64_int64" and gte_int64_int64 (i: int64, j: int64):<> bool = "atspre_gte_int64_int64" fun eq_int64_int64 (i: int64, j: int64):<> bool = "atspre_eq_int64_int64" and neq_int64_int64 (i: int64, j: int64):<> bool = "atspre_neq_int64_int64" overload < with lt_int64_int64 overload <= with lte_int64_int64 overload > with gt_int64_int64 overload >= with gte_int64_int64 overload = with eq_int64_int64 overload <> with neq_int64_int64 fun compare_int64_int64 (i1: int64, i2: int64):<> Sgn = "atspre_compare_int64_int64" overload compare with compare_int64_int64 fun max_int64_int64 (i: int64, j: int64):<> int64 = "atspre_max_int64_int64" and min_int64_int64 (i: int64, j: int64):<> int64 = "atspre_min_int64_int64" overload max with max_int64_int64 overload min with min_int64_int64 (* ****** ****** *) symintr fprint_int64 fun fprint0_int64 (out: FILEref, x: int64): void = "atspre_fprint_int64" overload fprint_int64 with fprint0_int64 fun fprint1_int64 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: int64): void = "atspre_fprint_int64" overload fprint_int64 with fprint1_int64 overload fprint with fprint_int64 fun print_int64 (i: int64): void = "atspre_print_int64" and prerr_int64 (i: int64): void = "atspre_prerr_int64" overload print with print_int64 overload prerr with prerr_int64 (* ****** ****** *) // // stringization // fun tostrptr_int64 (i: int64):<> strptr1 = "atspre_tostrptr_int64" overload tostrptr with tostrptr_int64 fun tostring_int64 (i: int64):<> string = "atspre_tostrptr_int64" overload tostring with tostring_int64 (* ****** ****** *) // unsigned integer of size 64bit typedef uint64 = uint64_t0ype symintr uint64_of fun uint64_of_int1 {i:nat} (i: int i):<> uint64 = "atspre_uint64_of_int1" overload uint64_of with uint64_of_int1 fun uint64_of_uint (i: uint):<> uint64 = "atspre_uint64_of_uint" overload uint64_of with uint64_of_uint fun uint64_of_ulint (i: ulint):<> uint64 = "atspre_uint64_of_ulint" overload uint64_of with uint64_of_ulint fun uint64_of_ullint (i: ullint):<> uint64 = "atspre_uint64_of_ullint" overload uint64_of with uint64_of_ullint fun uint_of_uint64 (i: uint64):<> uint = "atspre_uint_of_uint64" // ------ ------ fun succ_uint64 (i: uint64):<> uint64 = "atspre_succ_uint64" and pred_uint64 (i: uint64):<> uint64 = "atspre_pred_uint64" overload succ with succ_uint64 overload pred with pred_uint64 fun add_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_add_uint64_uint64" and sub_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_sub_uint64_uint64" and mul_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_mul_uint64_uint64" and div_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_div_uint64_uint64" and mod_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_mod_uint64_uint64" overload + with add_uint64_uint64 overload - with sub_uint64_uint64 overload * with mul_uint64_uint64 overload / with div_uint64_uint64 overload mod with mod_uint64_uint64 fun lt_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_lt_uint64_uint64" and lte_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_lte_uint64_uint64" fun gt_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_gt_uint64_uint64" and gte_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_gte_uint64_uint64" fun eq_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_eq_uint64_uint64" and neq_uint64_uint64 (i: uint64, j: uint64):<> bool = "atspre_neq_uint64_uint64" overload < with lt_uint64_uint64 overload <= with lte_uint64_uint64 overload > with gt_uint64_uint64 overload >= with gte_uint64_uint64 overload = with eq_uint64_uint64 overload <> with neq_uint64_uint64 fun max_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_max_uint64_uint64" and min_uint64_uint64 (i: uint64, j: uint64):<> uint64 = "atspre_min_uint64_uint64" overload max with max_uint64_uint64 overload min with min_uint64_uint64 (* ****** ****** *) symintr fprint_uint64 fun fprint0_uint64 (out: FILEref, x: uint64): void = "atspre_fprint_uint64" overload fprint_uint64 with fprint0_uint64 fun fprint1_uint64 {m:file_mode} (pf: file_mode_lte (m, w) | out: &FILE m, x: uint64): void = "atspre_fprint_uint64" overload fprint_uint64 with fprint1_uint64 overload fprint with fprint_uint64 fun print_uint64 (i: uint64): void = "atspre_print_uint64" and prerr_uint64 (i: uint64): void = "atspre_prerr_uint64" overload print with print_uint64 overload prerr with prerr_uint64 (* ****** ****** *) #if VERBOSE_PRELUDE #then #print "Loading [integer_fixed.sats] finishes!\n" #endif // end of [VERBOSE_PRELUDE] (* end of [integer_fixed.sats] *)