# HG changeset patch # User wenzelm # Date 1517307652 -3600 # Node ID d19686205f8684ad961bcb04ec72dd7e58fecf53 # Parent a7de81d847b07a00fb1165ce5da86ea7979f4ca3 tuned: more explicit types; diff -r a7de81d847b0 -r d19686205f86 src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Mon Jan 29 22:27:57 2018 +0100 +++ b/src/Pure/Syntax/parser.ML Tue Jan 30 11:20:52 2018 +0100 @@ -40,13 +40,36 @@ (*(([dependent_nts], [start_tokens]), [(start_token, [(rhs, name, prio)])])*) (*depent_nts is a list of all NTs whose lookahead depends on this NT's lookahead*) +type tags = nt_tag Symtab.table; +val tags_empty: tags = Symtab.empty; +fun tags_content (tags: tags) = sort_by #1 (Symtab.dest tags); +fun tags_lookup (tags: tags) = Symtab.lookup tags; +fun tags_insert tag (tags: tags) = Symtab.update_new tag tags; +fun tags_name (tags: tags) = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags))); + +type chains = unit Int_Graph.T; +fun chains_preds (chains: chains) = Int_Graph.immediate_preds chains; +fun chains_all_preds (chains: chains) = Int_Graph.all_preds chains; +fun chains_all_succs (chains: chains) = Int_Graph.all_succs chains; +val chains_empty: chains = Int_Graph.empty; +fun chains_member (chains: chains) = Int_Graph.is_edge chains; +fun chains_declare nt : chains -> chains = Int_Graph.default_node (nt, ()); +fun chains_insert (from, to) = + chains_declare from #> chains_declare to #> Int_Graph.add_edge (from, to); + +type lambdas = Inttab.set; +val lambdas_empty: lambdas = Inttab.empty; +fun lambdas_member (lambdas: lambdas) = Inttab.defined lambdas; +fun lambdas_insert nt : lambdas -> lambdas = Inttab.insert_set nt; +fun lambdas_fold f (lambdas: lambdas) = Inttab.fold (f o #1) lambdas; + datatype gram = Gram of {nt_count: int, prod_count: int, - tags: nt_tag Symtab.table, - chains: unit Int_Graph.T, - lambdas: Inttab.set, + tags: tags, + chains: chains, + lambdas: lambdas, 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 @@ -73,14 +96,10 @@ val (chain, new_chain, chains') = (case (pri, rhs) of (~1, [Nonterminal (from, ~1)]) => - if Int_Graph.is_edge chains (from, lhs) + if chains_member 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, ()))); + else (SOME from, true, chains_insert (from, lhs) chains) + | _ => (NONE, false, chains_declare lhs chains)); (*propagate new chain in lookahead and lambdas; added_starts is used later to associate existing @@ -103,28 +122,28 @@ copy_lookahead tos (if null new_tks then added else (to, new_tks) :: added) end; - val tos = Int_Graph.all_succs chains' [lhs]; + val tos = chains_all_succs chains' [lhs]; in (copy_lookahead tos [], - lambdas |> Inttab.defined lambdas lhs ? fold Inttab.insert_set tos) + lambdas |> lambdas_member lambdas lhs ? fold lambdas_insert tos) end; (*test if new production can produce lambda (rhs must either be empty or only consist of lambda NTs)*) val new_lambdas = if forall - (fn Nonterminal (id, _) => Inttab.defined lambdas' id + (fn Nonterminal (id, _) => lambdas_member lambdas' id | Terminal _ => false) rhs - then SOME (filter_out (Inttab.defined lambdas') (Int_Graph.all_succs chains' [lhs])) + then SOME (filter_out (lambdas_member lambdas') (chains_all_succs chains' [lhs])) else NONE; - val lambdas'' = fold Inttab.insert_set (these new_lambdas) lambdas'; + val lambdas'' = fold lambdas_insert (these new_lambdas) lambdas'; (*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 = - if Inttab.defined lambdas nt then + if lambdas_member lambdas nt then lookahead_dependency lambdas symbs (nt :: nts) else (NONE, nt :: nts); @@ -150,7 +169,7 @@ if member (op =) nts l then (*update production's lookahead*) let val new_lambda = - is_none tk andalso forall (Inttab.defined lambdas) nts; + is_none tk andalso forall (lambdas_member lambdas) nts; val new_tks = (if is_some tk then [the tk] else []) @@ -220,14 +239,14 @@ end; val (added_lambdas, added_starts') = process_nts dependent [] added_starts; - val added_lambdas' = filter_out (Inttab.defined lambdas) added_lambdas; + val added_lambdas' = filter_out (lambdas_member lambdas) added_lambdas; in propagate_lambda (ls @ added_lambdas') added_starts' - (fold Inttab.insert_set added_lambdas' lambdas) + (fold lambdas_insert added_lambdas' lambdas) end; in propagate_lambda - (Inttab.fold (fn (l, ()) => not (Inttab.defined lambdas l) ? cons l) lambdas'' []) + (lambdas_fold (fn l => not (lambdas_member lambdas l) ? cons l) lambdas'' []) added_starts lambdas'' end; @@ -304,7 +323,7 @@ end; val _ = add_nts start_nts; in - add_tks (Int_Graph.all_succs chains' [lhs]) [] prod_count + add_tks (chains_all_succs chains' [lhs]) [] prod_count end; (*associate productions with new lookaheads*) @@ -399,7 +418,7 @@ fun pretty_gram (Gram {tags, prods, chains, ...}) = let - val print_nt = the o Inttab.lookup (Inttab.make (map swap (Symtab.dest tags))); + val print_nt = tags_name tags; fun print_pri p = if p < 0 then "" else Symbol.make_sup ("(" ^ string_of_int p ^ ")"); fun pretty_symb (Terminal (Lexicon.Token (kind, s, _))) = @@ -413,11 +432,11 @@ fun pretty_prod (name, tag) = (fold (union (op =) o #2) (#2 (Vector.sub (prods, tag))) [] @ - map prod_of_chain (Int_Graph.immediate_preds chains tag)) + map prod_of_chain (chains_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))); - in maps pretty_prod (sort_by #1 (Symtab.dest tags)) end; + in maps pretty_prod (tags_content tags) end; @@ -427,9 +446,9 @@ Gram {nt_count = 0, prod_count = 0, - tags = Symtab.empty, - chains = Int_Graph.empty, - lambdas = Inttab.empty, + tags = tags_empty, + chains = chains_empty, + lambdas = lambdas_empty, prods = Vector.fromList [(([], []), [])]}; @@ -439,9 +458,9 @@ let (*Get tag for existing nonterminal or create a new one*) fun get_tag nt_count tags nt = - (case Symtab.lookup tags nt of + (case tags_lookup tags nt of SOME tag => (nt_count, tags, tag) - | NONE => (nt_count + 1, Symtab.update_new (nt, nt_count) tags, nt_count)); + | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); (*Convert symbols to the form used by the parser; delimiters and predefined terms are stored as terminals, @@ -620,7 +639,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 (Int_Graph.all_preds chains nts) [] end; + in get_prods (chains_all_preds chains nts) [] end; fun PROCESSS gram Estate i c states = @@ -707,7 +726,7 @@ fun earley (gram as Gram {tags, ...}) startsymbol indata = let val start_tag = - (case Symtab.lookup tags startsymbol of + (case tags_lookup tags startsymbol of SOME tag => tag | NONE => error ("Inner syntax: bad grammar root symbol " ^ quote startsymbol)); val S0 = [(~1, 0, [], [Nonterminal (start_tag, 0), Terminal Lexicon.eof], "", 0)];