--- a/src/Pure/Syntax/parser.ML Tue Apr 11 10:45:04 2023 +0200
+++ b/src/Pure/Syntax/parser.ML Tue Apr 11 10:46:43 2023 +0200
@@ -52,20 +52,10 @@
(* tokens *)
structure Tokens = Table(type key = Lexicon.token val ord = Lexicon.tokens_match_ord);
+structure Tokenset = Set(Tokens.Key);
-type tokens = Tokens.set;
-val tokens_empty: tokens = Tokens.empty;
-val tokens_merge: tokens * tokens -> tokens = Tokens.merge (K true);
-fun tokens_insert tk : tokens -> tokens = Tokens.insert_set tk;
-fun tokens_remove tk : tokens -> tokens = Tokens.remove_set tk;
-fun tokens_member (tokens: tokens) = Tokens.defined tokens;
-fun tokens_is_empty (tokens: tokens) = Tokens.is_empty tokens;
-fun tokens_fold f (tokens: tokens) = Tokens.fold (f o #1) tokens;
-val tokens_union = tokens_fold tokens_insert;
-val tokens_subtract = tokens_fold tokens_remove;
-fun tokens_find P (tokens: tokens) =
- Tokens.get_first (fn (tok, ()) => if P tok then SOME tok else NONE) tokens;
-fun tokens_add (nt: nt, tokens) = if tokens_is_empty tokens then I else cons (nt, tokens);
+fun tokens_find P tokens = Tokenset.get_first (fn tok => if P tok then SOME tok else NONE) tokens;
+fun tokens_add (nt: nt, tokens) = if Tokenset.is_empty tokens then I else cons (nt, tokens);
(* productions *)
@@ -81,10 +71,10 @@
fun prods_update entry : prods -> prods = Tokens.update entry;
fun prods_content (prods: prods) = distinct (op =) (maps #2 (Tokens.dest prods));
-type nt_gram = (nts * tokens) * prods; (*dependent_nts, start_tokens, prods*)
+type nt_gram = (nts * Tokenset.T) * prods; (*dependent_nts, start_tokens, prods*)
(*depent_nts is a set of all NTs whose lookahead depends on this NT's lookahead*)
-val nt_gram_empty: nt_gram = ((nts_empty, tokens_empty), prods_empty);
+val nt_gram_empty: nt_gram = ((nts_empty, Tokenset.empty), prods_empty);
type chains = unit Int_Graph.T;
fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains;
@@ -115,8 +105,8 @@
val unknown_start = Lexicon.eof;
fun get_start tks =
- (case Tokens.min tks of
- SOME (tk, _) => tk
+ (case Tokenset.min tks of
+ SOME tk => tk
| NONE => unknown_start);
fun add_production prods (lhs, new_prod as (rhs, _, pri)) (chains, lambdas) =
@@ -149,8 +139,8 @@
let
val ((to_nts, to_tks), ps) = Array.sub (prods, to);
- val new_tks = tokens_subtract to_tks from_tks; (*added lookahead tokens*)
- val to_tks' = tokens_merge (to_tks, new_tks);
+ val new_tks = Tokenset.subtract to_tks from_tks; (*added lookahead tokens*)
+ val to_tks' = Tokenset.merge (to_tks, new_tks);
val _ = Array.update (prods, to, ((to_nts, to_tks'), ps));
in tokens_add (to, new_tks) end;
@@ -204,12 +194,12 @@
is_none tk andalso nts_subset (nts, lambdas);
val new_tks =
- tokens_empty
- |> fold tokens_insert (the_list tk)
- |> nts_fold (tokens_union o starts_for_nt) nts
- |> tokens_subtract l_starts;
+ Tokenset.empty
+ |> fold Tokenset.insert (the_list tk)
+ |> nts_fold (curry Tokenset.merge o starts_for_nt) nts
+ |> Tokenset.subtract l_starts;
- val added_tks' = tokens_merge (added_tks, new_tks);
+ val added_tks' = Tokenset.merge (added_tks, new_tks);
val nt_dependencies' = nts_merge (nt_dependencies, nts);
@@ -218,7 +208,7 @@
prods_update (tk, p :: prods_lookup nt_prods tk) nt_prods;
val nt_prods' = nt_prods
- |> tokens_fold copy new_tks
+ |> Tokenset.fold copy new_tks
|> new_lambda ? copy Lexicon.dummy;
in
examine_prods ps (add_lambda orelse new_lambda)
@@ -239,10 +229,10 @@
(*add_lambda is true if an existing production of the nt
produces lambda due to the new lambda NT l*)
val (add_lambda, nt_dependencies, added_tks, nt_prods') =
- examine_prods tk_prods false nts_empty tokens_empty nt_prods;
+ examine_prods tk_prods false nts_empty Tokenset.empty nt_prods;
val new_nts = nts_merge (old_nts, nt_dependencies);
- val new_tks = tokens_merge (old_tks, added_tks);
+ val new_tks = Tokenset.merge (old_tks, added_tks);
val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
val _ = Array.update (prods, nt, ((new_nts, new_tks), nt_prods'));
@@ -276,14 +266,14 @@
val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty;
val start_tks =
- tokens_empty
- |> fold tokens_insert (the_list start_tk)
- |> nts_fold (tokens_union o starts_for_nt) start_nts;
+ Tokenset.empty
+ |> fold Tokenset.insert (the_list start_tk)
+ |> nts_fold (curry Tokenset.merge o starts_for_nt) start_nts;
val start_tks' =
start_tks
- |> (if is_some new_lambdas then tokens_insert Lexicon.dummy
- else if tokens_is_empty start_tks then tokens_insert unknown_start
+ |> (if is_some new_lambdas then Tokenset.insert Lexicon.dummy
+ else if Tokenset.is_empty start_tks then Tokenset.insert unknown_start
else I);
(*add lhs NT to list of dependent NTs in lookahead*)
@@ -302,7 +292,7 @@
let
val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
- val new_tks = tokens_subtract old_tks start_tks;
+ val new_tks = Tokenset.subtract old_tks start_tks;
(*store new production*)
fun store tk (prods, _) =
@@ -313,12 +303,12 @@
in (prods', true) end;
val (nt_prods', changed) = (nt_prods, false)
- |> nt = lhs ? tokens_fold store start_tks';
+ |> nt = lhs ? Tokenset.fold store start_tks';
val _ =
- if not changed andalso tokens_is_empty new_tks then ()
+ if not changed andalso Tokenset.is_empty new_tks then ()
else
Array.update
- (prods, nt, ((old_nts, tokens_merge (old_tks, new_tks)), nt_prods'));
+ (prods, nt, ((old_nts, Tokenset.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;
@@ -333,7 +323,7 @@
(*token under which old productions which
depend on changed_nt could be stored*)
val key =
- tokens_find (not o tokens_member new_tks) (starts_for_nt changed_nt)
+ tokens_find (not o Tokenset.member new_tks) (starts_for_nt changed_nt)
|> the_default unknown_start;
(*copy productions whose lookahead depends on changed_nt;
@@ -354,7 +344,7 @@
val lambda =
not (nts_is_unique depends) orelse
not (nts_is_empty depends) andalso is_some tk
- andalso tokens_member new_tks (the tk);
+ andalso Tokenset.member new_tks (the tk);
(*associate production with new starting tokens*)
fun copy tk nt_prods =
@@ -367,7 +357,7 @@
have to look for duplicates*)
in prods_update (tk, tk_prods') nt_prods end;
val result =
- if update then (tk_prods, tokens_fold copy new_tks nt_prods)
+ if update then (tk_prods, Tokenset.fold copy new_tks nt_prods)
else if key = unknown_start then (p :: tk_prods, nt_prods)
else (tk_prods, nt_prods);
in update_prods ps result end;
@@ -387,8 +377,8 @@
prods_update (key, tk_prods') nt_prods'
else nt_prods';
- val added_tks = tokens_subtract tks new_tks;
- val tks' = tokens_merge (tks, added_tks);
+ val added_tks = Tokenset.subtract tks new_tks;
+ val tks' = Tokenset.merge (tks, added_tks);
val _ = Array.update (prods, nt, ((nts, tks'), nt_prods''));
in tokens_add (nt, added_tks) end;