ported TFL to mixture of old and new datatypes
authorblanchet
Mon Sep 01 19:57:48 2014 +0200 (2014-09-01)
changeset 581326dcee1f6ea65
parent 58131 1abeda3c3bc2
child 58133 c7cc358a6972
ported TFL to mixture of old and new datatypes
src/HOL/Tools/SMT/smt_normalize.ML
src/HOL/Tools/TFL/casesplit.ML
src/HOL/Tools/TFL/tfl.ML
src/HOL/Tools/TFL/thry.ML
     1.1 --- a/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:28:00 2014 +0200
     1.2 +++ b/src/HOL/Tools/SMT/smt_normalize.ML	Mon Sep 01 19:57:48 2014 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4      | @{const HOL.implies} $ _ $ _ => dest_cond_eq (Thm.dest_arg ct)
     1.5      | _ => raise CTERM ("no equation", [ct]))
     1.6  
     1.7 -  fun get_constrs thy (Type (n, _)) = these (Old_Datatype_Data.get_constrs thy n)
     1.8 +  fun get_constrs thy (Type (n, _)) = these (BNF_LFP_Compat.get_constrs thy n)
     1.9      | get_constrs _ _ = []
    1.10  
    1.11    fun is_constr thy (n, T) =
     2.1 --- a/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:28:00 2014 +0200
     2.2 +++ b/src/HOL/Tools/TFL/casesplit.ML	Mon Sep 01 19:57:48 2014 +0200
     2.3 @@ -24,7 +24,7 @@
     2.4                       Type(ty_str, _) => ty_str
     2.5                     | TFree(s,_)  => error ("Free type: " ^ s)
     2.6                     | TVar((s,i),_) => error ("Free variable: " ^ s)
     2.7 -      val {induct, ...} = Old_Datatype_Data.the_info thy ty_str
     2.8 +      val {induct, ...} = BNF_LFP_Compat.the_info thy BNF_LFP_Compat.Keep_Nesting ty_str
     2.9      in
    2.10        cases_thm_of_induct_thm induct
    2.11      end;
     3.1 --- a/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 19:28:00 2014 +0200
     3.2 +++ b/src/HOL/Tools/TFL/tfl.ML	Mon Sep 01 19:57:48 2014 +0200
     3.3 @@ -435,7 +435,7 @@
     3.4         put_simpset HOL_basic_ss ctxt
     3.5            addsimps case_rewrites
     3.6            |> fold (Simplifier.add_cong o #case_cong_weak o snd)
     3.7 -              (Symtab.dest (Old_Datatype_Data.get_all theory))
     3.8 +              (Symtab.dest (BNF_LFP_Compat.get_all theory BNF_LFP_Compat.Keep_Nesting))
     3.9       val corollaries' = map (Simplifier.simplify case_simpset) corollaries
    3.10       val extract = Rules.CONTEXT_REWRITE_RULE
    3.11                       (f, [R], @{thm cut_apply}, meta_tflCongs @ context_congs)
     4.1 --- a/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 19:28:00 2014 +0200
     4.2 +++ b/src/HOL/Tools/TFL/thry.ML	Mon Sep 01 19:57:48 2014 +0200
     4.3 @@ -58,20 +58,20 @@
     4.4   *---------------------------------------------------------------------------*)
     4.5  
     4.6  fun match_info thy dtco =
     4.7 -  case (Old_Datatype_Data.get_info thy dtco,
     4.8 -         Old_Datatype_Data.get_constrs thy dtco) of
     4.9 -      (SOME { case_name, ... }, SOME constructors) =>
    4.10 +  case (BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco,
    4.11 +         BNF_LFP_Compat.get_constrs thy dtco) of
    4.12 +      (SOME {case_name, ... }, SOME constructors) =>
    4.13          SOME {case_const = Const (case_name, Sign.the_const_type thy case_name), constructors = map Const constructors}
    4.14      | _ => NONE;
    4.15  
    4.16 -fun induct_info thy dtco = case Old_Datatype_Data.get_info thy dtco of
    4.17 +fun induct_info thy dtco = case BNF_LFP_Compat.get_info thy BNF_LFP_Compat.Keep_Nesting dtco of
    4.18          NONE => NONE
    4.19        | SOME {nchotomy, ...} =>
    4.20            SOME {nchotomy = nchotomy,
    4.21 -                constructors = (map Const o the o Old_Datatype_Data.get_constrs thy) dtco};
    4.22 +                constructors = (map Const o the o BNF_LFP_Compat.get_constrs thy) dtco};
    4.23  
    4.24  fun extract_info thy =
    4.25 - let val infos = map snd (Symtab.dest (Old_Datatype_Data.get_all thy))
    4.26 + let val infos = map snd (Symtab.dest (BNF_LFP_Compat.get_all thy BNF_LFP_Compat.Keep_Nesting))
    4.27   in {case_congs = map (mk_meta_eq o #case_cong) infos,
    4.28       case_rewrites = maps (map mk_meta_eq o #case_rewrites) infos}
    4.29   end;