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

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

Hi Pablo,

I've had a quick look at this. It seems like a fault in the typechecker. 
I haven't got the time to look at it at the moment. Could you please 
submit a bug report at http://sourceforge.net/projects/czt/support? I'll 
take a closer look when I get the chance.

Thanks,
Tim

Pablo Rodriguez Monetti wrote:
> Hi czt'ers,
> 
> I had a problem trying to load an specification with uses before 
> declarations. In general, this kind of models are supported. For 
> example, I could correctly load the following specification:
> 
> \begin{zed}
> Integers == Positives \lor Negatives \lor Zero
> \end{zed}
> 
> \begin{zed}
> Positives == [a: \nat | a > 0] \\
> Negatives == [a: \nat | a < 0] \\
> Zero == [a: \nat | a = 0] \\
> \end{zed}
> 
> However, the following one could not be loaded in the given order:
> 
> \begin{gendef}[X]
> optional:\power X \fun \power (\power X)\\
> \end{gendef}
> 
> \begin{zed}
> FFName == String \{2\}\\
> \end{zed}
> 
> \begin{schema}{FF}
> name: FFName\\
> \end{schema}
> 
> \begin{schema}{NI}
> hI: optional~HI\\
> \end{schema}
> 
> \begin{schema}{HI}
> hF:FF\\
> \end{schema}
> 
> \begin{zed}
> STRING == \seq \nat \\
> \end{zed}
> 
> \begin{axdef}
> String : \power(\nat) \fun \power(STRING) \\
> \end{axdef}
> 
> reporting the following error:
> 
> "ubf2.tex", line 13: Implicit parameters not determined
>     Expression: optional
> 
> It's very sensitive to exactly what the declaration sequence is. For 
> example, if I change the declaration of FFName from String{2} to STRING, 
> it works fine. If I reorder the specification appropriately, it works 
> fine too.
> 
> Cheers,
> 
> Pablo
> 
> 
> 
> 
> 
> On Tue, Jun 1, 2010 at 3:13 PM, Pablo Rodriguez Monetti 
> <rod...@gm... <mailto:rod...@gm...>> wrote:
> 
>     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...
>     <mailto: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...>
>             <mailto: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...>
>                    <mailto:CZT...@li...
>             <mailto:CZT...@li...>>
> 
>                    https://lists.sourceforge.net/lists/listinfo/czt-users
> 
> 
> 
> 
> 
>