This package implements linear sets based on ordered lists. Note that this implementation should only be used for handling sets that are relatively small (e.g., containing less than 100 elements).
vtypedef set (a:t0p) = set_vtype (a)
absvtype set_vtype (a:t@ype+) = ptr
fun{a:t0p}
compare_elt_elt (x1: a, x2: a):<> int
fun{} linset_nil{a:t0p} ():<> set(a)
fun{} linset_make_nil{a:t0p} ():<> set(a)
fun{a:t0p} linset_sing (x: a):<!wrt> set(a)
fun{a:t0p} linset_make_sing (x: a):<!wrt> set(a)
fun{a:t0p}
linset_make_list (xs: List(INV(a))):<!wrt> set(a)
fun{a:t0p}
linset_insert
(xs: &set(INV(a)) >> _, x0: a):<!wrt> bool
fun{a:t0p} linset_takeout ( &set(INV(a)) >> _, a, res: &(a?) >> opt(a, b) ) :<!wrt> #[b:bool] bool(b) // endfun
fun{a:t0p}
linset_takeout_opt (&set(INV(a)) >> _, a):<!wrt> Option_vt(a)
fun{a:t0p}
linset_remove
(xs: &set(INV(a)) >> _, x0: a):<!wrt> bool
Synopsis for [linset_getmax] is unavailable.
Synopsis for [linset_getmax_opt] is unavailable.
Synopsis for [linset_getmin] is unavailable.
Synopsis for [linset_getmin_opt] is unavailable.
fun{a:t0p}
linset_takeoutmax
(
xs: &set(INV(a)) >> _, res: &a? >> opt(a, b)
) :<!wrt> #[b:bool] bool (b)
fun{a:t0p}
linset_takeoutmax_opt (xs: &set(INV(a)) >> _):<!wrt> Option_vt(a)
fun{a:t0p}
linset_takeoutmin
(
xs: &set(INV(a)) >> _, res: &a? >> opt(a, b)
) :<!wrt> #[b:bool] bool (b)
fun{a:t0p}
linset_takeoutmin_opt (xs: &set(INV(a)) >> _):<!wrt> Option_vt(a)
fun{a:t0p}
linset_foreach (set: !set(INV(a))): void
fun{
a:t0p}{env:vt0p
} linset_foreach_env
(set: !set(INV(a)), env: &(env) >> _): void
fun{
a:t0p}{env:vt0p
} linset_foreach$fwork
(x: a, env: &(env) >> _): void
fun{a:t0p}
linset_listize (xs: set(INV(a))): List0_vt (a)
fun{a:t0p}
linset_listize1 (xs: !set(INV(a))): List0_vt (a)
absvtype
linset_node_vtype (a:t@ype+, l:addr) = ptr
stadef mynode = linset_node_vtype
vtypedef mynode (a:t0p) = [l:addr] mynode (a, l)
vtypedef mynode0 (a:t0p) = [l:addr | l >= null] mynode (a, l)
vtypedef mynode1 (a:t0p) = [l:addr | l > null] mynode (a, l)
fun{a:t0p} linset_insert_ngc ( set: &set(INV(a)) >> _, nx0: mynode1 (a) ) :<!wrt> mynode0 (a) // endfun
fun{a:t0p}
linset_takeout_ngc
(set: &set(INV(a)) >> _, x0: a):<!wrt> mynode0 (a)
fun{a:t0p}
linset_takeoutmax_ngc
(set: &set(INV(a)) >> _):<!wrt> mynode0 (a)
fun{a:t0p}
linset_takeoutmin_ngc
(set: &set(INV(a)) >> _):<!wrt> mynode0 (a)
| This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi. |
|