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
    //may need to use the ">>" syntax in order to do the below cast
    //step 1: cast arrayptr to array_v & ptr using 
arrayptr_takeout_viewptr()
    var ar_copy = ar
    val (pf_ar | ar_p) = arrayptr_takeout_viewptr(ar_copy)
    //step 2: call array_ptr_takeout() to get the viewtype for the given 
element
    val (ar_ipf1, ar_ipf2 | ar_i) = array_ptr_takeout(pf_ar | ar_p, 
size_of_int(i))
  in
    mesh_print(!ar_i);
    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-users+unsubscr...@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.

Reply via email to