diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/nativecode.ml | 16 | ||||
| -rw-r--r-- | kernel/nativecode.mli | 6 | ||||
| -rw-r--r-- | kernel/nativelibrary.mli | 2 | ||||
| -rw-r--r-- | kernel/nativevalues.ml | 17 | ||||
| -rw-r--r-- | kernel/nativevalues.mli | 16 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 6 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 2 |
7 files changed, 39 insertions, 26 deletions
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 3f791dfc22..347fdc773d 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -141,18 +141,6 @@ let fresh_gnormtbl l = (** Symbols (pre-computed values) **) -type symbol = - | SymbValue of Nativevalues.t - | SymbSort of Sorts.t - | SymbName of Name.t - | SymbConst of Constant.t - | SymbMatch of annot_sw - | SymbInd of inductive - | SymbMeta of metavariable - | SymbEvar of Evar.t - | SymbLevel of Univ.Level.t - | SymbProj of (inductive * int) - let dummy_symb = SymbValue (dummy_value ()) let eq_symbol sy1 sy2 = @@ -194,10 +182,6 @@ let symb_tbl = HashtblSymbol.create 211 let clear_symbols () = HashtblSymbol.clear symb_tbl -type symbols = symbol array - -let empty_symbols = [||] - let get_value tbl i = match tbl.(i) with | SymbValue v -> v diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index b5c03b6ca3..caebbc63a6 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -12,6 +12,7 @@ open Constr open Declarations open Environ open Nativelambda +open Nativevalues (** This file defines the mllambda code generation phase of the native compiler. mllambda represents a fragment of ML, and can easily be printed @@ -25,11 +26,6 @@ val pp_global : Format.formatter -> global -> unit val mk_open : string -> global (* Precomputed values for a compilation unit *) -type symbol -type symbols - -val empty_symbols : symbols - val clear_symbols : unit -> unit val get_value : symbols -> int -> Nativevalues.t diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 31e5255fc4..1485e97b47 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -16,4 +16,4 @@ open Nativecode compiler *) val dump_library : ModPath.t -> DirPath.t -> env -> module_signature -> - global list * symbols + global list * Nativevalues.symbols diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3eb51ffc59..1102dd6cae 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -66,6 +66,23 @@ type atom = | Aevar of Evar.t * t array | Aproj of (inductive * int) * accumulator +type symbol = + | SymbValue of t + | SymbSort of Sorts.t + | SymbName of Name.t + | SymbConst of Constant.t + | SymbMatch of annot_sw + | SymbInd of inductive + | SymbMeta of metavariable + | SymbEvar of Evar.t + | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) + +type symbols = symbol array + +let empty_symbols = [| |] + + let accumulate_tag = 0 (** Unique pointer used to drive the accumulator function *) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 58cb6e2c30..c037d2bde7 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -56,6 +56,22 @@ type atom = | Aevar of Evar.t * t array (* arguments *) | Aproj of (inductive * int) * accumulator +type symbol = + | SymbValue of t + | SymbSort of Sorts.t + | SymbName of Name.t + | SymbConst of Constant.t + | SymbMatch of annot_sw + | SymbInd of inductive + | SymbMeta of metavariable + | SymbEvar of Evar.t + | SymbLevel of Univ.Level.t + | SymbProj of (inductive * int) + +type symbols = symbol array + +val empty_symbols : symbols + (* Constructors *) val mk_accu : atom -> t diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 824400b4e3..2284196efe 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -130,7 +130,7 @@ type safe_environment = required : vodigest DPMap.t; loads : (ModPath.t * module_body) list; local_retroknowledge : Retroknowledge.action list; - native_symbols : Nativecode.symbols DPMap.t } + native_symbols : Nativevalues.symbols DPMap.t } and modvariant = | NONE @@ -1076,7 +1076,7 @@ type compiled_library = { comp_mod : module_body; comp_deps : library_info array; comp_enga : engagement; - comp_natsymbs : Nativecode.symbols + comp_natsymbs : Nativevalues.symbols } let module_of_library lib = lib.comp_mod @@ -1128,7 +1128,7 @@ let export ?except ~output_native_objects senv dir = let ast, symbols = if output_native_objects then Nativelibrary.dump_library mp dir senv.env str - else [], Nativecode.empty_symbols + else [], Nativevalues.empty_symbols in let lib = { comp_name = dir; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 770caf5406..d8f7f0cc40 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -179,7 +179,7 @@ type native_library = Nativecode.global list val module_of_library : compiled_library -> Declarations.module_body -val get_library_native_symbols : safe_environment -> DirPath.t -> Nativecode.symbols +val get_library_native_symbols : safe_environment -> DirPath.t -> Nativevalues.symbols val start_library : DirPath.t -> ModPath.t safe_transformer |