ATSLIB/prelude/option_vt

This package contains some common functions for processing linear option-values.

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

option_vt

Option_vt

option_vt

Synopsis

stadef option_vt = option_vt0ype_bool_vtype

Synopsis

The full name for the linear option-type constructor option_vt is option_viewt0ype_bool_viewtype, which is given to the linear datatype (dataviewtype) declared as follows:

dataviewtype // viewt@ype+: covariant
option_viewt0ype_bool_viewtype
  (a:viewt@ype+, bool) = Some_vt (a, true) of a | None_vt (a, false)
// end of [option_viewt0ype_bool_viewtype]

Description

There are two data constructors Some_vt and None_vt associated with option_vt; 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 linear option-values into a single one:

fun{
a1,a2:t0p
} option_vt_zip {b1,b2:bool} (
  opt1: option_vt (a1, b1), opt2: option_vt (a2, b2)
) : option_vt (@(a1, a2), b1*b2) =
  case+ opt1 of
  | ~Some_vt (x1) => (
    case+ opt2 of
    | ~Some_vt (x2) => Some_vt @(x1, x2) | ~None_vt () => None_vt ()
    )
  | ~None_vt () => let
      val () = option_vt_free (opt2) in None_vt ()
    end // end of [None_vt]
// end of [option_vt_zip]

Option_vt

Synopsis

vtypedef Option_vt (a:vt0p) = [b:bool] option_vt (a, b)

option_vt_some

Synopsis

fun{a:vt0p}
option_vt_some (x: a):<!wrt> option_vt (a, true)

Description

This is just the function version of the constructor Some_vt.

option_vt_none

Synopsis

fun{a:vt0p}
option_vt_none ((*void*)):<!wrt> option_vt (a, false)

Description

This is just the function version of the constructor None_vt.

option_vt_is_some

Synopsis

fun{}
option_vt_is_some
  {a:vt0p}{b:bool}
  (opt: !option_vt(INV(a), b)):<> bool(b)

Description

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

option_vt_is_none

Synopsis

fun{}
option_vt_is_none
  {a:vt0p}{b:bool}
  (opt: !option_vt(INV(a), b)):<> bool(~b)

Description

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

option_vt_unsome

Synopsis

fun
{a:vt0p}
option_vt_unsome
  (opt: option_vt(INV(a), true)):<!wrt> (a)

Description

This is just the inverse of option_vt_some.

option_vt_unnone

Synopsis

fun
{a:vt0p}
option_vt_unnone
  (opt: option_vt(INV(a), false)):<!wrt> void

Description

This is just the inverse of option_vt_none.

option_vt_make_opt

Synopsis

fun{
a:vt0p
} option_vt_make_opt
  {b:bool}
(
  b: bool(b)
, x: &opt (INV(a), b) >> a?
) :<!wrt> option_vt(a, b) // end-of-fun

Description

This function creates a linear option-value according to the optional content of a given variable.

option_vt_free

Synopsis

fun{a:t0p}
option_vt_free
  (opt: Option_vt(INV(a))):<!wrt> void

Description

This function frees the memory occupied by a linear option-value.

Overloaded Symbols

fprint

Synopsis

overload fprint with fprint_option_vt

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