# HG changeset patch # User bulwahn # Date 1283260916 -7200 # Node ID b5d126d7be4b07c4b6f021f1582613f39240eed3 # Parent 3917c2acaec478d85bf33ee8f7346f3f4536eb38 adapting and tuning example theories diff -r 3917c2acaec4 -r b5d126d7be4b src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:07:51 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Tue Aug 31 15:21:56 2010 +0200 @@ -10,8 +10,12 @@ "append [] ys ys" | "append xs ys zs ==> append (x # xs) ys (x # zs)" -setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = false, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} values "{(x, y, z). append x y z}" @@ -20,14 +24,20 @@ setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.YAP}) *} values "{(x, y, z). append x y z}" setup {* Code_Prolog.map_code_options (K {ensure_groundness = false, - limited_types = [], limited_predicates = [], replacing = [], + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} @@ -191,11 +201,13 @@ where "y \ B \ notB y" -setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, - limited_types = [], - limited_predicates = [], - replacing = [], - prolog_system = Code_Prolog.SWI_PROLOG}) *} +setup {* Code_Prolog.map_code_options (K + {ensure_groundness = true, + limited_types = [], + limited_predicates = [], + replacing = [], + manual_reorder = [], + prolog_system = Code_Prolog.SWI_PROLOG}) *} values 2 "{y. notB y}" diff -r 3917c2acaec4 -r b5d126d7be4b src/HOL/Predicate_Compile_Examples/Hotel_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 31 15:07:51 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Hotel_Example.thy Tue Aug 31 15:21:56 2010 +0200 @@ -89,6 +89,7 @@ limited_types = [], limited_predicates = [], replacing = [], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} values 40 "{s. hotel s}" @@ -115,8 +116,9 @@ setup {* Code_Prolog.map_code_options (K {ensure_groundness = true, limited_types = [], - limited_predicates = [("hotel", 5)], + limited_predicates = [(["hotel"], 5)], replacing = [(("hotel", "limited_hotel"), "quickcheck")], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} lemma diff -r 3917c2acaec4 -r b5d126d7be4b src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Aug 31 15:07:51 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Tue Aug 31 15:21:56 2010 +0200 @@ -84,9 +84,10 @@ setup {* Code_Prolog.map_code_options (K { ensure_groundness = true, limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)], - limited_predicates = [("typing", 2), ("nthel1", 2)], + limited_predicates = [(["typing"], 2), (["nthel1"], 2)], replacing = [(("typing", "limited_typing"), "quickcheck"), (("nthel1", "limited_nthel1"), "lim_typing")], + manual_reorder = [], prolog_system = Code_Prolog.SWI_PROLOG}) *} lemma