(***********************************************************************)
(*                                                                     *)
(*                         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: September, 2011
//
(* ****** ****** *)
#include "prelude/params.hats"

(* ****** ****** *)
//
fun patsopt_version() : string =
  "ext#%"

//
(* ****** ****** *)

#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] starts!\n"
#endif // end of [VERBOSE_PRELUDE]
(* ****** ****** *)
//
sortdef t0p = t@ype and vt0p = vt@ype

//
(* ****** ****** *)
datatype TYPE(a: vt@ype) =
  | TYPE(a) of ()

(* ****** ****** *)
//
// HX-2012: In $ATSHOME/ccomp/runtime:
// atsbool_true/atsbool_false are mapped to 1/0
// this mapping is fixed and should never be changed!
//
#define true true_bool // shorthand
#define false false_bool // shorthand

//
val true_bool: bool(true) = "mac#atsbool_true"

// = 1
val false_bool: bool(false) = "mac#atsbool_false"

// = 0
//
(* ****** ****** *)
//
// HX: [false] implies all
//
prfun false_elim { X : prop | false } () : X

//
(* ****** ****** *)
//
typedef compopr_type(a: t@ype) = (a, a) -<fun0> bool
typedef compare_type(a: t@ype) = (a, a) -<fun0> int

(*-/0/+*)
//
(* ****** ****** *)
//
praxi lemma_subcls_reflexive {c:cls} () : [c <= c] void

//
praxi lemma_subcls_transitive { c1, c2, c3 : cls | c1 <= c2; c2 <= c3 }
() : [c1 <= c3] void

//
(* ****** ****** *)
//
praxi praxi_int {i:int} () : int(i)

//
dataprop MUL_prop(int, int, int) =
  | {n:int} MULbas((0, n, 0))
  | {m:nat}{n:int}{p:int} MULind((m + 1, n, p + n)) of MUL_prop((m, n, p))
  | {m:pos}{n:int}{p:int} MULneg((~(m), n, ~(p))) of MUL_prop((m, n, p))

propdef MUL (m : int, n : int, mn : int) = MUL_prop(m, n, mn)

//
(* ****** ****** *)
//
// HX-2010-12-30: 
//
absprop DIVMOD (x : int, y : int, q : int, r : int)

// end of [DIVMOD]
//
propdef DIV (x : int, y : int, q : int) = [r:int] DIVMOD(x, y, q, r)

propdef MOD (x : int, y : int, r : int) = [q:int] DIVMOD(x, y, q, r)

//
(* ****** ****** *)
dataprop EQINT(int, int) =
  | {x:int} EQINT(x, x)

prfun eqint_make { x, y : int | x == y } () : EQINT(x, y)

//
prfun eqint_make_gint {tk:tk}{x:int} (x : g1int(tk, x)) :
  [y:int] EQINT(x, y)

prfun eqint_make_guint {tk:tk}{x:int} (x : g1uint(tk, x)) :
  [y:int] EQINT(x, y)

//
(* ****** ****** *)
praxi praxi_ptr {l:addr} () : ptr(l)

praxi praxi_bool {b:bool} () : bool(b)

(* ****** ****** *)
dataprop EQADDR(addr, addr) =
  | {x:addr} EQADDR(x, x)

prfun eqaddr_make { x, y : addr | x == y } () : EQADDR(x, y)

//
prfun eqaddr_make_ptr {x:addr} (x : ptr(x)) : [y:addr] EQADDR(x, y)

//
(* ****** ****** *)
dataprop EQBOOL(bool, bool) =
  | {x:bool} EQBOOL(x, x)

prfun eqbool_make { x, y : bool | x == y } () : EQBOOL(x, y)

//
prfun eqbool_make_bool {x:bool} (x : bool(x)) : [y:bool] EQBOOL(x, y)

//
(* ****** ****** *)
//
dataprop EQTYPE(vt@ype, vt@ype) =
  | {a:vt@ype} EQTYPE((a, a))

(* ****** ****** *)
prfun prop_verify { b : bool | b } () :<prf> void

prfun prop_verify_and_add { b : bool | b } () :<prf> [b] void

(* ****** ****** *)
prfun pridentity_v {v:view} (x : !INV(v)) : void

prfun pridentity_vt {vt:vt@ype} (x : !INV(vt)) : void

(* ****** ****** *)
castfn viewptr_match {a:vt0ype}{ l1, l2 : addr | l1 == l2 }
(pf : INV(a) @ l1 | p : ptr(l2)) :<>
  [ l : addr | l == l1 ] (a @ l | ptr(l))

// end of [viewptr_match]
(* ****** ****** *)
//
val {a:vt0ype} sizeof : size_t(sizeof(a))

//
praxi lemma_sizeof {a:vt0ype} () : [sizeof(a) >= 0] void

//
(* ****** ****** *)
praxi topize {a:t0ype} (x : !INV(a) >> a?) : void

(* ****** ****** *)
castfn dataget {a:vt0ype} (x : !INV(a) >> a) : a?!

(* ****** ****** *)
//
// HX: returning the pf to GC
//
praxi mfree_gc_v_elim {l:addr} (pf : mfree_gc_v(l)) :<prf> void

// end of [mfree_gc_v_elim]
(* ****** ****** *)
praxi mfree_gcngc_v_nullify {l:addr} ( pf1 : mfree_gc_v(l)
                                     , pf1 : mfree_ngc_v(l)
                                     ) : void

// end of [mfree_gcngc_nullify_v]
(* ****** ****** *)
//
fun cloptr_free {a:t0p}(pclo : cloptr(a)) :<!wrt> void =
  "mac#%"

//
overload free with cloptr_free of 0

//
(* ****** ****** *)
//
fun {a:t0p} lazy_force (lazyval : lazy(INV(a))) :<!laz> (a)

fun {a:vt0p} lazy_vt_force (lazyval : lazy_vt(INV(a))) :<!all> (a)

(*
//
// HX-2016-08:
// this is assumed internally!
//
overload ! with lazy_force of 0
overload ! with lazy_vt_force of 0
*)
//
(* ****** ****** *)
//
// HX-2013:
// macro implemented in [pats_ccomp_instrset]
//
fun lazy_vt_free {a:vt0p}(lazyval : lazy_vt(a)) :<!wrt> void =
  "mac#%"

//
overload ~ with lazy_vt_free of 0

overload free with lazy_vt_free of 0

//
(* ****** ****** *)
//
// HX-2014:
// macro implemented in [pats_ccomp_instrset]
//
fun lazy2cloref {a:t0p}(lazy(a)) : () -<cloref1> (a) =
  "mac#%"

//
(* ****** ****** *)
(*
// HX-2012-05-23: this seems TOO complicated!
(*
** HX-2012-03: handling read-only views and vtypes
*)
castfn
read_getval // copy out a non-linear value
  {a:t@ype}{s:int}{n:int} (x: !READ (a, s, n)):<> a
// end of [read_getval]

praxi
read_takeout{v:view}
  (pf: !v >> READOUT (v, s)): #[s:int] READ (v, s, 0)
// end of [read_takeout]
praxi
read_addback // HX: there is no need to check
  {v1:view}{v2:view}{s:int} // if v1 and v2 match
  (pf1: !READOUT (v1, s) >> v1, pf2: READ (v2, s, 0)): void
// end of [read0_addback]

praxi
read_split
  {v:view}{s:int}{n:int}
  (pf: !READ (v, s, n) >> READ (v, s, n+1)): READ (v, s, 0)
// end of [read_split]
praxi
read_unsplit // HX: there is no need to check
  {v1:view}{v2:view}{s:int}{n1,n2:int} // if v1 and v2 match
  (pf1: READ (v1, s, n1), pf2: READ (v2, s, n2)): READ (v1, s, n1+n2-1)
// end of [read_unsplit]
*)
(* ****** ****** *)
//
castfn stamp_t {a:t@ype} (x : INV(a)) :<> stamped_t(a)

// end of [stamp_t]
castfn stamp_vt {a:vt@ype} (x : INV(a)) :<> stamped_vt(a)

// end of [stamp_vt]
//
(* ****** ****** *)
//
castfn unstamp_t {a:t@ype}{x:int} (x : stamped_t(INV(a), x)) :<> a

// end of [unstamp_t]
castfn unstamp_vt {a:vt@ype}{x:int} (x : stamped_vt(INV(a), x)) :<> a

// end of [unstamp_vt]
//
(* ****** ****** *)
//
castfn stamped_t2vt {a:t@ype}{x:int} (x : stamped_t(INV(a), x)) :<>
  stamped_vt(a, x)

// end of [stamped_t2vt]
//
castfn stamped_vt2t {a:t@ype}{x:int} (x : stamped_vt(INV(a), x)) :<>
  stamped_t(a, x)

// end of [stamped_vt2t]
//
fun {a:t@ype} stamped_vt2t_ref {x:int} (x : &stamped_vt(INV(a), x)) :<>
  stamped_t(a, x)

//
(* ****** ****** *)
//
praxi vcopyenv_v_decode {v:view} (x : vcopyenv_v(v)) : vtakeout0(v)

castfn vcopyenv_vt_decode {vt:vt0p} (x : vcopyenv_vt(vt)) :
  vttakeout0(vt)

//
overload decode with vcopyenv_v_decode

overload decode with vcopyenv_vt_decode

//
(* ****** ****** *)
//
// HX: the_null_ptr = (void*)0
//
val the_null_ptr: ptr(null) = "mac#the_atsptr_null"

//
(* ****** ****** *)
//
praxi lemma_addr_param {l:addr} () : [l >= null] void

//
(* ****** ****** *)
praxi lemma_string_param {n:int} (x : string(n)) : [n >= 0] void

// end of [lemma_string_param]
praxi lemma_stropt_param {n:int} (x : stropt(n)) : [n >= ~1] void

// end of [lemma_stropt_param]
(* ****** ****** *)
//
dataprop SGN(int, int) =
  | SGNzero((0, 0))
  | {i:neg} SGNneg((i, ~1))
  | {i:pos} SGNpos((i, 1))

(* ****** ****** *)
//
// HX-2012-06:
// indication of the failure of
exception AssertExn of ()

// an assertion
//
(* ****** ****** *)
//
// HX-2012-06:
// indication of something expected
exception NotFoundExn of ()

// to be found but not
//
(* ****** ****** *)
//
exception GenerallyExn of (string)

// for unspecified causes
(*
exception GenerallyExn2 of (string, ptr(*data*)) // for unspecified causes
*)
//
(* ****** ****** *)
//
// HX-2012-07:
// indication of a function argument being
exception IllegalArgExn of (string)

// out of its domain
//
(* ****** ****** *)
praxi __vfree_exn(x : exn) :<> void

// for freeing nullary exception-con
(* ****** ****** *)
//
datatype unit =
  | unit of ()

dataprop unit_p =
  | unit_p of ()

dataview unit_v =
  | unit_v of ()

datavtype unit_vt =
  | unit_vt of ()

//
prfun unit_v_elim(pf : unit_v) : void

//
(* ****** ****** *)
//
abstype boxed_t0ype_type(a: t@ype+) = unit
absvtype boxed_vt0ype_vtype(a: vt@ype+) = unit

//
vtypedef boxed(a: vt@ype) = boxed_vt0ype_vtype(a)
vtypedef boxed_vt(a: vt@ype) = boxed_vt0ype_vtype(a)

//
typedef boxed(a: t@ype) = boxed_t0ype_type(a)
typedef boxed_t(a: t@ype) = boxed_t0ype_type(a)

//
fun {a:type} box  : (INV(a)) -> boxed_t(a)

fun {a:type} unbox  : boxed_t(INV(a)) -> (a)

fun {a:vtype} box_vt  : (INV(a)) -> boxed_vt(a)

fun {a:vtype} unbox_vt  : boxed_vt(INV(a)) -> (a)

(* ****** ****** *)
//
stadef array (a: vt@ype, n: int) = @[a][n]

//
viewdef array_v(a: vt@ype, l: addr, n: int) = @[a][n] @ l

//
absvtype arrayptr_vt0ype_addr_int_vtype( a: vt0ype+
                                       , l: addr
                                       , n: int
                                       ) = ptr(l)

stadef arrayptr  = arrayptr_vt0ype_addr_int_vtype

vtypedef arrayptr(a: vt0p, n: int) = [l:addr] arrayptr(a, l, n)

//
abstype arrayref_vt0ype_int_type(a: vt@ype, n: int) = ptr

stadef arrayref  = arrayref_vt0ype_int_type

//
abstype arrszref_vt0ype_type(a: vt@ype) = ptr

typedef arrszref(a: vt0p) = arrszref_vt0ype_type(a)

//
(* ****** ****** *)
//
datatype list_t0ype_int_type(a: t@ype+, int) =
  | list_nil(a, 0) of ()
  | { n : int | n >= 0 } list_cons( a
                                  , n+1
                                  ) of (a, list_t0ype_int_type(a, n))

stadef list  = list_t0ype_int_type

typedef List(a: t0p) = [n:int] list(a, n)
typedef List0(a: t0p) = [ n : int | n >= 0 ] list(a, n)
typedef List1(a: t0p) = [ n : int | n >= 1 ] list(a, n)
typedef listLt(a: t0p, n: int) = [ k : nat | k < n ] list(a, k)
typedef listLte(a: t0p, n: int) = [ k : nat | k <= n ] list(a, k)
typedef listGt(a: t0p, n: int) = [ k : int | k > n ] list(a, k)
typedef listGte(a: t0p, n: int) = [ k : int | k >= n ] list(a, k)
typedef listBtw( a: t0p
               , m: int
               , n: int
               ) = [ k : int | m <= k; k < n ] list(a, k)
typedef listBtwe( a: t0p
                , m: int
                , n: int
                ) = [ k : int | m <= k; k <= n ] list(a, k)

//
(* ****** ****** *)
//
datavtype list_vt0ype_int_vtype(a: vt@ype+, int) =
  | list_vt_nil(a, 0) of ()
  | { n : int | n >= 0 } list_vt_cons( a
                                     , n+1
                                     ) of (a, list_vt0ype_int_vtype(a, n))

stadef list_vt  = list_vt0ype_int_vtype

vtypedef List_vt(a: vt0p) = [n:int] list_vt(a, n)
vtypedef List0_vt(a: vt0p) = [ n : int | n >= 0 ] list_vt(a, n)
vtypedef List1_vt(a: vt0p) = [ n : int | n >= 1 ] list_vt(a, n)
vtypedef listLt_vt(a: vt0p, n: int) = [ k : nat | k < n ] list_vt(a, k)
vtypedef listLte_vt(a: vt0p, n: int) =
  [ k : nat | k <= n ] list_vt(a, k)
vtypedef listGt_vt(a: vt0p, n: int) = [ k : int | k > n ] list_vt(a, k)
vtypedef listGte_vt(a: vt0p, n: int) =
  [ k : int | k >= n ] list_vt(a, k)
vtypedef listBtw_vt(a: vt0p, m: int, n: int) =
  [ k : int | m <= k; k < n ] list_vt(a, k)
vtypedef listBtwe_vt(a: vt0p, m: int, n: int) =
  [ k : int | m <= k; k <= n ] list_vt(a, k)

//
(* ****** ****** *)
//
datatype stream_con(a: t@ype+) =
  | stream_nil of ()
  | stream_cons of (a, stream(a))   where
                                    stream (a: t@ype) = lazy(stream_con(a))

//
datavtype stream_vt_con(a: vt@ype+) =
  | stream_vt_nil of ()
  | stream_vt_cons of (a, stream_vt(a))   where
                                          stream_vt (a: vt@ype) = lazy_vt(stream_vt_con(a))

//
(* ****** ****** *)
//
datatype option_t0ype_bool_type(a: t@ype+, bool) =
  | Some(a, true) of (INV(a))
  | None(a, false)

// end of [datatype]
stadef option  = option_t0ype_bool_type

typedef Option(a: t0p) = [b:bool] option(a, b)

//
datavtype option_vt0ype_bool_vtype(a: vt@ype+, bool) =
  | Some_vt(a, true) of (INV(a))
  | None_vt(a, false)

// end of [option_vt0ype_bool_vtype]
stadef option_vt  = option_vt0ype_bool_vtype

vtypedef Option_vt(a: vt0p) = [b:bool] option_vt(a, b)

//
(* ****** ****** *)
//
praxi opt_some {a:vt0p} (x : !INV(a) >> opt(a, true)) :<prf> void

praxi opt_unsome {a:vt0p} (x : !opt(INV(a), true) >> a) :<prf> void

//
fun {a:vt0p} opt_unsome_get (x : &opt(INV(a), true) >> a?) : (a)

praxi opt_none {a:vt0p} (x : !(a?) >> opt(a, false)) :<prf> void

praxi opt_unnone {a:vt0p} (x : !opt(INV(a), false) >> a?) :<prf> void

//
praxi opt_clear {a:t0p}{b:bool} (x : !opt(INV(a), b) >> a?) :<prf> void

//
(* ****** ****** *)
//
dataprop or_prop_prop_int_prop(a0: prop+, a1: prop+, int) =
  | POR_l(a0, a1, 0) of (INV(a0))
  | POR_r(a0, a1, 1) of (INV(a1))

dataview or_view_view_int_view(a0: view+, a1: view+, int) =
  | VOR_l(a0, a1, 0) of (INV(a0))
  | VOR_r(a0, a1, 1) of (INV(a1))

stadef por  = or_prop_prop_int_prop
stadef vor  = or_view_view_int_view

//
dataprop option_prop_bool_prop(a: prop+, bool) =
  | Some_p((a, true)) of (INV(a))
  | None_p((a, false))

stadef option_p  = option_prop_bool_prop

//
dataview option_view_bool_view(a: view+, bool) =
  | Some_v(a, true) of (INV(a))
  | None_v(a, false)

// end of [option_view_bool_view]
stadef option_v  = option_view_bool_view

//
(* ****** ****** *)
//
absvt@ype arrayopt(a: vt0p, n: int, b: bool) = array(a, n)

//
praxi arrayopt_some {a:vt0p}{n:int}
(A : &array(a, n) >> arrayopt(a, n, true)) : void

praxi arrayopt_none {a:vt0p}{n:int}
(A : &array(a?, n) >> arrayopt(a, n, false)) : void

praxi arrayopt_unsome {a:vt0p}{n:int}
(A : &arrayopt(a, n, true) >> array(a, n)) : void

praxi arrayopt_unnone {a:vt0p}{n:int}
(A : &arrayopt(a, n, false) >> array(a?, n)) : void

//
(* ****** ****** *)
absvtype argv_int_vtype(n: int) = ptr

stadef argv  = argv_int_vtype

(*
[argv_takeout_strarr] is declared in prelude/SATS/extern.sats
[argv_takeout_parrnull] is declared in prelude/SATS/extern.sats
*)
(* ****** ****** *)
praxi lemma_argv_param {n:int} (argv : !argv(n)) : [n >= 0] void

// end of [praxi]
(* ****** ****** *)
//
fun argv_get_at {n:int}(argv : !argv(n), i : natLt(n)) :<> string =
  "mac#%"

fun argv_set_at {n:int}(argv : !argv(n), i : natLt(n), x : string) 
  :<!wrt> void =
  "mac#%"

//
overload [] with argv_get_at

overload [] with argv_set_at

//
(* ****** ****** *)
//
fun listize_argc_argv {n:int} (argc : int(n), argv : !argv(n)) :
  list_vt(string, n)

//
(* ****** ****** *)
//
symintr main0

//
fun main_void_0() : void =
  "ext#mainats_void_0"

fun main_argc_argv_0 { n : int | n >= 1 }( argc : int(n)
                                         , argv : !argv(n)
                                         ) : void =
  "ext#mainats_argc_argv_0"

//
overload main0 with main_void_0

overload main0 with main_argc_argv_0

//
(* ****** ****** *)
//
symintr main

//
fun main_void_int() : int =
  "ext#mainats_void_int"

fun main_argc_argv_int { n : int | n >= 1 }( argc : int(n)
                                           , argv : !argv(n)
                                           ) : int =
  "ext#mainats_argc_argv_int"

fun main_argc_argv_envp_int { n : int | n >= 1 }( argc : int(n)
                                                , argv : !argv(n)
                                                , envp : ptr
                                                ) : int =
  "ext#mainats_argc_argv_envp_int"

//
overload main with main_void_int

overload main with main_argc_argv_int

overload main with main_argc_argv_envp_int

//
(* ****** ****** *)
//
fun exit(ecode : int) :<!exn> {a:t0p} (a) =
  "mac#%"

fun exit_errmsg(ecode : int, msg : string) :<!exn> {a:t0p} (a) =
  "mac#%"

//
(*
fun exit_fprintf{ts:types}
(
  ecode: int, out: FILEref, fmt: printf_c ts, args: ts
) :<!exn> {a:vt0p}(a) = "mac#%" // end of [exit_fprintf]
*)
//
(* *****p* ****** *)
//
fun exit_void(ecode : int) :<!exn> void =
  "mac#%"

fun exit_errmsg_void(ecode : int, msg : string) :<!exn> void =
  "mac#%"

//
(* ****** ****** *)
//
fun assert_bool0(x : bool) :<!exn> void =
  "mac#%"

fun assert_bool1 {b:bool}(x : bool(b)) :<!exn> [b] void =
  "mac#%"

//
overload assert with assert_bool0 of 0

overload assert with assert_bool1 of 10

//
(* ****** ****** *)
//
fun assertexn_bool0(x : bool) :<!exn> void

fun assertexn_bool1 {b:bool} (x : bool(b)) :<!exn> [b] void

//
symintr assertexn

overload assertexn with assertexn_bool0 of 0

overload assertexn with assertexn_bool1 of 10

//
(* ****** ****** *)
//
fun assert_errmsg_bool0(x : bool, msg : string) :<!exn> void =
  "mac#%"

fun assert_errmsg_bool1 {b:bool}(x : bool(b), msg : string) :<!exn>
  [b] void =
  "mac#%"

//
symintr assert_errmsg

overload assert_errmsg with assert_errmsg_bool0 of 0

overload assert_errmsg with assert_errmsg_bool1 of 10

//
(* ****** ****** *)
//
fun assert_errmsg2_bool0(x : bool, msg1 : string, msg2 : string) :<!exn>
  void =
  "mac#%"

fun assert_errmsg2_bool1 {b:bool}( x : bool(b)
                                 , msg1 : string
                                 , msg2 : string
                                 ) :<!exn> [b] void =
  "mac#%"

//
symintr assert_errmsg2

overload assert_errmsg2 with assert_errmsg2_bool0 of 0

overload assert_errmsg2 with assert_errmsg2_bool1 of 10

//
(* ****** ****** *)
//
datasort file_mode =
  | file_mode_r
  | file_mode_w
  | file_mode_rw

// end of [file_mode]
//
(* ****** ****** *)
local
  //
  stadef r () = file_mode_r()
  stadef w () = file_mode_w()
  stadef rw () = file_mode_rw()
  
  //
in
  (* in-of-local *)
  (* ****** ****** *)
  abstype file_mode(file_mode) = string
  
  typedef file_mode = [fm:file_mode] file_mode(fm)
  
  (* ****** ****** *)
  sortdef fmode = file_mode
  
  typedef fmode(fm: fmode) = file_mode(fm)
  typedef fmode = file_mode
  
  (* ****** ****** *)
  dataprop file_mode_lte(fmode, fmode) =
    | {m:fmode} file_mode_lte_refl((m, m))
    | { m1, m2, m3 : fmode } file_mode_lte_tran((m1, m3)) of (file_mode_lte( m1
                                                                           , m2
                                                                           ), file_mode_lte(m2, m3))
    | {m:fmode} file_mode_lte_rw_r(rw(), r()) of ()
    | {m:fmode} file_mode_lte_rw_w(rw(), w()) of ()
  
  (* ****** ****** *)
  //
  prval file_mode_lte_r_r : file_mode_lte(r(), r())
  
  // impled in [filebas_prf.dats]
  prval file_mode_lte_w_w : file_mode_lte(w(), w())
  
  // impled in [filebas_prf.dats]
  prval file_mode_lte_rw_rw : file_mode_lte(rw(), rw())
  
  // impled in [filebas_prf.dats]
  //
  (* ****** ****** *)
end

// end of [local]
(* ****** ****** *)
abstype FILEref_type = ptr

typedef FILEref = FILEref_type

(* ****** ****** *)
//
typedef print_type(a: t0p) = (a) -> void
typedef prerr_type(a: t0p) = (a) -> void
typedef fprint_type(a: t0p) = (FILEref, a) -> void

//
typedef print_vtype(a: vt0p) = (!a) -> void
typedef prerr_vtype(a: vt0p) = (!a) -> void
typedef fprint_vtype(a: vt0p) = (FILEref, !a) -> void

//
(* ****** ****** *)
(*
fun print_void(x: void): void = "mac#%"
*)
(* ****** ****** *)
fun print_newline() : void =
  "mac#%"

fun prerr_newline() : void =
  "mac#%"

fun fprint_newline(out : FILEref) : void =
  "mac#%"

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

#if VERBOSE_PRELUDE #then
#print "Loading [basics_dyn.sats] finishes!\n"
#endif // end of [VERBOSE_PRELUDE]
(* ****** ****** *)
(* end of [basics_dyn.sats] *)