On 14/07/11 17:57, Rob Arthan wrote:
2. Decorated global variable name clash

When both C and C' are schema references, (C)' is printed as C' which
is a different term.

In imp064, the problem appears to be in function do_decor. There
appear to be two routes to fixing this:

A. Print in Spivey-Z with minimal parentheses, using the current
theory to determine whether parentheses are necessary, i.e. print C'
for (C)' if C' is not the name of a global variable.

B. Print in Standard-Z by always using enclosing parentheses for
decoration, i.e. print (C)' even if it is valid to print C'.

I think B can be achieved by simply dropping the ZLVar and ZGVar cases
on lines 670 and 671 of imp064.

I think B is not very nice for those used to Spivey Z. The following
heuristic seems good to me (and also fixes the remaining failures in
your new tests).

I have no objections here - I don't need Standard-form printed out - happy to see it fixed either way!

C. Add brackets if any of the following hold: (1) the operand is not a
variable (as now), (2) the operand is a local variable,
(3) the operand is a global variable whose name ends in a decoration
character, or (4) the operand is a global variable called N and there is
non-empty prefix P of the decoration such that N^P is declared as a
global variable.

Here (2) is the case when a local variable of schema type is decorated.
(4) is for the obscure case when, for example, the user has declared
schemas ABS and ABC!? and then says something like (ABC)!?! which the
parser will interpret as (ABC!?)! if you leave the brackets out.

I can't think of any case where this wouldn't work. As long as unpack_ident and pack_ident are used in cases 3 and 4 (e.g. to test whether a name ends in a decoration character) there shouldn't be a problem with template forms.

I note that, as ProofPower stands, given

    generic (ab _)

    ab X == [a, b : X]


    ab' X

prints back as

    (ab X)'

To get the first form (which is in the spirit of your proposal) would need a change that is more than simply changing the condition for need_brackets in do_decor.


Proofpower mailing list

Reply via email to