1structure KernelTypes = 2struct 3 4(*--------------------------------------------------------------------------- 5 Elements in signatures are determined by a (name,theory) pair. 6 The reference cell is for uniqueness (an interactive session may 7 create more than one such pair, and they need to be distinguished). 8 ---------------------------------------------------------------------------*) 9 10type id = KernelSig.kernelid 11 12(*---------------------------------------------------------------------------* 13 * HOL types are somewhat akin to terms in first order logic. * 14 *---------------------------------------------------------------------------*) 15 16type tyconst = id * int 17 18datatype hol_type = Tyv of string 19 | Tyapp of tyconst * hol_type list; 20 21 22(*---------------------------------------------------------------------------* 23 * HOL terms are represented internally using deBruijn indices and explicit * 24 * substitutions. Externally, as always, the interface is to a * 25 * name-carrying syntax. The "holty" field in tmconst tells whether the * 26 * constant is polymorphic or not. Currently, this is only an approximation: * 27 * if it is GRND, then the constant has no type variables. If POLY, the * 28 * constant may or may not have type variables. * 29 *---------------------------------------------------------------------------*) 30 31datatype holty = GRND of hol_type 32 | POLY of hol_type 33 34fun to_hol_type (GRND ty) = ty 35 | to_hol_type (POLY ty) = ty; 36 37type tmconst = id * holty 38 39datatype term = Fv of string * hol_type 40 | Bv of int 41 | Const of tmconst 42 | Comb of term * term 43 | Abs of term * term 44 | Clos of term Subst.subs * term; 45 46(*--------------------------------------------------------------------------- 47 The representation of theorems. A "tag" is a pair of the oracles 48 used and the axioms used. Oracles are represented as ordered lists 49 of strings, and axioms are lists of string refs. 50 ---------------------------------------------------------------------------*) 51 52datatype thm = THM of Tag.tag * term HOLset.set * term 53 54(*--------------------------------------------------------------------------- 55 The type of witnesses for definitions, used in Theory. 56 ---------------------------------------------------------------------------*) 57 58datatype witness = TERM of term | THEOREM of thm 59 60end 61