# HG changeset patch # User wenzelm # Date 1701374140 -3600 # Node ID db7d6dcaeb32f6ee3c1ee60152dd0216fce41647 # Parent 06f380099b2ef5653b731942e92a88e0ee3dbcf5# Parent 48187f1a615e0f91e2f046ae4d20dab952b53ebd merged diff -r 06f380099b2e -r db7d6dcaeb32 src/Pure/General/table.ML --- a/src/Pure/General/table.ML Thu Nov 30 18:24:51 2023 +0100 +++ b/src/Pure/General/table.ML Thu Nov 30 20:55:40 2023 +0100 @@ -83,8 +83,8 @@ datatype 'a table = Empty | Leaf1 of key * 'a | - Leaf2 of key * 'a * key * 'a | - Leaf3 of key * 'a * key * 'a * key * 'a | + Leaf2 of (key * 'a) * (key * 'a) | + Leaf3 of (key * 'a) * (key * 'a) * (key * 'a) | Branch2 of 'a table * (key * 'a) * 'a table | Branch3 of 'a table * (key * 'a) * 'a table * (key * 'a) * 'a table | Size of int * 'a table; @@ -92,30 +92,27 @@ fun make2 (Empty, e, Empty) = Leaf1 e | make2 (Branch2 (Empty, e1, Empty), e2, right) = make2 (Leaf1 e1, e2, right) | make2 (left, e1, Branch2 (Empty, e2, Empty)) = make2 (left, e1, Leaf1 e2) - | make2 (Branch3 (Empty, (k1, x1), Empty, (k2, x2), Empty), e3, right) = - make2 (Leaf2 (k1, x1, k2, x2), e3, right) - | make2 (left, e1, Branch3 (Empty, (k2, x2), Empty, (k3, x3), Empty)) = - make2 (left, e1, Leaf2 (k2, x2, k3, x3)) - | make2 (Leaf1 (k1, x1), (k2, x2), Empty) = Leaf2 (k1, x1, k2, x2) - | make2 (Empty, (k1, x1), Leaf1 (k2, x2)) = Leaf2 (k1, x1, k2, x2) - | make2 (Leaf1 (k1, x1), (k2, x2), Leaf1 (k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3) - | make2 (Leaf2 (k1, x1, k2, x2), (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3) - | make2 (Empty, (k1, x1), Leaf2 (k2, x2, k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3) + | make2 (Branch3 (Empty, e1, Empty, e2, Empty), e3, right) = make2 (Leaf2 (e1, e2), e3, right) + | make2 (left, e1, Branch3 (Empty, e2, Empty, e3, Empty)) = make2 (left, e1, Leaf2 (e2, e3)) + | make2 (Leaf1 e1, e2, Empty) = Leaf2 (e1, e2) + | make2 (Empty, e1, Leaf1 e2) = Leaf2 (e1, e2) + | make2 (Leaf1 e1, e2, Leaf1 e3) = Leaf3 (e1, e2, e3) + | make2 (Leaf2 (e1, e2), e3, Empty) = Leaf3 (e1, e2, e3) + | make2 (Empty, e1, Leaf2 (e2, e3)) = Leaf3 (e1, e2, e3) | make2 arg = Branch2 arg; -fun make3 (Empty, (k1, x1), Empty, (k2, x2), Empty) = Leaf2 (k1, x1, k2, x2) +fun make3 (Empty, e1, Empty, e2, Empty) = Leaf2 (e1, e2) | make3 (Branch2 (Empty, e1, Empty), e2, mid, e3, right) = make3 (Leaf1 e1, e2, mid, e3, right) | make3 (left, e1, Branch2 (Empty, e2, Empty), e3, right) = make3 (left, e1, Leaf1 e2, e3, right) | make3 (left, e1, mid, e2, Branch2 (Empty, e3, Empty)) = make3 (left, e1, mid, e2, Leaf1 e3) - | make3 (Leaf1 (k1, x1), (k2, x2), Empty, (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3) - | make3 (Empty, (k1, x1), Leaf1 (k2, x2), (k3, x3), Empty) = Leaf3 (k1, x1, k2, x2, k3, x3) - | make3 (Empty, (k1, x1), Empty, (k2, x2), Leaf1 (k3, x3)) = Leaf3 (k1, x1, k2, x2, k3, x3) + | make3 (Leaf1 e1, e2, Empty, e3, Empty) = Leaf3 (e1, e2, e3) + | make3 (Empty, e1, Leaf1 e2, e3, Empty) = Leaf3 (e1, e2, e3) + | make3 (Empty, e1, Empty, e2, Leaf1 e3) = Leaf3 (e1, e2, e3) | make3 arg = Branch3 arg; fun unmake (Leaf1 e) = Branch2 (Empty, e, Empty) - | unmake (Leaf2 (k1, x1, k2, x2)) = Branch3 (Empty, (k1, x1), Empty, (k2, x2), Empty) - | unmake (Leaf3 (k1, x1, k2, x2, k3, x3)) = - Branch2 (Branch2 (Empty, (k1, x1), Empty), (k2, x2), Branch2 (Empty, (k3, x3), Empty)) + | unmake (Leaf2 (e1, e2)) = Branch3 (Empty, e1, Empty, e2, Empty) + | unmake (Leaf3 (e1, e2, e3)) = Branch2 (Branch2 (Empty, e1, Empty), e2, Branch2 (Empty, e3, Empty)) | unmake (Size (_, arg)) = arg | unmake arg = arg; @@ -167,14 +164,16 @@ fun map_table f = let + fun apply (k, x) = (k, f k x); + fun map Empty = Empty - | map (Leaf1 (k, x)) = Leaf1 (k, f k x) - | map (Leaf2 (k1, x1, k2, x2)) = Leaf2 (k1, f k1 x1, k2, f k2 x2) - | map (Leaf3 (k1, x1, k2, x2, k3, x3)) = Leaf3 (k1, f k1 x1, k2, f k2 x2, k3, f k3 x3) - | map (Branch2 (left, (k, x), right)) = - Branch2 (map left, (k, f k x), map right) - | map (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = - Branch3 (map left, (k1, f k1 x1), map mid, (k2, f k2 x2), map right) + | map (Leaf1 e) = Leaf1 (apply e) + | map (Leaf2 (e1, e2)) = Leaf2 (apply e1, apply e2) + | map (Leaf3 (e1, e2, e3)) = Leaf3 (apply e1, apply e2, apply e3) + | map (Branch2 (left, e, right)) = + Branch2 (map left, apply e, map right) + | map (Branch3 (left, e1, mid, e2, right)) = + Branch3 (map left, apply e1, map mid, apply e2, map right) | map (Size (m, arg)) = Size (m, map arg); in map end; @@ -182,8 +181,8 @@ let fun fold Empty a = a | fold (Leaf1 e) a = f e a - | fold (Leaf2 (k1, x1, k2, x2)) a = f (k2, x2) (f (k1, x1) a) - | fold (Leaf3 (k1, x1, k2, x2, k3, x3)) a = f (k3, x3) (f (k2, x2) (f (k1, x1) a)) + | fold (Leaf2 (e1, e2)) a = f e2 (f e1 a) + | fold (Leaf3 (e1, e2, e3)) a = f e3 (f e2 (f e1 a)) | fold (Branch2 (left, e, right)) a = fold right (f e (fold left a)) | fold (Branch3 (left, e1, mid, e2, right)) a = @@ -195,8 +194,8 @@ let fun fold_rev Empty a = a | fold_rev (Leaf1 e) a = f e a - | fold_rev (Leaf2 (k1, x1, k2, x2)) a = f (k1, x1) (f (k2, x2) a) - | fold_rev (Leaf3 (k1, x1, k2, x2, k3, x3)) a = f (k1, x1) (f (k2, x2) (f (k3, x3) a)) + | fold_rev (Leaf2 (e1, e2)) a = f e1 (f e2 a) + | fold_rev (Leaf3 (e1, e2, e3)) a = f e1 (f e2 (f e3 a)) | fold_rev (Branch2 (left, e, right)) a = fold_rev left (f e (fold_rev right a)) | fold_rev (Branch3 (left, e1, mid, e2, right)) a = @@ -212,8 +211,8 @@ fun min Empty = NONE | min (Leaf1 e) = SOME e - | min (Leaf2 (k, x, _, _)) = SOME (k, x) - | min (Leaf3 (k, x, _, _, _, _)) = SOME (k, x) + | min (Leaf2 (e, _)) = SOME e + | min (Leaf3 (e, _, _)) = SOME e | min (Branch2 (Empty, e, _)) = SOME e | min (Branch3 (Empty, e, _, _, _)) = SOME e | min (Branch2 (left, _, _)) = min left @@ -222,8 +221,8 @@ fun max Empty = NONE | max (Leaf1 e) = SOME e - | max (Leaf2 (_, _, k, x)) = SOME (k, x) - | max (Leaf3 (_, _, _, _, k, x)) = SOME (k, x) + | max (Leaf2 (_, e)) = SOME e + | max (Leaf3 (_, _, e)) = SOME e | max (Branch2 (_, e, Empty)) = SOME e | max (Branch3 (_, _, _, e, Empty)) = SOME e | max (Branch2 (_, _, right)) = max right @@ -237,9 +236,8 @@ let fun ex Empty = false | ex (Leaf1 e) = pred e - | ex (Leaf2 (k1, x1, k2, x2)) = pred (k1, x1) orelse pred (k2, x2) - | ex (Leaf3 (k1, x1, k2, x2, k3, x3)) = - pred (k1, x1) orelse pred (k2, x2) orelse pred (k3, x3) + | ex (Leaf2 (e1, e2)) = pred e1 orelse pred e2 + | ex (Leaf3 (e1, e2, e3)) = pred e1 orelse pred e2 orelse pred e3 | ex (Branch2 (left, e, right)) = ex left orelse pred e orelse ex right | ex (Branch3 (left, e1, mid, e2, right)) = @@ -256,15 +254,15 @@ let fun get Empty = NONE | get (Leaf1 e) = f e - | get (Leaf2 (k1, x1, k2, x2)) = - (case f (k1, x1) of - NONE => f (k2, x2) + | get (Leaf2 (e1, e2)) = + (case f e1 of + NONE => f e2 | some => some) - | get (Leaf3 (k1, x1, k2, x2, k3, x3)) = - (case f (k1, x1) of + | get (Leaf3 (e1, e2, e3)) = + (case f e1 of NONE => - (case f (k2, x2) of - NONE => f (k3, x3) + (case f e2 of + NONE => f e3 | some => some) | some => some) | get (Branch2 (left, e, right)) = @@ -291,111 +289,45 @@ in get end; -(* lookup *) - -fun lookup tab key = - let - fun key_ord k = Key.ord (key, k); - val key_eq = is_equal o key_ord; +(* retrieve *) - fun look Empty = NONE - | look (Leaf1 (k, x)) = - if key_eq k then SOME x else NONE - | look (Leaf2 (k1, x1, k2, x2)) = - (case key_ord k1 of - LESS => NONE - | EQUAL => SOME x1 - | GREATER => if key_eq k2 then SOME x2 else NONE) - | look (Leaf3 (k1, x1, k2, x2, k3, x3)) = - (case key_ord k2 of - LESS => if key_eq k1 then SOME x1 else NONE - | EQUAL => SOME x2 - | GREATER => if key_eq k3 then SOME x3 else NONE) - | look (Branch2 (left, (k, x), right)) = - (case key_ord k of - LESS => look left - | EQUAL => SOME x - | GREATER => look right) - | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = - (case key_ord k1 of - LESS => look left - | EQUAL => SOME x1 - | GREATER => - (case key_ord k2 of - LESS => look mid - | EQUAL => SOME x2 - | GREATER => look right)) - | look (Size (_, arg)) = look arg; - in look tab end; - -fun lookup_key tab key = +fun retrieve {result, no_result} tab (key: key) = let - fun key_ord k = Key.ord (key, k); - val key_eq = is_equal o key_ord; + fun compare (k, _) = Key.ord (key, k) + fun result_equal e = if is_equal (compare e) then result e else no_result; - fun look Empty = NONE - | look (Leaf1 (k, x)) = - if key_eq k then SOME (k, x) else NONE - | look (Leaf2 (k1, x1, k2, x2)) = - (case key_ord k1 of - LESS => NONE - | EQUAL => SOME (k1, x1) - | GREATER => if key_eq k2 then SOME (k2, x2) else NONE) - | look (Leaf3 (k1, x1, k2, x2, k3, x3)) = - (case key_ord k2 of - LESS => if key_eq k1 then SOME (k1, x1) else NONE - | EQUAL => SOME (k2, x2) - | GREATER => if key_eq k3 then SOME (k3, x3) else NONE) - | look (Branch2 (left, (k, x), right)) = - (case key_ord k of - LESS => look left - | EQUAL => SOME (k, x) - | GREATER => look right) - | look (Branch3 (left, (k1, x1), mid, (k2, x2), right)) = - (case key_ord k1 of - LESS => look left - | EQUAL => SOME (k1, x1) + fun find Empty = no_result + | find (Leaf1 e) = result_equal e + | find (Leaf2 (e1, e2)) = + (case compare e1 of + LESS => no_result + | EQUAL => result e1 + | GREATER => result_equal e2) + | find (Leaf3 (e1, e2, e3)) = + (case compare e2 of + LESS => result_equal e1 + | EQUAL => result e2 + | GREATER => result_equal e3) + | find (Branch2 (left, e, right)) = + (case compare e of + LESS => find left + | EQUAL => result e + | GREATER => find right) + | find (Branch3 (left, e1, mid, e2, right)) = + (case compare e1 of + LESS => find left + | EQUAL => result e1 | GREATER => - (case key_ord k2 of - LESS => look mid - | EQUAL => SOME (k2, x2) - | GREATER => look right)) - | look (Size (_, arg)) = look arg; - in look tab end; + (case compare e2 of + LESS => find mid + | EQUAL => result e2 + | GREATER => find right)) + | find (Size (_, arg)) = find arg; + in find tab end; -fun defined tab key = - let - fun key_ord k = Key.ord (key, k); - val key_eq = is_equal o key_ord; - - fun def Empty = false - | def (Leaf1 (k, _)) = key_eq k - | def (Leaf2 (k1, _, k2, _)) = - (case key_ord k1 of - LESS => false - | EQUAL => true - | GREATER => key_eq k2) - | def (Leaf3 (k1, _, k2, _, k3, _)) = - (case key_ord k2 of - LESS => key_eq k1 - | EQUAL => true - | GREATER => key_eq k3) - | def (Branch2 (left, (k, _), right)) = - (case key_ord k of - LESS => def left - | EQUAL => true - | GREATER => def right) - | def (Branch3 (left, (k1, _), mid, (k2, _), right)) = - (case key_ord k1 of - LESS => def left - | EQUAL => true - | GREATER => - (case key_ord k2 of - LESS => def mid - | EQUAL => true - | GREATER => def right)) - | def (Size (_, arg)) = def arg; - in def tab end; +fun lookup tab key = retrieve {result = SOME o #2, no_result = NONE} tab key; +fun lookup_key tab key = retrieve {result = SOME, no_result = NONE} tab key; +fun defined tab key = retrieve {result = K true, no_result = false} tab key; (* modify *) @@ -408,68 +340,68 @@ fun modify key f tab = let - fun key_ord k = Key.ord (key, k); + fun compare (k, _) = Key.ord (key, k) val inc = Unsynchronized.ref 0; - fun insert () = f NONE before ignore (Unsynchronized.inc inc); - fun update x = f (SOME x); + fun insert (k: key) = (k, f NONE) before ignore (Unsynchronized.inc inc); + fun update (k: key, x) = (k, f (SOME x)); - fun modfy Empty = Sprout (Empty, (key, insert ()), Empty) + fun modfy Empty = Sprout (Empty, (insert key), Empty) | modfy (t as Leaf1 _) = modfy (unmake t) | modfy (t as Leaf2 _) = modfy (unmake t) | modfy (t as Leaf3 _) = modfy (unmake t) - | modfy (Branch2 (left, p as (k, x), right)) = - (case key_ord k of + | modfy (Branch2 (left, e, right)) = + (case compare e of LESS => (case modfy left of - Stay left' => Stay (make2 (left', p, right)) - | Sprout (left1, q, left2) => Stay (make3 (left1, q, left2, p, right))) - | EQUAL => Stay (make2 (left, (k, update x), right)) + Stay left' => Stay (make2 (left', e, right)) + | Sprout (left1, e', left2) => Stay (make3 (left1, e', left2, e, right))) + | EQUAL => Stay (make2 (left, update e, right)) | GREATER => (case modfy right of - Stay right' => Stay (make2 (left, p, right')) - | Sprout (right1, q, right2) => - Stay (make3 (left, p, right1, q, right2)))) - | modfy (Branch3 (left, p1 as (k1, x1), mid, p2 as (k2, x2), right)) = - (case key_ord k1 of + Stay right' => Stay (make2 (left, e, right')) + | Sprout (right1, e', right2) => + Stay (make3 (left, e, right1, e', right2)))) + | modfy (Branch3 (left, e1, mid, e2, right)) = + (case compare e1 of LESS => (case modfy left of - Stay left' => Stay (make3 (left', p1, mid, p2, right)) - | Sprout (left1, q, left2) => - Sprout (make2 (left1, q, left2), p1, make2 (mid, p2, right))) - | EQUAL => Stay (make3 (left, (k1, update x1), mid, p2, right)) + Stay left' => Stay (make3 (left', e1, mid, e2, right)) + | Sprout (left1, e', left2) => + Sprout (make2 (left1, e', left2), e1, make2 (mid, e2, right))) + | EQUAL => Stay (make3 (left, update e1, mid, e2, right)) | GREATER => - (case key_ord k2 of + (case compare e2 of LESS => (case modfy mid of - Stay mid' => Stay (make3 (left, p1, mid', p2, right)) - | Sprout (mid1, q, mid2) => - Sprout (make2 (left, p1, mid1), q, make2 (mid2, p2, right))) - | EQUAL => Stay (make3 (left, p1, mid, (k2, update x2), right)) + Stay mid' => Stay (make3 (left, e1, mid', e2, right)) + | Sprout (mid1, e', mid2) => + Sprout (make2 (left, e1, mid1), e', make2 (mid2, e2, right))) + | EQUAL => Stay (make3 (left, e1, mid, update e2, right)) | GREATER => (case modfy right of - Stay right' => Stay (make3 (left, p1, mid, p2, right')) + Stay right' => Stay (make3 (left, e1, mid, e2, right')) | Sprout (right1, q, right2) => - Sprout (make2 (left, p1, mid), p2, make2 (right1, q, right2))))) + Sprout (make2 (left, e1, mid), e2, make2 (right1, q, right2))))) | modfy (Size (_, arg)) = modfy arg; val tab' = (case tab of - Empty => Leaf1 (key, insert ()) - | Leaf1 (k, x) => - (case key_ord k of - LESS => Leaf2 (key, insert (), k, x) - | EQUAL => Leaf1 (k, update x) - | GREATER => Leaf2 (k, x, key, insert ())) - | Leaf2 (k1, x1, k2, x2) => - (case key_ord k1 of - LESS => Leaf3 (key, insert (), k1, x1, k2, x2) - | EQUAL => Leaf2 (k1, update x1, k2, x2) + Empty => Leaf1 (insert key) + | Leaf1 e => + (case compare e of + LESS => Leaf2 (insert key, e) + | EQUAL => Leaf1 (update e) + | GREATER => Leaf2 (e, insert key)) + | Leaf2 (e1, e2) => + (case compare e1 of + LESS => Leaf3 (insert key, e1, e2) + | EQUAL => Leaf2 (update e1, e2) | GREATER => - (case key_ord k2 of - LESS => Leaf3 (k1, x1, key, insert (), k2, x2) - | EQUAL => Leaf2 (k1, x1, k2, update x2) - | GREATER => Leaf3 (k1, x1, k2, x2, key, insert ()))) + (case compare e2 of + LESS => Leaf3 (e1, insert key, e2) + | EQUAL => Leaf2 (e1, update e2) + | GREATER => Leaf3 (e1, e2, insert key))) | _ => (case modfy tab of Stay tab' => tab' @@ -498,20 +430,20 @@ fun del (SOME k) Empty = raise UNDEF k | del NONE Empty = raise Match - | del NONE (Leaf1 p) = (p, (true, Empty)) - | del NONE (Leaf2 (k1, x1, k2, x2)) = ((k1, x1), (false, Leaf1 (k2, x2))) - | del k (Leaf1 p) = - (case compare k p of - EQUAL => (p, (true, Empty)) + | del NONE (Leaf1 e) = (e, (true, Empty)) + | del NONE (Leaf2 (e1, e2)) = (e1, (false, Leaf1 e2)) + | del k (Leaf1 e) = + (case compare k e of + EQUAL => (e, (true, Empty)) | _ => raise UNDEF (the k)) - | del k (Leaf2 (k1, x1, k2, x2)) = - (case compare k (k1, x1) of - EQUAL => ((k1, x1), (false, Leaf1 (k2, x2))) + | del k (Leaf2 (e1, e2)) = + (case compare k e1 of + EQUAL => (e1, (false, Leaf1 e2)) | _ => - (case compare k (k2, x2) of - EQUAL => ((k2, x2), (false, Leaf1 (k1, x1))) + (case compare k e2 of + EQUAL => (e2, (false, Leaf1 e1)) | _ => raise UNDEF (the k))) - | del k (Leaf3 (k1, x1, k2, x2, k3, x3)) = del k (Branch2 (Leaf1 (k1, x1), (k2, x2), Leaf1 (k3, x3))) + | del k (Leaf3 (e1, e2, e3)) = del k (Branch2 (Leaf1 e1, e2, Leaf1 e3)) | del k (Branch2 (l, p, r)) = (case compare k p of LESS => diff -r 06f380099b2e -r db7d6dcaeb32 src/Pure/Tools/profiling.scala --- a/src/Pure/Tools/profiling.scala Thu Nov 30 18:24:51 2023 +0100 +++ b/src/Pure/Tools/profiling.scala Thu Nov 30 20:55:40 2023 +0100 @@ -39,6 +39,7 @@ sizeof_thms_id: Space = Space.zero, sizeof_terms: Space = Space.zero, sizeof_types: Space = Space.zero, + sizeof_names: Space = Space.zero, sizeof_spaces: Space = Space.zero) object Statistics { @@ -49,10 +50,10 @@ private val decode_result: XML.Decode.T[Session_Statistics] = (body: XML.Body) => { - val (a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))) = { + val (a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))) = { import XML.Decode._ pair(int, pair(int, pair(int, pair(int, pair(int, - pair(long, pair(long, pair(long, pair(long, long)))))))))(body) + pair(long, pair(long, pair(long, pair(long, pair(long, long))))))))))(body) } Session_Statistics( theories = a, @@ -64,7 +65,8 @@ sizeof_thms_id = Space.bytes(g), sizeof_terms = Space.bytes(h), sizeof_types = Space.bytes(i), - sizeof_spaces = Space.bytes(j)) + sizeof_names = Space.bytes(j), + sizeof_spaces = Space.bytes(k)) } def make( @@ -102,6 +104,7 @@ thms_id_size = session.sizeof_thms_id, terms_size = session.sizeof_terms, types_size = session.sizeof_types, + names_size = session.sizeof_names, spaces_size = session.sizeof_spaces) } @@ -121,6 +124,7 @@ "thms_id_size%", "terms_size%", "types_size%", + "names_size%", "spaces_size%") def header: List[String] = @@ -140,6 +144,7 @@ val thms_id_size: Space = Space.zero, val terms_size: Space = Space.zero, val types_size: Space = Space.zero, + val names_size: Space = Space.zero, val spaces_size: Space = Space.zero ) { private def print_total_theories: String = @@ -169,6 +174,7 @@ size_percentage(thms_id_size).toString, size_percentage(terms_size).toString, size_percentage(types_size).toString, + size_percentage(names_size).toString, size_percentage(spaces_size).toString) def fields: List[Any] = @@ -190,6 +196,7 @@ thms_id_size = other.cumulative.thms_id_size + thms_id_size, terms_size = other.cumulative.terms_size + terms_size, types_size = other.cumulative.types_size + types_size, + names_size = other.cumulative.names_size + names_size, spaces_size = other.cumulative.spaces_size + spaces_size) } diff -r 06f380099b2e -r db7d6dcaeb32 src/Pure/term_ord.ML --- a/src/Pure/term_ord.ML Thu Nov 30 18:24:51 2023 +0100 +++ b/src/Pure/term_ord.ML Thu Nov 30 20:55:40 2023 +0100 @@ -238,6 +238,7 @@ end; +structure Typset = Set(Typtab.Key); structure Termset = Set(Termtab.Key); structure Var_Graph = Graph(Vartab.Key); diff -r 06f380099b2e -r db7d6dcaeb32 src/Tools/profiling.ML --- a/src/Tools/profiling.ML Thu Nov 30 18:24:51 2023 +0100 +++ b/src/Tools/profiling.ML Thu Nov 30 20:55:40 2023 +0100 @@ -21,6 +21,7 @@ sizeof_thms_id: int, sizeof_terms: int, sizeof_types: int, + sizeof_names: int, sizeof_spaces: int} val session_statistics: string list -> session_statistics val main: unit -> unit @@ -63,8 +64,9 @@ val thms = maps all_thms thys; val thys_id = map Context.theory_id thys; val thms_id = map Thm.theory_id thms; - val terms = (fold o Thm.fold_terms {hyps = true}) cons thms []; - val types = (fold o fold_types) cons terms []; + val terms = + Termset.dest ((fold o Thm.fold_terms {hyps = true}) Termset.insert thms Termset.empty); + val types = Typset.dest ((fold o fold_types) Typset.insert terms Typset.empty); val spaces = maps (fn f => map f thys) [Sign.class_space, @@ -76,8 +78,14 @@ Locale.locale_space, Attrib.attribute_space o Context.Theory, Method.method_space o Context.Theory]; - in {thys_id = thys_id, thms_id = thms_id, terms = terms, types = types, spaces = spaces} end; + val names = Symset.dest (Symset.merges (map (Symset.make o Name_Space.get_names) spaces)); + in + {thys_id = thys_id, thms_id = thms_id, terms = terms, + types = types, names = names, spaces = spaces} + end; +fun sizeof1_diff (a, b) = ML_Heap.sizeof1 a - ML_Heap.sizeof1 b; +fun sizeof_list_diff (a, b) = ML_Heap.sizeof_list a - ML_Heap.sizeof_list b; fun sizeof_diff (a, b) = ML_Heap.sizeof a - ML_Heap.sizeof b; @@ -93,6 +101,7 @@ sizeof_thms_id: int, sizeof_terms: int, sizeof_types: int, + sizeof_names: int, sizeof_spaces: int}; fun session_statistics theories : session_statistics = @@ -111,9 +120,9 @@ val base_thys = filter_out theories_member all_thys; val {thys_id = all_thys_id, thms_id = all_thms_id, terms = all_terms, - types = all_types, spaces = all_spaces} = session_content all_thys; + types = all_types, names = all_names, spaces = all_spaces} = session_content all_thys; val {thys_id = base_thys_id, thms_id = base_thms_id, terms = base_terms, - types = base_types, spaces = base_spaces} = session_content base_thys; + types = base_types, names = base_names, spaces = base_spaces} = session_content base_thys; val n = length loaded_thys; val m = (case length loaded_context_thys of 0 => 0 | l => l - n); @@ -123,11 +132,22 @@ locales = Integer.sum (map (length o locales) loaded_thys), locale_thms = Integer.sum (map (length o locales_thms) loaded_thys), global_thms = Integer.sum (map (length o global_thms) loaded_thys), - sizeof_thys_id = sizeof_diff (all_thys_id, base_thys_id), - sizeof_thms_id = sizeof_diff (all_thms_id, base_thms_id), - sizeof_terms = sizeof_diff (all_terms, base_terms), - sizeof_types = sizeof_diff (all_types, base_types), - sizeof_spaces = sizeof_diff (all_spaces, base_spaces)} + sizeof_thys_id = + sizeof1_diff ((all_thys_id, all_thms_id), (base_thys_id, all_thms_id)) - + sizeof_list_diff (all_thys_id, base_thys_id), + sizeof_thms_id = + sizeof1_diff ((all_thms_id, all_thys_id), (base_thms_id, all_thys_id)) - + sizeof_list_diff (all_thms_id, base_thms_id), + sizeof_terms = + sizeof1_diff ((all_terms, all_types, all_names), (base_terms, all_types, all_names)) - + sizeof_list_diff (all_terms, base_terms), + sizeof_types = + sizeof1_diff ((all_types, all_names), (base_types, all_names)) - + sizeof_list_diff (all_types, base_types), + sizeof_spaces = + sizeof1_diff ((all_spaces, all_names), (base_spaces, all_names)) - + sizeof_list_diff (all_spaces, base_spaces), + sizeof_names = sizeof_diff (all_names, base_names)} end; @@ -148,9 +168,12 @@ sizeof_thms_id = g, sizeof_terms = h, sizeof_types = i, - sizeof_spaces = j} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, j))))))))))) #> - let open XML.Encode - in pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int (pair int int)))))))) end; + sizeof_names = j, + sizeof_spaces = k} => ((a, (b, (c, (d, (e, (f, (g, (h, (i, (j, k)))))))))))) #> + let open XML.Encode in + pair int (pair int (pair int (pair int (pair int (pair int (pair int + (pair int (pair int (pair int int))))))))) + end; in