author  wenzelm 
Wed, 13 May 1998 12:20:28 +0200  
changeset 4919  9397b1446cdb 
parent 4903  0f56199a8d97 
child 4924  cf6bb75968c4 
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 

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

8 
infix 5    ^^; 
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 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

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

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

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

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

23 

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

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

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

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

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

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

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

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

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

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

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

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

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

37 
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

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

39 
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

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

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

43 
val force: ('a > 'b) > 'a > 'b 
4756  44 
val prompt: string > ('a > 'b) > 'a > 'b 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

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

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

48 
val error: ('a > 'b) > 'a > 'b 
4903  49 
val source: string > (string > 'a > 'b list * 'a) > 
50 
('c * 'a > 'd) > ('e * 'b list > 'f * ('g * 'c)) > 'e * 'a > 'f * ('g * 'd) 

51 
val bulk: bool > ('a > 'b * 'a) > 'a > 'b list * 'a 

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

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

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

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

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

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

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

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

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

60 

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

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

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

63 

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

64 

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

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

66 

4756  67 
exception MORE of string option; (*need more input (use prompt)*) 
4919  68 
exception FAIL of string option; (*try alternatives (reason of failure)*) 
4756  69 
exception ABORT of string; (*dead end*) 
4702
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 

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

72 
(* scanner combinators *) 
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 
fun (scan >> f) xs = apfst f (scan xs); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

75 

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

77 

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

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

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

80 
val (x, ys) = scan1 xs; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

81 
val (y, zs) = scan2 ys; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

82 
in ((x, y), zs) end; 
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 (scan1  scan2) = scan1  scan2 >> #2; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

86 

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

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

88 

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

89 

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

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

91 

4919  92 
fun fail _ = raise FAIL None; 
93 
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

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

95 

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

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

99 

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

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

103 

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

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

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

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

108 

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

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

110 

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

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

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

113 

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

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

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

116 

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

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

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

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

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

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

123 
if leq (tok2, tok1) then (tok1, xs1') else (tok2, xs2')); 
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 ahead scan xs = (fst (scan xs), xs); 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

126 

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 
(* state based scanners *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

129 

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

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

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

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

133 

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

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

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

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

137 

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

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

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

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

141 

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

142 

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

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

144 

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

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

4756  148 
fun prompt str scan xs = scan xs handle MORE None => raise MORE (Some str); 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

149 
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

150 

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

151 

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

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

153 

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

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

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

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

157 

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

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

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

160 
let val (xs, x) = split_last lst 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

161 
in if x = stopper then ((), xs) else lost () end; 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

163 
if exists (equal stopper) input then 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

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

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

167 

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

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

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

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

171 

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

172 

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

174 

4903  175 
fun source def_prmpt get unget scan (state, src) = 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

177 
fun drain (xs, s) = 
4903  178 
(scan (state, xs), s) 
4756  179 
handle MORE prmpt => 
4903  180 
let val (xs', s') = get (if_none prmpt def_prmpt) s in 
181 
if null xs' then raise ABORT "Input source exhausted" 

182 
else drain (xs @ xs', s') 

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

183 
end; 
4903  184 
val ((ys, (state', rest)), src') = drain (get def_prmpt src); 
185 
in (ys, (state', unget (rest, src'))) end; 

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

186 

4756  187 
fun single scan = scan >> (fn x => [x]); 
188 
fun many scan = scan  repeat (try scan) >> (op ::); 

4903  189 
fun bulk do_many = if do_many then many else single; 
4702
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

190 

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

191 

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

192 

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

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

194 

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

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

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

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

198 

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

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

200 

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

201 

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

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

203 

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

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

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

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

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

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

209 

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

210 

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

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

212 

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

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

214 

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

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

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

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

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

219 
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

220 
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

221 
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

222 
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

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

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

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

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

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

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

229 
in foldl ext (lexicon, chrss \\ dest_lexicon lexicon) end; 
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 
val make_lexicon = extend_lexicon empty_lexicon; 
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 
fun merge_lexicons lex1 lex2 = 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

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

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

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

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

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

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

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

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

242 

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 
(* scan literal *) 
ffbaf431665d
Generic scanners (for potentially infinite input)  replaces Scanner;
wenzelm
parents:
diff
changeset

245 

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

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

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

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

250 
 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

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

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

253 
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

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

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

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

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

259 

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

260 

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

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

262 

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

263 

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

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

265 
open BasicScan; 