performance tuning: cached non-persistent Parser.gram reduces heap size by approx. 1-4%;

--- 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;
 
 
 

--- 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;
 

--- 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 =