src/Pure/Syntax/parser.ML

 
 Isabelle's main parser (used for terms and types).
 *)
 
 signature PARSER =
-  sig
+sig
   type gram
   val empty_gram: gram
   val extend_gram: gram -> SynExt.xprod list -> gram
+  val make_gram: SynExt.xprod list -> gram
   val merge_grams: gram -> gram -> gram
   val pretty_gram: gram -> Pretty.T list
   datatype parsetree =
     Node of string * parsetree list |
     Tip of Lexicon.token
   val parse: gram -> string -> Lexicon.token list -> parsetree list
   val branching_level: int ref
-  end;
-
-
-structure Parser : PARSER =
+end;
+
+structure Parser: PARSER =
 struct
+
 open Lexicon SynExt;
+
 
 (** datatype gram **)
 
 type nt_tag = int;              (*production for the NTs are stored in an array
                                   so we can identify NTs by their index*)

                          and also as an entry in "lambdas"*)
 
 val UnknownStart = EndToken;       (*productions for which no starting token is
                                      known yet are associated with this token*)
 
-(* get all NTs that are connected with a list of NTs 
+(* get all NTs that are connected with a list of NTs
    (used for expanding chain list)*)
 fun connected_with _ [] relatives = relatives
   | connected_with chains (root :: roots) relatives =
     let val branches = (assocs chains root) \\ relatives;
     in connected_with chains (branches @ roots) (branches @ relatives) end;

    prod_count is of type "int option" and is only updated if it is <> NONE*)
 fun add_prods _ chains lambdas prod_count [] = (chains, lambdas, prod_count)
   | add_prods prods chains lambdas prod_count
               ((lhs, new_prod as (rhs, name, pri)) :: ps) =
     let
