# HG changeset patch # User wenzelm # Date 1332187833 -3600 # Node ID 8eac39af4ec0cfa1999bbf48ba244dba8daa975a # Parent f35f654f297d99b24d6db154c6700d5b4396ec4e moved some legacy stuff; diff -r f35f654f297d -r 8eac39af4ec0 src/HOL/Tools/Meson/meson.ML --- a/src/HOL/Tools/Meson/meson.ML Mon Mar 19 20:32:57 2012 +0100 +++ b/src/HOL/Tools/Meson/meson.ML Mon Mar 19 21:10:33 2012 +0100 @@ -752,7 +752,7 @@ (*Converting one theorem from a disjunction to a meta-level clause*) fun make_meta_clause th = - let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th + let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th in (zero_var_indexes o Thm.varifyT_global o thaw 0 o negated_asm_of_head o make_horn resolution_clause_rules) fth diff -r f35f654f297d -r 8eac39af4ec0 src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Mar 19 20:32:57 2012 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Mon Mar 19 21:10:33 2012 +0100 @@ -374,7 +374,7 @@ do_formula pos body_t #> (if also_skolems andalso will_surely_be_skolemized then add_pconst_to_table true - (legacy_gensym skolem_prefix, PType (order_of_type abs_T, [])) + (Misc_Legacy.gensym skolem_prefix, PType (order_of_type abs_T, [])) else I) and do_term_or_formula ext_arg T = diff -r f35f654f297d -r 8eac39af4ec0 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Mar 19 20:32:57 2012 +0100 +++ b/src/Pure/drule.ML Mon Mar 19 21:10:33 2012 +0100 @@ -20,8 +20,6 @@ val forall_elim_list: cterm list -> thm -> thm val gen_all: thm -> thm val lift_all: cterm -> thm -> thm - val legacy_freeze_thaw: thm -> thm * (thm -> thm) - val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm) val implies_elim_list: thm -> thm list -> thm val implies_intr_list: cterm list -> thm -> thm val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm @@ -299,52 +297,6 @@ #> Thm.close_derivation; -(*Convert all Vars in a theorem to Frees. Also return a function for - reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) - -fun legacy_freeze_thaw_robust th = - let val fth = Thm.legacy_freezeT th - val thy = Thm.theory_of_thm fth - in - case Thm.fold_terms Term.add_vars fth [] of - [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) - | vars => - let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix)) - val alist = map newName vars - fun mk_inst (v,T) = - (cterm_of thy (Var(v,T)), - cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) - val insts = map mk_inst vars - fun thaw i th' = (*i is non-negative increment for Var indexes*) - th' |> forall_intr_list (map #2 insts) - |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) - in (Thm.instantiate ([],insts) fth, thaw) end - end; - -(*Basic version of the function above. No option to rename Vars apart in thaw. - The Frees created from Vars have nice names.*) -fun legacy_freeze_thaw th = - let val fth = Thm.legacy_freezeT th - val thy = Thm.theory_of_thm fth - in - case Thm.fold_terms Term.add_vars fth [] of - [] => (fth, fn x => x) - | vars => - let fun newName (ix, _) (pairs, used) = - let val v = singleton (Name.variant_list used) (string_of_indexname ix) - in ((ix,v)::pairs, v::used) end; - val (alist, _) = - fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth []) - fun mk_inst (v, T) = - (cterm_of thy (Var(v,T)), - cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) - val insts = map mk_inst vars - fun thaw th' = - th' |> forall_intr_list (map #2 insts) - |> forall_elim_list (map #1 insts) - in (Thm.instantiate ([],insts) fth, thaw) end - end; - (*Rotates a rule's premises to the left by k*) fun rotate_prems 0 = I | rotate_prems k = Thm.permute_prems 0 k; diff -r f35f654f297d -r 8eac39af4ec0 src/Pure/library.ML --- a/src/Pure/library.ML Mon Mar 19 20:32:57 2012 +0100 +++ b/src/Pure/library.ML Mon Mar 19 21:10:33 2012 +0100 @@ -213,7 +213,6 @@ 'a -> 'b -> 'c * 'b val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list - val legacy_gensym: string -> string type serial = int val serial: unit -> serial val serial_string: unit -> string @@ -1043,27 +1042,6 @@ in part end; - -(* generating identifiers -- often fresh *) - -local -(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*) -fun gensym_char i = - if i<26 then chr (ord "A" + i) - else if i<52 then chr (ord "a" + i - 26) - else chr (ord "0" + i - 52); - -val char_vec = Vector.tabulate (62, gensym_char); -fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); - -val gensym_seed = Unsynchronized.ref (0: int); - -in - fun legacy_gensym pre = - pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed)); -end; - - (* serial numbers and abstract stamps *) type serial = int; diff -r f35f654f297d -r 8eac39af4ec0 src/Tools/misc_legacy.ML --- a/src/Tools/misc_legacy.ML Mon Mar 19 20:32:57 2012 +0100 +++ b/src/Tools/misc_legacy.ML Mon Mar 19 21:10:33 2012 +0100 @@ -23,6 +23,9 @@ val mk_defpair: term * term -> string * term val get_def: theory -> xstring -> thm val METAHYPS: (thm list -> tactic) -> int -> tactic + val gensym: string -> string + val freeze_thaw_robust: thm -> thm * (int -> thm -> thm) + val freeze_thaw: thm -> thm * (thm -> thm) end; structure Misc_Legacy: MISC_LEGACY = @@ -229,5 +232,71 @@ end; + +(* generating identifiers -- often fresh *) + +local +(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*) +fun gensym_char i = + if i<26 then chr (ord "A" + i) + else if i<52 then chr (ord "a" + i - 26) + else chr (ord "0" + i - 52); + +val char_vec = Vector.tabulate (62, gensym_char); +fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n))); + +val gensym_seed = Unsynchronized.ref (0: int); + +in + fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed)); end; + +(*Convert all Vars in a theorem to Frees. Also return a function for + reversing that operation. DOES NOT WORK FOR TYPE VARIABLES.*) + +fun freeze_thaw_robust th = + let val fth = Thm.legacy_freezeT th + val thy = Thm.theory_of_thm fth + in + case Thm.fold_terms Term.add_vars fth [] of + [] => (fth, fn i => fn x => x) (*No vars: nothing to do!*) + | vars => + let fun newName (ix,_) = (ix, gensym (string_of_indexname ix)) + val alist = map newName vars + fun mk_inst (v,T) = + (cterm_of thy (Var(v,T)), + cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) + val insts = map mk_inst vars + fun thaw i th' = (*i is non-negative increment for Var indexes*) + th' |> forall_intr_list (map #2 insts) + |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts) + in (Thm.instantiate ([],insts) fth, thaw) end + end; + +(*Basic version of the function above. No option to rename Vars apart in thaw. + The Frees created from Vars have nice names.*) +fun freeze_thaw th = + let val fth = Thm.legacy_freezeT th + val thy = Thm.theory_of_thm fth + in + case Thm.fold_terms Term.add_vars fth [] of + [] => (fth, fn x => x) + | vars => + let fun newName (ix, _) (pairs, used) = + let val v = singleton (Name.variant_list used) (string_of_indexname ix) + in ((ix,v)::pairs, v::used) end; + val (alist, _) = + fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth []) + fun mk_inst (v, T) = + (cterm_of thy (Var(v,T)), + cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T))) + val insts = map mk_inst vars + fun thaw th' = + th' |> forall_intr_list (map #2 insts) + |> forall_elim_list (map #1 insts) + in (Thm.instantiate ([],insts) fth, thaw) end + end; + +end; +