1(* Title: Pure/General/source.ML 2 Author: Markus Wenzel, TU Muenchen 3 4Coalgebraic data sources -- efficient purely functional input streams. 5*) 6 7signature SOURCE = 8sig 9 type ('a, 'b) source 10 val get: ('a, 'b) source -> 'a list * ('a, 'b) source 11 val unget: 'a list * ('a, 'b) source -> ('a, 'b) source 12 val get_single: ('a, 'b) source -> ('a * ('a, 'b) source) option 13 val exhaust: ('a, 'b) source -> 'a list 14 val map_filter: ('a -> 'b option) -> ('a, 'c) source -> ('b, ('a, 'c) source) source 15 val filter: ('a -> bool) -> ('a, 'b) source -> ('a, ('a, 'b) source) source 16 val of_list: 'a list -> ('a, 'a list) source 17 val of_string: string -> (string, string list) source 18 val exhausted: ('a, 'b) source -> ('a, 'a list) source 19 val source': 'a -> 'b Scan.stopper -> ('a * 'b list -> 'c list * ('a * 'b list)) -> 20 ('b, 'e) source -> ('c, 'a * ('b, 'e) source) source 21 val source: 'a Scan.stopper -> ('a list -> 'b list * 'a list) -> 22 ('a, 'd) source -> ('b, ('a, 'd) source) source 23end; 24 25structure Source: SOURCE = 26struct 27 28 29(** datatype source **) 30 31datatype ('a, 'b) source = 32 Source of 33 {buffer: 'a list, 34 info: 'b, 35 drain: 'b -> 'a list * 'b}; 36 37fun make_source buffer info drain = 38 Source {buffer = buffer, info = info, drain = drain}; 39 40 41(* get / unget *) 42 43fun get (Source {buffer = [], info, drain}) = 44 let val (xs, info') = drain info 45 in (xs, make_source [] info' drain) end 46 | get (Source {buffer, info, drain}) = (buffer, make_source [] info drain); 47 48fun unget (xs, Source {buffer, info, drain}) = make_source (xs @ buffer) info drain; 49 50 51(* variations on get *) 52 53fun get_single src = 54 (case get src of 55 ([], _) => NONE 56 | (x :: xs, src') => SOME (x, unget (xs, src'))); 57 58fun exhaust src = 59 (case get src of 60 ([], _) => [] 61 | (xs, src') => xs @ exhaust src'); 62 63 64(* (map)filter *) 65 66fun drain_map_filter f src = 67 let 68 val (xs, src') = get src; 69 val xs' = map_filter f xs; 70 in 71 if null xs orelse not (null xs') then (xs', src') 72 else drain_map_filter f src' 73 end; 74 75fun map_filter f src = make_source [] src (drain_map_filter f); 76fun filter pred = map_filter (fn x => if pred x then SOME x else NONE); 77 78 79 80(** build sources **) 81 82(* list source *) 83 84fun of_list xs = make_source [] xs (fn xs => (xs, [])); 85 86val of_string = of_list o raw_explode; 87 88fun exhausted src = of_list (exhaust src); 89 90 91 92(** cascade sources **) 93 94(* state-based *) 95 96fun drain_source' stopper scan (state, src) = 97 let 98 val drain = Scan.drain get stopper; 99 val (xs, s) = get src; 100 val ((ys, (state', xs')), src') = 101 if null xs then (([], (state, [])), s) 102 else drain (Scan.error scan) ((state, xs), s); 103 in (ys, (state', unget (xs', src'))) end; 104 105fun source' init_state stopper scan src = 106 make_source [] (init_state, src) (drain_source' stopper scan); 107 108 109(* non state-based *) 110 111fun drain_source stopper scan = 112 Scan.unlift (drain_source' stopper (Scan.lift scan)); 113 114fun source stopper scan src = 115 make_source [] src (drain_source stopper scan); 116 117end; 118