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