(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2014 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
** 
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
** 
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author: Hongwei Xi
// Authoremail: hwxiATcsDOTbuDOTedu
//
// This one was
// there at the very beginning of ATS
//
(* ****** ****** *)
//
(*
HX: fixity declarations
*)
#include "prelude/params.hats"
//
(* ****** ****** *)

#if VERBOSE_FIXITY #then
#print "Loading [fixity.ats] starts!\n"
#endif // end of [VERBOSE_FIXITY]

(* ****** ****** *)
//
(*
prefix 00 ! (* static *)
*)
//
prefix 99 ! (* dynamic *)
//
(* ****** ****** *)

(*
prefix 81 ID (* identity *)
*)

(* ****** ****** *)

(*
postfix 80 .lab // dynamic
postfix 80 ->lab // dynamic
*)

(* ****** ****** *)

(*
prefix 79 & // dynamic
*)

(* ****** ****** *)

(*
infixl 70 app
*)

(* ****** ****** *)

(*
postfix 69 ?
*)

(* ****** ****** *)
//
// HX-2015-08-04:
// mostly following the Fortran convention
//
(* ****** ****** *)

infixr 61 ** (*exp*)

(* ****** ****** *)
//
// multiplicative
//
infixl 60 * / % mod
//
(*
infixl 60 nmul ndiv nmod
*)
//
(* ****** ****** *)

prefix 51 ~ (*negative*)

(* ****** ****** *)
//
infixl 50 + - (*additive*)
//
(*
infixr (+) ++ // concatenative
*)
//
(* ****** ****** *)

infixl 41 asl asr
infixl 41 lsl lsr

(* ****** ****** *)
//
infix 40 < <= > >=
//
(*
//
// HX-2012-07: removed
//
infixl ( < ) ilt flt plt ult
infixl ( <= ) ilte flte plte ulte
infixl ( > ) igt fgt pgt ugt
infixl ( >= ) igte fgte pgte ugte
*)
//
(* ****** ****** *)

infixr 40 :: @

(* ****** ****** *)

infix 30 = == != <>

(* ****** ****** *)

(*
//
// HX-2012-07: removed
//
infix ( = ) ieq feq peq ueq
infix ( <> ) ineq fneq pneq uneq
*)

(* ****** ****** *)

infixl 21 &&
infixl ( && ) andalso land

(* ****** ****** *)

infixl 20 ||
infixl ( || ) xor orelse lor lxor

(* ****** ****** *)

infixr 10 ->

(* ****** ****** *)

infix 0 := // HX: assign
infix 0 :=: // HX: exchange

(* ****** ****** *)

infixl 0 << (* g0int_asl, g0uint_lsl *)
infixr 0 >> (* g0int_asr, g0uint_lsr *)

(* ****** ****** *)

prefix 0 ++ -- // inc and dec
prefix 0 !++ --! // getinc and decget
infixr 0 =++ --= // setinc and decset

(* ****** ****** *)

infix 0 :+= :-= :*= :/= // x:=x+a, x:=x-a, ...
infix 0 :=+ :=- :=* :=/ // x:=a+x, x:=a-x, ...

(* ****** ****** *)

prefix 0 ignoret // ignoring a funcall return

(* ****** ****** *)

#if VERBOSE_FIXITY #then
#print "Loading [fixity.ats] finishes!\n"
#endif // end of [VERBOSE_FIXITY]

(* end of [fixity.ats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: September, 2011
//
(* ****** ****** *)

#include "prelude/params.hats"

(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_pre.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]

(* ****** ****** *)
//
// HX:
// some built-in static boolean constants
//
stacst
true_bool : bool = "ext#"
stacst
false_bool : bool = "ext#"
//
stadef
true = true_bool and false = false_bool
//
// HX: boolean negation
//
stacst
neg_bool
  : bool -> bool = "ext#"
//
stadef ~ = neg_bool // overloaded
stadef not = neg_bool // overloaded
//
// HX: disjunction
//
stacst
add_bool_bool
  : (bool, bool) -> bool = "ext#"
//
// HX: disjunction
//
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 (* for backward compatibility *)
//
(* ****** ****** *)

(*
//
// HX-2012-06-12: removed
//
stacst
eq_char_char
  : (char, char) -> bool = "ext#"
stacst
neq_char_char
  : (char, char) -> bool = "ext#"
//
stadef == = eq_char_char
stadef != = neq_char_char
stadef <> = neq_char_char (* for backward compatibility *)
//
*)

(* ****** ****** *)
//
stacst
neg_int
  : (int) -> int = "ext#"
//
stadef ~ = neg_int // overloaded
//
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
//
// HX: ndiv: divisor is positive
// HX: idiv: alias for div_int_int
//
stacst
ndiv_int_int
  : (int, int) -> int = "ext#"
stacst
idiv_int_int
  : (int, int) -> int = "ext#"
//
stadef ndiv = ndiv_int_int // divided by nat
stadef idiv = idiv_int_int // divided by 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 % (*adopted from C*) = 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 (* for backward compatibility *)
//
(* ****** ****** *)
//
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 // HX: y > 0
  (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) = ( // HX: y != 0
  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)
) (* end of [idivrel_int_int_int] *)
//
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

(* ****** ****** *)

(*
** HX: [char] = [int8]
** HX-2012-06-12: removed
//
stacst
int_of_char: char -> int = "ext#"
stacst
char_of_int : int -> char = "ext#"
//
stadef c2i = int_of_char and i2c = char_of_int
//
*)

(* ****** ****** *)

(*
** HX: pointer <-> integer
*)
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 (* for backward compatibility *)
//
(* ****** ****** *)
//
// HX-2013-09:
// for supporting inheritance in OOP
//
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 // end-of-stadef
stadef
gterel_cls_cls
(
  c1: cls, c2: cls, gterel_cls_cls_res: bool
) : bool = gterel_cls_cls_res // end-of-stadef
//
(* ****** ****** *)
//
// HX: this is a special constant!
//
stacst
sizeof_t0ype_int : t@ype -> int = "ext#"
stadef
sizeof(a:viewt@ype): int = sizeof_t0ype_int (a?)
//
(* ****** ****** *)

sortdef nat = { i:int | i >= 0 } // natural numbers
sortdef pos = { i:int | i > 0 }
sortdef neg = { i:int | i < 0 }
sortdef npos = { i:int | i <= 0 } // non-positive integers

sortdef nat1 = { n:nat | n < 1 } // for 0
sortdef nat2 = { n:nat | n < 2 } // for 0, 1
sortdef nat3 = { n:nat | n < 3 } // for 0, 1, 2
sortdef nat4 = { n:nat | n < 4 } // for 0, 1, 2, 3

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 // nothing
stacst effall : eff // everything
//
stacst effntm : eff // nonterm
stacst effexn : eff // exception
stacst effref : eff // reference
stacst effwrt : eff // writeover
//
stacst add_eff_eff : (eff, eff) -> eff
stadef + = add_eff_eff // union of effsets
stacst sub_eff_eff : (eff, eff) -> eff
stadef - = add_eff_eff // difference of effsets
//
(* ****** ****** *)
//
// HX: some overloaded symbols
//
symintr ~ not
(*
symintr && || // macros
*)
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 ! [] // deref subscript
symintr << >> // for L/R-shifting
//
symintr inc dec
symintr ++ -- // inc and dec
symintr get set exch
symintr getinc setinc exchinc
symintr decget decset decexch
symintr !++ --! // getinc and decget
symintr =++ --= // setinc and decset
//
symintr assert
//
symintr encode decode
//
symintr uncons unsome
//
symintr ptrcast (* taking the address of a boxed val *)
symintr g0ofg1 g1ofg0 (* casting: indexed <-> un-indexed *)
//
symintr copy free length
//
symintr print prerr fprint gprint
symintr println prerrln fprintln gprintln
//
(*
//
symintr forall
symintr iforall
//
symintr foreach
symintr foreach2
symintr iforeach
symintr rforeach
//
*)
//
symintr ofstring ofstrptr
symintr tostring tostrptr
//
(* ****** ****** *)
//
// HX-2014-02:
// for dot-notation overloading
//
symintr .size
symintr .len .length
symintr .get .set .exch
symintr .nrow .ncol
symintr .head .tail
symintr .next .prev
symintr .init .last
symintr .eval // HX: convention: using "!"
//
(* ****** ****** *)
//
// HX-2012-05-23: for template args
//
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 // S2Eat
at_vt0ype_addr_view(a:vt@ype+, l:addr)
//
viewdef @ // HX: @ is infix
  (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
//
(* ****** ****** *)
(*
absview
read_view_int_int_view
  (v:view, stamp:int, n:int)
stadef
READ = read_view_int_int_view
viewdef
READ (v:view) = [s,n:int] READ (v, s, n)
stadef RD = READ
//
absview
readout_view_int_view (v:view, stamp:int)
stadef
READOUT = readout_view_int_view
viewdef
READOUT (v:view) = [s:int] READOUT (v, s)
//
absvt@ype
read_vt0ype_int_int_vt0ype
  (a:vt@ype, stamp:int, n:int) = a
stadef
READ = read_vt0ype_int_int_vt0ype
vtypedef
READ (a:vt@ype) = [s,n:int] READ (a, s, n)
stadef RD = READ
//
absvt@ype
readout_vt0ype_int_vt0ype
  (a:vt@ype, stamp: int) = a
stadef
READOUT = readout_vt0ype_int_vt0ype
vtypedef
READOUT (a:vt@ype) = [s:int] READOUT (a, s)
*)

(* ****** ****** *)

(*
absvt@ype
write_vt0ype_vt0ype(a: vt@ype) = a
vtypedef
WRITE(a:vt@ype) = write_vt0ype_vt0ype (a)
stadef WR = WRITE
*)

(* ****** ****** *)
//
vtypedef READ (a:vt@ype) = a // HX: used as a comment
vtypedef WRITE (a:vt@ype) = a // HX: used as a comment (rarely)
//
(*
vtypedef SHARED (a:vt@ype) = a // HX: used as a comment
vtypedef NSHARED (a:vt@ype) = a // HX: used as a comment (rarely)
*)
//
(* ****** ****** *)
//
absprop invar_prop_prop (a:prop)
absview invar_view_view (a:view)
//
abst@ype // S2Einvar
invar_t0ype_t0ype (a:t@ype) = a
absvt@ype // S2Einvar
invar_vt0ype_vt0ype (a:vt@ype) = a
//
// HX: this order is significant
// 
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)
//
(* ****** ****** *)
(*
//
absprop optarg_prop_prop (a:prop)
absview optarg_view_view (a:view)
//
abst@ype
optarg_t0ype_t0ype (a:t@ype) = a
absvt@ype
optarg_vt0ype_vt0ype (a:vt@ype) = a
//
// HX: this order is significant
// 
viewdef
OPT (a: view) = optarg_view_view (a)
propdef
OPT (a: prop) = optarg_prop_prop (a)
//
vtypedef OPT
  (a:vt@ype) = optarg_vt0ype_vt0ype (a)
//
vtypedef
OPT (a: t@ype) = optarg_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 // end of [VERBOSE_PRELUDE]

(* ****** ****** *)

(* end of [basics_pre.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: September, 2011
//
(* ****** ****** *)

#include "prelude/params.hats"

(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_sta.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]

(* ****** ****** *)

#define RD(x) x // for commenting: read-only

(* ****** ****** *)
(*
//
// HX-2012-05-24:
// the following two styles are equivalent:
//
stadef
bool_kind = $extkind"atstype_bool"
tkindef bool_kind = "atstype_bool"
*)
(* ****** ****** *)
//
tkindef bool_kind = "atstype_bool"
//
abst@ype
bool_t0ype = tkind_t0ype (bool_kind)
stadef bool = bool_t0ype // shorthand
abst@ype
bool_bool_t0ype (b: bool) = bool_t0ype
stadef bool = bool_bool_t0ype // shorthand
//
typedef Bool = [b:bool] bool (b)
typedef boolLte
  (b1:bool) = [b2:bool] bool (b2 <= b1) // b2 -> b1
typedef boolGte
  (b1:bool) = [b2:bool] bool (b2 >= b1) // b1 -> b2
//
abst@ype atstype_bool // HX-2013-09: for internal use
//
(* ****** ****** *)

tkindef
byte_kind = "atstype_byte"
abst@ype
byte_t0ype = tkind_t0ype (byte_kind)
stadef byte = byte_t0ype

(* ****** ****** *)
//
// char is signed
//
sortdef int8 = {
  i:int | ~128 <= i; i < 128
} // end of [int8]
sortdef uint8 =
  { i:int | 0 <= i; i < 256 }
// end of [uint8]
//
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 // shorthand
stadef char = char_int_t0ype // shorthand
//
typedef Char = [c:int8] char(c)
typedef charNZ = [c:int8 | c != 0] char(c)
//
// signed characters
//
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 // shorthand
stadef schar = schar_int_t0ype // shorthand
typedef sChar = [c:int8] schar(c)
typedef scharNZ = [c:int8 | c != 0] schar(c)
//
// unsigned characters
//
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 // shorthand
stadef uchar = uchar_int_t0ype // shorthand
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 // shorthand
abst@ype
g1int_int_t0ype (tk:tkind, int) = g0int (tk)
stadef g1int = g1int_int_t0ype // shorthand
//
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 // shorthand
abst@ype
g1uint_int_t0ype (tk:tkind, int) = g0uint (tk)
stadef g1uint = g1uint_int_t0ype // shorthand
//
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 // 2nd-select
stadef int = int0 // 1st-select
//
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 // 2nd-select
stadef uint = uint0 // 1st-select
//
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 // HX-2013-09: for internal use
abst@ype atstype_uint // HX-2013-09: for internal use
//
(* ****** ****** *)
//
tkindef
lint_kind = "atstype_lint"
typedef
lint0 = g0int (lint_kind)
typedef
lint1 (i:int) = g1int (lint_kind, i)
stadef lint = lint1 // 2nd-select
stadef lint = lint0 // 1st-select
//
tkindef
ulint_kind = "atstype_ulint"
typedef
ulint0 = g0uint (ulint_kind)
typedef
ulint1 (i:int) = g1uint (ulint_kind, i)
stadef ulint = ulint1 // 2nd-select
stadef ulint = ulint0 // 1st-select
//
tkindef
llint_kind = "atstype_llint"
typedef llint0 = g0int (llint_kind)
typedef llint1 (i:int) = g1int (llint_kind, i)
stadef llint = llint1 // 2nd-select
stadef llint = llint0 // 1st-select
//
tkindef
ullint_kind = "atstype_ullint"
typedef
ullint0 = g0uint (ullint_kind)
typedef
ullint1 (i:int) = g1uint (ullint_kind, i)
stadef ullint = ullint1 // 2nd-select
stadef ullint = ullint0 // 1st-select
//
(* ****** ****** *)
//
tkindef
intptr_kind = "atstype_intptr"
typedef
intptr0 = g0int (intptr_kind)
typedef
intptr1 (i:int) = g1int (intptr_kind, i)
stadef intptr = intptr1 // 2nd-select
stadef intptr = intptr0 // 1st-select
//
tkindef
uintptr_kind = "atstype_uintptr"
typedef
uintptr0 = g0uint (uintptr_kind)
typedef
uintptr1 (i:int) = g1uint (uintptr_kind, i)
stadef uintptr = uintptr1 // 2nd-select
stadef uintptr = uintptr0 // 1st-select
//
(* ****** ****** *)
//
tkindef
sint_kind = "atstype_sint"
typedef
sint0 = g0int (sint_kind)
typedef
sint1 (i:int) = g1int (sint_kind, i)
stadef sint = sint1 // 2nd-select
stadef sint = sint0 // 1st-select
//
tkindef
usint_kind = "atstype_usint"
typedef
usint0 = g0uint (usint_kind)
typedef
usint1 (i:int) = g1uint (usint_kind, i)
stadef usint = usint1 // 2nd-select
stadef usint = usint0 // 1st-select
//
(* ****** ****** *)
//
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 // 2nd-select
stadef size_t = size0_t // 1st-select
//
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 // 2nd-select
stadef ssize_t = ssize0_t // 1st-select
//
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 // HX-2013-09: for internal use
abst@ype atstype_ssize // HX-2013-09: for internal use
//
(* ****** ****** *)

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 // 2nd-select
stadef int8 = int8_0 // 1st-select
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 // 2nd-select
stadef uint8 = uint8_0 // 1st-select
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 // 2nd-select
stadef int16 = int16_0 // 1st-select
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 // 2nd-select
stadef uint16 = uint16_0 // 1st-select
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 // 2nd-select
stadef int32 = int32_0 // 1st-select
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 // 2nd-select
stadef uint32 = uint32_0 // 1st-select
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 // 2nd-select
stadef int64 = int64_0 // 1st-select
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 // 2nd-select
stadef uint64 = uint64_0 // 1st-select
stadef uInt64 = [i:nat] uint64_1 (i)
//
(* ****** ****** *)
//
abst@ype
g0float_t0ype (tk:tk) = tkind_t0ype (tk)
stadef g0float = g0float_t0ype // shorthand
//
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)
//
(* ****** ****** *)
//
// HX: unindexed type for pointers
//
tkindef ptr_kind = "atstype_ptrk"
//
abstype ptr_type = tkind_type(ptr_kind)
abstype ptr_addr_type(l:addr) = ptr_type
//
typedef ptr = ptr_type // HX: a shorthand
typedef ptr(l:addr) = ptr_addr_type(l) // HX: a shorthand
//
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)
// end of [Ptrnull]
//
// HX-2012-02-14: it is an expriment for now:
//
typedef ptr(n:int) = ptr_addr_type(addr_of_int(n))
//
(* ****** ****** *)

(*
** HX: persistent read-only strings
*)
(*
//
// HX-2013-04: this confuses type-erasure
//
abstype
string_type = $extype"atstype_string"
*)
abstype
string_type = ptr // = char* in C
abstype
string_int_type(n: int) = string_type
//
stadef
string0 = string_type
stadef
string1 = string_int_type
//
stadef string = string1 // 2nd-select
stadef string = string0 // 1st-select
//
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)
//
(* ****** ****** *)
//
(*
** HX: linear mutable strings
*)
//
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)
//
(* ****** ****** *)

(*
** HX: persistent mutable strings
*)
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
(*
= $extype"atsvoid_t0ype"
*)
typedef void = atsvoid_t0ype // = C-void

(* ****** ****** *)
//
absvtype
exception_vtype = $extype"atstype_exnconptr"
//
vtypedef exn = exception_vtype // boxed vtype
//
(* ****** ****** *)

absvt@ype // covariance
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)
//
(* ****** ****** *)
//
// HX:
// for memory deallocation
// (with GC and without GC)
//
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) // libc-mfree
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 // invariance
vbox_view_prop (v:view)
propdef
vbox(v:view) = vbox_view_prop(v)

