# HG changeset patch # User bulwahn # Date 1258615557 -3600 # Node ID 47b7c9e0bf6e62b89b6e3b282d36924195905a27 # Parent 6dc1b67f2127bc50231dd82d285c7ccd57c68f37 replacing Predicate_Compile_Preproc_Const_Defs by more general Spec_Rules diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/HOL/HOL.thy --- a/src/HOL/HOL.thy Thu Nov 19 08:25:54 2009 +0100 +++ b/src/HOL/HOL.thy Thu Nov 19 08:25:57 2009 +0100 @@ -2060,7 +2060,6 @@ setup {* Predicate_Compile_Alternative_Defs.setup #> Predicate_Compile_Inline_Defs.setup - #> Predicate_Compile_Preproc_Const_Defs.setup *} diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:54 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:57 2009 +0100 @@ -137,7 +137,7 @@ th' end -fun store_thm_in_table options ignore_consts thy th= +fun store_thm_in_table options ignore thy th= let val th = th |> inline_equations options thy @@ -153,29 +153,29 @@ else if (is_introlike th) then (defining_const_of_introrule th, th) else error "store_thm: unexpected definition format" in - if not (member (op =) ignore_consts const) then - Symtab.cons_list (const, th) - else I + if ignore const then I else Symtab.cons_list (const, th) end fun make_const_spec_table options thy = let - fun store ignore_const f = - fold (store_thm_in_table options ignore_const thy) + fun store ignore f = + fold (store_thm_in_table options ignore 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 + |> store (K false) Predicate_Compile_Alternative_Defs.get + val ignore = Symtab.defined table in table - |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get - |> store ignore_consts Nitpick_Simps.get - |> store ignore_consts Nitpick_Intros.get + |> store ignore (fn ctxt => maps + (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else []) + (Spec_Rules.get ctxt)) + |> store ignore Nitpick_Simps.get + |> store ignore Nitpick_Intros.get end fun get_specification table constname = case Symtab.lookup table constname of - SOME thms => thms + SOME thms => thms | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed") val logic_operator_names = diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:54 2009 +0100 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:57 2009 +0100 @@ -83,7 +83,7 @@ val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac val _ = tracing (Display.string_of_thm ctxt' intro) val thy'' = thy' - |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro) + |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro) |> Predicate_Compile.preprocess options full_constname |> Predicate_Compile_Core.add_equations options [full_constname] (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*) diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Nov 19 08:25:54 2009 +0100 +++ b/src/Pure/Isar/code.ML Thu Nov 19 08:25:57 2009 +0100 @@ -775,49 +775,4 @@ end; -(** datastructure to log definitions for preprocessing of the predicate compiler **) -(* obviously a clone of Named_Thms *) - -signature PREDICATE_COMPILE_PREPROC_CONST_DEFS = -sig - val get: Proof.context -> thm list - val add_thm: thm -> Context.generic -> Context.generic - val del_thm: thm -> Context.generic -> Context.generic - - val add_attribute : attribute - val del_attribute : attribute - - val add_attrib : Attrib.src - - val setup: theory -> theory -end; - -structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS = -struct - -structure Data = Generic_Data -( - type T = thm list; - val empty = []; - val extend = I; - val merge = Thm.merge_thms; -); - -val get = Data.get o Context.Proof; - -val add_thm = Data.map o Thm.add_thm; -val del_thm = Data.map o Thm.del_thm; - -val add_attribute = Thm.declaration_attribute add_thm; -val del_attribute = Thm.declaration_attribute del_thm; - -val add_attrib = Attrib.internal (K add_attribute) - -val setup = - Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute) - ("declaration of definition for preprocessing of the predicate compiler") #> - PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get); - -end; - structure Code : CODE = struct open Code; end; diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/Pure/Isar/constdefs.ML --- a/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:54 2009 +0100 +++ b/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:57 2009 +0100 @@ -55,8 +55,7 @@ |> PureThy.add_defs false [((name, def), atts)] |-> (fn [thm] => (* FIXME thm vs. atts !? *) Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #> - Code.add_default_eqn thm #> - Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm)); + Code.add_default_eqn thm); in ((c, T), thy') end; fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy = diff -r 6dc1b67f2127 -r 47b7c9e0bf6e src/Pure/Isar/specification.ML --- a/src/Pure/Isar/specification.ML Thu Nov 19 08:25:54 2009 +0100 +++ b/src/Pure/Isar/specification.ML Thu Nov 19 08:25:57 2009 +0100 @@ -212,8 +212,7 @@ val ([(def_name, [th'])], lthy4) = lthy3 |> Local_Theory.notes_kind Thm.definitionK - [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib :: - Code.add_default_eqn_attrib :: atts), [([th], [])])]; + [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])]; val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs; val _ =