[tlaplus] Re: How come defined functions don't work in assignment?

On Thursday, January 7, 2021 at 3:54:03 PM UTC-5 Leslie Lamport wrote:

Supposed you defined:

MasterHeadIdx(i) == 2 * MasterState[7].HeadIdx + i

if you wrote

MasterHeadIdx(i) := MasterHeadIdx(i) + 1

would you expect the translator to look at your definition of
MasterHeadIdx and realize that what you were really writing is the
following?

i := i+1

It would be nice if the translator were that smart, but it isn't. It's
no smarter than a Java compiler, which wouldn't allow you to define
MasterHeadIdx as a method and then write

MasterHeadIdx(i) = MasterHeadIdx(i) + 1

Not even if you defined the method as in your definition of
MasterHeadIdx. The syntax of PlusCal (like the syntax of Java)
allows you to write only

(*) MasterHeadIdx[i] := MasterHeadIdx[i] + 1

So, you'd have to define MasterHeadIdx to be a function. You can look
up how to define functions in "Specifying Systems". However, that's
not going to solve your problem because to write (*), MasterHeadIdx
must be declared to be a variable, so it can't be a defined function.

You seem to want to define MasterHeadIdx to be some kind of syntactic
macro. I don't know how to do that in either Java or PlusCal.
Perhaps if you tried doing what you want to do in Java (or some other
programming language) you might be able to figure out how to do it in
PlusCal.

Leslie
On Thursday, January 7, 2021 at 12:13:35 PM UTC-8 nets...@xxxxxxxxx wrote:
To wit,
define
MasterHeadIdx(i) == MasterState[i].HeadIdx
end define;

This *does not work*:
\* fragment in a process, procedure
MasterHeadIdx(1) := MasterHeadIdx(1)+1;

This *does work*:
MasterState[1].HeadIdx := MasterState[1].HeadIdx + 1;

The inability to use defined functions in assignment half-defeats the utility
of the define by making one use **and not use** defined functions depending
on context.