package rocq-runtime

  1. Overview
  2. Docs
The Rocq Prover -- Core Binaries and Tools

Install 

dune-project
 Dependency

rocq-prover.org Readme Edit opam file Versions (5)

Authors

  1. T
    The Rocq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Rocq development team <rocq+rocq-development@discoursemail.com>

Sources

rocq-9.2.0.tar.gz
sha256=a45280ab4fbaac7540b136a6b073b4a6db15739ec1e149bded43fa6f4fc25f20

doc/rocq-runtime.kernel/Nativecode/index.html

Module NativecodeSource

This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed to OCaml code.

Sourcetype cenv
Sourceval make_cenv : unit -> cenv
Sourceval get_cenv_symbols : cenv -> Nativevalues.symbols
Sourcetype global
Sourceval debug_native_compiler : CDebug.t
Sourceval keep_debug_files : unit -> bool
Sourceval pp_global : Format.formatter -> global -> unit
Sourceval mk_open : string -> global
Sourceval get_value : Nativevalues.symbols -> int -> Nativevalues.t
Sourceval get_sort : Nativevalues.symbols -> int -> Sorts.t
Sourceval get_name : Nativevalues.symbols -> int -> Names.Name.t
Sourceval get_evar : Nativevalues.symbols -> int -> Evar.t
Sourceval get_instance : Nativevalues.symbols -> int -> UVars.Instance.t
Sourceval get_proj : Nativevalues.symbols -> int -> Names.inductive * int
Sourcetype code_location_updates
Sourceval empty_updates : code_location_updates
Sourceval register_native_file : string -> unit
Sourceval is_loaded_native_file : string -> bool
Sourceval compile_constant_field : cenv -> Environ.env -> Names.Constant.t -> global list -> Declarations.constant_body -> global list
Sourceval compile_mind_field : cenv -> Names.ModPath.t -> Names.Id.t -> global list -> Declarations.mutual_inductive_body -> global list
Sourceval compile_rewrite_rules : Environ.env -> Names.Id.t -> global list -> Declarations.rewrite_rules_body -> global list
Sourceval mk_norm_code : Environ.env -> Genlambda.evars -> string -> Constr.constr -> linkable_code
Sourceval mk_library_header : Nativevalues.symbols -> global list
Sourceval mod_uid_of_dirpath : Names.DirPath.t -> string
Sourceval update_locations : code_location_updates -> unit
Sourceval add_header_comment : global list -> string -> global list