tuned hidden_polymorphism;
authorwenzelm
Tue Oct 16 17:06:13 2007 +0200 (2007-10-16)
changeset 250500dc445970b4b
parent 25049 ec0547a4fcf0
child 25051 71cd45fdf332
tuned hidden_polymorphism;
added close_schematic_term;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Tue Oct 16 17:06:11 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Tue Oct 16 17:06:13 2007 +0200
     1.3 @@ -161,7 +161,7 @@
     1.4    val add_tfreesT: typ -> (string * sort) list -> (string * sort) list
     1.5    val add_tfrees: term -> (string * sort) list -> (string * sort) list
     1.6    val add_frees: term -> (string * typ) list -> (string * typ) list
     1.7 -  val hidden_polymorphism: term -> typ -> (indexname * sort) list
     1.8 +  val hidden_polymorphism: term -> (indexname * sort) list
     1.9    val strip_abs_eta: int -> term -> (string * typ) list * term
    1.10    val fast_indexname_ord: indexname * indexname -> order
    1.11    val indexname_ord: indexname * indexname -> order
    1.12 @@ -179,6 +179,7 @@
    1.13    val eq_var: (indexname * typ) * (indexname * typ) -> bool
    1.14    val tvar_ord: (indexname * sort) * (indexname * sort) -> order
    1.15    val var_ord: (indexname * typ) * (indexname * typ) -> order
    1.16 +  val close_schematic_term: term -> term
    1.17    val maxidx_typ: typ -> int -> int
    1.18    val maxidx_typs: typ list -> int -> int
    1.19    val maxidx_term: term -> int -> int
    1.20 @@ -513,15 +514,17 @@
    1.21  val add_tfrees = fold_types add_tfreesT;
    1.22  val add_frees = fold_aterms (fn Free v => insert (op =) v | _ => I);
    1.23  
    1.24 -(*extra type variables in a term, not covered by the type*)
    1.25 -fun hidden_polymorphism t T =
    1.26 +(*extra type variables in a term, not covered by its type*)
    1.27 +fun hidden_polymorphism t =
    1.28    let
    1.29 +    val T = fastype_of t;
    1.30      val tvarsT = add_tvarsT T [];
    1.31      val extra_tvars = fold_types (fold_atyps
    1.32        (fn TVar v => if member (op =) tvarsT v then I else insert (op =) v | _ => I)) t [];
    1.33    in extra_tvars end;
    1.34  
    1.35  
    1.36 +
    1.37  (** Comparing terms, types, sorts etc. **)
    1.38  
    1.39  (* alpha equivalence -- tuned for equalities *)
    1.40 @@ -1003,6 +1006,13 @@
    1.41            | subst (t $ u) = subst t $ subst u;
    1.42        in subst tm end;
    1.43  
    1.44 +fun close_schematic_term t =
    1.45 +  let
    1.46 +    val extra_types = map (fn v => Const ("TYPE", itselfT (TVar v))) (hidden_polymorphism t);
    1.47 +    val extra_terms = map Var (rev (add_vars t []));
    1.48 +  in fold_rev lambda (extra_types @ extra_terms) t end;
    1.49 +
    1.50 +
    1.51  
    1.52  (** Identifying first-order terms **)
    1.53