(***********************************************************************)
(*                                                                     *)
(*                         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.
*)

(* ****** ****** *)
//
// For supporting ML-style of functional programming
//
(* ****** ****** *)
//
// Author of the file: Hongwei Xi (gmhwxiATgmailDOTcom)
// Start Time: June, 2012
//
(* ****** ****** *)

#define ATS_PACKNAME "ATSLIB.libats"

(* ****** ****** *)
//
typedef
cfun0(b:vt0p) = ((*void*)) -<cloref1> b
typedef
cfun1(a:vt0p, b:vt0p) = (a) -<cloref1> b
typedef
cfun2(a1:vt0p, a2:vt0p, b:vt0p) = (a1, a2) -<cloref1> b
//
(* ****** ****** *)
//
typedef
cfun3 (
  a1:vt0p, a2:vt0p, a3:vt0p, b:vt0p
) = (a1, a2, a3) -<cloref1> b
typedef
cfun4 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, b:vt0p
) = (a1, a2, a3, a4) -<cloref1> b
typedef
cfun5 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, b:vt0p
) = (a1, a2, a3, a4, a5) -<cloref1> b
typedef
cfun6 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, a6:vt0p, b:vt0p
) = (a1, a2, a3, a4, a5, a6) -<cloref1> b
typedef
cfun7 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, a6:vt0p, a7:vt0p, b:vt0p
) = (a1, a2, a3, a4, a5, a6, a7) -<cloref1> b
typedef
cfun8 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, a6:vt0p, a7:vt0p, a8:vt0p, b:vt0p
) = (a1, a2, a3, a4, a5, a6, a7, a8) -<cloref1> b
typedef
cfun9 (
  a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, a6:vt0p, a7:vt0p, a8:vt0p, a9:vt0p, b:vt0p
) = (a1, a2, a3, a4, a5, a6, a7, a8, a9) -<cloref1> b
//
(* ****** ****** *)

stadef cfun = cfun0
stadef cfun = cfun1
stadef cfun = cfun2
stadef cfun = cfun3
stadef cfun = cfun4
stadef cfun = cfun5
stadef cfun = cfun6
stadef cfun = cfun7
stadef cfun = cfun8
stadef cfun = cfun9

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

datatype // t@ype+: covariant
list0_t0ype_type (a: t@ype+) =
  | list0_nil of () | list0_cons of (a, list0_t0ype_type a)
stadef list0 = list0_t0ype_type

#define nil0 list0_nil
#define cons0 list0_cons

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

datatype // t@ype+: covariant
option0_t0ype_type
  (a: t@ype+) = Some0 of (a) | None0 of ()
stadef option0 = option0_t0ype_type

(* ****** ****** *)
//
abstype
array0_vt0ype_type
  (a: vt@ype(*invariant*)) = ptr
stadef array0 = array0_vt0ype_type
(*
abstype
subarray0_vt0ype_type
  (a: vt@ype(*invariant*)) = ptr
stadef subarray0 = subarray0_vt0ype_type
*)
//
(* ****** ****** *)
//
abstype
matrix0_vt0ype_type
  (a: vt@ype(*invariant*)) = ptr
stadef matrix0 = matrix0_vt0ype_type
//
(* ****** ****** *)
//
abstype strarr_type = ptr
typedef strarr = strarr_type
(*
abstype substrarr_type = ptr
typedef substrarr = substrarr_type
*)
//
(* ****** ****** *)
//
abstype
dynarray_type(a:vt@ype) = ptr
//
typedef
dynarray(a:vt@ype) = dynarray_type(a)
//
(* ****** ****** *)
//
// HX: for maps of elements of type (a)
//
abstype
hashtbl_type
  (key:t@ype, itm:t@ype) = ptr
//
typedef
hashtbl(key:t@ype, itm:t@ype) = hashtbl_type(key, itm)
//
(* ****** ****** *)
//
// HX-2015-12-01:
// G-values for generic programming
//
(* ****** ****** *)
//
datatype gvalue =
//
  | GVnil of ()
//
  | GVint of (int)
//
  | GVptr of (ptr)
//
  | GVbool of (bool)
  | GVchar of (char)
//
  | GVfloat of (double)
//
  | GVstring of (string)
//
  | GVref of (gvref)
//
  | GVlist of (gvlist)
//
  | GVarray of (gvarray)
//
  | GVdynarr of (gvdynarr)
//
  | GVhashtbl of (gvhashtbl)
//
  | GVfunclo_fun of ((gvalue) -<fun1> gvalue)
  | GVfunclo_clo of ((gvalue) -<cloref1> gvalue)
//
where
gvref = ref(gvalue)
and
gvlist = list0(gvalue)
and
gvarray = array0(gvalue)
and
gvdynarr = dynarray(gvalue)
and
gvhashtbl = hashtbl(string, gvalue)
//
(* ****** ****** *)

(* end of [basis.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: gmmhwxiATgmailDOTcom *)
(* Start time: May, 2012 *)

(* ****** ****** *)
//
// HX-2013-01:
// A rule of thumb for effect-annotation is that
// higher-order functions should not be annotated!
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
//
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

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

(*
typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose
*)

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

#define nil0 list0_nil
#define cons0 list0_cons

(* ****** ****** *)
//
#define
list0_sing(x) list0_cons(x, list0_nil())
//
#define
list0_pair(x1, x2)
list0_cons(x1, list0_cons (x2, list0_nil()))
//
(* ****** ****** *)
//
castfn
list0_cast{x:t0p} (xs: list0(INV(x))):<> list0(x)
//
(* ****** ****** *)
//
castfn
list0_of_list
  {a:t@ype}(List(INV(a))):<> list0(a)
castfn
list0_of_list_vt
  {a:t@ype}(List_vt(INV(a))):<> list0(a)
//
(* ****** ****** *)
//
castfn
g0ofg1_list{a:t@ype}(List(INV(a))):<> list0(a)
castfn
g0ofg1_list_vt{a:t@ype}(List_vt(INV(a))):<> list0(a)
//
overload g0ofg1 with g0ofg1_list
overload g0ofg1 with g0ofg1_list_vt
//
(* ****** ****** *)
//
castfn
g1ofg0_list{a:t@ype}(list0(INV(a))):<> List0(a)
//
overload g1ofg0 with g1ofg0_list
//
(* ****** ****** *)

fun{a:t0p}
list0_make_sing (x: a):<> list0(a)
fun{a:t0p}
list0_make_pair (x1: a, x2: a):<> list0(a)

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

fun{a:t0p}
list0_make_elt (n: int, x: a):<!exn> list0(a)

(* ****** ****** *)
//
symintr list0
//
fun{a:t0p}
list0_make_arrpsz{n:int}
  (psz: arrpsz(INV(a), n)):<!wrt> list0(a)
//
overload list0 with list0_make_arrpsz
//
(* ****** ****** *)
//
fun{}
list0_make_intrange_lr
  (l: int, r: int):<> list0(int)
fun{}
list0_make_intrange_lrd
  (l: int, r: int, d: int):<!exn> list0(int)
//
symintr list0_make_intrange
//
overload list0_make_intrange with list0_make_intrange_lr
overload list0_make_intrange with list0_make_intrange_lrd
//
(* ****** ****** *)
//
fun{a:t0p}
list0_is_nil(list0(a)):<> bool
fun{a:t0p}
list0_is_cons(list0(a)):<> bool
//
(* ****** ****** *)
//
fun{a:t0p}
list0_is_empty(list0(a)):<> bool
fun{a:t0p}
list0_isnot_empty(list0(a)):<> bool
//
overload iseqz with list0_is_empty
overload isneqz with list0_isnot_empty
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_length
  (xs: list0(INV(a))):<> intGte(0)
//
overload length with list0_length of 0
//
(* ****** ****** *)
//
fun{a:t0p}
list0_head_exn
  (xs: list0(INV(a))):<!exn> (a)
fun{a:t0p}
list0_head_opt
  (xs: list0(INV(a))):<> Option_vt(a)
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_tail_exn
  (xs: SHR(list0(INV(a)))):<!exn> list0(a)
fun
{a:t0p}
list0_tail_opt
  (xs: SHR(list0(INV(a)))):<> Option_vt(list0(a))
//
(* ****** ****** *)
//
overload head with list0_head_exn of 0
overload tail with list0_tail_exn of 0
//
overload .head with list0_head_exn of 0
overload .tail with list0_tail_exn of 0
//
overload head_opt with list0_head_opt of 0
overload tail_opt with list0_tail_opt of 0
//
overload .head_opt with list0_head_opt of 0
overload .tail_opt with list0_tail_opt of 0
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_last_exn(xs: list0(INV(a))):<!exn> (a)
fun
{a:t0p}
list0_last_opt(xs: list0(INV(a))):<> Option_vt(a)
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_init_exn(xs: list0(INV(a))):<!exn> list0(a)
fun
{a:t0p}
list0_init_opt(xs: list0(INV(a))):<!exn> Option_vt(list0(a))
//
(* ****** ****** *)
//
fun{a:t0p}
list0_nth_exn
  (xs: list0(INV(a)), i: int):<!exn> (a)
fun{a:t0p}
list0_nth_opt
  (xs: list0(INV(a)), i: int):<> Option_vt(a)
//
(* ****** ****** *)
//
fun{a:t0p}
list0_get_at_exn
  (xs: list0(INV(a)), i0: int):<!exn> (a)
//
overload [] with list0_get_at_exn
//
(* ****** ****** *)
//
fun{a:t0p}
list0_fset_at_exn
  (list0(INV(a)), i0: int, x0: a):<!exn> list0(a)
fun{a:t0p}
list0_fset_at_opt
  (list0(INV(a)), i0: int, x0: a):<!exn> Option_vt(list0(a))
//
(* ****** ****** *)
//
fun{a:t0p}
print_list0(xs: list0(INV(a))): void
fun{a:t0p}
prerr_list0(xs: list0(INV(a))): void
//
fun{a:t0p}
fprint_list0
(
  out: FILEref, xs: list0(INV(a))
) : void // end of [fprint_list0]
fun{a:t0p}
fprint_list0_sep
(
  out: FILEref, xs: list0(INV(a)), sep: string
) : void // end of [fprint_list0_sep]
//
overload print with print_list0
overload prerr with prerr_list0
//
overload fprint with fprint_list0
overload fprint with fprint_list0_sep
//
(* ****** ****** *)
//
fun{a:t0p}
fprint_listlist0_sep
( out: FILEref
, xss: list0(list0(INV(a))), sep1: string, sep2: string
) : void // end of [fprint_list0_sep]
//
overload fprint with fprint_listlist0_sep
//
(* ****** ****** *)

fun{a:t0p}
list0_insert_at_exn
(
  SHR(list0(INV(a))), i: int, x: a
) :<!exn> list0(a) // endfun

(* ****** ****** *)
//
fun{a:t0p}
list0_remove_at_exn
  (SHR(list0(INV(a))), int):<!exn> list0(a)
// end of [list0_remove_at_exn]
//
fun{a:t0p}
list0_takeout_at_exn
(
  xs: SHR(list0(INV(a))), i: int, x: &a? >> a
) :<!exnwrt> list0(a) // end-of-function
//
overload remove_at with list0_remove_at_exn
overload takeout_at with list0_takeout_at_exn
//
(* ****** ****** *)
//
fun{a:t0p}
list0_append
(
  xs: NSH(list0(INV(a))), ys: SHR(list0(a))
) :<> list0(a)
//
overload + with list0_append
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_extend
  (xs: NSH(list0(INV(a))), y0: a):<> list0(a)
//
macdef list0_snoc = list0_extend
//
(* ****** ****** *)
//
fun{a:t0p}
mul_int_list0
(
  m0: intGte(0), xs: NSH(list0(INV(a)))
) :<> list0(a) // end of [mul_int_list0]
//
(* ****** ****** *)
//
fun{a:t0p}
list0_reverse
  (xs: list0(INV(a))):<> list0(a)
//
overload reverse with list0_reverse
//
fun{a:t0p}
list0_reverse_append
  (xs: list0(INV(a)), ys: list0(a)):<> list0(a)
// end of [list0_reverse_append]
//
macdef
list0_revapp = list0_reverse_append
//
overload revapp with list0_reverse_append
//
(* ****** ****** *)
//
fun{a:t0p}
list0_concat
  (xss: NSH(list0(list0(INV(a))))):<> list0(a)
//
overload concat with list0_concat
//
(* ****** ****** *)

fun{a:t0p}
list0_take_exn
  (xs: NSH(list0(INV(a))), i: int):<!exn> list0(a)
// end of [list0_take_exn]

fun{a:t0p}
list0_drop_exn
  (xs: SHR(list0(INV(a))), i: int):<!exn> list0(a)
// end of [list0_drop_exn]

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

fun
{a:t0p}
list0_app
(
  xs: list0(INV(a)), fwork: cfun(a, void)
) : void // end of [list0_app]

(* ****** ****** *)
//
fun{a:t0p}
list0_foreach
(
  xs: list0(INV(a)), fwork: cfun(a, void)
) : void // end of [list0_foreach]
//
fun{a:t0p}
list0_foreach_method
(
  xs: list0(INV(a))) (fwork: cfun(a, void)
) : void // end of [list0_foreach_method]
//
overload .foreach with list0_foreach_method
//
(* ****** ****** *)
//
fun{a:t0p}
list0_rforeach
(
  xs: list0(INV(a)), fwork: cfun(a, void)
) : void // end of [list0_rforeach]
//
fun{a:t0p}
list0_rforeach_method
(
  xs: list0(INV(a))) (fwork: cfun(a, void)
) : void // end of [list0_rforeach_method]
//
overload .rforeach with list0_rforeach_method
//
(* ****** ****** *)
//
fun{a:t0p}
list0_iforeach
(
  list0(INV(a)), fwork: cfun2(intGte(0), a, void)
) : intGte(0)(*length*) // end of [list0_iforeach]
//
fun{a:t0p}
list0_iforeach_method
(
  list0(INV(a))) (fwork: cfun2(intGte(0), a, void)
) : intGte(0)(*length*) // end of [list0_iforeach_method]
//
overload .iforeach with list0_iforeach_method
//
(* ****** ****** *)

fun
{a1,a2:t0p}
list0_foreach2
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, fwork: cfun2(a1, a2, void)
) : void // end of [list0_foreach2]

fun{a1,a2:t0p}
list0_foreach2_eq
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, fwork: cfun2(a1, a2, void), sgn: &int? >> int
) : void // end of [list0_foreach2_eq]

(* ****** ****** *)
//
fun{
res:t0p}{a:t0p
} list0_foldleft
  (list0(INV(a)), ini: res, fopr: cfun2(res, a, res)): res
//
fun{
res:t0p}{a:t0p
} list0_foldleft_method
  (list0(INV(a)), TYPE(res))(ini: res, fopr: cfun2(res, a, res)): res
//
overload .foldleft with list0_foldleft_method
//
(* ****** ****** *)
//
fun{
res:t0p}{a:t0p
} list0_ifoldleft
  (list0(INV(a)), ini: res, fopr: cfun3(res, int, a, res)): res
// end of [list0_ifoldleft]
//
fun{
res:t0p}{a:t0p
} list0_ifoldleft_method
  (list0(INV(a)), TYPE(res))(ini: res, fopr: cfun3(res, int, a, res)): res
// end of [list0_ifoldleft_method]
//
overload .ifoldleft with list0_ifoldleft_method
//
(* ****** ****** *)

fun{
res:t0p}{a1,a2:t0p
} list0_foldleft2 (
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, ini: res, fopr: cfun3(res, a1, a2, res)
) : res // end of [list0_foldleft2]

(* ****** ****** *)
//
fun{
a:t0p}{res:t0p
} list0_foldright
  (xs: list0(INV(a)), fopr: cfun2(a, res, res), snk: res): res
//
fun{
a:t0p}{res:t0p
} list0_foldright_method
  (list0(INV(a)), TYPE(res)) (fopr: cfun2(a, res, res), snk: res): res
//
overload .foldright with list0_foldright_method
//
(* ****** ****** *)
//
(*
fun{
a:t0p}{res:t0p
} list0_ifoldright
  (xs: list0(INV(a)), fopr: cfun3(int, a, res, res), snk: res): res
// end of [list0_ifoldright]
*)
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_exists
  (xs: list0(INV(a)), pred: cfun(a, bool)): bool
//
fun
{a:t0p}
list0_exists_method
  (xs: list0(INV(a))) (pred: cfun(a, bool)): bool
//
overload .exists with list0_exists_method
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_iexists
(
  xs: list0(INV(a)), pred: cfun(intGte(0), a, bool)
) : bool // end of [list0_iexists]
//
fun
{a:t0p}
list0_iexists_method
(
  xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool)
) : bool // end of [list0_iexists_method]
//
overload .iexists with list0_iexists_method
//
(* ****** ****** *)
//
fun
{a1,a2:t0p}
list0_exists2
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool)
) : bool // end of [list0_exists2]
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_forall
  (xs: list0(INV(a)), pred: cfun(a, bool)): bool
//
fun
{a:t0p}
list0_forall_method
  (xs: list0(INV(a))) (pred: cfun(a, bool)): bool
//
overload .forall with list0_forall_method
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_iforall
(
  xs: list0(INV(a)), pred: cfun(intGte(0), a, bool)
) : bool // end of [list0_iforall]
//
fun
{a:t0p}
list0_iforall_method
(
  xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool)
) : bool // end of [list0_iforall_method]
//
overload .iforall with list0_iforall_method
//
(* ****** ****** *)
//
fun
{a1,a2:t0p}
list0_forall2 (
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool)
) : bool // end of [list0_forall2]
fun
{a1,a2:t0p}
list0_forall2_eq
(
  xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, p: cfun2(a1, a2, bool), sgn: &int? >> int
) : bool // end of [list0_forall2_eq]
//
(* ****** ****** *)

fun
{a:t0p}
list0_equal
(
  xs1: list0(INV(a))
, xs2: list0(INV(a)), eqfn: cfun2(a, a, bool)
) : bool // end of [list0_equal]

(* ****** ****** *)
//
fun
{a:t0p}
list0_find_exn
  (xs: list0(INV(a)), pred: cfun(a, bool)): (a)
fun
{a:t0p}
list0_find_opt
  (xs: list0(INV(a)), pred: cfun(a, bool)): Option_vt(a)
//
fun
{a:t0p}
list0_find_exn_method
  (xs: list0(INV(a)))(pred: cfun(a, bool)): (a)
fun
{a:t0p}
list0_find_opt_method
  (xs: list0(INV(a)))(pred: cfun(a, bool)): Option_vt(a)
//
overload .find with list0_find_exn_method
overload .find_opt with list0_find_opt_method
//
(* ****** ****** *)
//
fun
{a:t0p}
list0_find_index
(
  xs: list0(INV(a)), pred: cfun(a, bool)
) : intGte(~1) // end of [list0_find_index]
//
(* ****** ****** *)
//
fun{
a,b:t0p
} list0_assoc_exn
(
  list0 @(INV(a), b), x0: a, eq: cfun(a, a, bool)
) : (b) // end-of-function
fun{
a,b:t0p
} list0_assoc_opt
(
  list0 @(INV(a), b), x0: a, eq: cfun(a, a, bool)
) : Option_vt (b) // end-of-function
//
(* ****** ****** *)
//
fun{a:t0p}
list0_filter
  (list0(INV(a)), pred: cfun(a, bool)): list0(a)
fun{a:t0p}
list0_filter_method
  (list0(INV(a)))(pred: cfun(a, bool)): list0(a)
