turned structure NetRules into general Item_Net, which is loaded earlier;
authorwenzelm
Tue Mar 17 14:12:06 2009 +0100 (2009-03-17 ago)
changeset 30559e5987a7ac5df
parent 30558 2ef9892114fd
child 30560 0cc3b7f03ade
turned structure NetRules into general Item_Net, which is loaded earlier;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/net_rules.ML
src/Pure/ROOT.ML
src/Pure/item_net.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Mar 17 14:09:20 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Tue Mar 17 14:12:06 2009 +0100
     1.3 @@ -61,7 +61,7 @@
     1.4    Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML			\
     1.5    Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML		\
     1.6    Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
     1.7 -  Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML	\
     1.8 +  Isar/method.ML Isar/object_logic.ML Isar/obtain.ML			\
     1.9    Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML		\
    1.10    Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML		\
    1.11    Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    1.12 @@ -89,12 +89,12 @@
    1.13    Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML	\
    1.14    conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    1.15    defs.ML display.ML drule.ML envir.ML facts.ML goal.ML			\
    1.16 -  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML	\
    1.17 -  morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML	\
    1.18 -  primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML	\
    1.19 -  sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML	\
    1.20 -  term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML		\
    1.21 -  type_infer.ML unify.ML variable.ML
    1.22 +  interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML	\
    1.23 +  more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML	\
    1.24 +  pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML	\
    1.25 +  search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML		\
    1.26 +  tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML		\
    1.27 +  type.ML type_infer.ML unify.ML variable.ML
    1.28  	@./mk
    1.29  
    1.30  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Tue Mar 17 14:09:20 2009 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Tue Mar 17 14:12:06 2009 +0100
     2.3 @@ -44,7 +44,6 @@
     2.4  use "proof.ML";
     2.5  use "../ML/ml_thms.ML";
     2.6  use "element.ML";
     2.7 -use "net_rules.ML";
     2.8  
     2.9  (*derived theory and proof elements*)
    2.10  use "calculation.ML";
    2.11 @@ -89,5 +88,3 @@
    2.12  use "../Thy/thm_deps.ML";
    2.13  use "isar_cmd.ML";
    2.14  use "isar_syn.ML";
    2.15 -
    2.16 -
     3.1 --- a/src/Pure/Isar/net_rules.ML	Tue Mar 17 14:09:20 2009 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,69 +0,0 @@
     3.4 -(*  Title:      Pure/Isar/net_rules.ML
     3.5 -    Author:     Markus Wenzel, TU Muenchen
     3.6 -
     3.7 -Efficient storage of rules: preserves order, prefers later entries.
     3.8 -*)
     3.9 -
    3.10 -signature NET_RULES =
    3.11 -sig
    3.12 -  type 'a T
    3.13 -  val rules: 'a T -> 'a list
    3.14 -  val retrieve: 'a T -> term -> 'a list
    3.15 -  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    3.16 -  val merge: 'a T * 'a T -> 'a T
    3.17 -  val delete: 'a -> 'a T -> 'a T
    3.18 -  val insert: 'a -> 'a T -> 'a T
    3.19 -  val intro: thm T
    3.20 -  val elim: thm T
    3.21 -end;
    3.22 -
    3.23 -structure NetRules: NET_RULES =
    3.24 -struct
    3.25 -
    3.26 -(* datatype rules *)
    3.27 -
    3.28 -datatype 'a T =
    3.29 -  Rules of {
    3.30 -    eq: 'a * 'a -> bool,
    3.31 -    index: 'a -> term,
    3.32 -    rules: 'a list,
    3.33 -    next: int,
    3.34 -    net: (int * 'a) Net.net};
    3.35 -
    3.36 -fun mk_rules eq index rules next net =
    3.37 -  Rules {eq = eq, index = index, rules = rules, next = next, net = net};
    3.38 -
    3.39 -fun rules (Rules {rules = rs, ...}) = rs;
    3.40 -
    3.41 -fun retrieve (Rules {rules, net, ...}) tm =
    3.42 -  Tactic.untaglist 
    3.43 -     ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm)));
    3.44 -
    3.45 -
    3.46 -(* build rules *)
    3.47 -
    3.48 -fun init eq index = mk_rules eq index [] ~1 Net.empty;
    3.49 -
    3.50 -fun add rule (Rules {eq, index, rules, next, net}) =
    3.51 -  mk_rules eq index (rule :: rules) (next - 1)
    3.52 -    (Net.insert_term (K false) (index rule, (next, rule)) net);
    3.53 -
    3.54 -fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) =
    3.55 -  let val rules = Library.merge eq (rules1, rules2)
    3.56 -  in fold_rev add rules (init eq index) end;
    3.57 -
    3.58 -fun delete rule (rs as Rules {eq, index, rules, next, net}) =
    3.59 -  if not (member eq rules rule) then rs
    3.60 -  else mk_rules eq index (remove eq rule rules) next
    3.61 -    (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net);
    3.62 -
    3.63 -fun insert rule rs = add rule (delete rule rs);    (*ensure that new rule gets precedence*)
    3.64 -
    3.65 -
    3.66 -(* intro/elim rules *)
    3.67 -
    3.68 -val intro = init Thm.eq_thm_prop Thm.concl_of;
    3.69 -val elim = init Thm.eq_thm_prop Thm.major_prem_of;
    3.70 -
    3.71 -
    3.72 -end;
     4.1 --- a/src/Pure/ROOT.ML	Tue Mar 17 14:09:20 2009 +0100
     4.2 +++ b/src/Pure/ROOT.ML	Tue Mar 17 14:12:06 2009 +0100
     4.3 @@ -52,11 +52,12 @@
     4.4  use "ML/ml_syntax.ML";
     4.5  
     4.6  (*core of tactical proof system*)
     4.7 +use "net.ML";
     4.8 +use "item_net.ML";
     4.9  use "envir.ML";
    4.10  use "consts.ML";
    4.11  use "primitive_defs.ML";
    4.12  use "defs.ML";
    4.13 -use "net.ML";
    4.14  use "sign.ML";
    4.15  use "pattern.ML";
    4.16  use "unify.ML";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/item_net.ML	Tue Mar 17 14:12:06 2009 +0100
     5.3 @@ -0,0 +1,58 @@
     5.4 +(*  Title:      Pure/item_net.ML
     5.5 +    Author:     Markus Wenzel, TU Muenchen
     5.6 +
     5.7 +Efficient storage of items indexed by terms; preserves order and
     5.8 +prefers later entries.
     5.9 +*)
    5.10 +
    5.11 +signature ITEM_NET =
    5.12 +sig
    5.13 +  type 'a T
    5.14 +  val content: 'a T -> 'a list
    5.15 +  val retrieve: 'a T -> term -> 'a list
    5.16 +  val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T
    5.17 +  val merge: 'a T * 'a T -> 'a T
    5.18 +  val delete: 'a -> 'a T -> 'a T
    5.19 +  val insert: 'a -> 'a T -> 'a T
    5.20 +end;
    5.21 +
    5.22 +structure Item_Net: ITEM_NET =
    5.23 +struct
    5.24 +
    5.25 +(* datatype *)
    5.26 +
    5.27 +datatype 'a T =
    5.28 +  Items of {
    5.29 +    eq: 'a * 'a -> bool,
    5.30 +    index: 'a -> term,
    5.31 +    content: 'a list,
    5.32 +    next: int,
    5.33 +    net: (int * 'a) Net.net};
    5.34 +
    5.35 +fun mk_items eq index content next net =
    5.36 +  Items {eq = eq, index = index, content = content, next = next, net = net};
    5.37 +
    5.38 +fun content (Items {content, ...}) = content;
    5.39 +fun retrieve (Items {net, ...}) = order_list o Net.unify_term net;
    5.40 +
    5.41 +
    5.42 +(* build net *)
    5.43 +
    5.44 +fun init eq index = mk_items eq index [] ~1 Net.empty;
    5.45 +
    5.46 +fun add x (Items {eq, index, content, next, net}) =
    5.47 +  mk_items eq index (x :: content) (next - 1)
    5.48 +    (Net.insert_term (K false) (index x, (next, x)) net);
    5.49 +
    5.50 +fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) =
    5.51 +  let val content = Library.merge eq (content1, content2)
    5.52 +  in fold_rev add content (init eq index) end;
    5.53 +
    5.54 +fun delete x (items as Items {eq, index, content, next, net}) =
    5.55 +  if not (member eq content x) then items
    5.56 +  else mk_items eq index (remove eq x content) next
    5.57 +    (Net.delete_term (eq o pairself #2) (index x, (0, x)) net);
    5.58 +
    5.59 +fun insert x items = add x (delete x items);   (*ensure that added entry gets precedence*)
    5.60 +
    5.61 +end;