--- a/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 08:39:24 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_utils.ML Wed Dec 15 10:12:44 2010 +0100
@@ -13,11 +13,13 @@
(*class dictionaries*)
type class = string list
val basicC: class
+ val string_of_class: class -> string
type 'a dict = (class * 'a) Ord_List.T
val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict
val dict_update: class * 'a -> 'a dict -> 'a dict
val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict
val dict_lookup: 'a dict -> class -> 'a list
+ val dict_get: 'a dict -> class -> 'a option
(*types*)
val dest_funT: int -> typ -> typ list * typ
@@ -76,6 +78,9 @@
val basicC = []
+fun string_of_class [] = "basic"
+ | string_of_class cs = "basic." ^ space_implode "." cs
+
type 'a dict = (class * 'a) Ord_List.T
fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2)
@@ -95,6 +100,11 @@
let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE
in map_filter match d end
+fun dict_get d cs =
+ (case AList.lookup (op =) d cs of
+ NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs))
+ | SOME x => SOME x)
+
(* types *)