|
1 (* Title: Pure/term_ord.ML |
|
2 Author: Tobias Nipkow and Makarius, TU Muenchen |
|
3 |
|
4 Term orderings. |
|
5 *) |
|
6 |
|
7 signature TERM_ORD = |
|
8 sig |
|
9 val fast_indexname_ord: indexname * indexname -> order |
|
10 val sort_ord: sort * sort -> order |
|
11 val typ_ord: typ * typ -> order |
|
12 val fast_term_ord: term * term -> order |
|
13 val indexname_ord: indexname * indexname -> order |
|
14 val tvar_ord: (indexname * sort) * (indexname * sort) -> order |
|
15 val var_ord: (indexname * typ) * (indexname * typ) -> order |
|
16 val term_ord: term * term -> order |
|
17 val hd_ord: term * term -> order |
|
18 val termless: term * term -> bool |
|
19 val term_lpo: (term -> int) -> term * term -> order |
|
20 end; |
|
21 |
|
22 structure TermOrd: TERM_ORD = |
|
23 struct |
|
24 |
|
25 (* fast syntactic ordering -- tuned for inequalities *) |
|
26 |
|
27 fun fast_indexname_ord ((x, i), (y, j)) = |
|
28 (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord); |
|
29 |
|
30 fun sort_ord SS = |
|
31 if pointer_eq SS then EQUAL |
|
32 else dict_ord fast_string_ord SS; |
|
33 |
|
34 local |
|
35 |
|
36 fun cons_nr (TVar _) = 0 |
|
37 | cons_nr (TFree _) = 1 |
|
38 | cons_nr (Type _) = 2; |
|
39 |
|
40 in |
|
41 |
|
42 fun typ_ord TU = |
|
43 if pointer_eq TU then EQUAL |
|
44 else |
|
45 (case TU of |
|
46 (Type (a, Ts), Type (b, Us)) => |
|
47 (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord) |
|
48 | (TFree (a, S), TFree (b, S')) => |
|
49 (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord) |
|
50 | (TVar (xi, S), TVar (yj, S')) => |
|
51 (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord) |
|
52 | (T, U) => int_ord (cons_nr T, cons_nr U)); |
|
53 |
|
54 end; |
|
55 |
|
56 local |
|
57 |
|
58 fun cons_nr (Const _) = 0 |
|
59 | cons_nr (Free _) = 1 |
|
60 | cons_nr (Var _) = 2 |
|
61 | cons_nr (Bound _) = 3 |
|
62 | cons_nr (Abs _) = 4 |
|
63 | cons_nr (_ $ _) = 5; |
|
64 |
|
65 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) |
|
66 | struct_ord (t1 $ t2, u1 $ u2) = |
|
67 (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) |
|
68 | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); |
|
69 |
|
70 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) |
|
71 | atoms_ord (t1 $ t2, u1 $ u2) = |
|
72 (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) |
|
73 | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) |
|
74 | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) |
|
75 | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) |
|
76 | atoms_ord (Bound i, Bound j) = int_ord (i, j) |
|
77 | atoms_ord _ = sys_error "atoms_ord"; |
|
78 |
|
79 fun types_ord (Abs (_, T, t), Abs (_, U, u)) = |
|
80 (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) |
|
81 | types_ord (t1 $ t2, u1 $ u2) = |
|
82 (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) |
|
83 | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) |
|
84 | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) |
|
85 | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) |
|
86 | types_ord (Bound _, Bound _) = EQUAL |
|
87 | types_ord _ = sys_error "types_ord"; |
|
88 |
|
89 in |
|
90 |
|
91 fun fast_term_ord tu = |
|
92 if pointer_eq tu then EQUAL |
|
93 else |
|
94 (case struct_ord tu of |
|
95 EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord) |
|
96 | ord => ord); |
|
97 |
|
98 end; |
|
99 |
|
100 |
|
101 (* term_ord *) |
|
102 |
|
103 (*a linear well-founded AC-compatible ordering for terms: |
|
104 s < t <=> 1. size(s) < size(t) or |
|
105 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or |
|
106 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and |
|
107 (s1..sn) < (t1..tn) (lexicographically)*) |
|
108 |
|
109 fun indexname_ord ((x, i), (y, j)) = |
|
110 (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord); |
|
111 |
|
112 val tvar_ord = prod_ord indexname_ord sort_ord; |
|
113 val var_ord = prod_ord indexname_ord typ_ord; |
|
114 |
|
115 |
|
116 local |
|
117 |
|
118 fun hd_depth (t $ _, n) = hd_depth (t, n + 1) |
|
119 | hd_depth p = p; |
|
120 |
|
121 fun dest_hd (Const (a, T)) = (((a, 0), T), 0) |
|
122 | dest_hd (Free (a, T)) = (((a, 0), T), 1) |
|
123 | dest_hd (Var v) = (v, 2) |
|
124 | dest_hd (Bound i) = ((("", i), dummyT), 3) |
|
125 | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4); |
|
126 |
|
127 in |
|
128 |
|
129 fun term_ord tu = |
|
130 if pointer_eq tu then EQUAL |
|
131 else |
|
132 (case tu of |
|
133 (Abs (_, T, t), Abs(_, U, u)) => |
|
134 (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) |
|
135 | (t, u) => |
|
136 (case int_ord (size_of_term t, size_of_term u) of |
|
137 EQUAL => |
|
138 (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of |
|
139 EQUAL => args_ord (t, u) | ord => ord) |
|
140 | ord => ord)) |
|
141 and hd_ord (f, g) = |
|
142 prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g) |
|
143 and args_ord (f $ t, g $ u) = |
|
144 (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord) |
|
145 | args_ord _ = EQUAL; |
|
146 |
|
147 fun termless tu = (term_ord tu = LESS); |
|
148 |
|
149 end; |
|
150 |
|
151 |
|
152 (* Lexicographic path order on terms *) |
|
153 |
|
154 (* |
|
155 See Baader & Nipkow, Term rewriting, CUP 1998. |
|
156 Without variables. Const, Var, Bound, Free and Abs are treated all as |
|
157 constants. |
|
158 |
|
159 f_ord maps terms to integers and serves two purposes: |
|
160 - Predicate on constant symbols. Those that are not recognised by f_ord |
|
161 must be mapped to ~1. |
|
162 - Order on the recognised symbols. These must be mapped to distinct |
|
163 integers >= 0. |
|
164 The argument of f_ord is never an application. |
|
165 *) |
|
166 |
|
167 local |
|
168 |
|
169 fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0) |
|
170 | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0) |
|
171 | unrecognized (Var v) = ((1, v), 1) |
|
172 | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2) |
|
173 | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3); |
|
174 |
|
175 fun dest_hd f_ord t = |
|
176 let val ord = f_ord t |
|
177 in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end; |
|
178 |
|
179 fun term_lpo f_ord (s, t) = |
|
180 let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in |
|
181 if forall (fn si => term_lpo f_ord (si, t) = LESS) ss |
|
182 then case hd_ord f_ord (f, g) of |
|
183 GREATER => |
|
184 if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts |
|
185 then GREATER else LESS |
|
186 | EQUAL => |
|
187 if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts |
|
188 then list_ord (term_lpo f_ord) (ss, ts) |
|
189 else LESS |
|
190 | LESS => LESS |
|
191 else GREATER |
|
192 end |
|
193 and hd_ord f_ord (f, g) = case (f, g) of |
|
194 (Abs (_, T, t), Abs (_, U, u)) => |
|
195 (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord) |
|
196 | (_, _) => prod_ord (prod_ord int_ord |
|
197 (prod_ord indexname_ord typ_ord)) int_ord |
|
198 (dest_hd f_ord f, dest_hd f_ord g); |
|
199 |
|
200 in |
|
201 val term_lpo = term_lpo |
|
202 end; |
|
203 |
|
204 |
|
205 end; |
|
206 |
|
207 structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord); |
|
208 structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord); |
|
209 structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord); |