(***********************************************************************) (* *) (* 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/DATS/CODEGEN/pointer.atxt ** Time of generation: Sun Nov 20 21:18:22 2016 *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: hwxi AT cs DOT bu DOT edu *) (* Start time: March, 2012 *) (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) primplmnt lemma_ptr_param {l} (p) = lemma_addr_param {l} () // end of [lemma_ptr_param] (* ****** ****** *) primplmnt ptr_get_index{l}(p) = eqaddr_make{l, l}() (* ****** ****** *) implement {a}(*tmp*) ptr0_succ(p) = add_ptr_bsz(p, sizeof) implement {a}(*tmp*) ptr0_pred(p) = sub_ptr_bsz(p, sizeof) (* ****** ****** *) // implement {a}{tk} ptr0_add_gint(p, i) = add_ptr_bsz(p, g0int2uint(i) * sizeof) implement {a}{tk} ptr0_sub_gint(p, i) = sub_ptr_bsz(p, g0int2uint(i) * sizeof) // implement {a}{tk} ptr0_add_guint(p, i) = add_ptr_bsz(p, g0uint2uint(i) * sizeof) implement {a}{tk} ptr0_sub_guint(p, i) = sub_ptr_bsz(p, g0uint2uint(i) * sizeof) // (* ****** ****** *) // implement {a}(*tmp*) ptr1_succ{l}(p) = $UN.cast{ptr(l+sizeof(a))}(add_ptr_bsz(p, sizeof)) implement {a}(*tmp*) ptr1_pred{l}(p) = $UN.cast{ptr(l-sizeof(a))}(sub_ptr_bsz(p, sizeof)) // (* ****** ****** *) // implement {a}{tk} ptr1_add_gint{l}{i}(p, i) = $UN.cast{ptr(l+i*sizeof(a))}(ptr0_add_gint(p, i)) implement {a}{tk} ptr1_sub_gint{l}{i}(p, i) = $UN.cast{ptr(l-i*sizeof(a))}(ptr0_sub_gint(p, i)) // implement {a}{tk} ptr1_add_guint{l}{i}(p, i) = $UN.cast{ptr(l+i*sizeof(a))}(ptr0_add_guint(p, i)) implement {a}{tk} ptr1_sub_guint{l}{i}(p, i) = $UN.cast{ptr(l-i*sizeof(a))}(ptr0_sub_guint(p, i)) // (* ****** ****** *) implement {a}(*tmp*) ptr_get(pf | p) = !p implement {a}(*tmp*) ptr_set(pf | p, x) = (!p := x) implement {a}(*tmp*) ptr_exch(pf | p, xr) = { val x0 = xr; val () = xr := !p; val () = !p := x0 } // end of [ptr_exch] (* ****** ****** *) implement {a}(*tmp*) ptr_nullize (pf | x) = ( ptr_nullize_tsz{a}(pf | x, sizeof) ) (* ptr_nullize *) (* ****** ****** *) implement {a}(*tmp*) ptr_alloc() = ptr_alloc_tsz{a}(sizeof) (* ****** ****** *) implement {a}(*tmp*) aptr_make_elt(x) = let // val (pf, fpf | p) = ptr_alloc() // in !p := x; $UN.castvwtp0{aPtr1(a)}((pf, fpf, p)) end // end of [aptr_make_elt] (* ****** ****** *) // implement {a}(*tmp*) cptr_succ{l}(cp) = $UN.cast(add_ptr_bsz(cptr2ptr(cp), sizeof)) implement {a}(*tmp*) cptr_pred{l}(cp) = $UN.cast(sub_ptr_bsz(cptr2ptr(cp), sizeof)) // (* ****** ****** *) // implement {a}(*tmp*) aptr_getfree_elt {l}(ap) = x0 where { // val p0 = aptr2ptr(ap) val x0 = $UN.ptr1_get(p0) // prval pfat_ = $UN.castview0{(a?)@l}(0) prval pfgc_ = $UN.castview0{mfree_gc_v(l)}(0) val () = ptr_free{a?}{l}(pfgc_, pfat_ | p0) // prval () = $UN.cast2void(ap) // } (* end of [aptr_getfree_elt] *) // (* ****** ****** *) // implement {a}(*tmp*) aptr_get_elt(ap) = $UN.ptr1_get(aptr2ptr(ap)) implement {a}(*tmp*) aptr_set_elt(ap, x0) = $UN.ptr1_set(aptr2ptr(ap), x0) // implement {a}(*tmp*) aptr_exch_elt(ap, x0) = $UN.ptr1_exch(aptr2ptr(ap), x0) // (* ****** ****** *) // // implement {a}(*tmp*) aptr_vtget0_elt {l}(ap) = x0 where { // val x0 = $UN.ptr1_get(aptr2ptr(ap)) // prval () = $UN.castvwtp2void(ap) // } (* end of [aptr_vtget0_elt] *) // implement {a}(*tmp*) aptr_vtget1_elt {l}(ap) = let // val x0 = $UN.ptr1_get(aptr2ptr(ap)) // vtypedef res_vt = (minus_v(aptr(a,l),a) | a) // in $UN.castvwtp0{res_vt}(x0) end // end of [aptr_vtget1_elt] // (* ****** ****** *) implement fprint_val (out, p) = fprint_ptr (out, p) (* ****** ****** *) (* end of [pointer.dats] *)