33 Free of string * typ | |
33 Free of string * typ | |
34 Var of indexname * typ | |
34 Var of indexname * typ | |
35 Bound of int | |
35 Bound of int | |
36 Abs of string * typ * term | |
36 Abs of string * typ * term | |
37 $ of term * term |
37 $ of term * term |
|
38 structure Vartab : TABLE |
|
39 structure Termtab : TABLE |
38 exception TYPE of string * typ list * term list |
40 exception TYPE of string * typ list * term list |
39 exception TERM of string * term list |
41 exception TERM of string * term list |
40 val is_Bound: term -> bool |
42 val is_Bound: term -> bool |
41 val is_Const: term -> bool |
43 val is_Const: term -> bool |
42 val is_Free: term -> bool |
44 val is_Free: term -> bool |
88 val loose_bvar: term * int -> bool |
90 val loose_bvar: term * int -> bool |
89 val loose_bvar1: term * int -> bool |
91 val loose_bvar1: term * int -> bool |
90 val subst_bounds: term list * term -> term |
92 val subst_bounds: term list * term -> term |
91 val subst_bound: term * term -> term |
93 val subst_bound: term * term -> term |
92 val subst_TVars: (indexname * typ) list -> term -> term |
94 val subst_TVars: (indexname * typ) list -> term -> term |
|
95 val subst_TVars_Vartab: typ Vartab.table -> term -> term |
93 val betapply: term * term -> term |
96 val betapply: term * term -> term |
94 val eq_ix: indexname * indexname -> bool |
97 val eq_ix: indexname * indexname -> bool |
95 val ins_ix: indexname * indexname list -> indexname list |
98 val ins_ix: indexname * indexname list -> indexname list |
96 val mem_ix: indexname * indexname list -> bool |
99 val mem_ix: indexname * indexname list -> bool |
97 val eq_sort: sort * class list -> bool |
100 val eq_sort: sort * class list -> bool |
112 val could_unify: term * term -> bool |
115 val could_unify: term * term -> bool |
113 val subst_free: (term * term) list -> term -> term |
116 val subst_free: (term * term) list -> term -> term |
114 val subst_atomic: (term * term) list -> term -> term |
117 val subst_atomic: (term * term) list -> term -> term |
115 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term |
118 val subst_vars: (indexname * typ) list * (indexname * term) list -> term -> term |
116 val typ_subst_TVars: (indexname * typ) list -> typ -> typ |
119 val typ_subst_TVars: (indexname * typ) list -> typ -> typ |
|
120 val typ_subst_TVars_Vartab : typ Vartab.table -> typ -> typ |
117 val subst_Vars: (indexname * term) list -> term -> term |
121 val subst_Vars: (indexname * term) list -> term -> term |
118 val incr_tvar: int -> typ -> typ |
122 val incr_tvar: int -> typ -> typ |
119 val xless: (string * int) * indexname -> bool |
123 val xless: (string * int) * indexname -> bool |
120 val atless: term * term -> bool |
124 val atless: term * term -> bool |
121 val insert_aterm: term * term list -> term list |
125 val insert_aterm: term * term list -> term list |
965 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) |
969 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) |
966 and terms_ord (ts, us) = list_ord term_ord (ts, us); |
970 and terms_ord (ts, us) = list_ord term_ord (ts, us); |
967 |
971 |
968 fun termless tu = (term_ord tu = LESS); |
972 fun termless tu = (term_ord tu = LESS); |
969 |
973 |
|
974 structure Vartab = TableFun(type key = indexname val ord = indexname_ord); |
|
975 structure Termtab = TableFun(type key = term val ord = term_ord); |
|
976 |
|
977 (*Substitute for type Vars in a type, version using Vartab*) |
|
978 fun typ_subst_TVars_Vartab iTs T = if Vartab.is_empty iTs then T else |
|
979 let fun subst(Type(a, Ts)) = Type(a, map subst Ts) |
|
980 | subst(T as TFree _) = T |
|
981 | subst(T as TVar(ixn, _)) = |
|
982 (case Vartab.lookup (iTs, ixn) of None => T | Some(U) => U) |
|
983 in subst T end; |
|
984 |
|
985 (*Substitute for type Vars in a term, version using Vartab*) |
|
986 val subst_TVars_Vartab = map_term_types o typ_subst_TVars_Vartab; |
970 |
987 |
971 |
988 |
972 (*** Compression of terms and types by sharing common subtrees. |
989 (*** Compression of terms and types by sharing common subtrees. |
973 Saves 50-75% on storage requirements. As it is fairly slow, |
990 Saves 50-75% on storage requirements. As it is fairly slow, |
974 it is called only for axioms, stored theorems, etc. ***) |
991 it is called only for axioms, stored theorems, etc. ***) |