#include "share/atspre_staload.hats"
staload "libats/ML/SATS/basis.sats"
(*
// dependent type
datatype option_t0ype_bool_type (a:t@ype+, bool) =
| Some (a, true) of a
| None (a, false) of ()
stadef option = option_t0ype_bool_type
typedef Option (a:t0p) = [b:bool] option (a, b)
*)
(*
// linear dependent type
dataviewtype option_viewt0ype_bool_viewtype (a:viewt@ype+, bool) =
| Some_vt (a, true) of a
| None_vt (a, false) of ()
stadef option_vt = option_vt0ype_bool_vtype
vtypedef Option_vt (a:vt0p) = [b:bool] option_vt (a, b)
*)
(*
// naive datatype
datatype option0_t0ype_type (a: t@ype+) =
| Some0 of (a)
| None0 of ()
stadef option0 = option0_t0ype_type
*)
implement main0 () = () where {
val some = (Some 1) : option (int, true)
val _ = case+ some of
| Some x => println! ("Some: ", x)
| None () => println! ("None")
val somevt = Some_vt 2 : option_vt (int, true)
val _ = case+ somevt of
| ~Some_vt x => println! ("SomeVt: ", x)
| ~None_vt () => println! ("NoneVt")
val some0 = Some0 3 : option0 (int)
val _ = case+ some0 of
| Some0 x => println! ("Some0: ", x)
| None0 () => println! ("None0")
}
