Merge PR #935: Handling evars in the VM

12 files changed, 68 insertions, 17 deletions

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