--- 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)
--- 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
--- 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'))
--- 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 \<in> {(1::nat)} ==> False"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x \<noteq> Suc 0"
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x = Suc 0"
+quickcheck[generator=predicate_compile]
+oops
+
+lemma "x \<in> {Suc 0, Suc (Suc 0)} ==> x <= Suc 0"
+quickcheck[generator=predicate_compile]
+oops
+
+section {* Numerals *}
+
+lemma
+ "x \<in> {1, 2, (3::nat)} ==> x < 3"
+(*quickcheck[generator=predicate_compile]*)
+oops
+lemma
+ "x \<in> {1, 2} \<union> {3, 4} ==> x > 4"
+(*quickcheck[generator=predicate_compile]*)
+oops
section {* Context Free Grammar *}
--- 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 .