Had to split Nativelambda in two files because of Retroknowledge

dependencies.

7 files changed, 177 insertions, 68 deletions

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