src/Pure/ML/ml_heap.ML

treat map_filter similar to list_all, list_ex, list_ex1

(*  Title:      Pure/ML/ml_heap.ML
    Author:     Makarius

ML heap operations.
*)

signature ML_HEAP =
sig
  val obj_size: 'a -> int
  val sizeof1: 'a -> int
  val sizeof_list: 'a list -> int
  val sizeof: 'a list -> int
  val full_gc: unit -> unit
  val gc_now: unit -> Time.time
  val share_common_data: unit -> unit
  val save_child: string -> unit
end;

structure ML_Heap: ML_HEAP =
struct

val obj_size = PolyML.objSize;

fun sizeof1 x = obj_size x * ML_System.platform_obj_size;

fun sizeof_list xs = 3 * length xs * ML_System.platform_obj_size;
fun sizeof xs = obj_size xs * ML_System.platform_obj_size - sizeof_list xs;

val full_gc = PolyML.fullGC;

fun gc_now () = #timeGCReal (PolyML.Statistics.getLocalStats ());

fun share_common_data () = PolyML.shareCommonData PolyML.rootFunction;

fun save_child name =
  PolyML.SaveState.saveChild (name, List.length (PolyML.SaveState.showHierarchy ()));

end;