abstype // invariance
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
//
(* ****** ****** *)
//
// HX: [lazy(T)] :
// suspended evaluation of type T
//
abstype
lazy_t0ype_type(t@ype+) = ptr
typedef
lazy(a:t@ype) = lazy_t0ype_type(a)
//
(* ****** ****** *)
//
// HX: [lazy_vt(VT)] :
// suspended computation of viewtype VT
//
absvtype
lazy_vt0ype_vtype(vt@ype+) = ptr
vtypedef
lazy_vt(a:vt@ype) = lazy_vt0ype_vtype(a)
//
(* ****** ****** *)
//
(*
//
// HX-2016-02-21:
// these are renamed/relocated elsewhere
//
abst0ype
literal_int(intlit) = $extype"atsliteral_int"
abst0ype
literal_float(float) = $extype"atsliteral_float"
abst1ype
literal_string(string) = $extype"atsliteral_string"
*)
//
(* ****** ****** *)
//
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 // end of [VERBOSE_PRELUDE]

(* ****** ****** *)

(* end of [basics_sta.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: September, 2011
//
(* ****** ****** *)

#include "prelude/params.hats"

(* ****** ****** *)
//
fun
patsopt_version(): string = "ext#%"
//
(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]

(* ****** ****** *)
//
sortdef t0p = t@ype and vt0p = vt@ype
//
(* ****** ****** *)

datatype TYPE(a:vt@ype) = TYPE(a) of ()

(* ****** ****** *)
//
// HX-2012: In $ATSHOME/ccomp/runtime:
// atsbool_true/atsbool_false are mapped to 1/0
// this mapping is fixed and should never be changed!
//
#define true true_bool // shorthand
#define false false_bool // shorthand
//
val true_bool : bool(true)  = "mac#atsbool_true" // = 1
val false_bool : bool(false) = "mac#atsbool_false" // = 0
//
(* ****** ****** *)
//
// HX: [false] implies all
//
prfun false_elim{X:prop | false} ((*void*)): X
//
(* ****** ****** *)
//
typedef
compopr_type(a: t@ype) = (a, a) -<fun0> bool
typedef
compare_type(a: t@ype) = (a, a) -<fun0> int(*-/0/+*)
//
(* ****** ****** *)
//
praxi
lemma_subcls_reflexive
  {c:cls}((*void*)): [c <= c] void
//
praxi
lemma_subcls_transitive
  {c1,c2,c3:cls | c1 <= c2; c2 <= c3}(): [c1 <= c3] void
//
(* ****** ****** *)
//
praxi
praxi_int{i:int} ((*void*)): int(i)
//
dataprop
MUL_prop
(
  int, int, int
) = // MUL_prop
  | {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)
//
(* ****** ****** *)
//
// HX-2010-12-30: 
//
absprop
DIVMOD (
  x:int, y: int, q: int, r: int // x = q * y + r
) // end of [DIVMOD]
//
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} ((*void*)): ptr(l)
praxi praxi_bool{b:bool} ((*void*)): 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))
// end of [viewptr_match]

