# HG changeset patch # User wenzelm # Date 1727467734 -7200 # Node ID 5e2b1588c5cb141490a7c4336f9cb8332c4fd25c # Parent a9782ba039fb7a71fd72403d3a42ae9329eac138 minor performance tuning: proper table for parsetree list; tuned signature; diff -r a9782ba039fb -r 5e2b1588c5cb src/Pure/General/position.ML --- a/src/Pure/General/position.ML Fri Sep 27 20:29:38 2024 +0200 +++ b/src/Pure/General/position.ML Fri Sep 27 22:08:54 2024 +0200 @@ -61,6 +61,7 @@ val here: T -> string val here_list: T list -> string type range = T * T + val range_ord: range ord val no_range: range val no_range_position: T -> T val range_position: range -> T @@ -299,6 +300,8 @@ type range = T * T; +val range_ord = prod_ord ord ord; + val no_range = (none, none); fun no_range_position (Pos {line, offset, end_offset = _, props}) = diff -r a9782ba039fb -r 5e2b1588c5cb src/Pure/Syntax/lexicon.ML --- a/src/Pure/Syntax/lexicon.ML Fri Sep 27 20:29:38 2024 +0200 +++ b/src/Pure/Syntax/lexicon.ML Fri Sep 27 22:08:54 2024 +0200 @@ -33,6 +33,7 @@ val is_dummy: token -> bool val literal: string -> token val is_literal: token -> bool + val token_ord: token ord val tokens_match_ord: token ord val mk_eof: Position.T -> token val eof: token @@ -156,6 +157,17 @@ fun literal s = Token (literal_index, s, Position.no_range); fun is_literal tok = index_of_token tok = literal_index; + +(* order *) + +fun token_ord (Token (i, s, r), Token (i', s', r')) = + (case int_ord (i, i') of + EQUAL => + (case fast_string_ord (s, s') of + EQUAL => Position.range_ord (r, r') + | ord => ord) + | ord => ord); + fun tokens_match_ord toks = let val is = apply2 index_of_token toks in (case int_ord is of diff -r a9782ba039fb -r 5e2b1588c5cb src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Fri Sep 27 20:29:38 2024 +0200 +++ b/src/Pure/Syntax/parser.ML Fri Sep 27 22:08:54 2024 +0200 @@ -14,6 +14,7 @@ datatype parsetree = Node of string * parsetree list | Tip of Lexicon.token + val parsetree_ord: parsetree ord val pretty_parsetree: parsetree -> Pretty.T list val parse: gram -> string -> Lexicon.token list -> parsetree list end; @@ -72,7 +73,10 @@ val no_prec = ~1; -fun until_prec min max ((_, _, p): prod) = +fun upto_prec min max p = + (min = no_prec orelse p >= min) andalso (max = no_prec orelse p <= max); + +fun until_prec min max p = (min = no_prec orelse p >= min) andalso (max = no_prec orelse p < max); @@ -518,6 +522,28 @@ Node of string * parsetree list | Tip of Lexicon.token; +local + +fun cons_nr (Node _) = 0 + | cons_nr (Tip _) = 1; + +in + +fun parsetree_ord pts = + if pointer_eq pts then EQUAL + else + (case pts of + (Node (s, ts), Node (s', ts')) => + (case fast_string_ord (s, s') of + EQUAL => list_ord parsetree_ord (ts, ts') + | ord => ord) + | (Tip t, Tip t') => Lexicon.token_ord (t, t') + | _ => int_ord (apply2 cons_nr pts)); + +structure Parsetrees = Table(type key = parsetree list val ord = list_ord parsetree_ord); + +end; + fun pretty_parsetree (Node (c, pts)) = [Pretty.enclose "(" ")" (Pretty.breaks (Pretty.quote (Pretty.str c) :: maps pretty_parsetree pts))] @@ -536,28 +562,18 @@ local -(*Add parse tree to list and eliminate duplicates - saving the maximum precedence*) -fun conc (t: parsetree list, prec: int) [] = (NONE, [(t, prec)]) - | conc (t, prec) ((t', prec') :: ts) = - if t = t' then - (SOME prec', - if prec' >= prec then (t', prec') :: ts - else (t, prec) :: ts) - else - let val (n, ts') = conc (t, prec) ts - in (n, (t', prec') :: ts') end; +fun update_trees (A, (t, p)) used = + let + val (i: int, ts) = the (Inttab.lookup used A); + fun update ts' = Inttab.update (A, (i, ts')); + in + (case Parsetrees.lookup ts t of + NONE => (no_prec, update (Parsetrees.make [(t, p)]) used) + | SOME q => (q, if p > q then update (Parsetrees.update (t, p) ts) used else used)) + end; -(*Update entry in used*) -fun update_trees (A, t) used = - let - val (i, ts) = the (Inttab.lookup used A); - val (n, ts') = conc t ts; - in (n, Inttab.update (A, (i, ts')) used) end; - -(*Replace entry in used*) -fun update_prec (A, prec) = - Inttab.map_entry A (fn (_, ts) => (prec, ts)); +fun update_prec (A, p) used = + Inttab.map_entry A (fn (_, ts) => (p, ts)) used; fun head_nonterm pred : state -> bool = let @@ -567,13 +583,8 @@ | check _ = false; in check o #2 end; -fun get_states_lambda A max opt_min = - let - val pred = - (case opt_min of - NONE => (fn (B, p) => A = B andalso p <= max) - | SOME min => (fn (B, p) => A = B andalso p <= max andalso p > min)); - in filter (head_nonterm pred) end; +fun get_states_lambda A min max = + filter (head_nonterm (fn (B, p) => A = B andalso upto_prec min max p)); fun get_states A max_prec = filter (head_nonterm (fn (B, p) => A = B andalso p <= max_prec)); @@ -586,8 +597,8 @@ be started by specified token*) fun add_prods i tok nt ok = let - fun add (prod as (rhs, id, prod_prec)) = - if ok prod then cons ((nt, prod_prec, id, i), rhs, []) else I; + fun add (rhs, id, prod_prec) = + if ok prod_prec then cons ((nt, prod_prec, id, i), rhs, []) else I; fun token_prods prods = fold add (prods_lookup prods tok) #> fold add (prods_lookup prods Lexicon.dummy); @@ -606,15 +617,15 @@ SOME (used_prec, l) => (*nonterminal has been processed*) if used_prec <= min_prec then (*wanted precedence has been processed*) - (used, fold_rev movedot_lambda l States) + (used, Parsetrees.fold movedot_lambda l States) else (*wanted precedence hasn't been parsed yet*) let val States' = States |> add_prods i c nt (until_prec min_prec used_prec) - |> fold movedot_lambda l; + |> Parsetrees.fold movedot_lambda l; in (update_prec (nt, min_prec) used, States') end | NONE => (*nonterminal is parsed for the first time*) let val States' = States |> add_prods i c nt (until_prec min_prec no_prec); - in (Inttab.update (nt, (min_prec, [])) used, States') end); + in (Inttab.update (nt, (min_prec, Parsetrees.empty)) used, States') end); in process used' States' (S :: Si, Sii) end | Terminal a :: sa => (*scanner operation*) let @@ -627,13 +638,13 @@ in process used States (S :: Si, Sii') end | [] => (*completer operation*) let - val (A, prec, id, j) = info; + val (A, p, id, j) = info; val tt = if id = "" then ts else [Node (id, rev ts)]; val (used', Slist) = if j = i then (*lambda production?*) - let val (prec', used') = update_trees (A, (tt, prec)) used - in (used', get_states_lambda A prec prec' Si) end - else (used, get_states A prec (Array.nth stateset j)); + let val (q, used') = update_trees (A, (tt, p)) used + in (used', get_states_lambda A q p Si) end + else (used, get_states A p (Array.nth stateset j)); val States' = map (movedot_nonterm tt) Slist; in process used' (States' @ States) (S :: Si, Sii) end)