1.1 --- a/src/Pure/Syntax/parser.ML Fri Feb 11 18:51:00 2005 +0100
1.2 +++ b/src/Pure/Syntax/parser.ML Sun Feb 13 17:15:14 2005 +0100
1.3 @@ -63,7 +63,7 @@
1.4
1.5 (* convert productions to grammar;
1.6 N.B. that the chains parameter has the form [(from, [to])];
1.7 - prod_count is of type "int option" and is only updated if it is <> None*)
1.8 + prod_count is of type "int option" and is only updated if it is <> NONE*)
1.9 fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count)
1.10 | add_prods prods chains lambdas prod_count
1.11 ((lhs, new_prod as (rhs, name, pri)) :: ps) =
1.12 @@ -73,13 +73,13 @@
1.13 let (*store chain if it does not already exist*)
1.14 fun store_chain from =
1.15 let val old_tos = assocs chains from;
1.16 - in if lhs mem old_tos then (None, chains)
1.17 - else (Some from, overwrite (chains, (from, lhs ins old_tos)))
1.18 + in if lhs mem old_tos then (NONE, chains)
1.19 + else (SOME from, overwrite (chains, (from, lhs ins old_tos)))
1.20 end;
1.21 in if pri = ~1 then
1.22 case rhs of [Nonterminal (id, ~1)] => store_chain id
1.23 - | _ => (None, chains)
1.24 - else (None, chains)
1.25 + | _ => (NONE, chains)
1.26 + else (NONE, chains)
1.27 end;
1.28
1.29 (*propagate new chain in lookahead and lambda lists;
1.30 @@ -118,12 +118,12 @@
1.31
1.32 (*list optional terminal and all nonterminals on which the lookahead
1.33 of a production depends*)
1.34 - fun lookahead_dependency _ [] nts = (None, nts)
1.35 - | lookahead_dependency _ ((Terminal tk) :: _) nts = (Some tk, nts)
1.36 + fun lookahead_dependency _ [] nts = (NONE, nts)
1.37 + | lookahead_dependency _ ((Terminal tk) :: _) nts = (SOME tk, nts)
1.38 | lookahead_dependency lambdas ((Nonterminal (nt, _)) :: symbs) nts =
1.39 if nt mem lambdas then
1.40 lookahead_dependency lambdas symbs (nt :: nts)
1.41 - else (None, nt :: nts);
1.42 + else (NONE, nt :: nts);
1.43
1.44 (*get all known starting tokens for a nonterminal*)
1.45 fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
1.46 @@ -170,8 +170,8 @@
1.47 end;
1.48
1.49 val nt_prods' =
1.50 - let val new_opt_tks = map Some new_tks;
1.51 - in copy ((if new_lambda then [None] else []) @
1.52 + let val new_opt_tks = map SOME new_tks;
1.53 + in copy ((if new_lambda then [NONE] else []) @
1.54 new_opt_tks) nt_prods
1.55 end;
1.56 in examine_prods ps (add_lambda orelse new_lambda)
1.57 @@ -193,7 +193,7 @@
1.58 (*existing productions whose lookahead may depend on l*)
1.59 val tk_prods =
1.60 assocs nt_prods
1.61 - (Some (hd l_starts handle LIST _ => UnknownStart));
1.62 + (SOME (hd l_starts handle LIST _ => UnknownStart));
1.63
1.64 (*add_lambda is true if an existing production of the nt
1.65 produces lambda due to the new lambda NT l*)
1.66 @@ -242,9 +242,9 @@
1.67 (if is_some start_tk then [the start_tk] else [],
1.68 map starts_for_nt start_nts);
1.69
1.70 - val opt_starts = (if new_lambda then [None]
1.71 - else if null start_tks then [Some UnknownStart]
1.72 - else []) @ (map Some start_tks);
1.73 + val opt_starts = (if new_lambda then [NONE]
1.74 + else if null start_tks then [SOME UnknownStart]
1.75 + else []) @ (map SOME start_tks);
1.76
1.77 (*add lhs NT to list of dependent NTs in lookahead*)
1.78 fun add_nts [] = ()
1.79 @@ -271,7 +271,7 @@
1.80 | store (tk :: tks) prods is_new =
1.81 let val tk_prods = assocs prods tk;
1.82
1.83 - (*if prod_count = None then we can assume that
1.84 + (*if prod_count = NONE then we can assume that
1.85 grammar does not contain new production already*)
1.86 val (tk_prods', is_new') =
1.87 if is_some prod_count then
1.88 @@ -309,11 +309,11 @@
1.89 val key =
1.90 case find_first (fn t => not (t mem new_tks))
1.91 (starts_for_nt changed_nt) of
1.92 - None => Some UnknownStart
1.93 + NONE => SOME UnknownStart
1.94 | t => t;
1.95
1.96 (*copy productions whose lookahead depends on changed_nt;
1.97 - if key = Some UnknownToken then tk_prods is used to hold
1.98 + if key = SOME UnknownToken then tk_prods is used to hold
1.99 the productions not copied*)
1.100 fun update_prods [] result = result
1.101 | update_prods ((p as (rhs, _, _)) :: ps)
1.102 @@ -335,7 +335,7 @@
1.103 fun copy [] nt_prods = nt_prods
1.104 | copy (tk :: tks) nt_prods =
1.105 let
1.106 - val tk_prods = assocs nt_prods (Some tk);
1.107 + val tk_prods = assocs nt_prods (SOME tk);
1.108
1.109 val tk_prods' =
1.110 if not lambda then p :: tk_prods
1.111 @@ -343,12 +343,12 @@
1.112 (*if production depends on lambda NT we
1.113 have to look for duplicates*)
1.114 in copy tks
1.115 - (overwrite (nt_prods, (Some tk, tk_prods')))
1.116 + (overwrite (nt_prods, (SOME tk, tk_prods')))
1.117 end;
1.118 val result =
1.119 if update then
1.120 (tk_prods, copy new_tks nt_prods)
1.121 - else if key = Some UnknownStart then
1.122 + else if key = SOME UnknownStart then
1.123 (p :: tk_prods, nt_prods)
1.124 else (tk_prods, nt_prods);
1.125 in update_prods ps result end;
1.126 @@ -367,7 +367,7 @@
1.127 update_prods tk_prods ([], nt_prods);
1.128
1.129 val nt_prods' =
1.130 - if key = Some UnknownStart then
1.131 + if key = SOME UnknownStart then
1.132 overwrite (nt_prods', (key, tk_prods'))
1.133 else nt_prods';
1.134
1.135 @@ -449,8 +449,8 @@
1.136 (*Get tag for existing nonterminal or create a new one*)
1.137 fun get_tag nt_count tags nt =
1.138 case Symtab.lookup (tags, nt) of
1.139 - Some tag => (nt_count, tags, tag)
1.140 - | None => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
1.141 + SOME tag => (nt_count, tags, tag)
1.142 + | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
1.143 nt_count);
1.144
1.145 (*Convert symbols to the form used by the parser;
1.146 @@ -463,10 +463,10 @@
1.147 let
1.148 val (nt_count', tags', new_symb) =
1.149 case predef_term s of
1.150 - None =>
1.151 + NONE =>
1.152 let val (nt_count', tags', s_tag) = get_tag nt_count tags s;
1.153 in (nt_count', tags', Nonterminal (s_tag, p)) end
1.154 - | Some tk => (nt_count, tags, Terminal tk);
1.155 + | SOME tk => (nt_count, tags, Terminal tk);
1.156 in symb_of ss nt_count' tags' (new_symb :: result) end
1.157 | symb_of (_ :: ss) nt_count tags result =
1.158 symb_of ss nt_count tags result;
1.159 @@ -499,7 +499,7 @@
1.160
1.161 (*Add new productions to old ones*)
1.162 val (fromto_chains', lambdas', _) =
1.163 - add_prods prods' fromto_chains lambdas None xprods';
1.164 + add_prods prods' fromto_chains lambdas NONE xprods';
1.165
1.166 val chains' = inverse_chains fromto_chains' [];
1.167 in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
1.168 @@ -524,8 +524,8 @@
1.169 (*get existing tag from grammar1 or create a new one*)
1.170 fun get_tag nt_count tags nt =
1.171 case Symtab.lookup (tags, nt) of
1.172 - Some tag => (nt_count, tags, tag)
1.173 - | None => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
1.174 + SOME tag => (nt_count, tags, tag)
1.175 + | NONE => (nt_count+1, Symtab.update_new ((nt, nt_count), tags),
1.176 nt_count)
1.177
1.178 val ((nt_count1', tags1'), tag_table) =
1.179 @@ -591,8 +591,8 @@
1.180
1.181 val fromto_chains = inverse_chains chains1 [];
1.182
1.183 - val (fromto_chains', lambdas', Some prod_count1') =
1.184 - add_prods prods1' fromto_chains lambdas1 (Some prod_count1) raw_prods;
1.185 + val (fromto_chains', lambdas', SOME prod_count1') =
1.186 + add_prods prods1' fromto_chains lambdas1 (SOME prod_count1) raw_prods;
1.187
1.188 val chains' = inverse_chains fromto_chains' [];
1.189 in Gram {nt_count = nt_count1', prod_count = prod_count1',
1.190 @@ -629,10 +629,10 @@
1.191
1.192 (*Add parse tree to list and eliminate duplicates
1.193 saving the maximum precedence*)
1.194 -fun conc (t, prec:int) [] = (None, [(t, prec)])
1.195 +fun conc (t, prec:int) [] = (NONE, [(t, prec)])
1.196 | conc (t, prec) ((t', prec') :: ts) =
1.197 if t = t' then
1.198 - (Some prec', if prec' >= prec then (t', prec') :: ts
1.199 + (SOME prec', if prec' >= prec then (t', prec') :: ts
1.200 else (t, prec) :: ts)
1.201 else
1.202 let val (n, ts') = conc (t, prec) ts
1.203 @@ -697,7 +697,7 @@
1.204 (*get all productions of a NT and NTs chained to it which can
1.205 be started by specified token*)
1.206 fun prods_for prods chains include_none tk nts =
1.207 -let (*similar to token_assoc but does not automatically include 'None' key*)
1.208 +let (*similar to token_assoc but does not automatically include 'NONE' key*)
1.209 fun token_assoc2 (list, key) =
1.210 let fun assoc [] result = result
1.211 | assoc ((keyi, pi) :: pairs) result =
1.212 @@ -725,7 +725,7 @@
1.213 let (*predictor operation*)
1.214 val (used', new_states) =
1.215 (case assoc (used, nt) of
1.216 - Some (usedPrec, l) => (*nonterminal has been processed*)
1.217 + SOME (usedPrec, l) => (*nonterminal has been processed*)
1.218 if usedPrec <= minPrec then
1.219 (*wanted precedence has been processed*)
1.220 (used, movedot_lambda S l)
1.221 @@ -739,7 +739,7 @@
1.222 movedot_lambda S l @ States')
1.223 end
1.224
1.225 - | None => (*nonterminal is parsed for the first time*)
1.226 + | NONE => (*nonterminal is parsed for the first time*)
1.227 let val tk_prods = all_prods_for nt;
1.228 val States' = mkStates i minPrec nt
1.229 (getRHS minPrec tk_prods);
1.230 @@ -766,11 +766,11 @@
1.231 val (used', O) = update_trees used (A, (tt, prec));
1.232 in
1.233 case O of
1.234 - None =>
1.235 + NONE =>
1.236 let val Slist = getS A prec Si;
1.237 val States' = map (movedot_nonterm tt) Slist;
1.238 in processS used' (States' @ States) (S :: Si, Sii) end
1.239 - | Some n =>
1.240 + | SOME n =>
1.241 if n >= prec then processS used' States (S :: Si, Sii)
1.242 else
1.243 let val Slist = getS' A prec n Si;
1.244 @@ -825,12 +825,12 @@
1.245 fun get_starts [] result = result
1.246 | get_starts ((nt, minPrec:int) :: nts) result =
1.247 let fun get [] result = result
1.248 - | get ((Some tk, prods) :: ps) result =
1.249 + | get ((SOME tk, prods) :: ps) result =
1.250 if not (null prods) andalso
1.251 exists (reduction tk minPrec [nt]) prods
1.252 then get ps (tk :: result)
1.253 else get ps result
1.254 - | get ((None, _) :: ps) result = get ps result;
1.255 + | get ((NONE, _) :: ps) result = get ps result;
1.256
1.257 val (_, nt_prods) = Array.sub (prods, nt);
1.258
1.259 @@ -842,12 +842,12 @@
1.260
1.261 val nts =
1.262 mapfilter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
1.263 - Some (a, prec) | _ => None)
1.264 + SOME (a, prec) | _ => NONE)
1.265 (Array.sub (stateset, i-1));
1.266 val allowed =
1.267 distinct (get_starts nts [] @
1.268 - (mapfilter (fn (_, _, _, Terminal a :: _, _, _) => Some a
1.269 - | _ => None)
1.270 + (mapfilter (fn (_, _, _, Terminal a :: _, _, _) => SOME a
1.271 + | _ => NONE)
1.272 (Array.sub (stateset, i-1))));
1.273 in syntax_error (if prev_token = EndToken then indata
1.274 else prev_token :: indata) allowed
1.275 @@ -863,14 +863,14 @@
1.276 end));
1.277
1.278
1.279 -fun get_trees l = mapfilter (fn (_, _, [pt], _, _, _) => Some pt | _ => None)
1.280 +fun get_trees l = mapfilter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
1.281 l;
1.282
1.283 fun earley prods tags chains startsymbol indata =
1.284 let
1.285 val start_tag = case Symtab.lookup (tags, startsymbol) of
1.286 - Some tag => tag
1.287 - | None => error ("parse: Unknown startsymbol " ^
1.288 + SOME tag => tag
1.289 + | NONE => error ("parse: Unknown startsymbol " ^
1.290 quote startsymbol);
1.291 val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal EndToken],
1.292 "", 0)];