modulo in constraints

[Brandon Barker]

Hi,

I've been playing around with P2 from project euler. I have a long way to go (for the proof; even a semi-shoddy proof at that), but think I've made significant progress. I'm now getting "ye olde constraint error": 

$ patsopt.exe -tc -d P2-bbarker.dats

/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats: 857(line=55, offs=28) -- 857(line=55, offs=28): error(3): unsolved constraint: C3NSTRprop(main; S2Eapp(S2Ecst(==); S2Eapp(S2Ecst(mod); S2Eapp(S2Ecst(+); S2EVar(4158->S2Evar(ln1(7667))), S2EVar(4159->S2Evar(ln2(7666)))), S2Eintinf(2)), S2Eintinf(0)))

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

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

Here's the version of code pertinent to the question:

https://github.com/bbarker/ATS-Postiats-test/blob/dc9fb2465d0c8a7cfdb9e693fdbfb657c5ff847a/contrib/bbarker/PEULER/P2/P2-bbarker.dats

Of course, it is probably more likely I have a typo somewhere else ... I've found many already, but am stuck now.

[gmhwxi]

nmod does not give you a type that is accurate enough for this task.
Try to use n - 2*half(n) (instead of nmod(n,2)) for this case.

As a rule of thumb, it is always a good idea to introduce a function of your own
in this kind of situation:

fun my_mod2 {n:nat} (int(n)): int(n%2)

Then move on. You can always come back to deal with these introduced
functions later.

When programming, a programmer so often follows whatever the library provides.

IMO, a programmer should be "self-centered" :)

Try to introduce whatever functions you need (if you can quickly convince yourself
that these functions can be readily implemented based on some kind library).

[Brandon Barker]

Good advice, thanks! But I now seem to be getting an invalid constraint popping up: ln1 + ln2 = ln1, i.e.:

/home/brand_000/ATS-Postiats-test/contrib/bbarker/PEULER/P2/P2-bbarker.dats: 1019(line=62, offs=7) -- 1064(line=62, offs=52): error(3): unsolved constraint: C3NSTRprop(main; S2Eeqeq(S2Eapp(S2Ecst(add_int_int); S2Evar(ln1(7703)), S2Evar(ln2(7702))); S2Evar(ln1(7703))))

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

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

Of course it is clear to me that is an invalid constraint, I just don't know why I have it. It is suggestive that I have a typo somewhere that is making the loop signature unhappy.

Here's my update: https://github.com/bbarker/ATS-Postiats-test/commit/46f94f770641b7916004a4fc550ff4e3f07c7b8a

--
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/09491914-f512-4716-a091-e072541c1e0d%40googlegroups.com.

--

Brandon Barker
brandon...@gmail.com

[Hongwei Xi]

The type for my_mod2 does not look right.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAORbNRoEFUjMdTrpiyij0ZzOYuMi6D%3DOtojPCVKWoecBFZpQxA%40mail.gmail.com.