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 ats-lang-users+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/8ff1323f-eb91-4a2b-a256-60c2d0d0e019o%40googlegroups.com.