//
overload .filter with list0_filter_method
//
(* ****** ****** *)
//
fun
{a:t0p}
{b:t0p}
list0_map
(
  xs: list0(INV(a)), fopr: cfun(a, b)
) : list0(b) // end-of-function
//
fun
{a:t0p}
{b:t0p}
list0_mapopt
(
  xs: list0(INV(a)), fopr: cfun(a, Option_vt(b))
) : list0(b) // end-of-function
//
(* ****** ****** *)
//
fun
{a:t0p}
{b:t0p}
list0_map_method
(
  list0(INV(a)), TYPE(b))(fopr: cfun(a, b)
) : list0(b) // end-of-function
//
fun
{a:t0p}
{b:t0p}
list0_mapopt_method
(
  list0(INV(a)), TYPE(b))(fopr: cfun(a, Option_vt(b))
) : list0(b) // end-of-function
//
overload .map with list0_map_method
overload .mapopt with list0_mapopt_method
//
(* ****** ****** *)
//
fun{a:t0p}
list0_mapcons
  (x0: a, xss: list0(list0(INV(a)))): list0(list0(a))
//
overload * with list0_mapcons
//
(* ****** ****** *)
//
fun{
a:t0p}{b:t0p
} list0_imap
  (list0(INV(a)), fopr: cfun2(int, a, b)): list0(b)
fun{
a:t0p}{b:t0p
} list0_imap_method
  (list0(INV(a)), TYPE(b))(fopr: cfun2(int, a, b)): list0(b)
//
overload .imap with list0_imap_method
//
(* ****** ****** *)

fun{
a1,a2:t0p}{b:t0p
} list0_map2
(
  list0(INV(a1)), list0(INV(a2)), fopr: cfun2(a1, a2, b)
) : list0(b) // end of [list0_map2]

(* ****** ****** *)
//
fun{a:t0p}
list0_tabulate
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): list0(a)
fun{a:t0p}
list0_tabulate_opt
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), Option_vt(a))): list0(a)
//
(* ****** ****** *)
//
fun
{x,y:t0p}
list0_zip
(
  list0(INV(x)), list0(INV(y))
) :<> list0 @(x, y) // end-of-fun
//
(*
fun{
x,y:t0p}{z:t0p
} list0_zipwith
  (list0(INV(x)), list0(INV(y)), fopr: cfun2(x, y, z)): list0(z)
*)
macdef
list0_zipwith = list0_map2
//
(* ****** ****** *)
//
fun
{x,y:t0p}
list0_cross
  (list0(INV(x)), list0(INV(y))):<> list0 @(x, y)
//
overload * with list0_cross of 10
//
(* ****** ****** *)
//
fun{
x,y:t0p}{z:t0p
} list0_crosswith
(
  list0(INV(x)), list0(INV(y)), fopr: cfun2(x, y, z)
) : list0(z) // end of [list0_crosswith]
//
(* ****** ****** *)
//
fun
{x:t0p}
list0_foreach_choose2
(
  list0(INV(x)), fwork: cfun2(x, x, void)
) : void // end-of-function
fun
{x:t0p}
list0_foreach_choose2_method
(
  list0(INV(x))) (fwork: cfun2(x, x, void)
) : void // end-of-function
//
overload .foreach_choose2 with list0_foreach_choose2_method
//
(* ****** ****** *)
//
fun{
x,y:t0p
} list0_foreach_xprod2
(
  list0(INV(x)), list0(INV(y)), fwork: cfun2(x, y, void)
) : void // end-of-function
fun
{x,y:t0p}
list0_foreach_xprod2_method
(
  list0(INV(x)), list0(INV(y)))(fwork: cfun2(x, y, void)
) : void // end-of-function
//
fun{
x,y:t0p
} list0_iforeach_xprod2
(
  list0(INV(x)), list0(INV(y)), fwork: cfun4(intGte(0), x, intGte(0), y, void)
) : void // end-of-function
fun
{x,y:t0p}
list0_iforeach_xprod2_method
(
  list0(INV(x)), list0(INV(y)))(fwork: cfun4(intGte(0), x, intGte(0), y, void)
) : void // end-of-function
//
overload .foreach_xprod2 with list0_foreach_xprod2_method
overload .iforeach_xprod2 with list0_iforeach_xprod2_method
//
(* ****** ****** *)
//
fun{a:t0p}
streamize_list0_elt
  (list0(INV(a))):<!wrt> stream_vt(a)
//
fun{a:t0p}
streamize_list0_choose2
  (list0(INV(a))):<!wrt> stream_vt(@(a, a))
//
(* ****** ****** *)
//
fun
{a:t0p}
streamize_list0_nchoose
  (list0(INV(a)), intGte(0)):<!wrt> stream_vt(list0(a))
//
(*
fun
{a:t0p}
streamize_list0_nchoose_rest
  (list0(INV(a)), intGte(0)):<!wrt> stream_vt(@(list0(a), list0(a)))
*)
//
(* ****** ****** *)
//
fun
{a,b:t0p}
streamize_list0_zip
  (list0(INV(a)), list0(INV(b))):<!wrt> stream_vt(@(a, b))
fun
{a,b:t0p}
streamize_list0_cross
  (list0(INV(a)), list0(INV(b))):<!wrt> stream_vt(@(a, b))
//
(* ****** ****** *)
//
fun{a:t0p}
list0_is_ordered
  (xs: list0(INV(a)), cmp:  (a, a) -<cloref> int): bool
//
(* ****** ****** *)

fun{a:t0p}
list0_mergesort
  (NSH(list0(INV(a))), cmp: (a, a) -<cloref> int):<> list0(a)
// end of [list0_mergesort]

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

fun{a:t0p}
list0_quicksort
  (NSH(list0(INV(a))), cmp: (a, a) -<cloref> int):<> list0(a)
// end of [list0_quicksort]

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

(* end of [list0.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: gmmhwxiATgmailDOTcom *)
(* Start time: July, 2012 *)

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
//
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)

%{#
#include \
"libats/ML/CATS/array0.cats"
%} // end of [%{#]

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

staload "libats/ML/SATS/basis.sats"

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

typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

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

#if(0)
//
// HX: in [basis.sats]
//
abstype
array0_vt0ype_type
  (a: vt@ype(*invariant*)) = ptr
//
stadef array0 = array0_vt0ype_type
//
#endif // end of [#if(0)]

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

(*
typedef array0(a: vt@ype) = arrszref(a)
*)

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

(*
sortdef t0p = t@ype
sortdef vt0p = viewt@ype
*)

(* ****** ****** *)
//
fun{}
array0_of_arrszref
  {a:vt0p} (arrszref(a)):<> array0(a)
//
fun{}
arrszref_of_array0
  {a:vt0p} (A: array0(a)):<> arrszref(a)
//
(* ****** ****** *)
//
symintr array0
//
fun{}
array0_make_arrpsz
  {a:vt0p}{n:int}
  (psz: arrpsz(INV(a), n)):<!wrt> array0(a)
overload array0 with array0_make_arrpsz
//
fun{}
array0_make_arrayref
  {a:vt0p}{n:int}
  (A: arrayref(a, n), n: size_t (n)):<!wrt> array0(a)
overload array0 with array0_make_arrayref
//
(* ****** ****** *)
//
fun{}
array0_get_ref{a:vt0p} (A: array0(a)):<> Ptr1
fun{}
array0_get_size{a:vt0p} (A: array0(a)):<> size_t
//
fun{}
array0_get_refsize
  {a:vt0p}
  (array0(a)):<> [n:nat] (arrayref(a, n), size_t(n))
//
(* ****** ****** *)
//
fun{a:t0p}
array0_make_elt (asz: size_t, x: a):<!wrt> array0(a)
//
(* ****** ****** *)
//
fun{a:t0p}
array0_make_list (xs: list0(INV(a))):<!wrt> array0(a)
fun{a:t0p}
array0_make_rlist (xs: list0(INV(a))):<!wrt> array0(a)
//
(* ****** ****** *)

fun{a:t0p}
array0_make_subarray
  (A: array0(a), st: size_t, ln: size_t):<!wrt> array0(a)
// end of [array0_make_subarray]

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

fun{a:t0p}
array0_get_at_size
  (A: array0(a), i: size_t):<!exnref> (a)
fun{a:t0p}{tk:tk}
array0_get_at_gint
  (A: array0(a), i: g0int(tk)):<!exnref> (a)
fun{a:t0p}{tk:tk}
array0_get_at_guint
  (A: array0(a), i: g0uint(tk)):<!exnref> (a)
//
symintr array0_get_at
//
overload array0_get_at with array0_get_at_gint
overload array0_get_at with array0_get_at_guint
//
(* ****** ****** *)
//
fun{a:t0p}
array0_set_at_size
  (A: array0(a), i: size_t, x: a):<!exnrefwrt> void
fun{a:t0p}{tk:tk}
array0_set_at_gint
  (A: array0(a), i: g0int(tk), x: a):<!exnrefwrt> void
fun{a:t0p}{tk:tk}
array0_set_at_guint
  (A: array0(a), i: g0uint(tk), x: a):<!exnrefwrt> void
//
symintr array0_set_at
//
overload array0_set_at with array0_set_at_gint
overload array0_set_at with array0_set_at_guint
//
(* ****** ****** *)
//
fun{a:vt0p}
array0_exch_at_size
  (A: array0(a), i: size_t, x: &a >> _):<!exnrefwrt> void
fun{a:vt0p}{tk:tk}
array0_exch_at_gint
  (A: array0(a), i: g0int(tk), x: &a >> _):<!exnrefwrt> void
fun{a:vt0p}{tk:tk}
array0_exch_at_guint
  (A: array0(a), i: g0uint(tk), x: &a >> _):<!exnrefwrt> void
//
symintr array0_exch_at
//
overload array0_exch_at with array0_exch_at_gint
overload array0_exch_at with array0_exch_at_guint
//
(* ****** ****** *)

fun{a:vt0p}
array0_interchange
  (A: array0(a), i: size_t, j: size_t):<!exnrefwrt> void
// end of [array0_interchange]

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

fun{a:vt0p}
array0_subcirculate
  (A: array0(a), i: size_t, j: size_t):<!exnrefwrt> void
// end of [array0_subcirculate]

(* ****** ****** *)
//
fun{a:vt0p}
print_array0 (A: array0(a)): void
fun{a:vt0p}
prerr_array0 (A: array0(a)): void
//
(*
fun{}
fprint_array$sep (out: FILEref): void
*)
fun{a:vt0p}
fprint_array0
  (out: FILEref, A: array0(a)): void
fun{a:vt0p}
fprint_array0_sep
  (out: FILEref, A: array0(a), sep: string): void
//
(* ****** ****** *)

fun{a:t0p}
array0_copy(array0(a)):<!refwrt> array0(a)

(* ****** ****** *)
//
fun{a:t0p}
array0_append
  (array0(a), array0(a)):<!refwrt> array0(a)
// end of [array0_append]
//
overload + with array0_append
//
(* ****** ****** *)
//
fun
{a:vt0p}
{b:vt0p}
array0_map
(
A0: array0(a), fopr: (&a) -<cloref1> b
) : array0(b) // end of [array0_map]
fun
{a:vt0p}
{b:vt0p}
array0_map_method
(
A0: array0(a), TYPE(b)) (fopr: (&a) -<cloref1> b
) : array0(b) // end of [array0_map_method]
//
overload .map with array0_map_method
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_tabulate
  {n:int}
(
  asz: size_t(n), fopr: (sizeLt(n)) -<cloref1> a
) : array0(a) // end of [array0_tabulate]
//
(* ****** ****** *)
//
(*
** HX:
** Raising NotFoundExn
** if no satisfying element is found
*)
fun
{a:vt0p}
array0_find_exn
(
  A: array0(a), pred: (&a) -<cloref1> bool
) : size_t // end of [array0_find_exn]
//
fun
{a:vt0p}
array0_find_opt
(
  A: array0(a), pred: (&a) -<cloref1> bool
) : Option_vt(size_t) // end-of-function
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_exists
(
  A0: array0(a), pred: (&a) -<cloref1> bool
) : bool // end of [array0_exists]
fun
{a:vt0p}
array0_exists_method
(
  A0: array0(a)) (pred: (&a) -<cloref1> bool
) : bool // end of [array0_exists_method]
//
overload .exists with array0_exists_method
//
(* ****** ****** *)
//
fun
{a:t0p}
array0_iexists
(
  xs: array0(a), pred: cfun(size_t, a, bool)
) : bool // end of [array0_iexists]
//
fun
{a:t0p}
array0_iexists_method
(
  xs: array0(a)) (pred: cfun(size_t, a, bool)
) : bool // end of [array0_iexists_method]
//
overload .iexists with array0_iexists_method
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_forall
(
  A0: array0(a), pred: (&a) -<cloref1> bool
) : bool // end of [array0_forall]
fun
{a:vt0p}
array0_forall_method
(
  A0: array0(a)) (pred: (&a) -<cloref1> bool
) : bool // end of [array0_forall_method]
//
overload .forall with array0_forall_method
//
(* ****** ****** *)
//
fun
{a:t0p}
array0_iforall
(
  xs: array0(a), pred: cfun(size_t, a, bool)
) : bool // end of [array0_iforall]
//
fun
{a:t0p}
array0_iforall_method
(
  xs: array0(a)) (pred: cfun(size_t, a, bool)
) : bool // end of [array0_iforall_method]
//
overload .iforall with array0_iforall_method
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_foreach
(
  A0: array0(a)
, fwork: (&a >> _) -<cloref1> void
) : void // end of [array0_foreach]
//
fun
{a:vt0p}
array0_foreach_method
(
  A0: array0(a)
) (fwork: (&a >> _) -<cloref1> void): void
// end of [array0_foreach_methon]
//
overload .foreach with array0_foreach_method
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_iforeach
(
  A0: array0(a)
, fwork: (size_t, &a >> _) -<cloref1> void
) : void // end of [array0_iforeach]
//
fun
{a:vt0p}
array0_iforeach_method
(
  A0: array0(a)
) (fwork: (size_t, &a >> _) -<cloref1> void): void
// end of [array0_iforeach_method]
//
overload .iforeach with array0_iforeach_method
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_rforeach
  (A: array0(a), fwork: (&a >> _) -<cloref1> void): void
// end of [array0_rforeach]
//
fun
{a:vt0p}
array0_rforeach_method
  (A: array0(a)) (fwork: (&a >> _) -<cloref1> void): void
// end of [array0_rforeach]
//
overload .rforeach with array0_rforeach_method
//
(* ****** ****** *)
//
fun{
res:vt0p}{a:vt0p
} array0_foldleft
(
  A0: array0(a)
, ini: res, fopr: (res, &a) -<cloref1> res
) : res // end of [array0_foldleft]
//
fun{
res:vt0p}{a:vt0p
} array0_foldleft_method
(
  A: array0(a), TYPE(res)
)
(
  ini: res, fopr: (res, &a) -<cloref1> res
) : res // end of [array0_foldleft_method]
//
overload .foldleft with array0_foldleft_method
//
(* ****** ****** *)
//
fun{
res:vt0p}{a:vt0p
} array0_ifoldleft
(
  A0: array0(a)
, ini: res, fopr: (res, size_t, &a) -<cloref1> res
) : res // end of [array0_ifoldleft]
//
fun{
res:vt0p}{a:vt0p
} array0_ifoldleft_method
(
  A: array0(a), TYPE(res)
)
(
  ini: res, fopr: (res, size_t, &a) -<cloref1> res
) : res // end of [array0_ifoldleft_method]
//
overload .ifoldleft with array0_ifoldleft_method
//
(* ****** ****** *)
//
// HX: this one is tail-recursive!
//
fun{
a:vt0p}{res:vt0p
} array0_foldright
(
  A0: array0(a)
, fopr: (&a, res) -<cloref1> res, snk: res
) : res // end of [array0_foldright]
//
fun{
a:vt0p}{res:vt0p
} array0_foldright_method
(
  A: array0(a), TYPE(res)
)
(
  fopr: (&a, res) -<cloref1> res, snk: res
) : res // end of [array0_foldright_method]
//
overload .foldright with array0_foldright_method
//
(* ****** ****** *)
//
fun
{a:t0p}
streamize_array0_elt(array0(a)):<!wrt> stream_vt(a)
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_is_ordered
  (A0: array0(a), cmp: (&a, &a) -<cloref1> int): bool
//
(* ****** ****** *)
//
fun
{a:vt0p}
array0_quicksort
  (A0: array0(a), cmp: (&a, &a) -<cloref1> int): void
//
(* ****** ****** *)
//
// Overloading certain symbols
//
(* ****** ****** *)

overload [] with array0_get_at_gint
overload [] with array0_get_at_guint
overload [] with array0_set_at_gint
overload [] with array0_set_at_guint

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

overload size with array0_get_size
overload .size with array0_get_size

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

overload print with print_array0
overload prerr with print_array0
overload fprint with fprint_array0
overload fprint with fprint_array0_sep

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

overload append with array0_append

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

