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.
