moved some legacy stuff;
authorwenzelm
Mon Mar 19 21:10:33 2012 +0100 (2012-03-19)
changeset 470228eac39af4ec0
parent 47021 f35f654f297d
child 47023 c7a89ecbc71e
moved some legacy stuff;
src/HOL/Tools/Meson/meson.ML
src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML
src/Pure/drule.ML
src/Pure/library.ML
src/Tools/misc_legacy.ML
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 20:32:57 2012 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Mon Mar 19 21:10:33 2012 +0100
     1.3 @@ -752,7 +752,7 @@
     1.4  
     1.5  (*Converting one theorem from a disjunction to a meta-level clause*)
     1.6  fun make_meta_clause th =
     1.7 -  let val (fth,thaw) = Drule.legacy_freeze_thaw_robust th
     1.8 +  let val (fth,thaw) = Misc_Legacy.freeze_thaw_robust th
     1.9    in  
    1.10        (zero_var_indexes o Thm.varifyT_global o thaw 0 o 
    1.11         negated_asm_of_head o make_horn resolution_clause_rules) fth
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 19 20:32:57 2012 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML	Mon Mar 19 21:10:33 2012 +0100
     2.3 @@ -374,7 +374,7 @@
     2.4        do_formula pos body_t
     2.5        #> (if also_skolems andalso will_surely_be_skolemized then
     2.6              add_pconst_to_table true
     2.7 -                (legacy_gensym skolem_prefix, PType (order_of_type abs_T, []))
     2.8 +                (Misc_Legacy.gensym skolem_prefix, PType (order_of_type abs_T, []))
     2.9            else
    2.10              I)
    2.11      and do_term_or_formula ext_arg T =
     3.1 --- a/src/Pure/drule.ML	Mon Mar 19 20:32:57 2012 +0100
     3.2 +++ b/src/Pure/drule.ML	Mon Mar 19 21:10:33 2012 +0100
     3.3 @@ -20,8 +20,6 @@
     3.4    val forall_elim_list: cterm list -> thm -> thm
     3.5    val gen_all: thm -> thm
     3.6    val lift_all: cterm -> thm -> thm
     3.7 -  val legacy_freeze_thaw: thm -> thm * (thm -> thm)
     3.8 -  val legacy_freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
     3.9    val implies_elim_list: thm -> thm list -> thm
    3.10    val implies_intr_list: cterm list -> thm -> thm
    3.11    val instantiate_normalize: (ctyp * ctyp) list * (cterm * cterm) list -> thm -> thm
    3.12 @@ -299,52 +297,6 @@
    3.13    #> Thm.close_derivation;
    3.14  
    3.15  
    3.16 -(*Convert all Vars in a theorem to Frees.  Also return a function for
    3.17 -  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
    3.18 -
    3.19 -fun legacy_freeze_thaw_robust th =
    3.20 - let val fth = Thm.legacy_freezeT th
    3.21 -     val thy = Thm.theory_of_thm fth
    3.22 - in
    3.23 -   case Thm.fold_terms Term.add_vars fth [] of
    3.24 -       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
    3.25 -     | vars =>
    3.26 -         let fun newName (ix,_) = (ix, legacy_gensym (string_of_indexname ix))
    3.27 -             val alist = map newName vars
    3.28 -             fun mk_inst (v,T) =
    3.29 -                 (cterm_of thy (Var(v,T)),
    3.30 -                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    3.31 -             val insts = map mk_inst vars
    3.32 -             fun thaw i th' = (*i is non-negative increment for Var indexes*)
    3.33 -                 th' |> forall_intr_list (map #2 insts)
    3.34 -                     |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
    3.35 -         in  (Thm.instantiate ([],insts) fth, thaw)  end
    3.36 - end;
    3.37 -
    3.38 -(*Basic version of the function above. No option to rename Vars apart in thaw.
    3.39 -  The Frees created from Vars have nice names.*)
    3.40 -fun legacy_freeze_thaw th =
    3.41 - let val fth = Thm.legacy_freezeT th
    3.42 -     val thy = Thm.theory_of_thm fth
    3.43 - in
    3.44 -   case Thm.fold_terms Term.add_vars fth [] of
    3.45 -       [] => (fth, fn x => x)
    3.46 -     | vars =>
    3.47 -         let fun newName (ix, _) (pairs, used) =
    3.48 -                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    3.49 -                   in  ((ix,v)::pairs, v::used)  end;
    3.50 -             val (alist, _) =
    3.51 -                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
    3.52 -             fun mk_inst (v, T) =
    3.53 -                 (cterm_of thy (Var(v,T)),
    3.54 -                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    3.55 -             val insts = map mk_inst vars
    3.56 -             fun thaw th' =
    3.57 -                 th' |> forall_intr_list (map #2 insts)
    3.58 -                     |> forall_elim_list (map #1 insts)
    3.59 -         in  (Thm.instantiate ([],insts) fth, thaw)  end
    3.60 - end;
    3.61 -
    3.62  (*Rotates a rule's premises to the left by k*)
    3.63  fun rotate_prems 0 = I
    3.64    | rotate_prems k = Thm.permute_prems 0 k;
     4.1 --- a/src/Pure/library.ML	Mon Mar 19 20:32:57 2012 +0100
     4.2 +++ b/src/Pure/library.ML	Mon Mar 19 21:10:33 2012 +0100
     4.3 @@ -213,7 +213,6 @@
     4.4      'a -> 'b -> 'c * 'b
     4.5    val partition_eq: ('a * 'a -> bool) -> 'a list -> 'a list list
     4.6    val partition_list: (int -> 'a -> bool) -> int -> int -> 'a list -> 'a list list
     4.7 -  val legacy_gensym: string -> string
     4.8    type serial = int
     4.9    val serial: unit -> serial
    4.10    val serial_string: unit -> string
    4.11 @@ -1043,27 +1042,6 @@
    4.12    in part end;
    4.13  
    4.14  
    4.15 -
    4.16 -(* generating identifiers -- often fresh *)
    4.17 -
    4.18 -local
    4.19 -(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
    4.20 -fun gensym_char i =
    4.21 -  if i<26 then chr (ord "A" + i)
    4.22 -  else if i<52 then chr (ord "a" + i - 26)
    4.23 -  else chr (ord "0" + i - 52);
    4.24 -
    4.25 -val char_vec = Vector.tabulate (62, gensym_char);
    4.26 -fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
    4.27 -
    4.28 -val gensym_seed = Unsynchronized.ref (0: int);
    4.29 -
    4.30 -in
    4.31 -  fun legacy_gensym pre =
    4.32 -    pre ^ newid (NAMED_CRITICAL "legacy_gensym" (fn () => Unsynchronized.inc gensym_seed));
    4.33 -end;
    4.34 -
    4.35 -
    4.36  (* serial numbers and abstract stamps *)
    4.37  
    4.38  type serial = int;
     5.1 --- a/src/Tools/misc_legacy.ML	Mon Mar 19 20:32:57 2012 +0100
     5.2 +++ b/src/Tools/misc_legacy.ML	Mon Mar 19 21:10:33 2012 +0100
     5.3 @@ -23,6 +23,9 @@
     5.4    val mk_defpair: term * term -> string * term
     5.5    val get_def: theory -> xstring -> thm
     5.6    val METAHYPS: (thm list -> tactic) -> int -> tactic
     5.7 +  val gensym: string -> string
     5.8 +  val freeze_thaw_robust: thm -> thm * (int -> thm -> thm)
     5.9 +  val freeze_thaw: thm -> thm * (thm -> thm)
    5.10  end;
    5.11  
    5.12  structure Misc_Legacy: MISC_LEGACY =
    5.13 @@ -229,5 +232,71 @@
    5.14  
    5.15  end;
    5.16  
    5.17 +
    5.18 +(* generating identifiers -- often fresh *)
    5.19 +
    5.20 +local
    5.21 +(*Maps 0-61 to A-Z, a-z, 0-9; exclude _ or ' to avoid clash with internal/unusual indentifiers*)
    5.22 +fun gensym_char i =
    5.23 +  if i<26 then chr (ord "A" + i)
    5.24 +  else if i<52 then chr (ord "a" + i - 26)
    5.25 +  else chr (ord "0" + i - 52);
    5.26 +
    5.27 +val char_vec = Vector.tabulate (62, gensym_char);
    5.28 +fun newid n = implode (map (fn i => Vector.sub (char_vec, i)) (radixpand (62, n)));
    5.29 +
    5.30 +val gensym_seed = Unsynchronized.ref (0: int);
    5.31 +
    5.32 +in
    5.33 +  fun gensym pre = pre ^ newid (CRITICAL (fn () => Unsynchronized.inc gensym_seed));
    5.34  end;
    5.35  
    5.36 +
    5.37 +(*Convert all Vars in a theorem to Frees.  Also return a function for
    5.38 +  reversing that operation.  DOES NOT WORK FOR TYPE VARIABLES.*)
    5.39 +
    5.40 +fun freeze_thaw_robust th =
    5.41 + let val fth = Thm.legacy_freezeT th
    5.42 +     val thy = Thm.theory_of_thm fth
    5.43 + in
    5.44 +   case Thm.fold_terms Term.add_vars fth [] of
    5.45 +       [] => (fth, fn i => fn x => x)   (*No vars: nothing to do!*)
    5.46 +     | vars =>
    5.47 +         let fun newName (ix,_) = (ix, gensym (string_of_indexname ix))
    5.48 +             val alist = map newName vars
    5.49 +             fun mk_inst (v,T) =
    5.50 +                 (cterm_of thy (Var(v,T)),
    5.51 +                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    5.52 +             val insts = map mk_inst vars
    5.53 +             fun thaw i th' = (*i is non-negative increment for Var indexes*)
    5.54 +                 th' |> forall_intr_list (map #2 insts)
    5.55 +                     |> forall_elim_list (map (Thm.incr_indexes_cterm i o #1) insts)
    5.56 +         in  (Thm.instantiate ([],insts) fth, thaw)  end
    5.57 + end;
    5.58 +
    5.59 +(*Basic version of the function above. No option to rename Vars apart in thaw.
    5.60 +  The Frees created from Vars have nice names.*)
    5.61 +fun freeze_thaw th =
    5.62 + let val fth = Thm.legacy_freezeT th
    5.63 +     val thy = Thm.theory_of_thm fth
    5.64 + in
    5.65 +   case Thm.fold_terms Term.add_vars fth [] of
    5.66 +       [] => (fth, fn x => x)
    5.67 +     | vars =>
    5.68 +         let fun newName (ix, _) (pairs, used) =
    5.69 +                   let val v = singleton (Name.variant_list used) (string_of_indexname ix)
    5.70 +                   in  ((ix,v)::pairs, v::used)  end;
    5.71 +             val (alist, _) =
    5.72 +                 fold_rev newName vars ([], Thm.fold_terms Term.add_free_names fth [])
    5.73 +             fun mk_inst (v, T) =
    5.74 +                 (cterm_of thy (Var(v,T)),
    5.75 +                  cterm_of thy (Free(((the o AList.lookup (op =) alist) v), T)))
    5.76 +             val insts = map mk_inst vars
    5.77 +             fun thaw th' =
    5.78 +                 th' |> forall_intr_list (map #2 insts)
    5.79 +                     |> forall_elim_list (map #1 insts)
    5.80 +         in  (Thm.instantiate ([],insts) fth, thaw)  end
    5.81 + end;
    5.82 +
    5.83 +end;
    5.84 +