(* end of [array0.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: December, 2012 *)

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
//
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

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

typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

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

#if(0)
//
// HX: in [basis.sats]
//
abstype
matrix0_vt0ype_type
  (a: vt@ype(*invariant*)) = ptr
stadef matrix0 = matrix0_vt0ype_type
//
#endif

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

(*
typedef matrix0 (a: vt@ype) = mtrxszref (a)
*)

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

sortdef t0p = t@ype and vt0p = viewt@ype

(* ****** ****** *)
//
fun{}
matrix0_of_mtrxszref
  {a:vt0p} (mtrxszref (a)):<> matrix0 (a)
//
fun{}
mtrxszref_of_matrix0
  {a:vt0p} (M: matrix0 (a)):<> mtrxszref (a)
//
(* ****** ****** *)

fun{a:t0p}
matrix0_make_elt
  (nrow: size_t, ncol: size_t, init: a):<!wrt> matrix0 (a)
// end of [matrix0_make_elt]

(* ****** ****** *)
//
fun{}
matrix0_get_ref{a:vt0p} (M: matrix0 a):<> Ptr1
//
fun{}
matrix0_get_nrow{a:vt0p} (M: matrix0 a):<> size_t
fun{}
matrix0_get_ncol{a:vt0p} (M: matrix0 a):<> size_t
//
fun{}
matrix0_get_refsize
  {a:vt0p}
(
  M: matrix0 (a)
) :<> [m,n:nat] (matrixref (a, m, n), size_t(m), size_t(n))
//
(* ****** ****** *)
//
fun{a:t0p}
matrix0_get_at_int
  (M: matrix0(a), i: int, j: int):<!exnref> a
//
fun{a:t0p}
matrix0_get_at_size
  (M: matrix0 (a), i: size_t, j: size_t):<!exnref> a
//
symintr matrix0_get_at
overload matrix0_get_at with matrix0_get_at_int
overload matrix0_get_at with matrix0_get_at_size
//
(* ****** ****** *)
//
fun{a:t0p}
matrix0_set_at_int
  (M: matrix0(a), i: int, j: int, x: a):<!exnrefwrt> void
//
fun{a:t0p}
matrix0_set_at_size
  (M: matrix0 (a), i: size_t, j: size_t, x: a):<!exnrefwrt> void
//
symintr matrix0_set_at
overload matrix0_set_at with matrix0_set_at_int
overload matrix0_set_at with matrix0_set_at_size
//
(* ****** ****** *)
//
fun{a:vt0p}
print_matrix0 (M: matrix0 (a)): void
fun{a:vt0p}
prerr_matrix0 (M: matrix0 (a)): void
//
(*
fprint_matrix$sep1 // col separation
fprint_matrix$sep2 // row separation
*)
fun{a:vt0p}
fprint_matrix0 (out: FILEref, M: matrix0 (a)): void
fun{a:vt0p}
fprint_matrix0_sep
  (out: FILEref, M: matrix0 (a), sep1: string, sep2: string): void
//
(* ****** ****** *)

fun{a:t0p}
matrix0_copy (M: matrix0 (a)): matrix0 (a)

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

fun{a:vt0p}
matrix0_tabulate
(
  nrow: size_t, ncol: size_t, f: cfun (size_t, size_t, a)
) : matrix0 (a) // end-of-fun

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

fun{a:vt0p}
matrix0_foreach
  (M: matrix0 (a), f: (&a >> _) -<cloref1> void): void
// end of [matrix0_foreach]

fun{a:vt0p}
matrix0_iforeach
  (M: matrix0 (a), f: (size_t, size_t, &a >> _) -<cloref1> void): void
// end of [matrix0_iforeach]

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

fun{
res:vt0p}{a:vt0p
} matrix0_foldleft
(
  M: matrix0 (a), ini: res, f: (res, &a) -<cloref1> res
) : res // end of [matrix0_foldleft]

fun{
res:vt0p}{a:vt0p
} matrix0_ifoldleft
(
  M: matrix0 (a), ini: res, f: (res, size_t, size_t, &a) -<cloref1> res
) : res // end of [matrix0_ifoldleft]

(* ****** ****** *)
//
// overloading for certain symbols
//
(* ****** ****** *)

overload .nrow with matrix0_get_nrow
overload .ncol with matrix0_get_ncol

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

overload [] with matrix0_get_at_int of 0
overload [] with matrix0_get_at_size of 0
overload [] with matrix0_set_at_int of 0
overload [] with matrix0_set_at_size of 0

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

overload print with print_matrix0
overload prerr with print_matrix0
overload fprint with fprint_matrix0
overload fprint with fprint_matrix0_sep

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

(* end of [matrix0.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2016 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: gmmhwxiATgmailDOTcom *)
(* Start time: October, 2016 *)

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

(* ****** ****** *)
//
fun
{a:t0p}
stream2list0
  (xs: stream(a)):<!laz> list0(a)
//
(* ****** ****** *)
//
fun
{a:t0p}
stream_make_list0
  (xs: list0(a)):<!laz> stream(a)
//
(* ****** ****** *)
//
fun
{a:t0p}{b:t0p}
stream_map_method
(
  stream(INV(a)), TYPE(b)
) (fopr: (a) -<cloref> b):<!laz> stream(b)
//
overload .map with stream_map_method
//
(* ****** ****** *)
//
fun
{a:t0p}{b:t0p}
stream_imap_method
(
  stream(INV(a)), TYPE(b)
) (fopr: (intGte(0), a) -<cloref> b):<!laz> stream(b)
//
overload .imap with stream_imap_method
//
(* ****** ****** *)
//
fun
{a:t0p}
stream_filter_method
(
  xs: stream(INV(a))
)
(
  pred: (a) -<cloref> bool
) :<!laz> stream(a) // end-of-fun
//
overload .filter with stream_filter_method
//
(* ****** ****** *)
//
fun{
res:t0p}{x:t0p
} stream_scan_method
(
  stream(INV(x)), TYPE(res)
) (res, (res, x) -<cloref> res) :<!laz> stream(res)
//
overload .scan with stream_scan_method
//
(* ****** ****** *)
//
fun
{a:t0p}
stream_foreach_method
  (xs: stream(INV(a)))(fwork: (a) -<cloref1> void): void
//
overload .foreach with stream_foreach_method
//
(* ****** ****** *)
//
fun{
res:vt0p}{a:t0p
} stream_foldleft_method
  (stream(INV(a)), TYPE(res))(res, (res, a) -<cloref1> res): res
//
overload .foldleft with stream_foldleft_method
//
(* ****** ****** *)

(* end of [stream.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2011-2016 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: gmmhwxiATgmailDOTcom *)
(* Start time: October, 2016 *)

(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)
//
staload
"libats/ML/SATS/basis.sats"
//
(* ****** ****** *)
//
fun{
a:vt0p}{b:vt0p
} stream_vt_map_method
(
  stream_vt(INV(a)), TYPE(b)
) :
(
  (&a >> a?!) -<cloptr1> b
) -<lincloptr1> stream_vt(b)
//
overload .map with stream_vt_map_method
//
(* ****** ****** *)
//
fun{a:t0p}
stream_vt_filter_method
(
xs: stream_vt(INV(a))
) : ((&a)-<cloptr1>bool)-<lincloptr1>stream_vt(a)
//
overload .filter with stream_vt_filter_method
//
(* ****** ****** *)
//
fun{a:vt0p}
stream_vt_foreach_method
  (xs: stream_vt(INV(a))) 
: ((&a >> a?!) -<cloptr1> void) -<lincloptr1> void
//
fun{a:vt0p}
stream_vt_rforeach_method
  (xs: stream_vt(INV(a))) 
: ((&a >> a?!) -<cloptr1> void) -<lincloptr1> void
//
overload .foreach with stream_vt_foreach_method
overload .rforeach with stream_vt_rforeach_method
//
(* ****** ****** *)
//
fun{a:vt0p}
stream_vt_iforeach_method
  (xs: stream_vt(INV(a))) 
: ((intGte(0), &a >> a?!) -<cloptr1> void) -<lincloptr1> void
//
overload .iforeach with stream_vt_iforeach_method
//
(* ****** ****** *)
//
fun{
res:vt0p
}{a:vt0p}
stream_vt_foldleft_method
(
  xs: stream_vt(INV(a)), TYPE(res)
) : (res, (res, &a >> a?!) -<cloptr1> res) -<lincloptr1> res
fun{
res:vt0p
}{a:vt0p}
stream_vt_ifoldleft_method
(
  xs: stream_vt(INV(a)), TYPE(res)
) : (res, (intGte(0), res, &a >> a?!) -<cloptr1> res) -<lincloptr1> res
//
overload .foldleft with stream_vt_foldleft_method
overload .ifoldleft with stream_vt_ifoldleft_method
//
(* ****** ****** *)

(* end of [stream_vt.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: January, 2013 *)

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

#define ATS_PACKNAME "ATSLIB.libats.ML"
#define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names

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

staload "libats/ML/SATS/basis.sats"

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

typedef SHR(a:type) = a // for commenting purpose
typedef NSH(a:type) = a // for commenting purpose

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

typedef charlst0 = list0 (char)
typedef stringlst0 = list0 (string)

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

(*
fun fileref_open_opt
  (path: NSH(string), fm: file_mode): option0 (FILEref)
// end of [fileref_open_opt]
*)

(* ****** ****** *)
//
fun
fileref_get_line_charlst(filr: FILEref): charlst0
//
(*
** HX: for handling files of "tiny" size
*)
fun
fileref_get_lines_charlstlst(filr: FILEref): list0(charlst0)
//
(* ****** ****** *)
//
fun
fileref_get_line_string(filr: FILEref): string
//
(*
** HX: for handling files of "tiny" size
*)
fun
fileref_get_lines_stringlst(filr: FILEref): stringlst0
//
(* ****** ****** *)
//
fun{}
streamize_fileref_char(inp: FILEref): stream_vt(char)
//
fun{}
streamize_fileref_line(inp: FILEref): stream_vt(string)
//
(* ****** ****** *)
//
(*
fun{}
fileref_get_word$isalpha(c0: charNZ): bool
*)
fun{}
streamize_fileref_word(inp: FILEref): stream_vt(string)
//
(* ****** ****** *)
//
fun
dirname_get_fnamelst(dirname: string): list0(string)
//
(* ****** ****** *)
//
fun{}
streamize_dirname_fname(dirname: string): stream_vt(string)
//
(* ****** ****** *)

(* end of [filebas.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2014 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: September, 2014 *)

(* ****** ****** *)
//
// HX-2013-04:
// intrange (l, r) is for integers i satisfying l <= i < r
//
(* ****** ****** *)
//
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

(* ****** ****** *)
//
fun{}
int_repeat_lazy
  (n: int, f: lazy(void)): void
fun{}
int_repeat_cloref
  (n: int, f: cfun0(void)): void
fun{}
int_repeat_method
  (n: int)(f: cfun0(void)): void
//
overload repeat with int_repeat_lazy
overload repeat with int_repeat_cloref
overload .repeat with int_repeat_method
//
(* ****** ****** *)
//
fun{}
int_forall_cloref
  (n: int, f: cfun1 (int, bool)): bool
fun{}
int_forall_method
  (n: int) (f: cfun1 (int, bool)): bool
//
overload .forall with int_forall_method
//
(* ****** ****** *)
//
fun{}
int_foreach_cloref
  (n: int, f: cfun1 (int, void)): void
fun{}
int_foreach_method
  (n: int) (f: cfun1 (int, void)): void
//
overload .foreach with int_foreach_method
//
(* ****** ****** *)
//
fun{res:vt0p}
int_foldleft_cloref
  (n: int, ini: res, f: cfun2 (res, int, res)): res
//
fun{res:vt0p}
int_foldleft_method
  (int, TYPE(res))(ini: res, f: cfun2 (res, int, res)): res
//
overload .foldleft with int_foldleft_method
//
(* ****** ****** *)
//
fun{}
intrange_forall_cloref
  (l: int, r: int, f: cfun1 (int, bool)): bool
fun{}
intrange_forall_method
  (lr: @(int, int)) (f: cfun1 (int, bool)): bool
//
overload .forall with intrange_forall_method
//
(* ****** ****** *)
//
fun{}
intrange_foreach_cloref
  (l: int, r: int, f: cfun1 (int, void)): void
fun{}
intrange_foreach_method
  (lr: @(int, int)) (f: cfun1 (int, void)): void
//
overload .foreach with intrange_foreach_method
//
(* ****** ****** *)
//
fun{res:vt0p}
intrange_foldleft_cloref
  (l: int, r: int, ini: res, f: cfun2 (res, int, res)): res
//
fun{res:vt0p}
intrange_foldleft_method
  ((int, int), TYPE(res))(ini: res, f: cfun2 (res, int, res)): res
//
overload .foldleft with intrange_foldleft_method
//
(* ****** ****** *)
//
fun{}
int_streamGte(n: int): stream(int)
//
overload .streamGte with int_streamGte
//
fun{}
int_streamGte_vt(n: int): stream_vt(int)
//
overload .streamGte_vt with int_streamGte_vt
//
(* ****** ****** *)
//
fun{a:t0p}
int_list0_map_cloref
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): list0(a)
fun{a:t0p}
int_list0_map_method
  {n:nat}
  (n: int(n), TYPE(a))(f: cfun(natLt(n), a)): list0(a)
//
overload .list0_map with int_list0_map_method
//
(* ****** ****** *)
//
fun{a:t0p}
int_array0_map_cloref
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): array0(a)
fun{a:t0p}
int_array0_map_method
  {n:nat}
  (n: int(n), TYPE(a))(f: cfun(natLt(n), a)): array0(a)
//
overload .array0_map with int_array0_map_method
//
(* ****** ****** *)
//
fun{a:t0p}
int_stream_map_cloref
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): stream(a)
fun{a:t0p}
int_stream_map_method
  {n:nat}
  (n: int(n), TYPE(a))(f: cfun(natLt(n), a)): stream(a)
//
overload .stream_map with int_stream_map_method
//
(* ****** ****** *)
//
fun{a:vt0p}
int_stream_vt_map_cloref
  {n:nat}
  (n: int(n), fopr: cfun(natLt(n), a)): stream_vt(a)
fun{a:vt0p}
int_stream_vt_map_method
  {n:nat}
  (n: int(n), TYPE(a))(f: cfun(natLt(n), a)): stream_vt(a)
//
overload .stream_vt_map with int_stream_vt_map_method
//
(* ****** ****** *)
//
fun{}
int2_foreach_cloref
  (n1: int, n2: int, f: cfun2(int, int, void)): void
//
fun{}
intrange2_foreach_cloref
  (l1: int, r1: int, l2: int, r2: int, f: cfun2(int, int, void)): void
//
(* ****** ****** *)

(* end of [intrange.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: August, 2013 *)

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

#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names

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

staload "libats/ML/SATS/basis.sats"

(* ****** ****** *)
//
// HX: for maps of elements of type (a)
//
abstype
map_type
(
  key:t@ype
, itm:t0ype+
) = ptr(*boxed*)
//
typedef
map(key:t0p, itm:t0p) = map_type(key, itm)
//
(* ****** ****** *)
//
fun{key:t0p}
compare_key_key(x1: key, x2: key):<> int
//
(* ****** ****** *)
//
fun{}
funmap_nil{key,itm:t0p}():<> map(key, itm)
fun{}
funmap_make_nil{key,itm:t0p}():<> map(key, itm)
//
(* ****** ****** *)

fun{}
funmap_is_nil
  {key,itm:t0p}(map: map(key, INV(itm))):<> bool
fun{}
funmap_isnot_nil
  {key,itm:t0p}(map: map(key, INV(itm))):<> bool

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

fun{
key,itm:t0p
} funmap_size(map: map(key, INV(itm))):<> size_t

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

fun{
key,itm:t0p
} funmap_search
  (map: map(key, INV(itm)), k: key): Option_vt(itm)
// end of [funmap_search]

(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_insert
(
  &map(key, INV(itm)) >> _, key, itm
) : Option_vt(itm) // end of [funmap_insert]
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_takeout
(
  map: &map(key, INV(itm)) >> _, k: key
) : Option_vt(itm) // end of [funmap_takeout]
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_remove
  (map: &map(key, INV(itm)) >> _, k: key): bool
//
(* ****** ****** *)
//
fun{
key,itm:t@ype
} fprint_funmap
(
  out: FILEref, map: map(key, itm)
) : void // end of [fprint_funmap]
//
fun{}
fprint_funmap$sep(out: FILEref): void // fprint("; ")
fun{}
fprint_funmap$mapto(out: FILEref): void // fprint("->")
//
overload fprint with fprint_funmap
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_foreach
  (map: map(key, itm)): void
fun
{key:t0p
;itm:t0p}
{env:vt0p}
funmap_foreach_env
  (map: map(key, itm), env: &(env) >> _): void
//
fun
{key:t0p
;itm:t0p}
{env:vt0p}
funmap_foreach$fwork
  (key: key, itm: &itm >> _, env: &(env) >> _): void
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_foreach_cloref
(
  map: map(key, itm)
, fwork: (key, itm) -<cloref1> void
) : void // end-of-function
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_listize
  (map: map(key, INV(itm))): list0 @(key, itm)
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} funmap_streamize
  (map: map(key, INV(itm))): stream_vt @(key, itm)
//
(* ****** ****** *)

typedef
map_modtype
(
  key: t0p, itm: t0p
) = $rec{
//
nil = () -<> map(key,itm)
,
size = $d2ctype(funmap_size<key,itm>)
,
is_nil = (map(key,itm)) -<> bool
,
isnot_nil = (map(key,itm)) -<> bool
,
search = $d2ctype(funmap_search<key,itm>)
,
insert = $d2ctype(funmap_insert<key,itm>)
,
remove = $d2ctype(funmap_remove<key,itm>)
,
takeout = $d2ctype(funmap_takeout<key,itm>)
,
listize = $d2ctype(funmap_listize<key,itm>)
,
streamiize = $d2ctype(funmap_streamize<key,itm>)
//
} (* end of [set_modtype] *)

(* ****** ****** *)
//
fun
{key:t0p
;itm:t0p}
funmap_make_module((*void*)): map_modtype(key,itm)
//
(* ****** ****** *)

(* end of [funmap.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: August, 2013 *)

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

#define ATS_PACKNAME "ATSLIB.libats.ML"
#define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names

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

staload "libats/ML/SATS/basis.sats"

(* ****** ****** *)
//
// HX-2013-08:
// for sets of elements of type a
//
abstype
set_type
(
  a:t@ype+
) = ptr(*boxed*)
//
typedef set(a:t0p) = set_type(a)
//
(* ****** ****** *)

fun{a:t0p}
compare_elt_elt(x: a, y: a):<> int

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

fun{} funset_nil{a:t0p}():<> set(a)
fun{} funset_make_nil{a:t0p}():<> set(a)

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

fun{a:t0p} funset_sing(x: a): set(a)
fun{a:t0p} funset_make_sing(x: a): set(a)

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

fun{a:t0p}
funset_make_list(xs: list0(INV(a))): set(a)

(* ****** ****** *)
//
fun
{a:t0p}
fprint_funset
(
  out: FILEref, set: set(INV(a))
) : void // end of [fprint_funset]
//
fun{}
fprint_funset$sep(out: FILEref): void // fprint(", ")
//
overload fprint with fprint_funset
//
(* ****** ****** *)

fun{}
funset_is_nil{a:t0p}(xs: set(INV(a))):<> bool
fun{}
funset_isnot_nil{a:t0p}(xs: set(INV(a))):<> bool

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

fun{a:t0p}
funset_size(xs: set(INV(a))):<> size_t

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

fun{a:t0p}
funset_is_member(xs: set(INV(a)), x0: a):<> bool
fun{a:t0p}
funset_isnot_member(xs: set(INV(a)), x0: a):<> bool

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

fun{a:t0p}
funset_insert
  (xs: &set(INV(a)) >> _, x0: a): bool(*[x0] in [xs]*)
// end of [funset_insert]

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

fun{a:t0p}
funset_remove
  (xs: &set(INV(a)) >> _, x0: a): bool(*[x0] in [xs]*)
// end of [funset_remove]

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

fun{a:t0p}
funset_getmax_opt(xs: set(INV(a))): Option_vt(a)
fun{a:t0p}
funset_getmin_opt(xs: set(INV(a))): Option_vt(a)

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

fun{a:t0p}
funset_takeoutmax_opt(xs: &set(INV(a)) >> _): Option_vt(a)
fun{a:t0p}
funset_takeoutmin_opt(xs: &set(INV(a)) >> _): Option_vt(a)

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

fun{a:t0p}
funset_union(xs1: set(INV(a)), xs2: set(a)):<> set(a)
fun{a:t0p}
funset_intersect(xs1: set(INV(a)), xs2: set(a)):<> set(a)
fun{a:t0p}
funset_differ(xs1: set(INV(a)), xs2: set(a)):<> set(a)
fun{a:t0p}
funset_symdiff(xs1: set(INV(a)), xs2: set(a)):<> set(a)

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

fun{a:t0p}
funset_equal(xs1: set(INV(a)), xs2: set(a)):<> bool

(* ****** ****** *)
//
// HX: set ordering induced by the ordering on elements
//
fun{a:t0p}
funset_compare(xs1: set(INV(a)), xs2: set(a)):<> int

(* ****** ****** *)
//
fun{a:t0p}
funset_is_subset(xs1: set(INV(a)), xs2: set(a)):<> bool
fun{a:t0p}
funset_is_supset(xs1: set(INV(a)), xs2: set(a)):<> bool
//
(* ****** ****** *)
//
fun{a:t0p}
funset_foreach(set: set(INV(a))): void
fun
{a:t0p}
{env:vt0p}
funset_foreach_env
  (set: set(INV(a)), env: &(env) >> _): void
// end of [funset_foreach_env]
//
fun
{a:t0p}
{env:vt0p}
funset_foreach$fwork(x: a, env: &(env) >> _): void
//
(* ****** ****** *)
//
fun{a:t0p}
funset_foreach_cloref
  (set: set(INV(a)), fwork: (a) -<cloref1> void): void
//
(* ****** ****** *)
//
fun{a:t0p}
funset_tabulate_cloref
  {n:nat}(int(n), fopr: (natLt(n)) -<cloref1> a): set(a)
//
(* ****** ****** *)
//
fun{a:t0p}
funset_listize(xs: set(INV(a))):<> list0(a)
//
fun{a:t0p}
funset_streamize(xs: set(INV(a))):<> stream_vt(a)
//
(* ****** ****** *)

typedef
set_modtype
(
  elt:t@ype
) = $rec{
//
nil = () -<> set(elt)
,
sing =
$d2ctype(funset_sing<elt>)
,
make_list =
$d2ctype(funset_make_list<elt>)
,
size = $d2ctype(funset_size<elt>)
,
is_nil = (set(elt)) -<> bool
,
isnot_nil = (set(elt)) -<> bool
,
insert = $d2ctype(funset_insert<elt>)
,
remove = $d2ctype(funset_remove<elt>)
,
union = $d2ctype(funset_union<elt>)
,
intersect = $d2ctype(funset_intersect<elt>)
,
listize = $d2ctype(funset_listize<elt>)
,
streamiize = $d2ctype(funset_streamize<elt>)
//
} (* end of [set_modtype] *)

(* ****** ****** *)
//
fun
{a:t@ype}
funset_make_module((*void*)): set_modtype(a)
//
(* ****** ****** *)

(* end of [funset.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: August, 2013 *)

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

#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names

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

staload "libats/ML/SATS/basis.sats"

(* ****** ****** *)
//
typedef
hashtbl // introduced in [basis.sats]
(key:t@ype, itm:t@ype) = hashtbl(key, itm)
//
(* ****** ****** *)
//
fun{
key:t0p
} hash_key(x: key):<> ulint
//
fun{
key:t0p
} equal_key_key(x1: key, x2: key):<> bool
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} hashtbl_make_nil
  (cap: sizeGte(1)): hashtbl(key, itm)
//
(* ****** ****** *)

fun{}
hashtbl_get_size
  {key,itm:t0p}(hashtbl(key, itm)): size_t
fun{}
hashtbl_get_capacity
  {key,itm:t0p}(hashtbl(key, itm)): sizeGte(1)

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

fun{
key,itm:t0p
} hashtbl_search
  (hashtbl(key, itm), key): Option_vt(itm)
// end of [hashtbl_search]

fun{
key,itm:t0p
} hashtbl_search_ref
  (tbl: hashtbl(key, itm), k: key): cPtr0(itm)
// end of [hashtbl_search_ref]

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

fun{
key,itm:t0p
} hashtbl_insert
  (hashtbl(key, itm), key, itm): Option_vt(itm)
// end of [hashtbl_insert]

fun{
key,itm:t0p
} hashtbl_insert_any(hashtbl(key, itm), key, itm): void

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

fun{
key,itm:t0p
} hashtbl_takeout
  (kxs: hashtbl(key, itm), k0: key): Option_vt(itm)
// end of [hashtbl_takeout]

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

fun{
key,itm:t0p
} hashtbl_remove
  (kxs: hashtbl(key, itm), key): bool

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

fun{
key,itm:t0p
} hashtbl_takeout_all
  (kxs: hashtbl(key, itm)): list0 @(key, itm)
// end of [hashtbl_takeout_all]

(* ****** ****** *)
//
fun{
key,itm:t@ype
} fprint_hashtbl
  (out: FILEref, tbl: hashtbl(key, itm)): void
//
overload fprint with fprint_hashtbl
//
fun{}
fprint_hashtbl$sep (out: FILEref): void // default: fprint("; ")
fun{}
fprint_hashtbl$mapto (out: FILEref): void // default: fprint("->")
//
(* ****** ****** *)
//
fun{
key,itm:t@ype
} fprint_hashtbl_sep_mapto
(
  out: FILEref, tbl: hashtbl(key, itm), sep: string, mapto: string
) : void // end of [fprint_hashtbl_sep_mapto]
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} hashtbl_foreach
  (tbl: hashtbl(key, itm)): void
fun
{key:t0p
;itm:t0p}
{env:vt0p}
hashtbl_foreach_env
  (tbl: hashtbl(key, itm), env: &(env) >> _): void
//
fun
{key:t0p
;itm:t0p}
{env:vt0p}
hashtbl_foreach$fwork
  (key: key, itm: &itm >> _, env: &(env) >> _): void
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} hashtbl_foreach_cloref
(
  tbl: hashtbl(key, itm), fwork: (key, &itm >> _) -<cloref1> void
) : void // end of [hashtbl_foreach_cloref]
//
(* ****** ****** *)
//
fun{
key,itm:t0p
} hashtbl_listize1(hashtbl(key, itm)): list0 @(key, itm)
//
(* ****** ****** *)

(* end of [hashtblref.sats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: June, 2012 *)

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

#define ATS_DYNLOADFLAG 0
  
(* ****** ****** *)
  
staload
UN = "prelude/SATS/unsafe.sats"

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

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_make_sing (x) =
  list0_cons{a}(x, list0_nil)
implement
{a}(*tmp*)
list0_make_pair (x1, x2) =
  list0_cons{a}(x1, list0_cons{a}(x2, list0_nil))
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_make_elt
  (n, x) = let
//
val n = g1ofg0(n)
//
in
//
if
n >= 0
then let
  val xs =
    $effmask_wrt(list_make_elt<a>(n, x))
  // end of [val]
in
  list0_of_list_vt{a}(xs)
end // end of [then]
else let
in
  $raise (IllegalArgExn"list0_make_elt:n")
end // end of [else]
//
end // end of [list0_make_elt]

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

implement
{}(*tmp*)
list0_make_intrange_lr
  (l, r) = let
  val d = (
    if l <= r then 1 else ~1
  ) : int // end of [val]
in
  $effmask_exn(list0_make_intrange_lrd(l, r, d))
end // end of [list0_make_intrange_lr]

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

implement
{}(*tmp*)
list0_make_intrange_lrd
  (l, r, d) = let
//
typedef res = list0 (int)
//
fun loop1 // d > 0
(
  l: int, r: int
, d: int, res: &ptr? >> res
) : void = let
in
//
if l < r then let
  val () =
  (
    res := list0_cons{int}(l, _)
  )
  val+list0_cons (_, res1) = res
  val () = loop1 (l+d, r, d, res1)
  prval () = fold@ (res)
in
  // nothing
end else (res := list0_nil)
//
end // end of [loop1]
//
fun loop2 // d < 0
(
  l: int, r: int
, d: int, res: &ptr? >> res
) : void = let
in
//
if l > r then let
  val () =
  (
    res := list0_cons{int}(l, _)
  )
  val+ list0_cons (_, res1) = res
  val () = loop2 (l+d, r, d, res1)
  prval () = fold@ (res)
in
  // nothing
end else (res := list0_nil)
//
end // end of [loop2]
//
in
//
$effmask_all
(
if d > 0 then (
  if l < r then let
    var res: ptr? // uninitialized
    val () = loop1 (l, r, d, res) in res
  end else list0_nil ()
) else if d < 0 then (
  if l > r then let
    var res: ptr? // uninitialized
    val () = loop2 (l, r, d, res) in res
  end else list0_nil ()
) else (
  $raise
  IllegalArgExn("list0_make_intrange_lrd:d")
) // end of [if]
) (* end of [$effmask_all] *)
//
end // end of [list0_make_intrange_lrd]

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_make_arrpsz
  (psz) =
  list0_of_list_vt{a}(list_make_arrpsz(psz))
// end of [list0_make_arrpsz]
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
print_list0
  (xs) = fprint_list0<a> (stdout_ref, xs)
implement
{a}(*tmp*)
prerr_list0
  (xs) = fprint_list0<a> (stderr_ref, xs)
//
implement
{a}(*tmp*)
fprint_list0
  (out, xs) = fprint_list<a> (out, g1ofg0(xs))
//
implement
{a}(*tmp*)
fprint_list0_sep
  (out, xs, sep) =
(
  fprint_list_sep<a> (out, g1ofg0(xs), sep)
) (* end of [fprint_list0_sep] *)
//
implement
{a}(*tmp*)
fprint_listlist0_sep
  (out, xss, sep1, sep2) =
(
  fprint_listlist_sep<a>
    (out, $UN.cast{List(List(a))}(xss), sep1, sep2)
) (* end of [fprint_listlist0_sep] *)
//
(* ****** ****** *)
//
(*
//
// HX: these have been declared as macros:
//
implement
{a}(*tmp*)
list0_sing (x) = list0_cons{a}(x, list0_nil)
implement
{a}(*tmp*)
list0_pair (x1, x2) =
  list0_cons{a}(x1, list0_cons{a}(x2, list0_nil))
//
*)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_is_nil(xs) = (
//
case+ xs of
| list0_cons _ => false | list0_nil() => true
//
) (* end of [list0_is_nil] *)

implement
{a}(*tmp*)
list0_is_cons(xs) = (
//
case+ xs of
| list0_cons _ => true | list0_nil() => false
//
) (* end of [list0_is_cons] *)

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_is_empty(xs) = list0_is_nil<a> (xs)
//
implement
{a}(*tmp*)
list0_isnot_empty(xs) = list0_is_cons<a> (xs)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_head_exn
  (xs) = let
in
//
case+ xs of
| list0_cons
    (x, _) => (x)
  // list0_cons
| list0_nil _ =>
    $raise ListSubscriptExn()
  // list0_nil
end // end of [list0_head_exn]

implement
{a}(*tmp*)
list0_head_opt
  (xs) = let
in
//
case+ xs of
| list0_nil() => None_vt()
| list0_cons(x, _) => Some_vt{a}(x)
//
end // end of [list0_head_opt]

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

implement
{a}(*tmp*)
list0_tail_exn
  (xs) = let
in
//
case+ xs of
| list0_cons
    (_, xs) => (xs)
  // list0_cons
| list0_nil _ =>
    $raise ListSubscriptExn()
  // list0_nil
//
end // end of [list0_tail_exn]

implement
{a}(*tmp*)
list0_tail_opt
  (xs) = let
in
//
case+ xs of
| list0_nil() => None_vt()
| list0_cons(_, xs) => Some_vt{list0(a)}(xs)
//
end // end of [list0_tail_opt]

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

implement
{a}(*tmp*)
list0_last_exn
  (xs) = let
//
val xs = g1ofg0_list(xs)
//
in
//
case+ xs of
| list_cons _ => list_last<a>(xs)
| list_nil () => $raise ListSubscriptExn()
//
end // end of [list0_last_exn]

implement
{a}(*tmp*)
list0_last_opt
  (xs) = let
//
val xs = g1ofg0_list(xs)
//
in
//
case+ xs of
| list_nil() => None_vt()
| list_cons _ => Some_vt{a}(list_last(xs))
//
end // end of [list0_last_opt]

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

implement
{a}(*tmp*)
list0_init_exn
  (xs) = let
//
fun
aux
{n:nat} .<n>.
(
  x0: a, xs: list(a, n)
) :<> list(a, n) =
(
case+ xs of
| list_nil() =>
  list_nil()
| list_cons(x, xs) =>
  list_cons(x0, aux(x, xs))
)
//
in
  case+ xs of
  | list0_cons
      (x, xs) =>
    (
      g0ofg1(aux(x, g1ofg0(xs)))
    ) (* end of [list0_cons] *)
  | list0_nil() => $raise ListSubscriptExn()
end // end of [list0_init_exn]

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

implement
{a}(*tmp*)
list0_init_opt
  (xs) = let
//
fun
aux
{n:nat} .<n>.
(
  x0: a, xs: list(a, n)
) :<> list(a, n) =
(
case+ xs of
| list_nil() =>
  list_nil()
| list_cons(x, xs) =>
  list_cons(x0, aux(x, xs))
)
//
in
//
case+ xs of
| list0_nil() =>
  None_vt(*void*)
| list0_cons(x, xs) =>
  Some_vt(g0ofg1(aux(x, g1ofg0(xs))))
//
end // end of [list0_init_opt]

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_nth_exn
  (xs, i0) = let
//
fun
loop
{i:nat} .<i>.
(
  xs: list0(a), i: int i
) :<!exn> (a) =
(
//
case+ xs of
| list0_cons
    (x, xs) =>
  (
    if i > 0 then loop(xs, i-1) else x
  ) // end of [list0_cons]
| list0_nil() => $raise ListSubscriptExn()
//
) (* end of [loop] *)
//
val i0 = g1ofg0_int(i0)
//
in
//
if i0 >= 0
  then loop(xs, i0) else $raise ListSubscriptExn()
// end of [if]
//
end // end of [list0_nth_exn]
//
implement
{a}(*tmp*)
list0_nth_opt
(
  xs, i0
) =
$effmask_exn
(
try
Some_vt{a}
(
  list0_nth_exn<a>(xs, i0)
)
with ~ListSubscriptExn((*void*)) => None_vt()
) (* $effmask_exn *)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_get_at_exn
  (xs, i0) = list0_nth_exn (xs, i0)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_fset_at_exn
  (xs, i0, x0) = let
//
fun
loop
{i:nat} .<i>.
(
  xs: list0(a), i: int i
) :<!exn> list0(a) =
(
//
case+ xs of
| list0_cons
    (x, xs) =>
  (
    if i > 0
      then cons0(x, loop(xs, i-1)) else cons0(x0, xs)
    // end of [if]
  ) // end of [list0_cons]
| list0_nil() => $raise ListSubscriptExn()
//
) (* end of [loop] *)
//
val i0 = g1ofg0(i0)
//
in
//
if i0 >= 0
  then loop(xs, i0) else $raise ListSubscriptExn()
//
end // end of [list0_fset_at_exn]
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_fset_at_opt
(
  xs, i0, x0
) =
$effmask_exn
(
try
Some_vt{list0(a)}
(
  list0_fset_at_exn<a>(xs, i0, x0)
)
with ~ListSubscriptExn((*void*)) => None_vt()
) (* $effmask_exn *)

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

implement
{a}(*tmp*)
list0_insert_at_exn
  (xs, i, x0) = let
//
fun
aux {i:nat} .<i>.
(
  xs: list0 a, i: int i, x0: a
) :<!exn> list0 a = let
in
//
if
i > 0
then (
//
case+ xs of
| list0_cons
    (x, xs) =>
  (
    list0_cons{a}(x, aux (xs, i-1, x0))
  )
| list0_nil() => $raise ListSubscriptExn()
//
) else (
  list0_cons{a}(x0, xs)
) (* end of [if] *)
//
end // end of [aux]
//
val i = g1ofg0_int(i)
//
in
//
if
i >= 0
then aux (xs, i, x0)
else $raise IllegalArgExn("list0_insert_at_exn:i")
//
end // end of [list0_insert_at_exn]

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

local

fun{
a:t0p
} auxlst {i:nat} .<i>.
(
  xs: list0 (a), i: int i, x0: &a? >> a
) :<!exnwrt> list0 a = let
//
extern praxi __assert : (&a? >> a) -<prf> void
//
in
//
case+ xs of
| list0_cons
    (x, xs) => let
  in
    if i > 0 then
      list0_cons{a}(x, auxlst<a> (xs, i-1, x0))
    else let
      val () = x0 := x in xs
    end (* end of [if] *)
  end // end of [list0_cons]
| list0_nil () => let
    prval () = __assert (x0) in $raise ListSubscriptExn()
  end // end of [list0_nil]
//
end // end of [auxlst]

in (* in of [local] *)

implement
{a}(*tmp*)
list0_remove_at_exn
  (xs, i) = let
//
var x0: a?
val i = g1ofg0_int (i)
//
in
$effmask_wrt
(
if
i >= 0
then
  auxlst<a> (xs, i, x0)
else (
  $raise
  IllegalArgExn("list0_remove_at_exn:i")
) (* end of [else] *)
)
end // end of [list0_remove_at_exn]

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

implement
{a}(*tmp*)
list0_takeout_at_exn
  (xs, i, x0) = let
//
val i = g1ofg0_int (i)
//
extern
praxi __assert : (&a? >> a) -<prf> void
//
in
//
if i >= 0 then
  auxlst<a> (xs, i, x0)
else let
  prval () = __assert (x0)
in
  $raise IllegalArgExn("list0_takeout_at_exn:i")
end // end of [if]
//
end // end of [list0_takeout_at_exn]

end // end of [local]

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_length
  (xs) =
  list_length<a>(g1ofg0(xs))
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_append
  (xs, ys) = let
  val xs = g1ofg0(xs)
  and ys = g1ofg0(ys)
in
//
list0_of_list(list_append<a>(xs, ys))
//
end // end of [list0_append]

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

implement
{a}(*tmp*)
list0_extend
  (xs, x) = let
//
val xs = g1ofg0(xs)
//
in
//
$effmask_wrt
(
list0_of_list_vt(list_extend<a>(xs, x))
) (* $effmask_wrt *)
//
end // end of [list0_extend]

(* ****** ****** *)
//
implement
{a}(*tmp*)
mul_int_list0
  (m, xs) =
$effmask_wrt
(
list0_of_list_vt
  (mul_int_list<a>(m, g1ofg0(xs)))
) (* end of [mul_int_list0] *)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_reverse(xs) =
  list0_reverse_append<a>(xs, list0_nil)
// end of [list0_reverse]

implement
{a}(*tmp*)
list0_reverse_append
  (xs, ys) = let
  val xs = g1ofg0(xs)
  and ys = g1ofg0(ys)
in
  list0_of_list(list_reverse_append<a>(xs, ys))
end // end of [list0_reverse_append]

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

implement
{a}(*tmp*)
list0_concat
  (xss) = let
//
typedef xss = List(List(a))
//
in
//
$effmask_wrt
(
list0_of_list_vt{a}
  (list_concat<a>($UN.cast{xss}(xss)))
) (* $effmask_wrt *)
end // end of [list0_concat]

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

implement
{a}(*tmp*)
list0_take_exn
  (xs, i) = let
//
val i = g1ofg0_int (i)
val xs = g1ofg0_list (xs)
//
in
  if i >= 0 then let
    val res =
      $effmask_wrt (list_take_exn<a>(xs, i))
    // end of [val]
  in
    list0_of_list_vt (res)
  end else
    $raise (IllegalArgExn"list0_take_exn:i")
  // end of [if]
end // end of [list0_take_exn]

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

implement
{a}(*tmp*)
list0_drop_exn
  (xs, i) = let
//
val i = g1ofg0_int (i)
val xs = g1ofg0_list (xs)
//
in
  if i >= 0 then
    list0_of_list (list_drop_exn<a>(xs, i))
  else
    $raise (IllegalArgExn"list0_drop_exn:i")
  // end of [if]
end // end of [list0_drop_exn]

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_app
  (xs, fopr) = list0_foreach<a>(xs, fopr)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_foreach
(
  xs, fwork
) = loop(xs) where
{
//
fun
loop(xs: list0(a)): void =
(
  case+ xs of
  | list0_nil() => ()
  | list0_cons(x, xs) => (fwork(x); loop(xs))
)
//
} (* end of [list0_foreach] *)
//
implement
{a}(*tmp*)
list0_foreach_method
  (xs) = lam(fwork) => list0_foreach<a>(xs, fwork)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_rforeach
(
  xs, fwork
) = aux0(xs) where
{
//
fun
aux0(xs: list0(a)): void =
(
  case+ xs of
  | list0_nil() => ()
  | list0_cons(x, xs) => (aux0(xs); fwork(x))
)
//
} (* end of [list0_rforeach] *)
//
implement
{a}(*tmp*)
list0_rforeach_method
  (xs) = lam(fwork) => list0_rforeach<a>(xs, fwork)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_iforeach
  (xs, fwork) = let
//
fun
loop
(
  i0: intGte(0), xs: list0(a)
) : intGte(0) =
(
  case+ xs of
  | list0_nil() => i0
  | list0_cons(x, xs) =>
      (fwork(i0, x); loop (i0+1, xs))
    // end of [list0_cons]
) (* end of [loop] *)
//
in
  loop (0, xs)
end // end of [list0_iforeach]
//
implement
{a}(*tmp*)
list0_iforeach_method
  (xs) =
  lam(fwork) => list0_iforeach<a>(xs, fwork)
//
(* ****** ****** *)

implement
{a1,a2}
list0_foreach2
  (xs1, xs2, fwork) = let
  var sgn: int // uninitialized
in
  list0_foreach2_eq (xs1, xs2, fwork, sgn)
end // end of [list0_foreach2]

implement
{a1,a2}
list0_foreach2_eq
(
  xs1, xs2, fwork, sgn
) = loop(xs1, xs2, sgn) where
{
//
fun
loop
(
  xs1: list0(a1)
, xs2: list0(a2)
, sgn: &int? >> int
) : void =
(
  case+ xs1 of
  | list0_nil() => (
    case+ xs2 of
    | list0_nil() => (sgn := 0)
    | list0_cons _ => (sgn := ~1)
    )
  | list0_cons(x1, xs1) => (
    case+ xs2 of
    | list0_nil () => (sgn := 1)
    | list0_cons(x2, xs2) =>
        (fwork(x1, x2); loop(xs1, xs2, sgn))
    )
)
//
} (* end of [list0_foreach2_eq] *)

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

implement
{res}{a}
list0_foldleft
  (xs, ini, fopr) = let
//
fun
loop
(
  xs: list0(a), res: res
) : res =
(
  case+ xs of
  | list0_nil () => res
  | list0_cons(x, xs) => loop(xs, fopr(res, x))
)
in
  loop(xs, ini)
end // end of [list0_foldleft]
//
implement
{res}{a}
list0_foldleft_method(xs, _) =
  lam(ini, fopr) =>list0_foldleft<res><a>(xs, ini, fopr)
//
(* ****** ****** *)

implement
{res}{a}
list0_ifoldleft
  (xs, ini, fopr) = let
//
fun
loop
(
  i: int, xs: list0 (a), res: res
) : res =
(
  case+ xs of
  | list0_nil () => res
  | list0_cons(x, xs) => loop(i+1, xs, fopr(res, i, x))
) (* end of [loop] *)
in
  loop (0, xs, ini)
end // end of [list0_ifoldleft]
//
implement
{res}{a}
list0_ifoldleft_method(xs, _) =
(
  lam(ini, fopr) =>
    list0_ifoldleft<res><a>(xs, ini, fopr)
  // end of [lam
)
//
(* ****** ****** *)

implement
{res}{a1,a2}
list0_foldleft2
(
  xs1, xs2, ini, fopr
) = loop(xs1, xs2, ini) where
{
//
fun
loop
(
  xs1: list0(a1)
, xs2: list0(a2), res: res
) : res =
(
  case+ xs1 of
  | list0_nil() => res
  | list0_cons(x1, xs1) => (
    case+ xs2 of
    | list0_nil() => res
    | list0_cons (x2, xs2) =>
      (
        loop(xs1, xs2, fopr(res, x1, x2))
      ) // end of [list0_cons]
    )
) (* end of [loop] *)
//
} (* end of [list0_foldleft2] *)

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

implement
{a}{res}
list0_foldright
(
  xs, fopr, snk
) = loop(xs) where
{
//
fun
loop(xs: list0(a)): res =
  case+ xs of
  | list0_nil() => snk
  | list0_cons (x, xs) => fopr(x, loop(xs))
//
} (* end of [list0_foldright] *)
//
implement
{a}{res}
list0_foldright_method(xs, _) =
  lam(f, snk) => list0_foldright<a><res>(xs, f, snk)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_exists
(
  xs, pred
) = loop(xs) where
{
//
fun
loop(xs: list0(a)): bool =
(
case+ xs of
| list0_nil() => false
| list0_cons (x, xs) =>
    if pred(x) then true else loop(xs)
  // list0_cons
) (* end of [loop] *)
//
} (* end of [list0_exists] *)
//
implement
{a}(*tmp*)
list0_exists_method(xs) =
  lam(p) => list0_exists<a>(xs, p)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_iexists
(
  xs, pred
) = loop(0, xs) where
{
//
fun
loop(i: intGte(0), xs: list0(a)): bool =
(
  case+ xs of
  | list0_nil() => false
  | list0_cons(x, xs) =>
      if pred(i, x) then true else loop(i+1, xs)
    // list0_cons
) (* end of [loop] *)
//
} (* end of [list0_iexists] *)
//
implement
{a}(*tmp*)
list0_iexists_method(xs) =
  lam(p) => list0_iexists<a> (xs, p)
//
(* ****** ****** *)

implement
{a1,a2}
list0_exists2
(
  xs1, xs2, pred
) = let
//
fun
loop
(
  xs1: list0(a1)
, xs2: list0(a2)
) : bool =
(
  case+ xs1 of
  | list0_nil() => false
  | list0_cons(x1, xs1) => (
    case+ xs2 of
    | list0_nil() => false
    | list0_cons(x2, xs2) =>
        if pred(x1, x2) then true else loop(xs1, xs2)
      // end of [list_cons]
    )
) (* end of [loop] *)
//
in
  loop(xs1, xs2)
end // end of [list0_exists2]

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

implement
{a}(*tmp*)
list0_forall
(
  xs, pred
) = loop(xs) where
{
//
fun
loop(xs: list0(a)): bool =
(
  case+ xs of
  | list0_nil() => true
  | list0_cons(x, xs) =>
      if pred(x) then loop(xs) else false
    // list0_cons
) (* end of [loop] *)
//
} (* end of [list0_forall] *)
//
implement
{a}(*tmp*)
list0_forall_method(xs) =
  lam(p) => list0_forall<a> (xs, p)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_iforall
(
  xs, pred
) = loop(0, xs) where
{
//
fun
loop(i: intGte(0), xs: list0(a)): bool =
(
  case+ xs of
  | list0_nil() => true
  | list0_cons(x, xs) =>
      if pred(i, x) then loop(i+1, xs) else false
    // list0_cons
) (* end of [loop] *)
//
} (* end of [list0_iforall] *)
//
implement
{a}(*tmp*)
list0_iforall_method(xs) =
  lam(p) => list0_iforall<a> (xs, p)
//
(* ****** ****** *)

implement
{a1,a2}
list0_forall2
  (xs1, xs2, p) = let
  var sgn: int // uninitialized
in
  list0_forall2_eq (xs1, xs2, p, sgn)
end // end of [list0_forall2]

implement
{a1,a2}
list0_forall2_eq
(
  xs1, xs2, pred, sgn
) = loop(xs1, xs2, sgn) where
{
//
fun
loop
(
  xs1: list0(a1)
, xs2: list0(a2)
, sgn: &int? >> _
) : bool =
(
  case+ xs1 of
  | list0_nil() => (
    case+ xs2 of
    | list0_nil() => (sgn := 0; true)
    | list0_cons _ => (sgn := ~1; true)
    )
  | list0_cons(x1, xs1) => (
    case+ xs2 of
    | list0_nil() => (sgn := 1; true)
    | list0_cons (x2, xs2) =>
      (
        if pred (x1, x2)
          then loop(xs1, xs2, sgn) else (sgn := 0; false)
        // end of [if]
      ) (* end of [list0_cons] *)
    )
)
} (* end of [list0_forall2_eq] *)

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

implement
{a}(*tmp*)
list0_equal
(
  xs1, xs2, eqfn
) = loop(xs1, xs2) where
{
//
fun
loop
(
  xs1: list0(a), xs2: list0(a)
) : bool =
(
  case+ xs1 of
  | list0_nil() => (
    case+ xs2 of
    | list0_nil() => true
    | list0_cons _ => false
    )
  | list0_cons(x1, xs1) => (
    case+ xs2 of
    | list0_nil() => false
    | list0_cons(x2, xs2) =>
        if eqfn (x1, x2) then loop(xs1, xs2) else false
      // end of [list0_cons]
    )
) (* end of [loop] *)
//
} (* end of [list0_equal] *)

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

implement
{a}(*tmp*)
list0_find_exn
(
  xs, pred
) = loop(xs) where
{
//
fun
loop(xs: list0(a)): a =
(
case+ xs of
| list0_nil() =>
    $raise NotFoundExn()
  // list0_nil
| list0_cons(x, xs) =>
    if pred(x) then x else loop(xs)
  // list0_cons
)
//
} (* end of [list0_find_exn] *)

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

implement
{a}(*tmp*)
list0_find_opt
(
  xs, pred
) = loop(xs) where
{
//
fun
loop
(
  xs: list0(a)
) : Option_vt(a) =
//
case+ xs of
| list0_nil() =>
    None_vt(*void*)
  // list0_nil
| list0_cons(x, xs) =>
  (
    if pred(x) then Some_vt{a}(x) else loop(xs)
  ) (* end of [list_cons] *)
//
} (* end of [list0_find_opt] *)

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_find_exn_method
  (xs) = lam(pred) => list0_find_exn<a>(xs, pred)
//
implement
{a}(*tmp*)
list0_find_opt_method
  (xs) = lam(pred) => list0_find_opt<a>(xs, pred)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_find_index
(
  xs, pred
) = loop(xs, 0) where
{
//
fun
loop
(
  xs: list0(a), i: intGte(0)
) : intGte(~1) =
//
case+ xs of
| list0_nil() => (~1)
| list0_cons(x, xs) =>
  (
    if pred(x) then (i) else loop(xs, i+1)
  ) (* end of [list0_cons] *)
//
} (* end of [list0_find_index] *)

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

implement
{a,b}(*tmp*)
list0_assoc_exn
(
  xys, x0, eq
) = loop(xys, x0, eq) where
{
//
fun
loop:
$d2ctype (
list0_assoc_exn<a,b>
) = lam(xys, x0, eq) =>
//
case+ xys of
| list0_nil() => $raise NotFoundExn()
| list0_cons(xy, xys) =>
    if eq (x0, xy.0) then xy.1 else loop(xys, x0, eq)
  // end of [list0_cons]
//
} (* end of [list0_assoc_exn] *)

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

implement
{a,b}(*tmp*)
list0_assoc_opt
(
  xys, x0, eq
) = loop(xys, x0, eq) where
{
fun
loop:
$d2ctype(
list0_assoc_opt<a,b>
) = lam(xys, x0, eq) =>
//
case+ xys of
| list0_nil() =>
    None_vt(*void*)
  // list0_nil
| list0_cons(xy, xys) =>
  (
    if eq (x0, xy.0)
      then Some_vt{b}(xy.1) else loop(xys, x0, eq)
    // end of [if]
  ) (* end of [list_cons] *)
//
} (* end of [list0_assoc_opt] *)

(* ****** ****** *)
//
(*
implement
{a}{b}
list0_map
  (xs, fopr) = let
  viewdef v = unit_v
  viewtypedef fun_vt = cfun (a, b)
  fun app .<>.
    (pfu: !unit_v | x: a, fopr: !fun_vt): b = fopr (x)
  // end of [fun]
  prval pfu = unit_v ()
  var
  fopr = fopr
  val ys =
  list_map_funenv<a><b> {v}{vt} (pfu | g1ofg0(xs), app, fopr)
  prval () = topize(fopr)
  prval unit_v((*void*)) = pfu
in
  list0_of_list_vt (ys)
end // end of [list0_map]
*)
//
implement
{a}{b}
list0_map(xs, fopr) = let
//
implement
{a2}{b2}
list_map$fopr(x) =
$UN.castvwtp0{b2}(fopr($UN.cast{a}(x)))
//
val ys = list_map<a><b>(g1ofg0_list(xs))
//
in
  list0_of_list_vt{b}(ys)
end // end of [list0_map]

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

implement
{a}{b}
list0_mapopt
  (xs, fopr) = res where
{
//
fun loop
(
  xs: list0 (a)
, res: &ptr? >> List0_vt (b)
) : void = let
in
//
case+ xs of
| list0_cons
    (x, xs) =>
  (
  case+ fopr(x) of
  | ~Some_vt y => let
      val () =
      (
      res :=
      list_vt_cons{b}{0}(y, _)
      )
      val+list_vt_cons (_, res1) = res
      val () = loop (xs, res1)
      prval () = fold@ (res)
    in
      // nothing
    end // end of [Some0]
  | ~None_vt () => loop (xs, res)
  ) (* end of [list0_cons] *)
| list0_nil () => (
    res := list_vt_nil ()
  ) (* end of [list0_nil] *)
//
end // end of [loop]
//
var res: ptr
val () = loop (xs, res)
val res = list0_of_list_vt (res)
//
} // end of [list0_mapopt]

(* ****** ****** *)
//
implement
{a}{b}
list0_map_method
  (xs, _) =
  lam(fopr) => list0_map<a><b>(xs, fopr)
implement
{a}{b}
list0_mapopt_method
  (xs, _) =
  lam(fopr) => list0_mapopt<a><b>(xs, fopr)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_mapcons
  (x0, xss) = let
//
implement
list_map$fopr<list0(a)><list0(a)>
  (xs) = list0_cons(x0, xs)
//
val xss = g1ofg0 (xss)
val res = list_map<list0(a)><list0(a)> (xss)
//
in
  list0_of_list_vt (res)
end // end of [list0_mapcons]

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

implement
{a}{b}
list0_imap
  (xs, fopr) = let
//
implement
{a2}{b2}
list_imap$fopr(i, x) =
let
  val x = $UN.cast{a}(x)
in
  $UN.castvwtp0{b2}(fopr(i, x))
end // end of [list_imap$fopr]
//
val ys = list_imap<a><b>(g1ofg0_list(xs))
//
in
  list0_of_list_vt{b}(ys)
end // end of [list0_imap]

(* ****** ****** *)
//
implement
{a}{b}
list0_imap_method
  (xs, _(*TYPE*)) =
  lam(fopr) => list0_imap<a><b>(xs, fopr)
//
(* ****** ****** *)
//
(*
implement
{a1,a2}{b}
list0_map2
  (xs1, xs2, fopr) = let
  viewdef v0 = unit_v
  viewtypedef fun_vt = cfun2 (a1, a2, b)
  val xs1 = g1ofg0_list(xs1)
  val xs2 = g1ofg0_list(xs2)
  fun app .<>.
    (pfu: !v0 | x1: a1, x2: a2, f: !fun_vt): b = fopr(x1, x2)
  // end of [fun]
  prval pfu = unit_v ()
  var
  fopr = fopr
  val ys =
  list_map2_funenv<a1,a2><b> {v0}{vt} (pfu | xs1, xs2, app, fopr)
  prval () = topize(fopr)
  prval unit_v((*void*)) = pfu
in
  list0_of_list_vt (ys)
end // end of [list0_map2]
*)
//
implement
{a1,a2}{b}
list0_map2
  (xs1, xs2, fopr) = let
//
implement
{a11,a12}{b2}
list_map2$fopr
  (x1, x2) =
$UN.castvwtp0{b2}
  (fopr($UN.cast{a1}(x1), $UN.cast{a2}(x2)))
//
in
  list0_of_list_vt{b}(list_map2<a1,a2><b>(g1ofg0(xs1), g1ofg0(xs2)))
end // end of [list0_map2]

(* ****** ****** *)
//
implement
{a}(*tmp*)
list0_filter
  (xs, pred) = let
//
implement{a2}
list_filter$pred
  (x) = pred($UN.cast{a}(x))
//
val ys = list_filter<a>(g1ofg0(xs))
//
in
  list0_of_list_vt (ys)
end // end of [list0_filter]
//
implement
{a}(*tmp*)
list0_filter_method
  (xs) = lam(pred) => list0_filter<a>(xs, pred)
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_tabulate
  {n}(n, fopr) = let
//
implement{a2}
list_tabulate$fopr
  (i) = let
  val i =
  $UN.cast{natLt(n)}(i)
in
  $UN.castvwtp0{a2}(fopr(i))
end // list_tabulate$fopr
//
val n = g1ofg0_int(n)
//
in
//
if
(n >= 0)
then
list0_of_list_vt(list_tabulate<a>(n))
else
$raise IllegalArgExn("list0_tabulate:n")
// end of [if]
end // end of [list0_tabulate]

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

implement
{a}(*tmp*)
list0_tabulate_opt
  (n, fopr) = res where
{
//
fun loop
(
  i: Nat
, res: &ptr? >> List0_vt(a)
) : void = let
in
//
if
(n > i)
then (
case+ fopr(i) of
| ~None_vt() =>
    loop(i+1, res)
  // end of [None_vt]
| ~Some_vt(x) => let
//
    val () =
    (
      res :=
      list_vt_cons{a}{0}(x, _)
    ) (* end of [val] *)
//
    val+list_vt_cons(_, res1) = res
//
    val () = loop (i+1, res1)
//
    prval ((*folded*)) = fold@ (res)
  in
    // nothing
  end // end of [Some0]
) else
(
  res := list_vt_nil((*void*))
) (* end of [if] *)
//
end // end of [loop]
//
var res: ptr
val () = loop (0, res)
val res = list0_of_list_vt (res)
//
} // end of [list0_tabulate_opt]

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

implement
{x,y}
list0_zip
  (xs, ys) = let
//
  val xs = g1ofg0(xs)
  and ys = g1ofg0(ys)
  val xys = $effmask_wrt(list_zip<x,y> (xs, ys))
//
in
  list0_of_list_vt{(x,y)}(xys)
end // end of [list0_zip]

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

implement
{x,y}
list0_cross
  (xs, ys) = let
//
  val xs = g1ofg0(xs)
  and ys = g1ofg0(ys)
  val xys = $effmask_wrt(list_cross<x,y> (xs, ys))
//
in
  list0_of_list_vt{(x,y)}(xys)
end // end of [list0_cross]

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

implement
{x,y}{z}
list0_crosswith
  (xs, ys, fopr) = let
//
implement
{x2,y2}{z2}
list_crosswith$fopr(x, y) =
$UN.castvwtp0{z2}
  (fopr($UN.cast{x}(x), $UN.cast{y}(y)))
//
val xs = g1ofg0(xs) and ys = g1ofg0(ys)
val zs = $effmask_wrt(list_crosswith<x,y><z> (xs, ys))
//
in
  list0_of_list_vt{z}(zs)
end // end of [list0_crosswith]

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

implement
{x}(*tmp*)
list0_foreach_choose2
(
  xs, fwork
) = loop(xs) where
{
//
fnx
loop(xs: list0(x)): void =
(
case+ xs of
| list0_nil() => ()
| list0_cons
    (x, xs) => loop2(x, xs, xs)
  // end of [list0_cons]
)
and
loop2
(
  x0: x, xs: list0(x), ys: list0(x)
) : void =
(
case+ ys of
| list0_nil
    () => loop(xs)
| list0_cons
    (y, ys) => let
    val () = fwork(x0, y) in loop2(x0, xs, ys)
  end // end of [list_cons]
)
//
} (* end of [list0_foreach_choose2] *)
//
implement
{x}(*tmp*)
list0_foreach_choose2_method(xs) =
  lam(fwork) => list0_foreach_choose2<x>(xs, fwork)
//
(* ****** ****** *)

implement
{x,y}(*tmp*)
list0_foreach_xprod2
(
  xs0, ys0, fwork
) = loop(xs0) where
{
//
fnx
loop(xs: list0(x)): void =
(
case+ xs of
| list0_nil() => ()
| list0_cons(x, xs) => loop2(x, xs, ys0)
)
and
loop2
(
  x0: x, xs: list0(x), ys: list0(y)
) : void =
(
case+ ys of
| list0_nil() => loop(xs)
| list0_cons(y, ys) => (fwork(x0, y); loop2(x0, xs, ys))
)
//
} (* end of [list0_foreach_xprod2] *)
//
implement
{x,y}(*tmp*)
list0_foreach_xprod2_method
  (xs, ys) =
  lam(fwork) => list0_foreach_xprod2<x,y>(xs, ys, fwork)
//
(* ****** ****** *)

implement
{x,y}(*tmp*)
list0_iforeach_xprod2
(
  xs0, ys0, fwork
) = loop(0, xs0) where
{
//
typedef int = intGte(0)
//
fnx
loop
(
  i: int, xs: list0(x)
) : void =
(
case+ xs of
| list0_nil() => ()
| list0_cons
    (x, xs) => loop2(i, x, xs, 0, ys0)
  // end of [list_cons]
)
and
loop2
(
  i0: int, x0: x, xs: list0(x), j: int, ys: list0(y)
) : void =
(
case+ ys of
| list0_nil() => loop(i0+1, xs)
| list0_cons(y, ys) =>
    (fwork(i0, x0, j, y); loop2(i0, x0, xs, j+1, ys))
  // end of [list0_cons]
)
//
} (* end of [list0_iforeach_xprod2] *)
//
implement
{x,y}(*tmp*)
list0_iforeach_xprod2_method
  (xs, ys) =
(
lam(fwork) => list0_iforeach_xprod2<x,y>(xs, ys, fwork)
) (* list0_iforeach_xprod2_method *)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
streamize_list0_elt
  (xs) = streamize_list_elt<a>(g1ofg0(xs))
implement
{a}(*tmp*)
streamize_list0_choose2
  (xs) = streamize_list_choose2<a>(g1ofg0(xs))
//
(* ****** ****** *)

implement
{a}(*tmp*)
streamize_list0_nchoose
  (xs, n) = let  
//
fun
auxmain
(
  xs: list0(a), n: intGte(0)
) : stream_vt(list0(a)) = $ldelay
(
//
if
(n > 0)
then
(
case+ xs of
| list0_nil() =>
  stream_vt_nil()
| list0_cons(x0, xs1) => let
    val res1 =
      auxmain(xs1, n-1)
    // end of [val]
    val res2 = auxmain(xs1, n)
  in
    !(stream_vt_append
      (
        stream_vt_map_cloptr<list0(a)><list0(a)>(res1, lam(ys) => list0_cons(x0, ys)), res2
      ) // stream_vt_append
     )
  end // end of [list0_cons]
) (* end of [then] *)
else
(
  stream_vt_cons(list0_nil, stream_vt_make_nil())
) (* end of [else] *)
//
) : stream_vt_con(list0(a)) // auxmain
//
in
  $effmask_all(auxmain(xs, n))
end // end of [streamize_list0_nchoose]

(* ****** ****** *)
//
implement
{a,b}(*tmp*)
streamize_list0_zip
  (xs, ys) =
  streamize_list_zip<a,b>(g1ofg0(xs), g1ofg0(ys))
//
implement
{a,b}(*tmp*)
streamize_list0_cross
  (xs, ys) =
  streamize_list_cross<a,b>(g1ofg0(xs), g1ofg0(ys))
//
(* ****** ****** *)

implement
{a}(*tmp*)
list0_is_ordered
  (xs, cmp) = let
//
implement
gcompare_val_val<a>(x, y) = cmp(x, y)
//
in
  list_is_ordered<a>(g1ofg0_list{a}(xs))
end // end of [list0_is_ordered]

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

implement
{a}(*tmp*)
list0_mergesort(xs, cmp) = let
//
implement
list_mergesort$cmp<a>(x, y) = cmp(x, y)
//
val ys = $effmask_wrt(list_mergesort<a>(g1ofg0(xs)))
//
in
  list0_of_list_vt (ys)
end // end of [list0_mergesort]

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

implement
{a}(*tmp*)
list0_quicksort(xs, cmp) = let
//
implement
list_quicksort$cmp<a>(x, y) = cmp(x, y)
//
val ys = $effmask_wrt(list_quicksort<a>(g1ofg0(xs)))
//
in
  list0_of_list_vt (ys)
end // end of [list0_quicksort]

(* ****** ****** *)
//
// HX: some common generic functions
//
(* ****** ****** *)
//
implement
(a)(*tmp*)
fprint_val<list0(a)> = fprint_list0<a>
//
(* ****** ****** *)

implement
(a)(*tmp*)
gcompare_val_val<list0(a)>
  (xs, ys) = let
//
fun
auxlst
(
  xs: list0(a), ys: list0(a)
) : int =
(
case+ xs of
| list0_nil() =>
  (
    case+ ys of
    | list0_nil() => 0
    | list0_cons _ => ~1
  ) (* list0_nil *)
| list0_cons(x, xs) =>
  (
    case+ ys of
    | list0_nil() => 1
    | list0_cons(y, ys) => let
        val sgn =
          gcompare_val_val<a>(x, y)
        // end of [val]
      in
        if sgn != 0 then sgn else auxlst(xs, ys)
      end // end of [list0_cons]
  ) (* list0_cons *)
) (* end of [auxlst] *)
//
in
  $effmask_all(auxlst(xs, ys))
end (* end of [gcompare_val_val] *)

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

(* end of [list0.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: July, 2012 *)

(* ****** ****** *)
//
staload
UN = "prelude/SATS/unsafe.sats"
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/array0.sats"

(* ****** ****** *)
//
extern
fun
memcpy
(
  d:ptr, s:ptr, n:size_t
) :<!wrt> ptr = "mac#atslib_ML_array0_memcpy"
// end of [memcpy]
//
(* ****** ****** *)
//
implement
{}(*tmp*)
array0_of_arrszref{a}(A) = $UN.cast{array0(a)}(A)
//
implement
{}(*tmp*)
arrszref_of_array0{a}(A) = $UN.cast{arrszref(a)}(A)
//
(* ****** ****** *)

implement
{}(*tmp*)
array0_get_ref
  (A0) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_get_ref (ASZ)
  // end of [val]
end // end of [array0_get_ref]

implement
{}(*tmp*)
array0_get_size
  (A0) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_get_size (ASZ)
  // end of [val]
end // end of [array0_get_size]

implement
{}(*tmp*)
array0_get_refsize
  (A0) = let
  var asz: size_t
  val ASZ = arrszref_of_array0 (A0)
  val A = $effmask_wrt (arrszref_get_refsize (ASZ, asz))
in
  @(A, asz)
end // end of [array0_get_refsize]

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

implement
{}(*tmp*)
array0_make_arrpsz
  (psz) = let
  val ASZ =
    arrszref_make_arrpsz(psz) in array0_of_arrszref(ASZ)
  // end of [val]
end // end of [array0_make_arrpsz]

implement
{}(*tmp*)
array0_make_arrayref
  (A, n) = let
  val ASZ =
    arrszref_make_arrayref(A, n) in array0_of_arrszref(ASZ)
  // end of [val]
end // end of [array0_make_arrpsz]

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

implement
{a}(*tmp*)
array0_make_elt
  (asz, x0) = let
  val ASZ =
    arrszref_make_elt<a>(asz, x0) in array0_of_arrszref(ASZ)
  // end of [val]
end // end of [array0_make_elt]

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

implement
{a}(*tmp*)
array0_make_list
  (xs) = let
  val xs = g1ofg0(xs)
  val ASZ = arrszref_make_list (xs) in array0_of_arrszref (ASZ)
end // end of [array0_make_list]

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

implement
{a}(*tmp*)
array0_make_rlist
  (xs) = let
  val xs = g1ofg0(xs)
  val ASZ = arrszref_make_rlist (xs) in array0_of_arrszref (ASZ)
end // end of [array0_make_rlist]

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

implement
{a}(*tmp*)
array0_make_subarray
  (A0, st, ln) = let
//
val st = g1ofg0(st)
val ln = g1ofg0(ln)
val [n:int] (A, asz) = array0_get_refsize (A0)
//
val [st:int] st =
  (if st <= asz then st else asz): sizeLte (n)
val [ln:int] ln =
  (if st + ln <= asz then ln else asz - st): sizeLte (n-st)
//
val A2 = arrayptr_make_uninitized<a> (ln)
val p2 = memcpy (ptrcast(A2), ptr_add<a> (ptrcast(A), st), ln*sizeof<a>)
val A2 = $UN.castvwtp0{arrayref(a,ln)}(A2)
//
in
  array0_make_arrayref (A2, ln)
end // end of [array0_make_subarray]

(* ****** ****** *)
//
implement
{a}(*tmp*)
print_array0 (A) =
  fprint_array0<a> (stdout_ref, A)
//
implement
{a}(*tmp*)
prerr_array0 (A) =
  fprint_array0<a> (stderr_ref, A)
//
implement
{a}(*tmp*)
fprint_array0 (out, A) =
  fprint_arrszref (out, arrszref_of_array0(A))
//
implement
{a}(*tmp*)
fprint_array0_sep (out, A, sep) =
  fprint_arrszref_sep (out, arrszref_of_array0(A), sep)
//
(* ****** ****** *)

implement
{a}{tk}
array0_get_at_gint
  (A0, i) = let
in
//
if i >= 0 then
  array0_get_at_size (A0, g0i2u(i))
else
  $raise ArraySubscriptExn() // neg index
//
end // end of [array0_get_at_gint]

implement
{a}{tk}
array0_get_at_guint
  (A0, i) = let
in
  array0_get_at_size (A0, g0u2u(i))
end // end of [array0_get_at_guint]

implement
{a}(*tmp*)
array0_get_at_size
  (A0, i) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_get_at_size (ASZ, i)
  // end of [val]
end // end of [array0_get_at_size]

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

implement
{a}{tk}
array0_set_at_gint
  (A0, i, x) = let
in
//
if i >= 0 then
  array0_set_at_size (A0, g0i2u(i), x)
else
  $raise ArraySubscriptExn() // neg index
//
end // end of [array0_set_at_gint]

implement
{a}{tk}
array0_set_at_guint
  (A0, i, x) =
(
  array0_set_at_size (A0, g0u2u(i), x)
) // end of [array0_set_at_guint]

implement
{a}(*tmp*)
array0_set_at_size
  (A0, i, x) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_set_at_size (ASZ, i, x)
  // end of [val]
end // end of [array0_set_at_size]

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

implement
{a}{tk}
array0_exch_at_gint
  (A0, i, x) = let
in
//
if i >= 0 then
  array0_exch_at_size (A0, g0i2u(i), x)
else
  $raise ArraySubscriptExn() // neg index
//
end // end of [array0_exch_at_gint]

implement
{a}{tk}
array0_exch_at_guint
  (A0, i, x) =
(
  array0_exch_at_size (A0, g0u2u(i), x)
) // end of [array0_exch_at_guint]

implement
{a}(*tmp*)
array0_exch_at_size
  (A0, i, x) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_exch_at_size (ASZ, i, x)
  // end of [val]
end // end of [array0_exch_at_size]

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

implement
{a}(*tmp*)
array0_interchange
  (A0, i, j) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_interchange (ASZ, i, j)
  // end of [val]
end // end of [array0_interchange]

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

implement
{a}(*tmp*)
array0_subcirculate
  (A0, i, j) = let
  val ASZ =
    arrszref_of_array0 (A0) in arrszref_subcirculate (ASZ, i, j)
  // end of [val]
end // end of [array0_subcirculate]

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

implement
{a}(*tmp*)
array0_copy
  (A0) = let
//
val ASZ = arrszref_of_array0 (A0)
//
var asz: size_t
val A = arrszref_get_refsize (ASZ, asz)
//
val (
  vbox pf | p
) = arrayref_get_viewptr (A)
val (pfarr, pfgc | q) = array_ptr_alloc<a> (asz)
val () = array_copy<a> (!q, !p, asz)
//
val A2 = arrayptr_encode (pfarr, pfgc | q)
val A2 = arrayptr_refize (A2) // non-linearizing
val ASZ2 = arrszref_make_arrayref (A2, asz)
//
in
  array0_of_arrszref (ASZ2)
end // end of [array0_copy]

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

implement
{a}(*tmp*)
array0_append
  (A01, A02) = let
//
val ASZ1 = arrszref_of_array0 (A01)
and ASZ2 = arrszref_of_array0 (A02)
//
var asz1: size_t and asz2: size_t
val A1 = arrszref_get_refsize (ASZ1, asz1)
and A2 = arrszref_get_refsize (ASZ2, asz2)
//
val (pf1box | p1) = arrayref_get_viewptr (A1)
and (pf2box | p2) = arrayref_get_viewptr (A2)
//
extern
praxi unbox
  : {v:view} vbox(v) -<prf> (v, v -<lin,prf> void)
//
prval (pf1, fpf1) = unbox (pf1box)
prval (pf2, fpf2) = unbox (pf2box)
//
val asz = asz1 + asz2
val (pfarr, pfgc | q) = array_ptr_alloc<a> (asz)
prval (pf1arr, pf2arr) = array_v_split_at (pfarr | asz1)
//
val () = array_copy<a> (!q, !p1, asz1)
val q2 = ptr1_add_guint<a> (q, asz1)
val (pf2arr | q2) = viewptr_match (pf2arr | q2)
val () = array_copy<a> (!q2, !p2, asz2)
//
prval () = fpf1 (pf1) and () = fpf2 (pf2)
//
prval pfarr = array_v_unsplit (pf1arr, pf2arr)
//
val A12 = arrayptr_encode (pfarr, pfgc | q)
val A12 = arrayptr_refize (A12)
val ASZ12 = arrszref_make_arrayref (A12, asz)
//
in
  array0_of_arrszref (ASZ12)
end // end of [array0_append]

(* ****** ****** *)
//
implement
{a}{b}
array0_map
  (A, fopr) = let
//
val p0 = array0_get_ref (A)
val asz = array0_get_size (A)
//
val fopr = $UN.cast{cfun1(ptr, b)}(fopr)
//
in
//
array0_tabulate<b>
  (g1ofg0(asz), lam i => fopr(ptr_add<a>(p0, i)))
//
end // end of [array0_map]
//
implement
{a}{b}
array0_map_method
  (A0, _(*TYPE*)) = lam(fopr) => array0_map<a>(A0, fopr)
//
(* ****** ****** *)

implement
{a}(*tmp*)
array0_tabulate
  {n}(asz, f) = let
//
implement{a2}
array_tabulate$fopr
  (i) = let
//
  val i =
  $UN.cast{sizeLt(n)}(i)
//
in
  $UN.castvwtp0{a2}(f(i))
end // array_tabulate$fopr
//
val ASZ = arrszref_tabulate<a> (asz)
//
in
  array0_of_arrszref (ASZ)  
end // end of [array0_tabulate]

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

implement
{a}(*tmp*)
array0_find_exn (A0, p) = let
//
val
ASZ = arrszref_of_array0 (A0)
//
var
asz : size_t
val A = arrszref_get_refsize (ASZ, asz)
//
implement(tenv)
array_foreach$cont<a><tenv>(x, env) = ~p(x)
implement(tenv)
array_foreach$fwork<a><tenv>(x, env) = ((*nothing*))
//
val idx = arrayref_foreach<a>(A, asz)
//
in
  if idx < asz then idx else $raise NotFoundExn()
end // end of [array0_find_exn]

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

(*
/*
implement
{a}(*tmp*)
array0_find_opt (A0, p) =
  try Some_vt(array0_find_exn<a> (A0, p)) with ~NotFoundExn() => None_vt()
// end of [array0_find_opt]
*/
*)

(* ****** ****** *)
//
implement
{a}(*tmp*)
array0_exists
  (A0, pred) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
array_foreach$cont<a><bool>
  (x, env) = not(env)
implement
array_foreach$fwork<a><bool>
  (x, env) =
  if pred(x) then env := true else ()
//
in
//
env where
{
//
var env:bool = false
val _(*asz*) =
  arrayref_foreach_env<a><bool>(A, asz, env)
//
} (* end of [where] *)
//
end // end of [array0_exists]
//
implement
{a}(*tmp*)
array0_exists_method(A0) =
  lam(pred) => array0_exists<a>(A0, pred)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
array0_iexists
  (A0, pred) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
array_iforeach$cont<a><bool>
  (i, x, env) = not(env)
implement
array_iforeach$fwork<a><bool>
  (i, x, env) =
  if pred(i, x) then env := true else ()
//
in
//
env where
{
//
var env:bool = false
val _(*asz*) =
  arrayref_iforeach_env<a><bool>(A, asz, env)
//
} (* end of [where] *)
//
end // end of [array0_iexists]
//
implement
{a}(*tmp*)
array0_iexists_method(A0) =
  lam(pred) => array0_iexists<a>(A0, pred)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
array0_forall
  (A0, pred) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
array_foreach$cont<a><bool>
  (x, env) = (env)
implement
array_foreach$fwork<a><bool>
  (x, env) =
  if pred(x) then () else env := false
//
in
//
env where
{
//
var env:bool = true
val _(*asz*) =
  arrayref_foreach_env<a><bool>(A, asz, env)
//
} (* end of [where] *)
//
end // end of [array0_forall]
//
implement
{a}(*tmp*)
array0_forall_method(A0) =
  lam(pred) => array0_forall<a>(A0, pred)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
array0_iforall
  (A0, pred) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
array_iforeach$cont<a><bool>
  (i, x, env) = (env)
implement
array_iforeach$fwork<a><bool>
  (i, x, env) =
  if pred(i, x) then () else env := false
//
in
//
env where
{
//
var env:bool = true
val _(*asz*) =
  arrayref_iforeach_env<a><bool>(A, asz, env)
//
} (* end of [where] *)
//
end // end of [array0_iforall]
//
implement
{a}(*tmp*)
array0_iforall_method(A0) =
  lam(pred) => array0_iforall<a>(A0, pred)
//
(* ****** ****** *)

implement
{a}(*tmp*)
array0_foreach
  (A0, fwork) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A = arrszref_get_refsize(ASZ, asz)
//
implement(tenv)
array_foreach$cont<a><tenv>(x, env) = true
implement(tenv)
array_foreach$fwork<a><tenv>(x, env) = fwork(x)
//
val _(*asz*) = arrayref_foreach<a>(A, asz)
//
in
  // nothing
end // end of [array0_foreach]
//
implement
{a}(*tmp*)
array0_foreach_method(A0) =
  lam(fwork) => array0_foreach<a>(A0, fwork)
//
(* ****** ****** *)

implement
{a}(*tmp*)
array0_iforeach
  (A0, fwork) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A = arrszref_get_refsize(ASZ, asz)
//
implement(tenv)
array_iforeach$cont<a><tenv>(i, x, env) = true
implement(tenv)
array_iforeach$fwork<a><tenv>(i, x, env) = fwork(i, x)
//
val _(*asz*) = arrayref_iforeach<a> (A, asz)
//
in
  // nothing
end // end of [array0_iforeach]
//
implement
{a}(*tmp*)
array0_iforeach_method(A0) =
  lam(fwork) => array0_iforeach<a>(A0, fwork)
//
(* ****** ****** *)

implement
{a}(*tmp*)
array0_rforeach
  (A0, fwork) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A = arrszref_get_refsize(ASZ, asz)
//
implement(tenv)
array_rforeach$cont<a><tenv>(x, env) = true
implement(tenv)
array_rforeach$fwork<a><tenv>(x, env) = fwork(x)
//
val _(*asz*) = arrayref_rforeach<a> (A, asz)
//
in
  // nothing
end // end of [array0_rforeach]
//
implement
{a}(*tmp*)
array0_rforeach_method(A0) =
  lam(fwork) => array0_rforeach<a>(A0, fwork)
//
(* ****** ****** *)

implement
{tres}{a}
array0_foldleft
(
  A0, ini, fopr
) = res where
{
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A = arrszref_get_refsize(ASZ, asz)
//
implement
array_foreach$cont<a><tres> (x, env) = true
implement
array_foreach$fwork<a><tres> (x, env) = env := fopr(env, x)
//
var
res: tres = ini
val _(*asz*) =
  arrayref_foreach_env<a><tres>(A, asz, res)
//
} (* end of [array0_foldleft] *)
//
implement
{tres}{a}
array0_foldleft_method(A0, _) =
  lam(ini, fopr) => array0_foldleft<tres><a>(A0, ini, fopr)
//
(* ****** ****** *)

implement
{tres}{a}
array0_ifoldleft
(
  A0, ini, fopr
) = res where
{
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A = arrszref_get_refsize(ASZ, asz)
//
implement
array_iforeach$cont<a><tres>(i, x, env) = true
implement
array_iforeach$fwork<a><tres>(i, x, env) = (env := fopr(env, i, x))
//
var
res: tres = ini
val _(*asz*) =
  arrayref_iforeach_env<a><tres>(A, asz, res)
//
} (* end of [array0_ifoldleft] *)
//
implement
{tres}{a}
array0_ifoldleft_method(A0, _) =
  lam(ini, fopr) => array0_ifoldleft<tres><a>(A0, ini, fopr)
//
(* ****** ****** *)

implement
{a}{tres}
array0_foldright
(
  A0, fopr, snk
) = res where
{
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
array_rforeach$cont<a><tres>
  (x, env) = true
implement
array_rforeach$fwork<a><tres>
  (x, env) = env := fopr(x, env)
//
var
res: tres = snk
//
val _(*asz*) =
arrayref_rforeach_env<a><tres>(A, asz, res)
//
} (* end of [array0_foldright] *)
//
implement
{a}{tres}
array0_foldright_method
  (A0, _) =
(
  lam(fopr, snk) =>
    array0_foldright<a><tres>(A0, fopr, snk)
) (* end of [lam] *)
//
(* ****** ****** *)

implement
{a}(*tmp*)
array0_is_ordered
  (A0, cmp) = let
//
implement
gcompare_ref_ref<a>
  (x, y) = $effmask_all(cmp(x, y))
//
in (* in-of-let *)
//
let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
in
//
  arrayref_is_ordered<a>(A, asz)
//
end // end of [let]
//
end // end of [array0_is_ordered]

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

implement
{a}(*tmp*)
array0_quicksort
  (A0, cmp) = let
//
val
ASZ = arrszref_of_array0(A0)
//
var
asz : size_t
val A =
  arrszref_get_refsize(ASZ, asz)
//
implement
{a}(*tmp*)
array_quicksort$cmp
  (x1, x2) = let
//
val
cmp =
$UN.cast{(&a,&a)-<cloref>int}(cmp)
//
in
   cmp(x1, x2)
end // end of [array_quicksort$cmp]
//
in
  arrayref_quicksort<a> (A, asz)
end // end of [array0_quicksort]

(* ****** ****** *)
//
// HX: some common generic functions
//
(* ****** ****** *)

implement
(a)(*tmp*)
fprint_val<array0(a)> = fprint_array0<a>

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

implement
(a)(*tmp*)
gcompare_val_val<array0(a)>
  (xs, ys) = let
//
val m = array0_get_size{a}(xs)
val n = array0_get_size{a}(ys)
//
fun
loop
(
  px: ptr, py: ptr, i: size_t, j: size_t
) : int =
(
if (
i < m
) then (
//
if j < n
  then let
    val (pfx, fpfx | px) =
      $UN.ptr_vtake{a}(px)
    val (pfy, fpfy | py) =
      $UN.ptr_vtake{a}(py)
    val sgn = gcompare_ref_ref(!px, !py)
    prval () = fpfx(pfx) and () = fpfy(pfy)
  in
    if sgn != 0
      then (sgn)
      else loop(ptr_succ<a>(px), ptr_succ<a>(py), succ(i), succ(j))
    // end of [if]
  end else (1) // end of [else]
//
) else (
//
if j < n then (~1) else (0)
//
) (* end of [else] *)
) (* end of [loop] *)
//
in
  $effmask_all(loop(array0_get_ref{a}(xs), array0_get_ref{a}(xs), i2sz(0), i2sz(0)))
end // end of [gcompare_val_val]

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

(* end of [array0.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2014 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: February, 2014 *)

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

staload
UN = "prelude/SATS/unsafe.sats"

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

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/matrix0.sats"

(* ****** ****** *)
//
implement{}
matrix0_of_mtrxszref{a}(A) = $UN.cast{matrix0(a)}(A)
//
implement{}
mtrxszref_of_matrix0{a}(A) = $UN.cast{mtrxszref(a)}(A)
//
(* ****** ****** *)
//
implement{
} matrix0_get_ref (M) =
  mtrxszref_get_ref (mtrxszref_of_matrix0(M))
//
implement{
} matrix0_get_nrow (M) =
  mtrxszref_get_nrow (mtrxszref_of_matrix0(M))
implement{
} matrix0_get_ncol (M) =
  mtrxszref_get_ncol (mtrxszref_of_matrix0(M))
//
(* ****** ****** *)

implement{
} matrix0_get_refsize (M) = let
  var nrow: size_t and ncol: size_t
  val Mref =
  $effmask_wrt
  (
    mtrxszref_get_refsize(mtrxszref_of_matrix0(M), nrow, ncol)
  ) (* end of [val] *)
in
  (Mref, nrow, ncol)
end // end of [matrix0_get_refsize]

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

implement
{a}(*tmp*)
matrix0_make_elt
  (nrow, ncol, x0) =
  matrix0_of_mtrxszref (mtrxszref_make_elt<a> (nrow, ncol, x0))
// end of [matrix0_make_elt]

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

implement
{a}(*tmp*)
matrix0_get_at_int
  (M0, i, j) = let
  val i = g1ofg0_int(i)
  and j = g1ofg0_int(j)
in
//
if i >= 0
then (
if j >= 0 then
  matrix0_get_at_size<a> (M0, i2sz(i), i2sz(j))
else
  $raise MatrixSubscriptExn((*void*)) // neg index
// end of [if]
) else
  $raise MatrixSubscriptExn((*void*)) // neg index
// end of [if]
//
end // end of [matrix0_get_at_int]

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

implement
{a}(*tmp*)
matrix0_get_at_size
  (M0, i, j) = let
  val MSZ =
    mtrxszref_of_matrix0 (M0) in mtrxszref_get_at_size (MSZ, i, j)
  // end of [val]
end // end of [matrix0_get_at_size]

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

implement
{a}(*tmp*)
matrix0_set_at_int
  (M0, i, j, x) = let
  val i = g1ofg0_int(i)
  and j = g1ofg0_int(j)
in
//
if i >= 0
then (
if j >= 0 then
  matrix0_set_at_size<a> (M0, i2sz(i), i2sz(j), x)
else
  $raise MatrixSubscriptExn((*void*)) (* neg index *)
// end of [if]
) else
  $raise MatrixSubscriptExn((*void*)) (* neg index *)
// end of [if]
//
end // end of [matrix0_set_at_int]

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

implement
{a}(*tmp*)
matrix0_set_at_size
  (M0, i, j, x) = let
  val MSZ =
    mtrxszref_of_matrix0 (M0) in mtrxszref_set_at_size (MSZ, i, j, x)
  // end of [val]
end // end of [matrix0_set_at_size]

(* ****** ****** *)
//
implement
{a}(*tmp*)
print_matrix0 (A) =
  fprint_matrix0<a> (stdout_ref, A)
//
implement
{a}(*tmp*)
prerr_matrix0 (A) =
  fprint_matrix0<a> (stderr_ref, A)
//
implement
{a}(*tmp*)
fprint_matrix0 (out, M) =
  fprint_mtrxszref (out, mtrxszref_of_matrix0(M))
//
implement
{a}(*tmp*)
fprint_matrix0_sep (out, M, sep1, sep2) =
  fprint_mtrxszref_sep (out, mtrxszref_of_matrix0(M), sep1, sep2)
//
(* ****** ****** *)

implement
{a}(*tmp*)
matrix0_copy (M0) = let
//
val M = matrix0_get_ref (M0)
val [m:int] m = g1ofg0 (M0.nrow())
val [n:int] n = g1ofg0 (M0.ncol())
val M =
  matrixref_copy<a> ($UN.cast{matrixref(a,m,n)}(M), m, n)
// end of [val]
in
//
matrix0_of_mtrxszref
  (mtrxszref_make_matrixref (matrixptr_refize{a}(M), m, n))
//
end // end of [matrix0_copy]

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

implement
{a}(*tmp*)
matrix0_tabulate
  (nrow, ncol, f) = let
//
implement{a2}
matrix_tabulate$fopr
  (i, j) = $UN.castvwtp0{a2}(f(i,j))
//
val MSZ = mtrxszref_tabulate<a> (nrow, ncol)
//
in
  matrix0_of_mtrxszref (MSZ)  
end // end of [matrix0_tabulate]

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

implement
{a}(*tmp*)
matrix0_foreach
  (M0, f) = let
//
fun loop
(
  p: ptr, i: size_t
) : void = (
if i > 0 then let
  val (pf, fpf | p) = $UN.ptr0_vtake (p)
  val ((*void*)) = f (!p)
  prval ((*void*)) = fpf (pf)
in
  loop (ptr_succ<a> (p), pred (i))
end else ((*void*)) // end of [if]
) (* end of [loop] *)
//
val (M, m, n) = matrix0_get_refsize (M0)
//
in
  loop (ptrcast(M), m * n)
end // end of [matrix0_foreach]

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

implement
{a}(*tmp*)
matrix0_iforeach
  (M0, f) = let
//
val (M, m, n) =
  matrix0_get_refsize (M0)
//
fun loop
(
  p: ptr
, k: size_t, i: size_t, j: size_t
) : void = (
if k > 0 then let
  val (
    pf, fpf | p
  ) = $UN.ptr0_vtake (p)
  val () = f (i, j, !p)
  prval ((*void*)) = fpf (pf)
  val p = ptr_succ<a> (p)
  val k = pred(k) and j = succ(j)
in
//
if j < n
  then loop (p, k, i, j)
  else loop (p, k, succ(i), i2sz(0))
// end of [if]
//
end else ((*void*)) // end of [if]
) (* end of [loop] *)
//
in
  loop (ptrcast(M), m * n, i2sz(0), i2sz(0))
end // end of [matrix0_iforeach]

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

implement
{res}{a}(*tmp*)
matrix0_foldleft
  (M0, ini, f) = let
//
var ini: res = ini
val p_ini = addr@(ini)
//
var f2 =
lam@ (x: &a): void =>
  $UN.ptr0_set<res> (p_ini, f ($UN.ptr0_get<res> (p_ini), x))
//
val () =
matrix0_foreach<a> (M0, $UN.cast{(&a)-<cloref1>void}(addr@f2))
//
in
  ini
end // end of [matrix0_foldleft]

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

implement
{res}{a}(*tmp*)
matrix0_ifoldleft
  (M0, ini, f) = let
//
var ini: res = ini
val p_ini = addr@(ini)
//
var f2 =
lam@ (i: size_t, j: size_t, x: &a): void =>
  $UN.ptr0_set<res> (p_ini, f ($UN.ptr0_get<res> (p_ini), i, j, x))
//
val () =
matrix0_iforeach<a> (M0, $UN.cast{(size_t,size_t,&a)-<cloref1>void}(addr@f2))
//
in
  ini
end // end of [matrix0_ifoldleft]

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

(* end of [matrix.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2016 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: October, 2016 *)

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

#define ATS_DYNLOADFLAG 0
  
(* ****** ****** *)
  
staload
UN = "prelude/SATS/unsafe.sats"

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

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/stream.sats"

(* ****** ****** *)
//
implement
{a}(*tmp*)
stream2list0(xs) =
list0_of_list_vt(stream2list(xs))
//
(* ****** ****** *)

implement
{a}(*tmp*)
stream_make_list0
  (xs) =
  auxmain(xs) where
{
//
fun
auxmain:
$d2ctype
(
stream_make_list0<a>
) = lam(xs) => $delay
(
case+ xs of
| list0_nil() => stream_nil()
| list0_cons(x, xs) => stream_cons(x, auxmain(xs))
)
//
} (* end of [stream_make_list0] *)

(* ****** ****** *)
//
implement
{a}{b}
stream_map_method
  (xs, _) =
(
lam(fopr) => stream_map_cloref<a><b>(xs, fopr)
)
//
(* ****** ****** *)
//
implement
{a}{b}
stream_imap_method
  (xs, _) =
(
lam(fopr) => stream_imap_cloref<a><b>(xs, fopr)
)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
stream_filter_method(xs) =
  lam(pred) => stream_filter_cloref<a>(xs, pred)
//
(* ****** ****** *)
//
implement
{res}{x}
stream_scan_method(xs, _) =
  lam(res, fopr) =>
  stream_scan_cloref<res><x>(xs, res, fopr)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
stream_foreach_method(xs) =
  lam(fwork) =>
    stream_foreach_cloref<a>(xs, fwork)
  // end of [lam]
//
(* ****** ****** *)
//
implement
{res}{a}
stream_foldleft_method
  (xs, _(*TYPE*)) =
  lam(ini, fopr) =>
    stream_foldleft_cloref<res><a>(xs, ini, fopr)
  // end of [lam]
//
(* ****** ****** *)

(* end of [stream.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         Applied Type System                         *)
(*                                                                     *)
(***********************************************************************)

(*
** ATS/Postiats - Unleashing the Potential of Types!
** Copyright (C) 2010-2016 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: October, 2016 *)

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

#define ATS_DYNLOADFLAG 0
  
(* ****** ****** *)
  
staload
UN = "prelude/SATS/unsafe.sats"

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

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/stream_vt.sats"

(* ****** ****** *)
//
implement
{a}{b}
stream_vt_map_method
  (xs, _) =
(
llam(fopr) => stream_vt_map_cloptr<a><b>(xs, fopr)
)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
stream_vt_filter_method
  (xs) =
(
  llam(pred) => stream_vt_filter_cloptr<a>(xs, pred)
)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
stream_vt_foreach_method
  (xs) =
(
llam(fwork) => stream_vt_foreach_cloptr<a>(xs, fwork)
)
//
implement
{a}(*tmp*)
stream_vt_rforeach_method
  (xs) =
(
llam(fwork) => stream_vt_rforeach_cloptr<a>(xs, fwork)
)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
stream_vt_iforeach_method
  (xs) =
(
llam(fwork) => stream_vt_iforeach_cloptr<a>(xs, fwork)
)
//
(* ****** ****** *)
//
implement
{res}{a}
stream_vt_foldleft_method
  (xs, _(*TYPE*)) =
(
llam(ini, fwork) => stream_vt_foldleft_cloptr<res><a>(xs, ini, fwork)
)
//
implement
{res}{a}
stream_vt_ifoldleft_method
  (xs, _(*TYPE*)) =
(
llam(ini, fwork) => stream_vt_ifoldleft_cloptr<res><a>(xs, ini, fwork)
)
//
(* ****** ****** *)

(* end of [stream_vt.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: January, 2013 *)

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

#define ATS_DYNLOADFLAG 0 // no dynloading at run-time

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

staload
UN = "prelude/SATS/unsafe.sats"

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

staload
_(*anon*) = "prelude/DATS/integer.dats"
staload
_(*anon*) = "prelude/DATS/integer_size.dats"

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

staload _(*anon*) = "prelude/DATS/filebas.dats"

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

(*
macdef
prelude_fileref_open_opt = fileref_open_opt
*)
macdef
prelude_fileref_get_line_charlst = fileref_get_line_charlst
macdef
prelude_fileref_get_lines_charlstlst = fileref_get_lines_charlstlst
macdef
prelude_fileref_get_line_string = fileref_get_line_string
macdef
prelude_fileref_get_lines_stringlst = fileref_get_lines_stringlst

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

macdef
prelude_streamize_fileref_char = streamize_fileref_char
macdef
prelude_streamize_fileref_line = streamize_fileref_line

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

staload "libats/ML/SATS/basis.sats"
staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/option0.sats"

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

staload "libats/ML/SATS/filebas.sats"

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

(*
implement
fileref_open_opt
  (path, mode) = let
  val opt = prelude_fileref_open_opt (path, mode)
in
  option0_of_option_vt (opt)
end // end of [fileref_open_opt]
*)

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

implement
fileref_get_line_charlst
  (filr) =
(
list0_of_list_vt
  (prelude_fileref_get_line_charlst (filr))
) // end of [fileref_get_line_charlst]

implement
fileref_get_lines_charlstlst
  (filr) =
(
$UN.castvwtp0{list0(charlst0)}
  (prelude_fileref_get_lines_charlstlst (filr))
) // end of [fileref_get_lines_charlstlst]

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

local

staload _(*anon*) = "prelude/DATS/strptr.dats"

in (* in of [local] *)

implement
fileref_get_line_string
  (filr) =
(
strptr2string
  (prelude_fileref_get_line_string(filr))
) // end of [fileref_get_line_string]

implement
fileref_get_lines_stringlst
  (filr) =
(
$UN.castvwtp0{list0(string)}
  (prelude_fileref_get_lines_stringlst(filr))
) // end of [fileref_get_lines_stringlst]

end // end of [local]

(* ****** ****** *)
//
implement
{}(*tmp*)
streamize_fileref_char
  (filr) =
  prelude_streamize_fileref_char(filr)
//
implement
{}(*tmp*)
streamize_fileref_line
  (filr) =
(
$UN.castvwtp0{stream_vt(string)}
  (prelude_streamize_fileref_line(filr))
) // end of [streamize_fileref_line]
//
(* ****** ****** *)

implement
{}(*tmp*)
streamize_fileref_word
  (filr) =
  auxmain(filr) where
{
//
fun
auxmain
(
  filr: FILEref
) :
stream_vt(string) =
$ldelay (
//
let
//
  val
  word =
  fileref_get_word<>(filr)
  val test = strptr_is_null(word)
//
  prval () = lemma_strptr_param(word)
//
in
  if test
    then let
    prval () =
      strptr_free_null(word) in stream_vt_nil()
    // end of [prval]
    end // end of [then]
    else stream_vt_cons(strptr2string(word), auxmain(filr))
  // end of [if]
end // end of [let]
//
) (* end of [auxmain] *)
//
} (* end of [streamize_fileref_word] *)

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

(* end of [filebas.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: September, 2014 *)

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

staload "libats/ML/SATS/basis.sats"

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

staload "libats/ML/SATS/list0.sats"
staload "libats/ML/SATS/array0.sats"
staload "libats/ML/SATS/intrange.sats"

(* ****** ****** *)
//
implement
{}(*tmp*)
int_repeat_lazy
  (n, fopr) =
  int_repeat_cloref<> (n, lazy2cloref(fopr))
//
(* ****** ****** *)

implement
{}(*tmp*)
int_repeat_cloref
  (n, fopr) = let
//
fun
loop
(
  n: int, f: cfun0(void)
) : void = (
//
if n > 0
  then let val () = fopr() in loop(n-1, fopr) end
  else ((*void*))
//
) (* end of [loop] *)
//
in
  loop (n, fopr)
end // end of [int_repeat_cloref]

(* ****** ****** *)
//
implement
{}(*tmp*)
int_repeat_method
  (n) = lam(fopr) => int_repeat_cloref(n, fopr)
//
(* ****** ****** *)
//
implement
{}(*tmp*)
int_forall_cloref
  (n, f) =
  intrange_forall_cloref<> (0, n, f)
//
implement
{}(*tmp*)
int_forall_method
  (n) = lam(f) => int_forall_cloref (n, f)
//
(* ****** ****** *)
//
implement
{}(*tmp*)
int_foreach_cloref
  (n, f) =
  intrange_foreach_cloref<> (0, n, f)
//
implement
{}(*tmp*)
int_foreach_method
  (n) = lam(f) => int_foreach_cloref (n, f)
//
(* ****** ****** *)
//
implement
{res}(*tmp*)
int_foldleft_cloref
  (n, ini, f) =
  intrange_foldleft_cloref<res> (0, n, ini, f)
//
implement
{res}(*tmp*)
int_foldleft_method
  (n, tres) =
  lam(ini, f) => int_foldleft_cloref (n, ini, f)
//
(* ****** ****** *)

implement
{}(*tmp*)
intrange_forall_cloref
  (l, r, f) = let
//
fun
loop
(
  l: int, r: int
, f: cfun1(int, bool)
) : bool = (
//
if l < r
  then (
    if f(l) then loop(l+1, r, f) else false
  ) else true
//
) (* end of [loop] *)
//
in
  loop (l, r, f)
end // end of [intrange_forall_cloref]
//
implement
{}(*tmp*)
intrange_forall_method
  ( @(l, r) ) = lam(f) => intrange_forall_cloref (l, r, f)
//
(* ****** ****** *)

implement
{}(*tmp*)
intrange_foreach_cloref
  (l, r, f) = let
//
fun
loop
(
  l: int, r: int, f: cfun1(int, void)
) : void = (
//
if l < r
  then let val () = f(l) in loop(l+1, r, f) end
  else ()
//
) (* end of [loop] *)
//
in
  loop (l, r, f)
end // end of [intrange_foreach_cloref]

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

implement
{}(*tmp*)
intrange_foreach_method
  ( @(l, r) ) = lam(f) => intrange_foreach_cloref (l, r, f)
//
(* ****** ****** *)

implement
{res}(*tmp*)
intrange_foldleft_cloref
  (l, r, ini, fopr) = let
//
fun
loop
(
  l: int, r: int
, ini: res, f: cfun2(res, int, res)
) : res = (
//
if l < r then loop (l+1, r, f(ini, l), f) else ini
//
) (* end of [loop] *)
//
in
  loop (l, r, ini, fopr)
end // end of [intrange_foldleft_cloref]

(* ****** ****** *)
//
implement
{res}(*tmp*)
intrange_foldleft_method
  ( @(l, r), tres ) =
(
//
lam(ini, f) =>
  intrange_foldleft_cloref<res> (l, r, ini, f)
//
) (* end of [intrange_foldleft_method] *)
//
(* ****** ****** *)
//
implement
{}(*tmp*)
int_streamGte(n) =
(
fix
aux
(
  n:int
) : stream(int) => $delay(stream_cons(n, aux(n+1)))
) (n) // end of [int_streamGte]
//
implement
{}(*tmp*)
int_streamGte_vt(n) =
(
fix
aux
(
  n:int
) : stream_vt(int) => $ldelay(stream_vt_cons(n, aux(n+1)))
) (n) // end of [int_streamGte_vt]
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
int_list0_map_cloref
  (n, f) = list0_tabulate<a> (n, f)
//
implement
{a}(*tmp*)
int_list0_map_method
  (n, tres) = lam(f) => int_list0_map_cloref<a> (n, f)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
int_array0_map_cloref
  (n, fopr) =
(
array0_tabulate<a>
  (i2sz(n), lam(i) => fopr(sz2i(i)))
)
//
implement
{a}(*tmp*)
int_array0_map_method
  (n, tres) = lam(f) => int_array0_map_cloref<a> (n, f)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
int_stream_map_cloref
  (n, f) = auxmain(0) where
{
//
fun
auxmain
(
  i: Nat
) : stream(a) = $delay
(
if
(i < n)
then stream_cons(f(i), auxmain(i+1)) else stream_nil()
) (* end of [auxmain] *)
//
} (* end of [int_stream_map_cloref] *)
//
implement
{a}(*tmp*)
int_stream_map_method
  (n, tres) = lam(f) => int_stream_map_cloref<a> (n, f)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
int_stream_vt_map_cloref
  (n, f) = auxmain(0) where
{
//
fun
auxmain
(
  i: Nat
) : stream_vt(a) = $ldelay
(
if
(i < n)
then stream_vt_cons(f(i), auxmain(i+1)) else stream_vt_nil()
) : stream_vt_con(a) // [auxmain]
//
} (* end of [int_stream_vt_map_cloref] *)
//
implement
{a}(*tmp*)
int_stream_vt_map_method
  (n, tres) = lam(f) => int_stream_vt_map_cloref<a> (n, f)
//
(* ****** ****** *)
//
implement
{}(*tmp*)
int2_foreach_cloref
  (n1, n2, f) =
  intrange2_foreach_cloref<> (0, n1, 0, n2, f)
//
implement
{}(*tmp*)
intrange2_foreach_cloref
  (l1, r1, l2, r2, f) = let
//
fnx
loop1
(
  m1: int, r1: int
, l2: int, r2: int
, f: cfun2 (int, int, void)
) : void = (
//
if
m1 < r1
then loop2(m1, r1, l2, l2, r2, f)
else ()
//
) (* end of [loop1] *)
//
and
loop2
(
  m1: int, r1: int
, l2: int, m2: int, r2: int
, f: cfun2 (int, int, void)
) : void = (
//
if
m2 < r2
then (
//
f(m1, m2);
loop2(m1, r1, l2, m2+1, r2, f)
//
) (* end of [then] *)
else loop1(m1+1, r1, l2, r2, f)
//
) (* end of [loop2] *)
//
in
  loop1 (l1, r1, l2, r2, f)
end // end of [intrange2_foreach_cloref]
//
(* ****** ****** *)

(* end of [intrange.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: August, 2013 *)

(* ****** ****** *)
//
// HX-2012-12:
// the map implementation is based on AVL trees
//
(* ****** ****** *)
//
staload FM =
"libats/SATS/funmap_avltree.sats"
//
(* ****** ****** *)

staload "libats/ML/SATS/list0.sats"

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

staload "libats/ML/SATS/funmap.sats"

(* ****** ****** *)
//
assume
map_type(key, itm) = $FM.map (key, itm)
//
(* ****** ****** *)

implement{a}
compare_key_key = gcompare_val_val<a>
implement{a}
$FM.compare_key_key = compare_key_key<a>

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

implement
{}(*tmp*)
funmap_nil() = $FM.funmap_nil<>()
implement
{}(*tmp*)
funmap_make_nil() = $FM.funmap_make_nil<>()

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

implement
{}(*tmp*)
funmap_is_nil(map) = $FM.funmap_is_nil<>(map)
implement
{}(*tmp*)
funmap_isnot_nil(map) = $FM.funmap_isnot_nil<>(map)

(* ****** ****** *)
//
implement
{key,itm}
funmap_size
  (map) = $FM.funmap_size<key,itm>(map)
//
(* ****** ****** *)
//
implement
{key,itm}
funmap_search
  (map, k) =
  $FM.funmap_search_opt<key,itm>(map, k)
//
(* ****** ****** *)
//
implement
{key,itm}
funmap_insert
  (map, k, x) =
  $FM.funmap_insert_opt<key,itm>(map, k, x)
//
(* ****** ****** *)
//
implement
{key,itm}
funmap_takeout
  (map, k) =
  $FM.funmap_takeout_opt<key,itm>(map, k)
//
(* ****** ****** *)
//
implement
{key,itm}
funmap_remove
  (map, k) = $FM.funmap_remove<key,itm>(map, k)
//
(* ****** ****** *)

implement
{key,itm}
fprint_funmap
  (out, map) = let
//
implement
$FM.fprint_funmap$sep<> = fprint_funmap$sep<>
implement
$FM.fprint_funmap$mapto<> = fprint_funmap$mapto<>
//
val () = $FM.fprint_funmap<key,itm>(out, map)
//
in
  // nothing
end // end of [fprint_funmap]

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

implement{}
fprint_funmap$sep(out) = fprint(out, "; ")
implement{}
fprint_funmap$mapto(out) = fprint(out, "->")

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

implement
{key,itm}
funmap_foreach_cloref
  (map, fwork) = () where
{
//
var env: void = ((*void*))
//
implement
(env)(*tmp*)
$FM.funmap_foreach$fwork<key,itm><env>
  (k, x, env) = fwork(k, x)
//
val ((*void*)) =
$FM.funmap_foreach_env<key,itm><void>(map, env)
//
} (* end of [funmap_foreach_cloref] *)

(* ****** ****** *)
//
implement
{key,itm}
funmap_listize
  (map) =
(
$effmask_wrt
(
list0_of_list_vt
  ($FM.funmap_listize<key,itm>(map))
)
) (* end of [funmap_listize] *)
//
(* ****** ****** *)

implement
{key,itm}
funmap_streamize
  (map) =
(
$effmask_wrt
  ($FM.funmap_streamize<key,itm>(map))
) (* end of [funmap_streamize] *)

(* ****** ****** *)
//
implement
{key,itm}
funmap_make_module
  ((*void*)) = $rec
{
//
nil = funmap_nil{key,itm}
,
size = funmap_size<key,itm>
,
is_nil = funmap_is_nil{key,itm}
,
isnot_nil = funmap_isnot_nil{key,itm}
,
search = funmap_search<key,itm>
,
insert = funmap_insert<key,itm>
,
remove = funmap_remove<key,itm>
,
takeout = funmap_takeout<key,itm>
,
listize = funmap_listize<key,itm>
,
streamiize = funmap_streamize<key,itm>
//
} (* end of [funmap_make_module] *)
//
(* ****** ****** *)

(* end of [funmap.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: December, 2012 *)

(* ****** ****** *)
//
// HX-2012-12: the set implementation is based on AVL trees
//
(* ****** ****** *)
//
staload
UN = "prelude/SATS/unsafe.sats"
//
(* ****** ****** *)
//
staload
FS =
"libats/SATS/funset_avltree.sats"
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

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

staload "libats/ML/SATS/list0.sats"

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

staload "libats/ML/SATS/funset.sats"

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

implement{a}
compare_elt_elt = gcompare_val_val<a>
implement{a}
$FS.compare_elt_elt = compare_elt_elt<a>

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

assume set_type (a:t0p) = $FS.set (a)

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

implement{}
funset_nil () = $FS.funset_nil ()
implement{}
funset_make_nil () = $FS.funset_make_nil ()

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

implement{a}
funset_sing (x) = $FS.funset_sing<a> (x)
implement{a}
funset_make_sing (x) = $FS.funset_make_sing<a> (x)

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

implement{a}
funset_make_list
  (xs) = let
//
val xs = g1ofg0_list(xs)
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_make_list<a>(xs)
end // end of [funset_make_list]

(* ****** ****** *)
//
implement{}
fprint_funset$sep
  (out) =
  fprint_string (out, ", ")
//
implement{a}
fprint_funset
  (out, xs) = let
//
implement
$FS.fprint_funset$sep<>
  (out) = fprint_funset$sep<>(out)
//
in
  $FS.fprint_funset<a>(out, xs)
end // end of [fprint_funset]
//
(* ****** ****** *)
//
implement
{}(*tmp*)
funset_is_nil
  (xs) = $FS.funset_is_nil<>(xs)
implement
{}(*tmp*)
funset_isnot_nil
  (xs) = $FS.funset_isnot_nil<>(xs)
//
(* ****** ****** *)

implement
{a}(*tmp*)
funset_size(xs) = $FS.funset_size<a>(xs)

(* ****** ****** *)
//
implement
{a}(*tmp*)
funset_is_member
  (xs, x0) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_is_member<a>(xs, x0)
end // end of [funset_is_member]
//
implement
{a}(*tmp*)
funset_isnot_member
  (xs, x0) = ~funset_is_member<a>(xs, x0)
//
(* ****** ****** *)

implement
{a}(*tmp*)
funset_insert
  (xs, x0) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_insert<a>(xs, x0)
end // end of [funset_insert]

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

implement
{a}(*tmp*)
funset_remove
  (xs, x0) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_remove<a>(xs, x0)
end // end of [funset_remove]

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

implement
{a}(*tmp*)
funset_getmax_opt = $FS.funset_getmax_opt<a>
implement
{a}(*tmp*)
funset_getmin_opt = $FS.funset_getmin_opt<a>

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

implement
{a}(*tmp*)
funset_takeoutmax_opt = $FS.funset_takeoutmax_opt<a>
implement
{a}(*tmp*)
funset_takeoutmin_opt = $FS.funset_takeoutmin_opt<a>

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

implement
{a}(*tmp*)
funset_union
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_union<a>(xs1, xs2)
end // end of [funset_union]

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

implement
{a}(*tmp*)
funset_intersect
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_intersect<a>(xs1, xs2)
end // end of [funset_intersect]

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

implement
{a}(*tmp*)
funset_differ
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_differ<a>(xs1, xs2)
end // end of [funset_differ]

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

implement
{a}(*tmp*)
funset_symdiff
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_symdiff<a>(xs1, xs2)
end // end of [funset_symdiff]

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

implement
{a}(*tmp*)
funset_equal
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_equal<a>(xs1, xs2)
end // end of [funset_equal]

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

implement
{a}(*tmp*)
funset_compare
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_compare<a>(xs1, xs2)
end // end of [funset_compare]

(* ****** ****** *)
//
implement
{a}(*tmp*)
funset_is_subset
  (xs1, xs2) = let
//
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
//
in
  $FS.funset_is_subset<a>(xs1, xs2)
end // end of [funset_is_subset]
//
implement
{a}(*tmp*)
funset_is_supset
  (xs1, xs2) = funset_is_subset<a>(xs2, xs1)
//
(* ****** ****** *)

implement
{a}(*tmp*)
funset_foreach(xs) = let
//
var env: void = ((*void*))
//
in
  funset_foreach_env<a><void>(xs, env)
end // end of [funset_foreach]

implement
{a}{env}
funset_foreach_env(xs, env) = let
//
implement
$FS.funset_foreach$fwork<a><env>
  (x, env) = funset_foreach$fwork<a><env>(x, env)
//
in
  $FS.funset_foreach_env<a><env>(xs, env)
end // end of [funset_foreach_env]

implement
{a}(*tmp*)
funset_foreach_cloref
  (xs, fwork) = let
//
var env: void = ((*void*))
//
implement
(env)(*tmp*)
$FS.funset_foreach$fwork<a><env>(x, env) = fwork(x)
//
in
  $FS.funset_foreach_env<a><void> (xs, env)
end // end of [funset_foreach_cloref]

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

implement
{a}(*tmp*)
funset_tabulate_cloref
  {n}(n, fopr) = let
//
implement
$FS.funset_tabulate$fopr<a>(i) = fopr($UN.cast{natLt(n)}(i))
//
in
  $FS.funset_tabulate<a> (n)
end // end of [funset_tabulate]

(* ****** ****** *)
//
implement
{a}(*tmp*)
funset_listize
  (xs) = (
//
$effmask_wrt
(
  list0_of_list_vt{a}($FS.funset_listize<a>(xs))
) (* $effmask_wrt *)
//
) (* funset_listize *)
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
funset_streamize
  (xs) = $effmask_wrt($FS.funset_streamize<a>(xs))
//
(* ****** ****** *)
//
implement
{a}(*tmp*)
funset_make_module
  ((*void*)) = $rec
{
//
nil = funset_nil{a}
,
sing = funset_sing<a>
,
make_list = funset_make_list<a>
,
size = funset_size<a>
,
is_nil = funset_is_nil{a}
,
isnot_nil = funset_isnot_nil{a}
,
insert= funset_insert<a>
,
remove= funset_remove<a>
,
union= funset_union<a>
,
intersect= funset_intersect<a>
,
listize = funset_listize<a>
,
streamiize = funset_streamize<a>
//
} (* end of [funset_make_module] *)
//
(* ****** ****** *)

(* end of [funset.dats] *)
(***********************************************************************)
(*                                                                     *)
(*                         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: Hongwei Xi *)
(* Authoremail: gmhwxiATgmailDOTcom *)
(* Start time: August, 2013 *)

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

staload
UN = "prelude/SATS/unsafe.sats"

(* ****** ****** *)
//
staload HT =
"libats/SATS/hashtbl_chain.sats"
//
(* ****** ****** *)

staload "libats/ML/SATS/basis.sats"

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

staload "libats/ML/SATS/list0.sats"

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

staload "libats/SATS/hashfun.sats"
staload "libats/ML/SATS/hashtblref.sats"

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

(*
implement
{key}(*tmp*)
hash_key = ghash_val<key>
*)

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

implement
{key}(*tmp*)
equal_key_key = gequal_val_val<key>

(* ****** ****** *)
//
implement
hash_key<int> (key) = let
  val key = $UN.cast{uint32}(key)
in
  $UN.cast{ulint}(inthash_jenkins<>(key))
end // end of [hash_key<int>]
//
implement
hash_key<uint> (key) = let
  val key = $UN.cast{uint32}(key)
in
  $UN.cast{ulint}(inthash_jenkins<>(key))
end // end of [hash_key<uint>]
//
(* ****** ****** *)
//
// HX: 31 and 37 are top choices
//
implement
hash_key<string> (key) =
  string_hash_multiplier (31UL, 31415926536UL, key)
//
(* ****** ****** *)
//
implement
{key}(*tmp*)
$HT.hash_key = hash_key<key>
//
implement
{key}(*tmp*)
$HT.equal_key_key = equal_key_key<key>
//
(* ****** ****** *)
//
extern
castfn
hashtbl_encode
  {key,itm:t0p}
(
  $HT.hashtbl(key, INV(itm))
) : hashtbl(key, itm)
//
extern
castfn
hashtbl_decode
  {key,itm:t0p}
  (hashtbl(key, INV(itm))): $HT.hashtbl(key, itm)
//
(* ****** ****** *)

#define htencode hashtbl_encode
#define htdecode hashtbl_decode

(* ****** ****** *)
//
implement
{key,itm}
hashtbl_make_nil (cap) =
  htencode($HT.hashtbl_make_nil<key,itm> (cap))
//
(* ****** ****** *)

implement{}
hashtbl_get_size
  (tbl) = nitm where
{
//
val tbl = htdecode (tbl)
val nitm = $HT.hashtbl_get_size (tbl)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_get_size] *)

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

implement{}
hashtbl_get_capacity
  (tbl) = cap where
{
//
val tbl = htdecode (tbl)
val cap = $HT.hashtbl_get_capacity (tbl)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_get_capacity] *)

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

implement
{key,itm}
hashtbl_search
  (tbl, k) = opt where
{
//
val tbl = htdecode (tbl)
val opt = $HT.hashtbl_search_opt (tbl, k)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_search] *)

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

implement
{key,itm}
hashtbl_search_ref
  (tbl, k) = cptr where
{
//
val tbl = htdecode (tbl)
val cptr = $HT.hashtbl_search_ref (tbl, k)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_search_ref] *)

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

implement
{key,itm}
hashtbl_insert
  (tbl, k, x) = opt where
{
//
val tbl = htdecode (tbl)
val opt = $HT.hashtbl_insert_opt<key,itm> (tbl, k, x)
prval () = $UN.cast2void (tbl)
//
} (* hashtbl_insert *)

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

implement
{key,itm}
hashtbl_insert_any
  (tbl, k, x) = () where
{
//
val tbl = htdecode (tbl)
val () = $HT.hashtbl_insert_any<key,itm> (tbl, k, x)
prval () = $UN.cast2void (tbl)
//
} (* hashtbl_insert_any *)

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

implement
{key,itm}
hashtbl_takeout
  (tbl, k) = opt where
{
//
val tbl = htdecode (tbl)
val opt = $HT.hashtbl_takeout_opt (tbl, k)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_takeout] *)

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

implement
{key,itm}
hashtbl_remove
  (tbl, k) = ans where
{
//
val tbl = htdecode (tbl)
val ans = $HT.hashtbl_remove (tbl, k)
prval () = $UN.cast2void (tbl)
//
} (* end of [hashtbl_remove] *)

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

implement
{key,itm}
hashtbl_takeout_all
  (tbl) = kxs where
{
//
val tbl = htdecode (tbl)
val kxs = $HT.hashtbl_takeout_all (tbl)
prval () = $UN.cast2void (tbl)
val kxs = list0_of_list_vt{(key,itm)}(kxs)
//
} (* end of [hashtbl_takeout_all] *)

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

implement
{key,itm}
fprint_hashtbl
  (out, tbl) = let
//
implement
$HT.fprint_hashtbl$sep<> = fprint_hashtbl$sep<>
implement
$HT.fprint_hashtbl$mapto<> = fprint_hashtbl$mapto<>
//
val tbl = htdecode (tbl)
val () = $HT.fprint_hashtbl (out, tbl)
prval () = $UN.cast2void (tbl)
//
in
  // nothing
end // end of [fprint_hashtbl]

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

implement{}
fprint_hashtbl$sep (out) = fprint (out, "; ")
implement{}
fprint_hashtbl$mapto (out) = fprint (out, "->")

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

implement
{key,itm}
fprint_hashtbl_sep_mapto
  (out, tbl, sep, mapto) = let
//
implement
fprint_hashtbl$sep<> (out) = fprint (out, sep)
implement
fprint_hashtbl$mapto<> (out) = fprint (out, mapto)
//
in
  fprint_hashtbl<key,itm>(out, tbl)
end // end of [fprint_hashtbl_sep_mapto]

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

implement
{key,itm}
hashtbl_foreach_cloref
  (tbl, fwork) = () where
{
//
var env: void = ((*void*))
//
implement
(env)(*tmp*)
$HT.hashtbl_foreach$fwork<key,itm><env> (k, x, env) = fwork(k, x)
//
val tbl = htdecode (tbl)
val ((*void*)) = $HT.hashtbl_foreach_env<key,itm><void> (tbl, env)
prval ((*void*)) = $UN.cast2void (tbl)
//
} (* end of [hashtbl_foreach_cloref] *)

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

implement
{key,itm}
hashtbl_listize1
  (tbl) = kxs where
{
//
typedef ki = @(key, itm)
//
val tbl = htdecode (tbl)
val kxs = $HT.hashtbl_listize1 (tbl)
prval () = $UN.cast2void (tbl)
val kxs = list0_of_list_vt{(key,itm)}(kxs)
//
} (* end of [hashtbl_listize1] *)

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

(* end of [hashtblref.dats] *)