diff options
Diffstat (limited to 'src/Tactics.v')
| -rw-r--r-- | src/Tactics.v | 73 |
1 files changed, 72 insertions, 1 deletions
diff --git a/src/Tactics.v b/src/Tactics.v index 14b984b..727e0b7 100644 --- a/src/Tactics.v +++ b/src/Tactics.v @@ -29,7 +29,7 @@ Ltac get_hyps_acc acc := | id _ => fail | _ => let _ := match goal with _ => change P with (id P) in H end in - match acc with + lazymatch acc with | Some ?t => get_hyps_acc (Some (H, t)) | None => get_hyps_acc (Some H) end @@ -94,6 +94,31 @@ Tactic Notation "verit_bool_no_check" := let Hs := get_hyps in fun Hs => verit_bool_no_check_base_auto Hs; vauto. +(** Tactics in bool with timeout **) + +Tactic Notation "verit_bool_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_base_timeout h timeout; auto with typeclass_instances. +Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) int_or_var(timeout) := verit_bool_no_check_base_timeout h timeout; auto with typeclass_instances. + +Tactic Notation "verit_bool_timeout" constr(h) int_or_var(timeout) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_base_auto_timeout (Some h) timeout + end; + vauto). +Tactic Notation "verit_bool_timeout" int_or_var(timeout) := + get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs timeout; vauto). + +Tactic Notation "verit_bool_no_check_timeout" constr(h) int_or_var (timeout) := + get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout + end; + vauto). +Tactic Notation "verit_bool_no_check_timeout" int_or_var(timeout) := + get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs timeout; vauto). + (** Tactics in Prop **) @@ -145,6 +170,52 @@ Tactic Notation "verit_no_check" := end; vauto ]. +Tactic Notation "verit_timeout" constr(h) int_or_var(timeout) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout] + | None => verit_bool_base_auto_timeout (Some h) timeout + end; vauto) + ] + ]. +Tactic Notation "verit_timeout" int_or_var(timeout) := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_base_auto_timeout (Some Hs) timeout] + | None => verit_bool_base_auto_timeout (@None nat) timeout + end; vauto) + ]. +Tactic Notation "verit_no_check_timeout" constr(h) int_or_var(timeout) := + prop2bool; + [ .. | prop2bool_hyps h; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some (h, Hs)) timeout ] + | None => verit_bool_no_check_base_auto_timeout (Some h) timeout + end; vauto) + ] + ]. +Tactic Notation "verit_no_check_timeout" int_or_var(timeout) := + prop2bool; + [ .. | get_hyps ltac:(fun Hs => + match Hs with + | Some ?Hs => + prop2bool_hyps Hs; + [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout] + | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout + end; vauto) + ]. + + Ltac cvc4 := prop2bool; [ .. | cvc4_bool; bool2prop ]. Ltac cvc4_no_check := prop2bool; [ .. | cvc4_bool_no_check; bool2prop ]. |