On 20/05/2012 11:48, Nicolai Schaffroth wrote:

I am currently working on integrating the QCheck/SML automatic unit testing library with the theorem prover Isabelle at TU M?nchen and automating the construction of random value generators. It would be very helpful to know if there is an internal representation of value and function types that can be accessed in some way other than parsing the string returned upon creation.

Thank you for any helpful information,

Nicolai

Not as such, at least at the moment. The best that is available is the pretty-print data structure which would reduce the amount of parsing you'd have to do. This is used to produce the actual string. An example is below.

David

Poly/ML 5.4.1 Release

PolyML.print_depth 1000;

val it = (): unit

val a = [1,2,3];

val a = [1, 2, 3]: int list

val aVal = valOf(#lookupVal PolyML.globalNameSpace "a");

val aVal = ?: PolyML.NameSpace.valueVal

PolyML.NameSpace.displayVal(aVal, 1000, PolyML.globalNameSpace);

val it = PrettyBlock (3, false, [], [PrettyBlock (0, false, [], [PrettyString "val", PrettyBreak (1, 0), PrettyBlock (0, false, [ContextLocation {file = "", endLine = 0, startLine = 0, endPosition = 0, startPosition = 0}], [PrettyString "a"]), PrettyBreak (1, 0), PrettyString "="]), PrettyBreak (1, 0), PrettyBlock (1, false, [], [PrettyString "[", PrettyString "1", PrettyString ",", PrettyBreak (1, 0), PrettyString "2", PrettyString ",", PrettyBreak (1, 0), PrettyString "3", PrettyString "]"]), PrettyString ":", PrettyBreak (1, 0), PrettyBlock (0, false, [], [PrettyBlock (0, false, [ContextLocation {file = "Standard Basis", endLine = 0, startLine = 0, endPosition = 0, startPosition = 0}], [PrettyString "int"]), PrettyBreak (1, 0), PrettyBlock (0, false, [ContextLocation {file = "Standard Basis", endLine = 0, startLine = 0, endPosition = 0, startPosition = 0}], [PrettyString "list"])])]): PolyML.pretty