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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi
// Authoremail: gmhwxiATgmailDOTcom
// Start Time: April, 2011
//
(* ****** ****** *)

%{#
#include \
"libats/libc/CATS/stdio.cats"
%} // end of [%{#]

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
//
// HX: prefix for external names
//
#define
ATS_EXTERN_PREFIX "atslib_libats_libc_"
//
(* ****** ****** *)

#define RD(x) x // for commenting: read-only
typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

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

sortdef fm = file_mode

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

stadef r() = file_mode_r()
stadef w() = file_mode_w()
stadef rw() = file_mode_rw()

(* ****** ****** *)
//
staload
TYPES =
"libats/libc/SATS/sys/types.sats"
//
stadef fildes = $TYPES.fildes
stadef fildes_v = $TYPES.fildes_v
//
(* ****** ****** *)

(*
abstype FILEref = ptr // declared in [prelude/basic_dyn.sats]
*)

(* ****** ****** *)
//
// HX-2011-04-02:
//
absview
FILE_view(l:addr, m:fm)
absvtype
FILEptr_vtype(addr, fm) = ptr
//
viewdef
FILE_v(l:addr, m:fm) = FILE_view(l, m)
vtypedef
FILEptr(l:addr, m: fm) = FILEptr_vtype(l, m)
//
(* ****** ****** *)
//
vtypedef
FILEptr0(m:fm) =
  [l:addr | l >= null] FILEptr(l, m)
//
vtypedef
FILEptr1(m:fm) = [l:agz] FILEptr(l, m)
vtypedef
FILEptr1(*none*) = [l:agz;m:fm] FILEptr(l, m)
//
(* ****** ****** *)

stadef fmlte = file_mode_lte

(* ****** ****** *)
//
castfn
FILEptr2ptr
  {l:addr}{m:fm}(filp: !FILEptr(l, m)):<> ptr(l)
//
overload ptrcast with FILEptr2ptr
//
(* ****** ****** *)

castfn
FILEptr_encode
{l:addr}{m:fm}
(
pf: FILE_v(l, m) | p: ptr(l)
) : FILEptr(l, m)
overload encode with FILEptr_encode

castfn
FILEptr_decode
  {l:agz}{m:fm}
(
p0: FILEptr(l, m)
) : (FILE_v(l, m) | ptr(l))
overload decode with FILEptr_decode

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

praxi
FILEptr_free_null
  {l:alez}{m:fm}(p0: FILEptr(l, m)):<prf> void
// end of [FILEptr_free_null]

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

castfn
FILEptr_refize(filp: FILEptr1):<> FILEref

(* ****** ****** *)
//
// HX:
// A lock is associated with each FILEref-value
//
castfn
FILEref_vttakeout
  {m:fm}
  (filr: FILEref):<> [l:agz] vttakeout0(FILEptr(l, m))
// end of [FILEref_vttakeout]
//
(* ****** ****** *)
//
abst@ype whence_type = int
//
typedef whence = whence_type
//
macdef SEEK_SET = $extval(whence, "SEEK_SET")
macdef SEEK_CUR = $extval(whence, "SEEK_CUR")
macdef SEEK_END = $extval(whence, "SEEK_END")
//
(* ****** ****** *)
(*
//
// FILE *fopen (const char *path, const char *mode);
//
The fopen function opens the file whose name is the string pointed to by
path and associates a stream with it.

The argument mode points to a string beginning with one of the follow
ing sequences (Additional characters may follow these sequences.):

  r      Open  text  file  for  reading.  The stream is positioned at the
         beginning of the file.

  r+     Open for reading and writing.  The stream is positioned  at  the
         beginning of the file.

  w      Truncate  file  to  zero length or create text file for writing.
         The stream is positioned at the beginning of the file.

  w+     Open for reading and writing.  The file is created  if  it  does
         not  exist, otherwise it is truncated.  The stream is positioned
         at the beginning of the file.

  a      Open for appending (writing at end of file).  The file is created
         if it does not exist.  The stream is positioned at the end of the
         file.

  a+     Open for reading and appending (writing at end  of  file).   The
         file  is created if it does not exist.  The stream is positioned
         at the end of the file.

*)

fun
fopen{m:fm}
(
  path: NSH(string), fmode(m)
) :<!wrt> FILEptr0(m) = "mac#%"

fun
fopen_exn{m:fm}
(
  path: NSH(string), fmode(m)
) :<!exnwrt> FILEptr1(m) = "ext#%"

fun
fopen_ref_exn{m:fm}
(
  path: NSH(string), fmode(m)
) :<!exnwrt> FILEref(*none*) = "ext#%"

(* ****** ****** *)
//
symintr fclose
symintr fclose_exn
//
fun
fclose0
(
  filr: FILEref
) :<!wrt> int = "mac#%"
fun
fclose1
  {l:addr}{m:fm}
(
  filp: !FILEptr(l, m) >> ptr(l)
) :<!wrt>
  [i:int | i <= 0]
(
  option_v (FILE_v (l, m), i < 0) | int i
) = "mac#%" // endfun
//
overload fclose with fclose0
overload fclose with fclose1
//
fun
fclose0_exn
  (filr: FILEref):<!exnwrt> void = "ext#%"
fun
fclose1_exn
  (filp: FILEptr1(*none*)):<!exnwrt> void = "ext#%"
//
overload fclose_exn with fclose0_exn
overload fclose_exn with fclose1_exn
//
(* ****** ****** *)

(*
fun fclose_stdin ():<!exnwrt> void = "ext#%"
fun fclose_stdout ():<!exnwrt> void = "ext#%"
fun fclose_stderr ():<!exnwrt> void = "ext#%"
*)

(* ****** ****** *)
(*
//
// FILE *freopen (const char *path, const char *mode, FILE *stream);
//
The [freopen] function opens the file whose name is the string pointed to
by path and associates the stream pointed to by stream with it.  The original
stream (if it exists) is closed.  The mode argument is used just as in the
fopen function.  The primary use of the freopen function is to change the file
associated with a standard text stream (stderr, stdin, or stdout).
//
*)
//
symintr freopen
symintr freopen_exn
//
fun
freopen0{m2:fm}
(
  path: NSH(string)
, mode: fmode(m2), filr: FILEref
) :<!wrt> Ptr0 = "mac#%"
//
// HX-2012-07:
// the original stream is closed even if [freopen] fails.
//
fun
freopen1
{m1,m2:fm}{l0:addr}
(
  path: NSH(string)
, mode: fmode(m2), filp: FILEptr(l0, m1)
) :<!wrt>
[
  l:addr | l==null || l==l0
] (
  option_v(FILE_v(l, m2), l > null) | ptr(l)
) = "mac#%" // end of [freopen1]
//
fun
freopen0_exn{m2:fm}
(
  path: NSH(string), mode: fmode(m2), filr: FILEref
) :<!exnwrt> void = "ext#%" // end of [freopen0_exn]
//
overload freopen with freopen0
overload freopen with freopen1
overload freopen_exn with freopen0_exn
//
(* ****** ****** *)

(*
fun
freopen_stdin
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stdin]
fun
freopen_stdout
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stdout]
fun
freopen_stderr
  (path: NSH(string)):<!exnwrt> void = "ext#%"
// end of [freopen_stderr]
*)

(* ****** ****** *)
(*
//
// int fileno (FILE* filp) ;
// 
The function fileno examines the argument stream and returns its integer
descriptor. In case fileno detects that its argument is not a valid stream,
it must return -1 and set errno to EBADF.
*)
//
fun
fileno0(filr: FILEref):<> int = "mac#%"
fun
fileno1(filp: !FILEptr1(*none*)):<> int = "mac#%"
//
symintr fileno
overload fileno with fileno0
overload fileno with fileno1
//
(* ****** ****** *)
//
(*
//
// HX-2011-08
//
*)
dataview
fdopen_v
(
  fd:int, addr, m: fmode
) = (* fdopen_v *)
  | {l:agz}
    fdopen_v_succ(fd, l, m) of FILE_v(l, m)
  | fdopen_v_fail(fd, null, m) of fildes_v(fd)
// end of [fdopen_v]
//
fun
fdopen
{fd:int}{m:fm}
(
  fd: fildes(fd), m: fmode(m)
) : [l:agez] 
(
  fdopen_v(fd, l, m) | ptr(l)
) = "mac#%" // end of [fdopen]
//
fun
fdopen_exn
{fd:int}{m:fm}
(fd: fildes(fd), m: fmode (m)): FILEptr1(m) = "ext#%"
// end of [fdopen_exn]
//
(* ****** ****** *)
(*  
//
// int feof (FILE *stream);
//
The function feof() returns a nonzero value if the end of the given file
stream has been reached.
//
*)
//
fun
feof0 (filr: FILEref):<> int = "mac#%"
fun
feof1 (filp: !FILEptr1(*none*)):<> int = "mac#%"
//
symintr feof
overload feof with feof0
overload feof with feof1
//
(* ****** ****** *)
(*
//
// int ferror (FILE *stream);
//
The function [ferror] tests the error indicator for the stream pointed to by
stream, returning non-zero if it is set.  The error indicator can only be
reset by the [clearerr] function.
*)
//
fun
ferror0 (filr: FILEref):<> int = "mac#%"
fun
ferror1 (filp: !FILEptr1(*none*)):<> int = "mac#%"
//
symintr ferror
overload ferror with ferror0
overload ferror with ferror1
//
(* ****** ****** *)
(*
//
// void clearerr (FILE *stream);
//
The function [clearerr] clears the end-of-file and error indicators for
the stream pointed to by stream.
//
*)
//
fun
clearerr0
  (filr: FILEref):<!wrt> void = "mac#%"
