From 15948adcbf406b7d4be156d2024d4717161f0b95 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Thu, 8 Nov 2018 19:05:36 -0500 Subject: Add a variant of cps_id that pulls the continuation from the lhs --- src/Util/Tactics/CPSId.v | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'src/Util') 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. -- cgit v1.2.3