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_some
  • option_vt_none
  • option_vt_is_some
  • option_vt_is_none
  • option_vt_unsome
  • option_vt_unnone
  • option_vt_make_opt
  • option_vt_free
  • Overloaded Symbols
  • fprint

  • 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) // endfun

    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. SourceForge.net Logo