src/HOL/Tools/smallvalue_generators.ML
changeset 40911 7febf76e0a69
parent 40907 45ba9f05583a
child 40913 99a4ef20704d
     1.1 --- a/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.2 +++ b/src/HOL/Tools/smallvalue_generators.ML	Fri Dec 03 08:40:47 2010 +0100
     1.3 @@ -7,7 +7,7 @@
     1.4  signature SMALLVALUE_GENERATORS =
     1.5  sig
     1.6    val compile_generator_expr:
     1.7 -    Proof.context -> term -> int -> term list option * (bool list * bool)
     1.8 +    Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.9    val put_counterexample: (unit -> int -> term list option)
    1.10      -> Proof.context -> Proof.context
    1.11    val smart_quantifier : bool Config.T;
    1.12 @@ -272,19 +272,15 @@
    1.13    in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end
    1.14  
    1.15  fun compile_generator_expr ctxt t =
    1.16 -  if Config.get ctxt Quickcheck.report then
    1.17 -    error "Compilation with reporting facility is not supported"
    1.18 -  else
    1.19 -    let
    1.20 -      val thy = ProofContext.theory_of ctxt
    1.21 -      val t' =
    1.22 -        (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
    1.23 -          ctxt t;
    1.24 -      val compile = Code_Runtime.dynamic_value_strict
    1.25 -        (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
    1.26 -        thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    1.27 -      val dummy_report = ([], false)
    1.28 -    in compile #> rpair dummy_report end;
    1.29 +  let
    1.30 +    val thy = ProofContext.theory_of ctxt
    1.31 +    val t' =
    1.32 +      (if Config.get ctxt smart_quantifier then mk_smart_generator_expr else mk_generator_expr)
    1.33 +        ctxt t;
    1.34 +    val compile = Code_Runtime.dynamic_value_strict
    1.35 +      (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample")
    1.36 +      thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' [];
    1.37 +  in fn size => rpair NONE (compile size) end;
    1.38  
    1.39  (** setup **)
    1.40