diff options
-rw-r--r-- | kernel/nativeconv.ml | 5 | ||||
-rw-r--r-- | kernel/nativeconv.mli | 2 | ||||
-rw-r--r-- | kernel/reduction.ml | 2 | ||||
-rw-r--r-- | kernel/typeops.ml | 2 | ||||
-rw-r--r-- | kernel/vconv.ml | 88 | ||||
-rw-r--r-- | kernel/vconv.mli | 8 | ||||
-rw-r--r-- | pretyping/nativenorm.ml | 4 | ||||
-rw-r--r-- | pretyping/pretyping.ml | 11 | ||||
-rw-r--r-- | pretyping/reductionops.ml | 3 | ||||
-rw-r--r-- | pretyping/reductionops.mli | 2 | ||||
-rw-r--r-- | pretyping/vnorm.ml | 4 | ||||
-rw-r--r-- | pretyping/vnorm.mli | 4 |
12 files changed, 48 insertions, 87 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index fc68575cd..7ae66c485 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -157,9 +157,8 @@ let native_conv cv_pb sigma env t1 t2 = if cv_pb = CUMUL then Constr.leq_constr_univs univs t1 t2 else Constr.eq_constr_univs univs t1 t2 in - let univs = (univs, checked_universes) in - if not b then begin + 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 () - end diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 21f0b2e9e..4dddb9fd3 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -15,4 +15,4 @@ 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 -> (constr, 'a) generic_conversion_function +val native_conv_gen : conv_pb -> evars -> (types, 'a) generic_conversion_function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b6c97b11d..c2ab22e99 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -670,7 +670,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 diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 70f6fd803..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 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 diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 949a28a1f..dafe88d8d 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -405,6 +405,6 @@ let native_norm env sigma c ty = let native_conv_generic pb sigma t = Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t -let native_infer_conv ?(pb=Reduction.CUMUL) env sigma x y = +let native_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> native_conv_generic pb sigma) - ~catch_incon:true ~pb env sigma x y + ~catch_incon:true ~pb env sigma t1 t2 diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index e1e8982e1..f6c186728 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -929,14 +929,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let cj = pretype empty_tycon env evdref lvar c in let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in if not (occur_existential cty || occur_existential tval) then - begin - try - let env = Environ.push_context_set (Evd.universe_context_set !evdref) env in - ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj - with Reduction.NotConvertible -> - error_actual_type_loc loc env !evdref cj tval + let (evd,b) = Vnorm.vm_infer_conv env !evdref cty tval in + if b then (evdref := evd; cj) + else + error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) - end else user_err_loc (loc,"",str "Cannot check cast with vm: " ++ str "unresolved arguments remain.") | NATIVEcast -> diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a24773b6e..d25e273a3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1251,9 +1251,6 @@ let pb_equal = function | Reduction.CUMUL -> Reduction.CONV | Reduction.CONV -> Reduction.CONV -let sort_cmp cv_pb s1 s2 u = - Reduction.check_sort_cmp_universes cv_pb s1 s2 u - let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y = try let evars ev = safe_evar_value sigma ev in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index b179dbc95..42c2c9c6e 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -251,8 +251,6 @@ type conversion_test = constraints -> constraints val pb_is_equal : conv_pb -> bool val pb_equal : conv_pb -> conv_pb -val sort_cmp : env -> conv_pb -> sorts -> sorts -> universes -> unit - val is_conv : env -> evar_map -> constr -> constr -> bool val is_conv_leq : env -> evar_map -> constr -> constr -> bool val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index f768e4fee..2c6ac7a29 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -312,3 +312,7 @@ and nf_cofix env cf = let cbv_vm env c t = let v = Vconv.val_of_constr env c in nf_val env v t + +let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 = + Reductionops.infer_conv_gen (fun pb ~l2r sigma ts -> Vconv.vm_conv_gen pb) + ~catch_incon:true ~pb env sigma t1 t2 diff --git a/pretyping/vnorm.mli b/pretyping/vnorm.mli index 7dabbc6cb..99856a8d9 100644 --- a/pretyping/vnorm.mli +++ b/pretyping/vnorm.mli @@ -8,7 +8,11 @@ open Term open Environ +open Evd (** {6 Reduction functions } *) val cbv_vm : env -> constr -> types -> constr +(** Conversion with inference of universe constraints *) +val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr -> + evar_map * bool |