fun
clearerr1
  (filp: !FILEptr1(*none*)):<!wrt> void = "mac#%"
//
symintr clearerr
overload clearerr with clearerr0
overload clearerr with clearerr1
//
(* ****** ****** *)
(*
//
// int fflush (FILE *stream);
//
The function fflush forces a write of all user-space buffered data for the
given output or update stream via the streams underlying write function.
The open status of the stream is unaffected.
//
Upon successful completion 0 is returned.  Otherwise, EOF is returned and
the global variable errno is set to indicate the error.
*)
//
fun
fflush0
  (out: FILEref):<!wrt> int = "mac#%"
fun
fflush1{m:fm}
(
  pf: fmlte(m, w) | out: !FILEptr1(m)
) :<!wrt> [i:int | i <= 0] int(i) = "mac#%"
//
fun
fflush0_exn
  (out: FILEref):<!exnwrt> void = "ext#%"
//
symintr fflush
symintr fflush_exn
overload fflush with fflush0
overload fflush with fflush1
overload fflush_exn with fflush0_exn
//
(* ****** ****** *)
//
fun fflush_all ():<!exnwrt> void = "ext#%"
fun fflush_stdout ():<!exnwrt> void = "ext#%"
//
(* ****** ****** *)
(*
//
// int fgetc (FILE *stream)
//
[fgetc] reads the next character from stream and returns it as an
unsigned char cast to an int, or EOF on end of file or error. Note
that EOF must be a negative number!
//
*)
//
fun
fgetc0
  (inp: FILEref):<!wrt> int = "mac#%"
fun
fgetc1 {m:fm}
(
  pf: fmlte(m, r()) | inp: !FILEptr1(m)
) :<!wrt> intLte (UCHAR_MAX) = "mac#%"
//
symintr fgetc
overload fgetc with fgetc0
overload fgetc with fgetc1
//
(* ****** ****** *)

macdef getc = fgetc

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

fun
getchar0():<!wrt> int = "mac#%"
fun
getchar1():<!wrt> [i:int|i <= UCHAR_MAX] int(i) = "mac#%"

(* ****** ****** *)
//
fun
fgets0
{sz:int}{n0:pos | n0 <= sz}
(
  buf: &b0ytes(sz) >> bytes(sz), n0: int n0, inp: FILEref
) :<!wrt> Ptr0 = "mac#%" // = addr@(buf) or NULL
fun
fgets1
{sz:int}{n0:pos | n0 <= sz}{m:fm}
(
  pfm: fmlte (m, r)
| buf: &b0ytes(sz) >> bytes(sz), n0: int n0, inp: !FILEptr1(m)
) :<!wrt> Ptr0 = "mac#%" // = addr@(buf) or NULL
//
symintr fgets
overload fgets with fgets0
overload fgets with fgets1
//
(* ****** ****** *)
//
dataview
fgets_v
(
  sz:int, n0: int, addr, addr
) = (* fgets_v *)
  | {l0:addr}
    fgets_v_fail (sz, n0, l0, null) of b0ytes(sz) @ l0
  | {n:nat | n < n0} {l0:agz}
    fgets_v_succ (sz, n0, l0, l0) of strbuf(sz, n) @ l0
// end of [fgets_v]
//
fun
fgets1_err
{sz,n0:int
| 0 < n0
; n0 <= sz}
{l0:addr}{m:fm}
(
  pf_mod: fmlte(m, r)
, pf_buf: b0ytes(sz)@l0
| p0: ptr(l0), n0: int(n0), inp: !FILEptr1(m)
) :<> [l1:addr] (fgets_v(sz, n0, l0, l1) | ptr(l1)) = "mac#%"
// end of [fgets_err]
//
overload fgets with fgets1_err
//
(* ****** ****** *)
//
// HX-2013-05:
// A complete line is read each time // [nullp] for error
//
fun
fgets0_gc
  (bsz: intGte(1), inp: FILEref): Strptr0 = "ext#%"
fun
fgets1_gc{m:fm}
(
  pf_mod: fmlte (m, r) | bsz: intGte(1), inp: FILEptr1(m)
) : Strptr0 = "ext#%" // end of [fget1_gc]
//
(* ****** ****** *)
(*
//
// int fgetpos(FILE *stream, fpos_t *pos);
//
The [fgetpos] function stores the file position indicator of the given file
stream in the given position variable. The position variable is of type
fpos_t (which is defined in stdio.h) and is an object that can hold every
possible position in a FILE. [fgetpos] returns zero upon success, and a
non-zero value upon failure.
//
*)
//
abst@ype fpos_t = $extype"ats_fpos_type"
//
fun
fgetpos0
(
  filp: FILEref, pos: &fpos_t? >> opt (fpos_t, i==0)
) :<!wrt> #[i:int | i <= 0] int (i) = "mac#%"
fun fgetpos1
(
  filp: !FILEptr1, pos: &fpos_t? >> opt (fpos_t, i==0)
) :<!wrt> #[i:int | i <= 0] int (i) = "mac#%"
//
fun
fgetpos0_exn 
  (filp: FILEref, pos: &fpos_t? >> _) :<!exnwrt> void = "ext#%"
//
symintr fgetpos
symintr fgetpos_exn
overload fgetpos with fgetpos0
overload fgetpos with fgetpos1
overload fgetpos_exn with fgetpos0_exn 
//
(* ****** ****** *)
(*
//
// int fputc (int c, FILE *stream)
//
The function [fputc] writes the given character [c] to the given output
stream. The return value is the character, unless there is an error, in
which case the return value is EOF.
//
*)
//
typedef
fputc0_type
  (a:t0p) = (a, FILEref) -<0,!wrt> int
//
fun
fputc0_int : fputc0_type (int) = "mac#%" 
fun
fputc0_char : fputc0_type (char) = "mac#%" 
//
symintr fputc
overload fputc with fputc0_int of 0
overload fputc with fputc0_char of 0
//
typedef
fputc1_type
  (a:t0p) = {m:fm}
(
  fmlte (m, w()) | a, !FILEptr1 (m)
) -<0,!wrt> intLte (UCHAR_MAX)
fun fputc1_int : fputc1_type (int) = "mac#%"
fun fputc1_char : fputc1_type (char) = "mac#%"
overload fputc with fputc1_int of 10
overload fputc with fputc1_char of 10
//
typedef
fputc0_exn_type
  (a:t0p) = (a, FILEref) -<0,!exnwrt> void
//
fun
fputc0_exn_int : fputc0_exn_type (int) = "ext#%"
fun
fputc0_exn_char : fputc0_exn_type (char) = "ext#%"
//
symintr fputc_exn
overload fputc_exn with fputc0_exn_int of 0
overload fputc_exn with fputc0_exn_char of 0
//
(* ****** ****** *)

macdef putc = fputc

(* ****** ****** *)
//
fun
putchar0 (c: int):<!wrt> int = "mac#%"
fun
putchar1
  (c: int):<!wrt> [i:int|i <= UCHAR_MAX] int(i) = "mac#%"
// end of [putchar1]
//
(* ****** ****** *)
(*
//
// int fputs (const char* s, FILE *stream)
//
The function [fputs] writes a string to a file. it returns
a non-negative number on success, or EOF on error.
*)
//
//
fun
fputs0
(
  str: NSH(string), fil: FILEref
) :<!wrt> int = "mac#%"
fun
fputs1{m:fm}
(
  pf: fmlte(m, w()) | str: NSH(string), out: !FILEptr1(m)
) :<!wrt> int = "mac#%"
//
fun
fputs0_exn
  (str: NSH(string), fil: FILEref):<!exnwrt> void = "ext#%"
//
symintr fputs
symintr fputs_exn
overload fputs with fputs0
overload fputs with fputs1
overload fputs_exn with fputs0_exn
//
(* ****** ****** *)
//
// [puts] puts a newline at the end
//
fun
puts(inp: NSH(string)):<!wrt> int = "mac#%"
//
fun
puts_exn(inp: NSH(string)):<!exnwrt> void = "ext#%"
//
(* ****** ****** *)
(*
//
// size_t fread (void *ptr, size_t size, size_t nmemb, FILE *stream);
//
The function [fread] reads [nmemb] elements of data, each [size] bytes
long, from the stream pointed to by stream, storing them at the location
given by ptr. The return value is the number of items that are actually
read.
//
[fread] does not distinguish between end-of-file and error, and callers
must use [feof] and [ferror] to determine which occurred.
//
*)
//
fun
fread0 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &bytes(nbf) >> _
, isz: size_t isz, n: size_t n
, inp: FILEref(*none*)
) :<!wrt> sizeLte n = "mac#%"
fun
fread1 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
  {m:fm}
