src/HOL/Tools/Quickcheck/narrowing_generators.ML

       thy
   end;
 
 (* testing framework *)
 
-val target = "Haskell"
+val target = "Haskell_Quickcheck"
 
 (** invocation of Haskell interpreter **)
 
 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
 val pnf_narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/PNF_Narrowing_Engine.hs")

   let
     val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ()))
     val _ = Isabelle_System.mkdirs path;
   in Exn.release (Exn.capture f path) end;
   
-fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
-  let
-    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
+fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
+  let
+    fun message s = if quiet then () else Output.urgent_message s
     val tmp_prefix = "Quickcheck_Narrowing"
     val with_tmp_dir =
       if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
     fun run in_path = 
       let

         val cmd = "exec \"$ISABELLE_GHC\" -fglasgow-exts " ^
           (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
           " -o " ^ executable ^ ";"
         val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
         fun with_size k =
-          if k > Config.get ctxt Quickcheck.size then
+          if k > size then
             NONE
           else
             let
               val _ = message ("Test data size: " ^ string_of_int k)
               val (response, _) = bash_output (executable ^ " " ^ string_of_int k)

                |> Context.proof_map (exec false ml_code);
            in get ctxt' () end     
       end
   in with_tmp_dir tmp_prefix run end;
 
-fun dynamic_value_strict contains_existentials cookie thy postproc t =
+fun dynamic_value_strict opts cookie thy postproc t =
   let
     val ctxt = Proof_Context.init_global thy
-    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
+    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
       (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
   in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
 
 (** counterexample generator **)
   

       map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps
     end
   
 fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
   let
+    val opts = (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
     val thy = Proof_Context.theory_of ctxt
     val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
     val pnf_t = make_pnf_term thy t'
   in
     if Config.get ctxt allow_existentials andalso contains_existentials pnf_t then

         val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
         val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
         val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
           ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
         val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
-        val result = dynamic_value_strict true
+        val result = dynamic_value_strict (true, opts)
           (Existential_Counterexample.get, Existential_Counterexample.put,
             "Narrowing_Generators.put_existential_counterexample")
           thy' (Option.map o map_counterexample) (mk_property qs prop_def')
         val result' = Option.map (mk_terms ctxt' (fst (strip_quantifiers pnf_t))) result
       in

         val t' = Term.list_abs_free (Term.add_frees t [], t)
         fun wrap f t = list_abs (f (strip_abs t))
         val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
         fun ensure_testable t =
           Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
-        val result = dynamic_value_strict false
+        val result = dynamic_value_strict (false, opts)
           (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
           thy (Option.map o map) (ensure_testable (finitize t'))
       in
         Quickcheck.Result {counterexample = Option.map ((curry (op ~~)) (Term.add_free_names t [])) result,
           evaluation_terms = Option.map (K []) result, timings = [], reports = []}