How do I store a viewtype in an array and then access that value?
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: 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?
Thank you to anyone who can help me out with this problem. Have an awesome
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-users+unsubscr...@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.
Re: How do I store a viewtype in an array and then access that value?
пт, 25 сент. 2020 г. в 13:52, d4v3y_5c0n3s :
> 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: 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-users+unsubscr...@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
>
> .
>
--
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/CAKO6%3Dqjb6nYhEFtY82dJ_ezKbtGuGo-qEbzM2QcxAOjQ2LpFKA%40mail.gmail.com.
Re: How do I store a viewtype in an array and then access that value?
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 :
>
>> 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: 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
>>
>>
>> .
>>
>
>
> --
> 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/bf350322-4188-4c33-961f-d2242c20bb45n%40googlegroups.com.
