adapted Item_Net;
authorwenzelm
Sun Nov 01 20:59:34 2009 +0100 (2009-11-01)
changeset 33373674df68d4df0
parent 33372 f380fbd6e329
child 33374 8099185908a4
adapted Item_Net;
tuned;
src/HOL/Tools/Function/function_common.ML
src/Pure/Isar/calculation.ML
src/Pure/consts.ML
src/Pure/more_thm.ML
src/Tools/induct.ML
     1.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Nov 01 20:55:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Nov 01 20:59:34 2009 +0100
     1.3 @@ -92,9 +92,7 @@
     1.4  structure FunctionData = GenericDataFun
     1.5  (
     1.6    type T = (term * function_context_data) Item_Net.T;
     1.7 -  val empty = Item_Net.init
     1.8 -    (op aconv o pairself fst : (term * function_context_data) * (term * function_context_data) -> bool)
     1.9 -    fst;
    1.10 +  val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
    1.11    val copy = I;
    1.12    val extend = I;
    1.13    fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
    1.14 @@ -138,7 +136,7 @@
    1.15  val all_function_data = Item_Net.content o get_function
    1.16  
    1.17  fun add_function_data (data as FunctionCtxData {fs, termination, ...}) =
    1.18 -    FunctionData.map (fold (fn f => Item_Net.insert (f, data)) fs)
    1.19 +    FunctionData.map (fold (fn f => Item_Net.update (f, data)) fs)
    1.20      #> store_termination_rule termination
    1.21  
    1.22  
     2.1 --- a/src/Pure/Isar/calculation.ML	Sun Nov 01 20:55:39 2009 +0100
     2.2 +++ b/src/Pure/Isar/calculation.ML	Sun Nov 01 20:59:34 2009 +0100
     2.3 @@ -66,8 +66,8 @@
     2.4  
     2.5  (* add/del rules *)
     2.6  
     2.7 -val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.insert);
     2.8 -val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.delete);
     2.9 +val trans_add = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.update);
    2.10 +val trans_del = Thm.declaration_attribute (CalculationData.map o apfst o apfst o Item_Net.remove);
    2.11  
    2.12  val sym_add =
    2.13    Thm.declaration_attribute (CalculationData.map o apfst o apsnd o Thm.add_thm)
    2.14 @@ -131,7 +131,8 @@
    2.15      fun combine ths =
    2.16        (case opt_rules of SOME rules => rules
    2.17        | NONE =>
    2.18 -          (case ths of [] => Item_Net.content (#1 (get_rules state))
    2.19 +          (case ths of
    2.20 +            [] => Item_Net.content (#1 (get_rules state))
    2.21            | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
    2.22        |> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
    2.23        |> Seq.filter (not o projection ths);
     3.1 --- a/src/Pure/consts.ML	Sun Nov 01 20:55:39 2009 +0100
     3.2 +++ b/src/Pure/consts.ML	Sun Nov 01 20:59:34 2009 +0100
     3.3 @@ -71,10 +71,10 @@
     3.4  (* reverted abbrevs *)
     3.5  
     3.6  val empty_abbrevs =
     3.7 -  Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') #1;
     3.8 +  Item_Net.init (fn ((t, u), (t', u')) => t aconv t' andalso u aconv u') (single o #1);
     3.9  
    3.10 -fun insert_abbrevs mode abbrs =
    3.11 -  Symtab.map_default (mode, empty_abbrevs) (Item_Net.insert abbrs);
    3.12 +fun update_abbrevs mode abbrs =
    3.13 +  Symtab.map_default (mode, empty_abbrevs) (Item_Net.update abbrs);
    3.14  
    3.15  fun retrieve_abbrevs (Consts {rev_abbrevs, ...}) modes =
    3.16    let val nets = map_filter (Symtab.lookup rev_abbrevs) modes
    3.17 @@ -290,7 +290,7 @@
    3.18          val (_, decls') = decls
    3.19            |> Name_Space.define true naming (b, (decl, SOME abbr));
    3.20          val rev_abbrevs' = rev_abbrevs
    3.21 -          |> insert_abbrevs mode (rev_abbrev lhs rhs);
    3.22 +          |> update_abbrevs mode (rev_abbrev lhs rhs);
    3.23        in (decls', constraints, rev_abbrevs') end)
    3.24      |> pair (lhs, rhs)
    3.25    end;
    3.26 @@ -299,7 +299,7 @@
    3.27    let
    3.28      val (T, rhs) = the_abbreviation consts c;
    3.29      val rev_abbrevs' = rev_abbrevs
    3.30 -      |> insert_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
    3.31 +      |> update_abbrevs mode (rev_abbrev (Const (c, T)) rhs);
    3.32    in (decls, constraints, rev_abbrevs') end);
    3.33  
    3.34  end;
     4.1 --- a/src/Pure/more_thm.ML	Sun Nov 01 20:55:39 2009 +0100
     4.2 +++ b/src/Pure/more_thm.ML	Sun Nov 01 20:59:34 2009 +0100
     4.3 @@ -246,8 +246,8 @@
     4.4  val del_thm = remove eq_thm_prop;
     4.5  val merge_thms = merge eq_thm_prop;
     4.6  
     4.7 -val intro_rules = Item_Net.init eq_thm_prop Thm.concl_of;
     4.8 -val elim_rules = Item_Net.init eq_thm_prop Thm.major_prem_of;
     4.9 +val intro_rules = Item_Net.init eq_thm_prop (single o Thm.concl_of);
    4.10 +val elim_rules = Item_Net.init eq_thm_prop (single o Thm.major_prem_of);
    4.11  
    4.12  
    4.13  
     5.1 --- a/src/Tools/induct.ML	Sun Nov 01 20:55:39 2009 +0100
     5.2 +++ b/src/Tools/induct.ML	Sun Nov 01 20:59:34 2009 +0100
     5.3 @@ -113,9 +113,10 @@
     5.4  
     5.5  type rules = (string * thm) Item_Net.T;
     5.6  
     5.7 -val init_rules =
     5.8 -  Item_Net.init (fn ((s1: string, th1), (s2, th2)) => s1 = s2 andalso
     5.9 -    Thm.eq_thm_prop (th1, th2));
    5.10 +fun init_rules index : rules =
    5.11 +  Item_Net.init
    5.12 +    (fn ((s1, th1), (s2, th2)) => s1 = s2 andalso Thm.eq_thm_prop (th1, th2))
    5.13 +    (single o index);
    5.14  
    5.15  fun filter_rules (rs: rules) th =
    5.16    filter (fn (_, th') => Thm.eq_thm_prop (th, th')) (Item_Net.content rs);
    5.17 @@ -203,18 +204,18 @@
    5.18    let val (x, thm) = g arg in (InductData.map (f (name, thm)) x, thm) end;
    5.19  
    5.20  fun del_att which = Thm.declaration_attribute (fn th => InductData.map (which (pairself (fn rs =>
    5.21 -  fold Item_Net.delete (filter_rules rs th) rs))));
    5.22 +  fold Item_Net.remove (filter_rules rs th) rs))));
    5.23  
    5.24  fun map1 f (x, y, z) = (f x, y, z);
    5.25  fun map2 f (x, y, z) = (x, f y, z);
    5.26  fun map3 f (x, y, z) = (x, y, f z);
    5.27  
    5.28 -fun add_casesT rule x = map1 (apfst (Item_Net.insert rule)) x;
    5.29 -fun add_casesP rule x = map1 (apsnd (Item_Net.insert rule)) x;
    5.30 -fun add_inductT rule x = map2 (apfst (Item_Net.insert rule)) x;
    5.31 -fun add_inductP rule x = map2 (apsnd (Item_Net.insert rule)) x;
    5.32 -fun add_coinductT rule x = map3 (apfst (Item_Net.insert rule)) x;
    5.33 -fun add_coinductP rule x = map3 (apsnd (Item_Net.insert rule)) x;
    5.34 +fun add_casesT rule x = map1 (apfst (Item_Net.update rule)) x;
    5.35 +fun add_casesP rule x = map1 (apsnd (Item_Net.update rule)) x;
    5.36 +fun add_inductT rule x = map2 (apfst (Item_Net.update rule)) x;
    5.37 +fun add_inductP rule x = map2 (apsnd (Item_Net.update rule)) x;
    5.38 +fun add_coinductT rule x = map3 (apfst (Item_Net.update rule)) x;
    5.39 +fun add_coinductP rule x = map3 (apsnd (Item_Net.update rule)) x;
    5.40  
    5.41  val consumes0 = Rule_Cases.consumes_default 0;
    5.42  val consumes1 = Rule_Cases.consumes_default 1;