Merge PR #935: Handling evars in the VM

16 files changed, 119 insertions, 22 deletions

diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index bb7a963aa..2ddf927d9 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -36,6 +36,10 @@ let print_idkey idk =
       print_string ")"
   | VarKey id -> print_string (Id.to_string id)
   | RelKey i -> print_string "~";print_int i
+  | EvarKey evk ->
+    print_string "Evar(";
+    print_int (Evar.repr evk);
+    print_string ")"
 
 let rec ppzipper z =
   match z with
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 586ef1709..6ed1ba539 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -180,6 +180,7 @@ type fv_elem =
   | FVnamed of Id.t
   | FVrel of int
   | FVuniv_var of int
+  | FVevar of Evar.t
 
 type fv = fv_elem array
 
@@ -194,12 +195,15 @@ type t = fv_elem
 
 let compare e1 e2 = match e1, e2 with
 | FVnamed id1, FVnamed id2 -> Id.compare id1 id2
-| FVnamed _, _ -> -1
+| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1
 | FVrel _, FVnamed _ -> 1
 | FVrel r1, FVrel r2 -> Int.compare r1 r2
-| FVrel _, FVuniv_var _ -> -1
+| FVrel _, (FVuniv_var _ | FVevar _) -> -1
 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2
-| FVuniv_var i1, _ -> 1
+| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1
+| FVuniv_var i1, FVevar _ -> -1
+| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1
+| FVevar e1, FVevar e2 -> Evar.compare e1 e2
 
 end
 
@@ -252,6 +256,7 @@ let pp_fv_elem = function
   | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")"
   | FVrel i -> str "Rel(" ++ int i ++ str ")"
   | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")"
+  | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")"
 
 let rec pp_instr i =
   match i with
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 71dd65186..11e07c00e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -137,6 +137,7 @@ type fv_elem =
   FVnamed of Id.t
 | FVrel of int
 | FVuniv_var of int
+| FVevar of Evar.t
 
 type fv = fv_elem array
 
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 0d7619e9f..10f82438c 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -257,6 +257,15 @@ let pos_universe_var i r sz =
       r.in_env := push_fv db env;
       Kenvacc(r.offset + pos)
 
+let pos_evar evk r =
+  let env = !(r.in_env) in
+  let cid = FVevar evk in
+  try Kenvacc(r.offset + find_at cid env)
+  with Not_found ->
+    let pos = env.size in
+    r.in_env := push_fv cid env;
+    Kenvacc (r.offset + pos)
+
 (*i  Examination of the continuation *)
 
 (* Discard all instructions up to the next label.                        *)
@@ -427,6 +436,7 @@ let compile_fv_elem reloc fv sz cont =
   | FVrel i -> pos_rel i reloc sz :: cont
   | FVnamed id -> pos_named id reloc :: cont
   | FVuniv_var i -> pos_universe_var i reloc sz :: cont
+  | FVevar evk -> pos_evar evk reloc :: cont
 
 let rec compile_fv reloc l sz cont =
   match l with
@@ -471,6 +481,12 @@ let rec compile_lam env reloc lam sz cont =
 
   | Lvar id -> pos_named id reloc :: cont
 
+  | Levar (evk, args) ->
+      if Array.is_empty args then
+        compile_fv_elem reloc (FVevar evk) sz cont
+      else
+        comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont
+
   | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont
 
   | Lind (ind,u) ->
diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli
index 2d9ec6050..c6f63872b 100644
--- a/kernel/cinstr.mli
+++ b/kernel/cinstr.mli
@@ -20,6 +20,7 @@ type uint =
 and lambda =
   | Lrel          of Name.t * int
   | Lvar          of Id.t
+  | Levar         of Evar.t * lambda array
   | Lprod         of lambda * lambda
   | Llam          of Name.t array * lambda
   | Llet          of Name.t * lambda * lambda
diff --git a/kernel/clambda.ml b/kernel/clambda.ml
index 636ed3510..7b637c20e 100644
--- a/kernel/clambda.ml
+++ b/kernel/clambda.ml
@@ -29,6 +29,9 @@ let rec pp_lam lam =
   match lam with
   | Lrel (id,n) -> pp_rel id n
   | Lvar id -> Id.print id
+  | Levar (evk, args) ->
+    hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++
+      prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")")
   | Lprod(dom,codom) -> hov 1
                           (str "forall(" ++
                            pp_lam dom ++
@@ -148,6 +151,9 @@ let shift subst = subs_shft (1, subst)
 let rec map_lam_with_binders g f n lam =
   match lam with
   | Lrel _ | Lvar _  | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam
+  | Levar (evk, args) ->
+    let args' = Array.smartmap (f n) args in
+    if args == args' then lam else Levar (evk, args')
   | Lprod(dom,codom) ->
     let dom' = f n dom in
     let codom' = f n codom in
