verit_timeout takes an integer as parameter

4 files changed, 48 insertions, 55 deletions

diff --git a/examples/Example.v b/examples/Example.v
index b949740..9fcb555 100644
--- a/examples/Example.v
+++ b/examples/Example.v
@@ -14,7 +14,6 @@
    If you are using native-coq instead of Coq 8.11, replace it with:
      Require Import SMTCoq.
    *)
-
 Require Import SMTCoq.SMTCoq.
 Require Import Bool.
 
@@ -425,3 +424,25 @@ Section CompCert.
   Qed.
 
 End CompCert.
+
+
+(** The verit solver can be called with an integer (the timeout in seconds).
+If the goal cannot be solved within timeout seconds, then an anomaly is raised **)
+
+Section test_timeout.
+
+Variable P : Z -> bool.
+Variable H0 : P 0.
+Variable HInd : forall n, implb (P n) (P (n + 1)).
+
+Goal P 3.
+(* verit_timeout 3. *) verit.
+Qed.
+
+Goal true -> P 1000000000.
+intro H.
+(* Fail verit_timeout 1. 
+Fail verit_timeout 5. *)
+Abort.
+
+End test_timeout.
diff --git a/examples/foo.v b/examples/foo.v
deleted file mode 100644
index c2162df..0000000
--- a/examples/foo.v
+++ /dev/null
@@ -1,28 +0,0 @@
-Add Rec LoadPath "../src" as SMTCoq.
-Require Import SMTCoq.SMTCoq.
-Require Import ZArith.
-
-Section test_timeout.
-
-Variable P : Z -> bool.
-Variable H0 : P 0.
-Variable HInd : forall n, implb (P n) (P (n + 1)).
-
-Goal P 3.
-verit.
-Qed.
-
-Tactic Notation "verit_timeout2"           :=
-  prop2bool;
-  [ .. | get_hyps ltac:(fun Hs =>
-                          lazymatch Hs with
-                          | Some ?Hs => idtac 1 ;
-                            prop2bool_hyps Hs; idtac 2 ;
-                            [ .. | idtac 3 ; verit_bool_base_auto_timeout (Some Hs) ]
-                          | None => idtac 4 ; verit_bool_base_auto_timeout (@None nat)
-                          end)
-  ].
-
-Goal true -> P 1000000000.
-intro H.
-verit_timeout2. constructor.
\ No newline at end of file
diff --git a/src/Tactics.v b/src/Tactics.v
index c44af14..316fcc1 100644
--- a/src/Tactics.v
+++ b/src/Tactics.v
@@ -91,28 +91,28 @@ Tactic Notation "verit_bool_no_check"           :=
 
 (** Tactics in bool with timeout **)
 
-Tactic Notation "verit_bool_base_auto_timeout" constr(h) := verit_bool_base_timeout h; auto with typeclass_instances.
-Tactic Notation "verit_bool_no_check_base_auto_timeout" constr(h) := verit_bool_no_check_base_timeout h; auto with typeclass_instances.
+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) :=
+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))
-                   | None => verit_bool_base_auto_timeout (Some h)
+                   | 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"           :=
-  get_hyps ltac:(fun Hs => verit_bool_base_auto_timeout Hs; 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) :=
+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))
-                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                   | 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"           :=
-  get_hyps ltac:(fun Hs => verit_bool_no_check_base_auto_timeout Hs; 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 **)
@@ -165,48 +165,48 @@ Tactic Notation "verit_no_check"           :=
                           end; vauto)
   ].
 
-Tactic Notation "verit_timeout" constr(h) :=
+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)) ]
-                                   | None => verit_bool_base_auto_timeout (Some h)
+                                     [ .. | verit_bool_base_auto_timeout (Some (h, Hs)) timeout]
+                                   | None => verit_bool_base_auto_timeout (Some h) timeout
                                  end; vauto)
          ]
   ].
-Tactic Notation "verit_timeout"           :=
+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) ]
-                          | None => verit_bool_base_auto_timeout (@None nat)
+                            [ .. | 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) :=
+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)) ]
-                                   | None => verit_bool_no_check_base_auto_timeout (Some h)
+                                     [ .. | 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"           :=
+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) ]
-                          | None => verit_bool_no_check_base_auto_timeout (@None nat)
+                            [ .. | verit_bool_no_check_base_auto_timeout (Some Hs) timeout]
+                          | None => verit_bool_no_check_base_auto_timeout (@None nat) timeout
                           end; vauto)
   ].
 
diff --git a/src/g_smtcoq.mlg b/src/g_smtcoq.mlg
index 19298f4..1d8f146 100644
--- a/src/g_smtcoq.mlg
+++ b/src/g_smtcoq.mlg
@@ -115,8 +115,8 @@ END
 TACTIC EXTEND Tactic_verit
 | [ "verit_bool_base" constr(lpl) ] -> { Verit.tactic None lpl (get_lemmas ()) }
 | [ "verit_bool_no_check_base" constr(lpl) ] -> { Verit.tactic_no_check None lpl (get_lemmas ()) }
-| [ "verit_bool_base_timeout" constr(lpl) ] -> { Verit.tactic (Some 5) lpl (get_lemmas ()) }
-| [ "verit_bool_no_check_base_timeout" constr(lpl) ] -> { Verit.tactic_no_check (Some 5) lpl (get_lemmas ()) }
+| [ "verit_bool_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic (Some timeout) lpl (get_lemmas ()) }
+| [ "verit_bool_no_check_base_timeout" constr(lpl) int_or_var(timeout) ] -> { Verit.tactic_no_check (Some timeout) lpl (get_lemmas ()) }
 END
 
 TACTIC EXTEND Tactic_cvc4