ATSLIB/prelude/integer

This package contains common functions on signed and unsigned integers of various finite precision.

g0int2int

g1int2int

g1ofg0_int

g0int2int

Synopsis

fun
{k1
,k2:tk}
g0int2int(x: g0int(k1)):<> g0int(k2)

g1int2int

Synopsis

fun{
k1,k2:tk
} g1int2int // i2i
  {i:int} (x: g1int (k1, i)):<> g1int (k2, i)

fun{
k1,k2:tk
} g1int2int : g1int2int_type(k1, k2)

g1ofg0_int

Synopsis

castfn
g1ofg0_int{tk:tk}(g0int(tk)):<> g1int(tk)

Description

This cast function is called to assign a dependent (or indexed) type to an integer of a non-dependent (or un-indexed) type. It is for signed integers.

g0string2int

Synopsis

fun{tk:tk}
g0string2int(rep: NSH(string)):<> g0int(tk)

Description

Given a string representation of an integer, this function, which is based on the function atoi in libc, returns the value of the integer.

g1int_get_index

Synopsis

prfun
g1int_get_index
  {tk:tk}{i1:int}
  (x: g1int(tk, i1)): [i2:int] EQINT(i1, i2)

g0int_neg

Synopsis

fun
{tk:tk}
g0int_neg : g0int_uop_type(tk)

g1int_neg

Synopsis

fun
{tk:tk}
g1int_neg : g1int_neg_type(tk)

g0int_succ

Synopsis

fun
{tk:tk}
g0int_succ : g0int_uop_type(tk)

g1int_succ

Synopsis

fun{tk:tk}
g1int_succ : g1int_succ_type(tk)

g0int_pred

Synopsis

fun
{tk:tk}
g0int_pred : g0int_uop_type(tk)

g1int_pred

Synopsis

fun{tk:tk}
g1int_pred : g1int_pred_type(tk)

g0int_add

Synopsis

fun
{tk:tk}
g0int_add : g0int_aop_type(tk)

g1int_add

Synopsis

fun
{tk:tk}
g1int_add : g1int_add_type(tk)

g0int_sub

Synopsis

fun
{tk:tk}
g0int_sub : g0int_aop_type(tk)

g1int_sub

Synopsis

fun
{tk:tk}
g1int_sub : g1int_sub_type(tk)

g0int_mul

Synopsis

fun
{tk:tk}
g0int_mul : g0int_aop_type(tk)

g1int_mul

Synopsis

fun
{tk:tk}
g1int_mul : g1int_mul_type(tk)

g1int_mul2

Synopsis

fun
{tk:tk}
g1int_mul2
  {i,j:int}
(
  x: g1int (tk, i)
, y: g1int (tk, j)
) :<> [ij:int]
  (MUL (i, j, ij) | g1int (tk, ij))

g0int_div

Synopsis

fun
{tk:tk}
g0int_div : g0int_aop_type(tk)

g1int_div

Synopsis

fun
{tk:tk}
g1int_div : g1int_div_type(tk)

g1int_ndiv

Synopsis

fun
{tk:tk}
g1int_ndiv : g1int_ndiv_type(tk)

g1int_ndiv2

Synopsis

fun
{tk:tk}
g1int_ndiv2
  {i,j:int | i >= 0; j > 0}
(
  x: g1int(tk, i), y: g1int(tk, j)
) :<>
[
  q,r:int | 0 <= r; r < j
] (
  DIVMOD (i, j, q, r) | g1int (tk, q)
) (* end of [g1int_ndiv2] *)

g0int_mod

Synopsis

fun
{tk:tk}
g0int_mod : g0int_aop_type(tk)

g1int_mod

Synopsis

Synopsis for [g1int_mod] is unavailable.

g1int_nmod

Synopsis

fun{tk:tk}
g1int_nmod : g1int_nmod_type(tk)

g1int_nmod2

Synopsis

fun{tk:tk}
g1int_nmod2
  {i,j:int | i >= 0; j > 0}
(
  x: g1int(tk, i), y: g1int(tk, j)
) :<> [q,r:nat | r < j]
(
  DIVMOD(i, j, q, r) | g1int(tk, r)
) (* end of [g1int_nmod2] *)

g0int_gcd

Synopsis

Synopsis for [g0int_gcd] is unavailable.

g1int_gcd

