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