%{^ #include <stdio.h> void* resource_new(); void resource_free(void* r); void do_something(void (*f)(void* r), void* arg); void resource_use(void* r); %} %{ void* resource_new() { return ATS_MALLOC(10); } void resource_use(void* r) { printf("using: %p\n", r); } void resource_free(void* r) { ATS_FREE(r); } void do_something(void (*f)(void*), void* arg) { printf("a\n"); f(arg); printf("b\n"); } %} absviewtype resource (l:addr) viewtypedef resource1 = [l:addr | l > null] resource l extern fun resource_isnot_null {l:addr} (p: !resource l):<> bool (l > null) = "atspre_ptr_isnot_null" overload ~ with resource_isnot_null extern fun resource_new():resource1 = "mac#resource_new" extern fun resource_use(r: !resource1):void = "mac#resource_use" extern fun resource_free(r: resource1):void = "mac#resource_free" viewtypedef env (l1:addr) = @{r1= resource l1, r2= Option_vt (resource1)} viewtypedef env = [l1:agz] env(l1) typedef callback = (&env) -<fun1> void extern fun do_something(f: callback, arg: &env):void = "mac#do_something" fun mycallback (e: &env): void = let val () = resource_use(e.r1); val () = case+ e.r2 of | ~Some_vt(x) => let val () = resource_use(x); val () = resource_free(x); val () = e.r2 := None_vt in () end | ~None_vt () => let val () = e.r2 := None_vt in () end in () end implement main() = let var env: env(null) val () = env.r1 := resource_new(); val () = env.r2 := Some_vt (resource_new()); val () = do_something(mycallback, env) val () = resource_free(env.r1); val () = case+ env.r2 of | ~Some_vt (x) => resource_free(x) | ~None_vt () => () in () end