diff options
Diffstat (limited to 'src/Util/Tactics')
-rw-r--r-- | src/Util/Tactics/CPSId.v | 41 |
1 files changed, 41 insertions, 0 deletions
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. |