--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 11:52:22 2010 +0200
@@ -12,6 +12,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -25,6 +26,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -34,6 +36,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = false,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -202,6 +205,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 30 11:52:22 2010 +0200
@@ -58,6 +58,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s1", "a1", "b1"], 2)],
replacing = [(("s1", "limited_s1"), "quickcheck")],
@@ -81,6 +82,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s2", "a2", "b2"], 3)],
replacing = [(("s2", "limited_s2"), "quickcheck")],
@@ -103,6 +105,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s3", "a3", "b3"], 6)],
replacing = [(("s3", "limited_s3"), "quickcheck")],
@@ -117,6 +120,7 @@
(*
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -143,6 +147,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["s4", "a4", "b4"], 6)],
replacing = [(("s4", "limited_s4"), "quickcheck")],
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Thu Sep 30 11:52:22 2010 +0200
@@ -86,6 +86,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [],
replacing = [],
@@ -97,7 +98,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 = 100000, report]*)
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
@@ -112,8 +113,24 @@
s = s\<^isub>3 @ [Enter g r c] @ s\<^isub>2 @ [Check_in g r c'] @ s\<^isub>1 \<and>
no_Check_in (s\<^isub>3 @ s\<^isub>2) r \<and> isin (s\<^isub>2 @ [Check_in g r c] @ s\<^isub>1) r = {})"
+section {* Manual setup to find the counterexample *}
+
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["hotel"], 4)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck")],
+ manual_reorder = []}) *}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [],
limited_predicates = [(["hotel"], 5)],
replacing = [(("hotel", "limited_hotel"), "quickcheck")],
@@ -124,4 +141,75 @@
quickcheck[generator = prolog, iterations = 1, expect = counterexample]
oops
+section {* Simulating a global depth limit manually by limiting all predicates *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 12)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = NONE,
+ limited_types = [],
+ limited_predicates = [(["feelssafe", "feelssafeaux", "noCheckin", "noCheckinaux", "appendP", "ownsP", "hotel", "hotelaux", "hotelauxaux", "roomkP", "issued", "currkP", "initkP",
+ "cards", "cardsauxauxaux", "cardsauxaux", "cardsaux", "isin", "isinauxauxa", "isinauxauxaux", "isinauxaux", "isinaux", "set"], 13)],
+ replacing = [(("hotel", "limited_hotel"), "quickcheck"), (("feelssafe", "limited_feelssafe"), "quickcheck"), (("isin", "limited_isin"), "quickcheck")],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
+section {* Using a global limit for limiting the execution *}
+
+text {* A global depth limit of 13 does not suffice to find the counterexample. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 13,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = no_counterexample]
+oops
+
+text {* But a global depth limit of 14 does. *}
+
+setup {*
+ Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limit_globally = SOME 14,
+ limited_types = [],
+ limited_predicates = [],
+ replacing = [],
+ manual_reorder = []})
+*}
+
+lemma
+ "hotel s ==> feels_safe s r ==> g \<in> isin s r ==> owns s r = Some g"
+quickcheck[generator = prolog, iterations = 1, expect = counterexample]
+oops
+
end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 11:52:22 2010 +0200
@@ -83,6 +83,7 @@
setup {* Code_Prolog.map_code_options (K
{ ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
replacing = [(("typing", "limited_typing"), "quickcheck"),
--- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 11:52:22 2010 +0200
@@ -6,6 +6,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
limited_predicates = [(["appendP"], 4), (["revP"], 4)],
replacing =
--- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 11:52:22 2010 +0200
@@ -100,6 +100,7 @@
setup {* Code_Prolog.map_code_options (K
{ensure_groundness = true,
+ limit_globally = NONE,
limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
(["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Sep 30 11:52:22 2010 +0200
@@ -9,6 +9,7 @@
datatype prolog_system = SWI_PROLOG | YAP
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
@@ -58,38 +59,45 @@
type code_options =
{ensure_groundness : bool,
+ limit_globally : int option,
limited_types : (typ * int) list,
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
manual_reorder : ((string * int) * int list) list}
-fun set_ensure_groundness {ensure_groundness, limited_types, limited_predicates,
+fun set_ensure_groundness {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = true, limited_types = limited_types,
+ {ensure_groundness = true, limit_globally = limit_globally, limited_types = limited_types,
limited_predicates = limited_predicates, replacing = replacing,
manual_reorder = manual_reorder}
-fun map_limit_predicates f {ensure_groundness, limited_types, limited_predicates,
+fun map_limit_predicates f {ensure_groundness, limit_globally, limited_types, limited_predicates,
replacing, manual_reorder} =
- {ensure_groundness = ensure_groundness, limited_types = limited_types,
+ {ensure_groundness = ensure_groundness, limit_globally = limit_globally, limited_types = limited_types,
limited_predicates = f limited_predicates, replacing = replacing,
manual_reorder = manual_reorder}
-
+
+fun merge_global_limit (NONE, NONE) = NONE
+ | merge_global_limit (NONE, SOME n) = SOME n
+ | merge_global_limit (SOME n, NONE) = SOME n
+ | merge_global_limit (SOME n, SOME m) = SOME (Int.max (n, m))
+
structure Options = Theory_Data
(
type T = code_options
- val empty = {ensure_groundness = false,
+ val empty = {ensure_groundness = false, limit_globally = NONE,
limited_types = [], limited_predicates = [], replacing = [], manual_reorder = []}
val extend = I;
fun merge
- ({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
- limited_predicates = limited_predicates1, replacing = replacing1,
- manual_reorder = manual_reorder1},
- {ensure_groundness = ensure_groundness2, limited_types = limited_types2,
- limited_predicates = limited_predicates2, replacing = replacing2,
- manual_reorder = manual_reorder2}) =
+ ({ensure_groundness = ensure_groundness1, limit_globally = limit_globally1,
+ limited_types = limited_types1, limited_predicates = limited_predicates1,
+ replacing = replacing1, manual_reorder = manual_reorder1},
+ {ensure_groundness = ensure_groundness2, limit_globally = limit_globally2,
+ limited_types = limited_types2, limited_predicates = limited_predicates2,
+ replacing = replacing2, manual_reorder = manual_reorder2}) =
{ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
+ limit_globally = merge_global_limit (limit_globally1, limit_globally2),
limited_types = AList.merge (op =) (K true) (limited_types1, limited_types2),
limited_predicates = AList.merge (op =) (K true) (limited_predicates1, limited_predicates2),
manual_reorder = AList.merge (op =) (K true) (manual_reorder1, manual_reorder2),
@@ -188,7 +196,7 @@
type clause = ((string * prol_term list) * prem);
type logic_program = clause list;
-
+
(* translation from introduction rules to internal representation *)
fun mk_conform f empty avoid name =
@@ -591,13 +599,14 @@
((mk_lim_rel_name rel_name, (Var "Lim") :: ts), prem)
end
-fun add_limited_predicates limited_predicates =
+fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
+
+fun add_limited_predicates limited_predicates (p, constant_table) =
let
- fun add (rel_names, limit) (p, constant_table) =
+ fun add (rel_names, limit) p =
let
val clauses = filter (fn ((rel, _), _) => member (op =) rel_names rel) p
val clauses' = map (mk_depth_limited rel_names) clauses
- fun nat_term_of n = funpow n (fn t => AppF ("suc", [t])) (Cons "zero")
fun mk_entry_clause rel_name =
let
val nargs = length (snd (fst
@@ -606,9 +615,9 @@
in
(("limited_" ^ rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
end
- in (p @ (map mk_entry_clause rel_names) @ clauses', constant_table) end
+ in (p @ (map mk_entry_clause rel_names) @ clauses') end
in
- fold add limited_predicates
+ (fold add limited_predicates p, constant_table)
end
@@ -663,10 +672,29 @@
val rename_vars_program = map rename_vars_clause
+(* limit computation globally by some threshold *)
+
+fun limit_globally ctxt limit const_name (p, constant_table) =
+ let
+ val rel_names = fold (fn ((r, _), _) => insert (op =) r) p []
+ val p' = map (mk_depth_limited rel_names) p
+ val rel_name = translate_const constant_table const_name
+ val nargs = length (snd (fst
+ (the (find_first (fn ((rel, _), _) => rel = rel_name) p))))
+ val vars = map (fn i => Var ("x" ^ string_of_int i)) (1 upto nargs)
+ val entry_clause = ((rel_name, vars), Rel ("lim_" ^ rel_name, nat_term_of limit :: vars))
+ val p'' = filter_out (fn ((rel, _), _) => rel = rel_name) p
+ in
+ (entry_clause :: p' @ p'', constant_table)
+ end
+
(* post processing of generated prolog program *)
-fun post_process ctxt options (p, constant_table) =
+fun post_process ctxt options const_name (p, constant_table) =
(p, constant_table)
+ |> (case #limit_globally options of
+ SOME limit => limit_globally ctxt limit const_name
+ | NONE => I)
|> (if #ensure_groundness options then
add_ground_predicates ctxt (#limited_types options)
else I)
@@ -915,7 +943,7 @@
val ctxt' = ProofContext.init_global thy'
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, #ensure_groundness options) ctxt' name (* FIXME *)
- |> post_process ctxt' options
+ |> post_process ctxt' options name
val constant_table' = declare_consts (fold Term.add_const_names all_args []) constant_table
val args' = map (translate_term ctxt constant_table') all_args
val _ = tracing "Running prolog program..."
@@ -991,7 +1019,7 @@
val ctxt' = ProofContext.init_global thy3
val _ = tracing "Generating prolog program..."
val (p, constant_table) = generate (NONE, true) ctxt' full_constname
- |> post_process ctxt' (set_ensure_groundness options)
+ |> post_process ctxt' (set_ensure_groundness options) full_constname
val _ = tracing "Running prolog program..."
val system_config = System_Config.get (Context.Proof ctxt)
val tss = run (#timeout system_config, #prolog_system system_config)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 30 09:45:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Thu Sep 30 11:52:22 2010 +0200
@@ -187,8 +187,6 @@
val (assms, concl) = Logic.strip_horn (prop_of split_thm)
val (P, [split_t]) = strip_comb (HOLogic.dest_Trueprop concl)
val subst = Pattern.match thy (split_t, t) (Vartab.empty, Vartab.empty)
- val (_, split_args) = strip_comb split_t
- val match = split_args ~~ args
fun flatten_of_assm assm =
let
val (vTs, assm') = strip_all (Envir.beta_norm (Envir.subst_term subst assm))