src/Pure/Syntax/parser.ML

 
 (** datatype gram **)
 
 (*production for the NTs are stored in a vector
   so we can identify NTs by their index*)
-type nt_tag = int;
+type nt = int;
+
+type nts = Inttab.set;
+val nts_empty: nts = Inttab.empty;
+val nts_merge: nts * nts -> nts = Inttab.merge (K true);
+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;
 
 datatype symb =
   Terminal of Lexicon.token
-| Nonterminal of nt_tag * int;  (*(tag, precedence)*)
+| Nonterminal of nt * int;  (*(tag, precedence)*)
 
 type nt_gram =
-  ((nt_tag list * Lexicon.token list) *
+  ((nts * Lexicon.token list) *
     (Lexicon.token option * (symb list * string * int) list) list);
   (*(([dependent_nts], [start_tokens]), [(start_token, [(rhs, name, prio)])])*)
   (*depent_nts is a list of all NTs whose lookahead depends on this NT's lookahead*)
 
-type tags = nt_tag Symtab.table;
+val nt_gram_empty: nt_gram = ((nts_empty, []), []);
+
+type tags = nt Symtab.table;
 val tags_empty: tags = Symtab.empty;
 fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags);
 fun tags_lookup (tags: tags) = Symtab.lookup tags;
 fun tags_insert tag (tags: tags) = Symtab.update_new tag tags;
 fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags)));

 fun chains_member (chains: chains) = Int_Graph.is_edge chains;
 fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ());
 fun chains_insert (from, to) =
   chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to);
 