(* ****** ****** *)
//
val{
a:vt0ype
} sizeof : size_t(sizeof(a))
//
praxi
lemma_sizeof
  {a:vt0ype}((*void*)): [sizeof(a) >= 0] void
//
(* ****** ****** *)

praxi topize{a:t0ype} (x: !INV(a) >> a?): void

(* ****** ****** *)

castfn dataget{a:vt0ype} (x: !INV(a) >> a): a?!

(* ****** ****** *)
//
// HX: returning the pf to GC
//
praxi
mfree_gc_v_elim
  {l:addr} (pf: mfree_gc_v l):<prf> void
// end of [mfree_gc_v_elim]

(* ****** ****** *)

praxi
mfree_gcngc_v_nullify
  {l:addr} (
  pf1: mfree_gc_v(l), pf1: mfree_ngc_v(l)
) : void // end of [mfree_gcngc_nullify_v]

(* ****** ****** *)
//
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)
//
(*
//
// HX-2016-08:
// this is assumed internally!
//
overload ! with lazy_force of 0
overload ! with lazy_vt_force of 0
*)
//
(* ****** ****** *)
//
// HX-2013:
// macro implemented in [pats_ccomp_instrset]
//
fun
lazy_vt_free
  {a:vt0p}
  (lazyval: lazy_vt(a)):<!wrt> void = "mac#%"
