378 $ Abs (x, T, t) |
378 $ Abs (x, T, t) |
379 | enclose (@{const_name All}, (x, T)) t = |
379 | enclose (@{const_name All}, (x, T)) t = |
380 Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property}) |
380 Const (@{const_name Quickcheck_Narrowing.all}, (T --> @{typ property}) --> @{typ property}) |
381 $ Abs (x, T, t) |
381 $ Abs (x, T, t) |
382 in |
382 in |
383 fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ |
383 fold_rev enclose qs (@{term Quickcheck_Narrowing.Property} $ t) |
384 (list_comb (t , map Bound (((length qs) - 1) downto 0)))) |
|
385 end |
384 end |
386 |
385 |
387 fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = |
386 fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = |
388 Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => |
387 Datatype.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => |
389 (t, mk_case_term ctxt (p - 1) qs' c)) cs) |
388 (t, mk_case_term ctxt (p - 1) qs' c)) cs) |
413 fun wrap f (qs, t) = |
412 fun wrap f (qs, t) = |
414 let val (qs1, qs2) = split_list qs in |
413 let val (qs1, qs2) = split_list qs in |
415 apfst (map2 pair qs1) (f (qs2, t)) end |
414 apfst (map2 pair qs1) (f (qs2, t)) end |
416 val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I |
415 val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I |
417 val (qs, prop_t) = finitize (strip_quantifiers pnf_t) |
416 val (qs, prop_t) = finitize (strip_quantifiers pnf_t) |
418 val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t |
|
419 (* FIXME proper naming convention for local_theory *) |
|
420 val ((prop_def, _), ctxt') = |
|
421 Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn), |
|
422 ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt |
|
423 val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt') |
|
424 val (counterexample, result) = dynamic_value_strict (true, opts) |
417 val (counterexample, result) = dynamic_value_strict (true, opts) |
425 (Existential_Counterexample.get, Existential_Counterexample.put, |
418 (Existential_Counterexample.get, Existential_Counterexample.put, |
426 "Narrowing_Generators.put_existential_counterexample") |
419 "Narrowing_Generators.put_existential_counterexample") |
427 thy' (apfst o Option.map o map_counterexample) (mk_property qs prop_def') |
420 thy (apfst o Option.map o map_counterexample) (mk_property qs prop_t) |
428 in |
421 in |
429 Quickcheck.Result |
422 Quickcheck.Result |
430 {counterexample = Option.map (mk_terms ctxt' qs) counterexample, |
423 {counterexample = Option.map (mk_terms ctxt qs) counterexample, |
431 evaluation_terms = Option.map (K []) counterexample, |
424 evaluation_terms = Option.map (K []) counterexample, |
432 timings = #timings (dest_result result), reports = #reports (dest_result result)} |
425 timings = #timings (dest_result result), reports = #reports (dest_result result)} |
433 end |
426 end |
434 else |
427 else |
435 let |
428 let |