var preservation constraint fails

[Mike Jones]

I'm totally stuck on a compile error, for some code that in other contexts/functions works just fine.

It is reasonable that incrementing by 1 when less than 123 satisfies the constraint. But it is not clear why in other contexts incrementing works, but in this one it does not.

If I change to s.holdcnt := 0, it works fine. So it is trouble with the + 1.

Any ideas why?

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

extern fun{} next (s: &state): void

implement{} next (s) = if s.holdcnt < 123 then s.holdcnt := s.holdcnt + 1 else s.err := s.err + ONE

/home/mike/cypress/workspace/USBFrameInOut/DATS/frames.dats: 6842(line=251, offs=51) -- 6868(line=251, offs=77): error(3): unsolved constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(<=); S2EVar(2574->S2Eapp(S2Ecst(add_int_int); S2Evar(i$4486$4487$4488$4491(8664)), S2Eintinf(1))), S2Eintinf(123)))

/home/mike/cypress/workspace/USBFrameInOut/DATS/frames.dats: 6842(line=251, offs=51) -- 6868(line=251, offs=77): 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)

make: *** [DATS/frames_dats.c] Error 1

[Eric Jones]

Hello Mike,

I too run into this problem often. I don't know why the following (reduced example) illustrates a work around. Assigning the value to a new var seems to give ATS enough of a hint. I'm interested in the reason behind this as much as you are sir.

typedef state = @{ holdcnt = natLte(123) ... }

extern fun{} next (s: &state): void

implement{} next (s) = let
    val holdcnt = s.holdcnt
    ...
  in
  if holdcnt < 123
    then s.holdcnt := holdcnt + 1
    else ...
  end


Best,
Eric

[Mike Jones]

Eric,

That worked. 

Perhaps the constraint solver gets confused by multiple uses of a reference in the same statement and does not know which is the "before" value vs. the "after" value.

But it seems to be context sensitive. I have cases where it figures it out, and can't see any real difference in the code structure. I also noticed that when I do it in a let clause, and then have a in clause, putting "_" vs "()" makes a difference. Sometimes with an "_" the compiler is happy.

Mike

[Hongwei Xi]

The type system does not track the types of the fields of a record.


You need to do the tracking explicitly:



implement
{}
next (s) =
let val n = s.holdcnt in if n < 123 then s.holdcnt := n+1 else s.err := s.err + ONE


--
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 https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/102e3513-4a29-40d9-aaa3-4cbb39d2cc94%40googlegroups.com.