fixed infinite loops in 'register' functions + more uniform API
authorblanchet
Fri Sep 05 00:41:01 2014 +0200 (2014-09-05)
changeset 58187d2ddd401d74d
parent 58186 a6c3962ea907
child 58188 cc71d2be4f0a
fixed infinite loops in 'register' functions + more uniform API
src/HOL/Inductive.thy
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML
src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
src/HOL/Tools/Old_Datatype/old_datatype_data.ML
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Fri Sep 05 00:41:01 2014 +0200
     1.3 @@ -273,7 +273,7 @@
     1.4  
     1.5  ML_file "Tools/Old_Datatype/old_datatype_aux.ML"
     1.6  ML_file "Tools/Old_Datatype/old_datatype_prop.ML"
     1.7 -ML_file "Tools/Old_Datatype/old_datatype_data.ML" setup Old_Datatype_Data.setup
     1.8 +ML_file "Tools/Old_Datatype/old_datatype_data.ML"
     1.9  ML_file "Tools/Old_Datatype/old_rep_datatype.ML"
    1.10  ML_file "Tools/Old_Datatype/old_datatype_codegen.ML"
    1.11  ML_file "Tools/Old_Datatype/old_primrec.ML"
     2.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Fri Sep 05 00:41:01 2014 +0200
     2.3 @@ -1532,7 +1532,8 @@
     2.4    Local_Theory.declaration {syntax = false, pervasive = true}
     2.5      (fn phi => Data.map (Symtab.update (key, morph_bnf phi bnf)));
     2.6  
     2.7 -fun register_bnf key bnf = register_bnf_raw key bnf #> interpret_bnf bnf;
     2.8 +fun register_bnf key bnf =
     2.9 +  register_bnf_raw key bnf #> interpret_bnf bnf;
    2.10  
    2.11  fun bnf_def const_policy fact_policy internal qualify tacs wit_tac Ds map_b rel_b set_bs =
    2.12    (fn (_, goals, (triv_tac_opt, wit_goalss), after_qed, lthy, one_step_defs) =>
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     3.3 @@ -237,7 +237,7 @@
     3.4      fp_sugars;
     3.5  
     3.6  fun register_fp_sugars fp_sugars =
     3.7 -  register_fp_sugars fp_sugars #> interpret_fp_sugars fp_sugars;
     3.8 +  register_fp_sugars_raw fp_sugars #> interpret_fp_sugars fp_sugars;
     3.9  
    3.10  fun interpret_bnfs_register_fp_sugars Ts BTs Xs fp pre_bnfs absT_infos fp_nesting_bnfs
    3.11      live_nesting_bnfs fp_res ctrXs_Tsss ctr_defss ctr_sugars co_recs co_rec_defs mapss
     4.1 --- a/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     4.2 +++ b/src/HOL/Tools/BNF/bnf_gfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     4.3 @@ -352,12 +352,11 @@
     4.4      Type (T_name, _) =>
     4.5      (case Ctr_Sugar.ctr_sugar_of ctxt T_name of
     4.6        NONE => not_codatatype ctxt res_T
     4.7 -    | SOME {ctrs, discs, selss, ...} =>
     4.8 +    | SOME {T = fpT, ctrs, discs, selss, ...} =>
     4.9        let
    4.10          val thy = Proof_Context.theory_of ctxt;
    4.11  
    4.12 -        val gfpT = body_type (fastype_of (hd ctrs));
    4.13 -        val As_rho = tvar_subst thy [gfpT] [res_T];
    4.14 +        val As_rho = tvar_subst thy [fpT] [res_T];
    4.15          val substA = Term.subst_TVars As_rho;
    4.16  
    4.17          fun mk_spec ctr disc sels = {ctr = substA ctr, disc = substA disc, sels = map substA sels};
    4.18 @@ -384,11 +383,11 @@
    4.19      val indices = map #fp_res_index fp_sugars;
    4.20      val perm_indices = map #fp_res_index perm_fp_sugars;
    4.21  
    4.22 -    val perm_gfpTs = map #T perm_fp_sugars;
    4.23 +    val perm_fpTs = map #T perm_fp_sugars;
    4.24      val perm_ctrXs_Tsss' = map (repair_nullary_single_ctr o #ctrXs_Tss) perm_fp_sugars;
    4.25  
    4.26      val nn0 = length res_Ts;
    4.27 -    val nn = length perm_gfpTs;
    4.28 +    val nn = length perm_fpTs;
    4.29      val kks = 0 upto nn - 1;
    4.30      val perm_ns' = map length perm_ctrXs_Tsss';
    4.31  
    4.32 @@ -426,10 +425,10 @@
    4.33      val f_issss = map (map (map (map (find_index_eq fun_arg_hs)))) (unpermute perm_f_hssss);
    4.34  
    4.35      val f_Tssss = unpermute perm_f_Tssss;
    4.36 -    val gfpTs = unpermute perm_gfpTs;
    4.37 +    val fpTs = unpermute perm_fpTs;
    4.38      val Cs = unpermute perm_Cs;
    4.39  
    4.40 -    val As_rho = tvar_subst thy (take nn0 gfpTs) res_Ts;
    4.41 +    val As_rho = tvar_subst thy (take nn0 fpTs) res_Ts;
    4.42      val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn arg_Ts;
    4.43  
    4.44      val substA = Term.subst_TVars As_rho;
     5.1 --- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     5.2 +++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     5.3 @@ -152,7 +152,7 @@
     5.4  
     5.5      val perm_ctr_offsets = map (fn kk => Integer.sum (map length (take kk perm_ctrss))) kks;
     5.6  
     5.7 -    val perm_lfpTs = map (body_type o fastype_of o hd) perm_ctrss;
     5.8 +    val perm_fpTs = map #T perm_basic_lfp_sugars;
     5.9      val perm_Cs = map #C perm_basic_lfp_sugars;
    5.10      val perm_fun_arg_Tssss = map #fun_arg_Tsss perm_basic_lfp_sugars;
    5.11  
    5.12 @@ -161,11 +161,11 @@
    5.13  
    5.14      val inducts = unpermute0 (conj_dests nn common_induct);
    5.15  
    5.16 -    val lfpTs = unpermute perm_lfpTs;
    5.17 +    val fpTs = unpermute perm_fpTs;
    5.18      val Cs = unpermute perm_Cs;
    5.19      val ctr_offsets = unpermute perm_ctr_offsets;
    5.20  
    5.21 -    val As_rho = tvar_subst thy (take nn0 lfpTs) arg_Ts;
    5.22 +    val As_rho = tvar_subst thy (take nn0 fpTs) arg_Ts;
    5.23      val Cs_rho = map (fst o dest_TVar) Cs ~~ pad_list HOLogic.unitT nn res_Ts;
    5.24  
    5.25      val substA = Term.subst_TVars As_rho;
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Fri Sep 05 00:41:01 2014 +0200
     6.3 @@ -8,7 +8,8 @@
     6.4  signature CTR_SUGAR =
     6.5  sig
     6.6    type ctr_sugar =
     6.7 -    {ctrs: term list,
     6.8 +    {T: typ,
     6.9 +     ctrs: term list,
    6.10       casex: term,
    6.11       discs: term list,
    6.12       selss: term list list,
    6.13 @@ -45,8 +46,10 @@
    6.14    val ctr_sugar_of_case_global: theory -> string -> ctr_sugar option
    6.15    val ctr_sugar_interpretation: string -> (ctr_sugar -> theory -> theory) ->
    6.16      (ctr_sugar -> local_theory -> local_theory) -> theory -> theory
    6.17 -  val register_ctr_sugar: string -> ctr_sugar -> local_theory -> local_theory
    6.18 -  val default_register_ctr_sugar_global: string -> ctr_sugar -> theory -> theory
    6.19 +  val interpret_ctr_sugar: ctr_sugar -> local_theory -> local_theory
    6.20 +  val register_ctr_sugar_raw: ctr_sugar -> local_theory -> local_theory
    6.21 +  val register_ctr_sugar: ctr_sugar -> local_theory -> local_theory
    6.22 +  val default_register_ctr_sugar_global: ctr_sugar -> theory -> theory
    6.23  
    6.24    val mk_half_pairss: 'a list * 'a list -> ('a * 'a) list list
    6.25    val join_halves: int -> 'a list list -> 'a list list -> 'a list * 'a list list list
    6.26 @@ -84,7 +87,8 @@
    6.27  open Ctr_Sugar_Code
    6.28  
    6.29  type ctr_sugar =
    6.30 -  {ctrs: term list,
    6.31 +  {T: typ,
    6.32 +   ctrs: term list,
    6.33     casex: term,
    6.34     discs: term list,
    6.35     selss: term list list,
    6.36 @@ -111,11 +115,12 @@
    6.37     split_sel_asms: thm list,
    6.38     case_eq_ifs: thm list};
    6.39  
    6.40 -fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    6.41 +fun morph_ctr_sugar phi {T, ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    6.42      case_thms, case_cong, case_cong_weak, split, split_asm, disc_defs, disc_thmss, discIs, sel_defs,
    6.43      sel_thmss, distinct_discsss, exhaust_discs, exhaust_sels, collapses, expands, split_sels,
    6.44      split_sel_asms, case_eq_ifs} =
    6.45 -  {ctrs = map (Morphism.term phi) ctrs,
    6.46 +  {T = Morphism.typ phi T,
    6.47 +   ctrs = map (Morphism.term phi) ctrs,
    6.48     casex = Morphism.term phi casex,
    6.49     discs = map (Morphism.term phi) discs,
    6.50     selss = map (map (Morphism.term phi)) selss,
    6.51 @@ -182,18 +187,22 @@
    6.52  fun ctr_sugar_interpretation name =
    6.53    Ctr_Sugar_Interpretation.interpretation name o with_transfer_ctr_sugar;
    6.54  
    6.55 -fun register_ctr_sugar key ctr_sugar =
    6.56 +val interpret_ctr_sugar = Ctr_Sugar_Interpretation.data;
    6.57 +
    6.58 +fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
    6.59    Local_Theory.declaration {syntax = false, pervasive = true}
    6.60 -    (fn phi => Data.map (Symtab.update (key, morph_ctr_sugar phi ctr_sugar)))
    6.61 -  #> Ctr_Sugar_Interpretation.data ctr_sugar;
    6.62 +    (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
    6.63  
    6.64 -fun default_register_ctr_sugar_global key ctr_sugar thy =
    6.65 +fun register_ctr_sugar ctr_sugar =
    6.66 +  register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar ctr_sugar;
    6.67 +
    6.68 +fun default_register_ctr_sugar_global (ctr_sugar as {T = Type (s, _), ...}) thy =
    6.69    let val tab = Data.get (Context.Theory thy) in
    6.70 -    if Symtab.defined tab key then
    6.71 +    if Symtab.defined tab s then
    6.72        thy
    6.73      else
    6.74        thy
    6.75 -      |> Context.theory_map (Data.put (Symtab.update_new (key, ctr_sugar) tab))
    6.76 +      |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
    6.77        |> Ctr_Sugar_Interpretation.data_global ctr_sugar
    6.78    end;
    6.79  
    6.80 @@ -1025,7 +1034,7 @@
    6.81            |>> name_noted_thms fcT_name exhaustN;
    6.82  
    6.83          val ctr_sugar =
    6.84 -          {ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    6.85 +          {T = fcT, ctrs = ctrs, casex = casex, discs = discs, selss = selss, exhaust = exhaust_thm,
    6.86             nchotomy = nchotomy_thm, injects = inject_thms, distincts = distinct_thms,
    6.87             case_thms = case_thms, case_cong = case_cong_thm, case_cong_weak = case_cong_weak_thm,
    6.88             split = split_thm, split_asm = split_asm_thm, disc_defs = disc_defs,
    6.89 @@ -1036,7 +1045,7 @@
    6.90             case_eq_ifs = case_eq_if_thms}
    6.91            |> morph_ctr_sugar (substitute_noted_thm noted);
    6.92        in
    6.93 -        (ctr_sugar, lthy' |> register_ctr_sugar fcT_name ctr_sugar)
    6.94 +        (ctr_sugar, lthy' |> register_ctr_sugar ctr_sugar)
    6.95        end;
    6.96    in
    6.97      (goalss, after_qed, lthy')
     7.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
     7.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype_data.ML	Fri Sep 05 00:41:01 2014 +0200
     7.3 @@ -25,7 +25,6 @@
     7.4    val mk_case_names_exhausts: descr -> string list -> attribute list
     7.5    val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
     7.6    val interpretation_data : config * string list -> theory -> theory
     7.7 -  val setup: theory -> theory
     7.8  end;
     7.9  
    7.10  structure Old_Datatype_Data: OLD_DATATYPE_DATA =
    7.11 @@ -97,32 +96,35 @@
    7.12  
    7.13  fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
    7.14      case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) =
    7.15 -  {ctrs = ctrs_of_exhaust exhaust,
    7.16 -   casex = case_of_case_rewrite (hd case_rewrites),
    7.17 -   discs = [],
    7.18 -   selss = [],
    7.19 -   exhaust = exhaust,
    7.20 -   nchotomy = nchotomy,
    7.21 -   injects = inject,
    7.22 -   distincts = distinct,
    7.23 -   case_thms = case_rewrites,
    7.24 -   case_cong = case_cong,
    7.25 -   case_cong_weak = case_cong_weak,
    7.26 -   split = split,
    7.27 -   split_asm = split_asm,
    7.28 -   disc_defs = [],
    7.29 -   disc_thmss = [],
    7.30 -   discIs = [],
    7.31 -   sel_defs = [],
    7.32 -   sel_thmss = [],
    7.33 -   distinct_discsss = [],
    7.34 -   exhaust_discs = [],
    7.35 -   exhaust_sels = [],
    7.36 -   collapses = [],
    7.37 -   expands = [],
    7.38 -   split_sels = [],
    7.39 -   split_sel_asms = [],
    7.40 -   case_eq_ifs = []};
    7.41 +  let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in
    7.42 +    {T = body_type (fastype_of ctr1),
    7.43 +     ctrs = ctrs,
    7.44 +     casex = case_of_case_rewrite (hd case_rewrites),
    7.45 +     discs = [],
    7.46 +     selss = [],
    7.47 +     exhaust = exhaust,
    7.48 +     nchotomy = nchotomy,
    7.49 +     injects = inject,
    7.50 +     distincts = distinct,
    7.51 +     case_thms = case_rewrites,
    7.52 +     case_cong = case_cong,
    7.53 +     case_cong_weak = case_cong_weak,
    7.54 +     split = split,
    7.55 +     split_asm = split_asm,
    7.56 +     disc_defs = [],
    7.57 +     disc_thmss = [],
    7.58 +     discIs = [],
    7.59 +     sel_defs = [],
    7.60 +     sel_thmss = [],
    7.61 +     distinct_discsss = [],
    7.62 +     exhaust_discs = [],
    7.63 +     exhaust_sels = [],
    7.64 +     collapses = [],
    7.65 +     expands = [],
    7.66 +     split_sels = [],
    7.67 +     split_sel_asms = [],
    7.68 +     case_eq_ifs = []}
    7.69 +  end;
    7.70  
    7.71  fun register dt_infos =
    7.72    Data.map (fn {types, constrs, cases} =>
    7.73 @@ -133,8 +135,7 @@
    7.74            map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
    7.75       cases = cases |> fold Symtab.update
    7.76         (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
    7.77 -  fold (fn (key, info) =>
    7.78 -    Ctr_Sugar.default_register_ctr_sugar_global key (ctr_sugar_of_info info)) dt_infos;
    7.79 +  fold (Ctr_Sugar.default_register_ctr_sugar_global o ctr_sugar_of_info o snd) dt_infos;
    7.80  
    7.81  
    7.82  (* complex queries *)
    7.83 @@ -283,9 +284,7 @@
    7.84  
    7.85  (** setup theory **)
    7.86  
    7.87 -val setup =
    7.88 -  antiq_setup #>
    7.89 -  Datatype_Interpretation.init;
    7.90 +val _ = Theory.setup (antiq_setup #> Datatype_Interpretation.init);
    7.91  
    7.92  open Old_Datatype_Aux;
    7.93  
     8.1 --- a/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
     8.2 +++ b/src/HOL/Tools/record.ML	Fri Sep 05 00:41:01 2014 +0200
     8.3 @@ -1781,14 +1781,15 @@
     8.4      end
     8.5    else thy;
     8.6  
     8.7 -fun add_ctr_sugar T_name ctr sels exhaust inject sel_defs sel_thms =
     8.8 -  Ctr_Sugar.default_register_ctr_sugar_global T_name
     8.9 -    {ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels], exhaust = exhaust,
    8.10 -     nchotomy = Drule.dummy_thm, injects = [inject], distincts = [], case_thms = [],
    8.11 -     case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm, split = Drule.dummy_thm,
    8.12 -     split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [], discIs = [], sel_defs = sel_defs,
    8.13 -     sel_thmss = [sel_thms], distinct_discsss = [], exhaust_discs = [], exhaust_sels = [],
    8.14 -     collapses = [], expands = [], split_sels = [], split_sel_asms = [], case_eq_ifs = []};
    8.15 +fun add_ctr_sugar ctr sels exhaust inject sel_defs sel_thms =
    8.16 +  Ctr_Sugar.default_register_ctr_sugar_global
    8.17 +    {T = body_type (fastype_of ctr), ctrs = [ctr], casex = Term.dummy, discs = [], selss = [sels],
    8.18 +     exhaust = exhaust, nchotomy = Drule.dummy_thm, injects = [inject], distincts = [],
    8.19 +     case_thms = [], case_cong = Drule.dummy_thm, case_cong_weak = Drule.dummy_thm,
    8.20 +     split = Drule.dummy_thm, split_asm = Drule.dummy_thm, disc_defs = [], disc_thmss = [],
    8.21 +     discIs = [], sel_defs = sel_defs, sel_thmss = [sel_thms], distinct_discsss = [],
    8.22 +     exhaust_discs = [], exhaust_sels = [], collapses = [], expands = [], split_sels = [],
    8.23 +     split_sel_asms = [], case_eq_ifs = []};
    8.24  
    8.25  
    8.26  (* definition *)
    8.27 @@ -2234,7 +2235,7 @@
    8.28        |> add_extfields extension_name (fields @ [(full_moreN, moreT)])
    8.29        |> add_fieldext (extension_name, snd extension) names
    8.30        |> add_code ext_tyco vs extT ext simps' ext_inject
    8.31 -      |> add_ctr_sugar ext_tyco (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
    8.32 +      |> add_ctr_sugar (Const ext) sels cases_scheme' ext_inject sel_defs' sel_convs'
    8.33        |> Sign.restore_naming thy;
    8.34  
    8.35    in final_thy end;