# HG changeset patch # User bulwahn # Date 1269243013 -3600 # Node ID f5422b736c44fd5ec5c836ebdfd519b9328c9a6a # Parent 7b39120a1494fae5ba6792de387ab4da43c31d36 reduced the debug output functions from 2 to 1 diff -r 7b39120a1494 -r f5422b736c44 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Mon Mar 22 08:30:13 2010 +0100 @@ -72,13 +72,9 @@ (* debug stuff *) -fun print_tac s = Seq.single; - -fun print_tac' options s = +fun print_tac options s = if show_proof_trace options then Tactical.print_tac s else Seq.single; -fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) - fun assert b = if not b then raise Fail "Assertion failed" else warning "Assertion holds" datatype assertion = Max_number_of_subgoals of int @@ -1932,9 +1928,9 @@ | Abs _ => raise Fail "prove_param: No valid parameter term" in REPEAT_DETERM (rtac @{thm ext} 1) - THEN print_tac' options "prove_param" + THEN print_tac options "prove_param" THEN f_tac - THEN print_tac' options "after prove_param" + THEN print_tac options "after prove_param" THEN (REPEAT_DETERM (atac 1)) THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations)) THEN REPEAT_DETERM (rtac @{thm refl} 1) @@ -1949,19 +1945,19 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - print_tac' options "before intro rule:" + print_tac options "before intro rule:" THEN rtac introrule 1 - THEN print_tac' options "after intro rule" + THEN print_tac options "after intro rule" (* for the right assumption in first position *) THEN rotate_tac premposition 1 THEN atac 1 - THEN print_tac' options "parameter goal" + THEN print_tac options "parameter goal" (* work with parameter arguments *) THEN (EVERY (map2 (prove_param options thy nargs) ho_args param_derivations)) THEN (REPEAT_DETERM (atac 1)) end | (Free _, _) => - print_tac' options "proving parameter call.." + print_tac options "proving parameter call.." THEN Subgoal.FOCUS_PREMS (fn {context = ctxt, params = params, prems = prems, asms = a, concl = cl, schematics = s} => let @@ -1978,7 +1974,7 @@ in rtac param_prem' 1 end) (ProofContext.init thy) 1 (* FIXME: proper context handling *) - THEN print_tac' options "after prove parameter call" + THEN print_tac options "after prove parameter call" fun SOLVED tac st = FILTER (fn st' => nprems_of st' = nprems_of st - 1) tac st; @@ -2012,14 +2008,14 @@ in (* make this simpset better! *) asm_full_simp_tac (HOL_basic_ss' addsimps simprules) 1 - THEN print_tac' options "after prove_match:" + THEN print_tac options "after prove_match:" THEN (DETERM (TRY (EqSubst.eqsubst_tac (ProofContext.init thy) [0] [@{thm HOL.if_P}] 1 THEN (REPEAT_DETERM (rtac @{thm conjI} 1 THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1)))) - THEN print_tac' options "if condition to be solved:" - THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac' options "after if simp; in SOLVED:")) + THEN print_tac options "if condition to be solved:" + THEN (SOLVED (asm_simp_tac HOL_basic_ss' 1 THEN print_tac options "after if simp; in SOLVED:")) THEN check_format thy - THEN print_tac' options "after if simplification - a TRY block"))) - THEN print_tac' options "after if simplification" + THEN print_tac options "after if simplification - a TRY block"))) + THEN print_tac options "after if simplification" end; (* corresponds to compile_fun -- maybe call that also compile_sidecond? *) @@ -2048,9 +2044,9 @@ val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems out_ts [] = (prove_match options thy out_ts) - THEN print_tac' options "before simplifying assumptions" + THEN print_tac options "before simplifying assumptions" THEN asm_full_simp_tac HOL_basic_ss' 1 - THEN print_tac' options "before single intro rule" + THEN print_tac options "before single intro rule" THEN (rtac (if null clause_out_ts then @{thm singleI_unit} else @{thm singleI}) 1) | prove_prems out_ts ((p, deriv) :: ps) = let @@ -2064,11 +2060,11 @@ val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems out_ts''' ps in - print_tac' options "before clause:" + print_tac options "before clause:" (*THEN asm_simp_tac HOL_basic_ss 1*) - THEN print_tac' options "before prove_expr:" + THEN print_tac options "before prove_expr:" THEN prove_expr options thy nargs premposition (t, deriv) - THEN print_tac' options "after prove_expr:" + THEN print_tac options "after prove_expr:" THEN rec_tac end | Negprem t => @@ -2082,16 +2078,16 @@ val param_derivations = param_derivations_of deriv val params = ho_args_of mode args in - print_tac' options "before prove_neg_expr:" + print_tac options "before prove_neg_expr:" THEN full_simp_tac (HOL_basic_ss addsimps [@{thm split_eta}, @{thm split_beta}, @{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}, @{thm Product_Type.split_conv}]) 1 THEN (if (is_some name) then - print_tac' options "before applying not introduction rule" + print_tac options "before applying not introduction rule" THEN rotate_tac premposition 1 THEN etac (the neg_intro_rule) 1 THEN rotate_tac (~premposition) 1 - THEN print_tac' options "after applying not introduction rule" + THEN print_tac options "after applying not introduction rule" THEN (EVERY (map2 (prove_param options thy nargs) params param_derivations)) THEN (REPEAT_DETERM (atac 1)) else @@ -2104,16 +2100,16 @@ end | Sidecond t => rtac @{thm if_predI} 1 - THEN print_tac' options "before sidecond:" + THEN print_tac options "before sidecond:" THEN prove_sidecond thy t - THEN print_tac' options "after sidecond:" + THEN print_tac options "after sidecond:" THEN prove_prems [] ps) in (prove_match options thy out_ts) THEN rest_tac end; val prems_tac = prove_prems in_ts moded_ps in - print_tac' options "Proving clause..." + print_tac options "Proving clause..." THEN rtac @{thm bindI} 1 THEN rtac @{thm singleI} 1 THEN prems_tac @@ -2130,20 +2126,20 @@ val pred_case_rule = the_elim_of thy pred in REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"})) - THEN print_tac' options "before applying elim rule" + THEN print_tac options "before applying elim rule" THEN etac (predfun_elim_of thy pred mode) 1 THEN etac pred_case_rule 1 - THEN print_tac' options "after applying elim rule" + THEN print_tac options "after applying elim rule" THEN (EVERY (map (fn i => EVERY' (select_sup (length moded_clauses) i) i) (1 upto (length moded_clauses)))) THEN (EVERY (map2 (prove_clause options thy nargs mode) clauses moded_clauses)) - THEN print_tac' options "proved one direction" + THEN print_tac options "proved one direction" end; (** Proof in the other direction **) -fun prove_match2 thy out_ts = let +fun prove_match2 options thy out_ts = let fun split_term_tac (Free _) = all_tac | split_term_tac t = if (is_constructor thy t) then let @@ -2155,11 +2151,11 @@ | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm") val (_, ts) = strip_comb t in - (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ + (print_tac options ("Term " ^ (Syntax.string_of_term_global thy t) ^ "splitting with rules \n" ^ commas (map (Display.string_of_thm_global thy) split_rules))) THEN TRY ((Splitter.split_asm_tac split_rules 1) - THEN (print_tac "after splitting with split_asm rules") + THEN (print_tac options "after splitting with split_asm rules") (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) THEN (REPEAT_DETERM_N (num_of_constrs - 1) @@ -2179,7 +2175,7 @@ *) (* TODO: remove function *) -fun prove_param2 thy t deriv = +fun prove_param2 options thy t deriv = let val (f, args) = strip_comb (Envir.eta_contract t) val mode = head_mode_of deriv @@ -2192,13 +2188,13 @@ | Free _ => all_tac | _ => error "prove_param2: illegal parameter term" in - print_tac "before simplification in prove_args:" + print_tac options "before simplification in prove_args:" THEN f_tac - THEN print_tac "after simplification in prove_args" - THEN EVERY (map2 (prove_param2 thy) ho_args param_derivations) + THEN print_tac options "after simplification in prove_args" + THEN EVERY (map2 (prove_param2 options thy) ho_args param_derivations) end -fun prove_expr2 thy (t, deriv) = +fun prove_expr2 options thy (t, deriv) = (case strip_comb t of (Const (name, T), args) => let @@ -2208,18 +2204,18 @@ in etac @{thm bindE} 1 THEN (REPEAT_DETERM (CHANGED (rewtac @{thm "split_paired_all"}))) - THEN print_tac "prove_expr2-before" + THEN print_tac options "prove_expr2-before" THEN etac (predfun_elim_of thy name mode) 1 - THEN print_tac "prove_expr2" - THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations)) - THEN print_tac "finished prove_expr2" + THEN print_tac options "prove_expr2" + THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations)) + THEN print_tac options "finished prove_expr2" end | _ => etac @{thm bindE} 1) (* FIXME: what is this for? *) (* replace defined by has_mode thy pred *) (* TODO: rewrite function *) -fun prove_sidecond2 thy t = let +fun prove_sidecond2 options thy t = let fun preds_of t nameTs = case strip_comb t of (f as Const (name, T), args) => if is_registered thy name then (name, T) :: nameTs @@ -2234,31 +2230,31 @@ (* only simplify the one assumption *) full_simp_tac (HOL_basic_ss' addsimps @{thm eval_pred} :: defs) 1 (* need better control here! *) - THEN print_tac "after sidecond2 simplification" + THEN print_tac options "after sidecond2 simplification" end -fun prove_clause2 thy pred mode (ts, ps) i = +fun prove_clause2 options thy pred mode (ts, ps) i = let val pred_intro_rule = nth (intros_of thy pred) (i - 1) val (in_ts, clause_out_ts) = split_mode mode ts; fun prove_prems2 out_ts [] = - print_tac "before prove_match2 - last call:" - THEN prove_match2 thy out_ts - THEN print_tac "after prove_match2 - last call:" + print_tac options "before prove_match2 - last call:" + THEN prove_match2 options thy out_ts + THEN print_tac options "after prove_match2 - last call:" THEN (etac @{thm singleE} 1) THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac HOL_basic_ss' 1) THEN (REPEAT_DETERM (etac @{thm Pair_inject} 1)) THEN (asm_full_simp_tac HOL_basic_ss' 1) - THEN SOLVED (print_tac "state before applying intro rule:" + THEN SOLVED (print_tac options "state before applying intro rule:" THEN (rtac pred_intro_rule 1) (* How to handle equality correctly? *) - THEN (print_tac "state before assumption matching") + THEN (print_tac options "state before assumption matching") THEN (REPEAT (atac 1 ORELSE (CHANGED (asm_full_simp_tac (HOL_basic_ss' addsimps [@{thm split_eta}, @{thm "split_beta"}, @{thm "fst_conv"}, @{thm "snd_conv"}, @{thm pair_collapse}]) 1) - THEN print_tac "state after simp_tac:")))) + THEN print_tac options "state after simp_tac:")))) | prove_prems2 out_ts ((p, deriv) :: ps) = let val mode = head_mode_of deriv @@ -2269,7 +2265,7 @@ val (_, out_ts''') = split_mode mode us val rec_tac = prove_prems2 out_ts''' ps in - (prove_expr2 thy (t, deriv)) THEN rec_tac + (prove_expr2 options thy (t, deriv)) THEN rec_tac end | Negprem t => let @@ -2280,14 +2276,14 @@ val param_derivations = param_derivations_of deriv val ho_args = ho_args_of mode args in - print_tac "before neg prem 2" + print_tac options "before neg prem 2" THEN etac @{thm bindE} 1 THEN (if is_some name then full_simp_tac (HOL_basic_ss addsimps [predfun_definition_of thy (the name) mode]) 1 THEN etac @{thm not_predE} 1 THEN simp_tac (HOL_basic_ss addsimps [@{thm not_False_eq_True}]) 1 - THEN (EVERY (map2 (prove_param2 thy) ho_args param_derivations)) + THEN (EVERY (map2 (prove_param2 options thy) ho_args param_derivations)) else etac @{thm not_predE'} 1) THEN rec_tac @@ -2295,20 +2291,20 @@ | Sidecond t => etac @{thm bindE} 1 THEN etac @{thm if_predE} 1 - THEN prove_sidecond2 thy t + THEN prove_sidecond2 options thy t THEN prove_prems2 [] ps) - in print_tac "before prove_match2:" - THEN prove_match2 thy out_ts - THEN print_tac "after prove_match2:" + in print_tac options "before prove_match2:" + THEN prove_match2 options thy out_ts + THEN print_tac options "after prove_match2:" THEN rest_tac end; val prems_tac = prove_prems2 in_ts ps in - print_tac "starting prove_clause2" + print_tac options "starting prove_clause2" THEN etac @{thm bindE} 1 THEN (etac @{thm singleE'} 1) THEN (TRY (etac @{thm Pair_inject} 1)) - THEN print_tac "after singleE':" + THEN print_tac options "after singleE':" THEN prems_tac end; @@ -2316,7 +2312,7 @@ let fun prove_clause clause i = (if i < length moded_clauses then etac @{thm supE} 1 else all_tac) - THEN (prove_clause2 thy pred mode clause i) + THEN (prove_clause2 options thy pred mode clause i) in (DETERM (TRY (rtac @{thm unit.induct} 1))) THEN (REPEAT_DETERM (CHANGED (rewtac @{thm split_paired_all}))) @@ -2338,11 +2334,11 @@ (if not (skip_proof options) then (fn _ => rtac @{thm pred_iffI} 1 - THEN print_tac' options "after pred_iffI" + THEN print_tac options "after pred_iffI" THEN prove_one_direction options thy clauses preds pred mode moded_clauses - THEN print_tac' options "proved one direction" + THEN print_tac options "proved one direction" THEN prove_other_direction options thy pred mode moded_clauses - THEN print_tac' options "proved other direction") + THEN print_tac options "proved other direction") else (fn _ => Skip_Proof.cheat_tac thy)) end; diff -r 7b39120a1494 -r f5422b736c44 src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Mar 22 08:30:13 2010 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Mon Mar 22 08:30:13 2010 +0100 @@ -181,8 +181,10 @@ val thy2 = Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) thy1 val (thy3, preproc_time) = cpu_time "predicate preprocessing" (fn () => Predicate_Compile.preprocess options const thy2) + (* FIXME: this is just for testing the predicate compiler proof procedure! *) + val thy3' = Predicate_Compile_Core.add_equations options [full_constname] thy3 val (thy4, core_comp_time) = cpu_time "random_dseq core compilation" - (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3) + (fn () => Predicate_Compile_Core.add_random_dseq_equations options [full_constname] thy3') val _ = Predicate_Compile_Core.print_all_modes Pos_Random_DSeq thy4 val modes = Predicate_Compile_Core.modes_of Pos_Random_DSeq thy4 full_constname val output_mode = fold_rev (curry Fun) (map (K Output) (binder_types constT)) Bool