equal
deleted
inserted
replaced
11 val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b |
11 val repeat_yield: ('a -> 'b -> ('a * 'b) option) -> 'a -> 'b -> 'a * 'b |
12 |
12 |
13 (*class dictionaries*) |
13 (*class dictionaries*) |
14 type class = string list |
14 type class = string list |
15 val basicC: class |
15 val basicC: class |
|
16 val string_of_class: class -> string |
16 type 'a dict = (class * 'a) Ord_List.T |
17 type 'a dict = (class * 'a) Ord_List.T |
17 val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict |
18 val dict_map_default: class * 'a -> ('a -> 'a) -> 'a dict -> 'a dict |
18 val dict_update: class * 'a -> 'a dict -> 'a dict |
19 val dict_update: class * 'a -> 'a dict -> 'a dict |
19 val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict |
20 val dict_merge: ('a * 'a -> 'a) -> 'a dict * 'a dict -> 'a dict |
20 val dict_lookup: 'a dict -> class -> 'a list |
21 val dict_lookup: 'a dict -> class -> 'a list |
|
22 val dict_get: 'a dict -> class -> 'a option |
21 |
23 |
22 (*types*) |
24 (*types*) |
23 val dest_funT: int -> typ -> typ list * typ |
25 val dest_funT: int -> typ -> typ list * typ |
24 |
26 |
25 (*terms*) |
27 (*terms*) |
74 |
76 |
75 type class = string list |
77 type class = string list |
76 |
78 |
77 val basicC = [] |
79 val basicC = [] |
78 |
80 |
|
81 fun string_of_class [] = "basic" |
|
82 | string_of_class cs = "basic." ^ space_implode "." cs |
|
83 |
79 type 'a dict = (class * 'a) Ord_List.T |
84 type 'a dict = (class * 'a) Ord_List.T |
80 |
85 |
81 fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2) |
86 fun class_ord ((cs1, _), (cs2, _)) = list_ord fast_string_ord (cs1, cs2) |
82 |
87 |
83 fun dict_insert (cs, x) d = |
88 fun dict_insert (cs, x) d = |
92 fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) |
97 fun dict_merge val_merge = sort class_ord o AList.join (op =) (K val_merge) |
93 |
98 |
94 fun dict_lookup d cs = |
99 fun dict_lookup d cs = |
95 let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE |
100 let fun match (cs', x) = if is_prefix (op =) cs' cs then SOME x else NONE |
96 in map_filter match d end |
101 in map_filter match d end |
|
102 |
|
103 fun dict_get d cs = |
|
104 (case AList.lookup (op =) d cs of |
|
105 NONE => (case cs of [] => NONE | _ => dict_get d (take (length cs - 1) cs)) |
|
106 | SOME x => SOME x) |
97 |
107 |
98 |
108 |
99 (* types *) |
109 (* types *) |
100 |
110 |
101 val dest_funT = |
111 val dest_funT = |