#define ATS_PACKNAME "ATSLIB.libats"
typedef
cfun0(b:vt0p) = () -<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
list0_t0ype_type
(
a: t0ype+
) =
| list0_nil of
()
| list0_cons of
(a, list0_t0ype_type(a))
datavtype
list0_vt0ype_vtype
(
a: vt0ype+
) =
| list0_vt_nil of
()
| list0_vt_cons of
(a, list0_vt0ype_vtype(a))
#define nil0 list0_nil
#define cons0 list0_cons
#define nil0_vt list0_vt_nil
#define cons0_vt list0_vt_cons
typedef
list0(a:t0ype) = list0_t0ype_type(a)
vtypedef
list0_vt(a:vt0ype) = list0_vt0ype_vtype(a)
datatype
option0_t0ype_type
(
a: t0ype+
) =
| None0 of () | Some0 of (a)
datavtype
option0_vt0ype_vtype
(
a: vt0ype+
) =
| None0_vt of () | Some0_vt of (a)
typedef
option0(a:t0ype) = option0_t0ype_type(a)
vtypedef
option0_vt(a:vt0ype) = option0_vt0ype_vtype(a)
abstype
array0_vt0ype_type
(a: vt0ype) = ptr
typedef
array0
(a:vt0ype) = array0_vt0ype_type(a)
abstype
matrix0_vt0ype_type
(a: vt0ype) = ptr
typedef
matrix0
(a:vt0ype) = matrix0_vt0ype_type(a)
abstype strarr_type = ptr
typedef strarr = strarr_type
abstype
dynarray_type(a:vt0ype) = ptr
typedef
dynarray(a:vt0ype) = dynarray_type(a)
abstype
hashtbl_type
(key:t0ype, itm:t0ype+) = ptr
typedef
hashtbl
( key:t0ype
, itm:t0ype) = hashtbl_type(key, itm)
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)
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
#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
g0ofg1_list
{a:t@ype}
(List(INV(a))):<> list0(a)
castfn
g1ofg0_list
{a:t@ype}
(list0(INV(a))):<> List0(a)
overload g0ofg1 with g0ofg1_list
overload g1ofg0 with g1ofg0_list
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)
fun{a:t0p}
list0_tuple_0(): list0(a)
fun{a:t0p}
list0_tuple_1(x0: a): list0(a)
fun{a:t0p}
list0_tuple_2(x0: a, x1: a): list0(a)
fun{a:t0p}
list0_tuple_3(x0: a, x1: a, x2: a): list0(a)
fun{a:t0p}
list0_tuple_4
(x0: a, x1: a, x2: a, x3: a): list0(a)
fun{a:t0p}
list0_tuple_5
(x0: a, x1: a, x2: a, x3: a, x4: a): list0(a)
fun{a:t0p}
list0_tuple_6
(x0: a, x1: a, x2: a, x3: a, x4: a, x5: a): list0(a)
symintr list0_tuple
overload
list0_tuple with list0_tuple_0
overload
list0_tuple with list0_tuple_1
overload
list0_tuple with list0_tuple_2
overload
list0_tuple with list0_tuple_3
overload
list0_tuple with list0_tuple_4
overload
list0_tuple with list0_tuple_5
overload
list0_tuple with list0_tuple_6
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
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_opt with list0_head_opt of 0
overload tail_opt with list0_tail_opt 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
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)), i0: int):<!exn> (a)
fun{a:t0p}
list0_nth_opt
(xs: list0(INV(a)), i0: int):<> Option_vt(a)
fun{a:t0p}
list0_get_at_exn
(xs: list0(INV(a)), i0: int):<!exn> (a)
fun{a:t0p}
list0_get_at_opt
(xs: list0(INV(a)), i0: int):<> Option_vt(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):<> Option_vt(list0(a))
fun{a:t0p}
list0_fexch_at_exn
(list0(INV(a)), i0: int, x0: &a >> a):<!exnwrt> list0(a)
fun{a:t0p}
list0_fexch_at_opt
(list0(INV(a)), i0: int, x0: &a >> a):<!wrt> 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
fun{a:t0p}
fprint_list0_sep
(
out: FILEref, xs: list0(INV(a)), sep: string
) : void
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
overload fprint with fprint_listlist0_sep
fun{a:t0p}
list0_insert_at_exn
(
SHR(list0(INV(a))), i: int, x: (a)
) :<!exn> list0(a)
fun{a:t0p}
list0_remove_at_exn
(SHR(list0(INV(a))), int):<!exn> list0(a)
fun{a:t0p}
list0_takeout_at_exn
(
xs: SHR(list0(INV(a))), i: int, x: &a? >> a
) :<!exnwrt> list0(a)
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
overload append with list0_append
overload .append with list0_append
fun
{a:t0p}
list0_extend
(xs: NSH(list0(INV(a))), y0: a):<> list0(a)
macdef list0_snoc = list0_extend
overload extend with list0_extend
overload .extend with list0_extend
fun
{a:t0p}
mul_int_list0
(
m0: intGte(0), xs: NSH(list0(INV(a)))
) :<> list0(a)
fun{a:t0p}
list0_reverse
(xs: list0(INV(a))):<> list0(a)
overload reverse with list0_reverse
overload .reverse with list0_reverse
fun{a:t0p}
list0_reverse_append
(xs: list0(INV(a)), ys: list0(a)):<> list0(a)
macdef
list0_revapp = list0_reverse_append
overload revapp with 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)
fun{a:t0p}
list0_drop_exn
(xs: SHR(list0(INV(a))), i: int):<!exn> list0(a)
fun
{a:t0p}
{res:t0p}
list0_cata
( xs: list0(INV(a))
, f_nil: cfun0(res), f_cons: cfun2(a, list0(a), res)
) : (res)
fun
{a:t0p}
list0_app
(
xs: list0(INV(a)), fwork: cfun(a, void)
) : void
fun{a:t0p}
list0_foreach
(
xs: list0(INV(a)), fwork: cfun(a, void)
) : void
fun{a:t0p}
list0_foreach_method
(
xs: list0(INV(a))) (fwork: cfun(a, void)
) : void
overload .foreach with list0_foreach_method
fun{a:t0p}
list0_rforeach
(
xs: list0(INV(a)), fwork: cfun(a, void)
) : void
fun{a:t0p}
list0_rforeach_method
(
xs: list0(INV(a))) (fwork: cfun(a, void)
) : void
overload .rforeach with list0_rforeach_method
fun{a:t0p}
list0_iforeach
(
xs: list0(INV(a)), fwork: cfun2(intGte(0), a, void)
) : intGte(0)
fun{a:t0p}
list0_iforeach_method
(
xs: list0(INV(a)))(fwork: cfun2(intGte(0), a, void)
) : intGte(0)
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
fun{a1,a2:t0p}
list0_foreach2_eq
(
xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, fwork: cfun2(a1, a2, void), sgn: &int? >> int
) : void
fun{
res:t0p}{a:t0p
} list0_foldleft
(
xs: list0(INV(a)), ini: res, fopr: cfun2(res, a, res)
) : res
fun{
res:t0p}{a:t0p
} list0_foldleft_method
(
xs: 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
(
xs: list0(INV(a)), ini: res, fopr: cfun3(res, int, a, res)
) : res
fun{
res:t0p}{a:t0p
} list0_ifoldleft_method
(
xs: list0(INV(a)), TYPE(res))(ini: res, fopr: cfun3(res, int, a, res)
) : res
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
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
(
xs: list0(INV(a)), TYPE(res))(fopr: cfun2(a, res, res), snk: res
) : res
overload .foldright with list0_foldright_method
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
fun
{a:t0p}
list0_iexists_method
(
xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool)
) : bool
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
fun
{a1,a2:t0p}
list0_exists2_eq
(
xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool), sgn: &int? >> int
) : bool
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
fun
{a:t0p}
list0_iforall_method
(
xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool)
) : bool
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
fun
{a1,a2:t0p}
list0_forall2_eq
(
xs1: list0(INV(a1))
, xs2: list0(INV(a2))
, pred: cfun2(a1, a2, bool), sgn: &int? >> int
) : bool
fun
{a:t0p}
list0_equal
(
xs1: list0(INV(a))
, xs2: list0(INV(a)), eqfn: cfun2(a, a, bool)
) : bool
fun
{a:t0p}
list0_compare
(
xs1: list0(INV(a))
, xs2: list0(INV(a)), cmpfn: cfun2(a, a, int)
) : (int)
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)
fun
{a:t0p}
list0_find_suffix
(
xs: list0(INV(a)), pred: cfun(list0(a), bool)
) : list0(a)
fun
{a:t0p}
list0_skip_while
(
xs: list0(INV(a)), pred: cfun(a, bool)
) : list0(a)
fun
{a:t0p}
list0_skip_until
(
xs: list0(INV(a)), pred: cfun(a, bool)
) : list0(a)
fun
{a:t0p}
list0_take_while
(
xs: list0(INV(a)), pred: cfun(a, bool)
) : list0(a)
fun
{a:t0p}
list0_take_until
(
xs: list0(INV(a)), pred: cfun(a, bool)
) : list0(a)
fun{
a,b:t0p
} list0_assoc_exn
(
list0@(INV(a), b), x0: a, eq: cfun(a, a, bool)
) : (b)
fun{
a,b:t0p
} list0_assoc_opt
(
list0@(INV(a), b), x0: a, eq: cfun(a, a, bool)
) : Option_vt (b)
fun
{a:t0p}
list0_filter
(xs: list0(INV(a)), pred: cfun(a, bool)): list0(a)
fun
{a:t0p}
list0_filter_method
(xs: 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)
fun
{a:t0p}
{b:t0p}
list0_mapopt
(
xs: list0(INV(a)), fopr: cfun(a, Option_vt(b))
) : list0(b)
fun
{a:t0p}
{b:t0p}
list0_map_method
(
xs: list0(INV(a)), TYPE(b))(fopr: cfun(a, b)
) : list0(b)
fun
{a:t0p}
{b:t0p}
list0_mapopt_method
(
xs: list0(INV(a)), TYPE(b))(fopr: cfun(a, Option_vt(b))
) : list0(b)
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_mapjoin
(
xs: list0(INV(a)), fopr: cfun(a, list0(b))
) : list0(b)
fun
{a:t0p}
{b:t0p}
list0_mapjoin_method
(
xs: list0(INV(a)))(fopr: cfun(a, list0(b))
) : list0(b)
overload .mapjoin with list0_mapjoin_method
fun
{a:t0p}
{b:t0p}
list0_imap
(list0(INV(a)), fopr: cfun2(int, a, b)): list0(b)
fun
{a:t0p}
{b:t0p}
list0_imapopt
(list0(INV(a)), fopr: cfun2(int, a, Option_vt(b))): list0(b)
fun
{a:t0p}
{b:t0p}
list0_imap_method
(list0(INV(a)), TYPE(b))(fopr: cfun2(int, a, b)): list0(b)
fun
{a:t0p}
{b:t0p}
list0_imapopt_method
(list0(INV(a)), TYPE(b))(fopr: cfun2(int, a, Option_vt(b))): list0(b)
overload .imap with list0_imap_method
overload .imapopt with list0_imapopt_method
fun{
a1,
a2:t0p}{b:t0p
} list0_map2
(
list0(INV(a1)), list0(INV(a2)), fopr: cfun2(a1, a2, b)
) : list0(b)
fun{
a1,
a2:t0p}{b:t0p
} list0_imap2
(
list0(INV(a1)), list0(INV(a2)), fopr: cfun3(int, a1, a2, b)
) : list0(b)
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)
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)
fun
{x:t0p}
list0_choose2_foreach
(
list0(INV(x)), fwork: cfun2(x, x, void)
) : void
fun
{x:t0p}
list0_choose2_foreach_method
(
list0(INV(x))) (fwork: cfun2(x, x, void)
) : void
overload
.choose2_foreach with list0_choose2_foreach_method
fun{
x,y:t0p
} list0_xprod2_foreach
( list0(INV(x))
, list0(INV(y)), fwork: cfun2(x, y, void)
) : void
fun
{x,y:t0p}
list0_xprod2_foreach_method
(
list0(INV(x))
, list0(INV(y)))(fwork: cfun2(x, y, void)
) : void
fun{
x,y:t0p
} list0_xprod2_iforeach
(
list0(INV(x))
, list0(INV(y))
, fwork: cfun4(intGte(0), x, intGte(0), y, void)
) : void
fun
{x,y:t0p}
list0_xprod2_iforeach_method
(
list0(INV(x)), list0(INV(y))
)
(
fwork: cfun4(intGte(0), x, intGte(0), y, void)
) : void
overload
.xprod2_foreach with list0_xprod2_foreach_method
overload
.xprod2_iforeach with list0_xprod2_iforeach_method
fun{a:t0p}
streamize_list0_elt
(list0(INV(a))):<!wrt> stream_vt(a)
fun{a:t0p}
un_streamize_list0_elt
(stream_vt(INV(a))):<!wrt> list0(a)
fun{a:t0p}
streamize_list0_suffix
(list0(INV(a))):<!wrt> stream_vt(list0(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,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)
fun{a:t0p}
list0_quicksort
(NSH(list0(INV(a))), cmp: (a, a) -<cloref> int):<> list0(a)
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
%{#
#include \
"libats/ML/CATS/array0.cats"
%}
staload "libats/ML/SATS/basis.sats"
typedef SHR(a:type) = a
typedef NSH(a:type) = a
#if(0)
abstype
array0_vt0ype_type
(a: vt@ype) = ptr
stadef array0 = array0_vt0ype_type
#endif
fun
{a:t0p}
array0_tuple_0(): array0(a)
fun
{a:t0p}
array0_tuple_1(x0: a): array0(a)
fun
{a:t0p}
array0_tuple_2(x0: a, x1: a): array0(a)
fun
{a:t0p}
array0_tuple_3(x0: a, x1: a, x2: a): array0(a)
fun
{a:t0p}
array0_tuple_4
(x0: a, x1: a, x2: a, x3: a): array0(a)
fun
{a:t0p}
array0_tuple_5
(x0: a, x1: a, x2: a, x3: a, x4: a): array0(a)
fun
{a:t0p}
array0_tuple_6
(x0: a, x1: a, x2: a, x3: a, x4: a, x5: a): array0(a)
symintr array0_tuple
overload
array0_tuple with array0_tuple_0
overload
array0_tuple with array0_tuple_1
overload
array0_tuple with array0_tuple_2
overload
array0_tuple with array0_tuple_3
overload
array0_tuple with array0_tuple_4
overload
array0_tuple with array0_tuple_5
overload
array0_tuple with array0_tuple_6
fun{}
array0_of_arrszref
{a:vt0p}(arrszref(a)):<> array0(a)
fun{}
arrszref_of_array0
{a:vt0p}(A: array0(a)):<> arrszref(a)
fun{}
array0_make_arrpsz
{a:vt0p}{n:int}
(psz: arrpsz(INV(a), n)):<!wrt> array0(a)
fun{}
array0_make_arrayref
{a:vt0p}{n:int}
(Arf: arrayref(a, n), n: size_t(n)):<!wrt> array0(a)
symintr array0
overload array0 with array0_make_arrpsz
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_length
{a:vt0p}(A: array0(a)):<> intGte(0)
fun{}
array0_get_refsize
{a:vt0p}
(
A : array0(a)
) :<> [n:nat] (arrayref(a, n), size_t(n))
symintr
array0_make_elt
fun{a:t0p}
array0_make_elt_int
(asz: int, x0: a):<!wrt> array0(a)
fun{a:t0p}
array0_make_elt_size
(asz: size_t, x0: a):<!wrt> array0(a)
overload
array0_make_elt with array0_make_elt_int
overload
array0_make_elt with array0_make_elt_size
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)
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
fun{a:vt0p}
array0_subcirculate
( A: array0(a)
, i: size_t, j: size_t):<!exnrefwrt> void
fun{a:vt0p}
print_array0 (A: array0(a)): void
fun{a:vt0p}
prerr_array0 (A: array0(a)): 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)
overload + with array0_append
overload append with array0_append
overload .append with array0_append
fun
{a:vt0p}
{b:vt0p}
array0_map
(
A0: array0(a), fopr: (&a) -<cloref1> b
) : array0(b)
fun
{a:vt0p}
{b:vt0p}
array0_map_method
(
A0: array0(a), TYPE(b))(fopr: (&a) -<cloref1> b
) : array0(b)
overload .map with array0_map_method
fun
{a:vt0p}
array0_tabulate
{n:int}
(
asz: size_t(n), fopr: (sizeLt(n)) -<cloref1> a
) : array0(a)
fun
{a:vt0p}
array0_tabulate_method_int
{n:nat}
(
asz: int(n))(fopr: (natLt(n)) -<cloref1> a
) : array0(a)
fun
{a:vt0p}
array0_tabulate_method_size
{n:int}
(
asz: size_t(n))(fopr: (sizeLt(n)) -<cloref1> a
) : array0(a)
overload
.array0_tabulate with array0_tabulate_method_int
overload
.array0_tabulate with array0_tabulate_method_size
fun
{a:vt0p}
array0_find_exn
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : size_t
fun
{a:vt0p}
array0_find_opt
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : Option_vt(size_t)
fun
{a:vt0p}
array0_exists
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : bool
fun
{a:vt0p}
array0_exists_method
(
xs: array0(a))(pred: (&a) -<cloref1> bool
) : bool
overload
.exists with array0_exists_method
fun
{a:t0p}
array0_iexists
( xs: array0(a)
, pred: (size_t, &a) -<cloref1> bool
) : bool
fun
{a:t0p}
array0_iexists_method
(xs: array0(a))
(pred: ( size_t, &a ) -<cloref1> bool
) : bool
overload
.iexists with array0_iexists_method
fun
{a:vt0p}
array0_forall
(
xs: array0(a), pred: (&a) -<cloref1> bool
) : bool
fun
{a:vt0p}
array0_forall_method
(
xs: array0(a)) (pred: (&a) -<cloref1> bool
) : bool
overload
.forall with array0_forall_method
fun
{a:t0p}
array0_iforall
( xs: array0(a)
, pred: (size_t, &a) -<cloref1> bool
) : bool
fun
{a:t0p}
array0_iforall_method
(xs: array0(a))
(pred: ( size_t, &a ) -<cloref1> bool
) : bool
overload
.iforall with array0_iforall_method
fun
{a:vt0p}
array0_foreach
(
A0: array0(a)
, fwork: (&a >> _) -<cloref1> void
) : void
fun
{a:vt0p}
array0_foreach_method
(A0: array0(a))
(fwork: (&a >> _) -<cloref1> void): void
overload
.foreach with array0_foreach_method
fun
{a:vt0p}
array0_iforeach
(
A0: array0(a)
, fwork: (size_t, &a >> _) -<cloref1> void
) : void
fun
{a:vt0p}
array0_iforeach_method
(A0: array0(a))
(fwork: (size_t, &a >> _) -<cloref1> void): void
overload
.iforeach with array0_iforeach_method
fun
{a:vt0p}
array0_rforeach
( A0: array0(a)
, fwork: (&a >> _) -<cloref1> void
) : void
fun
{a:vt0p}
array0_rforeach_method
(A0: array0(a))
(fwork: (&a >> _) -<cloref1> void): void
overload
.rforeach with array0_rforeach_method
fun{
res:vt0p}{a:vt0p
} array0_foldleft
( A0: array0(a)
, ini: res, fopr: (res, &a) -<cloref1> res
) : res
fun{
res:vt0p}{a:vt0p
} array0_foldleft_method
(
A: array0(a), TYPE(res)
)
(
ini: res, fopr: (res, &a) -<cloref1> res
) : res
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
fun{
res:vt0p}{a:vt0p
} array0_ifoldleft_method
(
A: array0(a), TYPE(res)
)
(
ini: res
, fopr: (res, size_t, &a) -<cloref1> res
) : res
overload
.ifoldleft with array0_ifoldleft_method
fun{
a:vt0p}{res:vt0p
} array0_foldright
(
A0: array0(a)
, fopr: (&a, res) -<cloref1> res, snk: res
) : res
fun{
a:vt0p}{res:vt0p
} array0_foldright_method
(
A: array0(a), TYPE(res)
)
(
fopr: (&a, res) -<cloref1> res, snk: res
) : res
overload
.foldright with array0_foldright_method
fun
{a:t0p}
streamize_array0_elt
(A0: 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
overload
[] with array0_get_at_gint
overload
[] with array0_set_at_gint
overload
[] with array0_get_at_guint
overload
[] with array0_set_at_guint
overload size with array0_get_size
overload length with array0_get_length
overload .size with array0_get_size
overload .length with array0_get_length
overload print with print_array0
overload prerr with print_array0
overload fprint with fprint_array0
overload fprint with fprint_array0_sep
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
typedef SHR(a:type) = a
typedef NSH(a:type) = a
#if(0)
abstype
matrix0_vt0ype_type
(a: vt@ype) = ptr
stadef matrix0 = matrix0_vt0ype_type
#endif
fun{}
matrix0_of_mtrxszref
{a:vt0p}(mtrxszref(a)):<> matrix0(a)
fun{}
mtrxszref_of_matrix0
{a:vt0p}(M: matrix0(a)):<> mtrxszref(a)
symintr
matrix0_make_elt
fun{a:t0p}
matrix0_make_elt_int
(nrow: int, ncol: int, init: a):<!wrt> matrix0(a)
fun{a:t0p}
matrix0_make_elt_size
(nrow: size_t, ncol: size_t, init: a):<!wrt> matrix0(a)
overload matrix0_make_elt with matrix0_make_elt_int
overload matrix0_make_elt with matrix0_make_elt_size
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
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
{m,n:int}
( nrow: size_t(m)
, ncol: size_t(n)
, fopr: cfun(sizeLt(m), sizeLt(n), a)
) : matrix0(a)
fun
{a:vt0p}
matrix0_tabulate_method_int
{m,n:nat}
( nrow: int(m)
, ncol: int(n))(fopr: cfun(natLt(m), natLt(n), a)
) : matrix0(a)
fun
{a:vt0p}
matrix0_tabulate_method_size
{m,n:int}
( nrow: size_t(m)
, ncol: size_t(n))(fopr: cfun(sizeLt(m), sizeLt(n), a)
) : matrix0(a)
overload
.matrix0_tabulate with matrix0_tabulate_method_int
overload
.matrix0_tabulate with matrix0_tabulate_method_size
fun
{a:vt0p}
matrix0_foreach
(
M : matrix0(a), fwork: (&a >> _) -<cloref1> void
) : void
fun
{a:vt0p}
matrix0_iforeach
(
M : matrix0(a), fwork: (size_t, size_t, &a >> _) -<cloref1> void
) : void
fun{
res:vt0p}{a:vt0p
} matrix0_foldleft
(
M: matrix0(a), ini: res, fopr: (res, &a) -<cloref1> res
) : res
fun{
res:vt0p}{a:vt0p
} matrix0_ifoldleft
(
M: matrix0(a), ini: res, fopr: (res, size_t, size_t, &a) -<cloref1> res
) : res
overload .nrow with matrix0_get_nrow
overload .ncol with matrix0_get_ncol
overload [] with matrix0_get_at_int of 0
overload [] with matrix0_set_at_int of 0
overload [] with matrix0_get_at_size 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
#define
ATS_PACKNAME
"ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
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{}
intgte_stream
(start: int):<!laz> stream(int)
fun{}
stream_make_intrange_lr
(l: int, r: int):<!laz> stream(int)
fun{}
stream_make_intrange_lrd
(l: int, r: int, d: int):<!laz> stream(int)
overload
intrange_stream with stream_make_intrange_lr
overload
intrange_stream with stream_make_intrange_lrd
fun{
a:t0p}{b:t0p
} stream_map
(
xs: stream(INV(a)), fopr: (a) -<cloref> b
) :<!laz> stream(b)
fun
{a:t0p}{b:t0p}
stream_map_method
(
xs: 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
(
xs: stream(INV(a)), fopr: (intGte(0), a) -<cloref> b
) :<!laz> stream(b)
fun
{a:t0p}{b:t0p}
stream_imap_method
(
xs: 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
(
xs: stream(INV(a)), pred: (a) -<cloref> bool
) :<!laz> stream(a)
fun
{a:t0p}
stream_filter_method
(
xs: stream(INV(a))
)
(
pred: (a) -<cloref> bool
) :<!laz> stream(a)
overload .filter with stream_filter_method
fun{
res:t0p}{x:t0p
} stream_scan
(
stream(INV(x)), ini: res, (res, x) -<cloref> res
) :<!laz> stream(res)
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
(xs: stream(a), fwork: (a) -<cloref1> void): void
fun
{a:t0p}
stream_foreach_method
(xs: stream(INV(a)))(fwork: (a) -<cloref1> void): void
overload .foreach with stream_foreach_method
fun
{a:t0p}
stream_iforeach
( xs: stream(a)
, fwork: (intGte(0), a) -<cloref1> void): void
fun
{a:t0p}
stream_iforeach_method
(xs: stream(INV(a)))
(fwork: (intGte(0), a) -<cloref1> void): void
overload .iforeach with stream_iforeach_method
fun{
res:vt0p}{a:t0p
} stream_foldleft
(stream(INV(a)), ini: res, fopr: (res, a) -<cloref1> res): res
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
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload
"libats/ML/SATS/basis.sats"
fun
{a:t0p}
stream2list0_vt
(xs: stream_vt(a)):<!wrt> list0(a)
fun
{a:t0p}
stream_vt_make_list0
(xs: list0(a)):<!laz> stream_vt(a)
fun{}
intgte_stream_vt
(start: int):<!laz> stream_vt(int)
fun{}
stream_vt_make_intrange_lr
(l: int, r: int):<!laz> stream_vt(int)
fun{}
stream_vt_make_intrange_lrd
(l: int, r: int, d: int):<!laz> stream_vt(int)
overload
intrange_stream_vt
with
stream_vt_make_intrange_lr
overload
intrange_stream_vt
with
stream_vt_make_intrange_lrd
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
#define ATS_PACKNAME "ATSLIB.libats.ML"
#define ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
typedef SHR(a:type) = a
typedef NSH(a:type) = a
typedef charlst0 = list0 (char)
typedef stringlst0 = list0 (string)
fun
fileref_get_line_charlst(filr: FILEref): charlst0
fun
fileref_get_lines_charlstlst(filr: FILEref): list0(charlst0)
fun
fileref_get_line_string(filr: FILEref): string
fun
fileref_get_lines_stringlst(filr: FILEref): stringlst0
fun{}
filename_get_lines_stringlst_opt(path: string): Option_vt(stringlst0)
fun{}
streamize_fileref_char
(inp: FILEref): stream_vt(char)
fun{}
streamize_fileptr_char
(inp: FILEptr1): stream_vt(char)
fun{}
streamize_fileref_line
(inp: FILEref): stream_vt(string)
fun{}
streamize_fileptr_line
(inp: FILEptr1): stream_vt(string)
fun{}
streamize_fileref_word
(inp: FILEref): stream_vt(string)
fun{}
streamize_fileptr_word
(inp: FILEptr1): stream_vt(string)
fun{}
streamize_filename_char
(fname: string): streamopt_vt(char)
fun{}
streamize_filename_line
(fname: string): streamopt_vt(string)
fun{}
streamize_filename_word
(fname: string): streamopt_vt(string)
fun
dirname_get_fnamelst(dirname: string): list0(string)
fun{}
streamize_dirname_fname(dirname: string): stream_vt(string)
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
fun{}
int_repeat_lazy
(n: int, f0: lazy(void)): void
fun{}
int_repeat_cloref
(n: int, f0: cfun0(void)): void
fun{}
int_repeat_method
(n: int)(f0: cfun0(void)): void
overload * with int_repeat_lazy
overload repeat with int_repeat_lazy
overload repeat with int_repeat_cloref
overload .repeat with int_repeat_method
fun{}
int_forall_cloref
(n: int, f0: cfun1(int, bool)): bool
fun{}
int_forall_method
(n: int)(f0: cfun1(int, bool)): bool
overload .forall with int_forall_method
fun{}
int_foreach_cloref
(n: int, f0: cfun1(int, void)): void
fun{}
int_foreach_method
(n: int)(f0: cfun1(int, void)): void
overload .foreach with int_foreach_method
fun{}
int_rforeach_cloref
(n: int, f0: cfun1(int, void)): void
fun{}
int_rforeach_method
(n: int)(f0: cfun1(int, void)): void
overload .rforeach with int_rforeach_method
fun
{res:vt0p}
int_foldleft_cloref
(n: int, ini: res, f0: cfun2(res, int, res)): res
fun
{res:vt0p}
int_foldleft_method
(int, TYPE(res))(ini: res, f0: cfun2(res, int, res)): res
overload .foldleft with int_foldleft_method
fun
{res:vt0p}
int_foldright_cloref
(n: int, f0: cfun2(int, res, res), snk: res): res
fun
{res:vt0p}
int_foldright_method
(int, TYPE(res))(f0: cfun2(int, res, res), snk: res): res
overload .foldright with int_foldright_method
fun{}
intrange_forall_cloref
(l: int, r: int, f0: cfun1(int, bool)): bool
fun{}
intrange_forall_method
(lr: @(int, int))(f0: cfun1(int, bool)): bool
overload .forall with intrange_forall_method
fun{}
intrange_foreach_cloref
(l: int, r: int, f0: cfun1(int, void)): void
fun{}
intrange_foreach_method
(lr: @(int, int))(f0: cfun1(int, void)): void
overload .foreach with intrange_foreach_method
fun{}
intrange_rforeach_cloref
(l: int, r: int, f0: cfun1(int, void)): void
fun{}
intrange_rforeach_method
(lr: @(int, int))(f0: cfun1(int, void)): void
overload .rforeach with intrange_rforeach_method
fun
{res:vt0p}
intrange_foldleft_cloref
(
l: int, r: int, ini: res, f0: cfun2(res, int, res)
) : res
fun
{res:vt0p}
intrange_foldleft_method
((int, int), TYPE(res))(ini: res, f0: cfun2(res, int, res)): res
overload .foldleft with intrange_foldleft_method
fun
{res:vt0p}
intrange_foldright_cloref
(
l: int, r: int, f0: cfun2(int, res, res), snk: res
) : res
fun
{res:vt0p}
intrange_foldright_method
((int, int), TYPE(res))(f0: cfun2(int, res, res), snk: res): res
overload .foldright with intrange_foldright_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))(f0: 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))(f0: 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))(f0: 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))(f0: 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, f0: cfun2(int, int, void)): void
fun{}
intrange2_foreach_cloref
(l1:int, r1:int, l2:int, r2:int, f0: cfun2(int,int,void)): void
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
abstype
map_type
(
key:t@ype
, itm:t0ype+
) = ptr
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{
key,itm:t0p
} funmap_size
(map: map(key, INV(itm))):<> size_t
overload size with funmap_size
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
overload iseqz with funmap_is_nil
overload isneqz with funmap_isnot_nil
fun{
key,itm:t0p
} funmap_search
(
map: map(key, INV(itm)), k0: key
) : Option_vt(itm)
fun{
key,itm:t0p
} funmap_insert
(
&map(key, INV(itm)) >> _, key, itm
) : Option_vt(itm)
fun{
key,itm:t0p
} funmap_takeout
(
map: &map(key, INV(itm)) >> _, k0: key
) : Option_vt(itm)
fun{
key,itm:t0p
} funmap_remove
(map: &map(key, INV(itm)) >> _, k0: key): bool
fun{}
fprint_funmap$sep
(out: FILEref): void
fun{}
fprint_funmap$mapto
(out: FILEref): void
fun
{key
,itm:t0p}
fprint_funmap
(out: FILEref, map: map(key, itm)): void
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
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>)
,
streamize = $d2ctype(funmap_streamize<key,itm>)
}
fun
{key:t0p
;itm:t0p}
funmap_make_module(): map_modtype(key,itm)
#define ATS_PACKNAME "ATSLIB.libats.ML"
#define ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
abstype
set_type
(
a:t@ype+
) = ptr
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
fun{}
fprint_funset$sep(out: FILEref): void
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
fun{a:t0p}
funset_remove
(xs: &set(INV(a)) >> _, x0: a): bool
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
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
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>)
,
streamize = $d2ctype(funset_streamize<elt>)
}
fun
{a:t@ype}
funset_make_module(): set_modtype(a)
#define
ATS_PACKNAME "ATSLIB.libats.ML"
#define
ATS_EXTERN_PREFIX "atslib_ML_"
staload "libats/ML/SATS/basis.sats"
typedef
hashtbl
(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)): sizeGte(0)
fun{}
hashtbl_get_capacity
{key,itm:t0p}(hashtbl(key, itm)): sizeGte(1)
fun{
key,itm:t0p
} hashtbl_search
(hashtbl(key, INV(itm)), key): Option_vt(itm)
fun{
key,itm:t0p
} hashtbl_search_ref
(tbl: hashtbl(key, INV(itm)), k: key): cPtr0(itm)
fun{
key,itm:t0p
} hashtbl_insert
(hashtbl(key, INV(itm)), key, itm): Option_vt(itm)
fun{
key,itm:t0p
} hashtbl_insert_any
(hashtbl(key, INV(itm)), key, itm): void
fun{
key,itm:t0p
} hashtbl_takeout
(kxs: hashtbl(key, INV(itm)), k0: key): Option_vt(itm)
fun{
key,itm:t0p
} hashtbl_remove
(kxs: hashtbl(key, INV(itm)), key): bool
fun{
key,itm:t0p
} hashtbl_takeout_all
(kxs: hashtbl(key, INV(itm))): list0(@(key, itm))
fun{
key,itm:t@ype
} fprint_hashtbl
(out: FILEref, tbl: hashtbl(key, INV(itm))): void
overload fprint with fprint_hashtbl
fun{}
fprint_hashtbl$sep (out: FILEref): void
fun{}
fprint_hashtbl$mapto (out: FILEref): void
fun{
key,itm:t@ype
} fprint_hashtbl_sep_mapto
( out: FILEref
, tbl: hashtbl(key, INV(itm)), sep: string, mapto: string
) : void
fun{
key,itm:t0p
} hashtbl_foreach
(tbl: hashtbl(key, INV(itm))): void
fun
{key:t0p
;itm:t0p}
{env:vt0p}
hashtbl_foreach_env
(hashtbl(key, INV(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
(
hashtbl(key, INV(itm)), fwork: (key, &itm >> _) -<cloref1> void
) : void
fun{
key,itm:t0p
} hashtbl_listize0
(kxs: hashtbl(key, INV(itm))): list0(@(key, itm))
fun{
key,itm:t0p
} hashtbl_listize1
(kxs: hashtbl(key, INV(itm))): list0(@(key, itm))
#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/list0_vt.sats"
implement
{a}
list0_tuple_0() = list0_nil()
implement
{a}
list0_tuple_1(x0) = g0ofg1($list{a}(x0))
implement
{a}
list0_tuple_2(x0, x1) = g0ofg1($list{a}(x0, x1))
implement
{a}
list0_tuple_3(x0, x1, x2) = g0ofg1($list{a}(x0, x1, x2))
implement
{a}
list0_tuple_4
(x0, x1, x2, x3) = g0ofg1($list{a}(x0, x1, x2, x3))
implement
{a}
list0_tuple_5
(x0, x1, x2, x3, x4) = g0ofg1($list{a}(x0, x1, x2, x3, x4))
implement
{a}
list0_tuple_6
(x0, x1, x2, x3, x4, x5) = g0ofg1($list{a}(x0, x1, x2, x3, x4, x5))
implement
{a}
list0_make_sing(x) =
list0_cons{a}(x, list0_nil)
implement
{a}
list0_make_pair(x1, x2) =
list0_cons{a}(x1, list0_cons{a}(x2, list0_nil))
implement
{a}
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))
in
list0_of_list_vt{a}(xs)
end
else let
in
$raise (IllegalArgExn"list0_make_elt:n")
end
end
implement
{}
list0_make_intrange_lr
(l, r) = let
val d = (
if l <= r then 1 else ~1
) : int
in
$effmask_exn(list0_make_intrange_lrd(l, r, d))
end
implement
{}
list0_make_intrange_lrd
(l, r, d) = let
typedef res = list0 (int)
fun loop1
(
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
end else (res := list0_nil)
end
fun loop2
(
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
end else (res := list0_nil)
end
in
$effmask_all
(
if d > 0 then (
if l < r then let
var res: ptr?
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?
val () = loop2 (l, r, d, res) in res
end else list0_nil ()
) else (
$raise
IllegalArgExn("list0_make_intrange_lrd:d")
)
)
end
implement
{a}
list0_make_arrpsz
(psz) =
list0_of_list_vt{a}(list_make_arrpsz(psz))
implement
{a}
print_list0
(xs) = fprint_list0<a> (stdout_ref, xs)
implement
{a}
prerr_list0
(xs) = fprint_list0<a> (stderr_ref, xs)
implement
{a}
fprint_list0
(out, xs) = fprint_list<a> (out, g1ofg0(xs))
implement
{a}
fprint_list0_sep
(out, xs, sep) =
(
fprint_list_sep<a> (out, g1ofg0(xs), sep)
)
implement
{a}
fprint_listlist0_sep
(out, xss, sep1, sep2) =
(
fprint_listlist_sep<a>
(out, $UN.cast{List(List(a))}(xss), sep1, sep2)
)
implement
{a}
list0_is_nil(xs) = (
case+ xs of
| list0_cons _ => false | list0_nil() => true
)
implement
{a}
list0_is_cons(xs) = (
case+ xs of
| list0_cons _ => true | list0_nil() => false
)
implement
{a}
list0_is_empty(xs) = list0_is_nil<a> (xs)
implement
{a}
list0_isnot_empty(xs) = list0_is_cons<a> (xs)
implement
{a}
list0_head_exn
(xs) = let
in
case+ xs of
| list0_cons
(x, _) => (x)
| list0_nil _ =>
$raise ListSubscriptExn()
end
implement
{a}
list0_head_opt
(xs) = let
in
case+ xs of
| list0_nil() => None_vt()
| list0_cons(x, _) => Some_vt{a}(x)
end
implement
{a}
list0_tail_exn
(xs) = let
in
case+ xs of
| list0_cons
(_, xs) => (xs)
| list0_nil _ =>
$raise ListSubscriptExn()
end
implement
{a}
list0_tail_opt
(xs) = let
in
case+ xs of
| list0_nil() => None_vt()
| list0_cons(_, xs) => Some_vt{list0(a)}(xs)
end
implement
{a}
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
implement
{a}
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
implement
{a}
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)))
)
| list0_nil() => $raise ListSubscriptExn()
end
implement
{a}
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
| list0_cons(x, xs) =>
Some_vt(g0ofg1(aux(x, g1ofg0(xs))))
end
implement
{a}
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
)
| list0_nil() =>
(
$raise ListSubscriptExn
)
)
val i0 = g1ofg0_int(i0)
in
if i0 >= 0
then loop(xs, i0)
else $raise ListSubscriptExn
end
implement
{a}
list0_nth_opt
(
xs, i0
) =
$effmask_exn
(
try
Some_vt{a}
(
list0_nth_exn<a>(xs, i0)
)
with ~ListSubscriptExn() => None_vt
)
implement
{a}
list0_get_at_exn
(xs, i0) = list0_nth_exn<a>(xs, i0)
implement
{a}
list0_get_at_opt
(xs, i0) = list0_nth_opt<a>(xs, i0)
implement
{a}
list0_fset_at_exn
(xs, i0, x0) = let
fun
fset
{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, fset(xs, i-1)) else cons0(x0, xs)
)
| list0_nil() => $raise ListSubscriptExn()
)
val i0 = g1ofg0(i0)
in
if i0 >= 0
then fset(xs, i0) else $raise ListSubscriptExn()
end
implement
{a}
list0_fset_at_opt
(
xs, i0, x0
) =
$effmask_exn
(
try
Some_vt{list0(a)}
(
list0_fset_at_exn<a>(xs, i0, x0)
)
with ~ListSubscriptExn() => None_vt()
)
implement
{a}
list0_fexch_at_exn
(xs, i0, x0) = let
val p0 = addr@(x0)
fun
fexch
{i:nat} .<i>.
(
xs: list0(a), i: int(i), visited: List0_vt(a)
) :<!exnwrt> list0(a) =
(
case+ xs of
| list0_cons
(x1, xs) =>
(
if
(i > 0)
then
(
fexch
(xs, i-1, list_vt_cons(x1, visited))
)
else let
val x2 = $UN.ptr0_get<a>(p0)
val () = $UN.ptr0_set<a>(p0, x1)
val x2_xs = g1ofg0(list0_cons(x2, xs))
in
g0ofg1(list_reverse_append1_vt(visited, x2_xs))
end
)
| list0_nil() => let
val () = list_vt_free(visited) in $raise ListSubscriptExn()
end
)
val i0 = g1ofg0(i0)
in
if i0 >= 0
then fexch(xs, i0, list_vt_nil()) else $raise ListSubscriptExn()
end
implement
{a}
list0_fexch_at_opt
(
xs, i0, x0
) = let
val p0 = addr@x0
in
$effmask_exn
(
try
Some_vt{list0(a)}
(
let
val
(pf, fpf | p0) =
$UN.ptr_vtake{a}(p0)
val res =
list0_fexch_at_exn<a>(xs, i0, !p0)
prval () = fpf(pf)
in
res
end
)
with ~ListSubscriptExn() => None_vt()
)
end
implement
{a}
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
val i = g1ofg0_int(i)
in
if
i >= 0
then aux (xs, i, x0)
else $raise IllegalArgExn("list0_insert_at_exn:i")
end
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
| list0_nil () => let
prval () = __assert (x0) in $raise ListSubscriptExn()
end
end
in
implement
{a}
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
implement
{a}
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
end
implement
{a}
list0_length
(xs) =
list_length<a>(g1ofg0(xs))
implement
{a}
list0_append
(xs, ys) = let
val xs = g1ofg0(xs)
and ys = g1ofg0(ys)
in
list0_of_list(list_append<a>(xs, ys))
end
implement
{a}
list0_extend
(xs, x) = let
val xs = g1ofg0(xs)
in
$effmask_wrt
(
list0_of_list_vt(list_extend<a>(xs, x))
)
end
implement
{a}
mul_int_list0
(m, xs) =
$effmask_wrt
(
list0_of_list_vt
(mul_int_list<a>(m, g1ofg0(xs)))
)
implement
{a}
list0_reverse(xs) =
list0_reverse_append<a>(xs, list0_nil)
implement
{a}
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
implement
{a}
list0_concat
(xss) = let
typedef xss = List(List(a))
in
$effmask_wrt
(
list0_of_list_vt{a}
(list_concat<a>($UN.cast{xss}(xss)))
)
end
implement
{a}
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))
in
list0_of_list_vt(res)
end else (
$raise(IllegalArgExn"list0_take_exn:i")
)
end
implement
{a}
list0_drop_exn
(xs, i) = let
val i = g1ofg0_int (i)
val xs = g1ofg0_list (xs)
in
if
(i >= 0)
then
g0ofg1(list_drop_exn<a>(xs, i))
else
$raise(IllegalArgExn"list0_drop_exn:i")
end
implement
{a}{b}
list0_cata
(xs, fnil, fcons) =
(
case+ xs of
| list0_nil() => fnil()
| list0_cons(x, xs) => fcons(x, xs)
)
implement
{a}
list0_app
(xs, fopr) = list0_foreach<a>(xs, fopr)
implement
{a}
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))
)
}
implement
{a}
list0_foreach_method(xs) =
lam(fwork) => list0_foreach<a>(xs, fwork)
implement
{a}
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))
)
}
implement
{a}
list0_rforeach_method(xs) =
lam(fwork) => list0_rforeach<a>(xs, fwork)
implement
{a}
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))
)
in
loop (0, xs)
end
implement
{a}
list0_iforeach_method(xs) =
lam(fwork) => list0_iforeach<a>(xs, fwork)
implement
{a1,a2}
list0_foreach2
(xs1, xs2, fwork) = let
var sgn: int
in
list0_foreach2_eq (xs1, xs2, fwork, sgn)
end
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))
)
)
}
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
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))
)
in
loop (0, xs, ini)
end
implement
{res}{a}
list0_ifoldleft_method(xs, _) =
(
lam(ini, fopr) =>
list0_ifoldleft<res><a>(xs, ini, fopr)
)
implement
{res}{a1,a2}
list0_foldleft2
(
xs1, xs2, ini, fopr
) = let
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))
)
)
)
in
loop(xs1, xs2, ini)
end
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))
}
implement
{a}{res}
list0_foldright_method(xs, _) =
lam(f, snk) => list0_foldright<a><res>(xs, f, snk)
implement
{a}
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)
)
}
implement
{a}
list0_exists_method(xs) =
lam(p) => list0_exists<a>(xs, p)
implement
{a}
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)
)
}
implement
{a}
list0_iexists_method(xs) =
lam(p) => list0_iexists<a> (xs, p)
implement
{a1,a2}
list0_exists2
(xs1, xs2, p0) = let
var sgn: int
in
list0_exists2_eq<a1,a2>(xs1, xs2, p0, sgn)
end
implement
{a1,a2}
list0_exists2_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; false)
| list0_cons _ =>
(sgn := ~1; false)
)
| list0_cons
(x1, xs1) =>
(
case+ xs2 of
| list0_nil() =>
(sgn := 1; false)
| list0_cons
(x2, xs2) =>
(
if pred(x1, x2)
then (sgn := 0; true) else loop(xs1, xs2, sgn)
)
)
)
}
implement
{a}
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
)
}
implement
{a}
list0_forall_method(xs) =
lam(p) => list0_forall<a> (xs, p)
implement
{a}
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
)
}
implement
{a}
list0_iforall_method(xs) =
lam(p) => list0_iforall<a> (xs, p)
implement
{a1,a2}
list0_forall2
(xs1, xs2, p0) = let
var sgn: int
in
list0_forall2_eq<a1,a2>(xs1, xs2, p0, sgn)
end
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)
)
)
)
}
implement
{a}
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
)
)
}
implement
{a}
list0_compare
(
xs1, xs2, cmpfn
) = loop(xs1, xs2) where
{
fun
loop
(
xs1: list0(a), xs2: list0(a)
) : int =
(
case+ xs1 of
| list0_nil() =>
(
case+ xs2 of
| list0_nil() => 0
| list0_cons _ => ~1
)
| list0_cons
(x1, xs1) =>
(
case+ xs2 of
| list0_nil() => (1)
| list0_cons
(x2, xs2) => let
val sgn = cmpfn(x1, x2)
in
if sgn != 0 then sgn else loop(xs1, xs2)
end
)
)
}
implement
{a}
list0_find_exn
(
xs, pred
) = loop(xs) where
{
fun
loop(xs: list0(a)): a =
(
case+ xs of
| list0_nil() =>
$raise NotFoundExn()
| list0_cons(x, xs) =>
if pred(x) then x else loop(xs)
)
}
implement
{a}
list0_find_opt
(
xs, pred
) = loop(xs) where
{
fun
loop
(
xs: list0(a)
) : Option_vt(a) =
case+ xs of
| list0_nil() =>
None_vt
| list0_cons(x, xs) =>
(
if pred(x)
then Some_vt{a}(x) else loop(xs)
)
}
implement
{a}
list0_find_exn_method
(xs) = lam(pred) => list0_find_exn<a>(xs, pred)
implement
{a}
list0_find_opt_method
(xs) = lam(pred) => list0_find_opt<a>(xs, pred)
implement
{a}
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)
)
}
implement
{a}
list0_find_suffix
(
xs, pred
) = loop(xs) where
{
fun
loop(xs: list0(a)): list0(a) =
(
case+ xs of
| list0_nil() =>
list0_nil()
| list0_cons(_, xs2) =>
if pred(xs) then xs else loop(xs2)
)
}
implement
{a}
list0_skip_while
(xs, pred) =
auxmain(xs) where
{
fun
auxmain
(
xs: list0(a)
) : list0(a) =
(
case+ xs of
| list0_nil() =>
list0_nil()
| list0_cons(x0, xs1) =>
if pred(x0) then auxmain(xs1) else xs
)
}
implement
{a}
list0_skip_until
(xs, pred) =
auxmain(xs) where
{
fun
auxmain
(
xs: list0(a)
) : list0(a) =
(
case+ xs of
| list0_nil() =>
list0_nil()
| list0_cons(x0, xs1) =>
if pred(x0) then xs else auxmain(xs1)
)
}
implement
{a}
list0_take_while
(xs, pred) = let
fun
auxmain
(
xs: list0(a), res: List0_vt(a)
) : List0_vt(a) =
(
case+ xs of
| list0_nil() => res
| list0_cons(x0, xs1) =>
if pred(x0)
then auxmain(xs1, list_vt_cons(x0, res)) else res
)
in
list0_vt2t
(g0ofg1(list_vt_reverse(auxmain(xs, list_vt_nil()))))
end
implement
{a}
list0_take_until
(xs, pred) = let
fun
auxmain
(
xs: list0(a), res: List0_vt(a)
) : List0_vt(a) =
(
case+ xs of
| list0_nil() => res
| list0_cons(x0, xs1) =>
if pred(x0)
then res else auxmain(xs1, list_vt_cons(x0, res))
)
in
list0_vt2t
(g0ofg1(list_vt_reverse(auxmain(xs, list_vt_nil()))))
end
implement
{a,b}
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)
}
implement
{a,b}
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
| list0_cons(xy, xys) =>
(
if eq (x0, xy.0)
then Some_vt{b}(xy.1) else loop(xys, x0, eq)
)
}
implement
{a}
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
implement
{a}
list0_filter_method
(xs) = lam(pred) => list0_filter<a>(xs, pred)
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
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_nil () =>
(
res := list_vt_nil ()
)
| 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
end
| ~None_vt() => loop(xs, res)
)
end
var res: ptr
val () = loop (xs, res)
val res = list0_of_list_vt (res)
}
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}
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
implement
{a}{b}
list0_mapjoin
( xs
, fopr
) =
list0_concat<b>
(list0_map<a><list0(b)>(xs, fopr))
implement
{a}{b}
list0_mapjoin_method
(xs) =
lam(fopr) => list0_mapjoin<a><b>(xs, fopr)
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
val ys = list_imap<a><b>(g1ofg0_list(xs))
in
list0_of_list_vt{b}(ys)
end
implement
{a}{b}
list0_imapopt
(xs, fopr) = res where
{
fun loop
(
i0: int
, xs: list0 (a)
, res: &ptr? >> List0_vt(b)
) : void = let
in
case+ xs of
| list0_nil () =>
(
res := list_vt_nil ()
)
| list0_cons
(x, xs) =>
(
case+
fopr(i0, x) of
| ~Some_vt(y) => let
val () =
(
res :=
list_vt_cons{b}{0}(y, _)
)
val+
list_vt_cons(_, res1) = res
val () = loop(i0+1, xs, res1)
prval () = fold@(res)
in
end
| ~None_vt() => loop(i0+1, xs, res)
)
end
var res: ptr
val () = loop(0, xs, res)
val res = list0_of_list_vt(res)
}
implement
{a}{b}
list0_imap_method
(xs, _) =
lam(fopr) => list0_imap<a><b>(xs, fopr)
implement
{a}{b}
list0_imapopt_method
(xs, _) =
lam(fopr) => list0_imapopt<a><b>(xs, fopr)
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
implement
{a1,a2}{b}
list0_imap2
(xs1, xs2, fopr) = let
var _n_: int = 0
val nptr = addr@(_n_)
implement
{a11,a12}{b2}
list_map2$fopr
(x1, x2) = let
val n0 =
$UN.ptr0_get<int>(nptr)
val res =
$UN.castvwtp0{b2}
(fopr(n0, $UN.cast{a1}(x1), $UN.cast{a2}(x2)))
in
$UN.ptr0_set<int>(nptr, n0+1); res
end
in
list0_of_list_vt{b}(list_map2<a1,a2><b>(g1ofg0(xs1), g1ofg0(xs2)))
end
implement
{a}
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
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
implement
{a}
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)
| ~Some_vt(x) => let
val () =
(
res :=
list_vt_cons{a}{0}(x, _)
)
val+list_vt_cons(_, res1) = res
val () = loop (i+1, res1)
prval () = fold@ (res)
in
end
) else
(
res := list_vt_nil()
)
end
var res: ptr
val () = loop (0, res)
val res = list0_of_list_vt (res)
}
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
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
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
implement
{x}
list0_choose2_foreach
(
xs, fwork
) = loop(xs) where
{
fnx
loop(xs: list0(x)): void =
(
case+ xs of
| list0_nil() => ()
| list0_cons
(x, xs) => loop2(x, xs, xs)
)
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
)
}
implement
{x}
list0_choose2_foreach_method(xs) =
lam(fwork) => list0_choose2_foreach<x>(xs, fwork)
implement
{x,y}
list0_xprod2_foreach
(
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))
)
}
implement
{x,y}
list0_xprod2_foreach_method
(xs, ys) =
(
lam(fwork) => list0_xprod2_foreach<x,y>(xs, ys, fwork)
)
implement
{x,y}
list0_xprod2_iforeach
(
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)
)
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))
)
}
implement
{x,y}
list0_xprod2_iforeach_method
(xs, ys) =
(
lam(fwork) => list0_xprod2_iforeach<x,y>(xs, ys, fwork)
)
implement
{a}
streamize_list0_elt
(xs) =
streamize_list_elt<a>(g1ofg0(xs))
implement
{a}
un_streamize_list0_elt
(xs) =
(
list0_of_list_vt{a}(stream2list_vt(xs))
)
implement
{a}
streamize_list0_suffix
(xs) = let
fun
auxmain:
$d2ctype
(
streamize_list0_suffix<a>
) = lam(xs) => $ldelay
(
case+ xs of
| list0_nil() =>
stream_vt_nil()
| list0_cons(x0, xs1) =>
stream_vt_cons(xs, auxmain(xs1))
)
in
auxmain(xs)
end
implement
{a}
streamize_list0_choose2
(xs) = streamize_list_choose2<a>(g1ofg0(xs))
implement
{a}
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)
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
)
)
end
)
else
(
stream_vt_cons(list0_nil, stream_vt_make_nil())
)
) : stream_vt_con(list0(a))
in
$effmask_all(auxmain(xs, n))
end
implement
{a,b}
streamize_list0_zip
(xs, ys) =
streamize_list_zip<a,b>(g1ofg0(xs), g1ofg0(ys))
implement
{a,b}
streamize_list0_cross
(xs, ys) =
streamize_list_cross<a,b>(g1ofg0(xs), g1ofg0(ys))
implement
{a}
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
implement
{a}
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
implement
{a}
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
implement
(a)
fprint_val<list0(a)> = fprint_list0<a>
implement
(a)
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_cons(x, xs) =>
(
case+ ys of
| list0_nil() => 1
| list0_cons(y, ys) => let
val sgn =
gcompare_val_val<a>(x, y)
in
if sgn != 0 then sgn else auxlst(xs, ys)
end
)
)
in
$effmask_all(auxlst(xs, ys))
end
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"
implement
{a}
array0_tuple_0
() = array0($arrpsz{a}())
implement
{a}
array0_tuple_1
(x0) = array0($arrpsz{a}(x0))
implement
{a}
array0_tuple_2
(x0, x1) = array0($arrpsz{a}(x0, x1))
implement
{a}
array0_tuple_3
(x0, x1, x2) = array0($arrpsz{a}(x0, x1, x2))
implement
{a}
array0_tuple_4
(x0, x1, x2, x3) =
array0($arrpsz{a}(x0, x1, x2, x3))
implement
{a}
array0_tuple_5
(x0, x1, x2, x3, x4) =
array0($arrpsz{a}(x0, x1, x2, x3, x4))
implement
{a}
array0_tuple_6
(x0, x1, x2, x3, x4, x5) =
array0($arrpsz{a}(x0, x1, x2, x3, x4, x5))
implement
{}
array0_of_arrszref
{a}(A) = $UN.cast{array0(a)}(A)
implement
{}
arrszref_of_array0
{a}(A) = $UN.cast{arrszref(a)}(A)
implement
{}
array0_get_ref
(A0) = let
val
ASZ =
arrszref_of_array0(A0) in arrszref_get_ref(ASZ)
end
implement
{}
array0_get_size
(A0) = let
val
ASZ =
arrszref_of_array0(A0) in arrszref_get_size(ASZ)
end
implement
{}
array0_get_length
(A0) = sz2i(g1ofg0_uint(array0_get_size<>(A0)))
implement
{}
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
implement
{}
array0_make_arrpsz
(psz) = let
val
ASZ =
arrszref_make_arrpsz(psz) in array0_of_arrszref(ASZ)
end
implement
{}
array0_make_arrayref
(A, n) = let
val
ASZ =
arrszref_make_arrayref(A, n) in array0_of_arrszref(ASZ)
end
implement
{a}
array0_make_elt_int
(asz, x0) = let
val asz = i2sz(max(g1ofg0(asz), 0))
in
array0_of_arrszref(arrszref_make_elt<a>(asz, x0))
end
implement
{a}
array0_make_elt_size
(asz, x0) =
(
array0_of_arrszref(arrszref_make_elt<a>(asz, x0))
)
implement
{a}
array0_make_list
(xs) = let
val xs = g1ofg0(xs)
in
array0_of_arrszref{a}(arrszref_make_list<a>(xs))
end
implement
{a}
array0_make_rlist
(xs) = let
val xs = g1ofg0(xs)
in
array0_of_arrszref{a}(arrszref_make_rlist<a>(xs))
end
implement
{a}
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{a}(A2, ln)
end
implement
{a}
print_array0(A) =
fprint_array0<a>(stdout_ref, A)
implement
{a}
prerr_array0(A) =
fprint_array0<a>(stderr_ref, A)
implement
{a}
fprint_array0(out, A) =
fprint_arrszref<a>(out, arrszref_of_array0(A))
implement
{a}
fprint_array0_sep (out, A, sep) =
fprint_arrszref_sep<a>(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<a>(A0, g0i2u(i))
else
$raise ArraySubscriptExn()
end
implement
{a}{tk}
array0_get_at_guint
(A0, i) = let
in
array0_get_at_size<a>(A0, g0u2u(i))
end
implement
{a}
array0_get_at_size
(A0, i) =
(
arrszref_get_at_size<a>(arrszref_of_array0(A0), i)
)
implement
{a}{tk}
array0_set_at_gint
(A0, i, x) =
(
if i >= 0 then
array0_set_at_size<a>(A0, g0i2u(i), x)
else
$raise ArraySubscriptExn()
)
implement
{a}{tk}
array0_set_at_guint
(A0, i, x) =
(
array0_set_at_size<a>(A0, g0u2u(i), x)
)
implement
{a}
array0_set_at_size
(A0, i, x) =
(
arrszref_set_at_size<a>(arrszref_of_array0(A0), i, x)
)
implement
{a}{tk}
array0_exch_at_gint
(A0, i, x) = let
in
if i >= 0 then
array0_exch_at_size<a>(A0, g0i2u(i), x)
else
$raise ArraySubscriptExn()
end
implement
{a}{tk}
array0_exch_at_guint
(A0, i, x) =
(
array0_exch_at_size<a>(A0, g0u2u(i), x)
)
implement
{a}
array0_exch_at_size
(A0, i, x) =
(
arrszref_exch_at_size(arrszref_of_array0(A0), i, x)
)
implement
{a}
array0_interchange
(A0, i, j) = let
val ASZ =
arrszref_of_array0(A0) in arrszref_interchange(ASZ, i, j)
end
implement
{a}
array0_subcirculate
(A0, i, j) = let
val ASZ =
arrszref_of_array0(A0) in arrszref_subcirculate(ASZ, i, j)
end
implement
{a}
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)
val ASZ2 = arrszref_make_arrayref(A2, asz)
in
array0_of_arrszref{a}(ASZ2)
end
implement
{a}
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) and (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{a}(ASZ12)
end
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
implement
{a}{b}
array0_map_method
(A0, _) = lam(fopr) => array0_map<a>(A0, fopr)
implement
{a}
array0_tabulate
{n}(asz, fopr) = let
implement{a2}
array_tabulate$fopr
(i) = let
val i =
$UN.cast{sizeLt(n)}(i)
in
$UN.castvwtp0{a2}(fopr(i))
end
in
array0_of_arrszref(arrszref_tabulate<a>(asz))
end
implement
{a}
array0_tabulate_method_int
(asz) =
(
lam(fopr) =>
array0_tabulate<a>
(i2sz(asz), lam(i) => fopr(sz2i(i)))
)
implement
{a}
array0_tabulate_method_size
(asz) =
(
lam(fopr) => array0_tabulate<a>(asz, fopr)
)
implement
{a}
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) = ()
val idx = arrayref_foreach<a>(A, asz)
in
if idx < asz then idx else $raise NotFoundExn()
end
implement
{a}
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 _ =
arrayref_foreach_env<a><bool>(A, asz, env)
}
end
implement
{a}
array0_exists_method(A0) =
lam(pred) => array0_exists<a>(A0, pred)
implement
{a}
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 _ =
arrayref_iforeach_env<a><bool>(A, asz, env)
}
end
implement
{a}
array0_iexists_method(A0) =
lam(pred) => array0_iexists<a>(A0, pred)
implement
{a}
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 _ =
arrayref_foreach_env<a><bool>(A, asz, env)
}
end
implement
{a}
array0_forall_method(A0) =
lam(pred) => array0_forall<a>(A0, pred)
implement
{a}
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 _ =
arrayref_iforeach_env<a><bool>(A, asz, env)
}
end
implement
{a}
array0_iforall_method(A0) =
lam(pred) => array0_iforall<a>(A0, pred)
implement
{a}
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 _ = arrayref_foreach<a>(A, asz)
in
end
implement
{a}
array0_foreach_method(A0) =
lam(fwork) => array0_foreach<a>(A0, fwork)
implement
{a}
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 _ = arrayref_iforeach<a> (A, asz)
in
end
implement
{a}
array0_iforeach_method(A0) =
lam(fwork) => array0_iforeach<a>(A0, fwork)
implement
{a}
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 _ = arrayref_rforeach<a> (A, asz)
in
end
implement
{a}
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 _ =
arrayref_foreach_env<a><tres>(A, asz, res)
}
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 _ =
arrayref_iforeach_env<a><tres>(A, asz, res)
}
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 _ =
arrayref_rforeach_env<a><tres>(A, asz, res)
}
implement
{a}{tres}
array0_foldright_method
(A0, _) =
(
lam(fopr, snk) =>
array0_foldright<a><tres>(A0, fopr, snk)
)
implement
{a}
array0_is_ordered
(A0, cmp) = let
implement
gcompare_ref_ref<a>
(x, y) = $effmask_all(cmp(x, y))
in
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
implement
{a}
array0_quicksort
(A0, cmp) = let
val
ASZ = arrszref_of_array0(A0)
var
asz : size_t
val A =
arrszref_get_refsize(ASZ, asz)
implement
{a}
array_quicksort$cmp
(x1, x2) = let
val
cmp =
$UN.cast{(&a,&a)-<cloref>int}(cmp)
in
cmp(x1, x2)
end
in
arrayref_quicksort<a> (A, asz)
end
implement
(a)
fprint_val<array0(a)> = fprint_array0<a>
implement
(a)
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 else (1)
) else (
if j < n then (~1) else (0)
)
)
in
$effmask_all(loop(array0_get_ref{a}(xs), array0_get_ref{a}(xs), i2sz(0), i2sz(0)))
end
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)
)
in
(Mref, nrow, ncol)
end
implement
{a}
matrix0_make_elt_int
(nrow, ncol, x0) = let
val
nrow = i2sz(max(0, g1ofg0(nrow)))
and
ncol = i2sz(max(0, g1ofg0(ncol)))
in
matrix0_of_mtrxszref(mtrxszref_make_elt<a>(nrow, ncol, x0))
end
implement
{a}
matrix0_make_elt_size
(nrow, ncol, x0) =
(
matrix0_of_mtrxszref(mtrxszref_make_elt<a>(nrow, ncol, x0))
)
implement
{a}
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()
) else
$raise MatrixSubscriptExn()
end
implement
{a}
matrix0_get_at_size
(M0, i, j) = let
val
MSZ = mtrxszref_of_matrix0(M0)
in
mtrxszref_get_at_size<a>(MSZ, i, j)
end
implement
{a}
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()
) else
$raise MatrixSubscriptExn()
end
implement
{a}
matrix0_set_at_size
(M0, i, j, x) = let
val
MSZ =
mtrxszref_of_matrix0{a}(M0)
in
mtrxszref_set_at_size<a>(MSZ, i, j, x)
end
implement
{a}
print_matrix0 (A) =
fprint_matrix0<a>(stdout_ref, A)
implement
{a}
prerr_matrix0 (A) =
fprint_matrix0<a>(stderr_ref, A)
implement
{a}
fprint_matrix0(out, M) =
fprint_mtrxszref<a>(out, mtrxszref_of_matrix0(M))
implement
{a}
fprint_matrix0_sep(out, M, sep1, sep2) =
fprint_mtrxszref_sep<a>(out, mtrxszref_of_matrix0(M), sep1, sep2)
implement
{a}
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)
in
matrix0_of_mtrxszref
(mtrxszref_make_matrixref{a}(matrixptr_refize{a}(M), m, n))
end
implement
{a}
matrix0_tabulate
{m,n}
(nrow, ncol, fopr) = let
implement
{a2}
matrix_tabulate$fopr
(i, j) = let
val i =
$UN.cast{sizeLt(m)}(i)
val j =
$UN.cast{sizeLt(n)}(j)
in
$UN.castvwtp0{a2}(fopr(i,j))
end
in
matrix0_of_mtrxszref{a}(mtrxszref_tabulate<a>(nrow, ncol))
end
implement
{a}
matrix0_tabulate_method_int
(nrow, ncol) =
(
lam(fopr) =>
matrix0_tabulate<a>
( i2sz(nrow)
, i2sz(ncol), lam(i, j) => fopr(sz2i(i), sz2i(j))
)
)
implement
{a}
matrix0_tabulate_method_size
(nrow, ncol) =
(
lam(fopr) => matrix0_tabulate<a>(nrow, ncol, fopr)
)
implement
{a}
matrix0_foreach
(M0, fwork) = let
fun
loop
(
p: ptr, i: size_t
) : void = (
if
(i > 0)
then let
val
(pf, fpf | p) =
$UN.ptr0_vtake(p)
val () = fwork(!p)
prval () = fpf(pf)
in
loop(ptr_succ<a>(p), pred(i))
end else ()
)
val (M, m, n) = matrix0_get_refsize(M0)
in
loop(ptrcast(M), m * n)
end
implement
{a}
matrix0_iforeach
(M0, fwork) = 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 () = fwork(i, j, !p)
prval () = 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 else ()
)
in
loop(ptrcast(M), m * n, i2sz(0), i2sz(0))
end
implement
{res}{a}
matrix0_foldleft
(
M0, ini, fopr
) = ini where
{
var ini: res = ini
val p_ini = addr@(ini)
var fopr2 =
lam@(x: &a): void =>
$UN.ptr0_set<res>(p_ini, fopr($UN.ptr0_get<res>(p_ini), x))
val () =
matrix0_foreach<a>(M0, $UN.cast{(&a)-<cloref1>void}(addr@fopr2))
}
implement
{res}{a}
matrix0_ifoldleft
(
M0, ini, fopr
) = ini where
{
var ini: res = ini
val p_ini = addr@(ini)
var fopr2 =
lam@(i: size_t, j: size_t, x: &a): void =>
$UN.ptr0_set<res>
(p_ini, fopr($UN.ptr0_get<res>(p_ini), i, j, x))
val () =
matrix0_iforeach<a>
(M0, $UN.cast{(size_t,size_t,&a)-<cloref1>void}(addr@fopr2))
}
#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
{}
intgte_stream(n) = f(n) where
{
fun
f(n:int):<!laz> stream(int) =
$delay(stream_cons(n, f(n+1)))
}
implement
{a}
stream2list0(xs) =
list0_of_list_vt(stream2list(xs))
implement
{a}
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))
)
}
implement
{}
stream_make_intrange_lr
(l, r) =
(
stream_make_intrange_lrd<>(l, r, 1)
)
implement
{}
stream_make_intrange_lrd
(l, r, d) = let
fun
auxmain
(
l: int
, r: int
, d: int
) :<!laz> stream(int) = $delay
(
if
(l >= r)
then stream_nil()
else stream_cons(l, auxmain(l+d, r, d))
)
in
auxmain(l, r, d)
end
implement
{a}{b}
stream_map
(xs, fopr) =
(
stream_map_cloref<a><b>(xs, fopr)
)
implement
{a}{b}
stream_map_method
(xs, _) =
(
lam(fopr) => stream_map_cloref<a><b>(xs, fopr)
)
implement
{a}{b}
stream_imap
(xs, fopr) =
(
stream_imap_cloref<a><b>(xs, fopr)
)
implement
{a}{b}
stream_imap_method
(xs, _) =
(
lam(fopr) => stream_imap_cloref<a><b>(xs, fopr)
)
implement
{a}
stream_filter
(xs, pred) = stream_filter_cloref<a>(xs, pred)
implement
{a}
stream_filter_method
(xs) =
(
lam(pred) => stream_filter_cloref<a>(xs, pred)
)
implement
{res}{x}
stream_scan
(xs, res, fopr) =
(
stream_scan_cloref<res><x>(xs, res, fopr)
)
implement
{res}{x}
stream_scan_method(xs, _) =
(
lam(res, fopr) =>
stream_scan_cloref<res><x>(xs, res, fopr)
)
implement
{a}
stream_foreach
(xs, fwork) =
stream_foreach_cloref<a>(xs, fwork)
implement
{a}
stream_foreach_method(xs) =
(
lam(fwork) =>
stream_foreach_cloref<a>(xs, fwork)
)
implement
{a}
stream_iforeach
(xs, fwork) =
stream_iforeach_cloref<a>(xs, fwork)
implement
{a}
stream_iforeach_method(xs) =
(
lam(fwork) =>
stream_iforeach_cloref<a>(xs, fwork)
)
implement
{res}{a}
stream_foldleft
(xs, ini, fopr) =
stream_foldleft_cloref<res><a>(xs, ini, fopr)
implement
{res}{a}
stream_foldleft_method
(xs, _) =
lam(ini, fopr) =>
stream_foldleft_cloref<res><a>(xs, ini, fopr)
#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/list0_vt.sats"
#staload "libats/ML/SATS/stream_vt.sats"
implement
{a}
stream2list0_vt
(xs) =
(
list0_vt2t
(g0ofg1(stream2list_vt<a>(xs)))
)
implement
{}
intgte_stream_vt(n) = f(n) where
{
fun
f(n:int):<!laz> stream_vt(int) =
$ldelay(stream_vt_cons(n, f(n+1)))
}
implement
{a}
stream_vt_make_list0
(xs) =
auxmain(xs) where
{
fun
auxmain:
$d2ctype
(
stream_vt_make_list0<a>
) = lam(xs) => $ldelay
(
case+ xs of
| list0_nil() =>
stream_vt_nil()
| list0_cons(x, xs) =>
stream_vt_cons(x, auxmain(xs))
)
}
implement
{}
stream_vt_make_intrange_lr
(l, r) =
(
stream_vt_make_intrange_lrd<>(l, r, 1)
)
implement
{}
stream_vt_make_intrange_lrd
(l, r, d) = let
fun
auxmain
(
l: int
, r: int
, d: int
) :<!laz> stream_vt(int) = $ldelay
(
if
(l >= r)
then stream_vt_nil()
else stream_vt_cons(l, auxmain(l+d, r, d))
)
in
auxmain(l, r, d)
end
implement
{a}{b}
stream_vt_map_method
(xs, _) =
(
llam(fopr) => stream_vt_map_cloptr<a><b>(xs, fopr)
)
implement
{a}
stream_vt_filter_method
(xs) =
(
llam(pred) => stream_vt_filter_cloptr<a>(xs, pred)
)
implement
{a}
stream_vt_foreach_method
(xs) =
(
llam(fwork) => stream_vt_foreach_cloptr<a>(xs, fwork)
)
implement
{a}
stream_vt_rforeach_method
(xs) =
(
llam(fwork) => stream_vt_rforeach_cloptr<a>(xs, fwork)
)
implement
{a}
stream_vt_iforeach_method
(xs) =
(
llam(fwork) => stream_vt_iforeach_cloptr<a>(xs, fwork)
)
implement
{res}{a}
stream_vt_foldleft_method
(xs, _) =
(
llam(ini, fwork) => stream_vt_foldleft_cloptr<res><a>(xs, ini, fwork)
)
implement
{res}{a}
stream_vt_ifoldleft_method
(xs, _) =
(
llam(ini, fwork) => stream_vt_ifoldleft_cloptr<res><a>(xs, ini, fwork)
)
#define
ATS_DYNLOADFLAG 0
staload
UN = "prelude/SATS/unsafe.sats"
staload
_ = "prelude/DATS/integer.dats"
staload
_ = "prelude/DATS/integer_size.dats"
staload
_ = "prelude/DATS/filebas.dats"
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_fileptr_char = streamize_fileptr_char
macdef
prelude_streamize_fileref_line = streamize_fileref_line
macdef
prelude_streamize_fileptr_line = streamize_fileptr_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_get_line_charlst
(filr) =
(
list0_of_list_vt
(prelude_fileref_get_line_charlst(filr))
)
implement
fileref_get_lines_charlstlst
(filr) =
(
$UN.castvwtp0{list0(charlst0)}
(prelude_fileref_get_lines_charlstlst(filr))
)
local
staload
_ = "prelude/DATS/strptr.dats"
in
implement
fileref_get_line_string
(filr) =
(
strptr2string
(prelude_fileref_get_line_string(filr))
)
implement
fileref_get_lines_stringlst
(filr) =
(
$UN.castvwtp0{list0(string)}
(prelude_fileref_get_lines_stringlst(filr))
)
end
implement
{}
filename_get_lines_stringlst_opt
(path) = let
val opt =
fileref_open_opt(path, file_mode_r)
in
case+ opt of
| ~None_vt() =>
None_vt()
| ~Some_vt(inp) =>
Some_vt(lines) where
{
val lines =
fileref_get_lines_stringlst(inp)
val () = fileref_close(inp)
}
end
implement
{}
streamize_fileref_char
(filr) =
prelude_streamize_fileref_char(filr)
implement
{}
streamize_fileptr_char
(filp) =
prelude_streamize_fileptr_char(filp)
implement
{}
streamize_fileref_line
(filr) =
(
$UN.castvwtp0{stream_vt(string)}
(prelude_streamize_fileref_line(filr))
)
implement
{}
streamize_fileptr_line
(filp) =
(
$UN.castvwtp0{stream_vt(string)}
(prelude_streamize_fileptr_line(filp))
)
implement
{}
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
else stream_vt_cons(strptr2string(word), auxmain(filr))
end
)
}
implement
{}
streamize_fileptr_word
(filp) = let
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 stream_vt_nil() where
{
val () = fileref_close(filr)
prval () = strptr_free_null(word)
}
else stream_vt_cons(strptr2string(word), auxmain(filr))
end
)
in
auxmain($UN.castvwtp0{FILEref}(filp))
end
implement
{}
streamize_filename_char
(fname) = let
val
opt =
fileref_open_opt(fname, file_mode_r)
in
case+ opt of
| ~None_vt() =>
None_vt()
| ~Some_vt(filr) =>
Some_vt(streamize_fileptr_char($UN.castvwtp0{FILEptr1}(filr)))
end
implement
{}
streamize_filename_line
(fname) = let
val
opt =
fileref_open_opt(fname, file_mode_r)
in
case+ opt of
| ~None_vt() =>
None_vt()
| ~Some_vt(filr) =>
Some_vt(streamize_fileptr_line($UN.castvwtp0{FILEptr1}(filr)))
end
implement
{}
streamize_filename_word
(fname) = let
val
opt =
fileref_open_opt(fname, file_mode_r)
in
case+ opt of
| ~None_vt() =>
None_vt()
| ~Some_vt(filr) =>
Some_vt(streamize_fileptr_word($UN.castvwtp0{FILEptr1}(filr)))
end
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
{}
int_repeat_lazy
(n, f) =
(
int_repeat_cloref<>(n, lazy2cloref(f))
)
implement
{}
int_repeat_cloref
(n, f) =
loop(n, f) where
{
fun
loop
(
n: int, f: cfun0(void)
) : void = (
if
n > 0
then (
let
val () = f() in loop(n-1, f)
end
) else ()
)
}
implement
{}
int_repeat_method
(n) =
(
lam(f) => int_repeat_cloref<>(n, f)
)
implement
{}
int_forall_cloref
(n, f) =
intrange_forall_cloref<>(0, n, f)
implement
{}
int_forall_method
(n) =
(
lam(f) => int_forall_cloref<>(n, f)
)
implement
{}
int_foreach_cloref
(n, f) =
intrange_foreach_cloref<>(0, n, f)
implement
{}
int_foreach_method
(n) =
(
lam(f) => int_foreach_cloref<>(n, f)
)
implement
{}
int_rforeach_cloref
(n, f) =
intrange_rforeach_cloref<>(0, n, f)
implement
{}
int_rforeach_method
(n) = lam(f) => int_rforeach_cloref<>(n, f)
implement
{res}
int_foldleft_cloref
(n, ini, f) =
intrange_foldleft_cloref<res>(0, n, ini, f)
implement
{res}
int_foldleft_method
(n, tres) =
(
lam(ini, f) => int_foldleft_cloref<res>(n, ini, f)
)
implement
{res}
int_foldright_cloref
(n, f, snk) =
intrange_foldright_cloref<res>(0, n, f, snk)
implement
{res}
int_foldright_method
(n, tres) =
(
lam(f, snk) => int_foldright_cloref<res>(n, f, snk)
)
implement
{}
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
)
in
loop (l, r, f)
end
implement
{}
intrange_forall_method
( @(l, r) ) =
lam(f) => intrange_forall_cloref<>(l, r, f)
implement
{}
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 ()
)
in
loop (l, r, f)
end
implement
{}
intrange_foreach_method
( @(l, r) ) =
lam(f) => intrange_foreach_cloref<>(l, r, f)
implement
{}
intrange_rforeach_cloref
(l, r, f) = let
fun
loop
(
l: int, r: int, f: cfun1(int, void)
) : void = (
if
(l < r)
then
(
let val () = f(r-1) in loop(l, r-1, f) end
)
else ()
)
in
loop (l, r, f)
end
implement
{}
intrange_rforeach_method
( @(l, r) ) =
lam(f) => intrange_rforeach_cloref<>(l, r, f)
implement
{res}
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
)
in
loop(l, r, ini, fopr)
end
implement
{res}
intrange_foldleft_method
( @(l, r), tres ) =
(
lam(ini, f) =>
intrange_foldleft_cloref<res>(l, r, ini, f)
)
implement
{res}
intrange_foldright_cloref
(l, r, f, snk) = let
fun
loop
(
l: int, r: int
, f: cfun2(int, res, res), snk: res
) : res = (
if
(l < r)
then let
val r1 = r-1 in loop(l, r1, f, f(r1, snk))
end
else snk
)
in
loop(l, r, f, snk)
end
implement
{res}
intrange_foldright_method
( @(l, r), tres ) =
(
lam(f, snk) =>
intrange_foldright_cloref<res>(l, r, f, snk)
)
implement
{}
int_streamGte(n) =
(
fix
aux
(
n: int
) : stream(int) => $delay(stream_cons(n, aux(n+1)))
) (n)
implement
{}
int_streamGte_vt(n) =
(
fix
aux
(
n: int
) : stream_vt(int) => $ldelay(stream_vt_cons(n, aux(n+1)))
) (n)
implement
{a}
int_list0_map_cloref
(n, f) = list0_tabulate<a>(n, f)
implement
{a}
int_list0_map_method
(n, tres) =
lam(f) => int_list0_map_cloref<a>(n, f)
implement
{a}
int_array0_map_cloref
(n, fopr) =
(
array0_tabulate<a>
(i2sz(n), lam(i) => fopr(sz2i(i)))
)
implement
{a}
int_array0_map_method
(n, tres) =
lam(f) => int_array0_map_cloref<a>(n, f)
implement
{a}
int_stream_map_cloref
(n, f) = auxmain(0) where
{
fun
auxmain
(
i: Nat
) : stream(a) = $delay
(
if
(i >= n)
then
stream_nil()
else
stream_cons(f(i), auxmain(i+1))
)
}
implement
{a}
int_stream_map_method
(n, tres) =
(
lam(f) =>
int_stream_map_cloref<a>(n, f)
)
implement
{a}
int_stream_vt_map_cloref
(n, f) = auxmain(0) where
{
fun
auxmain
(
i: Nat
) : stream_vt(a) = $ldelay
(
if
(i >= n)
then
stream_vt_nil()
else
stream_vt_cons(f(i), auxmain(i+1))
) : stream_vt_con(a)
}
implement
{a}
int_stream_vt_map_method
(n, tres) =
(
lam(f) =>
int_stream_vt_map_cloref<a>(n, f)
)
implement
{}
int2_foreach_cloref
(n1, n2, f0) =
(
intrange2_foreach_cloref<>
( 0, n1
, 0, n2, f0 )
)
implement
{}
intrange2_foreach_cloref
(l1, r1, l2, r2, f0) = let
fnx
loop1
(
m1: int, r1: int
, l2: int, r2: int
, f0: cfun2(int, int, void)
) : void = (
if
m1 < r1
then
loop2(m1, r1, l2, l2, r2, f0)
else ()
)
and
loop2
(
m1: int, r1: int
, l2: int, m2: int, r2: int
, f0: cfun2(int, int, void)
) : void = (
if
m2 < r2
then let
val () = f0(m1, m2)
in
loop2
(m1, r1, l2, m2+1, r2, f0)
end
else
(
loop1(m1+1, r1, l2, r2, f0)
)
)
in
loop1(l1, r1, l2, r2, f0)
end
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
{}
funmap_nil() = $FM.funmap_nil<>()
implement
{}
funmap_make_nil() = $FM.funmap_make_nil<>()
implement
{}
funmap_is_nil(map) = $FM.funmap_is_nil<>(map)
implement
{}
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
end
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 = ()
implement
(env)
$FM.funmap_foreach$fwork<key,itm><env>
(k, x, env) = fwork(k, x)
val () =
$FM.funmap_foreach_env<key,itm><void>(map, env)
}
implement
{key,itm}
funmap_listize
(map) =
(
$effmask_wrt
(
list0_of_list_vt
($FM.funmap_listize<key,itm>(map))
)
)
implement
{key,itm}
funmap_streamize
(map) =
(
$effmask_wrt
($FM.funmap_streamize<key,itm>(map))
)
implement
{key,itm}
funmap_make_module
() = $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>
,
streamize = funmap_streamize<key,itm>
}
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
(x0) = $FS.funset_sing<a>(x0)
implement
{a}
funset_make_sing
(x0) = $FS.funset_make_sing<a>(x0)
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
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
implement
{}
funset_is_nil
(xs) = $FS.funset_is_nil<>(xs)
implement
{}
funset_isnot_nil
(xs) = $FS.funset_isnot_nil<>(xs)
implement
{a}
funset_size(xs) = $FS.funset_size<a>(xs)
implement
{a}
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
implement
{a}
funset_isnot_member
(xs, x0) = ~funset_is_member<a>(xs, x0)
implement
{a}
funset_insert
(xs, x0) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_insert<a>(xs, x0)
end
implement
{a}
funset_remove
(xs, x0) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_remove<a>(xs, x0)
end
implement
{a}
funset_getmax_opt = $FS.funset_getmax_opt<a>
implement
{a}
funset_getmin_opt = $FS.funset_getmin_opt<a>
implement
{a}
funset_takeoutmax_opt = $FS.funset_takeoutmax_opt<a>
implement
{a}
funset_takeoutmin_opt = $FS.funset_takeoutmin_opt<a>
implement
{a}
funset_union
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_union<a>(xs1, xs2)
end
implement
{a}
funset_intersect
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_intersect<a>(xs1, xs2)
end
implement
{a}
funset_differ
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_differ<a>(xs1, xs2)
end
implement
{a}
funset_symdiff
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_symdiff<a>(xs1, xs2)
end
implement
{a}
funset_equal
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_equal<a>(xs1, xs2)
end
implement
{a}
funset_compare
(xs1, xs2) = let
implement
$FS.compare_elt_elt<a> = compare_elt_elt<a>
in
$FS.funset_compare<a>(xs1, xs2)
end
implement
{a}
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
implement
{a}
funset_is_supset
(xs1, xs2) = funset_is_subset<a>(xs2, xs1)
implement
{a}
funset_foreach(xs) = let
var env: void = ()
in
funset_foreach_env<a><void>(xs, env)
end
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
implement
{a}
funset_foreach_cloref
(xs, fwork) = let
var env: void = ()
implement
(env)
$FS.funset_foreach$fwork<a><env>(x, env) = fwork(x)
in
$FS.funset_foreach_env<a><void> (xs, env)
end
implement
{a}
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
implement
{a}
funset_listize
(xs) = (
$effmask_wrt
(
list0_of_list_vt{a}($FS.funset_listize<a>(xs))
)
)
implement
{a}
funset_streamize
(xs) = $effmask_wrt($FS.funset_streamize<a>(xs))
implement
{a}
funset_make_module
() = $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>
,
streamize = funset_streamize<a>
}
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}
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
implement
hash_key<uint> (key) = let
val key = $UN.cast{uint32}(key)
in
$UN.cast{ulint}(inthash_jenkins<>(key))
end
implement
hash_key<string> (key) =
string_hash_multiplier (31UL, 31415926536UL, key)
implement
{key}
$HT.hash_key = hash_key<key>
implement
{key}
$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)
}
implement
{}
hashtbl_get_capacity
(tbl) = cap where
{
val tbl = htdecode(tbl)
val cap = $HT.hashtbl_get_capacity<>(tbl)
prval () = $UN.cast2void(tbl)
}
implement
{key,itm}
hashtbl_search
(tbl, k) = opt where
{
val tbl = htdecode(tbl)
val opt =
$HT.hashtbl_search_opt<key,itm>(tbl, k)
prval () = $UN.cast2void(tbl)
}
implement
{key,itm}
hashtbl_search_ref
(tbl, k) = cptr where
{
val tbl = htdecode(tbl)
val cptr =
$HT.hashtbl_search_ref<key,itm>(tbl, k)
prval () = $UN.cast2void(tbl)
}
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)
}
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)
}
implement
{key,itm}
hashtbl_takeout
(tbl, k) = opt where
{
val tbl = htdecode(tbl)
val opt =
$HT.hashtbl_takeout_opt<key,itm>(tbl, k)
prval () = $UN.cast2void(tbl)
}
implement
{key,itm}
hashtbl_remove
(tbl, k) = ans where
{
val tbl = htdecode(tbl)
val ans = $HT.hashtbl_remove<key,itm>(tbl, k)
prval () = $UN.cast2void(tbl)
}
implement
{key,itm}
hashtbl_takeout_all
(tbl) = kxs where
{
val tbl = htdecode(tbl)
val kxs = $HT.hashtbl_takeout_all<key,itm>(tbl)
val kxs = list0_of_list_vt{(key,itm)}(kxs)
prval () = $UN.cast2void(tbl)
}
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
end
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
implement
{key,itm}
hashtbl_foreach_cloref
(tbl, fwork) = () where
{
var env: void = ()
implement
(env)
$HT.hashtbl_foreach$fwork<key,itm><env>
(k, x, env) = fwork(k, x)
val tbl = htdecode(tbl)
val
() =
$HT.hashtbl_foreach_env<key,itm><void>
(tbl, env)
prval () = $UN.cast2void(tbl)
}
implement
{key,itm}
hashtbl_listize0
(tbl) =
(
hashtbl_takeout_all<key,itm>(tbl)
)
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)
}