aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-20 10:55:17 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-01-20 13:51:50 +0100
commita9b76df171ceea443885bb4be919ea586a82beee (patch)
tree59ed773cbc4846fddf1156a7f9f6fb53a2ef6ae7 /kernel
parent8d783c10d9505cbc1beb1c8e3451ea5dd567f260 (diff)
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.
Diffstat (limited to 'kernel')
-rw-r--r--kernel/safe_typing.ml4
-rw-r--r--kernel/term_typing.mli1
2 files changed, 3 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09f7bd75c..95d9c75d3 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 fcd95576c..89b5fc40e 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 ->