diff options
author | Jason Gross <jgross@mit.edu> | 2018-11-08 19:05:36 -0500 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-11-08 19:05:36 -0500 |
commit | 15948adcbf406b7d4be156d2024d4717161f0b95 (patch) | |
tree | e4a585ca9cccb01c4b0767c6e757fd0435609762 /src/Util/Tactics/CPSId.v | |
parent | 10a53166839f97f92b64b353fac01c627e6d8e7c (diff) |
Add a variant of cps_id that pulls the continuation from the lhs
Diffstat (limited to 'src/Util/Tactics/CPSId.v')
-rw-r--r-- | src/Util/Tactics/CPSId.v | 24 |
1 files changed, 19 insertions, 5 deletions
diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v index 92b694396..6bedeb94f 100644 --- a/src/Util/Tactics/CPSId.v +++ b/src/Util/Tactics/CPSId.v @@ -16,12 +16,23 @@ Ltac ensure_complex_continuation allow_option k := end end. -Ltac cps_id_step allow_option lem := +Ltac continuation_of_rhs eqn := + match eqn with + | ?lhs = ?k ?rhs => k + end. + +Ltac continuation_of_lhs eqn := + match eqn with + | ?lhs ?k = ?rhs => k + end. + +Ltac cps_id_step continuation_of_eqn 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 + | ?T -> _ => cps_id_step continuation_of_eqn allow_option open_constr:(lem _) + | ?lhs = ?rhs :> ?T + => let k := continuation_of_eqn (@eq T lhs rhs) in + match goal with | [ |- context[?e] ] => (* take advantage of lazymatch treating evars as holes/wildcards *) lazymatch e with @@ -41,6 +52,9 @@ Ltac cps_id_step allow_option lem := end end. -Ltac cps_id allow_option lem := repeat cps_id_step allow_option lem. +Ltac cps_id allow_option lem := repeat cps_id_step continuation_of_rhs allow_option lem. +Ltac cps_id' allow_option lem := repeat cps_id_step continuation_of_lhs 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. +Tactic Notation "cps_id'_with_option" uconstr(lem) := cps_id' true lem. +Tactic Notation "cps_id'_no_option" uconstr(lem) := cps_id' false lem. |