diff -r 2587b492664a -r 91fc15d9dbdf src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue May 09 19:47:11 2023 +0200 +++ b/src/Pure/Syntax/parser.ML Tue May 09 19:56:31 2023 +0200 @@ -110,7 +110,7 @@ SOME tk => tk | NONE => unknown_start); -fun add_production prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) = +fun add_production array_prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) = let (*store chain if it does not already exist*) val (chain, new_chain, chains') = @@ -133,16 +133,16 @@ if not new_chain then ([], lambdas) else let (*lookahead of chain's source*) - val ((_, from_tks), _) = Array.nth prods (the chain); + val ((_, from_tks), _) = Array.nth array_prods (the chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead to = let - val ((to_nts, to_tks), ps) = Array.nth prods to; + val ((to_nts, to_tks), ps) = Array.nth array_prods to; val new_tks = Tokens.subtract to_tks from_tks; (*added lookahead tokens*) val to_tks' = Tokens.merge (to_tks, new_tks); - val _ = Array.upd prods to ((to_nts, to_tks'), ps); + val _ = Array.upd array_prods to ((to_nts, to_tks'), ps); in tokens_add (to, new_tks) end; val tos = chains_all_succs chains' [lhs]; @@ -171,7 +171,7 @@ else (NONE, nts_insert nt nts); (*get all known starting tokens for a nonterminal*) - fun starts_for_nt nt = snd (fst (Array.nth prods nt)); + fun starts_for_nt nt = snd (fst (Array.nth array_prods nt)); (*update prods, lookaheads, and lambdas according to new lambda NTs*) val (added_starts', lambdas') = @@ -181,7 +181,7 @@ | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) - val ((dependent, l_starts), _) = Array.nth prods l; + val ((dependent, l_starts), _) = Array.nth array_prods l; (*check productions whose lookahead may depend on lambda NT*) fun examine_prods [] add_lambda nt_dependencies added_tks nt_prods = @@ -222,7 +222,7 @@ (*check each NT whose lookahead depends on new lambda NT*) fun process_nts nt (added_lambdas, added_starts) = let - val ((old_nts, old_tks), nt_prods) = Array.nth prods nt; + val ((old_nts, old_tks), nt_prods) = Array.nth array_prods nt; (*existing productions whose lookahead may depend on l*) val tk_prods = prods_lookup nt_prods (get_start l_starts); @@ -236,7 +236,7 @@ val new_tks = Tokens.merge (old_tks, added_tks); val added_lambdas' = added_lambdas |> add_lambda ? cons nt; - val _ = Array.upd prods nt ((new_nts, new_tks), nt_prods'); + val _ = Array.upd array_prods nt ((new_nts, new_tks), nt_prods'); (*N.B. that because the tks component is used to access existing productions we have to add new @@ -280,9 +280,9 @@ (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts nt initial = (if initial then - let val ((old_nts, old_tks), ps) = Array.nth prods nt in + let val ((old_nts, old_tks), ps) = Array.nth array_prods nt in if nts_member old_nts lhs then () - else Array.upd prods nt ((nts_insert lhs old_nts, old_tks), ps) + else Array.upd array_prods nt ((nts_insert lhs old_nts, old_tks), ps) end else (); false); @@ -291,7 +291,7 @@ fun add_tks [] added = added | add_tks (nt :: nts) added = let - val ((old_nts, old_tks), nt_prods) = Array.nth prods nt; + val ((old_nts, old_tks), nt_prods) = Array.nth array_prods nt; val new_tks = Tokens.subtract old_tks start_tks; @@ -307,7 +307,7 @@ |> nt = lhs ? Tokens.fold store start_tks'; val _ = if not changed andalso Tokens.is_empty new_tks then () - else Array.upd prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'); + else Array.upd array_prods nt ((old_nts, Tokens.merge (old_tks, new_tks)), nt_prods'); in add_tks nts (tokens_add (nt, new_tks) added) end; val _ = nts_fold add_nts start_nts true; in add_tks (chains_all_succs chains' [lhs]) [] end; @@ -364,7 +364,7 @@ (*copy existing productions for new starting tokens*) fun process_nts nt = let - val ((nts, tks), nt_prods) = Array.nth prods nt; + val ((nts, tks), nt_prods) = Array.nth array_prods nt; val tk_prods = prods_lookup nt_prods key; @@ -378,10 +378,10 @@ val added_tks = Tokens.subtract tks new_tks; val tks' = Tokens.merge (tks, added_tks); - val _ = Array.upd prods nt ((nts, tks'), nt_prods''); + val _ = Array.upd array_prods nt ((nts, tks'), nt_prods''); in tokens_add (nt, added_tks) end; - val ((dependent, _), _) = Array.nth prods changed_nt; + val ((dependent, _), _) = Array.nth array_prods changed_nt; in add_starts (starts @ nts_fold process_nts dependent []) end; in add_starts added_starts' end; in (chains', lambdas') end; @@ -469,18 +469,13 @@ val (nt_count', prod_count', tags', xprods') = prod_of xprods nt_count prod_count tags []; - (*Copy array containing productions of old grammar; - this has to be done to preserve the old grammar while being able - to change the array's content*) - val prods' = - let - fun get_prod i = - if i < nt_count then Vector.nth prods i - else nt_gram_empty; - in Array.tabulate (nt_count', get_prod) end; + val array_prods' = + Array.tabulate (nt_count', fn i => + if i < nt_count then Vector.nth prods i + else nt_gram_empty); val (chains', lambdas') = - (chains, lambdas) |> fold (add_production prods') xprods'; + (chains, lambdas) |> fold (add_production array_prods') xprods'; in Gram {nt_count = nt_count', @@ -488,7 +483,7 @@ tags = tags', chains = chains', lambdas = lambdas', - prods = Array.vector prods'} + prods = Array.vector array_prods'} end; fun make_gram xprods = extend_gram xprods empty_gram;