Re: [CZT-Users] Loading specs with uses of variables before their declaration

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

Hi Pablo,

Can you post the example that you are trying to typecheck?

If I use the source code that you pasted into your email, everything 
seems to work ok for me. I have the following example:

\begin{zed}
  x == y
\end{zed}

\begin{zed}
  y == 1
\end{zed}

\begin{axdef}
  \where
  x \in y
\end{axdef}

in which 'y' is used before it is declared, and there is a type mismatch 
in the axdef. If I compile and run the following code, it reports the 
type mismatch, but not the use before declaration:

import java.util.List;

import net.sourceforge.czt.typecheck.z.*;
import net.sourceforge.czt.z.ast.*;
import net.sourceforge.czt.session.*;

public class Test
{

   public static void main(String [] args) throws Exception
   {
     String fileName = "usebeforedecl.tex";
     Source source = new FileSource(fileName);
     SectionManager manager = new SectionManager();
     manager.put(new Key(fileName, Source.class), source);
     Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
     List<? extends ErrorAnn> errors =
       TypeCheckUtils.typecheck(spec, manager, true);

     for (ErrorAnn error : errors) {
       System.out.println(error);
     }
   }
}


If I set the use before declaration flag to false, it reports both.

Can you try this and see what you get?

Thanks,
Tim

Pablo Rodriguez Monetti wrote:
> Hi Tim,
> 
> Many thanks for your answer!
> 
> I have tried with the typecheck() method, passing as first argument an 
> Spec object:
> 
>             Source source = new FileSource(fileName);
>             SectionManager manager = new SectionManager();
>             manager.put(new Key(fileName, Source.class), source);
>             Spec spec = (Spec) manager.get(new Key(fileName, Spec.class));
>             TypeCheckUtils.typecheck(spec, manager, true);
> 
> but it fails to detect type errors. As I could see, this method works 
> well with Expr and Pred terms, but fails with Spec and Para terms, among 
> others.
> 
> Previously, I was loading my specifications with a piece of code similar 
> to this:
> 
>              Source source = new FileSource(filename);
>              manager.put(new Key<Source>(filename, Source.class), source);
>              Spec spec = (Spec) manager.get(key);
>              String sectName = null;
>              for (Sect sect : spec.getSect()) {
>                   if (sect instanceof ZSect) {
>                        sectName = ((ZSect) sect).getName();
>                        Key<SectTypeEnvAnn> typekey =
>                        new Key<SectTypeEnvAnn>(sectName, 
> SectTypeEnvAnn.class);
>                        manager.get(typekey);
>                   }
>              }
> 
> but it fails to load specs with uses of variables before their declarations.
> 
> Any suggestion?
> 
> Cheers,
> 
> Pablo
> 
> 
> 
> 
> On Sun, May 30, 2010 at 3:58 AM, Tim Miller <tm...@un... 
> <mailto:tm...@un...>> wrote:
> 
>     Hi Pablo,
> 
>     The TypeCheckUtils class contains an overloaded static methods
>     called "typecheck". The one you want is:
> 
>      typecheck(Term term, SectionManager sectInfo, boolean useBeforeDecl)
> 
>     Set useBeforeDecl to "true" if you want to enable the use of
>     variables before declaration. There are several other "typecheck"
>     methods in the same class that also do this, but which offer several
>     other properties as well.
> 
>     Regards,
>     Tim
> 
>     Pablo Rodriguez Monetti wrote:
> 
>         Hi Czt'ers,
> 
>         I would like to know if there is any way to load, through the
>         CZT API, Z specifications that have uses of variables before
>         their declaration. With "load" I mean parse the specifications
>         as well as typeckeck them. The desired behaviour would be like
>         the the one provided by the -d (dependency analysis) feature of
>         fuzz.
> 
>         Cheers,
> 
>         Pablo Rodríguez Monetti
> 
> 
>         ------------------------------------------------------------------------
> 
>         ------------------------------------------------------------------------------
> 
> 
> 
>         ------------------------------------------------------------------------
> 
>         _______________________________________________
>         CZT-Users mailing list
>         CZT...@li...
>         <mailto:CZT...@li...>
>         https://lists.sourceforge.net/lists/listinfo/czt-users
> 
> 
>