# HG changeset patch # User wenzelm # Date 1007411515 -3600 # Node ID 5fad0e7129c3d3b2451df9d37551426bbb30ddd0 # Parent 94e812f9683e62679eb193dbcfb79e7e7c6e9447 renamed rule_context.ML to context_rules.ML; diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Mon Dec 03 21:03:06 2001 +0100 +++ b/src/Pure/IsaMakefile Mon Dec 03 21:31:55 2001 +0100 @@ -31,16 +31,17 @@ Interface/ROOT.ML Interface/isamode.ML Interface/proof_general.ML \ Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML \ Isar/auto_bind.ML Isar/calculation.ML Isar/comment.ML \ - Isar/induct_attrib.ML Isar/isar.ML Isar/isar_cmd.ML \ - Isar/isar_output.ML Isar/isar_syn.ML Isar/isar_thy.ML Isar/locale.ML \ - Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \ - Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \ - Isar/proof.ML Isar/proof_context.ML Isar/proof_data.ML \ - Isar/proof_history.ML Isar/rule_cases.ML Isar/rule_context.ML \ - Isar/session.ML Isar/skip_proof.ML Isar/thy_header.ML \ - Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml-3.x.ML \ - ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \ - Proof/ROOT.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ + Isar/context_rules.ML Isar/induct_attrib.ML Isar/isar.ML \ + Isar/isar_cmd.ML Isar/isar_output.ML Isar/isar_syn.ML \ + Isar/isar_thy.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \ + Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML \ + Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \ + Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \ + Isar/rule_cases.ML Isar/session.ML Isar/skip_proof.ML \ + Isar/thy_header.ML Isar/toplevel.ML ML-Systems/mlworks.ML \ + ML-Systems/polyml-3.x.ML ML-Systems/polyml.ML \ + ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML Proof/ROOT.ML \ + Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \ Proof/proofchecker.ML Proof/reconstruct.ML ROOT.ML Syntax/ROOT.ML \ Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ @@ -53,6 +54,7 @@ pattern.ML proofterm.ML pure.ML pure_thy.ML search.ML sign.ML \ sorts.ML tactic.ML tctical.ML term.ML theory.ML theory_data.ML \ thm.ML type.ML type_infer.ML unify.ML + @./mk diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Mon Dec 03 21:03:06 2001 +0100 +++ b/src/Pure/Isar/ROOT.ML Mon Dec 03 21:31:55 2001 +0100 @@ -17,7 +17,7 @@ use "proof_history.ML"; use "args.ML"; use "attrib.ML"; -use "rule_context.ML"; +use "context_rules.ML"; use "net_rules.ML"; use "induct_attrib.ML"; use "method.ML"; @@ -60,7 +60,7 @@ structure ProofHistory = ProofHistory; structure Args = Args; structure Attrib = Attrib; - structure RuleContext = RuleContext; + structure ContextRules = ContextRules; structure Method = Method; structure Calculation = Calculation; structure Obtain = Obtain; diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/Isar/context_rules.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/context_rules.ML Mon Dec 03 21:31:55 2001 +0100 @@ -0,0 +1,260 @@ +(* Title: Pure/Isar/context_rules.ML + ID: $Id$ + Author: Stefan Berghofer and Markus Wenzel, TU Muenchen + License: GPL (GNU GENERAL PUBLIC LICENSE) + +Declarations of intro/elim/dest rules in Pure; see +Provers/classical.ML for a more specialized version of the same idea. +*) + +signature CONTEXT_RULES = +sig + type netpair + type T + val netpair_bang: Proof.context -> netpair + val netpair: Proof.context -> netpair + val netpairs: Proof.context -> netpair list + val orderlist: ((int * int) * 'a) list -> 'a list + val orderlist_no_weight: ((int * int) * 'a) list -> 'a list + val print_global_rules: theory -> unit + val print_local_rules: Proof.context -> unit + val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory + val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory + val Swrap: Proof.context -> (int -> tactic) -> int -> tactic + val wrap: Proof.context -> (int -> tactic) -> int -> tactic + val intro_bang_global: int option -> theory attribute + val elim_bang_global: int option -> theory attribute + val dest_bang_global: int option -> theory attribute + val intro_global: int option -> theory attribute + val elim_global: int option -> theory attribute + val dest_global: int option -> theory attribute + val intro_query_global: int option -> theory attribute + val elim_query_global: int option -> theory attribute + val dest_query_global: int option -> theory attribute + val rule_del_global: theory attribute + val intro_bang_local: int option -> Proof.context attribute + val elim_bang_local: int option -> Proof.context attribute + val dest_bang_local: int option -> Proof.context attribute + val intro_local: int option -> Proof.context attribute + val elim_local: int option -> Proof.context attribute + val dest_local: int option -> Proof.context attribute + val intro_query_local: int option -> Proof.context attribute + val elim_query_local: int option -> Proof.context attribute + val dest_query_local: int option -> Proof.context attribute + val rule_del_local: Proof.context attribute + val setup: (theory -> theory) list +end; + +structure ContextRules: CONTEXT_RULES = +struct + + +(** rule declaration contexts **) + +(* rule kinds *) + +val intro_bangK = (0, false); +val elim_bangK = (0, true); +val introK = (1, false); +val elimK = (1, true); +val intro_queryK = (2, false); +val elim_queryK = (2, true); + +val kind_names = + [(intro_bangK, "safe introduction rules (intro!)"), + (elim_bangK, "safe elimination rules (elim!)"), + (introK, "introduction rules (intro)"), + (elimK, "elimination rules (elim)"), + (intro_queryK, "extra introduction rules (intro?)"), + (elim_queryK, "extra elimination rules (elim?)")]; + +val rule_kinds = map #1 kind_names; +val rule_indexes = distinct (map #1 rule_kinds); + + +(* raw data *) + +type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net; +val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty); + +datatype T = Rules of + {next: int, + rules: (int * ((int * bool) * thm)) list, + netpairs: netpair list, + wrappers: (((int -> tactic) -> int -> tactic) * stamp) list * + (((int -> tactic) -> int -> tactic) * stamp) list}; + +fun make_rules next rules netpairs wrappers = + Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; + +fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = + let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in + make_rules (next - 1) ((w, ((i, b), th)) :: rules) + (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers + end; + +fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) = + let + fun eq_th (_, (_, th')) = Thm.eq_thm (th, th'); + fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair; + in + if not (exists eq_th rules) then rs + else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers + end; + +fun print_rules prt x (Rules {rules, ...}) = + let + fun prt_kind (i, b) = + Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":") + (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None) + (sort (int_ord o pairself fst) rules)); + in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; + + +(* theory and proof data *) + +structure GlobalRulesArgs = +struct + val name = "Isar/rule_context"; + type T = T; + + val empty = make_rules ~1 [] empty_netpairs ([], []); + val copy = I; + val prep_ext = I; + + fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, + Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = + let + val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2'); + val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) => + k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2; + val next = ~ (length rules); + val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) => + map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps) + (empty_netpairs, next upto ~1 ~~ rules); + in make_rules (next - 1) rules netpairs wrappers end; + + val print = print_rules Display.pretty_thm_sg; +end; + +structure GlobalRules = TheoryDataFun(GlobalRulesArgs); +val print_global_rules = GlobalRules.print; + +structure LocalRulesArgs = +struct + val name = GlobalRulesArgs.name; + type T = GlobalRulesArgs.T; + val init = GlobalRules.get; + val print = print_rules ProofContext.pretty_thm; +end; + +structure LocalRules = ProofDataFun(LocalRulesArgs); +val print_local_rules = LocalRules.print; + + +(* access data *) + +fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end; +val netpair_bang = hd o netpairs; +val netpair = hd o tl o netpairs; + + +fun untaglist [] = [] + | untaglist [(k : int * int, x)] = [x] + | untaglist ((k, x) :: (rest as (k', x') :: _)) = + if k = k' then untaglist rest + else x :: untaglist rest; + +fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls); +fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls); + + +fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) => + make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)); + +val addSWrapper = gen_add_wrapper Library.apfst; +val addWrapper = gen_add_wrapper Library.apsnd; + + +fun gen_wrap which ctxt = + let val Rules {wrappers, ...} = LocalRules.get ctxt + in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end; + +val Swrap = gen_wrap #1; +val wrap = gen_wrap #2; + + + +(** attributes **) + +(* add and del rules *) + +local + +fun del map_data (x, th) = + (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th); + +fun add k view map_data opt_w = + (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data; + +in + +val intro_bang_global = add intro_bangK I GlobalRules.map; +val elim_bang_global = add elim_bangK I GlobalRules.map; +val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map; +val intro_global = add introK I GlobalRules.map; +val elim_global = add elimK I GlobalRules.map; +val dest_global = add elimK Tactic.make_elim GlobalRules.map; +val intro_query_global = add intro_queryK I GlobalRules.map; +val elim_query_global = add elim_queryK I GlobalRules.map; +val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map; +val rule_del_global = del GlobalRules.map; + +val intro_bang_local = add intro_bangK I LocalRules.map; +val elim_bang_local = add elim_bangK I LocalRules.map; +val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map; +val intro_local = add introK I LocalRules.map; +val elim_local = add elimK I LocalRules.map; +val dest_local = add elimK Tactic.make_elim LocalRules.map; +val intro_query_local = add intro_queryK I LocalRules.map; +val elim_query_local = add elim_queryK I LocalRules.map; +val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map; +val rule_del_local = del LocalRules.map; + +end; + + +(* concrete syntax *) + +fun add_args a b c x = Attrib.syntax + (Scan.lift (Scan.option Args.nat -- + (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x; + +fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att); + + +val rule_atts = + [("intro", + (add_args intro_bang_global intro_global intro_query_global, + add_args intro_bang_local intro_local intro_query_local), + "declaration of introduction rule"), + ("elim", + (add_args elim_bang_global elim_global elim_query_global, + add_args elim_bang_local elim_local elim_query_local), + "declaration of elimination rule"), + ("dest", + (add_args dest_bang_global dest_global dest_query_global, + add_args dest_bang_local dest_local dest_query_local), + "declaration of destruction rule"), + ("rule", (del_args rule_del_global, del_args rule_del_local), + "remove declaration of intro/elim/dest rule")]; + + + +(** theory setup **) + +val setup = + [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts]; + + +end; diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Mon Dec 03 21:03:06 2001 +0100 +++ b/src/Pure/Isar/method.ML Mon Dec 03 21:31:55 2001 +0100 @@ -36,7 +36,6 @@ val fold: thm list -> Proof.method val multi_resolve: thm list -> thm -> thm Seq.seq val multi_resolves: thm list -> thm list -> thm Seq.seq - val debug_rules: bool ref val rules_tac: Proof.context -> int option -> int -> tactic val rule_tac: thm list -> thm list -> int -> tactic val some_rule_tac: thm list -> Proof.context -> thm list -> int -> tactic @@ -217,15 +216,18 @@ length s1 = length s2 andalso gen_subset e (s1, s2) andalso gen_subset e (s2, s1); -val bires_tac = Tactic.biresolution_from_nets_tac RuleContext.orderlist; +val bires_tac = Tactic.biresolution_from_nets_tac ContextRules.orderlist; fun safe_step_tac ctxt = - RuleContext.Swrap ctxt (eq_assume_tac ORELSE' bires_tac true (RuleContext.Snetpair ctxt)); + ContextRules.Swrap ctxt + (eq_assume_tac ORELSE' + bires_tac true (ContextRules.netpair_bang ctxt)); fun unsafe_step_tac ctxt = - RuleContext.wrap ctxt (assume_tac APPEND' - bires_tac false (RuleContext.Snetpair ctxt) APPEND' - bires_tac false (RuleContext.netpair ctxt)); + ContextRules.wrap ctxt + (assume_tac APPEND' + bires_tac false (ContextRules.netpair_bang ctxt) APPEND' + bires_tac false (ContextRules.netpair ctxt)); fun step_tac ctxt i = REPEAT_DETERM1 (REMDUPS (safe_step_tac ctxt) i) ORELSE @@ -243,11 +245,7 @@ in -val debug_rules = ref false; - -fun rules_tac ctxt opt_lim = - (conditional (! debug_rules) (fn () => RuleContext.print_local_rules ctxt); - DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4); +fun rules_tac ctxt opt_lim = DEEPEN (2, if_none opt_lim 20) (intpr_tac ctxt [] 0) 4; end; @@ -256,8 +254,8 @@ local -fun may_unify t nets = RuleContext.orderlist_no_weight - (flat (map (fn net => Net.unify_term net t) nets)); +fun may_unify t nets = + flat (map (ContextRules.orderlist_no_weight o (fn net => Net.unify_term net t)) nets); fun find_erules [] = K [] | find_erules (fact :: _) = may_unify (Logic.strip_assums_concl (#prop (Thm.rep_thm fact))); @@ -274,7 +272,7 @@ fun gen_some_rule_tac tac arg_rules ctxt facts = SUBGOAL (fn (goal, i) => let - val netpairs = RuleContext.netpairs ctxt; + val netpairs = ContextRules.netpairs ctxt; val rules = if not (null arg_rules) then arg_rules else map #2 (find_erules facts (map #2 netpairs) @ find_rules goal (map #1 netpairs)); @@ -505,23 +503,23 @@ >> (pair (I: Proof.context -> Proof.context) o att); val rules_modifiers = - [modifier destN Args.query_colon Args.query RuleContext.dest_query_local, - modifier destN Args.bang_colon Args.bang RuleContext.dest_bang_local, - modifier destN Args.colon (Scan.succeed ()) RuleContext.dest_local, - modifier elimN Args.query_colon Args.query RuleContext.elim_query_local, - modifier elimN Args.bang_colon Args.bang RuleContext.elim_bang_local, - modifier elimN Args.colon (Scan.succeed ()) RuleContext.elim_local, - modifier introN Args.query_colon Args.query RuleContext.intro_query_local, - modifier introN Args.bang_colon Args.bang RuleContext.intro_bang_local, - modifier introN Args.colon (Scan.succeed ()) RuleContext.intro_local, - Args.del -- Args.colon >> K (I, RuleContext.rule_del_local)]; + [modifier destN Args.query_colon Args.query ContextRules.dest_query_local, + modifier destN Args.bang_colon Args.bang ContextRules.dest_bang_local, + modifier destN Args.colon (Scan.succeed ()) ContextRules.dest_local, + modifier elimN Args.query_colon Args.query ContextRules.elim_query_local, + modifier elimN Args.bang_colon Args.bang ContextRules.elim_bang_local, + modifier elimN Args.colon (Scan.succeed ()) ContextRules.elim_local, + modifier introN Args.query_colon Args.query ContextRules.intro_query_local, + modifier introN Args.bang_colon Args.bang ContextRules.intro_bang_local, + modifier introN Args.colon (Scan.succeed ()) ContextRules.intro_local, + Args.del -- Args.colon >> K (I, ContextRules.rule_del_local)]; in fun rules_args m = bang_sectioned_args' rules_modifiers (Scan.lift (Scan.option Args.nat)) m; fun rules_meth n prems ctxt = METHOD (fn facts => - HEADGOAL (insert_tac (prems @ facts) THEN' rules_tac ctxt n)); + HEADGOAL (insert_tac (prems @ facts) THEN' ObjectLogic.atomize_tac THEN' rules_tac ctxt n)); end; @@ -672,7 +670,7 @@ val setup = [MethodsData.init, add_methods pure_methods, - (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [RuleContext.intro_query_global None])])]; + (#1 o PureThy.add_thms [(("", Drule.equal_intr_rule), [ContextRules.intro_query_global None])])]; end; diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/Isar/obtain.ML --- a/src/Pure/Isar/obtain.ML Mon Dec 03 21:03:06 2001 +0100 +++ b/src/Pure/Isar/obtain.ML Mon Dec 03 21:31:55 2001 +0100 @@ -107,7 +107,7 @@ |> Proof.enter_forward |> Proof.begin_block |> Proof.fix_i [([thesisN], None)] - |> Proof.assume_i [((thatN, [RuleContext.intro_query_local None]), [(that_prop, ([], []))])] + |> Proof.assume_i [((thatN, [ContextRules.intro_query_local None]), [(that_prop, ([], []))])] |> (fn state' => state' |> Proof.from_facts chain_facts diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/Isar/rule_context.ML --- a/src/Pure/Isar/rule_context.ML Mon Dec 03 21:03:06 2001 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,259 +0,0 @@ -(* Title: Pure/Isar/rule_context.ML - ID: $Id$ - Author: Stefan Berghofer and Markus Wenzel, TU Muenchen - License: GPL (GNU GENERAL PUBLIC LICENSE) - -Declarations of intro/elim/dest rules in Pure; see -Provers/classical.ML for a more specialized version. -*) - -signature RULE_CONTEXT = -sig - type netpair - type T - val Snetpair: Proof.context -> netpair - val netpair: Proof.context -> netpair - val netpairs: Proof.context -> netpair list - val orderlist: ((int * int) * 'a) list -> 'a list - val orderlist_no_weight: ((int * int) * 'a) list -> 'a list - val print_global_rules: theory -> unit - val print_local_rules: Proof.context -> unit - val addSWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory - val addWrapper: ((int -> tactic) -> int -> tactic) -> theory -> theory - val Swrap: Proof.context -> (int -> tactic) -> int -> tactic - val wrap: Proof.context -> (int -> tactic) -> int -> tactic - val intro_bang_global: int option -> theory attribute - val elim_bang_global: int option -> theory attribute - val dest_bang_global: int option -> theory attribute - val intro_global: int option -> theory attribute - val elim_global: int option -> theory attribute - val dest_global: int option -> theory attribute - val intro_query_global: int option -> theory attribute - val elim_query_global: int option -> theory attribute - val dest_query_global: int option -> theory attribute - val rule_del_global: theory attribute - val intro_bang_local: int option -> Proof.context attribute - val elim_bang_local: int option -> Proof.context attribute - val dest_bang_local: int option -> Proof.context attribute - val intro_local: int option -> Proof.context attribute - val elim_local: int option -> Proof.context attribute - val dest_local: int option -> Proof.context attribute - val intro_query_local: int option -> Proof.context attribute - val elim_query_local: int option -> Proof.context attribute - val dest_query_local: int option -> Proof.context attribute - val rule_del_local: Proof.context attribute - val setup: (theory -> theory) list -end; - -structure RuleContext: RULE_CONTEXT = -struct - - -(** rule declaration contexts **) - -(* rule kinds *) - -val intro_bangK = (0, false); -val elim_bangK = (0, true); -val introK = (1, false); -val elimK = (1, true); -val intro_queryK = (2, false); -val elim_queryK = (2, true); - -val kind_names = - [(intro_bangK, "safe introduction rules (intro!)"), - (elim_bangK, "safe elimination rules (elim!)"), - (introK, "introduction rules (intro)"), - (elimK, "elimination rules (elim)"), - (intro_queryK, "extra introduction rules (intro?)"), - (elim_queryK, "extra elimination rules (elim?)")]; - -val rule_kinds = map #1 kind_names; -val rule_indexes = distinct (map #1 rule_kinds); - - -(* raw data *) - -type netpair = ((int * int) * (bool * thm)) Net.net * ((int * int) * (bool * thm)) Net.net; -val empty_netpairs: netpair list = replicate (length rule_indexes) (Net.empty, Net.empty); - -datatype T = Rules of - {next: int, - rules: (int * ((int * bool) * thm)) list, - netpairs: netpair list, - wrappers: (((int -> tactic) -> int -> tactic) * stamp) list * - (((int -> tactic) -> int -> tactic) * stamp) list}; - -fun make_rules next rules netpairs wrappers = - Rules {next = next, rules = rules, netpairs = netpairs, wrappers = wrappers}; - -fun add_rule (i, b) opt_w th (Rules {next, rules, netpairs, wrappers}) = - let val w = (case opt_w of Some w => w | None => Tactic.subgoals_of_brl (b, th)) in - make_rules (next - 1) ((w, ((i, b), th)) :: rules) - (map_nth_elem i (curry insert_tagged_brl ((w, next), (b, th))) netpairs) wrappers - end; - -fun del_rule th (rs as Rules {next, rules, netpairs, wrappers}) = - let - fun eq_th (_, (_, th')) = Thm.eq_thm (th, th'); - fun del b netpair = delete_tagged_brl ((b, th), netpair) handle Net.DELETE => netpair; - in - if not (exists eq_th rules) then rs - else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers - end; - -fun print_rules prt x (Rules {rules, ...}) = - let - fun prt_kind (i, b) = - Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":") - (mapfilter (fn (_, (k, th)) => if k = (i, b) then Some (prt x th) else None) - (sort (int_ord o pairself fst) rules)); - in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end; - - -(* theory and proof data *) - -structure GlobalRulesArgs = -struct - val name = "Isar/rule_context"; - type T = T; - - val empty = make_rules ~1 [] empty_netpairs ([], []); - val copy = I; - val prep_ext = I; - - fun merge (Rules {rules = rules1, wrappers = (ws1, ws1'), ...}, - Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) = - let - val wrappers = (gen_merge_lists' eq_snd ws1 ws2, gen_merge_lists' eq_snd ws1' ws2'); - val rules = gen_merge_lists' (fn ((_, (k1, th1)), (_, (k2, th2))) => - k1 = k2 andalso Thm.eq_thm (th1, th2)) rules1 rules2; - val next = ~ (length rules); - val netpairs = foldl (fn (nps, (n, (w, ((i, b), th)))) => - map_nth_elem i (curry insert_tagged_brl ((w, n), (b, th))) nps) - (empty_netpairs, next upto ~1 ~~ rules); - in make_rules (next - 1) rules netpairs wrappers end; - - val print = print_rules Display.pretty_thm_sg; -end; - -structure GlobalRules = TheoryDataFun(GlobalRulesArgs); -val print_global_rules = GlobalRules.print; - -structure LocalRulesArgs = -struct - val name = GlobalRulesArgs.name; - type T = GlobalRulesArgs.T; - val init = GlobalRules.get; - val print = print_rules ProofContext.pretty_thm; -end; - -structure LocalRules = ProofDataFun(LocalRulesArgs); -val print_local_rules = LocalRules.print; - -fun netpairs ctxt = let val Rules {netpairs, ...} = LocalRules.get ctxt in netpairs end; -val Snetpair = hd o netpairs; -val netpair = hd o tl o netpairs; - - -fun untaglist [] = [] - | untaglist [(k : int * int, x)] = [x] - | untaglist ((k, x) :: (rest as (k', x') :: _)) = - if k = k' then untaglist rest - else x :: untaglist rest; - -fun orderlist brls = untaglist (sort (prod_ord int_ord int_ord o pairself fst) brls); -fun orderlist_no_weight brls = untaglist (sort (int_ord o pairself (snd o fst)) brls); - - -(* wrappers *) - -fun gen_add_wrapper upd w = GlobalRules.map (fn (rs as Rules {next, rules, netpairs, wrappers}) => - make_rules next rules netpairs (upd (fn ws => (w, stamp ()) :: ws) wrappers)); - -val addSWrapper = gen_add_wrapper Library.apfst; -val addWrapper = gen_add_wrapper Library.apsnd; - - -fun gen_wrap which ctxt = - let val Rules {wrappers, ...} = LocalRules.get ctxt - in fn tac => foldr (fn ((w, _), t) => w t) (which wrappers, tac) end; - -val Swrap = gen_wrap #1; -val wrap = gen_wrap #2; - - - -(** attributes **) - -(* add and del rules *) - -local - -fun del map_data (x, th) = - (map_data (del_rule th o del_rule (Tactic.make_elim th)) x, th); - -fun add k view map_data opt_w = - (fn (x, th) => (map_data (add_rule k opt_w th) x, th)) o del map_data; - -in - -val intro_bang_global = add intro_bangK I GlobalRules.map; -val elim_bang_global = add elim_bangK I GlobalRules.map; -val dest_bang_global = add elim_bangK Tactic.make_elim GlobalRules.map; -val intro_global = add introK I GlobalRules.map; -val elim_global = add elimK I GlobalRules.map; -val dest_global = add elimK Tactic.make_elim GlobalRules.map; -val intro_query_global = add intro_queryK I GlobalRules.map; -val elim_query_global = add elim_queryK I GlobalRules.map; -val dest_query_global = add elim_queryK Tactic.make_elim GlobalRules.map; -val rule_del_global = del GlobalRules.map; - -val intro_bang_local = add intro_bangK I LocalRules.map; -val elim_bang_local = add elim_bangK I LocalRules.map; -val dest_bang_local = add elim_bangK Tactic.make_elim LocalRules.map; -val intro_local = add introK I LocalRules.map; -val elim_local = add elimK I LocalRules.map; -val dest_local = add elimK Tactic.make_elim LocalRules.map; -val intro_query_local = add intro_queryK I LocalRules.map; -val elim_query_local = add elim_queryK I LocalRules.map; -val dest_query_local = add elim_queryK Tactic.make_elim LocalRules.map; -val rule_del_local = del LocalRules.map; - -end; - - -(* concrete syntax *) - -fun add_args a b c x = Attrib.syntax - (Scan.lift (Scan.option Args.nat -- - (Args.bang >> K a || Args.query >> K c || Scan.succeed b) >> op |>)) x; - -fun del_args att = Attrib.syntax (Scan.lift Args.del >> K att); - - -val rule_atts = - [("intro", - (add_args intro_bang_global intro_global intro_query_global, - add_args intro_bang_local intro_local intro_query_local), - "declaration of introduction rule"), - ("elim", - (add_args elim_bang_global elim_global elim_query_global, - add_args elim_bang_local elim_local elim_query_local), - "declaration of elimination rule"), - ("dest", - (add_args dest_bang_global dest_global dest_query_global, - add_args dest_bang_local dest_local dest_query_local), - "declaration of destruction rule"), - ("rule", (del_args rule_del_global, del_args rule_del_local), - "remove declaration of intro/elim/dest rule")]; - - - -(** theory setup **) - -val setup = - [GlobalRules.init, LocalRules.init, Attrib.add_attributes rule_atts]; - - -end; diff -r 94e812f9683e -r 5fad0e7129c3 src/Pure/pure.ML --- a/src/Pure/pure.ML Mon Dec 03 21:03:06 2001 +0100 +++ b/src/Pure/pure.ML Mon Dec 03 21:31:55 2001 +0100 @@ -13,7 +13,7 @@ ProofContext.setup @ Locale.setup @ Attrib.setup @ - RuleContext.setup @ + ContextRules.setup @ InductAttrib.setup @ Method.setup @ Calculation.setup @