diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-10 19:28:41 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-10 19:28:41 +0000 |
commit | 9221176c38519e17522104f5adbbec3fcf755dd4 (patch) | |
tree | 9078dc616231819adcd923e205c6d6d0d2043fb3 /kernel/reduction.mli | |
parent | 71b3fd6a61aa58e88c4248dea242420ac7f8f437 (diff) |
Propagated information from the reduction tactics to the kernel so
that the kernel conversion solves the delta/delta critical pair the
same way the tactics did. This allows to improve Qed time when slow
down is due to conversion having (arbitrarily) made the wrong choice.
Propagation is done thanks to a new kind of cast called REVERTcast.
Notes:
- Vm conversion not modified
- size of vo generally grows because of additional casts
- this remains a heuristic... for the record, when a reduction tactic
is applied on the goal t leading to new goal t', this is translated
in the kernel in a conversion t' <= t where, hence, reducing in t'
must be preferred; what the propagation of reduction cast to the
kernel does not do is whether it is preferable to first unfold c or
to first compare u' and u in "c u' = c u"; in particular,
intermediate casts are sometimes useful to solve this kind of issues
(this is the case e.g. in Nijmegen/LinAlg/subspace_dim.v where the
combination "simpl;red" needs the intermediate cast to ensure Qed
answers quickly); henceforth the merge of nested casts in mkCast is
deactivated
- for tactic "change", REVERTcast should be used when conversion is in
the hypotheses, but convert_hyp does not (yet) support this (would
require e.g. that convert_hyp overwrite some given hyp id with a
body-cleared let-binding new_id := Cast(old_id,REVERTCast,t))
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14407 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.mli')
-rw-r--r-- | kernel/reduction.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index bee8815a2..aa78fbdad 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,27 +36,27 @@ val sort_cmp : val conv_sort : sorts conversion_function val conv_sort_leq : sorts conversion_function -val trans_conv_cmp : conv_pb -> constr trans_conversion_function +val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function val trans_conv : - ?evars:(existential->constr option) -> constr trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function val trans_conv_leq : - ?evars:(existential->constr option) -> types trans_conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function -val conv_cmp : conv_pb -> constr conversion_function +val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function val conv : - ?evars:(existential->constr option) -> constr conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function val conv_leq : - ?evars:(existential->constr option) -> types conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function val conv_leq_vecti : - ?evars:(existential->constr option) -> types array conversion_function + ?l2r:bool -> ?evars:(existential->constr option) -> types array conversion_function (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -val set_default_conv : (conv_pb -> types conversion_function) -> unit -val default_conv : conv_pb -> types conversion_function -val default_conv_leq : types conversion_function +val set_default_conv : (conv_pb -> ?l2r:bool -> types conversion_function) -> unit +val default_conv : conv_pb -> ?l2r:bool -> types conversion_function +val default_conv_leq : ?l2r:bool -> types conversion_function (************************************************************************) |