# HG changeset patch # User wenzelm # Date 1282751135 -7200 # Node ID 29d0298439bee55660e7cb734df838a24994508e # Parent f7688fd819a86d31350d40cc1fefd70f100c3329 eliminated some old camel case stuff; diff -r f7688fd819a8 -r 29d0298439be src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Wed Aug 25 17:34:10 2010 +0200 +++ b/src/Pure/Syntax/parser.ML Wed Aug 25 17:45:35 2010 +0200 @@ -56,7 +56,7 @@ (*productions for which no starting token is known yet are associated with this token*) -val UnknownStart = Lexicon.eof; +val unknown_start = Lexicon.eof; (*get all NTs that are connected with a list of NTs*) fun connected_with _ ([]: nt_tag list) relatives = relatives @@ -199,7 +199,7 @@ val tk_prods = these (AList.lookup (op =) nt_prods - (SOME (hd l_starts handle Empty => UnknownStart))); + (SOME (hd l_starts handle Empty => unknown_start))); (*add_lambda is true if an existing production of the nt produces lambda due to the new lambda NT l*) @@ -249,7 +249,7 @@ val opt_starts = (if new_lambda then [NONE] - else if null start_tks then [SOME UnknownStart] + else if null start_tks then [SOME unknown_start] else []) @ map SOME start_tks; (*add lhs NT to list of dependent NTs in lookahead*) @@ -318,11 +318,11 @@ depend on changed_nt could be stored*) val key = (case find_first (not o member (op =) new_tks) (starts_for_nt changed_nt) of - NONE => SOME UnknownStart + NONE => SOME unknown_start | t => t); (*copy productions whose lookahead depends on changed_nt; - if key = SOME UnknownToken then tk_prods is used to hold + if key = SOME unknown_start then tk_prods is used to hold the productions not copied*) fun update_prods [] result = result | update_prods ((p as (rhs, _: string, _: nt_tag)) :: ps) @@ -359,7 +359,7 @@ end; val result = if update then (tk_prods, copy new_tks nt_prods) - else if key = SOME UnknownStart then (p :: tk_prods, nt_prods) + else if key = SOME unknown_start then (p :: tk_prods, nt_prods) else (tk_prods, nt_prods); in update_prods ps result end; @@ -376,7 +376,7 @@ val nt_prods' = nt_prods' - |> (key = SOME UnknownStart) ? AList.update (op =) (key, tk_prods'); + |> (key = SOME unknown_start) ? AList.update (op =) (key, tk_prods'); val added_tks = subtract Lexicon.matching_tokens old_tks new_tks; in @@ -640,17 +640,17 @@ int; (*index for previous state list*) -(*Get all rhss with precedence >= minPrec*) -fun getRHS minPrec = filter (fn (_, _, prec:int) => prec >= minPrec); +(*Get all rhss with precedence >= min_prec*) +fun get_RHS min_prec = filter (fn (_, _, prec:int) => prec >= min_prec); -(*Get all rhss with precedence >= minPrec and < maxPrec*) -fun getRHS' minPrec maxPrec = - filter (fn (_, _, prec:int) => prec >= minPrec andalso prec < maxPrec); +(*Get all rhss with precedence >= min_prec and < max_prec*) +fun get_RHS' min_prec max_prec = + filter (fn (_, _, prec:int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) -fun mkStates i minPrec lhsID rhss = - let fun mkState (rhs, id, prodPrec) = (lhsID, prodPrec, [], rhs, id, i); - in map mkState rhss end; +fun mk_states i min_prec lhs_ID rhss = + let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i); + in map mk_state rhss end; (*Add parse tree to list and eliminate duplicates saving the maximum precedence*) @@ -682,20 +682,20 @@ else update (used, hd :: used') in update (used, []) end; -fun getS A maxPrec Si = +fun getS A max_prec Si = filter - (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec + (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) Si; -fun getS' A maxPrec minPrec Si = +fun getS' A max_prec min_prec Si = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) - => A = B andalso prec > minPrec andalso prec <= maxPrec + => A = B andalso prec > min_prec andalso prec <= max_prec | _ => false) Si; -fun getStates Estate i ii A maxPrec = +fun get_states Estate i ii A max_prec = filter - (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= maxPrec + (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) (Array.sub (Estate, ii)); @@ -745,29 +745,29 @@ fun processS used [] (Si, Sii) = (Si, Sii) | processS used (S :: States) (Si, Sii) = (case S of - (_, _, _, Nonterminal (nt, minPrec) :: _, _, _) => + (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => let (*predictor operation*) val (used', new_states) = (case AList.lookup (op =) used nt of - SOME (usedPrec, l) => (*nonterminal has been processed*) - if usedPrec <= minPrec then + SOME (used_prec, l) => (*nonterminal has been processed*) + if used_prec <= min_prec then (*wanted precedence has been processed*) (used, movedot_lambda S l) else (*wanted precedence hasn't been parsed yet*) let val tk_prods = all_prods_for nt; - val States' = mkStates i minPrec nt - (getRHS' minPrec usedPrec tk_prods); - in (update_prec (nt, minPrec) used, + val States' = mk_states i min_prec nt + (get_RHS' min_prec used_prec tk_prods); + in (update_prec (nt, min_prec) used, movedot_lambda S l @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = all_prods_for nt; - val States' = mkStates i minPrec nt (getRHS minPrec tk_prods); - in ((nt, (minPrec, [])) :: used, States') end); + val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods); + in ((nt, (min_prec, [])) :: used, States') end); val dummy = if not (! warned) andalso @@ -803,7 +803,7 @@ in processS used' (States' @ States) (S :: Si, Sii) end) end else - let val Slist = getStates Estate i j A prec + let val Slist = get_states Estate i j A prec in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end end) in processS [] states ([], []) end;