I’m trying to understand the behavior of the + and - operators in the context of the Int/int types. I’ve pored through the documentation, the book, and the source code for parsing, but I can’t figure this out. Maybe if I studied harder, I’d get it, but the notions in my noggin have become nugatory:
When I use this expression:
int[1+1], I get what I expect: the value of the union of Int[1] and Int[1], which is just 1.
Similarly,
int[2-1] gives me 2.
But when I do this:
int[1-1] I get an atom with the value 0
int[none] also gives an atom with the value 0, which is at least consistent, although I don’t know why that happens.
And when I do this:
int[2+1] I get 3
Why are + and - sometimes acting like set union/difference and sometimes like regular integer operators?
Bonus: at which level in the code is this happening? At the Kodkod level?
Also, the latest edition of the book doesn’t mention the int keyword as far as I can tell, only Int.
There is no need to tell me to use the integer module or the sum keyword. I’m just trying to grok the language.
They always act like union/difference (they are set operators). Function int takes a set of numbers and returns the sum of them all. I think all your examples are consistent with this semantics: 1+1 is a set just with 1 so the sum is 1. 1-1 is the empty set, the same as none, so its sum is 0. 2+1 is a set with with 2 and 1, so the sum is 3.
BTW, a good feature of the Analyzer that can be used to understand the semantics of operators is the evaluator. You can type different expressions there and see the result. I use it a lot when I don’t understand very well what is going on or to debug models.
I used the Evaluator to get these examples, actually. But you’re telling me that int behaves like sum.
This wasn’t documented in the latest edition of the book, although it looks like, indeed, it’s documented in an older edition I found online:
“Both integer expressions int e and sum e have an integer value that is the sum of the integer values associated with integer objects in the set denoted by the relational expression e. There is no semantic difference between the two.”
My initial understanding was that the int operator returned the value of a singular Int, which led to further confusion. This understanding was based on the, IMO, misleading documentation here:
integer — Alloy Documentation documentation https://alloy.readthedocs.io/en/latest/modules/integer.html
(Am I remiss in saying this is misleading? The example function uses deprecated syntax and doesn’t act like you’d expect an add function to act)
Thanks for your response, it was like removing a sliver.