# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 5378e61add1a1fd4d0ebe4699c8bb1abdd47bbeb # Parent 3c7c4372f9adbcfe94496dc45b85bd1173da10a6 continued cleaning up; moved tuple expanding to core diff -r 3c7c4372f9ad -r 5378e61add1a 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 @@ -137,4 +137,57 @@ if is_show_steps options then tracing s else () +(* tuple processing *) + +fun expand_tuples thy intro = + let + fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) + | rewrite_args (arg::args) (pats, intro_t, ctxt) = + (case HOLogic.strip_tupleT (fastype_of arg) of + (Ts as _ :: _ :: _) => + let + fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) + (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) + | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = + let + val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt + val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) + val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t + val args' = map (Pattern.rewrite_term thy [pat] []) args + in + rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) + end + | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) + val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) + (args, (pats, intro_t, ctxt)) + in + rewrite_args args' (pats, intro_t', ctxt') + end + | _ => rewrite_args args (pats, intro_t, ctxt)) + fun rewrite_prem atom = + let + val (_, args) = strip_comb atom + in rewrite_args args end + val ctxt = ProofContext.init thy + val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt + val intro_t = prop_of intro' + val concl = Logic.strip_imp_concl intro_t + val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) + val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) + val (pats', intro_t', ctxt3) = + fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) + fun rewrite_pat (ct1, ct2) = + (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) + val t_insts' = map rewrite_pat t_insts + val intro'' = Thm.instantiate (T_insts, t_insts') intro + val [intro'''] = Variable.export ctxt3 ctxt [intro''] + val intro'''' = Simplifier.full_simplify + (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) + intro''' + in + intro'''' + end + + + end; diff -r 3c7c4372f9ad -r 5378e61add1a 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 @@ -17,71 +17,6 @@ val priority = tracing; -(* tuple processing *) - -fun expand_tuples thy intro = - let - fun rewrite_args [] (pats, intro_t, ctxt) = (pats, intro_t, ctxt) - | rewrite_args (arg::args) (pats, intro_t, ctxt) = - (case HOLogic.strip_tupleT (fastype_of arg) of - (Ts as _ :: _ :: _) => - let - fun rewrite_arg' (Const ("Pair", _) $ _ $ t2, Type ("*", [_, T2])) - (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt)) - | rewrite_arg' (t, Type ("*", [T1, T2])) (args, (pats, intro_t, ctxt)) = - let - val ([x, y], ctxt') = Variable.variant_fixes ["x", "y"] ctxt - val pat = (t, HOLogic.mk_prod (Free (x, T1), Free (y, T2))) - (*val _ = tracing ("Rewriting term " ^ - (Syntax.string_of_term_global thy (fst pat)) ^ " to " ^ - (Syntax.string_of_term_global thy (snd pat)) ^ " in " ^ - (Syntax.string_of_term_global thy intro_t))*) - val intro_t' = Pattern.rewrite_term thy [pat] [] intro_t - val args' = map (Pattern.rewrite_term thy [pat] []) args - in - rewrite_arg' (Free (y, T2), T2) (args', (pat::pats, intro_t', ctxt')) - end - | rewrite_arg' _ (args, (pats, intro_t, ctxt)) = (args, (pats, intro_t, ctxt)) - val (args', (pats, intro_t', ctxt')) = rewrite_arg' (arg, fastype_of arg) - (args, (pats, intro_t, ctxt)) - in - rewrite_args args' (pats, intro_t', ctxt') - end - | _ => rewrite_args args (pats, intro_t, ctxt)) - fun rewrite_prem atom = - let - val (_, args) = strip_comb atom - in rewrite_args args end - val ctxt = ProofContext.init thy - val (((T_insts, t_insts), [intro']), ctxt1) = Variable.import false [intro] ctxt - val intro_t = prop_of intro' - val concl = Logic.strip_imp_concl intro_t - val (p, args) = strip_comb (HOLogic.dest_Trueprop concl) - val (pats', intro_t', ctxt2) = rewrite_args args ([], intro_t, ctxt1) - val (pats', intro_t', ctxt3) = - fold_atoms rewrite_prem intro_t' (pats', intro_t', ctxt2) - (*val _ = Output.tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t')) - val _ = Output.tracing ("pats : " ^ (commas (map - (fn (t1, t2) => (Syntax.string_of_term_global thy t1) ^ " -> " ^ - Syntax.string_of_term_global thy t2) pats'))*) - fun rewrite_pat (ct1, ct2) = - (ct1, cterm_of thy (Pattern.rewrite_term thy pats' [] (term_of ct2))) - val t_insts' = map rewrite_pat t_insts - (*val _ = Output.tracing ("t_insts':" ^ (commas (map - (fn (ct1, ct2) => (Syntax.string_of_term_global thy (term_of ct1) ^ " -> " ^ - Syntax.string_of_term_global thy (term_of ct2))) t_insts')))*) - val intro'' = Thm.instantiate (T_insts, t_insts') intro - (*val _ = Output.tracing ("intro'':" ^ (Display.string_of_thm_global thy intro''))*) - val [intro'''] = Variable.export ctxt3 ctxt [intro''] - (*val _ = Output.tracing ("intro''':" ^ (Display.string_of_thm_global thy intro'''))*) - in - intro''' - end - - (* eliminating fst/snd functions *) -val simplify_fst_snd = Simplifier.full_simplify - (HOL_basic_ss addsimps [@{thm fst_conv}, @{thm snd_conv}, @{thm Pair_eq}]) - (* Some last processing *) fun remove_pointless_clauses intro = @@ -145,8 +80,8 @@ val _ = print_intross thy''' "Introduction rules with new constants: " intross3 val intross4 = map (maps remove_pointless_clauses) intross3 val _ = print_intross thy''' "After removing pointless clauses: " intross4 - val intross5 = burrow (map (AxClass.overload thy''')) intross4 - val intross6 = burrow (map (simplify_fst_snd o expand_tuples thy''')) intross5 + val intross5 = map (map (AxClass.overload thy''')) intross4 + val intross6 = burrow (map (expand_tuples thy''')) intross5 val _ = print_intross thy''' "introduction rules before registering: " intross6 val _ = print_step options "Registering introduction rules..." val thy'''' = fold Predicate_Compile_Core.register_intros intross6 thy''' diff -r 3c7c4372f9ad -r 5378e61add1a 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 @@ -592,6 +592,8 @@ ([intro], elim) end +fun expand_tuples_elim th = th + fun fetch_pred_data thy name = case try (Inductive.the_inductive (ProofContext.init thy)) name of SOME (info as (_, result)) => @@ -600,17 +602,21 @@ let val (const, _) = strip_comb (HOLogic.dest_Trueprop (concl_of intro)) in (fst (dest_Const const) = name) end; - val intros = ind_set_codegen_preproc thy ((map (preprocess_intro thy)) - (filter is_intro_of (#intrs result))) + val intros = ind_set_codegen_preproc thy + (map (expand_tuples thy #> preprocess_intro thy) (filter is_intro_of (#intrs result))) val pre_elim = nth (#elims result) (find_index (fn s => s = name) (#names (fst info))) val nparams = length (Inductive.params_of (#raw_induct result)) - val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams pre_elim) + (*val elim = singleton (ind_set_codegen_preproc thy) (preprocess_elim thy nparams + (expand_tuples_elim pre_elim))*) + val elim = + (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) + (mk_casesrule (ProofContext.init thy) nparams intros) val (intros, elim) = if null intros then noclause thy name elim else (intros, elim) in mk_pred_data ((intros, SOME elim, nparams), ([], [], [])) end | NONE => error ("No such predicate: " ^ quote name) - + (* updaters *) fun apfst3 f (x, y, z) = (f x, y, z) @@ -2243,6 +2249,26 @@ forall (check_prem o dest_prem thy params o HOLogic.dest_Trueprop) prems end +(* +fun check_intros_elim_match thy prednames = + let + fun check predname = + let + val intros = intros_of thy predname + val elim = the_elim_of thy predname + val nparams = nparams_of thy predname + val elim' = + (Drule.standard o (setmp quick_and_dirty true (SkipProof.make_thm thy))) + (mk_casesrule (ProofContext.init thy) nparams intros) + val _ = Output.tracing (Display.string_of_thm_global thy elim) + val _ = Output.tracing (Display.string_of_thm_global thy elim') + in + if not (Thm.equiv_thm (elim, elim')) then + error "Introduction and elimination rules do not match!" + else true + end + in forall check prednames end +*) (** main function of predicate compiler **) @@ -2251,6 +2277,7 @@ let val _ = print_step options ("Starting predicate compiler for predicates " ^ commas prednames ^ "...") val _ = tracing (commas (map (Display.string_of_thm_global thy) (maps (intros_of thy) prednames))) + (*val _ = check_intros_elim_match thy prednames*) (*val _ = map (check_format_of_intro_rule thy) (maps (intros_of thy) prednames)*) val (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) = prepare_intrs thy prednames (maps (intros_of thy) prednames) diff -r 3c7c4372f9ad -r 5378e61add1a 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 @@ -7,7 +7,7 @@ | "even n \ odd (Suc n)" | "odd n \ even (Suc n)" -code_pred (mode: [], [1]) even . +code_pred (mode: [], [1]) [show_steps, inductify] even . thm odd.equation thm even.equation @@ -38,22 +38,23 @@ "append [] xs xs" | "append xs ys zs \ append (x # xs) ys (x # zs)" -code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) append . +code_pred (mode: [1, 2], [3], [2, 3], [1, 3], [1, 2, 3]) [inductify] append . thm append.equation -code_pred (inductify_all) (rpred) append . +code_pred [rpred] append . thm append.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 "{ys. append [0, Suc 0, 2] ys [0, Suc 0, 2, 17, 0, 5]}" value [code] "Predicate.the (append_1_2 [0::int, 1, 2] [3, 4, 5])" value [code] "Predicate.the (append_3 ([]::int list))" subsection {* Tricky case with alternative rules *} + text {* This cannot be handled correctly yet *} (* inductive append2 @@ -92,8 +93,8 @@ "tupled_append' ([], xs, xs)" | "[| ys = fst (xa, y); x # zs = snd (xa, y); tupled_append' (xs, ys, x # zs) |] ==> tupled_append' (x # xs, xa, y)" - -code_pred (inductify_all) tupled_append' . +ML {* aconv *} +code_pred tupled_append' . thm tupled_append'.equation (* TODO: Modeanalysis returns mode [2] ?? *) @@ -104,7 +105,7 @@ thm tupled_append''.cases -code_pred (inductify_all) tupled_append'' . +code_pred [inductify] tupled_append'' . thm tupled_append''.equation (* TODO: Modeanalysis returns mode [2] ?? *) @@ -113,7 +114,7 @@ "tupled_append''' ([], xs, xs)" | "yszs = (ys, zs) ==> tupled_append''' (xs, yszs) \ tupled_append''' (x # xs, ys, x # zs)" -code_pred (inductify_all) tupled_append''' . +code_pred [inductify] tupled_append''' . thm tupled_append'''.equation (* TODO: Missing a few modes *) @@ -130,7 +131,7 @@ "rev [] []" | "rev xs xs' ==> append xs' [x] ys ==> rev (x#xs) ys" -code_pred rev . +code_pred (mode: [1], [2], [1, 2]) rev . thm rev.equation @@ -149,7 +150,7 @@ | "f x \ partition f xs ys zs \ partition f (x # xs) (x # ys) zs" | "\ f x \ partition f xs ys zs \ partition f (x # xs) ys (x # zs)" -code_pred partition . +code_pred (mode: [1], [2, 3], [1, 2], [1, 3], [1, 2, 3]) partition . inductive tupled_partition :: "('a \ bool) \ ('a list \ 'a list \ 'a list) \ bool" for f where @@ -197,11 +198,10 @@ case tranclp from this converse_tranclpE[OF this(1)] show thesis by metis qed -(* -code_pred (inductify_all) (rpred) tranclp . + +code_pred [inductify, rpred] tranclp . thm tranclp.equation thm tranclp.rpred_equation -*) inductive succ :: "nat \ nat \ bool" where "succ 0 1" @@ -223,8 +223,6 @@ values 20 "{(n, m). tranclp succ n m}" *) -subsection{* *} - subsection{* IMP *} types @@ -319,7 +317,7 @@ definition Min where "Min s r x \ s x \ (\y. r x y \ x = y)" -code_pred (inductify_all) Min . +code_pred [inductify] Min . subsection {* Examples with lists *} (* @@ -334,7 +332,7 @@ thm filterP.rpred_equation *) -code_pred (inductify_all) lexord . +code_pred [inductify] lexord . thm lexord.equation @@ -344,20 +342,22 @@ lemmas [code_pred_def] = lexn_conv lex_conv lenlex_conv -code_pred (inductify_all) lexn . +code_pred [inductify] lexn . thm lexn.equation -code_pred (inductify_all) lenlex . +code_pred [inductify] lenlex . thm lenlex.equation -(* -code_pred (inductify_all) (rpred) lenlex . + +code_pred [inductify, rpred] lenlex . thm lenlex.rpred_equation -*) + thm lists.intros -code_pred (inductify_all) lists . +code_pred [inductify] lists . thm lists.equation +section {* AVL Tree Example *} + datatype 'a tree = ET | MKT 'a "'a tree" "'a tree" nat fun height :: "'a tree => nat" where "height ET = 0" @@ -369,9 +369,9 @@ "avl (MKT x l r h) = ((height l = height r \ height l = 1 + height r \ height r = 1+height l) \ h = max (height l) (height r) + 1 \ avl l \ avl r)" -code_pred (inductify_all) avl . +code_pred [inductify] avl . thm avl.equation -(* + fun set_of where "set_of ET = {}" @@ -383,11 +383,10 @@ "is_ord ET = True" | "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)" -ML {* *} -code_pred (inductify_all) set_of . +code_pred [inductify] set_of . thm set_of.equation -*) + text {* expected mode: [1], [1, 2] *} (* FIXME *) (* @@ -396,50 +395,47 @@ *) section {* Definitions about Relations *} -code_pred (inductify_all) converse . +code_pred [inductify] converse . thm converse.equation -code_pred (inductify_all) Domain . +code_pred [inductify] Domain . thm Domain.equation section {* List functions *} -code_pred (inductify_all) length . +code_pred [inductify] length . thm size_listP.equation -code_pred (inductify_all) concat . +code_pred [inductify] concat . thm concatP.equation -code_pred (inductify_all) hd . -code_pred (inductify_all) tl . -code_pred (inductify_all) last . -code_pred (inductify_all) butlast . -(*code_pred (inductify_all) listsum .*) -code_pred (inductify_all) take . -code_pred (inductify_all) drop . -code_pred (inductify_all) zip . -code_pred (inductify_all) upt . -code_pred set sorry -code_pred (inductify_all) remdups . -code_pred (inductify_all) remove1 . -code_pred (inductify_all) removeAll . -code_pred (inductify_all) distinct . -code_pred (inductify_all) replicate . -code_pred (inductify_all) splice . -code_pred (inductify_all) List.rev . -thm revP.equation - -code_pred (inductify_all) foldl . -thm foldlP.equation - -code_pred (inductify_all) filter . +code_pred [inductify] hd . +code_pred [inductify] tl . +code_pred [inductify] last . +code_pred [inductify] butlast . +thm listsum.simps +(*code_pred [inductify] listsum .*) +code_pred [inductify] take . +code_pred [inductify] drop . +code_pred [inductify] zip . +code_pred [inductify] upt . +code_pred [inductify] remdups . +code_pred [inductify] remove1 . +code_pred [inductify] removeAll . +code_pred [inductify] distinct . +code_pred [inductify] replicate . +code_pred [inductify] splice . +code_pred [inductify] List.rev . +code_pred [inductify] foldr . +code_pred [inductify] foldl . +code_pred [inductify] filter . definition test where "test xs = filter (\x. x = (1::nat)) xs" -term "one_nat_inst.one_nat" -code_pred (inductify_all) test . +(* +TODO: implement higher-order replacement correctly +code_pred [inductify] test . thm testP.equation -(* -code_pred (inductify_all) (rpred) test . +code_pred [inductify, rpred] test . *) section {* Handling set operations *} @@ -457,7 +453,7 @@ | "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_all) S\<^isub>1p . +code_pred [inductify] S\<^isub>1p . thm S\<^isub>1p.equation (* @@ -473,10 +469,12 @@ | "w \ S\<^isub>2 \ a # w \ A\<^isub>2" | "w \ S\<^isub>2 \ b # w \ B\<^isub>2" | "\v \ B\<^isub>2; v \ B\<^isub>2\ \ a # v @ w \ B\<^isub>2" -(* -code_pred (inductify_all) (rpred) S\<^isub>2 . -ML {* Predicate_Compile_Core.intros_of @{theory} @{const_name "B\<^isub>2"} *} -*) + +code_pred [inductify, rpred] S\<^isub>2 . +thm S\<^isub>2.rpred_equation +thm A\<^isub>2.rpred_equation +thm B\<^isub>2.rpred_equation + theorem S\<^isub>2_sound: "w \ S\<^isub>2 \ length [x \ w. x = a] = length [x \ w. x = b]" (*quickcheck[generator=SML]*) @@ -491,7 +489,7 @@ | "w \ S\<^isub>3 \ b # w \ B\<^isub>3" | "\v \ B\<^isub>3; w \ B\<^isub>3\ \ a # v @ w \ B\<^isub>3" -code_pred (inductify_all) S\<^isub>3 . +code_pred [inductify] S\<^isub>3 . theorem S\<^isub>3_sound: "w \ S\<^isub>3 \ length [x \ w. x = a] = length [x \ w. x = b]" @@ -598,21 +596,6 @@ lemma "Gamma \ t : T \ t \\<^sub>\ t' \ Gamma \ t' : T" quickcheck[generator = pred_compile, size = 10, iterations = 100] oops -(* FIXME *) - -inductive test' for P where -"[| filter P vs = res |] -==> test' P vs res" - -code_pred (inductify_all) test' . -thm test'.equation - -(* -export_code test_for_1_yields_1_2 in SML file - -code_pred (inductify_all) (rpred) test . - -thm test.equation -*) lemma filter_eq_ConsD: "filter P ys = x#xs \