package rocq-runtime

  1. Overview
  2. Docs

Module Coq_checklib.AnalyzeSource

Sourcetype data =
  1. | Int of int
  2. | Ptr of int
  3. | Atm of int
  4. | Fun of int

Representation of data allocated on the OCaml heap.

Sourcetype obj =
  1. | Struct of int * data array
  2. | Int64 of Int64.t
  3. | Float64 of float
  4. | String of string
Sourcemodule LargeArray : sig ... end

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

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

Type of inputs

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

Functorized version of the previous code.

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

Create the OCaml object out of the reified representation.