src/HOL/Tools/Quickcheck/narrowing_generators.ML
changeset 42024 51df23535105
parent 42023 1bd4b6d1c482
child 42027 5e40c152c396
     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 @@ -184,9 +184,34 @@
     1.4    fun init _ () = error "Counterexample"
     1.5  )
     1.6  
     1.7 -val put_counterexample =  Counterexample.put
     1.8 +val put_counterexample = Counterexample.put
     1.9  
    1.10 -fun finitize_functions t = t
    1.11 +fun finitize_functions t =
    1.12 +  let
    1.13 +    val ((names, Ts), t') = apfst split_list (strip_abs t)
    1.14 +    fun mk_eval_ffun dT rT =
    1.15 +      Const (@{const_name "Quickcheck_Narrowing.eval_ffun"}, 
    1.16 +        Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT]) --> dT --> rT)
    1.17 +    fun mk_eval_cfun dT rT =
    1.18 +      Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, 
    1.19 +        Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT)
    1.20 +    fun eval_function (T as Type (@{type_name fun}, [dT, rT])) =
    1.21 +      let
    1.22 +        val (rt', rT') = eval_function rT
    1.23 +      in
    1.24 +        case dT of
    1.25 +          Type (@{type_name fun}, _) =>
    1.26 +            (fn t => absdummy (dT, rt' (mk_eval_cfun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    1.27 +            Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT']))
    1.28 +        | _ => (fn t => absdummy (dT, rt' (mk_eval_ffun dT rT' $ incr_boundvars 1 t $ Bound 0)),
    1.29 +            Type (@{type_name "Quickcheck_Narrowing.ffun"}, [dT, rT']))
    1.30 +      end
    1.31 +      | eval_function T = (I, T)
    1.32 +    val (tt, Ts') = split_list (map eval_function Ts)
    1.33 +    val t'' = subst_bounds (map2 (fn f => fn x => f x) (rev tt) (map_index (Bound o fst) Ts), t')
    1.34 +  in
    1.35 +    list_abs (names ~~ Ts', t'')
    1.36 +  end
    1.37  
    1.38  fun compile_generator_expr ctxt t size =
    1.39    let