# HG changeset patch # User wenzelm # Date 1011050000 -3600 # Node ID b0c39f9837af6ebfe6cdf4ea3e0df27ea397c796 # Parent 2356740225ce4061b28d4e17c0a54fa067c848b1 save: be slightly more about absent tags; get/add: missing case_names default to numbers 1, 2, 3, ...; diff -r 2356740225ce -r b0c39f9837af src/Pure/Isar/rule_cases.ML --- a/src/Pure/Isar/rule_cases.ML Tue Jan 15 00:12:21 2002 +0100 +++ b/src/Pure/Isar/rule_cases.ML Tue Jan 15 00:13:20 2002 +0100 @@ -12,9 +12,9 @@ val consumes_default: int -> 'a attribute val name: string list -> thm -> thm val case_names: string list -> 'a attribute + val save: thm -> thm -> thm val get: thm -> string list * int val add: thm -> thm * (string list * int) - val save: thm -> thm -> thm type T val empty: T val make: bool -> thm -> string list -> (string * T) list @@ -34,44 +34,55 @@ (* number of consumed facts *) -fun lookup_consumes thm = Library.assoc (Thm.tags_of_thm thm, consumes_tagN); - -fun get_consumes thm = +fun lookup_consumes thm = let fun err () = raise THM ("Malformed 'consumes' tag of theorem", 0, [thm]) in - (case lookup_consumes thm of - None => 0 - | Some [s] => (case Syntax.read_nat s of Some n => n | _ => err ()) + (case Library.assoc (Thm.tags_of_thm thm, consumes_tagN) of + None => None + | Some [s] => (case Syntax.read_nat s of Some n => Some n | _ => err ()) | _ => err ()) end; -fun put_consumes n = - Drule.tag_rule (consumes_tagN, [Library.string_of_int n]) o Drule.untag_rule consumes_tagN; -val save_consumes = put_consumes o get_consumes; +fun put_consumes None th = th + | put_consumes (Some n) th = th + |> Drule.untag_rule consumes_tagN + |> Drule.tag_rule (consumes_tagN, [Library.string_of_int n]); -fun consumes n x = Drule.rule_attribute (K (put_consumes n)) x; +val save_consumes = put_consumes o lookup_consumes; + +fun consumes n x = Drule.rule_attribute (K (put_consumes (Some n))) x; fun consumes_default n x = if Library.is_some (lookup_consumes (#2 x)) then x else consumes n x; (* case names *) -fun name names thm = - thm - |> Drule.untag_rule cases_tagN - |> Drule.tag_rule (cases_tagN, names); +fun put_case_names None thm = thm + | put_case_names (Some names) thm = + thm + |> Drule.untag_rule cases_tagN + |> Drule.tag_rule (cases_tagN, names); -fun get_case_names thm = Library.assocs (Thm.tags_of_thm thm) cases_tagN; -val save_case_names = name o get_case_names; +fun lookup_case_names thm = Library.assoc (Thm.tags_of_thm thm, cases_tagN); +val save_case_names = put_case_names o lookup_case_names; +val name = put_case_names o Some; fun case_names ss = Drule.rule_attribute (K (name ss)); (* access hints *) -fun get thm = (get_case_names thm, get_consumes thm); +fun save thm = save_case_names thm o save_consumes thm; + +fun get thm = + let + val n = if_none (lookup_consumes thm) 0; + val ss = + (case lookup_case_names thm of + None => map Library.string_of_int (1 upto (Thm.nprems_of thm - n)) + | Some ss => ss); + in (ss, n) end; + fun add thm = (thm, get thm); -fun save thm = save_case_names thm o save_consumes thm; - (* prepare cases *) @@ -103,5 +114,4 @@ fun params xss = Drule.rule_attribute (K (rename_params xss)); - end;