TypeAnnot (nholz)

TypeAnnot Module

Namespace: HOL
Assembly: nholz.dll

This module defines type analysis routines for pretypes and preterms, used in parsing and printing type/term quotations. The primary routines are detyping, type unification, type inference and type consistency check. This module is used in the implementation of the pretty printer, and is a trusted component of the system.

Functions and values

Function or value	Description
`annotate_preterm_atoms thetaC atms ptm` Full Usage: `annotate_preterm_atoms thetaC atms ptm` Parameters: thetaC : `(pretype * pretype) list` atms : `preterm list` ptm : `preterm` Returns: `preterm`	This function transforms preterm 'ptm' by adding type annotations for atoms from 'atms' with types looked up from instn list 'thetaC'. Note that the preterm will already have been detyped, and that the resulting generated tyvars remain in the preterm until now, and so each atom in the atom list uniquely identifies a specific atom within the preterm. The resulting type-annotated preterm also has its original generated tyvars from detyping, but the added type annotations on atoms give all the information required to remove ambiguity in the printed quotation. thetaC : `(pretype * pretype) list` atms : `preterm list` ptm : `preterm` Returns: `preterm`
`atom_info thetaC ptm` Full Usage: `atom_info thetaC ptm` Parameters: thetaC : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm list * preterm list * preterm list * preterm list * (pretype * pretype) list`	thetaC : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm list * preterm list * preterm list * preterm list * (pretype * pretype) list`
`atom_info0 thetaC ptm` Full Usage: `atom_info0 thetaC ptm` Parameters: thetaC : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm list * preterm list * preterm list * preterm list * pretype * (pretype * pretype) list`	thetaC : `(pretype * pretype) list` ptm : `preterm` Returns: `preterm list * preterm list * preterm list * preterm list * pretype * (pretype * pretype) list`
`atom_type_complexity ptm` Full Usage: `atom_type_complexity ptm` Parameters: ptm : `preterm` Returns: `int`	ptm : `preterm` Returns: `int`
`closure_info (thetaC, theta0) fvs v` Full Usage: `closure_info (thetaC, theta0) fvs v` Parameters: thetaC : `(pretype * pretype) list` theta0 : `(pretype * pretype) list` fvs : `preterm list` v : `preterm` Returns: `preterm list * preterm list * (pretype * pretype) list`	thetaC : `(pretype * pretype) list` theta0 : `(pretype * pretype) list` fvs : `preterm list` v : `preterm` Returns: `preterm list * preterm list * (pretype * pretype) list`
`domain_restrict xs xys` Full Usage: `domain_restrict xs xys` Parameters: xs : `'a list` xys : `('a * 'b) list` Returns: `('a * 'b) list`	xs : `'a list` xys : `('a * 'b) list` Returns: `('a * 'b) list`
`full_annotate_preterm fl ptm` Full Usage: `full_annotate_preterm fl ptm` Parameters: fl : `bool` ptm : `preterm` Returns: `preterm`	fl : `bool` ptm : `preterm` Returns: `preterm`
`min_annotate_preterm pty_ ptm` Full Usage: `min_annotate_preterm pty_ ptm` Parameters: pty_ : `pretype option` ptm : `preterm` Returns: `preterm`	pty_ : `pretype option` ptm : `preterm` Returns: `preterm`
`ordered_unresolved_atoms atms` Full Usage: `ordered_unresolved_atoms atms` Parameters: atms : `preterm list` Returns: `preterm list`	atms : `preterm list` Returns: `preterm list`
`pick_atom_coverage thetaC pty_ ptm` Full Usage: `pick_atom_coverage thetaC pty_ ptm` Parameters: thetaC : `(pretype * pretype) list` pty_ : `pretype option` ptm : `preterm` Returns: `preterm list`	thetaC : `(pretype * pretype) list` pty_ : `pretype option` ptm : `preterm` Returns: `preterm list`
`preterm_var ptm` Full Usage: `preterm_var ptm` Parameters: ptm : `preterm` Returns: `preterm`	ptm : `preterm` Returns: `preterm`
`sift_atoms gtys0 atms` Full Usage: `sift_atoms gtys0 atms` Parameters: gtys0 : `pretype list` atms : `preterm list` Returns: `preterm list`	gtys0 : `pretype list` atms : `preterm list` Returns: `preterm list`
`sift_atoms0 (atms0, gtys0) atms` Full Usage: `sift_atoms0 (atms0, gtys0) atms` Parameters: atms0 : `preterm list` gtys0 : `pretype list` atms : `preterm list` Returns: `preterm list`	atms0 : `preterm list` gtys0 : `pretype list` atms : `preterm list` Returns: `preterm list`
`sort_by_type_complexity ptms` Full Usage: `sort_by_type_complexity ptms` Parameters: ptms : `preterm list` Returns: `preterm list`	ptms : `preterm list` Returns: `preterm list`
`unresolved_atoms atms` Full Usage: `unresolved_atoms atms` Parameters: atms : `preterm list` Returns: `preterm list`	atms : `preterm list` Returns: `preterm list`
`var_equiv1 v1 v2` Full Usage: `var_equiv1 v1 v2` Parameters: v1 : `preterm` v2 : `preterm` Returns: `bool`	v1 : `preterm` v2 : `preterm` Returns: `bool`
`var_equiv2 theta v1 v2` Full Usage: `var_equiv2 theta v1 v2` Parameters: theta : `(pretype * pretype) list` v1 : `preterm` v2 : `preterm` Returns: `bool`	theta : `(pretype * pretype) list` v1 : `preterm` v2 : `preterm` Returns: `bool`