Menu
▾
▴
Re: [CZT-Users] Loading specs with uses of variables before their declaration
|
From: Pablo R. M. <rod...@gm...> - 2010-07-07 15:37:19
|
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...> 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...>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
>>>
>>>
>>>
>>>
>>
>
|