-      (*test if new_prod is a chain production*)
-      val (new_chain, chains') =
-        let (*store chain if it does not already exist*)
-            fun store_chain from =
-              let val old_tos = assocs chains from;
-              in if lhs mem old_tos then (NONE, chains)
-                 else (SOME from, overwrite (chains, (from, lhs ins old_tos)))
-              end;
-        in if pri = ~1 then
-             case rhs of [Nonterminal (id, ~1)] => store_chain id
-                       | _ => (NONE, chains)
-           else (NONE, chains)
+      val chain_from = case (pri, rhs) of (~1, [Nonterminal (id, ~1)]) => SOME id | _ => NONE;
+
+      (*store chain if it does not already exist*)
+      val (new_chain, chains') = case chain_from of NONE => (NONE, chains) | SOME from =>
+        let val old_tos = assocs chains from in
+          if lhs mem old_tos then (NONE, chains)
+          else (SOME from, overwrite (chains, (from, lhs ins old_tos)))
         end;
 
       (*propagate new chain in lookahead and lambda lists;
         added_starts is used later to associate existing
         productions with new starting tokens*)

             | propagate_lambda (l :: ls) added_starts lambdas =
               let
                 (*get lookahead for lambda NT*)
                 val ((dependent, l_starts), _) = Array.sub (prods, l);
 
-                (*check productions whose lookahead may depend on lamdba NT*)
+                (*check productions whose lookahead may depend on lambda NT*)
                 fun examine_prods [] add_lambda nt_dependencies added_tks
                                   nt_prods =
                       (add_lambda, nt_dependencies, added_tks, nt_prods)
                   | examine_prods ((p as (rhs, _, _)) :: ps) add_lambda
                       nt_dependencies added_tks nt_prods =

                         val new_lambda = is_none tk andalso nts subset lambdas;
 
                         val new_tks = (if isSome tk then [valOf tk] else []) @
                           Library.foldl token_union ([], map starts_for_nt nts) \\
                           l_starts;
-  
+
                         val added_tks' = token_union (new_tks, added_tks);
 
                         val nt_dependencies' = nts union nt_dependencies;
 
                         (*associate production with new starting tokens*)

                             let val old_prods = assocs nt_prods tk;
 
                                 val prods' = p :: old_prods;
                             in copy tks (overwrite (nt_prods, (tk, prods')))
                             end;
-  
+
                         val nt_prods' =
                           let val new_opt_tks = map SOME new_tks;
                           in copy ((if new_lambda then [NONE] else []) @
                                    new_opt_tks) nt_prods
                           end;

               end;
         in propagate_lambda (lambdas' \\ lambdas) added_starts lambdas' end;
 
       (*insert production into grammar*)
       val (added_starts', prod_count') =
-        if isSome new_chain then (added_starts', prod_count)
-                                               (*don't store chain production*)
+        if isSome chain_from then (added_starts', prod_count)  (*don't store chain production*)
         else let
           (*lookahead tokens of new production and on which
             NTs lookahead depends*)
           val (start_tk, start_nts) = lookahead_dependency lambdas' rhs [];
 

 
         val nt_prods =
           Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @
           map prod_of_chain (assocs chains tag);
       in map (pretty_prod name) nt_prods end;
-        
+
   in List.concat (map pretty_nt taglist) end;
 
 
 (** Operations on gramars **)
 

     val chains' = inverse_chains fromto_chains' [];
   in Gram {nt_count = nt_count', prod_count = prod_count', tags = tags',
            chains = chains', lambdas = lambdas', prods = prods'}
   end;
 
+val make_gram = extend_gram empty_gram;
+
 
 (*Merge two grammars*)
 fun merge_grams gram_a gram_b =
   let
     (*find out which grammar is bigger*)

                      (fst (valOf (find_first (fn (n, t) => t = tag) tag_list)));
               in Array.update (table, tag, tag');
                  store_tag nt_count' tags' (tag-1)
               end;
       in (store_tag nt_count1 tags1 (nt_count2-1), table) end;
-    
+
     (*convert grammar2 tag to grammar1 tag*)
     fun convert_tag tag = Array.sub (tag_table, tag);
 
     (*convert chain list to raw productions*)
     fun mk_chain_prods [] result = result

 
           fun make [] result = result
             | make (from :: froms) result = make froms ((to_tag,
                 ([Nonterminal (convert_tag from, ~1)], "", ~1)) :: result);
         in mk_chain_prods cs (make froms [] @ result) end;
-        
+
     val chain_prods = mk_chain_prods chains2 [];
 
     (*convert prods2 array to productions*)
     fun process_nt ~1 result = result
       | process_nt nt result =

 (*Make states using a list of rhss*)
 fun mkStates i minPrec lhsID rhss =
   let fun mkState (rhs, id, prodPrec) = (lhsID, prodPrec, [], rhs, id, i);
   in map mkState rhss end;
 
-(*Add parse tree to list and eliminate duplicates 
+(*Add parse tree to list and eliminate duplicates
   saving the maximum precedence*)
 fun conc (t, prec:int) [] = (NONE, [(t, prec)])
   | conc (t, prec) ((t', prec') :: ts) =
       if t = t' then
-        (SOME prec', if prec' >= prec then (t', prec') :: ts 
+        (SOME prec', if prec' >= prec then (t', prec') :: ts
                      else (t, prec) :: ts)
       else
         let val (n, ts') = conc (t, prec) ts
         in (n, (t', prec') :: ts') end;
 

 let (*similar to token_assoc but does not automatically include 'NONE' key*)
     fun token_assoc2 (list, key) =
       let fun assoc [] result = result
             | assoc ((keyi, pi) :: pairs) result =
                 if isSome keyi andalso matching_tokens (valOf keyi, key)
-                   orelse include_none andalso is_none keyi then 
+                   orelse include_none andalso is_none keyi then
                   assoc pairs (pi @ result)
                 else assoc pairs result;
       in assoc list [] end;
 
     fun get_prods [] result = result

                                       (*wanted precedence has been processed*)
                     (used, movedot_lambda S l)
                   else            (*wanted precedence hasn't been parsed yet*)
                     let
                       val tk_prods = all_prods_for nt;
-                      
+
                       val States' = mkStates i minPrec nt
                                       (getRHS' minPrec usedPrec tk_prods);
-                    in (update_prec (nt, minPrec) used, 
+                    in (update_prec (nt, minPrec) used,
                         movedot_lambda S l @ States')
                     end
 
               | NONE =>           (*nonterminal is parsed for the first time*)
                   let val tk_prods = all_prods_for nt;

                     if n >= prec then processS used' States (S :: Si, Sii)
                     else
                       let val Slist = getS' A prec n Si;
                           val States' = map (movedot_nonterm tt) Slist;
                       in processS used' (States' @ States) (S :: Si, Sii) end
-              end 
+              end
             else
               let val Slist = getStates Estate i j A prec
               in processS used (map (movedot_nonterm tt) Slist @ States)
                           (S :: Si, Sii)
               end

     val msg =
       if null toks then Pretty.str "Inner syntax error: unexpected end of input"
       else
         Pretty.block (Pretty.str "Inner syntax error at: \"" ::
           Pretty.breaks (map (Pretty.str o str_of_token)
-		 (rev (tl (rev toks)))) @
+                 (rev (tl (rev toks)))) @
           [Pretty.str "\""]);
     val expected =
       Pretty.strs ("Expected tokens: " :: map (quote o str_of_token) allowed);
   in
     error (Pretty.string_of (Pretty.blk (0, [msg, Pretty.fbrk, expected])))

 
               (*test if tk is a lookahead for a given minimum precedence*)
               fun reduction _ minPrec _ (Terminal _ :: _, _, prec:int) =
                     if prec >= minPrec then true
                     else false
-                | reduction tk minPrec checked 
+                | reduction tk minPrec checked
                             (Nonterminal (nt, nt_prec) :: _, _, prec) =
                   if prec >= minPrec andalso not (nt mem checked) then
                     let val chained = connected_with chains [nt] [nt];
                     in exists
                          (reduction tk nt_prec (chained @ checked))
                          (some_prods_for tk nt)
                     end
                   else false;
 
-              (*compute a list of allowed starting tokens 
+              (*compute a list of allowed starting tokens
                 for a list of nonterminals considering precedence*)
               fun get_starts [] result = result
                 | get_starts ((nt, minPrec:int) :: nts) result =
                   let fun get [] result = result
                         | get ((SOME tk, prods) :: ps) result =

                   in get_starts (chained @ nts)
                                 ((get nt_prods []) union result)
                   end;
 
               val nts =
-                List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => 
+                List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
                            SOME (a, prec) | _ => NONE)
                           (Array.sub (stateset, i-1));
               val allowed =
                 distinct (get_starts nts [] @
                   (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a

           Array.update (stateset, i + 1, sii);
           produce prods chains stateset (i + 1) cs c
        end));
 
 
-fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) 
+fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
                             l;
 
 fun earley prods tags chains startsymbol indata =
   let
     val start_tag = case Symtab.lookup (tags, startsymbol) of
                        SOME tag => tag
-                     | NONE   => error ("parse: Unknown startsymbol " ^ 
+                     | NONE   => error ("parse: Unknown startsymbol " ^
                                         quote startsymbol);
     val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal EndToken],
                "", 0)];
     val s = length indata + 1;
     val Estate = Array.array (s, []);