author  wenzelm 
Mon, 16 Nov 1998 10:41:08 +0100  
changeset 5869  b279a84ac11c 
parent 5861  7536314d9a5f 
child 5987  389d03e6e093 
permissions  rwrr 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

1 
(* Title: Pure/Syntax/scan.ML 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

2 
ID: $Id$ 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

3 
Author: Markus Wenzel and Tobias Nipkow, TU Muenchen 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

4 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

5 
Generic scanners (for potentially infinite input). 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

6 
*) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

7 

4924  8 
infix 5  :   ^^; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

9 
infix 3 >>; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

10 
infix 0 ; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

11 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

12 
signature BASIC_SCAN = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

13 
sig 
4919  14 
val !! : ('a * string option > string) > ('a > 'b) > 'a > 'b 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

15 
val >> : ('a > 'b * 'c) * ('b > 'd) > 'a > 'd * 'c 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

16 
val  : ('a > 'b) * ('a > 'b) > 'a > 'b 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

17 
val  : ('a > 'b * 'c) * ('c > 'd * 'e) > 'a > ('b * 'd) * 'e 
4924  18 
val : : ('a > 'b * 'c) * ('b > 'c > 'd * 'e) > 'a > ('b * 'd) * 'e 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

19 
val  : ('a > 'b * 'c) * ('c > 'd * 'e) > 'a > 'd * 'e 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

20 
val  : ('a > 'b * 'c) * ('c > 'd * 'e) > 'a > 'b * 'e 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

21 
val ^^ : ('a > string * 'b) * ('b > string * 'c) > 'a > string * 'c 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

22 
val $$ : ''a > ''a list > ''a * ''a list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

23 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

24 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

25 
signature SCAN = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

26 
sig 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

27 
include BASIC_SCAN 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

28 
val fail: 'a > 'b 
4919  29 
val fail_with: ('a > string) > 'a > 'b 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

30 
val succeed: 'a > 'b > 'a * 'b 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

31 
val one: ('a > bool) > 'a list > 'a * 'a list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

32 
val any: ('a > bool) > 'a list > 'a list * 'a list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

33 
val any1: ('a > bool) > 'a list > 'a list * 'a list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

34 
val optional: ('a > 'b * 'a) > 'b > 'a > 'b * 'a 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

35 
val option: ('a > 'b * 'a) > 'a > 'b option * 'a 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

36 
val repeat: ('a > 'b * 'a) > 'a > 'b list * 'a 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

37 
val repeat1: ('a > 'b * 'a) > 'a > 'b list * 'a 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

38 
val max: ('a * 'a > bool) > ('b > 'a * 'b) > ('b > 'a * 'b) > 'b > 'a * 'b 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

39 
val ahead: ('a > 'b * 'c) > 'a > 'b * 'a 
5861  40 
val unless: ('a > 'b * 'a) > ('a > 'c * 'd) > 'a > 'c * 'd 
41 
val first: ('a > 'b) list > 'a > 'b 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

42 
val depend: ('a > 'b > ('c * 'd) * 'e) > 'a * 'b > 'd * ('c * 'e) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

43 
val lift: ('a > 'b * 'c) > 'd * 'a > 'b * ('d * 'c) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

44 
val pass: 'a > ('a * 'b > 'c * ('d * 'e)) > 'b > 'c * 'e 
4756  45 
val try: ('a > 'b) > 'a > 'b 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

46 
val force: ('a > 'b) > 'a > 'b 
4756  47 
val prompt: string > ('a > 'b) > 'a > 'b 
4937  48 
val finite': 'a * ('a > bool) > ('b * 'a list > 'c * ('d * 'a list)) 
49 
> 'b * 'a list > 'c * ('d * 'a list) 

50 
val finite: 'a * ('a > bool) > ('a list > 'b * 'a list) > 'a list > 'b * 'a list 

5869  51 
val read: 'a * ('a > bool) > ('a list > 'b * 'a list) > 'a list > 'b option 
4958  52 
val catch: ('a > 'b) > 'a > 'b 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

53 
val error: ('a > 'b) > 'a > 'b 
4958  54 
val source': string > (string > 'a > 'b list * 'a) > ('b list * 'a > 'c) > 
55 
'b * ('b > bool) > ('d * 'b list > 'e list * ('d * 'b list)) > 

56 
('d * 'b list > 'f * ('d * 'b list)) option > 'd * 'a > 'e list * ('d * 'c) 

57 
val source: string > (string > 'a > 'b list * 'a) > ('b list * 'a > 'c) > 

58 
'b * ('b > bool) > ('b list > 'd list * 'b list) > 

59 
('b list > 'e * 'b list) option > 'a > 'd list * 'c 

4937  60 
val single: ('a > 'b * 'a) > 'a > 'b list * 'a 
61 
val bulk: ('a > 'b * 'a) > 'a > 'b list * 'a 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

62 
type lexicon 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

63 
val dest_lexicon: lexicon > string list list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

64 
val make_lexicon: string list list > lexicon 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

65 
val empty_lexicon: lexicon 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

66 
val extend_lexicon: lexicon > string list list > lexicon 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

67 
val merge_lexicons: lexicon > lexicon > lexicon 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

68 
val literal: lexicon > string list > string list * string list 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

69 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

70 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

71 
structure Scan: SCAN = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

72 
struct 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

73 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

74 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

75 
(** scanners **) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

76 

4958  77 
exception MORE of string option; (*need more input (prompt)*) 
4919  78 
exception FAIL of string option; (*try alternatives (reason of failure)*) 
4756  79 
exception ABORT of string; (*dead end*) 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

80 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

81 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

82 
(* scanner combinators *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

83 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

84 
fun (scan >> f) xs = apfst f (scan xs); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

85 

4919  86 
fun (scan1  scan2) xs = scan1 xs handle FAIL _ => scan2 xs; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

87 

4937  88 
(*dependent pairing*) 
4924  89 
fun (scan1 : scan2) xs = 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

90 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

91 
val (x, ys) = scan1 xs; 
4924  92 
val (y, zs) = scan2 x ys; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

93 
in ((x, y), zs) end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

94 

4924  95 
fun (scan1  scan2) = scan1 : (fn _ => scan2); 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

96 
fun (scan1  scan2) = scan1  scan2 >> #2; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

97 
fun (scan1  scan2) = scan1  scan2 >> #1; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

98 
fun (scan1 ^^ scan2) = scan1  scan2 >> op ^; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

99 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

100 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

101 
(* generic scanners *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

102 

4919  103 
fun fail _ = raise FAIL None; 
104 
fun fail_with msg_of xs = raise FAIL (Some (msg_of xs)); 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

105 
fun succeed y xs = (y, xs); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

106 

4756  107 
fun one _ [] = raise MORE None 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

108 
 one pred (x :: xs) = 
4919  109 
if pred x then (x, xs) else raise FAIL None; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

110 

4756  111 
fun $$ _ [] = raise MORE None 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

112 
 $$ a (x :: xs) = 
4919  113 
if a = x then (x, xs) else raise FAIL None; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

114 

4756  115 
fun any _ [] = raise MORE None 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

116 
 any pred (lst as x :: xs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

117 
if pred x then apfst (cons x) (any pred xs) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

118 
else ([], lst); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

119 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

120 
fun any1 pred = one pred  any pred >> op ::; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

121 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

122 
fun optional scan def = scan  succeed def; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

123 
fun option scan = optional (scan >> Some) None; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

124 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

125 
fun repeat scan xs = (scan  repeat scan >> op ::  succeed []) xs; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

126 
fun repeat1 scan = scan  repeat scan >> op ::; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

127 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

128 
fun max leq scan1 scan2 xs = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

129 
(case (option scan1 xs, option scan2 xs) of 
4919  130 
((None, _), (None, _)) => raise FAIL None (*looses FAIL msg!*) 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

131 
 ((Some tok1, xs'), (None, _)) => (tok1, xs') 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

132 
 ((None, _), (Some tok2, xs')) => (tok2, xs') 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

133 
 ((Some tok1, xs1'), (Some tok2, xs2')) => 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

134 
if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2')); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

135 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

136 
fun ahead scan xs = (fst (scan xs), xs); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

137 

5861  138 
fun unless test scan = 
139 
ahead (option test) : (fn None => scan  _ => fail) >> #2; 

140 

141 
fun first [] = fail 

142 
 first (scan :: scans) = scan  first scans; 

143 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

144 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

145 
(* state based scanners *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

146 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

147 
fun depend scan (st, xs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

148 
let val ((st', y), xs') = scan st xs 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

149 
in (y, (st', xs')) end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

150 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

151 
fun lift scan (st, xs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

152 
let val (y, xs') = scan xs 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

153 
in (y, (st, xs')) end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

154 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

155 
fun pass st scan xs = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

156 
let val (y, (_, xs')) = scan (st, xs) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

157 
in (y, xs') end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

158 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

159 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

160 
(* exception handling *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

161 

4919  162 
fun !! err scan xs = scan xs handle FAIL msg => raise ABORT (err (xs, msg)); 
163 
fun try scan xs = scan xs handle MORE _ => raise FAIL None  ABORT _ => raise FAIL None; 

164 
fun force scan xs = scan xs handle MORE _ => raise FAIL None; 

4756  165 
fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str); 
4958  166 
fun catch scan xs = scan xs handle ABORT msg => raise FAIL (Some msg); 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

167 
fun error scan xs = scan xs handle ABORT msg => Library.error msg; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

168 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

169 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

170 
(* finite scans *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

171 

4937  172 
fun finite' (stopper, is_stopper) scan (state, input) = 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

173 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

174 
fun lost () = raise ABORT "Scanner bug: lost stopper of finite scan!"; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

175 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

176 
fun stop [] = lost () 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

177 
 stop lst = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

178 
let val (xs, x) = split_last lst 
4937  179 
in if is_stopper x then ((), xs) else lost () end; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

180 
in 
4937  181 
if exists is_stopper input then 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

182 
raise ABORT "Stopper may not occur in input of finite scan!" 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

183 
else (force scan  lift stop) (state, input @ [stopper]) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

184 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

185 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

186 
fun finite stopper scan xs = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

187 
let val (y, ((), xs')) = finite' stopper (lift scan) ((), xs) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

188 
in (y, xs') end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

189 

5869  190 
fun read stopper scan xs = 
191 
(case error (finite stopper (option scan)) xs of 

192 
(y as Some _, []) => y 

193 
 _ => None); 

194 

195 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

196 

4903  197 
(* infinite scans  draining statebased source *) 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

198 

4958  199 
fun drain def_prmpt get stopper scan ((state, xs), src) = 
200 
(scan (state, xs), src) handle MORE prmpt => 

201 
(case get (if_none prmpt def_prmpt) src of 

202 
([], _) => (finite' stopper scan (state, xs), src) 

203 
 (xs', src') => drain def_prmpt get stopper scan ((state, xs @ xs'), src')); 

204 

205 
fun source' def_prmpt get unget stopper scanner opt_recover (state, src) = 

4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

206 
let 
4968  207 
fun drain_with scan = drain def_prmpt get stopper scan; 
4958  208 

209 
fun drain_loop recover inp = 

210 
drain_with (catch scanner) inp handle FAIL msg => 

5048  211 
(error_msg (if_none msg "Syntax error."); error_msg "Trying to recover ..."; 
4958  212 
drain_loop recover (apfst snd (drain_with recover inp))); 
4937  213 

4958  214 
val ((ys, (state', xs')), src') = 
215 
(case (get def_prmpt src, opt_recover) of 

216 
(([], s), _) => (([], (state, [])), s) 

217 
 ((xs, s), None) => drain_with (error scanner) ((state, xs), s) 

218 
 ((xs, s), Some scan) => drain_loop scan ((state, xs), s)); 

4937  219 
in 
4958  220 
(ys, (state', unget (xs', src'))) 
4937  221 
end; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

222 

4958  223 
fun source def_prmpt get unget stopper scan opt_recover src = 
224 
let val (ys, ((), src')) = 

225 
source' def_prmpt get unget stopper (lift scan) (apsome lift opt_recover) ((), src) 

4953  226 
in (ys, src') end; 
227 

4756  228 
fun single scan = scan >> (fn x => [x]); 
4937  229 
fun bulk scan = scan  repeat (try scan) >> (op ::); 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

230 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

231 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

232 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

233 
(** datatype lexicon **) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

234 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

235 
datatype lexicon = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

236 
Empty  
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

237 
Branch of string * string list * lexicon * lexicon * lexicon; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

238 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

239 
val no_literal = []; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

240 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

241 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

242 
(* dest_lexicon *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

243 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

244 
fun dest_lexicon Empty = [] 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

245 
 dest_lexicon (Branch (_, [], lt, eq, gt)) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

246 
dest_lexicon lt @ dest_lexicon eq @ dest_lexicon gt 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

247 
 dest_lexicon (Branch (_, cs, lt, eq, gt)) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

248 
dest_lexicon lt @ [cs] @ dest_lexicon eq @ dest_lexicon gt; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

249 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

250 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

251 
(* empty, extend, make, merge lexicons *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

252 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

253 
val empty_lexicon = Empty; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

254 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

255 
fun extend_lexicon lexicon chrss = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

256 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

257 
fun ext (lex, chrs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

258 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

259 
fun add (Branch (d, a, lt, eq, gt)) (chs as c :: cs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

260 
if c < d then Branch (d, a, add lt chs, eq, gt) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

261 
else if c > d then Branch (d, a, lt, eq, add gt chs) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

262 
else Branch (d, if null cs then chrs else a, lt, add eq cs, gt) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

263 
 add Empty [c] = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

264 
Branch (c, chrs, Empty, Empty, Empty) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

265 
 add Empty (c :: cs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

266 
Branch (c, no_literal, Empty, add Empty cs, Empty) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

267 
 add lex [] = lex; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

268 
in add lex chrs end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

269 
in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

270 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

271 
val make_lexicon = extend_lexicon empty_lexicon; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

272 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

273 
fun merge_lexicons lex1 lex2 = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

274 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

275 
val chss1 = dest_lexicon lex1; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

276 
val chss2 = dest_lexicon lex2; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

277 
in 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

278 
if chss2 subset chss1 then lex1 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

279 
else if chss1 subset chss2 then lex2 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

280 
else extend_lexicon lex1 chss2 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

281 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

282 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

283 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

284 
(* scan literal *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

285 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

286 
fun literal lex chrs = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

287 
let 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

288 
fun lit Empty res _ = res 
4756  289 
 lit (Branch _) _ [] = raise MORE None 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

290 
 lit (Branch (d, a, lt, eq, gt)) res (chs as c :: cs) = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

291 
if c < d then lit lt res chs 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

292 
else if c > d then lit gt res chs 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

293 
else lit eq (if a = no_literal then res else Some (a, cs)) cs; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

294 
in 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

295 
(case lit lex None chrs of 
4919  296 
None => raise FAIL None 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

297 
 Some res => res) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

298 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

299 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

300 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

301 
end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

302 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

303 

ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

304 
structure BasicScan: BASIC_SCAN = Scan; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

305 
open BasicScan; 