@@ -344,6 +350,8 @@ let rec occurrence k kind lam =
       if kind then false else raise Not_found
     else kind
   | Lvar _  | Lconst _  | Lval _ | Lsort _ | Lind _ -> kind
+  | Levar (_, args) ->
+    occurrence_args k kind args
   | Lprod(dom, codom) ->
     occurrence k (occurrence k kind dom) codom
   | Llam(ids,body) ->
@@ -600,7 +608,9 @@ open Renv
 let rec lambda_of_constr env c =
   match Constr.kind c with
   | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta")
-  | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar")
+  | Evar (evk, args) ->
+    let args = lambda_of_args env 0 args in
+    Levar (evk, args)
 
   | Cast (c, _, _) -> lambda_of_constr env c
 
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 236d83576..a693e62a6 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -150,6 +150,7 @@ and slot_for_fv env fv =
         env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
+  | FVevar evk -> val_of_evar evk
   | FVuniv_var idu ->
     assert false
 
diff --git a/kernel/vars.ml b/kernel/vars.ml
index b3b3eff62..56d3f11b9 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -310,6 +310,3 @@ let subst_instance_constr subst c =
 let subst_instance_context s ctx = 
   if Univ.Instance.is_empty s then ctx
   else Context.Rel.map (fun x -> subst_instance_constr s x) ctx
-
-type id_key = Constant.t tableKey
-let eq_id_key x y = Names.eq_table_key Constant.equal x y
diff --git a/kernel/vars.mli b/kernel/vars.mli
index b74d25260..3d3a26e90 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -137,6 +137,3 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co
 (** Instance substitution for polymorphism. *)
 val subst_instance_constr : Instance.t -> constr -> constr
 val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t
-
-type id_key = Constant.t tableKey
-val eq_id_key : id_key -> id_key -> bool
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index ad9aa4267..f11803b67 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -115,7 +115,7 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
 	conv_stack env k stk1 stk2 cu
     else raise NotConvertible
   | Aid ik1, Aid ik2 ->
-    if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+    if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
 	conv_stack env k stk1 stk2 cu
       else raise NotConvertible
   | Asort s1, Asort s2 ->
diff --git a/kernel/vm.ml b/kernel/vm.ml
index f0bae98dc..a1b0c697c 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -28,7 +28,6 @@ let popstop_code i =
 
 let stop = popstop_code 0
 
-
 (************************************************)
 (* Abstract machine *****************************)
 (************************************************)
@@ -70,7 +69,6 @@ let apply_varray vf varray =
       interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1)
     end
 
-(* Functions over vfun *)
 let mkrel_vstack k arity =
   let max = k + arity - 1 in
   Array.init arity (fun i -> val_of_rel (max - i))
diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml
index 2a784fdf4..a286d2551 100644
--- a/kernel/vmvalues.ml
+++ b/kernel/vmvalues.ml
@@ -118,8 +118,21 @@ type vswitch = {
 
 (* Do not edit this type without editing C code, especially "coq_values.h" *)
 
+type id_key =
+| ConstKey of Constant.t
+| VarKey of Id.t
+| RelKey of Int.t
+| EvarKey of Evar.t
+
+let eq_id_key k1 k2 = match k1, k2 with
+| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2
+| VarKey id1, VarKey id2 -> Id.equal id1 id2
+| RelKey n1, RelKey n2 -> Int.equal n1 n2
+| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2
+| _ -> false
+
 type atom =
-  | Aid of Vars.id_key
+  | Aid of id_key
   | Aind of inductive
   | Asort of Sorts.t
 
@@ -303,13 +316,14 @@ let val_of_proj kn v =
 
 module IdKeyHash =
 struct
-  type t = Constant.t tableKey
-  let equal = Names.eq_table_key Constant.equal
+  type t = id_key
+  let equal = eq_id_key
   open Hashset.Combine
   let hash = function
   | ConstKey c -> combinesmall 1 (Constant.hash c)
   | VarKey id -> combinesmall 2 (Id.hash id)
   | RelKey i -> combinesmall 3 (Int.hash i)
+  | EvarKey evk -> combinesmall 4 (Evar.hash evk)
 end
 
 module KeyTable = Hashtbl.Make(IdKeyHash)
@@ -329,6 +343,8 @@ let val_of_named id = val_of_idkey (VarKey id)
 
 let val_of_constant c = val_of_idkey (ConstKey c)
 
+let val_of_evar evk = val_of_idkey (EvarKey evk)
+
 external val_of_annot_switch : annot_switch -> values = "%identity"
 
 (*************************************************)
diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli
index 570e3606a..86debd5d5 100644
--- a/kernel/vmvalues.mli
+++ b/kernel/vmvalues.mli
@@ -54,8 +54,16 @@ val fun_code : vfun -> tcode
 val fix_code : vfix -> tcode
 val cofix_upd_code : to_update -> tcode
 
+type id_key =
+| ConstKey of Constant.t
+| VarKey of Id.t
+| RelKey of Int.t
+| EvarKey of Evar.t
+
+val eq_id_key : id_key -> id_key -> bool
+
 type atom =
-  | Aid of Vars.id_key
+  | Aid of id_key
   | Aind of inductive
   | Asort of Sorts.t
 
@@ -91,6 +99,7 @@ val val_of_str_const : structured_constant -> values
 val val_of_rel : int -> values
 val val_of_named : Id.t -> values
 val val_of_constant : Constant.t -> values
+val val_of_evar : Evar.t -> values
 val val_of_proj : Constant.t -> values -> values
 val val_of_atom : atom -> values
 
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 6b7ea2996..eb174936c 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -200,7 +200,26 @@ and nf_univ_args ~nb_univs mk env sigma stk =
   let (t,ty) = mk u in
   nf_stk ~from:nb_univs env sigma t ty stk
 
-and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
+and nf_evar env sigma evk stk =
+  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
+  let concl = Evd.evar_concl evi in
+  if List.is_empty hyps then
+    nf_stk env sigma (mkEvar (evk, [||])) concl stk
+  else match stk with
+  | Zapp args :: stk ->
+    (** We assume that there is no consecutive Zapp nodes in a VM stack. Is that
+        really an invariant? *)
+    let fold accu d = Term.mkNamedProd_or_LetIn d accu in
+    let t = List.fold_left fold concl hyps in
+    let t, args = nf_args env sigma args t in
+    let inst, args = Array.chop (List.length hyps) args in
+    let c = mkApp (mkEvar (evk, inst), args) in
+    nf_stk env sigma c t stk
+  | _ ->
+    CErrors.anomaly (Pp.str "Argument size mismatch when decompiling an evar")
+
+and constr_type_of_idkey env sigma (idkey : Vmvalues.id_key) stk =
   match idkey with
   | ConstKey cst ->
      let cbody = Environ.lookup_constant cst env in
@@ -218,6 +237,8 @@ and constr_type_of_idkey env sigma (idkey : Vars.id_key) stk =
       let n = (nb_rel env - i) in
       let ty = RelDecl.get_type (lookup_rel n env) in
       nf_stk env sigma (mkRel n) (lift n ty) stk
+  | EvarKey evk ->
+      nf_evar env sigma evk stk
 
 and nf_stk ?from:(from=0) env sigma c t stk  =
   match stk with
@@ -355,8 +376,8 @@ and nf_cofix env sigma cf =
   mkCoFix (init,(name,cft,cfb))
 
 let cbv_vm env sigma c t  =
-  if Termops.occur_meta_or_existential sigma c then
-    CErrors.user_err Pp.(str "vm_compute does not support existential variables.");
+  if Termops.occur_meta sigma c then
+    CErrors.user_err Pp.(str "vm_compute does not support metas.");
   (** This evar-normalizes terms beforehand *)
   let c = EConstr.to_constr sigma c in
   let t = EConstr.to_constr sigma t in
diff --git a/test-suite/bugs/closed/2850.v b/test-suite/bugs/closed/2850.v
deleted file mode 100644
index 64a93aeb0..000000000
--- a/test-suite/bugs/closed/2850.v
+++ /dev/null
@@ -1,2 +0,0 @@
-Definition id {A} (x : A) := x.
-Fail Compute id.
diff --git a/test-suite/success/vm_evars.v b/test-suite/success/vm_evars.v
new file mode 100644
index 000000000..2c8b099ef
--- /dev/null
+++ b/test-suite/success/vm_evars.v
@@ -0,0 +1,23 @@
+Fixpoint iter {A} (n : nat) (f : A -> A) (x : A) :=
+match n with
+| 0 => x
+| S n => iter n f (f x)
+end.
+
+Goal nat -> True.
+Proof.
+intros n.
+evar (f : nat -> nat).
+cut (iter 10 f 0 = 0).
+vm_compute.
+intros; constructor.
+instantiate (f := (fun x => x)).
+reflexivity.
+Qed.
+
+Goal exists x, x = 5 + 5.
+Proof.
+  eexists.
+  vm_compute.
+  reflexivity.
+Qed.