src/Pure/General/scan.ML
changeset 7025 afbd8241797b
parent 6640 d2e8342bf5c3
child 8653 a88e91792f0a
equal deleted inserted replaced
7024:44bd3c094fd6 7025:afbd8241797b
    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;