OK, I'm making gradual progress on this. This is the next bit of code:
extern praxi vector_v_to_b0ytes_v{a:vt0p}{l:agz}{n:nat}
( vector_v(a, l, n) ): b0ytes_v(l, n * sizeof(a))
fun imul{n,m:int}(n: int(n), m: int(m)): (MUL(n, m, n*m) | int(n*m)) =
(mul_make{n,m}() | n*m)
fun{a:vt0p}
make_vector_vt{n:nat}(
n: int(n)
): [l:addr] option_vt(vector_vt(a?, l, n), l > null) = let
val (pf | sz) = imul(n, sz2i(sizeof<a>))
prval () = mul_nat_nat_nat(pf) // $UN.prop_assert{n * sizeof(a) >= 0}()
val [l:addr] (pfopt | p) = malloc_libc{n * sizeof(a)}(i2sz(sz))
in
case+ pfopt of
| malloc_libc_v_succ(pfbytes, pfmfree) =>
option_vt_some(vector_vt(pfmfree,
b0ytes_v_to_vector_v{a}{l}{n}(pfbytes) | p))
| malloc_libc_v_fail() =>
option_vt_none()
end
fun{a:vt0p}
free_vector_vt {l:agz}{n:int}
(
v: vector_vt(a, l, n)
): void = let
val ~vector_vt (pmfree, pfv_v | p) = v // notice the errors that are
produced if we omit ~!
prval pfBytes = vector_v_to_b0ytes_v(pfv_v)
in
mfree_libc(pfBytes, pmfree | p)
end
free_vector_vt seems to pass the typechecker, but make_vector_vt does not.
I don't know how to prove
that l > null is false in the malloc_libc_v_fail case.
--
You received this message because you are subscribed to the Google Groups
"ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To post to this group, send email to [email protected].
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/dca64a29-e014-4901-9173-25763452c7e8%40googlegroups.com.
