From 39fea17bac77535c9cff47cd6657a308e391ac8a Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 14 Aug 2018 18:15:24 +0100
Subject: Coq: attempt a quick proof before an indepth one

---
 lib/coq/Sail2_values.v | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

(limited to 'lib')

diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v
index 7766e6af..c63e8453 100644
--- a/lib/coq/Sail2_values.v
+++ b/lib/coq/Sail2_values.v
@@ -1021,6 +1021,9 @@ Ltac prepare_for_solver :=
  reduce_list_lengths;
  reduce_pow.
 Ltac solve_arithfact :=
+(* Attempt a simple proof first to avoid lengthy preparation steps (especially
+   as the large proof terms can upset subsequent proofs). *)
+try (constructor; omega);
 prepare_for_solver;
 (*dump_context;*)
  solve
@@ -1037,7 +1040,10 @@ prepare_for_solver;
  | constructor; eauto 3 with datatypes zarith sail
  | constructor; idtac "Unable to solve constraint"; dump_context; fail
  ].
-Hint Extern 0 (ArithFact _) => solve_arithfact : typeclass_instances.
+(* Add an indirection so that you can redefine run_solver to fail to get
+   slow running constraints into proof mode. *)
+Ltac run_solver := solve_arithfact.
+Hint Extern 0 (ArithFact _) => run_solver : typeclass_instances.
 
 Hint Unfold length_mword : sail.
 
-- 
cgit v1.2.3