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