diff options
-rw-r--r-- | dev/printers.mllib | 1 | ||||
-rw-r--r-- | kernel/kernel.mllib | 1 | ||||
-rw-r--r-- | kernel/nativecode.ml | 1 | ||||
-rw-r--r-- | kernel/nativeinstr.mli | 44 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 43 | ||||
-rw-r--r-- | kernel/nativelambda.mli | 32 | ||||
-rw-r--r-- | kernel/retroknowledge.ml | 88 | ||||
-rw-r--r-- | kernel/retroknowledge.mli | 36 |
8 files changed, 178 insertions, 68 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index ae0980cdb..c56982d99 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -62,6 +62,7 @@ Cbytecodes Copcodes Cemitcodes Nativevalues +Nativeinstr Future Opaqueproof Declareops diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 5008e4322..3267b7e75 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -13,6 +13,7 @@ Cbytecodes Copcodes Cemitcodes Nativevalues +Nativeinstr Opaqueproof Declareops Retroknowledge diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 511bb5f77..c294345e8 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -12,6 +12,7 @@ open Context open Declarations open Util open Nativevalues +open Nativeinstr open Nativelambda open Pre_env diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli new file mode 100644 index 000000000..4e0291ed9 --- /dev/null +++ b/kernel/nativeinstr.mli @@ -0,0 +1,44 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2013 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) +open Names +open Term +open Nativevalues + +(** This file defines the lambda code for the native compiler. It has been +extracted from Nativelambda.ml because of the retroknowledge architecture. *) + +type lambda = + | Lrel of name * int + | Lvar of identifier + | Lmeta of metavariable * lambda (* type *) + | Levar of existential * lambda (* type *) + | Lprod of lambda * lambda + | Llam of name array * lambda + | Llet of name * lambda * lambda + | Lapp of lambda * lambda array + | Lconst of string * constant (* prefix, constant name *) + | Lcase of annot_sw * lambda * lambda * lam_branches + (* annotations, term being matched, accu, branches *) + | Lif of lambda * lambda * lambda + | Lfix of (int array * int) * fix_decl + | Lcofix of int * fix_decl + | Lmakeblock of string * constructor * int * lambda array + (* prefix, constructor name, constructor tag, arguments *) + (* A fully applied constructor *) + | Lconstruct of string * constructor (* prefix, constructor name *) + (* A partially applied constructor *) + | Luint of Uint31.t + | Lval of Nativevalues.t + | Lsort of sorts + | Lind of string * inductive (* prefix, inductive name *) + | Llazy + | Lforce + +and lam_branches = (constructor * name array * lambda) array + +and fix_decl = name array * lambda array * lambda array diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index 376de3980..297ac6b99 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -12,38 +12,11 @@ open Term open Declarations open Pre_env open Nativevalues +open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) -type lambda = - | Lrel of name * int - | Lvar of identifier - | Lmeta of metavariable * lambda (* type *) - | Levar of existential * lambda (* type *) - | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of string * constant (* prefix, constant name *) - | Lcase of annot_sw * lambda * lambda * lam_branches - (* annotations, term being matched, accu, branches *) - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lmakeblock of string * constructor * int * lambda array - (* prefix, constructor name, constructor tag, arguments *) - (* A fully applied constructor *) - | Lconstruct of string * constructor (* prefix, constructor name *) - (* A partially applied constructor *) - | Luint of Uint31.t - | Lval of Nativevalues.t - | Lsort of sorts - | Lind of string * inductive (* prefix, inductive name *) - | Llazy - | Lforce - -and lam_branches = (constructor * name array * lambda) array - -and fix_decl = name array * lambda array * lambda array + +exception NotClosed type evars = { evars_val : existential -> constr option; @@ -667,11 +640,11 @@ and lambda_of_app env sigma f args = let expected = nparams + arity in let nargs = Array.length args in if Int.equal nargs expected then -(* try - try - Bstrconst (Retroknowledge.get_vm_constant_static_info + try + try + Retroknowledge.get_native_constant_static_info (!global_env).retroknowledge - f args) + f args with NotClosed -> assert false (* let rargs = Array.sub args nparams arity in @@ -681,7 +654,7 @@ and lambda_of_app env sigma f args = f), b_args) *) - with Not_found -> *) + with Not_found -> let args = lambda_of_args env sigma nparams args in makeblock !global_env c tag args else diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 751f11978..d4be2279d 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -9,40 +9,10 @@ open Names open Term open Pre_env open Nativevalues +open Nativeinstr (** This file defines the lambda code generation phase of the native compiler *) -type lambda = - | Lrel of name * int - | Lvar of identifier - | Lmeta of metavariable * lambda (* type *) - | Levar of existential * lambda (* type *) - | Lprod of lambda * lambda - | Llam of name array * lambda - | Llet of name * lambda * lambda - | Lapp of lambda * lambda array - | Lconst of string * constant (* prefix, constant name *) - | Lcase of annot_sw * lambda * lambda * lam_branches - (* annotations, term being matched, accu, branches *) - | Lif of lambda * lambda * lambda - | Lfix of (int array * int) * fix_decl - | Lcofix of int * fix_decl - | Lmakeblock of string * constructor * int * lambda array - (* prefix, constructor name, constructor tag, arguments *) - (* A fully applied constructor *) - | Lconstruct of string * constructor (* prefix, constructor name *) - (* A partially applied constructor *) - | Luint of Uint31.t - | Lval of Nativevalues.t - | Lsort of sorts - | Lind of string * inductive (* prefix, inductive name *) - | Llazy - | Lforce - -and lam_branches = (constructor * name array * lambda) array - -and fix_decl = name array * lambda array * lambda array - type evars = { evars_val : existential -> constr option; evars_typ : existential -> types; diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index b7fb6956f..1049ab94d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -132,8 +132,7 @@ type reactive_end = {(*information required by the compiler of the VM *) int->Cbytecodes.bytecodes->Cbytecodes.bytecodes) option; native_constant_static : - (bool->constr array->Cbytecodes.structured_constant) - option; + (bool -> constr array -> Nativeinstr.lambda) option; native_constant_dynamic : (bool->Cbytecodes.comp_env->Cbytecodes.block array->int-> Cbytecodes.bytecodes->Cbytecodes.bytecodes) @@ -239,7 +238,37 @@ let get_vm_decompile_constant_info knowledge key = | None -> raise Not_found | Some f -> f +let get_native_compiling_info knowledge key = + match (Reactive.find key knowledge.reactive).native_compiling + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation + +(* used for compilation of fully applied constructors *) +let get_native_constant_static_info knowledge key = + match (Reactive.find key knowledge.reactive).native_constant_static + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation +(* used for compilation of partially applied constructors *) +let get_native_constant_dynamic_info knowledge key = + match (Reactive.find key knowledge.reactive).native_constant_dynamic + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation + +let get_native_before_match_info knowledge key = + match (Reactive.find key knowledge.reactive).native_before_match + with + | None -> raise Not_found + | Some f -> f knowledge.flags.fastcomputation + +let get_native_decompile_constant_info knowledge key = + match (Reactive.find key knowledge.reactive).native_decompile_const + with + | None -> raise Not_found + | Some f -> f (* functions manipulating reactive knowledge *) let add_vm_compiling_info knowledge value nfo = @@ -297,5 +326,60 @@ let add_vm_decompile_constant_info knowledge value nfo = knowledge.reactive } +let add_native_compiling_info knowledge value nfo = + {knowledge with reactive = + try + Reactive.add value + {(Reactive.find value (knowledge.reactive)) with native_compiling = Some nfo} + knowledge.reactive + with Not_found -> + Reactive.add value {empty_reactive_end with native_compiling = Some nfo} + knowledge.reactive + } + +let add_native_constant_static_info knowledge value nfo = + {knowledge with reactive = + try + Reactive.add value + {(Reactive.find value (knowledge.reactive)) with native_constant_static = Some nfo} + knowledge.reactive + with Not_found -> + Reactive.add value {empty_reactive_end with native_constant_static = Some nfo} + knowledge.reactive + } + +let add_native_constant_dynamic_info knowledge value nfo = + {knowledge with reactive = + try + Reactive.add value + {(Reactive.find value (knowledge.reactive)) with native_constant_dynamic = Some nfo} + knowledge.reactive + with Not_found -> + Reactive.add value {empty_reactive_end with native_constant_dynamic = Some nfo} + knowledge.reactive + } + +let add_native_before_match_info knowledge value nfo = + {knowledge with reactive = + try + Reactive.add value + {(Reactive.find value (knowledge.reactive)) with native_before_match = Some nfo} + knowledge.reactive + with Not_found -> + Reactive.add value {empty_reactive_end with native_before_match = Some nfo} + knowledge.reactive + } + +let add_native_decompile_constant_info knowledge value nfo = + {knowledge with reactive = + try + Reactive.add value + {(Reactive.find value (knowledge.reactive)) with native_decompile_const = Some nfo} + knowledge.reactive + with Not_found -> + Reactive.add value {empty_reactive_end with native_decompile_const = Some nfo} + knowledge.reactive + } + let clear_info knowledge value = {knowledge with reactive = Reactive.remove value knowledge.reactive} diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 528f6ad16..097d207e4 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -117,6 +117,23 @@ val get_vm_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes val get_vm_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr +val get_native_compiling_info : retroknowledge -> entry -> Cbytecodes.comp_env -> + constr array -> + int -> Cbytecodes.bytecodes-> Cbytecodes.bytecodes + +val get_native_constant_static_info : retroknowledge -> entry -> + constr array -> Nativeinstr.lambda + +val get_native_constant_dynamic_info : retroknowledge -> entry -> + Cbytecodes.comp_env -> + Cbytecodes.block array -> + int -> Cbytecodes.bytecodes -> Cbytecodes.bytecodes + +val get_native_before_match_info : retroknowledge -> entry -> Cbytecodes.bytecodes + -> Cbytecodes.bytecodes + +val get_native_decompile_constant_info : retroknowledge -> entry -> int -> Term.constr + (** the following functions are solely used in Pre_env and Environ to implement the functions register and unregister (and mem) of Environ *) val add_field : retroknowledge -> field -> entry -> retroknowledge @@ -147,6 +164,25 @@ val add_vm_before_match_info : retroknowledge -> entry -> val add_vm_decompile_constant_info : retroknowledge -> entry -> (int -> constr) -> retroknowledge +val add_native_compiling_info : retroknowledge-> entry -> + (bool -> Cbytecodes.comp_env -> constr array -> int -> + Cbytecodes.bytecodes -> Cbytecodes.bytecodes) -> + retroknowledge +val add_native_constant_static_info : retroknowledge -> entry -> + (bool -> constr array -> + Nativeinstr.lambda) -> + retroknowledge +val add_native_constant_dynamic_info : retroknowledge-> entry -> + (bool -> Cbytecodes.comp_env -> + Cbytecodes.block array -> int -> + Cbytecodes.bytecodes -> Cbytecodes.bytecodes) -> + retroknowledge +val add_native_before_match_info : retroknowledge -> entry -> + (bool->Cbytecodes.bytecodes->Cbytecodes.bytecodes) -> + retroknowledge + +val add_native_decompile_constant_info : retroknowledge -> entry -> + (int -> constr) -> retroknowledge val clear_info : retroknowledge-> entry -> retroknowledge |