# HG changeset patch # User wenzelm # Date 1458322355 -3600 # Node ID c95b76681e65b3e2cade415ed060538e83c440cd # Parent 360d3464919ca8eefb70102223123c2797c00056 tuned -- fewer warnings; diff -r 360d3464919c -r c95b76681e65 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Fri Mar 18 17:58:19 2016 +0100 +++ b/src/Pure/Syntax/parser.ML Fri Mar 18 18:32:35 2016 +0100 @@ -71,7 +71,7 @@ N.B. that the chains parameter has the form [(from, [to])]; prod_count is of type "int option" and is only updated if it is <> NONE*) fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count) - | add_prods prods chains lambdas prod_count ((lhs, new_prod as (rhs, name, pri)) :: ps) = + | add_prods prods chains lambdas prod_count ((lhs, new_prod as (rhs, _, pri)) :: ps) = let val chain_from = (case (pri, rhs) of @@ -95,7 +95,7 @@ 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_tks), _) = Array.sub (prods, the new_chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead [] added = added @@ -195,7 +195,7 @@ (added_lambdas, added_starts) | process_nts (nt :: nts) added_lambdas added_starts = let - val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt); + val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt); (*existing productions whose lookahead may depend on l*) val tk_prods = @@ -235,7 +235,7 @@ in propagate_lambda (subtract (op =) lambdas lambdas') added_starts lambdas' end; (*insert production into grammar*) - val (added_starts', prod_count') = + val (added_starts', _) = if is_some chain_from then (added_starts', prod_count) (*don't store chain production*) else @@ -255,7 +255,7 @@ (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts [] = () - | add_nts (nt :: nts) = + | add_nts (nt :: _) = let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in if member (op =) old_nts lhs then () else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps)) @@ -567,7 +567,7 @@ filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) -fun mk_states i min_prec lhs_ID rhss = +fun mk_states i lhs_ID rhss = let fun mk_state (rhs, id, prod_prec) = (lhs_ID, prod_prec, [], rhs, id, i); in map mk_state rhss end; @@ -604,11 +604,11 @@ A = B andalso prec > min_prec andalso prec <= max_prec | _ => false) Si; -fun get_states Estate i ii A max_prec = +fun get_states Estate j A max_prec = filter (fn (_, _, _, Nonterminal (B, prec) :: _, _, _) => A = B andalso prec <= max_prec | _ => false) - (Array.sub (Estate, ii)); + (Array.sub (Estate, j)); fun movedot_term c (A, j, ts, Terminal a :: sa, id, i) = @@ -654,7 +654,7 @@ let fun all_prods_for nt = prods_for prods chains true c [nt]; - fun processS used [] (Si, Sii) = (Si, Sii) + fun processS _ [] (Si, Sii) = (Si, Sii) | processS used (S :: States) (Si, Sii) = (case S of (_, _, _, Nonterminal (nt, min_prec) :: _, _, _) => @@ -669,12 +669,12 @@ let val tk_prods = all_prods_for nt; val States' = - mk_states i min_prec nt (get_RHS' min_prec used_prec tk_prods); + mk_states i nt (get_RHS' min_prec used_prec tk_prods); in (update_prec (nt, min_prec) used, movedot_lambda l S @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = all_prods_for nt; - val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods); + val States' = mk_states i nt (get_RHS min_prec tk_prods); in (Inttab.update (nt, (min_prec, [])) used, States') end); in processS used' (new_states @ States) (S :: Si, Sii) @@ -692,7 +692,7 @@ val States' = map (movedot_nonterm tt) Slist; in processS used' (States' @ States) (S :: Si, Sii) end else - let val Slist = get_states Estate i j A prec + let val Slist = get_states Estate j A prec in processS used (map (movedot_nonterm tt) Slist @ States) (S :: Si, Sii) end end) in processS Inttab.empty states ([], []) end;