# HG changeset patch
# User bulwahn
# Date 1300468782 -3600
# Node ID a9445d87bc3e7d6e0b5a5e30ffaa290252510c3e
# Parent  1d7735ae42737d184d11876010a34891e9e730c3
adding size as static argument in quickcheck_narrowing compilation

diff -r 1d7735ae4273 -r a9445d87bc3e src/HOL/Tools/Quickcheck/narrowing_generators.ML
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 12:05:23 2011 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
@@ -118,7 +118,7 @@
 fun exec verbose code =
   ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
 
-fun value ctxt (get, put, put_ml) (code, value) =
+fun value ctxt (get, put, put_ml) (code, value) size =
   let
     val tmp_prefix = "Quickcheck_Narrowing"
     fun run in_path = 
@@ -129,7 +129,7 @@
         val main = "module Main where {\n\n" ^
           "import Narrowing_Engine;\n" ^
           "import Code;\n\n" ^
-          "main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^
+          "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
           "}\n"
         val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
           (unprefix "module Code where {" code)
@@ -154,18 +154,18 @@
       |> Context.proof_map (exec false ml_code);
   in get ctxt' () end;
 
-fun evaluation cookie thy evaluator vs_t args =
+fun evaluation cookie thy evaluator vs_t args size =
   let
     val ctxt = ProofContext.init_global thy;
     val (program_code, value_name) = evaluator vs_t;
     val value_code = space_implode " "
       (value_name :: "()" :: map (enclose "(" ")") args);
-  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
+  in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
 
-fun dynamic_value_strict cookie thy postproc t args =
+fun dynamic_value_strict cookie thy postproc t args size =
   let
     fun evaluator naming program ((_, vs_ty), t) deps =
-      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args;
+      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
 (* counterexample generator *)
@@ -185,7 +185,7 @@
       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
     val t = dynamic_value_strict
       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
-      thy (Option.map o map) (ensure_testable t) []
+      thy (Option.map o map) (ensure_testable t) [] size
   in
     (t, NONE)
   end;