diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-28 14:43:11 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-28 14:43:11 -0400 |
commit | d5298f223b503d8ca02c6869ba269bf8f4b84b96 (patch) | |
tree | 33c4a08ea1989007d1b22d9953c4722f661855b0 /src/Util/Tactics | |
parent | 083124d659fa6ca2d88c9bd9a8c64ad7b7de9224 (diff) |
Improve cps_id tactics, add add_var_types_cps_id, unify_extracted_cps_id tactics
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r-- | src/Util/Tactics/CPSId.v | 45 |
1 files changed, 25 insertions, 20 deletions
diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v index 076eed95a..92b694396 100644 --- a/src/Util/Tactics/CPSId.v +++ b/src/Util/Tactics/CPSId.v @@ -16,26 +16,31 @@ Ltac ensure_complex_continuation allow_option k := end end. -Ltac cps_id_step allow_option match_to_cont_lem := - match goal with - | [ |- context[?e] ] - => let res := match_to_cont_lem e in - lazymatch res with - | (?k, ?lem) - => ensure_complex_continuation allow_option k; - (* sometimes reduction mismatches happen, so we cast [lem] to fix them *) - (rewrite lem || rewrite (lem : e = _)) - end - | [ H : context[?e] |- _ ] - => let res := match_to_cont_lem e in - lazymatch res with - | (?k, ?lem) - => ensure_complex_continuation allow_option k; - (* sometimes reduction mismatches happen, so we cast [lem] to fix them *) - (rewrite lem in H || rewrite (lem : e = _) in H) +Ltac cps_id_step allow_option lem := + let lem := open_constr:(lem) in + lazymatch type of lem with + | ?T -> _ => cps_id_step allow_option open_constr:(lem _) + | ?lhs = ?k ?rhs + => match goal with + | [ |- context[?e] ] + => (* take advantage of lazymatch treating evars as holes/wildcards *) + lazymatch e with + | lhs + => let lem := constr:(lem : e = _) in + ensure_complex_continuation allow_option k; + rewrite lem + end + | [ H : context[?e] |- _ ] + => (* take advantage of lazymatch treating evars as holes/wildcards *) + lazymatch e with + | lhs + => let lem := constr:(lem : e = _) in + ensure_complex_continuation allow_option k; + rewrite lem in H + end end end. -Ltac cps_id allow_option match_to_cont_lem := repeat cps_id_step allow_option match_to_cont_lem. -Ltac cps_id_with_option match_to_cont_lem := cps_id true match_to_cont_lem. -Ltac cps_id_no_option match_to_cont_lem := cps_id false match_to_cont_lem. +Ltac cps_id allow_option lem := repeat cps_id_step allow_option lem. +Tactic Notation "cps_id_with_option" uconstr(lem) := cps_id true lem. +Tactic Notation "cps_id_no_option" uconstr(lem) := cps_id false lem. |