using static quantifiers as dynamical terms

[August Alm]

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.

[Hongwei Xi]

If you do that, you need a function that allows you to

compute the value of m1 based on p1 (of the type processor(m1, n1)).

There is really no other way to get the dynamic m1 if you do pass it

directly.

In 'm1: int(m1)', the first m1 is dynamic and the second one is static.

They live in different worlds. The m1 as the 2nd argument of list_vt_split_at

is a dynamic one.

--
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+unsubscribe@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/8a304e17-6c94-4392-a655-06ada53e0fbf%40googlegroups.com.

[Artyom Shalkhakov]

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.

[August Alm]

Thanks! I like this solution.

[August Alm]

Hrrm, I'm getting a compilation error that I don't understand. With the methodology you
suggested I now have the function:

         fun{}
         parallel_composition

         {m1, n1, m2, n2: nat}

         (p1: processor(m1, n1), p2: processor(m2, n2)):
         processor(m1+m2, n1+n2) =
           (m, n| f)
           where
             val (a1, b1| f1) = p1
             val (a2, b2| f2) = p2
             val m = a1 + a2
             val n = b1 + b2
             val f = llam(xs: signals(m1+m2)): signals(n1+n2) =<cloptr1>
               let val (xs1, xs2) = list_vt_split_at(xs, a1)
                   val ys1 = ev(f1, xs1)
                   val ys2 = ev(f2, xs2)
               in list_vt_append(ys1, ys2) end
           end

(Ordinarily I'd use the same letter for static and dynamic versions of the "same" integer but
in the above I've not done so, to ease discussion.) The function typechecks but during
compilation I get:

"warning: implicit declaration of function ‘PMVerr’ [-Wimplicit-function-declaration]
ATSINSmove(tmp2__1, atspre_g1int_add_int(PMVerr("/home/august/....
faust_dats.c:(.text+0x33d): undefined reference to `PMVerr' ...

The error is caused by [val m = a1+a2] and [val n = b1 + b2]. I've tried [g0ofg1] and [g1ofg0]
to ensure the types really match but, no luck. Any ideas?

Best wishes,
August

Den onsdag 12 april 2017 kl. 05:26:15 UTC+2 skrev Artyom Shalkhakov:

[gmh...@gmail.com]

a1,b1 are proofs. They are erased after typechecking. But m is not a proof.

Sent from my T-Mobile 4G LTE device

------ Original message------

From: August Alm

Date: Wed, Apr 12, 2017 12:43 PM

To: ats-lang-users;

Subject:Re: using static quantifiers as dynamical terms

--

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-user...@googlegroups.com.
To post to this group, send email to ats-lan...@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/230dcd49-80a8-4d2f-86a7-3195e88c5bba%40googlegroups.com.

[August Alm]

Right, obviously!! Not sure I can make Artyom's suggestion work. The [list_vt_split_at(xs, a1)]
needs an [a1] that is not a [prval]. I need to think.