author | blanchet |
Thu, 16 Dec 2010 22:45:02 +0100 | |
changeset 41220 | 4d11b0de7dd8 |
parent 39687 | 4e9b6ada3a21 |
permissions | -rw-r--r-- |
29262 | 1 |
(* Title: Pure/old_term.ML |
2 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
3 |
||
37783 | 4 |
Some outdated term operations. |
29262 | 5 |
*) |
6 |
||
7 |
signature OLD_TERM = |
|
8 |
sig |
|
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
9 |
val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
10 |
val add_term_names: term * string list -> string list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
11 |
val add_typ_tvars: typ * (indexname * sort) list -> (indexname * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
12 |
val add_typ_tfree_names: typ * string list -> string list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
13 |
val add_typ_tfrees: typ * (string * sort) list -> (string * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
14 |
val add_term_tvars: term * (indexname * sort) list -> (indexname * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
15 |
val add_term_tfrees: term * (string * sort) list -> (string * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
16 |
val add_term_tfree_names: term * string list -> string list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
17 |
val typ_tfrees: typ -> (string * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
18 |
val typ_tvars: typ -> (indexname * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
19 |
val term_tfrees: term -> (string * sort) list |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
20 |
val term_tvars: term -> (indexname * sort) list |
29262 | 21 |
val add_term_vars: term * term list -> term list |
22 |
val term_vars: term -> term list |
|
23 |
val add_term_frees: term * term list -> term list |
|
24 |
val term_frees: term -> term list |
|
25 |
end; |
|
26 |
||
27 |
structure OldTerm: OLD_TERM = |
|
28 |
struct |
|
29 |
||
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
30 |
(*iterate a function over all types in a term*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
31 |
fun it_term_types f = |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
32 |
let fun iter(Const(_,T), a) = f(T,a) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
33 |
| iter(Free(_,T), a) = f(T,a) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
34 |
| iter(Var(_,T), a) = f(T,a) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
35 |
| iter(Abs(_,T,t), a) = iter(t,f(T,a)) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
36 |
| iter(f$u, a) = iter(f, iter(u, a)) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
37 |
| iter(Bound _, a) = a |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
38 |
in iter end |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
39 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
40 |
(*Accumulates the names in the term, suppressing duplicates. |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
41 |
Includes Frees and Consts. For choosing unambiguous bound var names.*) |
30364
577edc39b501
moved basic algebra of long names from structure NameSpace to Long_Name;
wenzelm
parents:
30280
diff
changeset
|
42 |
fun add_term_names (Const(a,_), bs) = insert (op =) (Long_Name.base_name a) bs |
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
43 |
| add_term_names (Free(a,_), bs) = insert (op =) a bs |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
44 |
| add_term_names (f$u, bs) = add_term_names (f, add_term_names(u, bs)) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
45 |
| add_term_names (Abs(_,_,t), bs) = add_term_names(t,bs) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
46 |
| add_term_names (_, bs) = bs; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
47 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
48 |
(*Accumulates the TVars in a type, suppressing duplicates.*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
49 |
fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
50 |
| add_typ_tvars(TFree(_),vs) = vs |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
51 |
| add_typ_tvars(TVar(v),vs) = insert (op =) v vs; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
52 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
53 |
(*Accumulates the TFrees in a type, suppressing duplicates.*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
54 |
fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
55 |
| add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
56 |
| add_typ_tfree_names(TVar(_),fs) = fs; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
57 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
58 |
fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
59 |
| add_typ_tfrees(TFree(f),fs) = insert (op =) f fs |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
60 |
| add_typ_tfrees(TVar(_),fs) = fs; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
61 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
62 |
(*Accumulates the TVars in a term, suppressing duplicates.*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
63 |
val add_term_tvars = it_term_types add_typ_tvars; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
64 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
65 |
(*Accumulates the TFrees in a term, suppressing duplicates.*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
66 |
val add_term_tfrees = it_term_types add_typ_tfrees; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
67 |
val add_term_tfree_names = it_term_types add_typ_tfree_names; |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
68 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
69 |
(*Non-list versions*) |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
70 |
fun typ_tfrees T = add_typ_tfrees(T,[]); |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
71 |
fun typ_tvars T = add_typ_tvars(T,[]); |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
72 |
fun term_tfrees t = add_term_tfrees(t,[]); |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
73 |
fun term_tvars t = add_term_tvars(t,[]); |
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
74 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
75 |
|
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
76 |
(*Accumulates the Vars in the term, suppressing duplicates.*) |
29262 | 77 |
fun add_term_vars (t, vars: term list) = case t of |
39687 | 78 |
Var _ => Ord_List.insert Term_Ord.term_ord t vars |
29262 | 79 |
| Abs (_,_,body) => add_term_vars(body,vars) |
80 |
| f$t => add_term_vars (f, add_term_vars(t, vars)) |
|
81 |
| _ => vars; |
|
82 |
||
83 |
fun term_vars t = add_term_vars(t,[]); |
|
84 |
||
29270
0eade173f77e
moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
wenzelm
parents:
29269
diff
changeset
|
85 |
(*Accumulates the Frees in the term, suppressing duplicates.*) |
29262 | 86 |
fun add_term_frees (t, frees: term list) = case t of |
39687 | 87 |
Free _ => Ord_List.insert Term_Ord.term_ord t frees |
29262 | 88 |
| Abs (_,_,body) => add_term_frees(body,frees) |
89 |
| f$t => add_term_frees (f, add_term_frees(t, frees)) |
|
90 |
| _ => frees; |
|
91 |
||
92 |
fun term_frees t = add_term_frees(t,[]); |
|
93 |
||
94 |
end; |