Having Trouble Finding a Constraint Which is Failing

[d4v3y_5c0n3s]

    So, I'm having difficulty understanding a constraint that is failing in my code.  The constraint that is failing is "f1 + f1 = 1", which I am confused by, because there appears to be no such constraint in my code.

Here's what (most of) my code is:

        dataprop FBT_IN (int, a:addr) =

        | FBT_NIL(0, a)

        | {n:nat} FBT_CONS(n+1, a) of FBT_IN(n, a)

        

        typedef fb_count (a:addr, f:int, b:int) = [c:nat | f >= 0; b >= 0] (FBT_IN(c, a) | int f, int b)

        typedef f_ind (a:addr, f:int, i:int) = int i

        typedef b_ind (a:addr, b:int, i:int) = int i

        

        fn tri_fb_test {c:nat}{l:addr}

        (

        pfin: FBT_IN(c, l) | t: ctri, dv: plane

        ): (FBT_IN(c+1, l) | intBtwe(0,2)) =

          if ctri_inside_plane(t, dv) then (FBT_CONS(pfin) | 0)

          else if ctri_outside_plane(t, dv) then (FBT_CONS(pfin) | 1)

          else (FBT_CONS(pfin) | 2)

        

        fun loop1 {i,j:nat | i <= j}{a:addr}{f1,b1:nat}

        ( a: !arrayptr(ctri, a, j), dv: plane,

        fbc: fb_count(a, f1, b1),

        j: int j, i: int i ): [f2,b2:nat] fb_count(a, f2, b2) = (

          if i < j then let

            val c: ctri = a[i]

            val (pf_tr | tr) = tri_fb_test(fbc.0 | c, dv)

            val ret_fbc = ifcase

              | tr=0 => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2)

              | tr=1 => (FBT_CONS(fbc.0) | fbc.1, fbc.2+1)

              | _ => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2+1)

          in

            loop1(a, dv, ret_fbc, j, i+1)  // <-- constraint fails on this line at "ret_fbc"

          end else fbc

And here's the error produced:

$ patscc -tcats cmesh.dats

/home/tmj90/Goldelish-Engine/source/assets/cmesh.dats: 8604(line=235, offs=26) -- 8611(line=235, offs=33): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eeqeq(S2Evar(f1(8784)); S2Eapp(S2Ecst(add_int_int); S2Evar(f1(8784)), S2Eintinf(1))))

typechecking has failed: there are some unsolved constraints: please inspect the above reported error message(s) for information.

exit(ATS): uncaught exception: _2tmp_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

I suspect the issue is an implicitly generated constraint of some kind, but I have no idea where it's coming from.  However, I discovered that if I comment out these lines:

            val ret_fbc = ifcase

              //| tr=0 => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2)

              //| tr=1 => (FBT_CONS(fbc.0) | fbc.1, fbc.2+1)

              | _ => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2+1)

then everything typechecks.  That's the biggest hint I could find, but I don't know what going wrong.  Please let me know if you'd like me to provide more code, I just didn't want to clutter my initial post.

[Hongwei Xi]

This is due to a missing type annotation for 'ifcase'

in your code:

val ret_fbc =
(

ifcase
| tr=0 =>
  (FBT_CONS(fbc.0) | fbc.1+1, fbc.2)
| tr=1 =>
  (FBT_CONS(fbc.0) | fbc.1, fbc.2+1)
| _ => (FBT_CONS(fbc.0) | fbc.1+1, fbc.2+1)

) : [f1,b1:nat] fb_count(a, f1, b1)

In general, if-exp, case-exp and ifcase-exp should all be given a type annotation.

--
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/dcf7d7eb-d69f-4746-800b-24c02084ee65n%40googlegroups.com.

[d4v3y_5c0n3s]

Thanks, I appreciate the help.  I'm glad that the issue was a simple fix. :D

[Dambaev Alexander]

and by the way, the failing constraint was f1 == f1+1

сб, 8 мая 2021 г. в 22:09, d4v3y_5c0n3s <tmj...@gmail.com>:

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/c2070b8f-d112-426c-a69a-a2c23ca2dcffn%40googlegroups.com.

[d4v3y_5c0n3s]

Yea, that would make more sense.  I guess I still don't fully understand how to read constraint errors.  Thanks for letting me know.

[Dambaev Alexander]

The trick is to count the brackets :)

S2Eeqeq is quite easy, as it is a binary operator, so it has 2 operands: S2Evar(f1(8784)) is the first one, as it followed by ';', so the rest is the second operand :)