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]
then
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.
Phil
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
