diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/Tactics.v | 1 | ||||
| -rw-r--r-- | src/Util/Tactics/CPSId.v | 41 |
3 files changed, 43 insertions, 0 deletions
diff --git a/_CoqProject b/_CoqProject index eab813601..54f1cd4f7 100644 --- a/_CoqProject +++ b/_CoqProject @@ -6568,6 +6568,7 @@ src/Util/Strings/OctalString.v src/Util/Strings/Show.v src/Util/Strings/String.v src/Util/Tactics/BreakMatch.v +src/Util/Tactics/CPSId.v src/Util/Tactics/CacheTerm.v src/Util/Tactics/ChangeInAll.v src/Util/Tactics/ClearAll.v diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v index cd045fdbb..ee27e598f 100644 --- a/src/Util/Tactics.v +++ b/src/Util/Tactics.v @@ -8,6 +8,7 @@ Require Export Crypto.Util.Tactics.ClearDuplicates. Require Export Crypto.Util.Tactics.ClearbodyAll. Require Export Crypto.Util.Tactics.Contains. Require Export Crypto.Util.Tactics.ConvoyDestruct. +Require Export Crypto.Util.Tactics.CPSId. Require Export Crypto.Util.Tactics.DebugPrint. Require Export Crypto.Util.Tactics.DestructHead. Require Export Crypto.Util.Tactics.DestructHyps. diff --git a/src/Util/Tactics/CPSId.v b/src/Util/Tactics/CPSId.v new file mode 100644 index 000000000..a7672ca51 --- /dev/null +++ b/src/Util/Tactics/CPSId.v @@ -0,0 +1,41 @@ +(** * [cps_id] is a scaffold for writing tactics that convert to cps normal form (where the continuation is the identity *) + +Ltac ensure_complex_continuation allow_option k := + lazymatch k with + | id => fail + | (fun x => x) => fail + | _ + => lazymatch allow_option with + | true => lazymatch k with + | @Some _ => fail + | (fun x => Some x) => fail + | _ => idtac + end + | false => idtac + | ?ao => fail 100 "Argument allow_option to ensure_complex_continuation must be true or false, not" ao + 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) + 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. |