//
overload ~ with lazy_vt_free of 0
//
(* ****** ****** *)
//
// HX-2014:
// macro implemented in [pats_ccomp_instrset]
//
fun
lazy2cloref
  {a:t0p}(lazy(a)): ((*void*)) -<cloref1> (a) = "mac#%"
//
(* ****** ****** *)

(*
// HX-2012-05-23: this seems TOO complicated!
(*
** HX-2012-03: handling read-only views and vtypes
*)
castfn
read_getval // copy out a non-linear value
  {a:t@ype}{s:int}{n:int} (x: !READ (a, s, n)):<> a
// end of [read_getval]

praxi
read_takeout{v:view}
  (pf: !v >> READOUT (v, s)): #[s:int] READ (v, s, 0)
// end of [read_takeout]
praxi
read_addback // HX: there is no need to check
  {v1:view}{v2:view}{s:int} // if v1 and v2 match
  (pf1: !READOUT (v1, s) >> v1, pf2: READ (v2, s, 0)): void
// end of [read0_addback]

praxi
read_split
  {v:view}{s:int}{n:int}
  (pf: !READ (v, s, n) >> READ (v, s, n+1)): READ (v, s, 0)
// end of [read_split]
praxi
read_unsplit // HX: there is no need to check
  {v1:view}{v2:view}{s:int}{n1,n2:int} // if v1 and v2 match
  (pf1: READ (v1, s, n1), pf2: READ (v2, s, n2)): READ (v1, s, n1+n2-1)
// end of [read_unsplit]
*)
(* ****** ****** *)
//
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
// end of [unstamp_t]
castfn
unstamp_vt
  {a:vt@ype}{x:int}(x: stamped_vt(INV(a), x)):<> a
// end of [unstamp_vt]

(* ****** ****** *)
//
castfn
stamped_t2vt
  {a:t@ype}{x:int}
  (x: stamped_t(INV(a), x)):<> stamped_vt(a, x)
// end of [stamped_t2vt]
//
castfn
stamped_vt2t
  {a:t@ype}{x:int}
  (x: stamped_vt(INV(a), x)):<> stamped_t(a, x)
// end of [stamped_vt2t]
//
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
//
(* ****** ****** *)
//
// HX: the_null_ptr = (void*)0
//
val
the_null_ptr
  : ptr(null) = "mac#the_atsptr_null"
//
(* ****** ****** *)
//
praxi
lemma_addr_param
  {l:addr}((*void*)): [l >= null] void
//
(* ****** ****** *)

praxi
lemma_string_param
  {n:int} (x: string(n)): [n >= 0] void
// end of [lemma_string_param]
praxi
lemma_stropt_param
  {n:int} (x: stropt(n)): [n >= ~1] void
// end of [lemma_stropt_param]

(* ****** ****** *)
//
dataprop
SGN (int, int) =
  | SGNzero (0, 0)
  | {i:neg} SGNneg (i, ~1) | {i:pos} SGNpos (i,  1)
// end of [SGN] // end of [dataprop]
//
(* ****** ****** *)
//
// HX-2012-06:
// indication of the failure of
exception AssertExn of () // an assertion
//
(* ****** ****** *)
//
// HX-2012-06:
// indication of something expected
exception NotFoundExn of () // to be found but not
//
(* ****** ****** *)
//
exception GenerallyExn of (string) // for unspecified causes
(*
exception GenerallyExn2 of (string, ptr(*data*)) // for unspecified causes
*)
//
(* ****** ****** *)
//
// HX-2012-07:
// indication of a function argument being
exception IllegalArgExn of (string) // out of its domain
//
(* ****** ****** *)

praxi __vfree_exn (x: exn):<> void // for freeing nullary exception-con

(* ****** ****** *)
//
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(*size*)) = 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(*elt*), n:int(*size*)) = ptr
stadef arrayref = arrayref_vt0ype_int_type
//
abstype
arrszref_vt0ype_type(a: vt@ype) = ptr
typedef arrszref(a:vt0p) = arrszref_vt0ype_type(a)
//
(* ****** ****** *)
//
datatype
// t@ype+: covariant
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))
// end of [datatype]
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
// vt@ype+: covariant
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))
// end of [list_vt0ype_int_vtype]
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 ((*void*))
  | 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 ((*void*))
  | stream_vt_cons of (a, stream_vt(a))
