A list node contains two cells: one holding the content and the other
holding
the pointer to the next node (or null).
When xs matches the pattern @list_vt_cons(x, xs1), xs refers to a list node;
x refers to the content cell and xs1 refers to the pointer cell. In this
case, the
content is non-linear (a:t@ype) and thus does not need to be moved out. But
the pointer needs to be moved out before xs can be freed:
val xs1_ = xs
The above code was written long time ago. It could be prettified a bit as
follows:
fun
{a:t@ype}
list_vt_free
{n:nat} .<n>.
(xs: list_vt(a, n)): void =
(
case+ xs of
| ~list_vt_nil() => ()
| @list_vt_cons(_, xs1) =>
let
val xs1 = xs1
in
free@{a}{0}(xs); list_vt_free<a>(xs1)
end
)
People are often puzzled by a beautiful line like 'val xs1 = xs1' :)
On Sunday, February 10, 2019 at 6:17:03 PM UTC-5, rnagasam 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/e02a34b7-8150-482a-9f9b-93b89e063042%40googlegroups.com.
