author  wenzelm 
Mon, 09 Nov 1998 15:42:08 +0100  
changeset 5840  e2d2b896c717 
parent 5019  b6363fa0564f 
child 5943  576a7f5e5e39 
permissions  rwrr 
4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

1 
(* Title: Pure/Syntax/source.ML 
4939  2 
ID: $Id$ 
3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
Coalgebraic data sources. 

6 
*) 

7 

8 
signature SOURCE = 

9 
sig 

10 
type ('a, 'b) source 

4946  11 
val set_prompt: string > ('a, 'b) source > ('a, 'b) source 
12 
val get: ('a, 'b) source > 'a list * ('a, 'b) source 

4939  13 
val unget: 'a list * ('a, 'b) source > ('a, 'b) source 
4983
2c567fcdb36d
changed get_single: ('a, 'b) source > ('a * ('a, 'b) source) option;
wenzelm
parents:
4976
diff
changeset

14 
val get_single: ('a, 'b) source > ('a * ('a, 'b) source) option 
4946  15 
val exhaust: ('a, 'b) source > 'a list 
4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

16 
val mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c) source) source 
4939  17 
val filter: ('a > bool) > ('a, 'b) source > ('a, ('a, 'b) source) source 
4946  18 
val of_list: 'a list > ('a, 'a list) source 
19 
val of_string: string > (string, string list) source 

5019  20 
val of_file: string > (string, string list) source 
4939  21 
val of_stream: TextIO.instream > TextIO.outstream > (string, unit) source 
22 
val tty: (string, unit) source 

4960  23 
val source': 'a > 'b * ('b > bool) > ('a * 'b list > 'c list * ('a * 'b list)) > 
24 
('a * 'b list > 'd * ('a * 'b list)) option > 

25 
('b, 'e) source > ('c, 'a * ('b, 'e) source) source 

26 
val source: 'a * ('a > bool) > ('a list > 'b list * 'a list) > 

27 
('a list > 'c * 'a list) option > 

28 
('a, 'd) source > ('b, ('a, 'd) source) source 

4939  29 
end; 
30 

31 
structure Source: SOURCE = 

32 
struct 

33 

34 

35 
(** datatype source **) 

36 

37 
datatype ('a, 'b) source = 

38 
Source of 

39 
{buffer: 'a list, 

40 
info: 'b, 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

41 
prompt: string, 
4939  42 
drain: string > 'b > 'a list * 'b}; 
43 

4946  44 
fun make_source buffer info prompt drain = 
45 
Source {buffer = buffer, info = info, prompt = prompt, drain = drain}; 

46 

47 

48 
(* prompt *) 

49 

50 
val default_prompt = "> "; 

51 

52 
fun set_prompt prompt (Source {buffer, info, prompt = _, drain}) = 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

53 
make_source buffer info prompt drain; 
4939  54 

55 

56 
(* get / unget *) 

57 

4946  58 
fun get (Source {buffer = [], info, prompt, drain}) = 
4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

59 
let val (xs, info') = drain prompt info 
4946  60 
in (xs, make_source [] info' prompt drain) end 
61 
 get (Source {buffer, info, prompt, drain}) = 

62 
(buffer, make_source [] info prompt drain); 

4939  63 

4946  64 
fun unget (xs, Source {buffer, info, prompt, drain}) = 
65 
make_source (xs @ buffer) info prompt drain; 

4939  66 

67 

4946  68 
(* variations on get *) 
69 

70 
fun get_prompt prompt src = get (set_prompt prompt src); 

71 

72 
fun get_single src = 

73 
(case get src of 

4983
2c567fcdb36d
changed get_single: ('a, 'b) source > ('a * ('a, 'b) source) option;
wenzelm
parents:
4976
diff
changeset

74 
([], _) => None 
2c567fcdb36d
changed get_single: ('a, 'b) source > ('a * ('a, 'b) source) option;
wenzelm
parents:
4976
diff
changeset

75 
 (x :: xs, src') => Some (x, unget (xs, src'))); 
4939  76 

4946  77 
fun exhaust src = 
78 
(case get src of 

4939  79 
([], _) => [] 
4946  80 
 (xs, src') => xs @ exhaust src'); 
4939  81 

82 

4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

83 
(* (map)filter *) 
4939  84 

4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

85 
fun drain_mapfilter f prompt src = 
4939  86 
let 
4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

87 
val (xs, src') = get_prompt prompt src; 
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

88 
val xs' = Library.mapfilter f xs; 
4939  89 
in 
4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

90 
if null xs orelse not (null xs') then (xs', src') 
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

91 
else drain_mapfilter f prompt src' 
4939  92 
end; 
93 

4976
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

94 
fun mapfilter f src = make_source [] src default_prompt (drain_mapfilter f); 
19f48dafe5d3
added mapfilter: ('a > 'b option) > ('a, 'c) source > ('b, ('a, 'c)
wenzelm
parents:
4960
diff
changeset

95 
fun filter pred = mapfilter (fn x => if pred x then Some x else None); 
4939  96 

97 

98 

99 
(** build sources **) 

100 

101 
(* list source *) 

102 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

103 
(*limiting the input buffer considerably improves performance*) 
4946  104 
val limit = 4000; 
4939  105 

4946  106 
fun drain_list _ xs = (take (limit, xs), drop (limit, xs)); 
4939  107 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

108 
fun of_list xs = make_source [] xs default_prompt drain_list; 
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

109 
val of_string = of_list o explode; 
5019  110 
val of_file = of_string o File.read; 
4939  111 

112 

113 
(* stream source *) 

114 

115 
fun drain_stream instream outstream prompt () = 

116 
(TextIO.output (outstream, prompt); 

117 
TextIO.flushOut outstream; 

118 
(explode (TextIO.inputLine instream), ())); 

119 

120 
fun of_stream instream outstream = 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

121 
make_source [] () default_prompt (drain_stream instream outstream); 
4939  122 

123 
val tty = of_stream TextIO.stdIn TextIO.stdOut; 

124 

125 

126 

127 
(** compose sources **) 

128 

4960  129 
fun drain_source source stopper scan recover prompt src = 
130 
source prompt get_prompt unget stopper scan recover src; 

4939  131 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

132 

cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

133 
(* statebased *) 
4939  134 

4960  135 
fun source' init_state stopper scan recover src = 
136 
make_source [] (init_state, src) default_prompt 

137 
(drain_source Scan.source' stopper scan recover); 

4939  138 

139 

4954
cf1404c3f7bb
changed get_single: ('a, 'b) source > 'a option * ('a, 'b) source;
wenzelm
parents:
4946
diff
changeset

140 
(* non statebased *) 
4939  141 

4960  142 
fun source stopper scan recover src = 
143 
make_source [] src default_prompt 

144 
(drain_source Scan.source stopper scan recover); 

4939  145 

146 

147 
end; 