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.
  • option0
  • option0_of_option
  • option0_of_option_vt
  • g0ofg1_option
  • g1ofg0_option
  • option0_none
  • option0_some
  • option0_is_none
  • option0_is_some
  • option0_unsome_exn
  • option0_map
  • Overloaded Symbols
  • g0ofg1
  • g1ofg0
  • iseqz
  • isneqz
  • fprint

  • option0

    Synopsis

    The full name of the option0-type constructor is option0_t0ype_type, which is given to the datatype declared as follows:
    datatype // t@ype+: covariant
    option0_t0ype_type
      (a: t@ype+) = Some0 of (a) | None0 of ()
    // end of [option0_t0ype_type]
    

    option0_of_option

    Synopsis

    castfn
    option0_of_option
      {a:t@ype} (xs: Option a):<> option0 (a)

    Description

    This function casts an option-value of indexed type to an option-value of unindexed type.

    option0_of_option_vt

    Synopsis

    castfn
    option0_of_option_vt
      {a:t@ype} (xs: Option_vt a):<> option0 (a)

    Description

    This function casts a linear option-value of indexed type to an option-value of unindexed type.

    g0ofg1_option

    Synopsis

    castfn
    g0ofg1_option {a:t@ype} (xs: Option (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.

    g1ofg0_option

    Synopsis

    castfn
    g1ofg0_option {a:t@ype} (xs: option0 (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.

    option0_none

    Synopsis

    fun{
    } option0_none
      {a:t0p} ((*void*)):<> option0 (a)

    Description

    This is just the function version of the constructor None0.

    option0_some

    Synopsis

    fun{
    a:t0p
    } option0_some (x: a):<> option0 (a)

    Description

    This is just the function version of the constructor Some0.

    option0_is_none

    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.

    option0_is_some

    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.

    option0_unsome_exn

    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).

    option0_map

    Synopsis

    fun{
    a:t0p}{b:t0p
    } option0_map
    (
      opt: option0(INV(a)), fopr: cfun(a, b)
    ) : option0(b) // end of [option0_map]

    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().

    Overloaded Symbols


    g0ofg1

    Synopsis

    overload g0ofg1 with g0ofg1_option

    g1ofg0

    Synopsis

    overload g1ofg0 with g1ofg0_option

    iseqz

    Synopsis

    overload iseqz with option0_is_none

    isneqz

    Synopsis

    overload isneqz with option0_is_some

    fprint

    Synopsis

    overload fprint with fprint_option0

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