-type lambdas = Inttab.set;
-val lambdas_empty: lambdas = Inttab.empty;
-fun lambdas_member (lambdas: lambdas) = Inttab.defined lambdas;
-fun lambdas_insert nt : lambdas -> lambdas = Inttab.insert_set nt;
-fun lambdas_fold f (lambdas: lambdas) = Inttab.fold (f o #1) lambdas;
-
 datatype gram =
   Gram of
    {nt_count: int,
     prod_count: int,
     tags: tags,
     chains: chains,
-    lambdas: lambdas,
+    lambdas: nts,
     prods: nt_gram Vector.vector};
     (*"tags" is used to map NT names (i.e. strings) to tags;
      chain productions are not stored as normal productions
      but instead as an entry in "chains": from -> to;
      lambda productions are stored as normal productions

                     end;
 
               val tos = chains_all_succs chains' [lhs];
             in
               (copy_lookahead tos [],
-                lambdas |> lambdas_member lambdas lhs ? fold lambdas_insert tos)
+                lambdas |> nts_member lambdas lhs ? fold nts_insert tos)
             end;
 
         (*test if new production can produce lambda
           (rhs must either be empty or only consist of lambda NTs)*)
         val new_lambdas =
           if forall
-            (fn Nonterminal (id, _) => lambdas_member lambdas' id
+            (fn Nonterminal (id, _) => nts_member lambdas' id
               | Terminal _ => false) rhs
-          then SOME (filter_out (lambdas_member lambdas') (chains_all_succs chains' [lhs]))
+          then SOME (filter_out (nts_member lambdas') (chains_all_succs chains' [lhs]))
           else NONE;
-        val lambdas'' = fold lambdas_insert (these new_lambdas) lambdas';
+        val lambdas'' = fold nts_insert (these new_lambdas) lambdas';
 
         (*list optional terminal and all nonterminals on which the lookahead
           of a production depends*)
         fun lookahead_dependency _ [] nts = (NONE, nts)
           | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts)
           | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts =
-              if lambdas_member lambdas nt then
+              if nts_member lambdas nt then
                 lookahead_dependency lambdas symbs (nt :: nts)
               else (NONE, nt :: nts);
 
         (*get all known starting tokens for a nonterminal*)
         fun starts_for_nt nt = snd (fst (Array.sub (prods, nt)));

                             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 new_lambda =
-                                  is_none tk andalso forall (lambdas_member lambdas) nts;
+                                  is_none tk andalso forall (nts_member lambdas) nts;
 
                                 val new_tks =
                                   (if is_some tk then [the tk] else [])
                                   |> fold (tokens_union o starts_for_nt) nts
                                   |> subtract (op =) l_starts;
 
                                 val added_tks' = tokens_union added_tks new_tks;
 
-                                val nt_dependencies' = union (op =) nts nt_dependencies;
+                                val nt_dependencies' = fold nts_insert nts nt_dependencies;
 
                                 (*associate production with new starting tokens*)
                                 fun copy ([]: Lexicon.token option list) nt_prods = nt_prods
                                   | copy (tk :: tks) nt_prods =
                                       let

                             else (*skip production*)
                               examine_prods ps add_lambda nt_dependencies added_tks nt_prods
                           end;
 
                     (*check each NT whose lookahead depends on new lambda NT*)
-                    fun process_nts [] added_lambdas added_starts =
-                          (added_lambdas, added_starts)
-                      | process_nts (nt :: nts) added_lambdas added_starts =
-                          let
-                            val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
-
-                            (*existing productions whose lookahead may depend on l*)
-                            val tk_prods =
-                              these (AList.lookup (op =) nt_prods (SOME (get_start l_starts)));
-
-                            (*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 [] [] nt_prods;
-
-                            val added_nts = subtract (op =) old_nts nt_dependencies;
-
-                            val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
-                            val _ =
-                              Array.update
-                                (prods, nt, ((added_nts @ old_nts, old_tks @ added_tks), nt_prods'));
-                              (*N.B. that because the tks component
-                                is used to access existing
-                                productions we have to add new
-                                tokens at the _end_ of the list*)
-                          in
-                            if null added_tks then
-                              process_nts nts added_lambdas' added_starts
-                            else
-                              process_nts nts added_lambdas' ((nt, added_tks) :: added_starts)
-                          end;
-
-                    val (added_lambdas, added_starts') = process_nts dependent [] added_starts;
-                    val added_lambdas' = filter_out (lambdas_member lambdas) added_lambdas;
+                    fun process_nts nt (added_lambdas, added_starts) =
+                      let
+                        val ((old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+
+                        (*existing productions whose lookahead may depend on l*)
+                        val tk_prods =
+                          these (AList.lookup (op =) nt_prods (SOME (get_start l_starts)));
+
+                        (*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 [] nt_prods;
+
+                        val new_nts = nts_merge (old_nts, nt_dependencies);
+
+                        val added_lambdas' = added_lambdas |> add_lambda ? cons nt;
+                        val _ =
+                          Array.update (prods, nt, ((new_nts, old_tks @ added_tks), nt_prods'));
+                          (*N.B. that because the tks component
+                            is used to access existing
+                            productions we have to add new
+                            tokens at the _end_ of the list*)
+                        val added_starts' =
+                          if null added_tks then added_starts
+                          else ((nt, added_tks) :: added_starts);
+                      in (added_lambdas', added_starts') end;
+
+                    val (added_lambdas, added_starts') =
+                      nts_fold process_nts dependent ([], added_starts);
+                    val added_lambdas' = filter_out (nts_member lambdas) added_lambdas;
                   in
                     propagate_lambda (ls @ added_lambdas') added_starts'
-                      (fold lambdas_insert added_lambdas' lambdas)
+                      (fold nts_insert added_lambdas' lambdas)
                   end;
           in
             propagate_lambda
-              (lambdas_fold (fn l => not (lambdas_member lambdas l) ? cons l) lambdas'' [])
+              (nts_fold (fn l => not (nts_member lambdas l) ? cons l) lambdas'' [])
               added_starts lambdas''
           end;
 
         (*insert production into grammar*)
         val (added_starts', _) =

 
               (*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 member (op =) old_nts lhs then ()
-                      else Array.update (prods, nt, ((lhs :: old_nts, old_tks), ps))
+                      if nts_member old_nts lhs then ()
+                      else Array.update (prods, nt, ((nts_insert lhs old_nts, old_tks), ps))
                     end;
 
               (*add new start tokens to chained NTs' lookahead list;
                 also store new production for lhs NT*)
               fun add_tks [] added prod_count = (added, prod_count)

 
                     (*copy productions whose lookahead depends on changed_nt;
                       if key = SOME unknown_start then tk_prods is used to hold
                       the productions not copied*)
                     fun update_prods [] result = result
-                      | update_prods ((p as (rhs, _: string, _: nt_tag)) :: ps)
+                      | update_prods ((p as (rhs, _: string, _: nt)) :: ps)
                             (tk_prods, nt_prods) =
                           let
                             (*lookahead dependency for production*)
                             val (tk, depends) = lookahead_dependency lambdas' rhs [];
 

                               else if key = SOME unknown_start then (p :: tk_prods, nt_prods)
                               else (tk_prods, nt_prods);
                           in update_prods ps result end;
 
                     (*copy existing productions for new starting tokens*)
-                    fun process_nts [] added = added
-                      | process_nts (nt :: nts) added =
-                          let
-                            val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
-
-                            val tk_prods = these (AList.lookup (op =) nt_prods key);
-
-                            (*associate productions with new lookahead tokens*)
-                            val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods);
-
-                            val nt_prods'' =
-                              if key = SOME unknown_start then
-                                AList.update (op =) (key, tk_prods') nt_prods'
-                              else nt_prods';
-
-                            val added_tks = tokens_subtract old_tks new_tks;
-                          in
-                            if null added_tks then
-                              (Array.update (prods, nt, (lookahead, nt_prods''));
-                                process_nts nts added)
-                            else
-                              (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods''));
-                                process_nts nts ((nt, added_tks) :: added))
-                          end;
+                    fun process_nts nt added =
+                      let
+                        val (lookahead as (old_nts, old_tks), nt_prods) = Array.sub (prods, nt);
+
+                        val tk_prods = these (AList.lookup (op =) nt_prods key);
+
+                        (*associate productions with new lookahead tokens*)
+                        val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods);
+
+                        val nt_prods'' =
+                          if key = SOME unknown_start then
+                            AList.update (op =) (key, tk_prods') nt_prods'
+                          else nt_prods';
+
+                        val added_tks = tokens_subtract old_tks new_tks;
+                      in
+                        if null added_tks then
+                          (Array.update (prods, nt, (lookahead, nt_prods''));
+                            added)
+                        else
+                          (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods''));
+                            ((nt, added_tks) :: added))
+                      end;
 
                     val ((dependent, _), _) = Array.sub (prods, changed_nt);
-                  in add_starts (starts @ process_nts dependent []) end;
+                  in add_starts (starts @ nts_fold process_nts dependent []) end;
           in add_starts added_starts' end;
       in add_prods prods chains' lambdas' prod_count ps end;
 
 
 (* pretty_gram *)

   Gram
    {nt_count = 0,
     prod_count = 0,
     tags = tags_empty,
     chains = chains_empty,
-    lambdas = lambdas_empty,
-    prods = Vector.fromList [(([], []), [])]};
+    lambdas = nts_empty,
+    prods = Vector.fromList [nt_gram_empty]};
 
 
 (*Add productions to a grammar*)
 fun extend_gram [] gram = gram
   | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) =

           to change the array's content*)
         val prods' =
           let
             fun get_prod i =
               if i < nt_count then Vector.sub (prods, i)
-              else (([], []), []);
+              else nt_gram_empty;
           in Array.tabulate (nt_count', get_prod) end;
 
         (*Add new productions to old ones*)
         val (chains', lambdas', _) = add_prods prods' chains lambdas NONE xprods';
       in

 
 
 (* parser state *)
 
 type state =
-  nt_tag * int *    (*identification and production precedence*)
+  nt * int *    (*identification and production precedence*)
   parsetree list *  (*already parsed nonterminals on rhs*)
   symb list *       (*rest of rhs*)
   string *          (*name of production*)
   int;              (*index for previous state list*)