diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 15:34:46 +0200 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2015-10-16 15:34:46 +0200 |
commit | f93b5d45ed95816cb23ce2646437bb5037a17f72 (patch) | |
tree | e38ecd02addffe86cf05996c651fdd55034b7aaa /kernel | |
parent | 8cb3a606f7c72c32298fe028c9f98e44ea0d378b (diff) | |
parent | d1ce79ce293c9b77f2c6a9d0b9a8b4f84ea617e5 (diff) |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/fast_typeops.ml | 2 | ||||
-rw-r--r-- | kernel/nativeconv.ml | 115 | ||||
-rw-r--r-- | kernel/nativeconv.mli | 4 | ||||
-rw-r--r-- | kernel/reduction.ml | 32 | ||||
-rw-r--r-- | kernel/reduction.mli | 21 | ||||
-rw-r--r-- | kernel/typeops.ml | 4 | ||||
-rw-r--r-- | kernel/vconv.ml | 88 | ||||
-rw-r--r-- | kernel/vconv.mli | 8 |
8 files changed, 112 insertions, 162 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index d22abff10..063c9cf12 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -227,7 +227,7 @@ let judge_of_cast env c ct k expected_type = default_conv ~l2r:true CUMUL env ct expected_type | NATIVEcast -> let sigma = Nativelambda.empty_evars in - native_conv CUMUL sigma env ct expected_type + Nativeconv.native_conv CUMUL sigma env ct expected_type with NotConvertible -> error_actual_type env (make_judge c ct) expected_type diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d0aa96fd1..7ae66c485 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -16,21 +16,21 @@ open Nativecode (** This module implements the conversion test by compiling to OCaml code *) -let rec conv_val env pb lvl cu v1 v2 = - if v1 == v2 then () +let rec conv_val env pb lvl v1 v2 cu = + if v1 == v2 then cu else match kind_of_value v1, kind_of_value v2 with | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in - conv_val env CONV (lvl+1) cu (f1 v) (f2 v) + conv_val env CONV (lvl+1) (f1 v) (f2 v) cu | Vfun f1, _ -> - conv_val env CONV lvl cu v1 (fun x -> v2 x) + conv_val env CONV lvl v1 (fun x -> v2 x) cu | _, Vfun f2 -> - conv_val env CONV lvl cu (fun x -> v1 x) v2 + conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> - conv_accu env pb lvl cu k1 k2 + conv_accu env pb lvl k1 k2 cu | Vconst i1, Vconst i2 -> - if not (Int.equal i1 i2) then raise NotConvertible + if Int.equal i1 i2 then cu else raise NotConvertible | Vblock b1, Vblock b2 -> let n1 = block_size b1 in let n2 = block_size b2 in @@ -38,76 +38,76 @@ let rec conv_val env pb lvl cu v1 v2 = raise NotConvertible; let rec aux lvl max b1 b2 i cu = if Int.equal i max then - conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i) + conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu else - (conv_val env CONV lvl cu (block_field b1 i) (block_field b2 i); - aux lvl max b1 b2 (i+1) cu) + let cu = conv_val env CONV lvl (block_field b1 i) (block_field b2 i) cu in + aux lvl max b1 b2 (i+1) cu in aux lvl (n1-1) b1 b2 0 cu | Vaccu _, _ | Vconst _, _ | Vblock _, _ -> raise NotConvertible -and conv_accu env pb lvl cu k1 k2 = +and conv_accu env pb lvl k1 k2 cu = let n1 = accu_nargs k1 in let n2 = accu_nargs k2 in if not (Int.equal n1 n2) then raise NotConvertible; if Int.equal n1 0 then conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else - (conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu; - List.iter2 (conv_val env CONV lvl cu) (args_of_accu k1) (args_of_accu k2)) + let cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu in + List.fold_right2 (conv_val env CONV lvl) (args_of_accu k1) (args_of_accu k2) cu and conv_atom env pb lvl a1 a2 cu = - if a1 == a2 then () + if a1 == a2 then cu else match a1, a2 with | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false | Arel i1, Arel i2 -> - if not (Int.equal i1 i2) then raise NotConvertible + if Int.equal i1 i2 then cu else raise NotConvertible | Aind ind1, Aind ind2 -> - if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible + if eq_puniverses eq_ind ind1 ind2 then cu else raise NotConvertible | Aconstant c1, Aconstant c2 -> - if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible + if eq_puniverses eq_constant c1 c2 then cu else raise NotConvertible | Asort s1, Asort s2 -> - check_sort_cmp_universes env pb s1 s2 cu + sort_cmp_universes env pb s1 s2 cu | Avar id1, Avar id2 -> - if not (Id.equal id1 id2) then raise NotConvertible + if Id.equal id1 id2 then cu else raise NotConvertible | Acase(a1,ac1,p1,bs1), Acase(a2,ac2,p2,bs2) -> if not (eq_ind a1.asw_ind a2.asw_ind) then raise NotConvertible; - conv_accu env CONV lvl cu ac1 ac2; + let cu = conv_accu env CONV lvl ac1 ac2 cu in let tbl = a1.asw_reloc in let len = Array.length tbl in - if Int.equal len 0 then conv_val env CONV lvl cu p1 p2 + if Int.equal len 0 then conv_val env CONV lvl p1 p2 cu else begin - conv_val env CONV lvl cu p1 p2; - let max = len - 1 in - let rec aux i = - let tag,arity = tbl.(i) in - let ci = - if Int.equal arity 0 then mk_const tag - else mk_block tag (mk_rels_accu lvl arity) in - let bi1 = bs1 ci and bi2 = bs2 ci in - if Int.equal i max then conv_val env CONV (lvl + arity) cu bi1 bi2 - else (conv_val env CONV (lvl + arity) cu bi1 bi2; aux (i+1)) in - aux 0 + let cu = conv_val env CONV lvl p1 p2 cu in + let max = len - 1 in + let rec aux i cu = + let tag,arity = tbl.(i) in + let ci = + if Int.equal arity 0 then mk_const tag + else mk_block tag (mk_rels_accu lvl arity) in + let bi1 = bs1 ci and bi2 = bs2 ci in + if Int.equal i max then conv_val env CONV (lvl + arity) bi1 bi2 cu + else aux (i+1) (conv_val env CONV (lvl + arity) bi1 bi2 cu) in + aux 0 cu end | Afix(t1,f1,rp1,s1), Afix(t2,f2,rp2,s2) -> if not (Int.equal s1 s2) || not (Array.equal Int.equal rp1 rp2) then raise NotConvertible; - if f1 == f2 then () + if f1 == f2 then cu else conv_fix env lvl t1 f1 t2 f2 cu | (Acofix(t1,f1,s1,_) | Acofixe(t1,f1,s1,_)), (Acofix(t2,f2,s2,_) | Acofixe(t2,f2,s2,_)) -> if not (Int.equal s1 s2) then raise NotConvertible; - if f1 == f2 then () + if f1 == f2 then cu else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu | Aprod(_,d1,c1), Aprod(_,d2,c2) -> - conv_val env CONV lvl cu d1 d2; - let v = mk_rel_accu lvl in - conv_val env pb (lvl + 1) cu (d1 v) (d2 v) + let cu = conv_val env CONV lvl d1 d2 cu in + let v = mk_rel_accu lvl in + conv_val env pb (lvl + 1) (d1 v) (d2 v) cu | Aproj(p1,ac1), Aproj(p2,ac2) -> if not (Constant.equal p1 p2) then raise NotConvertible - else conv_accu env CONV lvl cu ac1 ac2 + else conv_accu env CONV lvl ac1 ac2 cu | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ | Aproj _, _ -> raise NotConvertible @@ -118,21 +118,15 @@ and conv_fix env lvl t1 f1 t2 f2 cu = let max = len - 1 in let fargs = mk_rels_accu lvl len in let flvl = lvl + len in - let rec aux i = - conv_val env CONV lvl cu t1.(i) t2.(i); + let rec aux i cu = + let cu = conv_val env CONV lvl t1.(i) t2.(i) cu in let fi1 = napply f1.(i) fargs in let fi2 = napply f2.(i) fargs in - if Int.equal i max then conv_val env CONV flvl cu fi1 fi2 - else (conv_val env CONV flvl cu fi1 fi2; aux (i+1)) in - aux 0 + if Int.equal i max then conv_val env CONV flvl fi1 fi2 cu + else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in + aux 0 cu -let native_conv pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin - let msg = "Native compiler is disabled, falling back to VM conversion test." in - Pp.msg_warning (Pp.str msg); - vm_conv pb env t1 t2 - end - else +let native_conv_gen pb sigma env univs t1 t2 = let penv = Environ.pre_env env in let ml_filename, prefix = get_ml_filename () in let code, upds = mk_conv_code penv sigma prefix t1 t2 in @@ -146,8 +140,25 @@ let native_conv pb sigma env t1 t2 = let time_info = Format.sprintf "Evaluation done in %.5f@." (t1 -. t0) in if !Flags.debug then Pp.msg_debug (Pp.str time_info); (* TODO change 0 when we can have deBruijn *) - conv_val env pb 0 (Environ.universes env) !rt1 !rt2 + fst (conv_val env pb 0 !rt1 !rt2 univs) end | _ -> anomaly (Pp.str "Compilation failure") -let _ = set_nat_conv native_conv +(* Wrapper for [native_conv] above *) +let native_conv cv_pb sigma env t1 t2 = + if Coq_config.no_native_compiler then begin + let msg = "Native compiler is disabled, falling back to VM conversion test." in + Pp.msg_warning (Pp.str msg); + vm_conv cv_pb env t1 t2 + end + else + let univs = Environ.universes env in + let b = + if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 + else Constr.eq_constr_univs univs t1 t2 + in + if not b then + let univs = (univs, checked_universes) in + let t1 = Term.it_mkLambda_or_LetIn t1 (Environ.rel_context env) in + let t2 = Term.it_mkLambda_or_LetIn t2 (Environ.rel_context env) in + let _ = native_conv_gen cv_pb sigma env univs t1 t2 in () diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 318a7d830..4dddb9fd3 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -12,3 +12,7 @@ open Nativelambda (** This module implements the conversion test by compiling to OCaml code *) val native_conv : conv_pb -> evars -> types conversion_function + +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 6e1c3c5b7..e081870ba 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -26,8 +26,6 @@ open Environ open Closure open Esubst -let left2right = ref false - let rec is_empty_stack = function [] -> true | Zupdate _::s -> is_empty_stack s @@ -208,9 +206,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = let cu1 = cmp_rec s1 s2 cuniv in (match (z1,z2) with | (Zlapp a1,Zlapp a2) -> - if !left2right then - Array.fold_left2 (fun cu x y -> f x y cu) cu1 a1 a2 - else Array.fold_right2 f a1 a2 cu1 + Array.fold_right2 f a1 a2 cu1 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> if not (eq_constant c1 c2) then raise NotConvertible @@ -632,7 +628,7 @@ let infer_cmp_universes env pb s0 s1 univs = let infer_convert_instances flex u u' (univs,cstrs) = (univs, Univ.enforce_eq_instances u u' cstrs) -let infered_universes : (UGraph.t * Univ.Constraint.t) universe_compare = +let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } @@ -665,7 +661,7 @@ let trans_conv_universes ?(l2r=false) ?(evars=fun _->None) reds = let trans_conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv_universes reds CUMUL l2r evars -let fconv = trans_fconv (Id.Pred.full, Cpred.full) +let fconv = trans_fconv full_transparent_state let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None) let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars @@ -680,7 +676,7 @@ let conv_leq_vecti ?(l2r=false) ?(evars=fun _->None) env v1 v2 = v1 v2 -let generic_conv cv_pb l2r evars reds env univs t1 t2 = +let generic_conv cv_pb ~l2r evars reds env univs t1 t2 = let (s, _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in s @@ -692,7 +688,7 @@ let infer_conv_universes cv_pb l2r evars reds env univs t1 t2 = in if b then cstrs else - let univs = ((univs, Univ.Constraint.empty), infered_universes) in + let univs = ((univs, Univ.Constraint.empty), inferred_universes) in let ((_,cstrs), _) = clos_fconv reds cv_pb l2r evars env univs t1 t2 in cstrs @@ -711,19 +707,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -(* option for conversion *) -let nat_conv = ref (fun cv_pb sigma -> - fconv cv_pb false (sigma.Nativelambda.evars_val)) -let set_nat_conv f = nat_conv := f - -let native_conv cv_pb sigma env t1 t2 = - if eq_constr t1 t2 then () - else begin - let t1 = (it_mkLambda_or_LetIn t1 (rel_context env)) in - let t2 = (it_mkLambda_or_LetIn t2 (rel_context env)) in - !nat_conv cv_pb sigma env t1 t2 - end - +(* This reference avoids always having to link C code with the kernel *) let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None)) let set_vm_conv f = vm_conv := f let vm_conv cv_pb env t1 t2 = @@ -734,11 +718,7 @@ let vm_conv cv_pb env t1 t2 = fconv cv_pb false (fun _->None) env t1 t2 let default_conv cv_pb ?(l2r=false) env t1 t2 = - try fconv cv_pb false (fun _ -> None) env t1 t2 - with Not_found | Invalid_argument _ -> - Pp.msg_warning (Pp.str "Compilation failed, falling back to standard conversion"); - fconv cv_pb false (fun _->None) env t1 t2 let default_conv_leq = default_conv CUMUL (* diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 2c1c0ec05..0bb855c67 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -10,8 +10,6 @@ open Term open Context open Environ -val left2right : bool ref - (*********************************************************************** s Reduction functions *) @@ -49,14 +47,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints -val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> UGraph.t -> unit - -(* val sort_cmp : *) -(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) +val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> + 'a * 'a universe_compare -> 'a * 'a universe_compare -(* val conv_sort : sorts conversion_function *) -(* val conv_sort_leq : sorts conversion_function *) +val checked_universes : UGraph.t universe_compare +val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -77,22 +72,20 @@ val conv_leq : val conv_leq_vecti : ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function +(** These conversion functions are used by module subtyping, which needs to infer + universe constraints inside the kernel *) val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> constr infer_conversion_function val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function -val generic_conv : conv_pb -> bool -> (existential->constr option) -> +val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_nat_conv : - (conv_pb -> Nativelambda.evars -> types conversion_function) -> unit -val native_conv : conv_pb -> Nativelambda.evars -> types conversion_function - val default_conv : conv_pb -> ?l2r:bool -> types conversion_function val default_conv_leq : ?l2r:bool -> types conversion_function diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 8895bae5d..09299f31d 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -300,7 +300,7 @@ let judge_of_cast env cj k tj = match k with | VMcast -> mkCast (cj.uj_val, k, expected_type), - vm_conv CUMUL env cj.uj_type expected_type + Reduction.vm_conv CUMUL env cj.uj_type expected_type | DEFAULTcast -> mkCast (cj.uj_val, k, expected_type), default_conv ~l2r:false CUMUL env cj.uj_type expected_type @@ -310,7 +310,7 @@ let judge_of_cast env cj k tj = | NATIVEcast -> let sigma = Nativelambda.empty_evars in mkCast (cj.uj_val, k, expected_type), - native_conv CUMUL sigma env cj.uj_type expected_type + Nativeconv.native_conv CUMUL sigma env cj.uj_type expected_type in { uj_val = c; uj_type = expected_type } diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 27e184ea3..2f6be0601 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -46,7 +46,7 @@ let rec conv_val env pb k v1 v2 cu = and conv_whd env pb k whd1 whd2 cu = match whd1, whd2 with - | Vsort s1, Vsort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu + | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu | Vprod p1, Vprod p2 -> let cu = conv_val env CONV k (dom p1) (dom p2) cu in conv_fun env pb k (codom p1) (codom p2) cu @@ -163,67 +163,25 @@ let rec eq_puniverses f (x,l1) (y,l2) cu = and conv_universes l1 l2 cu = if Univ.Instance.equal l1 l2 then cu else raise NotConvertible -let rec conv_eq env pb t1 t2 cu = - if t1 == t2 then cu - else - match kind_of_term t1, kind_of_term t2 with - | Rel n1, Rel n2 -> - if Int.equal n1 n2 then cu else raise NotConvertible - | Meta m1, Meta m2 -> - if Int.equal m1 m2 then cu else raise NotConvertible - | Var id1, Var id2 -> - if Id.equal id1 id2 then cu else raise NotConvertible - | Sort s1, Sort s2 -> check_sort_cmp_universes env pb s1 s2 cu; cu - | Cast (c1,_,_), _ -> conv_eq env pb c1 t2 cu - | _, Cast (c2,_,_) -> conv_eq env pb t1 c2 cu - | Prod (_,t1,c1), Prod (_,t2,c2) -> - conv_eq env pb c1 c2 (conv_eq env CONV t1 t2 cu) - | Lambda (_,t1,c1), Lambda (_,t2,c2) -> conv_eq env CONV c1 c2 cu - | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> - conv_eq env pb c1 c2 (conv_eq env CONV b1 b2 cu) - | App (c1,l1), App (c2,l2) -> - conv_eq_vect env l1 l2 (conv_eq env CONV c1 c2 cu) - | Evar (e1,l1), Evar (e2,l2) -> - if Evar.equal e1 e2 then conv_eq_vect env l1 l2 cu - else raise NotConvertible - | Const c1, Const c2 -> eq_puniverses eq_constant c1 c2 cu - | Proj (p1,c1), Proj (p2,c2) -> - if eq_constant (Projection.constant p1) (Projection.constant p2) then - conv_eq env pb c1 c2 cu - else raise NotConvertible - | Ind c1, Ind c2 -> - eq_puniverses eq_ind c1 c2 cu - | Construct c1, Construct c2 -> - eq_puniverses eq_constructor c1 c2 cu - | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> - let pcu = conv_eq env CONV p1 p2 cu in - let ccu = conv_eq env CONV c1 c2 pcu in - conv_eq_vect env bl1 bl2 ccu - | Fix ((ln1, i1),(_,tl1,bl1)), Fix ((ln2, i2),(_,tl2,bl2)) -> - if Int.equal i1 i2 && Array.equal Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu) - else raise NotConvertible - | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) -> - if Int.equal ln1 ln2 then conv_eq_vect env tl1 tl2 (conv_eq_vect env bl1 bl2 cu) - else raise NotConvertible - | _ -> raise NotConvertible - -and conv_eq_vect env vt1 vt2 cu = - let len = Array.length vt1 in - if Int.equal len (Array.length vt2) then - let rcu = ref cu in - for i = 0 to len-1 do - rcu := conv_eq env CONV vt1.(i) vt2.(i) !rcu - done; !rcu - else raise NotConvertible - -let vconv pb env t1 t2 = - let _cu = - try conv_eq env pb t1 t2 (universes env) - with NotConvertible -> - let v1 = val_of_constr env t1 in - let v2 = val_of_constr env t2 in - let cu = conv_val env pb (nb_rel env) v1 v2 (universes env) in - cu - in () - -let _ = Reduction.set_vm_conv vconv +let vm_conv_gen cv_pb env univs t1 t2 = + try + let v1 = val_of_constr env t1 in + let v2 = val_of_constr env t2 in + fst (conv_val env cv_pb (nb_rel env) v1 v2 univs) + with Not_found | Invalid_argument _ -> + (Pp.msg_warning + (Pp.str "Bytecode compilation failed, falling back to default conversion"); + Reduction.generic_conv cv_pb ~l2r:false (fun _ -> None) + full_transparent_state env univs t1 t2) + +let vm_conv cv_pb env t1 t2 = + let univs = Environ.universes env in + let b = + if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 + else Constr.eq_constr_univs univs t1 t2 + in + if not b then + let univs = (univs, checked_universes) in + let _ = vm_conv_gen cv_pb env univs t1 t2 in () + +let _ = Reduction.set_vm_conv vm_conv diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 1a29a4d51..49e5d23e6 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -12,7 +12,11 @@ open Reduction (********************************************************************** s conversion functions *) -val vconv : conv_pb -> types conversion_function +val vm_conv : conv_pb -> types conversion_function -val val_of_constr : env -> constr -> values +(** A conversion function parametrized by a universe comparator. Used outside of + the kernel. *) +val vm_conv_gen : conv_pb -> (types, 'a) generic_conversion_function +(** Precompute a VM value from a constr *) +val val_of_constr : env -> constr -> values |