Module Coq_checklib.Analyze

type data =
| Int of int
| Ptr of int
| Atm of int
| Fun of int

Representation of data allocated on the OCaml heap.

type obj =
| Struct of int * data array
| Int64 of Stdlib.Int64.t
| Float64 of float
| String of string
module LargeArray : sig ... end

A data structure similar to arrays but allowing to overcome the 2^22 length limitation on 32-bit architecture.

val parse_channel : Stdlib.in_channel -> data * obj LargeArray.t
val parse_string : string -> data * obj LargeArray.t
Functorized version
module type Input = sig ... end

Type of inputs

module type S = sig ... end
module Make (M : Input) : S with type input = M.t

Functorized version of the previous code.

val instantiate : (data * obj LargeArray.t) -> Stdlib.Obj.t

Create the OCaml object out of the reified representation.