src/Pure/term_ord.ML
author wenzelm
Wed, 31 Jul 2019 19:50:38 +0200
changeset 70451 550a5a822edb
parent 67561 f0b11413f1c9
child 70586 57df8a85317a
permissions -rw-r--r--
clarified export: retain proof boxes as local definitions -- more scalable;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
     7
signature BASIC_TERM_ORD =
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
     8
sig
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
     9
  structure Vartab: TABLE
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    10
  structure Sorttab: TABLE
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    11
  structure Typtab: TABLE
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    12
  structure Termtab: TABLE
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    13
end;
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    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
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    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
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    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
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
    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
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   221
(* tables and caches *)
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   222
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   223
structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   224
structure Sorttab = Table(type key = sort val ord = sort_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   225
structure Typtab = Table(type key = typ val ord = typ_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   226
structure Termtab = Table(type key = term val ord = fast_term_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   227
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   228
fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   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
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   232
structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
32841
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   233
open Basic_Term_Ord;
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   234
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   235
structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   236
structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   237
structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   238
structure Term_Graph = Graph(type key = term val ord = Term_Ord.fast_term_ord);
35404
de56579ae229 just one copy of structure Term_Graph (in Pure);
wenzelm
parents: 32841
diff changeset
   239