tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
authorwenzelm
Tue Apr 27 15:23:05 2010 +0200 (2010-04-27 ago)
changeset 3642066fd989c8e15
parent 36419 7aea10d10113
child 36421 066e35d1c0d7
tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
src/Pure/axclass.ML
     1.1 --- a/src/Pure/axclass.ML	Tue Apr 27 15:03:19 2010 +0200
     1.2 +++ b/src/Pure/axclass.ML	Tue Apr 27 15:23:05 2010 +0200
     1.3 @@ -79,13 +79,16 @@
     1.4      (string * thm) Symtab.table Symtab.table *
     1.5        (*constant name ~> type constructor ~> (constant name, equation)*)
     1.6      (string * string) Symtab.table (*constant name ~> (constant name, type constructor)*),
     1.7 -  diff_merge_classrels: (class * class) list};
     1.8 +  diff_classrels: (class * class) list};
     1.9  
    1.10  fun make_data
    1.11 -    (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =
    1.12 +    (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =
    1.13    Data {axclasses = axclasses, params = params, proven_classrels = proven_classrels,
    1.14      proven_arities = proven_arities, inst_params = inst_params,
    1.15 -    diff_merge_classrels = diff_merge_classrels};
    1.16 +    diff_classrels = diff_classrels};
    1.17 +
    1.18 +fun diff_table tab1 tab2 =
    1.19 +  Symreltab.fold (fn (x, _) => if Symreltab.defined tab2 x then I else cons x) tab1 [];
    1.20  
    1.21  structure Data = Theory_Data_PP
    1.22  (
    1.23 @@ -96,10 +99,10 @@
    1.24    fun merge pp
    1.25        (Data {axclasses = axclasses1, params = params1, proven_classrels = proven_classrels1,
    1.26          proven_arities = proven_arities1, inst_params = inst_params1,
    1.27 -        diff_merge_classrels = diff_merge_classrels1},
    1.28 +        diff_classrels = diff_classrels1},
    1.29         Data {axclasses = axclasses2, params = params2, proven_classrels = proven_classrels2,
    1.30          proven_arities = proven_arities2, inst_params = inst_params2,
    1.31 -        diff_merge_classrels = diff_merge_classrels2}) =
    1.32 +        diff_classrels = diff_classrels2}) =
    1.33      let
    1.34        val axclasses' = Symtab.merge (K true) (axclasses1, axclasses2);
    1.35        val params' =
    1.36 @@ -111,47 +114,45 @@
    1.37        val proven_arities' =
    1.38          Symtab.join (K (Library.merge (eq_fst op =))) (proven_arities1, proven_arities2);
    1.39  
    1.40 -      val classrels1 = Symreltab.keys proven_classrels1;
    1.41 -      val classrels2 = Symreltab.keys proven_classrels2;
    1.42 -      val diff_merge_classrels' =
    1.43 -        subtract (op =) classrels1 classrels2 @
    1.44 -        subtract (op =) classrels2 classrels1 @
    1.45 -        diff_merge_classrels1 @ diff_merge_classrels2;
    1.46 +      val diff_classrels' =
    1.47 +        diff_table proven_classrels1 proven_classrels2 @
    1.48 +        diff_table proven_classrels2 proven_classrels1 @
    1.49 +        diff_classrels1 @ diff_classrels2;
    1.50  
    1.51        val inst_params' =
    1.52          (Symtab.join (K (Symtab.merge (K true))) (#1 inst_params1, #1 inst_params2),
    1.53            Symtab.merge (K true) (#2 inst_params1, #2 inst_params2));
    1.54      in
    1.55 -      make_data (axclasses', params', proven_classrels', proven_arities', inst_params',
    1.56 -        diff_merge_classrels')
    1.57 +      make_data
    1.58 +        (axclasses', params', proven_classrels', proven_arities', inst_params', diff_classrels')
    1.59      end;
    1.60  );
    1.61  
    1.62  fun map_data f =
    1.63 -  Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels} =>
    1.64 -    make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels)));
    1.65 +  Data.map (fn Data {axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels} =>
    1.66 +    make_data (f (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels)));
    1.67  
    1.68  fun map_axclasses f =
    1.69 -  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
    1.70 -    (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
    1.71 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =>
    1.72 +    (f axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels));
    1.73  
    1.74  fun map_params f =
    1.75 -  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
    1.76 -    (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_merge_classrels));
    1.77 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =>
    1.78 +    (axclasses, f params, proven_classrels, proven_arities, inst_params, diff_classrels));
    1.79  
    1.80  fun map_proven_classrels f =
    1.81 -  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
    1.82 -    (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_merge_classrels));
    1.83 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =>
    1.84 +    (axclasses, params, f proven_classrels, proven_arities, inst_params, diff_classrels));
    1.85  
    1.86  fun map_proven_arities f =
    1.87 -  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
    1.88 -    (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_merge_classrels));
    1.89 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =>
    1.90 +    (axclasses, params, proven_classrels, f proven_arities, inst_params, diff_classrels));
    1.91  
    1.92  fun map_inst_params f =
    1.93 -  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_merge_classrels) =>
    1.94 -    (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_merge_classrels));
    1.95 +  map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, diff_classrels) =>
    1.96 +    (axclasses, params, proven_classrels, proven_arities, f inst_params, diff_classrels));
    1.97  
    1.98 -val clear_diff_merge_classrels =
    1.99 +val clear_diff_classrels =
   1.100    map_data (fn (axclasses, params, proven_classrels, proven_arities, inst_params, _) =>
   1.101      (axclasses, params, proven_classrels, proven_arities, inst_params, []));
   1.102  
   1.103 @@ -162,7 +163,7 @@
   1.104  val proven_classrels_of = #proven_classrels o rep_data;
   1.105  val proven_arities_of = #proven_arities o rep_data;
   1.106  val inst_params_of = #inst_params o rep_data;
   1.107 -val diff_merge_classrels_of = #diff_merge_classrels o rep_data;
   1.108 +val diff_classrels_of = #diff_classrels o rep_data;
   1.109  
   1.110  
   1.111  (* axclasses with parameters *)
   1.112 @@ -226,15 +227,15 @@
   1.113  fun complete_classrels thy =
   1.114    let
   1.115      val classrels = proven_classrels_of thy;
   1.116 -    val diff_merge_classrels = diff_merge_classrels_of thy;
   1.117 +    val diff_classrels = diff_classrels_of thy;
   1.118      val (needed, thy') = (false, thy) |>
   1.119        fold (fn rel => fn (needed, thy) =>
   1.120            put_trancl_classrel (rel, Symreltab.lookup classrels rel |> the) thy
   1.121            |>> (fn b => needed orelse b))
   1.122 -        diff_merge_classrels;
   1.123 +        diff_classrels;
   1.124    in
   1.125 -    if null diff_merge_classrels then NONE
   1.126 -    else SOME (clear_diff_merge_classrels thy')
   1.127 +    if null diff_classrels then NONE
   1.128 +    else SOME (clear_diff_classrels thy')
   1.129    end;
   1.130  
   1.131