package coq-core

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

Install

Dune Dependency

Authors

Maintainers

Sources

coq-8.19.1.tar.gz
md5=13d2793fc6413aac5168822313e4864e
sha512=ec8379df34ba6e72bcf0218c66fef248b0e4c5c436fb3f2d7dd83a2c5f349dd0874a67484fcf9c0df3e5d5937d7ae2b2a79274725595b4b0065a381f70769b42

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.