[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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

   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

On Thursday, January 7, 2021 at 12:13:35 PM UTC-8 nets...@xxxxxxxxx wrote:
To wit,
          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.