(
  pfm: fmlte (m, r)
| buf: &bytes(nbf) >> _
, isz: size_t isz, n: size_t n
, inp: !FILEptr1 (m)
) :<!wrt> sizeLte n = "mac#%"
//
fun
fread0_exn // [isz]: the size of each item
{isz:pos}
{nbf:int}
{n:int | n*isz <= nbf}
(
  buf: &bytes(nbf) >> _, isz: size_t isz, n: size_t n, inp: FILEref
) :<!exnwrt> sizeLte n = "ext#%" // endfun
//
symintr fread
symintr fread_exn
overload fread with fread0
overload fread with fread1
overload fread_exn with fread0_exn
//

(* ****** ****** *)
(*
//
// size_t fwrite (
//   const void *ptr,  size_t size,  size_t nmemb, FILE *stream
// ) ;
//
The function [fwrite] writes [nmemb] elements of data, each [size] bytes
long, to the stream pointed to by stream, obtaining them from the location
given by [ptr]. The return value is the number of items that are actually
written.
//
*)
//
fun
fwrite0 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: FILEref
) :<!wrt> sizeLte (n) = "mac#%"
fun
fwrite1 // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
  {m:fm}
(
  pfm: fmlte(m, w())
| buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: !FILEptr1 (m)
) :<!wrt> sizeLte (n) = "mac#%"
//
fun
fwrite0_exn // [isz]: the size of each item
  {isz:pos}
  {nbf:int}
  {n:int | n*isz <= nbf}
(
  buf: &RD(bytes(nbf))
, isz: size_t isz, n: size_t n
, out: FILEref(*none*)
) :<!exnwrt> sizeLte (n) = "ext#%"
//
symintr fwrite
symintr fwrite_exn
overload fwrite with fwrite0
overload fwrite with fwrite1
overload fwrite_exn with fwrite0_exn
//
(* ****** ****** *)
(*
//
// int fseek (FILE *stream, long offset, int whence)
//
The [fseek] function sets the file position indicator for the stream
pointed to by stream.  The new position, measured in bytes, is obtained by
adding offset bytes to the position specified by whence.  If whence is set
to [SEEK_SET], [SEEK_CUR], or [SEEK_END], the offset is relative to the
start of the file, the current position indicator, or end-of-file,
respectively.  A successful call to the [fseek] function clears the end-
of-file indicator for the stream and undoes any effects of the [ungetc]
function on the same stream. Upon success, [fseek] returns 0. Otherwise,
it returns -1.
//
*)
//
fun
fseek0
(
  filr: FILEref, offset: lint, whence: whence
) :<!wrt> int = "mac#%"
fun
fseek1
(
  filp: !FILEptr1, offset: lint, whence: whence
) :<!wrt> int = "mac#%"
//
fun
fseek0_exn
(
  filr: FILEref, offset: lint, whence: whence
) :<!exnwrt> void = "ext#%"
//
symintr fseek
symintr fseek_exn
overload fseek with fseek0
overload fseek with fseek1
overload fseek_exn with fseek0_exn
//
(* ****** ****** *)
(*
//
// void fsetpos(FILE *stream, const fpos_t *pos);
//
The [fsetpos] function moves the file position indicator for the given
stream to a location specified by the position object. The type fpos_t is
defined in stdio.h.  The return value for fsetpos() is zero upon success,
non-zero on failure.
//
*)
//
fun
fsetpos0
(filp: FILEref(*none*), pos: &RD(fpos_t)):<!wrt> int = "mac#%"
fun
fsetpos1
(filp: !FILEptr1(*none*), pos: &RD(fpos_t)):<!wrt> int = "mac#%"
//
fun
fsetpos0_exn
(filp: FILEref(*none*), pos: &RD(fpos_t)):<!exnwrt> void = "ext#%"
//
symintr fsetpos
symintr fsetpos_exn
overload fsetpos with fsetpos0
overload fsetpos with fsetpos1
overload fsetpos_exn with fsetpos0_exn
//
(* ****** ****** *)

(*
//
// long ftell (FILE *stream)
//
[ftell] returns the current offset of the given file stream upon on
success. Otherwise, -1 is returned and the global variable errno is set to
indicate the error.
//
*)
//
fun
ftell0
  (filr: FILEref):<!wrt> lint = "mac#%"
fun
ftell1
  (filp: !FILEptr1):<!wrt> lint = "mac#%"
//
fun
ftell0_exn
  (filr: FILEref):<!exnwrt> lint = "ext#%"
//
symintr ftell
symintr ftell_exn
overload ftell with ftell0
overload ftell with ftell1
overload ftell_exn with ftell0_exn
//
(* ****** ****** *)

(*
//
// perror - print a system error message
//
The routine [perror(s)] produces a message on the standard error output,
describing the last error encountered during a call to a system or library
function.  First (if s is not NULL and *s is not NULL) the argument string
s is printed, followed by a colon and a blank.  Then the message and a
newline.
//
*)
fun
perror
  (msg: NSH(string)):<!wrt> void = "mac#%"
// end of [perror]
//
(* ****** ****** *)
//
abstype
pmode_type(m:fm) = string
typedef
pmode(m:fm) = pmode_type(m)
//
absview
popen_view(l:addr)
viewdef
popen_v(l:addr) = popen_view(l)
//
praxi
popen_v_free_null (pf: popen_v (null)): void
//
fun
popen{m:fm}
(
  cmd: NSH(string), mode: pmode (m)
) : [l:addr] (popen_v (l) | FILEptr (l, m))
//
fun
popen_exn{m:fm}
(
  cmd: NSH(string), mode: pmode (m)
) : FILEref = "ext#%" // endfun
//
fun
pclose0_exn (filr: FILEref): int = "ext#%"
fun
pclose1_exn
{l:agz}{m:fm}
(pf: popen_v l | filr: FILEptr (l, m)): int= "ext#%"
// end of [pclose1_exn]
//
(* ****** ****** *)
//
fun
remove
  (inp: NSH(string)):<!wrt> int = "mac#%"
fun
remove_exn
  (inp: NSH(string)):<!exnwrt> void = "ext#%"
//
(* ****** ****** *)

fun rename
(
  oldpath: NSH(string), newpath: NSH(string)
) :<!wrt> int = "mac#%" // end of [fun]

fun rename_exn
(
  oldpath: NSH(string), newpath: NSH(string)
) :<!exnwrt> void = "ext#%" // end of [fun]

(* ****** ****** *)
(*
// HX: [rewind] generates no error
*)
//
fun
rewind0
  (fil: FILEref):<!wrt> void = "mac#%"
//
fun
rewind1
  (fil: !FILEptr1(*none*)):<!wrt> void = "mac#%"
//
symintr rewind
overload rewind with rewind0
overload rewind with rewind1
//
(* ****** ****** *)
//
fun
tmpfile() :<!wrt> FILEptr0 (rw()) = "mac#%"
//
fun
tmpfile_exn() :<!exnwrt> FILEptr1 (rw()) = "ext#%"
//
fun
tmpfile_ref_exn() :<!exnwrt> FILEref(*none*) = "ext#%"
//
(* ****** ****** *)
(*
//
// int ungetc(int c, FILE *stream);
//
[ungetc] pushes [c] back to stream, cast to unsigned char, where it is
available for subsequent read operations.  Pushed-back characters will be
returned in reverse order; only one pushback is guaranteed.
//
*)
//
fun
ungetc0
  (c: char, f: FILEref):<!wrt> int = "mac#%"
fun
ungetc1
  {l:agz}{m:fm}
(
  pfm: fmlte (m, rw()) | c: char, f: !FILEptr (l, m)
) :<!wrt> [i:int | i <= UCHAR_MAX] int (i) = "mac#%"
//
fun
ungetc0_exn
  (c: char, f: FILEref) :<!exnwrt> void = "ext#%"
//
symintr ungetc
symintr ungetc_exn
overload ungetc with ungetc0
overload ungetc with ungetc1
overload ungetc_exn with ungetc0_exn
//
(* ****** ****** *)
//
stacst
BUFSIZ : int
//
praxi BUFSIZ_gtez (): [BUFSIZ >= 0] void
//
macdef BUFSIZ = $extval(int(BUFSIZ), "BUFSIZ")
//
(* ****** ****** *)
//
abst@ype bufmode_t = int
//
macdef _IOFBF = $extval(bufmode_t, "_IOFBF") // fully buffered
macdef _IOLBF = $extval(bufmode_t, "_IOLBF") // buffered by line
macdef _IONBF = $extval(bufmode_t, "_IONBF") // there is no buffering
//
(* ****** ****** *)
//
fun
setbuf0_null
  (f: FILEref): void = "mac#%"
fun
setbuf1_null
  (f: !FILEptr1(*none*)): void = "mac#%"
