adapting manual configuration in examples
authorbulwahn
Thu, 30 Sep 2010 10:48:12 +0200
changeset 39800 17e29ddd538e
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
--- 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 = [],
--- 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")],
--- 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"),
--- 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 =
--- 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)],