Handling evars in the VM.

We simply treat them as as an application of an atom to its instance,
and in the decompilation phase we reconstruct the instance from the stack.

This grants wish BZ#5659.

12 files changed, 68 insertions, 17 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index aa6c49bc7..05399cc04 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -184,6 +184,7 @@ type fv_elem =
   | FVnamed of Id.t
   | FVrel of int
   | FVuniv_var of int
+  | FVevar of Evar.t
 
 type fv = fv_elem array
 
@@ -198,12 +199,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
 
@@ -257,6 +261,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 c8fbb27a9..47d8d9564 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -138,6 +138,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 3104d5751..3619bb94e 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 8c7658147..84303fc21 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -116,7 +116,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
   | Atype _ , _ | _, Atype _ -> assert false
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 352ea74a4..0f6e09521 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 2d8a1d976..039b75e1c 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
   | Atype of Univ.Universe.t
 
@@ -304,13 +317,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)
@@ -330,6 +344,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 350f71372..8f39cfae4 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
   | Atype of Univ.Universe.t
 
@@ -92,6 +100,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