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