blob: a7672ca517eab74dc0e21c3b7edc51c7511a2919 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
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.
|
