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