added declare_typ_names;
authorwenzelm
Sat Sep 29 21:39:47 2007 +0200 (2007-09-29)
changeset 247628d7da66b1a2c
parent 24761 d762ab297a07
child 24763 da4a9986eccd
added declare_typ_names;
replace_dummy_patterns: canonical argument order;
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Sat Sep 29 21:39:46 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Sat Sep 29 21:39:47 2007 +0200
     1.3 @@ -185,6 +185,7 @@
     1.4    val maxidx_term: term -> int -> int
     1.5    val has_abs: term -> bool
     1.6    val dest_abs: string * typ * term -> string * term
     1.7 +  val declare_typ_names: typ -> Name.context -> Name.context
     1.8    val declare_term_names: term -> Name.context -> Name.context
     1.9    val variant_frees: term -> (string * 'a) list -> (string * 'a) list
    1.10    val dummy_patternN: string
    1.11 @@ -192,7 +193,7 @@
    1.12    val is_dummy_pattern: term -> bool
    1.13    val free_dummy_patterns: term -> Name.context -> term * Name.context
    1.14    val no_dummy_patterns: term -> term
    1.15 -  val replace_dummy_patterns: int * term -> int * term
    1.16 +  val replace_dummy_patterns: term -> int -> term * int
    1.17    val is_replaced_dummy_pattern: indexname -> bool
    1.18    val show_dummy_patterns: term -> term
    1.19    val string_of_vname: indexname -> string
    1.20 @@ -1225,12 +1226,14 @@
    1.21  
    1.22  (* renaming variables *)
    1.23  
    1.24 +val declare_typ_names = fold_atyps (fn TFree (a, _) => Name.declare a | _ => I);
    1.25 +
    1.26  fun declare_term_names tm =
    1.27    fold_aterms
    1.28      (fn Const (a, _) => Name.declare (NameSpace.base a)
    1.29        | Free (a, _) => Name.declare a
    1.30        | _ => I) tm #>
    1.31 -  fold_types (fold_atyps (fn TFree (a, _) => Name.declare a | _ => I)) tm;
    1.32 +  fold_types declare_typ_names tm;
    1.33  
    1.34  fun variant_frees t frees =
    1.35    fst (Name.variants (map fst frees) (declare_term_names t Name.context)) ~~ map snd frees;
    1.36 @@ -1264,15 +1267,17 @@
    1.37        in (t' $ u', used'') end
    1.38    | free_dummy_patterns a used = (a, used);
    1.39  
    1.40 -fun replace_dummy Ts (i, Const ("dummy_pattern", T)) =
    1.41 -      (i + 1, list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)))
    1.42 -  | replace_dummy Ts (i, Abs (x, T, t)) =
    1.43 -      let val (i', t') = replace_dummy (T :: Ts) (i, t)
    1.44 -      in (i', Abs (x, T, t')) end
    1.45 -  | replace_dummy Ts (i, t $ u) =
    1.46 -      let val (i', t') = replace_dummy Ts (i, t); val (i'', u') = replace_dummy Ts (i', u)
    1.47 -      in (i'', t' $ u') end
    1.48 -  | replace_dummy _ (i, a) = (i, a);
    1.49 +fun replace_dummy Ts (Const ("dummy_pattern", T)) i =
    1.50 +      (list_comb (Var (("_dummy_", i), Ts ---> T), map Bound (0 upto length Ts - 1)), i + 1)
    1.51 +  | replace_dummy Ts (Abs (x, T, t)) i =
    1.52 +      let val (t', i') = replace_dummy (T :: Ts) t i
    1.53 +      in (Abs (x, T, t'), i') end
    1.54 +  | replace_dummy Ts (t $ u) i =
    1.55 +      let
    1.56 +        val (t', i') = replace_dummy Ts t i;
    1.57 +        val (u', i'') = replace_dummy Ts u i';
    1.58 +      in (t' $ u', i'') end
    1.59 +  | replace_dummy _ a i = (a, i);
    1.60  
    1.61  val replace_dummy_patterns = replace_dummy [];
    1.62