smlOpen.view

STRUCTURE

SYNOPSIS

Shows SML identifiers included in a structure (or substructure) s.

DESCRIPTION

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;
(* output omitted *)
> 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

(* viewing substructures is also possible *)
- view_struct "HolKernel.Definition";
val it =
   (["new_definition", "new_specification", "gen_new_specification",
     "new_definition_hook", "new_type_definition"], [], [], []):
   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.

SEEALSO

quse_string, exec_script