From de61c7d77e49286622c4aebd56f2e87b0df93903 Mon Sep 17 00:00:00 2001
From: Maxime Dénès <mail@maximedenes.fr>
Date: Sat, 5 Apr 2014 19:51:04 -0400
Subject: Had to split Nativelambda in two files because of Retroknowledge
 dependencies.

---
 kernel/nativelambda.ml | 43 ++++++++-----------------------------------
 1 file changed, 8 insertions(+), 35 deletions(-)

(limited to 'kernel/nativelambda.ml')

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
-- 
cgit v1.2.3