(***********************************************************************) (* *) (* 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/unsafe.atxt ** Time of generation: Thu Jan 11 11:00:05 2018 *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: hwxi AT cs DOT bu DOT edu *) (* Start time: April, 2012 *) (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.prelude.unsafe" (* ****** ****** *) sortdef t0p = t@ype and vt0p = viewt@ype (* ****** ****** *) // praxi prop_assert{b:bool}((*void*)): [b] void // praxi proof_assert{proof:prop}((*void*)): proof // praxi eqint_assert{i1,i2:int}((*void*)): EQINT(i1,i2) praxi eqaddr_assert{l1,l2:addr}((*void*)): EQADDR(l1,l2) praxi eqbool_assert{b1,b2:bool}((*void*)): EQBOOL(b1,b2) // (* ****** ****** *) // castfn cast{to:t0p}{from:t0p} (x: INV(from)):<> to // (* ****** ****** *) // castfn castvwtp0 {to:vt0p}{from:vt0p} (x: INV(from)):<> to // // HX: // [castvwtp1] is mostly used in a situation // where a linear value is passed as a read-only value; // for instance, casting [strptr] to [string] is often // done for treating a linear string as a nonlinear one // temporarily. // castfn castvwtp1 {to:vt0p}{from:vt0p} (x: !INV(from)>>from):<> to // (* ****** ****** *) // castfn cast2ptr {a:type} (x: INV(a)):<> ptr castfn cast2Ptr0 {a:type} (x: INV(a)):<> Ptr0 castfn cast2Ptr1 {a:type} (x: INV(a)):<> Ptr1 // castfn cast2int {a:t0p} (x: INV(a)):<> int castfn cast2uint {a:t0p} (x: INV(a)):<> uint // castfn cast2lint {a:t0p} (x: INV(a)):<> lint castfn cast2ulint {a:t0p} (x: INV(a)):<> ulint // castfn cast2llint {a:t0p} (x: INV(a)):<> llint castfn cast2ullint {a:t0p} (x: INV(a)):<> ullint // castfn cast2size {a:t0p} (x: INV(a)):<> size_t castfn cast2ssize {a:t0p} (x: INV(a)):<> ssize_t // castfn cast2sint {a:t0p} (x: INV(a)):<> sint castfn cast2usint {a:t0p} (x: INV(a)):<> usint // castfn cast2intptr {a:t0p} (x: INV(a)):<> intptr castfn cast2uintptr {a:t0p} (x: INV(a)):<> uintptr // (* ****** ****** *) praxi cast2void{a:vt0p}(x: INV(a)): void (* ****** ****** *) // praxi castview0 {to:view}{from:view} (pf: from): to praxi castview1 {to:view}{from:view} (pf: !INV(from)): to // (* ****** ****** *) // praxi castview2void {to:view}{from:view}(x: !INV(from) >> to): void praxi castvwtp2void {to:vt0p}{from:vt0p}(x: !INV(from) >> to): void // praxi castview2void_at {to:vt0p}{from:vt0p}{l:addr}(x: !INV(from@l) >> to@l): void // (* ****** ****** *) fun{} int2ptr (i: int): ptr and ptr2int (p: ptr): int (* ****** ****** *) // // HX: these are popular ones: // castfn list_vt2t {a:t0p}{n:int} (xs: !list_vt(INV(a), n)):<> list(a, n) // end of [list_vt2t] castfn arrayptr2ref {a:vt0p}{n:int} (x: !arrayptr (INV(a), n)):<> arrayref(a, n) // end of [arrayptr2ref] castfn strptr2string{l:agz}(x: !strptr(l)):<> String0 castfn strptr2stropt{l:addr}(x: !strptr(l)):<> Stropt0 castfn strnptr2string{l:addr}{n:nat}(x: !strnptr(l, n)):<> string(n) (* ****** ****** *) // // HX: only if you know what you are doing ... // symintr ptr_vtake // castfn ptr0_vtake {a:vt0p} ( p0: ptr ) :<> [l:addr] (a@l, a@l - void | ptr(l)) castfn ptr1_vtake {a:vt0p}{l:addr} (p0: ptr(l)):<> (a@l, a@l - void | ptr(l)) // overload ptr_vtake with ptr0_vtake of 0 overload ptr_vtake with ptr1_vtake of 10 // (* ****** ****** *) castfn ref_vtake {a:vt0p} {l:addr} ( ref: ref(a) ) :<> [ l:addr ] (a@l, a@l - void | ptr(l)) // end of [ref_vtake] (* ****** ****** *) praxi vtakeout_void{v:view}(pf: !v): vtakeout0(v) castfn vttakeout_void{a:vt0p}(x0: !a):<> vttakeout0(a) (* ****** ****** *) // // HX: only if you know what you are doing ... // fun{a:vt0p} ptr0_get(p: ptr):<> (a) fun{a:vt0p} ptr1_get(p: Ptr1):<> (a) // fun{a:vt0p} ptr0_set(p: ptr, x: INV(a)): void fun{a:vt0p} ptr1_set(p: Ptr1, x: INV(a)): void // fun{a:vt0p} ptr0_exch(p: ptr, x: &INV(a) >> a): void fun{a:vt0p} ptr1_exch(p: Ptr1, x: &INV(a) >> a): void // fun{a:vt0p} ptr0_intch(p1: ptr, p2: ptr): void fun{a:vt0p} ptr1_intch(p1: Ptr1, p2: Ptr1): void // (* ****** ****** *) // fun{a:vt0p} ptr0_getinc(p: &ptr >> _): (a) fun{a:vt0p} ptr1_getinc{l:addr}(p: &ptr(l) >> ptr(l+sizeof(a))): (a) // fun{a:vt0p} ptr0_setinc(p: &ptr >> _, x: a): void fun{a:vt0p} ptr1_setinc{l:addr}(p: &ptr(l) >> ptr(l+sizeof(a)), x: a): void // (* ****** ****** *) // fun{a:vt0p} ptr0_get_at_int(p: ptr, i: int):<> a fun{a:vt0p} ptr0_set_at_int(p: ptr, i: int, x: a): void // fun{a:vt0p} ptr0_get_at_size(p: ptr, i: size_t):<> a fun{a:vt0p} ptr0_set_at_size(p: ptr, i: size_t, x: a): void // symintr ptr0_get_at symintr ptr0_set_at // overload ptr0_get_at with ptr0_get_at_int overload ptr0_set_at with ptr0_set_at_int overload ptr0_get_at with ptr0_get_at_size overload ptr0_set_at with ptr0_set_at_size // (* ****** ****** *) // // HX-2012-06: // generic ops on numbers: +=, -=, *=, /=, %= // fun{a:t0p} ptr0_addby(p: ptr, x: a): void // !p += x fun{a:t0p} ptr1_addby(p: Ptr1, x: a): void // !p += x // fun{a:t0p} ptr0_subby(p: ptr, x: a): void // !p -= x fun{a:t0p} ptr1_subby(p: Ptr1, x: a): void // !p -= x // fun{a:t0p} ptr0_mulby(p: ptr, x: a): void // !p *= x fun{a:t0p} ptr1_mulby(p: Ptr1, x: a): void // !p *= x // fun{a:t0p} ptr0_divby(p: ptr, x: a): void // !p /= x fun{a:t0p} ptr1_divby(p: Ptr1, x: a): void // !p /= x // fun{a:t0p} ptr0_modby(p: ptr, x: a): void // !p %= x fun{a:t0p} ptr1_modby(p: Ptr1, x: a): void // !p %= x // (* ****** ****** *) fun {a:vt0p} ptr1_list_next(p: Ptr1): Ptr0 // HX: &(p->next) (* ****** ****** *) // // HX: only if you know what you are doing ... // castfn ptr2cptr{a:vt0p}{l:addr}(p: ptr(l)):<> cptr(a, l) // (* ****** ****** *) // castfn cptr_vtake {a:vt0p}{l:agz} ( cp: cptr(INV(a), l) ) :<> (a@l, a@l - void | ptr l) // end of [cptr_vtake] // fun {a:vt0p} cptr_get(cp: cPtr1(INV(a))):<> a fun {a:vt0p} cptr_set(cp: cPtr1(INV(a)), x: a): void fun {a:vt0p} cptr_exch(cp: cPtr1(INV(a)), xr: &a >> a): void // (* overload .get with cptr_get overload .set with cptr_set overload .exch with cptr_exch *) // (* ****** ****** *) (* end of [unsafe.sats] *)