# HG changeset patch # User wenzelm # Date 1201382047 -3600 # Node ID 26f1e4c172c3640efec1b685c0ff54babc17a8fb # Parent 8d69087f6a4b1c02864ad10b72ddb89539226640 syntax error: reduced spam -- print expected nonterminals instead of terminals; tuned pretty_gram; diff -r 8d69087f6a4b -r 26f1e4c172c3 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Sat Jan 26 20:01:37 2008 +0100 +++ b/src/Pure/Syntax/parser.ML Sat Jan 26 22:14:07 2008 +0100 @@ -53,6 +53,9 @@ lambda productions are stored as normal productions and also as an entry in "lambdas"*) +fun reverted_tags (tags: nt_tag Symtab.table) = + the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags))); + val UnknownStart = EndToken; (*productions for which no starting token is known yet are associated with this token*) @@ -392,13 +395,11 @@ let fun pretty_name name = [Pretty.str (name ^ " =")]; - val taglist = Symtab.dest tags; + val nt_name = reverted_tags tags; fun pretty_symb (Terminal (Token s)) = Pretty.quote (Pretty.str s) | pretty_symb (Terminal tok) = Pretty.str (str_of_token tok) - | pretty_symb (Nonterminal (tag, p)) = - let val name = fst (the (find_first (fn (n, t) => t = tag) taglist)); - in Pretty.str (name ^ "[" ^ string_of_int p ^ "]") end; + | pretty_symb (Nonterminal (tag, p)) = Pretty.str (nt_name tag ^ "[" ^ string_of_int p ^ "]"); fun pretty_const "" = [] | pretty_const c = [Pretty.str ("=> " ^ Library.quote c)]; @@ -418,7 +419,7 @@ map prod_of_chain ((these o AList.lookup (op =) chains) tag); in map (pretty_prod name) nt_prods end; - in maps pretty_nt taglist end; + in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end; (** Operations on gramars **) @@ -784,72 +785,30 @@ in processS [] states ([], []) end; -fun syntax_error toks allowed = - let - 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)))) @ - [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]))) - end; - -fun produce warned prods chains stateset i indata prev_token = - (*prev_token is used for error messages*) +fun produce warned prods tags chains stateset i indata prev_token = (case Array.sub (stateset, i) of - [] => let fun some_prods_for tk nt = prods_for prods chains false tk [nt]; + [] => + let + val toks = + if prev_token = EndToken then indata + else prev_token :: indata; - (*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 - (Nonterminal (nt, nt_prec) :: _, _, prec) = - if prec >= minPrec andalso not (member (op =) checked nt) 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; + val nt_name = reverted_tags tags; + val nts = + fold (fn (_, _, _, Nonterminal nt :: _, _, _) => insert (op =) nt | _ => I) + (Array.sub (stateset, i - 1)) [] + |> map (fn (a, prec) => nt_name a ^ "(" ^ signed_string_of_int prec ^ ")"); - (*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 = - if not (null prods) andalso - exists (reduction tk minPrec [nt]) prods - then get ps (tk :: result) - else get ps result - | get ((NONE, _) :: ps) result = get ps result; - - val (_, nt_prods) = Array.sub (prods, nt); - - val chained = map (fn nt => (nt, minPrec)) - ((these o AList.lookup (op =) chains) nt); - in get_starts (chained @ nts) - (gen_union (op =) (get nt_prods [], result)) - end; - - val nts = - map_filter (fn (_, _, _, Nonterminal (a, prec) :: _, _, _) => - SOME (a, prec) | _ => NONE) - (Array.sub (stateset, i-1)); - val allowed = - distinct (op =) (get_starts nts [] @ - (map_filter (fn (_, _, _, Terminal a :: _, _, _) => SOME a - | _ => NONE) - (Array.sub (stateset, i-1)))); - in syntax_error (if prev_token = EndToken then indata - else prev_token :: indata) allowed - 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) (#1 (split_last toks))) @ + [Pretty.str "\""])) :: + (if null nts then [] + else [Pretty.block + (Pretty.str "Expected syntax categories: " :: Pretty.commas (map Pretty.str nts))]); + in error (Pretty.string_of (Pretty.chunks msg)) end | s => (case indata of [] => Array.sub (stateset, i) @@ -857,7 +816,7 @@ let val (si, sii) = PROCESSS warned prods chains stateset i c s; in Array.update (stateset, i, si); Array.update (stateset, i + 1, sii); - produce warned prods chains stateset (i + 1) cs c + produce warned prods tags chains stateset (i + 1) cs c end)); @@ -876,7 +835,7 @@ val Estate = Array.array (s, []); in Array.update (Estate, 0, S0); - get_trees (produce (ref false) prods chains Estate 0 indata EndToken) + get_trees (produce (ref false) prods tags chains Estate 0 indata EndToken) end;