60 | cons_nr (Var _) = 2 |
60 | cons_nr (Var _) = 2 |
61 | cons_nr (Bound _) = 3 |
61 | cons_nr (Bound _) = 3 |
62 | cons_nr (Abs _) = 4 |
62 | cons_nr (Abs _) = 4 |
63 | cons_nr (_ $ _) = 5; |
63 | cons_nr (_ $ _) = 5; |
64 |
64 |
65 fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u) |
65 fun struct_ord tu = |
66 | struct_ord (t1 $ t2, u1 $ u2) = |
66 if pointer_eq tu then EQUAL |
67 (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) |
67 else |
68 | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u); |
68 (case tu of |
69 |
69 (Abs (_, _, t), Abs (_, _, u)) => struct_ord (t, u) |
70 fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u) |
70 | (t1 $ t2, u1 $ u2) => |
71 | atoms_ord (t1 $ t2, u1 $ u2) = |
71 (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord) |
72 (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) |
72 | (t, u) => int_ord (cons_nr t, cons_nr u)); |
73 | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b) |
73 |
74 | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y) |
74 fun atoms_ord tu = |
75 | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj) |
75 if pointer_eq tu then EQUAL |
76 | atoms_ord (Bound i, Bound j) = int_ord (i, j) |
76 else |
77 | atoms_ord _ = EQUAL; |
77 (case tu of |
78 |
78 (Abs (_, _, t), Abs (_, _, u)) => atoms_ord (t, u) |
79 fun types_ord (Abs (_, T, t), Abs (_, U, u)) = |
79 | (t1 $ t2, u1 $ u2) => |
80 (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) |
80 (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord) |
81 | types_ord (t1 $ t2, u1 $ u2) = |
81 | (Const (a, _), Const (b, _)) => fast_string_ord (a, b) |
82 (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) |
82 | (Free (x, _), Free (y, _)) => fast_string_ord (x, y) |
83 | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U) |
83 | (Var (xi, _), Var (yj, _)) => fast_indexname_ord (xi, yj) |
84 | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U) |
84 | (Bound i, Bound j) => int_ord (i, j) |
85 | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U) |
85 | _ => EQUAL); |
86 | types_ord _ = EQUAL; |
86 |
87 |
87 fun types_ord tu = |
88 fun comments_ord (Abs (x, _, t), Abs (y, _, u)) = |
88 if pointer_eq tu then EQUAL |
89 (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord) |
89 else |
90 | comments_ord (t1 $ t2, u1 $ u2) = |
90 (case tu of |
91 (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord) |
91 (Abs (_, T, t), Abs (_, U, u)) => |
92 | comments_ord _ = EQUAL; |
92 (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord) |
93 |
93 | (t1 $ t2, u1 $ u2) => |
94 in |
94 (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord) |
95 |
95 | (Const (_, T), Const (_, U)) => typ_ord (T, U) |
96 val fast_term_ord = pointer_eq_ord (struct_ord ||| atoms_ord ||| types_ord); |
96 | (Free (_, T), Free (_, U)) => typ_ord (T, U) |
|
97 | (Var (_, T), Var (_, U)) => typ_ord (T, U) |
|
98 | _ => EQUAL); |
|
99 |
|
100 fun comments_ord tu = |
|
101 if pointer_eq tu then EQUAL |
|
102 else |
|
103 (case tu of |
|
104 (Abs (x, _, t), Abs (y, _, u)) => |
|
105 (case fast_string_ord (x, y) of EQUAL => comments_ord (t, u) | ord => ord) |
|
106 | (t1 $ t2, u1 $ u2) => |
|
107 (case comments_ord (t1, u1) of EQUAL => comments_ord (t2, u2) | ord => ord) |
|
108 | _ => EQUAL); |
|
109 |
|
110 in |
|
111 |
|
112 val fast_term_ord = struct_ord ||| atoms_ord ||| types_ord; |
97 |
113 |
98 val syntax_term_ord = fast_term_ord ||| comments_ord; |
114 val syntax_term_ord = fast_term_ord ||| comments_ord; |
99 |
115 |
100 end; |
116 end; |
101 |
117 |