58 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) -> |
58 'b * ('b -> bool) -> ('b list -> 'd list * 'b list) -> |
59 ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c |
59 ('b list -> 'e * 'b list) option -> 'a -> 'd list * 'c |
60 val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
60 val single: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
61 val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
61 val bulk: ('a -> 'b * 'a) -> 'a -> 'b list * 'a |
62 type lexicon |
62 type lexicon |
63 val dest_lexicon: lexicon -> string list list |
63 val dest_lexicon: lexicon -> string list |
64 val make_lexicon: string list list -> lexicon |
64 val make_lexicon: string list list -> lexicon |
65 val empty_lexicon: lexicon |
65 val empty_lexicon: lexicon |
66 val extend_lexicon: lexicon -> string list list -> lexicon |
66 val extend_lexicon: lexicon -> string list list -> lexicon |
67 val merge_lexicons: lexicon -> lexicon -> lexicon |
67 val merge_lexicons: lexicon -> lexicon -> lexicon |
68 val literal: lexicon -> string list -> string list * string list |
68 val literal: lexicon -> string list -> string list * string list |
238 val no_literal = []; |
238 val no_literal = []; |
239 |
239 |
240 |
240 |
241 (* dest_lexicon *) |
241 (* dest_lexicon *) |
242 |
242 |
243 fun dest_lexicon Empty = [] |
243 fun dest_lex Empty = [] |
244 | dest_lexicon (Branch (_, [], lt, eq, gt)) = |
244 | dest_lex (Branch (_, [], lt, eq, gt)) = |
245 dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt |
245 dest_lex lt @ dest_lex eq @ dest_lex gt |
246 | dest_lexicon (Branch (_, cs, lt, eq, gt)) = |
246 | dest_lex (Branch (_, cs, lt, eq, gt)) = |
247 dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt; |
247 dest_lex lt @ [cs] @ dest_lex eq @ dest_lex gt; |
|
248 |
|
249 val dest_lexicon = map implode o dest_lex; |
248 |
250 |
249 |
251 |
250 (* empty, extend, make, merge lexicons *) |
252 (* empty, extend, make, merge lexicons *) |
251 |
253 |
252 val empty_lexicon = Empty; |
254 val empty_lexicon = Empty; |
263 Branch (c, chrs, Empty, Empty, Empty) |
265 Branch (c, chrs, Empty, Empty, Empty) |
264 | add Empty (c :: cs) = |
266 | add Empty (c :: cs) = |
265 Branch (c, no_literal, Empty, add Empty cs, Empty) |
267 Branch (c, no_literal, Empty, add Empty cs, Empty) |
266 | add lex [] = lex; |
268 | add lex [] = lex; |
267 in add lex chrs end; |
269 in add lex chrs end; |
268 in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; |
270 in foldl ext (lexicon, chrss \\ dest_lex lexicon) end; |
269 |
271 |
270 val make_lexicon = extend_lexicon empty_lexicon; |
272 val make_lexicon = extend_lexicon empty_lexicon; |
271 |
273 |
272 fun merge_lexicons lex1 lex2 = |
274 fun merge_lexicons lex1 lex2 = |
273 let |
275 let |
274 val chss1 = dest_lexicon lex1; |
276 val chss1 = dest_lex lex1; |
275 val chss2 = dest_lexicon lex2; |
277 val chss2 = dest_lex lex2; |
276 in |
278 in |
277 if chss2 subset chss1 then lex1 |
279 if chss2 subset chss1 then lex1 |
278 else if chss1 subset chss2 then lex2 |
280 else if chss1 subset chss2 then lex2 |
279 else extend_lexicon lex1 chss2 |
281 else extend_lexicon lex1 chss2 |
280 end; |
282 end; |