I made the function mat4_to_quat type-check. See the attached file. One noticeable change is the type for the 'loop' function in your code:
fun loop {n,m:nat | 0 <= m+1; m+1 <= n} .<m+1>. (m: int m, qs:
&(@[quat][n]), ws: &(@[float][n]), acc1: vec3) : vec3 = ...
Also, I modified
(mat4_at(m, j, j), mat4_at(m, k, k))
into
(mat4_at(m, j, j) + mat4_at(m, k, k)) // '+' is chosen randomly here.
######
Right now, there are a lot of casts needed in your code. Let me make a
suggestion.
When using an array of floats (instead of an array of doubles), you
primarily want to
save some memory. But for arithmetic operations, you probably want to use
doubles.
I would follow the rules below:
When a float is read from an array of floats, cast it to a double
immediately. Also, cast a
double into a float before writing to an array of floats. For example,
the following interface:
fun mat4_rotation_x ( a: float ) : mat4
should be changed to
fun mat4_rotation_x ( a: double ) : mat4
Also, please make mat4 an abstract type.
On Fri, Jul 17, 2020 at 8:04 AM d4v3y_5c0n3s <[email protected]> wrote:
> Okay, so gmhwxi's suggestion to use natLt(2) & natLt(3) seems to have
> worked, but I'm having trouble understanding what natLt(2) & natLt(3)
> actually is.
>
> *Could anyone explain what natLt(2) & natLt(3) mean, please?* After
> looking at the prelude the definition of natLt() doesn't seem
> self-explanatory.
>
> As for the suggestions to use separate val-declarations in a more
> functional style, my reason for taking this approach is that I am trying to
> replicate some C code in ATS. *I do agree that this is probably not the
> cleanest solution, I figure that I can revise it later once I get my
> overall project working.* But I appreciate the suggestions, so thank you.
>
> Going off of what Dambaev said, *it makes sense to prove to the compiler
> that 'i' is >= 0 && < 4, but what sort of statements might I use for this? *
> I worked through chapter 12 of Intro to Programming in ATS, but I'm still
> quite unsure on how to use proofs effectively. Thanks for this advice,
> Dambaev.
>
> Lastly, *I am running into an issue with indexing an array where the
> compiler says that the function argument must be a left-value.* I assume
> that 'nxt' is the one that needs to be a left-value, but !nxt doesn't make
> a difference. Any help that can be provided is appreciated.
>
> Apologies for the long response, I wanted to make sure I responded to as
> many of you as possible, because you've all been really helpful. :)
>
> Here's my updated function:
>
> implement mat4_to_quat ( m ) = let
> val tr = m.xx + m.yy + m.zz
> in
> if tr > 0.f then let
> val s = $MATH.sqrt(tr + 1.f)
> val w = s / 2.f
> val x = ( mat4_at(m, 1, 2) - mat4_at(m, 2, 1) ) * (0.5f / s)
> val y = ( mat4_at(m, 2, 0) - mat4_at(m, 0, 2) ) * (0.5f / s)
> val z = ( mat4_at(m, 0, 1) - mat4_at(m, 1, 0) ) * (0.5f / s)
> in
> quat_new(x, y, z, w)
> end else let
> val nxt = @[int](1, 2, 0)
> var q = @[float][4](0.f)
> var i = 0
> var j = 0
> var k = 0
> var s = 0
> in
> i := ((if mat4_at(m, 1, 1) > mat4_at(m, 0, 0) then 1 else i):natLt(2));
> i := ((if mat4_at(m, 2, 2) > mat4_at(m, i, i) then 2 else i):natLt(3));
> *j := nxt[i]; <-- first error message is on this line*
> k := nxt[j];
> s := $MATH.sqrt( (mat4_at(m, i, i) - (mat4_at(m, j, j), mat4_at(m, k,
> k))) + 1.f );
> q[i] := s * 0.5f;
> s := (if (s != 0.f) then 0.5f / s else s);
> q[3] := (mat4_at(m, j, k) - mat4_at(m, k, j)) * s;
> q[j] := (mat4_at(m, i, j) + mat4_at(m, j, i)) * s;
> q[k] := (mat4_at(m, i, k) + mat4_at(m, k, i)) * s;
> quat_new(q[0], q[1], q[2], q[3])
> end
> end
>
>
> Here's the new error message:
>
> patscc -tcats /home/d4v3y/Goldelish-Engine/source/g_engine.dats
> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35545(line=1374,
> offs=11) -- 35549(line=1374, offs=15): error(3): the function argument
> needs to be a left-value.
> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35544(line=1374,
> offs=10) -- 35551(line=1374, offs=17): error(3): the symbol [!] cannot be
> resolved as no match is found.
> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35539(line=1374,
> offs=5) -- 35551(line=1374, offs=17): error(3): assignment cannot be
> performed: mismatch of bef/aft type-sizes:
> bef: [S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_int),
> S2Eintinf(0))]
> aft: [S2Eerrexp()]
> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35562(line=1375,
> offs=10) -- 35568(line=1375, offs=16): error(3): the symbol [[]] cannot be
> resolved due to too many matches:
> D2ITMcst(array_get_at_guint) of 0
> D2ITMcst(array_get_at_gint) of 0
> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35557(line=1375,
> offs=5) -- 35568(line=1375, offs=16): error(3): assignment cannot be
> performed: mismatch of bef/aft type-sizes:
> bef: [S2Eapp(S2Ecst(g1int_int_t0ype); S2Eextkind(atstype_int),
> S2Eintinf(0))]
> aft: [S2Eerrexp()]
>
>
> On Thursday, July 16, 2020 at 8:12:39 AM UTC-4, d4v3y_5c0n3s wrote:
>>
>> So, I'm trying to mutate a var twice in order to replicate some C code
>> that I am trying to port to ATS. But, I've been scratching my head as to
>> why this would happen, so any help is appreciated. In an effort to not
>> waste your time, I will be showing you the function with my issue along
>> with the declarations for the relevant functions & typedefs. Please ask if
>> you'd like me to provide more details that I may have missed.
>>
>> The function I'm having trouble in:
>>
>> implement mat4_to_quat ( m ) = let
>> val tr = m.xx + m.yy + m.zz
>> in
>> if tr > 0.f then let
>> val s = $MATH.sqrt(tr + 1.f)
>> val w = s / 2.f
>> val x = ( mat4_at(m, 1, 2) - mat4_at(m, 2, 1) ) * (0.5f / s)
>> val y = ( mat4_at(m, 2, 0) - mat4_at(m, 0, 2) ) * (0.5f / s)
>> val z = ( mat4_at(m, 0, 1) - mat4_at(m, 1, 0) ) * (0.5f / s)
>> in
>> quat_new(x, y, z, w)
>> end else let
>> val nxt = @[int](1, 2, 0)
>> var q = @[float][4](0.f)
>> var i = 0
>> var j = 0
>> var k = 0
>> var s = 0
>> in
>> * i := ((if mat4_at(m, 1, 1) > mat4_at(m, 0, 0) then 1 else i):int);*
>> * i := ((if mat4_at(m, 2, 2) > mat4_at(m, $showtype(i), i) then 2 else
>> i):int); // <-- this line has the error*
>> j := nxt[i];
>> k := nxt[j];
>> s := $MATH.sqrt( (mat4_at(m, i, i) - (mat4_at(m, j, j), mat4_at(m, k,
>> k))) + 1.f );
>> q[i] := s * 0.5f;
>> s := (if (s != 0.f) then 0.5f / s else s);
>> q[3] := (mat4_at(m, j, k) - mat4_at(m, k, j)) * s;
>> q[j] := (mat4_at(m, i, j) + mat4_at(m, j, i)) * s;
>> q[k] := (mat4_at(m, i, k) + mat4_at(m, k, i)) * s;
>> quat_new(q[0], q[1], q[2], q[3])
>> end
>> end
>>
>>
>> Here's the function's declaration:
>>
>> fun mat4_to_quat ( m: mat4 ) : quat = "sta#%"
>>
>>
>> Here's the declaration for mat4_at:
>>
>> fun mat4_at {x:nat | x < 4}{y:nat | y < 4} ( m: mat4, x: int x, y: int y
>> ) : float = "sta#%"
>>
>>
>> My full repo can be found here:
>> https://github.com/d4v3y5c0n3s/Goldelish-Engine
>> Here's the error message:
>>
>> patscc -tcats /home/d4v3y/Goldelish-Engine/source/g_engine.dats
>> **SHOWTYPE[UP]**(/home/d4v3y/Goldelish-Engine/source/g_engine.dats:
>> 35508(line=1373, offs=55) -- 35509(line=1373, offs=56)):
>> S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int)): S2RTbas(S2RTBASimp(1;
>> t@ype))
>> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35508(line=1373,
>> offs=55) -- 35509(line=1373, offs=56): error(3): the dynamic expression
>> cannot be assigned the type [S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2EVar(6368))].
>> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35508(line=1373,
>> offs=55) -- 35509(line=1373, offs=56): error(3): mismatch of static terms
>> (tyleq):
>> The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
>> The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2EVar(6368))
>> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35512(line=1373,
>> offs=59) -- 35513(line=1373, offs=60): error(3): the dynamic expression
>> cannot be assigned the type [S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2EVar(6369))].
>> /home/d4v3y/Goldelish-Engine/source/g_engine.dats: 35512(line=1373,
>> offs=59) -- 35513(line=1373, offs=60): error(3): mismatch of static terms
>> (tyleq):
>> The actual term is: S2Eapp(S2Ecst(g0int_t0ype); S2Eextkind(atstype_int))
>> The needed term is: S2Eapp(S2Ecst(g1int_int_t0ype);
>> S2Eextkind(atstype_int), S2EVar(6369))
>>
>> |
>>
> --
> 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 [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/ats-lang-users/8ff1323f-eb91-4a2b-a256-60c2d0d0e019o%40googlegroups.com
> <https://groups.google.com/d/msgid/ats-lang-users/8ff1323f-eb91-4a2b-a256-60c2d0d0e019o%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLrhSst3mZcp6dm4ceQ0E%2BmaripZyxhTXgCKagKkiTnN%2BQ%40mail.gmail.com.
g_engine.dats
Description: Binary data
