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