# HG changeset patch # User wenzelm # Date 1721295369 -7200 # Node ID 9a40ec7a202796024da642402b101be3caf86735 # Parent 1bc7eef961ff78f5864e17fe429edf9a749d6c5c more operations; diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Jul 18 11:02:08 2024 +0200 +++ b/src/Pure/General/table.ML Thu Jul 18 11:36:09 2024 +0200 @@ -66,7 +66,7 @@ val insert_set: key -> set -> set val remove_set: key -> set -> set val make_set: key list -> set - type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit} + type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int} val unsynchronized_cache: (key -> 'a) -> 'a cache_ops end; @@ -592,7 +592,7 @@ (* cache *) -type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit}; +type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}; fun unsynchronized_cache f = let @@ -609,7 +609,8 @@ Exn.Res y => (Unsynchronized.change cache1 (update (x, y)); y) | Exn.Exn exn => (Unsynchronized.change cache2 (update (x, exn)); Exn.reraise exn)))); fun reset () = (cache2 := empty; cache1 := empty); - in {apply = apply, reset = reset} end; + fun total_size () = size (! cache1) + size (! cache2); + in {apply = apply, reset = reset, size = total_size} end; (* ML pretty-printing *) diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/term_items.ML --- a/src/Pure/term_items.ML Thu Jul 18 11:02:08 2024 +0200 +++ b/src/Pure/term_items.ML Thu Jul 18 11:36:09 2024 +0200 @@ -34,7 +34,7 @@ val make1: key * 'a -> 'a table val make2: key * 'a -> key * 'a -> 'a table val make3: key * 'a -> key * 'a -> key * 'a -> 'a table - type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit}; + type 'a cache_ops = {apply: key -> 'a, reset: unit -> unit, size: unit -> int}; val unsynchronized_cache: (key -> 'a) -> 'a cache_ops type set = int table val add_set: key -> set -> set diff -r 1bc7eef961ff -r 9a40ec7a2027 src/Pure/zterm.ML --- a/src/Pure/zterm.ML Thu Jul 18 11:02:08 2024 +0200 +++ b/src/Pure/zterm.ML Thu Jul 18 11:36:09 2024 +0200 @@ -254,6 +254,7 @@ val typ_of_tvar: indexname * sort -> typ val typ_of: ztyp -> typ val reset_cache: theory -> theory + val check_cache: theory -> {ztyp: int, typ: int} option val ztyp_cache: theory -> typ -> ztyp val typ_cache: theory -> ztyp -> typ val zterm_cache: theory -> {zterm: term -> zterm, ztyp: typ -> ztyp} @@ -633,6 +634,10 @@ SOME (cache1, cache2) => (#reset cache1 (); #reset cache2 (); thy) | NONE => thy); +fun check_cache thy = + Data.get thy + |> Option.map (fn (cache1, cache2) => {ztyp = #size cache1 (), typ = #size cache2 ()}); + fun ztyp_cache thy = (case Data.get thy of SOME (cache, _) => cache