[native_compute] Fix handling of evars in conversion

8 files changed, 44 insertions, 29 deletions

diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index 613b2f2ec..8fa254053 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -148,7 +148,7 @@ type symbol =
   | SymbMatch of annot_sw
   | SymbInd of inductive
   | SymbMeta of metavariable
-  | SymbEvar of existential
+  | SymbEvar of Evar.t
   | SymbLevel of Univ.Level.t
 
 let dummy_symb = SymbValue (dummy_value ())
@@ -162,8 +162,7 @@ let eq_symbol sy1 sy2 =
   | SymbMatch sw1, SymbMatch sw2 -> eq_annot_sw sw1 sw2
   | SymbInd ind1, SymbInd ind2 -> eq_ind ind1 ind2
   | SymbMeta m1, SymbMeta m2 -> Int.equal m1 m2
-  | SymbEvar (evk1,args1), SymbEvar (evk2,args2) ->
-     Evar.equal evk1 evk2 && Array.for_all2 Constr.equal args1 args2
+  | SymbEvar evk1, SymbEvar evk2 -> Evar.equal evk1 evk2
   | SymbLevel l1, SymbLevel l2 -> Univ.Level.equal l1 l2
   | _, _ -> false
 
@@ -176,10 +175,7 @@ let hash_symbol symb =
   | SymbMatch sw -> combinesmall 5 (hash_annot_sw sw)
   | SymbInd ind -> combinesmall 6 (ind_hash ind)
   | SymbMeta m -> combinesmall 7 m
-  | SymbEvar (evk,args) ->
-     let evh = Evar.hash evk in
-     let hl = Array.fold_left (fun h t -> combine h (Constr.hash t)) evh args in
-     combinesmall 8 hl
+  | SymbEvar evk -> combinesmall 8 (Evar.hash evk)
   | SymbLevel l -> combinesmall 9 (Univ.Level.hash l)
 
 module HashedTypeSymbol = struct
@@ -1047,11 +1043,12 @@ let ml_of_instance instance u =
      let tyn = fresh_lname Anonymous in
      let i = push_symbol (SymbMeta mv) in
      MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|])
-  | Levar(ev,ty) ->
+  | Levar(evk,ty,args) ->
      let tyn = fresh_lname Anonymous in
-     let i = push_symbol (SymbEvar ev) in
+     let i = push_symbol (SymbEvar evk) in
+     let args = MLarray(Array.map (ml_of_lam env l) args) in
      MLlet(tyn, ml_of_lam env l ty,
-       MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn|]))
+       MLapp(MLprimitive Mk_evar, [|get_evar_code i;MLlocal tyn; args|]))
   | Lprod(dom,codom) ->
       let dom = ml_of_lam env l dom in
       let codom = ml_of_lam env l codom in
diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli
index d08f49095..7d20054f7 100644
--- a/kernel/nativecode.mli
+++ b/kernel/nativecode.mli
@@ -44,7 +44,7 @@ val get_ind : symbols -> int -> inductive
 
 val get_meta : symbols -> int -> metavariable
 
-val get_evar : symbols -> int -> existential
+val get_evar : symbols -> int -> Evar.t
 
 val get_level : symbols -> int -> Univ.Level.t
 
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml
index 6c755290d..bfa982136 100644
--- a/kernel/nativeconv.ml
+++ b/kernel/nativeconv.ml
@@ -60,7 +60,12 @@ and conv_atom env pb lvl a1 a2 cu =
   if a1 == a2 then cu
   else
     match a1, a2 with
-    | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false
+    | Ameta (m1,_), Ameta (m2,_) ->
+      if Int.equal m1 m2 then cu else raise NotConvertible
+    | Aevar (ev1,_,args1), Aevar (ev2,_,args2) ->
+      if Evar.equal ev1 ev2 then
+        Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu
+      else raise NotConvertible
     | Arel i1, Arel i2 -> 
 	if Int.equal i1 i2 then cu else raise NotConvertible
     | Aind (ind1,u1), Aind (ind2,u2) ->
@@ -112,7 +117,7 @@ and conv_atom env pb lvl a1 a2 cu =
        else conv_accu env CONV lvl ac1 ac2 cu
     | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _
     | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _
-    | Aproj _, _ -> raise NotConvertible
+    | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible
 
 (* Precondition length t1 = length f1 = length f2 = length t2 *)
 and conv_fix env lvl t1 f1 t2 f2 cu =
diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli
index 928283a4d..48ad88444 100644
--- a/kernel/nativeinstr.mli
+++ b/kernel/nativeinstr.mli
@@ -23,7 +23,7 @@ and lambda =
   | Lrel          of Name.t * int 
   | Lvar          of Id.t
   | Lmeta         of metavariable * lambda (* type *)
-  | Levar         of existential * lambda (* type *)
+  | Levar         of Evar.t * lambda (* type *) * lambda array (* arguments *)
   | Lprod         of lambda * lambda 
   | Llam          of Name.t array * lambda  
   | Llet          of Name.t * lambda * lambda
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index b333b0fb9..29b3e59da 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -453,11 +453,12 @@ let rec lambda_of_constr env sigma c =
      let ty = meta_type sigma mv in
      Lmeta (mv, lambda_of_constr env sigma ty)
 
