# HG changeset patch # User wenzelm # Date 1517079457 -3600 # Node ID add9a9f6a29020846de737d2014b7245b5fc38ad # Parent 656720e8f44369e28c0b51bcb68a5cfdf313c075 explicit graph for chains, which contains all nts as nodes; diff -r 656720e8f443 -r add9a9f6a290 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Sat Jan 27 17:27:06 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Sat Jan 27 19:57:37 2018 +0100 @@ -45,12 +45,12 @@ {nt_count: int, prod_count: int, tags: nt_tag Symtab.table, - chains: (nt_tag * nt_tag list) list, (*[(to, [from])]*) + chains: unit Int_Graph.T, lambdas: nt_tag list, prods: nt_gram Vector.vector}; (*"tags" is used to map NT names (i.e. strings) to tags; chain productions are not stored as normal productions - but instead as an entry in "chains"; + but instead as an entry in "chains": from -> to; lambda productions are stored as normal productions and also as an entry in "lambdas"*) @@ -64,41 +64,32 @@ fun get_start (tok :: _) = tok | get_start [] = unknown_start; -(*get all NTs that are connected with a list of NTs*) -fun connected_with _ ([]: nt_tag list) relatives = relatives - | connected_with chains (root :: roots) relatives = - let val branches = subtract (op =) relatives (these (AList.lookup (op =) chains root)); - in connected_with chains (branches @ roots) (branches @ relatives) end; - (*convert productions to grammar; - N.B. that the chains parameter has the form [(from, [to])]; 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, _, pri)) :: ps) = let - val chain_from = + (*store chain if it does not already exist*) + val (chain, new_chain, chains') = (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 = these (AList.lookup (op =) chains from) in - if member (op =) old_tos lhs then (NONE, chains) - else (SOME from, AList.update (op =) (from, insert (op =) lhs old_tos) chains) - end); + (~1, [Nonterminal (from, ~1)]) => + if Int_Graph.is_edge chains (from, lhs) + then (SOME from, false, chains) + else (SOME from, true, + chains + |> Int_Graph.default_node (from, ()) + |> Int_Graph.default_node (lhs, ()) + |> Int_Graph.add_edge (from, lhs)) + | _ => (NONE, false, chains |> Int_Graph.default_node (lhs, ()))); (*propagate new chain in lookahead and lambda lists; added_starts is used later to associate existing productions with new starting tokens*) val (added_starts, lambdas') = - if is_none new_chain then ([], lambdas) + if not new_chain then ([], lambdas) else let (*lookahead of chain's source*) - val ((_, from_tks), _) = Array.sub (prods, the new_chain); + val ((_, from_tks), _) = Array.sub (prods, the chain); (*copy from's lookahead to chain's destinations*) fun copy_lookahead [] added = added @@ -112,7 +103,7 @@ copy_lookahead tos (if null new_tks then added else (to, new_tks) :: added) end; - val tos = connected_with chains' [lhs] [lhs]; + val tos = Int_Graph.all_succs chains' [lhs]; in (copy_lookahead tos [], union (op =) (if member (op =) lambdas lhs then tos else []) lambdas) @@ -124,7 +115,7 @@ if forall (fn Nonterminal (id, _) => member (op =) lambdas' id | Terminal _ => false) rhs - then (true, union (op =) (connected_with chains' [lhs] [lhs]) lambdas') + then (true, union (op =) (Int_Graph.all_succs chains' [lhs]) lambdas') else (false, lambdas'); (*list optional terminal and all nonterminals on which the lookahead @@ -237,7 +228,7 @@ (*insert production into grammar*) val (added_starts', _) = - if is_some chain_from + if is_some chain then (added_starts', prod_count) (*don't store chain production*) else let @@ -308,7 +299,7 @@ end; val _ = add_nts start_nts; in - add_tks (connected_with chains' [lhs] [lhs]) [] prod_count + add_tks (Int_Graph.all_succs chains' [lhs]) [] prod_count end; (*associate productions with new lookaheads*) @@ -417,7 +408,7 @@ fun pretty_prod (name, tag) = (fold (union (op =) o #2) (#2 (Vector.sub (prods, tag))) [] @ - map prod_of_chain (these (AList.lookup (op =) chains tag))) + map prod_of_chain (Int_Graph.immediate_preds chains tag)) |> map (fn (symbs, const, p) => Pretty.block (Pretty.breaks (Pretty.str (name ^ print_pri p ^ " =") :: map pretty_symb symbs @ pretty_const const))); @@ -431,22 +422,12 @@ Gram {nt_count = 0, prod_count = 0, - tags = Symtab.empty, chains = [], + tags = Symtab.empty, + chains = Int_Graph.empty, lambdas = [], prods = Vector.fromList [(([], []), [])]}; -(*Invert list of chain productions*) -fun inverse_chains [] result = result - | inverse_chains ((root, branches: nt_tag list) :: cs) result = - let - fun add ([]: nt_tag list) result = result - | add (id :: ids) result = - let val old = these (AList.lookup (op =) result id); - in add ids (AList.update (op =) (id, root :: old) result) end; - in inverse_chains cs (add branches result) end; - - (*Add productions to a grammar*) fun extend_gram [] gram = gram | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = @@ -501,13 +482,8 @@ else (([], []), []); in Array.tabulate (nt_count', get_prod) end; - val fromto_chains = inverse_chains chains []; - (*Add new productions to old ones*) - val (fromto_chains', lambdas', _) = - add_prods prods' fromto_chains lambdas NONE xprods'; - - val chains' = inverse_chains fromto_chains' []; + val (chains', lambdas', _) = add_prods prods' chains lambdas NONE xprods'; in Gram {nt_count = nt_count', @@ -639,7 +615,7 @@ | 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 (connected_with chains nts nts) [] end; + in get_prods (Int_Graph.all_preds chains nts) [] end; fun PROCESSS gram Estate i c states =