# HG changeset patch # User wenzelm # Date 1517070201 -3600 # Node ID fb87a0e9af21bb5849b3988d4f511c1f062a616e # Parent 6877af8bc18dc643a8cd59a86f46f88f8ca9ded5 tuned; diff -r 6877af8bc18d -r fb87a0e9af21 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Sat Jan 27 16:56:03 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Sat Jan 27 17:23:21 2018 +0100 @@ -622,7 +622,7 @@ (*get all productions of a NT and NTs chained to it which can be started by specified token*) -fun prods_for prods chains include_none tk nts = +fun prods_for (Gram {prods, chains, ...}) include_none tk nts = let fun token_assoc (list, key) = let @@ -641,9 +641,9 @@ in get_prods (connected_with chains nts nts) [] end; -fun PROCESSS prods chains Estate i c states = +fun PROCESSS gram Estate i c states = let - fun all_prods_for nt = prods_for prods chains true c [nt]; + fun all_prods_for nt = prods_for gram true c [nt]; fun processS _ [] (Si, Sii) = (Si, Sii) | processS used (S :: States) (Si, Sii) = @@ -689,7 +689,7 @@ in processS Inttab.empty states ([], []) end; -fun produce prods tags chains stateset i indata prev_token = +fun produce gram stateset i indata prev_token = (case Array.sub (stateset, i) of [] => let @@ -714,15 +714,15 @@ [] => s | c :: cs => let - val (si, sii) = PROCESSS prods chains stateset i c s; + val (si, sii) = PROCESSS gram stateset i c s; val _ = Array.update (stateset, i, si); val _ = Array.update (stateset, i + 1, sii); - in produce prods tags chains stateset (i + 1) cs c end)); + in produce gram stateset (i + 1) cs c end)); fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; -fun earley prods tags chains startsymbol indata = +fun earley (gram as Gram {tags, ...}) startsymbol indata = let val start_tag = (case Symtab.lookup tags startsymbol of @@ -733,18 +733,18 @@ val Estate = Array.array (s, []); val _ = Array.update (Estate, 0, S0); in - get_trees (produce prods tags chains Estate 0 indata Lexicon.eof) + get_trees (produce gram Estate 0 indata Lexicon.eof) end; -fun parse (Gram {tags, prods, chains, ...}) start toks = +fun parse gram start toks = let val end_pos = (case try List.last toks of NONE => Position.none | SOME (Lexicon.Token (_, _, (_, end_pos))) => end_pos); val r = - (case earley prods tags chains start (toks @ [Lexicon.mk_eof end_pos]) of + (case earley gram start (toks @ [Lexicon.mk_eof end_pos]) of [] => raise Fail "Inner syntax: no parse trees" | pts => pts); in r end;