ats2-lang 0.2.6-2 / usr / lib / ats2-postiats-0.2.6 / libc / sys / SATS / types.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: March, 2013
//
(* ****** ****** *)

%{#
#include "libc/sys/CATS/types.cats"
%} // end of [%{#]

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

#define ATS_PACKNAME "ATSLIB.libc"
#define ATS_EXTERN_PREFIX "atslib_" // prefix for external names

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

#define NSH (x) x // for commenting: no sharing
#define SHR (x) x // for commenting: it is shared

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

abst@ype
time_t0ype = $extype"atslib_time_type"
typedef time_t = time_t0ype // = its C-counterpart

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

fun time2lint (t: time_t):<> lint = "mac#%"
fun time2double (t: time_t):<> double = "mac#%"

(* ****** ****** *)
//
fun lt_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
fun lte_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
overload < with lt_time_time
overload <= with lte_time_time
//
fun gt_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
fun gte_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
overload > with gt_time_time
overload >= with gte_time_time
//
fun eq_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
fun neq_time_time (t1: time_t, t2: time_t):<> bool = "mac#%"
overload = with eq_time_time
overload <> with neq_time_time
overload != with neq_time_time
//
(* ****** ****** *)

abst@ype
clock_t0ype = $extype"atslib_clock_type"
typedef clock_t = clock_t0ype // = its C-counterpart

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

fun clock2lint (t: clock_t):<> lint = "mac#%"
fun clock2double (t: clock_t):<> double = "mac#%"

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

abst@ype
clockid_t0ype = $extype"atslib_clockid_type"
typedef clockid_t = clockid_t0ype // = its C-counterpart

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

abst@ype
mode_t0ype = $extype"atslib_mode_type"
typedef mode_t = mode_t0ype // = its C-counterpart

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

fun mode2int (m: mode_t):<> int = "mac#%"
fun mode2uint (m: mode_t):<> uint = "mac#%"

fun eq_mode_mode (m1: mode_t, m2: mode_t):<> bool
fun neq_mode_mode (m1: mode_t, m2: mode_t):<> bool
overload = with eq_mode_mode
overload != with neq_mode_mode
overload <> with neq_mode_mode

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

fun lor_mode_mode
  (m1: mode_t, m2: mode_t):<> mode_t = "mac#%"
overload lor with lor_mode_mode

fun land_mode_mode
  (m1: mode_t, m2: mode_t):<> mode_t = "mac#%"
overload land with land_mode_mode

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

abst@ype
dev_t0ype = $extype"atslib_dev_type"
typedef dev_t = dev_t0ype // = its C-counterpart

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

abst@ype
ino_t0ype = $extype"atslib_ino_type"
typedef ino_t = ino_t0ype // = its C-counterpart

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

abst@ype
nlink_t0ype = $extype"atslib_nlink_type"
typedef nlink_t = nlink_t0ype // = its C-counterpart

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

abst@ype
pid_t0ype = $extype"atslib_pid_type"
typedef pid_t = pid_t0ype // = its C-counterpart
castfn pid2int (x: pid_t):<> int
castfn pid2lint (x: pid_t):<> lint

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

abst@ype
uid_t0ype = $extype"atslib_uid_type"
typedef uid_t = uid_t0ype // = its C-counterpart
abst@ype
gid_t0ype = $extype"atslib_gid_type"
typedef gid_t = gid_t0ype // = its C-counterpart

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

abst@ype
off_t0ype = $extype"atslib_off_type"
typedef off_t = off_t0ype // = its C-counterpart

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

abst@ype
blkcnt_t0ype = $extype"atslib_blkcnt_type"
typedef blkcnt_t = blkcnt_t0ype // = its C-counterpart
abst@ype
blkcnt_t0ype = $extype"atslib_blkcnt_type"
typedef blkcnt_t = blkcnt_t0ype // = its C-counterpart

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

abst@ype
blksize_t0ype = $extype"atslib_blksize_type"
typedef blksize_t = blksize_t0ype // = its C-counterpart
abst@ype
blksize_t0ype = $extype"atslib_blksize_type"
typedef blksize_t = blksize_t0ype // = its C-counterpart

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

fun lint2off (x: lint):<> off_t = "mac#%"
fun off2lint (x: off_t):<> lint = "mac#%"
fun size2off (x: size_t):<> off_t = "mac#%"
fun off2size (x: off_t):<> size_t = "mac#%"

(* ****** ****** *)
//
absview fildes_view (fd: int)
viewdef fildes_v (i:int) = fildes_view (i)
//
absvt@ype
fildes_vtype (fd: int) = int
//
vtypedef
fildes (fd: int) = fildes_vtype (fd)
//
vtypedef Fildes = [fd:int] fildes (fd)
vtypedef Fildes0 = [fd:int | fd >= 0] fildes (fd)
//
(* ****** ****** *)

castfn
fildes_decode
  {fd:nat} (fd: fildes (fd)):<> (fildes_v (fd) | int fd)
// end of [fildes_decode]

castfn fildes_encode
  {fd:nat} (pf: fildes_v (fd) | fd: int fd):<> fildes (fd)
// end of [fildes_encode]

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

abst@ype
useconds_t = // microseconds
$extype"atslib_useconds_type"
castfn usec2lint (x: useconds_t):<> lint

abst@ype
suseconds_t = // microseconds
$extype"atslib_suseconds_type"
castfn susec2lint (x: suseconds_t):<> lint

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

abst@ype
pthread_t =
$extype"atslib_pthread_type"
castfn pthread2lint (x: pthread_t):<> lint

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

(* end of [types.sats] *)