--- 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);
--- 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
--- 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;
--- 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*)