The following code would not work (even if it could pass typechecking):
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()
Note that pfopt is a proof value, which is erased after typechecking. The
proper way
to do this is doing something like:
if
p > the_null_ptr
then let
prval malloc_libc_v_succ(pf) = pfopt
in
...
end
else let
prval malloc_libc_v_fail() = pfopt
in
...
end
I would like to point out that it is very difficult to code like what you
are doing (which I did
in the past). These days I mostly try to use the type system of ATS to do
what I call 'static debugging':
http://ats-lang.sourceforge.net/DOCUMENT/INT2PROGINATS/HTML/HTMLTOC/x4387.html
On Mon, Mar 11, 2019 at 8:21 PM Mark Thom <[email protected]> wrote:
>
> 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
> <https://groups.google.com/d/msgid/ats-lang-users/dca64a29-e014-4901-9173-25763452c7e8%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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/CAPPSPLrKzv-uRmSPCeUPNBMUegjTdJPtS99OdH3Wpoyu6PKC-Q%40mail.gmail.com.
