--- 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;