//
symintr setbuf_null
overload setbuf_null with setbuf0_null
overload setbuf_null with setbuf1_null
//
(* ****** ****** *)
(*
//
// HX-2010-10-03:
// the buffer can be freed only after it is no longer used by
// the stream to which it is attached!!!
*)
//
fun
setbuffer0
{n1,n2:nat | n2 <= n1}{l:addr}
(
  pf_buf: !b0ytes(n1)@l
| filr: FILEref, p_buf: ptr(l), n2: size_t(n2)
) : void = "mac#%"
//
fun
setbuffer1
{ n1
, n2: nat
| n2 <= n1
}{lbf:addr}
(
  pf_buf: !b0ytes(n1)@lbf
| filp: !FILEptr1(*none*), p_buf: ptr(lbf), n2: size_t(n2)
) : void = "mac#%"
//
symintr setbuffer
overload setbuffer with setbuffer0
overload setbuffer with setbuffer1
//
(* ****** ****** *)
//
fun
setlinebuf0
  (f: FILEref): void = "mac#%"
fun
setlinebuf1
  (f: !FILEptr1(*none*)): void = "mac#%"
//
symintr setlinebuf
overload setlinebuf with setlinebuf0
overload setlinebuf with setlinebuf1
//

(* ****** ****** *)
//
fun
setvbuf0_null
  (f: FILEref, mode: bufmode_t): int = "mac#%"
fun
setvbuf1_null
  (f: !FILEptr1(*none*), mode: bufmode_t): int = "mac#%"
//
symintr setvbuf_null
overload setvbuf_null with setvbuf0_null
overload setvbuf_null with setvbuf1_null
//
(* ****** ****** *)
//
fun
setvbuf0
{ n1
, n2:nat
| n2 <= n1
}{lbf:addr}
(
  pf: !b0ytes(n1)@lbf
| filr: FILEref, mode: bufmode_t, n2: size_t(n2)
) : int = "mac#%"
fun
setvbuf1
{ n1
, n2 : nat
| n2 <= n1
}{lbf:addr}
(
  pf: !b0ytes(n1) @ lbf
| filp: !FILEptr1(*none*), mode: bufmode_t, n2: size_t(n2)
) : int = "mac#%"
//
symintr setvbuf
overload setvbuf with setvbuf0
overload setvbuf with setvbuf1
//
(* ****** ****** *)

