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.

1 files changed, 68 insertions, 42 deletions

diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 800c8e5fb..258f03efd 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -17,6 +17,8 @@ open Nativevalues
 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
@@ -41,23 +43,28 @@ type lambda =
 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;
+      evars_metas : metavariable -> types }
+
 (*s Constructors *)
-  
+
 let mkLapp f args =
   if Array.is_empty args then f
   else
     match f with
     | Lapp(f', args') -> Lapp (f', Array.append args' args)
     | _ -> Lapp(f, args)
-	  
+
 let mkLlam ids body =
   if Array.is_empty ids then body
   else 
     match body with
     | Llam(ids', body) -> Llam(Array.append ids ids', body)
     | _ -> Llam(ids, body)
-  
+
 let decompose_Llam lam =
   match lam with
   | Llam(ids,body) -> ids, body
@@ -103,8 +110,8 @@ let get_const_prefix env c =
 
 let map_lam_with_binders g f n lam =
   match lam with
-  | Lrel _ | Lvar _  | Lconst _ | Lval _
-  | Lsort _ | Lind _ | Lconstruct _ | Llazy | Lforce -> lam
+  | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ | Lconstruct _
+  | Llazy | Lforce | Lmeta _ | Levar _ -> lam
   | Lprod(dom,codom) -> 
       let dom' = f n dom in
       let codom' = f n codom in
@@ -199,8 +206,8 @@ let lam_subst_args subst args =
   
 let can_subst lam = 
   match lam with
-  | Lrel _ | Lvar _ | Lconst _
-  | Lval _ | Lsort _ | Lind _ | Llam _ | Lconstruct _ -> true
+  | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ | Llam _
+  | Lconstruct _ | Lmeta _ | Levar _ -> true
   | _ -> false
 
 let can_merge_if bt bf =
@@ -307,7 +314,7 @@ let rec occurence k kind lam =
 	if kind then false else raise Not_found
       else kind
   | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _
-  | Lconstruct _ | Llazy | Lforce -> kind
+  | Lconstruct _ | Llazy | Lforce | Lmeta _ | Levar _ -> kind
   | Lprod(dom, codom) ->
       occurence k (occurence k kind dom) codom
   | Llam(ids,body) ->
@@ -509,29 +516,48 @@ module Renv =
 let is_lazy t = (* APPROXIMATION *)
   isApp t || isLetIn t
 
+let evar_value sigma ev = sigma.evars_val ev
+
+let evar_type sigma ev = sigma.evars_typ ev
+
+let meta_type sigma mv = sigma.evars_metas mv
+
+let empty_evars =
+  { evars_val = (fun _ -> None);
+    evars_typ = (fun _ -> assert false);
+    evars_metas = (fun _ -> assert false) }
+
 let empty_ids = [||]
 
-let rec lambda_of_constr env c =
-(*  try *)
+let rec lambda_of_constr env sigma c =
   match kind_of_term c with
-  | Meta _ -> invalid_arg "Nativelambda.lambda_of_constr: Meta"
-  | Evar _ -> invalid_arg "Nativelambda.lambda_of_constr : Evar"
+  | Meta mv ->
+     let ty = meta_type sigma mv in
+     Lmeta (mv, lambda_of_constr env sigma ty)
 
-  | Cast (c, _, _) -> lambda_of_constr env c
+  | Evar ev ->
+     (match evar_value sigma ev with
+     | None ->
+	let ty = evar_type sigma ev in
+	Levar(ev, lambda_of_constr env sigma ty)
+     | Some t -> lambda_of_constr env sigma t)
+
+  | Cast (c, _, _) -> lambda_of_constr env sigma c
 
   | Rel i -> Renv.get env i
 
   | Var id -> Lvar id
 
   | Sort s -> Lsort s
+
   | Ind ind ->
       let prefix = get_mind_prefix !global_env (fst ind) in
       Lind (prefix, ind)
-	
+
   | Prod(id, dom, codom) ->
-      let ld = lambda_of_constr env dom in
+      let ld = lambda_of_constr env sigma dom in
       Renv.push_rel env id;
-      let lc = lambda_of_constr env codom in
+      let lc = lambda_of_constr env sigma codom in
       Renv.pop env;
       Lprod(ld,  Llam([|id|], lc))
 
@@ -539,22 +565,22 @@ let rec lambda_of_constr env c =
       let params, body = decompose_lam c in
       let ids = get_names (List.rev params) in
       Renv.push_rels env ids;
-      let lb = lambda_of_constr env body in
+      let lb = lambda_of_constr env sigma body in
       Renv.popn env (Array.length ids);
       mkLlam ids lb
 
   | LetIn(id, def, _, body) ->
-      let ld = lambda_of_constr env def in
+      let ld = lambda_of_constr env sigma def in
       Renv.push_rel env id;
-      let lb = lambda_of_constr env body in
+      let lb = lambda_of_constr env sigma body in
       Renv.pop env;
       Llet(id, ld, lb)
 
-  | App(f, args) -> lambda_of_app env f args
+  | App(f, args) -> lambda_of_app env sigma f args
 