Synopsis

Synopsis for [g1int_gcd] is unavailable.

g1int_ngcd

Synopsis

Synopsis for [g1int_ngcd] is unavailable.

g1int_ngcd2

Synopsis

Synopsis for [g1int_ngcd2] is unavailable.

g0int_lt

Synopsis

fun
{tk:tk}
g0int_lt : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is less than its second argument. It is for signed integers.

g1int_lt

Synopsis

fun{tk:tk}
g1int_lt : g1int_lt_type(tk)

Description

This function does the same as g0int_lt but is assigned a more informative dependent type.

g0int_lte

Synopsis

fun
{tk:tk}
g0int_lte : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is less than or equal to its second argument. It is for signed integers.

g1int_lte

Synopsis

fun{tk:tk}
g1int_lte : g1int_lte_type(tk)

Description

This function does the same as g0int_lte but is assigned a more informative dependent type.

g0int_gt

Synopsis

fun
{tk:tk}
g0int_gt : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is greater than its second argument. It is for signed integers.

g1int_gt

Synopsis

fun
{tk:tk}
g1int_gt : g1int_gt_type(tk)

Description

This function does the same as g0int_gt but is assigned a more informative dependent type.

g0int_gte

Synopsis

fun
{tk:tk}
g0int_gte : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is greater than or equal to its second argument. It is for signed integers.

g1int_gte

Synopsis

fun
{tk:tk}
g1int_gte : g1int_gte_type(tk)

Description

This function does the same as g0int_gte but is assigned a more informative dependent type.

g0int_eq

Synopsis

fun
{tk:tk}
g0int_eq : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is equal to its second argument. It is for signed integers.

g1int_eq

Synopsis

fun
{tk:tk}
g1int_eq : g1int_eq_type(tk)

Description

This function does the same as g0int_eq but is assigned a more informative dependent type.

g0int_neq

Synopsis

fun
{tk:tk}
g0int_neq : g0int_cmp_type(tk)

Description

This function returns true if and only if its first argument is unequal to its second argument. It is for signed integers.

g1int_neq

Synopsis

fun
{tk:tk}
g1int_neq : g1int_neq_type(tk)

Description

This function does the same as g0int_neq but is assigned a more informative dependent type.

g0int_compare

Synopsis

fun{tk:tk}
g0int_compare
  (x: g0int(tk), y: g0int(tk)):<> int

Description

This function returns -1, 0, and 1 if its first argument is less than, equal to, and greater than its second argument, respectively. It is for signed integers.

g1int_compare

Synopsis

fun{tk:tk}
g1int_compare : g1int_compare_type(tk)

Description

This function does the same as g0int_compare but is assigned a more informative dependent type.

g0int_max

Synopsis

fun
{tk:tk}
g0int_max : g0int_aop_type(tk)

Description

This function returns the maximum of its two arguments. It is for signed integers.

g1int_max

Synopsis

fun
{tk:tk}
g1int_max : g1int_max_type(tk)

Description

This function does the same as g0int_max but is assigned a more informative dependent type.

g0int_min

Synopsis

fun
{tk:tk}
g0int_min : g0int_aop_type(tk)

Description

This function returns the minimum of its two arguments. It is for signed integers.

g1int_min

Synopsis

fun
{tk:tk}
g1int_min : g1int_min_type(tk)

Description

This function does the same as g0int_min but is assigned a more informative dependent type.

fprint_int

Synopsis

fun fprint_int : fprint_type (int) = "mac#%"

fprint_lint

Synopsis

Synopsis for [fprint_lint] is unavailable.

fprint_llint

Synopsis

Synopsis for [fprint_llint] is unavailable.

fprint_ssize

Synopsis

Synopsis for [fprint_ssize] is unavailable.

g0int2uint

Synopsis

fun{
k1,k2:tk
} g0int2uint(g0int(k1)):<> g0uint(k2)

g0uint2int

Synopsis

fun{
k1,k2:tk
} g0uint2int(g0uint(k1)):<> g0int(k2)

g0uint2uint

Synopsis

fun{
k1,k2:tk
} g0uint2uint(g0uint(k1)):<> g0uint(k2)

g1int2uint

Synopsis

fun{
k1,k2:tk
} g1int2uint : g1int2uint_type(k1, k2)

g1uint2int

Synopsis

