From 63ca4aac83ced14b9b8065ef43e29f7c2dfd331c Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Fri, 23 Dec 2016 09:28:47 +0100 Subject: Handle application of a primitive projection to a not yet evaluated cofixpoint (bug #5286). --- kernel/byterun/coq_interp.c | 63 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 48 insertions(+), 15 deletions(-) (limited to 'kernel') diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 35abd011bb..a67c27e87f 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -898,25 +898,58 @@ value coq_interprete Instruct(PROJ){ + do_proj: print_instr("PROJ"); if (Is_accu (accu)) { - value block; - /* Skip over the index of projected field */ - pc++; - /* Create atom */ - Alloc_small(block, 2, ATOM_PROJ_TAG); - Field(block, 0) = Field(coq_global_data, *pc); - Field(block, 1) = accu; - accu = block; - /* Create accumulator */ - Alloc_small(block, 2, Accu_tag); - Code_val(block) = accumulate; - Field(block, 1) = accu; - accu = block; + *--sp = accu; // Save matched block on stack + accu = Field(accu, 1); // Save atom to accu register + switch (Tag_val(accu)) { + case ATOM_COFIX_TAG: // We are forcing a cofix + { + mlsize_t i, nargs; + sp -= 2; + // Push the current instruction as the return address + sp[0] = (value)(pc - 1); + sp[1] = coq_env; + coq_env = Field(accu, 0); // Pointer to suspension + accu = sp[2]; // Save accumulator to accu register + sp[2] = Val_long(coq_extra_args); // Push number of args for return + nargs = Wosize_val(accu) - 2; // Number of args = size of accumulator - 1 (accumulator code) - 1 (atom) + // Push arguments to stack + CHECK_STACK(nargs + 1); + sp -= nargs; + for (i = 0; i < nargs; ++i) sp[i] = Field(accu, i + 2); + *--sp = accu; // Last argument is the pointer to the suspension + coq_extra_args = nargs; + pc = Code_val(coq_env); // Trigger evaluation + goto check_stack; + } + case ATOM_COFIXEVALUATED_TAG: + { + accu = Field(accu, 1); + ++sp; + goto do_proj; + } + default: + { + value block; + /* Skip over the index of projected field */ + ++pc; + /* Create atom */ + Alloc_small(accu, 2, ATOM_PROJ_TAG); + Field(accu, 0) = Field(coq_global_data, *pc++); + Field(accu, 1) = *sp++; + /* Create accumulator */ + Alloc_small(block, 2, Accu_tag); + Code_val(block) = accumulate; + Field(block, 1) = accu; + accu = block; + } + } } else { - accu = Field(accu, *pc++); + accu = Field(accu, *pc); + pc += 2; } - pc++; Next; } -- cgit v1.2.3 From a9b76df171ceea443885bb4be919ea586a82beee Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 20 Jan 2017 10:55:17 +0100 Subject: Do not add redundant side effects in tactic code. This was observable in long proofs, because side effects kept being duplicated, leading to an additional cost linear in the size of the proof. This commit touches kernel files, but the corresponding API is only used in tactic-facing code so that the side_effects type remains opaque. Thus it does not affect the kernel safety. --- kernel/safe_typing.ml | 4 ++-- kernel/term_typing.mli | 1 + 2 files changed, 3 insertions(+), 2 deletions(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 09f7bd75cd..95d9c75d30 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -213,8 +213,8 @@ type private_constant_role = Term_typing.side_effect_role = | Schema of inductive * string let empty_private_constants = [] -let add_private x xs = x :: xs -let concat_private xs ys = xs @ ys +let add_private x xs = if List.mem_f Term_typing.equal_eff x xs then xs else x :: xs +let concat_private xs ys = List.fold_right add_private xs ys let mk_pure_proof = Term_typing.mk_pure_proof let inline_private_constants_in_constr = Term_typing.inline_side_effects let inline_private_constants_in_definition_entry = Term_typing.inline_entry_side_effects diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fcd95576c0..89b5fc40e3 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -30,6 +30,7 @@ val inline_entry_side_effects : yet type checked proof. *) val uniq_seff : side_effects -> side_effects +val equal_eff : side_effect -> side_effect -> bool val translate_constant : structure_body -> env -> constant -> side_effects constant_entry -> -- cgit v1.2.3 From 86116b181bb866c7f63a37796e1388f731ce7204 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 26 Jan 2017 11:38:19 +0100 Subject: [native comp] Improve error message on linking error. The native compiler doesn't support `Require` inside `Module` sections in some cases, we improve the error message. See: https://coq.inria.fr/bugs/show_bug.cgi?id=4335 This patch improves the error message and gives the user some feedback. --- kernel/safe_typing.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 8b28cd87bd..7e28b1c567 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -795,7 +795,10 @@ type compiled_library = { type native_library = Nativecode.global list let get_library_native_symbols senv dir = - DPMap.find dir senv.native_symbols + try DPMap.find dir senv.native_symbols + with Not_found -> Errors.errorlabstrm "get_library_native_symbols" + Pp.((str "Linker error in the native compiler. Are you using Require inside a nested Module declaration?") ++ fnl () ++ + (str "This use case is not supported, but disabling the native compiler may help.")) (** FIXME: MS: remove?*) let current_modpath senv = senv.modpath -- cgit v1.2.3