(***********************************************************************) (* *) (* 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)) : a // fun {a:vt0p} gcopy_ref (x : &INV(a)) : a // (* ****** ****** *) // fun {a:vt0p} gfree_val (x : INV(a)) : void // (* fun {a:vt0p} gfree_ref (x: &INV(a) >> a?): void *) // (* ****** ****** *) fun {a:vt0p} ginit_ref (x : &a? >> a) : void (* ****** ****** *) fun {a:vt0p} gclear_ref (x : &a >> a?) : 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) : Strptr1 fun {a:vt0p} tostrptr_ref (x : &INV(a)) : 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) // (* ****** ****** *) // fun {a:t0p} print_stamped_t (stamped_t(a)) : void fun {a:t0p} prerr_stamped_t (stamped_t(a)) : void fun {a:t0p} fprint_stamped_t (out : FILEref, x : stamped_t(a)) : void (* // // HX-2017-12-09: // This one does not seem to be so useful // fun {a:vt0p} fprint_stamped_vt(out: FILEref, x: &stamped_vt(a)): void *) // overload print with print_stamped_t overload prerr with prerr_stamped_t overload fprint with fprint_stamped_t // (* ****** ****** *) #if VERBOSE_PRELUDE #then #print "Loading [basics_gen.sats] finishes!\n" #endif // end of [VERBOSE_PRELUDE] (* ****** ****** *) (* end of [basics_gen.sats] *)