# HG changeset patch # User wenzelm # Date 1137880947 -3600 # Node ID f5ea6b0d35018d6c93a434c657429df788118b28 # Parent 0508c80178395e81810a93c57e054da476f9037d simplified type attribute; removed rule/declaration (cf. thm.ML); removed obsolete theory/proof/generic/common; removed obsolete global/local/context_attribute(_i); added attribute(_i); renamed attribute to internal; diff -r 0508c8017839 -r f5ea6b0d3501 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Sat Jan 21 23:02:25 2006 +0100 +++ b/src/Pure/Isar/attrib.ML Sat Jan 21 23:02:27 2006 +0100 @@ -2,100 +2,62 @@ ID: $Id$ Author: Markus Wenzel, TU Muenchen -Symbolic theorem attributes. +Symbolic representation of attributes -- with name and syntax. *) signature BASIC_ATTRIB = sig val print_attributes: theory -> unit - val Attribute: bstring -> - (Args.src -> theory attribute) * (Args.src -> ProofContext.context attribute) -> - string -> unit + val Attribute: bstring -> (Args.src -> attribute) -> string -> unit end; signature ATTRIB = sig include BASIC_ATTRIB - val rule: ('a -> thm -> thm) -> 'a attribute - val declaration: (thm -> 'a -> 'a) -> 'a attribute type src - val theory: Context.generic attribute -> theory attribute - val context: Context.generic attribute -> ProofContext.context attribute - val generic: theory attribute * ProofContext.context attribute -> Context.generic attribute - val common: (src -> Context.generic attribute) -> - (src -> theory attribute) * (src -> ProofContext.context attribute) exception ATTRIB_FAIL of (string * Position.T) * exn val intern: theory -> xstring -> string val intern_src: theory -> src -> src - val global_attribute_i: theory -> src -> theory attribute - val global_attribute: theory -> src -> theory attribute - val local_attribute_i: theory -> src -> ProofContext.context attribute - val local_attribute: theory -> src -> ProofContext.context attribute - val context_attribute_i: ProofContext.context -> Args.src -> ProofContext.context attribute - val context_attribute: ProofContext.context -> Args.src -> ProofContext.context attribute - val undef_global_attribute: theory attribute - val undef_local_attribute: ProofContext.context attribute - val generic_attribute_i: theory -> src -> Context.generic attribute - val generic_attribute: theory -> src -> Context.generic attribute - val map_specs: ('a -> 'b attribute) -> - (('c * 'a list) * 'd) list -> (('c * 'b attribute list) * 'd) list - val map_facts: ('a -> 'b attribute) -> + val attribute: theory -> src -> attribute + val attribute_i: theory -> src -> attribute + val map_specs: ('a -> attribute) -> + (('c * 'a list) * 'd) list -> (('c * attribute list) * 'd) list + val map_facts: ('a -> attribute) -> (('c * 'a list) * ('d * 'a list) list) list -> - (('c * 'b attribute list) * ('d * 'b attribute list) list) list - val crude_closure: ProofContext.context -> src -> src - val add_attributes: (bstring * ((src -> theory attribute) * - (src -> ProofContext.context attribute)) * string) list -> theory -> theory + (('c * attribute list) * ('d * attribute list) list) list + val crude_closure: Context.proof -> src -> src + val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory val global_thm: theory * Args.T list -> thm * (theory * Args.T list) val global_thms: theory * Args.T list -> thm list * (theory * Args.T list) val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list) - val local_thm: ProofContext.context * Args.T list -> - thm * (ProofContext.context * Args.T list) - val local_thms: ProofContext.context * Args.T list -> - thm list * (ProofContext.context * Args.T list) - val local_thmss: ProofContext.context * Args.T list -> - thm list * (ProofContext.context * Args.T list) + val local_thm: Context.proof * Args.T list -> thm * (Context.proof * Args.T list) + val local_thms: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list) + val local_thmss: Context.proof * Args.T list -> thm list * (Context.proof * Args.T list) val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list) val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) val thmss: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list) - val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> src -> 'a attribute - val no_args: 'a attribute -> src -> 'a attribute - val add_del_args: 'a attribute -> 'a attribute -> src -> 'a attribute - val attribute: Context.generic attribute -> src + val syntax: (Context.generic * Args.T list -> + attribute * (Context.generic * Args.T list)) -> src -> attribute + val no_args: attribute -> src -> attribute + val add_del_args: attribute -> attribute -> src -> attribute + val internal: attribute -> src end; structure Attrib: ATTRIB = struct -val rule = Drule.rule_attribute; -val declaration = Drule.declaration_attribute; - type src = Args.src; -(** generic attributes **) - -fun generic (global_att, local_att) = - fn (Context.Theory thy, th) => apfst Context.Theory (global_att (thy, th)) - | (Context.Proof ctxt, th) => apfst Context.Proof (local_att (ctxt, th)); +(** named attributes **) -fun theory att (thy, th) = apfst Context.the_theory (att (Context.Theory thy, th)); -fun context att (ctxt, th) = apfst Context.the_proof (att (Context.Proof ctxt, th)); - -fun common att = (theory o att, context o att); - - - -(** attributes theory data **) - -(* datatype attributes *) +(* theory data *) structure AttributesData = TheoryDataFun (struct val name = "Isar/attributes"; - type T = - ((((src -> theory attribute) * (src -> ProofContext.context attribute)) - * string) * stamp) NameSpace.table; + type T = (((src -> attribute) * string) * stamp) NameSpace.table; val empty = NameSpace.empty_table; val copy = I; @@ -124,38 +86,22 @@ val intern_src = Args.map_name o intern; -(* get global / local attributes *) +(* get attributes *) exception ATTRIB_FAIL of (string * Position.T) * exn; -fun gen_attribute which thy = +fun attribute_i thy = let val attrs = #2 (AttributesData.get thy); fun attr src = let val ((name, _), pos) = Args.dest_src src in (case Symtab.lookup attrs name of NONE => error ("Unknown attribute: " ^ quote name ^ Position.str_of pos) - | SOME ((p, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (which p src)) + | SOME ((att, _), _) => transform_failure (curry ATTRIB_FAIL (name, pos)) (att src)) end; in attr end; -val global_attribute_i = gen_attribute fst; -fun global_attribute thy = global_attribute_i thy o intern_src thy; - -val local_attribute_i = gen_attribute snd; -fun local_attribute thy = local_attribute_i thy o intern_src thy; - -val context_attribute_i = local_attribute_i o ProofContext.theory_of; -val context_attribute = local_attribute o ProofContext.theory_of; - -val undef_global_attribute: theory attribute = - fn _ => error "attribute undefined in theory context"; - -val undef_local_attribute: ProofContext.context attribute = - fn _ => error "attribute undefined in proof context"; - -fun generic_attribute thy src = generic (global_attribute thy src, local_attribute thy src); -fun generic_attribute_i thy src = generic (global_attribute_i thy src, local_attribute_i thy src); +fun attribute thy = attribute_i thy o intern_src thy; (* attributed declarations *) @@ -167,11 +113,12 @@ (* crude_closure *) (*Produce closure without knowing facts in advance! The following - should work reasonably well for attribute parsers that do not peek - at the thm structure.*) + works reasonably well for attribute parsers that do not peek at the + thm structure.*) fun crude_closure ctxt src = - (try (fn () => context_attribute_i ctxt src (ctxt, Drule.asm_rl)) (); + (try (fn () => attribute_i (ProofContext.theory_of ctxt) src + (Context.Proof ctxt, Drule.asm_rl)) (); Args.closure src); @@ -179,8 +126,8 @@ fun add_attributes raw_attrs thy = let - val new_attrs = raw_attrs |> map (fn (name, (f, g), comment) => - (name, (((f, g), comment), stamp ()))); + val new_attrs = + raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ()))); fun add attrs = NameSpace.extend_table (Sign.naming_of thy) (attrs, new_attrs) handle Symtab.DUPS dups => error ("Duplicate declaration of attributes(s) " ^ commas_quote dups); @@ -202,7 +149,7 @@ local -fun gen_thm theory_of attrib get pick = Scan.depend (fn st => +fun gen_thm theory_of apply get pick = Scan.depend (fn st => (Scan.ahead Args.alt_name -- Args.named_fact (get st o Fact) >> (fn (s, fact) => ("", Fact s, fact)) || Scan.ahead Args.name -- Args.named_fact (get st o Name) -- Args.thm_sel @@ -213,26 +160,25 @@ >> (fn ((name, thmref, fact), srcs) => let val ths = PureThy.select_thm thmref fact; - val atts = map (attrib (theory_of st)) srcs; - val (st', ths') = Thm.applys_attributes atts (st, ths); + val atts = map (attribute_i (theory_of st)) srcs; + val (st', ths') = foldl_map (apply atts) (st, ths); in (st', pick name ths') end)); val get_thms = Context.cases PureThy.get_thms ProofContext.get_thms; in -val global_thm = gen_thm I global_attribute_i PureThy.get_thms PureThy.single_thm; -val global_thms = gen_thm I global_attribute_i PureThy.get_thms (K I); +val global_thm = gen_thm I Thm.theory_attributes PureThy.get_thms PureThy.single_thm; +val global_thms = gen_thm I Thm.theory_attributes PureThy.get_thms (K I); val global_thmss = Scan.repeat global_thms >> List.concat; val local_thm = - gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms PureThy.single_thm; -val local_thms = - gen_thm ProofContext.theory_of local_attribute_i ProofContext.get_thms (K I); + gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms PureThy.single_thm; +val local_thms = gen_thm ProofContext.theory_of Thm.proof_attributes ProofContext.get_thms (K I); val local_thmss = Scan.repeat local_thms >> List.concat; -val thm = gen_thm Context.theory_of generic_attribute_i get_thms PureThy.single_thm; -val thms = gen_thm Context.theory_of generic_attribute_i get_thms (K I); +val thm = gen_thm Context.theory_of Library.apply get_thms PureThy.single_thm; +val thms = gen_thm Context.theory_of Library.apply get_thms (K I); val thmss = Scan.repeat thms >> List.concat; end; @@ -264,14 +210,14 @@ val COMP_att = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm - >> (fn (i, B) => Drule.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)))); + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => Drule.compose_single (A, i, B)))); val THEN_att = syntax (Scan.lift (Scan.optional (Args.bracks Args.nat) 1) -- thm - >> (fn (i, B) => Drule.rule_attribute (fn _ => fn A => A RSN (i, B)))); + >> (fn (i, B) => Thm.rule_attribute (fn _ => fn A => A RSN (i, B)))); val OF_att = - syntax (thmss >> (fn Bs => Drule.rule_attribute (fn _ => fn A => Bs MRS A))); + syntax (thmss >> (fn Bs => Thm.rule_attribute (fn _ => fn A => Bs MRS A))); (* read_instantiate: named instantiation of type and term variables *) @@ -450,8 +396,8 @@ (* unfold / fold definitions *) -val unfolded = syntax (thmss >> (fn defs => Drule.rule_attribute (K (Tactic.rewrite_rule defs)))); -val folded = syntax (thmss >> (fn defs => Drule.rule_attribute (K (Tactic.fold_rule defs)))); +val unfolded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (Tactic.rewrite_rule defs)))); +val folded = syntax (thmss >> (fn defs => Thm.rule_attribute (K (Tactic.fold_rule defs)))); (* rule cases *) @@ -471,15 +417,15 @@ (* misc rules *) -fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x; -fun elim_format x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x; -fun no_vars x = no_args (Drule.rule_attribute (K (#1 o Drule.freeze_thaw))) x; -fun eta_long x = no_args (Drule.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x; +fun standard x = no_args (Thm.rule_attribute (K Drule.standard)) x; +fun elim_format x = no_args (Thm.rule_attribute (K Tactic.make_elim)) x; +fun no_vars x = no_args (Thm.rule_attribute (K (#1 o Drule.freeze_thaw))) x; +fun eta_long x = no_args (Thm.rule_attribute (K (Drule.fconv_rule Drule.eta_long_conversion))) x; (* internal attribute *) -fun attribute att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none); +fun internal att = Args.src (("Pure.attribute", [Args.mk_attribute att]), Position.none); fun internal_att x = syntax (Scan.lift Args.internal_attribute) x; @@ -488,30 +434,28 @@ val _ = Context.add_setup (add_attributes - [("tagged", common tagged, "tagged theorem"), - ("untagged", common untagged, "untagged theorem"), - ("COMP", common COMP_att, "direct composition with rules (no lifting)"), - ("THEN", common THEN_att, "resolution with rule"), - ("OF", common OF_att, "rule applied to facts"), - ("where", common where_att, "named instantiation of theorem"), - ("of", common of_att, "rule applied to terms"), - ("rename_abs", common rename_abs, "rename bound variables in abstractions"), - ("unfolded", common unfolded, "unfolded definitions"), - ("folded", common folded, "folded definitions"), - ("standard", common standard, "result put into standard form"), - ("elim_format", common elim_format, "destruct rule turned into elimination rule format"), - ("no_vars", common no_vars, "frozen schematic vars"), - ("eta_long", common eta_long, "put theorem into eta long beta normal form"), - ("consumes", common consumes, "number of consumed facts"), - ("case_names", common case_names, "named rule cases"), - ("case_conclusion", common case_conclusion, "named conclusion of rule cases"), - ("params", common params, "named rule parameters"), - ("atomize", (no_args ObjectLogic.declare_atomize, no_args undef_local_attribute), - "declaration of atomize rule"), - ("rulify", (no_args ObjectLogic.declare_rulify, no_args undef_local_attribute), - "declaration of rulify rule"), - ("rule_format", common rule_format_att, "result put into standard rule format"), - ("attribute", common internal_att, "internal attribute")]); + [("tagged", tagged, "tagged theorem"), + ("untagged", untagged, "untagged theorem"), + ("COMP", COMP_att, "direct composition with rules (no lifting)"), + ("THEN", THEN_att, "resolution with rule"), + ("OF", OF_att, "rule applied to facts"), + ("where", where_att, "named instantiation of theorem"), + ("of", of_att, "rule applied to terms"), + ("rename_abs", rename_abs, "rename bound variables in abstractions"), + ("unfolded", unfolded, "unfolded definitions"), + ("folded", folded, "folded definitions"), + ("standard", standard, "result put into standard form"), + ("elim_format", elim_format, "destruct rule turned into elimination rule format"), + ("no_vars", no_vars, "frozen schematic vars"), + ("eta_long", eta_long, "put theorem into eta long beta normal form"), + ("consumes", consumes, "number of consumed facts"), + ("case_names", case_names, "named rule cases"), + ("case_conclusion", case_conclusion, "named conclusion of rule cases"), + ("params", params, "named rule parameters"), + ("atomize", no_args ObjectLogic.declare_atomize, "declaration of atomize rule"), + ("rulify", no_args ObjectLogic.declare_rulify, "declaration of rulify rule"), + ("rule_format", rule_format_att, "result put into standard rule format"), + ("attribute", internal_att, "internal attribute")]); end;