From: Leo Freitas <leo.freitas@ne...>  20110922 08:41:42

Hi Tim, I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise. That is because after type checking the ZExprList will contain (possibly nonmaximal) generics which the user don't want explicitly given on the terms. Is that right? Assuming it is, what about proofs / conjectures involving nonmaximal generics? Ex: \begin{theorem}{lNonMaxCup}[X] \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B \end{theorem} \begin{theorem}{catGen}[X] \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t \end{theorem} In ZEves, these theorems could be written as \begin{theorem}{lNonMaxCup}[X] \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B \end{theorem} \begin{theorem}{catGen}[X] \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t \end{theorem} When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :(.... So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr? That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves throws back at you nonmaximal or maximal generics in places)..... :( .... any ideas? Best, Leo 
From: Tim Miller <tmiller@un...>  20110922 22:53:46

Hi Leo, That is definitely a violation of the standard, which allows only refnames. However, the parser is written as follows: inner_term:it LSQUARE expressionList:el RSQUARE:rsquare {: RESULT = factory_.createRefExpr(name(it), el, Boolean.FALSE, Boolean.TRUE); addLocAnn(RESULT, getLocation(it, rsquare)); :} This means that the grammar will allow the following: (A \cup B)[C] = A \cup B The CZT parser will report an error that a refname is expected for the generic instantiation when it calls name(it), and tries to cast the expression to a name. However, if this is for one of the dialects, you can easily add a new type of term to that dialect's schema, and then change the code body to create one of these terms. Tim On 22/09/11 18:39, Leo Freitas wrote: > Hi Tim, > > I am confused about the role of the "explicit" parameter in RefExpr. My understanding is that it is true when the user suplies the generics, and false otherwise. > That is because after type checking the ZExprList will contain (possibly nonmaximal) generics which the user don't want explicitly given on the terms. > > Is that right? Assuming it is, what about proofs / conjectures involving nonmaximal generics? Ex: > > \begin{theorem}{lNonMaxCup}[X] > \vdash? \forall C: \power~X @ \forall A, B: \power~C @ (\_ \cup \_)[C] (A,B) =A \cup B > \end{theorem} > > \begin{theorem}{catGen}[X] > \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ (\_\cat\_)[A] (s, t) = s \cat t > \end{theorem} > > In ZEves, these theorems could be written as > > \begin{theorem}{lNonMaxCup}[X] > \vdash? \forall C: \power~X @ \forall A, B: \power~C @ A \cup[C] B = A \cup B > \end{theorem} > > \begin{theorem}{catGen}[X] > \vdash? \forall A: \power~X @ \forall s, t: \seq~A @ s \cat[A] t = s \cat t > \end{theorem} > > When the expressions are large, it's rather ugly to need to write the whole thing with mixfix false :(.... > > So the question is, is there a way to have explicit generics mixfix=true appl expr or ref expr? > That is crucial, otherwise, translating legacy proofs or indeed doing new proofs (e.g., ZEves > throws back at you nonmaximal or maximal generics in places)..... :( .... any ideas? > > Best, > Leo 