adapting manual configuration in examples
authorbulwahn
Thu Sep 30 10:48:12 2010 +0200 (2010-09-30)
changeset 3980017e29ddd538e
parent 39799 fdbea66eae4b
child 39801 3a7e2964c9c0
adapting manual configuration in examples
src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy
src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy
src/HOL/Predicate_Compile_Examples/Lambda_Example.thy
src/HOL/Predicate_Compile_Examples/List_Examples.thy
src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy
     1.1 --- a/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 30 10:48:12 2010 +0200
     1.2 +++ b/src/HOL/Predicate_Compile_Examples/Code_Prolog_Examples.thy	Thu Sep 30 10:48:12 2010 +0200
     1.3 @@ -12,6 +12,7 @@
     1.4  
     1.5  setup {* Code_Prolog.map_code_options (K
     1.6    {ensure_groundness = false,
     1.7 +   limit_globally = NONE,
     1.8     limited_types = [],
     1.9     limited_predicates = [],
    1.10     replacing = [],
    1.11 @@ -25,6 +26,7 @@
    1.12  
    1.13  setup {* Code_Prolog.map_code_options (K
    1.14    {ensure_groundness = false,
    1.15 +   limit_globally = NONE,
    1.16     limited_types = [],
    1.17     limited_predicates = [],
    1.18     replacing = [],
    1.19 @@ -34,6 +36,7 @@
    1.20  
    1.21  setup {* Code_Prolog.map_code_options (K
    1.22    {ensure_groundness = false,
    1.23 +   limit_globally = NONE,
    1.24     limited_types = [],
    1.25     limited_predicates = [],
    1.26     replacing = [],
    1.27 @@ -202,6 +205,7 @@
    1.28  
    1.29  setup {* Code_Prolog.map_code_options (K
    1.30    {ensure_groundness = true,
    1.31 +   limit_globally = NONE,
    1.32     limited_types = [],
    1.33     limited_predicates = [],
    1.34     replacing = [],
     2.1 --- a/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Context_Free_Grammar_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     2.3 @@ -58,6 +58,7 @@
     2.4  
     2.5  setup {* Code_Prolog.map_code_options (K
     2.6    {ensure_groundness = true,
     2.7 +  limit_globally = NONE,
     2.8    limited_types = [],
     2.9    limited_predicates = [(["s1", "a1", "b1"], 2)],
    2.10    replacing = [(("s1", "limited_s1"), "quickcheck")],
    2.11 @@ -81,6 +82,7 @@
    2.12  
    2.13  setup {* Code_Prolog.map_code_options (K
    2.14    {ensure_groundness = true,
    2.15 +  limit_globally = NONE,
    2.16    limited_types = [],
    2.17    limited_predicates = [(["s2", "a2", "b2"], 3)],
    2.18    replacing = [(("s2", "limited_s2"), "quickcheck")],
    2.19 @@ -103,6 +105,7 @@
    2.20  
    2.21  setup {* Code_Prolog.map_code_options (K
    2.22    {ensure_groundness = true,
    2.23 +  limit_globally = NONE,
    2.24    limited_types = [],
    2.25    limited_predicates = [(["s3", "a3", "b3"], 6)],
    2.26    replacing = [(("s3", "limited_s3"), "quickcheck")],
    2.27 @@ -117,6 +120,7 @@
    2.28  (*
    2.29  setup {* Code_Prolog.map_code_options (K
    2.30    {ensure_groundness = true,
    2.31 +  limit_globally = NONE,
    2.32    limited_types = [],
    2.33    limited_predicates = [],
    2.34    replacing = [],
    2.35 @@ -143,6 +147,7 @@
    2.36  
    2.37  setup {* Code_Prolog.map_code_options (K
    2.38    {ensure_groundness = true,
    2.39 +  limit_globally = NONE,
    2.40    limited_types = [],
    2.41    limited_predicates = [(["s4", "a4", "b4"], 6)],
    2.42    replacing = [(("s4", "limited_s4"), "quickcheck")],
     3.1 --- a/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     3.2 +++ b/src/HOL/Predicate_Compile_Examples/Lambda_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     3.3 @@ -83,6 +83,7 @@
     3.4  
     3.5  setup {* Code_Prolog.map_code_options (K 
     3.6    { ensure_groundness = true,
     3.7 +    limit_globally = NONE,
     3.8      limited_types = [(@{typ nat}, 1), (@{typ "type"}, 1), (@{typ dB}, 1), (@{typ "type list"}, 1)],
     3.9      limited_predicates = [(["typing"], 2), (["nthel1"], 2)],
    3.10      replacing = [(("typing", "limited_typing"), "quickcheck"),
     4.1 --- a/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Thu Sep 30 10:48:12 2010 +0200
     4.2 +++ b/src/HOL/Predicate_Compile_Examples/List_Examples.thy	Thu Sep 30 10:48:12 2010 +0200
     4.3 @@ -6,6 +6,7 @@
     4.4  
     4.5  setup {* Code_Prolog.map_code_options (K 
     4.6    {ensure_groundness = true,
     4.7 +   limit_globally = NONE,
     4.8     limited_types = [(@{typ nat}, 2), (@{typ "nat list"}, 4)],
     4.9     limited_predicates = [(["appendP"], 4), (["revP"], 4)],
    4.10     replacing =
     5.1 --- a/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     5.2 +++ b/src/HOL/Predicate_Compile_Examples/Reg_Exp_Example.thy	Thu Sep 30 10:48:12 2010 +0200
     5.3 @@ -100,6 +100,7 @@
     5.4  
     5.5  setup {* Code_Prolog.map_code_options (K 
     5.6    {ensure_groundness = true,
     5.7 +   limit_globally = NONE,
     5.8     limited_types = [(@{typ Sym}, 0), (@{typ "Sym list"}, 2), (@{typ RE}, 6)],
     5.9     limited_predicates = [(["repIntPa"], 2), (["repP"], 2), (["subP"], 0),
    5.10      (["accepts", "acceptsaux", "seqSplit", "seqSplita", "seqSplitaux", "seqSplitb"], 25)],