author | wenzelm |
Mon, 20 Mar 2023 10:59:27 +0100 | |
changeset 77692 | 3e746e684f4b |
parent 69826 | 1bea05713dde |
child 77765 | 8db468bd1ec6 |
permissions | -rw-r--r-- |
62508
d0b68218ea55
discontinued RAW session: bootstrap directly from isabelle_process RAW_ML_SYSTEM;
wenzelm
parents:
62468
diff
changeset
|
1 |
(* Title: Pure/ML/ml_heap.ML |
62467 | 2 |
Author: Makarius |
3 |
||
4 |
ML heap operations. |
|
5 |
*) |
|
6 |
||
7 |
signature ML_HEAP = |
|
8 |
sig |
|
62825
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
9 |
val obj_size: 'a -> int |
77692 | 10 |
val sizeof1: 'a -> int |
11 |
val sizeof: 'a list -> int |
|
67622 | 12 |
val full_gc: unit -> unit |
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
67622
diff
changeset
|
13 |
val gc_now: unit -> Time.time |
62467 | 14 |
val share_common_data: unit -> unit |
62825
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
15 |
val save_child: string -> unit |
62467 | 16 |
end; |
17 |
||
18 |
structure ML_Heap: ML_HEAP = |
|
19 |
struct |
|
62825
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
20 |
|
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
21 |
val obj_size = PolyML.objSize; |
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
22 |
|
77692 | 23 |
fun sizeof1 x = obj_size x * ML_System.platform_obj_size; |
24 |
fun sizeof xs = (obj_size xs - 3 * length xs) * ML_System.platform_obj_size; |
|
25 |
||
67622 | 26 |
val full_gc = PolyML.fullGC; |
27 |
||
69826
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
67622
diff
changeset
|
28 |
fun gc_now () = #timeGCReal (PolyML.Statistics.getLocalStats ()); |
1bea05713dde
physical vs. logical events, the latter takes GC time into account;
wenzelm
parents:
67622
diff
changeset
|
29 |
|
62825
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
30 |
fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction; |
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
31 |
|
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
32 |
fun save_child name = |
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
33 |
PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ())); |
e6e80a8bf624
structure PolyML is sealed after bootstrap: all ML system access is managed by Isabelle;
wenzelm
parents:
62630
diff
changeset
|
34 |
|
62467 | 35 |
end; |