src/Pure/Syntax/parser.ML

--- a/src/Pure/Syntax/parser.ML	Tue Jan 30 16:05:33 2018 +0100
+++ b/src/Pure/Syntax/parser.ML	Tue Jan 30 16:12:50 2018 +0100
@@ -36,6 +36,9 @@
 fun nts_insert nt : nts -> nts = Inttab.insert_set nt;
 fun nts_member (nts: nts) = Inttab.defined nts;
 fun nts_fold f (nts: nts) = Inttab.fold (f o #1) nts;
+fun nts_subset (nts1: nts, nts2: nts) = Inttab.forall (nts_member nts2 o #1) nts1;
+fun nts_is_empty (nts: nts) = Inttab.is_empty nts;
+fun nts_is_unique (nts: nts) = nts_is_empty nts orelse Inttab.is_single nts;
 
 datatype symb =
   Terminal of Lexicon.token
@@ -154,8 +157,8 @@
           | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts)
           | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts =
               if nts_member lambdas nt then
-                lookahead_dependency lambdas symbs (nt :: nts)
-              else (NONE, nt :: nts);
+                lookahead_dependency lambdas symbs (nts_insert nt nts)
+              else (NONE, nts_insert nt nts);
 
         (*get all known starting tokens for a nonterminal*)
         fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));
@@ -175,20 +178,20 @@
                           (add_lambda, nt_dependencies, added_tks, nt_prods)
                       | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
                             nt_dependencies added_tks nt_prods =
-                          let val (tk, nts) = lookahead_dependency lambdas rhs [] in
-                            if member (op =) nts l then       (*update production's lookahead*)
+                          let val (tk, nts) = lookahead_dependency lambdas rhs nts_empty in
+                            if nts_member nts l then       (*update production's lookahead*)
                               let
                                 val new_lambda =
-                                  is_none tk andalso forall (nts_member lambdas) nts;
+                                  is_none tk andalso nts_subset (nts, lambdas);
 
                                 val new_tks =
                                   the_list tk
-                                  |> fold (tokens_union o starts_for_nt) nts
+                                  |> nts_fold (tokens_union o starts_for_nt) nts
                                   |> tokens_subtract l_starts;
 
                                 val added_tks' = tokens_union added_tks new_tks;
 
-                                val nt_dependencies' = fold nts_insert nts nt_dependencies;
+                                val nt_dependencies' = nts_merge (nt_dependencies, nts);
 
                                 (*associate production with new starting tokens*)
                                 fun copy ([]: Lexicon.token list) nt_prods = nt_prods
@@ -261,11 +264,11 @@
             let
               (*lookahead tokens of new production and on which
                 NTs lookahead depends*)
-              val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
+              val (start_tk, start_nts) = lookahead_dependency lambdas' rhs nts_empty;
 
               val start_tks =
                 the_list start_tk
-                |> fold (tokens_union o starts_for_nt) start_nts;
+                |> nts_fold (tokens_union o starts_for_nt) start_nts;
 
               val start_tks' =
                (if is_some new_lambdas then [token_none]
@@ -273,12 +276,13 @@
                 else []) @ start_tks;
 
               (*add lhs NT to list of dependent NTs in lookahead*)
-              fun add_nts [] = ()
-                | add_nts (nt :: _) =
-                    let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
-                      if nts_member old_nts lhs then ()
-                      else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
-                    end;
+              fun add_nts nt initial =
+                (if initial then
+                  let val ((old_nts, old_tks), ps) = Array.sub (prods, nt) in
+                    if nts_member old_nts lhs then ()
+                    else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
+                  end
+                 else (); false);
 
               (*add new start tokens to chained NTs' lookahead list;
                 also store new production for lhs NT*)
@@ -324,7 +328,7 @@
                       add_tks nts
                         (if null new_tks then added else (nt, new_tks) :: added) prod_count'
                     end;
-              val _ = add_nts start_nts;
+              val _ = nts_fold add_nts start_nts true;
             in
               add_tks (chains_all_succs chains' [lhs]) [] prod_count
             end;
@@ -350,16 +354,16 @@
                             (tk_prods, nt_prods) =
                           let
                             (*lookahead dependency for production*)
-                            val (tk, depends) = lookahead_dependency lambdas' rhs [];
+                            val (tk, depends) = lookahead_dependency lambdas' rhs nts_empty;
 
                             (*test if this production has to be copied*)
-                            val update = member (op =) depends changed_nt;
+                            val update = nts_member depends changed_nt;
 
                             (*test if production could already be associated with
                               a member of new_tks*)
                             val lambda =
-                              length depends > 1 orelse
-                              not (null depends) andalso is_some tk
+                              not (nts_is_unique depends) orelse
+                              not (nts_is_empty depends) andalso is_some tk
                               andalso member (op =) new_tks (the tk);
 
                             (*associate production with new starting tokens*)