fun{
k1,k2:tk
} g1uint2int : g1uint2int_type(k1, k2)

g1uint2uint

Synopsis

fun{
k1,k2:tk
} g1uint2uint : g1uint2uint_type(k1, k2)

g1ofg0_uint

Synopsis

castfn
g1ofg0_uint{tk:tk}(x: g0uint tk):<> g1uint0 (tk)

g0string2uint

Synopsis

fun{tk:tk}
g0string2uint(rep: NSH(string)):<> g0uint(tk)

g1uint_get_index

Synopsis

prfun
g1uint_get_index
  {tk:tk}{i1:int}
  (x: g1uint(tk, i1)): [i2:int] EQINT(i1, i2)

g0uint_succ

Synopsis

fun{tk:tk}
g0uint_succ
  (g0uint(tk)):<> g0uint(tk)

g1uint_succ

Synopsis

fun{tk:tk}
g1uint_succ : g1uint_succ_type(tk)

g0uint_pred

Synopsis

fun{tk:tk}
g0uint_pred
  (g0uint(tk)):<> g0uint(tk)

g1uint_pred

Synopsis

fun{tk:tk}
g1uint_pred : g1uint_pred_type(tk)

g0uint_add

Synopsis

fun{
tk:tk
} g0uint_add
  (x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)

g1uint_add

Synopsis

fun
{tk:tk}
g1uint_add : g1uint_add_type(tk)

g0uint_sub

Synopsis

fun{
tk:tk
} g0uint_sub
  (x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)

g1uint_sub

Synopsis

fun
{tk:tk}
g1uint_sub : g1uint_sub_type(tk)

g0uint_mul

Synopsis

fun{
tk:tk
} g0uint_mul
  (x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)

g1uint_mul

Synopsis

fun
{tk:tk}
g1uint_mul : g1uint_mul_type(tk)

g1uint_mul2

Synopsis

fun
{tk:tk}
g1uint_mul2
  {i,j:int}
(
  x: g1uint(tk, i), y: g1uint(tk, j)
) :<> [ij:int] (MUL(i, j, ij) | g1uint(tk, ij))

g0uint_div

Synopsis

fun{
tk:tk
} g0uint_div
  (x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)

g1uint_div

Synopsis

fun
{tk:tk}
g1uint_div : g1uint_div_type(tk)

g0uint_mod

Synopsis

fun{
tk:tk
} g0uint_mod
  (x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)

g1uint_mod

Synopsis

fun
{tk:tk}
g1uint_mod : g1uint_mod_type(tk)

g0uint_lt

Synopsis

fun{
tk:tk
} g0uint_lt
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is less than its second argument. It is for unsigned integers.

g1uint_lt

Synopsis

fun{tk:tk}
g1uint_lt : g1uint_lt_type(tk)

g0uint_lte

Synopsis

fun{
tk:tk
} g0uint_lte
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is less than or equal to its second argument. It is for unsigned integers.

g1uint_lte

Synopsis

fun{tk:tk}
g1uint_lte : g1uint_lte_type(tk)

g0uint_gt

Synopsis

fun{
tk:tk
} g0uint_gt
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is greater than its second argument. It is for unsigned integers.

g1uint_gt

Synopsis

fun
{tk:tk}
g1uint_gt : g1uint_gt_type(tk)

g0uint_gte

Synopsis

fun{
tk:tk
} g0uint_gte
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is greater than or equal to its second argument. It is for unsigned integers.

g1uint_gte

Synopsis

fun
{tk:tk}
g1uint_gte : g1uint_gte_type(tk)

g0uint_eq

Synopsis

fun{
tk:tk
} g0uint_eq
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is equal to its second argument. It is for unsigned integers.

g1uint_eq

Synopsis

fun
{tk:tk}
g1uint_eq : g1uint_eq_type(tk)

g0uint_neq

Synopsis

fun{
tk:tk
} g0uint_neq
  (x: g0uint (tk), y: g0uint (tk)):<> bool

Description

This function returns true if and only if its first argument is unequal to its second argument. It is for unsigned integers.

g1uint_neq

Synopsis

fun
{tk:tk}
g1uint_neq : g1uint_neq_type(tk)

g0uint_compare

Synopsis

fun{tk:tk}
g0uint_compare
  (x: g0uint(tk), y: g0uint(tk)):<> int

