--- a/src/Pure/term.ML Sat Jun 17 19:37:49 2006 +0200
+++ b/src/Pure/term.ML Sat Jun 17 19:37:50 2006 +0200
@@ -131,6 +131,7 @@
(*note reversed order of args wrt. variant!*)
val add_term_consts: term * string list -> string list
val term_consts: term -> string list
+ val exists_subtype: (typ -> bool) -> typ -> bool
val exists_subterm: (term -> bool) -> term -> bool
val exists_Const: (string * typ -> bool) -> term -> bool
val add_term_free_names: term * string list -> string list
@@ -185,6 +186,12 @@
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 internal: string -> string
+ val dest_internal: string -> string
+ val skolem: string -> string
+ val dest_skolem: string -> string
+ val generalize: string list * string list -> int -> term -> term
+ val generalizeT: string list -> int -> typ -> typ
val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
-> term -> term
val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
@@ -974,6 +981,60 @@
in subst tm end;
+(* internal identifiers *)
+
+val internal = suffix "_";
+val dest_internal = unsuffix "_";
+
+val skolem = suffix "__";
+val dest_skolem = unsuffix "__";
+
+
+(* generalization of fixed variables *)
+
+local exception SAME in
+
+fun generalizeT_same [] _ _ = raise SAME
+ | generalizeT_same tfrees idx ty =
+ let
+ fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
+ | gen_typ (TFree (a, S)) =
+ if member (op =) tfrees a then TVar ((a, idx), S)
+ else raise SAME
+ | gen_typ _ = raise SAME
+ and gen_typs (T :: Ts) =
+ (gen_typ T :: (gen_typs Ts handle SAME => Ts)
+ handle SAME => T :: gen_typs Ts)
+ | gen_typs [] = raise SAME;
+ in gen_typ ty end;
+
+fun generalize ([], []) _ tm = tm
+ | generalize (tfrees, frees) idx tm =
+ let
+ fun var ((x, i), T) =
+ (case try dest_internal x of
+ NONE => Var ((x, i), T)
+ | SOME x' => var ((x', i + 1), T));
+
+ val genT = generalizeT_same tfrees idx;
+ fun gen (Free (x, T)) =
+ if member (op =) frees x then var ((x, idx), genT T handle SAME => T)
+ else Free (x, genT T)
+ | gen (Var (xi, T)) = Var (xi, genT T)
+ | gen (Const (c, T)) = Const (c, genT T)
+ | gen (Bound _) = raise SAME
+ | gen (Abs (x, T, t)) =
+ (Abs (x, genT T, gen t handle SAME => t)
+ handle SAME => Abs (x, T, gen t))
+ | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
+ in gen tm handle SAME => tm end;
+
+fun generalizeT tfrees i ty =
+ generalizeT_same tfrees i ty handle SAME => ty;
+
+end;
+
+
(* instantiation of schematic variables (types before terms) *)
local exception SAME in
@@ -1094,14 +1155,13 @@
end;
-(** Consts etc. **)
+(* substructure *)
-fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
- | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
- | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
- | add_term_consts (_, cs) = cs;
-
-fun term_consts t = add_term_consts(t,[]);
+fun exists_subtype P =
+ let
+ fun ex ty = P ty orelse
+ (case ty of Type (_, Ts) => exists ex Ts | _ => false);
+ in ex end;
fun exists_subterm P =
let
@@ -1112,6 +1172,16 @@
| _ => false);
in ex end;
+
+(** Consts etc. **)
+
+fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
+ | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
+ | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
+ | add_term_consts (_, cs) = cs;
+
+fun term_consts t = add_term_consts(t,[]);
+
fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);