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