//
where
stream_vt(a:vt@ype) = lazy_vt(stream_vt_con(a))
//
(* ****** ****** *)
//
datatype
// t@ype+: covariant
option_t0ype_bool_type
(
  a:t@ype+, bool
) = // option_t0ype_bool_type
  | Some(a, true) of (INV(a)) | None(a, false)
// end of [datatype]
stadef option = option_t0ype_bool_type
typedef Option(a:t0p) = [b:bool] option(a, b)
//
datavtype
// vt@ype+: covariant
option_vt0ype_bool_vtype
(
  a:vt@ype+, bool
) = // option_vt0ype_bool_vtype
  | Some_vt(a, true) of (INV(a)) | None_vt(a, false)
// end of [option_vt0ype_bool_vtype]
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
) = // or_prop_prop_int_prop
  | 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
) = // or_view_view_int_view
  | 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
) = // option_prop_bool_prop
  | Some_p (a, true) of (INV(a)) | None_p (a, false)
// end of [option_prop_bool_prop]
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)
// end of [option_view_bool_view]
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

(*
[argv_takeout_strarr] is declared in prelude/SATS/extern.sats
[argv_takeout_parrnull] is declared in prelude/SATS/extern.sats
*)

(* ****** ****** *)

praxi
lemma_argv_param
  {n:int}(argv: !argv(n)): [n >= 0] void
// end of [praxi]

(* ****** ****** *)
//
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*)
) : 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
(
  (*void*)
) : 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_fprintf{ts:types}
(
  ecode: int, out: FILEref, fmt: printf_c ts, args: ts
) :<!exn> {a:vt0p}(a) = "mac#%" // end of [exit_fprintf]
*)
//
(* *****p* ****** *)
//
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 (* read *)
  | file_mode_w (* write *)
  | file_mode_rw (* read and write *)
// end of [file_mode]
//
(* ****** ****** *)

local
//
stadef r() = file_mode_r()
stadef w() = file_mode_w()
stadef rw() = file_mode_rw()
//
in (* in-of-local *)

(* ****** ****** *)

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 ()
// end of [file_mode_lte]

(* ****** ****** *)
//
prval
file_mode_lte_r_r
  : file_mode_lte(r(), r()) // impled in [filebas_prf.dats]
prval
file_mode_lte_w_w
  : file_mode_lte(w(), w()) // impled in [filebas_prf.dats]
prval
file_mode_lte_rw_rw
  : file_mode_lte(rw(), rw()) // impled in [filebas_prf.dats]
//
(* ****** ****** *)

end // end of [local]

(* ****** ****** *)

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*)): void = "mac#%"
fun prerr_newline((*void*)): void = "mac#%"
fun fprint_newline(out: FILEref): void = "mac#%"

(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] finishes!\n"
#endif // end of [VERBOSE_PRELUDE]

(* ****** ****** *)

(* end of [basics_dyn.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: July, 2012
//
(* ****** ****** *)

#include "prelude/params.hats"

(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_gen.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]

(* ****** ****** *)
//
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}
gfree_ref (x: &INV(a) >> 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}
print_val (x: a): void // = fprint_val (stdout_ref, x)
fun{a:t0p}
prerr_val (x: a): void // = fprint_val (stderr_ref, x)
//
fun{a:vt0p}
print_ref (x: &INV(a)): void // = fprint_ref (stdout_ref, x)
fun{a:vt0p}
prerr_ref (x: &INV(a)): void // = fprint_ref (stderr_ref, x)
//
*)

(* ****** ****** *)
//
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 // end of [VERBOSE_PRELUDE]

(* ****** ****** *)

(* end of [basics_gen.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: May, 2012
//
(* ****** ****** *)

#include "prelude/params.hats"

(* ****** ****** *)
//
(*
** HX: short form
*)
//
// [orelse] and [andalso] are declared as infix ops
//
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 effless(exp) = $effmask_all(,(exp))
*)
//
(* ****** ****** *)

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 // end of [undefined]
//
(* ****** ****** *)

macdef ignoret(x) = let val _ = ,(x) in (*nothing*) 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))
//
(* ****** ****** *)

