# HG changeset patch # User nipkow # Date 1283853874 -7200 # Node ID bb93713b09257be21f494f58f118fa25a39eb908 # Parent 35fcab3da1b71c37596cb908856a9171abb5dc46# Parent 720112792ba0361ad85ad4c0667cc1ca51c46f53 merged diff -r 720112792ba0 -r bb93713b0925 src/HOL/IsaMakefile --- 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Library/Fset.thy --- 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 \ A \ B \ B \ (A :: 'a fset)" instance proof diff -r 720112792ba0 -r bb93713b0925 src/HOL/New_DSequence.thy --- 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- 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}" diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- 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}) *} diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/IMP_1.thy --- /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" | + "\ 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/IMP_2.thy --- /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" | + "\ s ==> exec c2 s t ==> exec (IF c1 c2) s t" | + "\ 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/IMP_3.thy --- /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 \ set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec (While b c) s s" | + "s1 \ 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/IMP_4.thy --- /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 \ set b ==> exec c1 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec c2 s t ==> exec (IF b c1 c2) s t" | + "s \ set b ==> exec (While b c) s s" | + "s1 \ 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/List_Examples.thy --- /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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy --- 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 \ height l = 1 + height r \ height r = 1+height l) \ +| "avl (MKT x l r h) = ((height l = height r \ height l = 1 + height r \ height r = 1+height l) \ h = max (height l) (height r) + 1 \ avl l \ avl r)" (* code_pred [inductify] avl . diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Predicate_Compile_Quickcheck_Examples.thy --- 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 *} diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/ROOT.ML --- 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"]; diff -r 720112792ba0 -r bb93713b0925 src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- /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 \ Nat \ Nat" +where + "sub x y = (case y of + Zer \ x + | Suc y' \ case x of + Zer \ Zer + | Suc x' \ 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 \ Sym list \ bool" and + seqSplit :: "RE \ RE \ Sym list \ Sym list \ bool" and + seqSplit'' :: "RE \ RE \ Sym list \ Sym list \ bool" and + seqSplit' :: "RE \ RE \ Sym list \ Sym list \ bool" +where + "accepts re ss = (case re of + Sym n \ case ss of + Nil \ False + | (n' # ss') \ n = n' & List.null ss' + | Or re1 re2 \ accepts re1 ss | accepts re2 ss + | Seq re1 re2 \ seqSplit re1 re2 Nil ss + | And re1 re2 \ accepts re1 ss & accepts re2 ss + | Star re' \ case ss of + Nil \ True + | (s # ss') \ seqSplit re' re [s] ss' + | Empty \ 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 \ False + | (n # ss') \ seqSplit re1 re2 (ss2 @ [n]) ss')" +by pat_completeness auto + +termination + sorry + +fun rep :: "Nat \ RE \ RE" +where + "rep n re = (case n of + Zer \ Empty + | Suc n' \ Seq re (rep n' re))" + + +fun repMax :: "Nat \ RE \ RE" +where + "repMax n re = (case n of + Zer \ Empty + | Suc n' \ Or (rep n re) (repMax n' re))" + + +fun repInt' :: "Nat \ Nat \ RE \ RE" +where + "repInt' n k re = (case k of + Zer \ rep n re + | Suc k' \ Or (rep n re) (repInt' (Suc n) k' re))" + + +fun repInt :: "Nat \ Nat \ RE \ RE" +where + "repInt n k re = repInt' n (sub k n) re" + + +fun prop_regex :: "Nat * Nat * RE * RE * Sym list \ 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Tools/Predicate_Compile/code_prolog.ML --- 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 = diff -r 720112792ba0 -r bb93713b0925 src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 720112792ba0 -r bb93713b0925 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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! *)