# HG changeset patch # User wenzelm # Date 1301945759 -7200 # Node ID 1a2a53d03c3111fb31ead10756f142baefe7641d # Parent 183ea7f77b72d18a914045045e62de8c2eda27ee misc tuning and clarification; diff -r 183ea7f77b72 -r 1a2a53d03c31 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Mon Apr 04 16:35:46 2011 +0200 +++ b/src/Pure/Syntax/parser.ML Mon Apr 04 21:35:59 2011 +0200 @@ -9,7 +9,6 @@ type gram val empty_gram: gram val extend_gram: Syn_Ext.xprod list -> gram -> gram - val make_gram: Syn_Ext.xprod list -> gram val merge_gram: gram * gram -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = @@ -125,8 +124,8 @@ (*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 = + | lookahead_dependency _ (Terminal tk :: _) nts = (SOME tk, nts) + | lookahead_dependency lambdas (Nonterminal (nt, _) :: symbs) nts = if member (op =) lambdas nt then lookahead_dependency lambdas symbs (nt :: nts) else (NONE, nt :: nts); @@ -140,7 +139,7 @@ val (added_starts', lambdas') = let (*propagate added lambda NT*) - fun propagate_lambda [] added_starts lambdas= (added_starts, lambdas) + fun propagate_lambda [] added_starts lambdas = (added_starts, lambdas) | propagate_lambda (l :: ls) added_starts lambdas = let (*get lookahead for lambda NT*) @@ -256,10 +255,10 @@ (*add lhs NT to list of dependent NTs in lookahead*) fun add_nts [] = () | add_nts (nt :: nts) = - 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)) - end; + 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)) + end; (*add new start tokens to chained NTs' lookahead list; also store new production for lhs NT*) @@ -375,17 +374,18 @@ (*associate productions with new lookahead tokens*) val (tk_prods', nt_prods') = update_prods tk_prods ([], nt_prods); - val nt_prods' = - nt_prods' - |> (key = SOME unknown_start) ? AList.update (op =) (key, tk_prods'); + val nt_prods'' = + if key = SOME unknown_start then + AList.update (op =) (key, tk_prods') nt_prods' + else nt_prods'; val added_tks = subtract Lexicon.matching_tokens old_tks new_tks; in if null added_tks then - (Array.update (prods, nt, (lookahead, nt_prods')); + (Array.update (prods, nt, (lookahead, nt_prods'')); process_nts nts added) else - (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods')); + (Array.update (prods, nt, ((old_nts, added_tks @ old_tks), nt_prods'')); process_nts nts ((nt, added_tks) :: added)) end; @@ -429,6 +429,7 @@ in maps pretty_nt (sort_wrt fst (Symtab.dest tags)) end; + (** Operations on gramars **) val empty_gram = @@ -465,10 +466,10 @@ delimiters and predefined terms are stored as terminals, nonterminals are converted to integer tags*) fun symb_of [] nt_count tags result = (nt_count, tags, rev result) - | symb_of ((Syn_Ext.Delim s) :: ss) nt_count tags result = + | symb_of (Syn_Ext.Delim s :: ss) nt_count tags result = symb_of ss nt_count tags (Terminal (Lexicon.Token (Lexicon.Literal, s, Position.no_range)) :: result) - | symb_of ((Syn_Ext.Argument (s, p)) :: ss) nt_count tags result = + | symb_of (Syn_Ext.Argument (s, p) :: ss) nt_count tags result = let val (nt_count', tags', new_symb) = (case Lexicon.predef_term s of @@ -482,7 +483,7 @@ (*Convert list of productions by invoking symb_of for each of them*) fun prod_of [] nt_count prod_count tags result = (nt_count, prod_count, tags, result) - | prod_of ((Syn_Ext.XProd (lhs, xsymbs, const, pri)) :: ps) + | prod_of (Syn_Ext.XProd (lhs, xsymbs, const, pri) :: ps) nt_count prod_count tags result = let val (nt_count', tags', lhs_tag) = get_tag nt_count tags lhs; @@ -522,8 +523,6 @@ prods = Array.vector prods'} end; -fun make_gram xprods = extend_gram xprods empty_gram; - (*Merge two grammars*) fun merge_gram (gram_a, gram_b) = @@ -627,6 +626,7 @@ end; + (** Parser **) datatype parsetree = @@ -647,11 +647,11 @@ (*Get all rhss with precedence >= min_prec*) -fun get_RHS min_prec = filter (fn (_, _, prec:int) => prec >= min_prec); +fun get_RHS min_prec = filter (fn (_, _, prec: int) => prec >= min_prec); (*Get all rhss with precedence >= min_prec and < max_prec*) fun get_RHS' min_prec max_prec = - filter (fn (_, _, prec:int) => prec >= min_prec andalso prec < max_prec); + filter (fn (_, _, prec: int) => prec >= min_prec andalso prec < max_prec); (*Make states using a list of rhss*) fun mk_states i min_prec lhs_ID rhss = @@ -660,7 +660,7 @@ (*Add parse tree to list and eliminate duplicates saving the maximum precedence*) -fun conc (t: parsetree list, prec:int) [] = (NONE, [(t, prec)]) +fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) | conc (t, prec) ((t', prec') :: ts) = if t = t' then (SOME prec', @@ -741,7 +741,7 @@ fun get_prods [] result = result | get_prods (nt :: nts) result = let val nt_prods = snd (Vector.sub (prods, nt)); - in get_prods nts ((token_assoc (nt_prods, tk)) @ result) end; + in get_prods nts (token_assoc (nt_prods, tk) @ result) end; in get_prods (connected_with chains nts nts) [] end; @@ -763,22 +763,18 @@ else (*wanted precedence hasn't been parsed yet*) let val tk_prods = all_prods_for nt; - - val States' = mk_states i min_prec nt - (get_RHS' min_prec used_prec tk_prods); - in (update_prec (nt, min_prec) used, - movedot_lambda S l @ States') - end - + val States' = + mk_states i min_prec nt (get_RHS' min_prec used_prec tk_prods); + in (update_prec (nt, min_prec) used, movedot_lambda S l @ States') end | NONE => (*nonterminal is parsed for the first time*) let val tk_prods = all_prods_for nt; val States' = mk_states i min_prec nt (get_RHS min_prec tk_prods); in ((nt, (min_prec, [])) :: used, States') end); - val dummy = + val _ = if not (! warned) andalso - length (new_states @ States) > Config.get ctxt branching_level then + length new_states + length States > Config.get ctxt branching_level then (Context_Position.if_visible ctxt warning "Currently parsed expression could be extremely ambiguous"; warned := true) @@ -832,16 +828,16 @@ end | s => (case indata of - [] => Array.sub (stateset, i) - | c :: cs => - let val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s; - in Array.update (stateset, i, si); - Array.update (stateset, i + 1, sii); - produce ctxt warned prods tags chains stateset (i + 1) cs c - end)); + [] => Array.sub (stateset, i) + | c :: cs => + let + val (si, sii) = PROCESSS ctxt warned prods chains stateset i c s; + val _ = Array.update (stateset, i, si); + val _ = Array.update (stateset, i + 1, sii); + in produce ctxt warned prods tags chains stateset (i + 1) cs c end)); -fun get_trees l = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) l; +fun get_trees states = map_filter (fn (_, _, [pt], _, _, _) => SOME pt | _ => NONE) states; fun earley ctxt prods tags chains startsymbol indata = let diff -r 183ea7f77b72 -r 1a2a53d03c31 src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Mon Apr 04 16:35:46 2011 +0200 +++ b/src/Pure/Syntax/syntax.ML Mon Apr 04 21:35:59 2011 +0200 @@ -562,7 +562,7 @@ Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syn_Ext.delims_of input') else lexicon, - gram = if changed then Parser.make_gram input' else gram, + gram = if changed then Parser.extend_gram input' Parser.empty_gram else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab,