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

[Leslie Lamport <tlaplus.ll@xxxxxxxxx>]

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.

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6ed2c6ac-0ff5-4f1c-acac-303903f8141en%40googlegroups.com.