Re: [CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

[<an...@an...>]

Dear Julian

 

This seems to be a bug in the subset of CZT that is used in Z Word Tools. That is a very old snapshot of some  of the CZT code, and I’m trying to find out whether the bug is still present in the current version. If not, then I will update the Z Word Tools to incorporate the correct version. If so, I will need to wait for  the CZT project to fix the problem before updating the tools.

 

In the meantime, I think the bug is provoked by an error in your Z. I think perhaps you intended to declare r as ℙ (seq X) . If you do that, the typechecker works correctly (and identifies a subsequent problem with the application s <i>: that’s incorrect because s is a function from n to X, and you ae applying it to a sequence containing  just the number I as its first member).

 

I hope that helps, and I’ll get back to you when I have more information about the typechecker bug.

 

Regards

 

Anthony

 

From: Julian Rose [mailto:jro...@gm...] 
Sent: 29 May 2020 03:21
To: czt...@li...
Cc: Julian Rose
Subject: [CZT-Devel] bug report: net.sourceforge.czt.typecheck.z.PredChecker

 

Hei,

 

Summary.....: A general Throwable exception has happened - class net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl cannot be cast to class net.sourceforge.czt.z.ast.ProdType (net.sourceforge.czt.typecheck.z.impl.PowerTypeImpl and net.sourceforge.czt.z.ast.ProdType are in unnamed module of loader 'app')
Exception...: java.lang.ClassCastException
Cause.......: none

 

I use Microsoft Word 2007 with the plug-in ZWordTools Release 3.3.0.1 configured for CZT type-checking with option “Allow use before declaration”. 

 

The ZWordTools-generated temp.bat file contains (java -jar "C:\Users\Julian\AppData\Roaming\Microsoft\Word\STARTUP\ZWTools\cztinterface.jar" -d -t  "temp.zed8" > "temp.ztr" 2> "temp.zte")

Please see attached files.

Including a minimal temp.docx to reproduce the error.

The temp.ztr file is empty.

 

With thanks,

julian