(* end of [stdio.sats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi
// Authoremail: gmhwxiATgmailDOTcom
// Start Time: June, 2012
//
(* ****** ****** *)

%{#
//
#include \
"libats/libc/CATS/stdlib.cats"
//
%} // end of [%{#]

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
//
// HX: prefix for external names
//
#define
ATS_EXTERN_PREFIX "atslib_libats_libc_"
//
(* ****** ****** *)

vtypedef
RD(a:vt0p) = a // for commenting: read-only
#define NSH(x) x // for commenting: no sharing
#define SHR(x) x // for commenting: it is shared

(* ****** ****** *)
//
staload
STDDEF =
"libats/libc/SATS/stddef.sats"
//
typedef wchar_t = $STDDEF.wchar_t
//
(* ****** ****** *)

macdef EXIT_FAILURE = $extval(int, "EXIT_FAILURE")
macdef EXIT_SUCCESS = $extval(int, "EXIT_SUCCESS")

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

abst@ype div_t = $extype"div_t"
abst@ype ldiv_t = $extype"ldiv_t"
abst@ype lldiv_t = $extype"lldiv_t"

(* ****** ****** *)
/*
void _Exit(int);
*/
fun _Exit (int): void = "mac#%"

/*
int atexit(void (*)(void));
*/
fun atexit
  (f: ((*void*)) -> void): int(*err*) = "mac#%"
// end of [atexit]

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

/*
void abort(void);
*/
fun abort((*void*)): void = "mac#%"

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

/*
int abs(int)
*/
fun abs(int):<> int = "mac#%"
/*
long int labs(long int j);
*/
fun labs(lint):<> lint = "mac#%"
/*
long long int llabs(long long int j);
*/
fun llabs(lint):<> llint = "mac#%"

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

/*
div_t div(int, int);
*/
fun div(int, int):<> div_t
/*
ldiv_t ldiv(long, long);
*/
fun ldiv(lint, lint):<> ldiv_t
/*
lldiv_t lldiv(long long, long long);                              
*/
fun lldiv(llint, llint):<> lldiv_t

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

/*
long a64l(const char *);
*/
fun a64l(x: NSH(string)):<> lint = "mac#%"

/*
char *l64a(long value); // not defined for a negative value
*/
fun l64a
  {i:nat}
(
  x: lint i
) :<!refwrt> [l:agz] vttakeout0(strptr(l)) = "mac#%"
// end of [l64a]

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

/*
int atoi(const char *);
*/
fun atoi(x: NSH(string)):<> int = "mac#%"

/*
long atol(const char *);
*/
fun atol(x: NSH(string)):<> lint = "mac#%"

/*
long long atoll(const char *);
*/
fun atoll(x: NSH(string)):<> llint = "mac#%"
                                          
(* ****** ****** *)

/*
double atof(const char *);
*/
fun atof(x: NSH(string)):<> double = "mac#%"

(* ****** ****** *)
//
/*
long int
strtol(const char *nptr, char **endptr, int base);
*/
fun strtol0
  (nptr: string, base: intBtwe(2, 36)):<!wrt> lint = "mac#%"
fun strtol1
  (nptr: string, endptr: &ptr? >> _, base: intBtwe(2, 36)):<!wrt> lint = "mac#%"
fun strtol_unsafe
  (nptr: string, endptr: ptr, base: int):<!wrt> lint = "mac#%"
// end of [strtol_unsafe]
//
symintr strtol
overload strtol with strtol0
overload strtol with strtol1
//
/*
long long int
strtoll(const char *nptr, char **endptr, int base);
*/
fun strtoll0
  (nptr: string, base: intBtwe(2, 36)):<!wrt> llint
fun strtoll1
  (nptr: string, endptr: &ptr? >> _, base: intBtwe(2, 36)):<!wrt> llint
fun strtoll_unsafe
  (nptr: string, endptr: ptr, base: int):<!wrt> llint
// end of [strtoll_unsafe]
//
symintr strtoll
overload strtoll with strtoll0
overload strtoll with strtoll1
//
(* ****** ****** *)
//
/*
unsigned long
strtoul(const char *nptr, char **endptr, int base);
*/
fun strtoul0
  (nptr: string, base: intBtwe(2, 36)):<!wrt> ulint
fun strtoul1
  (nptr: string, endptr: &ptr? >> _, base: intBtwe(2, 36)):<!wrt> ulint
fun strtoul_unsafe
  (nptr: string, endptr: ptr, base: int):<!wrt> ulint
// end of [strtoul_unsafe]
//
symintr strtoul
overload strtoul with strtoul0
overload strtoul with strtoul1
//
/*
unsigned long long
strtoull(const char *nptr, char **endptr, int base);
*/
fun strtoull0
  (nptr: string, base: intBtwe(2, 36)):<!wrt> ullint
fun strtoull1
  (nptr: string, endptr: &ptr? >> _, base: intBtwe(2, 36)):<!wrt> ullint
fun strtoull_unsafe
  (nptr: string, endptr: ptr, base: int):<!wrt> ullint
// end of [strtoull_unsafe]
//
symintr strtoull
overload strtoull with strtoull0
overload strtoull with strtoull1
//
(* ****** ****** *)
/*
float
strtof(const char *nptr, char **endptr);
*/
fun
strtof0
  (nptr: string):<!wrt> float = "mac#%"
fun
strtof1
  (nptr: string, endptr: &ptr? >> _):<!wrt> float = "mac#%"
fun strtof_unsafe
  (nptr: string, endptr: ptr):<!wrt> float = "mac#%"
// end of [strtof_unsafe]
//
symintr strtof
overload strtof with strtof0
overload strtof with strtof1
//
(* ****** ****** *)
/*
double
strtod(const char *nptr, char **endptr);
*/
fun
strtod0
  (nptr: string):<!wrt> double = "mac#%"
fun
strtod1
  (nptr: string, endptr: &ptr? >> _):<!wrt> double = "mac#%"
fun
strtod_unsafe
  (nptr: string, endptr: ptr):<!wrt> double = "mac#%"
// end of [strtod_unsafe]
//
symintr strtod
overload strtod with strtod0
overload strtod with strtod1
//
(* ****** ****** *)
/*
long double
strtold(const char *nptr, char **endptr);
*/
fun
strtold0
  (nptr: string):<!wrt> ldouble = "mac#%"
fun
strtold1
  (nptr: string, endptr: &ptr? >> _):<!wrt> ldouble = "mac#%"
fun
strtold_unsafe
  (nptr: string, endptr: ptr):<!wrt> ldouble = "mac#%"
// end of [strtold_unsafe]
//
symintr strtold
overload strtold with strtold0
overload strtold with strtold1
//
(* ****** ****** *)

(*
//
// HX: these env-functions may not be reentrant!
//
*)

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

/*
char *getenv(char *);
*/
fun getenv
(
  name: NSH(string)
) :<!ref> [l:addr] vttakeout0(strptr(l)) = "mac#%"

fun{} getenv_gc(name: NSH(string)):<!refwrt> Strptr0

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

/*
int putenv(char *);
*/
//
// HX: [nameval] is shared!
//
fun putenv
  (nameval: SHR(string)):<!refwrt> int = "mac#%"
// end of [putenv]

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

/*
int setenv
(
  const char *name, const char *value, int overwrite
) ;
*/
fun setenv
(
  name: NSH(string), value: NSH(string), overwrite: int
) :<!refwrt> int = "mac#%"

/*
int unsetenv(const char *name);
*/
fun unsetenv
  (name: NSH(string)):<!refwrt> int = "mac#%"
// end of [unsetenv]

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

/*
int clearenv(void);
*/
fun clearenv ((*void*)):<!refwrt> int = "mac#%"

(* ****** ****** *)
//
// HX:
// these funs seem to have become obsolete
//
fun rand ((*void*)):<!refwrt> int = "mac#%"
fun srand (seed: uint):<!refwrt> void = "mac#%"

fun rand_r (seed: &uint >> _):<> int = "mac#%"

(* ****** ****** *)
//
/*
long int random(void);
*/
fun random((*void*)):<!refwrt> lint = "mac#%"
//
/*
void srandom(unsigned int seed);
*/
fun srandom(seed: uint):<!refwrt> void = "mac#%"
//
/*
char
*initstate
(
  unsigned int seed, char *state, size_t n
) ;
*/
fun
initstate_unsafe
(
  seed: uint, state: cPtr1(char), n: sizeGte(8)
) : cPtr0(char) = "mac#%"
// end of [initstate_unsafe]
//
/*
char *setstate(char *state);
*/
fun setstate_unsafe
  (state: cPtr1(char)):<!ref> cPtr0(char) = "mac#%"
// end of [setstate_unsafe]
//
(* ****** ****** *)
/*
double drand48(void); // obsolete
*/
fun drand48 ((*void*)):<!ref> double = "mac#%"
     
/*
double erand48(unsigned short xsubi[3]); // obsolete
*/
fun erand48
  (xsubi: &(@[usint][3])):<!ref> double = "mac#%"
// end of [erand48]

/*
long int lrand48(void); // obsolete
*/
fun lrand48 ((*void*)):<!ref> lint = "mac#%"
/*
long int nrand48(unsigned short xsubi[3]); // obsolete
*/
fun nrand48
  (xsubi: &(@[usint][3])):<!ref> lint = "mac#%"
// end of [nrand48]

/*
long int mrand48(void); // obsolete
*/
fun mrand48 ((*void*)):<!ref> lint = "mac#%"

/*
long int jrand48(unsigned short xsubi[3]); // obsolete
*/
fun jrand48
  (xsubi: &(@[usint][3])):<!ref> lint = "mac#%"
// end of [jrand48]

/*
void srand48(long int seedval); // obsolete
*/
fun srand48 (seedval: lint):<!ref> void = "mac#%"

/*
unsigned short *seed48(unsigned short seed16v[3]); // obsolete
*/
// HX: returning pointer to some internal buffer
fun seed48 (seed16v: &(@[usint][3])): Ptr1 = "mac#%"

/*
void lcong48(unsigned short param[7]); // obsolete
*/
fun lcong48 (param: &(@[usint][7])):<!ref> void = "mac#%"

(* ****** ****** *)
/*
void
*bsearch
(
  const void *key
, const void *base
, size_t nmemb, size_t size
, int (*compar)(const void *, const void *)
) ; // end of [bsearch]
*/
fun bsearch
  {a:vt0p}{n:int}
(
  key: &RD(a)
, arr: &RD(@[INV(a)][n])
, asz: size_t (n), tsz: sizeof_t (a)
, cmp: cmpref (a)
) :<> Ptr0 = "mac#%" // end of [bsearch]

(* ****** ****** *)
/*
void qsort
(
  void *base, size_t nmemb, size_t size
, int(*compar)(const void *, const void *)
) ; // end of [qsort]
*/
fun qsort
  {a:vt0p}{n:int}
(
  A: &(@[INV(a)][n]), asz: size_t (n), tsz: sizeof_t (a), cmp: cmpref (a)
) :<!wrt> void = "mac#%" // end of [qsort]

(* ****** ****** *)
/*
int mblen(const char *s, size_t);
*/
fun
mblen_unsafe
  (s: cPtr0(char), n: size_t):<!refwrt> int = "mac#%"
// end of [mblen_unsafe]

/*
int wctomb(char *s, wchar_t wc);
*/
fun
wctomb_unsafe
  (s: cPtr0(char), wc: wchar_t):<!refwrt> int = "mac#%"
// end of [wctomb_unsafe]

/*
size_t
wcstombs(char *dest, const wchar_t *src, size_t);
*/
fun
wcstombs_unsafe
(
  dest: cPtr0(char), src: cPtr1(wchar_t), n: size_t
) :<!refwrt> ssize_t = "mac#%" // endfun

(* ****** ****** *)
/*
void setkey(const char *key);
*/
fun setkey_unsafe (key: cPtr1(char)):<!ref> void = "mac#%"

(* ****** ****** *)
/*
int mkstemp(char *template);
*/
fun
mkstemp
{n:int | n >= 6}
  (template: !strnptr(n)): int = "mac#%"
// end of [mkstemp] // endfun
//
/*
int mkostemp(char *template, int flags);
*/
fun
mkostemp
{n:int | n >= 6}
  (template: !strnptr(n), flags: int): int = "mac#%"
// end of [mkostemp] // endfun
//
(* ****** ****** *)
/*
int grantpt(int fd);
*/
fun grantpt (fd: int): int = "mac#%"
//
(* ****** ****** *)

dataview
malloc_libc_v
  (addr, int) =
  | {n:int}
    malloc_libc_v_fail
      (null, n)
    // malloc_libc_v_fail
  | {l:agz}{n:int}
    malloc_libc_v_succ
      (l(*addr*), n) of (b0ytes(n) @ l, mfree_libc_v(l))
    // malloc_libc_v_succ
// end of [malloc_libc_v]

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

fun
malloc_libc
  {n:int}
(
  bsz: size_t n
) :<!wrt>
[
  l:addr
] (
  malloc_libc_v(l, n) | ptr(l)
) = "mac#%" // end of [malloc]

fun
malloc_libc_exn
  {n:int}
(
  bsz: size_t(n)
) :<!wrt>
[
  l:addr | l > null
] (
  b0ytes(n)@l, mfree_libc_v(l) | ptr(l)
) = "mac#%" // end of [malloc_exn]

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

fun mfree_libc
  {l:addr}{n:int}
(
  b0ytes(n)@l, mfree_libc_v(l) | ptr(l)
) :<!wrt> void = "mac#%" // end-of-fun

(* ****** ****** *)
//
/*
int system(const char *command);
*/
fun system(command: NSH(string)): int = "mac#%"
//
(* ****** ****** *)

(* end of [stdlib.sats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi (gmhwxi AT gmail DOT com)
// Start Time: March, 2013
//
(* ****** ****** *)

%{#
#include \
"libats/libc/CATS/string.cats"
%} // end of [%{#]

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
//
// HX: prefix for external names
//
#define
ATS_EXTERN_PREFIX "atslib_libats_libc_"
//
(* ****** ****** *)

vtypedef
RD(a:vt0p) = a // for commenting: read-only
#define NSH (x) x // for commenting: no sharing
#define SHR (x) x // for commenting: it is shared

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

fun strcmp (x1: string, x2: string):<> int = "mac#%"
fun strncmp (x1: string, x2: string, n: size_t):<> int = "mac#%"

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

fun strcoll (x1: string, x2: string):<> int = "mac#%"

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

fun strspn (x1: string, x2: string):<> size_t = "mac#%"
fun strcspn (x1: string, x2: string):<> size_t = "mac#%"

(* ****** ****** *)
//
fun strlen
  {n:int} (x: string n):<> size_t (n) = "mac#%"
fun strnlen {m,n:int}
  (x: string n, max: size_t m):<> size_t (min(m,n)) = "mac#%"
//
(* ****** ****** *)

fun strcat
  {l:addr}{m:int}{n1,n2:int | n1+n2 < m}
(
  !strbuf_v (l, m, n1) >> strbuf_v (l, m, n1+n2) | ptr (l), string (n2)
) :<!wrt> ptr (l) = "mac#%" // end of [strcat]

fun strcat_unsafe
  {l:addr} (x1: ptr (l), x2: string):<!wrt> ptr (l) = "mac#%"
fun strncat_unsafe
  {l:addr} (x1: ptr (l), x2: string, n: size_t):<!wrt> ptr (l) = "mac#%"

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

fun strcpy
  {l:addr}{m:int}{n:int | n < m}
(
  !b0ytes(m) @ l >> strbuf_v (l, m, n) | ptr (l), string (n)
) :<!wrt> ptr (l) = "mac#%" // endfun

fun strcpy_unsafe
  {l:addr} (dst: ptr (l), src: string):<!wrt> ptr (l) = "mac#%"
fun strncpy_unsafe
  {l:addr} (dst: ptr (l), src: string, n: size_t):<!wrt> ptr (l) = "mac#%"

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

absview strdup_view (l:addr)
viewdef strdup_v (l:addr) = strdup_view (l)

fun strdup
(
  str: string
) :<!wrt> [l:addr] (strdup_v (l) | strptr (l)) = "mac#%"
fun strndup
(
  str: string
) :<!wrt> [l:addr] (strdup_v (l) | strptr (l)) = "mac#%"

fun strdup_free
  {l:addr} (pf: strdup_v (l) | x: strptr l):<!wrt> void = "mac#%"
// end of [strdup_free]

(* ****** ****** *)
//
// HX-2013-03:
// strdupa-functions are gcc-functions;
// they use alloca for memory allocation
//
absview strdupa_view (l:addr)
viewdef strdupa_v (l:addr) = strdupa_view (l)

fun strdupa
(
  str: string
) :<!wrt> [l:addr] (strdupa_v (l) | strptr (l)) = "mac#%"
fun strndupa
(
  str: string
) :<!wrt> [l:addr] (strdupa_v (l) | strptr (l)) = "mac#%"

fun strdupa_free
  {l:addr} (pf: strdupa_v (l) | x: strptr l):<!wrt> void = "mac#%"
// end of [strdupa_free]

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

fun strfry {l:agz} (x: !strptr (l) >> _):<!wrt> ptr (l) = "mac#%"

(* ****** ****** *)
//
fun memcpy
  {l:addr}
  {n1,n2:int}
  {n:int | n <= n1; n <= n2}
(
  pf: !b0ytes(n1) @ l >> bytes(n1) @ l
| dst: ptr (l), src: &RD(@[byte][n2]), n: size_t (n)
) :<!wrt> ptr (l) = "mac#%" // end of [memcpy]
//
fun memcpy_unsafe{l:addr}
  (dst: ptr (l), src: ptr, n: size_t):<!wrt> ptr (l) = "mac#%"
//
(* ****** ****** *)
/*
void *memset(void *s, int c, size_t n);
*/
fun memset_unsafe{l:addr}
  (dst: ptr (l), c: int, n: size_t): ptr (l) = "mac#%"
//
(* ****** ****** *)
/*
void *memmove(void *dest, const void *src, size_t n);
*/
fun memmove_unsafe{l:addr}
  (dst: ptr (l), src: ptr, n: size_t):<!wrt> ptr (l) = "mac#%"
//
(* ****** ****** *)
/*
void *memccpy(void *dest, const void *src, int c, size_t n);
*/
fun memccpy_unsafe{l:addr}
  (dst: ptr (l), src: ptr, c: int, n: size_t):<!wrt> Ptr0 = "mac#%"
//
(* ****** ****** *)
//
fun mempcpy
  {l:addr}
  {n1,n2:int}
  {n:int | n <= n1; n <= n2}
(
  pf: !b0ytes(n1) @ l >> bytes(n1) @ l
| dst: ptr (l), src: &RD(@[byte][n2]), n: size_t (n)
) :<!wrt> ptr (l+n) = "mac#%" // end of [mempcpy]
//
fun mempcpy_unsafe{l:addr}{n:int}
  (dst: ptr (l), src: ptr, n: size_t (n)):<!wrt> ptr (l+n) = "mac#%"
//
(* ****** ****** *)
//
// HX: This one is non-reentrant:
//
fun strerror
  (errnum: int):<!ref> [l:agz] vttakeout0 (strptr l) = "mac#%"
// end of [strerror]

(* ****** ****** *)
/*
int strerror_r(int errnum, char *buf, size_t buflen);
*/
fun strerror_r{n:int}
  (errnum: int, buf: &bytes(n), n: size_t (n)):<> int = "mac#%"
// end of [strerror_r]

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

fun strerror_r_gc (errnum: int):<> Strptr1 = "ext#%"

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

(* end of [string.sats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: April, 2012 *)

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

%{#
#include \
"libats/libc/CATS/unistd.cats"
%} // end of [%{#]

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
//
// HX: prefix for external names
//
#define ATS_EXTERN_PREFIX "atslib_libats_libc_"
//
(* ****** ****** *)

#define SHR(x) x // SHARED // HX: for commenting
#define NSH(x) x // NSHARED // HX: for commenting

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

typedef interr = int

(* ****** ****** *)
//
staload
TYPES =
"libats/libc/SATS/sys/types.sats"
//
typedef off_t = $TYPES.off_t
//
typedef pid_t = $TYPES.pid_t
typedef uid_t = $TYPES.uid_t
typedef gid_t = $TYPES.gid_t
//
stadef fildes_v = $TYPES.fildes_v
//
vtypedef
fildes (i:int) = $TYPES.fildes (i)
//
vtypedef Fildes = $TYPES.Fildes
vtypedef Fildes0 = $TYPES.Fildes0
//
(* ****** ****** *)

macdef STDIN_FILENO = $extval(int, "STDIN_FILENO")
macdef STDOUT_FILENO = $extval(int, "STDOUT_FILENO")
macdef STDERR_FILENO = $extval(int, "STDERR_FILENO")

(* ****** ****** *)
/*
int close (int);
*/
symintr close
symintr close_exn
//
fun close0 (fd: int): interr = "mac#%"
//
// HX-2013-03-25: should this be moved to unistd.sats?
//
dataview
close_v (fd:int, int) =
  | close_v_succ (fd, 0) of ()
  | {i:int | i < 0} close_v_fail (fd, i) of fildes_v (fd)
//
fun close1{fd:nat}
  (fd: fildes (fd)): [i:int] (close_v (fd, i) | int i) = "mac#%"
//
overload close with close0
overload close with close1
//
fun close0_exn (fd: int): void = "ext#%"
fun close1_exn (fd: Fildes0):<!exn> void = "ext#%"
//
overload close_exn with close0_exn
overload close_exn with close1_exn
//
(* ****** ****** *)

fun dup (fildes: int): int = "mac#%"
fun dup_fildes (fd: !Fildes0): Fildes = "mac#%"

(* ****** ****** *)
//
fun dup2
  (fildes: int, fildes2: int): int = "mac#%"
//
// HX-2013-05:
// this one requires that [fd2] be not in use
//
fun dup2_fildes{fd2:nat}
  (fd: !Fildes0, fd2: int (fd2)): Fildes = "mac#%"
//
(* ****** ****** *)
//
// HX: this one requires -D_GNU_SOURCE
//
fun dup3
  (fildes: int, fildes2: int, flags: int): int = "mac#%"
//
(* ****** ****** *)
//
fun
execv
{n:pos}{l:addr}
(
  pf: !parray_v (string, l, n) | path: NSH(string), argv: ptr l
) : intLt(0) = "mac#atslib_libats_libc_execv"
fun
execv_unsafe // HX: for failure, ~1 is returned
  (path: NSH(string), argv: ptr): intLt(0) = "mac#atslib_libats_libc_execv"
//
fun
execvp
{n:pos}{l:addr}
(
  pf: !parray_v (string, l, n) | fname: NSH(string), argv: ptr l
) : intLt(0) = "mac#atslib_libats_libc_execvp"
fun
execvp_unsafe // HX: for failure, ~1 is returned
  (fname: NSH(string), argv: ptr): intLt(0) = "mac#atslib_libats_libc_execvp"
//
(* ****** ****** *)
/*
//
// HX: for failure, ~1 is returned
//
int
execve
(
  const char *filename
, char *const argv[], char *const envp[]
) ;
*/
fun
execve
{n1,n2:pos}
{l1,l2:addr}
(
  pf1: !parray_v(string, l1, n1)
, pf2: !parray_v(string, l2, n2)
| fname: NSH(string), argv: ptr(l1), envp: ptr(l2)
) : intLt(0) = "mac#atslib_libats_libc_execve"
fun
execve_unsafe
(
  fname: NSH(string), argv: ptr(*parray*), envp: ptr(*parray*)
) : intLt(0) = "mac#atslib_libats_libc_execve"
// end of [execve_unsafe]

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

/*
void
encrypt(char block[64], int edflag);
*/
fun
encrypt
(
  block: &(@[char][64]), edflag: int
) :<!ref> void = "mac#%" // endfun

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

fun fork ((*void*)): pid_t = "mac#%"

(* ****** ****** *)
//
dataview
getcwd_v
(
  m:int, l:addr, addr
) =
  | {l>null}{n:nat}
    getcwd_v_succ(m, l, l) of strbuf_v(l, m, n)
  | getcwd_v_fail(m, l, null) of b0ytes(m) @ (l)
// end of [getcwd_v]
//
fun getcwd
  {m:nat} {l:addr}
(
  pf: !b0ytes(m)@l >> getcwd_v(m, l, l1) | p: ptr(l), m: size_t(m)
) : #[l1:addr] ptr (l1) = "mac#%" // end of [getcwd]
//
fun getcwd_gc (): Strptr0 = "ext#%" // HX: this is a convenient wrapper
//
(* ****** ****** *)
//
/*
pid_t getpid(void);
pid_t getppid(void);
*/
fun getpid ((*void*)): pid_t = "mac#%"
fun getppid ((*void*)): pid_t = "mac#%"
//
(* ****** ****** *)

fun getuid(): uid_t = "mac#%"
fun setuid(uid: uid_t): int = "mac#%"
fun geteuid(): uid_t = "mac#%"
fun seteuid(uid: uid_t): int = "mac#%"

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

fun getgid(): gid_t = "mac#%"
fun setgid(gid: gid_t): int = "mac#%"
fun getegid(): gid_t = "mac#%"
fun setegid(gid: gid_t): int = "mac#%"
        
(* ****** ****** *)

fun setreuid(ruid: uid_t, euid: uid_t): int = "mac#%"
fun setregid(rgid: gid_t, egid: gid_t): int = "mac#%"

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

fun setresuid(ruid: uid_t, euid: uid_t, suid: uid_t): int = "mac#%"
fun setresgid(rgid: gid_t, egid: gid_t, sgid: gid_t): int = "mac#%"
          
(* ****** ****** *)
//
// HX: these are linux-specific!
//
fun setfsuid(fsuid: uid_t): int = "mac#%"
fun setfsgid(fsgid: gid_t): int = "mac#%"
//
(* ****** ****** *)
//
fun getlogin(): vStrptr0 = "mac#%"
//
fun getlogin_r
  {n:int | n >= 2}
  (buf: &bytes(n), size_t(n)): int = "mac#%"
//
fun getlogin_r_gc((*void*)): Strptr0 = "ext#%"
//
(* ****** ****** *)
//
// HX: [pause] can only returns -1
//
fun pause ((*void*)): int = "mac#%"
//
(* ****** ****** *)

fun read_err
  {sz,n:nat | n <= sz}
(
  fd: !Fildes0
, buf: &b0ytes(sz) >> bytes(sz), ntotal: size_t(n)
) : ssizeBtw(~1, n+1) = "mac#%" // end-of-fun

fun write_err
  {sz,n:nat | n <= sz}
(
  fd: !Fildes0, buf: &RD(bytes(sz)), ntotal: size_t(n)
) : ssizeBtw(~1, n+1) = "mac#%" // end-of-fun

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

fun pread{n:int}
(
  fd: !Fildes0, buf: &(@[byte][n])>>_, n: size_t (n), ofs: off_t
) : ssize_t = "mac#%" // end of [pread]

fun pwrite{n:int}
(
  fd: !Fildes0, buf: &RD(array(byte, n)), n: size_t (n), ofs: off_t
) : ssize_t = "mac#%" // end of [pwrite]

(* ****** ****** *)
//
absview
alarm_v(n: int) // n: remaining seconds
//
praxi
alarm_v_elim (pfrem: alarm_v(0)): void
//
fun
alarm_set{i:int}
  (t: uint(i)): (alarm_v(i) | uInt) = "mac#%"
// end of [alarm_set]
fun
alarm_cancel{i:int}
  (pf: alarm_v(i) | (*none*)): uInt = "mac#%"
// end of [alarm_cancel]
//
(* ****** ****** *)
//
// HX: [sleep] may be implemented using SIGARM
//
fun sleep_int
  {i:nat} (t: int i): [j:nat | j <= i] int j = "mac#%"
fun sleep_uint
  {i:int} (t: uint i): [j:nat | j <= i] uint j = "mac#%"
//
symintr sleep
overload sleep with sleep_int
overload sleep with sleep_uint
//
(* ****** ****** *)
//
// HX: some systems require that the argument <= 1 million
//
fun usleep_int // succ/fail: 0/~1
  {i:nat | i <= 1000000} (n: int i): intLte(0) = "mac#%"
fun usleep_uint // succ/fail: 0/~1
  {i:int | i <= 1000000} (n: uint i): intLte(0) = "mac#%"
//
symintr usleep
overload usleep with usleep_int
overload usleep with usleep_uint
//
(* ****** ****** *)

/*
int rmdir(const char *pathname);
*/
fun rmdir (path: NSH(string)): int = "mac#%"
fun rmdir_exn (path: NSH(string)): void = "ext#%"

(* ****** ****** *)
/*
int link(const char *old, const char *new)
*/
fun link
(
  old: NSH(string)
, new: NSH(string)
) :<!ref> intLte(0) = "mac#%"
fun link_exn
  (old: NSH(string), new: NSH(string)):<!ref> void = "ext#%"
//
(* ****** ****** *)
/*
int symlink(const char *old, const char *new)
*/
fun symlink
(
  old: NSH(string)
, new: NSH(string)
) :<!ref> intLte(0) = "mac#%"
fun symlink_exn
  (old: NSH(string), new: NSH(string)):<!ref> void = "ext#%"
//
(* ****** ****** *)
/*
int unlink(const char *pathname);
*/
fun unlink (path: NSH(string)):<!ref> intLte(0) = "mac#%"
fun unlink_exn (path: NSH(string)):<!exnref> void = "ext#%"

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

fun readlink{n:int}
(
  path: NSH(string), buf: &(@[byte][n]) >> _, n: size_t (n)
) : ssizeLte(n) = "mac#%" // end of [readlink]

fun readlink_gc (path: NSH(string)): Strptr0 = "ext#%"

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

fun sync ((*void*)): void = "mac#%"
fun fsync (fd: !Fildes0): int = "mac#%"
fun fdatasync (fd: !Fildes0): int = "mac#%"

(* ****** ****** *)
//
fun truncate
  (path: NSH(string), ofs: off_t): int = "mac#%"
//
fun ftruncate (fd: !Fildes0, ofs: off_t): int = "mac#%"
//
(* ****** ****** *)

#include "./unistd_sysconf.sats"
#include "./unistd_pathconf.sats"

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

(* end of [unistd.sats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi
// Start Time: May, 2012
// Authoremail: gmhwxiATgmailDOTcom
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
#define
ATS_DYNLOADFLAG 0 // no dynloading at run-time
#define
ATS_EXTERN_PREFIX
"atslib_libats_libc_" // prefix for external names
//
(* ****** ****** *)

%{^
#include "share/H/pats_atslib.h"
%} // end of [%{^]

(* ****** ****** *)
//
staload "libats/libc/SATS/stdio.sats"
//
(* ****** ****** *)

%{$
//
extern
atstype_ptr
atslib_libats_libc_fopen_exn
(
  atstype_string path
, atstype_string mode
) {
  FILE *filp ;
  filp = fopen ((char*)path, (char*)mode) ;
  if (!filp) ATSLIBfailexit("fopen") ; // HX: failure
  return filp ;
} /* end of [atslib_libats_libc_fopen_exn] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_fclose_exn
  (atstype_ptr filp) {
  int err ;
  err = fclose ((FILE*)filp) ;
  if (0 > err) ATSLIBfailexit("fclose") ;
  return ;
} /* end of [atslib_libats_libc_fclose_exn] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_fflush_exn
(
  atstype_ptr filp
) {
  int err = fflush((FILE*)filp) ;
  if (0 > err) ATSLIBfailexit("fflush") ;
  return ;
} /* end of [atslib_libats_libc_fflush_exn] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_fputc_exn
(
  atstype_int c, atstype_ptr filp
) {
  int err ;
  err = fputc(c, (FILE*)filp) ;
  if (0 > err) {
    ATSLIBfailexit("fputc") ; // abnormal exit
  } // end of [if]
  return ;  
} /* end of [atslib_libats_libc_fputc_exn] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_fgets_exn
(
  atstype_ptr buf0
, atstype_int bsz0
, atstype_ptr filp
) {
  char *buf, *pres ;
  buf = (char*)buf0 ;
  pres = fgets(buf, (int)bsz0, (FILE*)filp) ;
  if (!pres)
  {
    if (feof((FILE*)filp))
    {
      buf[0] = '\000' ; // EOF is reached
    } else {
      ATSLIBfailexit("fgets") ; // abnormal exit
    } // end of [if]
  } // end of [if]
  return ;  
} /* end of [atslib_libats_libc_fgets_exn] */
//
%}

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

%{$
//
extern
atstype_ptr
atslib_libats_libc_fgets_gc
(
  atstype_int bsz0
, atstype_ptr filp0
)
{
  int bsz = bsz0 ;
  FILE *filp = (FILE*)filp0 ;
  int ofs = 0, ofs2 ;
  char *buf, *buf2, *pres ;
  buf = atspre_malloc_gc(bsz) ;
  while (1) {
    buf2 = buf+ofs ;
    pres = fgets(buf2, bsz-ofs, filp) ;
    if (!pres)
    {
      if (feof(filp))
      {
        *buf2 = '\000' ; return buf ;
      } else {
        atspre_mfree_gc(buf) ; return (char*)0 ;
      } // end of [if]
    }
    ofs2 = strlen(buf2) ;
    if (ofs2==0) return buf ;
    ofs += ofs2 ; // HX: ofs > 0
    if (buf[ofs-1]=='\n') return buf ;
    bsz *= 2 ; buf2 = buf ;
    buf = atspre_malloc_gc(bsz) ;
    memcpy(buf, buf2, ofs) ;
    atspre_mfree_gc(buf2) ;
  } // end of [while]
  return buf ; // HX: deadcode
} /* end of [atslib_libats_libc_fgets_gc] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_fputs_exn
(
  atstype_string str, atstype_ptr filp
) {
  int err ;
  err = fputs((char*)str, (FILE*)filp) ;
  if (0 > err) {
    ATSLIBfailexit("fputs") ; // abnormal exit
  } // end of [if]
  return ;  
} /* end of [atslib_libats_libc_fputs_exn] */
//
%}

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

%{$
//
extern
atsvoid_t0ype
atslib_libats_libc_puts_exn
(
  atstype_string str
) {
  int err ;
  err = puts((char*)str) ;
  if (0 > err) {
    ATSLIBfailexit("puts") ; // abnormal exit
  } // end of [if]
  return ;  
} /* end of [atslib_libats_libc_puts_exn] */
//
%}

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

%{$
//
extern
atstype_ptr
atslib_libats_libc_popen_exn
(
  atstype_string cmd
, atstype_string type
) {
  FILE *filp ;
  filp = popen((char*)cmd, (char*)type) ;
  if (!filp) {
    ATSLIBfailexit("popen") ; // abnormal exit
  } // end of [if]
  return filp ;
} /* end of [atslib_libats_libc_popen_exn] */
//
%}

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

%{$
//
extern
atstype_int
atslib_libats_libc_pclose_exn
(
  atstype_ptr filp
) {
  int res ;
  res = pclose((FILE*)filp) ;
  if (0 > res) {
    ATSLIBfailexit("pclose") ; // abnormal exit
  } // end of [if]
  return res ;
} /* end of [atslib_libats_libc_pclose_exn] */
//
%}

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

%{$
//
extern
atstype_ptr
atslib_libats_libc_tmpfile_exn
(
// argumentless
) {
  FILE *filp = tmpfile() ;
  if (!filp) ATSLIBfailexit("tmpfile") ;
  return (filp) ;
} /* end of [atslib_libats_libc_tmpfile_exn] */
//
%}

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

(* end of [stdio.dats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi
// Start Time: May, 2012
// Authoremail: gmhwxiATgmailDOTcom
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
#define
ATS_DYNLOADFLAG 0 // no dynloading at run-time
#define
ATS_EXTERN_PREFIX
"atslib_libats_libc_" // prefix for external names
//
(* ****** ****** *)

%{^
//
#include "share/H/pats_atslib.h"
//
%} // end of [%{^]

(* ****** ****** *)
//
staload "libats/libc/SATS/stdlib.sats"
//
(* ****** ****** *)

implement
{}(*tmp*)
getenv_gc
  (name) = str2 where
{
//
val
fpfstr = getenv(name)
//
val str2 = strptr0_copy(fpfstr.1)
//
prval ((*void*)) = fpfstr.0(fpfstr.1)
//
} (* end of [getenv_gc] *)

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

%{$
//
extern
atstype_ptr
atslib_libats_libc_malloc_libc_exn
  (atstype_size bsz)
{
  void *p0 ;
  p0 = atslib_libats_libc_malloc_libc(bsz) ;
  if (!p0) {
    fprintf(stderr, "exit(ATSLIB): [malloc] failed\n") ; exit(1) ;
  } // end of [if]
  return p0 ;
} /* end of [atslib_libats_libc_malloc_libc_exn] */
//
%}

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

(* end of [stdlib.dats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi (gmhwxi AT gmail DOT com)
// Start Time: March, 2013
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
#define
ATS_DYNLOADFLAG 0 // no dynloading at run-time
#define
ATS_EXTERN_PREFIX
"atslib_libats_libc_" // prefix for external names
//
(* ****** ****** *)
//
staload
"libats/libc/SATS/string.sats"
//
(* ****** ****** *)

%{$
extern
atstype_ptr
atslib_libats_libc_strerror_r_gc
(
  atstype_int errnum
) {
  char *p_err ;
  int bsz ;
  int myerr, myeno ;
//
// HX: [64] is chosen nearly randomly
//
  bsz = 64 ;
  p_err = (char*)0 ;
//
  while (1)
  {
    p_err = atspre_malloc_gc(bsz) ;
    myerr = atslib_libats_libc_strerror_r(errnum, p_err, bsz) ; myeno = errno ;
    if (!myerr) return p_err ;
    if (myeno != ERANGE) break ;
    atspre_mfree_gc(p_err) ; bsz = 2 * bsz ;
  }
//
  return p_err ;
//
} /* end of [atslib_libats_libc_strerror_r_gc] */
%}

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

(* end of [string.dats] *)

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

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-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: Hongwei Xi (gmhwxi AT gmail DOT com)
// Start Time: March, 2013
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.libc"
#define
ATS_DYNLOADFLAG 0 // no need for dynloading at run-time
#define
ATS_EXTERN_PREFIX "atslib_libats_libc_" // prefix for external names
//
(* ****** ****** *)

%{^
#include"share/H/pats_atslib.h"
%} // end of [%{^]

(* ****** ****** *)
//
staload "libats/libc/SATS/errno.sats"
staload "libats/libc/SATS/fcntl.sats"
staload "libats/libc/SATS/unistd.sats"
//
(* ****** ****** *)

%{$
extern
atsvoid_t0ype
atslib_libats_libc_close_exn
(
  atstype_int fd
) {
  int err ;
  err = atslib_libats_libc_close(fd) ;
  if (0 > err) ATSLIBfailexit("close") ;
  return ;
} /* end of [atslib_libats_libc_close_exn] */
%}

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

%{$
extern
atstype_int
atslib_libats_libc_dup2_fildes
(
  atstype_int fd, atstype_int fd2
) {
  int flags ;
//
  flags = fcntl(fd, F_GETFD) ;
//
  if (flags >= 0) {
    errno = EINVAL ; return -1 ; // [fd2] in use
  } /* end of [if] */
//
  return atslib_libats_libc_dup2(fd, fd2) ;
//
} /* end of [atslib_libats_libc_dup2_fildes] */
%}

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

%{$
extern
atstype_strptr
atslib_libats_libc_getcwd_gc (
) {
  char *p_cwd ;
  int bsz ;
  int myeno ;
  char *p2_cwd ;
//
// HX: [64] is chosen nearly randomly
//
  bsz = 64 ;
  p_cwd = (char*)0 ;
//
  while (1)
  {
    p_cwd = atspre_malloc_gc(bsz) ;
    p2_cwd = atslib_libats_libc_getcwd(p_cwd, bsz) ; myeno = errno ;
    if (p2_cwd != 0) return p_cwd ; else atspre_mfree_gc(p_cwd) ;
    if (myeno != ERANGE) break ;
    bsz = 2 * bsz ;
  }
//
  return (char*)0 ;
//
} /* end of [atslib_libats_libc_getcwd_gc] */
%}

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

%{$
extern
atstype_strptr
atslib_libats_libc_getlogin_r_gc (
) {
  char *p_uid ;
  int bsz ;
  int err, myeno ;
//
// HX: [16] is chosen nearly randomly
//
  bsz = 16 ;
  p_uid = (char*)0 ;
//
  while (1)
  {
    p_uid = atspre_malloc_gc(bsz) ;
    err = atslib_libats_libc_getlogin_r(p_uid, bsz) ; myeno = errno ;
    if (err==0) return p_uid ; else atspre_mfree_gc(p_uid) ;
    if (myeno != ERANGE) break ;
    bsz = 2 * bsz ;
  }
//
  return (char*)0 ;
//
} /* end of [atslib_libats_libc_getlogin_r_gc] */
%}

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

%{$
extern
atsvoid_t0ype
atslib_libats_libc_rmdir_exn
(
  atstype_string path
) {
  int err ;
  err = atslib_libats_libc_rmdir(path) ;
  if (0 > err) ATSLIBfailexit("rmdir") ;
  return ;
} /* end of [atslib_libats_libc_rmdir_exn] */
%}

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

%{$
extern
atsvoid_t0ype
atslib_libats_libc_link_exn
(
  atstype_string old, atstype_string new
) {
  int err ;
  err = atslib_libats_libc_link(old, new) ;
  if (0 > err) ATSLIBfailexit("link") ;
  return ;
} /* end of [atslib_libats_libc_link_exn] */
%}

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

%{$
extern
atsvoid_t0ype
atslib_libats_libc_unlink_exn
(
  atstype_string path
) {
  int err ;
  err = atslib_libats_libc_unlink(path) ;
  if (0 > err) ATSLIBfailexit("unlink") ;
  return ;
} /* end of [atslib_libats_libc_unlink_exn] */
%}

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

%{$
extern
atsvoid_t0ype
atslib_libats_libc_symlink_exn
(
  atstype_string old, atstype_string new
) {
  int err ;
  err = atslib_libats_libc_symlink(old, new) ;
  if (0 > err) ATSLIBfailexit("symlink") ;
  return ;
} /* end of [atslib_libats_libc_symlink_exn] */
%}

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

%{$
extern
atstype_strptr
atslib_libats_libc_readlink_gc
(
  atstype_string path
) {
  char *bfp ;
//
// HX: [64] is chosen nearly randomly
//
  int bsz = 64 ;
  ssize_t bsz2 ;
  bfp = (char*)0 ;
//
  while (1)
  {
    bfp = atspre_malloc_gc(bsz) ;
    bsz2 = atslib_libats_libc_readlink(path, bfp, bsz) ;
/*
    fprintf(stderr, "atslib_libats_libc_readlink_gc: bsz2 = %li\n", bsz2) ;
*/
    if (bsz2 < 0) {
      atspre_mfree_gc(bfp) ; break ;
    }
    if (bsz2 < bsz) {
      bfp[bsz2] = '\000' ; return bfp ;
    }
    atspre_mfree_gc(bfp) ; bsz *= 2 ;
  }
//
  return (char*)0 ; // HX: deadcode
//
} /* end of [atslib_libats_libc_readlink_gc] */
%}

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

(* end of [unistd.dats] *)