ats

What is S2Etop(knd=0; …)? How do I get my proof value out of this top-level realm?

I am FFIing to a C lib whose initialization can return a null pointer for foo_init. I want to capture this invariance so I created these types in my *.sats.

absvt@ype foo
vtypedef foo_ptr = [l: agz] (foo @ l | ptr l)
vtypedef foo_opt_ptr = [l: addr] (option_v (foo? @ l, l > null) | ptr l)

After checking p > 0, I matched a value from prval Some(foo) = foo_opt. When trying to create the unoptional type like

(* … *)
val (pf_opt | p): foo_opt_ptr = foo_init(p_options)
if p > 0 then {
    prval Some_v(pf) = pf_opt
    // can type assert failure here too:
    // val x: {l: agz}(foo @ l) = pf
    val nc: foo_ptr = (pf | p)
    (* … *)
    val _ = foo_stop(foo_ptr) // frees foo_ptr
else
    prval None_v(pf) = pf_opt
    (* … *)
    val () = $raise FooFailedInit()
end

I get an error for the pf side of the tuple.

mismatch of static terms (tyleq):
The actual term is: S2Etop(knd=0; S2Ecst(foo_ptr))
The needed term is: S2Ecst(foo_ptr)

I can see my type is right there, but it appears wrapped & I don’t know how to get it. Some files appear to reference vtakeout0 which looks like it comes from prelude/basics_sta.sats but compiler seems to not know where it is.

Solution

  • I am not entirely sure what is going on with the ? postfix operator, but removing it works & allows me use prval to match out my value as expected.

     absvt@ype foo
 vtypedef foo_ptr = [l: agz] (foo @ l | ptr l)
-vtypedef foo_opt_ptr = [l: addr] (option_v (foo @ l?, l > null) | ptr l)
+vtypedef foo_opt_ptr = [l: addr] (option_v (foo @ l, l > null) | ptr l)