diff -r 1b3115d1a8df -r 8d8c70b41bab src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Thu Mar 03 09:22:35 2005 +0100 +++ b/src/Pure/Syntax/parser.ML Thu Mar 03 12:43:01 2005 +0100 @@ -88,7 +88,7 @@ val (added_starts, lambdas') = if is_none new_chain then ([], lambdas) else let (*lookahead of chain's source*) - val ((from_nts, from_tks), _) = Array.sub (prods, the new_chain); + val ((from_nts, from_tks), _) = Array.sub (prods, valOf new_chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead [] added = added @@ -152,8 +152,8 @@ let val new_lambda = is_none tk andalso nts subset lambdas; - val new_tks = (if is_some tk then [the tk] else []) @ - foldl token_union ([], map starts_for_nt nts) \\ + val new_tks = (if isSome tk then [valOf tk] else []) @ + Library.foldl token_union ([], map starts_for_nt nts) \\ l_starts; val added_tks' = token_union (new_tks, added_tks); @@ -193,7 +193,7 @@ (*existing productions whose lookahead may depend on l*) val tk_prods = assocs nt_prods - (SOME (hd l_starts handle LIST _ => UnknownStart)); + (SOME (hd l_starts handle Empty => UnknownStart)); (*add_lambda is true if an existing production of the nt produces lambda due to the new lambda NT l*) @@ -231,15 +231,15 @@ (*insert production into grammar*) val (added_starts', prod_count') = - if is_some new_chain then (added_starts', prod_count) + if isSome new_chain then (added_starts', prod_count) (*don't store chain production*) else let (*lookahead tokens of new production and on which NTs lookahead depends*) val (start_tk, start_nts) = lookahead_dependency lambdas' rhs []; - val start_tks = foldl token_union - (if is_some start_tk then [the start_tk] else [], + val start_tks = Library.foldl token_union + (if isSome start_tk then [valOf start_tk] else [], map starts_for_nt start_nts); val opt_starts = (if new_lambda then [NONE] @@ -265,8 +265,8 @@ (*store new production*) fun store [] prods is_new = - (prods, if is_some prod_count andalso is_new then - apsome (fn x => x+1) prod_count + (prods, if isSome prod_count andalso is_new then + Option.map (fn x => x+1) prod_count else prod_count, is_new) | store (tk :: tks) prods is_new = let val tk_prods = assocs prods tk; @@ -274,7 +274,7 @@ (*if prod_count = NONE then we can assume that grammar does not contain new production already*) val (tk_prods', is_new') = - if is_some prod_count then + if isSome prod_count then if new_prod mem tk_prods then (tk_prods, false) else (new_prod :: tk_prods, true) else (new_prod :: tk_prods, true); @@ -328,8 +328,8 @@ (*test if production could already be associated with a member of new_tks*) val lambda = length depends > 1 orelse - not (null depends) andalso is_some tk - andalso the tk mem new_tks; + not (null depends) andalso isSome tk + andalso valOf tk mem new_tks; (*associate production with new starting tokens*) fun copy [] nt_prods = nt_prods @@ -399,7 +399,7 @@ fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s) | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok) | pretty_symb (Nonterminal (tag, p)) = - let val name = fst (the (find_first (fn (n, t) => t = tag) taglist)); + let val name = fst (valOf (find_first (fn (n, t) => t = tag) taglist)); in Pretty.str (name ^ "[" ^ string_of_int p ^ "]") end; fun pretty_const "" = [] @@ -416,11 +416,11 @@ fun prod_of_chain from = ([Nonterminal (from, ~1)], "", ~1); val nt_prods = - foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @ + Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @ map prod_of_chain (assocs chains tag); in map (pretty_prod name) nt_prods end; - in flat (map pretty_nt taglist) end; + in List.concat (map pretty_nt taglist) end; (** Operations on gramars **) @@ -537,7 +537,7 @@ | store_tag nt_count tags tag = let val (nt_count', tags', tag') = get_tag nt_count tags - (fst (the (find_first (fn (n, t) => t = tag) tag_list))); + (fst (valOf (find_first (fn (n, t) => t = tag) tag_list))); in Array.update (table, tag, tag'); store_tag nt_count' tags' (tag-1) end; @@ -563,7 +563,7 @@ fun process_nt ~1 result = result | process_nt nt result = let - val nt_prods = foldl (op union) + val nt_prods = Library.foldl (op union) ([], map snd (snd (Array.sub (prods2, nt)))); val lhs_tag = convert_tag nt; @@ -616,11 +616,11 @@ (*Get all rhss with precedence >= minPrec*) -fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec); +fun getRHS minPrec = List.filter (fn (_, _, prec:int) => prec >= minPrec); (*Get all rhss with precedence >= minPrec and < maxPrec*) fun getRHS' minPrec maxPrec = - filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec); + List.filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec); (*Make states using a list of rhss*) fun mkStates i minPrec lhsID rhss = @@ -656,19 +656,19 @@ in update (used, []) end; fun getS A maxPrec Si = - filter + List.filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec | _ => false) Si; fun getS' A maxPrec minPrec Si = - filter + List.filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec > minPrec andalso prec <= maxPrec | _ => false) Si; fun getStates Estate i ii A maxPrec = - filter + List.filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec | _ => false) @@ -701,7 +701,7 @@ fun token_assoc2 (list, key) = let fun assoc [] result = result | assoc ((keyi, pi) :: pairs) result = - if is_some keyi andalso matching_tokens (the keyi, key) + if isSome keyi andalso matching_tokens (valOf keyi, key) orelse include_none andalso is_none keyi then assoc pairs (pi @ result) else assoc pairs result; @@ -841,12 +841,12 @@ end; val nts = - mapfilter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => + List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => SOME (a, prec) | _ => NONE) (Array.sub (stateset, i-1)); val allowed = distinct (get_starts nts [] @ - (mapfilter (fn (_, _, _, Terminal a :: _, _, _) => SOME a + (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a | _ => NONE) (Array.sub (stateset, i-1)))); in syntax_error (if prev_token = EndToken then indata @@ -863,7 +863,7 @@ end)); -fun get_trees l = mapfilter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) +fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l; fun earley prods tags chains startsymbol indata =