src/Pure/term_ord.ML
author wenzelm
Fri, 21 Apr 2017 15:26:24 +0200
changeset 65534 b6250ee6ce79
parent 43794 49cbbe2768a8
child 67561 f0b11413f1c9
permissions -rw-r--r--
clarified local_theories: exclude ancestor sessions;
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 termless: term * term -> bool
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    29
  val term_lpo: (term -> int) -> term * term -> order
32841
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
    30
  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
    31
end;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    32
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
    33
structure Term_Ord: TERM_ORD =
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    34
struct
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    35
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    36
(* fast syntactic ordering -- tuned for inequalities *)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    37
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    38
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
    39
  (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
    40
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    41
fun sort_ord SS =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    42
  if pointer_eq SS then EQUAL
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    43
  else dict_ord fast_string_ord SS;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    44
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    45
local
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    46
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    47
fun cons_nr (TVar _) = 0
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    48
  | cons_nr (TFree _) = 1
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    49
  | cons_nr (Type _) = 2;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    50
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    51
in
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    52
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    53
fun typ_ord TU =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    54
  if pointer_eq TU then EQUAL
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    55
  else
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    56
    (case TU of
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    57
      (Type (a, Ts), Type (b, Us)) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    58
        (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
    59
    | (TFree (a, S), TFree (b, S')) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    60
        (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
    61
    | (TVar (xi, S), TVar (yj, S')) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    62
        (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
    63
    | (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
    64
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    65
end;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    66
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    67
local
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    68
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    69
fun cons_nr (Const _) = 0
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    70
  | cons_nr (Free _) = 1
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    71
  | cons_nr (Var _) = 2
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    72
  | cons_nr (Bound _) = 3
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    73
  | cons_nr (Abs _) = 4
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    74
  | cons_nr (_ $ _) = 5;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    75
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    76
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
    77
  | struct_ord (t1 $ t2, u1 $ u2) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    78
      (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
    79
  | 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
    80
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    81
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
    82
  | atoms_ord (t1 $ t2, u1 $ u2) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    83
      (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
    84
  | 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
    85
  | 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
    86
  | 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
    87
  | 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
    88
  | atoms_ord _ = EQUAL;
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    89
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    90
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
    91
      (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
    92
  | types_ord (t1 $ t2, u1 $ u2) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
    93
      (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
    94
  | 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
    95
  | 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
    96
  | 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
    97
  | 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
    98
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
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
   100
      (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
   101
  | 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
   102
      (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
   103
  | comments_ord _ = EQUAL;
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   104
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   105
in
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   106
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   107
fun fast_term_ord tu =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   108
  if pointer_eq tu then EQUAL
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   109
  else
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   110
    (case struct_ord tu of
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   111
      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
   112
    | ord => ord);
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   113
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
   114
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
   115
  (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
   116
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   117
end;
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
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   120
(* term_ord *)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   121
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   122
(*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
   123
  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
   124
            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
   125
            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
   126
               (s1..sn) < (t1..tn) (lexicographically)*)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   127
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   128
fun indexname_ord ((x, i), (y, j)) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   129
  (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
   130
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   131
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
   132
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
   133
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   134
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   135
local
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   136
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   137
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
   138
  | hd_depth p = p;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   139
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   140
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
   141
  | 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
   142
  | dest_hd (Var v) = (v, 2)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   143
  | dest_hd (Bound i) = ((("", i), dummyT), 3)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   144
  | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   145
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   146
in
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   147
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   148
fun term_ord tu =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   149
  if pointer_eq tu then EQUAL
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   150
  else
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   151
    (case tu of
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   152
      (Abs (_, T, t), Abs(_, U, u)) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   153
        (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
   154
    | (t, u) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   155
        (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
   156
          EQUAL =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   157
            (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
   158
              EQUAL => args_ord (t, u) | ord => ord)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   159
        | ord => ord))
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   160
and hd_ord (f, g) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   161
  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
   162
and args_ord (f $ t, g $ u) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   163
      (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
   164
  | args_ord _ = EQUAL;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   165
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   166
fun termless tu = (term_ord tu = LESS);
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
end;
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
(* Lexicographic path order on terms *)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   172
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   173
(*
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   174
  See Baader & Nipkow, Term rewriting, CUP 1998.
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   175
  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
   176
  constants.
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   177
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   178
  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
   179
  - 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
   180
    must be mapped to ~1.
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   181
  - 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
   182
    integers >= 0.
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   183
  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
   184
*)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   185
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   186
local
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   187
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   188
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
   189
  | 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
   190
  | unrecognized (Var v) = ((1, v), 1)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   191
  | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   192
  | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   193
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   194
fun dest_hd f_ord t =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   195
  let val ord = f_ord t
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   196
  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
   197
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   198
fun term_lpo f_ord (s, t) =
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   199
  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
   200
    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
   201
    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
   202
        GREATER =>
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 GREATER else LESS
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   205
      | EQUAL =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   206
          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
   207
          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
   208
          else LESS
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   209
      | LESS => LESS
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   210
    else GREATER
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   211
  end
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   212
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
   213
    (Abs (_, T, t), Abs (_, U, u)) =>
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   214
      (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
   215
  | (_, _) => prod_ord (prod_ord int_ord
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   216
                  (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
   217
                (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
   218
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   219
in
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   220
val term_lpo = term_lpo
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   221
end;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   222
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   223
32841
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   224
(* tables and caches *)
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   225
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   226
structure Vartab = Table(type key = indexname val ord = fast_indexname_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   227
structure Sorttab = Table(type key = sort val ord = sort_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   228
structure Typtab = Table(type key = typ val ord = typ_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   229
structure Termtab = Table(type key = term val ord = fast_term_ord);
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   230
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   231
fun term_cache f = Cache.create Termtab.empty Termtab.lookup Termtab.update f;
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   232
29269
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   233
end;
5c25a2012975 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
wenzelm
parents:
diff changeset
   234
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   235
structure Basic_Term_Ord: BASIC_TERM_ORD = Term_Ord;
32841
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   236
open Basic_Term_Ord;
57dcddf81b01 added term_cache;
wenzelm
parents: 31976
diff changeset
   237
35408
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   238
structure Var_Graph = Graph(type key = indexname val ord = Term_Ord.fast_indexname_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   239
structure Sort_Graph = Graph(type key = sort val ord = Term_Ord.sort_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   240
structure Typ_Graph = Graph(type key = typ val ord = Term_Ord.typ_ord);
b48ab741683b modernized structure Term_Ord;
wenzelm
parents: 35406
diff changeset
   241
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
   242