# HG changeset patch # User bulwahn # Date 1256979757 -3600 # Node ID 5cb663aa48ee75788cdd6e49f2a5dcf949118c33 # Parent fd3e861f8d3135c4cd4e6bca2b428bca3023ada4 predicate compiler creates code equations for predicates with full mode diff -r fd3e861f8d31 -r 5cb663aa48ee src/HOL/Tools/Predicate_Compile/predicate_compile.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Oct 30 09:55:15 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Sat Oct 31 10:02:37 2009 +0100 @@ -18,8 +18,6 @@ open Predicate_Compile_Aux; -val priority = tracing; - (* Some last processing *) fun remove_pointless_clauses intro = @@ -27,14 +25,12 @@ [] else [intro] -fun tracing s = () - fun print_intross options thy msg intross = if show_intermediate_results options then - Output.tracing (msg ^ - (space_implode "\n" (map - (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ - commas (map (Display.string_of_thm_global thy) intros)) intross))) + tracing (msg ^ + (space_implode "\n" (map + (fn (c, intros) => "Introduction rule(s) of " ^ c ^ ":\n" ^ + commas (map (Display.string_of_thm_global thy) intros)) intross))) else () fun print_specs thy specs = diff -r fd3e861f8d31 -r 5cb663aa48ee src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Oct 30 09:55:15 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sat Oct 31 10:02:37 2009 +0100 @@ -2018,6 +2018,8 @@ map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t)) compiled_terms +(* preparation of introduction rules into special datastructures *) + fun dest_prem thy params t = (case strip_comb t of (v as Free _, ts) => if v mem params then Prem (ts, v) else Sidecond t @@ -2091,6 +2093,8 @@ val all_modes = map (fn (s, T) => (s, modes_of_typ T)) preds in (preds, nparams, all_vs, param_vs, extra_modes, clauses, all_modes) end; +(* sanity check of introduction rules *) + fun check_format_of_intro_rule thy intro = let val concl = Logic.strip_imp_concl (prop_of intro) @@ -2132,6 +2136,40 @@ in forall check prednames end *) +(* create code equation *) + +fun add_code_equations thy nparams preds result_thmss = + let + fun add_code_equation ((predname, T), (pred, result_thms)) = + let + val full_mode = (replicate nparams NONE, + map (rpair NONE) (1 upto (length (binder_types T) - nparams))) + in + if member (op =) (modes_of thy predname) full_mode then + let + val Ts = binder_types T + val arg_names = Name.variant_list [] + (map (fn i => "x" ^ string_of_int i) (1 upto length Ts)) + val args = map Free (arg_names ~~ Ts) + val predfun = Const (predfun_name_of thy predname full_mode, + Ts ---> PredicateCompFuns.mk_predT @{typ unit}) + val rhs = PredicateCompFuns.mk_Eval (list_comb (predfun, args), @{term "Unity"}) + val eq_term = HOLogic.mk_Trueprop + (HOLogic.mk_eq (list_comb (Const (predname, T), args), rhs)) + val def = predfun_definition_of thy predname full_mode + val tac = fn {...} => Simplifier.simp_tac + (HOL_basic_ss addsimps [def, @{thm eval_pred}]) 1 + val eq = Goal.prove (ProofContext.init thy) arg_names [] eq_term tac + in + (pred, result_thms @ [eq]) + end + else + (pred, result_thms) + end + in + map add_code_equation (preds ~~ result_thmss) + end + (** main function of predicate compiler **) datatype steps = Steps of @@ -2145,6 +2183,8 @@ prove : options -> theory -> (string * (term list * indprem list) list) list -> (string * typ) list -> (string * mode list) list -> moded_clause list pred_mode_table -> term pred_mode_table -> thm pred_mode_table, + add_code_equations : theory -> int -> (string * typ) list + -> (string * thm list) list -> (string * thm list) list, are_not_defined : theory -> string list -> bool, qname : bstring } @@ -2174,14 +2214,15 @@ val _ = print_step options "Proving equations..." val result_thms = #prove (dest_steps steps) options thy' clauses preds (extra_modes @ modes) moded_clauses compiled_terms + val result_thms' = #add_code_equations (dest_steps steps) thy' nparams preds + (maps_modes result_thms) val qname = #qname (dest_steps steps) val attrib = fn thy => Attrib.attribute_i thy (Attrib.internal (K (Thm.declaration_attribute (fn thm => Context.mapping (Code.add_eqn thm) I)))) val thy'' = fold (fn (name, result_thms) => fn thy => snd (PureThy.add_thmss [((Binding.qualify true (Long_Name.base_name name) (Binding.name qname), result_thms), [attrib thy ])] thy)) - (maps_modes result_thms) thy' - |> Theory.checkpoint + result_thms' thy' |> Theory.checkpoint in thy'' end @@ -2272,6 +2313,7 @@ create_definitions = create_definitions, compile_preds = compile_preds predicate_comp_modifiers PredicateCompFuns.compfuns, prove = prove, + add_code_equations = add_code_equations, are_not_defined = fn thy => forall (null o modes_of thy), qname = "equation"}) @@ -2280,6 +2322,7 @@ create_definitions = create_definitions_of_depth_limited_functions, compile_preds = compile_preds depth_limited_comp_modifiers PredicateCompFuns.compfuns, prove = prove_by_skip, + add_code_equations = K (K (K I)), are_not_defined = fn thy => forall (null o depth_limited_modes_of thy), qname = "depth_limited_equation"}) @@ -2288,6 +2331,7 @@ create_definitions = random_create_definitions, compile_preds = compile_preds random_comp_modifiers RandomPredCompFuns.compfuns, prove = prove_by_skip, + add_code_equations = K (K (K I)), are_not_defined = fn thy => forall (null o random_modes_of thy), qname = "random_equation"}) diff -r fd3e861f8d31 -r 5cb663aa48ee src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Fri Oct 30 09:55:15 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sat Oct 31 10:02:37 2009 +0100 @@ -126,8 +126,9 @@ |> 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 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 store_thm_in_table ignore_consts thy th= let