Yea, that would make more sense. I guess I still don't fully understand how to read constraint errors. Thanks for letting me know.
On Saturday, May 8, 2021 at 9:30:11 PM UTC-4 [email protected] wrote: > and by the way, the failing constraint was f1 == f1+1 > > сб, 8 мая 2021 г. в 22:09, d4v3y_5c0n3s <[email protected]>: > >> Thanks, I appreciate the help. I'm glad that the issue was a simple fix. >> :D >> >> On Saturday, May 8, 2021 at 3:14:33 PM UTC-4 gmhwxi wrote: >> >>> 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. >>> >>> >>> On Sat, May 8, 2021 at 9:39 AM d4v3y_5c0n3s <[email protected]> wrote: >>> >>>> 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. >>>> >>>> -- >>>> 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/dcf7d7eb-d69f-4746-800b-24c02084ee65n%40googlegroups.com >>>> >>>> <https://groups.google.com/d/msgid/ats-lang-users/dcf7d7eb-d69f-4746-800b-24c02084ee65n%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/c2070b8f-d112-426c-a69a-a2c23ca2dcffn%40googlegroups.com >> >> <https://groups.google.com/d/msgid/ats-lang-users/c2070b8f-d112-426c-a69a-a2c23ca2dcffn%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/a0349f8c-4e24-4b0c-801f-33118e9da26dn%40googlegroups.com.
