diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-23 23:35:02 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-25 18:36:19 +0200 |
commit | bf018569405c0ae1c5d08dfa27600102b9d77977 (patch) | |
tree | d8b4435ee65ceb8cd03977748711c13e028c131c /pretyping/find_subterm.mli | |
parent | b39465da31bfd488dfad4ea4627186f9a1843e56 (diff) |
This commit introduces changes in induction and destruct.
The main change is that selection of subterm is made similar whether
the given term is fully applied or not.
- The selection of subterm now works as follows depending on whether
the "at" is given, of whether the subterm is fully applied or not,
and whether there are incompatible subterms matching the pattern. In
particular, we have:
"at" given
| subterm fully applied
| | incompatible subterms
| | |
Y Y - it works like in 8.4
Y N - this was broken in 8.4 ("at" was ineffective and it was finding
all subterms syntactically equal to the first one which matches)
N Y Y it now finds all subterms like the first one which matches
while in 8.4 it used to fail (I hope it is not a too risky in-draft
for a semantics we would regret...) (e.g. "destruct (S _)" on
goal "S x = S y + S x" now selects the two occurrences of "S x"
while it was failing before)
N Y N it works like in 8.4
N N - it works like in 8.4, selecting all subterms like the
first one which matches
- Note that the "historical" semantics, when looking for a subterm, to
select all subterms that syntactically match the first subterm to
match the pattern (looking from left to right) is now internally called
"like first".
- Selection of subterms can now find the type by pattern-matching (useful e.g.
for "induction (nat_rect _ _ _ _)")
- A version of Unification.w_unify w/o any conversion is used for
finding the subterm: it could be easily replaced by an other
matching algorithm.
In particular, "destruct H" now works on a goal such as "H:True -> x<=y |- P y".
Secondary change is in the interpretation of terms with existential
variables:
- When several arguments are given, interpretation is delayed at the
time of execution
- Because we aim at eventually accepting "edestruct c" with unresolved
holes in c, we need the sigma obtained from c to be an extension of
the sigma of the tactics, while before, we just type-checked c
independently of the sigma of the tactic
- Finishing the resolution of evars (using type classes, candidates,
pending conversion problems) is made slightly cleaner: it now takes
three states: a term is evaluated in state sigma, leading to state
sigma' >= sigma, with evars finally solved in state sigma'' >=
sigma'; we solve evars in the diff of sigma' and sigma and report
the solution in sigma''
- We however renounce to give now a success semantics to "edestruct c"
when "c" has unresolved holes, waiting instead for a decision on
what to do in the case of a similar eapply (see mail to coqdev).
An auxiliary change is that an "in" clause can be attached to each component
of a "destruct t, u, v", etc.
Incidentally, make_abstraction does not do evar resolution itself any longer.
Diffstat (limited to 'pretyping/find_subterm.mli')
-rw-r--r-- | pretyping/find_subterm.mli | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index b24c95807..ea1ce6228 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -26,11 +26,12 @@ exception SubtermUnificationError of subterm_unification_error function to merge substitutions and an initial substitution; last_found is used for error messages and it has to be initialized with None. *) + type 'a testing_function = { match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option + mutable last_found : position_reporting option } (** This is the basic testing function, looking for exact matches of a @@ -42,25 +43,26 @@ val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function matching subterms at the indicated occurrences [occl] with [mk ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) -val replace_term_occ_modulo : - occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr +val replace_term_occ_modulo : occurrences or_like_first -> + 'a testing_function -> (unit -> constr) -> constr -> constr (** [replace_term_occ_decl_modulo] is similar to [replace_term_occ_modulo] but for a named_declaration. *) val replace_term_occ_decl_modulo : - occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) -> + (occurrences * hyp_location_flag) or_like_first -> + 'a testing_function -> (unit -> constr) -> named_declaration -> named_declaration (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), unifying universes which results in a set of constraints. *) -val subst_closed_term_occ : env -> evar_map -> occurrences -> constr -> - constr -> constr * evar_map +val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> + constr -> constr -> constr * evar_map (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> - occurrences * hyp_location_flag -> + (occurrences * hyp_location_flag) or_like_first -> constr -> named_declaration -> named_declaration * evar_map (** Miscellaneous *) |