ATSLIB/prelude/option

This package contains some common functions for processing (functional) option-values.

Please see option.sats and option.dats for the SATS file and DATS file in ATSLIB where the functions in this package are declared and implemented, respectively.

option

Option

option

Synopsis

The full name for the option-type constructor option is option_t0ype_bool_type, which is given to the datatype declared as follows:

datatype // t@ype+: covariant
option_t0ype_bool_type
  (a:t@ype+, bool) = Some (a, true) of a | None (a, false)
// end of [datatype]

Description

There are two data constructors Some and None associated with option; the former constructs a null option-value while the latter takes an element x to construct a non-null option-value carrying x.

Example

The following code implements a function that combines two given option-values into a single one:

fun{
a1,a2:t@ype
} option_zip {b1,b2:bool} (
  opt1: option (a1, b1), opt2: option (a2, b2)
) : option (@(a1, a2), b1*b2) =
  case+ opt1 of
  | Some (x1) => (
    case+ opt2 of
    | Some (x2) => Some @(x1, x2) | None () => None ()
    )
  | None () => None ()
// end of [option_zip]

Option

Synopsis

typedef
Option (a:t0p) = [b:bool] option(a, b)

NotSomeExn

Synopsis

exception NotSomeExn of ()

Description

By convention, this exception is raised to indicate a situation where an option-value expected to be non-null is actually null.

option_cast

Synopsis

castfn
option_cast
  {a:t0p}{b:bool}
(
  opt: option(INV(a), b)
) :<> option(a, b) // end-of-fun

option_vt2t

Synopsis

castfn
option_vt2t
  {a:t0p}{b:bool}
(
  opt: option_vt(INV(a), b)
) :<> option(a, b) // end-of-fun

option_of_option_vt

Synopsis

castfn
option_of_option_vt
  {a:t0p}{b:bool}
(
  opt: option_vt(INV(a), b)
) :<> option(a, b) // end-of-fun

option_some

Synopsis

fun{a:t0p}
option_some
  (x0: a):<> option(a, true)

Description

This is just the function version of the constructor Some.

option_none

Synopsis

fun{a:t0p}
option_none
  ((*void*)):<> option(a, false)

Description

This is just the function version of the constructor None.

option_is_some

Synopsis

fun{}
option_is_some
  {a:t0p}{b:bool}
  (opt: option(a, b)):<> bool(b)

Description

This funtion returns true if and only a given option-value is formed with the constructor Some.

option_is_none

Synopsis

fun{}
option_is_none
  {a:t0p}{b:bool}
  (opt: option(a, b)):<> bool(~b)

Description

This funtion returns true if and only a given option-value is formed with the constructor None.

option_unsome

Synopsis

fun{a:t0p}
option_unsome
  (option(INV(a), true)):<> (a)

Description

This is just the inverse of option_some.

option_unsome_exn

Synopsis

fun{a:t0p}
option_unsome_exn
  (opt: Option(INV(a))):<!exn> (a)

Description

If a given option-value is of the form Some(v), then this function returns v. Otherwise, it raises an exception (NotSomeExn).

Overloaded Symbols

fprint

Synopsis

overload fprint with fprint_option of 0

This page is created with ATS by Hongwei Xi and also maintained by Hongwei Xi.