#include "prelude/params.hats"
#if VERBOSE_FIXITY #then
#print "Loading [fixity.ats] starts!\n"
#endif
prefix 99 !
infixr 61 **
infixl 60 * / % mod
prefix 51 ~
infixl 50 + -
infixl 41 asl asr
infixl 41 lsl lsr
infix 40 < <= > >=
infixr 40 :: @
infix 30 = == != <>
infixl 21 &&
infixl ( && ) andalso land
infixl 20 ||
infixl ( || ) xor orelse lor lxor
infixr 10 ->
infix 0 :=
infix 0 :=:
infixl 0 <<
infixr 0 >>
prefix 0 ++ --
prefix 0 !++ --!
infixr 0 =++ --=
infix 0 :+= :-= :*= :/=
infix 0 :=+ :=- :=* :=/
prefix 0 ignoret
#if VERBOSE_FIXITY #then
#print "Loading [fixity.ats] finishes!\n"
#endif
#include "prelude/params.hats"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_pre.sats] starts!\n"
#endif
stacst
true_bool : bool = "ext#"
stacst
false_bool : bool = "ext#"
stadef
true = true_bool and false = false_bool
stacst
neg_bool
: bool -> bool = "ext#"
stadef ~ = neg_bool
stadef not = neg_bool
stacst
add_bool_bool
: (bool, bool) -> bool = "ext#"
stacst
mul_bool_bool
: (bool, bool) -> bool = "ext#"
stadef + = add_bool_bool and * = mul_bool_bool
stadef || = add_bool_bool and && = mul_bool_bool
stacst lt_bool_bool
: (bool, bool) -> bool = "ext#"
stacst lte_bool_bool
: (bool, bool) -> bool = "ext#"
stacst gt_bool_bool
: (bool, bool) -> bool = "ext#"
stacst gte_bool_bool
: (bool, bool) -> bool = "ext#"
stadef < = lt_bool_bool and <= = lte_bool_bool
stadef > = gt_bool_bool and >= = gte_bool_bool
stacst eq_bool_bool
: (bool, bool) -> bool = "ext#"
stacst neq_bool_bool
: (bool, bool) -> bool = "ext#"
stadef == = eq_bool_bool
stadef != = neq_bool_bool
stadef <> = neq_bool_bool
stacst
neg_int
: (int) -> int = "ext#"
stadef ~ = neg_int
stacst
add_int_int
: (int, int) -> int = "ext#"
stacst
sub_int_int
: (int, int) -> int = "ext#"
stacst
mul_int_int
: (int, int) -> int = "ext#"
stacst
div_int_int
: (int, int) -> int = "ext#"
stadef + = add_int_int and - = sub_int_int
stadef * = mul_int_int and / = div_int_int
stacst
ndiv_int_int
: (int, int) -> int = "ext#"
stacst
idiv_int_int
: (int, int) -> int = "ext#"
stadef ndiv = ndiv_int_int
stadef idiv = idiv_int_int
stadef
nmod_int_int
(
x:int, y:int
) = x - y * (x \ndiv_int_int y)
stadef mod = nmod_int_int
stadef nmod = nmod_int_int
stadef % = nmod_int_int
stacst lt_int_int
: (int, int) -> bool = "ext#"
stacst lte_int_int
: (int, int) -> bool = "ext#"
stacst gt_int_int
: (int, int) -> bool = "ext#"
stacst gte_int_int
: (int, int) -> bool = "ext#"
stadef < = lt_int_int and <= = lte_int_int
stadef > = gt_int_int and >= = gte_int_int
stacst eq_int_int
: (int, int) -> bool = "ext#"
stacst neq_int_int
: (int, int) -> bool = "ext#"
stadef == = eq_int_int
stadef != = neq_int_int
stadef <> = neq_int_int
stacst
abs_int
: (int) -> int = "ext#"
stadef
absrel_int_int
(x: int, v: int): bool =
(x >= 0 && x == v) || (x <= 0 && ~x == v)
stadef abs = abs_int
stadef absrel = absrel_int_int
stacst
sgn_int
: (int) -> int = "ext#"
stadef
sgnrel_int_int
(x: int, v: int): bool =
(x > 0 && v==1) || (x==0 && v==0) || (x < 0 && v==(~1))
stadef sgn = sgn_int
stadef sgnrel = sgnrel_int_int
stacst
max_int_int
: (int, int) -> int = "ext#"
stacst
min_int_int
: (int, int) -> int = "ext#"
stadef
maxrel_int_int_int
(x: int, y: int, v: int): bool =
(x >= y && x == v) || (x <= y && y == v)
stadef
minrel_int_int_int
(x: int, y: int, v: int): bool =
(x >= y && y == v) || (x <= y && x == v)
stadef max = max_int_int
stadef min = min_int_int
stadef maxrel = maxrel_int_int_int
stadef minrel = minrel_int_int_int
stadef
nsub (x:int, y:int) = max (x-y, 0)
stadef
ndivrel_int_int_int
(x: int, y: int, q: int): bool =
(q * y <= x) && (x < q * y + y)
stadef ndivrel = ndivrel_int_int_int
stadef
idivrel_int_int_int
(x: int, y: int, q: int) = (
x >= 0 && y > 0 && ndivrel_int_int_int ( x, y, q)
) || (
x >= 0 && y < 0 && ndivrel_int_int_int ( x, ~y, ~q)
) || (
x < 0 && y > 0 && ndivrel_int_int_int (~x, y, ~q)
) || (
x < 0 && y < 0 && ndivrel_int_int_int (~x, ~y, q)
)
stadef idivrel = idivrel_int_int_int
stadef
divmodrel_int_int_int_int
(x: int, y: int, q: int, r: int) : bool =
(0 <= r && r < y && x == q*y + r)
stadef divmodrel = divmodrel_int_int_int_int
stacst
ifint_bool_int_int
: (bool, int, int) -> int = "ext#"
stadef
ifintrel_bool_int_int_int
(
b:bool, x:int, y:int, r:int
) : bool = (b && r==x) || (~b && r==y)
stadef ifint = ifint_bool_int_int
stadef ifintrel = ifintrel_bool_int_int_int
stadef
bool2int(b: bool): int = ifint(b, 1, 0)
stadef int2bool (i: int): bool = (i != 0)
stadef b2i = bool2int and i2b = int2bool
stacst int_of_addr: addr -> int = "ext#"
stacst addr_of_int: int -> addr = "ext#"
stadef a2i = int_of_addr and i2a = addr_of_int
stadef pow2_7 = 128
stadef pow2_8 = 256
stadef i2u_int8 (i:int) = ifint (i >= 0, i, i+pow2_8)
stadef i2u8 = i2u_int8
stadef u2i_int8 (u:int) = ifint (u < pow2_7, u, u-pow2_8)
stadef u2i8 = u2i_int8
stadef pow2_15 = 32768
stadef pow2_16 = 65536
stadef i2u_int16 (i:int) = ifint (i >= 0, i, i+pow2_16)
stadef i2u16 = i2u_int16
stadef u2i_int16 (u:int) = ifint (u < pow2_15, u, u-pow2_16)
stadef u2i16 = u2i_int16
stadef pow2_32 = 0x100000000
stadef pow2_64 = 0x10000000000000000
stacst
null_addr : addr = "ext#"
stadef
null = null_addr and NULL = null_addr
stacst add_addr_int
: (addr, int) -> addr = "ext#"
stacst sub_addr_int
: (addr, int) -> addr = "ext#"
stacst sub_addr_addr
: (addr, addr) -> int = "ext#"
stadef + = add_addr_int
stadef - = sub_addr_int
stadef - = sub_addr_addr
stacst lt_addr_addr
: (addr, addr) -> bool = "ext#"
stacst lte_addr_addr
: (addr, addr) -> bool = "ext#"
stadef < = lt_addr_addr
stadef <= = lte_addr_addr
stacst gt_addr_addr
: (addr, addr) -> bool = "ext#"
stacst gte_addr_addr
: (addr, addr) -> bool = "ext#"
stadef > = gt_addr_addr
stadef >= = gte_addr_addr
stacst eq_addr_addr
: (addr, addr) -> bool = "ext#"
stacst neq_addr_addr
: (addr, addr) -> bool = "ext#"
stadef == = eq_addr_addr
stadef != = neq_addr_addr
stadef <> = neq_addr_addr
stacst
lte_cls_cls : (cls, cls) -> bool = "ext#"
stacst
gte_cls_cls : (cls, cls) -> bool = "ext#"
stadef <= = lte_cls_cls and >= = gte_cls_cls
stadef
lterel_cls_cls
(
c1: cls, c2: cls, lterel_cls_cls_res: bool
) : bool = lterel_cls_cls_res
stadef
gterel_cls_cls
(
c1: cls, c2: cls, gterel_cls_cls_res: bool
) : bool = gterel_cls_cls_res
stacst
sizeof_t0ype_int : t@ype -> int = "ext#"
stadef
sizeof(a:viewt@ype): int = sizeof_t0ype_int (a?)
sortdef nat = { i:int | i >= 0 }
sortdef pos = { i:int | i > 0 }
sortdef neg = { i:int | i < 0 }
sortdef npos = { i:int | i <= 0 }
sortdef nat1 = { n:nat | n < 1 }
sortdef nat2 = { n:nat | n < 2 }
sortdef nat3 = { n:nat | n < 3 }
sortdef nat4 = { n:nat | n < 4 }
sortdef sgn = { i:int | ~1 <= i; i <= 1 }
sortdef agz = { l:addr | l > null }
sortdef agez = { l:addr | l >= null }
sortdef alez = { l:addr | l <= null }
#define CHAR_MAX 127
#define CHAR_MIN ~128
#define UCHAR_MAX 0xFF
stacst effnil : eff
stacst effall : eff
stacst effntm : eff
stacst effexn : eff
stacst effref : eff
stacst effwrt : eff
stacst add_eff_eff : (eff, eff) -> eff
stadef + = add_eff_eff
stacst sub_eff_eff : (eff, eff) -> eff
stadef - = add_eff_eff
symintr ~ not
symintr lnot lor lxor land
symintr + - * / % mod ndiv nmod
symintr < <= > >= = == != <> compare
symintr isltz isltez isgtz isgtez iseqz isneqz
symintr neg abs max min
symintr succ pred half double
symintr square sqrt cube cbrt pow
symintr ! []
symintr << >>
symintr inc dec
symintr ++ --
symintr get set exch
symintr getinc setinc exchinc
symintr decget decset decexch
symintr !++ --!
symintr =++ --=
symintr assert
symintr encode decode
symintr uncons unsome
symintr ptrcast
symintr g0ofg1 g1ofg0
symintr copy free length
symintr print prerr fprint gprint
symintr println prerrln fprintln gprintln
symintr ofstring ofstrptr
symintr tostring tostrptr
symintr .size
symintr .len .length
symintr .get .set .exch
symintr .nrow .ncol
symintr .head .tail
symintr .next .prev
symintr .init .last
symintr .eval
abstype atstkind_type(tk: tkind)
abst@ype atstkind_t0ype(tk: tkind)
typedef
tkind_type(tk:tkind) = atstkind_type(tk)
typedef
tkind_t0ype(tk:tkind) = atstkind_t0ype(tk)
absview
at_vt0ype_addr_view(a:vt@ype+, l:addr)
viewdef @
(a:vt@ype, l:addr) = at_vt0ype_addr_view(a, l)
abst@ype clo_t0ype_t0ype(a:t@ype) = a
absvt@ype clo_vt0ype_vt0ype(a:vt@ype) = a
vtypedef READ (a:vt@ype) = a
vtypedef WRITE (a:vt@ype) = a
absprop invar_prop_prop (a:prop)
absview invar_view_view (a:view)
abst@ype
invar_t0ype_t0ype (a:t@ype) = a
absvt@ype
invar_vt0ype_vt0ype (a:vt@ype) = a
viewdef
INV (a: view) = invar_view_view (a)
propdef
INV (a: prop) = invar_prop_prop (a)
vtypedef INV
(a:vt@ype) = invar_vt0ype_vt0ype (a)
vtypedef
INV (a: t@ype) = invar_t0ype_t0ype (a)
abst@ype
stamped_t0ype(a:t@ype, int) = a
absvt@ype
stamped_vt0ype(a:vt@ype, int) = a
stadef stamped_t = stamped_t0ype
stadef stamped_vt = stamped_vt0ype
absview
vcopyenv_view_view(v:view)
absvt@ype
vcopyenv_vt0ype_vt0ype(vt: vt0ype) = vt
stadef vcopyenv_v = vcopyenv_view_view
stadef vcopyenv_vt = vcopyenv_vt0ype_vt0ype
#if VERBOSE_PRELUDE #then
#print "Loading [basics_pre.sats] finishes!\n"
#endif
#include "prelude/params.hats"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_sta.sats] starts!\n"
#endif
#define RD(x) x
tkindef bool_kind = "atstype_bool"
abst@ype
bool_t0ype = tkind_t0ype (bool_kind)
stadef bool = bool_t0ype
abst@ype
bool_bool_t0ype (b: bool) = bool_t0ype
stadef bool = bool_bool_t0ype
typedef Bool = [b:bool] bool (b)
typedef boolLte
(b1:bool) = [b2:bool] bool (b2 <= b1)
typedef boolGte
(b1:bool) = [b2:bool] bool (b2 >= b1)
abst@ype atstype_bool
tkindef
byte_kind = "atstype_byte"
abst@ype
byte_t0ype = tkind_t0ype (byte_kind)
stadef byte = byte_t0ype
sortdef int8 = {
i:int | ~128 <= i; i < 128
}
sortdef uint8 =
{ i:int | 0 <= i; i < 256 }
tkindef char_kind = "atstype_char"
abst@ype
char_t0ype = tkind_t0ype(char_kind)
abst@ype
char_int_t0ype(c:int) = char_t0ype
stadef char = char_t0ype
stadef char = char_int_t0ype
typedef Char = [c:int8] char(c)
typedef charNZ = [c:int8 | c != 0] char(c)
tkindef schar_kind = "atstype_schar"
abst@ype
schar_t0ype = tkind_t0ype(schar_kind)
abst@ype
schar_int_t0ype (c:int) = schar_t0ype
stadef schar = schar_t0ype
stadef schar = schar_int_t0ype
typedef sChar = [c:int8] schar(c)
typedef scharNZ = [c:int8 | c != 0] schar(c)
tkindef uchar_kind = "atstype_uchar"
abst@ype
uchar_t0ype = tkind_t0ype(uchar_kind)
abst@ype
uchar_int_t0ype (c:int) = uchar_t0ype
stadef uchar = uchar_t0ype
stadef uchar = uchar_int_t0ype
typedef uChar = [c:uint8] uchar (c)
typedef scharNZ = [c:uint8 | c != 0] uchar(c)
sortdef tk = tkind
abst@ype
g0int_t0ype (tk:tk) = tkind_t0ype (tk)
stadef g0int = g0int_t0ype
abst@ype
g1int_int_t0ype (tk:tkind, int) = g0int (tk)
stadef g1int = g1int_int_t0ype
typedef g1int (tk:tkind) = [i:int] g1int (tk, i)
typedef g1int0 (tk:tkind) = [i:int | i >= 0] g1int (tk, i)
typedef g1int1 (tk:tkind) = [i:int | i >= 1] g1int (tk, i)
typedef g1intLt
(tk:tk, n:int) = [i:int | i < n] g1int (tk, i)
typedef g1intLte
(tk:tk, n:int) = [i:int | i <= n] g1int (tk, i)
typedef g1intGt
(tk:tk, n:int) = [i:int | i > n] g1int (tk, i)
typedef g1intGte
(tk:tk, n:int) = [i:int | i >= n] g1int (tk, i)
typedef g1intBtw
(tk:tk, lb:int, ub:int) = [i: int | lb <= i; i < ub] g1int (tk, i)
typedef g1intBtwe
(tk:tk, lb:int, ub:int) = [i: int | lb <= i; i <= ub] g1int (tk, i)
abst@ype
g0uint_t0ype (tk:tkind) = tkind_t0ype (tk)
stadef g0uint = g0uint_t0ype
abst@ype
g1uint_int_t0ype (tk:tkind, int) = g0uint (tk)
stadef g1uint = g1uint_int_t0ype
typedef g1uint (tk:tk) = [i:int] g1uint (tk, i)
typedef g1uint0 (tk:tk) = [i:int | i >= 0] g1uint (tk, i)
typedef g1uint1 (tk:tk) = [i:int | i >= 1] g1uint (tk, i)
typedef g1uintLt
(tk:tk, n:int) = [i:nat | i < n] g1uint (tk, i)
typedef g1uintLte
(tk:tk, n:int) = [i:nat | i <= n] g1uint (tk, i)
typedef g1uintGt
(tk:tk, n:int) = [i:int | i > n] g1uint (tk, i)
typedef g1uintGte
(tk:tk, n:int) = [i:int | i >= n] g1uint (tk, i)
typedef g1uintBtw
(tk:tk, lb:int, ub:int) = [i: int | lb <= i; i < ub] g1uint (tk, i)
typedef g1uintBtwe
(tk:tk, lb:int, ub:int) = [i: int | lb <= i; i <= ub] g1uint (tk, i)
tkindef int_kind = "atstype_int"
typedef int0 = g0int (int_kind)
typedef int1 (i:int) = g1int (int_kind, i)
stadef int = int1
stadef int = int0
typedef Int = [i:int] int1 (i)
typedef Nat = [i:int | i >= 0] int1 (i)
typedef intLt (n:int) = g1intLt (int_kind, n)
typedef intLte (n:int) = g1intLte (int_kind, n)
typedef intGt (n:int) = g1intGt (int_kind, n)
typedef intGte (n:int) = g1intGte (int_kind, n)
typedef intBtw (lb:int, ub:int) = g1intBtw (int_kind, lb, ub)
typedef intBtwe (lb:int, ub:int) = g1intBtwe (int_kind, lb, ub)
typedef Two = intBtw (0, 2)
typedef Sgn = intBtwe (~1, 1)
typedef natLt (n:int) = intBtw (0, n)
typedef natLte (n:int) = intBtwe (0, n)
tkindef uint_kind = "atstype_uint"
typedef uint0 = g0uint (uint_kind)
typedef uint1 (n:int) = g1uint (uint_kind, n)
stadef uint = uint1
stadef uint = uint0
stadef uInt = [n:int] uint1 (n)
typedef uintLt (n:int) = g1uintLt (uint_kind, n)
typedef uintLte (n:int) = g1uintLte (uint_kind, n)
typedef uintGt (n:int) = g1uintGt (uint_kind, n)
typedef uintGte (n:int) = g1uintGte (uint_kind, n)
typedef uintBtw (lb:int, ub:int) = g1uintBtw (uint_kind, lb, ub)
typedef uintBtwe (lb:int, ub:int) = g1uintBtwe (uint_kind, lb, ub)
abst@ype atstype_int
abst@ype atstype_uint
tkindef
lint_kind = "atstype_lint"
typedef
lint0 = g0int (lint_kind)
typedef
lint1 (i:int) = g1int (lint_kind, i)
stadef lint = lint1
stadef lint = lint0
tkindef
ulint_kind = "atstype_ulint"
typedef
ulint0 = g0uint (ulint_kind)
typedef
ulint1 (i:int) = g1uint (ulint_kind, i)
stadef ulint = ulint1
stadef ulint = ulint0
tkindef
llint_kind = "atstype_llint"
typedef llint0 = g0int (llint_kind)
typedef llint1 (i:int) = g1int (llint_kind, i)
stadef llint = llint1
stadef llint = llint0
tkindef
ullint_kind = "atstype_ullint"
typedef
ullint0 = g0uint (ullint_kind)
typedef
ullint1 (i:int) = g1uint (ullint_kind, i)
stadef ullint = ullint1
stadef ullint = ullint0
tkindef
intptr_kind = "atstype_intptr"
typedef
intptr0 = g0int (intptr_kind)
typedef
intptr1 (i:int) = g1int (intptr_kind, i)
stadef intptr = intptr1
stadef intptr = intptr0
tkindef
uintptr_kind = "atstype_uintptr"
typedef
uintptr0 = g0uint (uintptr_kind)
typedef
uintptr1 (i:int) = g1uint (uintptr_kind, i)
stadef uintptr = uintptr1
stadef uintptr = uintptr0
tkindef
sint_kind = "atstype_sint"
typedef
sint0 = g0int (sint_kind)
typedef
sint1 (i:int) = g1int (sint_kind, i)
stadef sint = sint1
stadef sint = sint0
tkindef
usint_kind = "atstype_usint"
typedef
usint0 = g0uint (usint_kind)
typedef
usint1 (i:int) = g1uint (usint_kind, i)
stadef usint = usint1
stadef usint = usint0
tkindef
size_kind = "atstype_size"
typedef size0_t = g0uint (size_kind)
typedef size1_t (i:int) = g1uint (size_kind, i)
stadef size_t = size1_t
stadef size_t = size0_t
typedef Size =
[i:int | i >= 0] g1uint (size_kind, i)
typedef Size_t = Size
typedef sizeLt (n:int) = g1uintLt (size_kind, n)
typedef sizeLte (n:int) = g1uintLte (size_kind, n)
typedef sizeGt (n:int) = g1uintGt (size_kind, n)
typedef sizeGte (n:int) = g1uintGte (size_kind, n)
typedef sizeBtw (lb:int, ub:int) = g1uintBtw (size_kind, lb, ub)
typedef sizeBtwe (lb:int, ub:int) = g1uintBtwe (size_kind, lb, ub)
tkindef
ssize_kind = "atstype_ssize"
typedef ssize0_t = g0int (ssize_kind)
typedef ssize1_t (i:int) = g1int (ssize_kind , i)
stadef ssize_t = ssize1_t
stadef ssize_t = ssize0_t
typedef SSize =
[i:int] g1int (ssize_kind, i)
typedef SSize_t = SSize
typedef ssizeLt (n:int) = g1intLt (ssize_kind, n)
typedef ssizeLte (n:int) = g1intLte (ssize_kind, n)
typedef ssizeGt (n:int) = g1intGt (ssize_kind, n)
typedef ssizeGte (n:int) = g1intGte (ssize_kind, n)
typedef ssizeBtw (lb:int, ub:int) = g1intBtw (ssize_kind, lb, ub)
typedef ssizeBtwe (lb:int, ub:int) = g1intBtwe (ssize_kind, lb, ub)
abst@ype atstype_size
abst@ype atstype_ssize
typedef sizeof_t (a:vt@ype) = size_t (sizeof(a?))
tkindef
int8_kind = "atstype_int8"
typedef
int8_0 = g0int (int8_kind)
typedef
int8_1
(i:int) = g1int (int8_kind, i)
stadef int8 = int8_1
stadef int8 = int8_0
stadef Int8 = [i:int] int8_1 (i)
tkindef
uint8_kind = "atstype_uint8"
typedef
uint8_0 = g0uint (uint8_kind)
typedef
uint8_1
(i:int) = g1uint (uint8_kind, i)
stadef uint8 = uint8_1
stadef uint8 = uint8_0
stadef uInt8 = [i:nat] uint8_1 (i)
tkindef
int16_kind = "atstype_int16"
typedef
int16_0 = g0int (int16_kind)
typedef
int16_1
(i:int) = g1int (int16_kind, i)
stadef int16 = int16_1
stadef int16 = int16_0
stadef Int16 = [i:int] int16_1 (i)
tkindef
uint16_kind = "atstype_uint16"
typedef
uint16_0 = g0uint (uint16_kind)
typedef
uint16_1
(i:int) = g1uint (uint16_kind, i)
stadef uint16 = uint16_1
stadef uint16 = uint16_0
stadef uInt16 = [i:nat] uint16_1 (i)
tkindef
int32_kind = "atstype_int32"
typedef
int32_0 = g0int (int32_kind)
typedef
int32_1
(i:int) = g1int (int32_kind, i)
stadef int32 = int32_1
stadef int32 = int32_0
stadef Int32 = [i:int] int32_1 (i)
tkindef
uint32_kind = "atstype_uint32"
typedef
uint32_0 = g0uint (uint32_kind)
typedef
uint32_1
(i:int) = g1uint (uint32_kind, i)
stadef uint32 = uint32_1
stadef uint32 = uint32_0
stadef uInt32 = [i:nat] uint32_1 (i)
tkindef
int64_kind = "atstype_int64"
typedef
int64_0 = g0int (int64_kind)
typedef
int64_1
(i:int) = g1int (int64_kind, i)
stadef int64 = int64_1
stadef int64 = int64_0
stadef Int64 = [i:int] int64_1 (i)
tkindef
uint64_kind = "atstype_uint64"
typedef
uint64_0 = g0uint (uint64_kind)
typedef
uint64_1
(i:int) = g1uint (uint64_kind, i)
stadef uint64 = uint64_1
stadef uint64 = uint64_0
stadef uInt64 = [i:nat] uint64_1 (i)
abst@ype
g0float_t0ype (tk:tk) = tkind_t0ype (tk)
stadef g0float = g0float_t0ype
tkindef float_kind = "atstype_float"
typedef float = g0float (float_kind)
tkindef double_kind = "atstype_double"
typedef double = g0float (double_kind)
tkindef ldouble_kind = "atstype_ldouble"
typedef ldouble = g0float (ldouble_kind)
tkindef ptr_kind = "atstype_ptrk"
abstype ptr_type = tkind_type(ptr_kind)
abstype ptr_addr_type(l:addr) = ptr_type
typedef ptr = ptr_type
typedef ptr(l:addr) = ptr_addr_type(l)
typedef Ptr = [l:addr] ptr(l)
typedef Ptr0 = [l:agez] ptr(l)
typedef Ptr1 = [l:addr|l > null] ptr(l)
typedef
Ptrnull (l:addr) =
[l1:addr | l1 == null || l1 == l] ptr(l1)
typedef ptr(n:int) = ptr_addr_type(addr_of_int(n))
abstype
string_type = ptr
abstype
string_int_type(n: int) = string_type
stadef
string0 = string_type
stadef
string1 = string_int_type
stadef string = string1
stadef string = string0
typedef String = [n:int] string_int_type(n)
typedef String0 = [n:int | n >= 0] string_int_type(n)
typedef String1 = [n:int | n >= 1] string_int_type(n)
abstype
stropt_int_type(n:int) = ptr
typedef
stropt(n:int) = stropt_int_type(n)
typedef stropt = [n:int] stropt_int_type(n)
typedef Stropt = [n:int] stropt_int_type(n)
typedef Stropt0 = [n:int] stropt_int_type(n)
typedef Stropt1 = [n:int | n >= 0] stropt_int_type(n)
absvtype
strptr_addr_vtype(l:addr) = ptr
vtypedef strptr(l:addr) = strptr_addr_vtype(l)
vtypedef strptr = [l:addr] strptr(l)
vtypedef Strptr = [l:addr] strptr(l)
vtypedef Strptr0 = [l:addr] strptr(l)
vtypedef Strptr1 = [l:addr|l > null] strptr(l)
absvtype
strnptr_addr_int_vtype(l:addr, n:int) = ptr
vtypedef
strnptr(l:addr, n:int) = strnptr_addr_int_vtype(l, n)
vtypedef
strnptr(n:int) = [l:addr] strnptr_addr_int_vtype(l, n)
vtypedef Strnptr = [l:addr;n:int] strnptr(l, n)
vtypedef Strnptr0 = [l:addr;n:int] strnptr(l, n)
vtypedef Strnptr1 = [l:addr;n:int | n >= 0] strnptr(l, n)
abstype
strref_addr_type (l:addr) = ptr
stadef strref = strref_addr_type
typedef Strref0 = [l:addr] strref (l)
typedef Strref1 = [l:addr | l > null] strref (l)
abst@ype
atsvoid_t0ype
typedef void = atsvoid_t0ype
absvtype
exception_vtype = $extype"atstype_exnconptr"
vtypedef exn = exception_vtype
absvt@ype
opt_vt0ype_bool_vt0ype (a:vt@ype+, opt:bool) = a
stadef opt = opt_vt0ype_bool_vt0ype
typedef bytes (n:int) = @[byte][n]
viewdef bytes_v (l:addr, n:int) = bytes (n) @ l
typedef b0ytes (n:int) = @[byte?][n]
viewdef b0ytes_v (l:addr, n:int) = b0ytes (n) @ l
abstype
cloref_t0ype_type (a:t@ype) = ptr
stadef cloref = cloref_t0ype_type
absvtype
cloptr_vt0ype_vtype (a:t@ype) = ptr
stadef cloptr = cloptr_vt0ype_vtype
vtypedef
cloptr0 = cloptr_vt0ype_vtype (void)
typedef
stamped_t
(a:t@ype) = [x:int] stamped_t(a, x)
vtypedef
stamped_vt
(a:vt@ype) = [x:int] stamped_vt(a, x)
absview
mfree_gc_addr_view(addr)
stadef
mfree_gc_v = mfree_gc_addr_view
absview
mfree_ngc_addr_view(addr)
stadef
mfree_ngc_v = mfree_ngc_addr_view
absview
mfree_libc_addr_view(addr)
stadef
mfree_libc_v = mfree_libc_addr_view
absvt@ype
arrpsz_vt0ype_int_vt0ype
(a:vt@ype+, n:int) = $extype"atstype_arrpsz"
stadef
arrpsz = arrpsz_vt0ype_int_vt0ype
absprop
vbox_view_prop (v:view)
propdef
vbox(v:view) = vbox_view_prop(v)
abstype
ref_vt0ype_type(a:vt@ype) = ptr
typedef
ref(a:vt@ype) = ref_vt0ype_type(a)
viewdef
vtakeout
( v1: view
, v2: view ) = (v2, v2 -<lin,prf> v1)
viewdef
vtakeout0 (v:view) = vtakeout(void, v)
vtypedef
vttakeout
( vt1:vt@ype
, vt2:vt@ype ) = (vt2 -<lin,prf> vt1 | vt2)
vtypedef
vttakeout0 (vt:vt@ype) = vttakeout(void, vt)
vtypedef
vtakeoutptr
(a:vt@ype) =
[l:addr] (a@l, a@l -<lin,prf> void | ptr l)
vtypedef
vstrptr(l:addr) = vttakeout0(strptr(l))
vtypedef vStrptr0 = [l:agez] vstrptr(l)
vtypedef vStrptr1 = [l:addr | l > null] vstrptr(l)
typedef
bottom_t0ype_uni = {a:t@ype} (a)
typedef
bottom_t0ype_exi = [a:t@ype | false] (a)
vtypedef
bottom_vt0ype_uni = {a:vt@ype} (a)
vtypedef
bottom_vt0ype_exi = [a:vt@ype | false] (a)
typedef
cmpval_fun
(a: t@ype) = (a, a) -<fun> int
typedef
cmpval_funenv
(a: t@ype, vt: t@ype) = (a, a, !vt) -<fun> int
stadef cmpval = cmpval_fun and cmpval = cmpval_funenv
typedef
cmpref_fun
(a: vt@ype) = (&RD(a), &RD(a)) -<fun> int
typedef
cmpref_funenv
(a: vt@ype, vt: vt@ype) = (&RD(a), &RD(a), !vt) -<fun> int
stadef cmpref = cmpref_fun and cmpref = cmpref_funenv
abstype
lazy_t0ype_type(t@ype+) = ptr
typedef
lazy(a:t@ype) = lazy_t0ype_type(a)
absvtype
lazy_vt0ype_vtype(vt@ype+) = ptr
vtypedef
lazy_vt(a:vt@ype) = lazy_vt0ype_vtype(a)
abst@ype
undefined_t0ype = $extype"atstype_undefined"
absvt@ype
undefined_vt0ype = $extype"atstype_undefined"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_sta.sats] finishes!\n"
#endif
#include "prelude/params.hats"
fun
patsopt_version(): string = "ext#%"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] starts!\n"
#endif
sortdef t0p = t@ype and vt0p = vt@ype
datatype TYPE(a:vt@ype) = TYPE(a) of ()
#define true true_bool
#define false false_bool
val true_bool : bool(true) = "mac#atsbool_true"
val false_bool : bool(false) = "mac#atsbool_false"
prfun false_elim{X:prop | false} (): X
typedef
compopr_type(a: t@ype) = (a, a) -<fun0> bool
typedef
compare_type(a: t@ype) = (a, a) -<fun0> int
praxi
lemma_subcls_reflexive
{c:cls}(): [c <= c] void
praxi
lemma_subcls_transitive
{c1,c2,c3:cls | c1 <= c2; c2 <= c3}(): [c1 <= c3] void
praxi
praxi_int{i:int} (): int(i)
dataprop
MUL_prop
(
int, int, int
) =
| {n:int}
MULbas (0, n, 0)
| {m:nat}{n:int}{p:int}
MULind (m+1, n, p+n) of MUL_prop (m, n, p)
| {m:pos}{n:int}{p:int}
MULneg (~(m), n, ~(p)) of MUL_prop (m, n, p)
propdef MUL(m:int, n:int, mn:int) = MUL_prop(m, n, mn)
absprop
DIVMOD (
x:int, y: int, q: int, r: int
)
propdef DIV (x:int, y:int, q:int) = [r:int] DIVMOD(x, y, q, r)
propdef MOD (x:int, y:int, r:int) = [q:int] DIVMOD(x, y, q, r)
dataprop
EQINT(int, int) = {x:int} EQINT(x, x)
prfun
eqint_make{x,y:int | x == y}(): EQINT(x, y)
prfun
eqint_make_gint
{tk:tk}{x:int}(x: g1int(tk, x)): [y:int] EQINT(x, y)
prfun
eqint_make_guint
{tk:tk}{x:int}(x: g1uint(tk, x)): [y:int] EQINT(x, y)
praxi praxi_ptr{l:addr} (): ptr(l)
praxi praxi_bool{b:bool} (): bool(b)
dataprop
EQADDR(addr, addr) = {x:addr} EQADDR(x, x)
prfun
eqaddr_make{x,y:addr | x == y}(): EQADDR(x, y)
prfun
eqaddr_make_ptr{x:addr}(x: ptr(x)): [y:addr] EQADDR(x, y)
dataprop
EQBOOL(bool, bool) = {x:bool} EQBOOL(x, x)
prfun
eqbool_make{x,y:bool | x == y}(): EQBOOL(x, y)
prfun
eqbool_make_bool{x:bool}(x: bool(x)): [y:bool] EQBOOL(x, y)
dataprop
EQTYPE(vt@ype, vt@ype) = {a:vt@ype} EQTYPE (a, a)
prfun
prop_verify{b:bool | b} ():<prf> void
prfun
prop_verify_and_add{b:bool | b} ():<prf> [b] void
prfun pridentity_v{v:view} (x: !INV(v)): void
prfun pridentity_vt{vt:viewt@ype} (x: !INV(vt)): void
castfn
viewptr_match
{a:vt0ype}{l1,l2:addr|l1==l2}
(
pf: INV(a) @ l1 | p: ptr(l2)
) :<> [l:addr | l==l1] (a @ l | ptr(l))
val{
a:vt0ype
} sizeof : size_t(sizeof(a))
praxi
lemma_sizeof
{a:vt0ype}(): [sizeof(a) >= 0] void
praxi topize{a:t0ype} (x: !INV(a) >> a?): void
castfn dataget{a:vt0ype} (x: !INV(a) >> a): a?!
praxi
mfree_gc_v_elim
{l:addr} (pf: mfree_gc_v l):<prf> void
praxi
mfree_gcngc_v_nullify
{l:addr} (
pf1: mfree_gc_v(l), pf1: mfree_ngc_v(l)
) : void
fun
cloptr_free
{a:t0p}
(pclo: cloptr(a)):<!wrt> void = "mac#%"
fun
{a:t0p}
lazy_force(lazyval: lazy(INV(a))):<!laz> (a)
fun
{a:vt0p}
lazy_vt_force(lazyval: lazy_vt(INV(a))):<!all> (a)
fun
lazy_vt_free
{a:vt0p}
(lazyval: lazy_vt(a)):<!wrt> void = "mac#%"
overload ~ with lazy_vt_free of 0
fun
lazy2cloref
{a:t0p}(lazy(a)): () -<cloref1> (a) = "mac#%"
castfn
stamp_t{a:t@ype}(x: a):<> stamped_t(a)
castfn
stamp_vt{a:vt@ype}(x: a):<> stamped_vt(a)
castfn
unstamp_t
{a:t@ype}{x:int}(x: stamped_t(INV(a), x)):<> a
castfn
unstamp_vt
{a:vt@ype}{x:int}(x: stamped_vt(INV(a), x)):<> a
castfn
stamped_t2vt
{a:t@ype}{x:int}
(x: stamped_t(INV(a), x)):<> stamped_vt(a, x)
castfn
stamped_vt2t
{a:t@ype}{x:int}
(x: stamped_vt(INV(a), x)):<> stamped_t(a, x)
fun{a:t@ype}
stamped_vt2t_ref{x:int}
(x: &stamped_vt(INV(a), x)):<> stamped_t(a, x)
praxi
vcopyenv_v_decode
{v:view}(x: vcopyenv_v(v)): vtakeout0(v)
castfn
vcopyenv_vt_decode
{vt:vt0p}(x: vcopyenv_vt(vt)): vttakeout0(vt)
overload decode with vcopyenv_v_decode
overload decode with vcopyenv_vt_decode
val
the_null_ptr
: ptr(null) = "mac#the_atsptr_null"
praxi
lemma_addr_param
{l:addr}(): [l >= null] void
praxi
lemma_string_param
{n:int} (x: string(n)): [n >= 0] void
praxi
lemma_stropt_param
{n:int} (x: stropt(n)): [n >= ~1] void
dataprop
SGN (int, int) =
| SGNzero (0, 0)
| {i:neg} SGNneg (i, ~1) | {i:pos} SGNpos (i, 1)
exception AssertExn of ()
exception NotFoundExn of ()
exception GenerallyExn of (string)
exception IllegalArgExn of (string)
praxi __vfree_exn (x: exn):<> void
datatype unit = unit of ()
dataprop unit_p = unit_p of ()
dataview unit_v = unit_v of ()
datavtype unit_vt = unit_vt of ()
prfun unit_v_elim (pf: unit_v): void
abstype
boxed_t0ype_type(a:t@ype+) = unit
absvtype
boxed_vt0ype_vtype(a:vt@ype+) = unit
vtypedef
boxed(a:vt@ype) = boxed_vt0ype_vtype(a)
vtypedef
boxed_vt(a:vt@ype) = boxed_vt0ype_vtype(a)
typedef boxed(a:t@ype) = boxed_t0ype_type(a)
typedef boxed_t(a:t@ype) = boxed_t0ype_type(a)
fun{a:type} box: (INV(a)) -> boxed_t(a)
fun{a:type} unbox: boxed_t(INV(a)) -> (a)
fun{a:vtype} box_vt: (INV(a)) -> boxed_vt(a)
fun{a:vtype} unbox_vt: boxed_vt(INV(a)) -> (a)
stadef
array(a:vt@ype, n:int) = @[a][n]
viewdef
array_v
(a:vt@ype, l:addr, n:int) = @[a][n] @ l
absvtype
arrayptr_vt0ype_addr_int_vtype
(a:vt0ype+, l:addr, n:int) = ptr(l)
stadef
arrayptr = arrayptr_vt0ype_addr_int_vtype
vtypedef
arrayptr
(a:vt0p, n:int) = [l:addr] arrayptr(a, l, n)
abstype
arrayref_vt0ype_int_type
(a:vt@ype, n:int) = ptr
stadef arrayref = arrayref_vt0ype_int_type
abstype
arrszref_vt0ype_type(a: vt@ype) = ptr
typedef arrszref(a:vt0p) = arrszref_vt0ype_type(a)
datatype
list_t0ype_int_type
(a:t@ype+, int) =
| list_nil(a, 0) of ()
| {n:int | n >= 0}
list_cons(a, n+1) of (a, list_t0ype_int_type(a, n))
stadef list = list_t0ype_int_type
typedef
List(a:t0p) = [n:int] list(a, n)
typedef
List0(a:t0p) = [n:int | n >= 0] list(a, n)
typedef
List1(a:t0p) = [n:int | n >= 1] list(a, n)
typedef listLt
(a:t0p, n:int) = [k:nat | k < n] list(a, k)
typedef listLte
(a:t0p, n:int) = [k:nat | k <= n] list(a, k)
typedef listGt
(a:t0p, n:int) = [k:int | k > n] list(a, k)
typedef listGte
(a:t0p, n:int) = [k:int | k >= n] list(a, k)
typedef listBtw
(a:t0p, m:int, n:int) = [k:int | m <= k; k < n] list(a, k)
typedef listBtwe
(a:t0p, m:int, n:int) = [k:int | m <= k; k <= n] list(a, k)
datavtype
list_vt0ype_int_vtype
(a:vt@ype+, int) =
| list_vt_nil(a, 0) of ()
| {n:int | n >= 0}
list_vt_cons(a, n+1) of (a, list_vt0ype_int_vtype(a, n))
stadef list_vt = list_vt0ype_int_vtype
vtypedef
List_vt(a:vt0p) = [n:int] list_vt(a, n)
vtypedef
List0_vt(a:vt0p) = [n:int | n >= 0] list_vt(a, n)
vtypedef
List1_vt(a:vt0p) = [n:int | n >= 1] list_vt(a, n)
vtypedef listLt_vt
(a:vt0p, n:int) = [k:nat | k < n] list_vt(a, k)
vtypedef listLte_vt
(a:vt0p, n:int) = [k:nat | k <= n] list_vt(a, k)
vtypedef listGt_vt
(a:vt0p, n:int) = [k:int | k > n] list_vt(a, k)
vtypedef listGte_vt
(a:vt0p, n:int) = [k:int | k >= n] list_vt(a, k)
vtypedef listBtw_vt
(a:vt0p, m:int, n:int) = [k:int | m <= k; k < n] list_vt(a, k)
vtypedef listBtwe_vt
(a:vt0p, m:int, n:int) = [k:int | m <= k; k <= n] list_vt(a, k)
datatype
stream_con(a:t@ype+) =
| stream_nil of ()
| stream_cons of (a, stream(a))
where stream (a:t@ype) = lazy (stream_con(a))
datavtype
stream_vt_con
(a:vt@ype+) =
| stream_vt_nil of ()
| stream_vt_cons of (a, stream_vt(a))
where
stream_vt(a:vt@ype) = lazy_vt(stream_vt_con(a))
datatype
option_t0ype_bool_type
(
a:t@ype+, bool
) =
| Some(a, true) of (INV(a)) | None(a, false)
stadef option = option_t0ype_bool_type
typedef Option(a:t0p) = [b:bool] option(a, b)
datavtype
option_vt0ype_bool_vtype
(
a:vt@ype+, bool
) =
| Some_vt(a, true) of (INV(a)) | None_vt(a, false)
stadef option_vt = option_vt0ype_bool_vtype
vtypedef Option_vt(a:vt0p) = [b:bool] option_vt(a, b)
praxi
opt_some{a:vt0p}
(x: !INV(a) >> opt(a, true)):<prf> void
praxi
opt_unsome{a:vt0p}
(x: !opt(INV(a), true) >> a):<prf> void
fun{a:vt0p}
opt_unsome_get(x: &opt(INV(a), true) >> a?): (a)
praxi
opt_none{a:vt0p}
(x: !(a?) >> opt(a, false)):<prf> void
praxi
opt_unnone{a:vt0p}
(x: !opt(INV(a), false) >> a?):<prf> void
praxi
opt_clear{a:t0p}
{b:bool}(x: !opt(INV(a), b) >> a?):<prf> void
dataprop
or_prop_prop_int_prop
(
a0: prop+, a1: prop+, int
) =
| POR_l(a0, a1, 0) of (INV(a0))
| POR_r(a0, a1, 1) of (INV(a1))
dataview
or_view_view_int_view
(
a0: view+, a1: view+, int
) =
| VOR_l(a0, a1, 0) of (INV(a0))
| VOR_r(a0, a1, 1) of (INV(a1))
stadef por = or_prop_prop_int_prop
stadef vor = or_view_view_int_view
dataprop
option_prop_bool_prop
(
a:prop+, bool
) =
| Some_p (a, true) of (INV(a)) | None_p (a, false)
stadef option_p = option_prop_bool_prop
dataview
option_view_bool_view
(a:view+, bool) =
| Some_v (a, true) of (INV(a)) | None_v (a, false)
stadef option_v = option_view_bool_view
absvt@ype
arrayopt(a:vt0p, n:int, b:bool) = array(a, n)
praxi
arrayopt_some
{a:vt0p}{n:int}
(A: &array(a, n) >> arrayopt(a, n, true)): void
praxi
arrayopt_none
{a:vt0p}{n:int}
(A: &array(a?, n) >> arrayopt(a, n, false)): void
praxi
arrayopt_unsome
{a:vt0p}{n:int}
(A: &arrayopt(a, n, true) >> array(a, n)): void
praxi
arrayopt_unnone
{a:vt0p}{n:int}
(A: &arrayopt(a, n, false) >> array(a?, n)): void
absvtype
argv_int_vtype (n:int) = ptr
stadef argv = argv_int_vtype
praxi
lemma_argv_param
{n:int}(argv: !argv(n)): [n >= 0] void
fun
argv_get_at{n:int}
(argv: !argv(n), i: natLt(n)):<> string = "mac#%"
fun
argv_set_at{n:int}
(argv: !argv(n), i: natLt(n), x: string):<!wrt> void = "mac#%"
overload [] with argv_get_at
overload [] with argv_set_at
fun{}
listize_argc_argv
{n:int}
(argc: int(n), argv: !argv(n)): list_vt(string, n)
symintr main0
fun
main_void_0
(
) : void = "ext#mainats_void_0"
fun
main_argc_argv_0
{n:int | n >= 1}
(argc: int n, argv: !argv(n)): void = "ext#mainats_argc_argv_0"
overload main0 with main_void_0
overload main0 with main_argc_argv_0
symintr main
fun
main_void_int
(
) : int = "ext#mainats_void_int"
fun
main_argc_argv_int
{n:int | n >= 1}
(argc: int n, argv: !argv(n)): int = "ext#mainats_argc_argv_int"
fun
main_argc_argv_envp_int
{n:int | n >= 1}
(argc: int n, argv: !argv n, envp: ptr): int = "ext#mainats_argc_argv_envp_int"
overload main with main_void_int
overload main with main_argc_argv_int
overload main with main_argc_argv_envp_int
fun
exit(ecode: int):<!exn> {a:t0p}(a) = "mac#%"
fun
exit_errmsg
(ecode: int, msg: string):<!exn> {a:t0p}(a) = "mac#%"
fun
exit_void
(ecode: int):<!exn> void = "mac#%"
fun
exit_errmsg_void
(ecode: int, msg: string):<!exn> void = "mac#%"
fun
assert_bool0
(x: bool):<!exn> void = "mac#%"
fun
assert_bool1
{b:bool} (x: bool (b)):<!exn> [b] void = "mac#%"
overload assert with assert_bool0 of 0
overload assert with assert_bool1 of 10
fun{}
assertexn_bool0 (x: bool):<!exn> void
fun{}
assertexn_bool1 {b:bool} (x: bool (b)):<!exn> [b] void
symintr assertexn
overload assertexn with assertexn_bool0 of 0
overload assertexn with assertexn_bool1 of 10
fun
assert_errmsg_bool0
(x: bool, msg: string):<!exn> void = "mac#%"
fun
assert_errmsg_bool1
{b:bool} (x: bool b, msg: string):<!exn> [b] void = "mac#%"
symintr assert_errmsg
overload assert_errmsg with assert_errmsg_bool0 of 0
overload assert_errmsg with assert_errmsg_bool1 of 10
fun
assert_errmsg2_bool0
(x: bool, msg1: string, msg2: string):<!exn> void = "mac#%"
fun
assert_errmsg2_bool1{b:bool}
(x: bool b, msg1: string, msg2: string):<!exn> [b] void = "mac#%"
symintr assert_errmsg2
overload assert_errmsg2 with assert_errmsg2_bool0 of 0
overload assert_errmsg2 with assert_errmsg2_bool1 of 10
datasort
file_mode =
| file_mode_r
| file_mode_w
| file_mode_rw
local
stadef r() = file_mode_r()
stadef w() = file_mode_w()
stadef rw() = file_mode_rw()
in
abstype
file_mode (file_mode) = string
typedef
file_mode = [fm:file_mode] file_mode (fm)
sortdef fmode = file_mode
typedef fmode (fm:fmode) = file_mode (fm)
typedef fmode = file_mode
dataprop
file_mode_lte
(fmode, fmode) =
| {m:fmode} file_mode_lte_refl (m, m)
| {m1,m2,m3:fmode}
file_mode_lte_tran (m1, m3) of
(file_mode_lte(m1, m2), file_mode_lte(m2, m3))
| {m:fmode} file_mode_lte_rw_r(rw(), r()) of ()
| {m:fmode} file_mode_lte_rw_w(rw(), w()) of ()
prval
file_mode_lte_r_r
: file_mode_lte(r(), r())
prval
file_mode_lte_w_w
: file_mode_lte(w(), w())
prval
file_mode_lte_rw_rw
: file_mode_lte(rw(), rw())
end
abstype FILEref_type = ptr
typedef FILEref = FILEref_type
typedef
print_type(a: t0p) = (a) -> void
typedef
prerr_type(a: t0p) = (a) -> void
typedef
fprint_type(a: t0p) = (FILEref, a) -> void
typedef
print_vtype(a: vt0p) = (!a) -> void
typedef
prerr_vtype(a: vt0p) = (!a) -> void
typedef
fprint_vtype(a: vt0p) = (FILEref, !a) -> void
fun print_newline(): void = "mac#%"
fun prerr_newline(): void = "mac#%"
fun fprint_newline(out: FILEref): void = "mac#%"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] finishes!\n"
#endif
#include "prelude/params.hats"
#if VERBOSE_PRELUDE #then
#print "Loading [basics_gen.sats] starts!\n"
#endif
fun
{a:t0p}
gidentity (x: INV(a)):<> a
fun
{a:vt0p}
gidentity_vt (x: INV(a)):<> a
fun
{a:vt0p}
gcopy_val (x: !INV(a)):<!wrt> a
fun
{a:vt0p}
gcopy_ref (x: &INV(a)):<!wrt> a
fun
{a:vt0p}
gfree_val (x: INV(a)):<!wrt> void
fun
{a:vt0p}
ginit_ref (x: &a? >> a):<!wrt> void
fun
{a:vt0p}
gclear_ref (x: &a >> a?):<!wrt> void
fun
{a:t0p}
gequal_val_val (x: a, y: a):<> bool
fun
{a:vt0p}
gequal_ref_ref (x: &INV(a), y: &a):<> bool
fun{a:t0p}
tostring_val (x: a):<> string
fun{a:vt0p}
tostring_ref (x: &INV(a)):<> string
fun{a:t0p}
tostrptr_val (x: a):<!wrt> Strptr1
fun{a:vt0p}
tostrptr_ref (x: &INV(a)):<!wrt> Strptr1
fun{a:t0p}
fprint_val (out: FILEref, x: a): void
fun{a:vt0p}
fprint_ref (out: FILEref, x: &INV(a)): void
fun
{src:vt0p}
{elt:vt0p}
streamize_val (source: src): stream_vt(elt)
#if VERBOSE_PRELUDE #then
#print "Loading [basics_gen.sats] finishes!\n"
#endif
#include "prelude/params.hats"
macdef
orelse(x, y) =
(if ,(x) then true else ,(y)): bool
macdef
andalso(x, y) =
(if ,(x) then ,(y) else false): bool
macdef
ifval(test, v_then, v_else) =
(if ,(test) then ,(v_then) else ,(v_else))
macdef delay(exp) = $delay(,(exp))
macdef raise(exn) = $raise(,(exn))
macdef assign(lv, rv) = ,(lv) := ,(rv)
macdef
exitloc(ecode) =
exit_errmsg (,(ecode), $mylocation)
macdef
assertloc(tf) =
assert_errmsg (,(tf), $mylocation)
macdef
assertlocmsg
(tf, msg) =
assert_errmsg2 (,(tf), $mylocation, ,(msg))
macdef
assertmsgloc
(tf, msg) =
assert_errmsg2 (,(tf), ,(msg), $mylocation)
macdef
undefined() = let
val () =
assertlocmsg
(false, ": undefined!!!") in $raise(AssertExn)
end
macdef ignoret(x) = let val _ = ,(x) in end
macdef foldret(x) = let val x = ,(x) in fold@ (x); x end
macdef showtype(x) = $showtype ,(x)
macdef showview(x) = pridentity_v ($showtype ,(x))
macdef showvtype(x) = pridentity_vt ($showtype ,(x))
macdef showviewtype(x) = pridentity_vt ($showtype ,(x))
macdef :+= (x, a) = let val v = ,(x) in ,(x) := ,(a) + v end
macdef :-= (x, a) = let val v = ,(x) in ,(x) := ,(a) - v end
macdef :*= (x, a) = let val v = ,(x) in ,(x) := ,(a) * v end
macdef :/= (x, a) = let val v = ,(x) in ,(x) := ,(a) / v end
macdef :=+ (x, a) = let val v = ,(x) in ,(x) := v + ,(a) end
macdef :=- (x, a) = let val v = ,(x) in ,(x) := v - ,(a) end
macdef :=* (x, a) = let val v = ,(x) in ,(x) := v * ,(a) end
macdef :=/ (x, a) = let val v = ,(x) in ,(x) := v / ,(a) end
macdef
println(x) = (print(,(x)); print_newline())
macdef
prerrln(x) = (prerr(,(x)); prerr_newline())
macdef
fprintln(out, x) = (fprint(,(out), ,(x)); fprint_newline(,(out)))
macdef
eqfn(x0) = lam(x) =<cloref1> (,(x0) = x)
macdef
cmpfn(x0) = lam(x) =<cloref1> compare(,(x0), x)
sortdef tk = tkind
typedef SHR(a:t@ype) = a
typedef NSH(a:t@ype) = a
stadef intknd = int_kind
stadef uintknd = uint_kind
fun{
k1,k2:tk
} g0int2int(x: g0int(k1)):<> g0int(k2)
fun
g0int2int_int_int(i0: int):<> int = "mac#%"
fun{tk:tk}
g0int2string(g0int(tk)):<!wrt> Strptr1
fun
g0int2string_int(i0: int):<!wrt> Strptr1 = "mac#%"
fun{tk:tk}
g0string2int(rep: NSH(string)):<> g0int(tk)
fun
g0string2int_int(rep: NSH(string)):<> int = "mac#%"
typedef
g0int_uop_type
(tk: tk) =
(g0int(tk)) -<fun0> g0int(tk)
fun
{tk:tk}
g0int_neg : g0int_uop_type(tk)
overload ~ with g0int_neg of 0
overload neg with g0int_neg of 0
fun
{tk:tk}
g0int_abs : g0int_uop_type(tk)
overload abs with g0int_abs of 0
fun
{tk:tk}
g0int_succ : g0int_uop_type(tk)
fun
{tk:tk}
g0int_pred : g0int_uop_type(tk)
overload succ with g0int_succ of 0
overload pred with g0int_pred of 0
fun
{tk:tk}
g0int_half : g0int_uop_type(tk)
overload half with g0int_half of 0
typedef
g0int_aop_type
(tk: tk) =
(
g0int(tk)
, g0int(tk)
) -<fun0> g0int (tk)
fun
{tk:tk}
g0int_add : g0int_aop_type(tk)
overload + with g0int_add of 0
fun
{tk:tk}
g0int_sub : g0int_aop_type(tk)
overload - with g0int_sub of 0
fun
{tk:tk}
g0int_mul : g0int_aop_type(tk)
overload * with g0int_mul of 0
fun
{tk:tk}
g0int_div : g0int_aop_type(tk)
overload / with g0int_div of 0
fun
{tk:tk}
g0int_mod : g0int_aop_type(tk)
overload % with g0int_mod of 0
overload mod with g0int_mod of 0
fun{}
mul_int1_size0{i:nat}(int(i), size_t):<> size_t
fun{}
mul_size0_int1{j:nat}(size_t, int(j)):<> size_t
overload * with mul_int1_size0 of 11
overload * with mul_size0_int1 of 11
fun
{tk:tk}
g0int_asl
(x: g0int(tk), n: intGte(0)):<> g0int(tk)
fun
{tk:tk}
g0int_asr
(x: g0int(tk), n: intGte(0)):<> g0int(tk)
overload << with g0int_asl of 0
overload >> with g0int_asr of 0
fun
{tk:tk}
g0int_npow
(x: g0int(tk), n: intGte(0)):<> g0int(tk)
overload ** with g0int_npow of 0
fun{tk:tk}
g0int_isltz (x: g0int (tk)):<> bool
fun{tk:tk}
g0int_isltez (x: g0int (tk)):<> bool
fun{tk:tk}
g0int_isgtz (x: g0int (tk)):<> bool
fun{tk:tk}
g0int_isgtez (x: g0int (tk)):<> bool
fun{tk:tk}
g0int_iseqz (x: g0int (tk)):<> bool
fun{tk:tk}
g0int_isneqz (x: g0int (tk)):<> bool
overload isltz with g0int_isltz of 0
overload isltez with g0int_isltez of 0
overload isgtz with g0int_isgtz of 0
overload isgtez with g0int_isgtez of 0
overload iseqz with g0int_iseqz of 0
overload isneqz with g0int_isneqz of 0
typedef
g0int_cmp_type(tk:tk) =
(g0int(tk), g0int(tk)) -<fun0> bool
fun
{tk:tk}
g0int_lt : g0int_cmp_type(tk)
overload < with g0int_lt of 0
fun
{tk:tk}
g0int_lte : g0int_cmp_type(tk)
overload <= with g0int_lte of 0
fun
{tk:tk}
g0int_gt : g0int_cmp_type(tk)
overload > with g0int_gt of 0
fun
{tk:tk}
g0int_gte : g0int_cmp_type(tk)
overload >= with g0int_gte of 0
fun
{tk:tk}
g0int_eq : g0int_cmp_type(tk)
overload = with g0int_eq of 0
fun
{tk:tk}
g0int_neq : g0int_cmp_type(tk)
overload != with g0int_neq of 0
overload <> with g0int_neq of 0
fun{tk:tk}
g0int_sgn(g0int(tk)): intBtwe(~1,1)
fun{tk:tk}
g0int_compare
(x: g0int(tk), y: g0int(tk)):<> int
overload compare with g0int_compare of 0
fun
{tk:tk}
g0int_max : g0int_aop_type(tk)
overload max with g0int_max of 0
fun
{tk:tk}
g0int_min : g0int_aop_type(tk)
overload min with g0int_min of 0
fun{tk:tk}
lt_g0int_int (x: g0int (tk), y: int):<> bool
overload < with lt_g0int_int of 11
fun{tk:tk}
lte_g0int_int (x: g0int (tk), y: int):<> bool
overload <= with lte_g0int_int of 11
fun{tk:tk}
gt_g0int_int (x: g0int (tk), y: int):<> bool
overload > with gt_g0int_int of 11
fun{tk:tk}
gte_g0int_int (x: g0int (tk), y: int):<> bool
overload >= with gte_g0int_int of 11
fun{tk:tk}
eq_g0int_int (x: g0int (tk), y: int):<> bool
overload = with eq_g0int_int of 11
fun{tk:tk}
neq_g0int_int (x: g0int (tk), y: int):<> bool
overload != with neq_g0int_int of 11
overload <> with neq_g0int_int of 11
fun{tk:tk}
compare_g0int_int (x: g0int (tk), y: int):<> int
overload compare with compare_g0int_int of 11
castfn
g0ofg1_int{tk:tk}(g1int(tk)):<> g0int(tk)
castfn
g1ofg0_int{tk:tk}(g0int(tk)):<> g1int(tk)
overload g0ofg1 with g0ofg1_int
overload g1ofg0 with g1ofg0_int
fun{
k1,k2:tk
} g1int2int
{i:int} (x: g1int (k1, i)):<> g1int (k2, i)
fun
g1int2int_int_int{i:int}(int(i)):<> int(i) = "mac#%"
fun{tk:tk}
g1string2int (str: NSH(string)):<> g1int(tk)
prfun
g1int_get_index
{tk:tk}{i1:int}
(x: g1int(tk, i1)): [i2:int] EQINT(i1, i2)
typedef
g1int_neg_type (tk:tk) =
{i:int} g1int(tk, i) -<fun0> g1int(tk, ~i)
fun
{tk:tk}
g1int_neg : g1int_neg_type(tk)
overload ~ with g1int_neg of 10
overload neg with g1int_neg of 10
typedef
g1int_abs_type (tk:tk) =
{i:int} g1int (tk, i) -<fun0> g1int(tk, abs(i))
fun
{tk:tk}
g1int_abs : g1int_abs_type(tk)
overload abs with g1int_abs of 10
typedef
g1int_succ_type (tk:tk) =
{i:int} g1int (tk, i) -<fun0> g1int (tk, i+1)
fun{tk:tk}
g1int_succ : g1int_succ_type(tk)
overload succ with g1int_succ of 10
typedef
g1int_pred_type (tk:tk) =
{i:int} g1int (tk, i) -<fun0> g1int (tk, i-1)
fun{tk:tk}
g1int_pred : g1int_pred_type(tk)
overload pred with g1int_pred of 10
typedef
g1int_half_type (tk:tk) =
{i:int} g1int (tk, i) -<fun0> g1int (tk, i/2)
fun{tk:tk}
g1int_half : g1int_half_type(tk)
overload half with g1int_half of 10
typedef
g1int_add_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> g1int(tk, i+j)
fun
{tk:tk}
g1int_add : g1int_add_type(tk)
fun{}
add_size1_int1
{i,j:int | i+j >= 0}
(i: size_t(i), j: int(j)):<> size_t(i+j)
fun{}
add_int1_size1
{i,j:int | i+j >= 0}
(i: int(i), j: size_t(j)):<> size_t(i+j)
overload + with g1int_add of 20
overload + with add_size1_int1 of 22
overload + with add_int1_size1 of 22
typedef
g1int_sub_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> g1int(tk, i-j)
fun
{tk:tk}
g1int_sub : g1int_sub_type(tk)
fun{}
sub_size1_int1
{i,j:int | i-j >= 0}
(i: size_t(i), j: int(j)):<> size_t(i-j)
overload - with g1int_sub of 20
overload - with sub_size1_int1 of 22
typedef
g1int_mul_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> g1int(tk, i*j)
fun
{tk:tk}
g1int_mul : g1int_mul_type(tk)
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))
fun{}
mul_int1_size1
{i,j:int | i >= 0}
(i: int(i), j: size_t(j)):<> size_t(i*j)
fun{}
mul_size1_int1
{i,j:int | j >= 0}
(i: size_t(i), j: int(j)):<> size_t(i*j)
overload * with g1int_mul of 20
overload * with mul_int1_size1 of 22
overload * with mul_size1_int1 of 22
typedef
g1int_div_type
(tk:tk) =
{i,j:int | j != 0}
(
g1int(tk, i), g1int(tk, j)
) -<fun0>
[r:int | r == i/j ] g1int(tk, r)
typedef
g1int_ndiv_type
(tk:tk) =
{i,j:int | i >= 0; j > 0}
(
g1int(tk, i), g1int(tk, j)
) -<fun0> g1int(tk, ndiv_int_int(i,j))
fun
{tk:tk}
g1int_div : g1int_div_type(tk)
fun
{tk:tk}
g1int_ndiv : g1int_ndiv_type(tk)
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)
)
fun{tk:tk}
ndiv_g1int_int1
{i,j:int | i >= 0; j > 0}
(
g1int(tk, i), int(j)
) :<> g1int(tk, ndiv_int_int(i,j))
overload / with g1int_div of 20
overload ndiv with g1int_ndiv of 20
overload ndiv with ndiv_g1int_int1 of 21
typedef
g1int_nmod_type
(tk:tk) =
{i,j:int | i >= 0; j > 0}
(
g1int(tk, i), g1int(tk, j)
) -<fun0> g1int(tk, nmod_int_int(i, j))
fun{tk:tk}
g1int_nmod : g1int_nmod_type(tk)
overload nmod with g1int_nmod of 20
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)
)
fun{tk:tk}
nmod_g1int_int1
{i,j:int | i >= 0; j > 0}
(x: g1int(tk, i), y: int(j)):<> int(i%j)
fun{tk:tk}
nmod2_g1int_int1
{i,j:int | i >= 0; j > 0}
(
x: g1int(tk, i), y: int(j)
) :<> [q,r:nat | r < j] (DIVMOD(i, j, q, r) | int(r))
overload nmod with nmod_g1int_int1 of 21
typedef
g1int_isltz_type
(tk:tk) =
{i:int}
(g1int(tk, i)) -<fun0> bool(i < 0)
typedef
g1int_isltez_type
(tk:tk) =
{i:int}
(g1int (tk, i)) -<fun0> bool(i <= 0)
fun{tk:tk}
g1int_isltz : g1int_isltz_type(tk)
fun{tk:tk}
g1int_isltez : g1int_isltez_type(tk)
overload isltz with g1int_isltz of 10
overload isltez with g1int_isltez of 10
typedef
g1int_isgtz_type
(tk:tk) =
{i:int}
(g1int(tk, i)) -<fun0> bool(i > 0)
typedef
g1int_isgtez_type
(tk:tk) =
{i:int}
(g1int (tk, i)) -<fun0> bool(i >= 0)
fun{tk:tk}
g1int_isgtz : g1int_isgtz_type(tk)
fun{tk:tk}
g1int_isgtez : g1int_isgtez_type(tk)
overload isgtz with g1int_isgtz of 10
overload isgtez with g1int_isgtez of 10
typedef
g1int_iseqz_type
(tk:tk) =
{i:int}
(g1int (tk, i)) -<fun0> bool(i > 0)
typedef
g1int_isneqz_type
(tk:tk) =
{i:int}
(g1int (tk, i)) -<fun0> bool(i >= 0)
fun{tk:tk}
g1int_iseqz : g1int_iseqz_type(tk)
fun{tk:tk}
g1int_isneqz : g1int_isneqz_type(tk)
overload iseqz with g1int_iseqz of 10
overload isneqz with g1int_isneqz of 10
typedef
g1int_lt_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i < j)
typedef
g1int_lte_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i <= j)
fun{tk:tk}
g1int_lt : g1int_lt_type(tk)
overload < with g1int_lt of 20
fun{tk:tk}
g1int_lte : g1int_lte_type(tk)
overload <= with g1int_lte of 20
typedef
g1int_gt_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i > j)
typedef
g1int_gte_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i >= j)
fun
{tk:tk}
g1int_gt : g1int_gt_type(tk)
overload > with g1int_gt of 20
fun
{tk:tk}
g1int_gte : g1int_gte_type(tk)
overload >= with g1int_gte of 20
typedef
g1int_eq_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i == j)
typedef
g1int_neq_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> bool(i != j)
fun
{tk:tk}
g1int_eq : g1int_eq_type(tk)
overload = with g1int_eq of 20
fun
{tk:tk}
g1int_neq : g1int_neq_type(tk)
overload != with g1int_neq of 20
overload <> with g1int_neq of 20
typedef
g1int_compare_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> int(sgn(i-j))
fun{tk:tk}
g1int_compare : g1int_compare_type(tk)
overload compare with g1int_compare of 20
typedef
g1int_max_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> g1int(tk, max(i, j))
fun
{tk:tk}
g1int_max : g1int_max_type(tk)
overload max with g1int_max of 20
typedef
g1int_min_type
(tk:tk) =
{i,j:int}
(
g1int(tk, i)
, g1int(tk, j)
) -<fun0> g1int(tk, min(i, j))
fun
{tk:tk}
g1int_min : g1int_min_type(tk)
overload min with g1int_min of 20
fun{tk:tk}
lt_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i < j)
fun{tk:tk}
lte_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i <= j)
overload < with lt_g1int_int of 21
overload <= with lte_g1int_int of 21
fun{tk:tk}
gt_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i > j)
fun{tk:tk}
gte_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i >= j)
overload > with gt_g1int_int of 21
overload >= with gte_g1int_int of 21
fun{tk:tk}
eq_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i == j)
overload = with eq_g1int_int of 21
fun{tk:tk}
neq_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> bool(i != j)
overload != with neq_g1int_int of 21
overload <> with neq_g1int_int of 21
fun{tk:tk}
compare_g1int_int{i,j:int}
(g1int(tk, i), int(j)):<> int(sgn(i-j))
overload compare with compare_g1int_int of 21
fun
{tk:tk}
g1int_sgn{i:int}(g1int(tk, i)):<> int(sgn(i))
fun{
k1,k2:tk
} g0int2uint(g0int(k1)):<> g0uint(k2)
fun
g0int2uint_int_uint(int):<> uint = "mac#%"
fun{
k1,k2:tk
} g0uint2int(g0uint(k1)):<> g0int(k2)
fun
g0uint2int_uint_int(uint):<> int = "mac#%"
fun{
k1,k2:tk
} g0uint2uint(g0uint(k1)):<> g0uint(k2)
fun
g0uint2uint_uint_uint(uint):<> uint = "mac#%"
fun{tk:tk}
g0string2uint(rep: NSH(string)):<> g0uint(tk)
fun
g0string2uint_uint(rep: NSH(string)):<> uint = "mac#%"
fun{tk:tk}
g0uint_succ
(g0uint(tk)):<> g0uint(tk)
fun{tk:tk}
g0uint_pred
(g0uint(tk)):<> g0uint(tk)
overload succ with g0uint_succ of 0
overload pred with g0uint_pred of 0
fun{tk:tk}
g0uint_half
(g0uint(tk)):<> g0uint(tk)
overload half with g0uint_half of 0
fun{
tk:tk
} g0uint_add
(x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)
overload + with g0uint_add of 0
fun{
tk:tk
} g0uint_sub
(x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)
overload - with g0uint_sub of 0
fun{
tk:tk
} g0uint_mul
(x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)
overload * with g0uint_mul of 0
fun{
tk:tk
} g0uint_div
(x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)
overload / with g0uint_div of 0
fun{
tk:tk
} g0uint_mod
(x: g0uint (tk), y: g0uint (tk)):<> g0uint (tk)
overload % with g0uint_mod of 0
overload mod with g0uint_mod of 0
fun
{tk:tk}
g0uint_lsl
(
x: g0uint(tk), n: intGte(0)
) :<> g0uint(tk)
fun
{tk:tk}
g0uint_lsr
(
x: g0uint(tk), n: intGte(0)
) :<> g0uint(tk)
overload << with g0uint_lsl of 10
overload >> with g0uint_lsr of 10
fun
{tk:tk}
g0uint_lnot
(g0uint(tk)):<> g0uint(tk)
overload ~ with g0uint_lnot
overload lnot with g0uint_lnot
fun
{tk:tk}
g0uint_lor
(g0uint(tk), g0uint(tk)):<> g0uint(tk)
fun
{tk:tk}
g0uint_lxor
(g0uint(tk), g0uint(tk)):<> g0uint(tk)
fun
{tk:tk}
g0uint_land
(g0uint(tk), g0uint(tk)):<> g0uint(tk)
overload lor with g0uint_lor
overload lxor with g0uint_lxor
overload land with g0uint_land
fun{tk:tk}
g0uint_isgtz(x: g0uint(tk)):<> bool
fun{tk:tk}
g0uint_iseqz(x: g0uint(tk)):<> bool
fun{tk:tk}
g0uint_isneqz(x: g0uint(tk)):<> bool
overload isgtz with g0uint_isgtz of 0
overload iseqz with g0uint_iseqz of 0
overload isneqz with g0uint_isneqz of 0
fun{
tk:tk
} g0uint_lt
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload < with g0uint_lt of 0
fun{
tk:tk
} g0uint_lte
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload <= with g0uint_lte of 0
fun{
tk:tk
} g0uint_gt
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload > with g0uint_gt of 0
fun{
tk:tk
} g0uint_gte
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload >= with g0uint_gte of 0
fun{
tk:tk
} g0uint_eq
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload = with g0uint_eq of 0
fun{
tk:tk
} g0uint_neq
(x: g0uint (tk), y: g0uint (tk)):<> bool
overload != with g0uint_neq of 0
overload <> with g0uint_neq of 0
fun{tk:tk}
g0uint_compare
(x: g0uint(tk), y: g0uint(tk)):<> int
overload compare with g0uint_compare of 0
fun
{tk:tk}
g0uint_max
(g0uint(tk), g0uint(tk)):<> g0uint(tk)
fun
{tk:tk}
g0uint_min
(g0uint(tk), g0uint(tk)):<> g0uint(tk)
overload max with g0uint_max of 0
overload min with g0uint_min of 0
fun{tk:tk}
lt_g0uint_int
(x: g0uint(tk), y: int):<> bool
fun{tk:tk}
lte_g0uint_int
(x: g0uint(tk), y: int):<> bool
overload < with lt_g0uint_int of 11
overload <= with lte_g0uint_int of 11
fun{tk:tk}
gt_g0uint_int
(x: g0uint(tk), y: int):<> bool
fun{tk:tk}
gte_g0uint_int
(x: g0uint(tk), y: int):<> bool
overload > with gt_g0uint_int of 11
overload >= with gte_g0uint_int of 11
fun{tk:tk}
eq_g0uint_int
(x: g0uint(tk), y: int):<> bool
fun{tk:tk}
neq_g0uint_int
(x: g0uint(tk), y: int):<> bool
overload = with eq_g0uint_int of 11
overload != with neq_g0uint_int of 11
overload <> with neq_g0uint_int of 11
praxi
lemma_g1uint_param
{tk:tk}{i:int}(g1uint(tk, i)):<> [i >= 0] void
castfn
size_of_int{i:nat}(x: int(i)):<> size_t(i)
castfn
ssize_of_int{i:int}(x: int(i)):<> ssize_t(i)
castfn
g0ofg1_uint{tk:tk}(x: g1uint tk):<> g0uint (tk)
castfn
g1ofg0_uint{tk:tk}(x: g0uint tk):<> g1uint0 (tk)
overload g0ofg1 with g0ofg1_uint
overload g1ofg0 with g1ofg0_uint
typedef
g1int2int_type
(k1:tk, k2:tk) =
{i:int}
(g1int(k1, i)) -<fun0> g1int(k2, i)
typedef
g1int2uint_type
(k1:tk, k2:tk) =
{i:nat}
(g1int(k1, i)) -<fun0> g1uint(k2, i)
fun{
k1,k2:tk
} g1int2int : g1int2int_type(k1, k2)
fun{
k1,k2:tk
} g1int2uint : g1int2uint_type(k1, k2)
fun
g1int2int_int_int:
g1int2int_type(intknd, intknd) = "mac#%"
fun
g1int2uint_int_uint:
g1int2uint_type(intknd, uintknd) = "mac#%"
typedef
g1uint2int_type
(k1:tk, k2:tk) =
{u:int}
(
g1uint(k1, u)
) -<fun0> [u>=0] g1int(k2, u)
typedef
g1uint2uint_type
(k1:tk, k2:tk) =
{u:int}
(g1uint(k1, u)) -<fun0> g1uint(k2, u)
fun{
k1,k2:tk
} g1uint2int : g1uint2int_type(k1, k2)
fun{
k1,k2:tk
} g1uint2uint : g1uint2uint_type(k1, k2)
fun
g1uint2int_uint_int:
g1uint2int_type(uintknd, intknd) = "mac#%"
fun
g1uint2uint_uint_uint:
g1uint2uint_type(uintknd, uintknd) = "mac#%"
fun{tk:tk}
g1string2uint(rep: NSH(string)):<> g1uint(tk)
prfun
g1uint_get_index
{tk:tk}{i1:int}
(x: g1uint(tk, i1)): [i2:int] EQINT(i1, i2)
typedef
g1uint_succ_type
(tk:tk) =
{i:int}
(g1uint(tk, i)) -<fun0> g1uint(tk, i+1)
typedef
g1uint_pred_type
(tk:tk) =
{i:int | i > 0}
(g1uint(tk, i)) -<fun0> g1uint(tk, i-1)
fun{tk:tk}
g1uint_succ : g1uint_succ_type(tk)
overload succ with g1uint_succ of 10
fun{tk:tk}
g1uint_pred : g1uint_pred_type(tk)
overload pred with g1uint_pred of 10
typedef
g1uint_half_type
(tk:tk) =
{i:int}
(
g1uint(tk, i)
) -<fun0> g1uint(tk, i/2)
fun{tk:tk}
g1uint_half : g1uint_half_type(tk)
overload half with g1uint_half of 10
typedef
g1uint_double_type
(tk:tk) =
{i:int}
(
g1uint(tk, i)
) -<fun0> g1uint(tk, 2*i)
fun{tk:tk}
g1uint_double : g1uint_double_type(tk)
overload double with g1uint_double of 10
typedef
g1uint_add_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> g1uint(tk, i+j)
typedef
g1uint_sub_type
(tk:tk) =
{i,j:int | i >= j}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> g1uint (tk, i-j)
fun
{tk:tk}
g1uint_add : g1uint_add_type(tk)
fun
{tk:tk}
g1uint_sub : g1uint_sub_type(tk)
overload + with g1uint_add of 20
overload - with g1uint_sub of 20
typedef
g1uint_mul_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> g1uint (tk, i*j)
fun
{tk:tk}
g1uint_mul : g1uint_mul_type(tk)
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))
overload * with g1uint_mul of 20
typedef
g1uint_div_type
(tk:tk) =
{i,j:int | j > 0}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0>
[r:nat | r == ndiv_int_int(i,j)] g1uint(tk, r)
fun
{tk:tk}
g1uint_div : g1uint_div_type(tk)
fun
{tk:tk}
g1uint_div2 {i,j:int | j > 0}
(
x: g1uint (tk, i), y: g1uint (tk, j)
) :<> [q,r:int | 0 <= r; r < j] (DIVMOD (i, j, q, r) | g1uint (tk, q))
overload / with g1uint_div of 20
typedef
g1uint_mod_type
(tk:tk) =
{i,j:int | j > 0}
(
g1uint(tk, i)
, g1uint (tk, j)
) -<fun0> [r:nat | r < j] g1uint (tk, r)
fun
{tk:tk}
g1uint_mod : g1uint_mod_type(tk)
fun
{tk:tk}
g1uint_mod2
{i,j:int | j > 0}
(
x: g1uint (tk, i), y: g1uint (tk, j)
) :<>
[
q,r:int | 0 <= r; r < j
] (
DIVMOD (i, j, q, r) | g1uint (tk, r)
)
overload mod with g1uint_mod of 20
typedef
g1uint_isgtz_type
(tk:tk) =
{i:int}
(g1uint(tk, i)) -<fun0> bool(i > 0)
fun{tk:tk}
g1uint_isgtz : g1uint_isgtz_type(tk)
overload isgtz with g1uint_isgtz of 10
typedef
g1uint_iseqz_type
(tk:tk) =
{i:int}
(g1uint(tk, i)) -<fun0> bool(i > 0)
typedef
g1uint_isneqz_type
(tk:tk) =
{i:int}
(g1uint(tk, i)) -<fun0> bool(i >= 0)
fun{tk:tk}
g1uint_iseqz : g1uint_iseqz_type(tk)
fun{tk:tk}
g1uint_isneqz : g1uint_isneqz_type(tk)
overload iseqz with g1uint_iseqz of 10
overload isneqz with g1uint_isneqz of 10
typedef
g1uint_lt_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i < j)
typedef
g1uint_lte_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i <= j)
fun{tk:tk}
g1uint_lt : g1uint_lt_type(tk)
fun{tk:tk}
g1uint_lte : g1uint_lte_type(tk)
overload < with g1uint_lt of 20
overload <= with g1uint_lte of 20
typedef
g1uint_gt_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i > j)
typedef
g1uint_gte_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i >= j)
fun
{tk:tk}
g1uint_gt : g1uint_gt_type(tk)
fun
{tk:tk}
g1uint_gte : g1uint_gte_type(tk)
overload > with g1uint_gt of 20
overload >= with g1uint_gte of 20
typedef
g1uint_eq_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> bool(i == j)
typedef
g1uint_neq_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> bool(i != j)
fun
{tk:tk}
g1uint_eq : g1uint_eq_type(tk)
fun
{tk:tk}
g1uint_neq : g1uint_neq_type(tk)
overload = with g1uint_eq of 20
overload != with g1uint_neq of 20
overload <> with g1uint_neq of 20
typedef
g1uint_compare_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> int(sgn(i-j))
fun{tk:tk}
g1uint_compare : g1uint_compare_type(tk)
overload compare with g1uint_compare of 20
typedef
g1uint_max_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> g1uint(tk, max(i, j))
typedef
g1uint_min_type
(tk:tk) =
{i,j:int}
(
g1uint(tk, i)
, g1uint(tk, j)
) -<fun0> g1uint(tk, min(i, j))
fun
{tk:tk}
g1uint_max : g1uint_max_type(tk)
fun
{tk:tk}
g1uint_min : g1uint_min_type(tk)
overload max with g1uint_max of 20
overload min with g1uint_min of 20
fun{tk:tk}
lt_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i < j)
fun{tk:tk}
lte_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i <= j)
overload < with lt_g1uint_int of 21
overload <= with lte_g1uint_int of 21
fun{tk:tk}
gt_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i > j)
fun{tk:tk}
gte_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i >= j)
overload > with gt_g1uint_int of 21
overload >= with gte_g1uint_int of 21
fun{tk:tk}
eq_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i == j)
fun{tk:tk}
neq_g1uint_int{i:int;j:nat}
(g1uint(tk, i), int(j)):<> bool(i != j)
overload = with eq_g1uint_int of 21
overload != with neq_g1uint_int of 21
overload <> with neq_g1uint_int of 21
fun print_int (int): void = "mac#%"
fun prerr_int (int): void = "mac#%"
fun fprint_int : fprint_type (int) = "mac#%"
overload print with print_int
overload prerr with prerr_int
overload fprint with fprint_int
fun print_uint (uint): void = "mac#%"
fun prerr_uint (uint): void = "mac#%"
fun fprint_uint : fprint_type (uint) = "mac#%"
overload print with print_uint
overload prerr with prerr_uint
overload fprint with fprint_uint
fun g0int_neg_int (x: int):<> int = "mac#%"
fun g0int_abs_int (x: int):<> int = "mac#%"
fun g0int_succ_int (x: int):<> int = "mac#%"
fun g0int_pred_int (x: int):<> int = "mac#%"
fun g0int_half_int (x: int):<> int = "mac#%"
fun g0int_asl_int (x: int, n: intGte(0)):<> int = "mac#%"
fun g0int_asr_int (x: int, n: intGte(0)):<> int = "mac#%"
fun g0int_add_int (x: int, y: int):<> int = "mac#%"
fun g0int_sub_int (x: int, y: int):<> int = "mac#%"
fun g0int_mul_int (x: int, y: int):<> int = "mac#%"
fun g0int_div_int (x: int, y: int):<> int = "mac#%"
fun g0int_mod_int (x: int, y: int):<> int = "mac#%"
fun g0int_lt_int (x: int, y: int):<> bool = "mac#%"
fun g0int_lte_int (x: int, y: int):<> bool = "mac#%"
fun g0int_gt_int (x: int, y: int):<> bool = "mac#%"
fun g0int_gte_int (x: int, y: int):<> bool = "mac#%"
fun g0int_eq_int (x: int, y: int):<> bool = "mac#%"
fun g0int_neq_int (x: int, y: int):<> bool = "mac#%"
fun g0int_compare_int (x: int, y: int):<> int = "mac#%"
fun g0int_max_int (x: int, y: int):<> int = "mac#%"
fun g0int_min_int (x: int, y: int):<> int = "mac#%"
fun g0int_isltz_int (x: int):<> bool = "mac#%"
fun g0int_isltez_int (x: int):<> bool = "mac#%"
fun g0int_isgtz_int (x: int):<> bool = "mac#%"
fun g0int_isgtez_int (x: int):<> bool = "mac#%"
fun g0int_iseqz_int (x: int):<> bool = "mac#%"
fun g0int_isneqz_int (x: int):<> bool = "mac#%"
fun g0uint_succ_uint (x: uint):<> uint = "mac#%"
fun g0uint_pred_uint (x: uint):<> uint = "mac#%"
fun g0uint_half_uint (x: uint):<> uint = "mac#%"
fun g0uint_add_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_sub_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_mul_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_div_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_mod_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_lsl_uint (x: uint, n: intGte(0)):<> uint = "mac#%"
fun g0uint_lsr_uint (x: uint, n: intGte(0)):<> uint = "mac#%"
fun g0uint_lnot_uint (x: uint):<> uint = "mac#%"
fun g0uint_lor_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_lxor_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_land_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_lt_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_lte_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_gt_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_gte_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_eq_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_neq_uint (x: uint, y: uint):<> bool = "mac#%"
fun g0uint_compare_uint (x: uint, y: uint):<> int = "mac#%"
fun g0uint_max_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_min_uint (x: uint, y: uint):<> uint = "mac#%"
fun g0uint_isgtz_uint (x: uint):<> bool = "mac#%"
fun g0uint_iseqz_uint (x: uint):<> bool = "mac#%"
fun g0uint_isneqz_uint (x: uint):<> bool = "mac#%"
fun g1int_neg_int : g1int_neg_type (intknd) = "mac#%"
fun g1int_abs_int : g1int_abs_type (intknd) = "mac#%"
fun g1int_succ_int : g1int_succ_type (intknd) = "mac#%"
fun g1int_pred_int : g1int_pred_type (intknd) = "mac#%"
fun g1int_half_int : g1int_half_type (intknd) = "mac#%"
fun g1int_add_int : g1int_add_type (intknd) = "mac#%"
fun g1int_sub_int : g1int_sub_type (intknd) = "mac#%"
fun g1int_mul_int : g1int_mul_type (intknd) = "mac#%"
fun g1int_div_int : g1int_div_type (intknd) = "mac#%"
fun g1int_nmod_int : g1int_nmod_type (intknd) = "mac#%"
fun g1int_lt_int : g1int_lt_type (intknd) = "mac#%"
fun g1int_lte_int : g1int_lte_type (intknd) = "mac#%"
fun g1int_gt_int : g1int_gt_type (intknd) = "mac#%"
fun g1int_gte_int : g1int_gte_type (intknd) = "mac#%"
fun g1int_eq_int : g1int_eq_type (intknd) = "mac#%"
fun g1int_neq_int : g1int_neq_type (intknd) = "mac#%"
fun g1int_compare_int : g1int_compare_type (intknd) = "mac#%"
fun g1int_max_int : g1int_max_type (intknd) = "mac#%"
fun g1int_min_int : g1int_min_type (intknd) = "mac#%"
fun g1int_isltz_int : g1int_isltz_type (intknd) = "mac#%"
fun g1int_isltez_int : g1int_isltez_type (intknd) = "mac#%"
fun g1int_isgtz_int : g1int_isgtz_type (intknd) = "mac#%"
fun g1int_isgtez_int : g1int_isgtez_type (intknd) = "mac#%"
fun g1int_iseqz_int : g1int_iseqz_type (intknd) = "mac#%"
fun g1int_isneqz_int : g1int_isneqz_type (intknd) = "mac#%"
fun g1uint_succ_uint : g1uint_succ_type (uintknd) = "mac#%"
fun g1uint_pred_uint : g1uint_pred_type (uintknd) = "mac#%"
fun g1uint_half_uint : g1uint_half_type (uintknd) = "mac#%"
fun g1uint_add_uint : g1uint_add_type (uintknd) = "mac#%"
fun g1uint_sub_uint : g1uint_sub_type (uintknd) = "mac#%"
fun g1uint_mul_uint : g1uint_mul_type (uintknd) = "mac#%"
fun g1uint_div_uint : g1uint_div_type (uintknd) = "mac#%"
fun g1uint_mod_uint : g1uint_mod_type (uintknd) = "mac#%"
fun g1uint_lt_uint : g1uint_lt_type (uintknd) = "mac#%"
fun g1uint_lte_uint : g1uint_lte_type (uintknd) = "mac#%"
fun g1uint_gt_uint : g1uint_gt_type (uintknd) = "mac#%"
fun g1uint_gte_uint : g1uint_gte_type (uintknd) = "mac#%"
fun g1uint_eq_uint : g1uint_eq_type (uintknd) = "mac#%"
fun g1uint_neq_uint : g1uint_neq_type (uintknd) = "mac#%"
fun g1uint_compare_uint : g1uint_compare_type (uintknd) = "mac#%"
fun g1uint_max_uint : g1uint_max_type (uintknd) = "mac#%"
fun g1uint_min_uint : g1uint_min_type (uintknd) = "mac#%"
fun g1uint_isgtz_uint : g1uint_isgtz_type (uintknd) = "mac#%"
fun g1uint_iseqz_uint : g1uint_iseqz_type (uintknd) = "mac#%"
fun g1uint_isneqz_uint : g1uint_isneqz_type (uintknd) = "mac#%"
macdef
i2u(x) = g1int2uint_int_uint(,(x))
macdef
u2i(x) = g1uint2int_uint_int(,(x))
macdef g0i2i(x) = g0int2int(,(x))
macdef g1i2i(x) = g1int2int(,(x))
macdef g0i2u(x) = g0int2uint(,(x))
macdef g1i2u(x) = g1int2uint(,(x))
macdef g0u2i(x) = g0uint2int(,(x))
macdef g1u2i(x) = g1uint2int(,(x))
macdef g0u2u(x) = g0uint2uint(,(x))
macdef g1u2u(x) = g1uint2uint(,(x))
fun{tk:tk}
listize_g0int_rep
{b:int | b >= 2}
(g0int(tk), int(b)):<!wrt> List0_vt(intBtw(0, b))
fun{tk:tk}
listize_g0uint_rep
{b:int | b >= 2}
(g0uint(tk), int(b)):<!wrt> List0_vt(intBtw(0, b))
sortdef tk = tkind
sortdef
t0p = t@ype and vt0p = viewt@ype
stadef ptrknd = ptr_kind
absprop is_word_aligned_p (l:addr)
castfn
g0ofg1_ptr (p: Ptr):<> ptr
castfn
g1ofg0_ptr (p: ptr):<> Ptr0
overload g0ofg1 with g0ofg1_ptr
overload g1ofg0 with g1ofg0_ptr
prfun
lemma_ptr_param
{l:addr} (p: ptr l): [l >= null] void
prfun
ptr_get_index
{l1:addr} (p: ptr l1): [l2:addr] EQADDR(l1, l2)
symintr ptr_is_null
symintr ptr_isnot_null
symintr add_ptr_bsz
symintr sub_ptr_bsz
symintr ptr_succ
symintr ptr_pred
symintr ptr_add ptr_sub
fun ptr0_is_null (p: ptr):<> bool = "mac#%"
overload ptr_is_null with ptr0_is_null of 0
fun ptr0_isnot_null (p: ptr):<> bool = "mac#%"
overload ptr_isnot_null with ptr0_isnot_null of 0
fun add_ptr0_bsz
(p: ptr, ofs: size_t):<> ptr = "mac#%"
fun sub_ptr0_bsz
(p: ptr, ofs: size_t):<> ptr = "mac#%"
overload add_ptr_bsz with add_ptr0_bsz of 0
overload sub_ptr_bsz with sub_ptr0_bsz of 0
fun sub_ptr0_ptr0
(p1: ptr, p2: ptr):<> ssize_t = "mac#%"
overload - with sub_ptr0_ptr0 of 0
fun{a:vt0p} ptr0_succ(p: ptr):<> ptr
fun{a:vt0p} ptr0_pred(p: ptr):<> ptr
overload ptr_succ with ptr0_succ of 0
overload ptr_pred with ptr0_pred of 0
fun{
a:vt0p
} ptr0_diff(p1: ptr, p2: ptr): ssize_t
fun{
a:vt0p}{tk:tk
} ptr0_add_gint(p: ptr, ofs: g0int(tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr0_add_guint(p: ptr, ofs: g0uint(tk)):<> ptr
overload ptr_add with ptr0_add_gint of 0
overload ptr_add with ptr0_add_guint of 0
fun{
a:vt0p}{tk:tk
} ptr0_sub_gint (p: ptr, ofs: g0int (tk)):<> ptr
fun{
a:vt0p}{tk:tk
} ptr0_sub_guint (p: ptr, ofs: g0uint (tk)):<> ptr
overload ptr_sub with ptr0_sub_gint of 0
overload ptr_sub with ptr0_sub_guint of 0
fun lt_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload < with lt_ptr0_ptr0 of 0
fun lte_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload <= with lte_ptr0_ptr0 of 0
fun gt_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload > with gt_ptr0_ptr0 of 0
fun gte_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload >= with gte_ptr0_ptr0 of 0
fun eq_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload = with eq_ptr0_ptr0 of 0
fun neq_ptr0_ptr0
(p1: ptr, p2: ptr):<> bool = "mac#%"
overload != with neq_ptr0_ptr0 of 0
overload <> with neq_ptr0_ptr0 of 0
fun
compare_ptr0_ptr0
(p1: ptr, p2: ptr):<> int = "mac#%"
overload compare with compare_ptr0_ptr0 of 0
fun
gt_ptr0_intz
(p: ptr, i: int(0)):<> bool = "mac#%"
fun
eq_ptr0_intz
(p: ptr, i: int(0)):<> bool = "mac#%"
fun
neq_ptr0_intz
(p: ptr, i: int(0)):<> bool = "mac#%"
overload > with gt_ptr0_intz of 0
overload = with eq_ptr0_intz of 0
overload != with neq_ptr0_intz of 0
overload <> with neq_ptr0_intz of 0
fun
print_ptr (p: ptr): void = "mac#%"
fun
prerr_ptr (p: ptr): void = "mac#%"
fun
fprint_ptr : fprint_type (ptr) = "mac#%"
overload print with print_ptr
overload prerr with prerr_ptr
overload fprint with fprint_ptr
praxi
ptr1_is_gtez
{l:addr}(p: ptr l): [l >= null] void
fun
ptr1_is_null
{l:addr}(p: ptr l):<> bool (l==null) = "mac#%"
fun
ptr1_isnot_null
{l:addr}(p: ptr l):<> bool (l > null) = "mac#%"
overload ptr_is_null with ptr1_is_null of 10
overload ptr_isnot_null with ptr1_isnot_null of 10
fun
add_ptr1_bsz{l:addr}{i:int}
(p: ptr l, ofs: size_t (i)):<> ptr (l+i) = "mac#%"
fun
sub_ptr1_bsz{l:addr}{i:int}
(p: ptr l, ofs: size_t (i)):<> ptr (l-i) = "mac#%"
overload add_ptr_bsz with add_ptr1_bsz of 20
overload sub_ptr_bsz with sub_ptr1_bsz of 20
fun
sub_ptr1_ptr1{l1,l2:addr}
(p1: ptr l1, p2: ptr l2):<> ssize_t (l1-l2) = "mac#%"
overload - with sub_ptr1_ptr1 of 20
fun{
a:vt0p
} ptr1_succ{l:addr} (p: ptr l):<> ptr (l+sizeof(a))
fun{
a:vt0p
} ptr1_pred{l:addr} (p: ptr l):<> ptr (l-sizeof(a))
overload ptr_succ with ptr1_succ of 10
overload ptr_pred with ptr1_pred of 10
fun{
a:vt0p}{tk:tk
} ptr1_add_gint
{l:addr}{i:int}
(p: ptr l, ofs: g1int (tk, i)):<> ptr(l+i*sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr1_add_guint
{l:addr}{i:int}
(p: ptr l, ofs: g1uint (tk, i)):<> ptr(l+i*sizeof(a))
overload ptr_add with ptr1_add_gint of 20
overload ptr_add with ptr1_add_guint of 20
fun{
a:vt0p}{tk:tk
} ptr1_sub_gint
{l:addr}{i:int}
(p: ptr l, ofs: g1int (tk, i)):<> ptr(l-i*sizeof(a))
fun{
a:vt0p}{tk:tk
} ptr1_sub_guint
{l:addr}{i:int}
(p: ptr l, ofs: g1uint (tk, i)):<> ptr(l-i*sizeof(a))
overload ptr_sub with ptr1_sub_gint of 20
overload ptr_sub with ptr1_sub_guint of 20
fun lt_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 < l2) = "mac#%"
overload < with lt_ptr1_ptr1 of 20
fun lte_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 <= l2) = "mac#%"
overload <= with lte_ptr1_ptr1 of 20
fun gt_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 > l2) = "mac#%"
overload > with gt_ptr1_ptr1 of 20
fun gte_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 >= l2) = "mac#%"
overload >= with gte_ptr1_ptr1 of 20
fun eq_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 == l2) = "mac#%"
overload = with eq_ptr1_ptr1 of 20
fun neq_ptr1_ptr1
{l1,l2:addr} (
p1: ptr (l1), p2: ptr (l2)
) :<> bool (l1 != l2) = "mac#%"
overload != with neq_ptr1_ptr1 of 20
overload <> with neq_ptr1_ptr1 of 20
fun compare_ptr1_ptr1
{l1,l2:addr} (p1: ptr l1, p2: ptr l2) :<> int = "mac#%"
overload compare with compare_ptr1_ptr1 of 20
fun
gt_ptr1_intz{l:addr}
(p: ptr(l), i: int(0)):<> bool(l > null) = "mac#%"
fun
eq_ptr1_intz{l:addr}
(p: ptr(l), i: int(0)):<> bool(l== null) = "mac#%"
fun
neq_ptr1_intz{l:addr}
(p: ptr(l), i: int(0)):<> bool(l > null) = "mac#%"
overload > with gt_ptr1_intz of 10
overload = with eq_ptr1_intz of 10
overload != with neq_ptr1_intz of 10
overload <> with neq_ptr1_intz of 10
fun{a:vt0p}
ptr_get{l:addr}
(pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a
fun{a:vt0p}
ptr_set{l:addr}
(pf: !a? @ l >> a @ l | p: ptr l, x: INV(a)):<!wrt> void
fun{a:vt0p}
ptr_exch{l:addr}
(pf: !INV(a) @ l | p: ptr l, x: &a >> a):<!wrt> void
abstype
cptr_vt0ype_addr_type
(a:vt@ype+, addr) = ptr
stadef cptr = cptr_vt0ype_addr_type
stadef cPtr0 (a:vt0p) = [l:addr] cptr (a, l)
stadef cPtr1 (a:vt0p) = [l:addr | l > null] cptr(a, l)
castfn
cptr2ptr{a:vt0p}{l:addr} (cp: cptr(a, l)):<> ptr(l)
fun cptr_null{a:vt0p} ():<> cptr(a, null) = "mac#%"
castfn cptr_rvar{a:vt0p} (x: &INV(a)):<> cPtr1(a)
castfn cptr_wvar{a:vt0p} (x: &a? >> a):<> cPtr1(a)
fun
{a:vt0p}
cptr_succ{l:addr}(cp: cptr(a, l)):<> cptr(a, l+sizeof(a))
fun
{a:vt0p}
cptr_pred{l:addr}(cp: cptr(a, l)):<> cptr(a, l-sizeof(a))
fun
cptr_is_null
{a:vt0p}{l:addr}(cp: cptr(a, l)):<> bool(l==null) = "mac#%"
fun
cptr_isnot_null
{a:vt0p}{l:addr}(cp: cptr(a, l)):<> bool(l > null) = "mac#%"
fun
gt_cptr_intz
{a:vt0p}{l:addr}
(cp: cptr(a, l), i: int(0)):<> bool(l > null) = "mac#%"
fun
eq_cptr_intz
{a:vt0p}{l:addr}
(cp: cptr(a, l), i: int(0)):<> bool(l== null) = "mac#%"
fun
neq_cptr_intz
{a:vt0p}{l:addr}
(cp: cptr(a, l), i: int(0)):<> bool(l > null) = "mac#%"
overload > with gt_cptr_intz of 0
overload = with eq_cptr_intz of 0
overload != with neq_cptr_intz of 0
overload <> with neq_cptr_intz of 0
typedef voidptr (l:addr) = cptr (void, l)
typedef voidptr0 = [l:addr] voidptr (l)
typedef voidptr1 = [l:addr | l > null] voidptr (l)
typedef charptr (l:addr) = cptr (char, l)
typedef charptr0 = [l:addr] charptr (l)
typedef charptr1 = [l:addr | l > null] charptr (l)
typedef constcharptr (l:addr) = charptr (l)
typedef constcharptr0 = charptr0
typedef constcharptr1 = charptr1
absprop
is_nullable(a: vt@ype+)
fun{a:vt0p}
ptr_nullize
(pf: is_nullable (a) | x: &a? >> a):<!wrt> void
fun
ptr_nullize_tsz{a:vt0p}
(
pf: is_nullable(a) | x: &a? >> a, tsz: sizeof_t(a)
) :<!wrt> void = "mac#%"
fun
{a:vt0p}
ptr_alloc()
:<> [l:agz] (a? @ l, mfree_gc_v(l) | ptr(l))
fun
ptr_alloc_tsz
{a:vt0p}(tsz: sizeof_t(a))
:<> [l:agz] (a? @ l, mfree_gc_v(l) | ptr(l)) = "mac#%"
fun
ptr_free{a:t@ype}{l:addr}
(pfgc: mfree_gc_v(l), pfat: a @ l | p: ptr(l)):<> void = "mac#%"
absvtype
ptrlin_vtype(l:addr) = ptr
vtypedef
ptrlin(l:addr) = ptrlin_vtype(l)
praxi ptrlin_free{l:addr} (p: ptrlin(l)): void
castfn ptr2ptrlin{l:addr} (p: ptr(l)):<> ptrlin(l)
castfn ptrlin2ptr{l:addr} (p: ptrlin(l)):<> ptr(l)
absvtype
aptr_vt0ype_addr_type
(a:vt@ype+, addr) = ptr
stadef aptr = aptr_vt0ype_addr_type
stadef aPtr0 (a:vt0p) = [l:addr] aptr(a, l)
stadef aPtr1 (a:vt0p) = [l:addr | l > null] aptr(a, l)
castfn
aptr2ptr{a:vt0p}{l:addr}(ap: !aptr(INV(a), l)):<> ptr(l)
fun
{a:vt0p}
aptr_make_elt(x: a):<!wrt> aPtr1(a)
fun
{a:vt0p}
aptr_getfree_elt{l:agz}(aptr(a, l)):<!wrt> (a)
fun
{a:vt0p}
aptr_get_elt
{l:agz}
(ap: !aptr(a, l) >> aptr(a?!, l)):<!wrt> (a)
fun
{a:vt0p}
aptr_set_elt
{l:agz}
(ap: !aptr(a?, l) >> aptr(a, l), x: a):<!wrt> void
fun
{a:vt0p}
aptr_exch_elt
{l:agz}
(ap: !aptr(INV(a), l) >> _, x: &(a) >> _):<!wrt> void
fun aptr_null{a:vt0p}():<> aptr(a, null) = "mac#%"
fun
aptr_is_null
{a:vt0p}{l:addr}
(ap: !aptr(INV(a), l)):<> bool(l==null) = "mac#%"
fun
aptr_isnot_null
{a:vt0p}{l:addr}
(ap: !aptr(INV(a), l)):<> bool(l > null) = "mac#%"
overload iseqz with aptr_is_null
overload isneqz with aptr_isnot_null
fun ptr_as_volatile (p: ptr): void
overload succ with ptr0_succ
overload succ with ptr1_succ
overload succ with cptr_succ
overload pred with ptr0_pred
overload pred with ptr1_pred
overload pred with cptr_pred
overload iseqz with ptr0_is_null of 0
overload isneqz with ptr0_isnot_null of 0
overload iseqz with ptr1_is_null of 10
overload isneqz with ptr1_isnot_null of 10
overload iseqz with cptr_is_null of 10
overload isneqz with cptr_isnot_null of 10
typedef bytes (n:int) = @[byte][n]
typedef b0ytes (n:int) = @[byte?][n]
viewdef bytes_v (l:addr, n:int) = bytes (n) @ l
viewdef b0ytes_v (l:addr, n:int) = b0ytes (n) @ l
praxi
b0ytes2bytes
{l:addr}{n:int} (&b0ytes(n) >> bytes(n)): void
praxi
b0ytes2bytes_v
{l:addr}{n:int} (pf: b0ytes_v (l, n)): bytes_v (l, n)
prfun
bytes_v_split
{l:addr}
{n:int}{i:nat | i <= n}
(pf: bytes_v (l, n)): (bytes_v (l, i), bytes_v (l+i, n-i))
prfun
bytes_v_split_at
{l:addr}
{n:int}{i:nat | i <= n}
(pf: bytes_v (l, n) | i: size_t (i)): (bytes_v (l, i), bytes_v (l+i, n-i))
prfun
bytes_v_unsplit
{l:addr}{n1,n2:int}
(pf1: bytes_v (l, n1), pf2: bytes_v (l+n1, n2)): bytes_v (l, n1+n2)
fun minit_gc (): void = "mac#%"
fun
mfree_gc
{l:addr}{n:int}
(
pfat: b0ytes n @ l
, pfgc: mfree_gc_v (l) | ptr l
) :<!wrt> void = "mac#%"
fun
malloc_gc
{n:int}
(
bsz: size_t (n)
) :<!wrt>
[l:agz]
(
b0ytes n @ l, mfree_gc_v (l) | ptr l
) = "mac#%"
absview memory$free_v (l:addr)
fun{
} memory$free
{l:addr}{n:int}
(
pfat: b0ytes n @ l
, pfmf: memory$free_v (l) | ptr l
) :<!wrt> void
fun{
} memory$alloc
{n:int}
(
bsz: size_t (n)
) :<!wrt>
[l:agz]
(
b0ytes n @ l, memory$free_v (l) | ptr l
)
castfn g0ofg1_bool (x: Bool):<> bool
castfn g1ofg0_bool (x: bool):<> Bool
overload g0ofg1 with g0ofg1_bool
overload g1ofg0 with g1ofg0_bool
fun
int2bool0 (i: int):<> bool = "mac#%"
fun
int2bool1
{i:int} (i: int i):<> bool(i != 0) = "mac#%"
symintr int2bool
overload int2bool with int2bool0 of 0
overload int2bool with int2bool1 of 10
fun
bool2int0 (b: bool):<> natLt(2) = "mac#%"
fun
bool2int1
{b:bool} (b: bool b):<> int(bool2int(b)) = "mac#%"
symintr bool2int
overload bool2int with bool2int0 of 0
overload bool2int with bool2int1 of 10
macdef || (b1, b2) = (if ,(b1) then true else ,(b2)): bool
macdef && (b1, b2) = (if ,(b1) then ,(b2) else false): bool
typedef boolLte (b: bool) = [a: bool | a <= b] bool (a)
typedef boolGte (b: bool) = [a: bool | a >= b] bool (a)
fun
neg_bool0
(b: bool):<> bool = "mac#%"
overload ~ with neg_bool0 of 0
overload not with neg_bool0 of 0
fun
add_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
fun
mul_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload + with add_bool0_bool0 of 0
overload * with mul_bool0_bool0 of 0
fun
xor_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload xor with xor_bool0_bool0 of 0
fun
lt_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload < with lt_bool0_bool0 of 0
fun
lte_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload <= with lte_bool0_bool0 of 0
fun
gt_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload > with gt_bool0_bool0 of 0
fun
gte_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload >= with gte_bool0_bool0 of 0
fun
eq_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload = with eq_bool0_bool0 of 0
fun
neq_bool0_bool0
(b1: bool, b2: bool):<> bool = "mac#%"
overload != with neq_bool0_bool0 of 0
overload <> with neq_bool0_bool0 of 0
fun compare_bool0_bool0
(b1: bool, b2: bool):<> Sgn = "mac#%"
overload compare with compare_bool0_bool0
fun
bool2string(b: bool):<> string = "mac#%"
fun print_bool (x: bool): void = "mac#%"
fun prerr_bool (x: bool): void = "mac#%"
fun fprint_bool : fprint_type (bool) = "mac#%"
overload print with print_bool
overload prerr with prerr_bool
overload fprint with fprint_bool
fun
neg_bool1
{b:bool}
(b: bool b):<> bool (~b) = "mac#%"
overload ~ with neg_bool1 of 10
overload not with neg_bool1 of 10
fun
add_bool0_bool1
{b2:bool}
(
b1: bool, b2: bool b2
) :<> [b1:bool] bool(b1 || b2) = "mac#%"
overload + with add_bool0_bool1 of 10
fun
add_bool1_bool0
{b1:bool}
(
b1: bool b1, b2: bool
) :<> [b2:bool] bool(b1 || b2) = "mac#%"
overload + with add_bool1_bool0 of 10
fun
add_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool(b1 || b2) = "mac#%"
overload + with add_bool1_bool1 of 20
fun
mul_bool0_bool1
{b2:bool}
(
b1: bool, b2: bool b2
) :<> [b1:bool] bool(b1 && b2) = "mac#%"
overload * with mul_bool0_bool1 of 10
fun
mul_bool1_bool0
{b1:bool}
(
b1: bool b1, b2: bool
) :<> [b2:bool] bool(b1 && b2) = "mac#%"
overload * with mul_bool1_bool0 of 10
fun
mul_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool(b1 && b2) = "mac#%"
overload * with mul_bool1_bool1 of 20
fun
xor_bool1_bool1
{b1,b2:bool}
(b1: bool b1, b2: bool b2):<> bool((b1)==(~b2)) = "mac#%"
overload xor with xor_bool1_bool1 of 20
fun
lt_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 < b2) = "mac#%"
overload < with lt_bool1_bool1 of 20
fun
lte_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 <= b2) = "mac#%"
overload <= with lte_bool1_bool1 of 20
fun
gt_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 > b2) = "mac#%"
overload > with gt_bool1_bool1 of 20
fun
gte_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 >= b2) = "mac#%"
overload >= with gte_bool1_bool1 of 20
fun
eq_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 == b2) = "mac#%"
overload = with eq_bool1_bool1 of 20
fun
neq_bool1_bool1 {b1,b2:bool}
(b1: bool (b1), b2: bool (b2)) :<> bool (b1 != b2) = "mac#%"
overload != with neq_bool1_bool1 of 20
overload <> with neq_bool1_bool1 of 20
fun
compare_bool1_bool1
{b1,b2:bool}
(
b1: bool b1, b2: bool b2
) :<> int (bool2int(b1) - bool2int(b2)) = "mac#%"
overload compare with compare_bool1_bool1 of 20
praxi
lemma_char_size
(
) : [sizeof(char)==sizeof(byte)] void
praxi
lemma_schar_size
(
) : [sizeof(schar)==sizeof(byte)] void
praxi
lemma_uchar_size
(
) : [sizeof(uchar)==sizeof(byte)] void
castfn char2schar0(c: char):<> schar
castfn schar2char0(c: schar):<> char
castfn char2uchar0(c: char):<> uchar
castfn uchar2char0(c: uchar):<> char
fun int2char0(i: int):<> char = "mac#%"
fun int2schar0(i: int):<> schar = "mac#%"
fun int2uchar0(i: int):<> uchar = "mac#%"
fun uint2uchar0(u: uint):<> uchar = "mac#%"
fun char2int0(c: char):<> int = "mac#%"
fun schar2int0(c: schar):<> int = "mac#%"
fun uchar2int0(c: uchar):<> int = "mac#%"
fun char2uint0(c: char):<> uint = "mac#%"
fun schar2uint0(c: schar):<> uint = "mac#%"
fun uchar2uint0(c: uchar):<> uint = "mac#%"
fun char2u2int0(c: char):<> int = "mac#%"
fun char2u2uint0(c: char):<> uint = "mac#%"
fun
char0_iseqz(c: char):<> bool = "mac#%"
fun
char0_isneqz(c: char):<> bool = "mac#%"
overload iseqz with char0_iseqz of 0
overload isneqz with char0_isneqz of 0
fun add_char0_int0
(c: char, i: int):<> char = "mac#%"
fun sub_char0_int0
(c: char, i: int):<> char = "mac#%"
fun sub_char0_char0
(c1: char, c2: char):<> int = "mac#%"
overload + with add_char0_int0 of 0
overload - with sub_char0_int0 of 0
overload - with sub_char0_char0 of 0
fun lt_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload < with lt_char0_char0 of 0
fun lte_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload <= with lte_char0_char0 of 0
fun gt_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload > with gt_char0_char0 of 0
fun gte_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload >= with gte_char0_char0 of 0
fun eq_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload = with eq_char0_char0 of 0
fun neq_char0_char0
(c1: char, c2: char):<> bool = "mac#%"
overload != with neq_char0_char0 of 0
overload <> with neq_char0_char0 of 0
fun compare_char0_char0
(c1: char, c2: char):<> int = "mac#%"
overload compare with compare_char0_char0 of 0
castfn g0ofg1_char(c: Char):<> char
castfn g1ofg0_char(c: char):<> Char
overload g0ofg1 with g0ofg1_char
overload g1ofg0 with g1ofg0_char
castfn
char2schar1
{c:int}(c: char(c)):<> schar(c)
castfn
schar2char1
{c:int}(c: schar(c)):<> char(c)
castfn
char2uchar1
{c:int}(c: char(c)):<> uchar(i2u8(c))
castfn
uchar2char1
{c:int}(c: uchar(c)):<> char(u2i8(c))
fun
char2int1
{c:int}(c: char(c)):<> int(c) = "mac#%"
fun
schar2int1
{c:int}(c: schar(c)):<> int(c) = "mac#%"
fun
uchar2int1
{c:int}(c: uchar(c)):<> int(c) = "mac#%"
fun
char1_iseqz
{c:int}(c: char(c)):<> bool(c == 0) = "mac#%"
fun
char1_isneqz
{c:int}(c: char(c)):<> bool(c != 0) = "mac#%"
overload iseqz with char1_iseqz of 10
overload isneqz with char1_isneqz of 10
fun
lt_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 < c2) = "mac#%"
overload < with lt_char1_char1 of 20
fun
lte_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 <= c2) = "mac#%"
overload <= with lte_char1_char1 of 20
fun
gt_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 > c2) = "mac#%"
overload > with gt_char1_char1 of 20
fun
gte_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 >= c2) = "mac#%"
overload >= with gte_char1_char1 of 20
fun
eq_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 == c2) = "mac#%"
overload = with eq_char1_char1 of 20
fun
neq_char1_char1
{c1,c2:int}
(c1: char(c1), c2: char(c2)):<> bool(c1 != c2) = "mac#%"
overload != with neq_char1_char1 of 20
overload <> with neq_char1_char1 of 20
fun compare_char1_char1
{c1,c2:int}
(c1: char c1, c2: char c2) :<> int(c1-c2) = "mac#%"
overload compare with compare_char1_char1 of 20
fun eq_char0_int0 : (char, int) -<fun0> bool = "mac#%"
fun eq_int0_char0 : (int, char) -<fun0> bool = "mac#%"
overload = with eq_char0_int0 of 0
overload = with eq_int0_char0 of 0
fun neq_char0_int0 : (char, int) -<fun0> bool = "mac#%"
fun neq_int0_char0 : (int, char) -<fun0> bool = "mac#%"
overload != with neq_char0_int0 of 0
overload <> with neq_char0_int0 of 0
overload != with neq_int0_char0 of 0
overload <> with neq_int0_char0 of 0
fun compare_char0_int0 : (char, int) -<fun0> int = "mac#%"
fun compare_int0_char0 : (int, char) -<fun0> int = "mac#%"
overload compare with compare_char0_int0
overload compare with compare_int0_char0
fun lt_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload < with lt_uchar0_uchar0 of 0
fun lte_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload <= with lte_uchar0_uchar0 of 0
fun gt_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload > with gt_uchar0_uchar0 of 0
fun gte_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload >= with gte_uchar0_uchar0 of 0
fun eq_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload = with eq_uchar0_uchar0 of 0
fun neq_uchar0_uchar0
(c1: uchar, c2: uchar):<> bool = "mac#%"
overload != with neq_uchar0_uchar0 of 0
overload <> with neq_uchar0_uchar0 of 0
fun compare_uchar0_uchar0
(c1: uchar, c2: uchar):<> int = "mac#%"
overload compare with compare_uchar0_uchar0 of 0
fun
lt_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 < c2) = "mac#%"
overload < with lt_uchar1_uchar1 of 20
fun
lte_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 <= c2) = "mac#%"
overload <= with lte_uchar1_uchar1 of 20
fun
gt_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 > c2) = "mac#%"
overload > with gt_uchar1_uchar1 of 20
fun
gte_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 >= c2) = "mac#%"
overload >= with gte_uchar1_uchar1 of 20
fun
eq_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 == c2) = "mac#%"
overload = with eq_uchar1_uchar1 of 20
fun
neq_uchar1_uchar1
{c1,c2:int}
(c1: uchar(c1), c2: uchar(c2)) :<> bool(c1 != c2) = "mac#%"
overload != with neq_uchar1_uchar1 of 20
overload <> with neq_uchar1_uchar1 of 20
fun compare_uchar1_uchar1
{c1,c2:int}
(c1: uchar c1, c2: uchar c2) :<> int(c1-c2) = "mac#%"
overload compare with compare_uchar1_uchar1 of 20
sortdef tk = tkind
fun{tk:tk}
g0int_of_char(c: char):<> g0int(tk)
fun{tk:tk}
g0int_of_schar(c: schar):<> g0int(tk)
fun{tk:tk}
g0int_of_uchar(c: uchar):<> g0int(tk)
fun{tk:tk}
g0uint_of_uchar(c: uchar):<> g0uint(tk)
fun{tk:tk}
g1int_of_char1
{c:int} (c: char(c)):<> g1int(tk, c)
fun{tk:tk}
g1int_of_schar1
{c:int} (c: schar(c)):<> g1int(tk, c)
fun{tk:tk}
g1int_of_uchar1
{c:int} (c: uchar(c)):<> g1int(tk, c)
fun{tk:tk}
g1uint_of_uchar1
{c:int} (c: uchar(c)):<> g1uint(tk, c)
fun{}
char2string(c: char):<> string
fun{}
char2strptr(c: char):<!wrt> Strptr1
fun print_char(x: char): void = "mac#%"
fun prerr_char(x: char): void = "mac#%"
overload print with print_char
overload prerr with prerr_char
fun fprint_char : fprint_type (char) = "mac#%"
overload fprint with fprint_char
fun print_schar(x: schar): void = "mac#%"
fun prerr_schar(x: schar): void = "mac#%"
overload print with print_schar
overload prerr with prerr_schar
fun fprint_schar : fprint_type (schar) = "mac#%"
overload fprint with fprint_schar
fun print_uchar(x: uchar): void = "mac#%"
fun prerr_uchar(x: uchar): void = "mac#%"
overload print with print_uchar
overload prerr with prerr_uchar
fun fprint_uchar : fprint_type (uchar) = "mac#%"
overload fprint with fprint_uchar
fun isalpha_int(c: int):<> bool = "mac#%"
fun isalpha_char(c: char):<> bool = "mac#%"
symintr isalpha
overload isalpha with isalpha_int of 0
overload isalpha with isalpha_char of 0
fun isalnum_int(c: int):<> bool = "mac#%"
fun isalnum_char(c: char):<> bool = "mac#%"
symintr isalnum
overload isalnum with isalnum_int of 0
overload isalnum with isalnum_char of 0
fun isascii_int(c: int):<> bool = "mac#%"
fun isascii_char(c: char):<> bool = "mac#%"
symintr isascii
overload isascii with isascii_int of 0
overload isascii with isascii_char of 0
fun isblank_int(c: int):<> bool = "mac#%"
fun isblank_char(c: char):<> bool = "mac#%"
symintr isblank
overload isblank with isblank_int of 0
overload isblank with isblank_char of 0
fun isspace_int(c: int):<> bool = "mac#%"
fun isspace_char(c: char):<> bool = "mac#%"
symintr isspace
overload isspace with isspace_int of 0
overload isspace with isspace_char of 0
fun iscntrl_int(c: int):<> bool = "mac#%"
fun iscntrl_char(c: char):<> bool = "mac#%"
symintr iscntrl
overload iscntrl with iscntrl_int of 0
overload iscntrl with iscntrl_char of 0
fun isdigit_int(c: int):<> bool = "mac#%"
fun isdigit_char(c: char):<> bool = "mac#%"
symintr isdigit
overload isdigit with isdigit_int of 0
overload isdigit with isdigit_char of 0
fun isxdigit_int(c: int):<> bool = "mac#%"
fun isxdigit_char(c: char):<> bool = "mac#%"
symintr isxdigit
overload isxdigit with isxdigit_int of 0
overload isxdigit with isxdigit_char of 0
fun isgraph_int(c: int):<> bool = "mac#%"
fun isgraph_char(c: char):<> bool = "mac#%"
symintr isgraph
overload isgraph with isgraph_int of 0
overload isgraph with isgraph_char of 0
fun isprint_int(c: int):<> bool = "mac#%"
fun isprint_char(c: char):<> bool = "mac#%"
symintr isprint
overload isprint with isprint_int of 0
overload isprint with isprint_char of 0
fun ispunct_int(c: int):<> bool = "mac#%"
fun ispunct_char(c: char):<> bool = "mac#%"
symintr ispunct
overload ispunct with ispunct_int of 0
overload ispunct with ispunct_char of 0
fun islower_int(c: int):<> bool = "mac#%"
fun islower_char(c: char):<> bool = "mac#%"
symintr islower
overload islower with islower_int of 0
overload islower with islower_char of 0
fun isupper_int(c: int):<> bool = "mac#%"
fun isupper_char(c: char):<> bool = "mac#%"
symintr isupper
overload isupper with isupper_int of 0
overload isupper with isupper_char of 0
fun toascii (c: int):<> int = "mac#%"
symintr tolower
fun tolower_int(c: int):<> int = "mac#%"
fun tolower_char(c: char):<> char = "mac#%"
overload tolower with tolower_int
overload tolower with tolower_char
symintr toupper
fun toupper_int(c: int):<> int = "mac#%"
fun toupper_char(c: char):<> char = "mac#%"
overload toupper with toupper_int
overload toupper with toupper_char
fun int2digit (i: intBtw(0, 10)): char = "mac#%"
fun int2xdigit (i: intBtw(0, 16)): char = "mac#%"
fun int2xxdigit (i: intBtw(0, 16)): char = "mac#%"
symintr c2uc
overload c2uc with char2uchar0 of 0
overload c2uc with char2uchar1 of 10
symintr uc2c
overload uc2c with uchar2char0 of 0
overload uc2c with uchar2char1 of 10
symintr char2i
overload char2i with char2int0 of 0
symintr char2ui
overload char2ui with char2uint0 of 0
symintr uchar2i
overload uchar2i with uchar2int0 of 0
symintr uchar2ui
overload uchar2ui with uchar2uint0 of 0
symintr char2u2i
overload char2u2i with char2u2int0 of 0
symintr char2u2ui
overload char2u2ui with char2u2uint0 of 0
fun int2byte0(i: int): byte = "mac#%"
fun byte2int0(b: byte):<> int = "mac#%"
fun uint2byte0(u: uint): byte = "mac#%"
fun byte2uint0(b: byte):<> uint = "mac#%"
symintr byte2i
overload byte2i with byte2int0 of 0
symintr i2byte
overload i2byte with int2byte0 of 0
symintr byte2ui
overload byte2i with byte2uint0 of 0
symintr ui2byte
overload i2byte with uint2byte0 of 0
stadef fltknd = float_kind
stadef dblknd = double_kind
stadef ldblknd = ldouble_kind
fun
{tk1,tk2:tk}
g0int2float(x: g0int(tk1)):<> g0float(tk2)
fun
g0int2float_int_float(x: int):<> float = "mac#%"
fun
g0int2float_int_double(x: int):<> double = "mac#%"
fun
g0int2float_lint_double(x: lint):<> double = "mac#%"
fun
{tk1,tk2:tk}
g0float2int(x: g0float(tk1)):<> g0int(tk2)
fun
g0float2int_float_int(x: float):<> int = "mac#%"
fun
g0float2int_float_lint(x: float):<> lint = "mac#%"
fun
g0float2int_double_int(x: double):<> int = "mac#%"
fun
g0float2int_double_lint(x: double):<> lint = "mac#%"
fun
g0float2int_double_llint(x: double):<> llint = "mac#%"
fun
{tk1,tk2:tk}
g0float2float(x: g0float(tk1)):<> g0float(tk2)
fun
g0float2float_float_float(x: float):<> float = "mac#%"
fun
g0float2float_float_double(x: float):<> double = "mac#%"
fun
g0float2float_double_float(x: double):<> float = "mac#%"
fun
g0float2float_double_double(x: double):<> double = "mac#%"
fun
{tk:tk}
g0string2float(rep: NSH(string)):<> g0float(tk)
fun
g0string2float_double(rep: NSH(string)):<> double = "mac#%"
typedef
g0float_uop_type
(tk:tk) =
g0float(tk) -<fun0> g0float(tk)
fun
{tk:tk}
g0float_abs : g0float_uop_type(tk)
fun
{tk:tk}
g0float_neg : g0float_uop_type(tk)
overload abs with g0float_abs of 0
overload ~ with g0float_neg of 0
overload neg with g0float_neg of 0
fun
{tk:tk}
g0float_succ : g0float_uop_type(tk)
fun
{tk:tk}
g0float_pred : g0float_uop_type(tk)
overload succ with g0float_succ of 0
overload pred with g0float_pred of 0
typedef
g0float_aop_type
(tk:tk) =
(g0float(tk), g0float(tk)) -<fun0> g0float(tk)
fun
{tk:tk}
g0float_add : g0float_aop_type(tk)
overload + with g0float_add of 0
fun
{tk:tk}
g0float_sub : g0float_aop_type(tk)
overload - with g0float_sub of 0
fun
{tk:tk}
g0float_mul : g0float_aop_type(tk)
overload * with g0float_mul of 0
fun
{tk:tk}
g0float_div : g0float_aop_type(tk)
overload / with g0float_div of 0
fun
{tk:tk}
g0float_mod : g0float_aop_type(tk)
overload % with g0float_mod of 0
overload mod with g0float_mod of 0
fun
{tk:tk}
g0float_isltz(g0float(tk)):<> bool
fun
{tk:tk}
g0float_isltez(g0float(tk)):<> bool
overload isltz with g0float_isltz of 0
overload isltez with g0float_isltez of 0
fun
{tk:tk}
g0float_isgtz(g0float(tk)):<> bool
fun
{tk:tk}
g0float_isgtez(g0float(tk)):<> bool
overload isgtz with g0float_isgtz of 0
overload isgtez with g0float_isgtez of 0
fun
{tk:tk}
g0float_iseqz(g0float(tk)):<> bool
fun
{tk:tk}
g0float_isneqz(g0float(tk)):<> bool
overload iseqz with g0float_iseqz of 0
overload isneqz with g0float_isneqz of 0
typedef
g0float_cmp_type
(tk:tk) =
(g0float(tk), g0float(tk)) -<fun0> bool
fun
{tk:tk}
g0float_lt : g0float_cmp_type(tk)
overload < with g0float_lt of 0
fun
{tk:tk}
g0float_lte : g0float_cmp_type(tk)
overload <= with g0float_lte of 0
fun
{tk:tk}
g0float_gt : g0float_cmp_type(tk)
overload > with g0float_gt of 0
fun
{tk:tk}
g0float_gte : g0float_cmp_type(tk)
overload >= with g0float_gte of 0
fun
{tk:tk}
g0float_eq : g0float_cmp_type(tk)
overload = with g0float_eq of 0
fun
{tk:tk}
g0float_neq : g0float_cmp_type(tk)
overload != with g0float_neq of 0
overload <> with g0float_neq of 0
typedef
g0float_compare_type
(tk:tk) =
(g0float(tk), g0float(tk)) -<fun0> int
fun
{tk:tk}
g0float_compare
: g0float_compare_type(tk)
overload compare with g0float_compare of 0
fun
{tk:tk}
g0float_max : g0float_aop_type(tk)
fun
{tk:tk}
g0float_min : g0float_aop_type(tk)
overload max with g0float_max of 0
overload min with g0float_min of 0
fun g0float_neg_float
: g0float_uop_type(fltknd) = "mac#%"
fun g0float_abs_float
: g0float_uop_type(fltknd) = "mac#%"
fun g0float_succ_float
: g0float_uop_type(fltknd) = "mac#%"
fun g0float_pred_float
: g0float_uop_type(fltknd) = "mac#%"
fun g0float_add_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_sub_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_mul_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_div_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_mod_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_lt_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_lte_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_gt_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_gte_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_eq_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_neq_float
: g0float_cmp_type(fltknd) = "mac#%"
fun g0float_compare_float
: g0float_compare_type(fltknd) = "mac#%"
fun g0float_max_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_min_float
: g0float_aop_type(fltknd) = "mac#%"
fun g0float_neg_double
: g0float_uop_type(dblknd) = "mac#%"
fun g0float_abs_double
: g0float_uop_type(dblknd) = "mac#%"
fun g0float_succ_double
: g0float_uop_type(dblknd) = "mac#%"
fun g0float_pred_double
: g0float_uop_type(dblknd) = "mac#%"
fun g0float_add_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_sub_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_mul_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_div_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_mod_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_lt_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_lte_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_gt_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_gte_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_eq_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_neq_double
: g0float_cmp_type(dblknd) = "mac#%"
fun g0float_compare_double
: g0float_compare_type(dblknd) = "mac#%"
fun g0float_max_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_min_double
: g0float_aop_type(dblknd) = "mac#%"
fun g0float_neg_ldouble
: g0float_uop_type(ldblknd) = "mac#%"
fun g0float_abs_ldouble
: g0float_uop_type(ldblknd) = "mac#%"
fun g0float_succ_ldouble
: g0float_uop_type(ldblknd) = "mac#%"
fun g0float_pred_ldouble
: g0float_uop_type(ldblknd) = "mac#%"
fun g0float_add_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_sub_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_mul_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_div_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_mod_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_lt_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_lte_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_gt_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_gte_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_eq_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_neq_ldouble
: g0float_cmp_type(ldblknd) = "mac#%"
fun g0float_compare_ldouble
: g0float_compare_type(ldblknd) = "mac#%"
fun g0float_max_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun g0float_min_ldouble
: g0float_aop_type(ldblknd) = "mac#%"
fun print_float (float): void = "mac#%"
fun prerr_float (float): void = "mac#%"
fun fprint_float : fprint_type (float) = "mac#%"
overload print with print_float
overload prerr with prerr_float
overload fprint with fprint_float
fun print_double (double): void = "mac#%"
fun prerr_double (double): void = "mac#%"
fun fprint_double : fprint_type (double) = "mac#%"
overload print with print_double
overload prerr with prerr_double
overload fprint with fprint_double
fun print_ldouble (ldouble): void = "mac#%"
fun prerr_ldouble (ldouble): void = "mac#%"
fun fprint_ldouble : fprint_type (ldouble) = "mac#%"
overload print with print_ldouble
overload prerr with prerr_ldouble
overload fprint with fprint_ldouble
fun
add_int_float
(int, float):<> float = "mac#%"
fun
add_float_int
(float, int):<> float = "mac#%"
overload + with add_int_float of 0
overload + with add_float_int of 0
fun
add_int_double
(int, double):<> double = "mac#%"
fun
add_double_int
(double, int):<> double = "mac#%"
overload + with add_int_double of 0
overload + with add_double_int of 0
fun
sub_int_float
(int, float):<> float = "mac#%"
fun
sub_float_int
(float, int):<> float = "mac#%"
overload - with sub_int_float of 0
overload - with sub_float_int of 0
fun
sub_int_double
(int, double):<> double = "mac#%"
fun
sub_double_int
(double, int):<> double = "mac#%"
overload - with sub_int_double of 0
overload - with sub_double_int of 0
fun
mul_int_float
(int, float):<> float = "mac#%"
fun
mul_float_int
(float, int):<> float = "mac#%"
overload * with mul_int_float of 0
overload * with mul_float_int of 0
fun
mul_int_double
(int, double):<> double = "mac#%"
fun
mul_double_int
(double, int):<> double = "mac#%"
overload * with mul_int_double of 0
overload * with mul_double_int of 0
fun
div_int_float
(int, float):<> float = "mac#%"
fun
div_float_int
(float, int):<> float = "mac#%"
overload / with div_int_float of 0
overload / with div_float_int of 0
fun
div_int_double
(int, double):<> double = "mac#%"
fun
div_double_int
(double, int):<> double = "mac#%"
overload / with div_int_double of 0
overload / with div_double_int of 0
fun
{tk:tk}
g0float_npow
(x: g0float(tk), n: intGte(0)):<> g0float(tk)
overload ** with g0float_npow of 0
macdef g0i2f (x) = g0int2float (,(x))
macdef g0f2i (x) = g0float2int (,(x))
macdef g0f2f (x) = g0float2float (,(x))
sortdef tk = tkind
typedef SHR(a:type) = a
typedef NSH(a:type) = a
typedef
stringLt(n:int) = [k:nat | k < n] string(k)
typedef
stringLte(n:int) = [k:nat | k <= n] string(k)
typedef
stringGt(n:int) = [k:int | k > n] string(k)
typedef
stringGte(n:int) = [k:int | k >= n] string(k)
typedef
stringBtw
(m:int, n:int) = [k:int | m <= k; k < n] string(k)
typedef
stringBtwe
(m:int, n:int) = [k:int | m <= k; k <= n] string(k)
typedef stringlst = List0(string)
vtypedef stringlst_vt = List0_vt(string)
typedef stringopt = Option(string)
dataprop
string_index_p
(
n: int, int, int
) =
| string_index_p_eqz(n, n, 0)
| {i:int | n > i}
{c:int8 | c != 0}
string_index_p_neqz(n, i, c)
exception StringSubscriptExn of ()
praxi
lemma_string_param{n:int}(string n): [n >= 0] void
castfn
string2ptr (x: string):<> Ptr1
overload ptrcast with string2ptr
castfn g0ofg1_string (x: String):<> string
castfn g1ofg0_string (x: string):<> String0
overload g0ofg1 with g0ofg1_string
overload g1ofg0 with g1ofg0_string
fun{}
string_char (str: string):<> char
fun{}
string_nil():<!wrt> strnptr(0)
fun{}
string_sing(chr: charNZ):<!wrt> strnptr(1)
fun{}
string_is_empty
{n:int}(str: string(n)):<> bool(n==0)
fun{}
string_isnot_empty
{n:int}(str: string(n)):<> bool(n > 0)
fun{}
string_is_atend_size
{n:int}{i:nat | i <= n}
(s: string(n), i: size_t(i)):<> bool(i==n)
fun{tk:tk}
string_is_atend_gint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1int(tk, i)):<> bool(i==n)
fun{tk:tk}
string_is_atend_guint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1uint(tk, i)):<> bool(i==n)
symintr string_is_atend
overload string_is_atend with string_is_atend_gint
overload string_is_atend with string_is_atend_guint
macdef
string_isnot_atend
(string, index) = ~string_is_atend (,(string), ,(index))
fun{}
string_head{n:pos} (str: string(n)):<> charNZ
fun{}
string_tail{n:pos} (str: string(n)):<> string(n-1)
fun{}
string_get_at_size
{n:int}{i:nat | i < n}
(s: string(n), i: size_t(i)):<> charNZ
fun{tk:tk}
string_get_at_gint
{n:int}{i:nat | i < n}
(s: string(n), i: g1int(tk, i)):<> charNZ
fun{tk:tk}
string_get_at_guint
{n:int}{i:nat | i < n}
(s: string(n), i: g1uint(tk, i)):<> charNZ
symintr string_get_at
overload string_get_at with string_get_at_size of 1
overload string_get_at with string_get_at_gint of 0
overload string_get_at with string_get_at_guint of 0
fun{}
string_test_at_size
{n:int}{i:nat | i <= n}
(s: string(n), i: size_t(i)):<> [c:int] (string_index_p(n, i, c) | char(c))
fun{tk:tk}
string_test_at_gint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1int(tk, i)):<> [c:int] (string_index_p(n, i, c) | char(c))
fun{tk:tk}
string_test_at_guint
{n:int}{i:nat | i <= n}
(s: string(n), i: g1uint(tk, i)):<> [c:int] (string_index_p(n, i, c) | char(c))
symintr string_test_at
overload string_test_at with string_test_at_size of 1
overload string_test_at with string_test_at_gint of 0
overload string_test_at with string_test_at_guint of 0
fun lt_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload < with lt_string_string
fun lte_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload <= with lte_string_string
fun gt_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload > with gt_string_string
fun gte_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload >= with gte_string_string
fun eq_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload = with eq_string_string
fun neq_string_string
(x1: string, x2: string):<> bool = "mac#%"
overload != with neq_string_string
overload <> with neq_string_string
fun compare_string_string
(x1: string, x2: string):<> Sgn = "mac#%"
overload compare with compare_string_string
fun{
} strcmp (x1: string, x2: string):<> int
fun{
} strintcmp
{n1,n2:int | n2 >=0}
(x1: string n1, n2: int n2):<> int(sgn(n1-n2))
fun{
} strlencmp
{n1,n2:int}
(x1: string n1, x2: string n2):<> int(sgn(n1-n2))
fun{}
string_make_list
{n:int}
(cs: list(charNZ, n)):<!wrt> strnptr(n)
fun{}
string_make_listlen
{n:int}
(cs: list(charNZ, n), n: int(n)):<!wrt> strnptr(n)
fun{}
string_make_rlist
{n:int}
(cs: list(charNZ, n)):<!wrt> strnptr(n)
fun{}
string_make_rlistlen
{n:int}
(cs: list(charNZ, n), n: int(n)):<!wrt> strnptr(n)
fun{}
string_make_list_vt
{n:int}
(cs: list_vt(charNZ, n)):<!wrt> strnptr(n)
fun{}
string_make_listlen_vt
{n:int}
(cs: list_vt(charNZ, n), n: int(n)):<!wrt> strnptr(n)
fun{}
string_make_rlist_vt
{n:int}
(cs: list_vt(charNZ, n)):<!wrt> strnptr(n)
fun{}
string_make_rlistlen_vt
{n:int}
(cs: list_vt(charNZ, n), n: int(n)):<!wrt> strnptr(n)
fun{}
string_make_stream
{n:int}(cs: stream(charNZ)):<!wrt> Strptr1
fun{}
string_make_stream_vt
{n:int}(cs: stream_vt(charNZ)):<!wrt> Strptr1
fun{}
string_make_stream$bufsize
():<> intGte(1)
fun{}
string_make_substring
{n:int}{st,ln:nat | st+ln <= n}
(str: string(n), st: size_t st, ln: size_t ln):<!wrt> strnptr(ln)
fun
print_string(x: string): void = "mac#%"
fun
prerr_string(x: string): void = "mac#%"
fun
fprint_string(out: FILEref, x: string): void = "mac#%"
fun
fprint_substring
{n:int}{st,ln:nat | st+ln <= n}
(
out: FILEref, str: string(n), st: size_t(st), ln: size_t(ln)
) : void = "mac#%"
fun{}
strchr{n:int}
(str: string(n), c0: char):<> ssizeBtwe(~1, n)
fun{}
strrchr{n:int}
(str: string(n), c0: char):<> ssizeBtwe(~1, n)
fun{}
strstr{n:int}
(haystack: string(n), needle: string):<> ssizeBtw(~1, n)
fun{}
strspn{n:int}
(str: string(n), accept: string):<> sizeLte(n)
fun{}
strcspn{n:int}
(str: string(n), accept: string):<> sizeLte(n)
fun{
} string_index{n:int}
(str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
fun{
} string_rindex{n:int}
(str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
fun{}
string0_length
(x: NSH(string)):<> size_t
fun{}
string1_length
{n:int} (x: NSH(string(n))):<> size_t(n)
symintr strlen
symintr string_length
overload strlen with string0_length of 0
overload strlen with string1_length of 10
overload string_length with string0_length of 0
overload string_length with string1_length of 10
fun{}
string0_nlength
(x: NSH(string), n: size_t):<> size_t
fun{}
string1_nlength
{n1,n2:int}
(NSH(string(n1)), size_t(n2)):<> size_t(min(n1,n2))
symintr string_nlength
overload string_nlength with string0_nlength of 0
overload string_nlength with string1_nlength of 10
fun{}
string0_copy
(cs: NSH(string)):<!wrt> Strptr1
fun{}
string1_copy
{n:int}
(cs: NSH(string(n))):<!wrt> strnptr(n)
fun{}
string_fset_at_size
{n:int}{i:nat | i < n}
(NSH(string(n)), i: size_t(i), c: charNZ):<!wrt> string(n)
symintr string_fset_at
overload string_fset_at with string_fset_at_size of 1
fun{}
string0_append
(
x1: NSH(string), x2: NSH(string)
) :<!wrt> Strptr1
fun{}
string1_append
{n1,n2:int} (
x1: NSH(string(n1)), x2: NSH(string(n2))
) :<!wrt> strnptr(n1+n2)
symintr string_append
overload string_append with string0_append of 0
fun{}
string0_append3
(
x1: NSH(string)
, x2: NSH(string), x3: NSH(string)
) :<!wrt> Strptr1
fun{}
string0_append4
(
x1: NSH(string), x2: NSH(string)
, x3: NSH(string), x4: NSH(string)
) :<!wrt> Strptr1
fun{}
string0_append5
(
x1: NSH(string), x2: NSH(string)
, x3: NSH(string), x4: NSH(string), x5: NSH(string)
) :<!wrt> Strptr1
fun{}
string0_append6
(
x1: NSH(string), x2: NSH(string), x3: NSH(string)
, x4: NSH(string), x5: NSH(string), x6: NSH(string)
) :<!wrt> Strptr1
overload string_append with string0_append3 of 0
overload string_append with string0_append4 of 0
overload string_append with string0_append5 of 0
overload string_append with string0_append6 of 0
fun{}
stringarr_concat{n:int}
(
xs: arrayref(string, n), n: size_t(n)
) :<!wrt> Strptr1
fun{}
stringlst_concat(List(string)):<!wrt> Strptr1
fun{}
string_implode
{n:int}
(cs: list(charNZ, n)):<!wrt> strnptr(n)
fun{}
string_explode
{n:int} (x: string(n)):<!wrt> list_vt(charNZ, n)
fun{}
string_tabulate$fopr(size_t): charNZ
fun{}
string_tabulate{n:int}(n: size_t(n)): strnptr(n)
fun{}
string_tabulate_cloref{n:int}
(n: size_t(n), f: (sizeLt(n)) -<cloref1> charNZ): strnptr(n)
fun{}
string_forall(str: string): bool
fun{}
string_forall$pred(c: char): bool
fun{}
string_iforall(str: string): bool
fun{}
string_iforall$pred(i: int, c: char): bool
fun{env:vt0p}
string_foreach$cont(c: char, env: &env): bool
fun{env:vt0p}
string_foreach$fwork(c: char, env: &(env) >> _): void
fun{
} string_foreach {n:int} (str: string(n)): sizeLte(n)
fun{
env:vt0p
} string_foreach_env
{n:int} (str: string(n), env: &(env) >> _): sizeLte(n)
fun{env:vt0p}
string_rforeach$cont(c: char, env: &env): bool
fun{env:vt0p}
string_rforeach$fwork(c: char, env: &(env) >> _): void
fun{}
string_rforeach{n:int}(str: string(n)): sizeLte(n)
fun{
env:vt0p
} string_rforeach_env
{n:int}(str: string(n), env: &(env) >> _): sizeLte(n)
fun{}
streamize_string_char(string): stream_vt(charNZ)
fun stropt_none(): stropt(~1) = "mac#%"
castfn stropt0_some(x: SHR(string)): Stropt1
castfn stropt1_some{n:int}(x: SHR(string(n))): stropt(n)
symintr stropt_some
overload stropt_some with stropt0_some of 0
overload stropt_some with stropt1_some of 10
fun{}
stropt_is_none{n:int}(stropt(n)):<> bool(n < 0)
fun{}
stropt_is_some{n:int}(stropt(n)):<> bool(n >= 0)
castfn
stropt_unsome{n:nat}(opt: stropt(n)):<> string(n)
fun{}
stropt_length{n:int}(opt: stropt(n)):<> ssize_t(n)
fun
print_stropt(opt: Stropt0): void = "mac#%"
fun
prerr_stropt(opt: Stropt0): void = "mac#%"
fun
fprint_stropt(out: FILEref, opt: Stropt0): void = "mac#%"
overload
[] with string_get_at_size of 1
overload
[] with string_get_at_gint of 0
overload
[] with string_get_at_guint of 0
overload
iseqz with string_is_empty of 10
overload
isneqz with string_isnot_empty of 10
overload length with string_length
overload .head with string_head of 10
overload .tail with string_tail of 10
overload copy with string0_copy of 0
overload print with print_string of 0
overload prerr with prerr_string of 0
overload fprint with fprint_string of 0
overload unsome with stropt_unsome
overload iseqz with stropt_is_none
overload isneqz with stropt_is_some
overload length with stropt_length of 0
overload print with print_stropt of 0
overload prerr with prerr_stropt of 0
overload fprint with fprint_stropt of 0
abst@ype
strbuf_t0ype
(m:int, n:int)
stadef
strbuf = strbuf_t0ype
viewdef
strbuf_v
(l:addr, m:int, n:int) = strbuf (m, n) @ l
praxi
strbuf2bytes
{m,n:int}
(buf: &strbuf (m, n) >> b0ytes (m)): void
praxi
strbuf2bytes_v
{l:addr}{m,n:int}
(pf: strbuf_v (l, m, n)): b0ytes_v (l, m)
praxi
lemma_strptr_param
{l:addr} (x: !strptr l): [l>=null] void
praxi
lemma_strnptr_param
{l:addr}{n:int}
(
x: !strnptr (l, n)
) : [(l>null&&n>=0) || (l==null&&n==(~1))] void
praxi
lemma_strbuf_param
{l:addr}{m,n:int}
(x: &strbuf (m, n)): [m>n] void
praxi
lemma_strbuf_v_param
{l:addr}{m,n:int}
(pf: !strbuf_v (l, m, n)): [l>null;m>n] void
castfn
strptr2ptr
{l:addr} (x: !strptr l):<> ptr (l)
castfn
strnptr2ptr
{l:addr}{n:int} (x: !strnptr(l, n)):<> ptr(l)
castfn
strnptr2strptr
{l:addr}{n:int} (x: strnptr(l, n)):<> strptr(l)
castfn
strptr2strnptr
{l:addr} (x: strptr(l)):<> [n:int] strnptr(l, n)
castfn
strptr2stropt
{l:addr}
(
x: strptr (l)
) :<>
[n:int
|(l==null&&n < 0)||(l>null&&n>=0)
] stropt(n)
castfn
strptr2stropt0(x: Strptr0):<> Stropt0
castfn
stropt2stropt1(x: Strptr1):<> Stropt1
castfn
strnptr2stropt
{l:addr}{n:int}
(x: strnptr(l, n)):<> stropt(n)
castfn
strptr2string(x: Strptr1):<> String
castfn
strnptr2string
{l:addr}{n:nat}(x: strnptr(l, n)):<> string(n)
fun strptr_null():<> strptr(null) = "mac#%"
praxi
strptr_free_null
{l:addr | l <= null} (x: strptr(l)):<> void
fun{}
strptr_is_null
{l:addr} (x: !strptr(l)):<> bool(l==null)
fun{}
strptr_isnot_null
{l:addr} (x: !strptr(l)):<> bool(l > null)
fun{}
strptr_is_empty(x: !Strptr1):<> bool
fun{}
strptr_isnot_empty(x: !Strptr1):<> bool
fun{}
strnptr_is_null
{l:addr}{n:int}
(x: !strnptr(l, n)):<> bool(l==null)
fun{}
strnptr_isnot_null
{l:addr}{n:int}
(x: !strnptr(l, n)):<> bool(l > null)
praxi
strnptr_free_null
{l:addr|l <= null}{n:int}(x: strnptr(l, n)):<> void
fun lt_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload < with lt_strptr_strptr
fun lte_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload <= with lte_strptr_strptr
fun gt_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload > with gt_strptr_strptr
fun gte_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload >= with gte_strptr_strptr
fun eq_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload = with eq_strptr_strptr
fun neq_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> bool = "mac#%"
overload != with neq_strptr_strptr
overload <> with neq_strptr_strptr
fun compare_strptr_strptr
(x1: !Strptr0, x2: !Strptr0):<> Sgn = "mac#%"
fun eq_strptr_string
(x1: !Strptr1, x2: string):<> bool = "mac#%"
overload = with eq_strptr_string
fun neq_strptr_string
(x1: !Strptr1, x2: string):<> bool = "mac#%"
overload != with neq_strptr_string
overload <> with neq_strptr_string
fun compare_strptr_string
(x1: !Strptr1, x2: string):<> Sgn = "mac#%"
fun strptr_free (x: Strptr0):<!wrt> void = "mac#%"
fun strnptr_free (x: Strnptr0):<!wrt> void = "mac#%"
fun
fprint_strptr
(
out: FILEref, x: !Strptr0
) : void = "mac#%"
fun print_strptr (x: !Strptr0): void = "mac#%"
fun prerr_strptr (x: !Strptr0): void = "mac#%"
fun
print_strbuf
{m,n:int}(buf: &strbuf(m, n)): void = "mac#%"
fun
prerr_strbuf
{m,n:int}(buf: &strbuf(m, n)): void = "mac#%"
fun
fprint_strbuf{m,n:int}
(out: FILEref, buf: &strbuf (m, n)): void = "mac#%"
fun{}
strnptr_get_at_size
{n:int}
(str: !strnptr (n), i: sizeLt n):<> charNZ
fun{tk:tk}
strnptr_get_at_gint
{n:int}{i:nat | i < n}
(str: !strnptr(n), i: g1int(tk, i)):<> charNZ
fun{tk:tk}
strnptr_get_at_guint
{n:int}{i:nat | i < n}
(str: !strnptr(n), i: g1uint(tk, i)):<> charNZ
symintr strnptr_get_at
overload strnptr_get_at with strnptr_get_at_size of 1
overload strnptr_get_at with strnptr_get_at_gint of 0
overload strnptr_get_at with strnptr_get_at_guint of 0
fun{}
strnptr_set_at_size
{n:int}
(str: !strnptr(n), i: sizeLt n, c: charNZ):<!wrt> void
fun{tk:tk}
strnptr_set_at_gint
{n:int}{i:nat | i < n}
(str: !strnptr(n), i: g1int(tk, i), c: charNZ):<!wrt> void
fun{tk:tk}
strnptr_set_at_guint
{n:int}{i:nat | i < n}
(str: !strnptr(n), i: g1uint(tk, i), c: charNZ):<!wrt> void
symintr strnptr_set_at
overload strnptr_set_at with strnptr_set_at_size of 1
overload strnptr_set_at with strnptr_set_at_gint of 0
overload strnptr_set_at with strnptr_set_at_guint of 0
fun{}
strptr_length (x: !Strptr0):<> ssize_t
fun{}
strnptr_length {n:int} (x: !strnptr n):<> ssize_t (n)
fun{}
strptr0_copy (x: !Strptr0):<!wrt> Strptr0
fun{}
strptr1_copy (x: !Strptr1):<!wrt> Strptr1
fun{}
strnptr_copy
{n:int} (x: !strnptr (n)):<!wrt> strnptr (n)
fun{}
strptr_append
(x1: !Strptr0, x2: !Strptr0):<!wrt> Strptr0
fun{}
strnptr_append{n1,n2:nat}
(x1: !strnptr n1, x2: !strnptr n2):<!wrt> strnptr(n1+n2)
fun{}
strptrlst_free (xs: List_vt(Strptr0)):<!wrt> void
fun{}
strptrlst_concat (xs: List_vt(Strptr0)):<!wrt> Strptr0
fun{
env:vt0p
} strnptr_foreach$cont (c: &charNZ, env: &env): bool
fun{
env:vt0p
} strnptr_foreach$fwork (c: &charNZ >> _, env: &env): void
fun{}
strnptr_foreach {n:nat} (str: !strnptr n): sizeLte(n)
fun{
env:vt0p
} strnptr_foreach_env
{n:nat} (str: !strnptr n, env: &(env) >> _): sizeLte(n)
fun{
env:vt0p
} strnptr_rforeach$cont (c: &charNZ, env: &env): bool
fun{
env:vt0p
} strnptr_rforeach$fwork (c: &charNZ >> _, env: &env): void
fun{}
strnptr_rforeach {n:nat} (str: !strnptr n): sizeLte(n)
fun{
env:vt0p
} strnptr_rforeach_env
{n:nat} (str: !strnptr n, env: &(env) >> _): sizeLte(n)
overload
[] with strnptr_get_at_size of 1