From e844ba2919fd2795d1e0082f69e018dc5ddb093d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 28 Oct 2018 14:22:35 -0400 Subject: Add CPSId tactics --- src/Util/Tactics/CPSId.v | 41 +++++++++++++++++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 src/Util/Tactics/CPSId.v (limited to 'src/Util/Tactics') 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. -- cgit v1.2.3