package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.20.0.tar.gz
md5=66e57ea55275903bef74d5bf36fbe0f1
sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.clib/CObj/index.html

Module CObjSource

Physical size of an ocaml value.

These functions explore objects recursively and may allocate a lot.

Sourceval size : 'a -> int

Physical size of an object in words.

Sourceval size_b : 'a -> int

Same as size in bytes.

Sourceval size_kb : 'a -> int

Same as size in kilobytes.

Physical size of an ocaml value with sharing.

This time, all the size of objects are computed with respect to a larger object containing them all, and we only count the new blocks not already seen earlier in the left-to-right visit of the englobing object.

Provides the global object in which we'll search shared sizes

Sourceval register_shared_size : 'a -> unit

Shared size (in word) of an object with respect to the global object given by the last register_shared_size.

Sourceval shared_size_of_obj : 'a -> int

Same, with an object indicated by its occurrence in the global object. The very same object could have a zero size or not, depending of the occurrence we're considering in the englobing object. For speaking of occurrences, we use an int list for a path of field indexes (leftmost = deepest block, rightmost = top block of the global object).

Sourceval shared_size_of_pos : int list -> int
Logical size of an OCaml value.
Sourceval obj_stats : 'a -> int * int * int

Return the (logical) value size, the string size, and the maximum depth of the object. This loops on cyclic structures.

Total size of the allocated ocaml heap.
Sourceval heap_size : unit -> int

Heap size, in words.

Sourceval heap_size_kb : unit -> int

Heap size, in kilobytes.

OCaml

Innovation. Community. Security.