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

[Pablo R. M. <rod...@gm...>]

Hi Tim,

You are right! The problem was that I was mistakenly expecting the
typecheck() method to throw an exception whenever there was an error (like I
did with manager.get() ) and forgot to check the return value :S

However, a few weeks ago, I cloned and "manually" modify the AST structure
of an AxPara (conjugating its predicate to a given predicate P, to typecheck
P in the context of the variables declared in the AxPara) and when I wanted
to typecheck the resulting AxPara, calling typecheck() with the AxPara
object failed to find errors while calling the method with the SchExpr
associated to the AxPara was successful (ie. it found errors, if any).
That's why I believed that the typecheck() method failed with some types of
terms and was ok with others.

Many thanks!

Pablo


On Mon, May 31, 2010 at 8:19 PM, Tim Miller <tm...@un...> wrote:

> 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
>>
>>
>>
>>
>