Calculation breaks constraint

Google Group
1

If s.holdcnt = 123, s.holdcnt := s.holdcnt +1 causes a type error.On Nov 5, 2015 5:39 PM, “Mike Jones” proc...@gmail.com wrote:

Struggling with a compiler error again. state.holdcnt has type natl.(123)
and a function with a type {n0: nat | n0 >= 3 && n0 <= 127} needs to be
called.

As a temporary cheat, I made a converter c73 to clamp values (to be
removed later)

when I call set_n with a calculated value in c73(3 + s.holdcnt), the
compiler is ok with that line, but give the error on the last line at 450.
There is a portion like (S2Ecst(add_int_int)). Is there something about the
way I express 3 + s.holdcnt that results in the wrong type? My assumption
is the 3 takes the type of s.holdcnt, and would pass to c73 properly.

Note, I will eventually try to remove c73, but that will be hard because
s.holdcnt is global state used all over. Probably can only be carefully
managed at run time.

typedef state = @{ addr = uint8, err = uint8, pm = pmode, ps = pstate,
holdcnt = natLte(123), zerocnt = uint16 }

extern fun{} c73 (x: natLte(127)): [n: int | n >= 3; n <= 127] int(n)
implement{} c73 (x) =
case+ 0 of
| _ when x < 3 => 3
| _ => $UN.cast{intBtwe(3,127)}(x)

extern fun{} set_n {n0: nat | n0 >= 3 && n0 <= 127} (count: int(n0)): void

| ReadByte() => let
    val (ok,byte) = (case+ pec of
                      | Pec()   =>

i2c_read_byte_data_pec(!smbusInAddress, !smbusInCommand)
| NoPec() => i2c_read_byte_data(!smbusInAddress,
!smbusInCommand)): (uint8, uint8)
val () = if (ok <> OK)
then let
val () = s.err := s.err + ONE
in _ end
else let
val () = packetOutContents[s.holdcnt] := byte
val () = s.holdcnt := s.holdcnt + 1
in set_n(c73(3 + s.holdcnt)) end
in () end // Line 450

13378(line=450, offs=12) – 13380(line=450, offs=14): error(3): unsolved
constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); S2Eintinf(0),
S2EVar(2284->S2Eapp(S2Ecst(add_int_int);
S2Evar(i$3823$3824$3825$3828(7996)), S2Eintinf(1)))))
/home/mike/linti/linti-avr/DATS/frames.dats: 13378(line=450, offs=12) –
13380(line=450, offs=14): error(3): unsolved constraint for var preservation
/home/mike/linti/linti-avr/DATS/frames.dats: 14535(line=471, offs=12) –
14537(line=471, offs=14): error(3): unsolved constraint for var preservation
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2hwxi_2Research_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)

–
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 post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at http://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/dd4ac5f9-8bb8-4542-bd78-a2e95b7ecbea%40googlegroups.com
https://groups.google.com/d/msgid/ats-lang-users/dd4ac5f9-8bb8-4542-bd78-a2e95b7ecbea%40googlegroups.com?utm_medium=email&utm_source=footer
.