more liberal merging of BNFs and constructor sugar
authorblanchet
Wed Feb 12 08:35:56 2014 +0100 (2014-02-12)
changeset 55394d5ebe055b599
parent 55393 ce5cebfaedda
child 55395 4e79187f847e
more liberal merging of BNFs and constructor sugar
* * *
make sure that the cache doesn't produce 'DUP's
src/HOL/Tools/BNF/bnf_def.ML
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/BNF/bnf_fp_n2m.ML
src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
src/HOL/Tools/BNF/bnf_fp_util.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 08:35:56 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_def.ML	Wed Feb 12 08:35:56 2014 +0100
     1.3 @@ -12,7 +12,6 @@
     1.4    type nonemptiness_witness = {I: int list, wit: term, prop: thm list}
     1.5  
     1.6    val morph_bnf: morphism -> bnf -> bnf
     1.7 -  val eq_bnf: bnf * bnf -> bool
     1.8    val bnf_of: Proof.context -> string -> bnf option
     1.9    val register_bnf: string -> (bnf * local_theory) -> (bnf * local_theory)
    1.10  
    1.11 @@ -452,16 +451,12 @@
    1.12      wits = List.map (morph_witness phi) wits,
    1.13      rel = Morphism.term phi rel};
    1.14  
    1.15 -fun eq_bnf (BNF {T = T1, live = live1, dead = dead1, ...},
    1.16 -  BNF {T = T2, live = live2, dead = dead2, ...}) =
    1.17 -  Type.could_unify (T1, T2) andalso live1 = live2 andalso dead1 = dead2;
    1.18 -
    1.19  structure Data = Generic_Data
    1.20  (
    1.21    type T = bnf Symtab.table;
    1.22    val empty = Symtab.empty;
    1.23    val extend = I;
    1.24 -  val merge = Symtab.merge eq_bnf;
    1.25 +  fun merge data : T = Symtab.merge (K true) data;
    1.26  );
    1.27  
    1.28  fun bnf_of ctxt =
     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     2.3 @@ -25,7 +25,6 @@
     2.4       sel_co_iterssss: thm list list list list};
     2.5  
     2.6    val of_fp_sugar: (fp_sugar -> 'a list) -> fp_sugar -> 'a
     2.7 -  val eq_fp_sugar: fp_sugar * fp_sugar -> bool
     2.8    val morph_fp_sugar: morphism -> fp_sugar -> fp_sugar
     2.9    val transfer_fp_sugar: Proof.context -> fp_sugar -> fp_sugar
    2.10    val fp_sugar_of: Proof.context -> string -> fp_sugar option
    2.11 @@ -136,10 +135,6 @@
    2.12  
    2.13  fun of_fp_sugar f (fp_sugar as ({index, ...}: fp_sugar)) = nth (f fp_sugar) index;
    2.14  
    2.15 -fun eq_fp_sugar ({T = T1, fp = fp1, index = index1, fp_res = fp_res1, ...} : fp_sugar,
    2.16 -    {T = T2, fp = fp2, index = index2, fp_res = fp_res2, ...} : fp_sugar) =
    2.17 -  T1 = T2 andalso fp1 = fp2 andalso index1 = index2 andalso eq_fp_result (fp_res1, fp_res2);
    2.18 -
    2.19  fun morph_fp_sugar phi ({T, fp, index, pre_bnfs, nested_bnfs, nesting_bnfs, fp_res, ctr_defss,
    2.20      ctr_sugars, co_iterss, mapss, co_inducts, co_iter_thmsss, disc_co_itersss, sel_co_iterssss}
    2.21      : fp_sugar) =
    2.22 @@ -163,7 +158,7 @@
    2.23    type T = fp_sugar Symtab.table;
    2.24    val empty = Symtab.empty;
    2.25    val extend = I;
    2.26 -  val merge = Symtab.merge eq_fp_sugar;
    2.27 +  fun merge data : T = Symtab.merge (K true) data;
    2.28  );
    2.29  
    2.30  fun fp_sugar_of ctxt =
     3.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
     3.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML	Wed Feb 12 08:35:56 2014 +0100
     3.3 @@ -97,12 +97,12 @@
     3.4      val pre_bnfss = map #pre_bnfs fp_sugars;
     3.5      val nesty_bnfss = map (fn sugar => #nested_bnfs sugar @ #nesting_bnfs sugar) fp_sugars;
     3.6      val fp_nesty_bnfss = fp_bnfs :: nesty_bnfss;
     3.7 -    val fp_nesty_bnfs = distinct eq_bnf (flat fp_nesty_bnfss);
     3.8 +    val fp_nesty_bnfs = distinct (op = o pairself T_of_bnf) (flat fp_nesty_bnfss);
     3.9  
    3.10      val rels =
    3.11        let
    3.12          fun find_rel T As Bs = fp_nesty_bnfss
    3.13 -          |> map (filter_out (curry eq_bnf BNF_Comp.DEADID_bnf))
    3.14 +          |> map (filter_out (curry (op = o pairself name_of_bnf) BNF_Comp.DEADID_bnf))
    3.15            |> get_first (find_first (fn bnf => Type.could_unify (T_of_bnf bnf, T)))
    3.16            |> Option.map (fn bnf =>
    3.17              let val live = live_of_bnf bnf;
     4.1 --- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     4.2 +++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     4.3 @@ -43,7 +43,7 @@
     4.4    type T = n2m_sugar Typtab.table;
     4.5    val empty = Typtab.empty;
     4.6    val extend = I;
     4.7 -  fun merge data : T = Typtab.merge (eq_fst (eq_list eq_fp_sugar)) data;
     4.8 +  fun merge data : T = Typtab.merge (K true) data;
     4.9  );
    4.10  
    4.11  fun morph_n2m_sugar phi (fp_sugars, (lfp_sugar_thms_opt, gfp_sugar_thms_opt)) =
     5.1 --- a/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:56 2014 +0100
     5.2 +++ b/src/HOL/Tools/BNF/bnf_fp_util.ML	Wed Feb 12 08:35:56 2014 +0100
     5.3 @@ -30,7 +30,6 @@
     5.4       rel_xtor_co_induct_thm: thm}
     5.5  
     5.6    val morph_fp_result: morphism -> fp_result -> fp_result
     5.7 -  val eq_fp_result: fp_result * fp_result -> bool
     5.8    val un_fold_of: 'a list -> 'a
     5.9    val co_rec_of: 'a list -> 'a
    5.10  
    5.11 @@ -239,9 +238,6 @@
    5.12     xtor_co_iter_o_map_thmss = map (map (Morphism.thm phi)) xtor_co_iter_o_map_thmss,
    5.13     rel_xtor_co_induct_thm = Morphism.thm phi rel_xtor_co_induct_thm};
    5.14  
    5.15 -fun eq_fp_result ({bnfs = bnfs1, ...} : fp_result, {bnfs = bnfs2, ...} : fp_result) =
    5.16 -  eq_list eq_bnf (bnfs1, bnfs2);
    5.17 -
    5.18  fun un_fold_of [f, _] = f;
    5.19  fun co_rec_of [_, r] = r;
    5.20  
     6.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     6.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Wed Feb 12 08:35:56 2014 +0100
     6.3 @@ -96,10 +96,6 @@
     6.4     sel_split_asms: thm list,
     6.5     case_eq_ifs: thm list};
     6.6  
     6.7 -fun eq_ctr_sugar ({ctrs = ctrs1, casex = case1, discs = discs1, selss = selss1, ...} : ctr_sugar,
     6.8 -    {ctrs = ctrs2, casex = case2, discs = discs2, selss = selss2, ...} : ctr_sugar) =
     6.9 -  ctrs1 = ctrs2 andalso case1 = case2 andalso discs1 = discs2 andalso selss1 = selss2;
    6.10 -
    6.11  fun morph_ctr_sugar phi {ctrs, casex, discs, selss, exhaust, nchotomy, injects, distincts,
    6.12      case_thms, case_cong, weak_case_cong, split, split_asm, disc_thmss, discIs, sel_thmss,
    6.13      disc_excludesss, disc_exhausts, sel_exhausts, collapses, expands, sel_splits, sel_split_asms,
    6.14 @@ -137,7 +133,7 @@
    6.15    type T = ctr_sugar Symtab.table;
    6.16    val empty = Symtab.empty;
    6.17    val extend = I;
    6.18 -  val merge = Symtab.merge eq_ctr_sugar;
    6.19 +  fun merge data : T = Symtab.merge (K true) data;
    6.20  );
    6.21  
    6.22  fun ctr_sugar_of ctxt =