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