# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 83951822bfd0ffe5c0d7c0b079dd31f951c8f0ba # Parent 9c01ee6f8ee958ff2d5100d789ca2ca8312fc4e9 cleaning the signature of the predicate compiler core; renaming signature and structures to uniform long names diff -r 9c01ee6f8ee9 -r 83951822bfd0 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML Sat Oct 24 16:55:42 2009 +0200 @@ -3,7 +3,7 @@ Book-keeping datastructure for the predicate compiler *) -signature PRED_COMPILE_DATA = +signature PREDICATE_COMPILE_DATA = sig type specification_table; val make_const_spec_table : theory -> specification_table @@ -12,7 +12,7 @@ val normalize_equation : theory -> thm -> thm end; -structure Pred_Compile_Data : PRED_COMPILE_DATA = +structure Predicate_Compile_Data : PREDICATE_COMPILE_DATA = struct open Predicate_Compile_Aux; @@ -119,7 +119,7 @@ fun normalize_equation thy th = mk_meta_equation th - |> Pred_Compile_Set.unfold_set_notation + |> Predicate_Compile_Set.unfold_set_notation |> full_fun_cong_expand |> split_all_pairs thy |> tap check_equation_format @@ -131,7 +131,7 @@ let val th = th |> inline_equations thy - |> Pred_Compile_Set.unfold_set_notation + |> Predicate_Compile_Set.unfold_set_notation |> AxClass.unoverload thy val (const, th) = if is_equationlike th then diff -r 9c01ee6f8ee9 -r 83951822bfd0 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 @@ -3,14 +3,14 @@ A quickcheck generator based on the predicate compiler *) -signature PRED_COMPILE_QUICKCHECK = +signature PREDICATE_COMPILE_QUICKCHECK = sig val quickcheck : Proof.context -> term -> int -> term list option val test_ref : ((unit -> int -> int * int -> term list Predicate.pred * (int * int)) option) Unsynchronized.ref end; -structure Pred_Compile_Quickcheck : PRED_COMPILE_QUICKCHECK = +structure Predicate_Compile_Quickcheck : PREDICATE_COMPILE_QUICKCHECK = struct val test_ref = @@ -85,7 +85,7 @@ mk_split_lambda (map Free vs') (mk_return (HOLogic.mk_list @{typ term} (map2 HOLogic.mk_term_of (map snd vs') (map Free vs')))))) val _ = tracing (Syntax.string_of_term ctxt' qc_term) - val compile = Code_ML.eval (SOME target) ("Pred_Compile_Quickcheck.test_ref", test_ref) + val compile = Code_ML.eval (SOME target) ("Predicate_Compile_Quickcheck.test_ref", test_ref) (fn proc => fn g => fn s => g s #>> (Predicate.map o map) proc) thy'' qc_term [] in diff -r 9c01ee6f8ee9 -r 83951822bfd0 src/HOL/Tools/Predicate_Compile/pred_compile_set.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_set.ML Sat Oct 24 16:55:42 2009 +0200 @@ -3,7 +3,7 @@ Preprocessing sets to predicates *) -signature PRED_COMPILE_SET = +signature PREDICATE_COMPILE_SET = sig (* val preprocess_intro : thm -> theory -> thm * theory @@ -12,7 +12,7 @@ val unfold_set_notation : thm -> thm; end; -structure Pred_Compile_Set : PRED_COMPILE_SET = +structure Predicate_Compile_Set : PREDICATE_COMPILE_SET = struct (*FIXME: unfolding Ball in pretty adhoc here *) val unfold_set_lemmas = [@{thm Collect_def}, @{thm mem_def}, diff -r 9c01ee6f8ee9 -r 83951822bfd0 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 @@ -41,7 +41,7 @@ let val _ = print_step options "Compiling predicates to flat introrules..." val specs = map (apsnd (map - (fn th => if is_equationlike th then Pred_Compile_Data.normalize_equation thy' th else th))) specs + (fn th => if is_equationlike th then Predicate_Compile_Data.normalize_equation thy' th else th))) specs val (intross1, thy'') = apfst flat (fold_map Predicate_Compile_Pred.preprocess specs thy') val _ = print_intross options thy'' "Flattened introduction rules: " intross1 val _ = print_step options "Replacing functions in introrules..." @@ -94,8 +94,8 @@ fun preprocess options const thy = let val _ = print_step options "Fetching definitions from theory..." - val table = Pred_Compile_Data.make_const_spec_table thy - val gr = Pred_Compile_Data.obtain_specification_graph thy table const + val table = Predicate_Compile_Data.make_const_spec_table thy + val gr = Predicate_Compile_Data.obtain_specification_graph thy table const val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr in fold_rev (preprocess_strong_conn_constnames options gr) (Graph.strong_conn gr) thy diff -r 9c01ee6f8ee9 -r 83951822bfd0 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 @@ -17,7 +17,6 @@ val is_registered : theory -> string -> bool val predfun_intro_of: theory -> string -> mode -> thm val predfun_elim_of: theory -> string -> mode -> thm - (* val strip_intro_concl: int -> term -> term * (term list * term list)*) val predfun_name_of: theory -> string -> mode -> string val all_preds_of : theory -> string list val modes_of: theory -> string -> mode list @@ -33,17 +32,13 @@ val set_nparams : string -> int -> theory -> theory val print_stored_rules: theory -> unit val print_all_modes: theory -> unit - val do_proofs: bool Unsynchronized.ref val mk_casesrule : Proof.context -> int -> thm list -> term - (* val analyze_compr: theory -> compfuns -> int option * bool -> term -> term*) val eval_ref : (unit -> term Predicate.pred) option Unsynchronized.ref val random_eval_ref : (unit -> int * int -> term Predicate.pred * (int * int)) option Unsynchronized.ref val add_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val code_pred_intros_attrib : attribute (* used by Quickcheck_Generator *) (* temporary for testing of the compilation *) - datatype indprem = Prem of term list * term | Negprem of term list * term | Sidecond of term | - GeneratorPrem of term list * term | Generator of (string * typ); datatype compilation_funs = CompilationFuns of { mk_predT : typ -> typ, dest_predT : typ -> typ, @@ -55,45 +50,14 @@ mk_not : term -> term, mk_map : typ -> typ -> term -> term -> term, lift_pred : term -> term - }; - type moded_clause = term list * (indprem * tmode) list - type 'a pred_mode_table = (string * (mode * 'a) list) list - val infer_modes : Predicate_Compile_Aux.options -> theory -> (string * mode list) list - -> (string * mode list) list - -> string list - -> (string * (term list * indprem list) list) list - -> (moded_clause list) pred_mode_table - val infer_modes_with_generator : Predicate_Compile_Aux.options -> theory -> (string * mode list) list - -> (string * mode list) list - -> string list - -> (string * (term list * indprem list) list) list - -> (moded_clause list) pred_mode_table - (*val compile_preds : theory -> compilation_funs -> string list -> string list - -> (string * typ) list -> (moded_clause list) pred_mode_table -> term pred_mode_table - val rpred_create_definitions :(string * typ) list -> string * mode list - -> theory -> theory - val split_smode : int list -> term list -> (term list * term list) *) + }; val pred_compfuns : compilation_funs val rpred_compfuns : compilation_funs - val dest_funT : typ -> typ * typ - (* val depending_preds_of : theory -> thm list -> string list *) val add_quickcheck_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory val add_depth_limited_equations : Predicate_Compile_Aux.options -> string list -> theory -> theory - val is_inductive_predicate : theory -> string -> bool - val terms_vs : term list -> string list - val subsets : int -> int -> int list list - val check_mode_clause : bool -> theory -> string list -> - (string * mode list) list -> (string * mode list) list -> mode -> (term list * indprem list) - -> (term list * (indprem * tmode) list) option - val string_of_moded_prem : theory -> (indprem * tmode) -> string + (*val is_inductive_predicate : theory -> string -> bool*) val all_modes_of : theory -> (string * mode list) list val all_generator_modes_of : theory -> (string * mode list) list - val preprocess_intro : theory -> thm -> thm - val is_constrt : theory -> term -> bool - val is_predT : typ -> bool - val guess_nparams : typ -> int - val cprods_subset : 'a list list -> 'a list list - val dest_prem : theory -> term list -> term -> indprem end; structure Predicate_Compile_Core : PREDICATE_COMPILE_CORE = @@ -113,8 +77,6 @@ fun debug_tac msg = Seq.single; (* (fn st => (Output.tracing msg; Seq.single st)); *) -val do_proofs = Unsynchronized.ref true; - datatype assertion = Max_number_of_subgoals of int fun assert_tac (Max_number_of_subgoals i) st = if (nprems_of st <= i) then Seq.single st @@ -1515,7 +1477,8 @@ $ compilation else let - val compilation_without_depth_limit = foldr1 (mk_sup compfuns) + 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 diff -r 9c01ee6f8ee9 -r 83951822bfd0 src/HOL/ex/Predicate_Compile.thy --- a/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile.thy Sat Oct 24 16:55:42 2009 +0200 @@ -12,6 +12,6 @@ begin setup {* Predicate_Compile.setup *} -setup {* Quickcheck.add_generator ("pred_compile", Pred_Compile_Quickcheck.quickcheck) *} +setup {* Quickcheck.add_generator ("pred_compile", Predicate_Compile_Quickcheck.quickcheck) *} end \ No newline at end of file diff -r 9c01ee6f8ee9 -r 83951822bfd0 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 @@ -8,16 +8,17 @@ | "odd n \ even (Suc n)" code_pred (mode: [], [1]) [show_steps] even . -code_pred [depth_limited] even . -code_pred [rpred] even . +code_pred [depth_limited, show_compilation] even . +(*code_pred [rpred] even .*) thm odd.equation thm even.equation thm odd.depth_limited_equation thm even.depth_limited_equation +(* thm even.rpred_equation thm odd.rpred_equation - +*) (* lemma unit: "unit_case f = (\x. f)" apply (rule ext) @@ -82,17 +83,17 @@ code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) [inductify] append . code_pred [depth_limited] append . -code_pred [rpred] append . +(*code_pred [rpred] append .*) thm append.equation thm append.depth_limited_equation -thm append.rpred_equation +(*thm append.rpred_equation*) values "{(ys, xs). append xs ys [0, Suc 0, 2]}" values "{zs. append [0, Suc 0, 2] [17, 8] zs}" values "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" values [depth_limit = 3] "{(xs, ys). append xs ys [1, 2, 3, 4, (5::nat)]}" -values [depth_limit = 10 random] 15 "{(ys, zs). append [1::nat, 2] ys zs}" +(*values [depth_limit = 10 random] 15 "{(ys, zs). append [1::nat, 2] ys zs}"*) value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" @@ -130,7 +131,7 @@ | "tupled_append (xs, ys, zs) \ tupled_append (x # xs, ys, x # zs)" code_pred tupled_append . -code_pred [rpred] tupled_append . +(*code_pred [rpred] tupled_append .*) thm tupled_append.equation (* TODO: values with tupled modes @@ -198,8 +199,8 @@ | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . -code_pred [depth_limited] partition . -thm partition.depth_limited_equation +(*code_pred [depth_limited] partition .*) +(*thm partition.depth_limited_equation*) (*code_pred [rpred] partition .*) inductive tupled_partition :: "('a \ bool) \ ('a list \ 'a list \ 'a list) \ bool" @@ -258,9 +259,9 @@ | "succ m n \ succ (Suc m) (Suc n)" code_pred succ . -code_pred [rpred] succ . +(*code_pred [rpred] succ .*) thm succ.equation -thm succ.rpred_equation +(*thm succ.rpred_equation*) values 10 "{(m, n). succ n m}" values "{m. succ 0 m}" @@ -384,7 +385,7 @@ *) thm lexord_def code_pred [inductify] lexord . -code_pred [inductify, rpred] lexord . +(*code_pred [inductify, rpred] lexord .*) thm lexord.equation inductive less_than_nat :: "nat * nat => bool" where @@ -393,25 +394,25 @@ code_pred less_than_nat . code_pred [depth_limited] less_than_nat . -code_pred [rpred] less_than_nat . +(*code_pred [rpred] less_than_nat .*) inductive test_lexord :: "nat list * nat list => bool" where "lexord less_than_nat (xs, ys) ==> test_lexord (xs, ys)" -code_pred [rpred] test_lexord . +(*code_pred [rpred] test_lexord .*) code_pred [depth_limited] test_lexord . thm test_lexord.depth_limited_equation -thm test_lexord.rpred_equation +(*thm test_lexord.rpred_equation*) -values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}" +(*values [depth_limit = 5] "{x. test_lexord ([1, 2, 3], [1, 2, 5])}"*) -values [depth_limit = 25 random] "{xys. test_lexord xys}" +(*values [depth_limit = 25 random] "{xys. test_lexord xys}"*) -values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}" -ML {* Predicate_Compile_Core.do_proofs := false *} +(*values [depth_limit = 5 random] "{xy. lexord less_than_nat xy}"*) + lemma "(u, v) : lexord less_than_nat ==> (x @ u, y @ v) : lexord less_than_nat" -quickcheck[generator=pred_compile] +(*quickcheck[generator=pred_compile]*) oops lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv @@ -419,9 +420,9 @@ code_pred [inductify] lexn . thm lexn.equation *) -code_pred [inductify, rpred] lexn . +(*code_pred [inductify, rpred] lexn .*) -thm lexn.rpred_equation +(*thm lexn.rpred_equation*) code_pred [inductify] lenlex . thm lenlex.equation @@ -450,15 +451,15 @@ code_pred [inductify] avl . thm avl.equation *) -code_pred [inductify, rpred] avl . +(*code_pred [inductify, rpred] avl . 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 = {}" @@ -470,10 +471,9 @@ | "is_ord (MKT n l r h) = ((\n' \ set_of l. n' < n) \ (\n' \ set_of r. n < n') \ is_ord l \ is_ord r)" -code_pred [inductify] set_of . +code_pred (mode: [1], [1, 2]) [inductify] set_of . thm set_of.equation -text {* expected mode: [1], [1, 2] *} (* FIXME *) (* code_pred (inductify_all) is_ord . @@ -491,11 +491,11 @@ code_pred [inductify] length . thm size_listP.equation - +(* code_pred [inductify, rpred] length . thm size_listP.rpred_equation values [depth_limit = 10 random] 20 "{xs. size_listP (xs::nat list) (5::nat)}" - +*) code_pred [inductify] concat . thm concatP.equation @@ -548,12 +548,12 @@ | "w \ S\<^isub>1 \ b # w \ S\<^isub>1" | "\v \ B\<^isub>1; v \ B\<^isub>1\ \ a # v @ w \ B\<^isub>1" -code_pred [inductify, rpred] S\<^isub>1p . +code_pred [inductify] S\<^isub>1p . thm S\<^isub>1p.equation -thm S\<^isub>1p.rpred_equation +(*thm S\<^isub>1p.rpred_equation*) -values [depth_limit = 5 random] "{x. S\<^isub>1p x}" +(*values [depth_limit = 5 random] "{x. S\<^isub>1p x}"*) inductive is_a where "is_a a" @@ -568,31 +568,36 @@ 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}" +(*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.intros thm filterP.equation values [depth_limit=3] "{x. filterP is_b [a, b] x}"