src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42023 1bd4b6d1c482
parent 42020 2da02764d523
child 42024 51df23535105
     1.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML	Fri Mar 18 18:19:42 2011 +0100
     1.3 @@ -9,12 +9,19 @@
     1.4    val compile_generator_expr:
     1.5      Proof.context -> term -> int -> term list option * Quickcheck.report option
     1.6    val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
     1.7 +  val finite_functions : bool Config.T
     1.8    val setup: theory -> theory
     1.9  end;
    1.10  
    1.11  structure Narrowing_Generators : NARROWING_GENERATORS =
    1.12  struct
    1.13  
    1.14 +(* configurations *)
    1.15 +
    1.16 +val (finite_functions, setup_finite_functions) =
    1.17 +  Attrib.config_bool "quickcheck_finite_functions" (K true)
    1.18 +
    1.19 +
    1.20  fun mk_undefined T = Const(@{const_name undefined}, T)
    1.21  
    1.22  (* narrowing specific names and types *)
    1.23 @@ -178,23 +185,27 @@
    1.24  )
    1.25  
    1.26  val put_counterexample =  Counterexample.put
    1.27 -  
    1.28 +
    1.29 +fun finitize_functions t = t
    1.30 +
    1.31  fun compile_generator_expr ctxt t size =
    1.32    let
    1.33      val thy = ProofContext.theory_of ctxt
    1.34 +    val t' = if Config.get ctxt finite_functions then finitize_functions t else t
    1.35      fun ensure_testable t =
    1.36        Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
    1.37 -    val t = dynamic_value_strict
    1.38 +    val result = dynamic_value_strict
    1.39        (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
    1.40 -      thy (Option.map o map) (ensure_testable t) [] size
    1.41 +      thy (Option.map o map) (ensure_testable t') [] size
    1.42    in
    1.43 -    (t, NONE)
    1.44 +    (result, NONE)
    1.45    end;
    1.46  
    1.47  
    1.48  val setup =
    1.49    Datatype.interpretation
    1.50      (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
    1.51 +  #> setup_finite_functions
    1.52    #> Context.theory_map
    1.53      (Quickcheck.add_generator ("narrowing", compile_generator_expr))
    1.54