diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/cClosure.ml | 7 | ||||
| -rw-r--r-- | kernel/nativelib.ml | 21 | ||||
| -rw-r--r-- | kernel/reduction.ml | 39 |
3 files changed, 43 insertions, 24 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 952237ab99..174125fc57 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1535,7 +1535,12 @@ let whd_stack infos tab m stk = match Mark.red_state m.mark with knh infos m stk | Red | Cstr -> let k = kni infos tab m stk in - let () = if infos.i_cache.i_share then ignore (fapp_stack k) in (* to unlock Zupdates! *) + let () = + if infos.i_cache.i_share then + (* to unlock Zupdates! *) + let (m', stk') = k in + if not (m == m' && stk == stk') then ignore (zip m' stk') + in k let create_clos_infos ?univs ?(evars=fun _ -> None) flgs env = diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 494282d4e1..c1f14923fa 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -25,7 +25,8 @@ let open_header = ["Nativevalues"; let open_header = List.map mk_open open_header (* Directory where compiled files are stored *) -let output_dir = ref ".coq-native" +let dft_output_dir = ".coq-native" +let output_dir = ref dft_output_dir (* Extension of generated ml files, stored for debugging purposes *) let source_ext = ".native" @@ -92,9 +93,14 @@ let error_native_compiler_failed e = CErrors.user_err msg let call_compiler ?profile:(profile=false) ml_filename = - let load_path = !get_load_paths () in - let load_path = List.map (fun dn -> dn / !output_dir) load_path in - let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ load_path)) in + (* The below path is computed from Require statements, by uniquizing + the paths, see [Library.get_used_load_paths] This is in general + hacky and we should do a bit better once we move loadpath to its + own library *) + let require_load_path = !get_load_paths () in + (* We assume that installed files always go in .coq-native for now *) + let install_load_path = List.map (fun dn -> dn / dft_output_dir) require_load_path in + let include_dirs = List.flatten (List.map (fun x -> ["-I"; x]) (get_include_dirs () @ install_load_path)) in let f = Filename.chop_extension ml_filename in let link_filename = f ^ ".cmo" in let link_filename = Dynlink.adapt_filename link_filename in @@ -186,5 +192,10 @@ let call_linker ?(fatal=true) env ~prefix f upds = match upds with Some upds -> update_locations upds | _ -> () let link_library env ~prefix ~dirname ~basename = - let f = dirname / !output_dir / basename in + (* We try both [output_dir] and [.coq-native], unfortunately from + [Require] we don't know if we are loading a library in the build + dir or in the installed layout *) + let install_location = dirname / dft_output_dir / basename in + let build_location = dirname / !output_dir / basename in + let f = if Sys.file_exists build_location then build_location else install_location in call_linker env ~fatal:false ~prefix f None diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 5589ae3483..c891b885c4 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -301,7 +301,7 @@ let unfold_ref_with_args infos tab fl v = | Primitive op when check_native_args op v -> let c = match fl with ConstKey c -> c | _ -> assert false in let rargs, a, nargs, v = get_native_args1 op c v in - Some (whd_stack infos tab a (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) + Some (a, (Zupdate a::(Zprimitive(op,c,rargs,nargs)::v))) | Undef _ | OpaqueDef _ | Primitive _ -> None type conv_tab = { @@ -411,23 +411,26 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = let cuniv = conv_table_key infos.cnv_inf fl1 fl2 cuniv in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with NotConvertible | Univ.UniverseInconsistency _ -> - (* else the oracle tells which constant is to be expanded *) - let oracle = CClosure.oracle_of_infos infos.cnv_inf in - let (app1,app2) = - let aux appr1 lft1 fl1 tab1 v1 appr2 lft2 fl2 tab2 v2 = - match unfold_ref_with_args infos.cnv_inf tab1 fl1 v1 with - | Some t1 -> ((lft1, t1), appr2) - | None -> match unfold_ref_with_args infos.cnv_inf tab2 fl2 v2 with - | Some t2 -> (appr1, (lft2, t2)) - | None -> raise NotConvertible - in - if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then - aux appr1 lft1 fl1 infos.lft_tab v1 appr2 lft2 fl2 infos.rgt_tab v2 - else - let (app2,app1) = aux appr2 lft2 fl2 infos.rgt_tab v2 appr1 lft1 fl1 infos.lft_tab v1 in - (app1,app2) - in - eqappr cv_pb l2r infos app1 app2 cuniv) + let r1 = unfold_ref_with_args infos.cnv_inf infos.lft_tab fl1 v1 in + let r2 = unfold_ref_with_args infos.cnv_inf infos.rgt_tab fl2 v2 in + match r1, r2 with + | None, None -> raise NotConvertible + | Some t1, Some t2 -> + (* else the oracle tells which constant is to be expanded *) + let oracle = CClosure.oracle_of_infos infos.cnv_inf in + if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + else + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + | Some (t1, v1), None -> + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let t1 = whd_stack (infos_with_reds infos.cnv_inf all) infos.lft_tab t1 v1 in + eqappr cv_pb l2r infos (lft1, t1) appr2 cuniv + | None, Some (t2, v2) -> + let all = RedFlags.red_add_transparent all (RedFlags.red_transparent (info_flags infos.cnv_inf)) in + let t2 = whd_stack (infos_with_reds infos.cnv_inf all) infos.rgt_tab t2 v2 in + eqappr cv_pb l2r infos appr1 (lft2, t2) cuniv + ) | (FProj (p1,c1), FProj (p2, c2)) -> (* Projections: prefer unfolding to first-order unification, |