# HG changeset patch # User wenzelm # Date 1237295526 -3600 # Node ID e5987a7ac5dfa5219b0f2578a3184f0a5d3e6460 # Parent 2ef9892114fd43c7cd7447d0ce436f0c7ff26088 turned structure NetRules into general Item_Net, which is loaded earlier; diff -r 2ef9892114fd -r e5987a7ac5df src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Mar 17 14:09:20 2009 +0100 +++ b/src/Pure/IsaMakefile Tue Mar 17 14:12:06 2009 +0100 @@ -61,7 +61,7 @@ Isar/element.ML Isar/expression.ML Isar/isar_cmd.ML \ Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \ Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \ - Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ + Isar/method.ML Isar/object_logic.ML Isar/obtain.ML \ Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \ Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \ Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \ @@ -89,12 +89,12 @@ Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \ conjunction.ML consts.ML context.ML context_position.ML conv.ML \ defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \ - interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML \ - morphism.ML name.ML net.ML old_goals.ML old_term.ML pattern.ML \ - primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML search.ML \ - sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML \ - term.ML term_ord.ML term_subst.ML theory.ML thm.ML type.ML \ - type_infer.ML unify.ML variable.ML + interpretation.ML item_net.ML library.ML logic.ML meta_simplifier.ML \ + more_thm.ML morphism.ML name.ML net.ML old_goals.ML old_term.ML \ + pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML pure_thy.ML \ + search.ML sign.ML simplifier.ML sorts.ML subgoal.ML tactic.ML \ + tctical.ML term.ML term_ord.ML term_subst.ML theory.ML thm.ML \ + type.ML type_infer.ML unify.ML variable.ML @./mk diff -r 2ef9892114fd -r e5987a7ac5df src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Tue Mar 17 14:09:20 2009 +0100 +++ b/src/Pure/Isar/ROOT.ML Tue Mar 17 14:12:06 2009 +0100 @@ -44,7 +44,6 @@ use "proof.ML"; use "../ML/ml_thms.ML"; use "element.ML"; -use "net_rules.ML"; (*derived theory and proof elements*) use "calculation.ML"; @@ -89,5 +88,3 @@ use "../Thy/thm_deps.ML"; use "isar_cmd.ML"; use "isar_syn.ML"; - - diff -r 2ef9892114fd -r e5987a7ac5df src/Pure/Isar/net_rules.ML --- a/src/Pure/Isar/net_rules.ML Tue Mar 17 14:09:20 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,69 +0,0 @@ -(* Title: Pure/Isar/net_rules.ML - Author: Markus Wenzel, TU Muenchen - -Efficient storage of rules: preserves order, prefers later entries. -*) - -signature NET_RULES = -sig - type 'a T - val rules: 'a T -> 'a list - val retrieve: 'a T -> term -> 'a list - val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T - val merge: 'a T * 'a T -> 'a T - val delete: 'a -> 'a T -> 'a T - val insert: 'a -> 'a T -> 'a T - val intro: thm T - val elim: thm T -end; - -structure NetRules: NET_RULES = -struct - -(* datatype rules *) - -datatype 'a T = - Rules of { - eq: 'a * 'a -> bool, - index: 'a -> term, - rules: 'a list, - next: int, - net: (int * 'a) Net.net}; - -fun mk_rules eq index rules next net = - Rules {eq = eq, index = index, rules = rules, next = next, net = net}; - -fun rules (Rules {rules = rs, ...}) = rs; - -fun retrieve (Rules {rules, net, ...}) tm = - Tactic.untaglist - ((Library.sort (int_ord o pairself #1) (Net.unify_term net tm))); - - -(* build rules *) - -fun init eq index = mk_rules eq index [] ~1 Net.empty; - -fun add rule (Rules {eq, index, rules, next, net}) = - mk_rules eq index (rule :: rules) (next - 1) - (Net.insert_term (K false) (index rule, (next, rule)) net); - -fun merge (Rules {eq, index, rules = rules1, ...}, Rules {rules = rules2, ...}) = - let val rules = Library.merge eq (rules1, rules2) - in fold_rev add rules (init eq index) end; - -fun delete rule (rs as Rules {eq, index, rules, next, net}) = - if not (member eq rules rule) then rs - else mk_rules eq index (remove eq rule rules) next - (Net.delete_term (eq o pairself #2) (index rule, (0, rule)) net); - -fun insert rule rs = add rule (delete rule rs); (*ensure that new rule gets precedence*) - - -(* intro/elim rules *) - -val intro = init Thm.eq_thm_prop Thm.concl_of; -val elim = init Thm.eq_thm_prop Thm.major_prem_of; - - -end; diff -r 2ef9892114fd -r e5987a7ac5df src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Tue Mar 17 14:09:20 2009 +0100 +++ b/src/Pure/ROOT.ML Tue Mar 17 14:12:06 2009 +0100 @@ -52,11 +52,12 @@ use "ML/ml_syntax.ML"; (*core of tactical proof system*) +use "net.ML"; +use "item_net.ML"; use "envir.ML"; use "consts.ML"; use "primitive_defs.ML"; use "defs.ML"; -use "net.ML"; use "sign.ML"; use "pattern.ML"; use "unify.ML"; diff -r 2ef9892114fd -r e5987a7ac5df src/Pure/item_net.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/item_net.ML Tue Mar 17 14:12:06 2009 +0100 @@ -0,0 +1,58 @@ +(* Title: Pure/item_net.ML + Author: Markus Wenzel, TU Muenchen + +Efficient storage of items indexed by terms; preserves order and +prefers later entries. +*) + +signature ITEM_NET = +sig + type 'a T + val content: 'a T -> 'a list + val retrieve: 'a T -> term -> 'a list + val init: ('a * 'a -> bool) -> ('a -> term) -> 'a T + val merge: 'a T * 'a T -> 'a T + val delete: 'a -> 'a T -> 'a T + val insert: 'a -> 'a T -> 'a T +end; + +structure Item_Net: ITEM_NET = +struct + +(* datatype *) + +datatype 'a T = + Items of { + eq: 'a * 'a -> bool, + index: 'a -> term, + content: 'a list, + next: int, + net: (int * 'a) Net.net}; + +fun mk_items eq index content next net = + Items {eq = eq, index = index, content = content, next = next, net = net}; + +fun content (Items {content, ...}) = content; +fun retrieve (Items {net, ...}) = order_list o Net.unify_term net; + + +(* build net *) + +fun init eq index = mk_items eq index [] ~1 Net.empty; + +fun add x (Items {eq, index, content, next, net}) = + mk_items eq index (x :: content) (next - 1) + (Net.insert_term (K false) (index x, (next, x)) net); + +fun merge (Items {eq, index, content = content1, ...}, Items {content = content2, ...}) = + let val content = Library.merge eq (content1, content2) + in fold_rev add content (init eq index) end; + +fun delete x (items as Items {eq, index, content, next, net}) = + if not (member eq content x) then items + else mk_items eq index (remove eq x content) next + (Net.delete_term (eq o pairself #2) (index x, (0, x)) net); + +fun insert x items = add x (delete x items); (*ensure that added entry gets precedence*) + +end;