g1uint_compare

Synopsis

fun{tk:tk}
g1uint_compare : g1uint_compare_type(tk)

g0uint_max

Synopsis

fun
{tk:tk}
g0uint_max
  (g0uint(tk), g0uint(tk)):<> g0uint(tk)

g1uint_max

Synopsis

fun
{tk:tk}
g1uint_max : g1uint_max_type(tk)

g0uint_min

Synopsis

fun
{tk:tk}
g0uint_min
  (g0uint(tk), g0uint(tk)):<> g0uint(tk)

g1uint_min

Synopsis

fun
{tk:tk}
g1uint_min : g1uint_min_type(tk)

fprint_uint

Synopsis

fun fprint_uint : fprint_type (uint) = "mac#%"

fprint_ulint

Synopsis

Synopsis for [fprint_ulint] is unavailable.

fprint_ullint

Synopsis

Synopsis for [fprint_ullint] is unavailable.

fprint_size

Synopsis

Synopsis for [fprint_size] is unavailable.

Macro Definitions

g0i2i

Synopsis

macdef g0i2i(x) = g0int2int(,(x))

g1i2i

Synopsis

macdef g1i2i(x) = g1int2int(,(x))

g0i2u

Synopsis

macdef g0i2u(x) = g0int2uint(,(x))

g1i2u

Synopsis

macdef g1i2u(x) = g1int2uint(,(x))

g0u2i

Synopsis

macdef g0u2i(x) = g0uint2int(,(x))

g1u2i

Synopsis

macdef g1u2i(x) = g1uint2int(,(x))

g0u2u

Synopsis

macdef g0u2u(x) = g0uint2uint(,(x))

g1u2u

Synopsis

macdef g1u2u(x) = g1uint2uint(,(x))

i2u

Synopsis

macdef
i2u(x) = g1int2uint_int_uint(,(x))

i2sz

Synopsis

Synopsis for [i2sz] is unavailable.

i2ssz

Synopsis

Synopsis for [i2ssz] is unavailable.

u2i

Synopsis

macdef
u2i(x) = g1uint2int_uint_int(,(x))

u2sz

Synopsis

Synopsis for [u2sz] is unavailable.

sz2i

Synopsis

Synopsis for [sz2i] is unavailable.

sz2u

Synopsis

Synopsis for [sz2u] is unavailable.

Overloaded Symbols

g0ofg1

Synopsis

overload g0ofg1 with g0ofg1_int // index-erasing

overload g0ofg1 with g0ofg1_uint // index-erasing

g1ofg0

Synopsis

overload g1ofg0 with g1ofg0_int // index-inducing

overload g1ofg0 with g1ofg0_uint // index-inducing

~

Synopsis

overload ~ with g0int_neg of 0

overload ~ with g1int_neg of 10 // ~ for uminus

overload ~ with g0uint_lnot

neg

Synopsis

overload neg with g0int_neg of 0

overload neg with g1int_neg of 10

abs

Synopsis

overload abs with g0int_abs of 0

overload abs with g1int_abs of 10

succ

Synopsis

overload succ with g0int_succ of 0

overload succ with g1int_succ of 10

overload succ with g0uint_succ of 0

overload succ with g1uint_succ of 10

pred

Synopsis

overload pred with g0int_pred of 0

overload pred with g1int_pred of 10

overload pred with g0uint_pred of 0

overload pred with g1uint_pred of 10

half

Synopsis

overload half with g0int_half of 0

overload half with g1int_half of 10

overload half with g0uint_half of 0

overload half with g1uint_half of 10

+

Synopsis

overload + with g0int_add of 0

overload + with add_int1_size0 of 11

overload + with add_size0_int1 of 11

overload + with g1int_add of 20

overload + with add_size1_int1 of 22

overload + with add_int1_size1 of 22

overload + with g0uint_add of 0

overload + with g1uint_add of 20

-

Synopsis

overload - with g0int_sub of 0

overload - with g1int_sub of 20

overload - with sub_size1_int1 of 22

overload - with g0uint_sub of 0

overload - with g1uint_sub of 20

*

Synopsis

overload * with g0int_mul of 0

overload * with mul_int1_size0 of 11

overload * with mul_size0_int1 of 11

overload * with g1int_mul of 20

overload * with mul_int1_size1 of 22

