diff options
author | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:45:27 +0530 |
---|---|---|
committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2015-01-15 18:59:00 +0530 |
commit | 8309a98096facfba448c9d8d298ba3903145831a (patch) | |
tree | 38a09851cb687921193b4368a93eed34ccd55a58 /kernel | |
parent | 58153a5bc59bbde6534425d66a2fe5d9943eb44b (diff) |
Correct restriction of vm_compute when handling universe polymorphic
definitions. Instead of failing with an anomaly when trying to do
conversion or computation with the vm's, consider polymorphic constants
as being opaque and keep instances around. This way the code is still
correct but (obviously) incomplete for polymorphic definitions and we
avoid introducing an anomaly. The patch does nothing clever, it only
keeps around instances with constants/inductives and compile constant
bodies only for non-polymorphic definitions.
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/cbytecodes.ml | 6 | ||||
-rw-r--r-- | kernel/cbytecodes.mli | 4 | ||||
-rw-r--r-- | kernel/cbytegen.ml | 18 | ||||
-rw-r--r-- | kernel/cbytegen.mli | 4 | ||||
-rw-r--r-- | kernel/cemitcodes.ml | 14 | ||||
-rw-r--r-- | kernel/cemitcodes.mli | 4 | ||||
-rw-r--r-- | kernel/conv_oracle.ml | 10 | ||||
-rw-r--r-- | kernel/conv_oracle.mli | 3 | ||||
-rw-r--r-- | kernel/csymtable.ml | 14 | ||||
-rw-r--r-- | kernel/environ.ml | 4 | ||||
-rw-r--r-- | kernel/modops.ml | 2 | ||||
-rw-r--r-- | kernel/names.ml | 4 | ||||
-rw-r--r-- | kernel/names.mli | 3 | ||||
-rw-r--r-- | kernel/nativecode.ml | 6 | ||||
-rw-r--r-- | kernel/nativelambda.ml | 8 | ||||
-rw-r--r-- | kernel/nativelambda.mli | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 2 | ||||
-rw-r--r-- | kernel/univ.ml | 2 | ||||
-rw-r--r-- | kernel/univ.mli | 2 | ||||
-rw-r--r-- | kernel/vars.ml | 3 | ||||
-rw-r--r-- | kernel/vars.mli | 3 | ||||
-rw-r--r-- | kernel/vconv.ml | 11 | ||||
-rw-r--r-- | kernel/vm.ml | 13 | ||||
-rw-r--r-- | kernel/vm.mli | 8 |
24 files changed, 80 insertions, 70 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 473a14c24..ae679027d 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -27,7 +27,7 @@ let cofix_evaluated_tag = 6 type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -67,7 +67,7 @@ type instruction = (* nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (* nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (* size, tag *) | Kmakeprod @@ -185,7 +185,7 @@ let rec instruction ppf = function Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblt; print_string " bodies = "; Array.iter (fun lbl -> fprintf ppf " %i" lbl) lblb; - | Kgetglobal id -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) + | Kgetglobal (id,u) -> fprintf ppf "\tgetglobal %s" (Names.string_of_con id) | Kconst cst -> fprintf ppf "\tconst" | Kmakeblock(n, m) -> diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 225198fcc..b65268f72 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -23,7 +23,7 @@ val cofix_evaluated_tag : tag type structured_constant = | Const_sorts of sorts - | Const_ind of inductive + | Const_ind of pinductive | Const_b0 of tag | Const_bn of tag * structured_constant array @@ -60,7 +60,7 @@ type instruction = (** nb fv, init, lbl types, lbl bodies *) | Kclosurecofix of int * int * Label.t array * Label.t array (** nb fv, init, lbl types, lbl bodies *) - | Kgetglobal of constant + | Kgetglobal of pconstant | Kconst of structured_constant | Kmakeblock of int * tag (** size, tag *) | Kmakeprod diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 39d800737..65ee655da 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -422,7 +422,7 @@ let rec str_const c = end | _ -> Bconstr c end - | Ind (ind,u) -> Bstrconst (Const_ind ind) + | Ind ind -> Bstrconst (Const_ind ind) | Construct (((kn,j),i),u) -> begin (* spiwack: tries first to apply the run-time compilation @@ -486,12 +486,12 @@ let rec compile_fv reloc l sz cont = (* Compiling constants *) -let rec get_allias env kn = +let rec get_allias env (kn,u as p) = let cb = lookup_constant kn env in let tps = cb.const_body_code in (match Cemitcodes.force tps with | BCallias kn' -> get_allias env kn' - | _ -> kn) + | _ -> p) (* Compiling expressions *) @@ -700,10 +700,10 @@ and compile_const = (mkConstU (kn,u)) reloc args sz cont with Not_found -> if Int.equal nargs 0 then - Kgetglobal (get_allias !global_env kn) :: cont + Kgetglobal (get_allias !global_env (kn, u)) :: cont else comp_app (fun _ _ _ cont -> - Kgetglobal (get_allias !global_env kn) :: cont) + Kgetglobal (get_allias !global_env (kn,u)) :: cont) compile_constr reloc () args sz cont let compile env c = @@ -729,10 +729,10 @@ let compile_constant_body env = function | Def sb -> let body = Mod_subst.force_constr sb in match kind_of_term body with - | Const kn' -> + | Const (kn',u) -> (* we use the canonical name of the constant*) - let con= constant_of_kn (canonical_con (Univ.out_punivs kn')) in - BCallias (get_allias env con) + let con= constant_of_kn (canonical_con kn') in + BCallias (get_allias env (con,u)) | _ -> let res = compile env body in let to_patch = to_memory res in @@ -740,7 +740,7 @@ let compile_constant_body env = function (* Shortcut of the previous function used during module strengthening *) -let compile_alias kn = BCallias (constant_of_kn (canonical_con kn)) +let compile_alias (kn,u) = BCallias (constant_of_kn (canonical_con kn), u) (* spiwack: additional function which allow different part of compilation of the 31-bit integers *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index d0bfd46c0..eab36d8b2 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -13,7 +13,7 @@ val compile_constant_body : env -> constant_def -> body_code (** Shortcut of the previous function used during module strengthening *) -val compile_alias : constant -> body_code +val compile_alias : pconstant -> body_code (** spiwack: this function contains the information needed to perform the static compilation of int31 (trying and obtaining @@ -33,7 +33,7 @@ val dynamic_int31_compilation : bool -> comp_env -> works as follow: checks if all the arguments are non-pointers if they are applies the operation (second argument) if not all of them are, returns to a coq definition (third argument) *) -val op_compilation : int -> instruction -> constant -> bool -> comp_env -> +val op_compilation : int -> instruction -> pconstant -> bool -> comp_env -> constr array -> int -> bytecodes-> bytecodes (*spiwack: compiling function to insert dynamic decompilation before diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 209144044..3c9692a5c 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -20,7 +20,7 @@ open Mod_subst type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of pconstant type patch = reloc_info * int @@ -147,8 +147,8 @@ and slot_for_annot a = enter (Reloc_annot a); out_int 0 -and slot_for_getglobal id = - enter (Reloc_getglobal id); +and slot_for_getglobal p = + enter (Reloc_getglobal p); out_int 0 @@ -320,7 +320,7 @@ let rec subst_strcst s sc = match sc with | Const_sorts _ | Const_b0 _ -> sc | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) - | Const_ind(ind) -> let kn,i = ind in Const_ind((subst_mind s kn, i)) + | Const_ind(ind,u) -> let kn,i = ind in Const_ind((subst_mind s kn, i), u) let subst_patch s (ri,pos) = match ri with @@ -329,19 +329,19 @@ let subst_patch s (ri,pos) = let ci = {a.ci with ci_ind = (subst_mind s kn,i)} in (Reloc_annot {a with ci = ci},pos) | Reloc_const sc -> (Reloc_const (subst_strcst s sc), pos) - | Reloc_getglobal kn -> (Reloc_getglobal (fst (subst_con_kn s kn)), pos) + | Reloc_getglobal kn -> (Reloc_getglobal (subst_pcon s kn), pos) let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = | BCdefined of to_patch - | BCallias of constant + | BCallias of pconstant | BCconstant let subst_body_code s = function | BCdefined tp -> BCdefined (subst_to_patch s tp) - | BCallias kn -> BCallias (fst (subst_con_kn s kn)) + | BCallias (kn,u) -> BCallias (fst (subst_con_kn s kn), u) | BCconstant -> BCconstant type to_patch_substituted = body_code substituted diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 287c39304..cec901306 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -4,7 +4,7 @@ open Cbytecodes type reloc_info = | Reloc_annot of annot_switch | Reloc_const of structured_constant - | Reloc_getglobal of constant + | Reloc_getglobal of constant Univ.puniverses type patch = reloc_info * int @@ -25,7 +25,7 @@ val subst_to_patch : Mod_subst.substitution -> to_patch -> to_patch type body_code = | BCdefined of to_patch - | BCallias of constant + | BCallias of constant Univ.puniverses | BCconstant diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 1c2eea17b..3b01538b9 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -40,12 +40,12 @@ let empty = { cst_trstate = Cpred.full; } -let get_strategy { var_opacity; cst_opacity } = function +let get_strategy { var_opacity; cst_opacity } f = function | VarKey id -> (try Id.Map.find id var_opacity with Not_found -> default) | ConstKey c -> - (try Cmap.find c cst_opacity + (try Cmap.find (f c) cst_opacity with Not_found -> default) | RelKey _ -> Expand @@ -83,9 +83,11 @@ let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, expand the second one. *) -let oracle_order o l2r k1 k2 = - match get_strategy o k1, get_strategy o k2 with +let oracle_order f o l2r k1 k2 = + match get_strategy o f k1, get_strategy o f k2 with | Expand, _ -> true | Level n1, Opaque -> true | Level n1, Level n2 -> n1 < n2 | _ -> l2r (* use recommended default *) + +let get_strategy o = get_strategy o (fun x -> x) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 550076782..629912220 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -16,7 +16,8 @@ val empty : oracle If [oracle_order kn1 kn2] is true, then unfold kn1 first. Note: the oracle does not introduce incompleteness, it only tries to postpone unfolding of "opaque" constants. *) -val oracle_order : oracle -> bool -> constant tableKey -> constant tableKey -> bool +val oracle_order : ('a -> constant) -> oracle -> bool -> + 'a tableKey -> 'a tableKey -> bool (** Priority for the expansion of constant in the conversion test. * Higher levels means that the expansion is less prioritary. diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 794d94581..ed8b0a6d1 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -57,7 +57,7 @@ let set_global v = let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_ind i1, Const_ind i2 -> eq_ind i1 i2 +| Const_ind i1, Const_ind i2 -> Univ.eq_puniverses eq_ind i1 i2 | Const_b0 t1, Const_b0 t2 -> Int.equal t1 t2 | Const_bn (t1, a1), Const_bn (t2, a2) -> Int.equal t1 t2 && Array.equal eq_structured_constant a1 a2 @@ -67,7 +67,7 @@ let rec hash_structured_constant c = let open Hashset.Combine in match c with | Const_sorts s -> combinesmall 1 (Sorts.hash s) - | Const_ind i -> combinesmall 2 (ind_hash i) + | Const_ind (i,u) -> combinesmall 2 (combine (ind_hash i) (Univ.Instance.hash u)) | Const_b0 t -> combinesmall 3 (Int.hash t) | Const_bn (t, a) -> let fold h c = combine h (hash_structured_constant c) in @@ -142,7 +142,7 @@ let slot_for_annot key = AnnotTable.add annot_tbl key n; n -let rec slot_for_getglobal env kn = +let rec slot_for_getglobal env (kn,u) = let (cb,(_,rk)) = lookup_constant_key kn env in try key rk with NotEvaluated -> @@ -150,10 +150,12 @@ let rec slot_for_getglobal env kn = let pos = match Cemitcodes.force cb.const_body_code with | BCdefined(code,pl,fv) -> - let v = eval_to_patch env (code,pl,fv) in - set_global v + if Univ.Instance.is_empty u then + let v = eval_to_patch env (code,pl,fv) in + set_global v + else set_global (val_of_constant (kn,u)) | BCallias kn' -> slot_for_getglobal env kn' - | BCconstant -> set_global (val_of_constant kn) in + | BCconstant -> set_global (val_of_constant (kn,u)) in (*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some (Ephemeron.create pos); pos diff --git a/kernel/environ.ml b/kernel/environ.ml index 8b1e49919..0ebff440a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -594,7 +594,7 @@ let dispatch = let int31_op n op prim kn = { empty_reactive_info with vm_compiling = Some (Cbytegen.op_compilation n op kn); - native_compiling = Some (Nativelambda.compile_prim prim kn); + native_compiling = Some (Nativelambda.compile_prim prim (Univ.out_punivs kn)); } in @@ -602,7 +602,7 @@ fun rk value field -> (* subfunction which shortens the (very common) dispatch of operations *) let int31_op_from_const n op prim = match kind_of_term value with - | Const (kn,_) -> int31_op n op prim kn + | Const kn -> int31_op n op prim kn | _ -> anomaly ~label:"Environ.register" (Pp.str "should be a constant") in let int31_binop_from_const op prim = int31_op_from_const 2 op prim in diff --git a/kernel/modops.ml b/kernel/modops.ml index e04eb354e..392e667b8 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -337,7 +337,7 @@ let strengthen_const mp_from l cb resolver = in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias con) } + const_body_code = Cemitcodes.from_val (Cbytegen.compile_alias (con,u)) } let rec strengthen_mod mp_from mp_to mb = if mp_in_delta mb.mod_mp mb.mod_delta then mb diff --git a/kernel/names.ml b/kernel/names.ml index 2c2886623..b349ccb00 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -686,8 +686,6 @@ type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - let eq_table_key f ik1 ik2 = if ik1 == ik2 then true else match ik1,ik2 with @@ -696,8 +694,6 @@ let eq_table_key f ik1 ik2 = | RelKey k1, RelKey k2 -> Int.equal k1 k2 | _ -> false -let eq_id_key = eq_table_key Constant.UserOrd.equal - let eq_con_chk = Constant.UserOrd.equal let eq_mind_chk = MutInd.UserOrd.equal let eq_ind_chk (kn1,i1) (kn2,i2) = Int.equal i1 i2 && eq_mind_chk kn1 kn2 diff --git a/kernel/names.mli b/kernel/names.mli index 9fbe7d5e5..d82043da1 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -458,11 +458,8 @@ type inv_rel_key = int (** index in the [rel_context] part of environment starting by the end, {e inverse} of de Bruijn indice *) -type id_key = Constant.t tableKey - val eq_table_key : ('a -> 'a -> bool) -> 'a tableKey -> 'a tableKey -> bool val eq_constant_key : Constant.t -> Constant.t -> bool -val eq_id_key : id_key -> id_key -> bool (** equalities on constant and inductive names (for the checker) *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 433e2c505..66577fecc 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1772,7 +1772,7 @@ let compile_constant env sigma prefix ~interactive con cb = match cb.const_proj with | None -> begin match cb.const_body with - | Def t -> + | Def t when not cb.const_polymorphic -> let t = Mod_subst.force_constr t in let code = lambda_of_constr env sigma t in if !Flags.debug then Pp.msg_debug (Pp.str "Generated lambda code"); @@ -1902,8 +1902,8 @@ let compile_mind_deps env prefix ~interactive let rec compile_deps env sigma prefix ~interactive init t = match kind_of_term t with | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind - | Const (c,u) -> - let c = get_allias env c in + | Const c -> + let c,u = get_allias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index c5417b2b6..947e0a148 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -373,11 +373,11 @@ let makeblock env cn tag args = (* Translation of constants *) -let rec get_allias env kn = +let rec get_allias env (kn, u as p) = let tps = (lookup_constant kn env).const_body_code in match Cemitcodes.force tps with | Cemitcodes.BCallias kn' -> get_allias env kn' - | _ -> kn + | _ -> p (*i Global environment *) @@ -647,8 +647,8 @@ let rec lambda_of_constr env sigma c = and lambda_of_app env sigma f args = match kind_of_term f with - | Const (kn,u) -> - let kn = get_allias !global_env kn in + | Const (kn,u as c) -> + let kn,u = get_allias !global_env c in let cb = lookup_constant kn !global_env in (try let prefix = get_const_prefix !global_env kn in diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 10818e1aa..6a97edc40 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -27,7 +27,7 @@ val mk_lazy : lambda -> lambda val get_mind_prefix : env -> mutual_inductive -> string -val get_allias : env -> constant -> constant +val get_allias : env -> pconstant -> pconstant val lambda_of_constr : env -> evars -> Constr.constr -> lambda diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 62f454047..4153b323b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -350,7 +350,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = (* else the oracle tells which constant is to be expanded *) let oracle = Closure.oracle_of_infos infos in let (app1,app2) = - if Conv_oracle.oracle_order oracle l2r (conv_key fl1) (conv_key fl2) then + if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then match unfold_reference infos fl1 with | Some def1 -> ((lft1, whd def1 v1), appr2) | None -> diff --git a/kernel/univ.ml b/kernel/univ.ml index d5939c67e..e2a19b0e8 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1744,6 +1744,8 @@ type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t let out_punivs (x, y) = x let in_punivs x = (x, Instance.empty) +let eq_puniverses f (x, u) (y, u') = + f x y && Instance.equal u u' (** A context of universe levels with universe constraints, representiong local universe variables and constraints *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 36f3349c0..454134f21 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -306,6 +306,8 @@ type 'a puniverses = 'a * universe_instance val out_punivs : 'a puniverses -> 'a val in_punivs : 'a -> 'a puniverses +val eq_puniverses : ('a -> 'a -> bool) -> 'a puniverses -> 'a puniverses -> bool + (** A vector of universe levels with universe constraints, representiong local universe variables and associated constraints *) diff --git a/kernel/vars.ml b/kernel/vars.ml index 1685817a3..88c1e1038 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -336,3 +336,6 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else map_rel_context (fun x -> subst_instance_constr s x) ctx + +type id_key = pconstant tableKey +let eq_id_key x y = Names.eq_table_key (Univ.eq_puniverses Constant.equal) x y diff --git a/kernel/vars.mli b/kernel/vars.mli index bdbecdedc..fdd4603b5 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -87,3 +87,6 @@ val subst_univs_level_context : Univ.universe_level_subst -> rel_context -> rel_ (** Instance substitution for polymorphism. *) val subst_instance_constr : universe_instance -> constr -> constr val subst_instance_context : universe_instance -> rel_context -> rel_context + +type id_key = pconstant tableKey +val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 3f9345ff8..80b15f8ba 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -86,23 +86,24 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = match a1, a2 with - | Aind (kn1,i1), Aind(kn2,i2) -> - if eq_ind (kn1,i1) (kn2,i2) && compare_stack stk1 stk2 + | Aind ind1, Aind ind2 -> + if eq_puniverses eq_ind ind1 ind2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> - if eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible | Aiddef(ik1,v1), Aiddef(ik2,v2) -> begin try - if eq_table_key ik1 ik2 && compare_stack stk1 stk2 then + if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible with NotConvertible -> - if oracle_order (oracle_of_infos !infos) false ik1 ik2 then + if oracle_order Univ.out_punivs (oracle_of_infos !infos) + false ik1 ik2 then conv_whd env pb k (whd_stack v1 stk1) (Vatom_stk(a2,stk2)) cu else conv_whd env pb k (Vatom_stk(a1,stk1)) (whd_stack v2 stk2) cu end diff --git a/kernel/vm.ml b/kernel/vm.ml index a7e5a55c4..2cc1efe43 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -137,10 +137,11 @@ type vswitch = { (* Generally the first field is a code pointer. *) (* Do not edit this type without editing C code, especially "coq_values.h" *) + type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive + | Aid of Vars.id_key + | Aiddef of Vars.id_key * values + | Aind of pinductive (* Zippers *) @@ -306,11 +307,11 @@ let val_of_atom a = val_of_obj (obj_of_atom a) module IdKeyHash = struct - type t = id_key - let equal = Names.eq_id_key + type t = pconstant tableKey + let equal = Names.eq_table_key (Univ.eq_puniverses Constant.equal) open Hashset.Combine let hash = function - | ConstKey c -> combinesmall 1 (Constant.hash c) + | ConstKey (c,u) -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) end diff --git a/kernel/vm.mli b/kernel/vm.mli index fa88418ce..295ea83c4 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -24,9 +24,9 @@ type vswitch type arguments type atom = - | Aid of id_key - | Aiddef of id_key * values - | Aind of inductive + | Aid of Vars.id_key + | Aiddef of Vars.id_key * values + | Aind of pinductive (** Zippers *) @@ -54,7 +54,7 @@ type whd = 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 -> values +val val_of_constant : pconstant -> values external val_of_annot_switch : annot_switch -> values = "%identity" |