#include "share/atspre_staload.hats"
#staload "libats/ML/SATS/basis.sats" // Not allowed on glot.io!
#staload UN = "prelude/SATS/unsafe.sats"
#staload "libats/SATS/qlist.sats"
#staload "libats/DATS/qlist.dats"
(* ****** ****** ****** *)
sortdef fvtype = vt0ype -> vtype
abstype MONAD(fvtype) = ptr
extern fun{m: fvtype}{a: vt0ype}
monad_return
(MONAD(m)| a): m(a)
extern fun{m: fvtype}{a, b: vt0ype}
monad_bind
(MONAD(m)| m(a), cfun(a, m(b))): m(b)
extern prfun // 0_0
believe_me_this_is_a_monad{m: fvtype}(): MONAD(m)
(* ****** ****** ****** *)
extern fun{m: fvtype}{a, b: vt0ype}
mapM_list_vt$fopr(a): m(b)
fun{m: fvtype}{a, b: vt0ype}
mapM_list_vt$aux
{n: int}
( pfm: MONAD(m)
| xs: list_vt(INV(a), n) ):
m(list_vt(b, n)) =
let
prval () = lemma_list_vt_param(xs)
fun loop
{n: nat}.<n>.
{k: nat}
( pfm: MONAD(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><list_vt(b, k+n)>(pfm| ys) end
| ~list_vt_cons(x, xs1) => let
val fx = mapM_list_vt$fopr<m><a, b>(x)
val xs1 = $UN.castvwtp0{ptr}(xs1)
val acc = $UN.castvwtp0{ptr}(acc)
in monad_bind<m><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(pfm| xs, acc)
end
fun{m: fvtype}{a, b: vt0ype}
mapM_list_vt_fun
{n: int}
( pfm: MONAD(m)
| xs: list_vt(INV(a), n)
, fopr: a -<fun1> m(b) ):
m(list_vt(b, n)) = let
implement mapM_list_vt$fopr<m><a, b>(x) = fopr(x)
in mapM_list_vt$aux<m><a, b>(pfm| xs) end
fun{m: fvtype}{a, b: vt0ype}
mapM_list_vt_cloref
{n: int}
( pfm: MONAD(m)
| xs: list_vt(INV(a), n)
, fopr: a -<cloref1> m(b) ):
m(list_vt(b, n)) = let
implement mapM_list_vt$fopr<m><a, b>(x) = fopr(x)
in mapM_list_vt$aux<m><a, b>(pfm| xs) end
(* ****** ****** ****** *)
implement(a: vt0ype)
monad_return<Option_vt><a>(pfm| x) = Some_vt(x)
implement(a, b: vt0ype)
monad_bind<Option_vt><a, b>
(pfm| x_opt, fopr) = case x_opt of
| ~Some_vt(x) => fopr(x)
| ~None_vt() => None_vt()
prval pfm = believe_me_this_is_a_monad{Option_vt}()
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(pfm| xs, lam(x) => monad_return(pfm| 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
*) // Example test will not compile! =(