-  | Evar ev ->
+  | Evar (evk,args as ev) ->
      (match evar_value sigma ev with
      | None ->
 	let ty = evar_type sigma ev in
-	Levar(ev, lambda_of_constr env sigma ty)
+        let args = Array.map (lambda_of_constr env sigma) args in
+        Levar(evk, lambda_of_constr env sigma ty, args)
      | Some t -> lambda_of_constr env sigma t)
 
   | Cast (c, _, _) -> lambda_of_constr env sigma c
diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml
index 95a8fc5a4..3d47b1672 100644
--- a/kernel/nativevalues.ml
+++ b/kernel/nativevalues.ml
@@ -61,7 +61,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of existential * t
+  | Aevar of Evar.t * t * t array
   | Aproj of Constant.t * accumulator
 
 let accumulate_tag = 0
@@ -132,8 +132,8 @@ let mk_prod_accu s dom codom =
 let mk_meta_accu mv ty =
   mk_accu (Ameta (mv,ty))
 
-let mk_evar_accu ev ty =
-  mk_accu (Aevar (ev,ty))
+let mk_evar_accu ev ty args =
+  mk_accu (Aevar (ev,ty,args))
 
 let mk_proj_accu kn c = 
   mk_accu (Aproj (kn,c))
diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli
index 17d6978cd..993842740 100644
--- a/kernel/nativevalues.mli
+++ b/kernel/nativevalues.mli
@@ -51,7 +51,7 @@ type atom =
   | Acofixe of t array * t array * int * t
   | Aprod of Name.t * t * (t -> t)
   | Ameta of metavariable * t
-  | Aevar of existential * t
+  | Aevar of Evar.t * t (* type *) * t array (* arguments *)
   | Aproj of Constant.t * accumulator
 
 (* Constructors *)
@@ -68,7 +68,7 @@ val mk_prod_accu : Name.t -> t -> t -> t
 val mk_fix_accu : rec_pos  -> int -> t array -> t array -> t
 val mk_cofix_accu : int -> t array -> t array -> t
 val mk_meta_accu : metavariable -> t
-val mk_evar_accu : existential -> t -> t
+val mk_evar_accu : Evar.t -> t -> t array -> t
 val mk_proj_accu : Constant.t -> accumulator -> t
 val upd_cofix : t -> t -> unit
 val force_cofix : t -> t 
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 18ae22ab6..b41e15f5a 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -224,7 +224,7 @@ and nf_accu env sigma accu =
   if Int.equal (accu_nargs accu) 0 then nf_atom env sigma atom
   else
     let a,typ = nf_atom_type env sigma atom in
-    let _, args = nf_args env sigma accu typ in
+    let _, args = nf_args env sigma (args_of_accu accu) typ in
     mkApp(a,Array.of_list args)
 
 and nf_accu_type env sigma accu =
@@ -232,10 +232,10 @@ and nf_accu_type env sigma accu =
   if Int.equal (accu_nargs accu) 0 then nf_atom_type env sigma atom
   else
     let a,typ = nf_atom_type env sigma atom in
-    let t, args = nf_args env sigma accu typ in
+    let t, args = nf_args env sigma (args_of_accu accu) typ in
     mkApp(a,Array.of_list args), t
 
-and nf_args env sigma accu t =
+and nf_args env sigma args t =
   let aux arg (t,l) = 
     let _,dom,codom =
       try decompose_prod env t with
@@ -246,7 +246,7 @@ and nf_args env sigma accu t =
     let c = nf_val env sigma arg dom in
     (subst1 c codom, c::l)
   in
-  let t,l = Array.fold_right aux (args_of_accu accu) (t,[]) in
+  let t,l = Array.fold_right aux args (t,[]) in
   t, List.rev l
 
 and nf_bargs env sigma b t =
@@ -277,7 +277,6 @@ and nf_atom env sigma atom =
       let codom = nf_type env sigma (codom vn) in
       mkProd(n,dom,codom)
   | Ameta (mv,_) -> mkMeta mv
-  | Aevar (ev,_) -> mkEvar ev
   | Aproj(p,c) ->
       let c = nf_accu env sigma c in
 	mkProj(Projection.make p true,c)
@@ -347,9 +346,9 @@ and nf_atom_type env sigma atom =
       let env = push_rel (LocalAssum (n,dom)) env in
       let codom,s2 = nf_type_sort env sigma (codom vn) in
       mkProd(n,dom,codom), Typeops.type_of_product env n s1 s2
-  | Aevar(ev,ty) ->
-     let ty = nf_type env sigma ty in
-     mkEvar ev, ty
+  | Aevar(evk,ty,args) ->
+    let ty = nf_type env sigma ty in
+    nf_evar env sigma evk ty args
   | Ameta(mv,ty) ->
      let ty = nf_type env sigma ty in
      mkMeta mv, ty
@@ -386,6 +385,19 @@ and  nf_predicate env sigma ind mip params v pT =
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_type env sigma v
 
+and nf_evar env sigma evk ty args =
+  let evi = try Evd.find sigma evk with Not_found -> assert false in
+  let hyps = Environ.named_context_of_val (Evd.evar_filtered_hyps evi) in
+  if List.is_empty hyps then begin
+    assert (Int.equal (Array.length args) 0);
+    mkEvar (evk, [||]), ty
+  end
+  else
+    let fold accu d = Term.mkNamedProd_or_LetIn d accu in
+    let t = List.fold_left fold ty hyps in
+    let ty, args = nf_args env sigma args t in
+    mkEvar (evk, Array.of_list args), ty
+
 let evars_of_evar_map sigma =
   { Nativelambda.evars_val = Evd.existential_opt_value sigma;
     Nativelambda.evars_typ = Evd.existential_type sigma;