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

`overload fprint with fprint_option_vt`