Term (nholz)

Term Module

Namespace: HOL
Assembly: nholz.dll

This module defines the internal representation of HOL terms. This is done by defining an abstract datatype for terms, and then primitive syntax functions for constructing and destructing terms, and support for constant declaration. The primitive syntax constructors ensure that only well- formed terms can be constructed. This module is a trusted component of the system.

Types

Type	Description
term	This is the datatype for internal HOL terms. It has 4 classes, corresponding to the 4 primitive syntactic categories of term: Variable - This denotes an occurrence of a variable. It has name and type attributes. Any two occurrences of variables within a given object refer the same entity iff they have the same name, type and scope. Constant - This denotes an occurrence of a constant. It has name and type attributes, where the name must be a declared constant's name and the type must match the declared constant's generic type. Function Application - This consists of a function subterm and an argument subterm, where the function's type must be a function type with domain type equal to the argument's type. Lambda Astraction - This consists of a binding variable and a body subterm. It bounds the scope of the binding variable to the body, and this is the only primitive means of bounding variable scope.

Type

Description

term

This is the datatype for internal HOL terms. It has 4 classes, corresponding to the 4 primitive syntactic categories of term:

Variable - This denotes an occurrence of a variable. It has name and type attributes. Any two occurrences of variables within a given object refer the same entity iff they have the same name, type and scope.

Constant - This denotes an occurrence of a constant. It has name and type attributes, where the name must be a declared constant's name and the type must match the declared constant's generic type.

Function Application - This consists of a function subterm and an argument subterm, where the function's type must be a function type with domain type equal to the argument's type.

Lambda Astraction - This consists of a binding variable and a body subterm. It bounds the scope of the binding variable to the body, and this is the only primitive means of bounding variable scope.

Functions and values

Function or value	Description
`dest_abs tm` Full Usage: `dest_abs tm` Parameters: tm : `term` Returns: `term * term`	Takes a lambda abstraction term and returns its component terms. Fails if the supplied term is not a lambda abstraction. tm : `term` Returns: `term * term`
`dest_comb tm` Full Usage: `dest_comb tm` Parameters: tm : `term` Returns: `term * term`	Takes a function application term and returns its component terms. Fails if the spupplied term is not a function application. tm : `term` Returns: `term * term`
`dest_const tm` Full Usage: `dest_const tm` Parameters: tm : `term` Returns: `string * hol_type`	Takes a constant term and returns its name and type. Fails if the supplied term is not a constant. tm : `term` Returns: `string * hol_type`
`dest_var tm` Full Usage: `dest_var tm` Parameters: tm : `term` Returns: `string * hol_type`	Takes a variable term and returns its name and type. Fails if the supplied term is not a variable. tm : `term` Returns: `string * hol_type`
`get_all_consts ()` Full Usage: `get_all_consts ()` Parameters: () : `unit` Returns: `(string * hol_type) list`	Returns the name and generic type of each declared constant. () : `unit` Returns: `(string * hol_type) list`
`get_const_gtype x` Full Usage: `get_const_gtype x` Parameters: x : `string` Returns: `hol_type`	Returns the generic type of the constant with the supplied name. Fails if the costant has not been declared x : `string` Returns: `hol_type`
`is_abs tm` Full Usage: `is_abs tm` Parameters: tm : `term` Returns: `bool`	Checks if a term is a function application term. tm : `term` Returns: `bool`
`is_comb tm` Full Usage: `is_comb tm` Parameters: tm : `term` Returns: `bool`	Checks if a term is a function application term. tm : `term` Returns: `bool`
`is_const tm` Full Usage: `is_const tm` Parameters: tm : `term` Returns: `bool`	Checks if a term is a constant term tm : `term` Returns: `bool`
`is_const_name x` Full Usage: `is_const_name x` Parameters: x : `string` Returns: `bool`	The test for whether a given name is the name of a declared constant. x : `string` Returns: `bool`
`is_var tm` Full Usage: `is_var tm` Parameters: tm : `term` Returns: `bool`	Checks if a term is a variable term tm : `term` Returns: `bool`
`mk_abs (v, tm0)` Full Usage: `mk_abs (v, tm0)` Parameters: v : `term` tm0 : `term` Returns: `term`	The primitive constructor for lambda abstraction checks that the supplied binding variable is indeed a variable. Fails if the first term is not a variable term v : `term` tm0 : `term` Returns: `term`
`mk_comb (tm1, tm2)` Full Usage: `mk_comb (tm1, tm2)` Parameters: tm1 : `term` tm2 : `term` Returns: `term`	The primitive constructor for function application checks that the type of the supplied function term is a function type with a domain type equal to the type of the argument term. Fails if the first term is not a function or if the domain of the function is not equal to the argument type. tm1 : `term` tm2 : `term` Returns: `term`
`mk_gconst x` Full Usage: `mk_gconst x` Parameters: x : `string` Returns: `term`	Takes a constant name that has already been declared and returns a constant term. Fails if the supplied constant name has not been declared. x : `string` Returns: `term`
`mk_iconst (x, tytheta)` Full Usage: `mk_iconst (x, tytheta)` Parameters: x : `string` tytheta : `(hol_type * hol_type) list` Returns: `term`	Takes a constant name and an old-to-new tyvar instantiation list, and returns the constant term with its generic type's tyvars instantiated accordingly. Note that the instantiation domain is allowed to contain tyvars that are not in the generic type: these are just ignored. Fails if the constant has not been declared. x : `string` tytheta : `(hol_type * hol_type) list` Returns: `term`
`mk_var (x, ty)` Full Usage: `mk_var (x, ty)` Parameters: x : `string` ty : `hol_type` Returns: `term`	Takes a name and a type , with no restrictions on these arguments: any name can be used for a variable, including the name of a declared constant. x : `string` ty : `hol_type` Returns: `term`
`prim_new_const (x, ty)` Full Usage: `prim_new_const (x, ty)` Parameters: x : `string` ty : `hol_type`	This is the primitive declaration command for constants. It takes a string and a type: the string becomes the name of a new constant in the theory, and the type becomes its generic type. Any name can be used for a constant, but supplying an existing constant's name will cause failure. A note of the declaration is reported, and unit is returned. x : `string` ty : `hol_type`
`term_eq x y` Full Usage: `term_eq x y` Parameters: x : `term` y : `term` Returns: `bool`	x : `term` y : `term` Returns: `bool`
`term_lt x y` Full Usage: `term_lt x y` Parameters: x : `term` y : `term` Returns: `bool`	x : `term` y : `term` Returns: `bool`
`the_consts` Full Usage: `the_consts` Returns: `dltree<string, hol_type> ref`	Returns: `dltree<string, hol_type> ref`
`type_of tm` Full Usage: `type_of tm` Parameters: tm : `term` Returns: `hol_type`	A term's type is calculated ultimately from the types of its constituent atoms. Although potentially a derived utility, it is defined as a primitive for use in 'mk_comb'. tm : `term` Returns: `hol_type`