# HG changeset patch # User bulwahn # Date 1285836492 -7200 # Node ID 17e29ddd538e822ad12d352069a93871e68ef55c # Parent fdbea66eae4bd3ad46e678e4179e4c8d222225e3 adapting manual configuration in examples diff -r fdbea66eae4b -r 17e29ddd538e src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 10:48:12 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy Thu Sep 30 10:48:12 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 = [], diff -r fdbea66eae4b -r 17e29ddd538e src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 30 10:48:12 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy Thu Sep 30 10:48:12 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")], diff -r fdbea66eae4b -r 17e29ddd538e src/HOL/Predicate_Compile_Examples/Lambda_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 10:48:12 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy Thu Sep 30 10:48:12 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"), diff -r fdbea66eae4b -r 17e29ddd538e src/HOL/Predicate_Compile_Examples/List_Examples.thy --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 10:48:12 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy Thu Sep 30 10:48:12 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 = diff -r fdbea66eae4b -r 17e29ddd538e src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 10:48:12 2010 +0200 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy Thu Sep 30 10:48:12 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)],