Support for evars and metas in native compiler.

Experimental. Turned out to be much harder to implement than I thought. The main
issue is that the reification in the native compiler and the VM is not quite
untyped. Indeed, type annotations for lambdas have to be reconstructed. Hence,
when reifying an application u = t a1 ... an, the type of t has to be known or
reconstructed. It is always possible to do so in plain CIC, when u is in normal
form and its type is known. However, with partial terms this may no longer be
the case, as in: ?1 a1 ... an. So we also compile and evaluate the type of
evars and metas.

This still has to be tested more extensively, but the correction of the kernel
native conversion (on terms without evars or metas) should not be impacted.

Much of this could be reused for the VM.

3 files changed, 54 insertions, 20 deletions

diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index ed52f574ff..cc2054d100 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -21,9 +21,15 @@ open Nativecode
 open Inductiveops
 open Closure
 open Nativevalues
+open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
+let evars_of_evar_map evd =
+  { evars_val = Evd.existential_opt_value evd;
+    evars_typ = Evd.existential_type evd;
+    evars_metas = Evd.meta_type evd }
+
 exception Find_at of int
 
 let invert_tag cst tag reloc_tbl =
@@ -215,9 +221,14 @@ and nf_accu_type env accu =
 
 and nf_args env accu t =
   let aux arg (t,l) = 
-	let _,dom,codom = try decompose_prod env t with DestKO -> exit 123 in
-	let c = nf_val env arg dom in
-	(subst1 c codom, c::l)
+    let _,dom,codom =
+      try decompose_prod env t with
+	DestKO ->
+	Errors.anomaly
+	  (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+    in
+    let c = nf_val env arg dom in
+    (subst1 c codom, c::l)
   in
   let t,l = List.fold_right aux (args_of_accu accu) (t,[]) in
   t, List.rev l
@@ -227,7 +238,12 @@ and nf_bargs env b t =
   let len = block_size b in
   Array.init len
     (fun i ->
-      let _,dom,codom = try decompose_prod env !t with DestKO -> exit 124 in
+      let _,dom,codom =
+	try decompose_prod env !t with
+	  DestKO ->
+	  Errors.anomaly
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+      in
       let c = nf_val env (block_field b i) dom in
       t := subst1 c codom; c)
 
@@ -244,9 +260,11 @@ and nf_atom env atom =
       let env = push_rel (n,None,dom) env in
       let codom = nf_type env (codom vn) in
       mkProd(n,dom,codom)
+  | Ameta (mv,_) -> mkMeta mv
+  | Aevar (ev,_) -> mkEvar ev
   | _ -> fst (nf_atom_type env atom)
 
-and nf_atom_type env atom = 
+and nf_atom_type env atom =
   match atom with
   | Arel i ->
       let n = (nb_rel env - i) in
@@ -308,13 +326,24 @@ and nf_atom_type env atom =
       let env = push_rel (n,None,dom) env in
       let codom,s2 = nf_type_sort env (codom vn) in
       mkProd(n,dom,codom), mkSort (sort_of_product env s1 s2)
+  | Aevar(ev,ty) ->
+     let ty = nf_type env ty in
+     mkEvar ev, ty
+  | Ameta(mv,ty) ->
+     let ty = nf_type env ty in
+     mkMeta mv, ty
 
 and  nf_predicate env ind mip params v pT =
   match kind_of_value v, kind_of_term pT with
   | Vfun f, Prod _ ->
       let k = nb_rel env in
       let vb = f (mk_rel_accu k) in
-      let name,dom,codom = try decompose_prod env pT with DestKO -> exit 121 in
+      let name,dom,codom =
+	try decompose_prod env pT with
+	  DestKO ->
+	  Errors.anomaly
+	    (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
+      in
       let dep,body = 
 	nf_predicate (push_rel (name,None,dom) env) ind mip params vb codom in
       dep, mkLambda(name,dom,body)
@@ -330,7 +359,7 @@ and  nf_predicate env ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env v
 
-let native_norm env c ty =  
+let native_norm env sigma c ty =  
   if !Flags.no_native_compiler then
     error "Native_compute reduction has been disabled"
   else
@@ -340,7 +369,7 @@ let native_norm env c ty =
   Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
   *)
   let ml_filename, prefix = Nativelib.get_ml_filename () in
-  let code, upd = mk_norm_code penv prefix c in
+  let code, upd = mk_norm_code penv sigma prefix c in
   match Nativelib.compile ml_filename code with
     | 0,fn ->
         if !Flags.debug then Pp.msg_debug (Pp.str "Running norm ...");
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index ecc3489bee..a589846b9a 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -9,7 +9,11 @@ open Names
 open Term
 open Environ
 open Reduction
+open Evd
+open Nativelambda
 
 (** This module implements normalization by evaluation to OCaml code *)
 
-val native_norm : env -> constr -> types -> constr
+val evars_of_evar_map : evar_map -> evars
+
+val native_norm : env -> evars -> constr -> types -> constr
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a7e1cf481b..74248301d4 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -709,17 +709,18 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
 				   str "unresolved arguments remain.")
 	    | NATIVEcast ->
  	      let cj = pretype empty_tycon env evdref lvar c in
-	      let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in
-		if not (occur_existential cty || occur_existential tval) then
-		  begin 
-		    try 
-		      ignore (Nativeconv.native_conv Reduction.CUMUL env cty tval); cj
-		    with Reduction.NotConvertible -> 
-		      error_actual_type_loc loc env !evdref cj tval 
-                        (ConversionFailed (env,cty,tval))
-		  end
-		else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++
-				   str "unresolved arguments remain.")
+	      let cty = nf_evar !evdref cj.uj_type and
+		  tval = nf_evar !evdref tj.utj_val in
+	      let evars = Nativenorm.evars_of_evar_map !evdref in
+	      begin
+	      try
+		ignore
+		  (Nativeconv.native_conv Reduction.CUMUL evars env cty tval);
+		cj
+	      with Reduction.NotConvertible -> 
+		error_actual_type_loc loc env !evdref cj tval 
+                  (ConversionFailed (env,cty,tval))
+	      end
 
 	    | _ -> 
  	      pretype (mk_tycon tval) env evdref lvar c