#include "share/atspre_staload.hats"
staload "libats/ML/SATS/basis.sats"
staload UN = "prelude/SATS/unsafe.sats"
staload "libats/SATS/qlist.sats"
staload "libats/DATS/qlist.dats"
(* ****** ****** ****** *)
sortdef
fvtype = vt0ype -> vtype
absprop
FUNCTOR(f_name: type, f: fvtype)
dataprop
EQ_fvtype(f: fvtype, f: fvtype) = {f: fvtype} Eq_fvtype(f, f)
extern fun{f_name: type}{a, b: vt0ype}
functor_map
{f: fvtype}
(FUNCTOR(f_name, f)| cfun(a, b)): cfun(f(a), f(b))
(* ****** ****** ****** *)
absprop
MONAD(m_name: type, m: fvtype)
extern fun{m_name: type}{a: vt0ype}
monad_return
{m: fvtype}
(MONAD(m_name, m)| a): m(a)
extern fun{m_name: type}{a, b: vt0ype}
monad_bind
{m: fvtype}
(MONAD(m_name, m)| m(a), cfun(a, m(b))): m(b)
praxi{m_name: type}
believe_me_this_is_the_monad
{m: fvtype}.<m>.(): MONAD(m_name, m) =
$UN.proof_assert{MONAD(m_name, m)}()
extern praxi{t_name: type}
monad_is_functor
{t: fvtype}
(MONAD(t_name, t)): FUNCTOR(t_name, t)
(* ****** ****** ****** *)
extern fun{a, s: vt0ype}
mapM_list_vt$fopr(a): s // [s = m(b)] in implementation!
fun{m_name: type}{a, b: vt0ype}
mapM_list_vt$aux
{m: fvtype}
{n: int}
( pfm: MONAD(m_name, m)
| xs: list_vt(INV(a), n) ):
m(list_vt(b, n)) =
let
prval () = lemma_list_vt_param(xs)
fun loop
{m: fvtype}
{n: nat}.<n>.
{k: nat}
( pfm: MONAD(m_name, m)
| xs: list_vt(a, n)
, acc: qlist(INV(b), k) ):
m(list_vt(b, k+n)) =
case xs of
| ~list_vt_nil() => let
val ys = qlist_takeout_list{b}{k}(acc) // takeout is O(1)
in qlist_free_nil{b}(acc)
; monad_return<m_name><list_vt(b, k+n)>(pfm| ys) end
| ~list_vt_cons(x, xs1) => let
val fx = mapM_list_vt$fopr<a, m(b)>(x)
val xs1 = $UN.castvwtp0{ptr}(xs1)
val acc = $UN.castvwtp0{ptr}(acc)
in monad_bind<m_name><b, list_vt(b, k+n)>
( pfm
| fx
, lam(y: b) => let
val xs1 = $UN.castvwtp0{list_vt(a, n-1)}(xs1)
val acc = $UN.castvwtp0{qlist(b, k)}(acc)
in qlist_insert<b>{k}(acc, y)
; loop(pfm| xs1, acc) end ) end
val acc = qlist_make_nil{b}()
in
loop{m}{n}(pfm| xs, acc)
end
fun{m_name: type}{a, b: vt0ype}
mapM_list_vt_fun
{m: fvtype}
{n: int}
( pfm: MONAD(m_name, m)
| xs: list_vt(INV(a), n)
, fopr: a -<fun1> m(b) ):
m(list_vt(b, n)) =
let implement mapM_list_vt$fopr<a, m(b)>(x) = fopr(x)
in mapM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs) end
fun{m_name: type}{a, b: vt0ype}
mapM_list_vt_cloref
{m: fvtype}
{n: int}
( pfm: MONAD(m_name, m)
| xs: list_vt(INV(a), n)
, fopr: a -<cloref1> m(b) ):
m(list_vt(b, n)) =
let implement mapM_list_vt$fopr<a, m(b)>(x) = fopr(x)
in mapM_list_vt$aux<m_name><a, b>{m}{n}(pfm| xs) end
(* ****** ****** ****** *)
abstype
Option_vt_name
prval pfoptm = believe_me_this_is_the_monad<Option_vt_name>{Option_vt}()
extern praxi
MONAD_Option_vt_elim
{m: fvtype}
(pfm: MONAD(Option_vt_name, m)): EQ_fvtype(Option_vt, m)
implement(a: vt0ype)
monad_return<Option_vt_name><a>(pfm| x) = let
prval Eq_fvtype() = MONAD_Option_vt_elim(pfm)
in Some_vt(x) end
implement(a, b: vt0ype)
monad_bind<Option_vt_name><a, b>(pfm| x_opt, fopr) = let
prval Eq_fvtype() = MONAD_Option_vt_elim(pfm)
in case x_opt of
| ~Some_vt(x) => fopr(x)
| ~None_vt() => None_vt()
end
implement
main0() = let
datavtype I_dvt(a: t0p) = I of a
vtypedef int_vt = I_dvt(int)
val xs: list_vt(int_vt, 3) = $list_vt(I(1), I(2), I(3))
val xsopt: Option_vt(list_vt(int_vt, 3)) =
mapM_list_vt_fun
( pfoptm
| xs
, lam(x) => monad_return<Option_vt_name><int_vt>(pfoptm| x) )
val- ~Some_vt(xs) = xsopt
fun printout{n: int}(ks: list_vt(int_vt, n)): void =
case ks of
| ~list_vt_nil() => ()
| ~list_vt_cons(k, ks1) => let val- ~I(k) = k
in (println!(k); printout(ks1)) end
in
printout{3}(xs)
end
// Will not compile! =(
