# HG changeset patch # User wenzelm # Date 1183917125 -7200 # Node ID 2332c79f4dc8a3f49328e6a3dd0f700a1aacba9d # Parent 4bdcb024e95dd158ad5334a5ad98c58a4ebab1e6 thm tag: Markup.property list; diff -r 4bdcb024e95d -r 2332c79f4dc8 src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Sun Jul 08 19:52:04 2007 +0200 +++ b/src/Pure/Isar/rule_cases.ML Sun Jul 08 19:52:05 2007 +0200 @@ -214,12 +214,11 @@ val consumes_tagN = "consumes"; fun lookup_consumes th = - let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [th]) in - (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of - NONE => NONE - | SOME [s] => (case Syntax.read_nat s of SOME n => SOME n | _ => err ()) - | _ => err ()) - end; + (case AList.lookup (op =) (Thm.get_tags th) (consumes_tagN) of + NONE => NONE + | SOME s => + (case Syntax.read_nat s of SOME n => SOME n + | _ => raise THM ("Malformed 'consumes' tag of theorem", 0, [th]))); fun get_consumes th = the_default 0 (lookup_consumes th); @@ -227,7 +226,7 @@ | put_consumes (SOME n) th = th |> PureThy.untag_rule consumes_tagN |> PureThy.tag_rule - (consumes_tagN, [Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)]); + (consumes_tagN, Library.string_of_int (if n < 0 then Thm.nprems_of th + n else n)); fun add_consumes k th = put_consumes (SOME (k + get_consumes th)) th; @@ -242,14 +241,19 @@ (** case names **) +val implode_args = space_implode ";"; +val explode_args = space_explode ";"; + val case_names_tagN = "case_names"; fun add_case_names NONE = I | add_case_names (SOME names) = PureThy.untag_rule case_names_tagN - #> PureThy.tag_rule (case_names_tagN, names); + #> PureThy.tag_rule (case_names_tagN, implode_args names); -fun lookup_case_names th = AList.lookup (op =) (Thm.get_tags th) case_names_tagN; +fun lookup_case_names th = + AList.lookup (op =) (Thm.get_tags th) case_names_tagN + |> Option.map explode_args; val save_case_names = add_case_names o lookup_case_names; val name = add_case_names o SOME; @@ -261,22 +265,23 @@ val case_concl_tagN = "case_conclusion"; -fun is_case_concl name ((a, b :: _): tag) = (a = case_concl_tagN andalso b = name) - | is_case_concl _ _ = false; +fun get_case_concl name (a, b) = + if a = case_concl_tagN then + (case explode_args b of c :: cs => if c = name then SOME cs else NONE) + else NONE; fun add_case_concl (name, cs) = Thm.map_tags (fn tags => - filter_out (is_case_concl name) tags @ [(case_concl_tagN, name :: cs)]); + filter_out (is_some o get_case_concl name) tags @ + [(case_concl_tagN, implode_args (name :: cs))]); fun get_case_concls th name = - (case find_first (is_case_concl name) (Thm.get_tags th) of - SOME (_, _ :: cs) => cs - | _ => []); + these (get_first (get_case_concl name) (Thm.get_tags th)); fun save_case_concls th = let val concls = Thm.get_tags th |> map_filter - (fn (a, b :: cs) => - if a = case_concl_tagN then SOME (b, cs) else NONE - | _ => NONE) + (fn (a, b) => + if a = case_concl_tagN then (case explode_args b of c :: cs => SOME (c, cs) | _ => NONE) + else NONE) in fold add_case_concl concls end; fun case_conclusion concl = Thm.rule_attribute (fn _ => add_case_concl concl); diff -r 4bdcb024e95d -r 2332c79f4dc8 src/Pure/display.ML --- a/src/Pure/display.ML Sun Jul 08 19:52:04 2007 +0200 +++ b/src/Pure/display.ML Sun Jul 08 19:52:05 2007 +0200 @@ -62,7 +62,7 @@ val show_hyps = ref false; (*false: print meta-hypotheses as dots*) val show_tags = ref false; (*false: suppress tags*) -fun pretty_tag (name, args) = Pretty.strs (name :: map Library.quote args); +fun pretty_tag (name, arg) = Pretty.strs [name, Library.quote arg]; val pretty_tags = Pretty.list "[" "]" o map pretty_tag; fun pretty_flexpair pp (t, u) = Pretty.block diff -r 4bdcb024e95d -r 2332c79f4dc8 src/Pure/pure_thy.ML --- a/src/Pure/pure_thy.ML Sun Jul 08 19:52:04 2007 +0200 +++ b/src/Pure/pure_thy.ML Sun Jul 08 19:52:05 2007 +0200 @@ -27,9 +27,9 @@ signature PURE_THY = sig include BASIC_PURE_THY - val tag_rule: tag -> thm -> thm + val tag_rule: Markup.property -> thm -> thm val untag_rule: string -> thm -> thm - val tag: tag -> attribute + val tag: Markup.property -> attribute val untag: string -> attribute val has_name_hint: thm -> bool val get_name_hint: thm -> string @@ -39,7 +39,7 @@ val kind_rule: string -> thm -> thm val kind: string -> attribute val kind_internal: attribute - val has_internal: tag list -> bool + val has_internal: Markup.property list -> bool val is_internal: thm -> bool val string_of_thmref: thmref -> string val get_thm_closure: theory -> thmref -> thm @@ -112,36 +112,28 @@ fun tag tg x = Thm.rule_attribute (K (tag_rule tg)) x; fun untag s x = Thm.rule_attribute (K (untag_rule s)) x; -fun simple_tag name x = tag (name, []) x; - (* unofficial theorem names *) -fun the_name_hint thm = - (case AList.lookup (op =) (Thm.get_tags thm) "name" of - SOME (k :: _) => k - | _ => raise Option); +fun the_name_hint thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.nameN); val has_name_hint = can the_name_hint; val get_name_hint = the_default "??.unknown" o try the_name_hint; -fun put_name_hint name = untag_rule "name" #> tag_rule ("name", [name]); +fun put_name_hint name = untag_rule Markup.nameN #> tag_rule (Markup.nameN, name); (* theorem kinds *) -fun the_kind thm = - (case AList.lookup (op =) (Thm.get_tags thm) "kind" of - SOME (k :: _) => k - | _ => raise Option); +fun the_kind thm = the (AList.lookup (op =) (Thm.get_tags thm) Markup.kindN); val has_kind = can the_kind; val get_kind = the_default "??.unknown" o try the_kind; -fun kind_rule k = tag_rule ("kind", [k]) o untag_rule "kind"; +fun kind_rule k = tag_rule (Markup.kindN, k) o untag_rule Markup.kindN; fun kind k x = if k = "" then x else Thm.rule_attribute (K (kind_rule k)) x; fun kind_internal x = kind Thm.internalK x; -fun has_internal tags = exists (fn ("kind", [k]) => k = Thm.internalK | _ => false) tags; +fun has_internal tags = exists (fn tg => tg = (Markup.kindN, Thm.internalK)) tags; val is_internal = has_internal o Thm.get_tags; diff -r 4bdcb024e95d -r 2332c79f4dc8 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun Jul 08 19:52:04 2007 +0200 +++ b/src/Pure/thm.ML Sun Jul 08 19:52:05 2007 +0200 @@ -35,8 +35,6 @@ val cterm_of: theory -> term -> cterm val ctyp_of_term: cterm -> ctyp - type tag = string * string list - (*meta theorems*) type thm type conv = cterm -> thm @@ -44,7 +42,7 @@ val rep_thm: thm -> {thy: theory, der: bool * Proofterm.proof, - tags: tag list, + tags: Markup.property list, maxidx: int, shyps: sort list, hyps: term list, @@ -53,7 +51,7 @@ val crep_thm: thm -> {thy: theory, der: bool * Proofterm.proof, - tags: tag list, + tags: Markup.property list, maxidx: int, shyps: sort list, hyps: cterm list, @@ -140,8 +138,8 @@ val full_prop_of: thm -> term val get_name: thm -> string val put_name: string -> thm -> thm - val get_tags: thm -> tag list - val map_tags: (tag list -> tag list) -> thm -> thm + val get_tags: thm -> Markup.property list + val map_tags: (Markup.property list -> Markup.property list) -> thm -> thm val compress: thm -> thm val adjust_maxidx_thm: int -> thm -> thm val rename_boundvars: term -> term -> thm -> thm @@ -356,12 +354,10 @@ (*** Meta theorems ***) -type tag = string * string list; - abstype thm = Thm of {thy_ref: theory_ref, (*dynamic reference to theory*) der: bool * Pt.proof, (*derivation*) - tags: tag list, (*additional annotations/comments*) + tags: Markup.property list, (*additional annotations/comments*) maxidx: int, (*maximum index of any Var or TVar*) shyps: sort list, (*sort hypotheses as ordered list*) hyps: term list, (*hypotheses as ordered list*)