On Wednesday, April 12, 2017 at 5:16:50 AM UTC+6, August Alm wrote:
>
> I have a function that looks as follows:
>
> fun{}
> parallel_composition_aux
> {m1, n1, m2, n2: nat}
> (m1: int m1, p1: processor(m1, n1), p2: processor(m2, n2)):
> processor(m1+m2, n1+n2) =
> llam(ys) =<cloptr1>
> let val (xs1, xs2) = list_vt_split_at(ys, m1)
> val ys1 = ev(p1, xs1)
> val ys2 = ev(p2, xs2)
> in list_vt_append(ys1, ys2) end
>
> Nevermind what it does, it should not matter for my question. I would like
> to be able to remove [m1: int m1] from the list of input variables! But if
> I do, then
> [list_vt_split_at] does not recognize [m1]. Is there a fix? I gather this
> issue must
> be discussed somewhere in the documentation but I can't find it.
>
What if you put the [m1: int m1] inside of [processor], so it can be
queried at runtime?
I guess this is what HX is proposing to do.
Static terms are all erased, as are proof terms, so if you did:
fun{}
parallel_composition_aux
{m1, n1, m2, n2: nat}
(m1: int m1 | p1: processor(m1, n1), p2: processor(m2, n2)):
processor(m1+m2, n1+n2) = ...
Then it would basically get translated to:
fun{}
parallel_composition_aux
(p1: processor, p2: processor):
processor = ...
at runtime. I think HX published a paper where he goes into a lot of detail
on this erasure process.
--
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 ats-lang-users+unsubscr...@googlegroups.com.
To post to this group, send email to ats-lang-users@googlegroups.com.
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/970b4bf4-bbc5-4c6b-addc-cbd6dc3438ea%40googlegroups.com.
