--- a/src/Pure/term.ML Wed Dec 31 00:08:14 2008 +0100
+++ b/src/Pure/term.ML Wed Dec 31 15:30:10 2008 +0100
@@ -76,9 +76,6 @@
val it_term_types: (typ * 'a -> 'a) -> term * 'a -> 'a
val add_term_names: term * string list -> string list
val aconv: term * term -> bool
- structure Vartab: TABLE
- structure Typtab: TABLE
- structure Termtab: TABLE
val propT: typ
val strip_all_body: term -> term
val strip_all_vars: term -> (string * typ) list
@@ -92,8 +89,6 @@
val subst_bound: term * term -> term
val betapply: term * term -> term
val betapplys: term * term list -> term
- val eq_ix: indexname * indexname -> bool
- val could_unify: term * term -> bool
val subst_free: (term * term) list -> term -> term
val abstract_over: term * term -> term
val lambda: term -> term -> term
@@ -156,23 +151,14 @@
val add_free_names: term -> string list -> string list
val add_frees: term -> (string * typ) list -> (string * typ) list
val hidden_polymorphism: term -> (indexname * sort) list
+ val eq_ix: indexname * indexname -> bool
+ val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
+ val eq_var: (indexname * typ) * (indexname * typ) -> bool
+ val could_unify: term * term -> bool
val strip_abs_eta: int -> term -> (string * typ) list * term
- val fast_indexname_ord: indexname * indexname -> order
- val indexname_ord: indexname * indexname -> order
- val sort_ord: sort * sort -> order
- val typ_ord: typ * typ -> order
- val fast_term_ord: term * term -> order
- val term_ord: term * term -> order
- val hd_ord: term * term -> order
- val termless: term * term -> bool
- val term_lpo: (term -> int) -> term * term -> order
val match_bvars: (term * term) * (string * string) list -> (string * string) list
val map_abs_vars: (string -> string) -> term -> term
val rename_abs: term -> term -> term -> term option
- val eq_tvar: (indexname * sort) * (indexname * sort) -> bool
- val eq_var: (indexname * typ) * (indexname * typ) -> bool
- val tvar_ord: (indexname * sort) * (indexname * sort) -> order
- val var_ord: (indexname * typ) * (indexname * typ) -> order
val close_schematic_term: term -> term
val maxidx_typ: typ -> int -> int
val maxidx_typs: typ list -> int -> int
@@ -514,9 +500,17 @@
-(** Comparing terms, types, sorts etc. **)
+(** Comparing terms **)
+
+(* variables *)
+
+fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
-(* alpha equivalence -- tuned for equalities *)
+fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
+fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
+
+
+(* alpha equivalence *)
fun tm1 aconv tm2 =
pointer_eq (tm1, tm2) orelse
@@ -526,184 +520,24 @@
| (a1, a2) => a1 = a2);
-(* fast syntactic ordering -- tuned for inequalities *)
-
-fun fast_indexname_ord ((x, i), (y, j)) =
- (case int_ord (i, j) of EQUAL => fast_string_ord (x, y) | ord => ord);
-
-fun sort_ord SS =
- if pointer_eq SS then EQUAL
- else dict_ord fast_string_ord SS;
-
-local
-
-fun cons_nr (TVar _) = 0
- | cons_nr (TFree _) = 1
- | cons_nr (Type _) = 2;
-
-in
-
-fun typ_ord TU =
- if pointer_eq TU then EQUAL
- else
- (case TU of
- (Type (a, Ts), Type (b, Us)) =>
- (case fast_string_ord (a, b) of EQUAL => dict_ord typ_ord (Ts, Us) | ord => ord)
- | (TFree (a, S), TFree (b, S')) =>
- (case fast_string_ord (a, b) of EQUAL => sort_ord (S, S') | ord => ord)
- | (TVar (xi, S), TVar (yj, S')) =>
- (case fast_indexname_ord (xi, yj) of EQUAL => sort_ord (S, S') | ord => ord)
- | (T, U) => int_ord (cons_nr T, cons_nr U));
-
-end;
-
-local
-
-fun cons_nr (Const _) = 0
- | cons_nr (Free _) = 1
- | cons_nr (Var _) = 2
- | cons_nr (Bound _) = 3
- | cons_nr (Abs _) = 4
- | cons_nr (_ $ _) = 5;
-
-fun struct_ord (Abs (_, _, t), Abs (_, _, u)) = struct_ord (t, u)
- | struct_ord (t1 $ t2, u1 $ u2) =
- (case struct_ord (t1, u1) of EQUAL => struct_ord (t2, u2) | ord => ord)
- | struct_ord (t, u) = int_ord (cons_nr t, cons_nr u);
-
-fun atoms_ord (Abs (_, _, t), Abs (_, _, u)) = atoms_ord (t, u)
- | atoms_ord (t1 $ t2, u1 $ u2) =
- (case atoms_ord (t1, u1) of EQUAL => atoms_ord (t2, u2) | ord => ord)
- | atoms_ord (Const (a, _), Const (b, _)) = fast_string_ord (a, b)
- | atoms_ord (Free (x, _), Free (y, _)) = fast_string_ord (x, y)
- | atoms_ord (Var (xi, _), Var (yj, _)) = fast_indexname_ord (xi, yj)
- | atoms_ord (Bound i, Bound j) = int_ord (i, j)
- | atoms_ord _ = sys_error "atoms_ord";
-
-fun types_ord (Abs (_, T, t), Abs (_, U, u)) =
- (case typ_ord (T, U) of EQUAL => types_ord (t, u) | ord => ord)
- | types_ord (t1 $ t2, u1 $ u2) =
- (case types_ord (t1, u1) of EQUAL => types_ord (t2, u2) | ord => ord)
- | types_ord (Const (_, T), Const (_, U)) = typ_ord (T, U)
- | types_ord (Free (_, T), Free (_, U)) = typ_ord (T, U)
- | types_ord (Var (_, T), Var (_, U)) = typ_ord (T, U)
- | types_ord (Bound _, Bound _) = EQUAL
- | types_ord _ = sys_error "types_ord";
-
-in
-
-fun fast_term_ord tu =
- if pointer_eq tu then EQUAL
- else
- (case struct_ord tu of
- EQUAL => (case atoms_ord tu of EQUAL => types_ord tu | ord => ord)
- | ord => ord);
-
-structure Vartab = TableFun(type key = indexname val ord = fast_indexname_ord);
-structure Typtab = TableFun(type key = typ val ord = typ_ord);
-structure Termtab = TableFun(type key = term val ord = fast_term_ord);
-
-end;
-
-
-(* term_ord *)
-
-(*a linear well-founded AC-compatible ordering for terms:
- s < t <=> 1. size(s) < size(t) or
- 2. size(s) = size(t) and s=f(...) and t=g(...) and f<g or
- 3. size(s) = size(t) and s=f(s1..sn) and t=f(t1..tn) and
- (s1..sn) < (t1..tn) (lexicographically)*)
+(*A fast unification filter: true unless the two terms cannot be unified.
+ Terms must be NORMAL. Treats all Vars as distinct. *)
+fun could_unify (t, u) =
+ let
+ fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
+ | matchrands _ _ = true;
+ in
+ case (head_of t, head_of u) of
+ (_, Var _) => true
+ | (Var _, _) => true
+ | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
+ | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
+ | (Bound i, Bound j) => i = j andalso matchrands t u
+ | (Abs _, _) => true (*because of possible eta equality*)
+ | (_, Abs _) => true
+ | _ => false
+ end;
-fun indexname_ord ((x, i), (y, j)) =
- (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
-
-local
-
-fun hd_depth (t $ _, n) = hd_depth (t, n + 1)
- | hd_depth p = p;
-
-fun dest_hd (Const (a, T)) = (((a, 0), T), 0)
- | dest_hd (Free (a, T)) = (((a, 0), T), 1)
- | dest_hd (Var v) = (v, 2)
- | dest_hd (Bound i) = ((("", i), dummyT), 3)
- | dest_hd (Abs (_, T, _)) = ((("", 0), T), 4);
-
-in
-
-fun term_ord tu =
- if pointer_eq tu then EQUAL
- else
- (case tu of
- (Abs (_, T, t), Abs(_, U, u)) =>
- (case term_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
- | (t, u) =>
- (case int_ord (size_of_term t, size_of_term u) of
- EQUAL =>
- (case prod_ord hd_ord int_ord (hd_depth (t, 0), hd_depth (u, 0)) of
- EQUAL => args_ord (t, u) | ord => ord)
- | ord => ord))
-and hd_ord (f, g) =
- prod_ord (prod_ord indexname_ord typ_ord) int_ord (dest_hd f, dest_hd g)
-and args_ord (f $ t, g $ u) =
- (case args_ord (f, g) of EQUAL => term_ord (t, u) | ord => ord)
- | args_ord _ = EQUAL;
-
-fun termless tu = (term_ord tu = LESS);
-
-end;
-
-
-(** Lexicographic path order on terms **)
-
-(*
- See Baader & Nipkow, Term rewriting, CUP 1998.
- Without variables. Const, Var, Bound, Free and Abs are treated all as
- constants.
-
- f_ord maps terms to integers and serves two purposes:
- - Predicate on constant symbols. Those that are not recognised by f_ord
- must be mapped to ~1.
- - Order on the recognised symbols. These must be mapped to distinct
- integers >= 0.
- The argument of f_ord is never an application.
-*)
-
-local
-
-fun unrecognized (Const (a, T)) = ((1, ((a, 0), T)), 0)
- | unrecognized (Free (a, T)) = ((1, ((a, 0), T)), 0)
- | unrecognized (Var v) = ((1, v), 1)
- | unrecognized (Bound i) = ((1, (("", i), dummyT)), 2)
- | unrecognized (Abs (_, T, _)) = ((1, (("", 0), T)), 3);
-
-fun dest_hd f_ord t =
- let val ord = f_ord t
- in if ord = ~1 then unrecognized t else ((0, (("", ord), fastype_of t)), 0) end;
-
-fun term_lpo f_ord (s, t) =
- let val (f, ss) = strip_comb s and (g, ts) = strip_comb t in
- if forall (fn si => term_lpo f_ord (si, t) = LESS) ss
- then case hd_ord f_ord (f, g) of
- GREATER =>
- if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
- then GREATER else LESS
- | EQUAL =>
- if forall (fn ti => term_lpo f_ord (s, ti) = GREATER) ts
- then list_ord (term_lpo f_ord) (ss, ts)
- else LESS
- | LESS => LESS
- else GREATER
- end
-and hd_ord f_ord (f, g) = case (f, g) of
- (Abs (_, T, t), Abs (_, U, u)) =>
- (case term_lpo f_ord (t, u) of EQUAL => typ_ord (T, U) | ord => ord)
- | (_, _) => prod_ord (prod_ord int_ord
- (prod_ord indexname_ord typ_ord)) int_ord
- (dest_hd f_ord f, dest_hd f_ord g);
-
-in
-val term_lpo = term_lpo
-end;
(** Connectives of higher order logic **)
@@ -854,35 +688,6 @@
in (vs1 @ vs2, t'') end;
-(* comparing variables *)
-
-fun eq_ix ((x, i): indexname, (y, j)) = i = j andalso x = y;
-
-fun eq_tvar ((xi, S: sort), (xi', S')) = eq_ix (xi, xi') andalso S = S';
-fun eq_var ((xi, T: typ), (xi', T')) = eq_ix (xi, xi') andalso T = T';
-
-val tvar_ord = prod_ord indexname_ord sort_ord;
-val var_ord = prod_ord indexname_ord typ_ord;
-
-
-(*A fast unification filter: true unless the two terms cannot be unified.
- Terms must be NORMAL. Treats all Vars as distinct. *)
-fun could_unify (t, u) =
- let
- fun matchrands (f $ t) (g $ u) = could_unify (t, u) andalso matchrands f g
- | matchrands _ _ = true;
- in
- case (head_of t, head_of u) of
- (_, Var _) => true
- | (Var _, _) => true
- | (Const (a, _), Const (b, _)) => a = b andalso matchrands t u
- | (Free (a, _), Free (b, _)) => a = b andalso matchrands t u
- | (Bound i, Bound j) => i = j andalso matchrands t u
- | (Abs _, _) => true (*because of possible eta equality*)
- | (_, Abs _) => true
- | _ => false
- end;
-
(*Substitute new for free occurrences of old in a term*)
fun subst_free [] = I
| subst_free pairs =