Added a Register Inline command for the native compiler. Will be ported to the VM

too. Almost only a new grammar entry since the inlining machinery was already
implemented.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16623 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 17 insertions, 0 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 62e2d46a85..636644ec3a 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -771,3 +771,18 @@ let j_type j = j.uj_type
 let safe_infer senv = infer (env_of_senv senv)
 
 let typing senv = Typeops.typing (env_of_senv senv)
+
+(* This function serves only for inlining constants in native compiler for now,
+but it is meant to become a replacement for environ.register *)
+let register_inline kn senv =
+  if not (evaluable_constant kn senv.env) then
+    Errors.error "Register inline: an evaluable constant is expected";
+  let env = pre_env senv.env in
+  let (cb,r) = Cmap_env.find kn env.Pre_env.env_globals.Pre_env.env_constants in
+  let cb = {cb with const_inline_code = true} in 
+  let new_constants =
+    Cmap_env.add kn (cb,r) env.Pre_env.env_globals.Pre_env.env_constants
+  in
+  let new_globals = { env.Pre_env.env_globals with Pre_env.env_constants = new_constants } in
+  let env = { env with Pre_env.env_globals = new_globals } in
+  { senv with env = env_of_pre_env env }
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 31bb8143e9..7ca0333833 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -136,3 +136,5 @@ val retroknowledge : (retroknowledge-> 'a) -> safe_environment -> 'a
 
 val register : safe_environment -> field -> Retroknowledge.entry -> constr
                                          -> safe_environment
+
+val register_inline : constant -> safe_environment -> safe_environment