David,

On 28 Dec 2014, at 05:08, David Topham <dtop...@gmail.com> wrote:

> I am not sure if this is a bug in xpp or if it is a user (me!) error, but I 
> am trying to use a unit test framework named QCheck within xpp and it fails. 
> I have attached the doc file and the sml and pdf file produced via docsml. In 
> the files, I have shown where the error occurs. Since it works ok in poly, 
> then I expected it to also work within xpp so I am asking if anyone has tried 
> this; or sees why it may not work as I expect.
> 

The problem is not with xpp but with the extensions to Standard ML that 
ProofPower uses
to provide object language quotations and support an extended character set for 
use in forming
ML names (so we can use mathematical symbols to form ML names). The extended 
language is
called ProofPower-ML. When you run xpp with a command line something like:

        xpp -d hol
or
        xpp UT.doc -d zed

xpp just spawns a process running the command “pp -d hol” or “pp -d zed” which 
invokes
a session on the hol or zed database and communicates with that process via a
UN*X pseudo-terminal. Unless you do something special, “pp -d XYZ” will 
run the ProofPower-ML read-eval-print loop. ProofPower-ML is implemented by
a pre-processor that encodes it into ASCII Standard ML  and a post-processor
that converts the ASCII output from the ML compiler’s eval-print function
into the extended character set.

Your problem is then occurring because we use “Q” to encode
non-ASCII characters, “Q” itself being encoded as “QQQQ”. So somewhat
bizarrely, you will find that:

        size “QCheck” 

evaluates to 9 in ProofPower-ML. PolyML.make expects a Standard ML
string, rather than a ProofPower-ML string, so it can’t find the file and
raises an error.

If you just want to use xpp as a user interface to Poly/ML and you don’t want
the ProofPower specification and theorem-proving tools, then you can
ask xpp to run a different command line. E.g.,

        xpp -c poly

or

        xpp -f UT.doc -c poly

will bring up xpp talking to a poly session (and editing a new empty file
in the first case and the file UT.doc in the second). (Note that for
not very good reasons, the command line requires -f before the
name of the file to edit when you use -c.)

(You can actually change the command line within one xpp session if  you
like using Tools/Options, but I don’t think you are likely to want that.)

If you want the ProofPower tools, then you can reverse the encoding
using the function translate_for_output:

        PolyML.make(translate_for_output “QCheck”);

or you can switch between ProofPower-ML and Standard ML using
the commands abandon_reader_writer() (ProofPower-ML -> Standard ML)
and use_terminal() (Standard ML -> ProofPower-ML).

However, I don’t get much further with QCheck. Even when I try to load
it directly from poly, I get the following error message:

> PolyML.make "QCheck";
Making QCheck
Making QCheckVersion
Created structure QCheckVersion
structure QCheckVersion :
  sig val context : string val version : int * int end
Error- in 'QCheck.sml', line 14.
Structure (RandGen) has not been declared Found near RandGen

Did you have to do something else to QCheck to get it to work?

Regards,

Rob.

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to