On 29 Dec 2014, at 15:16, Rob Arthan <r...@lemma-one.com> wrote:

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

> ...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?

I don’t know what was going on here. The above error occurred repeatedly
before I made this posting but I can no longer reproduce it. Here, for
the record, is ProofPower-ML code to build QCheck and run David’s
example:

OS.FileSys.chDir "/Users/rda/bld/qcheck/qcheck-1.0/src”; (* change as 
appropriate *)
structure PPList = List;
structure List = SML97BasisLibrary.List;
PolyML.make (translate_for_output "QCheck");  (* or PolyML.make "%Q%Check"; *)
open %Q%Check;
fun checkSum n = n = n ; 
val int = (Gen.Int.int, SOME Int.toString) ;
checkGen int ("unit test", pred checkSum) ;

In the above “%Q%” lets you generate something whose underlying Standard ML
representation is single Q. The only additional wrinkle is that ProofPower
overwrites the Basis Library binding for the structure List, but it also keeps
a copy of the original so you can get it back again if you need it

Regards,

Rob.


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

Reply via email to