From 2280477a96e19ba5060de2d48dcc8fd7c8079d22 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 13 Nov 2015 11:31:34 +0100 Subject: Imported Upstream version 8.5~beta3+dfsg --- kernel/nativeconv.ml | 136 +++++++++++++++++++++++++++++---------------------- 1 file changed, 77 insertions(+), 59 deletions(-) (limited to 'kernel/nativeconv.ml') diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index 75a3fc45..0242fd46 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -16,17 +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 - | Vaccu k1, Vaccu k2 -> - conv_accu env pb lvl cu k1 k2 | 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 v1 (fun x -> v2 x) cu + | _, Vfun f2 -> + conv_val env CONV lvl (fun x -> v1 x) v2 cu + | Vaccu k1, Vaccu 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 @@ -34,77 +38,81 @@ 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 - | Vfun f1, _ -> - conv_val env CONV lvl cu v1 (fun x -> v2 x) - | _, Vfun f2 -> - conv_val env CONV lvl cu (fun x -> v1 x) v2 - | _, _ -> raise NotConvertible + | 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 - | Aind ind1, Aind ind2 -> - if not (eq_puniverses eq_ind ind1 ind2) then raise NotConvertible - | Aconstant c1, Aconstant c2 -> - if not (eq_puniverses eq_constant c1 c2) then raise NotConvertible + if Int.equal i1 i2 then cu else raise NotConvertible + | Aind (ind1,u1), Aind (ind2,u2) -> + if eq_ind ind1 ind2 then convert_instances ~flex:false u1 u2 cu + else raise NotConvertible + | Aconstant (c1,u1), Aconstant (c2,u2) -> + if Constant.equal c1 c2 then convert_instances ~flex:true u1 u2 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) - | _, _ -> raise NotConvertible + 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 ac1 ac2 cu + | Arel _, _ | Aind _, _ | Aconstant _, _ | Asort _, _ | Avar _, _ + | Acase _, _ | Afix _, _ | Acofix _, _ | Acofixe _, _ | Aprod _, _ + | Aproj _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) and conv_fix env lvl t1 f1 t2 f2 cu = @@ -112,22 +120,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 !Flags.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 @@ -141,8 +142,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 () -- cgit v1.2.3