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
  • NotSomeExn
  • option_cast
  • option_vt2t
  • option_of_option_vt
  • option_some
  • option_none
  • option_is_some
  • option_is_none
  • option_unsome
  • option_unsome_exn
  • Overloaded Symbols
  • fprint

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