ATS Option Type Example

#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")
            
}