# HG changeset patch # User haftmann # Date 1352660162 -3600 # Node ID 0051dc4f301f0c86a50bc752224616b85bc195e3 # Parent 2214bc566f88a00225e6caf91342e12aef6205d8 dropped dead code; tuned theory text diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Quickcheck.thy --- a/src/HOL/Quickcheck.thy Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Quickcheck.thy Sun Nov 11 19:56:02 2012 +0100 @@ -157,11 +157,11 @@ (i, random j \\ (%x. random_aux_set (i - 1) j \\ (%s. Pair (valtermify_insert x s))))])" proof (induct i rule: code_numeral.induct) case zero - show ?case by (subst select_weight_drop_zero[symmetric]) - (simp add: filter.simps random_aux_set.simps[simplified]) + show ?case by (subst select_weight_drop_zero [symmetric]) + (simp add: random_aux_set.simps [simplified]) next case (Suc i) - show ?case by (simp only: random_aux_set.simps(2)[of "i"] Suc_code_numeral_minus_one) + show ?case by (simp only: random_aux_set.simps(2) [of "i"] Suc_code_numeral_minus_one) qed definition "random_set i = random_aux_set i i" diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Quickcheck_Narrowing.thy --- a/src/HOL/Quickcheck_Narrowing.thy Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Quickcheck_Narrowing.thy Sun Nov 11 19:56:02 2012 +0100 @@ -411,34 +411,6 @@ Code_Evaluation.term_of (- (int_of i) div 2) else Code_Evaluation.term_of ((int_of i + 1) div 2))" by (rule partial_term_of_anything)+ -text {* Defining integers by positive and negative copy of naturals *} -(* -datatype simple_int = Positive nat | Negative nat - -primrec int_of_simple_int :: "simple_int => int" -where - "int_of_simple_int (Positive n) = int n" -| "int_of_simple_int (Negative n) = (-1 - int n)" - -instantiation int :: narrowing -begin - -definition narrowing_int :: "code_int => int cons" -where - "narrowing_int d = map_cons int_of_simple_int ((narrowing :: simple_int narrowing) d)" - -instance .. - -end - -text {* printing the partial terms *} - -lemma [code]: - "partial_term_of (ty :: int itself) t == Code_Evaluation.App (Code_Evaluation.Const (STR ''Quickcheck_Narrowing.int_of_simple_int'') - (Typerep.Typerep (STR ''fun'') [Typerep.Typerep (STR ''Quickcheck_Narrowing.simple_int'') [], Typerep.Typerep (STR ''Int.int'') []])) (partial_term_of (TYPE(simple_int)) t)" -by (rule partial_term_of_anything) - -*) subsection {* The @{text find_unused_assms} command *} diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Tools/Quickcheck/exhaustive_generators.ML --- a/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Tools/Quickcheck/exhaustive_generators.ML Sun Nov 11 19:56:02 2012 +0100 @@ -45,25 +45,6 @@ val full_support = Attrib.setup_config_bool @{binding quickcheck_full_support} (K true) val quickcheck_pretty = Attrib.setup_config_bool @{binding quickcheck_pretty} (K true) -(** general term functions **) - -fun mk_measure f = - let - val Type ("fun", [T, @{typ nat}]) = fastype_of f - in - Const (@{const_name Wellfounded.measure}, - (T --> @{typ nat}) --> HOLogic.mk_prodT (T, T) --> @{typ bool}) - $ f - end - -fun mk_sumcases rT f (Type (@{type_name Sum_Type.sum}, [TL, TR])) = - let - val lt = mk_sumcases rT f TL - val rt = mk_sumcases rT f TR - in - SumTree.mk_sumcase TL TR rT lt rt - end - | mk_sumcases _ f T = f T (** abstract syntax **) @@ -80,9 +61,6 @@ Const (@{const_name "Quickcheck_Exhaustive.orelse"}, T --> T --> T) $ x $ y end -fun mk_unit_let (x, y) = - Const (@{const_name "Let"}, @{typ "unit => (unit => unit) => unit"}) $ x $ absdummy @{typ unit} y - fun mk_if (b, t, e) = let val T = fastype_of t @@ -100,7 +78,6 @@ val exhaustiveN = "exhaustive"; val full_exhaustiveN = "full_exhaustive"; -val fast_exhaustiveN = "fast_exhaustive"; val bounded_forallN = "bounded_forall"; fun fast_exhaustiveT T = (T --> @{typ unit}) @@ -145,20 +122,6 @@ val bounds = map Bound (((length xs) - 1) downto 0) val start_term = test_function simpleT $ list_comb (constr, bounds) in fold_rev (fn f => fn t => f t) fns start_term end - -fun mk_fast_equations functerms = - let - fun test_function T = Free ("f", T --> @{typ "unit"}) - val mk_call = gen_mk_call (fn T => - Const (@{const_name "Quickcheck_Exhaustive.fast_exhaustive_class.fast_exhaustive"}, - fast_exhaustiveT T)) - val mk_aux_call = gen_mk_aux_call functerms - val mk_consexpr = gen_mk_consexpr test_function - fun mk_rhs exprs = @{term "If :: bool => unit => unit => unit"} - $ size_ge_zero $ (foldr1 mk_unit_let exprs) $ @{term "()"} - in - mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) - end fun mk_equations functerms = let @@ -228,26 +191,6 @@ mk_equation_terms (mk_call, mk_aux_call, mk_consexpr, mk_rhs, test_function, functerms) end -(** foundational definition with the function package **) - -val less_int_pred = @{lemma "i > 0 ==> Code_Numeral.nat_of ((i :: code_numeral) - 1) < Code_Numeral.nat_of i" by auto} - -fun mk_single_measure T = HOLogic.mk_comp (@{term "Code_Numeral.nat_of"}, - Const (@{const_name "Product_Type.snd"}, T --> @{typ "code_numeral"})) - -fun mk_termination_measure T = - let - val T' = fst (HOLogic.dest_prodT (HOLogic.dest_setT T)) - in - mk_measure (mk_sumcases @{typ nat} mk_single_measure T') - end - -fun termination_tac ctxt = - Function_Relation.relation_tac ctxt mk_termination_measure 1 - THEN rtac @{thm wf_measure} 1 - THEN (REPEAT_DETERM (Simplifier.asm_full_simp_tac - (HOL_basic_ss addsimps [@{thm in_measure}, @{thm o_def}, @{thm snd_conv}, - @{thm nat_mono_iff}, less_int_pred] @ @{thms sum.cases}) 1)) (** instantiating generator classes **) @@ -278,10 +221,6 @@ ("bounded universal quantifiers", bounded_forallN, @{sort bounded_forall}, mk_bounded_forall_equations, bounded_forallT, ["P", "i"]); -val instantiate_fast_exhaustive_datatype = instantiate_datatype - ("fast exhaustive generators", fast_exhaustiveN, @{sort fast_exhaustive}, - mk_fast_equations, fast_exhaustiveT, ["f", "i"]) - val instantiate_exhaustive_datatype = instantiate_datatype ("exhaustive generators", exhaustiveN, @{sort exhaustive}, mk_equations, exhaustiveT, ["f", "i"]) @@ -479,7 +418,7 @@ Const (@{const_name "Quickcheck_Exhaustive.bounded_forall_class.bounded_forall"}, bounded_forallT T) $ lambda (Free (s, T)) t $ depth fun mk_safe_if (cond, then_t, else_t) genuine = mk_if (cond, then_t, else_t genuine) - fun mk_let safe def v_opt t e = mk_let_expr (the_default def v_opt, t, e) + fun mk_let _ def v_opt t e = mk_let_expr (the_default def v_opt, t, e) val mk_test_term = mk_test_term lookup mk_bounded_forall mk_safe_if mk_let @{term True} (K @{term False}) ctxt in lambda depth (mk_test_term t) end diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Tools/Quickcheck/narrowing_generators.ML --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Nov 11 19:56:02 2012 +0100 @@ -126,8 +126,6 @@ fun narrowingT T = @{typ Quickcheck_Narrowing.code_int} --> Type (@{type_name Quickcheck_Narrowing.narrowing_cons}, [T]) -fun mk_empty T = Const (@{const_name Quickcheck_Narrowing.empty}, narrowingT T) - fun mk_cons c T = Const (@{const_name Quickcheck_Narrowing.cons}, T --> narrowingT T) $ Const (c, T) fun mk_apply (T, t) (U, u) = @@ -147,7 +145,7 @@ (** deriving narrowing instances **) -fun mk_equations descr vs tycos narrowings (Ts, Us) = +fun mk_equations descr vs narrowings = let fun mk_call T = (T, Const (@{const_name "Quickcheck_Narrowing.narrowing_class.narrowing"}, narrowingT T)) @@ -188,7 +186,7 @@ thy |> Class.instantiation (tycos, vs, @{sort narrowing}) |> Quickcheck_Common.define_functions - (fn narrowings => mk_equations descr vs tycos narrowings (Ts, Us), NONE) + (fn narrowings => mk_equations descr vs narrowings, NONE) prfx [] narrowingsN (map narrowingT (Ts @ Us)) |> Class.prove_instantiation_exit (K (Class.intro_classes_tac [])) else @@ -221,15 +219,13 @@ let val ({elapsed, ...}, result) = Timing.timing e () in (result, (description, Time.toMilliseconds elapsed)) end -fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) = +fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, _) = let val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie fun message s = if quiet then () else Output.urgent_message s fun verbose_message s = if not quiet andalso verbose then Output.urgent_message s else () val current_size = Unsynchronized.ref 0 val current_result = Unsynchronized.ref Quickcheck.empty_result - fun excipit () = - "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) val tmp_prefix = "Quickcheck_Narrowing" val ghc_options = Config.get ctxt ghc_options val with_tmp_dir = @@ -262,7 +258,7 @@ ghc_options ^ " " ^ (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^ " -o " ^ executable ^ ";" - val (result, compilation_time) = + val (_, compilation_time) = elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd) val _ = Quickcheck.add_timing compilation_time current_result fun haskell_string_of_bool v = if v then "True" else "False" @@ -357,7 +353,7 @@ fun mk_eval_cfun dT rT = Const (@{const_name "Quickcheck_Narrowing.eval_cfun"}, Type (@{type_name "Quickcheck_Narrowing.cfun"}, [rT]) --> dT --> rT) - fun eval_function (T as Type (@{type_name fun}, [dT, rT])) = + fun eval_function (Type (@{type_name fun}, [dT, rT])) = let val (rt', rT') = eval_function rT in @@ -433,7 +429,7 @@ fun mk_case_term ctxt p ((@{const_name Ex}, (x, T)) :: qs') (Existential_Counterexample cs) = Datatype_Case.make_case ctxt Datatype_Case.Quiet [] (Free (x, T)) (map (fn (t, c) => (t, mk_case_term ctxt (p - 1) qs' c)) cs) - | mk_case_term ctxt p ((@{const_name All}, (x, T)) :: qs') (Universal_Counterexample (t, c)) = + | mk_case_term ctxt p ((@{const_name All}, _) :: qs') (Universal_Counterexample (t, c)) = if p = 0 then t else mk_case_term ctxt (p - 1) qs' c val post_process = (perhaps (try Quickcheck_Common.post_process_term)) o eval_finite_functions @@ -443,11 +439,11 @@ val ps = filter (fn (_, (@{const_name All}, _)) => true | _ => false) (map_index I qs) in - map (fn (p, (_, (x, T))) => (x, mk_case_term ctxt p qs result)) ps + map (fn (p, (_, (x, _))) => (x, mk_case_term ctxt p qs result)) ps |> map (apsnd post_process) end -fun test_term ctxt catch_code_errors (t, eval_terms) = +fun test_term ctxt catch_code_errors (t, _) = let fun dest_result (Quickcheck.Result r) = r val opts = diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Tools/Quickcheck/quickcheck_common.ML --- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML Sun Nov 11 19:56:02 2012 +0100 @@ -83,8 +83,6 @@ val names = Term.add_free_names t [] val current_size = Unsynchronized.ref 0 val current_result = Unsynchronized.ref Quickcheck.empty_result - fun excipit () = - "Quickcheck ran out of time while testing at size " ^ string_of_int (!current_size) val act = if catch_code_errors then try else (fn f => SOME o f) val (test_fun, comp_time) = cpu_time "quickcheck compilation" (fn () => act (compile ctxt) [(t, eval_terms)]); @@ -134,44 +132,6 @@ in !current_result end end; -fun validate_terms ctxt ts = - let - val _ = map check_test_term ts - val size = Config.get ctxt Quickcheck.size - val (test_funs, comp_time) = cpu_time "quickcheck batch compilation" - (fn () => Quickcheck.mk_batch_validator ctxt ts) - fun with_size tester k = - if k > size then true - else if tester k then with_size tester (k + 1) else false - val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => - TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) - (fn () => with_size test_fun 1) () - handle TimeLimit.TimeOut => true)) test_funs) - in - (results, [comp_time, exec_time]) - end - -fun test_terms ctxt ts = - let - val _ = map check_test_term ts - val size = Config.get ctxt Quickcheck.size - val namess = map (fn t => Term.add_free_names t []) ts - val (test_funs, comp_time) = - cpu_time "quickcheck batch compilation" (fn () => Quickcheck.mk_batch_tester ctxt ts) - fun with_size tester k = - if k > size then NONE - else case tester k of SOME ts => SOME ts | NONE => with_size tester (k + 1) - val (results, exec_time) = cpu_time "quickcheck batch execution" (fn () => - Option.map (map (fn test_fun => - TimeLimit.timeLimit (seconds (Config.get ctxt Quickcheck.timeout)) - (fn () => with_size test_fun 1) () - handle TimeLimit.TimeOut => NONE)) test_funs) - in - (Option.map (map2 (fn names => Option.map (fn ts => names ~~ ts)) namess) results, - [comp_time, exec_time]) - end - fun test_term_with_cardinality (name, (size_matters_for, compile)) ctxt catch_code_errors ts = let val genuine_only = Config.get ctxt Quickcheck.genuine_only @@ -294,7 +254,7 @@ fun subtype_preprocess ctxt (T, (t, ts)) = let val preds = Subtype_Predicates.get (Context.Proof ctxt) - fun matches (p $ x) = AList.defined Term.could_unify preds p + fun matches (p $ _) = AList.defined Term.could_unify preds p fun get_match (p $ x) = Option.map (rpair x) (AList.lookup Term.could_unify preds p) fun subst_of (tyco, v as Free (x, repT)) = let @@ -330,9 +290,9 @@ [(NONE, Term (preprocess lthy check_goal, eval_terms))]) goals val error_msg = cat_lines - (maps (map_filter (fn (_, Term t) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) + (maps (map_filter (fn (_, Term _) => NONE | (_, Wellsorted_Error s) => SOME s)) inst_goals) fun is_wellsorted_term (T, Term t) = SOME (T, t) - | is_wellsorted_term (_, Wellsorted_Error s) = NONE + | is_wellsorted_term (_, Wellsorted_Error _) = NONE val correct_inst_goals = case map (map_filter is_wellsorted_term) inst_goals of [[]] => error error_msg @@ -498,7 +458,7 @@ | make_set T1 ((t1, @{const True}) :: tps) = Const (@{const_name insert}, T1 --> (T1 --> @{typ bool}) --> T1 --> @{typ bool}) $ t1 $ (make_set T1 tps) - | make_set T1 ((_, t) :: tps) = raise TERM ("make_set", [t]) + | make_set T1 ((_, t) :: _) = raise TERM ("make_set", [t]) fun make_coset T [] = Const (@{const_abbrev UNIV}, T --> @{typ bool}) | make_coset T tps = diff -r 2214bc566f88 -r 0051dc4f301f src/HOL/Tools/Quickcheck/random_generators.ML --- a/src/HOL/Tools/Quickcheck/random_generators.ML Sun Nov 11 19:24:01 2012 +0100 +++ b/src/HOL/Tools/Quickcheck/random_generators.ML Sun Nov 11 19:56:02 2012 +0100 @@ -42,7 +42,7 @@ let val fun_upd = Const (@{const_name fun_upd}, (T1 --> T2) --> T1 --> T2 --> T1 --> T2); - val ((y, t2), seed') = random seed; + val ((_, t2), seed') = random seed; val (seed'', seed''') = random_split seed'; val state = Unsynchronized.ref (seed'', [], fn () => Abs ("x", T1, t2 ())); @@ -62,10 +62,6 @@ fun term_fun' () = #3 (! state) (); in ((random_fun', term_fun'), seed''') end; -fun mk_if (b, t, e) = - let - val T = fastype_of t - in Const (@{const_name "HOL.If"}, @{typ bool} --> T --> T --> T) $ b $ t $ e end (** datatypes **) @@ -77,7 +73,6 @@ val eq = Thm.cprop_of @{thm random_aux_rec} |> Thm.dest_arg |> Thm.dest_arg |> Thm.dest_arg; val lhs = eq |> Thm.dest_arg1; val pt_random_aux = lhs |> Thm.dest_fun; -val ct_k = lhs |> Thm.dest_arg; val pt_rhs = eq |> Thm.dest_arg |> Thm.dest_fun; val aT = pt_random_aux |> Thm.ctyp_of_term |> dest_ctyp_nth 1; @@ -187,14 +182,13 @@ val random_auxN = "random_aux"; -fun mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us) = +fun mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us) = let val mk_const = curry (Sign.mk_const thy); val random_auxsN = map (prefix (random_auxN ^ "_")) (names @ auxnames); val rTs = Ts @ Us; 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)) @@ -257,7 +251,7 @@ $ HOLogic.mk_number @{typ code_numeral} l $ size | NONE => size; val (random_auxs, auxs_eqs) = (apsnd o map) mk_prop_eq - (mk_random_aux_eqs thy descr vs tycos (names, auxnames) (Ts, Us)); + (mk_random_aux_eqs thy descr vs (names, auxnames) (Ts, Us)); val random_defs = map_index (fn (k, T) => mk_prop_eq (HOLogic.mk_random T size, nth random_auxs k $ mk_size_arg k $ size)) Ts; in @@ -294,7 +288,7 @@ val target = "Quickcheck"; -fun mk_generator_expr ctxt (t, eval_terms) = +fun mk_generator_expr ctxt (t, _) = let val thy = Proof_Context.theory_of ctxt val prop = fold_rev absfree (Term.add_frees t []) t @@ -304,7 +298,7 @@ (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 ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt + val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt val genuine_only = Free (genuine_only_name, @{typ bool}) val none_t = Const (@{const_name "None"}, resultT) val check = Quickcheck_Common.mk_safe_if genuine_only none_t (result, none_t, @@ -327,7 +321,7 @@ (Abs ("n", @{typ code_numeral}, fold_rev mk_bindclause bounds (return $ check true))) end; -fun mk_reporting_generator_expr ctxt (t, eval_terms) = +fun mk_reporting_generator_expr ctxt (t, _) = let val thy = Proof_Context.theory_of ctxt val resultT = @{typ "(bool * term list) option * (bool list * bool)"} @@ -348,7 +342,7 @@ fun mk_concl_report b = HOLogic.mk_prod (HOLogic.mk_list HOLogic.boolT (replicate (length assms) @{term True}), Quickcheck_Common.reflect_bool b) - val ([genuine_only_name], ctxt') = Variable.variant_fixes ["genuine_only"] ctxt + val ([genuine_only_name], _) = Variable.variant_fixes ["genuine_only"] ctxt val genuine_only = Free (genuine_only_name, @{typ bool}) val none_t = HOLogic.mk_prod (@{term "None :: (bool * term list) option"}, mk_concl_report true) val concl_check = Quickcheck_Common.mk_safe_if genuine_only none_t (concl, none_t, @@ -422,7 +416,7 @@ (fn proc => fn g => fn c => fn b => fn s => g c b s #>> (apfst o Option.map o apsnd o map) proc) t' []; fun single_tester c b s = compile c b s |> Random_Engine.run - fun iterate_and_collect _ (card, size) 0 report = (NONE, report) + fun iterate_and_collect _ _ 0 report = (NONE, report) | iterate_and_collect genuine_only (card, size) j report = let val (test_result, single_report) = apsnd Run (single_tester card genuine_only size) @@ -444,7 +438,7 @@ (fn proc => fn g => fn c => fn b => fn s => g c b s #>> (Option.map o apsnd o map) proc) t' []; fun single_tester c b s = compile c b s |> Random_Engine.run - fun iterate _ (card, size) 0 = NONE + fun iterate _ _ 0 = NONE | iterate genuine_only (card, size) j = case single_tester card genuine_only size of NONE => iterate genuine_only (card, size) (j - 1)