# HG changeset patch # User haftmann # Date 1244581194 -7200 # Node ID bd2f7211a420fb56ca9d7d4a22704d2f9775d107 # Parent a94aa5f045fb2f8bc4baa09b2c71715b8363e700 first running version of qc generators for datatypes diff -r a94aa5f045fb -r bd2f7211a420 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Tue Jun 09 22:59:53 2009 +0200 +++ b/src/HOL/IsaMakefile Tue Jun 09 22:59:54 2009 +0200 @@ -854,7 +854,7 @@ ex/Lagrange.thy ex/LocaleTest2.thy ex/MT.thy ex/MergeSort.thy \ ex/Meson_Test.thy ex/MonoidGroup.thy ex/Multiquote.thy ex/NatSum.thy \ ex/Numeral.thy ex/PER.thy ex/PresburgerEx.thy ex/Primrec.thy \ - ex/Quickcheck_Examples.thy ex/Quickcheck_Generators.thy ex/ROOT.ML \ + ex/Quickcheck_Examples.thy ex/ROOT.ML \ ex/Recdefs.thy ex/Records.thy ex/ReflectionEx.thy \ ex/Refute_Examples.thy ex/SAT_Examples.thy ex/SVC_Oracle.thy \ ex/Serbian.thy ex/Sqrt.thy ex/Sqrt_Script.thy \ diff -r a94aa5f045fb -r bd2f7211a420 src/HOL/Tools/quickcheck_generators.ML --- a/src/HOL/Tools/quickcheck_generators.ML Tue Jun 09 22:59:53 2009 +0200 +++ b/src/HOL/Tools/quickcheck_generators.ML Tue Jun 09 22:59:54 2009 +0200 @@ -12,6 +12,10 @@ -> seed -> (('a -> 'b) * (unit -> Term.term)) * seed val ensure_random_typecopy: string -> theory -> theory val random_aux_specification: string -> term list -> local_theory -> local_theory + val mk_random_aux_eqs: theory -> DatatypeAux.descr -> (string * sort) list + -> typ list -> typ list -> string list -> string list + -> string * (term list * (term * term) list) + val ensure_random_datatype: string list -> theory -> theory val eval_ref: (unit -> int -> int * int -> term list option * (int * int)) option ref val setup: theory -> theory end; @@ -208,19 +212,19 @@ fun random_aux_specification prefix eqs lthy = let - val _ $ Free (v, _) $ Free (w, _) = - (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o hd) eqs; + val vs = fold Term.add_free_names ((snd o strip_comb o fst o HOLogic.dest_eq + o HOLogic.dest_Trueprop o hd) eqs) []; fun mk_proto_eq eq = let - val (head $ arg, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; - in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda arg rhs)) end; + val (head $ t $ u, rhs) = (HOLogic.dest_eq o HOLogic.dest_Trueprop) eq; + in ((HOLogic.mk_Trueprop o HOLogic.mk_eq) (head, lambda t (lambda u rhs))) end; val proto_eqs = map mk_proto_eq eqs; fun prove_simps proto_simps lthy = let - val ext_simps = map (fn thm => fun_cong OF [thm]) proto_simps; + val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps; val tac = ALLGOALS Goal.conjunction_tac THEN ALLGOALS (ProofContext.fact_tac ext_simps); - in (Goal.prove_multi lthy [v, w] [] eqs (K tac), lthy) end; + in (Goal.prove_multi lthy vs [] eqs (K tac), lthy) end; val b = Binding.qualify true prefix (Binding.name "simps"); in lthy @@ -236,13 +240,141 @@ (* constructing random instances on datatypes *) -(*still under construction*) +fun mk_random_aux_eqs thy descr vs Ts rtyps tycos names = + let + val mk_const = curry (Sign.mk_const thy); + val i = @{term "i\code_numeral"}; + val i1 = @{term "(i\code_numeral) - 1"}; + val j = @{term "j\code_numeral"}; + val seed = @{term "s\Random.seed"}; + val random_auxN = "random_aux"; + val random_auxsN = map (prefix (random_auxN ^ "_")) + (map Long_Name.base_name names @ map DatatypeAux.name_of_typ rtyps); + fun termifyT T = HOLogic.mk_prodT (T, @{typ "unit \ term"}); + val rTs = Ts @ rtyps; + fun random_resultT T = @{typ Random.seed} + --> HOLogic.mk_prodT (termifyT T,@{typ Random.seed}); + val pTs = map random_resultT rTs; + fun sizeT T = @{typ code_numeral} --> @{typ code_numeral} --> T; + val random_auxT = sizeT o random_resultT; + val random_auxs = map2 (fn s => fn rT => Free (s, random_auxT rT)) + random_auxsN rTs; + fun mk_random_call T = (NONE, (HOLogic.mk_random T j, T)); + fun mk_random_aux_call T = + let + val k = find_index (fn T' => T = T') rTs; + val random = nth random_auxs k; + val size = Option.map snd (DatatypeCodegen.find_shortest_path descr k) + |> the_default 0; + in (SOME size, (random $ i1 $ j, T)) end; + fun atom T = mk_random_call T; + fun dtyp tyco = mk_random_aux_call (Type (tyco, map TFree vs)); + fun rtyp (tyco, Ts) _ = mk_random_aux_call (Type (tyco, Ts)); + val (tss1, tss2) = DatatypePackage.construction_interpretation thy + {atom = atom, dtyp = dtyp, rtyp = rtyp} vs tycos; + fun mk_consexpr simpleT (c, xs) = + let + val (ks, simple_tTs) = split_list xs; + val T = termifyT simpleT; + val tTs = (map o apsnd) termifyT simple_tTs; + val is_rec = exists is_some ks; + val k = fold (fn NONE => I | SOME k => curry Int.max k) ks 0; + val vs = Name.names Name.context "x" (map snd simple_tTs); + val vs' = (map o apsnd) termifyT vs; + val tc = HOLogic.mk_return T @{typ Random.seed} + (HOLogic.mk_valtermify_app c vs simpleT); + val t = HOLogic.mk_ST (map (fn (t, _) => (t, @{typ Random.seed})) tTs ~~ map SOME vs') + tc @{typ Random.seed} (SOME T, @{typ Random.seed}); + val tk = if is_rec + then if k = 0 then i + else @{term "Quickcheck.beyond :: code_numeral \ code_numeral \ code_numeral"} + $ HOLogic.mk_number @{typ code_numeral} k $ i + else @{term "1::code_numeral"} + in (is_rec, HOLogic.mk_prod (tk, t)) end; + fun sort_rec xs = + map_filter (fn (true, t) => SOME t | _ => NONE) xs + @ map_filter (fn (false, t) => SOME t | _ => NONE) xs; + val gen_exprss = (map o apfst) (fn tyco => Type (tyco, map TFree vs)) tss1 + @ (map o apfst) Type tss2 + |> map (fn (T, cs) => (T, (sort_rec o map (mk_consexpr T)) cs)); + fun mk_select (rT, xs) = + mk_const @{const_name Quickcheck.collapse} [@{typ "Random.seed"}, termifyT rT] + $ (mk_const @{const_name Random.select_weight} [random_resultT rT] + $ HOLogic.mk_list (HOLogic.mk_prodT (@{typ code_numeral}, random_resultT rT)) xs) + $ seed; + val auxs_lhss = map (fn t => t $ i $ j $ seed) random_auxs; + val auxs_rhss = map mk_select gen_exprss; + val prefix = space_implode "_" (random_auxN :: names); + in (prefix, (random_auxs, auxs_lhss ~~ auxs_rhss)) end; + +fun mk_random_datatype descr vs rtyps tycos names thy = + let + val i = @{term "i\code_numeral"}; + val mk_prop_eq = HOLogic.mk_Trueprop o HOLogic.mk_eq; + val Ts = map (fn tyco => Type (tyco, map TFree vs)) tycos; + fun mk_size_arg k = case DatatypeCodegen.find_shortest_path descr k + of SOME (_, l) => if l = 0 then i + else @{term "max :: code_numeral \ code_numeral \ code_numeral"} + $ HOLogic.mk_number @{typ code_numeral} l $ i + | NONE => i; + val (prefix, (random_auxs, auxs_eqs)) = (apsnd o apsnd o map) mk_prop_eq + (mk_random_aux_eqs thy descr vs Ts rtyps tycos names); + val random_defs = map_index (fn (k, T) => mk_prop_eq + (HOLogic.mk_random T i, nth random_auxs k $ mk_size_arg k $ i)) Ts; + in + thy + |> TheoryTarget.instantiation (tycos, vs, @{sort random}) + |> random_aux_specification prefix auxs_eqs + |> `(fn lthy => map (Syntax.check_term lthy) random_defs) + |-> (fn random_defs' => fold_map (fn random_def => + Specification.definition (NONE, (Attrib.empty_binding, + random_def))) random_defs') + |> snd + |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) + end; + +fun ensure_random_datatype (raw_tycos as tyco :: _) thy = + let + val pp = Syntax.pp_global thy; + val algebra = Sign.classes_of thy; + val info = DatatypePackage.the_datatype thy tyco; + val descr = #descr info; + val tycos = Library.take (length raw_tycos, descr) + |> map (fn (_, (tyco, dTs, _)) => tyco); + val names = map Long_Name.base_name (the_default tycos (#alt_names info)); + val (raw_vs :: _, raw_coss) = (split_list + o map (DatatypePackage.the_datatype_spec thy)) tycos; + val raw_Ts = maps (maps snd) raw_coss; + val vs' = (fold o fold_atyps) (fn TFree (v, _) => insert (op =) v) raw_Ts []; + val vs = map (fn (v, sort) => (v, if member (op =) vs' v + then Sorts.inter_sort algebra (sort, @{sort random}) else sort)) raw_vs; + val rtyps = Library.drop (length tycos, descr) + |> map (fn (_, (tyco, dTs, _)) => + Type (tyco, map (DatatypeAux.typ_of_dtyp descr vs) dTs)); + val sorts = map snd vs; + val constrain = map_atyps + (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)); + val Ts = map constrain raw_Ts; + val algebra' = algebra + |> fold (fn tyco => Sorts.add_arities pp + (tyco, map (rpair sorts) @{sort random})) tycos; + val can_inst = forall (fn T => + Sorts.of_sort algebra' (T, @{sort random})) Ts; + val hast_inst = exists (fn tyco => + can (Sorts.mg_domain algebra tyco) @{sort random}) tycos; + in if can_inst andalso not hast_inst then (mk_random_datatype descr vs rtyps tycos names thy + (*FIXME ephemeral handles*) + handle e as TERM (msg, ts) => (tracing (cat_lines (msg :: map (Syntax.string_of_term_global thy) ts)); raise e) + | e as TYPE (msg, _, _) => (tracing msg; raise e) + | e as ERROR msg => (tracing msg; raise e)) + else thy end; (** setup **) val setup = Code_Target.extend_target (target, (Code_ML.target_Eval, K I)) #> Quickcheck.add_generator ("code", compile_generator_expr o ProofContext.theory_of) - #> TypecopyPackage.interpretation ensure_random_typecopy; + #> TypecopyPackage.interpretation ensure_random_typecopy + #> DatatypePackage.interpretation ensure_random_datatype; end; diff -r a94aa5f045fb -r bd2f7211a420 src/HOL/ex/Quickcheck_Generators.thy --- a/src/HOL/ex/Quickcheck_Generators.thy Tue Jun 09 22:59:53 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,274 +0,0 @@ -(* Author: Florian Haftmann, TU Muenchen *) - -header {* Experimental counterexample generators *} - -theory Quickcheck_Generators -imports Quickcheck State_Monad -begin - -subsection {* Datatypes *} - -definition collapse :: "('a \ ('a \ 'b \ 'a) \ 'a) \ 'a \ 'b \ 'a" where - "collapse f = (do g \ f; g done)" - -lemma random'_if: - fixes random' :: "code_numeral \ code_numeral \ Random.seed \ ('a \ (unit \ term)) \ Random.seed" - assumes "random' 0 j = (\s. undefined)" - and "\i. random' (Suc_code_numeral i) j = rhs2 i" - shows "random' i j s = (if i = 0 then undefined else rhs2 (i - 1) s)" - by (cases i rule: code_numeral.exhaust) (insert assms, simp_all) - -setup {* -let - fun liftT T sT = sT --> HOLogic.mk_prodT (T, sT); - fun scomp T1 T2 sT f g = Const (@{const_name scomp}, - liftT T1 sT --> (T1 --> liftT T2 sT) --> liftT T2 sT) $ f $ g; - exception REC of string; - exception TYP of string; - fun mk_collapse thy ty = Sign.mk_const thy - (@{const_name collapse}, [@{typ Random.seed}, ty]); - fun term_ty ty = HOLogic.mk_prodT (ty, @{typ "unit \ term"}); - fun mk_split thy ty ty' = Sign.mk_const thy - (@{const_name split}, [ty, @{typ "unit \ term"}, liftT (term_ty ty') @{typ Random.seed}]); - fun mk_scomp_split thy ty ty' t t' = - scomp (term_ty ty) (term_ty ty') @{typ Random.seed} t - (mk_split thy ty ty' $ Abs ("", ty, Abs ("", @{typ "unit \ term"}, t'))) - fun mk_cons thy this_ty (c, args) = - let - val tys = map (fst o fst) args; - val c_ty = tys ---> this_ty; - val c = Const (c, tys ---> this_ty); - val t_indices = map (curry ( op * ) 2) (length tys - 1 downto 0); - val c_indices = map (curry ( op + ) 1) t_indices; - val c_t = list_comb (c, map Bound c_indices); - val t_t = Abs ("", @{typ unit}, HOLogic.reflect_term - (list_comb (c, map (fn k => Bound (k + 1)) t_indices)) - |> map_aterms (fn t as Bound _ => t $ @{term "()"} | t => t)); - val return = HOLogic.mk_return (term_ty this_ty) @{typ Random.seed} - (HOLogic.mk_prod (c_t, t_t)); - val t = fold_rev (fn ((ty, _), random) => - mk_scomp_split thy ty this_ty random) - args return; - val is_rec = exists (snd o fst) args; - in (is_rec, t) end; - fun mk_conss thy ty [] = NONE - | mk_conss thy ty [(_, t)] = SOME t - | mk_conss thy ty ts = SOME (mk_collapse thy (term_ty ty) $ - (Sign.mk_const thy (@{const_name Random.select}, [liftT (term_ty ty) @{typ Random.seed}]) $ - HOLogic.mk_list (liftT (term_ty ty) @{typ Random.seed}) (map snd ts))); - fun mk_clauses thy ty (tyco, (ts_rec, ts_atom)) = - let - val SOME t_atom = mk_conss thy ty ts_atom; - in case mk_conss thy ty ts_rec - of SOME t_rec => mk_collapse thy (term_ty ty) $ - (Sign.mk_const thy (@{const_name Random.select_default}, [liftT (term_ty ty) @{typ Random.seed}]) $ - @{term "i\code_numeral"} $ t_rec $ t_atom) - | NONE => t_atom - end; - fun mk_random_eqs thy vs tycos = - let - val this_ty = Type (hd tycos, map TFree vs); - val this_ty' = liftT (term_ty this_ty) @{typ Random.seed}; - val random_name = Long_Name.base_name @{const_name random}; - val random'_name = random_name ^ "_" ^ Class.type_name (hd tycos) ^ "'"; - fun random ty = Sign.mk_const thy (@{const_name random}, [ty]); - val random' = Free (random'_name, - @{typ code_numeral} --> @{typ code_numeral} --> this_ty'); - fun atom ty = if Sign.of_sort thy (ty, @{sort random}) - then ((ty, false), random ty $ @{term "j\code_numeral"}) - else raise TYP - ("Will not generate random elements for type(s) " ^ quote (hd tycos)); - fun dtyp tyco = ((this_ty, true), random' $ @{term "i\code_numeral"} $ @{term "j\code_numeral"}); - fun rtyp (tyco, Ts) _ = raise REC - ("Will not generate random elements for mutual recursive type " ^ quote (hd tycos)); - val rhss = DatatypePackage.construction_interpretation thy - { atom = atom, dtyp = dtyp, rtyp = rtyp } vs tycos - |> fst - |> (map o apsnd o map) (mk_cons thy this_ty) - |> (map o apsnd) (List.partition fst) - |> map (mk_clauses thy this_ty) - val eqss = map ((apsnd o map) (HOLogic.mk_Trueprop o HOLogic.mk_eq) o (fn rhs => ((this_ty, random'), [ - (random' $ @{term "0\code_numeral"} $ @{term "j\code_numeral"}, Abs ("s", @{typ Random.seed}, - Const (@{const_name undefined}, HOLogic.mk_prodT (term_ty this_ty, @{typ Random.seed})))), - (random' $ @{term "Suc_code_numeral i"} $ @{term "j\code_numeral"}, rhs) - ]))) rhss; - in eqss end; - fun random_inst [tyco] thy = - let - val (raw_vs, _) = DatatypePackage.the_datatype_spec thy tyco; - val vs = (map o apsnd) - (curry (Sorts.inter_sort (Sign.classes_of thy)) @{sort random}) raw_vs; - val ((this_ty, random'), eqs') = singleton (mk_random_eqs thy vs) tyco; - val eq = (HOLogic.mk_Trueprop o HOLogic.mk_eq) - (Sign.mk_const thy (@{const_name random}, [this_ty]) $ @{term "i\code_numeral"}, - random' $ @{term "max (i\code_numeral) 1"} $ @{term "i\code_numeral"}) - val del_func = Attrib.internal (fn _ => Thm.declaration_attribute - (fn thm => Context.mapping (Code.del_eqn thm) I)); - fun add_code simps lthy = - let - val thy = ProofContext.theory_of lthy; - val thm = @{thm random'_if} - |> Drule.instantiate' [SOME (Thm.ctyp_of thy this_ty)] [SOME (Thm.cterm_of thy random')] - |> (fn thm => thm OF simps) - |> singleton (ProofContext.export lthy (ProofContext.init thy)); - val c = (fst o dest_Const o fst o strip_comb o fst - o HOLogic.dest_eq o HOLogic.dest_Trueprop o Thm.prop_of) thm; - in - lthy - |> LocalTheory.theory (Code.del_eqns c - #> PureThy.add_thm ((Binding.name (fst (dest_Free random') ^ "_code"), thm), [Thm.kind_internal]) - #-> Code.add_eqn) - end; - in - thy - |> TheoryTarget.instantiation ([tyco], vs, @{sort random}) - |> PrimrecPackage.add_primrec - [(Binding.name (fst (dest_Free random')), SOME (snd (dest_Free random')), NoSyn)] - (map (fn eq => ((Binding.empty, [del_func]), eq)) eqs') - |-> add_code - |> `(fn lthy => Syntax.check_term lthy eq) - |-> (fn eq => Specification.definition (NONE, (Attrib.empty_binding, eq))) - |> snd - |> Class.prove_instantiation_instance (K (Class.intro_classes_tac [])) - |> LocalTheory.exit_global - end - | random_inst tycos thy = raise REC - ("Will not generate random elements for mutual recursive type(s) " ^ commas (map quote tycos)); - fun add_random_inst [@{type_name bool}] thy = thy - | add_random_inst [@{type_name nat}] thy = thy - | add_random_inst [@{type_name char}] thy = thy - | add_random_inst [@{type_name String.literal}] thy = thy - | add_random_inst tycos thy = random_inst tycos thy - handle REC msg => (warning msg; thy) - | TYP msg => (warning msg; thy) -in DatatypePackage.interpretation add_random_inst end -*} - - -subsection {* Examples *} - -theorem "map g (map f xs) = map (g o f) xs" - quickcheck [generator = code] - by (induct xs) simp_all - -theorem "map g (map f xs) = map (f o g) xs" - quickcheck [generator = code] - oops - -theorem "rev (xs @ ys) = rev ys @ rev xs" - quickcheck [generator = code] - by simp - -theorem "rev (xs @ ys) = rev xs @ rev ys" - quickcheck [generator = code] - oops - -theorem "rev (rev xs) = xs" - quickcheck [generator = code] - by simp - -theorem "rev xs = xs" - quickcheck [generator = code] - oops - -primrec app :: "('a \ 'a) list \ 'a \ 'a" where - "app [] x = x" - | "app (f # fs) x = app fs (f x)" - -lemma "app (fs @ gs) x = app gs (app fs x)" - quickcheck [generator = code] - by (induct fs arbitrary: x) simp_all - -lemma "app (fs @ gs) x = app fs (app gs x)" - quickcheck [generator = code] - oops - -primrec occurs :: "'a \ 'a list \ nat" where - "occurs a [] = 0" - | "occurs a (x#xs) = (if (x=a) then Suc(occurs a xs) else occurs a xs)" - -primrec del1 :: "'a \ 'a list \ 'a list" where - "del1 a [] = []" - | "del1 a (x#xs) = (if (x=a) then xs else (x#del1 a xs))" - -lemma "Suc (occurs a (del1 a xs)) = occurs a xs" - -- {* Wrong. Precondition needed.*} - quickcheck [generator = code] - oops - -lemma "xs ~= [] \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck [generator = code] - -- {* Also wrong.*} - oops - -lemma "0 < occurs a xs \ Suc (occurs a (del1 a xs)) = occurs a xs" - quickcheck [generator = code] - by (induct xs) auto - -primrec replace :: "'a \ 'a \ 'a list \ 'a list" where - "replace a b [] = []" - | "replace a b (x#xs) = (if (x=a) then (b#(replace a b xs)) - else (x#(replace a b xs)))" - -lemma "occurs a xs = occurs b (replace a b xs)" - quickcheck [generator = code] - -- {* Wrong. Precondition needed.*} - oops - -lemma "occurs b xs = 0 \ a=b \ occurs a xs = occurs b (replace a b xs)" - quickcheck [generator = code] - by (induct xs) simp_all - - -subsection {* Trees *} - -datatype 'a tree = Twig | Leaf 'a | Branch "'a tree" "'a tree" - -primrec leaves :: "'a tree \ 'a list" where - "leaves Twig = []" - | "leaves (Leaf a) = [a]" - | "leaves (Branch l r) = (leaves l) @ (leaves r)" - -primrec plant :: "'a list \ 'a tree" where - "plant [] = Twig " - | "plant (x#xs) = Branch (Leaf x) (plant xs)" - -primrec mirror :: "'a tree \ 'a tree" where - "mirror (Twig) = Twig " - | "mirror (Leaf a) = Leaf a " - | "mirror (Branch l r) = Branch (mirror r) (mirror l)" - -theorem "plant (rev (leaves xt)) = mirror xt" - quickcheck [generator = code] - --{* Wrong! *} - oops - -theorem "plant (leaves xt @ leaves yt) = Branch xt yt" - quickcheck [generator = code] - --{* Wrong! *} - oops - -datatype 'a ntree = Tip "'a" | Node "'a" "'a ntree" "'a ntree" - -primrec inOrder :: "'a ntree \ 'a list" where - "inOrder (Tip a)= [a]" - | "inOrder (Node f x y) = (inOrder x)@[f]@(inOrder y)" - -primrec root :: "'a ntree \ 'a" where - "root (Tip a) = a" - | "root (Node f x y) = f" - -theorem "hd (inOrder xt) = root xt" - quickcheck [generator = code] - --{* Wrong! *} - oops - -lemma "int (f k) = k" - quickcheck [generator = code] - oops - -lemma "int (nat k) = k" - quickcheck [generator = code] - oops - -end diff -r a94aa5f045fb -r bd2f7211a420 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Tue Jun 09 22:59:53 2009 +0200 +++ b/src/HOL/ex/ROOT.ML Tue Jun 09 22:59:54 2009 +0200 @@ -9,7 +9,6 @@ "FuncSet", "Word", "Eval_Examples", - "Quickcheck_Generators", "Codegenerator_Test", "Codegenerator_Pretty_Test", "NormalForm",