#126 Bad printing of parentheses to Z/EVES

[Andrius Velykis]

There seems to be an issue with printing parentheses when converting CZT to Z/EVES. The issue appears when relational image is applied to a complex relation (that involves union of two relations). A failing example is:

\begin[disabled]{theorem}{rule cupImgTest}[X]
  \forall r : X \rel X; x : X @ (r \cup \{(x, x)\}) \limg \{x\} \rimg = r \limg \{x\} \rimg
\end{theorem}

CZT typechecks this correctly (as expected), however Z/EVES gives typechecking errors:

Error FunctionArgType (line 4) [Type checker]: in application of (∪) , argument 2 has the wrong type.
Error TypesNotSame (line 4) [Type checker]: types of r ∪ ({(x, x)} ⦇ {x} ⦈) and r ⦇ {x} ⦈ are not the same.

It appears that the ZEvesPrinter is introducing an error with incorrectly placed parentheses. The original rule is printed as:

<cmd name="add-paragraph">
  <theorem-def location="L414;C0;S17,057;E17,210;G153;Rptab_zd.zed"     ability="disabled" usage="rule" >cupImgTest [X]

    <ax-part/>&forall;  r: ((X) &lrarr; (X));x: X &bullet; (r &cup; { (x,x) } &lvparen; { x } &rvparen;    )  =  (r &lvparen; { x } &rvparen;)
  </theorem-def>
</cmd>

[Andrius Velykis]

A similar issue also appears with HideExpr. If the hidden expression is complex (e.g. schema composition), parentheses are not added. In this case Z/EVES applies the hiding to the last element only. An example to reproduce is:

\begin{schema}{T1}
  a! : \nat
\end{schema}

\begin{schema}{T2}
  a? : \nat
\end{schema}

\begin{zed}
  T3 \defs T1[a/a!] \semi T2[a/a?] \hide (a) 
\end{zed}

[Andrius Velykis]

Fixed in 5a2f5b67c5f4ebd50ad34a64db6144c073a0d26a.

Fixed the printing of both relational image and HideExpr. Also updated the parsing of Z/EVES results accordingly to avoid losing the parentheses on the way back.

[Andrius Velykis]

Also had a missing parentheses issue with schema expressions, (e.g. A \land (B \lor C) would be incorrectly printed without parentheses). Fixed this in 93b844811eb61aeffd5571e28c85944487d26929.