Phil, On 12 Jul 2011, at 12:00, Phil Clayton wrote:
> I have updated mdt064.doc (attached) to add tests that demonstrate two > printing issues relating to global variable names that contain strokes. Many thanks for those. Good test cases are always appreciated. > > > 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. > Agreed. > > 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). 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. Regards, Rob.
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
