Preterm (nholz)

Preterm Module

Namespace: HOL
Assembly: nholz.dll

This module defines the pretype and preterm datatypes (called 'pretype' and 'preterm'), and various basic operations on them. These are used during parsing and printing as intermediate representations of types/terms between their quotation and internal representations. They incorporate extra datatype classes, that don't occur in the corresponding internal datatypes and are only used during parsing and printing. Being intermediate datatypes, there is no need for well-formedness restrictions on their constructors, and so the datatypes are not made abstract.

Types

Type	Description
preterm
pretype	This is the datatype for the intermediate representation of HOL types. It includes an extra class for "generated tyvars", used in term parsing and printing as a temporary placeholder for an as-yet-undetermined type (whereas "conventional tyvars" come from user annotations and internal types and are fixed for the purposes of parsing and printing). Generated tyvars have a number attribute. This is by default '0', which imparts no information, but gets assigned a unique non-zero value during preterm detyping (see 'TypeAnal' module).

Functions and values

Function or value	Description
`atom_preterm_name ptm` Full Usage: `atom_preterm_name ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`bool_bin_pty` Full Usage: `bool_bin_pty` Returns: `pretype`	Returns: `pretype`
`bool_pty` Full Usage: `bool_pty` Returns: `pretype`	Returns: `pretype`
`cond_fn` Full Usage: `cond_fn` Returns: `preterm`	Returns: `preterm`
`const_preterm_name ptm` Full Usage: `const_preterm_name ptm` Parameters: ptm : `preterm` Returns: `string`	ptm : `preterm` Returns: `string`
`dest_abs_preterm ptm` Full Usage: `dest_abs_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm`	ptm : `preterm` Returns: `preterm * preterm`
`dest_bigint_nat_preterm ptm` Full Usage: `dest_bigint_nat_preterm ptm` Parameters: ptm : `preterm` Returns: `BigInteger`	ptm : `preterm` Returns: `BigInteger`
`dest_bigint_nat_preterm0 zok ptm` Full Usage: `dest_bigint_nat_preterm0 zok ptm` Parameters: zok : `bool` ptm : `preterm` Returns: `BigInteger`	zok : `bool` ptm : `preterm` Returns: `BigInteger`
`dest_bin_preterm ptm` Full Usage: `dest_bin_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm * preterm`	ptm : `preterm` Returns: `preterm * preterm * preterm`
`dest_bin_preterm0 f0 ptm` Full Usage: `dest_bin_preterm0 f0 ptm` Parameters: f0 : `preterm` ptm : `preterm` Returns: `preterm * preterm`	f0 : `preterm` ptm : `preterm` Returns: `preterm * preterm`
`dest_binder_preterm ptm` Full Usage: `dest_binder_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm * preterm`	ptm : `preterm` Returns: `preterm * preterm * preterm`
`dest_comb_preterm ptm` Full Usage: `dest_comb_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm`	ptm : `preterm` Returns: `preterm * preterm`
`dest_cond_preterm ptm` Full Usage: `dest_cond_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm * preterm`	ptm : `preterm` Returns: `preterm * preterm * preterm`
`dest_enum_preterm ptm` Full Usage: `dest_enum_preterm ptm` Parameters: ptm : `preterm` Returns: `string * preterm list * string`	ptm : `preterm` Returns: `string * preterm list * string`
`dest_fun_pretype pty` Full Usage: `dest_fun_pretype pty` Parameters: pty : `pretype` Returns: `pretype * pretype`	pty : `pretype` Returns: `pretype * pretype`
`dest_gtyvar_pretype pty` Full Usage: `dest_gtyvar_pretype pty` Parameters: pty : `pretype` Returns: `int`	pty : `pretype` Returns: `int`
`dest_infix_pretype pty` Full Usage: `dest_infix_pretype pty` Parameters: pty : `pretype` Returns: `string * pretype * pretype`	pty : `pretype` Returns: `string * pretype * pretype`
`dest_let_preterm ptm` Full Usage: `dest_let_preterm ptm` Parameters: ptm : `preterm` Returns: `(preterm * preterm) list * preterm`	ptm : `preterm` Returns: `(preterm * preterm) list * preterm`
`dest_tyvar_pretype pty` Full Usage: `dest_tyvar_pretype pty` Parameters: pty : `pretype` Returns: `string`	pty : `pretype` Returns: `string`
`dest_var_preterm ptm` Full Usage: `dest_var_preterm ptm` Parameters: ptm : `preterm` Returns: `string * pretype`	ptm : `preterm` Returns: `string * pretype`
`is_atom_preterm ptm` Full Usage: `is_atom_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_binder_preterm ptm` Full Usage: `is_binder_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_cond_preterm ptm` Full Usage: `is_cond_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_enum_preterm ptm` Full Usage: `is_enum_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_gtyvar_pretype pty` Full Usage: `is_gtyvar_pretype pty` Parameters: pty : `pretype` Returns: `bool`	pty : `pretype` Returns: `bool`
`is_infix_preterm ptm` Full Usage: `is_infix_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_let_preterm ptm` Full Usage: `is_let_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_nat_preterm ptm` Full Usage: `is_nat_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_pair_preterm ptm` Full Usage: `is_pair_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_postfix_preterm ptm` Full Usage: `is_postfix_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_prefix_preterm ptm` Full Usage: `is_prefix_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`is_typed_preterm ptm` Full Usage: `is_typed_preterm ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`let_fn` Full Usage: `let_fn` Returns: `preterm`	Returns: `preterm`
`list_mk_abs_preterm (vs, ptm0)` Full Usage: `list_mk_abs_preterm (vs, ptm0)` Parameters: vs : `preterm list` ptm0 : `preterm` Returns: `preterm`	vs : `preterm list` ptm0 : `preterm` Returns: `preterm`
`list_mk_bin_preterm h f ptms` Full Usage: `list_mk_bin_preterm h f ptms` Parameters: h : `assochand` f : `preterm` ptms : `preterm list` Returns: `preterm`	h : `assochand` f : `preterm` ptms : `preterm list` Returns: `preterm`
`list_mk_binder_preterm (f, vs, ptm0)` Full Usage: `list_mk_binder_preterm (f, vs, ptm0)` Parameters: f : `preterm` vs : `preterm list` ptm0 : `preterm` Returns: `preterm`	f : `preterm` vs : `preterm list` ptm0 : `preterm` Returns: `preterm`
`list_mk_comb_preterm (f, ptms)` Full Usage: `list_mk_comb_preterm (f, ptms)` Parameters: f : `preterm` ptms : `preterm list` Returns: `preterm`	f : `preterm` ptms : `preterm list` Returns: `preterm`
`list_mk_pair_preterm ptms` Full Usage: `list_mk_pair_preterm ptms` Parameters: ptms : `preterm list` Returns: `preterm`	ptms : `preterm list` Returns: `preterm`
`mk_bigint_nat_preterm n` Full Usage: `mk_bigint_nat_preterm n` Parameters: n : `BigInteger` Returns: `preterm`	n : `BigInteger` Returns: `preterm`
`mk_bigint_nat_preterm0 n` Full Usage: `mk_bigint_nat_preterm0 n` Parameters: n : `BigInteger` Returns: `preterm`	n : `BigInteger` Returns: `preterm`
`mk_bin_preterm (ptmf, ptm1, ptm2)` Full Usage: `mk_bin_preterm (ptmf, ptm1, ptm2)` Parameters: ptmf : `preterm` ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`	ptmf : `preterm` ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`
`mk_bin_pretype (x, ptm1, ptm2)` Full Usage: `mk_bin_pretype (x, ptm1, ptm2)` Parameters: x : `string` ptm1 : `pretype` ptm2 : `pretype` Returns: `pretype`	x : `string` ptm1 : `pretype` ptm2 : `pretype` Returns: `pretype`
`mk_binder_preterm (f, v, ptm0)` Full Usage: `mk_binder_preterm (f, v, ptm0)` Parameters: f : `preterm` v : `preterm` ptm0 : `preterm` Returns: `preterm`	f : `preterm` v : `preterm` ptm0 : `preterm` Returns: `preterm`
`mk_comb_preterm (f, ptm)` Full Usage: `mk_comb_preterm (f, ptm)` Parameters: f : `preterm` ptm : `preterm` Returns: `preterm`	f : `preterm` ptm : `preterm` Returns: `preterm`
`mk_cond_preterm (ptm0, ptm1, ptm2)` Full Usage: `mk_cond_preterm (ptm0, ptm1, ptm2)` Parameters: ptm0 : `preterm` ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`	ptm0 : `preterm` ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`
`mk_enum_preterm (br1, ptms, br2)` Full Usage: `mk_enum_preterm (br1, ptms, br2)` Parameters: br1 : `string` ptms : `preterm list` br2 : `string` Returns: `preterm`	br1 : `string` ptms : `preterm list` br2 : `string` Returns: `preterm`
`mk_fun_pretype (pty1, pty2)` Full Usage: `mk_fun_pretype (pty1, pty2)` Parameters: pty1 : `pretype` pty2 : `pretype` Returns: `pretype`	pty1 : `pretype` pty2 : `pretype` Returns: `pretype`
`mk_let_preterm (vptms, ptm0)` Full Usage: `mk_let_preterm (vptms, ptm0)` Parameters: vptms : `(preterm * preterm) list` ptm0 : `preterm` Returns: `preterm`	vptms : `(preterm * preterm) list` ptm0 : `preterm` Returns: `preterm`
`mk_null_const_preterm x` Full Usage: `mk_null_const_preterm x` Parameters: x : `string` Returns: `preterm`	x : `string` Returns: `preterm`
`mk_null_var_preterm x` Full Usage: `mk_null_var_preterm x` Parameters: x : `string` Returns: `preterm`	x : `string` Returns: `preterm`
`mk_pair_preterm (ptm1, ptm2)` Full Usage: `mk_pair_preterm (ptm1, ptm2)` Parameters: ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`	ptm1 : `preterm` ptm2 : `preterm` Returns: `preterm`
`numeral_fn` Full Usage: `numeral_fn` Returns: `preterm`	Returns: `preterm`
`pair_fn` Full Usage: `pair_fn` Returns: `preterm`	Returns: `preterm`
`preterm_gtyvars ptm` Full Usage: `preterm_gtyvars ptm` Parameters: ptm : `preterm` Returns: `pretype list`	ptm : `preterm` Returns: `pretype list`
`preterm_has_gtyvars ptm` Full Usage: `preterm_has_gtyvars ptm` Parameters: ptm : `preterm` Returns: `bool`	ptm : `preterm` Returns: `bool`
`preterm_inst theta ptm` Full Usage: `preterm_inst theta ptm` Parameters: theta : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm`	theta : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm`
`preterm_pretype_match (mptm, ptm)` Full Usage: `preterm_pretype_match (mptm, ptm)` Parameters: mptm : `preterm` ptm : `preterm` Returns: `(pretype * pretype) list`	mptm : `preterm` ptm : `preterm` Returns: `(pretype * pretype) list`
`preterm_pretype_match0 theta (mptm, ptm)` Full Usage: `preterm_pretype_match0 theta (mptm, ptm)` Parameters: theta : `(pretype * pretype) list` mptm : `preterm` ptm : `preterm` Returns: `(pretype * pretype) list`	theta : `(pretype * pretype) list` mptm : `preterm` ptm : `preterm` Returns: `(pretype * pretype) list`
`preterm_to_term ptm` Full Usage: `preterm_to_term ptm` Parameters: ptm : `preterm` Returns: `term`	ptm : `preterm` Returns: `term`
`preterm_to_term0 nxs ptm` Full Usage: `preterm_to_term0 nxs ptm` Parameters: nxs : `(int * string) list` ptm : `preterm` Returns: `term`	nxs : `(int * string) list` ptm : `preterm` Returns: `term`
`preterm_tyvars ptm` Full Usage: `preterm_tyvars ptm` Parameters: ptm : `preterm` Returns: `pretype list`	ptm : `preterm` Returns: `pretype list`
`pretype_complexity pty` Full Usage: `pretype_complexity pty` Parameters: pty : `pretype` Returns: `int`	pty : `pretype` Returns: `int`
`pretype_gtyvars pty` Full Usage: `pretype_gtyvars pty` Parameters: pty : `pretype` Returns: `pretype list`	pty : `pretype` Returns: `pretype list`
`pretype_has_gtyvars pty` Full Usage: `pretype_has_gtyvars pty` Parameters: pty : `pretype` Returns: `bool`	pty : `pretype` Returns: `bool`
`pretype_inst theta pty` Full Usage: `pretype_inst theta pty` Parameters: theta : `(pretype * pretype) list` pty : `pretype` Returns: `pretype`	theta : `(pretype * pretype) list` pty : `pretype` Returns: `pretype`
`pretype_match (mpty, pty)` Full Usage: `pretype_match (mpty, pty)` Parameters: mpty : `pretype` pty : `pretype` Returns: `(pretype * pretype) list`	mpty : `pretype` pty : `pretype` Returns: `(pretype * pretype) list`
`pretype_match0 theta (mpty, pty)` Full Usage: `pretype_match0 theta (mpty, pty)` Parameters: theta : `(pretype * pretype) list` mpty : `pretype` pty : `pretype` Returns: `(pretype * pretype) list`	theta : `(pretype * pretype) list` mpty : `pretype` pty : `pretype` Returns: `(pretype * pretype) list`
`pretype_to_type pty` Full Usage: `pretype_to_type pty` Parameters: pty : `pretype` Returns: `hol_type`	pty : `pretype` Returns: `hol_type`
`pretype_to_type0 nxs pty` Full Usage: `pretype_to_type0 nxs pty` Parameters: nxs : `(int * string) list` pty : `pretype` Returns: `hol_type`	nxs : `(int * string) list` pty : `pretype` Returns: `hol_type`
`pretype_tyvars pty` Full Usage: `pretype_tyvars pty` Parameters: pty : `pretype` Returns: `pretype list`	pty : `pretype` Returns: `pretype list`
`remove_identities theta` Full Usage: `remove_identities theta` Parameters: theta : `('a * 'a) list` Returns: `('a * 'a) list`	theta : `('a * 'a) list` Returns: `('a * 'a) list`
`same_atom_preterm ptm1 ptm2` Full Usage: `same_atom_preterm ptm1 ptm2` Parameters: ptm1 : `preterm` ptm2 : `preterm` Returns: `bool`	ptm1 : `preterm` ptm2 : `preterm` Returns: `bool`
`strip_abs_preterm ptm` Full Usage: `strip_abs_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm list * preterm`	ptm : `preterm` Returns: `preterm list * preterm`
`strip_bin_preterm h f0 ptm` Full Usage: `strip_bin_preterm h f0 ptm` Parameters: h : `assochand` f0 : `preterm` ptm : `preterm` Returns: `preterm list`	h : `assochand` f0 : `preterm` ptm : `preterm` Returns: `preterm list`
`strip_binder_preterm ptm` Full Usage: `strip_binder_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm list * preterm`	ptm : `preterm` Returns: `preterm * preterm list * preterm`
`strip_binder_preterm0 f0 ptm` Full Usage: `strip_binder_preterm0 f0 ptm` Parameters: f0 : `preterm` ptm : `preterm` Returns: `preterm list * preterm`	f0 : `preterm` ptm : `preterm` Returns: `preterm list * preterm`
`strip_comb_preterm ptm` Full Usage: `strip_comb_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm list`	ptm : `preterm` Returns: `preterm * preterm list`
`strip_infix_preterm ptm` Full Usage: `strip_infix_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm * preterm list`	ptm : `preterm` Returns: `preterm * preterm list`
`strip_infix_pretype pty` Full Usage: `strip_infix_pretype pty` Parameters: pty : `pretype` Returns: `string * pretype list`	pty : `pretype` Returns: `string * pretype list`
`strip_infix_pretype0 (x, h) pty` Full Usage: `strip_infix_pretype0 (x, h) pty` Parameters: x : `string` h : `assochand` pty : `pretype` Returns: `pretype list`	x : `string` h : `assochand` pty : `pretype` Returns: `pretype list`
`strip_pair_preterm ptm` Full Usage: `strip_pair_preterm ptm` Parameters: ptm : `preterm` Returns: `preterm list`	ptm : `preterm` Returns: `preterm list`
`term_to_preterm tm` Full Usage: `term_to_preterm tm` Parameters: tm : `term` Returns: `preterm`	tm : `term` Returns: `preterm`
`tynum_mapping xs0 ns` Full Usage: `tynum_mapping xs0 ns` Parameters: xs0 : `string list` ns : `'a list` Returns: `('a * string) list`	xs0 : `string list` ns : `'a list` Returns: `('a * string) list`
`tynum_mapping0 xs0 i ns` Full Usage: `tynum_mapping0 xs0 i ns` Parameters: xs0 : `string list` i : `int` ns : `'a list` Returns: `('a * string) list`	xs0 : `string list` i : `int` ns : `'a list` Returns: `('a * string) list`
`type_to_pretype ty` Full Usage: `type_to_pretype ty` Parameters: ty : `hol_type` Returns: `pretype`	ty : `hol_type` Returns: `pretype`