# HG changeset patch # User bulwahn # Date 1256396142 -7200 # Node ID 9d9afd478016971b1c408cfecb93d9f88bd1c2cb # Parent 6aa76ce59ef281186acbe69864d8d157c19741ab added test for higher-order function inductification; added debug messages diff -r 6aa76ce59ef2 -r 9d9afd478016 src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML --- a/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:40 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_fun.ML Sat Oct 24 16:55:42 2009 +0200 @@ -210,7 +210,7 @@ let fun mk_prems' (t as Const (name, T)) (names, prems) = if is_constr thy name orelse (is_none (try lookup_pred t)) then - [(t ,(names, prems))] + [(t, (names, prems))] else [(lookup_pred t, (names, prems))] | mk_prems' (t as Free (f, T)) (names, prems) = [(lookup_pred t, (names, prems))] @@ -243,7 +243,8 @@ maps mk_prems_of_assm assms end else - let + let + val _ = tracing ("Flattening term " ^ (Syntax.string_of_term_global thy t)) val (f, args) = strip_comb t val resname = Name.variant names "res" val resvar = Free (resname, body_type (fastype_of t)) @@ -281,7 +282,15 @@ val prem = HOLogic.mk_Trueprop (list_comb (pred, argvs @ [resvar])) in (names', prem :: prems') end) end - | mk_prems'' t = error ("Invalid term: " ^ Syntax.string_of_term_global thy t) + | mk_prems'' t = + let + val _ = tracing ("must define new constant for " + ^ (Syntax.string_of_term_global thy t)) + in + (*if is_predT (fastype_of t) then + else*) + error ("Invalid term: " ^ Syntax.string_of_term_global thy t) + end in map (pair resvar) (mk_prems'' f) end diff -r 6aa76ce59ef2 -r 9d9afd478016 src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:40 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 24 16:55:42 2009 +0200 @@ -10,6 +10,9 @@ structure Predicate_Compile : PREDICATE_COMPILE = struct +(* options *) +val fail_safe_mode = false + open Predicate_Compile_Aux; val priority = tracing; @@ -39,9 +42,11 @@ val _ = priority "Replacing functions in introrules..." (* val _ = burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross *) val intross' = - case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of - SOME intross' => intross' - | NONE => let val _ = warning "Function replacement failed!" in intross end + if fail_safe_mode then + case try (burrow (maps (Predicate_Compile_Fun.rewrite_intro thy''))) intross of + SOME intross' => intross' + | NONE => let val _ = warning "Function replacement failed!" in intross end + else burrow (maps (Predicate_Compile_Fun.rewrite_intro thy'')) intross val _ = tracing ("Introduction rules with replaced functions: " ^ commas (map (Display.string_of_thm_global thy'') (flat intross'))) val intross'' = burrow (maps remove_pointless_clauses) intross' diff -r 6aa76ce59ef2 -r 9d9afd478016 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:40 2009 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 24 16:55:42 2009 +0200 @@ -120,11 +120,18 @@ fun tracing s = (if ! Toplevel.debug then Output.tracing s else ()); -fun print_tac s = Seq.single; (*Tactical.print_tac s;*) (* (if ! Toplevel.debug then Tactical.print_tac s else Seq.single); *) +fun print_tac s = Seq.single; 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 + else error ("assert_tac: Numbers of subgoals mismatch at goal state :" + ^ "\n" ^ Pretty.string_of (Pretty.chunks + (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); + (* reference to preprocessing of InductiveSet package *) val ind_set_codegen_preproc = (fn thy => I) (*Inductive_Set.codegen_preproc;*) @@ -1433,7 +1440,7 @@ (u, rest) end in - compile_match thy compfuns constr_vs' eqs out_ts'' + compile_match thy compfuns constr_vs' eqs out_ts'' (mk_bind compfuns (compiled_clause, rest)) end val prem_t = compile_prems in_ts' param_vs all_vs' moded_ps; @@ -1914,10 +1921,15 @@ | _ => PureThy.get_thms thy (((fst o dest_Type o fastype_of) t) ^ ".split_asm") val (_, ts) = strip_comb t in - (Splitter.split_asm_tac split_rules 1) -(* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) - THEN (DETERM (TRY (etac @{thm Pair_inject} 1))) *) + (print_tac ("Term " ^ (Syntax.string_of_term_global thy t) ^ + "splitting with rules \n" ^ + commas (map (Display.string_of_thm_global thy) split_rules))) + THEN (Splitter.split_asm_tac split_rules 1) + THEN (print_tac "after splitting with split_asm rules") + (* THEN (Simplifier.asm_full_simp_tac HOL_basic_ss 1) + THEN (DETERM (TRY (etac @{thm Pair_inject} 1)))*) THEN (REPEAT_DETERM_N (num_of_constrs - 1) (etac @{thm botE} 1 ORELSE etac @{thm botE} 2)) + THEN (assert_tac (Max_number_of_subgoals 2)) THEN (EVERY (map split_term_tac ts)) end else all_tac @@ -2241,9 +2253,11 @@ fold (rewrite_prem o dest_prem thy params o HOLogic.dest_Trueprop) (Logic.strip_imp_prems intro_t') (intro_t', frees') val _ = tracing ("intro_t': " ^ (Syntax.string_of_term_global thy intro_t')) + val tac = + (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy) in Goal.prove (ProofContext.init thy) (Term.add_free_names intro_t' []) [] - intro_t' (fn _ => setmp quick_and_dirty true SkipProof.cheat_tac thy) + intro_t' tac end (** main function of predicate compiler **) diff -r 6aa76ce59ef2 -r 9d9afd478016 src/HOL/ex/Predicate_Compile_ex.thy --- a/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:40 2009 +0200 +++ b/src/HOL/ex/Predicate_Compile_ex.thy Sat Oct 24 16:55:42 2009 +0200 @@ -333,7 +333,7 @@ code_pred (inductify_all) S\<^isub>1p . thm S\<^isub>1p.equation - +(* theorem S\<^isub>1_sound: "w \ S\<^isub>1 \ length [x \ w. x = a] = length [x \ w. x = b]" quickcheck[generator=pred_compile] @@ -375,6 +375,12 @@ lemma "\ (length w > 2) \ \ (length [x \ w. x = a] = length [x \ w. x = b])" quickcheck[size=10, generator = pred_compile] oops +*) +inductive test +where + "length [x \ w. x = a] = length [x \ w. x = b] ==> test w" +ML {* @{term "[x \ w. x = a]"} *} +code_pred (inductify_all) test . theorem S\<^isub>3_complete: "length [x \ w. x = a] = length [x \ w. x = b] \ w \ S\<^isub>3"