src/Pure/term.ML
changeset 19909 6b5574d64aa4
parent 19647 043921b0e587
child 20001 392e39bd1811
     1.1 --- a/src/Pure/term.ML	Sat Jun 17 19:37:49 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Sat Jun 17 19:37:50 2006 +0200
     1.3 @@ -131,6 +131,7 @@
     1.4      (*note reversed order of args wrt. variant!*)
     1.5    val add_term_consts: term * string list -> string list
     1.6    val term_consts: term -> string list
     1.7 +  val exists_subtype: (typ -> bool) -> typ -> bool
     1.8    val exists_subterm: (term -> bool) -> term -> bool
     1.9    val exists_Const: (string * typ -> bool) -> term -> bool
    1.10    val add_term_free_names: term * string list -> string list
    1.11 @@ -185,6 +186,12 @@
    1.12    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.13    val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.14    val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.15 +  val internal: string -> string
    1.16 +  val dest_internal: string -> string
    1.17 +  val skolem: string -> string
    1.18 +  val dest_skolem: string -> string
    1.19 +  val generalize: string list * string list -> int -> term -> term
    1.20 +  val generalizeT: string list -> int -> typ -> typ
    1.21    val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list
    1.22      -> term -> term
    1.23    val instantiateT: ((indexname * sort) * typ) list -> typ -> typ
    1.24 @@ -974,6 +981,60 @@
    1.25        in subst tm end;
    1.26  
    1.27  
    1.28 +(* internal identifiers *)
    1.29 +
    1.30 +val internal = suffix "_";
    1.31 +val dest_internal = unsuffix "_";
    1.32 +
    1.33 +val skolem = suffix "__";
    1.34 +val dest_skolem = unsuffix "__";
    1.35 +
    1.36 +
    1.37 +(* generalization of fixed variables *)
    1.38 +
    1.39 +local exception SAME in
    1.40 +
    1.41 +fun generalizeT_same [] _ _ = raise SAME
    1.42 +  | generalizeT_same tfrees idx ty =
    1.43 +      let
    1.44 +        fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
    1.45 +          | gen_typ (TFree (a, S)) =
    1.46 +              if member (op =) tfrees a then TVar ((a, idx), S)
    1.47 +              else raise SAME
    1.48 +          | gen_typ _ = raise SAME
    1.49 +        and gen_typs (T :: Ts) =
    1.50 +            (gen_typ T :: (gen_typs Ts handle SAME => Ts)
    1.51 +              handle SAME => T :: gen_typs Ts)
    1.52 +          | gen_typs [] = raise SAME;
    1.53 +      in gen_typ ty end;
    1.54 +
    1.55 +fun generalize ([], []) _ tm = tm
    1.56 +  | generalize (tfrees, frees) idx tm =
    1.57 +      let
    1.58 +        fun var ((x, i), T) =
    1.59 +          (case try dest_internal x of
    1.60 +            NONE => Var ((x, i), T)
    1.61 +          | SOME x' => var ((x', i + 1), T));
    1.62 +
    1.63 +        val genT = generalizeT_same tfrees idx;
    1.64 +        fun gen (Free (x, T)) =
    1.65 +              if member (op =) frees x then var ((x, idx), genT T handle SAME => T)
    1.66 +              else Free (x, genT T)
    1.67 +          | gen (Var (xi, T)) = Var (xi, genT T)
    1.68 +          | gen (Const (c, T)) = Const (c, genT T)
    1.69 +          | gen (Bound _) = raise SAME
    1.70 +          | gen (Abs (x, T, t)) =
    1.71 +              (Abs (x, genT T, gen t handle SAME => t)
    1.72 +                handle SAME => Abs (x, T, gen t))
    1.73 +          | gen (t $ u) = (gen t $ (gen u handle SAME => u) handle SAME => t $ gen u);
    1.74 +      in gen tm handle SAME => tm end;
    1.75 +
    1.76 +fun generalizeT tfrees i ty =
    1.77 +  generalizeT_same tfrees i ty handle SAME => ty;
    1.78 +
    1.79 +end;
    1.80 +
    1.81 +
    1.82  (* instantiation of schematic variables (types before terms) *)
    1.83  
    1.84  local exception SAME in
    1.85 @@ -1094,14 +1155,13 @@
    1.86        end;
    1.87  
    1.88  
    1.89 -(** Consts etc. **)
    1.90 +(* substructure *)
    1.91  
    1.92 -fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
    1.93 -  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
    1.94 -  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
    1.95 -  | add_term_consts (_, cs) = cs;
    1.96 -
    1.97 -fun term_consts t = add_term_consts(t,[]);
    1.98 +fun exists_subtype P =
    1.99 +  let
   1.100 +    fun ex ty = P ty orelse
   1.101 +      (case ty of Type (_, Ts) => exists ex Ts | _ => false);
   1.102 +  in ex end;
   1.103  
   1.104  fun exists_subterm P =
   1.105    let
   1.106 @@ -1112,6 +1172,16 @@
   1.107        | _ => false);
   1.108    in ex end;
   1.109  
   1.110 +
   1.111 +(** Consts etc. **)
   1.112 +
   1.113 +fun add_term_consts (Const (c, _), cs) = insert (op =) c cs
   1.114 +  | add_term_consts (t $ u, cs) = add_term_consts (t, add_term_consts (u, cs))
   1.115 +  | add_term_consts (Abs (_, _, t), cs) = add_term_consts (t, cs)
   1.116 +  | add_term_consts (_, cs) = cs;
   1.117 +
   1.118 +fun term_consts t = add_term_consts(t,[]);
   1.119 +
   1.120  fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
   1.121  
   1.122