overload * with mul_size1_int1 of 22

overload * with g0uint_mul of 0

overload * with g1uint_mul of 20

/

Synopsis

overload / with g0int_div of 0

overload / with g1int_div of 20

overload / with g0uint_div of 0

overload / with g1uint_div of 20

mod

Synopsis

overload mod with g0int_mod of 0

overload mod with g0uint_mod of 0

overload mod with g1uint_mod of 20

isltz

Synopsis

overload isltz with g0int_isltz of 0

overload isltz with g1int_isltz of 10

isltez

Synopsis

overload isltez with g0int_isltez of 0

overload isltez with g1int_isltez of 10

isgtz

Synopsis

overload isgtz with g0int_isgtz of 0

overload isgtz with g1int_isgtz of 10

overload isgtz with g0uint_isgtz of 0

overload isgtz with g1uint_isgtz of 10

isgtez

Synopsis

overload isgtez with g0int_isgtez of 0

overload isgtez with g1int_isgtez of 10

iseqz

Synopsis

overload iseqz with g0int_iseqz of 0

overload iseqz with g1int_iseqz of 10

overload iseqz with g0uint_iseqz of 0

overload iseqz with g1uint_iseqz of 10

isneqz

Synopsis

overload isneqz with g0int_isneqz of 0

overload isneqz with g1int_isneqz of 10

overload isneqz with g0uint_isneqz of 0

overload isneqz with g1uint_isneqz of 10

<

Synopsis

overload < with g0int_lt of 0

overload < with lt_g0int_int of 11

overload < with g1int_lt of 20

overload < with lt_g1int_int of 21

overload < with g0uint_lt of 0

overload < with lt_g0uint_int of 11

overload < with g1uint_lt of 20

overload < with lt_g1uint_int of 21

<=

Synopsis

overload <= with g0int_lte of 0

overload <= with lte_g0int_int of 11

overload <= with g1int_lte of 20

overload <= with lte_g1int_int of 21

overload <= with g0uint_lte of 0

overload <= with lte_g0uint_int of 11

overload <= with g1uint_lte of 20

overload <= with lte_g1uint_int of 21

>

Synopsis

overload > with g0int_gt of 0

overload > with gt_g0int_int of 11

overload > with g1int_gt of 20

overload > with gt_g1int_int of 21

overload > with g0uint_gt of 0

overload > with gt_g0uint_int of 11

overload > with g1uint_gt of 20

overload > with gt_g1uint_int of 21

>=

Synopsis

overload >= with g0int_gte of 0

overload >= with gte_g0int_int of 11

overload >= with g1int_gte of 20

overload >= with gte_g1int_int of 21

overload >= with g0uint_gte of 0

overload >= with gte_g0uint_int of 11

overload >= with g1uint_gte of 20

overload >= with gte_g1uint_int of 21

=

Synopsis

overload = with g0int_eq of 0

overload = with eq_g0int_int of 11

overload = with g1int_eq of 20

overload = with eq_g1int_int of 21

overload = with g0uint_eq of 0

overload = with eq_g0uint_int of 11

overload = with g1uint_eq of 20

overload = with eq_g1uint_int of 21

!=

Synopsis

overload != with g0int_neq of 0

overload != with neq_g0int_int of 11

overload != with g1int_neq of 20

overload != with neq_g1int_int of 21

overload != with g0uint_neq of 0

overload != with neq_g0uint_int of 11

overload != with g1uint_neq of 20

overload != with neq_g1uint_int of 21

compare

Synopsis

overload compare with g0int_compare of 0

overload compare with compare_g0int_int of 11

overload compare with g1int_compare of 20

overload compare with compare_g1int_int of 21

overload compare with g0uint_compare of 0

overload compare with g1uint_compare of 20

max

Synopsis

overload max with g0int_max of 0

overload max with g1int_max of 20

overload max with g0uint_max of 0

overload max with g1uint_max of 20

min

Synopsis

overload min with g0int_min of 0

overload min with g1int_min of 20

overload min with g0uint_min of 0

overload min with g1uint_min of 20

print

Synopsis

overload print with print_int

overload print with print_uint

prerr

Synopsis

overload prerr with prerr_int

overload prerr with prerr_uint

fprint

Synopsis

overload fprint with fprint_int

overload fprint with fprint_uint

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.