Also, as a side note, I noticed that the "array_ptr_takeout()" function
calls the array_v_takeout() proof function, but why is there no
array_v_addback()?
On Sunday, September 27, 2020 at 5:13:32 PM UTC-4 d4v3y_5c0n3s wrote:
> Ice, thank you for your suggestion, once I get this working I should
> replace my handmade loops with arrayptr_foreach() calls like you suggested.
> Artyom, I see what you were trying to do with your suggestion, but it
> didn't work due to the proof pf_ar being consumed by the
> array_ptr_takeout() call.
>
> Here is the code for anyone who wants to see it:
> implement model_print ( m ) = let
> fun mesh_print_loop {l:addr}{i,j:int | 0 <= i+1; i+1 <= j} .<i+1>.
> ( i: int i, ar: !arrayptr(mesh, l, j)): void =
> if i >= 0 then let
> val (pf_ar | ar_p) = arrayptr_takeout_viewptr(ar)
> val (ar_ipf1, ar_ipf2 | ar_i) = array_ptr_takeout(pf_ar | ar_p,
> size_of_int(i))
> val () = mesh_print(!ar_i)
> prval () = arrayptr_addback(pf_ar | ar_p)
> in
> mesh_print_loop(i-1, ar)
> end else ()
> in
> mesh_print_loop((m.0)-1, m.1)
> end
>
> Here is the error message from the compiler:
> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79153(line=2750,
> offs=33) -- 79158(line=2750, offs=38): error(3): the linear dynamic
> variable [pf_ar$5913(-1)] is no longer available.
> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79153(line=2750,
> offs=33) -- 79158(line=2750, offs=38): error(3): the dynamic expression
> cannot be assigned the type [S2Eat(S2Etyarr(S2Einvar(S2EVar(7937));
> S2EVar(7939)), S2EVar(7938))].
>
> I will continue to work on this, and I'll post if I come to a solution.
> On Saturday, September 26, 2020 at 12:10:11 PM UTC-4 d4v3y_5c0n3s wrote:
>
>> Awesome! Thanks for all of these suggestions! I'll try them later on
>> and then post how it went.
>>
>> On Saturday, September 26, 2020 at 10:56:07 AM UTC-4
>> artyom.s...@gmail.com wrote:
>>
>>> Hi d4v3y,
>>>
>>> I will make a fix below that might work. However, as Alexander
>>> mentioned, if you only want to map an array (i.e. apply a function to each
>>> element), then you probably don't want to hand-roll a loop.
>>>
>>> сб, 26 сент. 2020 г. в 16:54, d4v3y_5c0n3s <tmj...@gmail.com>:
>>>
>>>> So, I tried to call the prelude's array_ptr_takeout() function, but
>>>> that only works with a pointer of view array_v(), wereas I am using the
>>>> arrayptr() viewtype. To solve this, I called the cast function
>>>> arrayptr_takeout_viewptr(), which seemed to suit my needs perfectly.
>>>> Here's my code currently:
>>>
>>> implement model_print ( m ) = let
>>>> fun mesh_print_loop {l:addr}{i,j:int | 0 <= i+1; i+1 <= j} .<i+1>.
>>>> ( i: int i, ar: !arrayptr(mesh, l, j)): void =
>>>> if i >= 0 then let
>>>>
>>> val (pf_ar | ar_p) = arrayptr_takeout_viewptr(ar) // take out the
>>>> view: the type of [ar] is changed!
>>>>
>>> val (ar_ipf1, ar_ipf2 | ar_i) = array_ptr_takeout(pf_ar | ar_p,
>>>> size_of_int(i))
>>>>
>>> val () = mesh_print(!ar_i)
>>> prval () = arrayptr_addback (pf_ar | ar) // put it back where it
>>> belongs: [ar] is now the same type as it was on entry
>>>
>>>> in
>>>>
>>> mesh_print_loop(i-1, ar)
>>>> end else ()
>>>> in
>>>> mesh_print_loop((m.0)-1, m.1)
>>>> end
>>>>
>>>
>>>> But, my code is producing the following errors:
>>>> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
>>>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79400(line=2755,
>>>> offs=26) -- 79402(line=2755, offs=28): error(3): the linear dynamic
>>>> variable [ar$5912(-1)] is no longer available.
>>>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79400(line=2755,
>>>> offs=26) -- 79402(line=2755, offs=28): error(3): the dynamic expression
>>>> cannot be assigned the type
>>>> [S2Eapp(S2Ecst(arrayptr_vt0ype_addr_int_vtype);
>>>> S2Ecst(mesh), S2EVar(7940), S2EVar(7942))].
>>>>
>>>> I assume the way to fix this would be to change "ar: !arrayptr(mesh, l,
>>>> j)" to "ar: !arrayptr(mesh, l, j) >> ..." in the function inputs, but I'm
>>>> unsure what exactly needs to go in the ".." part. Any help is
>>>> appreciated,
>>>> and thanks for the previous suggestion.
>>>> On Friday, September 25, 2020 at 8:43:10 AM UTC-4 d4v3y_5c0n3s wrote:
>>>>
>>>>> Thanks for the help! Once I get the opportunity to test your
>>>>> suggestion of using array_ptr_takeout, I'll post whether it worked or not.
>>>>>
>>>>> On Friday, September 25, 2020 at 8:00:15 AM UTC-4
>>>>> artyom.s...@gmail.com wrote:
>>>>>
>>>>>> пт, 25 сент. 2020 г. в 13:52, d4v3y_5c0n3s <tmj...@gmail.com>:
>>>>>>
>>>>>>> So, what I'm trying to do is create a type which resembles the
>>>>>>> following:
>>>>>>>
>>>>>>> absvt@ype model = [l:addr][n:nat] ( int n, arrayptr(mesh, l, n) )
>>>>>>>
>>>>>>> Where "mesh" is also an absvt@ype. ATS lets me create this type
>>>>>>> fine, but I run into an issue when I try to index the array in the
>>>>>>> following code:
>>>>>>>
>>>>>>> implement model_print ( m ) = let
>>>>>>> fun mesh_print_loop {l:addr}{i,j:int | 0 <= i+1; i+1 <= j} .<i+1>.
>>>>>>> ( i: int i, ar: !arrayptr(mesh, l, j)): void =
>>>>>>> if i >= 0 then let
>>>>>>> in
>>>>>>> mesh_print(ar[i]);
>>>>>>> mesh_print_loop(i-1, ar)
>>>>>>> end else ()
>>>>>>> in
>>>>>>> mesh_print_loop((m.0)-1, m.1)
>>>>>>> end
>>>>>>>
>>>>>>> I get the following error messages:
>>>>>>>
>>>>>>> patscc -tcats /home/tmj90/Goldelish-Engine/source/g_engine.dats
>>>>>>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79208(line=2749,
>>>>>>> offs=16) -- 79211(line=2749, offs=19): error(3): the dynamic expression
>>>>>>> cannot be assigned the type
>>>>>>> [S2Eapp(S2Ecst(arrayptr_vt0ype_addr_int_vtype);
>>>>>>> S2Einvar(S2EVar(7929)), S2EVar(7933), S2EVar(7931))].
>>>>>>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79208(line=2749,
>>>>>>> offs=16) -- 79211(line=2749, offs=19): error(3): mismatch of sorts in
>>>>>>> unification:
>>>>>>> The sort of variable is: S2RTbas(S2RTBASimp(1; t@ype))
>>>>>>> The sort of solution is: S2RTbas(S2RTBASimp(3; viewt0ype))
>>>>>>> /home/tmj90/Goldelish-Engine/source/g_engine.dats: 79208(line=2749,
>>>>>>> offs=16) -- 79211(line=2749, offs=19): error(3): mismatch of static
>>>>>>> terms
>>>>>>> (tyleq):
>>>>>>> The actual term is: S2Ecst(mesh)
>>>>>>> The needed term is: S2Einvar(S2EVar(7929->S2Ecst(mesh)))
>>>>>>>
>>>>>>> I've looked at the prelude, and the issue appears to be that all of
>>>>>>> the functions for indexing an array use "t0p" instead of "vt0p," which
>>>>>>> is
>>>>>>> what I need. What I'd like to know is, is there cleaner way to do what
>>>>>>> I'm
>>>>>>> trying to accomplish? I figure I could write my own function that
>>>>>>> overrides [], but is there another way?
>>>>>>>
>>>>>>
>>>>>> A subscription like a[i] involves copying the element at position i
>>>>>> in the array. If this element is itself linear (i.e. vt0p), we can't
>>>>>> easily
>>>>>> duplicate it (copy it).
>>>>>>
>>>>>> You will have to use array_ptr_takeout instead. It will give you a
>>>>>> pointer to the i'th element of the array and a proof function for
>>>>>> "trading"
>>>>>> the associated at-view for the full array view.
>>>>>>
>>>>>>
>>>>>>>
>>>>>>> Thank you to anyone who can help me out with this problem. Have an
>>>>>>> awesome day.
>>>>>>>
>>>>>>
>>>>>> Thanks! You too, have a great day.
>>>>>>
>>>>>>
>>>>>>> --
>>>>>>> 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 view this discussion on the web visit
>>>>>>> https://groups.google.com/d/msgid/ats-lang-users/084b0cda-c769-4078-a20b-ab10345958a9n%40googlegroups.com
>>>>>>>
>>>>>>> <https://groups.google.com/d/msgid/ats-lang-users/084b0cda-c769-4078-a20b-ab10345958a9n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>>>>> .
>>>>>>>
>>>>>>
>>>>>>
>>>>>> --
>>>>>> Cheers,
>>>>>> Artyom Shalkhakov
>>>>>>
>>>>> --
>>>> 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 view this discussion on the web visit
>>>> https://groups.google.com/d/msgid/ats-lang-users/98a801d0-3c66-4833-9748-9b086e29bfb9n%40googlegroups.com
>>>>
>>>> <https://groups.google.com/d/msgid/ats-lang-users/98a801d0-3c66-4833-9748-9b086e29bfb9n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>>
>>>
>>>
>>> --
>>> Cheers,
>>> Artyom Shalkhakov
>>>
>>
--
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 view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/3ea56132-06c8-409c-8d71-7594d41f3c91n%40googlegroups.com.
