--- a/doc-src/Nitpick/nitpick.tex Mon Oct 25 22:47:02 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex Tue Oct 26 11:06:12 2010 +0200
@@ -1751,7 +1751,7 @@
{\slshape Nitpick ran out of time after checking 9 of 10 scopes.}
\postw
-Furthermore, applying \textit{skew} or \textit{split} to a well-formed tree
+Furthermore, applying \textit{skew} or \textit{split} on a well-formed tree
should not alter the tree:
\prew
@@ -1802,10 +1802,10 @@
\postw
Nitpick's output reveals that the element $0$ was added as a left child of $1$,
-where both have a level of 1. This violates the second AA tree invariant, which
-states that a left child's level must be less than its parent's. This shouldn't
-come as a surprise, considering that we commented out the tree rebalancing code.
-Reintroducing the code seems to solve the problem:
+where both nodes have a level of 1. This violates the second AA tree invariant,
+which states that a left child's level must be less than its parent's. This
+shouldn't come as a surprise, considering that we commented out the tree
+rebalancing code. Reintroducing the code seems to solve the problem:
\prew
\textbf{theorem}~\textit{wf\_insort\/}:\kern.4em ``$\textit{wf}~t\,\Longrightarrow\, \textit{wf}~(\textit{insort}~t~x)$'' \\
--- a/src/HOL/IsaMakefile Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Oct 26 11:06:12 2010 +0200
@@ -306,12 +306,15 @@
Tools/numeral.ML \
Tools/numeral_simprocs.ML \
Tools/numeral_syntax.ML \
+ Tools/Predicate_Compile/core_data.ML \
+ Tools/Predicate_Compile/mode_inference.ML \
Tools/Predicate_Compile/predicate_compile_aux.ML \
Tools/Predicate_Compile/predicate_compile_compilations.ML \
Tools/Predicate_Compile/predicate_compile_core.ML \
Tools/Predicate_Compile/predicate_compile_data.ML \
Tools/Predicate_Compile/predicate_compile_fun.ML \
Tools/Predicate_Compile/predicate_compile.ML \
+ Tools/Predicate_Compile/predicate_compile_proof.ML \
Tools/Predicate_Compile/predicate_compile_specialisation.ML \
Tools/Predicate_Compile/predicate_compile_pred.ML \
Tools/quickcheck_generators.ML \
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Prolog.thy Tue Oct 26 11:06:12 2010 +0200
@@ -23,7 +23,7 @@
setup {* Context.theory_map (Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck)) *}
lemma "\<lbrakk> hotel s; g \<in> isin s r \<rbrakk> \<Longrightarrow> owns s r = Some g"
-quickcheck[generator = code, iterations = 100000, report]
+quickcheck[generator = code, iterations = 10000, report]
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example_Small_Generator.thy Tue Oct 26 11:06:12 2010 +0200
@@ -5,6 +5,12 @@
declare Let_def[code_pred_inline]
+lemma [code_pred_inline]: "insert == (%y A x. y = x | A x)"
+by (auto simp add: insert_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+
+lemma [code_pred_inline]: "(op -) == (%A B x. A x \<and> \<not> B x)"
+by (auto simp add: Diff_iff[unfolded mem_def] fun_eq_iff intro!: eq_reflection)
+
instantiation room :: small_lazy
begin
@@ -44,8 +50,8 @@
lemma
"hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
-quickcheck[generator = small_generators_depth_14, iterations = 1, expect = no_counterexample]
-quickcheck[generator = small_generators_depth_15, iterations = 1, expect = counterexample]
+quickcheck[generator = small_generators_depth_14, iterations = 1, size = 1, expect = no_counterexample]
+quickcheck[generator = small_generators_depth_15, iterations = 1, size = 1, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Tue Oct 26 11:06:12 2010 +0200
@@ -16,7 +16,7 @@
manual_reorder = []}) *}
lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
-quickcheck[generator = code, iterations = 200000, expect = counterexample]
+quickcheck[generator = code, iterations = 10000]
quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
quickcheck[generator = prolog, expect = counterexample]
oops
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Tests.thy Tue Oct 26 11:06:12 2010 +0200
@@ -974,9 +974,10 @@
code_pred [new_random_dseq inductify] avl .
thm avl.new_random_dseq_equation
+(* TODO: has highly non-deterministic execution time!
values [new_random_dseq 2, 1, 7] 5 "{t:: int tree. avl t}"
-
+*)
fun set_of
where
"set_of ET = {}"
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Oct 26 11:06:12 2010 +0200
@@ -5,9 +5,9 @@
"Specialisation_Examples",
"Hotel_Example_Small_Generator",
"IMP_1",
- "IMP_2",
- "IMP_3",
- "IMP_4"];
+ "IMP_2"
+(* "IMP_3",
+ "IMP_4"*)];
if getenv "EXEC_SWIPL" = "" andalso getenv "EXEC_YAP" = "" then
(warning "No prolog system found - skipping some example theories"; ())
--- a/src/HOL/Tools/Metis/metis_translate.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Metis/metis_translate.ML Tue Oct 26 11:06:12 2010 +0200
@@ -68,7 +68,7 @@
val combtyp_of : combterm -> combtyp
val strip_combterm_comb : combterm -> combterm * combterm list
val combterm_from_term :
- theory -> int -> (string * typ) list -> term -> combterm * typ list
+ theory -> (string * typ) list -> term -> combterm * typ list
val reveal_old_skolem_terms : (string * term) list -> term -> term
val tfree_classes_of_terms : term list -> string list
val tvar_classes_of_terms : term list -> string list
@@ -215,10 +215,9 @@
(s, Sign.the_const_type thy s) |> Sign.const_typargs thy |> length
fun new_skolem_var_from_const s =
- let
- val ss = s |> space_explode Long_Name.separator
- val n = length ss
- in (nth ss (n - 2), nth ss (n - 3) |> Int.fromString |> the) end
+ let val ss = s |> space_explode Long_Name.separator in
+ (nth ss (length ss - 2), 0)
+ end
(**** Definitions and functions for FOL clauses for TPTP format output ****)
@@ -396,17 +395,18 @@
| simple_combtype_of (TVar (x, _)) =
CombTVar (make_schematic_type_var x, string_of_indexname x)
-fun new_skolem_const_name th_no s num_T_args =
- [new_skolem_const_prefix, string_of_int th_no, s, string_of_int num_T_args]
+fun new_skolem_const_name s num_T_args =
+ [new_skolem_const_prefix, s, string_of_int num_T_args]
|> space_implode Long_Name.separator
-(* Converts a term (with combinators) into a combterm. Also accummulates sort
+(* Converts a term (with combinators) into a combterm. Also accumulates sort
infomation. *)
-fun combterm_from_term thy th_no bs (P $ Q) =
- let val (P', tsP) = combterm_from_term thy th_no bs P
- val (Q', tsQ) = combterm_from_term thy th_no bs Q
- in (CombApp (P', Q'), union (op =) tsP tsQ) end
- | combterm_from_term thy _ _ (Const (c, T)) =
+fun combterm_from_term thy bs (P $ Q) =
+ let
+ val (P', tsP) = combterm_from_term thy bs P
+ val (Q', tsQ) = combterm_from_term thy bs Q
+ in (CombApp (P', Q'), union (op =) tsP tsQ) end
+ | combterm_from_term thy _ (Const (c, T)) =
let
val (tp, ts) = combtype_of T
val tvar_list =
@@ -417,43 +417,42 @@
|> map simple_combtype_of
val c' = CombConst (`make_fixed_const c, tp, tvar_list)
in (c',ts) end
- | combterm_from_term _ _ _ (Free (v, T)) =
+ | combterm_from_term _ _ (Free (v, T)) =
let val (tp, ts) = combtype_of T
val v' = CombConst (`make_fixed_var v, tp, [])
in (v',ts) end
- | combterm_from_term _ th_no _ (Var (v as (s, _), T)) =
+ | combterm_from_term _ _ (Var (v as (s, _), T)) =
let
val (tp, ts) = combtype_of T
val v' =
if String.isPrefix Meson_Clausify.new_skolem_var_prefix s then
let
val tys = T |> strip_type |> swap |> op ::
- val s' = new_skolem_const_name th_no s (length tys)
+ val s' = new_skolem_const_name s (length tys)
in
CombConst (`make_fixed_const s', tp, map simple_combtype_of tys)
end
else
CombVar ((make_schematic_var v, string_of_indexname v), tp)
in (v', ts) end
- | combterm_from_term _ _ bs (Bound j) =
+ | combterm_from_term _ bs (Bound j) =
let
val (s, T) = nth bs j
val (tp, ts) = combtype_of T
val v' = CombConst (`make_bound_var s, tp, [])
in (v', ts) end
- | combterm_from_term _ _ _ (Abs _) = raise Fail "HOL clause: Abs"
+ | combterm_from_term _ _ (Abs _) = raise Fail "HOL clause: Abs"
-fun predicate_of thy th_no ((@{const Not} $ P), pos) =
- predicate_of thy th_no (P, not pos)
- | predicate_of thy th_no (t, pos) =
- (combterm_from_term thy th_no [] (Envir.eta_contract t), pos)
+fun predicate_of thy ((@{const Not} $ P), pos) = predicate_of thy (P, not pos)
+ | predicate_of thy (t, pos) =
+ (combterm_from_term thy [] (Envir.eta_contract t), pos)
-fun literals_of_term1 args thy th_no (@{const Trueprop} $ P) =
- literals_of_term1 args thy th_no P
- | literals_of_term1 args thy th_no (@{const HOL.disj} $ P $ Q) =
- literals_of_term1 (literals_of_term1 args thy th_no P) thy th_no Q
- | literals_of_term1 (lits, ts) thy th_no P =
- let val ((pred, ts'), pol) = predicate_of thy th_no (P, true) in
+fun literals_of_term1 args thy (@{const Trueprop} $ P) =
+ literals_of_term1 args thy P
+ | literals_of_term1 args thy (@{const HOL.disj} $ P $ Q) =
+ literals_of_term1 (literals_of_term1 args thy P) thy Q
+ | literals_of_term1 (lits, ts) thy P =
+ let val ((pred, ts'), pol) = predicate_of thy (P, true) in
(FOLLiteral (pol, pred) :: lits, union (op =) ts ts')
end
val literals_of_term = literals_of_term1 ([], [])
@@ -607,9 +606,10 @@
metis_lit pos "=" (map hol_term_to_fol_FT tms)
| _ => metis_lit pos "{}" [hol_term_to_fol_FT tm]) (*hBOOL*);
-fun literals_of_hol_term thy th_no mode t =
- let val (lits, types_sorts) = literals_of_term thy th_no t
- in (map (hol_literal_to_fol mode) lits, types_sorts) end;
+fun literals_of_hol_term thy mode t =
+ let val (lits, types_sorts) = literals_of_term thy t in
+ (map (hol_literal_to_fol mode) lits, types_sorts)
+ end
(*Sign should be "true" for conjecture type constraints, "false" for type lits in clauses.*)
fun metis_of_type_literals pos (TyLitVar ((s, _), (s', _))) =
@@ -623,13 +623,13 @@
fun metis_of_tfree tf =
Metis_Thm.axiom (Metis_LiteralSet.singleton (metis_of_type_literals true tf));
-fun hol_thm_to_fol is_conjecture th_no ctxt type_lits mode j old_skolems th =
+fun hol_thm_to_fol is_conjecture ctxt type_lits mode j old_skolems th =
let
val thy = ProofContext.theory_of ctxt
val (old_skolems, (mlits, types_sorts)) =
th |> prop_of |> Logic.strip_imp_concl
|> conceal_old_skolem_terms j old_skolems
- ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy th_no mode)
+ ||> (HOLogic.dest_Trueprop #> literals_of_hol_term thy mode)
in
if is_conjecture then
(Metis_Thm.axiom (Metis_LiteralSet.fromList mlits),
@@ -732,21 +732,20 @@
| set_mode FT = FT
val mode = set_mode mode0
(*transform isabelle clause to metis clause *)
- fun add_thm th_no is_conjecture (metis_ith, isa_ith)
+ fun add_thm is_conjecture (metis_ith, isa_ith)
{axioms, tfrees, old_skolems} : logic_map =
let
val (mth, tfree_lits, old_skolems) =
- hol_thm_to_fol is_conjecture th_no ctxt type_lits mode (length axioms)
+ hol_thm_to_fol is_conjecture ctxt type_lits mode (length axioms)
old_skolems metis_ith
in
{axioms = (mth, Meson.make_meta_clause isa_ith) :: axioms,
tfrees = union (op =) tfree_lits tfrees, old_skolems = old_skolems}
end;
val lmap = {axioms = [], tfrees = init_tfrees ctxt, old_skolems = []}
- |> fold (add_thm 0 true o `I) cls
+ |> fold (add_thm true o `I) cls
|> add_tfrees
- |> fold (fn (th_no, ths) => fold (add_thm th_no false o `I) ths)
- (1 upto length thss ~~ thss)
+ |> fold (fold (add_thm false o `I)) thss
val clause_lists = map (Metis_Thm.clause o #1) (#axioms lmap)
fun is_used c =
exists (Metis_LiteralSet.exists (const_in_metis c o #2)) clause_lists
@@ -763,7 +762,7 @@
[]
else
thms)
- in lmap |> fold (add_thm ~1 false) helper_ths end
+ in lmap |> fold (add_thm false) helper_ths end
in
(mode, add_type_thm (type_ext thy (maps (map prop_of) (cls :: thss))) lmap)
end
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Oct 26 11:06:12 2010 +0200
@@ -505,29 +505,29 @@
end
fun solve max_var (lits, comps, sexps) =
- let
- fun do_assigns assigns =
- SOME (literals_from_assignments max_var assigns lits
- |> tap print_solution)
- val _ = print_problem lits comps sexps
- val prop = PropLogic.all (map prop_for_literal lits @
- map prop_for_comp comps @
- map prop_for_sign_expr sexps)
- val default_val = bool_from_sign Minus
- in
- if PropLogic.eval (K default_val) prop then
- do_assigns (K (SOME default_val))
- else
- let
- (* use the first ML solver (to avoid startup overhead) *)
- val solvers = !SatSolver.solvers
- |> filter (member (op =) ["dptsat", "dpll"] o fst)
- in
- case snd (hd solvers) prop of
- SatSolver.SATISFIABLE assigns => do_assigns assigns
- | _ => NONE
- end
- end
+ let
+ fun do_assigns assigns =
+ SOME (literals_from_assignments max_var assigns lits
+ |> tap print_solution)
+ val _ = print_problem lits comps sexps
+ val prop = PropLogic.all (map prop_for_literal lits @
+ map prop_for_comp comps @
+ map prop_for_sign_expr sexps)
+ val default_val = bool_from_sign Minus
+ in
+ if PropLogic.eval (K default_val) prop then
+ do_assigns (K (SOME default_val))
+ else
+ let
+ (* use the first ML solver (to avoid startup overhead) *)
+ val solvers = !SatSolver.solvers
+ |> filter (member (op =) ["dptsat", "dpll"] o fst)
+ in
+ case snd (hd solvers) prop of
+ SatSolver.SATISFIABLE assigns => do_assigns assigns
+ | _ => NONE
+ end
+ end
type mtype_schema = mtyp * constraint_set
type mtype_context =
--- a/src/HOL/Tools/Predicate_Compile/core_data.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/core_data.ML Tue Oct 26 11:06:12 2010 +0200
@@ -186,7 +186,7 @@
fun lookup_predfun_data ctxt name mode =
Option.map rep_predfun_data
- (AList.lookup (op =) (#predfun_data (the_pred_data ctxt name)) mode)
+ (AList.lookup eq_mode (#predfun_data (the_pred_data ctxt name)) mode)
fun the_predfun_data ctxt name mode =
case lookup_predfun_data ctxt name mode of
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Oct 26 11:06:12 2010 +0200
@@ -35,7 +35,7 @@
val split_map_modeT : (mode -> typ -> typ option * typ option)
-> mode -> typ list -> typ list * typ list
val split_mode : mode -> term list -> term list * term list
- val split_modeT' : mode -> typ list -> typ list * typ list
+ val split_modeT : mode -> typ list -> typ list * typ list
val string_of_mode : mode -> string
val ascii_string_of_mode : mode -> string
(* premises *)
@@ -393,24 +393,22 @@
fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
| map_filter_prod f t = f t
-
-(* obviously, split_mode' and split_modeT' do not match? where does that cause problems? *)
-fun split_modeT' mode Ts =
+fun split_modeT mode Ts =
let
- fun split_arg_mode' (Fun _) T = ([], [])
- | split_arg_mode' (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
+ fun split_arg_mode (Fun _) T = ([], [])
+ | split_arg_mode (Pair (m1, m2)) (Type (@{type_name Product_Type.prod}, [T1, T2])) =
let
- val (i1, o1) = split_arg_mode' m1 T1
- val (i2, o2) = split_arg_mode' m2 T2
+ val (i1, o1) = split_arg_mode m1 T1
+ val (i2, o2) = split_arg_mode m2 T2
in
(i1 @ i2, o1 @ o2)
end
- | split_arg_mode' Input T = ([T], [])
- | split_arg_mode' Output T = ([], [T])
- | split_arg_mode' _ _ = raise Fail "split_modeT': mode and type do not match"
+ | split_arg_mode Input T = ([T], [])
+ | split_arg_mode Output T = ([], [T])
+ | split_arg_mode _ _ = raise Fail "split_modeT: mode and type do not match"
in
- (pairself flat o split_list) (map2 split_arg_mode' (strip_fun_mode mode) Ts)
+ (pairself flat o split_list) (map2 split_arg_mode (strip_fun_mode mode) Ts)
end
fun string_of_mode mode =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Oct 26 11:06:12 2010 +0200
@@ -167,7 +167,7 @@
(* validity checks *)
-fun check_expected_modes preds options modes =
+fun check_expected_modes options preds modes =
case expected_modes options of
SOME (s, ms) => (case AList.lookup (op =) modes s of
SOME modes =>
@@ -183,7 +183,7 @@
| NONE => ())
| NONE => ()
-fun check_proposed_modes preds options modes errors =
+fun check_proposed_modes options preds modes errors =
map (fn (s, _) => case proposed_modes options s of
SOME ms => (case AList.lookup (op =) modes s of
SOME inferred_ms =>
@@ -319,7 +319,7 @@
fn compfuns => fn s => fn T => fn mode => fn additional_arguments => fn compilation =>
let
val [depth] = additional_arguments
- val (_, Ts) = split_modeT' mode (binder_types T)
+ val (_, Ts) = split_modeT mode (binder_types T)
val T' = mk_predT compfuns (HOLogic.mk_tupleT Ts)
val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T')
in
@@ -1379,8 +1379,8 @@
options (lookup_mode, lookup_neg_mode, needs_random) ctxt preds all_modes param_vs clauses)
val thy' = fold (fn (s, ms) => set_needs_random s ms) needs_random thy
val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses
- val _ = check_expected_modes preds options modes
- val _ = check_proposed_modes preds options modes errors
+ val _ = check_expected_modes options preds modes
+ val _ = check_proposed_modes options preds modes errors
val _ = print_modes options modes
val _ = print_step options "Defining executable functions..."
val thy'' =
@@ -1799,7 +1799,7 @@
mk_map compfuns T HOLogic.termT (HOLogic.term_of_const T) t
val thy = ProofContext.theory_of ctxt
val (ts, statistics) =
- case compilation of
+ (case compilation of
(* Random =>
fst (Predicate.yieldn k
(Code_Eval.eval NONE ("Predicate_Compile_Core.random_eval_ref", random_eval_ref)
@@ -1809,25 +1809,25 @@
let
val [nrandom, size, depth] = arguments
in
- rpair NONE (fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Random_Result.get, put_dseq_random_result, "Predicate_Compile_Core.put_dseq_random_result")
thy NONE (fn proc => fn g => fn nrandom => fn size => fn s => g nrandom size s |>> DSequence.map proc)
t' [] nrandom size
|> Random_Engine.run)
- depth true))
+ depth true)) ())
end
| DSeq =>
- rpair NONE (fst (DSequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (DSequence.yieldn k
(Code_Runtime.dynamic_value_strict (Dseq_Result.get, put_dseq_result, "Predicate_Compile_Core.put_dseq_result")
- thy NONE DSequence.map t' []) (the_single arguments) true))
+ thy NONE DSequence.map t' []) (the_single arguments) true)) ())
| Pos_Generator_DSeq =>
let
val depth = (the_single arguments)
in
- rpair NONE (fst (Lazy_Sequence.yieldn k
+ rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict (New_Dseq_Result.get, put_new_dseq_result, "Predicate_Compile_Core.put_new_dseq_result")
thy NONE (fn proc => fn g => fn depth => g depth |> Lazy_Sequence.mapa proc)
- t' [] depth)))
+ t' [] depth))) ())
end
| New_Pos_Random_DSeq =>
let
@@ -1835,27 +1835,28 @@
val seed = Random_Engine.next_seed ()
in
if stats then
- apsnd (SOME o accumulate) (split_list
- (fst (Lazy_Sequence.yieldn k
+ apsnd (SOME o accumulate) (split_list (TimeLimit.timeLimit (Time.fromSeconds 20)
+ (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Stats_Result.get, put_lseq_random_stats_result, "Predicate_Compile_Core.put_lseq_random_stats_result")
thy NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa (apfst proc))
- t' [] nrandom size seed depth))))
+ t' [] nrandom size seed depth))) ()))
else rpair NONE
- (fst (Lazy_Sequence.yieldn k
+ (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Lazy_Sequence.yieldn k
(Code_Runtime.dynamic_value_strict
(Lseq_Random_Result.get, put_lseq_random_result, "Predicate_Compile_Core.put_lseq_random_result")
thy NONE
(fn proc => fn g => fn nrandom => fn size => fn s => fn depth => g nrandom size s depth
|> Lazy_Sequence.mapa proc)
- t' [] nrandom size seed depth)))
+ t' [] nrandom size seed depth))) ())
end
| _ =>
- rpair NONE (fst (Predicate.yieldn k
+ rpair NONE (TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => fst (Predicate.yieldn k
(Code_Runtime.dynamic_value_strict (Pred_Result.get, put_pred_result, "Predicate_Compile_Core.put_pred_result")
- thy NONE Predicate.map t' [])))
+ thy NONE Predicate.map t' []))) ()))
+ handle TimeLimit.TimeOut => error "Reached timeout during execution of values"
in ((T, ts), statistics) end;
fun values ctxt param_user_modes ((raw_expected, stats), comp_options) k t_compr =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Oct 26 11:06:12 2010 +0200
@@ -74,6 +74,11 @@
*)
val defining_term_of_introrule = defining_term_of_introrule_term o prop_of
+fun defining_const_of_introrule th =
+ case defining_term_of_introrule th
+ of Const (c, _) => c
+ | _ => raise TERM ("defining_const_of_introrule failed: Not a constant", [prop_of th])
+
(*TODO*)
fun is_introlike_term t = true
@@ -194,7 +199,7 @@
defining_const_of_equation (normalize_equation thy th) = fst (dest_Const t) then
SOME (normalize_equation thy th)
else
- if is_introlike th andalso defining_term_of_introrule th = t then
+ if is_introlike th andalso defining_const_of_introrule th = fst (dest_Const t) then
SOME th
else
NONE
@@ -206,7 +211,8 @@
| ths => rev ths
val _ =
if show_intermediate_results options then
- Output.tracing (commas (map (Display.string_of_thm_global thy) spec))
+ Output.tracing ("Specification for " ^ (Syntax.string_of_term_global thy t) ^ ":\n" ^
+ commas (map (Display.string_of_thm_global thy) spec))
else ()
in
spec
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Tue Oct 26 11:06:12 2010 +0200
@@ -53,7 +53,7 @@
fun combformula_for_prop thy =
let
- val do_term = combterm_from_term thy ~1
+ val do_term = combterm_from_term thy
fun do_quant bs q s T t' =
let val s = Name.variant (map fst bs) s in
do_formula ((s, T) :: bs) t'
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Tue Oct 26 11:06:12 2010 +0200
@@ -157,7 +157,7 @@
prover :: avoid_too_many_local_threads thy n provers
end
-val num_processors = try Thread.numProcessors #> the_default 1
+fun num_processors () = try Thread.numProcessors () |> the_default 1
(* The first ATP of the list is used by Auto Sledgehammer. Because of the low
timeout, it makes sense to put SPASS first. *)
@@ -362,6 +362,6 @@
(minimize_command [] 1) state
end
-val setup = Auto_Tools.register_tool ("sledgehammer", auto_sledgehammer)
+val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
end;
--- a/src/Tools/quickcheck.ML Mon Oct 25 22:47:02 2010 +0200
+++ b/src/Tools/quickcheck.ML Tue Oct 26 11:06:12 2010 +0200
@@ -196,10 +196,12 @@
val (result, new_report) = with_testers k testers
val reports = ((k, new_report) :: reports)
in case result of NONE => with_size (k + 1) reports | SOME q => (SOME q, reports) end);
- val ((result, reports), exec_time) = cpu_time "quickcheck execution"
+ val ((result, reports), exec_time) =
+ TimeLimit.timeLimit (Time.fromSeconds 20) (fn () => cpu_time "quickcheck execution"
(fn () => apfst
(fn result => case result of NONE => NONE
- | SOME ts => SOME (names ~~ ts)) (with_size 1 []))
+ | SOME ts => SOME (names ~~ ts)) (with_size 1 []))) ()
+ handle TimeLimit.TimeOut => error "Reached timeout during Quickcheck"
in
(result, ([exec_time, comp_time], if report ctxt then SOME reports else NONE))
end;