Leak my coroutine

hello,
I cannot find out why this code does not work.

#include “share/atspre_staload_tmpdef.hats”

staload UN = “prelude/SATS/unsafe.sats”

staload _(anonymous) = "prelude/DATS/list.dats"
staload _(anonymous) = “prelude/DATS/list_vt.dats”

vtypedef lcfun1 (a:vt0p, b:vt0p) = (a) -<lin,cloptr1> b

// automaton signature
absvtype automaton_vt (inp: vt0p, out: vt0p) = ptr

extern castfn automaton_of_linc {a, b: vt0p}
(cf: lcfun1 (a, @(b, automaton_vt (a, b)))):<> automaton_vt (a, b)

extern castfn linc_of_automaton {a, b:vt0p}
(au: automaton_vt (a, b)):<> lcfun1 (a, @(b, automaton_vt (a, b)))

extern fun{a,b: vt0p} au_run(au: automaton_vt(a, b), x: a): (b,automaton_vt(
a,b))
extern fun{a,b: vt0p} au_run_seq{n: nat} (au: automaton_vt(a, b), seq:list_vt
(a, n)): list_vt(b, n)

extern fun print_free_list{n: nat} (l: list_vt(int, n)): void

// automaton implementation
implement{a,b} au_run(au, x) = res where {
val f = linc_of_automaton{a, b}(au)
val res = f x
val () = cloptr_free ($UN.castvwtp0{cloptr0}(f))
}

implement{a,b} au_run_seq(au, seq) = case+ seq of
| ~list_vt_nil () => let
extern castfn __leak {v:view} (pf: v):<> void
val () = __leak(au) // !!!
in
list_vt_nil{b} ()
end
| ~list_vt_cons (x, xs) => let
val (res, au’) = au_run<a, b>(au, x)
in
list_vt_cons{b} (res, au_run_seq(au’, xs))
end

implement print_free_list(l) = let
fun print_free_list_aux{n: nat} (l: list_vt(int,n)): void = case+ l of
| ~list_vt_nil () => ()
| ~list_vt_cons (x, xs) => let
val () = print! (" ", x)
val () = print_free_list_aux xs
in end
val () = print_free_list_aux l
in print_newline () end

extern fun ints_from (x: int): automaton_vt (unit, int)
implement ints_from(x) = automaton_of_linc{unit,int}(llam _ = (x,ints_from
(x+1)))

implement main0(argc, argv) = let
extern castfn __leak {v:view} (pf: v):<> void

val au = ints_from 10

val (x0, au1) = au_run<unit, int>(au, unit) //
val () = __leak(au1) // <- this
fails here

//val l = au_run_seq<unit, int>( au, $list_vt{unit}(unit)) // <- this
works
//val () = print_free_list(l) // <- this
works

in end

the compiler complains :

@ patscc -DATS_MEMALLOC_LIBC -o test_coroutine test_coroutine.dats
exec(patsopt --output test_coroutine_dats.c --dynamic test_coroutine.dats)
Hello from ATS/Postiats!
Loading [fixity.ats] starts!
Loading [fixity.ats] finishes!
Loading [basics_pre.sats] starts!
Loading [basics_pre.sats] finishes!
Loading [basics_sta.sats] starts!
Loading [basics_sta.sats] finishes!
Loading [basics_dyn.sats] starts!
Loading [basics_dyn.sats] finishes!
Loading [basics_gen.sats] starts!
Loading [basics_gen.sats] finishes!
The 1st translation (fixity) of [test_coroutine.dats] is successfully
completed!
The 2nd translation (binding) of [test_coroutine.dats] is successfully
completed!
The 3rd translation (type-checking) of [test_coroutine.dats] issuccessfully completed
!
The 4th translation (type/proof-erasing) of [test_coroutine.dats] issuccessfully completed
!
exec(patsopt --output test_coroutine_dats.c --dynamic test_coroutine.dats) =
0
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime
-L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64 -DATS_MEMALLOC_LIBC
-o test_coroutine test_coroutine_dats.c)
test_coroutine_dats.c: In function ‘mainats_argc_argv_0’:
test_coroutine_dats.c:883: error: expected expression before ‘)’ token
exec(gcc -std=c99 -D_XOPEN_SOURCE -I${PATSHOME} -I${PATSHOME}/ccomp/runtime
-L${PATSHOME}/ccomp/atslib/lib -L${PATSHOME}/ccomp/atslib/lib64 -DATS_MEMALLOC_LIBC
-o test_coroutine test_coroutine_dats.c) = 256

He cannot bear my __leak trick but when I use the au_run_seq method, it
compiles and runs fine !
Any clue ?

Thanks a lot

right !

thanks :wink:

‘leak’ should be declared as a proof function (instead of a castfn):

praxi __leak …

Then you do

prval () = __leak (…)

It should work.

By the way, you can also use the proof function declared
in unsafe.sats:

praxi castview0 {to:view}{from:view} (pf: from): to

Just do

staload
UN = “prelude/SATS/unsafe.sats”

prval () = $UN.castview0{void}(pf)