--- a/src/HOL/Inductive.thy Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Inductive.thy Fri Sep 05 00:41:01 2014 +0200
@@ -273,7 +273,7 @@
ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
-ML_file "Tools/Old_Datatype/old_datatype_data.ML" setup Old_Datatype_Data.setup
+ML_file "Tools/Old_Datatype/old_datatype_data.ML"
ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
ML_file "Tools/Old_Datatype/old_primrec.ML"
--- a/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_def.ML Fri Sep 05 00:41:01 2014 +0200
@@ -1532,7 +1532,8 @@
Local_Theory.declaration {syntax = false, pervasive = true}
(fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
-fun register_bnf key bnf = register_bnf_raw key bnf #> interpret_bnf bnf;
+fun register_bnf key bnf =
+ register_bnf_raw key bnf #> interpret_bnf bnf;
fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
(fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -237,7 +237,7 @@
fp_sugars;
fun register_fp_sugars fp_sugars =
- register_fp_sugars fp_sugars #> interpret_fp_sugars fp_sugars;
+ register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
--- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -352,12 +352,11 @@
Type (T_name, _) =>
(case Ctr_Sugar.ctr_sugar_of ctxt T_name of
NONE => not_codatatype ctxt res_T
- | SOME {ctrs, discs, selss, ...} =>
+ | SOME {T = fpT, ctrs, discs, selss, ...} =>
let
val thy = Proof_Context.theory_of ctxt;
- val gfpT = body_type (fastype_of (hd ctrs));
- val As_rho = tvar_subst thy [gfpT] [res_T];
+ val As_rho = tvar_subst thy [fpT] [res_T];
val substA = Term.subst_TVars As_rho;
fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
@@ -384,11 +383,11 @@
val indices = map #fp_res_index fp_sugars;
val perm_indices = map #fp_res_index perm_fp_sugars;
- val perm_gfpTs = map #T perm_fp_sugars;
+ val perm_fpTs = map #T perm_fp_sugars;
val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
val nn0 = length res_Ts;
- val nn = length perm_gfpTs;
+ val nn = length perm_fpTs;
val kks = 0 upto nn - 1;
val perm_ns' = map length perm_ctrXs_Tsss';
@@ -426,10 +425,10 @@
val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
val f_Tssss = unpermute perm_f_Tssss;
- val gfpTs = unpermute perm_gfpTs;
+ val fpTs = unpermute perm_fpTs;
val Cs = unpermute perm_Cs;
- val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts;
+ val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
val substA = Term.subst_TVars As_rho;
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -152,7 +152,7 @@
val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
- val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
+ val perm_fpTs = map #T perm_basic_lfp_sugars;
val perm_Cs = map #C perm_basic_lfp_sugars;
val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
@@ -161,11 +161,11 @@
val inducts = unpermute0 (conj_dests nn common_induct);
- val lfpTs = unpermute perm_lfpTs;
+ val fpTs = unpermute perm_fpTs;
val Cs = unpermute perm_Cs;
val ctr_offsets = unpermute perm_ctr_offsets;
- val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
+ val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
val substA = Term.subst_TVars As_rho;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Sep 05 00:41:01 2014 +0200
@@ -8,7 +8,8 @@
signature CTR_SUGAR =
sig
type ctr_sugar =
- {ctrs: term list,
+ {T: typ,
+ ctrs: term list,
casex: term,
discs: term list,
selss: term list list,
@@ -45,8 +46,10 @@
val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
(ctr_sugar -> local_theory -> local_theory) -> theory -> theory
- val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
- val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
+ val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory
+ val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
+ val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory
+ val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory
val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
@@ -84,7 +87,8 @@
open Ctr_Sugar_Code
type ctr_sugar =
- {ctrs: term list,
+ {T: typ,
+ ctrs: term list,
casex: term,
discs: term list,
selss: term list list,
@@ -111,11 +115,12 @@
split_sel_asms: thm list,
case_eq_ifs: thm list};
-fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
+fun morph_ctr_sugar phi {T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
split_sel_asms, case_eq_ifs} =
- {ctrs = map (Morphism.term phi) ctrs,
+ {T = Morphism.typ phi T,
+ ctrs = map (Morphism.term phi) ctrs,
casex = Morphism.term phi casex,
discs = map (Morphism.term phi) discs,
selss = map (map (Morphism.term phi)) selss,
@@ -182,18 +187,22 @@
fun ctr_sugar_interpretation name =
Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
-fun register_ctr_sugar key ctr_sugar =
+val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
+
+fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
- #> Ctr_Sugar_Interpretation.data ctr_sugar;
+ (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
-fun default_register_ctr_sugar_global key ctr_sugar thy =
+fun register_ctr_sugar ctr_sugar =
+ register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar;
+
+fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy =
let val tab = Data.get (Context.Theory thy) in
- if Symtab.defined tab key then
+ if Symtab.defined tab s then
thy
else
thy
- |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab))
+ |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
|> Ctr_Sugar_Interpretation.data_global ctr_sugar
end;
@@ -1025,7 +1034,7 @@
|>> name_noted_thms fcT_name exhaustN;
val ctr_sugar =
- {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
+ {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
@@ -1036,7 +1045,7 @@
case_eq_ifs = case_eq_if_thms}
|> morph_ctr_sugar (substitute_noted_thm noted);
in
- (ctr_sugar, lthy' |> register_ctr_sugar fcT_name ctr_sugar)
+ (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar)
end;
in
(goalss, after_qed, lthy')
--- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML Fri Sep 05 00:41:01 2014 +0200
@@ -25,7 +25,6 @@
val mk_case_names_exhausts: descr -> string list -> attribute list
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
val interpretation_data : config * string list -> theory -> theory
- val setup: theory -> theory
end;
structure Old_Datatype_Data: OLD_DATATYPE_DATA =
@@ -97,32 +96,35 @@
fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) =
- {ctrs = ctrs_of_exhaust exhaust,
- casex = case_of_case_rewrite (hd case_rewrites),
- discs = [],
- selss = [],
- exhaust = exhaust,
- nchotomy = nchotomy,
- injects = inject,
- distincts = distinct,
- case_thms = case_rewrites,
- case_cong = case_cong,
- case_cong_weak = case_cong_weak,
- split = split,
- split_asm = split_asm,
- disc_defs = [],
- disc_thmss = [],
- discIs = [],
- sel_defs = [],
- sel_thmss = [],
- distinct_discsss = [],
- exhaust_discs = [],
- exhaust_sels = [],
- collapses = [],
- expands = [],
- split_sels = [],
- split_sel_asms = [],
- case_eq_ifs = []};
+ let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in
+ {T = body_type (fastype_of ctr1),
+ ctrs = ctrs,
+ casex = case_of_case_rewrite (hd case_rewrites),
+ discs = [],
+ selss = [],
+ exhaust = exhaust,
+ nchotomy = nchotomy,
+ injects = inject,
+ distincts = distinct,
+ case_thms = case_rewrites,
+ case_cong = case_cong,
+ case_cong_weak = case_cong_weak,
+ split = split,
+ split_asm = split_asm,
+ disc_defs = [],
+ disc_thmss = [],
+ discIs = [],
+ sel_defs = [],
+ sel_thmss = [],
+ distinct_discsss = [],
+ exhaust_discs = [],
+ exhaust_sels = [],
+ collapses = [],
+ expands = [],
+ split_sels = [],
+ split_sel_asms = [],
+ case_eq_ifs = []}
+ end;
fun register dt_infos =
Data.map (fn {types, constrs, cases} =>
@@ -133,8 +135,7 @@
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
- fold (fn (key, info) =>
- Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
+ fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
(* complex queries *)
@@ -283,9 +284,7 @@
(** setup theory **)
-val setup =
- antiq_setup #>
- Datatype_Interpretation.init;
+val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
open Old_Datatype_Aux;
--- a/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200
+++ b/src/HOL/Tools/record.ML Fri Sep 05 00:41:01 2014 +0200
@@ -1781,14 +1781,15 @@
end
else thy;
-fun add_ctr_sugar T_name ctr sels exhaust inject sel_defs sel_thms =
- Ctr_Sugar.default_register_ctr_sugar_global T_name
- {ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
- nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
- case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
- split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
- sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
- collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
+fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
+ Ctr_Sugar.default_register_ctr_sugar_global
+ {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
+ exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
+ case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
+ split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
+ discIs = [], sel_defs = sel_defs, sel_thmss = [sel_thms], distinct_discsss = [],
+ exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
+ split_sel_asms = [], case_eq_ifs = []};
(* definition *)
@@ -2234,7 +2235,7 @@
|> add_extfields extension_name (fields @ [(full_moreN, moreT)])
|> add_fieldext (extension_name, snd extension) names
|> add_code ext_tyco vs extT ext simps' ext_inject
- |> add_ctr_sugar ext_tyco (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
+ |> add_ctr_sugar (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
|> Sign.restore_naming thy;
in final_thy end;