Re: [CZT-Users] Working with the predicate from the AST

[Petra M. <Pet...@ec...>]

Hi Paulo,

You wrote:
> [...] I was able to retrieve most of the predicate by
> doing some interpretation of how it is generated but for a few
> predicates there were some parts missing.
> 
> For instance in the schema:
> 
> \begin{schema}{Remind}
>   \Xi BirthdayBook \\
>   today?: DATE \\
>   cards!: \power NAME
> \where
>   cards! = \{ n: known | birthday(n) = today? \}
> \end{schema}

To see how this gets translated into an AST, it might help to look at
the corresponding XML.  You can use the czt tools to translate a latex
file into XML, or have a look at
zml/src/main/resources/net/sourceforge/czt/zml/examples/z/birthdaybook.xml
(in your CZT directory).

Note that "cards! = \{ n: known | birthday(n) = today? \}" gets
transformed into "cards! \in \{\{ n: known | birthday(n) = today? \}\}",
which is equivalent.  That's why the predicate part of the schema is a
membership (MemPred).

> I got the structure:
> 
> net.sourceforge.czt.z.impl.MemPredImpl
>     net.sourceforge.czt.z.base.impl.ListTermImpl
>         net.sourceforge.czt.z.impl.RefExprImpl
>             cards!
>         net.sourceforge.czt.z.impl.SetExprImpl
>             net.sourceforge.czt.z.impl.ZExprListImpl
>                 net.sourceforge.czt.z.impl.SetCompExprImpl

Here is the corresponding bit of the ZML that shows what's inside this
SetCompExpr:

    <SetCompExpr>
      <ZSchText>
         <ZDeclList>
           <VarDecl>
             <ZNameList>
               <ZName>
                 <Word>n</Word>
                 <ZStrokeList/>
               </ZName>
             </ZNameList>
             <RefExpr Mixfix="false" Explicit="false">
               <ZName>
                 <Word>known</Word>
                 <ZStrokeList/>
               </ZName>
               <ZExprList/>
             </RefExpr>
             ...

So the SetCompExpr should have a method getSchText() which gives you the
ZSchText.  ZSchText in turn should have a method getDeclList() etc.

> I have tried using some print methods from the package such as the
> net.sourceforge.czt.print.z.PrintUtils.printLatex(term, writer, manager)
> but I could only print the whole specification and wasn't able to print
> a predicate from a single schema.

Try providing the section manager that you've used for parsing the
specification as well as the section name the predicate is defined in.
The problem with printing just a predicate is that it might contain user
defined operators, and their operator definition needs to be looked up.

If you need more help with this, maybe provide your source code so we
can have a look at it.  You should also tell us which CZT version you
are using.

Hope this helps,
Petra