-  | Const _ -> lambda_of_app env c empty_args
+  | Const _ -> lambda_of_app env sigma c empty_args
 
-  | Construct _ ->  lambda_of_app env c empty_args
+  | Construct _ ->  lambda_of_app env sigma c empty_args
 
   | Case(ci,t,a,branches) ->  
       let (mind,i as ind) = ci.ci_ind in
@@ -571,14 +597,14 @@ let rec lambda_of_constr env c =
           asw_prefix = prefix}
       in
       (* translation of the argument *)
-      let la = lambda_of_constr env a in
+      let la = lambda_of_constr env sigma a in
       (* translation of the type *)
-      let lt = lambda_of_constr env t in
+      let lt = lambda_of_constr env sigma t in
       (* translation of branches *)
       let mk_branch i b =
 	let cn = (ind,i+1) in
 	let _, arity = tbl.(i) in
-	let b = lambda_of_constr env b in
+	let b = lambda_of_constr env sigma b in
 	if Int.equal arity 0 then (cn, empty_ids, b)
 	else 
 	  match b with
@@ -592,20 +618,20 @@ let rec lambda_of_constr env c =
       Lcase(annot_sw, lt, la, bs)
 	
   | Fix(rec_init,(names,type_bodies,rec_bodies)) ->
-      let ltypes = lambda_of_args env 0 type_bodies in
+      let ltypes = lambda_of_args env sigma 0 type_bodies in
       Renv.push_rels env names;
-      let lbodies = lambda_of_args env 0 rec_bodies in
+      let lbodies = lambda_of_args env sigma 0 rec_bodies in
       Renv.popn env (Array.length names);
       Lfix(rec_init, (names, ltypes, lbodies))
 	
   | CoFix(init,(names,type_bodies,rec_bodies)) ->
-      let ltypes = lambda_of_args env 0 type_bodies in 
+      let ltypes = lambda_of_args env sigma 0 type_bodies in 
       Renv.push_rels env names;
-      let lbodies = lambda_of_args env 0 rec_bodies in
+      let lbodies = lambda_of_args env sigma 0 rec_bodies in
       Renv.popn env (Array.length names);
       Lcofix(init, (names, ltypes, lbodies))
 
-and lambda_of_app env f args =
+and lambda_of_app env sigma f args =
   match kind_of_term f with
   | Const kn ->
       let kn = get_allias !global_env kn in
@@ -613,7 +639,7 @@ and lambda_of_app env f args =
       begin match cb.const_body with
       | Def csubst ->
           if cb.const_inline_code then
-            lambda_of_app env (Lazyconstr.force csubst) args
+            lambda_of_app env sigma (Lazyconstr.force csubst) args
           else
           let prefix = get_const_prefix !global_env kn in
           let t =
@@ -621,31 +647,31 @@ and lambda_of_app env f args =
               mkLapp Lforce [|Lconst (prefix, kn)|]
             else Lconst (prefix, kn)
           in
-        mkLapp t (lambda_of_args env 0 args)
+        mkLapp t (lambda_of_args env sigma 0 args)
       | OpaqueDef _ | Undef _ ->
           let prefix = get_const_prefix !global_env kn in
-          mkLapp (Lconst (prefix, kn)) (lambda_of_args env 0 args)
+          mkLapp (Lconst (prefix, kn)) (lambda_of_args env sigma 0 args)
       end
   | Construct c ->
       let tag, nparams, arity = Renv.get_construct_info env c in
       let expected = nparams + arity in
       let nargs = Array.length args in
       if Int.equal nargs expected then 
-	let args = lambda_of_args env nparams args in
+	let args = lambda_of_args env sigma nparams args in
 	makeblock !global_env c tag args
       else
         let prefix = get_mind_prefix !global_env (fst (fst c)) in
-        mkLapp (Lconstruct (prefix, c)) (lambda_of_args env 0 args)
+        mkLapp (Lconstruct (prefix, c)) (lambda_of_args env sigma 0 args)
   | _ -> 
-      let f = lambda_of_constr env f in
-      let args = lambda_of_args env 0 args in
+      let f = lambda_of_constr env sigma f in
+      let args = lambda_of_args env sigma 0 args in
       mkLapp f args
 	
-and lambda_of_args env start args =
+and lambda_of_args env sigma start args =
   let nargs = Array.length args in
   if start < nargs then
     Array.init (nargs - start) 
-      (fun i -> lambda_of_constr env args.(start + i))
+      (fun i -> lambda_of_constr env sigma args.(start + i))
   else empty_args
 
 let optimize lam =
@@ -657,12 +683,12 @@ let optimize lam =
     (msgerrnl (str "Remove let = \n" ++ pp_lam lam);flush_all()); *)
   lam
 
-let lambda_of_constr env c =
+let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
   let ids = List.rev_map (fun (id, _, _) -> id) !global_env.env_rel_context in
   Renv.push_rels env (Array.of_list ids);
-  let lam = lambda_of_constr env c in
+  let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
     (msgerrnl (str "Constr = \n" ++ pr_constr c);flush_all()); 
     (msgerrnl (str "Lambda = \n" ++ pp_lam lam);flush_all());