src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 43308 fd6cc1378fec
parent 43240 da47097bd589
child 43314 a9090cabca14
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:31:41 2011 +0200
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Thu Jun 09 08:32:13 2011 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  
     1.5  (* testing framework *)
     1.6  
     1.7 -val target = "Haskell"
     1.8 +val target = "Haskell_Quickcheck"
     1.9  
    1.10  (** invocation of Haskell interpreter **)
    1.11  
    1.12 @@ -210,9 +210,9 @@
    1.13      val _ = Isabelle_System.mkdirs path;
    1.14    in Exn.release (Exn.capture f path) end;
    1.15    
    1.16 -fun value contains_existentials ctxt (get, put, put_ml) (code, value_name) =
    1.17 +fun value (contains_existentials, (quiet, size)) ctxt (get, put, put_ml) (code, value_name) =
    1.18    let
    1.19 -    fun message s = if Config.get ctxt Quickcheck.quiet then () else Output.urgent_message s
    1.20 +    fun message s = if quiet then () else Output.urgent_message s
    1.21      val tmp_prefix = "Quickcheck_Narrowing"
    1.22      val with_tmp_dir =
    1.23        if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir 
    1.24 @@ -239,7 +239,7 @@
    1.25            " -o " ^ executable ^ ";"
    1.26          val _ = if bash cmd <> 0 then error "Compilation with GHC failed" else ()
    1.27          fun with_size k =
    1.28 -          if k > Config.get ctxt Quickcheck.size then
    1.29 +          if k > size then
    1.30              NONE
    1.31            else
    1.32              let
    1.33 @@ -264,10 +264,10 @@
    1.34        end
    1.35    in with_tmp_dir tmp_prefix run end;
    1.36  
    1.37 -fun dynamic_value_strict contains_existentials cookie thy postproc t =
    1.38 +fun dynamic_value_strict opts cookie thy postproc t =
    1.39    let
    1.40      val ctxt = Proof_Context.init_global thy
    1.41 -    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value contains_existentials ctxt cookie)
    1.42 +    fun evaluator naming program ((_, vs_ty), t) deps = Exn.interruptible_capture (value opts ctxt cookie)
    1.43        (Code_Target.evaluator thy target naming program deps (vs_ty, t));    
    1.44    in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
    1.45  
    1.46 @@ -373,6 +373,7 @@
    1.47    
    1.48  fun test_term ctxt (limit_time, is_interactive) (t, eval_terms) =
    1.49    let
    1.50 +    val opts = (Config.get ctxt Quickcheck.quiet, Config.get ctxt Quickcheck.size)
    1.51      val thy = Proof_Context.theory_of ctxt
    1.52      val t' = fold_rev (fn (x, T) => fn t => HOLogic.mk_all (x, T, t)) (Term.add_frees t []) t
    1.53      val pnf_t = make_pnf_term thy t'
    1.54 @@ -388,7 +389,7 @@
    1.55          val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
    1.56            ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
    1.57          val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') 
    1.58 -        val result = dynamic_value_strict true
    1.59 +        val result = dynamic_value_strict (true, opts)
    1.60            (Existential_Counterexample.get, Existential_Counterexample.put,
    1.61              "Narrowing_Generators.put_existential_counterexample")
    1.62            thy' (Option.map o map_counterexample) (mk_property qs prop_def')
    1.63 @@ -404,7 +405,7 @@
    1.64          val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
    1.65          fun ensure_testable t =
    1.66            Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.67 -        val result = dynamic_value_strict false
    1.68 +        val result = dynamic_value_strict (false, opts)
    1.69            (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.70            thy (Option.map o map) (ensure_testable (finitize t'))
    1.71        in