From 3116aeff0cdc51e6801f3e8ae4a6c0533e1a75ac Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 8 Oct 2015 18:06:55 +0200 Subject: Fix #4346 1/2: native casts were not inferring universe constraints. --- kernel/fast_typeops.ml | 2 +- kernel/nativeconv.ml | 116 +++++++++++++++++++++++++++---------------------- kernel/nativeconv.mli | 4 ++ kernel/reduction.ml | 19 ++------ kernel/reduction.mli | 19 +++----- kernel/typeops.ml | 2 +- 6 files changed, 80 insertions(+), 82 deletions(-) (limited to 'kernel') 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..fc68575cd 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,26 @@ 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 + let univs = (univs, checked_universes) in + if not b then begin + 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 318a7d830..21f0b2e9e 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 -> (constr, 'a) generic_conversion_function diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 0f105b048..b6c97b11d 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -637,7 +637,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 : (Univ.universes * Univ.Constraint.t) universe_compare = +let inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare = { compare = infer_cmp_universes; compare_instances = infer_convert_instances } @@ -685,7 +685,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 @@ -697,7 +697,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 @@ -716,19 +716,6 @@ 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 - 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 = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 90c008b19..b71356d03 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -49,14 +49,11 @@ type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints -val check_sort_cmp_universes : - env -> conv_pb -> sorts -> sorts -> Univ.universes -> unit +val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> + 'a * 'a universe_compare -> 'a * 'a universe_compare -(* val sort_cmp : *) -(* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) - -(* val conv_sort : sorts conversion_function *) -(* val conv_sort_leq : sorts conversion_function *) +val checked_universes : Univ.universes universe_compare +val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : @@ -77,22 +74,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..70f6fd803 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -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 } -- cgit v1.2.3