I have just downloaded the latest CZT ide tool (version 2.0pre1) from the web site and would like to use it in my research.
I tried the IDE with an enhanced Birthday book example (see attached). However, the editor gave me the compile error: Undeclared name \poly
at the line in the schema MyBirthdayBook that uses the poly type "\poly BirthdayBook" .
I have just downloaded the latest CZT ide tool (version 2.0pre1) from the web site and would like to use it in my research.
I have tried the IDE with an enhanced Birthday book example (see below). However, the editor gave me the compile error: Undeclared name \poly
at the line in the schema MyBirthdayBook that uses the poly type "\poly BirthdayBook" .
I am primarily working with Object-Z in my current research project so it would be tremendous if CZT supports it.
Yes \poly (down arrow) is an Object-Z operator that creates a polymorphic type. It is available in the list of Object-Z character table of CZT ide.
Based on your suggestion, I noticed that there are two Z dialect compilers for Object-Z: oz and ozpatt. Both allowed me to use \poly exactly as you suggested.
However, there are new errors that occured.
For oz: the following error occured at line 1 (i.e. \documentclass)
Error in Z compiler: Can't find resource for bundle net.sourceforge.czt.typecheck.z.TypeCheckResources, key NON_REF_IN_POLYEXPR
For ozpatt, the following error occured at line 47 when i added a function named sameBook that uses the MyBirthdayBook class (see 1st attached file)
Implicit parameters not determined
Expression: { b2 . book }
The thing is that if I use the same code but without \poly (see 2nd attached file) then the code compiles no problems.
Just wanted to add that after restarting the ide with the compiler dialect set to 'oz', I got a different error message than the one given in the previous post. It is the same as the following error that was printed on the terminal when I run 'czt.jar ozedtypecheck' on the file:
"bbook_enhanced_latex.zed", line 35: Class reference required in polymorphic expression
Expression: \poly BirthdayBook
Type: \power [ known : \power NAME ; birthday : \power ( NAME \cross DATE ) ]
I guess the error posted previously was because I had not restarted the ide.
Do you have any suggestions?
Thanks,
Duc
Last edit: David Le 2016-04-08
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
CZT does have a fully fledged parser and type checker for OZ that is thoroughly tested, as far as I know.
Its integration with jEdit is also well made. The integration with Eclipse is what I was saying is primitive and hasn’t had (and is unlikely to have) much development.
Would you be interested in taking it up?
I would say, the best bet (and a trustworthy one) is the command line. But be careful to get the latest jar. The one you mentioned (in the next message) seems quite old.
The “can’t find resources” seems to me to indicate either you are using the wrong parser/typechecker, or a very old version of the jar. Have you tried building from sources?
ozpatt includes jokers/placeholder terms, so I unless you are in need of term rewriting (as done by Z-live), you shouldn’t use/worry about it.
I am not familiar enough with oz and its errors to give you feedback on why the error is happening. But, grep-ing the repository, you can see where \poly is used.
In particular, you should definitely look at CZT_HOME/typechecker/typechecker-oz/src. In there you will see
which does include NON_REF_IN_POLYEXPR, so if you are using the right tool, you shouldn’t see the “can’t find resource” error. More interestingly, look into
for examples of adequate and inadequate use of \poly.
Gripping the directory you will see other files with interesting use of \poly like
ClassUnionExpr.tex
Downcasting.tex
OID.tex
Hope this helps. I strongly recommend downloading and building from sources to get the latest jar. If you can’t do that, I could send you a link to it.
I am primarily working with Object-Z in my current research project so it would be tremendous if CZT supports it.
Yes \poly (down arrow) is an Object-Z operator that creates a polymorphic type. It is available in the list of Object-Z character table of CZT ide.
Based on your suggestion, I noticed that there are two Z dialect compilers for Object-Z: oz and ozpatt. Both allowed me to use \poly exactly as you suggested.
However, there are new errors that occured.
For oz: the following error occured at line 1 (i.e. \documentclass)
Error in Z compiler: Can't find resource for bundle net.sourceforge.czt.typecheck.z.TypeCheckResources, key NON_REF_IN_POLYEXPR
For ozpatt, the following error occured at line 47 when i added a function named sameBook that uses the MyBirthdayBook class (see 1st attached file)
Implicit parameters not determined
Expression: { b2 . book }
The thing is that if I use the same code but without \poly (see 2nd attached file) then the code compiles no problems.
Regarding to taking up the oz-eclipse integration challenge, I am very tempted to say 'Yes', given that it is such a useful feature. However, let me first have some time to play with OZ, in general, and with the existing czt tool, in particular to gain sufficient understanding. Also, I will need to organise my schedule because my current research project currently requires coding a Java framework, which is also a significant effort. I will let you know.
Please provide a link to download the latest source code that you mentioned. I assume the build process uses ant, correct?
I will also take a look at the examples that you mentioned to learn about how to use \poly; and also try the jEdit plugin that you mentioned.
I will let you know how I go.
Thank you very much.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Sure. Please do that. The extension within Eclipse shouldn’t be too much effort, but does require understanding how Eclipse works.
For instance, I started it for Circus (another Z extension) and managed to get the syntax highlight and other things in place quickly.
The build process uses maven, which is similar (but a bit more strict / annoying at times) to ant. You can get the sources from
Ah, I also played with your specification in the command line and apart from a few typos (i.e. it should be standard_toolkit instead of standard_toolkit; you need a new line in birthday etc), I get the error you refer to as
: czt $ java -jar czt.jar ozedtypecheck ~/Temp/test.tex
ERROR “~/Temp/test.tex", line 35, column 7: Class reference required in polymorphic expression
Expression: \poly BirthdayBook
Type: \power [ known : \power NAME ; birthday : \power ( NAME \cross DATE ) ]
And here, the error is correct: BirthdayBook is not a class but a schema, so it cannot be part of a polymorphic expression. This is just like the file in NonRefInPolyExpr-PolyExpr-1.error that I referred to when it says
Regarding to taking up the oz-eclipse integration challenge, I am very tempted to say 'Yes', given that it is such a useful feature. However, let me first have some time to play with OZ, in general, and with the existing czt tool, in particular to gain sufficient understanding. Also, I will need to organise my schedule because my current research project currently requires coding a Java framework, which is also a significant effort. I will let you know.
Please provide a link to download the latest source code that you mentioned. I assume the build process uses ant, correct?
I will also take a look at the examples that you mentioned to learn about how to use \poly; and also try the jEdit plugin that you mentioned.
Hi,
I have just downloaded the latest CZT ide tool (version 2.0pre1) from the web site and would like to use it in my research.
I tried the IDE with an enhanced Birthday book example (see attached). However, the editor gave me the compile error: Undeclared name \poly
at the line in the schema MyBirthdayBook that uses the poly type "\poly BirthdayBook" .
Is \poly currently supported?
Thanks very much for your help.
Last edit: David Le 2016-04-07
Hi
I guess poly is something from oz? Have you changed the compiler preferences to use the oz tools?
Mind you that support for Eclipse is mostly for Z and Zeves; very little on oz for syntax highlighting etc.
Best
Leo
On 7 Apr 2016, at 02:40, David Le dmle@users.sf.netamp#100;amp#109;amp#108;amp#101;amp#64;amp#117;amp#115;amp#101;amp#114;amp#115;amp#46;amp#115;amp#102;amp#46;amp#110;amp#101;amp#116; wrote:
Hi,
I have just downloaded the latest CZT ide tool (version 2.0pre1) from the web site and would like to use it in my research.
I have tried the IDE with an enhanced Birthday book example (see below). However, the editor gave me the compile error: Undeclared name \poly
at the line in the schema MyBirthdayBook that uses the poly type "\poly BirthdayBook" .
Is \poly currently supported?
Thanks very much for your help.
===============================
\documentclass{article}
\usepackage{czt}
\begin{document}
This is the enhanced BirthdayBook specification.
\section{Main}
\begin{zsection}
\SECTION Main \parents standard_toolkit, oz_toolkit
\end{zsection}
\begin{zed}
[NAME, ~ DATE]
\end{zed}
The $BirthdayBook$ schema defines the \emph{state space} of the birthday book system.
\begin{schema}{BirthdayBook}
known: \power NAME \
birthday: NAME \pfun DATE
\where
known=\dom birthday
\end{schema}
$RestrictedBirthdayBook$ is a sub-type of birthday book that contains at most 100 entries.
\begin{schema}{RestrictedBirthdayBook}
BirthdayBook
\where
~known \leq 100
\end{schema}
$MyBirthdayBook$ is a collection of all types of birthday books
\begin{schema}{MyBirthdayBook}
book : \poly BirthdayBook
\end{schema}
\end{document}
===============================
Error: Undeclared name \polyhttps://sourceforge.net/p/czt/discussion/295268/thread/1e4d6310/?limit=25#f514
Sent from sourceforge.nethttp://sourceforge.net because you indicated interest in https://sourceforge.net/p/czt/discussion/295268/
To unsubscribe from further messages, please visit https://sourceforge.net/auth/subscriptions/
Hi Leo,
Thank you very much for your response.
I am primarily working with Object-Z in my current research project so it would be tremendous if CZT supports it.
Yes \poly (down arrow) is an Object-Z operator that creates a polymorphic type. It is available in the list of Object-Z character table of CZT ide.
Based on your suggestion, I noticed that there are two Z dialect compilers for Object-Z: oz and ozpatt. Both allowed me to use \poly exactly as you suggested.
However, there are new errors that occured.
For oz: the following error occured at line 1 (i.e. \documentclass)
Error in Z compiler: Can't find resource for bundle net.sourceforge.czt.typecheck.z.TypeCheckResources, key NON_REF_IN_POLYEXPR
For ozpatt, the following error occured at line 47 when i added a function named sameBook that uses the MyBirthdayBook class (see 1st attached file)
Implicit parameters not determined
Expression: { b2 . book }
The thing is that if I use the same code but without \poly (see 2nd attached file) then the code compiles no problems.
Thank you very much for your help.
Hi Leo,
Just wanted to add that after restarting the ide with the compiler dialect set to 'oz', I got a different error message than the one given in the previous post. It is the same as the following error that was printed on the terminal when I run 'czt.jar ozedtypecheck' on the file:
java -jar czt_1_5_0_bin.jar ozedtypecheck bbook_enhanced_latex.zed
"bbook_enhanced_latex.zed", line 35: Class reference required in polymorphic expression
Expression: \poly BirthdayBook
Type: \power [ known : \power NAME ; birthday : \power ( NAME \cross DATE ) ]
I guess the error posted previously was because I had not restarted the ide.
Do you have any suggestions?
Thanks,
Duc
Last edit: David Le 2016-04-08
Hi,
CZT does have a fully fledged parser and type checker for OZ that is thoroughly tested, as far as I know.
Its integration with jEdit is also well made. The integration with Eclipse is what I was saying is primitive and hasn’t had (and is unlikely to have) much development.
Would you be interested in taking it up?
I would say, the best bet (and a trustworthy one) is the command line. But be careful to get the latest jar. The one you mentioned (in the next message) seems quite old.
The “can’t find resources” seems to me to indicate either you are using the wrong parser/typechecker, or a very old version of the jar. Have you tried building from sources?
ozpatt includes jokers/placeholder terms, so I unless you are in need of term rewriting (as done by Z-live), you shouldn’t use/worry about it.
I am not familiar enough with oz and its errors to give you feedback on why the error is happening. But, grep-ing the repository, you can see where \poly is used.
In particular, you should definitely look at CZT_HOME/typechecker/typechecker-oz/src. In there you will see
main/resources/net/sourceforge/czt/typecheck/oz/ErrorMessage_en.properties
which does include NON_REF_IN_POLYEXPR, so if you are using the right tool, you shouldn’t see the “can’t find resource” error. More interestingly, look into
test/resources/oz/PolyExpr.tex
test/resources/oz/NonRefInPolyExpr-PolyExpr-1.error
test/resources/oz/NonRefInPolyExpr-PolyExpr-2.error
for examples of adequate and inadequate use of \poly.
Gripping the directory you will see other files with interesting use of \poly like
ClassUnionExpr.tex
Downcasting.tex
OID.tex
Hope this helps. I strongly recommend downloading and building from sources to get the latest jar. If you can’t do that, I could send you a link to it.
Best,
Leo
Hi Leo,
Regarding to taking up the oz-eclipse integration challenge, I am very tempted to say 'Yes', given that it is such a useful feature. However, let me first have some time to play with OZ, in general, and with the existing czt tool, in particular to gain sufficient understanding. Also, I will need to organise my schedule because my current research project currently requires coding a Java framework, which is also a significant effort. I will let you know.
Please provide a link to download the latest source code that you mentioned. I assume the build process uses ant, correct?
I will also take a look at the examples that you mentioned to learn about how to use \poly; and also try the jEdit plugin that you mentioned.
I will let you know how I go.
Thank you very much.
Hi David,
Sure. Please do that. The extension within Eclipse shouldn’t be too much effort, but does require understanding how Eclipse works.
For instance, I started it for Circus (another Z extension) and managed to get the syntax highlight and other things in place quickly.
The build process uses maven, which is similar (but a bit more strict / annoying at times) to ant. You can get the sources from
git clone git://git.code.sf.net/p/czt/code czt-code
or https://sourceforge.net/p/czt/code/ci/master/tree/
I just built it locally and the (6.8MB) czt.jar file is here https://www.dropbox.com/s/z88gifvelnus5y9/czt.jar?dl=0
Ah, I also played with your specification in the command line and apart from a few typos (i.e. it should be standard_toolkit instead of standard_toolkit; you need a new line in birthday etc), I get the error you refer to as
And here, the error is correct: BirthdayBook is not a class but a schema, so it cannot be part of a polymorphic expression. This is just like the file in NonRefInPolyExpr-PolyExpr-1.error that I referred to when it says
\begin{axdef}
x : \poly \nat
\end{axdef}
Best,
Leo
Hi Leo,
You are right! I should have declared the types using the \begin{class}...\end{class} construct.
I fixed it (see attached file) and the code is compiled fine.
And yes syntax highlight does not work for the Object-Z part.
I will keep using the 2.0-pre1 version for now. Hope that is sufficient for my need.
Thanks very much.