If I remember correctly the node that is freed is based on the second static
argument provided ( in this case, the 0 in ‘free@{a}{0}(xs)’ )
On Sunday, February 10, 2019 at 6:17:03 PM UTC-5, [email protected] wrote:
> Hi all,
>
>
> I'm facing some difficulty understanding how `free@' is used. I'm going
> through the Introduction to Programming in ATS book, and the example I'm
> facing trouble with is this,
>
>
>
>
> fun{
> a:t@ype
> } list_vt_free
> {n:nat}.<n>. (xs: list_vt (a, n)): void =
> case+ xs of
> | @list_vt_cons(x, xs1) => let
> val xs1_ = xs1
> val () = free@{a}{0}(xs) in list_vt_free (xs1_)
> end
> | @list_vt_nil () => free@{a} (xs)
> Why is it `free@{a}{0} (xs)' and not `free@{a}{0} (x)'? It seems that `free@'
> requires an unfolded constructor (here, it is operating on
> `list_vt_cons_unfold'). However, that begs the question -- how does `free@'
> know to free only the first node of the list and not the rest of the list?
> Any help understanding this will be much appreciated!
>
>
> Thanks,
> Ramana
--
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/7ad6f308-def1-48e1-87aa-22c352f932d6%40googlegroups.com.