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