src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42019 a9445d87bc3e
parent 41963 d8c3b26b3da4
child 42020 2da02764d523
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 12:05:23 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -118,7 +118,7 @@
     1.4  fun exec verbose code =
     1.5    ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
     1.6  
     1.7 -fun value ctxt (get, put, put_ml) (code, value) =
     1.8 +fun value ctxt (get, put, put_ml) (code, value) size =
     1.9    let
    1.10      val tmp_prefix = "Quickcheck_Narrowing"
    1.11      fun run in_path = 
    1.12 @@ -129,7 +129,7 @@
    1.13          val main = "module Main where {\n\n" ^
    1.14            "import Narrowing_Engine;\n" ^
    1.15            "import Code;\n\n" ^
    1.16 -          "main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^
    1.17 +          "main = Narrowing_Engine.smallCheck " ^ string_of_int size ^ " (Code.value ())\n\n" ^
    1.18            "}\n"
    1.19          val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
    1.20            (unprefix "module Code where {" code)
    1.21 @@ -154,18 +154,18 @@
    1.22        |> Context.proof_map (exec false ml_code);
    1.23    in get ctxt' () end;
    1.24  
    1.25 -fun evaluation cookie thy evaluator vs_t args =
    1.26 +fun evaluation cookie thy evaluator vs_t args size =
    1.27    let
    1.28      val ctxt = ProofContext.init_global thy;
    1.29      val (program_code, value_name) = evaluator vs_t;
    1.30      val value_code = space_implode " "
    1.31        (value_name :: "()" :: map (enclose "(" ")") args);
    1.32 -  in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
    1.33 +  in Exn.interruptible_capture (value ctxt cookie (program_code, value_code)) size end;
    1.34  
    1.35 -fun dynamic_value_strict cookie thy postproc t args =
    1.36 +fun dynamic_value_strict cookie thy postproc t args size =
    1.37    let
    1.38      fun evaluator naming program ((_, vs_ty), t) deps =
    1.39 -      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args;
    1.40 +      evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args size;
    1.41    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    1.42  
    1.43  (* counterexample generator *)
    1.44 @@ -185,7 +185,7 @@
    1.45        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.46      val t = dynamic_value_strict
    1.47        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.48 -      thy (Option.map o map) (ensure_testable t) []
    1.49 +      thy (Option.map o map) (ensure_testable t) [] size
    1.50    in
    1.51      (t, NONE)
    1.52    end;