Module `Nativecode`Source

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 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 clear_symbols : unit -> unit

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_const : Nativevalues.symbols -> int -> Names.Constant.t

Sourceval get_match : Nativevalues.symbols -> int -> Nativevalues.annot_sw

Sourceval get_ind : Nativevalues.symbols -> int -> Names.inductive

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

Sourceval get_symbols : unit -> Nativevalues.symbols

Sourcetype code_location_updates

Sourcetype linkable_code = global list * code_location_updates

Sourceval clear_global_tbl : unit -> unit

Sourceval empty_updates : code_location_updates

Sourceval register_native_file : string -> unit

Sourceval is_loaded_native_file : string -> bool

Source

val compile_constant_field : 
  Environ.env ->
  Names.Constant.t ->
  global list ->
  Declarations.constant_body ->
  global list

Source

val compile_mind_field : 
  Names.ModPath.t ->
  Names.Label.t ->
  global list ->
  Declarations.mutual_inductive_body ->
  global list

Source

val compile_rewrite_rules : 
  Environ.env ->
  Names.Label.t ->
  global list ->
  Declarations.rewrite_rules_body ->
  global list

Source

val mk_conv_code : 
  Environ.env ->
  Genlambda.evars ->
  string ->
  Constr.constr ->
  Constr.constr ->
  linkable_code

Source

val 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 link_info_of_dirpath : Names.DirPath.t -> Environ.link_info

Sourceval update_locations : code_location_updates -> unit

Sourceval add_header_comment : global list -> string -> global list

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module `Nativecode`Source

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

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

Module NativecodeSource

Module `Nativecode`Source