diff options
Diffstat (limited to 'kernel/nativeconv.ml')
| -rw-r--r-- | kernel/nativeconv.ml | 52 |
1 files changed, 29 insertions, 23 deletions
diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index d2f050d3bc..931b8bbc86 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -54,13 +56,18 @@ and conv_accu env pb lvl k1 k2 cu = conv_atom env pb lvl (atom_of_accu k1) (atom_of_accu k2) cu else 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 + Array.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 cu else match a1, a2 with - | Ameta _, _ | _, Ameta _ | Aevar _, _ | _, Aevar _ -> assert false + | Ameta (m1,_), Ameta (m2,_) -> + if Int.equal m1 m2 then cu else raise NotConvertible + | Aevar (ev1,_,args1), Aevar (ev2,_,args2) -> + if Evar.equal ev1 ev2 then + Array.fold_right2 (conv_val env CONV lvl) args1 args2 cu + else raise NotConvertible | Arel i1, Arel i2 -> if Int.equal i1 i2 then cu else raise NotConvertible | Aind (ind1,u1), Aind (ind2,u2) -> @@ -107,12 +114,12 @@ and conv_atom env pb lvl a1 a2 cu = 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 + | Aproj((ind1, i1), ac1), Aproj((ind2, i2), ac2) -> + if not (eq_ind ind1 ind2 && Int.equal i1 i2) 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 + | Aproj _, _ | Ameta _, _ | Aevar _, _ -> raise NotConvertible (* Precondition length t1 = length f1 = length f2 = length t2 *) and conv_fix env lvl t1 f1 t2 f2 cu = @@ -128,11 +135,21 @@ and conv_fix env lvl t1 f1 t2 f2 cu = else aux (i+1) (conv_val env CONV flvl fi1 fi2 cu) in aux 0 cu +let warn_no_native_compiler = + let open Pp in + CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" + (fun () -> strbrk "Native compiler is disabled," ++ + strbrk " falling back to VM conversion test.") + let native_conv_gen pb sigma env univs t1 t2 = - let penv = Environ.pre_env env in + if not Coq_config.native_compiler then begin + warn_no_native_compiler (); + Vconv.vm_conv_gen pb env univs t1 t2 + end + else let ml_filename, prefix = get_ml_filename () in - let code, upds = mk_conv_code penv sigma prefix t1 t2 in - match compile ml_filename code with + let code, upds = mk_conv_code env sigma prefix t1 t2 in + match compile ml_filename code ~profile:false with | (true, fn) -> begin if !Flags.debug then Feedback.msg_debug (Pp.str "Running test..."); @@ -146,19 +163,8 @@ let native_conv_gen pb sigma env univs t1 t2 = end | _ -> anomaly (Pp.str "Compilation failure.") -let warn_no_native_compiler = - let open Pp in - CWarnings.create ~name:"native-compiler-disabled" ~category:"native-compiler" - (fun () -> strbrk "Native compiler is disabled," ++ - strbrk " falling back to VM conversion test.") - (* Wrapper for [native_conv] above *) let native_conv cv_pb sigma env t1 t2 = - if Coq_config.no_native_compiler then begin - warn_no_native_compiler (); - 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 |