# HG changeset patch # User bulwahn # Date 1290418918 -3600 # Node ID f1f0e6adca0ae313fd0025b16888f9c0f50e1b8b # Parent 6b137c96df07525ff9434669910ef44c456ac6c9 adding function generation to SmallCheck; activating exhaustive search space testing diff -r 6b137c96df07 -r f1f0e6adca0a src/HOL/Smallcheck.thy --- a/src/HOL/Smallcheck.thy Mon Nov 22 10:41:57 2010 +0100 +++ b/src/HOL/Smallcheck.thy Mon Nov 22 10:41:58 2010 +0100 @@ -16,7 +16,7 @@ instantiation unit :: small begin -definition "find_first f d = f ()" +definition "small f d = f ()" instance .. @@ -48,6 +48,73 @@ end +section {* full small value generator type classes *} + +class full_small = term_of + +fixes full_small :: "('a * (unit => term) \ term list option) \ code_numeral \ term list option" + +instantiation unit :: full_small +begin + +definition "full_small f d = f (Code_Evaluation.valtermify ())" + +instance .. + +end + +instantiation int :: full_small +begin + +function full_small' :: "(int * (unit => term) => term list option) => int => int => term list option" + where "full_small' f d i = (if d < i then None else (case f (i, %_. Code_Evaluation.term_of i) of Some t => Some t | None => full_small' f d (i + 1)))" +by pat_completeness auto + +termination + by (relation "measure (%(_, d, i). nat (d + 1 - i))") auto + +definition "full_small f d = full_small' f (Code_Numeral.int_of d) (- (Code_Numeral.int_of d))" + +instance .. + +end + +instantiation prod :: (full_small, full_small) full_small +begin +ML {* @{const_name "Pair"} *} +definition + "full_small f d = full_small (%(x, t1). full_small (%(y, t2). f ((x, y), + %u. Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.term_of (Pair :: 'a => 'b => ('a * 'b))) (t1 ())) (t2 ()))) d) d" + +instance .. + +end + +instantiation "fun" :: ("{equal, full_small}", full_small) full_small +begin + +fun full_small_fun' :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => code_numeral => term list option" +where + "full_small_fun' f i d = (if i > 1 then + full_small (%(a, at). full_small (%(b, bt). + full_small_fun' (%(g, gt). f (g(a := b), + (%_. let T1 = (Typerep.typerep (TYPE('a))); T2 = (Typerep.typerep (TYPE('b))) in Code_Evaluation.App (Code_Evaluation.App (Code_Evaluation.App + +(Code_Evaluation.Const (STR ''Fun.fun_upd'') + +(Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''fun'') [T1, T2], Typerep.Typerep (STR ''fun'') [T1, Typerep.Typerep (STR ''fun'') [T2, Typerep.Typerep (STR ''fun'') [T1, T2]]]])) + + (gt ())) (at ())) (bt ())))) (i - 1) d) d) d else (if i > 0 then + full_small (%(b, t). f (%_. b, %_. Code_Evaluation.Abs (STR ''x'') (Typerep.typerep TYPE('a)) (t ()))) d else None))" + +definition full_small_fun :: "(('a => 'b) * (unit => term) => term list option) => code_numeral => term list option" +where + "full_small_fun f d = full_small_fun' f d d" + + +instance .. + +end + subsection {* Defining combinators for any first-order data type *} definition catch_match :: "term list option => term list option => term list option" @@ -59,7 +126,7 @@ use "Tools/smallvalue_generators.ML" -(* We do not activate smallcheck yet. +(* We do not activate smallcheck yet. setup {* Smallvalue_Generators.setup *} *) diff -r 6b137c96df07 -r f1f0e6adca0a src/HOL/Tools/smallvalue_generators.ML --- a/src/HOL/Tools/smallvalue_generators.ML Mon Nov 22 10:41:57 2010 +0100 +++ b/src/HOL/Tools/smallvalue_generators.ML Mon Nov 22 10:41:58 2010 +0100 @@ -6,7 +6,6 @@ signature SMALLVALUE_GENERATORS = sig - val ensure_smallvalue_datatype: Datatype.config -> string list -> theory -> theory val compile_generator_expr: Proof.context -> term -> int -> term list option * (bool list * bool) val put_counterexample: (unit -> int -> term list option) @@ -51,10 +50,12 @@ (** abstract syntax **) +fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit => Code_Evaluation.term"}); + val size = @{term "i :: code_numeral"} val size_pred = @{term "(i :: code_numeral) - 1"} val size_ge_zero = @{term "(i :: code_numeral) > 0"} -fun test_function T = Free ("f", T --> @{typ "term list option"}) +fun test_function T = Free ("f", termifyT T --> @{typ "term list option"}) fun mk_none_continuation (x, y) = let @@ -75,16 +76,23 @@ fun smallT T = (T --> @{typ "Code_Evaluation.term list option"}) --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} +val full_smallN = "full_small"; + +fun full_smallT T = (termifyT T --> @{typ "Code_Evaluation.term list option"}) + --> @{typ code_numeral} --> @{typ "Code_Evaluation.term list option"} + fun mk_equations thy descr vs tycos (names, auxnames) (Ts, Us) = let - val smallsN = map (prefix (smallN ^ "_")) (names @ auxnames); - val smalls = map2 (fn name => fn T => Free (name, smallT T)) + val smallsN = map (prefix (full_smallN ^ "_")) (names @ auxnames); + val smalls = map2 (fn name => fn T => Free (name, full_smallT T)) smallsN (Ts @ Us) fun mk_small_call T = let - val small = Const (@{const_name "Smallcheck.small_class.small"}, smallT T) + val small = Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) in - (T, (fn t => small $ absdummy (T, t) $ size_pred)) + (T, (fn t => small $ + (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) + $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) end fun mk_small_aux_call fTs (k, _) (tyco, Ts) = let @@ -92,14 +100,23 @@ val _ = if not (null fTs) then raise FUNCTION_TYPE else () val small = nth smalls k in - (T, (fn t => small $ absdummy (T, t) $ size_pred)) + (T, (fn t => small $ + (HOLogic.split_const (T, @{typ "unit => Code_Evaluation.term"}, @{typ "Code_Evaluation.term list option"}) + $ absdummy (T, absdummy (@{typ "unit => Code_Evaluation.term"}, t))) $ size_pred)) end fun mk_consexpr simpleT (c, xs) = let val (Ts, fns) = split_list xs val constr = Const (c, Ts ---> simpleT) - val bounds = map Bound (((length xs) - 1) downto 0) - val start_term = test_function simpleT $ (list_comb (constr, bounds)) + val bounds = map (fn x => Bound (2 * x + 1)) (((length xs) - 1) downto 0) + val term_bounds = map (fn x => Bound (2 * x)) (((length xs) - 1) downto 0) + val Eval_App = Const ("Code_Evaluation.App", HOLogic.termT --> HOLogic.termT --> HOLogic.termT) + val Eval_Const = Const ("Code_Evaluation.Const", HOLogic.literalT --> @{typ typerep} --> HOLogic.termT) + val term = fold (fn u => fn t => Eval_App $ t $ (u $ @{term "()"})) + bounds (Eval_Const $ HOLogic.mk_literal c $ HOLogic.mk_typerep (Ts ---> simpleT)) + val start_term = test_function simpleT $ + (HOLogic.pair_const simpleT @{typ "unit => Code_Evaluation.term"} + $ (list_comb (constr, bounds)) $ absdummy (@{typ unit}, term)) in fold_rev (fn f => fn t => f t) fns start_term end fun mk_rhs exprs = @{term "If :: bool => term list option => term list option => term list option"} @@ -129,7 +146,7 @@ PRIMITIVE (Drule.cterm_instantiate [(cert (Var v), rel')]) st' end | _ => Seq.empty; - + fun instantiate_smallvalue_datatype config descr vs tycos prfx (names, auxnames) (Ts, Us) thy = let val _ = Datatype_Aux.message config "Creating smallvalue generators ..."; @@ -155,45 +172,22 @@ Pat_Completeness.pat_completeness_tac ctxt 1 THEN auto_tac (clasimpset_of ctxt) in - thy - |> Class.instantiation (tycos, vs, @{sort small}) + (thy + |> Class.instantiation (tycos, vs, @{sort full_small}) |> Function.add_function (map (fn (T, (name, _)) => - Syntax.no_syn (Binding.conceal (Binding.name name), SOME (smallT T))) eqs) + Syntax.no_syn (Binding.conceal (Binding.name name), SOME (full_smallT T))) eqs) (map (pair (apfst Binding.conceal Attrib.empty_binding) o snd o snd) eqs) Function_Common.default_config pat_completeness_auto |> snd |> Local_Theory.restore |> (fn lthy => Function.prove_termination NONE (termination_tac lthy) lthy) |> snd - |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) - end; - -fun ensure_smallvalue_datatype config raw_tycos thy = - let - val algebra = Sign.classes_of thy; - val (descr, raw_vs, tycos, prfx, (names, auxnames), raw_TUs) = - Datatype.the_descr thy raw_tycos; - val typerep_vs = (map o apsnd) - (curry (Sorts.inter_sort algebra) @{sort typerep}) raw_vs; - val smallvalue_insts = (map (rpair @{sort small}) o flat o maps snd o maps snd) - (Datatype_Aux.interpret_construction descr typerep_vs - { atyp = single, dtyp = (K o K o K) [] }); - (*val term_of_insts = (map (rpair @{sort term_of}) o flat o maps snd o maps snd) - (Datatype_Aux.interpret_construction descr typerep_vs - { atyp = K [], dtyp = K o K });*) - val has_inst = exists (fn tyco => - can (Sorts.mg_domain algebra tyco) @{sort small}) tycos; - in if has_inst then thy - else case Quickcheck_Generators.perhaps_constrain thy smallvalue_insts typerep_vs - of SOME constrain => (instantiate_smallvalue_datatype config descr - (map constrain typerep_vs) tycos prfx (names, auxnames) - ((pairself o map o map_atyps) (fn TFree v => TFree (constrain v)) raw_TUs) thy - handle FUNCTION_TYPE => - (Datatype_Aux.message config - "Creation of smallvalue generators failed because the datatype contains a function type"; - thy)) - | NONE => thy + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac []))) + handle FUNCTION_TYPE => + (Datatype_Aux.message config + "Creation of smallvalue generators failed because the datatype contains a function type"; + thy) end; (** building and compiling generator expressions **) @@ -209,19 +203,20 @@ fun mk_generator_expr thy prop Ts = let val bound_max = length Ts - 1; - val bounds = map Bound (bound_max downto 0) - val result = list_comb (prop, bounds); - val terms = HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of Ts bounds); + val bounds = map_index (fn (i, ty) => + (2 * (bound_max - i) + 1, 2 * (bound_max - i), 2 * i, ty)) Ts; + val result = list_comb (prop, map (fn (i, _, _, _) => Bound i) bounds); + val terms = HOLogic.mk_list @{typ term} (map (fn (_, i, _, _) => Bound i $ @{term "()"}) bounds); val check = @{term "Smallcheck.catch_match :: term list option => term list option => term list option"} $ (@{term "If :: bool => term list option => term list option => term list option"} - $ result $ @{term "None :: term list option"} - $ (@{term "Some :: term list => term list option"} $ terms)) + $ result $ @{term "None :: term list option"} $ (@{term "Some :: term list => term list option"} $ terms)) $ @{term "None :: term list option"}; - fun mk_small_closure (depth, T) t = - Const (@{const_name "Smallcheck.small_class.small"}, smallT T) - $ absdummy (T, t) $ depth - in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure (rev bounds ~~ Ts) check) end + fun mk_small_closure (_, _, i, T) t = + Const (@{const_name "Smallcheck.full_small_class.full_small"}, full_smallT T) + $ (HOLogic.split_const (T, @{typ "unit => term"}, @{typ "term list option"}) + $ absdummy (T, absdummy (@{typ "unit => term"}, t))) $ Bound i + in Abs ("d", @{typ code_numeral}, fold_rev mk_small_closure bounds check) end fun compile_generator_expr ctxt t = let @@ -242,7 +237,8 @@ (** setup **) val setup = - Datatype.interpretation ensure_smallvalue_datatype + Datatype.interpretation + (Quickcheck_Generators.ensure_sort_datatype (@{sort full_small}, instantiate_smallvalue_datatype)) #> Context.theory_map (Quickcheck.add_generator ("small", compile_generator_expr));