# HG changeset patch # User bulwahn # Date 1292431605 -3600 # Node ID ede546773fd6877ae7eeb741a373b3396d65a5b5 # Parent 95167879f67526b78d461d8575bce6a923eae50d adding postprocessing for sets in term construction of quickcheck diff -r 95167879f675 -r ede546773fd6 src/HOL/Tools/smallvalue_generators.ML --- a/src/HOL/Tools/smallvalue_generators.ML Wed Dec 15 17:14:44 2010 +0100 +++ b/src/HOL/Tools/smallvalue_generators.ML Wed Dec 15 17:46:45 2010 +0100 @@ -280,6 +280,28 @@ $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end +fun make_set T1 [] = Const (@{const_abbrev Set.empty}, T1 --> @{typ bool}) + | make_set T1 ((t1, @{const False}) :: tps) = make_set T1 tps + | make_set T1 ((t1, @{const True}) :: tps) = insert_const t1 (make_set T1 tps) + | make_set T1 ((t1, _) :: tps) = raise TERM ("make_set", [t]) + +fun dest_fun_upd (Const (@{const_name fun_upd}, _) $ t0 $ t1 $ t2) = (t0, (t1, t2)) + | dest_fun_upd t = raise TERM ("dest_fun_upd", [t]) + +fun dest_plain_fun t = + case try (dest_fun_upd t) of + NONE => + case t of + (Abs (_, _, Const (@{const_name HOL.undefined}, _))) => [] + | _ => raise TERM ("dest_plain_fun", [t]) + | SOME (t0, (t1, t2)) => (t1, t2) :: dest_plain_fun t0 + +fun post_process_term t = + case fastype_of t of + Type (@{type_name fun}, [T1, @{typ bool}]) => + dest_plain_fun t |> map (pairself post_process_term) |> make_set + | _ => t + fun compile_generator_expr ctxt t = let val thy = ProofContext.theory_of ctxt @@ -289,7 +311,9 @@ val compile = Code_Runtime.dynamic_value_strict (Counterexample.get, put_counterexample, "Smallvalue_Generators.put_counterexample") thy (SOME target) (fn proc => fn g => g #> (Option.map o map) proc) t' []; - in fn size => rpair NONE (compile size) end; + in + fn size => rpair NONE (compile size |> Option.map post_process_term) + end; (** setup **)