I have updated mdt064.doc (attached) to add tests that demonstrate two printing issues relating to global variable names that contain strokes.


1. Generic global variables

Under certain conditions, strokes in the names of generic global variables (other than %bbU%) are not printed. (In particular, this affects generic global variables that are not "template forms with one or more non-%bbU% generic actual parameters".)

In imp064, function do_generic, I believe references to 'name' on lines 1350 and 1353 should refer to 'fullname'. That change fixes most of the test failures.


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.

Phil

Attachment: mdt064.doc.gz
Description: GNU Zip compressed data

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to