# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 9c01ee6f8ee958ff2d5100d789ca2ca8312fc4e9 # Parent e2e23987c59ac17aaf4f56606b8a66a3ff7a683c added skip_proof option; playing with compilation of depth-limited predicates diff -r e2e23987c59a -r 9c01ee6f8ee9 src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML Sat Oct 24 16:55:42 2009 +0200 @@ -138,6 +138,8 @@ show_mode_inference : bool, show_proof_trace : bool, show_intermediate_results : bool, + show_compilation : bool, + skip_proof : bool, inductify : bool, rpred : bool, @@ -149,6 +151,8 @@ fun show_mode_inference (Options opt) = #show_mode_inference opt fun show_intermediate_results (Options opt) = #show_intermediate_results opt fun show_proof_trace (Options opt) = #show_proof_trace opt +fun show_compilation (Options opt) = #show_compilation opt +fun skip_proof (Options opt) = #skip_proof opt fun is_inductify (Options opt) = #inductify opt fun is_rpred (Options opt) = #rpred opt @@ -160,6 +164,9 @@ show_intermediate_results = false, show_proof_trace = false, show_mode_inference = false, + show_compilation = false, + skip_proof = false, + inductify = false, rpred = false, depth_limited = false @@ -169,7 +176,6 @@ fun print_step options s = if show_steps options then tracing s else () - (* tuple processing *) fun expand_tuples thy intro = diff -r e2e23987c59a -r 9c01ee6f8ee9 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML Sat Oct 24 16:55:42 2009 +0200 @@ -65,7 +65,7 @@ |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) |> Predicate_Compile.preprocess Predicate_Compile_Aux.default_options full_constname |> Predicate_Compile_Core.add_equations Predicate_Compile_Aux.default_options [full_constname] - |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname] + (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) |> Predicate_Compile_Core.add_quickcheck_equations Predicate_Compile_Aux.default_options [full_constname] val depth_limited_modes = Predicate_Compile_Core.depth_limited_modes_of thy'' full_constname val modes = Predicate_Compile_Core.generator_modes_of thy'' full_constname diff -r e2e23987c59a -r 9c01ee6f8ee9 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -11,7 +11,7 @@ struct (* options *) -val fail_safe_mode = false +val fail_safe_mode = true open Predicate_Compile_Aux; @@ -111,6 +111,8 @@ show_intermediate_results = chk "show_intermediate_results", show_proof_trace = chk "show_proof_trace", show_mode_inference = chk "show_mode_inference", + show_compilation = chk "show_compilation", + skip_proof = chk "skip_proof", inductify = chk "inductify", rpred = chk "rpred", depth_limited = chk "depth_limited" @@ -141,7 +143,7 @@ val setup = Predicate_Compile_Fun.setup_oracle #> Predicate_Compile_Core.setup val bool_options = ["show_steps", "show_intermediate_results", "show_proof_trace", - "show_mode_inference", "inductify", "rpred", "depth_limited"] + "show_mode_inference", "show_compilation", "skip_proof", "inductify", "rpred", "depth_limited"] val _ = List.app OuterKeyword.keyword ("mode" :: bool_options) diff -r e2e23987c59a -r 9c01ee6f8ee9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -73,10 +73,6 @@ val rpred_create_definitions :(string * typ) list -> string * mode list -> theory -> theory val split_smode : int list -> term list -> (term list * term list) *) - val print_moded_clauses : - theory -> (moded_clause list) pred_mode_table -> unit - val print_compiled_terms : theory -> term pred_mode_table -> unit - (*val rpred_prove_preds : theory -> term pred_mode_table -> thm pred_mode_table*) val pred_compfuns : compilation_funs val rpred_compfuns : compilation_funs val dest_funT : typ -> typ * typ @@ -111,6 +107,7 @@ fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); fun print_tac s = Seq.single; + fun print_tac' options s = if show_proof_trace options then Tactical.print_tac s else Seq.single; @@ -438,9 +435,11 @@ (map (string_of_prem thy) prems)) ^ " --> " ^ pred ^ " " ^ (space_implode " " (map (Syntax.string_of_term_global thy) ts)) -fun print_compiled_terms thy = - print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy - +fun print_compiled_terms options thy = + if show_compilation options then + print_pred_mode_table (fn _ => fn _ => Syntax.string_of_term_global thy) thy + else K () + fun print_stored_rules thy = let val preds = (Graph.keys o PredData.get) thy @@ -1294,8 +1293,6 @@ let val params' = map (compile_param depth_limited thy compfuns mk_fun_of) (ms ~~ params) (*val mk_fun_of = if depth_limited then mk_depth_limited_fun_of else mk_fun_of*) - val _ = if mode = ([], [(0, NONE)]) then error "something is wrong" else () - val _ = Output.tracing ("compile_expr mode: " ^ string_of_mode mode) in (*lift_pred compfuns*)(list_comb (mk_fun_of compfuns thy (name, T) mode, params' @ inargs)) end @@ -1475,7 +1472,7 @@ mk_bind compfuns (mk_single compfuns inp, prem_t) end -fun compile_pred compfuns mk_fun_of depth_limited thy all_vs param_vs s T mode moded_cls = +fun compile_pred compfuns mk_fun_of' depth_limited thy all_vs param_vs s T mode moded_cls = let val (Ts1, Ts2) = chop (length (fst mode)) (binder_types T) val (Us1, Us2) = split_smodeT (snd mode) Ts2 @@ -1504,20 +1501,30 @@ else NONE val cl_ts = - map (compile_clause compfuns mk_fun_of decr_depth + map (compile_clause compfuns mk_fun_of' decr_depth thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls; val compilation = foldr1 (mk_sup compfuns) cl_ts val T' = mk_predT compfuns (mk_tupleT Us2) val if_const = Const (@{const_name "If"}, @{typ bool} --> T' --> T' --> T') val full_mode = null Us2 - val depth_compilation = - if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) - $ (if full_mode then - if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $ mk_single compfuns HOLogic.unit - else - mk_bot compfuns (dest_predT compfuns T')) - $ compilation - val fun_const = mk_fun_of compfuns thy (s, T) mode + val depth_compilation = + if full_mode then + if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) + $ (if_const $ polarity $ mk_bot compfuns (dest_predT compfuns T') $ + mk_single compfuns HOLogic.unit) + $ compilation + else + let + val compilation_without_depth_limit = foldr1 (mk_sup compfuns) + (map (compile_clause compfuns mk_fun_of NONE + thy all_vs param_vs mode (mk_tuple in_ts)) moded_cls) + in + if_const $ polarity $ + (if_const $ HOLogic.mk_eq (depth, @{term "0 :: code_numeral"}) $ + mk_bot compfuns (dest_predT compfuns T') $ compilation) + $ compilation_without_depth_limit + end + val fun_const = mk_fun_of' compfuns thy (s, T) mode val eq = if depth_limited then (list_comb (fun_const, params @ in_ts @ [polarity, depth]), depth_compilation) else @@ -1733,7 +1740,6 @@ val T = AList.lookup (op =) preds name |> the fun create_definition mode thy = let - val _ = Output.tracing ("mode: " ^ string_of_mode mode) val mode_cname = create_constname_of_mode thy "gen_" name mode val funT = generator_funT_of mode T in @@ -2121,7 +2127,7 @@ val clauses = the (AList.lookup (op =) clauses pred) in Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term - (if !do_proofs then + (if skip_proof options then (fn _ => rtac @{thm pred_iffI} 1 THEN print_tac' options "after pred_iffI" @@ -2284,14 +2290,14 @@ val modes = map (fn (p, mps) => (p, map fst mps)) moded_clauses val _ = check_expected_modes options modes val _ = print_modes modes - val _ = print_moded_clauses thy moded_clauses + (*val _ = print_moded_clauses thy moded_clauses*) val _ = print_step options "Defining executable functions..." val thy' = fold (#create_definitions steps preds) modes thy |> Theory.checkpoint val _ = print_step options "Compiling equations..." val compiled_terms = (#compile_preds steps) thy' all_vs param_vs preds moded_clauses - val _ = print_compiled_terms thy' compiled_terms + val _ = print_compiled_terms options thy' compiled_terms val _ = print_step options "Proving equations..." val result_thms = #prove steps options thy' clauses preds (extra_modes @ modes) moded_clauses compiled_terms diff -r e2e23987c59a -r 9c01ee6f8ee9 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -409,15 +409,19 @@ values [depth_limit = 25 random] "{xys. test_lexord xys}" values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}" - -lemma "(u, v) : lexord r ==> (x @ u, y @ v) : lexord r" +ML {* Predicate_Compile_Core.do_proofs := false *} +lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat" quickcheck[generator=pred_compile] oops lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv - +(* code_pred [inductify] lexn . thm lexn.equation +*) +code_pred [inductify, rpred] lexn . + +thm lexn.rpred_equation code_pred [inductify] lenlex . thm lenlex.equation @@ -447,9 +451,14 @@ thm avl.equation *) code_pred [inductify, rpred] avl . -find_theorems "avl_aux" thm avl.rpred_equation values [depth_limit = 50 random] 10 "{t. avl (t::int tree)}" + +lemma "avl t ==> t = ET" +quickcheck[generator=code] +quickcheck[generator = pred_compile] +oops + fun set_of where "set_of ET = {}" @@ -546,12 +555,73 @@ values [depth_limit = 5 random] "{x. S\<^isub>1p x}" +inductive is_a where +"is_a a" + +inductive is_b where + "is_b b" + +code_pred is_a . +code_pred [depth_limited] is_a . +code_pred [rpred] is_a . + +values [depth_limit=5 random] "{x. is_a x}" +code_pred [rpred] is_b . + +code_pred [rpred] filterP . +values [depth_limit=5 random] "{x. filterP is_a [a, b] x}" +values [depth_limit=3 random] "{x. filterP is_b [a, b] x}" + +lemma "w \ S\<^isub>1 \ length (filter (\x. x = a) w) = 1" +quickcheck[generator=pred_compile, size=10] +oops + +inductive test_lemma where + "S\<^isub>1p w ==> filterP is_a w r1 ==> size_listP r1 r2 ==> filterP is_b w r3 ==> size_listP r3 r4 ==> r2 \ r4 ==> test_lemma w" + +code_pred [rpred] test_lemma . + +definition test_lemma' where + "test_lemma' w == (w \ S\<^isub>1 \ (\ length [x <- w. x = a] = length [x <- w. x = b]))" + +code_pred [inductify, rpred] test_lemma' . +thm test_lemma'.rpred_equation +(*thm test_lemma'.rpred_equation*) +(* +values [depth_limit=3 random] "{x. S\<^isub>1 x}" +*) +code_pred [depth_limited] is_b . +code_pred [inductify, depth_limited] filter . +thm filterP.intros +thm filterP.equation + +values [depth_limit=3] "{x. filterP is_b [a, b] x}" +find_theorems "test_lemma'_hoaux" +code_pred [depth_limited] test_lemma'_hoaux . +thm test_lemma'_hoaux.depth_limited_equation +values [depth_limit=2] "{x. test_lemma'_hoaux b}" +inductive test1 where + "\ test_lemma'_hoaux x ==> test1 x" +code_pred test1 . +code_pred [depth_limited] test1 . +thm test1.depth_limited_equation +thm test_lemma'_hoaux.depth_limited_equation +thm test1.intros + +values [depth_limit=2] "{x. test1 b}" + +thm filterP.intros +thm filterP.depth_limited_equation +values [depth_limit=3] "{x. filterP test_lemma'_hoaux [a, b] x}" +values [depth_limit=4 random] "{w. test_lemma w}" +values [depth_limit=4 random] "{w. test_lemma' w}" theorem S\<^isub>1_sound: -"w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=pred_compile]*) +"w \ S\<^isub>1p \ length [x \ w. x = a] = length [x \ w. x = b]" +quickcheck[generator=pred_compile, size=5] oops + inductive_set S\<^isub>2 and A\<^isub>2 and B\<^isub>2 where "[] \ S\<^isub>2" | "w \ A\<^isub>2 \ b # w \ S\<^isub>2" @@ -565,12 +635,12 @@ thm A\<^isub>2.rpred_equation thm B\<^isub>2.rpred_equation -values [depth_limit = 10 random] "{x. S\<^isub>2 x}" +values [depth_limit = 4 random] "{x. S\<^isub>2 x}" theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" (*quickcheck[generator=SML]*) -(*quickcheck[generator=pred_compile, size=15, iterations=100]*) +quickcheck[generator=pred_compile, size=4, iterations=1] oops inductive_set S\<^isub>3 and A\<^isub>3 and B\<^isub>3 where @@ -588,7 +658,7 @@ theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" -(*quickcheck[generator=pred_compile, size=10, iterations=1]*) +quickcheck[generator=pred_compile, size=10, iterations=1] oops lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])"