ATSLIB/libats/ML/option0
The functions declared in this package are primarily for supporting
ML-style processing of option-values. The programmer is encouraged to use
the dependent datatype option instead of option0
after gaining some familiarity with dependent types.
Synopsis
The full name of the option0-type constructor is
option0_t0ype_type, which is given to the datatype declared as
follows:
datatype
option0_t0ype_type
(a: t@ype+) = Some0 of (a) | None0 of ()
Synopsis
castfn
option0_of_option
{a:t@ype}
(xs: Option(INV(a))):<> option0(a)
Description
This function casts an option-value of indexed type to an option-value of
unindexed type.
Synopsis
castfn
option0_of_option_vt
{a:t@ype}
(xs: Option_vt(INV(a))):<> option0(a)
Description
This function casts a linear option-value of indexed type to an option-value of
unindexed type.
Synopsis
castfn
g0ofg1_option
{a:t@ype}
(xs: Option(INV(a))):<> option0(a)
Description
This function, which overloads the symbol g0ofg1, casts an
option-value of indexed type to another option-value of unindexed type.
Synopsis
castfn
g1ofg0_option
{a:t@ype}
(xs: option0(INV(a))):<> Option(a)
Description
This function, which overloads the symbol g1ofg0, casts an
option-value of unindexed type to another option-value of indexed type.
Synopsis
fun{}
option0_none
{a:t0p}():<> option0(a)
Description
This is just the function version of the constructor None0.
Synopsis
fun
{a:t0p}
option0_some(x0: a):<> option0(a)
Description
This is just the function version of the constructor Some0.
Synopsis
fun{}
option0_is_none
{a:t0p}(x: option0(a)):<> bool
Description
This funtion returns true if and only a given option-value is formed with
the constructor None0.
Synopsis
fun{}
option0_is_some
{a:t0p}(x: option0(a)):<> bool
Description
This funtion returns true if and only a given option-value is formed with
the constructor Some0.
Synopsis
fun{a:t0p}
option0_unsome_exn(opt: option0(a)):<!exn> a
Description
If a given option-value is of the form Some0(v), then
this function returns the value v. Otherwise, it raises an exception
(NotSomeExn).
Synopsis
fun{
a:t0p}{b:t0p
} option0_map
(
opt: option0(INV(a)), fopr: cfun(a, b)
) : option0(b)
Description
Given an option-value opt and a function f, this function returns
Some0(f(v)) if opt is of the form
Some0(v). Otherwise, it returns None0().
Synopsis
overload g0ofg1 with g0ofg1_option
Synopsis
overload g1ofg0 with g1ofg0_option
Synopsis
overload iseqz with option0_is_none
Synopsis
overload isneqz with option0_is_some
Synopsis
overload fprint with fprint_option0