--- a/src/HOL/IsaMakefile Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/IsaMakefile Tue Sep 07 12:04:34 2010 +0200
@@ -243,6 +243,8 @@
Map.thy \
Nat_Numeral.thy \
Nat_Transfer.thy \
+ New_DSequence.thy \
+ New_Random_Sequence.thy \
Nitpick.thy \
Numeral_Simprocs.thy \
Presburger.thy \
@@ -1339,8 +1341,15 @@
Predicate_Compile_Examples/Predicate_Compile_Examples.thy \
Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy \
Predicate_Compile_Examples/Code_Prolog_Examples.thy \
+ Predicate_Compile_Examples/Context_Free_Grammar_Example.thy \
Predicate_Compile_Examples/Hotel_Example.thy \
- Predicate_Compile_Examples/Lambda_Example.thy
+ Predicate_Compile_Examples/IMP_1.thy \
+ Predicate_Compile_Examples/IMP_2.thy \
+ Predicate_Compile_Examples/IMP_3.thy \
+ Predicate_Compile_Examples/IMP_4.thy \
+ Predicate_Compile_Examples/Lambda_Example.thy \
+ Predicate_Compile_Examples/List_Examples.thy \
+ Predicate_Compile_Examples/Reg_Exp_Example.thy
@$(ISABELLE_TOOL) usedir $(OUT)/HOL Predicate_Compile_Examples
--- a/src/HOL/Library/Fset.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Library/Fset.thy Tue Sep 07 12:04:34 2010 +0200
@@ -230,7 +230,7 @@
instantiation fset :: (type) equal
begin
-definition
+definition [code]:
"HOL.equal A B \<longleftrightarrow> A \<le> B \<and> B \<le> (A :: 'a fset)"
instance proof
--- a/src/HOL/New_DSequence.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/New_DSequence.thy Tue Sep 07 12:04:34 2010 +0200
@@ -83,7 +83,7 @@
definition pos_not_seq :: "unit neg_dseq => unit pos_dseq"
where
- "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq i))"
+ "pos_not_seq xq = (%i. Lazy_Sequence.hb_not_seq (xq (3 * i)))"
definition neg_not_seq :: "unit pos_dseq => unit neg_dseq"
where
--- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Sep 07 12:04:34 2010 +0200
@@ -16,6 +16,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
values "{(x, y, z). append x y z}"
@@ -28,6 +29,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.YAP}) *}
values "{(x, y, z). append x y z}"
@@ -38,6 +40,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
@@ -207,6 +210,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 2 "{y. notB y}"
--- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Tue Sep 07 12:04:34 2010 +0200
@@ -62,6 +62,7 @@
limited_predicates = [(["s1", "a1", "b1"], 2)],
replacing = [(("s1", "limited_s1"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
@@ -86,6 +87,7 @@
limited_predicates = [(["s2", "a2", "b2"], 3)],
replacing = [(("s2", "limited_s2"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
@@ -109,6 +111,7 @@
limited_predicates = [(["s3", "a3", "b3"], 6)],
replacing = [(("s3", "limited_s3"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
lemma S\<^isub>3_sound:
@@ -124,6 +127,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
@@ -149,6 +153,7 @@
limited_predicates = [(["s4", "a4", "b4"], 6)],
replacing = [(("s4", "limited_s4"), "quickcheck")],
manual_reorder = [(("quickcheck", 1), [0,2,1,4,3,5])],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
--- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Sep 07 12:04:34 2010 +0200
@@ -90,6 +90,7 @@
limited_predicates = [],
replacing = [],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
values 40 "{s. hotel s}"
@@ -119,6 +120,7 @@
limited_predicates = [(["hotel"], 5)],
replacing = [(("hotel", "limited_hotel"), "quickcheck")],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
lemma
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_1.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,34 @@
+theory IMP_1
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, and IF.
+*}
+
+types
+ var = unit
+ state = bool
+
+datatype com =
+ Skip |
+ Ass bool |
+ Seq com com |
+ IF com com
+
+inductive exec :: "com => state => state => bool" where
+ "exec Skip s s" |
+ "exec (Ass e) s e" |
+ "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+ "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
+ "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t"
+
+lemma
+ "exec c s s' ==> exec (Seq c c) s s'"
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1, expect = counterexample]
+oops
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_2.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_2
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+ In this example, the state is one boolean variable and the commands are Skip, Ass, Seq, IF and While.
+*}
+
+types
+ var = unit
+ state = bool
+
+datatype com =
+ Skip |
+ Ass bool |
+ Seq com com |
+ IF com com |
+ While com
+
+inductive exec :: "com => state => state => bool" where
+ "exec Skip s s" |
+ "exec (Ass e) s e" |
+ "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+ "s ==> exec c1 s t ==> exec (IF c1 c2) s t" |
+ "\<not> s ==> exec c2 s t ==> exec (IF c1 c2) s t" |
+ "\<not> s ==> exec (While c) s s" |
+ "s ==> exec c s s' ==> exec (While c) s' s'' ==> exec (While c) s s''"
+
+lemma
+ "exec c s s' ==> exec (Seq c c) s s'"
+quickcheck[generator = predicate_compile_wo_ff, size = 2, iterations = 1]
+oops
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_3.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_3
+imports "Predicate_Compile_Quickcheck"
+begin
+
+subsection {* IMP *}
+
+text {*
+ In this example, the state is one integer variable and the commands are Skip, Ass, Seq, IF, and While.
+*}
+
+types
+ var = unit
+ state = int
+
+datatype com =
+ Skip |
+ Ass var "int" |
+ Seq com com |
+ IF "state list" com com |
+ While "state list" com
+
+inductive exec :: "com => state => state => bool" where
+ "exec Skip s s" |
+ "exec (Ass x e) s e" |
+ "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+ "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+ "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+ "s \<notin> set b ==> exec (While b c) s s" |
+ "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+lemma
+ "exec c s s' ==> exec (Seq c c) s s'"
+ quickcheck[generator = predicate_compile_ff_nofs, size=2, iterations=3, quiet = false, expect = counterexample]
+oops
+
+
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/IMP_4.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,37 @@
+theory IMP_4
+imports Predicate_Compile_Quickcheck
+begin
+
+subsection {* IMP *}
+
+text {*
+ In this example, the state is a list of integers and the commands are Skip, Ass, Seq, IF and While.
+*}
+
+types
+ var = nat
+ state = "int list"
+
+datatype com =
+ Skip |
+ Ass var "int" |
+ Seq com com |
+ IF "state list" com com |
+ While "state list" com
+
+inductive exec :: "com => state => state => bool" where
+ "exec Skip s s" |
+ "exec (Ass x e) s (s[x := e])" |
+ "exec c1 s1 s2 ==> exec c2 s2 s3 ==> exec (Seq c1 c2) s1 s3" |
+ "s \<in> set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" |
+ "s \<notin> set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" |
+ "s \<notin> set b ==> exec (While b c) s s" |
+ "s1 \<in> set b ==> exec c s1 s2 ==> exec (While b c) s2 s3 ==> exec (While b c) s1 s3"
+
+lemma
+ "exec c s s' ==> exec (Seq c c) s s'"
+ nitpick (* nitpick fails here! *)
+ quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10, expect=counterexample]
+oops
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Sep 07 12:04:34 2010 +0200
@@ -88,6 +88,7 @@
replacing = [(("typing", "limited_typing"), "quickcheck"),
(("nthel1", "limited_nthel1"), "lim_typing")],
manual_reorder = [],
+ timeout = Time.fromSeconds 10,
prolog_system = Code_Prolog.SWI_PROLOG}) *}
lemma
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,25 @@
+theory List_Examples
+imports Main "Predicate_Compile_Quickcheck" "Code_Prolog"
+begin
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
+ limited_predicates = [(["appendP"], 4), (["revP"], 4)],
+ replacing =
+ [(("appendP", "limited_appendP"), "quickcheck"),
+ (("revP", "limited_revP"), "quickcheck"),
+ (("appendP", "limited_appendP"), "lim_revP")],
+ manual_reorder = [],
+ timeout = Time.fromSeconds 10,
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+lemma "(xs :: nat list) = ys @ ys --> rev xs = xs"
+quickcheck[generator = code, iterations = 200000, expect = counterexample]
+quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]
+quickcheck[generator = prolog, expect = counterexample]
+oops
+
+end
\ No newline at end of file
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy Tue Sep 07 12:04:34 2010 +0200
@@ -810,8 +810,7 @@
(let (y', x') = f i y x; (y'', xs') = fold_map_idx f (Suc i) y' xs
in (y'', x' # xs'))"
-text {* mode analysis explores thousand modes - this is infeasible at the moment... *}
-(*code_pred [inductify, show_steps] fold_map_idx .*)
+code_pred [inductify] fold_map_idx .
subsection {* Minimum *}
@@ -939,10 +938,10 @@
"height ET = 0"
| "height (MKT x l r h) = max (height l) (height r) + 1"
-consts avl :: "'a tree => bool"
-primrec
+primrec avl :: "'a tree => bool"
+where
"avl ET = True"
- "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
+| "avl (MKT x l r h) = ((height l = height r \<or> height l = 1 + height r \<or> height r = 1+height l) \<and>
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)"
(*
code_pred [inductify] avl .
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy Tue Sep 07 12:04:34 2010 +0200
@@ -187,7 +187,7 @@
lemma
"exec c s s' ==> exec (Seq c c) s s'"
-(*quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=10]*)
+ quickcheck[generator = predicate_compile_wo_ff, size=2, iterations=20, expect = counterexample]
oops
subsection {* Lambda *}
--- a/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/ROOT.ML Tue Sep 07 12:04:34 2010 +0200
@@ -1,2 +1,3 @@
-use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples"];
-if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Hotel_Example", "Lambda_Example"];
+use_thys ["Predicate_Compile_Examples", "Predicate_Compile_Quickcheck_Examples", "Specialisation_Examples", "IMP_1", "IMP_2", "IMP_3", "IMP_4"];
+if getenv "PROLOG_HOME" = "" then () else use_thys ["Code_Prolog_Examples", "Context_Free_Grammar_Example", "Hotel_Example", "Lambda_Example", "List_Examples"];
+setmp_noncritical quick_and_dirty true use_thys ["Reg_Exp_Example"];
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Tue Sep 07 12:04:34 2010 +0200
@@ -0,0 +1,184 @@
+theory Reg_Exp_Example
+imports Predicate_Compile_Quickcheck Code_Prolog
+begin
+
+text {* An example from the experiments from SmallCheck (http://www.cs.york.ac.uk/fp/smallcheck/) *}
+text {* The example (original in Haskell) was imported with Haskabelle and
+ manually slightly adapted.
+*}
+
+datatype Nat = Zer
+ | Suc Nat
+
+fun sub :: "Nat \<Rightarrow> Nat \<Rightarrow> Nat"
+where
+ "sub x y = (case y of
+ Zer \<Rightarrow> x
+ | Suc y' \<Rightarrow> case x of
+ Zer \<Rightarrow> Zer
+ | Suc x' \<Rightarrow> sub x' y')"
+
+datatype Sym = N0
+ | N1 Sym
+
+datatype RE = Sym Sym
+ | Or RE RE
+ | Seq RE RE
+ | And RE RE
+ | Star RE
+ | Empty
+
+
+function accepts :: "RE \<Rightarrow> Sym list \<Rightarrow> bool" and
+ seqSplit :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
+ seqSplit'' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool" and
+ seqSplit' :: "RE \<Rightarrow> RE \<Rightarrow> Sym list \<Rightarrow> Sym list \<Rightarrow> bool"
+where
+ "accepts re ss = (case re of
+ Sym n \<Rightarrow> case ss of
+ Nil \<Rightarrow> False
+ | (n' # ss') \<Rightarrow> n = n' & List.null ss'
+ | Or re1 re2 \<Rightarrow> accepts re1 ss | accepts re2 ss
+ | Seq re1 re2 \<Rightarrow> seqSplit re1 re2 Nil ss
+ | And re1 re2 \<Rightarrow> accepts re1 ss & accepts re2 ss
+ | Star re' \<Rightarrow> case ss of
+ Nil \<Rightarrow> True
+ | (s # ss') \<Rightarrow> seqSplit re' re [s] ss'
+ | Empty \<Rightarrow> List.null ss)"
+| "seqSplit re1 re2 ss2 ss = (seqSplit'' re1 re2 ss2 ss | seqSplit' re1 re2 ss2 ss)"
+| "seqSplit'' re1 re2 ss2 ss = (accepts re1 ss2 & accepts re2 ss)"
+| "seqSplit' re1 re2 ss2 ss = (case ss of
+ Nil \<Rightarrow> False
+ | (n # ss') \<Rightarrow> seqSplit re1 re2 (ss2 @ [n]) ss')"
+by pat_completeness auto
+
+termination
+ sorry
+
+fun rep :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+ "rep n re = (case n of
+ Zer \<Rightarrow> Empty
+ | Suc n' \<Rightarrow> Seq re (rep n' re))"
+
+
+fun repMax :: "Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+ "repMax n re = (case n of
+ Zer \<Rightarrow> Empty
+ | Suc n' \<Rightarrow> Or (rep n re) (repMax n' re))"
+
+
+fun repInt' :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+ "repInt' n k re = (case k of
+ Zer \<Rightarrow> rep n re
+ | Suc k' \<Rightarrow> Or (rep n re) (repInt' (Suc n) k' re))"
+
+
+fun repInt :: "Nat \<Rightarrow> Nat \<Rightarrow> RE \<Rightarrow> RE"
+where
+ "repInt n k re = repInt' n (sub k n) re"
+
+
+fun prop_regex :: "Nat * Nat * RE * RE * Sym list \<Rightarrow> bool"
+where
+ "prop_regex (n, (k, (p, (q, s)))) = ((accepts (repInt n k (And p q)) s) = (accepts (And (repInt n k p) (repInt n k q)) s))"
+
+
+
+lemma "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
+(*nitpick
+quickcheck[generator = code, iterations = 10000]
+quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[generator = predicate_compile_ff_fs]
+oops*)
+oops
+
+
+setup {* Quickcheck.add_generator ("prolog", Code_Prolog.quickcheck) *}
+
+setup {* Code_Prolog.map_code_options (K
+ {ensure_groundness = true,
+ limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
+ limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
+ (["accepts", "acceptsaux", "acceptsauxauxa", "acceptsauxaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],
+ replacing =
+ [(("repP", "limited_repP"), "lim_repIntPa"),
+ (("subP", "limited_subP"), "repIntP"),
+ (("repIntPa", "limited_repIntPa"), "repIntP"),
+ (("accepts", "limited_accepts"), "quickcheck")],
+ manual_reorder = [],
+ timeout = Time.fromSeconds 10,
+ prolog_system = Code_Prolog.SWI_PROLOG}) *}
+
+text {* Finding the counterexample still seems out of reach for the
+ prolog-style generation. *}
+
+lemma "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
+quickcheck[generator = code, iterations = 100000, expect = counterexample]
+(*quickcheck[generator = predicate_compile_wo_ff]*)
+(*quickcheck[generator = predicate_compile_ff_fs, iterations = 1]*)
+(*quickcheck[generator = prolog, iterations = 1, size = 1]*)
+oops
+
+section {* Given a partial solution *}
+
+lemma
+(* assumes "n = Zer"
+ assumes "k = Suc (Suc Zer)"*)
+ assumes "p = Sym N0"
+ assumes "q = Seq (Sym N0) (Sym N0)"
+(* assumes "s = [N0, N0]"*)
+ shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
+(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1]*)
+quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+oops
+
+section {* Checking the counterexample *}
+
+definition a_sol
+where
+ "a_sol = (Zer, (Suc (Suc Zer), (Sym N0, (Seq (Sym N0) (Sym N0), [N0, N0]))))"
+
+lemma
+ assumes "n = Zer"
+ assumes "k = Suc (Suc Zer)"
+ assumes "p = Sym N0"
+ assumes "q = Seq (Sym N0) (Sym N0)"
+ assumes "s = [N0, N0]"
+ shows "accepts (repInt n k (And p q)) s --> accepts (And (repInt n k p) (repInt n k q)) s"
+(*quickcheck[generator = predicate_compile_wo_ff]*)
+oops
+
+lemma
+ assumes "n = Zer"
+ assumes "k = Suc (Suc Zer)"
+ assumes "p = Sym N0"
+ assumes "q = Seq (Sym N0) (Sym N0)"
+ assumes "s = [N0, N0]"
+ shows "accepts (And (repInt n k p) (repInt n k q)) s --> accepts (repInt n k (And p q)) s"
+(*quickcheck[generator = predicate_compile_wo_ff, iterations = 1, expect = counterexample]*)
+quickcheck[generator = prolog, iterations = 1, size = 1, expect = counterexample]
+oops
+
+lemma
+ assumes "n = Zer"
+ assumes "k = Suc (Suc Zer)"
+ assumes "p = Sym N0"
+ assumes "q = Seq (Sym N0) (Sym N0)"
+ assumes "s = [N0, N0]"
+shows "prop_regex (n, (k, (p, (q, s))))"
+quickcheck[generator = predicate_compile_wo_ff]
+quickcheck[generator = prolog, expect = counterexample]
+oops
+
+lemma "prop_regex a_sol"
+quickcheck[generator = code, expect = counterexample]
+quickcheck[generator = predicate_compile_ff_fs]
+oops
+
+value [code] "prop_regex a_sol"
+
+
+end
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Sep 07 12:04:34 2010 +0200
@@ -13,6 +13,7 @@
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
manual_reorder : ((string * int) * int list) list,
+ timeout : Time.time,
prolog_system : prolog_system}
val code_options_of : theory -> code_options
val map_code_options : (code_options -> code_options) -> theory -> theory
@@ -32,7 +33,7 @@
val generate : bool -> Proof.context -> string -> (logic_program * constant_table)
val write_program : logic_program -> string
- val run : prolog_system -> logic_program -> string -> string list -> int option -> prol_term list list
+ val run : (Time.time * prolog_system) -> logic_program -> string -> string list -> int option -> prol_term list list
val quickcheck : Proof.context -> bool -> term -> int -> term list option * (bool list * bool)
@@ -60,6 +61,7 @@
limited_predicates : (string list * int) list,
replacing : ((string * string) * string) list,
manual_reorder : ((string * int) * int list) list,
+ timeout : Time.time,
prolog_system : prolog_system}
structure Options = Theory_Data
@@ -67,20 +69,21 @@
type T = code_options
val empty = {ensure_groundness = false,
limited_types = [], limited_predicates = [], replacing = [], manual_reorder = [],
- prolog_system = SWI_PROLOG}
+ timeout = Time.fromSeconds 10, prolog_system = SWI_PROLOG}
val extend = I;
fun merge
({ensure_groundness = ensure_groundness1, limited_types = limited_types1,
limited_predicates = limited_predicates1, replacing = replacing1,
- manual_reorder = manual_reorder1, prolog_system = prolog_system1},
+ manual_reorder = manual_reorder1, timeout = timeout1, prolog_system = prolog_system1},
{ensure_groundness = ensure_groundness2, limited_types = limited_types2,
limited_predicates = limited_predicates2, replacing = replacing2,
- manual_reorder = manual_reorder2, prolog_system = prolog_system2}) =
+ manual_reorder = manual_reorder2, timeout = timeout2, prolog_system = prolog_system2}) =
{ensure_groundness = ensure_groundness1 orelse ensure_groundness2,
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),
replacing = Library.merge (op =) (replacing1, replacing2),
+ timeout = timeout1,
prolog_system = prolog_system1};
);
@@ -309,6 +312,11 @@
fst (extend' key (G, []))
end
+fun print_intros ctxt gr consts =
+ tracing (cat_lines (map (fn const =>
+ "Constant " ^ const ^ "has intros:\n" ^
+ cat_lines (map (Display.string_of_thm ctxt) (Graph.get_node gr const))) consts))
+
fun generate ensure_groundness ctxt const =
let
fun strong_conn_of gr keys =
@@ -316,6 +324,7 @@
val gr = Predicate_Compile_Core.intros_graph_of ctxt
val gr' = add_edges depending_preds_of const gr
val scc = strong_conn_of gr' [const]
+ val _ = print_intros ctxt gr (flat scc)
val constant_table = declare_consts (flat scc) []
in
apfst flat (fold_map (translate_intros ensure_groundness ctxt gr) (flat scc) constant_table)
@@ -628,7 +637,7 @@
(* calling external interpreter and getting results *)
-fun run system p query_rel vnames nsols =
+fun run (timeout, system) p query_rel vnames nsols =
let
val p' = rename_vars_program p
val _ = tracing "Renaming variable names..."
@@ -636,8 +645,8 @@
val vnames' = map (fn v => the (AList.lookup (op =) renaming v)) vnames
val prog = prelude system ^ query system nsols query_rel vnames' ^ write_program p'
val _ = tracing ("Generated prolog program:\n" ^ prog)
- val solution = Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
- (File.write prolog_file prog; invoke system (Path.implode prolog_file)))
+ val solution = TimeLimit.timeLimit timeout (fn prog => Cache_IO.with_tmp_file "prolog_file" (fn prolog_file =>
+ (File.write prolog_file prog; invoke system (Path.implode prolog_file)))) prog
val _ = tracing ("Prolog returned solution(s):\n" ^ solution)
val tss = parse_solutions solution
in
@@ -721,7 +730,7 @@
|> apfst (fold replace (#replacing options))
|> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
- val tss = run (#prolog_system options)
+ val tss = run (#timeout options, #prolog_system options)
p (translate_const constant_table name) (map first_upper vnames) soln
val _ = tracing "Restoring terms..."
val empty = Const("Orderings.bot_class.bot", fastype_of t_compr)
@@ -817,7 +826,7 @@
|> apfst (fold replace (#replacing options))
|> apfst (reorder_manually (#manual_reorder options))
val _ = tracing "Running prolog program..."
- val tss = run (#prolog_system options)
+ val tss = run (#timeout options, #prolog_system options)
p (translate_const constant_table full_constname) (map fst vs') (SOME 1)
val _ = tracing "Restoring terms..."
val res =
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Tue Sep 07 12:04:34 2010 +0200
@@ -222,10 +222,11 @@
fold_rev (fn m1 => fn m2 => map_product (curry Fun) m1 m2)
(map all_modes_of_typ' S) [Bool]
else
- [Input, Output]
+ raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
end
| all_modes_of_typ @{typ bool} = [Bool]
- | all_modes_of_typ T = all_modes_of_typ' T
+ | all_modes_of_typ T =
+ raise Fail "Invocation of all_modes_of_typ with a non-predicate type"
fun all_smodes_of_typ (T as Type ("fun", _)) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 07 12:04:18 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Tue Sep 07 12:04:34 2010 +0200
@@ -164,8 +164,8 @@
| mode_of (Term m) = m
| mode_of (Mode_App (d1, d2)) =
(case mode_of d1 of Fun (m, m') =>
- (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of")
- | _ => raise Fail "mode_of2")
+ (if eq_mode (m, mode_of d2) then m' else raise Fail "mode_of: derivation has mismatching modes")
+ | _ => raise Fail "mode_of: derivation has a non-functional mode")
| mode_of (Mode_Pair (d1, d2)) =
Pair (mode_of d1, mode_of d2)
@@ -1123,9 +1123,13 @@
raise Fail "all_input_of: not a predicate"
end
-fun partial_hd [] = NONE
- | partial_hd (x :: xs) = SOME x
-
+fun find_least ord xs =
+ let
+ fun find' x y = (case y of NONE => SOME x | SOME y' => if ord (x, y') = LESS then SOME x else y)
+ in
+ fold find' xs NONE
+ end
+
fun term_vs tm = fold_aterms (fn Free (x, T) => cons x | _ => I) tm [];
val terms_vs = distinct (op =) o maps term_vs;
@@ -1268,11 +1272,11 @@
case mode_of d1 of
Fun (m', _) => map (fn (d2, mvars2) =>
(Mode_App (d1, d2), union (op =) mvars1 mvars2)) (derivations_of ctxt modes vs t2 m')
- | _ => raise Fail "Something went wrong") derivs1
+ | _ => raise Fail "all_derivations_of: derivation has an unexpected non-functional mode") derivs1
end
| all_derivations_of _ modes vs (Const (s, T)) = the (lookup_mode modes (Const (s, T)))
| all_derivations_of _ modes vs (Free (x, T)) = the (lookup_mode modes (Free (x, T)))
- | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of"
+ | all_derivations_of _ modes vs _ = raise Fail "all_derivations_of: unexpected term"
fun rev_option_ord ord (NONE, NONE) = EQUAL
| rev_option_ord ord (NONE, SOME _) = GREATER
@@ -1362,17 +1366,16 @@
fun select_mode_prem (mode_analysis_options : mode_analysis_options) (ctxt : Proof.context) pred
pol (modes, (pos_modes, neg_modes)) vs ps =
let
- fun choose_mode_of_prem (Prem t) = partial_hd
- (sort (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t))
+ fun choose_mode_of_prem (Prem t) =
+ find_least (deriv_ord ctxt pol pred modes t) (all_derivations_of ctxt pos_modes vs t)
| choose_mode_of_prem (Sidecond t) = SOME (Context Bool, missing_vars vs t)
- | choose_mode_of_prem (Negprem t) = partial_hd
- (sort (deriv_ord ctxt (not pol) pred modes t)
+ | choose_mode_of_prem (Negprem t) = find_least (deriv_ord ctxt (not pol) pred modes t)
(filter (fn (d, missing_vars) => is_all_input (head_mode_of d))
- (all_derivations_of ctxt neg_modes vs t)))
- | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: " ^ string_of_prem ctxt p)
+ (all_derivations_of ctxt neg_modes vs t))
+ | choose_mode_of_prem p = raise Fail ("choose_mode_of_prem: unexpected premise " ^ string_of_prem ctxt p)
in
if #reorder_premises mode_analysis_options then
- partial_hd (sort (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps))
+ find_least (premise_ord ctxt pol pred modes) (ps ~~ map choose_mode_of_prem ps)
else
SOME (hd ps, choose_mode_of_prem (hd ps))
end
@@ -1398,7 +1401,7 @@
Prem t => union (op =) vs (term_vs t)
| Sidecond t => union (op =) vs (term_vs t)
| Negprem t => union (op =) vs (term_vs t)
- | _ => raise Fail "I do not know")
+ | _ => raise Fail "unexpected premise")
fun check_mode_prems acc_ps rnd vs [] = SOME (acc_ps, vs, rnd)
| check_mode_prems acc_ps rnd vs ps =
(case
@@ -2303,9 +2306,10 @@
if (is_constructor thy t) then let
val case_rewrites = (#case_rewrites (Datatype.the_info thy
((fst o dest_Type o fastype_of) t)))
- in case_rewrites @ maps get_case_rewrite (snd (strip_comb t)) end
+ in fold (union Thm.eq_thm) (case_rewrites :: map get_case_rewrite (snd (strip_comb t))) [] end
else []
- val simprules = @{thm "unit.cases"} :: @{thm "prod.cases"} :: maps get_case_rewrite out_ts
+ val simprules = insert Thm.eq_thm @{thm "unit.cases"} (insert Thm.eq_thm @{thm "prod.cases"}
+ (fold (union Thm.eq_thm) (map get_case_rewrite out_ts) []))
(* replace TRY by determining if it necessary - are there equations when calling compile match? *)
in
(* make this simpset better! *)