Issue with conditionally mutating a var twice

[d4v3y_5c0n3s]

  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))

|

[Dambaev Alexander]

Hi,

just a quick tip:

```

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))

```

means, that you passing an argument of primitive type, but you need a higher kinded type (int n, where n >= 0 && x < 4) and (int y), where y >= 0 && y < 4

first try is to replace 'i' with g1ofg0(i). then compiler may ask you to prove, that i>=0 && i < 4

чт, 16 июл. 2020 г. в 12:12, d4v3y_5c0n3s <tmj...@gmail.com>:

--
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/32da2a64-1760-418e-8d45-1960f16f13d5o%40googlegroups.com.

[Hongwei Xi]

>> 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

'i' is later used to index an array.

It seems that you just need:

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, $showtype(i), i) then 2 else i):natLt(3);

--

[artyom.s...@gmail.com]

Additionally, you might want to use different variables for i. It’s allowed to use the same variable name in successive let bindings. The different i will have different types, making it simpler for type checker to solve constraints.

Sent from my iPhone

On 16 Jul 2020, at 19:01, Hongwei Xi <gmh...@gmail.com> wrote:



To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAPPSPLqDLKzw8QZHUNeGoNqBGHJTQnzp6Gd0S0DAK%3Dy81BSpKQ%40mail.gmail.com.

[Hongwei Xi]

Great advice :)

In functional programming, using 'val' is preferred over using 'var'.

For instance, if you do

let

val x = 0

val x = x + 1

val x = 5 * x

in

  ...

end

The compiler is very likely to map the three x's to one register as if the code was written in

the following imperative style:

let

var x = 0

val () = x := x + 1

val () = x := 5 * x

in

   ...

end

On a modern architecture, register allocation is a complicated issue. By using more val's (instead

of var's), you allow more freedom during register allocation, potentially resulting in the generation of

more efficient object code.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/BB1AE44F-6247-41B3-8358-13E0A4DCC5FD%40gmail.com.

[d4v3y_5c0n3s]

Thanks everyone, I will be trying all of your suggestions and let you know whether they resolve my issue. :D

[d4v3y_5c0n3s]

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:

[Dambaev Alexander]

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.

Sorry, I am far from keyboard now, so can't test/play with code, but:

by using natLt(n), you are using a sort {i: nat | i < n}, so it actually the same as I suggested but more clear way - it proves, that the value of i is less then specified number

based on your error message, I can guess:

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

    var nxt = @[int](1, 2, 0) (* try var instead of val *)

but, I think, that error is not from the function, as errors complain on '!', which is missing in your line of code, so I can try to suggest to remove '!' and specify the non-overload function for '[]', so you can try to replace:

```

j := nxt[i];

```

with:

```

j := array_get_at_guint(nxt, i);

```

or

```

j := nxt{uint}[i];// <-- but I am not sure, if this is a correct syntax

```

[Hongwei Xi]

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.

--

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/8ff1323f-eb91-4a2b-a256-60c2d0d0e019o%40googlegroups.com.

[d4v3y_5c0n3s]

Thanks everyone, you were all extremely helpful!  I appreciate the advice too, and I'll look into using your suggestions to improve the code. Again, thanks! :D

On Thursday, July 16, 2020 at 8:12:39 AM UTC-4, d4v3y_5c0n3s wrote: