diff options
author | Jason Gross <jgross@mit.edu> | 2018-10-28 14:22:35 -0400 |
---|---|---|
committer | Jason Gross <jgross@mit.edu> | 2018-10-28 14:22:35 -0400 |
commit | e844ba2919fd2795d1e0082f69e018dc5ddb093d (patch) | |
tree | b45fd413b4096f069dcbe7ea687ca74b17fce36f /src/Util/Tactics | |
parent | e0f3e8819de459fbe120ad0f717f987eb8d41da3 (diff) |
Add CPSId tactics
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. |