src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42023 1bd4b6d1c482
parent 42020 2da02764d523
child 42024 51df23535105
equal deleted inserted replaced
42022:101ce92333f4 42023:1bd4b6d1c482
     7 signature NARROWING_GENERATORS =
     7 signature NARROWING_GENERATORS =
     8 sig
     8 sig
     9   val compile_generator_expr:
     9   val compile_generator_expr:
    10     Proof.context -> term -> int -> term list option * Quickcheck.report option
    10     Proof.context -> term -> int -> term list option * Quickcheck.report option
    11   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
    11   val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
       
    12   val finite_functions : bool Config.T
    12   val setup: theory -> theory
    13   val setup: theory -> theory
    13 end;
    14 end;
    14 
    15 
    15 structure Narrowing_Generators : NARROWING_GENERATORS =
    16 structure Narrowing_Generators : NARROWING_GENERATORS =
    16 struct
    17 struct
       
    18 
       
    19 (* configurations *)
       
    20 
       
    21 val (finite_functions, setup_finite_functions) =
       
    22   Attrib.config_bool "quickcheck_finite_functions" (K true)
       
    23 
    17 
    24 
    18 fun mk_undefined T = Const(@{const_name undefined}, T)
    25 fun mk_undefined T = Const(@{const_name undefined}, T)
    19 
    26 
    20 (* narrowing specific names and types *)
    27 (* narrowing specific names and types *)
    21 
    28 
   176   type T = unit -> term list option
   183   type T = unit -> term list option
   177   fun init _ () = error "Counterexample"
   184   fun init _ () = error "Counterexample"
   178 )
   185 )
   179 
   186 
   180 val put_counterexample =  Counterexample.put
   187 val put_counterexample =  Counterexample.put
   181   
   188 
       
   189 fun finitize_functions t = t
       
   190 
   182 fun compile_generator_expr ctxt t size =
   191 fun compile_generator_expr ctxt t size =
   183   let
   192   let
   184     val thy = ProofContext.theory_of ctxt
   193     val thy = ProofContext.theory_of ctxt
       
   194     val t' = if Config.get ctxt finite_functions then finitize_functions t else t
   185     fun ensure_testable t =
   195     fun ensure_testable t =
   186       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   196       Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
   187     val t = dynamic_value_strict
   197     val result = dynamic_value_strict
   188       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   198       (Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
   189       thy (Option.map o map) (ensure_testable t) [] size
   199       thy (Option.map o map) (ensure_testable t') [] size
   190   in
   200   in
   191     (t, NONE)
   201     (result, NONE)
   192   end;
   202   end;
   193 
   203 
   194 
   204 
   195 val setup =
   205 val setup =
   196   Datatype.interpretation
   206   Datatype.interpretation
   197     (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
   207     (Quickcheck_Common.ensure_sort_datatype (@{sort narrowing}, instantiate_narrowing_datatype))
       
   208   #> setup_finite_functions
   198   #> Context.theory_map
   209   #> Context.theory_map
   199     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   210     (Quickcheck.add_generator ("narrowing", compile_generator_expr))
   200     
   211     
   201 end;
   212 end;