(***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) // // For supporting ML-style of functional programming // (* ****** ****** *) // // Author of the file: Hongwei Xi (gmhwxiATgmailDOTcom) // Start Time: June, 2012 // (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.libats" (* ****** ****** *) // typedef cfun0(b:vt0p) = ((*void*)) - b typedef cfun1(a:vt0p, b:vt0p) = (a) - b typedef cfun2(a1:vt0p, a2:vt0p, b:vt0p) = (a1, a2) - b // (* ****** ****** *) // typedef cfun3 ( a1:vt0p, a2:vt0p, a3:vt0p, b:vt0p ) = (a1, a2, a3) - b typedef cfun4 ( a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, b:vt0p ) = (a1, a2, a3, a4) - b typedef cfun5 ( a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, b:vt0p ) = (a1, a2, a3, a4, a5) - b typedef cfun6 ( a1:vt0p, a2:vt0p, a3:vt0p, a4:vt0p, a5:vt0p, a6:vt0p, b:vt0p ) = (a1, a2, a3, a4, a5, a6) - 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) - 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) - 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) - 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 (* ****** ****** *) // // t0ype+: covariant // vt0ype+: covariant // datatype list0_t0ype_type ( a: t0ype+ ) = | list0_nil of ((*void*)) | list0_cons of (a, list0_t0ype_type(a)) // end of [list0_cons] // datavtype list0_vt0ype_vtype ( a: vt0ype+ ) = | list0_vt_nil of ((*void*)) | list0_vt_cons of (a, list0_vt0ype_vtype(a)) // end of [list0_vt_cons] // #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) // (* ****** ****** *) // // t0ype+: covariant // vt0ype+: covariant // 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(*invariant*)) = ptr // typedef array0 (a:vt0ype) = array0_vt0ype_type(a) // (* abstype subarray0_vt0ype_type (a: vt0ype(*invariant*)) = ptr stadef subarray0 = subarray0_vt0ype_type *) // (* ****** ****** *) // abstype matrix0_vt0ype_type (a: vt0ype(*invariant*)) = ptr // typedef matrix0 (a:vt0ype) = matrix0_vt0ype_type(a) // (* ****** ****** *) // abstype strarr_type = ptr typedef strarr = strarr_type // (* abstype substrarr_type = ptr typedef substrarr = substrarr_type *) // (* ****** ****** *) // abstype dynarray_type(a:vt0ype) = ptr // typedef dynarray(a:vt0ype) = dynarray_type(a) // (* ****** ****** *) // // HX: // for elements of type (a) // abstype hashtbl_type (key:t0ype, itm:t0ype+) = ptr // typedef hashtbl ( key:t0ype , itm:t0ype) = hashtbl_type(key, itm) // (* ****** ****** *) // // HX-2015-12-01: // G-values for generic programming // (* ****** ****** *) // datatype gvalue = // | GVnil of () // | GVint of (int) // | GVptr of (ptr) // | GVbool of (bool) | GVchar of (char) // | GVfloat of (double) // | GVstring of (string) // | GVref of (gvref) // | GVlist of (gvlist) // | GVarray of (gvarray) // | GVdynarr of (gvdynarr) // | GVhashtbl of (gvhashtbl) // | GVfunclo_fun of ((gvalue) - gvalue) | GVfunclo_clo of ((gvalue) - gvalue) // where gvref = ref(gvalue) and gvlist = list0(gvalue) and gvarray = array0(gvalue) and gvdynarr = dynarray(gvalue) and gvhashtbl = hashtbl(string, gvalue) // (* typedef gvopt = Option(gvalue) vtypedef gvopt_vt = Option_vt(gvalue) *) // (* ****** ****** *) (* end of [basis.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2017 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: December, 2017 *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) #staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // // HX: prelude/string // (* ****** ****** *) // fun{} string_tabulate_cloref {n:int} ( n: size_t(n) , f: (sizeLt(n)) - charNZ): strnptr(n) // (* ****** ****** *) // // HX-2017-12-30: // prelude/intrange // (* ****** ****** *) fun{} int_forall_cloptr ( n: int, pred: (int) - bool ) : bool // end of [int_forall_cloptr] fun{} int_forall_cloref ( n: int, pred: (int) - bool ) : bool // end of [int_forall_cloref] (* ****** ****** *) fun{} intrange_forall_cloptr ( m: int, n: int, pred: (int) - bool ) : bool // end of [intrange_forall_cloptr] fun{} intrange_forall_cloref ( m: int, n: int, pred: (int) - bool ) : bool // end of [intrange_forall_cloref] (* ****** ****** *) // fun{} int_foreach_cloptr ( n: int, fwork: (int) - void ) : int // end of [int_foreach_cloptr] fun{} int_foreach_cloref ( n: int, fwork: (int) - void ) : int // end of [int_foreach_cloref] // fun{} intrange_foreach_cloptr ( l: int, r: int, fwork: (int) - void ) : int // end of [intrange_foreach_cloptr] fun{} intrange_foreach_cloref ( l: int, r: int, fwork: (int) - void ) : int // end of [intrange_foreach_cloref] // (* ****** ****** *) // fun{} int_rforeach_cloptr ( n: int, fwork: (int) - void ) : int // end of [int_rforeach_cloptr] fun{} int_rforeach_cloref ( n: int, fwork: (int) - void ) : int // end of [int_rforeach_cloref] // fun{} intrange_rforeach_cloptr ( l: int, r: int, fwork: (int) - void ) : int // end of [intrange_rforeach_cloptr] fun{} intrange_rforeach_cloref ( l: int, r: int, fwork: (int) - void ) : int // end of [intrange_rforeach_cloref] // (* ****** ****** *) // // HX: prelude/list // (* ****** ****** *) // fun{x:t0p} list_exists_cloptr ( xs: List(INV(x)) , pred: (x) - bool): bool fun{x:t0p} list_exists_cloref ( xs: List(INV(x)) , pred: (x) - bool):<(*0*)> bool // fun{x:t0p} list_iexists_cloptr {n:int} ( xs: list(INV(x), n), pred: (natLt(n), x) - bool ) : bool // end of [list_iexists_cloptr] fun{x:t0p} list_iexists_cloref {n:int} ( xs: list(INV(x), n), pred: (natLt(n), x) - bool ) :<(*0*)> bool // end of [list_iexists_cloref] // (* ****** ****** *) // fun{x:t0p} list_forall_cloptr ( xs: List(INV(x)) , pred: (x) - bool): bool fun{x:t0p} list_forall_cloref ( xs: List(INV(x)) , pred: (x) - bool):<(*0*)> bool // fun{x:t0p} list_iforall_cloptr {n:int} ( xs: list(INV(x), n), pred: (natLt(n), x) - bool ) : bool // end of [list_iforall_cloptr] fun{x:t0p} list_iforall_cloref {n:int} ( xs: list(INV(x), n), pred: (natLt(n), x) - bool ) :<(*0*)> bool // end of [list_iforall_cloref] // (* ****** ****** *) // fun{x:t0p} list_equal_cloref (List(INV(x)), List(x), eqfn: (x, x) - bool):<> bool // fun{x:t0p} list_compare_cloref (List(INV(x)), List(x), cmpfn: (x, x) - int):<> int // (* ****** ****** *) // fun{x:t0p} list_app_fun (List(INV(x)), fwork: (x) - void): void fun{x:t0p} list_app_clo (List(INV(x)), fwork: &(x) - void): void // fun{x:t0p} list_app_cloref (xs: List(INV(x)), fwork: (x) - void): void // (* ****** ****** *) // fun{ x:t0p}{y:vt0p } list_map_fun{n:int} (xs: list(INV(x), n), f: (x) - y): list_vt(y, n) fun{ x:t0p}{y:vt0p } list_map_clo{n:int} (xs: list(INV(x), n), f: &(x) - y): list_vt(y, n) // fun{ x:t0p}{y:vt0p } list_map_cloref{n:int} (xs: list(INV(x), n), f: (x) - y): list_vt(y, n) // (* ****** ****** *) // fun{ a:vt0p } list_tabulate_fun{n:nat} (n: int n, f: natLt(n) - a): list_vt(a, n) fun{ a:vt0p } list_tabulate_clo{n:nat} (n: int n, f: &(natLt(n)) - a): list_vt(a, n) // fun{ a:vt0p } list_tabulate_cloref{n:nat} (n: int n, f: natLt(n) - a): list_vt(a, n) // (* ****** ****** *) // fun {x:t0p} list_foreach_fun {fe:eff} ( xs: List(INV(x)), f: (x) - void ) : void // end of [list_foreach_fun] // fun {x:t0p} list_foreach_clo {fe:eff} ( xs: List(INV(x)), f0: &(x) - void ) : void // end of [list_foreach_clo] fun {x:t0p} list_foreach_vclo {v:view}{fe:eff} ( pf: !v | xs: List(INV(x)) , f0: &(!v | x) - void ) : void // end of [list_foreach_vclo] // fun {x:t0p} list_foreach_cloptr {fe:eff} ( xs: List(INV(x)), f0: (x) - void ) : void // end of [list_foreach_cloptr] fun {x:t0p} list_foreach_vcloptr {v:view}{fe:eff} ( pf: !v | xs: List(INV(x)) , f0: (!v | x) - void ) : void // end of [list_foreach_vcloptr] // fun {x:t0p} list_foreach_cloref {fe:eff} ( xs: List(INV(x)), f: (x) - void ) : void // end of [list_foreach_cloref] // (* ****** ****** *) // fun {a:t0p} list_foreach_method ( xs: List(INV(a)) ) : (cfun(a,void)) - void // overload .foreach with list_foreach_method // (* ****** ****** *) // fun{ x:t0p } list_iforeach_cloref {n:int} ( xs: list(INV(x), n) , fwork: (natLt(n), x) - void ) : void // end of [list_iforeach_cloref] // (* ****** ****** *) // fun {a:t0p} list_iforeach_method {n:int} ( xs: list(INV(a), n) ) : (cfun(natLt(n),a,void)) - void // overload .iforeach with list_iforeach_method // (* ****** ****** *) // fun{ res:vt0p}{x:t0p } list_foldleft_cloptr (xs: List(INV(x)), ini: res, fopr: (res, x) - res): res fun{ res:vt0p}{x:t0p } list_foldleft_cloref (xs: List(INV(x)), ini: res, fopr: (res, x) - res): res // (* ****** ****** *) // fun{ x:t0p}{res:vt0p } list_foldright_cloptr (xs: List(INV(x)), fopr: (x, res) - res, snk: res): res fun{ x:t0p}{res:vt0p } list_foldright_cloref (xs: List(INV(x)), fopr: (x, res) - res, snk: res): res // (* ****** ****** *) // // HX: prelude/list_vt // (* ****** ****** *) // fun {x:vt0p} {y:vt0p} list_vt_map_fun{n:int} ( xs: !list_vt(INV(x), n) , f0: (&x) - y): list_vt(y, n) fun {x:vt0p} {y:vt0p} list_vt_map_clo{n:int} ( xs: !list_vt(INV(x), n) , f0: &(&x) - y): list_vt(y, n) // fun {x:vt0p} {y:vt0p} list_vt_map_cloptr{n:int} ( xs: !list_vt(INV(x), n) , f0: ( &x ) - y): list_vt(y, n) fun {x:vt0p} {y:vt0p} list_vt_map_cloref{n:int} ( xs: !list_vt(INV(x), n) , f0: ( &x ) - y): list_vt(y, n) // (* ****** ****** *) // fun {x:vt0p} {y:vt0p} list_vt_mapfree_fun {n:int} ( xs: list_vt(INV(x), n) , f0: (&x >> x?!) - y): list_vt(y, n) fun {x:vt0p} {y:vt0p} list_vt_mapfree_clo {n:int} ( xs: list_vt(INV(x), n) , f0: &(&x >> x?!) - y): list_vt(y, n) // fun {a:vt0p} {b:vt0p} list_vt_mapfree_cloptr {n:nat} ( xs: list_vt(INV(a), n), fopr: (&a >> a?!) - b ) : list_vt(b, n) // end-of-function fun {x:vt0p}{y:vt0p} list_vt_mapfree_cloref{n:int} ( xs: list_vt(INV(x), n), fopr: (&x >> x?!) - y ) : list_vt(y, n) // end-of-function // (* ****** ****** *) // fun {a:vt0p} {b:vt0p} list_vt_mapfree_method {n:nat} ( list_vt(INV(a), n), TYPE(b) ) : ((&a >> a?!) - b) - list_vt(b, n) // overload .mapfree with list_vt_mapfree_method // (* ****** ****** *) // fun{ x:vt0p } list_vt_foreach_fun {fe:eff} ( xs: !List_vt(INV(x)), f0: (&x >> _) - void ) : void // end of [list_vt_foreach_fun] fun{ x:vt0p } list_vt_foreach_clo {fe:eff} ( xs: !List_vt(INV(x)), f0: &(&x >> _) - void ) : void // end of [list_vt_foreach_fun] // fun{ x:vt0p } list_vt_foreach_cloptr ( xs: !List_vt(INV(x)), f0: (&x >> _) - void ) :<1> void // end of [list_vt_foreach_cloptr] fun{ x:vt0p } list_vt_foreach_cloref ( xs: !List_vt(INV(x)), f0: (&x >> _) - void ) :<1> void // end of [list_vt_foreach_cloref] // (* ****** ****** *) // fun {r:vt0p} {x:vt0p} list_vt_foldleft_cloptr (xs: !List_vt(INV(x)), r0: r, f0: (r, &x) - r): (r) fun {r:vt0p} {x:vt0p} list_vt_foldleft_cloref (xs: !List_vt(INV(x)), r0: r, f0: (r, &x) - r): (r) // (* ****** ****** *) // // HX: prelude/array // (* ****** ****** *) // fun {a:vt0p} array_foreach_fun {n:int}{fe:eff} ( A0: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n), fwork: (&a >> _) - void ) : void // end of [array_foreach_fun] fun {a:vt0p} array_foreach_clo {n:int}{fe:eff} ( A0: &(@[INV(a)][n]) >> @[a][n], asz: size_t (n), fwork: &(&a >> _) - void ) : void // end of [array_foreach_clo] fun {a:vt0p} array_foreach_cloptr {n:int}{fe:eff} ( A0: &(@[INV(a)][n]) >> @[a][n], asz: size_t n, fwork: (&a >> _) - void ) : void // end of [array_foreach_cloptr] fun {a:vt0p} array_foreach_cloref {n:int}{fe:eff} ( A0: &(@[INV(a)][n]) >> @[a][n], asz: size_t(n), fwork: (&a >> _) - void ) : void // end of [array_foreach_cloref] // (* ****** ****** *) // fun {a:vt0p} array_foreach_vclo {v:view}{n:int}{fe:eff} ( pf: !v | A0: &(@[INV(a)][n]) >> @[a][n] , asz: size_t n, f0: &(!v | &a >> _) - void ) : void // end of [array_foreach_vclo] fun {a:vt0p} array_foreach_vcloptr {v:view}{n:int}{fe:eff} ( pf: !v | A0: &(@[INV(a)][n]) >> @[a][n] , asz: size_t(n), f0: !(!v | &a >> _) - void ) : void // end of [array_foreach_vcloptr] // (* ****** ****** *) // // HX: prelude/arrayptr // (* ****** ****** *) // fun {a:vt0p} arrayptr_foreach_fun {n:int}{fe:eff} ( A0: !arrayptr(INV(a), n), asz: size_t(n), fwork: (&a) - void ) : void // end of [arrayptr_foreach_fun] // (* ****** ****** *) // fun{a:vt0p} arrayptr_tabulate_cloref {n:int} ( asz: size_t(n) , fopr: (sizeLt(n)) - a): arrayptr(a, n) // (* ****** ****** *) // // HX: prelude/arrayref // (* ****** ****** *) // fun{a:vt0p} arrayref_tabulate_cloref {n:int} ( asz: size_t(n) , fopr: (sizeLt(n)) - (a)): arrayref(a, n) // fun{a:vt0p} arrszref_tabulate_cloref {n:int} (size_t(n), (sizeLt(n)) - a): arrszref(a) // (* ****** ****** *) // // HX: prelude/option // (* ****** ****** *) // fun {x:t0p} {y:vt0p} option_map_fun {b:bool} (option(INV(x), b), fopr: (x) - y): option_vt(y, b) fun {x:t0p} {y:vt0p} option_map_clo {b:bool} (option(INV(x), b), fopr: &(x) - y): option_vt(y, b) // fun {x:t0p} {y:vt0p} option_map_cloptr {b:bool} (option(INV(x), b), fopr: (x) - y): option_vt(y, b) fun {x:t0p} {y:vt0p} option_map_cloref {b:bool} (option(INV(x), b), fopr: (x) - y): option_vt(y, b) // (* ****** ****** *) // // HX: prelude/matrixptr // (* ****** ****** *) // fun {a:vt0p} matrixptr_tabulate_cloptr {m,n:int} ( nrow: size_t(m) , ncol: size_t(n) , fopr: (sizeLt(m), sizeLt(n)) - (a) ) : matrixptr(a, m, n) // end-of-function // fun {a:vt0p} matrixptr_tabulate_cloref {m,n:int} ( nrow: size_t(m) , ncol: size_t(n) , fopr: (sizeLt(m), sizeLt(n)) - (a) ) : matrixptr(a, m, n) // end-of-function // (* ****** ****** *) // fun {a:vt0p} matrixref_tabulate_cloref {m,n:int} ( nrow: size_t(m) , ncol: size_t(n) , fopr: (sizeLt(m), sizeLt(n)) - (a) ) : matrixref(a, m, n) // end-of-function fun {a:vt0p} mtrxszref_tabulate_cloref {m,n:int} ( nrow: size_t(m) , ncol: size_t(n) , fopr: (sizeLt(m), sizeLt(n)) - (a)): mtrxszref(a) // fun {a:vt0p} matrixref_foreach_cloref {m,n:int} ( M: matrixref(a, m, n) , m: size_t(m), n: size_t(n), fwork: (&(a) >> _) - void ) : void // end of [mtrxszref_foreach_cloref] fun {a:vt0p} mtrxszref_foreach_cloref (M0: mtrxszref(a), fwork: (&(a) >> _) - void): void // (* ****** ****** *) (* end of [atspre.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: May, 2012 *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* ****** ****** *) // // HX-2013-01: // A rule of thumb for effect-annotation is that // higher-order functions should not be annotated! // (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) (* typedef SHR(a:type) = a // for commenting purpose typedef NSH(a:type) = a // for commenting purpose *) (* ****** ****** *) #define nil0 list0_nil #define cons0 list0_cons (* ****** ****** *) // #define list0_sing(x) list0_cons(x, list0_nil()) // #define list0_pair(x1, x2) list0_cons(x1, list0_cons(x2, list0_nil())) // (* ****** ****** *) // castfn list0_cast{x:t0p} (xs: list0(INV(x))):<> list0(x) // (* ****** ****** *) // castfn 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): list0(a) (* ****** ****** *) // symintr list0 // fun{a:t0p} list0_make_arrpsz{n:int} (psz: arrpsz(INV(a), n)): 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): 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))): (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)))): 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))): (a) fun {a:t0p} list0_last_opt (xs: list0(INV(a))):<> Option_vt(a) // (* ****** ****** *) // fun {a:t0p} list0_init_exn (xs: list0(INV(a))): list0(a) fun {a:t0p} list0_init_opt (xs: list0(INV(a))): Option_vt(list0(a)) // (* ****** ****** *) // fun{a:t0p} list0_nth_exn (xs: list0(INV(a)), i0: int): (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): (a) fun{a:t0p} list0_get_at_opt (xs: list0(INV(a)), i0: int):<> Option_vt(a) // overload [] with list0_get_at_exn // ListSubscriptExn // (* ****** ****** *) // fun{a:t0p} list0_fset_at_exn (list0(INV(a)), i0: int, x0: a): 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): list0(a) fun{a:t0p} list0_fexch_at_opt (list0(INV(a)), i0: int, x0: &a >> a): Option_vt(list0(a)) // (* ****** ****** *) // fun{a:t0p} print_list0(xs: list0(INV(a))): void fun{a:t0p} prerr_list0(xs: list0(INV(a))): void // fun{a:t0p} fprint_list0 ( out: FILEref, xs: list0(INV(a)) ) : void // end of [fprint_list0] fun{a:t0p} fprint_list0_sep ( out: FILEref, xs: list0(INV(a)), sep: string ) : void // end of [fprint_list0_sep] // overload print with print_list0 overload prerr with prerr_list0 // overload fprint with fprint_list0 overload fprint with fprint_list0_sep // (* ****** ****** *) // fun{a:t0p} fprint_listlist0_sep ( out: FILEref , xss: list0(list0(INV(a))), sep1: string, sep2: string ) : void // end of [fprint_list0_sep] // overload fprint with fprint_listlist0_sep // (* ****** ****** *) fun{a:t0p} list0_insert_at_exn ( SHR(list0(INV(a))), i: int, x: (a) ) : list0(a) // endfun (* ****** ****** *) // fun{a:t0p} list0_remove_at_exn (SHR(list0(INV(a))), int): list0(a) // end of [list0_remove_at_exn] // fun{a:t0p} list0_takeout_at_exn ( xs: SHR(list0(INV(a))), i: int, x: &a? >> a ) : list0(a) // end-of-function // overload remove_at with list0_remove_at_exn overload takeout_at with list0_takeout_at_exn // (* ****** ****** *) // fun {a:t0p} list0_append ( xs: NSH(list0(INV(a))), ys: SHR(list0(a)) ) :<> list0(a) // overload + with list0_append // 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) // end of [mul_int_list0] // (* ****** ****** *) // 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) // end of [list0_reverse_append] // 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): list0(a) // end of [list0_take_exn] fun{a:t0p} list0_drop_exn (xs: SHR(list0(INV(a))), i: int): list0(a) // end of [list0_drop_exn] (* ****** ****** *) // fun {a:t0p} {res:t0p} list0_cata ( xs: list0(INV(a)) , f_nil: cfun0(res), f_cons: cfun2(a, list0(a), res) ) : (res) // end of [list0_cata] // (* ****** ****** *) // fun {a:t0p} list0_app ( xs: list0(INV(a)), fwork: cfun(a, void) ) : void // end of [list0_app] // (* ****** ****** *) // fun{a:t0p} list0_foreach ( xs: list0(INV(a)), fwork: cfun(a, void) ) : void // end of [list0_foreach] // fun{a:t0p} list0_foreach_method ( xs: list0(INV(a))) (fwork: cfun(a, void) ) : void // end of [list0_foreach_method] // overload .foreach with list0_foreach_method // (* ****** ****** *) // fun{a:t0p} list0_rforeach ( xs: list0(INV(a)), fwork: cfun(a, void) ) : void // end of [list0_rforeach] // fun{a:t0p} list0_rforeach_method ( xs: list0(INV(a))) (fwork: cfun(a, void) ) : void // end of [list0_rforeach_method] // overload .rforeach with list0_rforeach_method // (* ****** ****** *) // fun{a:t0p} list0_iforeach ( xs: list0(INV(a)), fwork: cfun2(intGte(0), a, void) ) : intGte(0)(*length*) // end of [list0_iforeach] // fun{a:t0p} list0_iforeach_method ( xs: list0(INV(a)))(fwork: cfun2(intGte(0), a, void) ) : intGte(0)(*length*) // end of [list0_iforeach_method] // overload .iforeach with list0_iforeach_method // (* ****** ****** *) fun {a1,a2:t0p} list0_foreach2 ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , fwork: cfun2(a1, a2, void) ) : void // end of [list0_foreach2] fun{a1,a2:t0p} list0_foreach2_eq ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , fwork: cfun2(a1, a2, void), sgn: &int? >> int ) : void // end of [list0_foreach2_eq] (* ****** ****** *) // fun{ res:t0p}{a:t0p } list0_foldleft ( xs: list0(INV(a)), ini: res, fopr: cfun2(res, a, res) ) : res // end of [list0_foldleft] // fun{ res:t0p}{a:t0p } list0_foldleft_method ( xs: list0(INV(a)), TYPE(res))(ini: res, fopr: cfun2(res, a, res) ) : res // end of [list0_foldleft_method] // 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 // end of [list0_ifoldleft] // fun{ res:t0p}{a:t0p } list0_ifoldleft_method ( xs: list0(INV(a)), TYPE(res))(ini: res, fopr: cfun3(res, int, a, res) ) : res // end of [list0_ifoldleft_method] // overload .ifoldleft with list0_ifoldleft_method // (* ****** ****** *) fun {res:t0p} {a1,a2:t0p} list0_foldleft2 ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , ini: res, fopr: cfun3(res, a1, a2, res) ) : res // end of [list0_foldleft2] (* ****** ****** *) // fun{ a:t0p}{res:t0p } list0_foldright ( xs: list0(INV(a)), fopr: cfun2(a, res, res), snk: res ) : res // end of [list0_foldright] // fun{ a:t0p}{res:t0p } list0_foldright_method ( xs: list0(INV(a)), TYPE(res))(fopr: cfun2(a, res, res), snk: res ) : res // end of [list0_foldright_method] // overload .foldright with list0_foldright_method // (* ****** ****** *) // (* fun{ a:t0p}{res:t0p } list0_ifoldright (xs: list0(INV(a)), fopr: cfun3(int, a, res, res), snk: res): res // end of [list0_ifoldright] *) // (* ****** ****** *) // fun {a:t0p} list0_exists (xs: list0(INV(a)), pred: cfun(a, bool)): bool // fun {a:t0p} list0_exists_method (xs: list0(INV(a))) (pred: cfun(a, bool)): bool // overload .exists with list0_exists_method // (* ****** ****** *) // fun {a:t0p} list0_iexists ( xs: list0(INV(a)), pred: cfun(intGte(0), a, bool) ) : bool // end of [list0_iexists] // fun {a:t0p} list0_iexists_method ( xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool) ) : bool // end of [list0_iexists_method] // overload .iexists with list0_iexists_method // (* ****** ****** *) // fun {a1,a2:t0p} list0_exists2 ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , pred: cfun2(a1, a2, bool) ) : bool // end of [list0_exists2] // fun {a1,a2:t0p} list0_exists2_eq ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , pred: cfun2(a1, a2, bool), sgn: &int? >> int ) : bool // end of [list0_exists2_eq] // (* ****** ****** *) // fun {a:t0p} list0_forall (xs: list0(INV(a)), pred: cfun(a, bool)): bool // fun {a:t0p} list0_forall_method (xs: list0(INV(a))) (pred: cfun(a, bool)): bool // overload .forall with list0_forall_method // (* ****** ****** *) // fun {a:t0p} list0_iforall ( xs: list0(INV(a)), pred: cfun(intGte(0), a, bool) ) : bool // end of [list0_iforall] // fun {a:t0p} list0_iforall_method ( xs: list0(INV(a))) (pred: cfun(intGte(0), a, bool) ) : bool // end of [list0_iforall_method] // overload .iforall with list0_iforall_method // (* ****** ****** *) // fun {a1,a2:t0p} list0_forall2 ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , pred: cfun2(a1, a2, bool) ) : bool // end of [list0_forall2] fun {a1,a2:t0p} list0_forall2_eq ( xs1: list0(INV(a1)) , xs2: list0(INV(a2)) , pred: cfun2(a1, a2, bool), sgn: &int? >> int ) : bool // end of [list0_forall2_eq] // (* ****** ****** *) fun {a:t0p} list0_equal ( xs1: list0(INV(a)) , xs2: list0(INV(a)), eqfn: cfun2(a, a, bool) ) : bool // end of [list0_equal] fun {a:t0p} list0_compare ( xs1: list0(INV(a)) , xs2: list0(INV(a)), cmpfn: cfun2(a, a, int) ) : (int) // end of [list0_compare] (* ****** ****** *) // fun {a:t0p} list0_find_exn (xs: list0(INV(a)), pred: cfun(a, bool)): (a) fun {a:t0p} list0_find_opt (xs: list0(INV(a)), pred: cfun(a, bool)): Option_vt(a) // fun {a:t0p} list0_find_exn_method (xs: list0(INV(a)))(pred: cfun(a, bool)): (a) fun {a:t0p} list0_find_opt_method (xs: list0(INV(a)))(pred: cfun(a, bool)): Option_vt(a) // overload .find with list0_find_exn_method overload .find_opt with list0_find_opt_method // (* ****** ****** *) // fun {a:t0p} list0_find_index ( xs: list0(INV(a)), pred: cfun(a, bool) ) : intGte(~1) // end of [list0_find_index] // (* ****** ****** *) // fun {a:t0p} list0_find_suffix ( xs: list0(INV(a)), pred: cfun(list0(a), bool) ) : list0(a) // end of [list0_find_suffix] // (* ****** ****** *) // fun {a:t0p} list0_skip_while ( xs: list0(INV(a)), pred: cfun(a, bool) ) : list0(a) // end of [list0_skip_while] fun {a:t0p} list0_skip_until ( xs: list0(INV(a)), pred: cfun(a, bool) ) : list0(a) // end of [list0_skip_until] // (* ****** ****** *) // fun {a:t0p} list0_take_while ( xs: list0(INV(a)), pred: cfun(a, bool) ) : list0(a) // end of [list0_take_while] fun {a:t0p} list0_take_until ( xs: list0(INV(a)), pred: cfun(a, bool) ) : list0(a) // end of [list0_take_until] // (* ****** ****** *) // fun{ a,b:t0p } list0_assoc_exn ( list0@(INV(a), b), x0: a, eq: cfun(a, a, bool) ) : (b) // end-of-function fun{ a,b:t0p } list0_assoc_opt ( list0@(INV(a), b), x0: a, eq: cfun(a, a, bool) ) : Option_vt (b) // end-of-function // (* ****** ****** *) // fun {a:t0p} list0_filter (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) // end of [list0_map] // fun {a:t0p} {b:t0p} list0_mapopt ( xs: list0(INV(a)), fopr: cfun(a, Option_vt(b)) ) : list0(b) // end of [list0_mapopt] // (* ****** ****** *) // fun {a:t0p} {b:t0p} list0_map_method ( xs: list0(INV(a)), TYPE(b))(fopr: cfun(a, b) ) : list0(b) // end-of-function // fun {a:t0p} {b:t0p} list0_mapopt_method ( xs: list0(INV(a)), TYPE(b))(fopr: cfun(a, Option_vt(b)) ) : list0(b) // end-of-function // overload .map with list0_map_method overload .mapopt with list0_mapopt_method // (* ****** ****** *) // fun {a:t0p} list0_mapcons (x0: a, xss: list0(list0(INV(a)))): list0(list0(a)) // overload * with list0_mapcons // (* ****** ****** *) // fun {a:t0p} {b:t0p} list0_mapjoin ( xs: list0(INV(a)), fopr: cfun(a, list0(b)) ) : list0(b) // end-of-function // fun {a:t0p} {b:t0p} list0_mapjoin_method ( xs: list0(INV(a)))(fopr: cfun(a, list0(b)) ) : list0(b) // end of [list0_mapjoin_method] // 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) // end of [list0_map2] // fun{ a1, a2:t0p}{b:t0p } list0_imap2 ( list0(INV(a1)), list0(INV(a2)), fopr: cfun3(int, a1, a2, b) ) : list0(b) // end of [list0_imap2] // (* ****** ****** *) // fun{a:t0p} list0_tabulate {n:nat} (n: int(n), fopr: cfun(natLt(n), a)): list0(a) fun{a:t0p} list0_tabulate_opt {n:nat} (n: int(n), fopr: cfun(natLt(n), Option_vt(a))): list0(a) // (* ****** ****** *) // fun {x,y:t0p} list0_zip ( list0(INV(x)), list0(INV(y)) ) :<> list0 @(x, y) // end-of-fun // (* fun{ x,y:t0p}{z:t0p } list0_zipwith (list0(INV(x)), list0(INV(y)), fopr: cfun2(x, y, z)): list0(z) *) macdef list0_zipwith = list0_map2 // (* ****** ****** *) // fun {x,y:t0p} list0_cross (list0(INV(x)), list0(INV(y))):<> list0 @(x, y) // overload * with list0_cross of 10 // (* ****** ****** *) // fun{ x,y:t0p}{z:t0p } list0_crosswith ( list0(INV(x)), list0(INV(y)), fopr: cfun2(x, y, z) ) : list0(z) // end of [list0_crosswith] // (* ****** ****** *) // fun {x:t0p} list0_choose2_foreach ( list0(INV(x)), fwork: cfun2(x, x, void) ) : void // end-of-function fun {x:t0p} list0_choose2_foreach_method ( list0(INV(x))) (fwork: cfun2(x, x, void) ) : void // end-of-function // 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 // end-of-function fun {x,y:t0p} list0_xprod2_foreach_method ( list0(INV(x)) , list0(INV(y)))(fwork: cfun2(x, y, void) ) : void // end-of-function // fun{ x,y:t0p } list0_xprod2_iforeach ( list0(INV(x)) , list0(INV(y)) , fwork: cfun4(intGte(0), x, intGte(0), y, void) ) : void // end-of-function fun {x,y:t0p} list0_xprod2_iforeach_method ( list0(INV(x)), list0(INV(y)) ) ( fwork: cfun4(intGte(0), x, intGte(0), y, void) ) : void // end-of-function // 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))): stream_vt(a) // fun{a:t0p} un_streamize_list0_elt (stream_vt(INV(a))): list0(a) // (* ****** ****** *) // fun{a:t0p} streamize_list0_suffix (list0(INV(a))): stream_vt(list0(a)) // (* ****** ****** *) // fun{a:t0p} streamize_list0_choose2 (list0(INV(a))): stream_vt(@(a, a)) // (* ****** ****** *) // fun {a:t0p} streamize_list0_nchoose (list0(INV(a)), intGte(0)): stream_vt(list0(a)) // (* fun {a:t0p} streamize_list0_nchoose_rest (list0(INV(a)), intGte(0)): stream_vt(@(list0(a), list0(a))) *) // (* ****** ****** *) // fun {a,b:t0p} streamize_list0_zip ( list0(INV(a)) , list0(INV(b))): stream_vt(@(a, b)) fun {a,b:t0p} streamize_list0_cross ( list0(INV(a)) , list0(INV(b))): stream_vt(@(a, b)) // (* ****** ****** *) // fun{a:t0p} list0_is_ordered (xs: list0(INV(a)), cmp: (a, a) - int): bool // (* ****** ****** *) fun{a:t0p} list0_mergesort (NSH(list0(INV(a))), cmp: (a, a) - int):<> list0(a) // end of [list0_mergesort] (* ****** ****** *) fun{a:t0p} list0_quicksort (NSH(list0(INV(a))), cmp: (a, a) - int):<> list0(a) // end of [list0_quicksort] (* ****** ****** *) (* end of [list0.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2017 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: January, 2018 *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // #define list0_vt_sing(x) list0_vt_cons(x, list0_vt_nil()) // #define list0_vt_pair(x1, x2) list0_vt_cons (x1, list0_vt_cons(x2, list0_vt_nil())) // (* ****** ****** *) // castfn list0_vt2t {a:t@ype}(list0_vt(INV(a))):<> list0(a) // (* ****** ****** *) // castfn g0ofg1_list_vt {a:vt@ype} (List_vt(INV(a))):<> list0_vt(a) castfn g1ofg0_list_vt {a:vt@ype} (list0_vt(INV(a))):<> List0_vt(a) // overload g0ofg1 with g0ofg1_list_vt overload g1ofg0 with g1ofg0_list_vt // (* ****** ****** *) // fun {a:t0p} list0_vt_free(xs: list0_vt(a)): void // (* ****** ****** *) // fun {a:vt0p} list0_vt_append (list0_vt(a), list0_vt(a)): list0_vt(a) // (* ****** ****** *) // fun {a:vt0p} list0_vt_reverse(xs: list0_vt(a)): list0_vt(a) // (* ****** ****** *) (* end of [list0_vt.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: July, 2012 *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) %{# #include \ "libats/ML/CATS/array0.cats" %} // end of [%{#] (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) typedef SHR(a:type) = a // for commenting purpose typedef NSH(a:type) = a // for commenting purpose (* ****** ****** *) #if(0) // // HX: in [basis.sats] // abstype array0_vt0ype_type (a: vt@ype(*invariant*)) = ptr // stadef array0 = array0_vt0ype_type // #endif // end of [#if(0)] (* ****** ****** *) (* typedef array0(a: vt@ype) = arrszref(a) *) (* ****** ****** *) (* sortdef t0p = t@ype sortdef vt0p = viewt@ype *) (* ****** ****** *) // fun {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)): array0(a) // fun{} array0_make_arrayref {a:vt0p}{n:int} (Arf: arrayref(a, n), n: size_t(n)): 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): array0(a) // fun{a:t0p} array0_make_elt_size (asz: size_t, x0: a): 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))): array0(a) fun{a:t0p} array0_make_rlist (xs: list0(INV(a))): array0(a) // (* ****** ****** *) fun{a:t0p} array0_make_subarray ( A: array0(a) , st: size_t, ln: size_t): array0(a) // end of [array0_make_subarray] (* ****** ****** *) fun{a:t0p} array0_get_at_size (A: array0(a), i: size_t): (a) fun {a:t0p}{tk:tk} array0_get_at_gint (A: array0(a), i: g0int(tk)): (a) fun {a:t0p}{tk:tk} array0_get_at_guint (A: array0(a), i: g0uint(tk)): (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): void fun {a:t0p}{tk:tk} array0_set_at_gint ( A: array0(a) , i: g0int(tk), x: a): void fun {a:t0p}{tk:tk} array0_set_at_guint ( A: array0(a) , i: g0uint(tk), x: a): 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 >> _): void // fun {a:vt0p}{tk:tk} array0_exch_at_gint ( A: array0(a) , i: g0int(tk), x: &a >> _): void fun {a:vt0p}{tk:tk} array0_exch_at_guint ( A: array0(a) , i: g0uint(tk), x: &a >> _): 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): void // end of [array0_interchange] // (* ****** ****** *) // fun{a:vt0p} array0_subcirculate ( A: array0(a) , i: size_t, j: size_t): void // end of [array0_subcirculate] // (* ****** ****** *) // fun{a:vt0p} print_array0 (A: array0(a)): void fun{a:vt0p} prerr_array0 (A: array0(a)): void // (* fun{} fprint_array$sep (out: FILEref): void *) fun{a:vt0p} fprint_array0 (out: FILEref, A: array0(a)): void fun{a:vt0p} fprint_array0_sep (out: FILEref, A: array0(a), sep: string): void // (* ****** ****** *) fun{a:t0p} array0_copy(array0(a)): array0(a) (* ****** ****** *) // fun{a:t0p} array0_append (array0(a), array0(a)): array0(a) // end of [array0_append] // 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) - b ) : array0(b) // end of [array0_map] fun {a:vt0p} {b:vt0p} array0_map_method ( A0: array0(a), TYPE(b))(fopr: (&a) - b ) : array0(b) // end of [array0_map_method] // overload .map with array0_map_method // (* ****** ****** *) // fun {a:vt0p} array0_tabulate {n:int} ( asz: size_t(n), fopr: (sizeLt(n)) - a ) : array0(a) // end of [array0_tabulate] // (* ****** ****** *) // fun {a:vt0p} array0_tabulate_method_int {n:nat} ( asz: int(n))(fopr: (natLt(n)) - a ) : array0(a) // end of [array0_tabulate_method_int] fun {a:vt0p} array0_tabulate_method_size {n:int} ( asz: size_t(n))(fopr: (sizeLt(n)) - a ) : array0(a) // end of [array0_tabulate_method_size] // overload .array0_tabulate with array0_tabulate_method_int overload .array0_tabulate with array0_tabulate_method_size // (* ****** ****** *) // (* ** HX: ** Raising NotFoundExn ** if no satisfying element is found *) fun {a:vt0p} array0_find_exn ( xs: array0(a), pred: (&a) - bool ) : size_t // end of [array0_find_exn] // fun {a:vt0p} array0_find_opt ( xs: array0(a), pred: (&a) - bool ) : Option_vt(size_t) // end-of-function // (* ****** ****** *) // fun {a:vt0p} array0_exists ( xs: array0(a), pred: (&a) - bool ) : bool // end of [array0_exists] fun {a:vt0p} array0_exists_method ( xs: array0(a))(pred: (&a) - bool ) : bool // end of [array0_exists_method] // overload .exists with array0_exists_method // (* ****** ****** *) // fun {a:t0p} array0_iexists ( xs: array0(a) , pred: (size_t, &a) - bool ) : bool // end of [array0_iexists] // fun {a:t0p} array0_iexists_method (xs: array0(a)) (pred: ( size_t, &a ) - bool ) : bool // end of [array0_iexists_method] // overload .iexists with array0_iexists_method // (* ****** ****** *) // fun {a:vt0p} array0_forall ( xs: array0(a), pred: (&a) - bool ) : bool // end of [array0_forall] fun {a:vt0p} array0_forall_method ( xs: array0(a)) (pred: (&a) - bool ) : bool // end of [array0_forall_method] // overload .forall with array0_forall_method // (* ****** ****** *) // fun {a:t0p} array0_iforall ( xs: array0(a) , pred: (size_t, &a) - bool ) : bool // end of [array0_iforall] // fun {a:t0p} array0_iforall_method (xs: array0(a)) (pred: ( size_t, &a ) - bool ) : bool // end of [array0_iforall_method] // overload .iforall with array0_iforall_method // (* ****** ****** *) // fun {a:vt0p} array0_foreach ( A0: array0(a) , fwork: (&a >> _) - void ) : void // end of [array0_foreach] // fun {a:vt0p} array0_foreach_method (A0: array0(a)) (fwork: (&a >> _) - void): void // end of [array0_foreach_methon] // overload .foreach with array0_foreach_method // (* ****** ****** *) // fun {a:vt0p} array0_iforeach ( A0: array0(a) , fwork: (size_t, &a >> _) - void ) : void // end of [array0_iforeach] // fun {a:vt0p} array0_iforeach_method (A0: array0(a)) (fwork: (size_t, &a >> _) - void): void // end of [array0_iforeach_method] // overload .iforeach with array0_iforeach_method // (* ****** ****** *) // fun {a:vt0p} array0_rforeach ( A0: array0(a) , fwork: (&a >> _) - void ) : void // end of [array0_rforeach] // fun {a:vt0p} array0_rforeach_method (A0: array0(a)) (fwork: (&a >> _) - void): void // end of [array0_rforeach] // overload .rforeach with array0_rforeach_method // (* ****** ****** *) // fun{ res:vt0p}{a:vt0p } array0_foldleft ( A0: array0(a) , ini: res, fopr: (res, &a) - res ) : res // end of [array0_foldleft] // fun{ res:vt0p}{a:vt0p } array0_foldleft_method ( A: array0(a), TYPE(res) ) ( ini: res, fopr: (res, &a) - res ) : res // end of [array0_foldleft_method] // overload .foldleft with array0_foldleft_method // (* ****** ****** *) // fun{ res:vt0p}{a:vt0p } array0_ifoldleft ( A0: array0(a), ini: res , fopr: (res, size_t, &a) - res ) : res // end of [array0_ifoldleft] // fun{ res:vt0p}{a:vt0p } array0_ifoldleft_method ( A: array0(a), TYPE(res) ) ( ini: res , fopr: (res, size_t, &a) - res ) : res // end of [array0_ifoldleft_method] // overload .ifoldleft with array0_ifoldleft_method // (* ****** ****** *) // // HX: this one is tail-recursive! // fun{ a:vt0p}{res:vt0p } array0_foldright ( A0: array0(a) , fopr: (&a, res) - res, snk: res ) : res // end of [array0_foldright] // fun{ a:vt0p}{res:vt0p } array0_foldright_method ( A: array0(a), TYPE(res) ) ( fopr: (&a, res) - res, snk: res ) : res // end of [array0_foldright_method] // overload .foldright with array0_foldright_method // (* ****** ****** *) // fun {a:t0p} streamize_array0_elt (A0: array0(a)): stream_vt(a) // (* ****** ****** *) // fun {a:vt0p} array0_is_ordered ( A0: array0(a) , cmp: (&a, &a) - int): bool // (* ****** ****** *) // fun {a:vt0p} array0_quicksort ( A0: array0(a) , cmp: (&a, &a) - int): void // (* ****** ****** *) // // Overloading certain symbols // (* ****** ****** *) // 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 (* ****** ****** *) (* end of [array0.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: December, 2012 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // #define // prefix for external ATS_EXTERN_PREFIX "atslib_ML_" // names // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) typedef SHR(a:type) = a // for commenting purpose typedef NSH(a:type) = a // for commenting purpose (* ****** ****** *) #if(0) // // HX: in [basis.sats] // abstype matrix0_vt0ype_type (a: vt@ype(*invariant*)) = ptr stadef matrix0 = matrix0_vt0ype_type // #endif // #if(0) (* ****** ****** *) // (* typedef matrix0(a: vt@ype) = mtrxszref(a) *) // (* ****** ****** *) // (* // // HX: already defined // sortdef t0p = t@ype and vt0p = viewt@ype // *) // (* ****** ****** *) // fun{} matrix0_of_mtrxszref {a:vt0p}(mtrxszref(a)):<> matrix0(a) // fun{} mtrxszref_of_matrix0 {a:vt0p}(M: matrix0(a)):<> mtrxszref(a) // (* ****** ****** *) // symintr matrix0_make_elt // fun{a:t0p} matrix0_make_elt_int (nrow: int, ncol: int, init: a): matrix0(a) // end of [matrix0_make_elt] fun{a:t0p} matrix0_make_elt_size (nrow: size_t, ncol: size_t, init: a): matrix0(a) // end of [matrix0_make_elt] // 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): a // fun{a:t0p} matrix0_get_at_size (M: matrix0(a), i: size_t, j: size_t): 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): void // fun{a:t0p} matrix0_set_at_size (M: matrix0(a), i: size_t, j: size_t, x: a): void // symintr matrix0_set_at // overload matrix0_set_at with matrix0_set_at_int overload matrix0_set_at with matrix0_set_at_size // (* ****** ****** *) // fun {a:vt0p} print_matrix0(M: matrix0(a)): void fun {a:vt0p} prerr_matrix0(M: matrix0(a)): void // (* fprint_matrix$sep1 // col separation fprint_matrix$sep2 // row separation *) // fun {a:vt0p} fprint_matrix0 (out: FILEref, M: matrix0(a)): void // fun {a:vt0p} fprint_matrix0_sep ( out: FILEref, M: matrix0(a), sep1: string, sep2: string ) : void // end of [fprint_matrix0_sep] // (* ****** ****** *) 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) // end of [matrix0_tabulate] // (* ****** ****** *) // 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) // end of [matrix0_tabulate_method_int] // 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) // end of [matrix0_tabulate_method_size] // 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 >> _) - void ) : void // end of [matrix0_foreach] // fun {a:vt0p} matrix0_iforeach ( M : matrix0(a), fwork: (size_t, size_t, &a >> _) - void ) : void // end of [matrix0_iforeach] // (* ****** ****** *) fun{ res:vt0p}{a:vt0p } matrix0_foldleft ( M: matrix0(a), ini: res, fopr: (res, &a) - res ) : res // end of [matrix0_foldleft] fun{ res:vt0p}{a:vt0p } matrix0_ifoldleft ( M: matrix0(a), ini: res, fopr: (res, size_t, size_t, &a) - res ) : res // end of [matrix0_ifoldleft] (* ****** ****** *) // // overloading for certain symbols // (* ****** ****** *) overload .nrow with matrix0_get_nrow overload .ncol with matrix0_get_ncol (* ****** ****** *) // overload [] with matrix0_get_at_int of 0 overload [] with matrix0_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 // (* ****** ****** *) (* end of [matrix0.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2016 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: October, 2016 *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" // // HX: prefix for external names // #define ATS_EXTERN_PREFIX "atslib_ML_" // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // fun {a:t0p} stream2list0 (xs: stream(a)): list0(a) // (* ****** ****** *) // fun {a:t0p} stream_make_list0 (xs: list0(a)): stream(a) // (* ****** ****** *) // fun{} intgte_stream (start: int): stream(int) // (* ****** ****** *) // fun{} stream_make_intrange_lr (l: int, r: int): stream(int) fun{} stream_make_intrange_lrd (l: int, r: int, d: int): 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) - b ) : stream(b) // fun {a:t0p}{b:t0p} stream_map_method ( xs: stream(INV(a)), TYPE(b) ) (fopr: (a) - b): stream(b) // overload .map with stream_map_method // (* ****** ****** *) // fun{ a:t0p}{b:t0p } stream_imap ( xs: stream(INV(a)), fopr: (intGte(0), a) - b ) : stream(b) // end-of-fun // fun {a:t0p}{b:t0p} stream_imap_method ( xs: stream(INV(a)), TYPE(b) ) (fopr: (intGte(0), a) - b): stream(b) // overload .imap with stream_imap_method // (* ****** ****** *) // fun {a:t0p} stream_filter ( xs: stream(INV(a)), pred: (a) - bool ) : stream(a) // end-of-function // fun {a:t0p} stream_filter_method ( xs: stream(INV(a)) ) ( pred: (a) - bool ) : stream(a) // end-of-function // overload .filter with stream_filter_method // (* ****** ****** *) // fun{ res:t0p}{x:t0p } stream_scan ( stream(INV(x)), ini: res, (res, x) - res ) : stream(res) // end-of-function // fun{ res:t0p}{x:t0p } stream_scan_method ( stream(INV(x)), TYPE(res) ) (res, (res, x) - res) : stream(res) // overload .scan with stream_scan_method // (* ****** ****** *) // fun {a:t0p} stream_foreach (xs: stream(a), fwork: (a) - void): void // fun {a:t0p} stream_foreach_method (xs: stream(INV(a)))(fwork: (a) - void): void // overload .foreach with stream_foreach_method // (* ****** ****** *) // fun {a:t0p} stream_iforeach ( xs: stream(a) , fwork: (intGte(0), a) - void): void // fun {a:t0p} stream_iforeach_method (xs: stream(INV(a))) (fwork: (intGte(0), a) - void): void // overload .iforeach with stream_iforeach_method // (* ****** ****** *) // fun{ res:vt0p}{a:t0p } stream_foldleft (stream(INV(a)), ini: res, fopr: (res, a) - res): res fun{ res:vt0p}{a:t0p } stream_foldleft_method (stream(INV(a)), TYPE(res))(res, (res, a) - res): res // overload .foldleft with stream_foldleft_method // (* ****** ****** *) (* end of [stream.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2011-2016 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmmhwxiATgmailDOTcom *) (* Start time: October, 2016 *) (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) // staload "libats/ML/SATS/basis.sats" // (* ****** ****** *) // fun {a:t0p} stream2list0_vt (xs: stream_vt(a)): list0(a) // (* ****** ****** *) // fun {a:t0p} stream_vt_make_list0 (xs: list0(a)): stream_vt(a) // (* ****** ****** *) // fun{} intGte_stream_vt (start: int): stream_vt(int) // (* ****** ****** *) // fun{} stream_vt_make_intrange_lr (l: int, r: int): stream_vt(int) fun{} stream_vt_make_intrange_lrd (l: int, r: int, d: int): 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?!) - b ) - stream_vt(b) // overload .map with stream_vt_map_method // (* ****** ****** *) // fun{a:t0p} stream_vt_filter_method ( xs: stream_vt(INV(a)) ) : ((&a)-bool)-stream_vt(a) // overload .filter with stream_vt_filter_method // (* ****** ****** *) // fun{a:vt0p} stream_vt_foreach_method (xs: stream_vt(INV(a))) : ((&a >> a?!) - void) - void // fun{a:vt0p} stream_vt_rforeach_method (xs: stream_vt(INV(a))) : ((&a >> a?!) - void) - 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?!) - void) - 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?!) - res) - res fun{ res:vt0p }{a:vt0p} stream_vt_ifoldleft_method ( xs: stream_vt(INV(a)), TYPE(res) ) : (res, (intGte(0), res, &a >> a?!) - res) - res // overload .foldleft with stream_vt_foldleft_method overload .ifoldleft with stream_vt_ifoldleft_method // (* ****** ****** *) (* end of [stream_vt.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: January, 2013 *) (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) typedef SHR(a:type) = a // for commenting purpose typedef NSH(a:type) = a // for commenting purpose (* ****** ****** *) typedef charlst0 = list0 (char) typedef stringlst0 = list0 (string) (* ****** ****** *) (* fun fileref_open_opt (path: NSH(string), fm: file_mode): option0 (FILEref) // end of [fileref_open_opt] *) (* ****** ****** *) // fun fileref_get_line_charlst(filr: FILEref): charlst0 // (* ** HX: for handling files of "tiny" size *) fun fileref_get_lines_charlstlst(filr: FILEref): list0(charlst0) // (* ****** ****** *) // fun fileref_get_line_string(filr: FILEref): string // (* ** HX: for handling files of "tiny" size *) fun fileref_get_lines_stringlst(filr: FILEref): stringlst0 // fun{} 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) // (* ****** ****** *) // (* // // HX: this one is in prelude/filebas // fun{} fileref_get_word$isalpha(c0: charNZ): bool *) 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) // (* ****** ****** *) (* end of [filebas.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2014 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: September, 2014 *) (* Authoremail: gmhwxiATgmailDOTcom*) (* ****** ****** *) // // HX-2013-04: // intrange(l, r) is for integers i satisfying l <= i < r // (* ****** ****** *) // #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // fun{} int_repeat_lazy (n: int, 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_cloref *) 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_cloref *) 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_cloref *) 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_cloref *) 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_cloref *) 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_cloref *) 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_cloref *) 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_cloref *) overload .rforeach with intrange_rforeach_method // (* ****** ****** *) // fun {res:vt0p} intrange_foldleft_cloref ( l: int, r: int, ini: res, f0: cfun2(res, int, res) ) : res // end of [intrange_foldleft_cloref] // fun {res:vt0p} intrange_foldleft_method ((int, int), TYPE(res))(ini: res, f0: cfun2(res, int, res)): res // (* overload foldleft with intrange_foldleft_cloref *) overload .foldleft with intrange_foldleft_method // (* ****** ****** *) // fun {res:vt0p} intrange_foldright_cloref ( l: int, r: int, f0: cfun2(int, res, res), snk: res ) : res // end of [intrange_foldright_cloref] // fun {res:vt0p} intrange_foldright_method ((int, int), TYPE(res))(f0: cfun2(int, res, res), snk: res): res // (* overload foldright with intrange_foldright_cloref *) 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 // (* ****** ****** *) // (* HX: cross product *) // 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 // (* ****** ****** *) (* end of [intrange.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: August, 2013 *) (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // // HX: for maps of elements of type (a) // abstype map_type ( key:t@ype , itm:t0ype+ ) = ptr(*boxed*) // typedef map(key:t0p , itm:t0p) = map_type(key, itm) // (* ****** ****** *) // fun {key:t0p} compare_key_key(x1: key, x2: key):<> int // (* ****** ****** *) // fun{} funmap_nil {key,itm:t0p}():<> map(key, itm) fun{} funmap_make_nil {key,itm:t0p}():<> map(key, itm) // (* ****** ****** *) // fun{ 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) // end of [funmap_search] (* ****** ****** *) // fun{ key,itm:t0p } funmap_insert ( &map(key, INV(itm)) >> _, key, itm ) : Option_vt(itm) // end of [funmap_insert] // (* ****** ****** *) // fun{ key,itm:t0p } funmap_takeout ( map: &map(key, INV(itm)) >> _, k0: key ) : Option_vt(itm) // end of [funmap_takeout] // (* ****** ****** *) // fun{ key,itm:t0p } funmap_remove (map: &map(key, INV(itm)) >> _, k0: key): bool // (* ****** ****** *) // fun{} fprint_funmap$sep (out: FILEref): void // fprint("; ") fun{} fprint_funmap$mapto (out: FILEref): void // fprint("->") // 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) - void ) : void // end-of-function // (* ****** ****** *) // fun{ key,itm:t0p } funmap_listize (map: map(key, INV(itm))): list0 @(key, itm) // (* ****** ****** *) // fun{ key,itm:t0p } funmap_streamize (map: map(key, INV(itm))): stream_vt @(key, itm) // (* ****** ****** *) typedef map_modtype ( key: t0p, itm: t0p ) = $rec{ // nil = () -<> map(key,itm) , size = $d2ctype(funmap_size) , is_nil = (map(key,itm)) -<> bool , isnot_nil = (map(key,itm)) -<> bool , search = $d2ctype(funmap_search) , insert = $d2ctype(funmap_insert) , remove = $d2ctype(funmap_remove) , takeout = $d2ctype(funmap_takeout) , listize = $d2ctype(funmap_listize) , streamize = $d2ctype(funmap_streamize) // } (* end of [set_modtype] *) (* ****** ****** *) // fun {key:t0p ;itm:t0p} funmap_make_module((*void*)): map_modtype(key,itm) // (* ****** ****** *) (* end of [funmap.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: August, 2013 *) (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // // HX-2013-08: // for sets of elements of type a // abstype set_type ( a:t@ype+ ) = ptr(*boxed*) // typedef set(a:t0p) = set_type(a) // (* ****** ****** *) fun{a:t0p} compare_elt_elt(x: a, y: a):<> int (* ****** ****** *) fun{} funset_nil{a:t0p}():<> set(a) fun{} funset_make_nil{a:t0p}():<> set(a) (* ****** ****** *) fun{a:t0p} funset_sing(x: a): set(a) fun{a:t0p} funset_make_sing(x: a): set(a) (* ****** ****** *) fun{a:t0p} funset_make_list(xs: list0(INV(a))): set(a) (* ****** ****** *) // fun {a:t0p} fprint_funset ( out: FILEref, set: set(INV(a)) ) : void // end of [fprint_funset] // fun{} fprint_funset$sep(out: FILEref): void // fprint(", ") // overload fprint with fprint_funset // (* ****** ****** *) fun{} funset_is_nil{a:t0p}(xs: set(INV(a))):<> bool fun{} funset_isnot_nil{a:t0p}(xs: set(INV(a))):<> bool (* ****** ****** *) fun{a:t0p} funset_size(xs: set(INV(a))):<> size_t (* ****** ****** *) fun{a:t0p} funset_is_member(xs: set(INV(a)), x0: a):<> bool fun{a:t0p} funset_isnot_member(xs: set(INV(a)), x0: a):<> bool (* ****** ****** *) fun{a:t0p} funset_insert (xs: &set(INV(a)) >> _, x0: a): bool(*[x0] in [xs]*) // end of [funset_insert] (* ****** ****** *) fun{a:t0p} funset_remove (xs: &set(INV(a)) >> _, x0: a): bool(*[x0] in [xs]*) // end of [funset_remove] (* ****** ****** *) fun{a:t0p} funset_getmax_opt(xs: set(INV(a))): Option_vt(a) fun{a:t0p} funset_getmin_opt(xs: set(INV(a))): Option_vt(a) (* ****** ****** *) fun{a:t0p} funset_takeoutmax_opt(xs: &set(INV(a)) >> _): Option_vt(a) fun{a:t0p} funset_takeoutmin_opt(xs: &set(INV(a)) >> _): Option_vt(a) (* ****** ****** *) fun{a:t0p} funset_union(xs1: set(INV(a)), xs2: set(a)):<> set(a) fun{a:t0p} funset_intersect(xs1: set(INV(a)), xs2: set(a)):<> set(a) fun{a:t0p} funset_differ(xs1: set(INV(a)), xs2: set(a)):<> set(a) fun{a:t0p} funset_symdiff(xs1: set(INV(a)), xs2: set(a)):<> set(a) (* ****** ****** *) fun{a:t0p} funset_equal(xs1: set(INV(a)), xs2: set(a)):<> bool (* ****** ****** *) // // HX: set ordering induced by the ordering on elements // fun{a:t0p} funset_compare(xs1: set(INV(a)), xs2: set(a)):<> int (* ****** ****** *) // fun{a:t0p} funset_is_subset(xs1: set(INV(a)), xs2: set(a)):<> bool fun{a:t0p} funset_is_supset(xs1: set(INV(a)), xs2: set(a)):<> bool // (* ****** ****** *) // fun{a:t0p} funset_foreach(set: set(INV(a))): void fun {a:t0p} {env:vt0p} funset_foreach_env (set: set(INV(a)), env: &(env) >> _): void // end of [funset_foreach_env] // fun {a:t0p} {env:vt0p} funset_foreach$fwork(x: a, env: &(env) >> _): void // (* ****** ****** *) // fun{a:t0p} funset_foreach_cloref (set: set(INV(a)), fwork: (a) - void): void // (* ****** ****** *) // fun{a:t0p} funset_tabulate_cloref {n:nat}(int(n), fopr: (natLt(n)) - 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) , make_list = $d2ctype(funset_make_list) , size = $d2ctype(funset_size) , is_nil = (set(elt)) -<> bool , isnot_nil = (set(elt)) -<> bool , insert = $d2ctype(funset_insert) , remove = $d2ctype(funset_remove) , union = $d2ctype(funset_union) , intersect = $d2ctype(funset_intersect) , listize = $d2ctype(funset_listize) , streamize = $d2ctype(funset_streamize) // } (* end of [set_modtype] *) (* ****** ****** *) // fun {a:t@ype} funset_make_module((*void*)): set_modtype(a) // (* ****** ****** *) (* end of [funset.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: August, 2013 *) (* ****** ****** *) #define ATS_PACKNAME "ATSLIB.libats.ML" #define ATS_EXTERN_PREFIX "atslib_ML_" // prefix for external names (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) // typedef hashtbl // introduced in [basis.sats] (key:t@ype, itm:t@ype) = hashtbl(key, itm) // (* ****** ****** *) // fun{ key:t0p } hash_key(x: key):<> ulint // fun{ key:t0p } equal_key_key(x1: key, x2: key):<> bool // (* ****** ****** *) // fun{ key,itm:t0p } hashtbl_make_nil (cap: sizeGte(1)): hashtbl(key, itm) // (* ****** ****** *) // fun{} hashtbl_get_size {key,itm:t0p}(hashtbl(key, itm)): 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) // end of [hashtbl_search] fun{ key,itm:t0p } hashtbl_search_ref (tbl: hashtbl(key, INV(itm)), k: key): cPtr0(itm) // end of [hashtbl_search_ref] (* ****** ****** *) fun{ key,itm:t0p } hashtbl_insert (hashtbl(key, INV(itm)), key, itm): Option_vt(itm) // end of [hashtbl_insert] fun{ key,itm:t0p } hashtbl_insert_any (hashtbl(key, INV(itm)), key, itm): void(*inserted*) (* ****** ****** *) fun{ key,itm:t0p } hashtbl_takeout (kxs: hashtbl(key, INV(itm)), k0: key): Option_vt(itm) // end of [hashtbl_takeout] (* ****** ****** *) 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)) // end of [hashtbl_takeout_all] (* ****** ****** *) // 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 // default: fprint("; ") fun{} fprint_hashtbl$mapto (out: FILEref): void // default: fprint("->") // (* ****** ****** *) // fun{ key,itm:t@ype } fprint_hashtbl_sep_mapto ( out: FILEref , tbl: hashtbl(key, INV(itm)), sep: string, mapto: string ) : void // end of [fprint_hashtbl_sep_mapto] // (* ****** ****** *) // 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 >> _) - void ) : void // end of [hashtbl_foreach_cloref] // (* ****** ****** *) // 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)) // (* ****** ****** *) (* end of [hashtblref.sats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2017 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: December, 2017 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) #define ATS_DYNLOADFLAG 0 (* ****** ****** *) #staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) #staload "libats/ML/SATS/basis.sats" #staload "libats/ML/SATS/atspre.sats" (* ****** ****** *) // // HX-2017-12-30: // prelude/intrange // (* ****** ****** *) // implement {}(*tmp*) int_forall_cloptr (n, pred) = ( intrange_forall_cloptr<>(0, n, pred) ) (* end of [int_forall_cloref] *) implement {}(*tmp*) int_forall_cloref (n, pred) = ( intrange_forall_cloref<>(0, n, pred) ) (* end of [int_forall_cloref] *) // (* ****** ****** *) // implement {}(*tmp*) intrange_forall_cloptr ( l, r, pred ) = res where { // val res = intrange_forall_cloref<> (l, r, $UN.castvwtp1(pred)) val ((*void*)) = cloptr_free{void}($UN.castvwtp0(pred)) } // end of [intrange_forall_cloptr] // implement {}(*tmp*) intrange_forall_cloref (l, r, pred) = loop(l, r) where { // fun loop (l: int, r: int): bool = if (l < r) then ( if pred(l) then loop(l+1, r) else false ) else true // } // end of [intrange_forall_cloref] // (* ****** ****** *) // implement {}(*tmp*) int_foreach_cloptr (n, fwork) = ( intrange_foreach_cloptr<>(0, n, fwork) ) (* end of [int_foreach_cloref] *) implement {}(*tmp*) int_foreach_cloref (n, fwork) = ( intrange_foreach_cloref<>(0, n, fwork) ) (* end of [int_foreach_cloref] *) // (* ****** ****** *) // implement {}(*tmp*) intrange_foreach_cloptr ( l, r, fwork ) = res where { // val res = intrange_foreach_cloref<> (l, r, $UN.castvwtp1(fwork)) val ((*void*)) = cloptr_free{void}($UN.castvwtp0(fwork)) } // end of [intrange_foreach_cloptr] // implement {}(*tmp*) intrange_foreach_cloref (l, r, fwork) = let // implement (env)(*tmp*) intrange_foreach$cont(i, env) = true implement (env)(*tmp*) intrange_foreach$fwork(i, env) = fwork(i) // var env: void = () // in intrange_foreach_env(l, r, env) end // end of [intrange_foreach_cloref] // (* ****** ****** *) // implement {}(*tmp*) int_rforeach_cloptr (n, fwork) = ( intrange_rforeach_cloptr<>(0, n, fwork) ) (* end of [int_rforeach_cloptr] *) implement {}(*tmp*) int_rforeach_cloref (n, fwork) = ( intrange_rforeach_cloref<>(0, n, fwork) ) (* end of [int_rforeach_cloref] *) // // implement {}(*tmp*) intrange_rforeach_cloptr ( l, r, fwork ) = res where { // val res = intrange_rforeach_cloref<> (l, r, $UN.castvwtp1(fwork)) val ((*void*)) = cloptr_free{void}($UN.castvwtp0(fwork)) } // end of [intrange_rforeach_cloptr] implement {}(*tmp*) intrange_rforeach_cloref (l, r, fwork) = let // implement (env)(*tmp*) intrange_rforeach$cont(i, env) = true implement (env)(*tmp*) intrange_rforeach$fwork(i, env) = fwork(i) // var env: void = () // in intrange_rforeach_env(l, r, env) end // end of [intrange_rforeach_cloref] // (* ****** ****** *) // // HX: prelude/list // (* ****** ****** *) // implement {x}(*tmp*) list_exists_cloptr (xs, p0) = res where { // val p1 = $UN.castvwtp1(p0) val res = list_exists_cloref(xs, p1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(p0)) // } // end of [list_exists_cloptr] // implement {x}(*tmp*) list_exists_cloref (xs, pred) = let // implement(x2) list_exists$pred(x2) = pred($UN.cast{x}(x2)) // in list_exists(xs) end // end of [list_exists_cloref] // (* ****** ****** *) // implement {x}(*tmp*) list_iexists_cloptr (xs, p0) = res where { // val p1 = $UN.castvwtp1(p0) val res = list_iexists_cloref(xs, p1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(p0)) // } // end of [list_iexists_cloptr] // implement {x}(*tmp*) list_iexists_cloref {n}(xs, pred) = let // prval() = lemma_list_param(xs) // fun loop { i,j:nat | i+j == n } .. ( i: int(i), xs: list(x, j) ) :<> bool = ( case+ xs of | list_nil() => false | list_cons(x, xs) => if pred(i, x) then true else loop(i+1, xs) // end of [list_cons] ) // in loop(0, xs) end // end of [list_iexists_cloref] // (* ****** ****** *) // implement {x}(*tmp*) list_forall_cloptr (xs, p0) = res where { // val p1 = $UN.castvwtp1(p0) val res = list_forall_cloref(xs, p1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(p0)) // } // end of [list_forall_cloptr] // implement {x}(*tmp*) list_forall_cloref (xs, pred) = let // implement(x2) list_forall$pred(x2) = pred($UN.cast{x}(x2)) // in list_forall(xs) end // end of [list_forall_cloref] // (* ****** ****** *) // implement {x}(*tmp*) list_iforall_cloptr (xs, p0) = res where { // val p1 = $UN.castvwtp1(p0) val res = list_iforall_cloref(xs, p1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(p0)) // } // end of [list_iforall_cloptr] // implement {x}(*tmp*) list_iforall_cloref {n}(xs, pred) = let // prval() = lemma_list_param(xs) // fun loop { i,j:nat | i+j == n } .. ( i: int(i), xs: list(x, j) ) :<> bool = ( case+ xs of | list_nil() => true | list_cons(x, xs) => if pred(i, x) then loop(i+1, xs) else false // end of [list_cons] ) // in loop(0, xs) end // end of [list_iforall_cloref] // (* ****** ****** *) implement {x}(*tmp*) list_equal_cloref (xs1, xs2, eqfn) = list_equal(xs1, xs2) where { // implement{y} list_equal$eqfn (x1, x2) = eqfn($UN.cast(x1), $UN.cast(x2)) // } (* end of [list_equal_cloref] *) (* ****** ****** *) implement {x}(*tmp*) list_compare_cloref (xs1, xs2, cmpfn) = list_compare(xs1, xs2) where { // implement{y} list_compare$cmpfn (x1, x2) = cmpfn($UN.cast(x1), $UN.cast(x2)) // } (* end of [list_compare_cloref] *) (* ****** ****** *) implement {x}(*tmp*) list_app_fun (xs, fwork) = list_app(xs) where { // implement {x2}(*tmp*) list_app$fwork(x2) = fwork($UN.cast{x}(x2)) // } (* end of [list_app_fun] *) implement {x}(*tmp*) list_app_clo (xs, fwork) = list_app(xs) where { // val fwork = $UN.cast{cfun(x,void)}(addr@fwork) // implement {x2}(*tmp*) list_app$fwork(x2) = fwork($UN.cast{x}(x2)) // } (* end of [list_app_clo] *) implement {x}(*tmp*) list_app_cloref (xs, fwork) = let // fun loop {n:nat} .. ( xs: list(x, n) , fwork: (x) - void ) : void = ( // case+ xs of | list_nil() => () | list_cons(x, xs) => (fwork(x); loop(xs, fwork)) // ) (* end of [loop] *) // prval() = lemma_list_param(xs) // in loop(xs, fwork) end // end of [list_app_cloref] (* ****** ****** *) implement {x}{y}(*tmp*) list_map_fun (xs, fopr) = let // implement {x2}{y2} list_map$fopr(x2) = $UN.castvwtp0{y2}(fopr($UN.cast{x}(x2))) // in list_map(xs) end // end of [list_map_fun] implement {x}{y}(*tmp*) list_map_clo (xs, fopr) = let // val fopr = $UN.cast{(x) - y}(addr@fopr) // implement {x2}{y2} list_map$fopr(x2) = $UN.castvwtp0{y2}(fopr($UN.cast{x}(x2))) // in list_map(xs) end // end of [list_map_clo] implement {x}{y}(*tmp*) list_map_cloref (xs, fopr) = let // implement {x2}{y2} list_map$fopr(x2) = $UN.castvwtp0{y2}(fopr($UN.cast{x}(x2))) // in list_map(xs) end // end of [list_map_cloref] (* ****** ****** *) implement {a}(*tmp*) list_tabulate_fun (n, fopr) = list_tabulate(n) where { // val fopr = $UN.cast{int->a}(fopr) // implement(a2) list_tabulate$fopr(n) = $UN.castvwtp0{a2}(fopr(n)) // } (* end of [list_tabulate_fun] *) implement {a}(*tmp*) list_tabulate_clo (n, fopr) = list_tabulate(n) where { // val fopr = $UN.cast{cfun(int,a)}(addr@fopr) // implement(a) list_tabulate$fopr(n) = $UN.castvwtp0{a}(fopr(n)) // } (* end of [list_tabulate_clo] *) implement {a}(*tmp*) list_tabulate_cloref (n, fopr) = let // val fopr = $UN.cast{int - a}(fopr) // implement(a) list_tabulate$fopr(n) = $UN.castvwtp0{a}(fopr(n)) // in list_tabulate(n) end // end of [list_tabulate_cloref] (* ****** ****** *) implement {x}(*tmp*) list_foreach_fun (xs, fwork) = let // fun loop(xs: List(x)): void = // case+ xs of | list_nil() => () | list_cons(x, xs) => (fwork(x); loop(xs)) // in $effmask_all (loop(xs)) end // end of [list_foreach_fun] (* ****** ****** *) // implement {x}(*tmp*) list_foreach_clo (xs, fwork) = ( $effmask_all (list_foreach_cloref(xs, $UN.cast(addr@fwork))) ) (* list_foreach_clo *) implement {x}(*tmp*) list_foreach_vclo (pf | xs, fwork) = ( $effmask_all (list_foreach_cloref(xs, $UN.cast(addr@fwork))) ) (* list_foreach_vclo *) // (* ****** ****** *) implement {x}(*tmp*) list_foreach_cloptr (xs, fwork) = cloptr_free ($UN.castvwtp0{cloptr(void)}(fwork)) where { val () = $effmask_all (list_foreach_cloref(xs, $UN.castvwtp1(fwork))) } (* list_foreach_cloptr *) implement {x}(*tmp*) list_foreach_vcloptr (pf | xs, fwork) = cloptr_free ($UN.castvwtp0{cloptr(void)}(fwork)) where { val () = $effmask_all (list_foreach_cloref(xs, $UN.castvwtp1(fwork))) } (* list_foreach_vcloptr *) (* ****** ****** *) implement {x}(*tmp*) list_foreach_cloref (xs, fwork) = let // fun loop(xs: List(x)): void = // case+ xs of | list_nil() => () | list_cons(x, xs) => (fwork(x); loop(xs)) // in $effmask_all (loop(xs)) end // end of [list_foreach_cloref] (* ****** ****** *) // implement {a}(*tmp*) list_foreach_method(xs) = lam(fwork) => list_foreach_cloref(xs, fwork) // (* ****** ****** *) implement {x}(*tmp*) list_iforeach_cloref {n}(xs, fwork) = let // prval() = lemma_list_param(xs) // fun loop { i,j:nat | i+j == n } .. ( i: int(i), xs: list(x, j) ) : void = // case+ xs of | list_nil() => () | list_cons(x, xs) => (fwork (i, x); loop(i+1, xs)) // in loop(0, xs) end // end of [list_iforeach_cloref] (* ****** ****** *) // implement {a}(*tmp*) list_iforeach_method(xs) = lam(fwork) => list_iforeach_cloref(xs, fwork) // (* ****** ****** *) implement {res}{x} list_foldleft_cloptr ( xs, ini, f0 ) = res where { // val f1 = $UN.castvwtp1(f0) val res = list_foldleft_cloref(xs, ini, f1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [list_foldleft_cloptr] implement {res}{x} list_foldleft_cloref (xs, ini, fopr) = let // implement {res2}{x2} list_foldleft$fopr (res2, x2) = ( $UN.castvwtp0{res2} (fopr($UN.castvwtp0{res}(res2), $UN.cast{x}(x2))) ) // in list_foldleft(xs, ini) end // end of [list_foldleft_cloref] (* ****** ****** *) implement {x}{res} list_foldright_cloptr ( xs, f0, snk ) = res where { // val f1 = $UN.castvwtp1(f0) val res = list_foldright_cloref(xs, f1, snk) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [list_foldright_cloptr] implement {x}{res} list_foldright_cloref (xs, fopr, snk) = let // implement {x2}{res2} list_foldright$fopr (x2, res2) = ( $UN.castvwtp0{res2} (fopr($UN.cast{x}(x2), $UN.castvwtp0{res}(res2))) ) // in list_foldright(xs, snk) end // end of [list_foldright_cloref] (* ****** ****** *) // // HX: prelude/list_vt // (* ****** ****** *) implement {x}{y}(*tmp*) list_vt_map_fun (xs, f0) = let // implement {x2}{y2} list_vt_map$fopr(x2) = let // val f0 = $UN.cast{(&x2)->y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_map$fopr] // in list_vt_map(xs) end // end of [list_vt_map_fun] implement {x}{y}(*tmp*) list_vt_map_clo (xs, f0) = let // val f0 = $UN.cast{(&x) - y}(addr@f0) // implement {x2}{y2} list_vt_map$fopr(x2) = let // val f0 = $UN.cast{(&x2)-y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_map$fopr] // in list_vt_map(xs) end // end of [list_vt_map_clo] implement {x}{y}(*tmp*) list_vt_map_cloptr (xs, f0) = ys where { // val f1 = $UN.castvwtp1(f0) val ys = list_vt_map_cloref(xs, f1) val () = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } (* end of [list_vt_map_cloptr] *) implement {x}{y}(*tmp*) list_vt_map_cloref (xs, f0) = let // implement {x2}{y2} list_vt_map$fopr(x2) = let // val f0 = $UN.cast{(&x2)-y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_map$fopr] // in list_vt_map(xs) end // end of [list_vt_map_cloref] (* ****** ****** *) implement {x}{y}(*tmp*) list_vt_mapfree_fun (xs, f0) = let // implement {x2}{y2} list_vt_mapfree$fopr (x2) = let // val f0 = $UN.cast{(&x2>>_?)->y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_mapfree$fopr] // in list_vt_mapfree(xs) end // end of [list_vt_mapfree_fun] implement {x}{y}(*tmp*) list_vt_mapfree_clo (xs, f0) = let // val f0 = $UN.cast{(&x>>_?) - y}(addr@f0) // implement {x2}{y2} list_vt_mapfree$fopr(x2) = let // val f0 = $UN.cast{(&x2>>_?)-y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_mapfree$fopr] // in list_vt_mapfree(xs) end // end of [list_vt_mapfree_clo] implement {x}{y}(*tmp*) list_vt_mapfree_cloptr (xs, f0) = ys where { // val f1 = $UN.castvwtp1(f0) val ys = list_vt_mapfree_cloref(xs, f1) val () = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } (* end of [list_vt_mapfree_cloptr] *) implement {x}{y}(*tmp*) list_vt_mapfree_cloref (xs, f0) = let // implement {x2}{y2} list_vt_mapfree$fopr(x2) = let // val f0 = $UN.cast{(&x2>>_?)-y}(f0) in $UN.castvwtp0{y2}(f0(x2)) // end // end of [list_vt_mapfree$fopr] // in list_vt_mapfree(xs) end // end of [list_vt_mapfree_cloref] (* ****** ****** *) implement {a}{b} list_vt_mapfree_method (xs, _(*type*)) = ( llam(fopr) => list_vt_mapfree_cloptr(xs, fopr) ) (* list_vt_mapfree_method *) (* ****** ****** *) implement {a}(*tmp*) list_vt_foreach_fun {fe}(xs, f0) = let // prval() = lemma_list_vt_param(xs) // fun loop {n:nat} .. ( xs: !list_vt(a, n), f0: (&a) - void ) : void = case+ xs of | @list_vt_cons (x, xs1) => let val () = f0(x) val () = loop(xs1, f0) in fold@ (xs) end // end of [cons] | list_vt_nil((*void*)) => () // end of [loop] in loop(xs, f0) end // end of [list_vt_foreach_fun] (* ****** ****** *) implement {a}(*tmp*) list_vt_foreach_cloptr ( xs, f0 ) = () where { // val f1 = $UN.castvwtp1(f0) val () = list_vt_foreach_cloref(xs, f1) val () = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [list_vt_foreach_cloptr] implement {a}(*tmp*) list_vt_foreach_cloref (xs, f0) = loop(xs, f0) where { // fun loop{n:nat} .. ( xs: !list_vt(a, n), f0: (&a) - void ) : void = case+ xs of | @list_vt_cons (x, xs1) => fold@(xs) where { val () = f0(x) val () = loop(xs1, f0) } // end of [cons] | list_vt_nil((*void*)) => () // end of [loop] // prval() = lemma_list_vt_param(xs) // } // end of [list_vt_foreach_cloref] (* ****** ****** *) implement {r}{x}//tmp list_vt_foldleft_cloptr ( xs, r0, f0 ) = res where { // val f1 = $UN.castvwtp1(f0) val res = list_vt_foldleft_cloref(xs, r0, f1) val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [list_vt_foldleft_cloptr] implement {r}{x}//tmp list_vt_foldleft_cloref (xs, r0, f0) = let // fun auxlst: $d2ctype ( list_vt_foldleft_cloref ) = lam(xs, r0, f0) => ( case+ xs of | @list_vt_nil () => (fold@(xs); r0) | @list_vt_cons (x0, xs1) => res where { val res = auxlst(xs1, f0(r0, x0), f0) prval ((*folded*)) = fold@(xs) } (* end of [list_vt_cons] *) ) // in auxlst(xs, r0, f0) end // end of [list_vt_foldleft_cloref] (* ****** ****** *) // // HX: prelude/array // (* ****** ****** *) implement {a}(*tmp*) array_foreach_fun {n}{fe} ( A0, asz, fwork ) = let // typedef fwork_t = (!unit_v | &a, !ptr) - void // end of [typedef] // prval pfu = unit_v() // var env: ptr = the_null_ptr val fwork = $UN.cast{fwork_t}(fwork) // val ((*void*)) = array_foreach_funenv(pfu | A0, asz, fwork, env) // prval ((*freed*)) = unit_v_elim(pfu) // in // nothing end // end of [array_foreach_fun] implement {a}(*tmp*) array_foreach_cloref {n}{fe} ( A0, asz, fwork ) = let // viewdef v = unit_v typedef tenv = (&a) - void // fun app .<>. (pf: !v | x: &a, fwork: !tenv): void = fwork(x) // end of [fun] // var env = fwork prval pfu = unit_v() // val ((*void*)) = array_foreach_funenv{v}{tenv}(pfu | A0, asz, app, env) // prval ((*freed*)) = unit_v_elim(pfu) // in // nothing end // end of [array_foreach_cloref] (* ****** ****** *) // // HX: prelude/arrayptr // (* ****** ****** *) implement {a}(*tmp*) arrayptr_tabulate_cloref {n}(asz, f0) = let // implement(a2) array_tabulate$fopr(i) = $UN.castvwtp0{a2} (f0($UN.cast{sizeLt(n)}(i))) // in arrayptr_tabulate(asz) end // end of [arrayptr_tabulate_cloref] (* ****** ****** *) // // HX: prelude/arrayref // (* ****** ****** *) implement {a}(*tmp*) arrayptr_foreach_fun ( A0, asz, f0 ) = ((*void*)) where { // val p0 = ptrcast(A0) prval pf0 = arrayptr_takeout(A0) // val () = array_foreach_fun(!p0, asz, f0) // prval () = arrayptr_addback{a}(pf0 | A0) // } // end of [arrayptr_foreach_fun] (* ****** ****** *) // implement {a}(*tmp*) arrayref_tabulate_cloref {n}(asz, f0) = let // implement(a2) array_tabulate$fopr(i) = $UN.castvwtp0{a2} (f0($UN.cast{sizeLt(n)}(i))) // in arrayref_tabulate(asz) end // end of [arrayptr_tabulate_cloref] // (* ****** ****** *) // implement {a}(*tmp*) arrszref_tabulate_cloref (asz, f0) = ( arrszref_make_arrayref (arrayref_tabulate_cloref(asz, f0), asz) ) // (* ****** ****** *) // implement {x}{y} option_map_fun (opt, fopr) = ( // case+ opt of | None() => None_vt() | Some(x0) => Some_vt(fopr(x0)) // ) // end of [option_map_fun] // implement {x}{y} option_map_clo (opt, fopr) = let // val fopr = $UN.cast{cfun(x,y)}(addr@fopr) // in option_map_cloref(opt, fopr) end // end of [option_map_clo] // implement {x}{y} option_map_cloref (opt, fopr) = ( // case+ opt of | None() => None_vt() | Some(x0) => Some_vt(fopr(x0)) // ) // end of [option_map_cloref] // implement {x}{y} option_map_cloptr (xs, f0) = res where { // val f1 = $UN.castvwtp1(f0) val res = option_map_cloref(xs, f1) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [option_map_cloptr] // (* ****** ****** *) // // HX: prelude/matrixptr // (* ****** ****** *) // implement {a}(*tmp*) matrixptr_tabulate_cloptr (nrow, ncol, f0) = mat where { // val mat = matrixptr_tabulate_cloref (nrow, ncol, $UN.castvwtp1(f0)) // val ((*freed*)) = cloptr_free($UN.castvwtp0{cloptr(void)}(f0)) // } // end of [matrixptr_tabulate_cloptr] // implement {a}(*tmp*) matrixptr_tabulate_cloref {m,n}(nrow, ncol, fopr) = let // implement(a2) matrix_tabulate$fopr(i, j) = $UN.castvwtp0{a2} (fopr($UN.cast{sizeLt(m)}(i), $UN.cast{sizeLt(n)}(j))) // in matrixptr_tabulate(nrow, ncol) end // end of [matrixptr_tabulate_cloref] (* ****** ****** *) // // HX: prelude/matrixref // (* ****** ****** *) // implement {a}(*tmp*) matrixref_tabulate_cloref {m,n}(nrow, ncol, fopr) = let // implement(a2) matrix_tabulate$fopr(i, j) = $UN.castvwtp0{a2} (fopr($UN.cast{sizeLt(m)}(i), $UN.cast{sizeLt(n)}(j))) // in matrixptr_refize (matrixptr_tabulate(nrow, ncol)) end // end of [matrixref_tabulate_cloref] // (* ****** ****** *) implement {a}(*tmp*) mtrxszref_tabulate_cloref ( nrow, ncol, fopr ) = let // val M = matrixref_tabulate_cloref (nrow, ncol, fopr) // in // mtrxszref_make_matrixref(M, nrow, ncol) // end // end of [mtrxszref_tabulate_cloref] (* ****** ****** *) implement {a}(*tmp*) matrixref_foreach_cloref (A, m, n, fwork) = let // implement {a2}{env} matrix_foreach$fwork (x, env) = let val (pf,fpf|p) = $UN.ptr_vtake{a}(addr@x) // end of [val] val ((*void*)) = fwork(!p) prval ((*returned*)) = fpf(pf) in // nothing end // end of [matrix_foreach$work] // in matrixref_foreach(A, m, n) end // end of [matrixref_foreach_cloref] (* ****** ****** *) implement {a}(*tmp*) mtrxszref_foreach_cloref (MSZ, fwork) = let // implement {a2}{env} matrix_foreach$fwork (x, env) = let val (pf,fpf|p) = $UN.ptr_vtake{a}(addr@x) // end of [val] val ((*void*)) = fwork(!p) prval ((*returned*)) = fpf(pf) in // nothing end // end of [matrix_foreach$work] // in mtrxszref_foreach(MSZ) end // end of [mtrxszref_foreach_cloref] (* ****** ****** *) implement {}(*tmp*) string_tabulate_cloref {n}(n, fopr) = let // implement string_tabulate$fopr<>(i) = fopr($UN.cast{sizeLt(n)}(i)) // in string_tabulate<>(n) end // end of [string_tabulate_cloref] (* ****** ****** *) (* end of [atspre.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: June, 2012 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) #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}(*tmp*) list0_tuple_0() = list0_nil() // implement {a}(*tmp*) list0_tuple_1(x0) = g0ofg1($list{a}(x0)) implement {a}(*tmp*) list0_tuple_2(x0, x1) = g0ofg1($list{a}(x0, x1)) implement {a}(*tmp*) list0_tuple_3(x0, x1, x2) = g0ofg1($list{a}(x0, x1, x2)) // implement {a}(*tmp*) list0_tuple_4 (x0, x1, x2, x3) = g0ofg1($list{a}(x0, x1, x2, x3)) implement {a}(*tmp*) list0_tuple_5 (x0, x1, x2, x3, x4) = g0ofg1($list{a}(x0, x1, x2, x3, x4)) implement {a}(*tmp*) list0_tuple_6 (x0, x1, x2, x3, x4, x5) = g0ofg1($list{a}(x0, x1, x2, x3, x4, x5)) // (* ****** ****** *) // implement {a}(*tmp*) list0_make_sing(x) = list0_cons{a}(x, list0_nil) implement {a}(*tmp*) list0_make_pair(x1, x2) = list0_cons{a}(x1, list0_cons{a}(x2, list0_nil)) // (* ****** ****** *) implement {a}(*tmp*) list0_make_elt (n, x) = let // val n = g1ofg0(n) // in // if n >= 0 then let val xs = $effmask_wrt(list_make_elt(n, x)) // end of [val] in list0_of_list_vt{a}(xs) end // end of [then] else let in $raise (IllegalArgExn"list0_make_elt:n") end // end of [else] // end // end of [list0_make_elt] (* ****** ****** *) implement {}(*tmp*) list0_make_intrange_lr (l, r) = let val d = ( if l <= r then 1 else ~1 ) : int // end of [val] in $effmask_exn(list0_make_intrange_lrd(l, r, d)) end // end of [list0_make_intrange_lr] (* ****** ****** *) implement {}(*tmp*) list0_make_intrange_lrd (l, r, d) = let // typedef res = list0 (int) // fun loop1 // d > 0 ( l: int, r: int , d: int, res: &ptr? >> res ) : void = let in // if l < r then let val () = ( res := list0_cons{int}(l, _) ) val+list0_cons (_, res1) = res val () = loop1 (l+d, r, d, res1) prval () = fold@ (res) in // nothing end else (res := list0_nil) // end // end of [loop1] // fun loop2 // d < 0 ( l: int, r: int , d: int, res: &ptr? >> res ) : void = let in // if l > r then let val () = ( res := list0_cons{int}(l, _) ) val+ list0_cons (_, res1) = res val () = loop2 (l+d, r, d, res1) prval () = fold@ (res) in // nothing end else (res := list0_nil) // end // end of [loop2] // in // $effmask_all ( if d > 0 then ( if l < r then let var res: ptr? // uninitialized val () = loop1 (l, r, d, res) in res end else list0_nil () ) else if d < 0 then ( if l > r then let var res: ptr? // uninitialized val () = loop2 (l, r, d, res) in res end else list0_nil () ) else ( $raise IllegalArgExn("list0_make_intrange_lrd:d") ) // end of [if] ) (* end of [$effmask_all] *) // end // end of [list0_make_intrange_lrd] (* ****** ****** *) // implement {a}(*tmp*) list0_make_arrpsz (psz) = list0_of_list_vt{a}(list_make_arrpsz(psz)) // end of [list0_make_arrpsz] // (* ****** ****** *) // implement {a}(*tmp*) print_list0 (xs) = fprint_list0 (stdout_ref, xs) implement {a}(*tmp*) prerr_list0 (xs) = fprint_list0 (stderr_ref, xs) // implement {a}(*tmp*) fprint_list0 (out, xs) = fprint_list (out, g1ofg0(xs)) // implement {a}(*tmp*) fprint_list0_sep (out, xs, sep) = ( fprint_list_sep (out, g1ofg0(xs), sep) ) (* end of [fprint_list0_sep] *) // implement {a}(*tmp*) fprint_listlist0_sep (out, xss, sep1, sep2) = ( fprint_listlist_sep (out, $UN.cast{List(List(a))}(xss), sep1, sep2) ) (* end of [fprint_listlist0_sep] *) // (* ****** ****** *) // (* // // HX: these have been declared as macros: // implement {a}(*tmp*) list0_sing (x) = list0_cons{a}(x, list0_nil) implement {a}(*tmp*) list0_pair (x1, x2) = list0_cons{a}(x1, list0_cons{a}(x2, list0_nil)) // *) // (* ****** ****** *) implement {a}(*tmp*) list0_is_nil(xs) = ( // case+ xs of | list0_cons _ => false | list0_nil() => true // ) (* end of [list0_is_nil] *) implement {a}(*tmp*) list0_is_cons(xs) = ( // case+ xs of | list0_cons _ => true | list0_nil() => false // ) (* end of [list0_is_cons] *) (* ****** ****** *) // implement {a}(*tmp*) list0_is_empty(xs) = list0_is_nil (xs) // implement {a}(*tmp*) list0_isnot_empty(xs) = list0_is_cons (xs) // (* ****** ****** *) implement {a}(*tmp*) list0_head_exn (xs) = let in // case+ xs of | list0_cons (x, _) => (x) // list0_cons | list0_nil _ => $raise ListSubscriptExn() // list0_nil end // end of [list0_head_exn] implement {a}(*tmp*) list0_head_opt (xs) = let in // case+ xs of | list0_nil() => None_vt() | list0_cons(x, _) => Some_vt{a}(x) // end // end of [list0_head_opt] (* ****** ****** *) implement {a}(*tmp*) list0_tail_exn (xs) = let in // case+ xs of | list0_cons (_, xs) => (xs) // list0_cons | list0_nil _ => $raise ListSubscriptExn() // list0_nil // end // end of [list0_tail_exn] implement {a}(*tmp*) list0_tail_opt (xs) = let in // case+ xs of | list0_nil() => None_vt() | list0_cons(_, xs) => Some_vt{list0(a)}(xs) // end // end of [list0_tail_opt] (* ****** ****** *) implement {a}(*tmp*) list0_last_exn (xs) = let // val xs = g1ofg0_list(xs) // in // case+ xs of | list_cons _ => list_last(xs) | list_nil () => $raise ListSubscriptExn() // end // end of [list0_last_exn] implement {a}(*tmp*) list0_last_opt (xs) = let // val xs = g1ofg0_list(xs) // in // case+ xs of | list_nil() => None_vt() | list_cons _ => Some_vt{a}(list_last(xs)) // end // end of [list0_last_opt] (* ****** ****** *) implement {a}(*tmp*) list0_init_exn (xs) = let // fun aux {n:nat} .. ( x0: a, xs: list(a, n) ) :<> list(a, n) = ( case+ xs of | list_nil() => list_nil() | list_cons(x, xs) => list_cons(x0, aux(x, xs)) ) // in case+ xs of | list0_cons (x, xs) => ( g0ofg1(aux(x, g1ofg0(xs))) ) (* end of [list0_cons] *) | list0_nil() => $raise ListSubscriptExn() end // end of [list0_init_exn] (* ****** ****** *) implement {a}(*tmp*) list0_init_opt (xs) = let // fun aux {n:nat} .. ( x0: a, xs: list(a, n) ) :<> list(a, n) = ( case+ xs of | list_nil() => list_nil() | list_cons(x, xs) => list_cons(x0, aux(x, xs)) ) // in // case+ xs of | list0_nil() => None_vt(*void*) | list0_cons(x, xs) => Some_vt(g0ofg1(aux(x, g1ofg0(xs)))) // end // end of [list0_init_opt] (* ****** ****** *) // implement {a}(*tmp*) list0_nth_exn (xs, i0) = let // fun loop {i:nat} .. ( xs: list0(a), i: int i ) : (a) = ( // case+ xs of | list0_cons (x, xs) => ( if i > 0 then loop(xs, i-1) else x ) // end of [list0_cons] | list0_nil() => ( $raise ListSubscriptExn(*void*) ) (* end of [list0_nil] *) // ) (* end of [loop] *) // val i0 = g1ofg0_int(i0) // in // if i0 >= 0 then loop(xs, i0) else $raise ListSubscriptExn(*void*) // end of [if] // end // end of [list0_nth_exn] // implement {a}(*tmp*) list0_nth_opt ( xs, i0 ) = $effmask_exn ( try Some_vt{a} ( list0_nth_exn(xs, i0) ) with ~ListSubscriptExn() => None_vt(*void*) ) (* $effmask_exn *) // (* ****** ****** *) // implement {a}(*tmp*) list0_get_at_exn (xs, i0) = list0_nth_exn(xs, i0) implement {a}(*tmp*) list0_get_at_opt (xs, i0) = list0_nth_opt(xs, i0) // (* ****** ****** *) // implement {a}(*tmp*) list0_fset_at_exn (xs, i0, x0) = let // fun fset {i:nat} .. ( xs: list0(a), i: int i ) : list0(a) = ( // case+ xs of | list0_cons (x, xs) => ( if i > 0 then cons0(x, fset(xs, i-1)) else cons0(x0, xs) // end of [if] ) // end of [list0_cons] | list0_nil() => $raise ListSubscriptExn() // ) (* end of [fset] *) // val i0 = g1ofg0(i0) // in // if i0 >= 0 then fset(xs, i0) else $raise ListSubscriptExn() // end // end of [list0_fset_at_exn] // (* ****** ****** *) implement {a}(*tmp*) list0_fset_at_opt ( xs, i0, x0 ) = $effmask_exn ( try Some_vt{list0(a)} ( list0_fset_at_exn(xs, i0, x0) ) with ~ListSubscriptExn((*void*)) => None_vt() ) (* $effmask_exn *) (* ****** ****** *) implement {a}(*tmp*) list0_fexch_at_exn (xs, i0, x0) = let // val p0 = addr@(x0) // fun fexch {i:nat} .. ( xs: list0(a), i: int(i), visited: List0_vt(a) ) : 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(p0) val () = $UN.ptr0_set(p0, x1) val x2_xs = g1ofg0(list0_cons(x2, xs)) in g0ofg1(list_reverse_append1_vt(visited, x2_xs)) end // end of [else] ) | list0_nil() => let val () = list_vt_free(visited) in $raise ListSubscriptExn() end // end of [list0_nil] ) // val i0 = g1ofg0(i0) // in if i0 >= 0 then fexch(xs, i0, list_vt_nil()) else $raise ListSubscriptExn() // end of [if] end // end of [list0_fexch_at_exn] (* ****** ****** *) implement {a}(*tmp*) 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(xs, i0, !p0) prval ((*returned*)) = fpf(pf) in res end // end of [let] ) with ~ListSubscriptExn((*void*)) => None_vt() ) (* $effmask_exn *) // end // end of [list0_fexch_at_opt] (* ****** ****** *) implement {a}(*tmp*) list0_insert_at_exn (xs, i, x0) = let // fun aux {i:nat} .. ( xs: list0 a, i: int i, x0: a ) : list0 a = let in // if i > 0 then ( // case+ xs of | list0_cons (x, xs) => ( list0_cons{a}(x, aux (xs, i-1, x0)) ) | list0_nil() => $raise ListSubscriptExn() // ) else ( list0_cons{a}(x0, xs) ) (* end of [if] *) // end // end of [aux] // val i = g1ofg0_int(i) // in // if i >= 0 then aux (xs, i, x0) else $raise IllegalArgExn("list0_insert_at_exn:i") // end // end of [list0_insert_at_exn] (* ****** ****** *) local fun{ a:t0p } auxlst {i:nat} .. ( xs: list0 (a), i: int i, x0: &a? >> a ) : list0 a = let // extern praxi __assert : (&a? >> a) - void // in // case+ xs of | list0_cons (x, xs) => let in if i > 0 then list0_cons{a}(x, auxlst (xs, i-1, x0)) else let val () = x0 := x in xs end (* end of [if] *) end // end of [list0_cons] | list0_nil () => let prval () = __assert (x0) in $raise ListSubscriptExn() end // end of [list0_nil] // end // end of [auxlst] in (* in of [local] *) implement {a}(*tmp*) list0_remove_at_exn (xs, i) = let // var x0: a? val i = g1ofg0_int (i) // in $effmask_wrt ( if i >= 0 then auxlst (xs, i, x0) else ( $raise IllegalArgExn("list0_remove_at_exn:i") ) (* end of [else] *) ) end // end of [list0_remove_at_exn] (* ****** ****** *) implement {a}(*tmp*) list0_takeout_at_exn (xs, i, x0) = let // val i = g1ofg0_int (i) // extern praxi __assert : (&a? >> a) - void // in // if i >= 0 then auxlst (xs, i, x0) else let prval () = __assert (x0) in $raise IllegalArgExn("list0_takeout_at_exn:i") end // end of [if] // end // end of [list0_takeout_at_exn] end // end of [local] (* ****** ****** *) // implement {a}(*tmp*) list0_length (xs) = list_length(g1ofg0(xs)) // (* ****** ****** *) implement {a}(*tmp*) list0_append (xs, ys) = let val xs = g1ofg0(xs) and ys = g1ofg0(ys) in // list0_of_list(list_append(xs, ys)) // end // end of [list0_append] (* ****** ****** *) implement {a}(*tmp*) list0_extend (xs, x) = let // val xs = g1ofg0(xs) // in // $effmask_wrt ( list0_of_list_vt(list_extend(xs, x)) ) (* $effmask_wrt *) // end // end of [list0_extend] (* ****** ****** *) // implement {a}(*tmp*) mul_int_list0 (m, xs) = $effmask_wrt ( list0_of_list_vt (mul_int_list(m, g1ofg0(xs))) ) (* end of [mul_int_list0] *) // (* ****** ****** *) implement {a}(*tmp*) list0_reverse(xs) = list0_reverse_append(xs, list0_nil) // end of [list0_reverse] implement {a}(*tmp*) list0_reverse_append (xs, ys) = let val xs = g1ofg0(xs) and ys = g1ofg0(ys) in list0_of_list(list_reverse_append(xs, ys)) end // end of [list0_reverse_append] (* ****** ****** *) implement {a}(*tmp*) list0_concat (xss) = let // typedef xss = List(List(a)) // in // $effmask_wrt ( list0_of_list_vt{a} (list_concat($UN.cast{xss}(xss))) ) (* $effmask_wrt *) end // end of [list0_concat] (* ****** ****** *) implement {a}(*tmp*) list0_take_exn (xs, i) = let // val i = g1ofg0_int(i) val xs = g1ofg0_list(xs) // in // if (i >= 0) then let // val res = $effmask_wrt(list_take_exn(xs, i)) // in list0_of_list_vt(res) end else ( $raise(IllegalArgExn"list0_take_exn:i") ) (* end of [if] *) end // end of [list0_take_exn] (* ****** ****** *) implement {a}(*tmp*) list0_drop_exn (xs, i) = let // val i = g1ofg0_int (i) val xs = g1ofg0_list (xs) // in // if (i >= 0) then g0ofg1(list_drop_exn(xs, i)) else $raise(IllegalArgExn"list0_drop_exn:i") // end // end of [list0_drop_exn] (* ****** ****** *) // implement {a}{b}//tmp list0_cata (xs, fnil, fcons) = ( case+ xs of | list0_nil() => fnil() | list0_cons(x, xs) => fcons(x, xs) ) // (* ****** ****** *) // implement {a}(*tmp*) list0_app (xs, fopr) = list0_foreach(xs, fopr) // (* ****** ****** *) // implement {a}(*tmp*) list0_foreach ( xs, fwork ) = loop(xs) where { // fun loop(xs: list0(a)): void = ( case+ xs of | list0_nil() => () | list0_cons (x, xs) => (fwork(x); loop(xs)) // end of [list0_cons] ) // } (* end of [list0_foreach] *) // implement {a}(*tmp*) list0_foreach_method(xs) = lam(fwork) => list0_foreach(xs, fwork) // (* ****** ****** *) // implement {a}(*tmp*) list0_rforeach ( xs, fwork ) = aux0(xs) where { // fun aux0(xs: list0(a)): void = ( case+ xs of | list0_nil() => () | list0_cons(x, xs) => (aux0(xs); fwork(x)) ) // } (* end of [list0_rforeach] *) // implement {a}(*tmp*) list0_rforeach_method(xs) = lam(fwork) => list0_rforeach(xs, fwork) // (* ****** ****** *) implement {a}(*tmp*) list0_iforeach (xs, fwork) = let // fun loop ( i0: intGte(0), xs: list0(a) ) : intGte(0) = ( case+ xs of | list0_nil() => i0 | list0_cons(x, xs) => (fwork(i0, x); loop (i0+1, xs)) // end of [list0_cons] ) (* end of [loop] *) // in loop (0, xs) end // end of [list0_iforeach] // implement {a}(*tmp*) list0_iforeach_method(xs) = lam(fwork) => list0_iforeach(xs, fwork) // (* ****** ****** *) implement {a1,a2} list0_foreach2 (xs1, xs2, fwork) = let var sgn: int // uninitialized in list0_foreach2_eq (xs1, xs2, fwork, sgn) end // end of [list0_foreach2] implement {a1,a2} list0_foreach2_eq ( xs1, xs2, fwork, sgn ) = loop(xs1, xs2, sgn) where { // fun loop ( xs1: list0(a1) , xs2: list0(a2) , sgn: &int? >> int ) : void = ( case+ xs1 of | list0_nil() => ( case+ xs2 of | list0_nil() => (sgn := 0) | list0_cons _ => (sgn := ~1) ) | list0_cons(x1, xs1) => ( case+ xs2 of | list0_nil () => (sgn := 1) | list0_cons(x2, xs2) => (fwork(x1, x2); loop(xs1, xs2, sgn)) ) ) // } (* end of [list0_foreach2_eq] *) (* ****** ****** *) implement {res}{a} list0_foldleft (xs, ini, fopr) = let // fun loop ( xs: list0(a), res: res ) : res = ( case+ xs of | list0_nil () => res | list0_cons(x, xs) => loop(xs, fopr(res, x)) ) in loop(xs, ini) end // end of [list0_foldleft] // implement {res}{a} list0_foldleft_method(xs, _) = lam(ini, fopr) =>list0_foldleft(xs, ini, fopr) // (* ****** ****** *) implement {res}{a} list0_ifoldleft (xs, ini, fopr) = let // fun loop ( i: int, xs: list0 (a), res: res ) : res = ( case+ xs of | list0_nil () => res | list0_cons(x, xs) => loop(i+1, xs, fopr(res, i, x)) ) (* end of [loop] *) in loop (0, xs, ini) end // end of [list0_ifoldleft] // implement {res}{a} list0_ifoldleft_method(xs, _) = ( lam(ini, fopr) => list0_ifoldleft(xs, ini, fopr) // end of [lam ) // (* ****** ****** *) 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)) ) (* end of [list0_cons] *) ) ) (* end of [loop] *) // in loop(xs1, xs2, ini) end (* end of [list0_foldleft2] *) (* ****** ****** *) implement {a}{res} list0_foldright ( xs, fopr, snk ) = loop(xs) where { // fun loop(xs: list0(a)): res = case+ xs of | list0_nil() => snk | list0_cons (x, xs) => fopr(x, loop(xs)) // } (* end of [list0_foldright] *) // implement {a}{res} list0_foldright_method(xs, _) = lam(f, snk) => list0_foldright(xs, f, snk) // (* ****** ****** *) implement {a}(*tmp*) list0_exists ( xs, pred ) = loop(xs) where { // fun loop(xs: list0(a)): bool = ( case+ xs of | list0_nil() => false | list0_cons (x, xs) => if pred(x) then true else loop(xs) // list0_cons ) (* end of [loop] *) // } (* end of [list0_exists] *) // implement {a}(*tmp*) list0_exists_method(xs) = lam(p) => list0_exists(xs, p) // (* ****** ****** *) implement {a}(*tmp*) list0_iexists ( xs, pred ) = loop(0, xs) where { // fun loop(i: intGte(0), xs: list0(a)): bool = ( case+ xs of | list0_nil() => false | list0_cons(x, xs) => if pred(i, x) then true else loop(i+1, xs) // list0_cons ) (* end of [loop] *) // } (* end of [list0_iexists] *) // implement {a}(*tmp*) list0_iexists_method(xs) = lam(p) => list0_iexists (xs, p) // (* ****** ****** *) implement {a1,a2} list0_exists2 (xs1, xs2, p0) = let // var sgn: int // uninitized // in list0_exists2_eq(xs1, xs2, p0, sgn) end // end of [list0_exists2] 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) // end of [if] ) (* end of [list0_cons] *) ) ) } (* end of [list0_exists2_eq] *) (* ****** ****** *) implement {a}(*tmp*) list0_forall ( xs, pred ) = loop(xs) where { // fun loop(xs: list0(a)): bool = ( case+ xs of | list0_nil() => true | list0_cons(x, xs) => if pred(x) then loop(xs) else false // list0_cons ) (* end of [loop] *) // } (* end of [list0_forall] *) // implement {a}(*tmp*) list0_forall_method(xs) = lam(p) => list0_forall (xs, p) // (* ****** ****** *) implement {a}(*tmp*) list0_iforall ( xs, pred ) = loop(0, xs) where { // fun loop(i: intGte(0), xs: list0(a)): bool = ( case+ xs of | list0_nil() => true | list0_cons(x, xs) => if pred(i, x) then loop(i+1, xs) else false // list0_cons ) (* end of [loop] *) // } (* end of [list0_iforall] *) // implement {a}(*tmp*) list0_iforall_method(xs) = lam(p) => list0_iforall (xs, p) // (* ****** ****** *) implement {a1,a2} list0_forall2 (xs1, xs2, p0) = let // var sgn: int // uninitized // in list0_forall2_eq(xs1, xs2, p0, sgn) end // end of [list0_forall2] implement {a1,a2} list0_forall2_eq ( xs1, xs2, pred, sgn ) = loop(xs1, xs2, sgn) where { // fun loop ( xs1: list0(a1) , xs2: list0(a2) , sgn: &int? >> _ ) : bool = ( case+ xs1 of | list0_nil() => ( case+ xs2 of | list0_nil() => (sgn := 0; true) | list0_cons _ => (sgn := ~1; true) ) | list0_cons (x1, xs1) => ( case+ xs2 of | list0_nil() => (sgn := 1; true) | list0_cons (x2, xs2) => ( if pred(x1, x2) then loop(xs1, xs2, sgn) else (sgn := 0; false) // end of [if] ) (* end of [list0_cons] *) ) ) } (* end of [list0_forall2_eq] *) (* ****** ****** *) implement {a}(*tmp*) list0_equal ( xs1, xs2, eqfn ) = loop(xs1, xs2) where { // fun loop ( xs1: list0(a), xs2: list0(a) ) : bool = ( case+ xs1 of | list0_nil() => ( case+ xs2 of | list0_nil() => true | list0_cons _ => false ) | list0_cons (x1, xs1) => ( case+ xs2 of | list0_nil () => false // list0_nil | list0_cons (x2, xs2) => if eqfn(x1, x2) then loop(xs1, xs2) else false // end of [if] // end of [list0_cons] ) ) (* end of [loop] *) // } (* end of [list0_equal] *) (* ****** ****** *) implement {a}(*tmp*) 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 // end of [list0_cons] ) ) (* end of [loop] *) // } (* end of [list0_compare] *) (* ****** ****** *) implement {a}(*tmp*) list0_find_exn ( xs, pred ) = loop(xs) where { // fun loop(xs: list0(a)): a = ( case+ xs of | list0_nil() => $raise NotFoundExn() // list0_nil | list0_cons(x, xs) => if pred(x) then x else loop(xs) // list0_cons ) // } (* end of [list0_find_exn] *) (* ****** ****** *) implement {a}(*tmp*) list0_find_opt ( xs, pred ) = loop(xs) where { // fun loop ( xs: list0(a) ) : Option_vt(a) = // case+ xs of | list0_nil() => None_vt(*void*) // list0_nil | list0_cons(x, xs) => ( if pred(x) then Some_vt{a}(x) else loop(xs) // end of [if] ) (* end of [list_cons] *) // } (* end of [list0_find_opt] *) (* ****** ****** *) // implement {a}(*tmp*) list0_find_exn_method (xs) = lam(pred) => list0_find_exn(xs, pred) // implement {a}(*tmp*) list0_find_opt_method (xs) = lam(pred) => list0_find_opt(xs, pred) // (* ****** ****** *) implement {a}(*tmp*) list0_find_index ( xs, pred ) = loop(xs, 0) where { // fun loop ( xs: list0(a), i: intGte(0) ) : intGte(~1) = // case+ xs of | list0_nil() => (~1) | list0_cons(x, xs) => ( if pred(x) then (i) else loop(xs, i+1) // end of [if] ) (* end of [list0_cons] *) // } (* end of [list0_find_index] *) (* ****** ****** *) implement {a}(*tmp*) 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) ) // } (* end of [list0_find_suffix] *) (* ****** ****** *) implement {a}(*tmp*) 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 ) // } // end of [list0_skip_while] implement {a}(*tmp*) 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) ) // } // end of [list0_skip_until] (* ****** ****** *) implement {a}(*tmp*) 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 // end of [if] ) // in // list0_vt2t (g0ofg1(list_vt_reverse(auxmain(xs, list_vt_nil())))) // end // end of [list0_take_while] implement {a}(*tmp*) 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)) // end of [if] ) // in // list0_vt2t (g0ofg1(list_vt_reverse(auxmain(xs, list_vt_nil())))) // end // end of [list0_take_until] (* ****** ****** *) implement {a,b}(*tmp*) list0_assoc_exn ( xys, x0, eq ) = loop(xys, x0, eq) where { // fun loop: $d2ctype ( list0_assoc_exn ) = lam(xys, x0, eq) => // case+ xys of | list0_nil() => $raise NotFoundExn() | list0_cons(xy, xys) => if eq (x0, xy.0) then xy.1 else loop(xys, x0, eq) // end of [list0_cons] // } (* end of [list0_assoc_exn] *) (* ****** ****** *) implement {a,b}(*tmp*) list0_assoc_opt ( xys, x0, eq ) = loop(xys, x0, eq) where { fun loop: $d2ctype( list0_assoc_opt ) = lam(xys, x0, eq) => // case+ xys of | list0_nil() => None_vt(*void*) // list0_nil | list0_cons(xy, xys) => ( if eq (x0, xy.0) then Some_vt{b}(xy.1) else loop(xys, x0, eq) // end of [if] ) (* end of [list_cons] *) // } (* end of [list0_assoc_opt] *) (* ****** ****** *) // implement {a}(*tmp*) list0_filter (xs, pred) = let // implement{a2} list_filter$pred (x) = pred($UN.cast{a}(x)) // val ys = list_filter(g1ofg0(xs)) // in list0_of_list_vt (ys) end // end of [list0_filter] // implement {a}(*tmp*) list0_filter_method (xs) = lam(pred) => list0_filter(xs, pred) // (* ****** ****** *) // (* implement {a}{b} list0_map (xs, fopr) = let viewdef v = unit_v viewtypedef fun_vt = cfun (a, b) fun app .<>. (pfu: !unit_v | x: a, fopr: !fun_vt): b = fopr (x) // end of [fun] prval pfu = unit_v () var fopr = fopr val ys = list_map_funenv {v}{vt} (pfu | g1ofg0(xs), app, fopr) prval () = topize(fopr) prval unit_v((*void*)) = pfu in list0_of_list_vt (ys) end // end of [list0_map] *) // implement {a}{b} list0_map(xs, fopr) = let // implement {a2}{b2} list_map$fopr(x) = $UN.castvwtp0{b2}(fopr($UN.cast{a}(x))) // val ys = list_map(g1ofg0_list(xs)) // in list0_of_list_vt{b}(ys) end // end of [list0_map] (* ****** ****** *) implement {a}{b} list0_mapopt (xs, fopr) = res where { // fun loop ( xs: list0 (a) , res: &ptr? >> List0_vt(b) ) : void = let in // case+ xs of | list0_nil () => ( res := list_vt_nil () ) (* end of [list0_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 ((*folded*)) = fold@(res) in // nothing end // end of [Some0] | ~None_vt((*void*)) => loop(xs, res) ) (* end of [list0_cons] *) // end // end of [loop] // var res: ptr val () = loop (xs, res) val res = list0_of_list_vt (res) // } // end of [list0_mapopt] (* ****** ****** *) // implement {a}{b} list0_map_method (xs, _) = lam(fopr) => list0_map(xs, fopr) implement {a}{b} list0_mapopt_method (xs, _) = lam(fopr) => list0_mapopt(xs, fopr) // (* ****** ****** *) implement {a}(*tmp*) list0_mapcons (x0, xss) = let // implement list_map$fopr (xs) = list0_cons(x0, xs) // val xss = g1ofg0 (xss) val res = list_map (xss) // in list0_of_list_vt (res) end // end of [list0_mapcons] (* ****** ****** *) // implement {a}{b} list0_mapjoin ( xs , fopr ) = list0_concat (list0_map(xs, fopr)) // implement {a}{b} list0_mapjoin_method (xs) = lam(fopr) => list0_mapjoin(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 // end of [list_imap$fopr] // val ys = list_imap(g1ofg0_list(xs)) // in list0_of_list_vt{b}(ys) end // end of [list0_imap] (* ****** ****** *) 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 () ) (* end of [list0_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 ((*folded*)) = fold@(res) in // nothing end // end of [Some0] | ~None_vt((*void*)) => loop(i0+1, xs, res) ) (* end of [list0_cons] *) // end // end of [loop] // var res: ptr val () = loop(0, xs, res) val res = list0_of_list_vt(res) // } // end of [list0_imapopt] (* ****** ****** *) // implement {a}{b} list0_imap_method (xs, _(*TYPE*)) = lam(fopr) => list0_imap(xs, fopr) // implement {a}{b} list0_imapopt_method (xs, _(*TYPE*)) = lam(fopr) => list0_imapopt(xs, fopr) // (* ****** ****** *) // (* implement {a1,a2}{b} list0_map2 (xs1, xs2, fopr) = let viewdef v0 = unit_v viewtypedef fun_vt = cfun2 (a1, a2, b) val xs1 = g1ofg0_list(xs1) val xs2 = g1ofg0_list(xs2) fun app .<>. (pfu: !v0 | x1: a1, x2: a2, f: !fun_vt): b = fopr(x1, x2) // end of [fun] prval pfu = unit_v () var fopr = fopr val ys = list_map2_funenv {v0}{vt} (pfu | xs1, xs2, app, fopr) prval () = topize(fopr) prval unit_v((*void*)) = pfu in list0_of_list_vt (ys) end // end of [list0_map2] *) // implement {a1,a2}{b} list0_map2 (xs1, xs2, fopr) = let // implement {a11,a12}{b2} list_map2$fopr (x1, x2) = $UN.castvwtp0{b2} (fopr($UN.cast{a1}(x1), $UN.cast{a2}(x2))) // in list0_of_list_vt{b}(list_map2(g1ofg0(xs1), g1ofg0(xs2))) end // end of [list0_map2] // (* ****** ****** *) // 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(nptr) val res = $UN.castvwtp0{b2} (fopr(n0, $UN.cast{a1}(x1), $UN.cast{a2}(x2))) in $UN.ptr0_set(nptr, n0+1); res end // end of [list_map2$fopr] // in list0_of_list_vt{b}(list_map2(g1ofg0(xs1), g1ofg0(xs2))) end // end of [list0_imap2] // (* ****** ****** *) implement {a}(*tmp*) list0_tabulate {n}(n, fopr) = let // implement{a2} list_tabulate$fopr (i) = let val i = $UN.cast{natLt(n)}(i) in $UN.castvwtp0{a2}(fopr(i)) end // list_tabulate$fopr // val n = g1ofg0_int(n) // in // if (n >= 0) then list0_of_list_vt(list_tabulate(n)) else $raise IllegalArgExn("list0_tabulate:n") // end of [if] end // end of [list0_tabulate] (* ****** ****** *) implement {a}(*tmp*) list0_tabulate_opt (n, fopr) = res where { // fun loop ( i: Nat , res: &ptr? >> List0_vt(a) ) : void = let in // if (n > i) then ( case+ fopr(i) of | ~None_vt() => loop(i+1, res) // end of [None_vt] | ~Some_vt(x) => let // val () = ( res := list_vt_cons{a}{0}(x, _) ) (* end of [val] *) // val+list_vt_cons(_, res1) = res // val () = loop (i+1, res1) // prval ((*folded*)) = fold@ (res) in // nothing end // end of [Some0] ) else ( res := list_vt_nil((*void*)) ) (* end of [if] *) // end // end of [loop] // var res: ptr val () = loop (0, res) val res = list0_of_list_vt (res) // } // end of [list0_tabulate_opt] (* ****** ****** *) implement {x,y} list0_zip (xs, ys) = let // val xs = g1ofg0(xs) and ys = g1ofg0(ys) val xys = $effmask_wrt(list_zip (xs, ys)) // in list0_of_list_vt{(x,y)}(xys) end // end of [list0_zip] (* ****** ****** *) implement {x,y} list0_cross (xs, ys) = let // val xs = g1ofg0(xs) and ys = g1ofg0(ys) val xys = $effmask_wrt(list_cross (xs, ys)) // in list0_of_list_vt{(x,y)}(xys) end // end of [list0_cross] (* ****** ****** *) implement {x,y}{z} list0_crosswith (xs, ys, fopr) = let // implement {x2,y2}{z2} list_crosswith$fopr(x, y) = $UN.castvwtp0{z2} (fopr($UN.cast{x}(x), $UN.cast{y}(y))) // val xs = g1ofg0(xs) and ys = g1ofg0(ys) val zs = $effmask_wrt(list_crosswith (xs, ys)) // in list0_of_list_vt{z}(zs) end // end of [list0_crosswith] (* ****** ****** *) implement {x}(*tmp*) 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) // end of [list0_cons] ) and loop2 ( x0: x, xs: list0(x), ys: list0(x) ) : void = ( case+ ys of | list0_nil () => loop(xs) | list0_cons (y, ys) => let val () = fwork(x0, y) in loop2(x0, xs, ys) end // end of [list_cons] ) // } (* end of [list0_choose2_foreach] *) // implement {x}(*tmp*) list0_choose2_foreach_method(xs) = lam(fwork) => list0_choose2_foreach(xs, fwork) // (* ****** ****** *) implement {x,y}(*tmp*) 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)) ) // } (* end of [list0_xprod2_foreach] *) // implement {x,y}(*tmp*) list0_xprod2_foreach_method (xs, ys) = ( lam(fwork) => list0_xprod2_foreach(xs, ys, fwork) ) // (* ****** ****** *) implement {x,y}(*tmp*) 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) // end of [list_cons] ) and loop2 ( i0: int, x0: x , xs: list0(x), j: int, ys: list0(y) ) : void = ( case+ ys of | list0_nil() => loop(i0+1, xs) | list0_cons(y, ys) => (fwork(i0, x0, j, y); loop2(i0, x0, xs, j+1, ys)) // end of [list0_cons] ) // } (* end of [list0_xprod2_iforeach] *) // implement {x,y}(*tmp*) list0_xprod2_iforeach_method (xs, ys) = ( lam(fwork) => list0_xprod2_iforeach(xs, ys, fwork) ) (* list0_xprod2_iforeach_method *) // (* ****** ****** *) // implement {a}(*tmp*) streamize_list0_elt (xs) = streamize_list_elt(g1ofg0(xs)) // (* ****** ****** *) // implement {a}(*tmp*) un_streamize_list0_elt (xs) = ( list0_of_list_vt{a}(stream2list_vt(xs)) ) // (* ****** ****** *) implement {a}(*tmp*) streamize_list0_suffix (xs) = let // fun auxmain: $d2ctype ( streamize_list0_suffix ) = 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 (* end of [streamize_list0_suffix] *) (* ****** ****** *) // implement {a}(*tmp*) streamize_list0_choose2 (xs) = streamize_list_choose2(g1ofg0(xs)) // (* ****** ****** *) implement {a}(*tmp*) streamize_list0_nchoose (xs, n) = let // fun auxmain ( xs: list0(a), n: intGte(0) ) : stream_vt(list0(a)) = $ldelay ( // if (n > 0) then ( case+ xs of | list0_nil() => stream_vt_nil() | list0_cons(x0, xs1) => let val res1 = auxmain(xs1, n-1) // end of [val] val res2 = auxmain(xs1, n) in !(stream_vt_append ( stream_vt_map_cloptr(res1, lam(ys) => list0_cons(x0, ys)), res2 ) // stream_vt_append ) end // end of [list0_cons] ) (* end of [then] *) else ( stream_vt_cons(list0_nil, stream_vt_make_nil()) ) (* end of [else] *) // ) : stream_vt_con(list0(a)) // auxmain // in $effmask_all(auxmain(xs, n)) end // end of [streamize_list0_nchoose] (* ****** ****** *) // implement {a,b}(*tmp*) streamize_list0_zip (xs, ys) = streamize_list_zip(g1ofg0(xs), g1ofg0(ys)) // implement {a,b}(*tmp*) streamize_list0_cross (xs, ys) = streamize_list_cross(g1ofg0(xs), g1ofg0(ys)) // (* ****** ****** *) implement {a}(*tmp*) list0_is_ordered (xs, cmp) = let // implement gcompare_val_val(x, y) = cmp(x, y) // in list_is_ordered(g1ofg0_list{a}(xs)) end // end of [list0_is_ordered] (* ****** ****** *) implement {a}(*tmp*) list0_mergesort(xs, cmp) = let // implement list_mergesort$cmp(x, y) = cmp(x, y) // val ys = $effmask_wrt(list_mergesort(g1ofg0(xs))) // in list0_of_list_vt (ys) end // end of [list0_mergesort] (* ****** ****** *) implement {a}(*tmp*) list0_quicksort(xs, cmp) = let // implement list_quicksort$cmp(x, y) = cmp(x, y) // val ys = $effmask_wrt(list_quicksort(g1ofg0(xs))) // in list0_of_list_vt (ys) end // end of [list0_quicksort] (* ****** ****** *) // // HX: some common generic functions // (* ****** ****** *) // implement (a)(*tmp*) fprint_val = fprint_list0 // (* ****** ****** *) implement (a)(*tmp*) gcompare_val_val (xs, ys) = let // fun auxlst ( xs: list0(a), ys: list0(a) ) : int = ( case+ xs of | list0_nil() => ( case+ ys of | list0_nil() => 0 | list0_cons _ => ~1 ) (* list0_nil *) | list0_cons(x, xs) => ( case+ ys of | list0_nil() => 1 | list0_cons(y, ys) => let val sgn = gcompare_val_val(x, y) // end of [val] in if sgn != 0 then sgn else auxlst(xs, ys) end // end of [list0_cons] ) (* list0_cons *) ) (* end of [auxlst] *) // in $effmask_all(auxlst(xs, ys)) end (* end of [gcompare_val_val] *) (* ****** ****** *) (* end of [list0.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2017 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: January, 2018 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) #define ATS_DYNLOADFLAG 0 (* ****** ****** *) #staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) #staload "libats/ML/SATS/basis.sats" #staload "libats/ML/SATS/list0_vt.sats" (* ****** ****** *) implement {a}(*tmp*) list0_vt_free (xs) = ( list_vt_free(xs) ) where { val xs = $UN.castvwtp0(xs) } (* ****** ****** *) implement {a}(*tmp*) list0_vt_append (xs, ys) = let // val xs = $UN.castvwtp0(xs) val ys = $UN.castvwtp0(ys) // in $UN.castvwtp0 (list_vt_append(xs, ys)) end // end of [list0_vt_append] (* ****** ****** *) implement {a}(*tmp*) list0_vt_reverse (xs) = let // val xs = $UN.castvwtp0(xs) // in $UN.castvwtp0(list_vt_reverse(xs)) end // end of [list0_vt_append] (* ****** ****** *) (* end of [list0_vt.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: July, 2012 *) (* ****** ****** *) // staload UN = "prelude/SATS/unsafe.sats" // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" staload "libats/ML/SATS/list0.sats" staload "libats/ML/SATS/array0.sats" (* ****** ****** *) // extern fun memcpy ( d:ptr, s:ptr, n:size_t ) : ptr = "mac#atslib_ML_array0_memcpy" // end of [memcpy] // (* ****** ****** *) // implement {a}(*tmp*) array0_tuple_0 () = array0($arrpsz{a}()) // implement {a}(*tmp*) array0_tuple_1 (x0) = array0($arrpsz{a}(x0)) implement {a}(*tmp*) array0_tuple_2 (x0, x1) = array0($arrpsz{a}(x0, x1)) implement {a}(*tmp*) array0_tuple_3 (x0, x1, x2) = array0($arrpsz{a}(x0, x1, x2)) // implement {a}(*tmp*) array0_tuple_4 (x0, x1, x2, x3) = array0($arrpsz{a}(x0, x1, x2, x3)) implement {a}(*tmp*) array0_tuple_5 (x0, x1, x2, x3, x4) = array0($arrpsz{a}(x0, x1, x2, x3, x4)) implement {a}(*tmp*) array0_tuple_6 (x0, x1, x2, x3, x4, x5) = array0($arrpsz{a}(x0, x1, x2, x3, x4, x5)) // (* ****** ****** *) // implement {}(*tmp*) array0_of_arrszref {a}(A) = $UN.cast{array0(a)}(A) // implement {}(*tmp*) arrszref_of_array0 {a}(A) = $UN.cast{arrszref(a)}(A) // (* ****** ****** *) implement {}(*tmp*) array0_get_ref (A0) = let // val ASZ = arrszref_of_array0(A0) in arrszref_get_ref(ASZ) // end of [val] end // end of [array0_get_ref] (* ****** ****** *) implement {}(*tmp*) array0_get_size (A0) = let // val ASZ = arrszref_of_array0(A0) in arrszref_get_size(ASZ) // end of [val] end // end of [array0_get_size] (* ****** ****** *) // implement {}(*tmp*) array0_get_length (A0) = sz2i(g1ofg0_uint(array0_get_size<>(A0))) // (* ****** ****** *) implement {}(*tmp*) array0_get_refsize (A0) = let // var asz: size_t val ASZ = arrszref_of_array0(A0) val A = $effmask_wrt(arrszref_get_refsize(ASZ, asz)) // in @(A, asz) end // end of [array0_get_refsize] (* ****** ****** *) // implement {}(*tmp*) array0_make_arrpsz (psz) = let // val ASZ = arrszref_make_arrpsz(psz) in array0_of_arrszref(ASZ) // end of [val] end // end of [array0_make_arrpsz] // implement {}(*tmp*) array0_make_arrayref (A, n) = let val ASZ = arrszref_make_arrayref(A, n) in array0_of_arrszref(ASZ) // end of [val] end // end of [array0_make_arrpsz] // (* ****** ****** *) // implement {a}(*tmp*) array0_make_elt_int (asz, x0) = let // val asz = i2sz(max(g1ofg0(asz), 0)) // in // array0_of_arrszref(arrszref_make_elt(asz, x0)) // end // end of [array0_make_elt_int] // implement {a}(*tmp*) array0_make_elt_size (asz, x0) = ( array0_of_arrszref(arrszref_make_elt(asz, x0)) ) (* end of [array0_make_elt_size] *) // (* ****** ****** *) implement {a}(*tmp*) array0_make_list (xs) = let val xs = g1ofg0(xs) in array0_of_arrszref{a}(arrszref_make_list(xs)) end // end of [array0_make_list] (* ****** ****** *) implement {a}(*tmp*) array0_make_rlist (xs) = let val xs = g1ofg0(xs) in array0_of_arrszref{a}(arrszref_make_rlist(xs)) end // end of [array0_make_rlist] (* ****** ****** *) implement {a}(*tmp*) array0_make_subarray (A0, st, ln) = let // val st = g1ofg0(st) val ln = g1ofg0(ln) // val [n:int] (A, asz) = array0_get_refsize(A0) // val [st:int] st = (if st <= asz then st else asz): sizeLte(n) val [ln:int] ln = (if st + ln <= asz then ln else asz - st): sizeLte(n-st) // val A2 = arrayptr_make_uninitized(ln) val p2 = memcpy (ptrcast(A2), ptr_add(ptrcast(A), st), ln*sizeof) val A2 = $UN.castvwtp0{arrayref(a,ln)}(A2) // in array0_make_arrayref{a}(A2, ln) end // end of [array0_make_subarray] (* ****** ****** *) // implement {a}(*tmp*) print_array0(A) = fprint_array0(stdout_ref, A) // implement {a}(*tmp*) prerr_array0(A) = fprint_array0(stderr_ref, A) // implement {a}(*tmp*) fprint_array0(out, A) = fprint_arrszref(out, arrszref_of_array0(A)) // implement {a}(*tmp*) fprint_array0_sep (out, A, sep) = fprint_arrszref_sep(out, arrszref_of_array0(A), sep) // (* ****** ****** *) implement {a}{tk} array0_get_at_gint (A0, i) = let in // if i >= 0 then array0_get_at_size(A0, g0i2u(i)) else $raise ArraySubscriptExn() // neg index // end // end of [array0_get_at_gint] implement {a}{tk} array0_get_at_guint (A0, i) = let in array0_get_at_size(A0, g0u2u(i)) end // end of [array0_get_at_guint] implement {a}(*tmp*) array0_get_at_size (A0, i) = ( arrszref_get_at_size(arrszref_of_array0(A0), i) ) // end of [array0_get_at_size] (* ****** ****** *) implement {a}{tk} array0_set_at_gint (A0, i, x) = ( // if i >= 0 then array0_set_at_size(A0, g0i2u(i), x) else $raise ArraySubscriptExn() // neg index // ) // end of [array0_set_at_gint] implement {a}{tk} array0_set_at_guint (A0, i, x) = ( array0_set_at_size(A0, g0u2u(i), x) ) // end of [array0_set_at_guint] implement {a}(*tmp*) array0_set_at_size (A0, i, x) = ( arrszref_set_at_size(arrszref_of_array0(A0), i, x) ) // end of [array0_set_at_size] (* ****** ****** *) implement {a}{tk} array0_exch_at_gint (A0, i, x) = let in // if i >= 0 then array0_exch_at_size(A0, g0i2u(i), x) else $raise ArraySubscriptExn() // neg index // end // end of [array0_exch_at_gint] implement {a}{tk} array0_exch_at_guint (A0, i, x) = ( array0_exch_at_size(A0, g0u2u(i), x) ) // end of [array0_exch_at_guint] implement {a}(*tmp*) array0_exch_at_size (A0, i, x) = ( arrszref_exch_at_size(arrszref_of_array0(A0), i, x) ) // end of [array0_exch_at_size] (* ****** ****** *) implement {a}(*tmp*) array0_interchange (A0, i, j) = let val ASZ = arrszref_of_array0(A0) in arrszref_interchange(ASZ, i, j) // end of [val] end // end of [array0_interchange] (* ****** ****** *) implement {a}(*tmp*) array0_subcirculate (A0, i, j) = let val ASZ = arrszref_of_array0(A0) in arrszref_subcirculate(ASZ, i, j) // end of [val] end // end of [array0_subcirculate] (* ****** ****** *) implement {a}(*tmp*) array0_copy (A0) = let // val ASZ = arrszref_of_array0(A0) // var asz: size_t // val A = arrszref_get_refsize(ASZ, asz) // val (vbox pf | p) = arrayref_get_viewptr(A) val (pfarr, pfgc | q) = array_ptr_alloc(asz) // val () = array_copy(!q, !p, asz) // val A2 = arrayptr_encode(pfarr, pfgc | q) val A2 = arrayptr_refize(A2) // non-linearizing val ASZ2 = arrszref_make_arrayref(A2, asz) // in array0_of_arrszref{a}(ASZ2) end // end of [array0_copy] (* ****** ****** *) implement {a}(*tmp*) array0_append (A01, A02) = let // val ASZ1 = arrszref_of_array0(A01) and ASZ2 = arrszref_of_array0(A02) // var asz1: size_t and asz2: size_t // val A1 = arrszref_get_refsize(ASZ1, asz1) and A2 = arrszref_get_refsize(ASZ2, asz2) // val (pf1box | p1) = arrayref_get_viewptr(A1) and (pf2box | p2) = arrayref_get_viewptr(A2) // extern praxi unbox{v:view} : vbox(v) - (v, v - void) // prval (pf1, fpf1) = unbox(pf1box) and (pf2, fpf2) = unbox(pf2box) // val asz = asz1 + asz2 // val (pfarr,pfgc|q) = array_ptr_alloc(asz) // prval (pf1arr, pf2arr) = array_v_split_at(pfarr | asz1) // val () = array_copy(!q, !p1, asz1) val q2 = ptr1_add_guint(q, asz1) val (pf2arr | q2) = viewptr_match(pf2arr | q2) val () = array_copy(!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 // end of [array0_append] (* ****** ****** *) // implement {a}{b} array0_map (A, fopr) = let // val p0 = array0_get_ref(A) val asz = array0_get_size(A) // val fopr = $UN.cast{cfun1(ptr, b)}(fopr) // in // array0_tabulate (g1ofg0(asz), lam i => fopr(ptr_add(p0, i))) // end // end of [array0_map] // implement {a}{b} array0_map_method (A0, _(*TYPE*)) = lam(fopr) => array0_map(A0, fopr) // (* ****** ****** *) implement {a}(*tmp*) 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 // array_tabulate$fopr // in // array0_of_arrszref(arrszref_tabulate(asz)) // end // end of [array0_tabulate] (* ****** ****** *) // implement {a}(*tmp*) array0_tabulate_method_int (asz) = ( lam(fopr) => array0_tabulate (i2sz(asz), lam(i) => fopr(sz2i(i))) ) // implement {a}(*tmp*) array0_tabulate_method_size (asz) = ( lam(fopr) => array0_tabulate(asz, fopr) ) // (* ****** ****** *) implement {a}(*tmp*) array0_find_exn (A0, p) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement(tenv) array_foreach$cont(x, env) = ~p(x) implement(tenv) array_foreach$fwork(x, env) = ((*nothing*)) // val idx = arrayref_foreach(A, asz) // in if idx < asz then idx else $raise NotFoundExn() end // end of [array0_find_exn] (* ****** ****** *) (* /* implement {a}(*tmp*) array0_find_opt (A0, p) = try Some_vt(array0_find_exn (A0, p)) with ~NotFoundExn() => None_vt() // end of [array0_find_opt] */ *) (* ****** ****** *) // implement {a}(*tmp*) array0_exists (A0, pred) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement array_foreach$cont (x, env) = not(env) implement array_foreach$fwork (x, env) = if pred(x) then env := true else () // in // env where { // var env:bool = false val _(*asz*) = arrayref_foreach_env(A, asz, env) // } (* end of [where] *) // end // end of [array0_exists] // implement {a}(*tmp*) array0_exists_method(A0) = lam(pred) => array0_exists(A0, pred) // (* ****** ****** *) // implement {a}(*tmp*) array0_iexists (A0, pred) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement array_iforeach$cont (i, x, env) = not(env) implement array_iforeach$fwork (i, x, env) = if pred(i, x) then env := true else () // in // env where { // var env:bool = false val _(*asz*) = arrayref_iforeach_env(A, asz, env) // } (* end of [where] *) // end // end of [array0_iexists] // implement {a}(*tmp*) array0_iexists_method(A0) = lam(pred) => array0_iexists(A0, pred) // (* ****** ****** *) // implement {a}(*tmp*) array0_forall (A0, pred) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement array_foreach$cont (x, env) = (env) implement array_foreach$fwork (x, env) = if pred(x) then () else env := false // in // env where { // var env:bool = true val _(*asz*) = arrayref_foreach_env(A, asz, env) // } (* end of [where] *) // end // end of [array0_forall] // implement {a}(*tmp*) array0_forall_method(A0) = lam(pred) => array0_forall(A0, pred) // (* ****** ****** *) // implement {a}(*tmp*) array0_iforall (A0, pred) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement array_iforeach$cont (i, x, env) = (env) implement array_iforeach$fwork (i, x, env) = if pred(i, x) then () else env := false // in // env where { // var env:bool = true val _(*asz*) = arrayref_iforeach_env(A, asz, env) // } (* end of [where] *) // end // end of [array0_iforall] // implement {a}(*tmp*) array0_iforall_method(A0) = lam(pred) => array0_iforall(A0, pred) // (* ****** ****** *) implement {a}(*tmp*) array0_foreach (A0, fwork) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement(tenv) array_foreach$cont(x, env) = true implement(tenv) array_foreach$fwork(x, env) = fwork(x) // val _(*asz*) = arrayref_foreach(A, asz) // in // nothing end // end of [array0_foreach] // implement {a}(*tmp*) array0_foreach_method(A0) = lam(fwork) => array0_foreach(A0, fwork) // (* ****** ****** *) implement {a}(*tmp*) array0_iforeach (A0, fwork) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement(tenv) array_iforeach$cont(i, x, env) = true implement(tenv) array_iforeach$fwork(i, x, env) = fwork(i, x) // val _(*asz*) = arrayref_iforeach (A, asz) // in // nothing end // end of [array0_iforeach] // implement {a}(*tmp*) array0_iforeach_method(A0) = lam(fwork) => array0_iforeach(A0, fwork) // (* ****** ****** *) implement {a}(*tmp*) array0_rforeach (A0, fwork) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement(tenv) array_rforeach$cont(x, env) = true implement(tenv) array_rforeach$fwork(x, env) = fwork(x) // val _(*asz*) = arrayref_rforeach (A, asz) // in // nothing end // end of [array0_rforeach] // implement {a}(*tmp*) array0_rforeach_method(A0) = lam(fwork) => array0_rforeach(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 (x, env) = true implement array_foreach$fwork (x, env) = env := fopr(env, x) // var res: tres = ini val _(*asz*) = arrayref_foreach_env(A, asz, res) // } (* end of [array0_foldleft] *) // implement {tres}{a} array0_foldleft_method(A0, _) = lam(ini, fopr) => array0_foldleft(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(i, x, env) = true implement array_iforeach$fwork(i, x, env) = (env := fopr(env, i, x)) // var res: tres = ini val _(*asz*) = arrayref_iforeach_env(A, asz, res) // } (* end of [array0_ifoldleft] *) // implement {tres}{a} array0_ifoldleft_method(A0, _) = lam(ini, fopr) => array0_ifoldleft(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 (x, env) = true implement array_rforeach$fwork (x, env) = env := fopr(x, env) // var res: tres = snk // val _(*asz*) = arrayref_rforeach_env(A, asz, res) // } (* end of [array0_foldright] *) // implement {a}{tres} array0_foldright_method (A0, _) = ( lam(fopr, snk) => array0_foldright(A0, fopr, snk) ) (* end of [lam] *) // (* ****** ****** *) implement {a}(*tmp*) array0_is_ordered (A0, cmp) = let // implement gcompare_ref_ref (x, y) = $effmask_all(cmp(x, y)) // in (* in-of-let *) // let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // in // arrayref_is_ordered(A, asz) // end // end of [let] // end // end of [array0_is_ordered] (* ****** ****** *) implement {a}(*tmp*) array0_quicksort (A0, cmp) = let // val ASZ = arrszref_of_array0(A0) // var asz : size_t val A = arrszref_get_refsize(ASZ, asz) // implement {a}(*tmp*) array_quicksort$cmp (x1, x2) = let // val cmp = $UN.cast{(&a,&a)-int}(cmp) // in cmp(x1, x2) end // end of [array_quicksort$cmp] // in arrayref_quicksort (A, asz) end // end of [array0_quicksort] (* ****** ****** *) // // HX: some common generic functions // (* ****** ****** *) implement (a)(*tmp*) fprint_val = fprint_array0 (* ****** ****** *) implement (a)(*tmp*) gcompare_val_val (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(px), ptr_succ(py), succ(i), succ(j)) // end of [if] end else (1) // end of [else] // ) else ( // if j < n then (~1) else (0) // ) (* end of [else] *) ) (* end of [loop] *) // in $effmask_all(loop(array0_get_ref{a}(xs), array0_get_ref{a}(xs), i2sz(0), i2sz(0))) end // end of [gcompare_val_val] (* ****** ****** *) (* end of [array0.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2014 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: February, 2014 *) (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) staload "libats/ML/SATS/basis.sats" staload "libats/ML/SATS/matrix0.sats" (* ****** ****** *) // implement {}(*tmp*) matrix0_of_mtrxszref{a}(A) = $UN.cast{matrix0(a)}(A) // implement {}(*tmp*) mtrxszref_of_matrix0{a}(A) = $UN.cast{mtrxszref(a)}(A) // (* ****** ****** *) // implement{ } matrix0_get_ref (M) = mtrxszref_get_ref (mtrxszref_of_matrix0(M)) // implement {}(*tmp*) matrix0_get_nrow(M) = mtrxszref_get_nrow(mtrxszref_of_matrix0(M)) implement {}(*tmp*) matrix0_get_ncol (M) = mtrxszref_get_ncol(mtrxszref_of_matrix0(M)) // (* ****** ****** *) implement{ } matrix0_get_refsize (M) = let // var nrow: size_t // uninitized and ncol: size_t // uninitized // val Mref = $effmask_wrt ( mtrxszref_get_refsize(mtrxszref_of_matrix0(M), nrow, ncol) ) (* end of [val] *) // in (Mref, nrow, ncol) end // end of [matrix0_get_refsize] (* ****** ****** *) // implement {a}(*tmp*) matrix0_make_elt_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(nrow, ncol, x0)) end // end of [matrix0_make_elt_int] // implement {a}(*tmp*) matrix0_make_elt_size (nrow, ncol, x0) = ( matrix0_of_mtrxszref(mtrxszref_make_elt(nrow, ncol, x0)) ) (* end of [matrix0_make_elt_size] *) // (* ****** ****** *) implement {a}(*tmp*) matrix0_get_at_int (M0, i, j) = let val i = g1ofg0_int(i) and j = g1ofg0_int(j) in // if i >= 0 then ( if j >= 0 then matrix0_get_at_size(M0, i2sz(i), i2sz(j)) else $raise MatrixSubscriptExn((*void*)) // neg index // end of [if] ) else $raise MatrixSubscriptExn((*void*)) // neg index // end of [if] // end // end of [matrix0_get_at_int] (* ****** ****** *) implement {a}(*tmp*) matrix0_get_at_size (M0, i, j) = let // val MSZ = mtrxszref_of_matrix0(M0) // in mtrxszref_get_at_size(MSZ, i, j) // end of [val] end // end of [matrix0_get_at_size] (* ****** ****** *) implement {a}(*tmp*) matrix0_set_at_int (M0, i, j, x) = let val i = g1ofg0_int(i) and j = g1ofg0_int(j) in // if i >= 0 then ( if j >= 0 then matrix0_set_at_size(M0, i2sz(i), i2sz(j), x) else $raise MatrixSubscriptExn((*void*)) (* neg index *) // end of [if] ) else $raise MatrixSubscriptExn((*void*)) (* neg index *) // end of [if] // end // end of [matrix0_set_at_int] (* ****** ****** *) implement {a}(*tmp*) matrix0_set_at_size (M0, i, j, x) = let // val MSZ = mtrxszref_of_matrix0{a}(M0) // in mtrxszref_set_at_size(MSZ, i, j, x) end // end of [matrix0_set_at_size] (* ****** ****** *) // implement {a}(*tmp*) print_matrix0 (A) = fprint_matrix0(stdout_ref, A) // implement {a}(*tmp*) prerr_matrix0 (A) = fprint_matrix0(stderr_ref, A) // implement {a}(*tmp*) fprint_matrix0(out, M) = fprint_mtrxszref(out, mtrxszref_of_matrix0(M)) // implement {a}(*tmp*) fprint_matrix0_sep(out, M, sep1, sep2) = fprint_mtrxszref_sep(out, mtrxszref_of_matrix0(M), sep1, sep2) // (* ****** ****** *) implement {a}(*tmp*) matrix0_copy(M0) = let // val M = matrix0_get_ref(M0) // val [m:int] m = g1ofg0(M0.nrow()) val [n:int] n = g1ofg0(M0.ncol()) // val M = matrixref_copy($UN.cast{matrixref(a,m,n)}(M), m, n) // end of [val] in // matrix0_of_mtrxszref (mtrxszref_make_matrixref{a}(matrixptr_refize{a}(M), m, n)) // end // end of [matrix0_copy] (* ****** ****** *) implement {a}(*tmp*) matrix0_tabulate {m,n} (nrow, ncol, fopr) = let // implement {a2}(*tmp*) 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 // end of [matrix_tabulate$fopr] // in matrix0_of_mtrxszref{a}(mtrxszref_tabulate(nrow, ncol)) end // end of [matrix0_tabulate] (* ****** ****** *) // implement {a}(*tmp*) matrix0_tabulate_method_int (nrow, ncol) = ( lam(fopr) => matrix0_tabulate ( i2sz(nrow) , i2sz(ncol), lam(i, j) => fopr(sz2i(i), sz2i(j)) ) ) // implement {a}(*tmp*) matrix0_tabulate_method_size (nrow, ncol) = ( lam(fopr) => matrix0_tabulate(nrow, ncol, fopr) ) // (* ****** ****** *) implement {a}(*tmp*) 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 ((*void*)) = fwork(!p) // prval ((*returned*)) = fpf(pf) // in loop(ptr_succ(p), pred(i)) end else ((*void*)) // end of [if] ) (* end of [loop] *) // val (M, m, n) = matrix0_get_refsize(M0) // in loop(ptrcast(M), m * n) end // end of [matrix0_foreach] (* ****** ****** *) implement {a}(*tmp*) matrix0_iforeach (M0, 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 ((*returned*)) = fpf(pf) // val p = ptr_succ(p) val k = pred(k) and j = succ(j) // in // if j < n then loop(p, k, i, j) else loop(p, k, succ(i), i2sz(0)) // end of [if] // end else ((*void*)) // end of [if] ) (* end of [loop] *) // in loop(ptrcast(M), m * n, i2sz(0), i2sz(0)) end // end of [matrix0_iforeach] (* ****** ****** *) implement {res}{a}(*tmp*) matrix0_foldleft ( M0, ini, fopr ) = ini where { // var ini: res = ini val p_ini = addr@(ini) // var fopr2 = lam@(x: &a): void => $UN.ptr0_set(p_ini, fopr($UN.ptr0_get(p_ini), x)) // val () = matrix0_foreach(M0, $UN.cast{(&a)-void}(addr@fopr2)) // } (* end of [matrix0_foldleft] *) (* ****** ****** *) implement {res}{a}(*tmp*) 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 (p_ini, fopr($UN.ptr0_get(p_ini), i, j, x)) // val () = matrix0_iforeach (M0, $UN.cast{(size_t,size_t,&a)-void}(addr@fopr2)) // } (* end of [matrix0_ifoldleft] *) (* ****** ****** *) (* end of [matrix0.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2016 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: October, 2016 *) (* ****** ****** *) #define ATS_DYNLOADFLAG 0 (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) staload "libats/ML/SATS/basis.sats" staload "libats/ML/SATS/list0.sats" staload "libats/ML/SATS/stream.sats" (* ****** ****** *) // implement {}(*tmp*) intgte_stream(n) = f(n) where { fun f(n:int): stream(int) = $delay(stream_cons(n, f(n+1))) } // (* ****** ****** *) // implement {a}(*tmp*) stream2list0(xs) = list0_of_list_vt(stream2list(xs)) // (* ****** ****** *) implement {a}(*tmp*) stream_make_list0 (xs) = auxmain(xs) where { // fun auxmain: $d2ctype ( stream_make_list0 ) = lam(xs) => $delay ( case+ xs of | list0_nil() => stream_nil() | list0_cons(x, xs) => stream_cons(x, auxmain(xs)) ) // } (* end of [stream_make_list0] *) (* ****** ****** *) // implement {}(*tmp*) stream_make_intrange_lr (l, r) = ( stream_make_intrange_lrd<>(l, r, 1) ) // implement {}(*tmp*) stream_make_intrange_lrd (l, r, d) = let // fun auxmain ( l: int , r: int , d: int ) : stream(int) = $delay ( if (l >= r) then stream_nil() else stream_cons(l, auxmain(l+d, r, d)) ) // in auxmain(l, r, d) end // end of [stream_make_intrange_lrd] // (* ****** ****** *) // implement {a}{b} stream_map (xs, fopr) = ( stream_map_cloref(xs, fopr) ) // implement {a}{b} stream_map_method (xs, _) = ( lam(fopr) => stream_map_cloref(xs, fopr) ) // (* ****** ****** *) // implement {a}{b} stream_imap (xs, fopr) = ( stream_imap_cloref(xs, fopr) ) // implement {a}{b} stream_imap_method (xs, _) = ( lam(fopr) => stream_imap_cloref(xs, fopr) ) // (* ****** ****** *) // implement {a}(*tmp*) stream_filter (xs, pred) = stream_filter_cloref(xs, pred) implement {a}(*tmp*) stream_filter_method (xs) = ( lam(pred) => stream_filter_cloref(xs, pred) ) // (* ****** ****** *) // implement {res}{x} stream_scan (xs, res, fopr) = ( stream_scan_cloref(xs, res, fopr) ) // implement {res}{x} stream_scan_method(xs, _) = ( lam(res, fopr) => stream_scan_cloref(xs, res, fopr) ) // (* ****** ****** *) // implement {a}(*tmp*) stream_foreach (xs, fwork) = stream_foreach_cloref(xs, fwork) // implement {a}(*tmp*) stream_foreach_method(xs) = ( lam(fwork) => stream_foreach_cloref(xs, fwork) // end of [lam] ) // (* ****** ****** *) // implement {a}(*tmp*) stream_iforeach (xs, fwork) = stream_iforeach_cloref(xs, fwork) // implement {a}(*tmp*) stream_iforeach_method(xs) = ( lam(fwork) => stream_iforeach_cloref(xs, fwork) // end of [lam] ) // (* ****** ****** *) // implement {res}{a} stream_foldleft (xs, ini, fopr) = stream_foldleft_cloref(xs, ini, fopr) // implement {res}{a} stream_foldleft_method (xs, _(*TYPE*)) = lam(ini, fopr) => stream_foldleft_cloref(xs, ini, fopr) // end of [lam] // (* ****** ****** *) (* end of [stream.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2016 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: October, 2016 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) #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}(*tmp*) stream2list0_vt (xs) = ( list0_vt2t (g0ofg1(stream2list_vt(xs))) ) // (* ****** ****** *) // implement {}(*tmp*) intGte_stream_vt(n) = f(n) where { fun f(n:int): stream_vt(int) = $ldelay(stream_vt_cons(n, f(n+1))) } // (* ****** ****** *) implement {a}(*tmp*) stream_vt_make_list0 (xs) = auxmain(xs) where { // fun auxmain: $d2ctype ( stream_vt_make_list0 ) = lam(xs) => $ldelay ( case+ xs of | list0_nil() => stream_vt_nil() | list0_cons(x, xs) => stream_vt_cons(x, auxmain(xs)) ) // } (* end of [stream_vt_make_list0] *) (* ****** ****** *) // implement {}(*tmp*) stream_vt_make_intrange_lr (l, r) = ( stream_vt_make_intrange_lrd<>(l, r, 1) ) // implement {}(*tmp*) stream_vt_make_intrange_lrd (l, r, d) = let // fun auxmain ( l: int , r: int , d: int ) : 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 // end of [stream_vt_make_intrange_lrd] // (* ****** ****** *) // implement {a}{b} stream_vt_map_method (xs, _) = ( llam(fopr) => stream_vt_map_cloptr(xs, fopr) ) // (* ****** ****** *) // implement {a}(*tmp*) stream_vt_filter_method (xs) = ( llam(pred) => stream_vt_filter_cloptr(xs, pred) ) // (* ****** ****** *) // implement {a}(*tmp*) stream_vt_foreach_method (xs) = ( llam(fwork) => stream_vt_foreach_cloptr(xs, fwork) ) // implement {a}(*tmp*) stream_vt_rforeach_method (xs) = ( llam(fwork) => stream_vt_rforeach_cloptr(xs, fwork) ) // (* ****** ****** *) // implement {a}(*tmp*) stream_vt_iforeach_method (xs) = ( llam(fwork) => stream_vt_iforeach_cloptr(xs, fwork) ) // (* ****** ****** *) // implement {res}{a} stream_vt_foldleft_method (xs, _(*TYPE*)) = ( llam(ini, fwork) => stream_vt_foldleft_cloptr(xs, ini, fwork) ) // implement {res}{a} stream_vt_ifoldleft_method (xs, _(*TYPE*)) = ( llam(ini, fwork) => stream_vt_ifoldleft_cloptr(xs, ini, fwork) ) // (* ****** ****** *) (* end of [stream_vt.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: January, 2013 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) // #define ATS_DYNLOADFLAG 0 // // no dynloading at run-time // (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) staload _(*anon*) = "prelude/DATS/integer.dats" staload _(*anon*) = "prelude/DATS/integer_size.dats" (* ****** ****** *) staload _(*anon*) = "prelude/DATS/filebas.dats" (* ****** ****** *) // macdef prelude_fileref_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_open_opt (path, mode) = let // val opt = prelude_fileref_open_opt (path, mode) // in option0_of_option_vt{FILEref}(opt) end // end of [fileref_open_opt] *) (* ****** ****** *) implement fileref_get_line_charlst (filr) = ( list0_of_list_vt (prelude_fileref_get_line_charlst(filr)) ) // end of [fileref_get_line_charlst] implement fileref_get_lines_charlstlst (filr) = ( $UN.castvwtp0{list0(charlst0)} (prelude_fileref_get_lines_charlstlst(filr)) ) // end of [fileref_get_lines_charlstlst] (* ****** ****** *) local // staload _(*anon*) = "prelude/DATS/strptr.dats" // in (* in of [local] *) implement fileref_get_line_string (filr) = ( strptr2string (prelude_fileref_get_line_string(filr)) ) // end of [fileref_get_line_string] implement fileref_get_lines_stringlst (filr) = ( $UN.castvwtp0{list0(string)} (prelude_fileref_get_lines_stringlst(filr)) ) // end of [fileref_get_lines_stringlst] end // end of [local] (* ****** ****** *) implement {}(*tmp*) 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) // end of [val] val ((*void*)) = fileref_close(inp) } (* end of [Some_vt] *) // end // end of [filename_get_lines_stringlst_opt] (* ****** ****** *) // implement {}(*tmp*) streamize_fileref_char (filr) = prelude_streamize_fileref_char(filr) implement {}(*tmp*) streamize_fileptr_char (filp) = prelude_streamize_fileptr_char(filp) // (* ****** ****** *) // implement {}(*tmp*) streamize_fileref_line (filr) = ( $UN.castvwtp0{stream_vt(string)} (prelude_streamize_fileref_line(filr)) ) // end of [streamize_fileref_line] implement {}(*tmp*) streamize_fileptr_line (filp) = ( $UN.castvwtp0{stream_vt(string)} (prelude_streamize_fileptr_line(filp)) ) // end of [streamize_fileptr_line] // (* ****** ****** *) implement {}(*tmp*) streamize_fileref_word (filr) = auxmain(filr) where { // fun auxmain ( filr: FILEref ) : stream_vt(string) = $ldelay ( // let // val word = fileref_get_word<>(filr) val test = strptr_is_null(word) // prval () = lemma_strptr_param(word) // in if test then let prval () = strptr_free_null(word) in stream_vt_nil() // end of [prval] end // end of [then] else stream_vt_cons(strptr2string(word), auxmain(filr)) // end of [if] end // end of [let] // ) (* end of [auxmain] *) // } (* end of [streamize_fileref_word] *) (* ****** ****** *) implement {}(*tmp*) 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) } (* end of [then] *) else stream_vt_cons(strptr2string(word), auxmain(filr)) // end of [if] end // end of [let] // ) (* end of [auxmain] *) // in auxmain($UN.castvwtp0{FILEref}(filp)) end (* end of [streamize_fileptr_word] *) (* ****** ****** *) implement {}(*tmp*) 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 // end of [streamize_filename_char] (* ****** ****** *) implement {}(*tmp*) 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 // end of [streamize_filename_line] (* ****** ****** *) implement {}(*tmp*) 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 // end of [streamize_filename_word] (* ****** ****** *) (* end of [filebas.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: September, 2014 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) staload "libats/ML/SATS/list0.sats" staload "libats/ML/SATS/array0.sats" staload "libats/ML/SATS/intrange.sats" (* ****** ****** *) // implement {}(*tmp*) int_repeat_lazy (n, f) = ( int_repeat_cloref<>(n, lazy2cloref(f)) ) // (* ****** ****** *) implement {}(*tmp*) 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 ((*void*)) // ) (* end of [loop] *) // } // end of [int_repeat_cloref] (* ****** ****** *) // implement {}(*tmp*) int_repeat_method (n) = ( lam(f) => int_repeat_cloref<>(n, f) ) // (* ****** ****** *) // implement {}(*tmp*) int_forall_cloref (n, f) = intrange_forall_cloref<>(0, n, f) // implement {}(*tmp*) int_forall_method (n) = ( lam(f) => int_forall_cloref<>(n, f) ) // (* ****** ****** *) // implement {}(*tmp*) int_foreach_cloref (n, f) = intrange_foreach_cloref<>(0, n, f) // implement {}(*tmp*) int_foreach_method (n) = ( lam(f) => int_foreach_cloref<>(n, f) ) // (* ****** ****** *) // implement {}(*tmp*) int_rforeach_cloref (n, f) = intrange_rforeach_cloref<>(0, n, f) // implement {}(*tmp*) int_rforeach_method (n) = lam(f) => int_rforeach_cloref<>(n, f) // (* ****** ****** *) // implement {res}(*tmp*) int_foldleft_cloref (n, ini, f) = intrange_foldleft_cloref(0, n, ini, f) // implement {res}(*tmp*) int_foldleft_method (n, tres) = ( lam(ini, f) => int_foldleft_cloref(n, ini, f) ) // (* ****** ****** *) // implement {res}(*tmp*) int_foldright_cloref (n, f, snk) = intrange_foldright_cloref(0, n, f, snk) // implement {res}(*tmp*) int_foldright_method (n, tres) = ( lam(f, snk) => int_foldright_cloref(n, f, snk) ) // (* ****** ****** *) implement {}(*tmp*) intrange_forall_cloref (l, r, f) = let // fun loop ( l: int, r: int , f: cfun1(int, bool) ) : bool = ( // if l < r then ( if f(l) then loop(l+1, r, f) else false ) else true // ) (* end of [loop] *) // in loop (l, r, f) end // end of [intrange_forall_cloref] // implement {}(*tmp*) intrange_forall_method ( @(l, r) ) = lam(f) => intrange_forall_cloref<>(l, r, f) // (* ****** ****** *) // implement {}(*tmp*) intrange_foreach_cloref (l, r, f) = let // fun loop ( l: int, r: int, f: cfun1(int, void) ) : void = ( // if (l < r) then ( let val () = f(l) in loop(l+1, r, f) end ) else ((*void*)) // ) (* end of [loop] *) // in loop (l, r, f) end // end of [intrange_foreach_cloref] // implement {}(*tmp*) intrange_foreach_method ( @(l, r) ) = lam(f) => intrange_foreach_cloref<>(l, r, f) // (* ****** ****** *) // implement {}(*tmp*) 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 ((*void*)) // ) (* end of [loop] *) // in loop (l, r, f) end // end of [intrange_rforeach_cloref] // implement {}(*tmp*) intrange_rforeach_method ( @(l, r) ) = lam(f) => intrange_rforeach_cloref<>(l, r, f) // (* ****** ****** *) implement {res}(*tmp*) intrange_foldleft_cloref (l, r, ini, fopr) = let // fun loop ( l: int, r: int , ini: res, f: cfun2(res, int, res) ) : res = ( // if (l < r) then loop(l+1, r, f(ini, l), f) else ini // end of [if] // ) (* end of [loop] *) // in loop(l, r, ini, fopr) end // end of [intrange_foldleft_cloref] (* ****** ****** *) // implement {res}(*tmp*) intrange_foldleft_method ( @(l, r), tres ) = ( // lam(ini, f) => intrange_foldleft_cloref(l, r, ini, f) // ) (* end of [intrange_foldleft_method] *) // (* ****** ****** *) implement {res}(*tmp*) 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 // end of [then] else snk // end of [else] // ) (* end of [loop] *) // in loop(l, r, f, snk) end // end of [intrange_foldright_cloref] (* ****** ****** *) // implement {res}(*tmp*) intrange_foldright_method ( @(l, r), tres ) = ( // lam(f, snk) => intrange_foldright_cloref(l, r, f, snk) // ) (* end of [intrange_foldright_method] *) // (* ****** ****** *) // implement {}(*tmp*) int_streamGte(n) = ( fix aux ( n: int ) : stream(int) => $delay(stream_cons(n, aux(n+1))) ) (n) // end of [int_streamGte] // implement {}(*tmp*) int_streamGte_vt(n) = ( fix aux ( n: int ) : stream_vt(int) => $ldelay(stream_vt_cons(n, aux(n+1))) ) (n) // end of [int_streamGte_vt] // (* ****** ****** *) // implement {a}(*tmp*) int_list0_map_cloref (n, f) = list0_tabulate(n, f) // implement {a}(*tmp*) int_list0_map_method (n, tres) = lam(f) => int_list0_map_cloref(n, f) // (* ****** ****** *) // implement {a}(*tmp*) int_array0_map_cloref (n, fopr) = ( array0_tabulate (i2sz(n), lam(i) => fopr(sz2i(i))) ) // implement {a}(*tmp*) int_array0_map_method (n, tres) = lam(f) => int_array0_map_cloref(n, f) // (* ****** ****** *) // implement {a}(*tmp*) int_stream_map_cloref (n, f) = auxmain(0) where { // fun auxmain ( i: Nat ) : stream(a) = $delay ( if (i >= n) then stream_nil((*void*)) else stream_cons(f(i), auxmain(i+1)) ) (* end of [auxmain] *) // } (* end of [int_stream_map_cloref] *) // implement {a}(*tmp*) int_stream_map_method (n, tres) = ( // lam(f) => int_stream_map_cloref(n, f) // ) (* int_stream_map_method *) // (* ****** ****** *) // implement {a}(*tmp*) int_stream_vt_map_cloref (n, f) = auxmain(0) where { // fun auxmain ( i: Nat ) : stream_vt(a) = $ldelay ( if (i >= n) then stream_vt_nil((*void*)) else stream_vt_cons(f(i), auxmain(i+1)) // end of [then] // ) : stream_vt_con(a) // [auxmain] // } (* end of [int_stream_vt_map_cloref] *) // implement {a}(*tmp*) int_stream_vt_map_method (n, tres) = ( // lam(f) => int_stream_vt_map_cloref(n, f) // ) // (* ****** ****** *) // implement {}(*tmp*) int2_foreach_cloref (n1, n2, f0) = ( intrange2_foreach_cloref<> ( 0(*l1*), n1(*r1*) , 0(*l2*), n2(*r2*), f0 ) ) // implement {}(*tmp*) 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 ((*void*)) // end of [if] // ) (* end of [loop1] *) // 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 // end of [then] else ( loop1(m1+1, r1, l2, r2, f0) ) (* end of [else] *) // ) (* end of [loop2] *) // in loop1(l1, r1, l2, r2, f0) end // end of [intrange2_foreach_cloref] // (* ****** ****** *) (* end of [intrange.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: August, 2013 *) (* ****** ****** *) // // HX-2012-12: // the map implementation is based on AVL trees // (* ****** ****** *) // staload FM = "libats/SATS/funmap_avltree.sats" // (* ****** ****** *) staload "libats/ML/SATS/list0.sats" (* ****** ****** *) staload "libats/ML/SATS/funmap.sats" (* ****** ****** *) // assume map_type(key, itm) = $FM.map (key, itm) // (* ****** ****** *) implement{a} compare_key_key = gcompare_val_val implement{a} $FM.compare_key_key = compare_key_key (* ****** ****** *) implement {}(*tmp*) funmap_nil() = $FM.funmap_nil<>() implement {}(*tmp*) funmap_make_nil() = $FM.funmap_make_nil<>() (* ****** ****** *) implement {}(*tmp*) funmap_is_nil(map) = $FM.funmap_is_nil<>(map) implement {}(*tmp*) funmap_isnot_nil(map) = $FM.funmap_isnot_nil<>(map) (* ****** ****** *) // implement {key,itm} funmap_size (map) = $FM.funmap_size(map) // (* ****** ****** *) // implement {key,itm} funmap_search (map, k) = $FM.funmap_search_opt(map, k) // (* ****** ****** *) // implement {key,itm} funmap_insert (map, k, x) = $FM.funmap_insert_opt(map, k, x) // (* ****** ****** *) // implement {key,itm} funmap_takeout (map, k) = $FM.funmap_takeout_opt(map, k) // (* ****** ****** *) // implement {key,itm} funmap_remove (map, k) = $FM.funmap_remove(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(out, map) // in // nothing end // end of [fprint_funmap] (* ****** ****** *) implement{} fprint_funmap$sep(out) = fprint(out, "; ") implement{} fprint_funmap$mapto(out) = fprint(out, "->") (* ****** ****** *) implement {key,itm} funmap_foreach_cloref (map, fwork) = () where { // var env: void = ((*void*)) // implement (env)(*tmp*) $FM.funmap_foreach$fwork (k, x, env) = fwork(k, x) // val ((*void*)) = $FM.funmap_foreach_env(map, env) // } (* end of [funmap_foreach_cloref] *) (* ****** ****** *) // implement {key,itm} funmap_listize (map) = ( $effmask_wrt ( list0_of_list_vt ($FM.funmap_listize(map)) ) ) (* end of [funmap_listize] *) // (* ****** ****** *) implement {key,itm} funmap_streamize (map) = ( $effmask_wrt ($FM.funmap_streamize(map)) ) (* end of [funmap_streamize] *) (* ****** ****** *) // implement {key,itm} funmap_make_module ((*void*)) = $rec { // nil = funmap_nil{key,itm} , size = funmap_size , is_nil = funmap_is_nil{key,itm} , isnot_nil = funmap_isnot_nil{key,itm} , search = funmap_search , insert = funmap_insert , remove = funmap_remove , takeout = funmap_takeout , listize = funmap_listize , streamize = funmap_streamize // } (* end of [funmap_make_module] *) // (* ****** ****** *) (* end of [funmap.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Start time: December, 2012 *) (* Authoremail: gmhwxiATgmailDOTcom *) (* ****** ****** *) // // HX-2012-12: // this set implementation // is based on the AVL trees // (* ****** ****** *) // staload UN = "prelude/SATS/unsafe.sats" // (* ****** ****** *) // staload FS = "libats/SATS/funset_avltree.sats" // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) staload "libats/ML/SATS/list0.sats" (* ****** ****** *) staload "libats/ML/SATS/funset.sats" (* ****** ****** *) implement {a}(*tmp*) compare_elt_elt = gcompare_val_val implement {a}(*tmp*) $FS.compare_elt_elt = compare_elt_elt (* ****** ****** *) assume set_type(a:t0p) = $FS.set(a) (* ****** ****** *) // implement {}(*tmp*) funset_nil ((*void*)) = $FS.funset_nil() implement {}(*tmp*) funset_make_nil ((*void*)) = $FS.funset_make_nil() // (* ****** ****** *) // implement {a}(*tmp*) funset_sing (x0) = $FS.funset_sing(x0) implement {a}(*tmp*) funset_make_sing (x0) = $FS.funset_make_sing(x0) // (* ****** ****** *) implement {a}(*tmp*) funset_make_list (xs) = let // val xs = g1ofg0_list(xs) // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_make_list(xs) end // end of [funset_make_list] (* ****** ****** *) // implement {}(*tmp*) fprint_funset$sep (out) = fprint_string (out, ", ") // implement {a}(*tmp*) fprint_funset (out, xs) = let // implement $FS.fprint_funset$sep<> (out) = fprint_funset$sep<>(out) // in $FS.fprint_funset(out, xs) end // end of [fprint_funset] // (* ****** ****** *) // implement {}(*tmp*) funset_is_nil (xs) = $FS.funset_is_nil<>(xs) implement {}(*tmp*) funset_isnot_nil (xs) = $FS.funset_isnot_nil<>(xs) // (* ****** ****** *) // implement {a}(*tmp*) funset_size(xs) = $FS.funset_size(xs) // (* ****** ****** *) // implement {a}(*tmp*) funset_is_member (xs, x0) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_is_member(xs, x0) end // end of [funset_is_member] // implement {a}(*tmp*) funset_isnot_member (xs, x0) = ~funset_is_member(xs, x0) // (* ****** ****** *) implement {a}(*tmp*) funset_insert (xs, x0) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_insert(xs, x0) end // end of [funset_insert] (* ****** ****** *) implement {a}(*tmp*) funset_remove (xs, x0) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_remove(xs, x0) end // end of [funset_remove] (* ****** ****** *) // implement {a}(*tmp*) funset_getmax_opt = $FS.funset_getmax_opt implement {a}(*tmp*) funset_getmin_opt = $FS.funset_getmin_opt // (* ****** ****** *) // implement {a}(*tmp*) funset_takeoutmax_opt = $FS.funset_takeoutmax_opt implement {a}(*tmp*) funset_takeoutmin_opt = $FS.funset_takeoutmin_opt // (* ****** ****** *) implement {a}(*tmp*) funset_union (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_union(xs1, xs2) end // end of [funset_union] (* ****** ****** *) // implement {a}(*tmp*) funset_intersect (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_intersect(xs1, xs2) end // end of [funset_intersect] // (* ****** ****** *) // implement {a}(*tmp*) funset_differ (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_differ(xs1, xs2) end // end of [funset_differ] (* ****** ****** *) // implement {a}(*tmp*) funset_symdiff (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_symdiff(xs1, xs2) end // end of [funset_symdiff] // (* ****** ****** *) // implement {a}(*tmp*) funset_equal (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_equal(xs1, xs2) end // end of [funset_equal] // (* ****** ****** *) // implement {a}(*tmp*) funset_compare (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_compare(xs1, xs2) end // end of [funset_compare] // (* ****** ****** *) // implement {a}(*tmp*) funset_is_subset (xs1, xs2) = let // implement $FS.compare_elt_elt = compare_elt_elt // in $FS.funset_is_subset(xs1, xs2) end // end of [funset_is_subset] // implement {a}(*tmp*) funset_is_supset (xs1, xs2) = funset_is_subset(xs2, xs1) // (* ****** ****** *) implement {a}(*tmp*) funset_foreach(xs) = let // var env: void = ((*void*)) // in funset_foreach_env(xs, env) end // end of [funset_foreach] implement {a}{env} funset_foreach_env(xs, env) = let // implement $FS.funset_foreach$fwork (x, env) = funset_foreach$fwork(x, env) // in $FS.funset_foreach_env(xs, env) end // end of [funset_foreach_env] implement {a}(*tmp*) funset_foreach_cloref (xs, fwork) = let // var env: void = ((*void*)) // implement (env)(*tmp*) $FS.funset_foreach$fwork(x, env) = fwork(x) // in $FS.funset_foreach_env (xs, env) end // end of [funset_foreach_cloref] (* ****** ****** *) implement {a}(*tmp*) funset_tabulate_cloref {n}(n, fopr) = let // implement $FS.funset_tabulate$fopr(i) = fopr($UN.cast{natLt(n)}(i)) // in $FS.funset_tabulate (n) end // end of [funset_tabulate] (* ****** ****** *) // implement {a}(*tmp*) funset_listize (xs) = ( // $effmask_wrt ( list0_of_list_vt{a}($FS.funset_listize(xs)) ) (* $effmask_wrt *) // ) (* funset_listize *) // (* ****** ****** *) // implement {a}(*tmp*) funset_streamize (xs) = $effmask_wrt($FS.funset_streamize(xs)) // (* ****** ****** *) // implement {a}(*tmp*) funset_make_module ((*void*)) = $rec { // nil = funset_nil{a} , sing = funset_sing , make_list = funset_make_list , size = funset_size , is_nil = funset_is_nil{a} , isnot_nil = funset_isnot_nil{a} , insert= funset_insert , remove= funset_remove , union= funset_union , intersect= funset_intersect , listize = funset_listize , streamize = funset_streamize // } (* end of [funset_make_module] *) // (* ****** ****** *) (* end of [funset.dats] *) (***********************************************************************) (* *) (* Applied Type System *) (* *) (***********************************************************************) (* ** ATS/Postiats - Unleashing the Potential of Types! ** Copyright (C) 2010-2013 Hongwei Xi, ATS Trustful Software, Inc. ** All rights reserved ** ** ATS is free software; you can redistribute it and/or modify it under ** the terms of the GNU GENERAL PUBLIC LICENSE (GPL) as published by the ** Free Software Foundation; either version 3, or (at your option) any ** later version. ** ** ATS is distributed in the hope that it will be useful, but WITHOUT ANY ** WARRANTY; without even the implied warranty of MERCHANTABILITY or ** FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License ** for more details. ** ** You should have received a copy of the GNU General Public License ** along with ATS; see the file COPYING. If not, please write to the ** Free Software Foundation, 51 Franklin Street, Fifth Floor, Boston, MA ** 02110-1301, USA. *) (* ****** ****** *) (* Author: Hongwei Xi *) (* Authoremail: gmhwxiATgmailDOTcom *) (* Start time: August, 2013 *) (* ****** ****** *) staload UN = "prelude/SATS/unsafe.sats" (* ****** ****** *) // staload HT = "libats/SATS/hashtbl_chain.sats" // (* ****** ****** *) staload "libats/ML/SATS/basis.sats" (* ****** ****** *) staload "libats/ML/SATS/list0.sats" (* ****** ****** *) staload "libats/SATS/hashfun.sats" staload "libats/ML/SATS/hashtblref.sats" (* ****** ****** *) (* implement {key}(*tmp*) hash_key = ghash_val *) (* ****** ****** *) implement {key}(*tmp*) equal_key_key = gequal_val_val (* ****** ****** *) // implement hash_key (key) = let val key = $UN.cast{uint32}(key) in $UN.cast{ulint}(inthash_jenkins<>(key)) end // end of [hash_key] // implement hash_key (key) = let val key = $UN.cast{uint32}(key) in $UN.cast{ulint}(inthash_jenkins<>(key)) end // end of [hash_key] // (* ****** ****** *) // // HX: 31 and 37 are top choices // implement hash_key (key) = string_hash_multiplier (31UL, 31415926536UL, key) // (* ****** ****** *) // implement {key}(*tmp*) $HT.hash_key = hash_key // implement {key}(*tmp*) $HT.equal_key_key = equal_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(cap) ) (* end of [htencode] *) // (* ****** ****** *) implement {}(*tmp*) hashtbl_get_size (tbl) = nitm where { // val tbl = htdecode(tbl) val nitm = $HT.hashtbl_get_size<>(tbl) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_get_size] *) (* ****** ****** *) implement {}(*tmp*) hashtbl_get_capacity (tbl) = cap where { // val tbl = htdecode(tbl) val cap = $HT.hashtbl_get_capacity<>(tbl) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_get_capacity] *) (* ****** ****** *) implement {key,itm} hashtbl_search (tbl, k) = opt where { // val tbl = htdecode(tbl) val opt = $HT.hashtbl_search_opt(tbl, k) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_search] *) (* ****** ****** *) implement {key,itm} hashtbl_search_ref (tbl, k) = cptr where { // val tbl = htdecode(tbl) // val cptr = $HT.hashtbl_search_ref(tbl, k) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_search_ref] *) (* ****** ****** *) implement {key,itm} hashtbl_insert (tbl, k, x) = opt where { // val tbl = htdecode(tbl) // val opt = $HT.hashtbl_insert_opt(tbl, k, x) // prval () = $UN.cast2void (tbl) // } (* hashtbl_insert *) (* ****** ****** *) implement {key,itm} hashtbl_insert_any (tbl, k, x) = () where { // val tbl = htdecode(tbl) // val () = $HT.hashtbl_insert_any(tbl, k, x) // prval () = $UN.cast2void (tbl) // } (* hashtbl_insert_any *) (* ****** ****** *) implement {key,itm} hashtbl_takeout (tbl, k) = opt where { // val tbl = htdecode(tbl) // val opt = $HT.hashtbl_takeout_opt(tbl, k) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_takeout] *) (* ****** ****** *) implement {key,itm} hashtbl_remove (tbl, k) = ans where { // val tbl = htdecode(tbl) val ans = $HT.hashtbl_remove(tbl, k) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_remove] *) (* ****** ****** *) implement {key,itm} hashtbl_takeout_all (tbl) = kxs where { // val tbl = htdecode(tbl) val kxs = $HT.hashtbl_takeout_all(tbl) val kxs = list0_of_list_vt{(key,itm)}(kxs) // prval () = $UN.cast2void(tbl) // } (* end of [hashtbl_takeout_all] *) (* ****** ****** *) implement {key,itm} fprint_hashtbl (out, tbl) = let // implement $HT.fprint_hashtbl$sep<> = fprint_hashtbl$sep<> implement $HT.fprint_hashtbl$mapto<> = fprint_hashtbl$mapto<> // val tbl = htdecode (tbl) val () = $HT.fprint_hashtbl (out, tbl) prval () = $UN.cast2void (tbl) // in // nothing end // end of [fprint_hashtbl] (* ****** ****** *) // implement{} fprint_hashtbl$sep(out) = fprint(out, "; ") implement{} fprint_hashtbl$mapto(out) = fprint(out, "->") // (* ****** ****** *) implement {key,itm} fprint_hashtbl_sep_mapto (out, tbl, sep, mapto) = let // implement fprint_hashtbl$sep<>(out) = fprint(out, sep) implement fprint_hashtbl$mapto<>(out) = fprint(out, mapto) // in fprint_hashtbl(out, tbl) end // end of [fprint_hashtbl_sep_mapto] (* ****** ****** *) implement {key,itm} hashtbl_foreach_cloref (tbl, fwork) = () where { // var env: void = ((*void*)) // implement (env)(*tmp*) $HT.hashtbl_foreach$fwork (k, x, env) = fwork(k, x) // val tbl = htdecode(tbl) // val ((*void*)) = $HT.hashtbl_foreach_env (tbl, env) // prval ((*returned*)) = $UN.cast2void(tbl) // } (* end of [hashtbl_foreach_cloref] *) (* ****** ****** *) // implement {key,itm} hashtbl_listize0 (tbl) = ( hashtbl_takeout_all(tbl) ) // (* ****** ****** *) implement {key,itm} hashtbl_listize1 (tbl) = kxs where { // typedef ki = @(key, itm) // val tbl = htdecode(tbl) // val kxs = $HT.hashtbl_listize1(tbl) // prval ((*returned*)) = $UN.cast2void(tbl) // val kxs = list0_of_list_vt{(key,itm)}(kxs) // } (* end of [hashtbl_listize1] *) (* ****** ****** *) (* end of [hashtblref.dats] *) (* end of [ATSLIB_ML_all_in_one.raw] *)