# HG changeset patch # User haftmann # Date 1257264537 -3600 # Node ID 22be9021cf7431c1a260d2c7b902a4f217913f9d # Parent 5c1928d5db38c309b03aef388f2a0e07b740691e# Parent 3789fe962a08adbbe70c071eb53cc205d3da01fa merged diff -r 3789fe962a08 -r 22be9021cf74 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Nov 03 17:06:35 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Tue Nov 03 17:08:57 2009 +0100 @@ -37,6 +37,9 @@ map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n" ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs +(* TODO: *) +fun overload_const thy s = s + fun map_specs f specs = map (fn (s, ths) => (s, f ths)) specs @@ -59,15 +62,14 @@ val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'') val (new_intross, thy'''') = if not (null new_defs) then - let - val _ = print_step options "Recursively obtaining introduction rules for new definitions..." - in process_specification options new_defs thy''' end - else ([], thy''') + let + val _ = print_step options "Recursively obtaining introduction rules for new definitions..." + in process_specification options new_defs thy''' end + else ([], thy''') in (intross3 @ new_intross, thy'''') end - fun preprocess_strong_conn_constnames options gr constnames thy = let val get_specs = map (fn k => (k, Graph.get_node gr k)) @@ -85,7 +87,7 @@ val _ = print_intross options thy''' "Introduction rules with new constants: " intross3 val intross4 = map_specs (maps remove_pointless_clauses) intross3 val _ = print_intross options thy''' "After removing pointless clauses: " intross4 - (*val intross5 = map (fn s, ths) => ( s, map (AxClass.overload thy''') ths)) intross4*) + val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4 val intross6 = map_specs (map (expand_tuples thy''')) intross4 val _ = print_intross options thy''' "introduction rules before registering: " intross6 val _ = print_step options "Registering introduction rules..." @@ -97,7 +99,7 @@ fun preprocess options const thy = let val _ = print_step options "Fetching definitions from theory..." - val table = Predicate_Compile_Data.make_const_spec_table thy + val table = Predicate_Compile_Data.make_const_spec_table options thy val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr in fold_rev (preprocess_strong_conn_constnames options gr) diff -r 3789fe962a08 -r 22be9021cf74 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Nov 03 17:06:35 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Tue Nov 03 17:08:57 2009 +0100 @@ -7,7 +7,7 @@ signature PREDICATE_COMPILE_DATA = sig type specification_table; - val make_const_spec_table : theory -> specification_table + val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table val get_specification : specification_table -> string -> thm list val obtain_specification_graph : Predicate_Compile_Aux.options -> theory -> specification_table -> string -> thm list Graph.T @@ -126,14 +126,22 @@ |> split_all_pairs thy |> tap check_equation_format -fun inline_equations thy th = Conv.fconv_rule - (Simplifier.rewrite ((Simplifier.theory_context thy Simplifier.empty_ss) - addsimps (Predicate_Compile_Inline_Defs.get (ProofContext.init thy)))) th +fun inline_equations options thy th = + let + val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy) + val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th + (*val _ = print_step options + ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th)) + ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs)) + ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*) + in + th' + end -fun store_thm_in_table ignore_consts thy th= +fun store_thm_in_table options ignore_consts thy th= let val th = th - |> inline_equations thy + |> inline_equations options thy |> Predicate_Compile_Set.unfold_set_notation |> AxClass.unoverload thy val (const, th) = @@ -151,9 +159,9 @@ else I end -fun make_const_spec_table thy = +fun make_const_spec_table options thy = let - fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) + fun store ignore_const f = fold (store_thm_in_table options ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy))) val table = Symtab.empty |> store [] Predicate_Compile_Alternative_Defs.get val ignore_consts = Symtab.keys table diff -r 3789fe962a08 -r 22be9021cf74 src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Nov 03 17:06:35 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML Tue Nov 03 17:08:57 2009 +0100 @@ -141,7 +141,6 @@ fun process constname atom (new_defs, thy) = let val (pred, args) = strip_comb atom - val abs_args = filter is_Abs args fun replace_abs_arg (abs_arg as Abs _ ) (new_defs, thy) = let val vars = map Var (Term.add_vars abs_arg []) @@ -160,7 +159,12 @@ in (list_comb (Logic.varify const, vars), ((full_constname, [definition])::new_defs, thy')) end - | replace_abs_arg arg (new_defs, thy) = (arg, (new_defs, thy)) + | replace_abs_arg arg (new_defs, thy) = + if (is_predT (fastype_of arg)) then + process constname arg (new_defs, thy) + else + (arg, (new_defs, thy)) + val (args', (new_defs', thy')) = fold_map replace_abs_arg args (new_defs, thy) in (list_comb (pred, args'), (new_defs', thy')) diff -r 3789fe962a08 -r 22be9021cf74 src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy --- a/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Nov 03 17:06:35 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_Quickcheck_ex.thy Tue Nov 03 17:08:57 2009 +0100 @@ -5,6 +5,31 @@ section {* Sets *} +lemma "x \ {(1::nat)} ==> False" +quickcheck[generator=predicate_compile] +oops + +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x \ Suc 0" +oops + +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x = Suc 0" +quickcheck[generator=predicate_compile] +oops + +lemma "x \ {Suc 0, Suc (Suc 0)} ==> x <= Suc 0" +quickcheck[generator=predicate_compile] +oops + +section {* Numerals *} + +lemma + "x \ {1, 2, (3::nat)} ==> x < 3" +(*quickcheck[generator=predicate_compile]*) +oops +lemma + "x \ {1, 2} \ {3, 4} ==> x > 4" +(*quickcheck[generator=predicate_compile]*) +oops section {* Context Free Grammar *} diff -r 3789fe962a08 -r 22be9021cf74 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Tue Nov 03 17:06:35 2009 +0100 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Tue Nov 03 17:08:57 2009 +0100 @@ -153,12 +153,12 @@ definition "equals == (op =)" -inductive zerozero' where +inductive zerozero' :: "nat * nat => bool" where "equals (x, y) (0, 0) ==> zerozero' (x, y)" code_pred (mode: [1]) zerozero' . -lemma zerozero'_eq: "zerozero' == zerozero" +lemma zerozero'_eq: "zerozero' x == zerozero x" proof - have "zerozero' = zerozero" apply (auto simp add: mem_def) @@ -167,7 +167,7 @@ apply (cases rule: zerozero.cases) apply (auto simp add: equals_def intro: zerozero'.intros) done - from this show "zerozero' == zerozero" by auto + from this show "zerozero' x == zerozero x" by auto qed declare zerozero'_eq [code_pred_inline] @@ -175,9 +175,27 @@ definition "zerozero'' x == zerozero' x" text {* if preprocessing fails, zerozero'' will not have all modes. *} -ML {* Predicate_Compile_Inline_Defs.get @{context} *} -(* TODO: *) -code_pred (mode: [1]) [inductify, show_intermediate_results] zerozero'' . + +code_pred (mode: [o], [(i, o)], [(o,i)], [i]) [inductify] zerozero'' . + +subsection {* Numerals *} + +definition + "one_or_two == {Suc 0, (Suc (Suc 0))}" + +(*code_pred [inductify] one_or_two .*) +code_pred [inductify, random] one_or_two . +(*values "{x. one_or_two x}"*) +values [random] "{x. one_or_two x}" + +definition one_or_two': + "one_or_two' == {1, (2::nat)}" + +code_pred [inductify] one_or_two' . +thm one_or_two'.equation +(* TODO: handling numerals *) +(*values "{x. one_or_two' x}"*) + subsection {* even predicate *} @@ -666,12 +684,12 @@ subsection {* Inverting list functions *} -code_pred [inductify] length . +code_pred [inductify, show_intermediate_results] length . code_pred [inductify, random] length . thm size_listP.equation thm size_listP.random_equation -values [random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" +(*values [random] 1 "{xs. size_listP (xs::nat list) (5::nat)}"*) code_pred [inductify] concat . code_pred [inductify] hd .