blob: 3ced233319b481c8b9684a631d677969f5f84a10 (
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
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
|
Ltac debuglevel := constr:(0%nat).
Ltac solve_debugfail tac :=
solve [tac] ||
( let dbg := debuglevel in
match dbg with
| O => idtac
| _ => match goal with |- ?G => idtac "couldn't prove" G end
end;
fail).
(** constr-based [idtac] *)
Class cidtac {T} (msg : T) := Build_cidtac : True.
Hint Extern 0 (cidtac ?msg) => idtac msg; exact I : typeclass_instances.
(** constr-based [idtac] *)
Class cidtac2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cidtac2 : True.
Hint Extern 0 (cidtac2 ?msg1 ?msg2) => idtac msg1 msg2; exact I : typeclass_instances.
Class cidtac3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cidtac3 : True.
Hint Extern 0 (cidtac3 ?msg1 ?msg2 ?msg3) => idtac msg1 msg2 msg3; exact I : typeclass_instances.
Class cidtac4 {T1 T2 T3 T4} (msg1 : T1) (msg2 : T2) (msg3 : T3) (msg4 : T4) := Build_cidtac4 : True.
Hint Extern 0 (cidtac4 ?msg1 ?msg2 ?msg3 ?msg4) => idtac msg1 msg2 msg3 msg4; exact I : typeclass_instances.
Class cfail {T} (msg : T) := Build_cfail : True.
Hint Extern 0 (cfail ?msg) => idtac "Error:" msg; exact I : typeclass_instances.
Class cfail2 {T1 T2} (msg1 : T1) (msg2 : T2) := Build_cfail2 : True.
Hint Extern 0 (cfail2 ?msg1 ?msg2) => idtac "Error:" msg1 msg2; exact I : typeclass_instances.
Class cfail3 {T1 T2 T3} (msg1 : T1) (msg2 : T2) (msg3 : T3) := Build_cfail3 : True.
Hint Extern 0 (cfail3 ?msg1 ?msg2 ?msg3) => idtac "Error:" msg1 msg2 msg3; exact I : typeclass_instances.
Ltac constr_run_tac tac :=
let dummy := match goal with
| _ => tac ()
end in
constr:(I).
Ltac constr_run_tac_fail tac :=
let dummy := match goal with
| _ => tac ()
end in
constr:(I : I).
Ltac cidtac msg :=
constr_run_tac ltac:(fun _ => idtac msg).
Ltac cidtac2 msg1 msg2 :=
constr_run_tac ltac:(fun _ => idtac msg1 msg2).
Ltac cidtac3 msg1 msg2 msg3 :=
constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3).
Ltac cidtac4 msg1 msg2 msg3 msg4 :=
constr_run_tac ltac:(fun _ => idtac msg1 msg2 msg3 msg4).
Ltac cfail msg :=
constr_run_tac_fail ltac:(fun _ => idtac "Error:" msg).
Ltac cfail2 msg1 msg2 :=
constr_run_tac_fail ltac:(fun _ => idtac "Error:" msg1 msg2).
Ltac cfail3 msg1 msg2 msg3 :=
constr_run_tac_fail ltac:(fun _ => idtac "Error:" msg1 msg2 msg3).
Ltac idtac_goal := lazymatch goal with |- ?G => idtac "Goal:" G end.
Ltac idtac_context :=
try (repeat match goal with H : _ |- _ => revert H end;
idtac_goal;
lazymatch goal with |- ?G => idtac "Context:" G end;
fail).
|
