src/Pure/Syntax/parser.ML
changeset 19482 9f11af8f7ef9
parent 19305 5c16895d548b
child 20664 ffbc5a57191a
equal deleted inserted replaced
19481:a6205c6203ea 19482:9f11af8f7ef9
   416         val nt_prods =
   416         val nt_prods =
   417           Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @
   417           Library.foldl (op union) ([], map snd (snd (Array.sub (prods, tag)))) @
   418           map prod_of_chain ((these o AList.lookup (op =) chains) tag);
   418           map prod_of_chain ((these o AList.lookup (op =) chains) tag);
   419       in map (pretty_prod name) nt_prods end;
   419       in map (pretty_prod name) nt_prods end;
   420 
   420 
   421   in List.concat (map pretty_nt taglist) end;
   421   in maps pretty_nt taglist end;
   422 
   422 
   423 
   423 
   424 (** Operations on gramars **)
   424 (** Operations on gramars **)
   425 
   425 
   426 (*The mother of all grammars*)
   426 (*The mother of all grammars*)
   838                   in get_starts (chained @ nts)
   838                   in get_starts (chained @ nts)
   839                                 ((get nt_prods []) union result)
   839                                 ((get nt_prods []) union result)
   840                   end;
   840                   end;
   841 
   841 
   842               val nts =
   842               val nts =
   843                 List.mapPartial (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
   843                 map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) =>
   844                            SOME (a, prec) | _ => NONE)
   844                            SOME (a, prec) | _ => NONE)
   845                           (Array.sub (stateset, i-1));
   845                           (Array.sub (stateset, i-1));
   846               val allowed =
   846               val allowed =
   847                 distinct (op =) (get_starts nts [] @
   847                 distinct (op =) (get_starts nts [] @
   848                   (List.mapPartial (fn (_, _, _, Terminal a :: _, _, _) => SOME a
   848                   (map_filter (fn (_, _, _, Terminal a :: _, _, _) => SOME a
   849                                | _ => NONE)
   849                                | _ => NONE)
   850                              (Array.sub (stateset, i-1))));
   850                              (Array.sub (stateset, i-1))));
   851           in syntax_error (if prev_token = EndToken then indata
   851           in syntax_error (if prev_token = EndToken then indata
   852                            else prev_token :: indata) allowed
   852                            else prev_token :: indata) allowed
   853           end
   853           end
   860           Array.update (stateset, i + 1, sii);
   860           Array.update (stateset, i + 1, sii);
   861           produce prods chains stateset (i + 1) cs c
   861           produce prods chains stateset (i + 1) cs c
   862        end));
   862        end));
   863 
   863 
   864 
   864 
   865 fun get_trees l = List.mapPartial (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
   865 fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE)
   866                             l;
   866                             l;
   867 
   867 
   868 fun earley prods tags chains startsymbol indata =
   868 fun earley prods tags chains startsymbol indata =
   869   let
   869   let
   870     val start_tag = case Symtab.lookup tags startsymbol of
   870     val start_tag = case Symtab.lookup tags startsymbol of