diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2015-07-09 21:08:44 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2015-07-10 00:01:22 +0200 |
| commit | c4486dfda07b872d20746778df5c443b052b92b9 (patch) | |
| tree | a1388b2bc366d249e7da63065181b81d12f5283b /kernel/nativecode.mli | |
| parent | 2c59d19ad207a6bf193e9f0c9d73258b3133d484 (diff) | |
Native compiler: refactor code handling pre-computed values.
Fixes #4139 (Not_found exception with Require in modules).
Diffstat (limited to 'kernel/nativecode.mli')
| -rw-r--r-- | kernel/nativecode.mli | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 893db92dd..5d4c9e1e2 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -22,29 +22,33 @@ val pp_global : Format.formatter -> global -> unit val mk_open : string -> global +(* Precomputed values for a compilation unit *) type symbol +type symbols -val clear_symb_tbl : unit -> unit +val empty_symbols : symbols -val get_value : symbol array -> int -> Nativevalues.t +val clear_symbols : unit -> unit -val get_sort : symbol array -> int -> sorts +val get_value : symbols -> int -> Nativevalues.t -val get_name : symbol array -> int -> name +val get_sort : symbols -> int -> sorts -val get_const : symbol array -> int -> constant +val get_name : symbols -> int -> name -val get_match : symbol array -> int -> Nativevalues.annot_sw +val get_const : symbols -> int -> constant -val get_ind : symbol array -> int -> inductive +val get_match : symbols -> int -> Nativevalues.annot_sw -val get_meta : symbol array -> int -> metavariable +val get_ind : symbols -> int -> inductive -val get_evar : symbol array -> int -> existential +val get_meta : symbols -> int -> metavariable -val get_level : symbol array -> int -> Univ.Level.t +val get_evar : symbols -> int -> existential -val get_symbols_tbl : unit -> symbol array +val get_level : symbols -> int -> Univ.Level.t + +val get_symbols : unit -> symbols type code_location_update type code_location_updates |