view_struct
smlOpen.view_struct : string -> (string list * string list * string list * string list)
Shows SML identifiers included in a structure (or substructure) s.
The first field contains values, the second exceptions (i.e Match), the third constructions (i.e SOME) and the fourth substructures. This output is computed by inspecting PolyML.globalNameSpace () in an external HOL4 environment.
Failure
Fails if the structure s cannot be loaded by a script in the directory
src/AI/sml_inspection/open.
Example
> load "smlOpen"; open smlOpen;
val it = (): unit
> view_struct "Math";
val it =
(["sin", "sinh", "cos", "tan", "cosh", "e", "asin", "tanh", "atan2", "ln",
"acos", "log10", "pi", "sqrt", "atan", "exp", "pow"], [], [], []):
string list * string list * string list * string list
> view_struct "HolKernel.Definition";
val it =
(["new_definition", "new_specification", "located_new_type_definition",
"located_new_definition", "gen_new_specification",
"located_new_specification", "new_definition_hook",
"new_type_definition", "located_gen_new_specification"], [], [], []):
string list * string list * string list * string list
Comments
Including a Holmakefile in the directory src/AI/sml_inspection/open
with the line INCLUDES = path-to-your-structure should remove the
requirement for the structure to be in sigobj.