Re: [CZT-Devel] explicit generics again

[Tim M. <tm...@un...>]

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 non-maximal) generics which the user don't want explicitly given on the terms.
>
> Is that right? Assuming it is, what about proofs / conjectures involving non-maximal 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