1signature FinalTerm =
2sig
3
4  eqtype term
5  eqtype hol_type
6  type ('a,'b)subst = ('a,'b)Lib.subst
7  type 'a set       = 'a HOLset.set
8
9  val equality      : term
10
11  val type_of       : term -> hol_type
12  val free_vars     : term -> term list
13  val free_vars_lr  : term -> term list
14  val FVL           : term list -> term set -> term set
15  val free_in       : term -> term -> bool
16  val all_vars      : term -> term list
17  val all_atoms     : term -> term set
18  val all_atomsl    : term list -> term set -> term set
19  val free_varsl    : term list -> term list
20  val all_varsl     : term list -> term list
21  val type_vars_in_term : term -> hol_type list
22  val var_occurs    : term -> term -> bool
23
24  val genvar        : hol_type -> term
25  val genvars       : hol_type -> int -> term list
26  val variant       : term list -> term -> term
27  val prim_variant  : term list -> term -> term
28  val gen_variant   : (string -> bool) -> string -> term list -> term -> term
29
30  val mk_var        : string * hol_type -> term
31  val mk_primed_var : string * hol_type -> term
32  val decls         : string -> term list
33  val all_consts    : unit -> term list
34  val mk_const      : string * hol_type -> term
35  val prim_mk_const : {Thy:string, Name:string} -> term
36  val mk_thy_const  : {Thy:string, Name:string, Ty:hol_type} -> term
37  val list_mk_comb  : term * term list -> term
38  val mk_comb       : term * term -> term
39  val mk_abs        : term * term -> term
40  val list_mk_binder : term option -> term list * term -> term
41  val list_mk_abs   : term list * term -> term
42  val dest_var      : term -> string * hol_type
43  val dest_const    : term -> string * hol_type
44  val dest_thy_const : term -> {Thy:string, Name:string, Ty:hol_type}
45  val dest_comb     : term -> term * term
46  val strip_binder  : term option -> term -> term list * term
47  val strip_abs     : term -> term list * term
48  val dest_abs      : term -> term * term
49  val is_var        : term -> bool
50  val is_genvar     : term -> bool
51  val is_const      : term -> bool
52  val is_comb       : term -> bool
53  val is_abs        : term -> bool
54  val rator         : term -> term
55  val rand          : term -> term
56  val bvar          : term -> term
57  val body          : term -> term
58  val rename_bvar   : string -> term -> term
59
60  val same_const    : term -> term -> bool
61  val aconv         : term -> term -> bool
62  val beta_conv     : term -> term
63  val eta_conv      : term -> term
64  val subst         : (term,term) subst -> term -> term
65  val inst          : (hol_type,hol_type) subst -> term -> term
66
67  val raw_match     : hol_type list -> term set
68                      -> term -> term
69                      -> (term,term)subst * (hol_type,hol_type)subst
70                      -> ((term,term)subst * term set) *
71                         ((hol_type,hol_type)subst * hol_type list)
72  val match_terml   : hol_type list -> term set -> term -> term
73                        -> (term,term)subst * (hol_type,hol_type)subst
74  val match_term    : term -> term -> (term,term)subst*(hol_type,hol_type)subst
75  val norm_subst    : ((term,term)subst * term set) *
76                      ((hol_type,hol_type)subst * hol_type list)
77                      -> ((term,term)subst * (hol_type,hol_type)subst)
78
79  val var_compare   : term * term -> order
80  val compare       : term * term -> order
81  val term_eq       : term -> term -> bool
82  val fast_term_eq  : term -> term -> bool
83
84  val empty_tmset   : term set
85  val empty_varset  : term set
86
87  val term_size     : term -> int
88
89  (* theory segment related functionality *)
90  val uptodate_term     : term -> bool
91
92  val thy_consts        : string -> term list
93  val del_segment       : string -> unit
94
95  val prim_new_const    : KernelSig.kernelname -> hol_type -> term
96  val prim_delete_const : KernelSig.kernelname -> unit
97
98  (* printed theory functionality *)
99  val read_raw : term vector -> string -> term
100  val write_raw : (term -> int) -> term -> string
101
102  datatype lambda =
103          VAR of string * hol_type
104        | CONST of {Name : string, Thy : string, Ty : hol_type}
105        | COMB of term * term
106        | LAMB of term * term
107  val dest_term : term -> lambda
108  val identical : term -> term -> bool
109
110
111end
112