(* end of [macrodef.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)
//
// Author of the file:
// Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: March, 2013
//
(* ****** ****** *)
//
// HX-2013-03:
// lmacrodef: local macro definitions
//
(* ****** ****** *)
//
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)))
//
(* ****** ****** *)
(*
//
// HX-2012-08:
//
// this example makes use of recursive macrodef
//
*)
(*
//
local
//
macrodef
rec
auxlist
  (xs, y) =
(
//
if
iscons! (xs)
then `(print ,(car! xs); ,(auxlist (cdr! xs, y))) else y
// end of [if]
//
) (* end of [auxlist] *)
//
in (* in of [local] *)

macdef
print_mac (x) =
,(
  if islist! (x) then auxlist (x, `()) else `(print ,(x))
) (* end of [print_mac] *)

macdef
println_mac (x) =
,(
  if islist! (x)
    then auxlist (x, `(print_newline())) else `(print ,(x); print_newline())
  // end of [if]
) (* end of [println_mac] *)

end // end of [local]
//
*)

(* ****** ****** *)
//
macdef
eqfn(x0) = lam(x) =<cloref1> (,(x0) = x)
macdef
cmpfn(x0) = lam(x) =<cloref1> compare(,(x0), x)
//
(* ****** ****** *)

(* end of [lmacrodef.hats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: September, 2011 *)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/integer.atxt
** Time of generation: Wed May  3 17:36:07 2017
*)

(* ****** ****** *)
//
// HX: for unindexed integer types
//
(* ****** ****** *)

sortdef tk = tkind

(* ****** ****** *)

typedef SHR(a:t@ype) = a // for commenting purpose
typedef NSH(a:t@ype) = a // for commenting purpose

(* ****** ****** *)
//
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#%"
//
(* ****** ****** *)
//
// HX-2015-09-20:
// These are implemented in prelude/string.cats:
//
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
//
(*
fun
{tk:tk}
g0int_double : g0int_uop_type(tk)
overload double with g0int_double of 0
*)
//
(* ****** ****** *)

typedef
g0int_aop_type
  (tk: tk) =
(
  g0int(tk)
, g0int(tk)
) -<fun0> g0int (tk)
// end of [g0int_aop_type]

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
// end of [g0int_cmp_type]

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

(* ****** ****** *)
//
// HX: for indexed integer types
//
castfn
g0ofg1_int{tk:tk}(g1int(tk)):<> g0int(tk)
castfn
g1ofg0_int{tk:tk}(g0int(tk)):<> g1int(tk)
overload g0ofg1 with g0ofg1_int // index-erasing
overload g1ofg0 with g1ofg0_int // index-inducing
//
(* ****** ****** *)
//
fun{
k1,k2:tk
} g1int2int // i2i
  {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)
// end of [g1int_get_index]

(* ****** ****** *)
//
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 // ~ for uminus
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_double_type
  (tk:tk) =
  {i:int}
  g1int (tk, i) -<fun0> g1int (tk, 2*i)
//
fun{tk:tk}
g1int_double : g1int_double_type(tk)
overload double with g1int_double 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))
// end of [g1int_mul2]
//
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)
) (* end of [g1int_ndiv2] *)

(* ****** ****** *)
//
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
//
(* ****** ****** *)

(*
** HX: [g1int_mod] is intentionally skipped
*)

(* ****** ****** *)
//
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)
) (* end of [g1int_nmod2] *)

(* ****** ****** *)
//
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
//
(* ****** ****** *)
//
(*
//
// HX-2016-12:
// [ngcd] is no longer pre-declared
//
typedef
g1int_ngcd_type
  (tk:tk) =
  {i,j:int | i >= 0; j >= 0}
(
  g1int(tk, i), g1int(tk, j)
) -<fun0> g1int(tk, ngcd_int_int(i, j))
//
fun{tk:tk}
g1int_ngcd : g1int_ngcd_type(tk)
//
// overload ngcd with g1int_ngcd of 20
//
*)
//
(* ****** ****** *)
//
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))

(* ****** ****** *)
//
// HX: for unsigned unindexed integer types
//
(* ****** ****** *)

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_double
  (g0uint(tk)):<> g0uint(tk)
overload double with g0uint_double 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
//
(* ****** ****** *)
//
// HX: for unsigned indexed integer types
//
praxi
lemma_g1uint_param
  {tk:tk}{i:int}(g1uint(tk, i)):<> [i >= 0] void
// end of [lemma_g1uint_param]
//
(* ****** ****** *)

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 // index-erasing
overload g1ofg0 with g1ofg0_uint // index-inducing
//
(* ****** ****** *)
//
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)
// end of [g1uint_div_type]
//
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)
// end of [g1uint_mod_type]
//
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)
) (* end of [g1uint_mod2] *)
//
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) // endfun
typedef
g1uint_lte_type
  (tk:tk) =
  {i,j:int}
(
  g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i <= j) // endfun
//
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) // endfun
typedef
g1uint_gte_type
  (tk:tk) =
  {i,j:int}
(
  g1uint(tk, i), g1uint(tk, j)
) -<fun0> bool(i >= j) // endfun
//
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))
//
(* ****** ****** *)
//
// HX: implemented in [list_vt.dats]
//
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))
//
(* ****** ****** *)

(* end of [integer.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/pointer.atxt
** Time of generation: Wed May  3 17:36:07 2017
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Start time: March, 2012 *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)

(* ****** ****** *)

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)
// end of [ptr_get_index]

(* ****** ****** *)
//
symintr ptr_is_null
symintr ptr_isnot_null
//
(* ****** ****** *)
//
symintr add_ptr_bsz
symintr sub_ptr_bsz
//
// add_ptr_bsz (p, ofs) = p + ofs
// sub_ptr_bsz (p, ofs) = p - ofs
//
(* ****** ****** *)
//
symintr ptr_succ
symintr ptr_pred
//
// ptr_succ<a>(p) = p + sizeof<a>
// ptr_pred<a>(p) = p - sizeof<a>
//
(* ****** ****** *)
//
symintr ptr_add ptr_sub
//
// ptr_add<a> (p, ofs) = p + ofs*sizeof<a>
// ptr_sub<a> (p, ofs) = p - ofs*sizeof<a>
//
(* ****** ****** *)

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{a:vt0p}
ptr0_add_int (p: ptr, i: int): ptr
fun{a:vt0p}
ptr0_add_lint (p: ptr, i: lint): ptr
fun{a:vt0p}
ptr0_add_ssize (p: ptr, i: ssize): ptr
fun{a:vt0p}
ptr0_add_uint (p: ptr, u: uint): ptr
fun{a:vt0p}
ptr0_add_ulint (p: ptr, u: ulint): ptr
fun{a:vt0p}
ptr0_add_size (p: ptr, u: size): ptr
*)

(*
fun{a:vt0p}
ptr0_sub_int (p: ptr, i: int): ptr
fun{a:vt0p}
ptr0_sub_lint (p: ptr, i: lint): ptr
fun{a:vt0p}
ptr0_sub_ssize (p: ptr, i: ssize): ptr
fun{a:vt0p}
ptr0_sub_uint (p: ptr, u: uint): ptr
fun{a:vt0p}
ptr0_sub_ulint (p: ptr, u: ulint): ptr
fun{a:vt0p}
ptr0_sub_size (p: ptr, u: size): ptr
*)

(* ****** ****** *)
//
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
//
(* ****** ****** *)
//
// HX: implemented in [prelude/DATS/pointer.dats]
//
fun{a:vt0p}
ptr_get{l:addr}
  (pf: !INV(a) @ l >> a?! @ l | p: ptr l):<> a
// end of [ptr_get]

fun{a:vt0p}
ptr_set{l:addr}
  (pf: !a? @ l >> a @ l | p: ptr l, x: INV(a)):<!wrt> void
// end of [ptr_set]

fun{a:vt0p}
ptr_exch{l:addr}
  (pf: !INV(a) @ l | p: ptr l, x: &a >> a):<!wrt> void
// end of [ptr_exch]

(* ****** ****** *)
//
abstype
cptr_vt0ype_addr_type
  (a:vt@ype+, addr) = ptr // HX: for simulating C pointers
//
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) // read
castfn cptr_wvar{a:vt0p} (x: &a? >> a):<> cPtr1(a) // write
//
(* ****** ****** *)
//
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) // HX: commenting
typedef constcharptr0 = charptr0 // HX: for commenting purpose
typedef constcharptr1 = charptr1 // HX: for commenting purpose

(* ****** ****** *)
//
absprop
is_nullable(a: vt@ype+) // covariant
//
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#%" // end of [ptr_nullize_tsz]
//
(* ****** ****** *)

fun
{a:vt0p}
ptr_alloc((*void*))
  :<> [l:agz] (a? @ l, mfree_gc_v(l) | ptr(l))
// end of [ptr_alloc]

fun
ptr_alloc_tsz
  {a:vt0p}(tsz: sizeof_t(a))
  :<> [l:agz] (a? @ l, mfree_gc_v(l) | ptr(l)) = "mac#%"
// end of [ptr_alloc_tsz]

(* ****** ****** *)

fun
ptr_free{a:t@ype}{l:addr}
  (pfgc: mfree_gc_v(l), pfat: a @ l | p: ptr(l)):<> void = "mac#%"
// end of [ptr_free]

(* ****** ****** *)
//
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)
//
(* ****** ****** *)
//
// HX-2015-03-24:
// singleton linear arrayptr
//
absvtype
aptr_vt0ype_addr_type
  (a:vt@ype+, addr) = ptr // HX: for safe ATS pointers
//
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
//
(*
overload [] with aptr_get_elt // HX: template arg needed
overload [] with aptr_set_elt // HX: template arg needed
*)
//
(* ****** ****** *)
//
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
//
(* ****** ****** *)
//
// HX-2014-05-16:
// A hack to stop buggy compilation
//
fun ptr_as_volatile (p: ptr): void
//
(* ****** ****** *)
//
// overloading for certain symbols
//
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
//
(* ****** ****** *)

(* end of [pointer.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/memory.atxt
** Time of generation: Wed May  3 17:36:10 2017
*)

(* ****** ****** *)

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
// end of [b0ytes2bytes]
praxi
b0ytes2bytes_v
  {l:addr}{n:int} (pf: b0ytes_v (l, n)): bytes_v (l, n)
// end of [b0ytes2bytes_v]

(* ****** ****** *)

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))
// end of [bytes_v_split]

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))
// end of [bytes_v_split_at]

(* ****** ****** *)

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)
// end of [bytes_v_unsplit]

(* ****** ****** *)
//
// HX-2013-08:
// for memory initialization
//
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#%" // endfun

(* ****** ****** *)

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 // end-of-fun

fun{
} memory$alloc
  {n:int}
(
  bsz: size_t (n)
) :<!wrt>
  [l:agz]
(
  b0ytes n @ l, memory$free_v (l) | ptr l
) (* end of [memory$alloc] *)

(* ****** ****** *)

(* end of [memory.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/bool.atxt
** Time of generation: Wed May  3 17:36:08 2017
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)

(* ****** ****** *)
//
castfn g0ofg1_bool (x: Bool):<> bool
castfn g1ofg0_bool (x: bool):<> Bool
//
overload g0ofg1 with g0ofg1_bool // index-erasing
overload g1ofg0 with g1ofg0_bool // index-inducing
//
(* ****** ****** *)
//
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
//
(* ****** ****** *)

(*
//
// HX: declared in [prelude/basics_dyn.sats]
//
val true : bool (true) and false : bool (false)
*)

(* ****** ****** *)

(*
** HX-2012-06:
** shortcut version of disjuction and conjuction
** note that these two cannot be declared as functions
*)
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

(* ****** ****** *)
//
// HX:
// return is statically allocated
//
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
//
(* ****** ****** *)

//
// (b1 < b2) == (~b1 && b2)
//
fun
lt_bool1_bool1 {b1,b2:bool}
  (b1: bool (b1), b2: bool (b2)) :<> bool (b1 < b2) = "mac#%"
overload < with lt_bool1_bool1 of 20
//
// (b1 <= b2) == (~b1 || b2)
//
fun
lte_bool1_bool1 {b1,b2:bool}
  (b1: bool (b1), b2: bool (b2)) :<> bool (b1 <= b2) = "mac#%"
overload <= with lte_bool1_bool1 of 20
//
// (b1 > b2) == (b1 && ~b2)
//
fun
gt_bool1_bool1 {b1,b2:bool}
  (b1: bool (b1), b2: bool (b2)) :<> bool (b1 > b2) = "mac#%"
overload > with gt_bool1_bool1 of 20
//
// (b1 >= b2) == (b1 || ~b2)
//
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} // HX: this one is a function
(
 b1: bool b1, b2: bool b2
) :<> int (bool2int(b1) - bool2int(b2)) = "mac#%"
overload compare with compare_bool1_bool1 of 20

(* ****** ****** *)

(* end of [bool.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)
(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/char.atxt
** Time of generation: Wed May  3 18:42:21 2017
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)

(* ****** ****** *)
//
praxi
lemma_char_size
(
// argumentless
) : [sizeof(char)==sizeof(byte)] void
praxi
lemma_schar_size
(
// argumentless
) : [sizeof(schar)==sizeof(byte)] void
praxi
lemma_uchar_size
(
// argumentless
) : [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 // index-erasing
overload g1ofg0 with g1ofg0_char // index-inducing
//
(* ****** ****** *)
//
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
//
(* ****** ****** *)
//
// unsigned characters
//
(* ****** ****** *)

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:int8
  {c:int} (c: char(c)):<> g1int(tk, c)
// end of [g1int_of_char1]
fun{tk:tk}
g1int_of_schar1 // c:int8
  {c:int} (c: schar(c)):<> g1int(tk, c)
// end of [g1int_of_schar1]
fun{tk:tk}
g1int_of_uchar1 // c:uint8
  {c:int} (c: uchar(c)):<> g1int(tk, c)
// end of [g1int_of_uchar1]

(*
** HX: g1uint_of_schar1: schar -> int -> uint
*)
fun{tk:tk}
g1uint_of_uchar1
  {c:int} (c: uchar(c)):<> g1uint(tk, c)
// end of [g1uint_of_uchar1]

(* ****** ****** *)
//
// HX:
// return is dynamically allocated
//
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
//
(* ****** ****** *)

(* end of [char.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/float.atxt
** Time of generation: Wed May  3 17:36:09 2017
*)

(* ****** ****** *)

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 // ~ for uminus
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)
// end of [g0float_aop_type]
//
(* ****** ****** *)
//
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
// end of [g0float_cmp_type]
//
(* ****** ****** *)
//
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
// end of [g0float_compare_type]
//
(* ****** ****** *)
//
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))

(* ****** ****** *)

(* end of [float.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/string.atxt
** Time of generation: Wed May  3 17:36:09 2017
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: September, 2011 *)

(* ****** ****** *)

(*
** HX: a string is a null-terminated arrayref of characters
*)

(* ****** ****** *)

sortdef tk = tkind

(* ****** ****** *)

typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

(* ****** ****** *)
//
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(*i*), int(*c*)
) =
  | string_index_p_eqz(n, n, 0)
  | {i:int | n > i}
    {c:int8 | c != 0}
    string_index_p_neqz(n, i, c)
// end of [string_index_p]

(* ****** ****** *)

exception StringSubscriptExn of ((*void*))

(* ****** ****** *)
//
praxi
lemma_string_param{n:int}(string n): [n >= 0] void
//
(* ****** ****** *)

castfn
string2ptr (x: string):<> Ptr1
overload ptrcast with string2ptr

(* ****** ****** *)
//
// HX:
// [string2string] = [string1_of_string0]
//
castfn g0ofg1_string (x: String):<> string
castfn g1ofg0_string (x: string):<> String0
//
overload g0ofg1 with g0ofg1_string // index-erasing
overload g1ofg0 with g1ofg0_string // index-inducing
//
(* ****** ****** *)

fun{}
string_char (str: string):<> char

(* ****** ****** *)
//
fun{}
string_nil((*void*)):<!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))
// end of [string_isnot_atend]

(* ****** ****** *)
//
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))
// end of [strintcmp]

fun{
} strlencmp
  {n1,n2:int}
  (x1: string n1, x2: string n2):<> int(sgn(n1-n2))
// end of [strlencmp]

(* ****** ****** *)

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)
// end of [string_make_rlist]

fun{}
string_make_rlistlen
  {n:int}
  (cs: list(charNZ, n), n: int(n)):<!wrt> strnptr(n)
// end of [string_make_rlistlen]

(* ****** ****** *)
//
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
   ((*void*)):<> intGte(1) // HX: the default = 16
//
(* ****** ****** *)

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)
// end of [string_make_substring]

(* ****** ****** *)
//
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#%" // end of [fprint_substring]
//
(* ****** ****** *)

fun{}
strchr{n:int}
  (str: string(n), c0: char):<> ssizeBtwe(~1, n)
// end of [strchr]

fun{}
strrchr{n:int}
  (str: string(n), c0: char):<> ssizeBtwe(~1, n)
// end of [strrchr]

fun{}
strstr{n:int}
  (haystack: string(n), needle: string):<> ssizeBtw(~1, n)
// end of [strstr]

(* ****** ****** *)

fun{}
strspn{n:int} // spanning
  (str: string(n), accept: string):<> sizeLte(n)
// end of [strspn]
fun{}
strcspn{n:int} // complement spanning
  (str: string(n), accept: string):<> sizeLte(n)
// end of [strcspn]

(* ****** ****** *)

fun{
} string_index{n:int}
  (str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
// end of [string_index]

fun{
} string_rindex{n:int}
  (str: string(n), c0: charNZ):<> ssizeBtw(~1, n)
// end of [string_rindex]

(* ****** ****** *)
//
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)
//
(* ****** ****** *)
//
// HX-2016-11-13:
// This can be done by calling
// [string_copy] and then [strptr_set_at]
//
fun{}
string_fset_at_size
  {n:int}{i:nat | i < n}
  (NSH(string(n)), i: size_t(i), c: charNZ):<!wrt> string(n)
//
(*
fun{tk:tk}
string_fset_at_gint
  {n:int}{i:nat | i < n}
  (NSH(string(n)), i: g1int(tk, i), c: charNZ):<!wrt> string(n)
fun{tk:tk}
string_fset_at_guint
  {n:int}{i:nat | i < n}
  (NSH(string(n)), i: g1uint(tk, 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 // end-of-function
fun{}
string1_append
  {n1,n2:int} (
  x1: NSH(string(n1)), x2: NSH(string(n2))
) :<!wrt> strnptr(n1+n2) // end of [string1_append]
//
symintr string_append
overload string_append with string0_append of 0
(*
//
// HX: too much of a surprise!
//
overload string_append with string1_append of 20
*)
//
(* ****** ****** *)
//
fun{}
string0_append3
(
  x1: NSH(string)
, x2: NSH(string), x3: NSH(string)
) :<!wrt> Strptr1 // end-of-function
fun{}
string0_append4
(
  x1: NSH(string), x2: NSH(string)
, x3: NSH(string), x4: NSH(string)
) :<!wrt> Strptr1 // end-of-function
fun{}
string0_append5
(
  x1: NSH(string), x2: NSH(string)
, x3: NSH(string), x4: NSH(string), x5: NSH(string)
) :<!wrt> Strptr1 // end-of-function
fun{}
string0_append6
(
  x1: NSH(string), x2: NSH(string), x3: NSH(string)
, x4: NSH(string), x5: NSH(string), x6: NSH(string)
) :<!wrt> Strptr1 // end-of-function
//
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 // end of [stringarr]
//
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)
// end of [string_foreach_env]
//
(* ****** ****** *)
//
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)
// end of [string_rforeach_env]
//
(* ****** ****** *)
//
fun{}
streamize_string_char(string): stream_vt(charNZ)
//
(* ****** ****** *)
//
(*
** HX:
** [stropt_none] is just the null pointer
*)
fun stropt_none((*void*)): 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#%"
//
(* ****** ****** *)
//
// overloading for certain symbols
//
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
//
(*
//
// HX: too much of a surprise!
//
overload copy with string1_copy of 10
*)
//
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
//
(* ****** ****** *)

(* end of [string.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2015 Hongwei Xi, ATS Trustful Software, Inc.
** All rights reserved
**
** ATS is free software;  you can  redistribute it and/or modify it under
** the terms of  the GNU GENERAL PUBLIC LICENSE (GPL) as published by the
** Free Software Foundation; either version 3, or (at  your  option)  any
** later version.
**
** ATS is distributed in the hope that it will be useful, but WITHOUT ANY
** WARRANTY; without  even  the  implied  warranty  of MERCHANTABILITY or
** FITNESS FOR A PARTICULAR PURPOSE.  See the  GNU General Public License
** for more details.
**
** You  should  have  received  a  copy of the GNU General Public License
** along  with  ATS;  see the  file COPYING.  If not, please write to the
** Free Software Foundation,  51 Franklin Street, Fifth Floor, Boston, MA
** 02110-1301, USA.
*)

(* ****** ****** *)

(*
** Source:
** $PATSHOME/prelude/SATS/CODEGEN/strptr.atxt
** Time of generation: Wed May  3 17:36:09 2017
*)

(* ****** ****** *)

(* Author: Hongwei Xi *)
(* Authoremail: hwxi AT cs DOT bu DOT edu *)
(* Start time: February, 2012 *)

(* ****** ****** *)

(*
** HX-2012:
** a Strptr0 is either the null-pointer or Strptr1
** a Strptr1 is a null-terminated arrayptr of characters
*)

(* ****** ****** *)
//
abst@ype
strbuf_t0ype
  (m:int, n:int) // HX: [m] byte size
//
(* ****** ****** *)
//
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
// end of [lemma_strptr_param]

praxi
lemma_strnptr_param
  {l:addr}{n:int}
(
  x: !strnptr (l, n)
) : [(l>null&&n>=0) || (l==null&&n==(~1))] void
// end of [lemma_strnptr_param]

(* ****** ****** *)

praxi
lemma_strbuf_param
  {l:addr}{m,n:int}
  (x: &strbuf (m, n)): [m>n] void
// end of [lemma_strbuf_param]

praxi
lemma_strbuf_v_param
  {l:addr}{m,n:int}
  (pf: !strbuf_v (l, m, n)): [l>null;m>n] void
// end of [lemma_strbuf_v_param]

(* ****** ****** *)

castfn
strptr2ptr
  {l:addr} (x: !strptr l):<> ptr (l)
castfn
strnptr2ptr
  {l:addr}{n:int} (x: !strnptr(l, n)):<> ptr(l)
// end of [strnptr2ptr]

(* ****** ****** *)
//
castfn
strnptr2strptr
  {l:addr}{n:int} (x: strnptr(l, n)):<> strptr(l)
// end of [strnptr2strptr]

castfn
strptr2strnptr
  {l:addr} (x: strptr(l)):<> [n:int] strnptr(l, n)
// end of [strptr2strnptr]
//
(* ****** ****** *)
//
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
// end of [strptr_free_null]

(* ****** ****** *)

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
// end of [strnptr_free_null]
//
(* ****** ****** *)

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)
// end of [strnptr_foreach_env]

(* ****** ****** *)

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)
// end of [strnptr_rforeach_env]

(* ****** ****** *)
//
// overloading for certain symbols
//
overload
[] with strnptr_get_at_size of 1