# HG changeset patch # User wenzelm # Date 1683660723 -7200 # Node ID f906f7f83daee0ad369291978a2aebaa24e42d48 # Parent 620d0a5d61a2e9e6516fcfbda4d04bb740ba9d66 performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%; diff -r 620d0a5d61a2 -r f906f7f83dae src/Pure/Syntax/parser.ML --- a/src/Pure/Syntax/parser.ML Tue May 09 20:32:49 2023 +0200 +++ b/src/Pure/Syntax/parser.ML Tue May 09 21:32:03 2023 +0200 @@ -9,8 +9,7 @@ sig type gram val empty_gram: gram - val extend_gram: Syntax_Ext.xprod list -> gram -> gram - val make_gram: Syntax_Ext.xprod list -> gram + val make_gram: Syntax_Ext.xprod list -> Syntax_Ext.xprod list -> gram option -> gram val pretty_gram: gram -> Pretty.T list datatype parsetree = Node of string * parsetree list | @@ -425,68 +424,68 @@ lambdas = nts_empty, prods = Vector.fromList [nt_gram_empty]}; - -(*Add productions to a grammar*) -fun extend_gram [] gram = gram - | extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = - let - (*Get tag for existing nonterminal or create a new one*) - fun get_tag nt_count tags nt = - (case tags_lookup tags nt of - SOME tag => (nt_count, tags, tag) - | NONE => (nt_count + 1, tags_insert (nt, nt_count) tags, nt_count)); +fun extend_gram xprods (Gram {nt_count, prod_count, tags, chains, lambdas, prods}) = + let + (*Get tag for existing nonterminal or create a new one*) + fun get_tag nt_count tags nt = + (case tags_lookup tags nt of + SOME tag => (nt_count, tags, tag) + | 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, - nonterminals are converted to integer tags*) - fun symb_of [] nt_count tags result = (nt_count, tags, rev result) - | symb_of (Syntax_Ext.Delim s :: ss) nt_count tags result = - symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) - | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = - let - val (nt_count', tags', new_symb) = - (case Lexicon.get_terminal s of - NONE => - let val (nt_count', tags', s_tag) = get_tag nt_count tags s; - in (nt_count', tags', Nonterminal (s_tag, p)) end - | SOME tk => (nt_count, tags, Terminal tk)); - in symb_of ss nt_count' tags' (new_symb :: result) end - | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; + (*Convert symbols to the form used by the parser; + 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 (Syntax_Ext.Delim s :: ss) nt_count tags result = + symb_of ss nt_count tags (Terminal (Lexicon.literal s) :: result) + | symb_of (Syntax_Ext.Argument (s, p) :: ss) nt_count tags result = + let + val (nt_count', tags', new_symb) = + (case Lexicon.get_terminal s of + NONE => + let val (nt_count', tags', s_tag) = get_tag nt_count tags s; + in (nt_count', tags', Nonterminal (s_tag, p)) end + | SOME tk => (nt_count, tags, Terminal tk)); + in symb_of ss nt_count' tags' (new_symb :: result) end + | symb_of (_ :: ss) nt_count tags result = symb_of ss nt_count tags result; - (*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 (Syntax_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; - val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; - in - prod_of ps nt_count'' (prod_count + 1) tags'' - ((lhs_tag, (prods, const, pri)) :: result) - end; + (*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 (Syntax_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; + val (nt_count'', tags'', prods) = symb_of xsymbs nt_count' tags' []; + in + prod_of ps nt_count'' (prod_count + 1) tags'' + ((lhs_tag, (prods, const, pri)) :: result) + end; - val (nt_count', prod_count', tags', xprods') = - prod_of xprods nt_count prod_count tags []; + val (nt_count', prod_count', tags', xprods') = + prod_of xprods nt_count prod_count tags []; - val array_prods' = - Array.tabulate (nt_count', fn i => - if i < nt_count then Vector.nth prods i - else nt_gram_empty); + val array_prods' = + Array.tabulate (nt_count', fn i => + if i < nt_count then Vector.nth prods i + else nt_gram_empty); - val (chains', lambdas') = - (chains, lambdas) |> fold (add_production array_prods') xprods'; - in - Gram - {nt_count = nt_count', - prod_count = prod_count', - tags = tags', - chains = chains', - lambdas = lambdas', - prods = Array.vector array_prods'} - end; + val (chains', lambdas') = + (chains, lambdas) |> fold (add_production array_prods') xprods'; + in + Gram + {nt_count = nt_count', + prod_count = prod_count', + tags = tags', + chains = chains', + lambdas = lambdas', + prods = Array.vector array_prods'} + end; -fun make_gram xprods = extend_gram xprods empty_gram; +fun make_gram [] _ (SOME gram) = gram + | make_gram new_xprods _ (SOME gram) = extend_gram new_xprods gram + | make_gram [] [] NONE = empty_gram + | make_gram new_xprods old_xprods NONE = extend_gram (new_xprods @ old_xprods) empty_gram; diff -r 620d0a5d61a2 -r f906f7f83dae src/Pure/Syntax/syntax.ML --- a/src/Pure/Syntax/syntax.ML Tue May 09 20:32:49 2023 +0200 +++ b/src/Pure/Syntax/syntax.ML Tue May 09 21:32:03 2023 +0200 @@ -73,7 +73,6 @@ val pretty_flexpair: Proof.context -> term * term -> Pretty.T list type syntax val eq_syntax: syntax * syntax -> bool - val force_syntax: syntax -> unit datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int} val get_approx: syntax -> string -> approx option val lookup_const: syntax -> string -> string option @@ -409,7 +408,7 @@ Syntax of { input: Syntax_Ext.xprod list, lexicon: Scan.lexicon, - gram: Parser.gram lazy, + gram: Parser.gram Synchronized.cache, consts: string Symtab.table, prmodes: string list, parse_ast_trtab: ((Proof.context -> Ast.ast list -> Ast.ast) * stamp) Symtab.table, @@ -422,8 +421,6 @@ fun eq_syntax (Syntax (_, s1), Syntax (_, s2)) = s1 = s2; -fun force_syntax (Syntax ({gram, ...}, _)) = ignore (Lazy.force gram); - datatype approx = Prefix of string | Infix of {assoc: Printer.assoc, delim: string, pri: int}; fun get_approx (Syntax ({prtabs, ...}, _)) c = (case Printer.get_infix prtabs c of @@ -437,7 +434,7 @@ fun lookup_const (Syntax ({consts, ...}, _)) = Symtab.lookup consts; fun is_keyword (Syntax ({lexicon, ...}, _)) = Scan.is_literal lexicon o Symbol.explode; fun tokenize (Syntax ({lexicon, ...}, _)) = Lexicon.tokenize lexicon; -fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Lazy.force gram); +fun parse (Syntax ({gram, ...}, _)) = Parser.parse (Synchronized.cache_eval gram); fun parse_ast_translation (Syntax ({parse_ast_trtab, ...}, _)) = lookup_tr parse_ast_trtab; fun parse_translation (Syntax ({parse_trtab, ...}, _)) = lookup_tr parse_trtab; @@ -452,13 +449,20 @@ val mode_default = ("", true); val mode_input = (Print_Mode.input, true); +fun extend_gram new_xprods old_xprods gram = + Synchronized.cache (fn () => + Parser.make_gram new_xprods old_xprods (Synchronized.cache_peek gram)); + +fun new_gram new_xprods = + Synchronized.cache (fn () => Parser.make_gram new_xprods [] NONE); + (* empty_syntax *) val empty_syntax = Syntax ({input = [], lexicon = Scan.empty_lexicon, - gram = Lazy.value Parser.empty_gram, + gram = Synchronized.cache (fn () => Parser.empty_gram), consts = Symtab.empty, prmodes = [], parse_ast_trtab = Symtab.empty, @@ -491,7 +495,7 @@ Syntax ({input = new_xprods @ input, lexicon = fold Scan.extend_lexicon (Syntax_Ext.delims_of new_xprods) lexicon, - gram = if null new_xprods then gram else Lazy.map (Parser.extend_gram new_xprods) gram, + gram = if null new_xprods then gram else extend_gram new_xprods input gram, consts = fold update_const consts2 consts1, prmodes = insert (op =) mode prmodes, parse_ast_trtab = @@ -520,7 +524,7 @@ Syntax ({input = input', lexicon = if changed then Scan.make_lexicon (Syntax_Ext.delims_of input') else lexicon, - gram = if changed then Lazy.value (Parser.make_gram input') else gram, + gram = if changed then new_gram input' else gram, consts = consts, prmodes = prmodes, parse_ast_trtab = remove_trtab (if_inout parse_ast_translation) parse_ast_trtab, @@ -557,7 +561,7 @@ else let val input' = new_xprods2 @ input1; - val gram' = Lazy.lazy_name "Syntax.merge_syntax" (fn () => Parser.make_gram input'); + val gram' = new_gram input'; in (input', gram') end); in Syntax @@ -592,7 +596,7 @@ in [Pretty.block (Pretty.breaks (Pretty.str "lexicon:" :: map (Pretty.quote o Pretty.keyword1) (Scan.dest_lexicon lexicon))), - Pretty.big_list "productions:" (Parser.pretty_gram (Lazy.force gram)), + Pretty.big_list "productions:" (Parser.pretty_gram (Synchronized.cache_eval gram)), pretty_strs_qs "print modes:" prmodes'] end; diff -r 620d0a5d61a2 -r f906f7f83dae src/Pure/theory.ML --- a/src/Pure/theory.ML Tue May 09 20:32:49 2023 +0200 +++ b/src/Pure/theory.ML Tue May 09 21:32:03 2023 +0200 @@ -189,7 +189,6 @@ |> Sign.init_naming |> Sign.local_path |> apply_wrappers wrappers - |> tap (Syntax.force_syntax o Sign.syn_of) end; fun end_theory thy =