Module Nativecode

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.

type mllambda
type global
val debug_native_compiler : CDebug.t
val keep_debug_files : unit -> bool
val pp_global : Stdlib.Format.formatter -> global -> unit
val mk_open : string -> global
val clear_symbols : unit -> unit
val get_value : Nativevalues.symbols -> int -> Nativevalues.t
val get_sort : Nativevalues.symbols -> int -> Sorts.t
val get_name : Nativevalues.symbols -> int -> Names.Name.t
val get_const : Nativevalues.symbols -> int -> Names.Constant.t
val get_ind : Nativevalues.symbols -> int -> Names.inductive
val get_evar : Nativevalues.symbols -> int -> Evar.t
val get_level : Nativevalues.symbols -> int -> Univ.Level.t
val get_proj : Nativevalues.symbols -> int -> Names.inductive * int
val get_symbols : unit -> Nativevalues.symbols
type code_location_updates
type linkable_code = global list * code_location_updates
val clear_global_tbl : unit -> unit
val empty_updates : code_location_updates
val register_native_file : string -> unit
val is_loaded_native_file : string -> bool
val compile_constant_field : Environ.env -> Names.Constant.t -> global list -> 'a Declarations.pconstant_body -> global list
val compile_mind_field : Names.ModPath.t -> Names.Label.t -> global list -> Declarations.mutual_inductive_body -> global list
val mk_conv_code : Environ.env -> Genlambda.evars -> string -> Constr.constr -> Constr.constr -> linkable_code
val mk_norm_code : Environ.env -> Genlambda.evars -> string -> Constr.constr -> linkable_code
val mk_library_header : Nativevalues.symbols -> global list
val mod_uid_of_dirpath : Names.DirPath.t -> string
val update_locations : code_location_updates -> unit
val add_header_comment : global list -> string -> global list