switched merge_alists'' to AList.merge'' whenever appropriate
authorhaftmann
Mon Oct 23 16:49:21 2006 +0200 (2006-10-23)
changeset 21098d0d8a48ae4e6
parent 21097 5a59f8ff96cc
child 21099 6a0cdb6f72d3
switched merge_alists'' to AList.merge'' whenever appropriate
src/HOL/Tools/recdef_package.ML
src/HOL/Tools/refute.ML
src/Pure/codegen.ML
     1.1 --- a/src/HOL/Tools/recdef_package.ML	Mon Oct 23 11:18:50 2006 +0200
     1.2 +++ b/src/HOL/Tools/recdef_package.ML	Mon Oct 23 16:49:21 2006 +0200
     1.3 @@ -54,7 +54,7 @@
     1.4  
     1.5  fun pretty_hints ({simps, congs, wfs}: hints) =
     1.6   [Pretty.big_list "recdef simp hints:" (map Display.pretty_thm simps),
     1.7 -  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map #2 congs)),
     1.8 +  Pretty.big_list "recdef cong hints:" (map Display.pretty_thm (map snd congs)),
     1.9    Pretty.big_list "recdef wf hints:" (map Display.pretty_thm wfs)];
    1.10  
    1.11  
    1.12 @@ -71,14 +71,20 @@
    1.13  in
    1.14  
    1.15  fun add_cong raw_thm congs =
    1.16 -  let val (c, thm) = prep_cong raw_thm
    1.17 -  in overwrite_warn (congs, (c, thm)) ("Overwriting recdef congruence rule for " ^ quote c) end;
    1.18 +  let
    1.19 +    val (c, thm) = prep_cong raw_thm;
    1.20 +    val _ = if AList.defined (op =) congs c
    1.21 +      then warning ("Overwriting recdef congruence rule for " ^ quote c)
    1.22 +      else ();
    1.23 +  in AList.update (op =) (c, thm) congs end;
    1.24  
    1.25  fun del_cong raw_thm congs =
    1.26    let
    1.27      val (c, thm) = prep_cong raw_thm;
    1.28 -    val (del, rest) = List.partition (Library.equal c o fst) congs;
    1.29 -  in if null del then (warning ("No recdef congruence rule for " ^ quote c); congs) else rest end;
    1.30 +    val _ = if AList.defined (op =) congs c
    1.31 +      then ()
    1.32 +      else warning ("No recdef congruence rule for " ^ quote c);
    1.33 +  in AList.delete (op =) c congs end;
    1.34  
    1.35  end;
    1.36  
    1.37 @@ -103,7 +109,7 @@
    1.38      (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
    1.39        (Symtab.merge (K true) (tab1, tab2),
    1.40          mk_hints (Drule.merge_rules (simps1, simps2),
    1.41 -          Library.merge_alists congs1 congs2,
    1.42 +          AList.merge (op =) eq_thm (congs1, congs2),
    1.43            Drule.merge_rules (wfs1, wfs2)));
    1.44  
    1.45    fun print thy (tab, hints) =
    1.46 @@ -194,13 +200,13 @@
    1.47      val {simps, congs, wfs} = get_local_hints ctxt;
    1.48      val cs = local_claset_of ctxt;
    1.49      val ss = local_simpset_of ctxt addsimps simps;
    1.50 -  in (cs, ss, map #2 congs, wfs) end;
    1.51 +  in (cs, ss, rev (map snd congs), wfs) end;
    1.52  
    1.53  fun prepare_hints_i thy () =
    1.54    let
    1.55      val ctxt0 = ProofContext.init thy;
    1.56      val {simps, congs, wfs} = get_global_hints thy;
    1.57 -  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, map #2 congs, wfs) end;
    1.58 +  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
    1.59  
    1.60  
    1.61  
    1.62 @@ -226,7 +232,7 @@
    1.63      val (thy, {rules = rules_idx, induct, tcs}) =
    1.64          tfl_fn not_permissive thy cs (ss delcongs [imp_cong])
    1.65                 congs wfs name R eqs;
    1.66 -    val rules = map (map #1) (Library.partition_eq (Library.eq_snd (op =)) rules_idx);
    1.67 +    val rules = (map o map) fst (partition_eq (eq_snd (op = : int * int -> bool)) rules_idx);
    1.68      val simp_att = if null tcs then [Simplifier.simp_add, RecfunCodegen.add NONE] else [];
    1.69  
    1.70      val ((simps' :: rules', [induct']), thy) =
     2.1 --- a/src/HOL/Tools/refute.ML	Mon Oct 23 11:18:50 2006 +0200
     2.2 +++ b/src/HOL/Tools/refute.ML	Mon Oct 23 16:49:21 2006 +0200
     2.3 @@ -187,8 +187,8 @@
     2.4  		fun merge _
     2.5  			({interpreters = in1, printers = pr1, parameters = pa1},
     2.6  			 {interpreters = in2, printers = pr2, parameters = pa2}) =
     2.7 -			{interpreters = rev (merge_alists (rev in1) (rev in2)),
     2.8 -			 printers = rev (merge_alists (rev pr1) (rev pr2)),
     2.9 +			{interpreters = AList.merge (op =) (K true) (in1, in2),
    2.10 +			 printers = AList.merge (op =) (K true) (pr1, pr2),
    2.11  			 parameters = Symtab.merge (op=) (pa1, pa2)};
    2.12  		fun print sg {interpreters, printers, parameters} =
    2.13  			Pretty.writeln (Pretty.chunks
     3.1 --- a/src/Pure/codegen.ML	Mon Oct 23 11:18:50 2006 +0200
     3.2 +++ b/src/Pure/codegen.ML	Mon Oct 23 16:49:21 2006 +0200
     3.3 @@ -229,9 +229,9 @@
     3.4        preprocs = preprocs2, modules = modules2, test_params = test_params2}) =
     3.5      {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
     3.6       tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
     3.7 -     consts = merge_alists consts1 consts2,
     3.8 -     types = merge_alists types1 types2,
     3.9 -     attrs = merge_alists attrs1 attrs2,
    3.10 +     consts = AList.merge (op =) (K true) (consts1, consts2),
    3.11 +     types = AList.merge (op =) (K true) (types1, types2),
    3.12 +     attrs = AList.merge (op =) (K true) (attrs1, attrs2),
    3.13       preprocs = AList.merge (op =) (K true) (preprocs1, preprocs2),
    3.14       modules = Symtab.merge (K true) (modules1, modules2),
    3.15       test_params = merge_test_params test_params1 test_params2};
    3.16 @@ -418,7 +418,7 @@
    3.17      | _ => error ("Not a type constructor: " ^ s)
    3.18    end) (thy, xs);
    3.19  
    3.20 -fun get_assoc_type thy s = AList.lookup (op =) ((#types o CodegenData.get) thy) s;
    3.21 +fun get_assoc_type thy = AList.lookup (op =) ((#types o CodegenData.get) thy);
    3.22  
    3.23  
    3.24  (**** make valid ML identifiers ****)