1.1 --- a/src/HOL/HOL.thy Thu Nov 19 08:25:54 2009 +0100
1.2 +++ b/src/HOL/HOL.thy Thu Nov 19 08:25:57 2009 +0100
1.3 @@ -2060,7 +2060,6 @@
1.4 setup {*
1.5 Predicate_Compile_Alternative_Defs.setup
1.6 #> Predicate_Compile_Inline_Defs.setup
1.7 - #> Predicate_Compile_Preproc_Const_Defs.setup
1.8 *}
1.9
1.10
2.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:54 2009 +0100
2.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Thu Nov 19 08:25:57 2009 +0100
2.3 @@ -137,7 +137,7 @@
2.4 th'
2.5 end
2.6
2.7 -fun store_thm_in_table options ignore_consts thy th=
2.8 +fun store_thm_in_table options ignore thy th=
2.9 let
2.10 val th = th
2.11 |> inline_equations options thy
2.12 @@ -153,29 +153,29 @@
2.13 else if (is_introlike th) then (defining_const_of_introrule th, th)
2.14 else error "store_thm: unexpected definition format"
2.15 in
2.16 - if not (member (op =) ignore_consts const) then
2.17 - Symtab.cons_list (const, th)
2.18 - else I
2.19 + if ignore const then I else Symtab.cons_list (const, th)
2.20 end
2.21
2.22 fun make_const_spec_table options thy =
2.23 let
2.24 - fun store ignore_const f =
2.25 - fold (store_thm_in_table options ignore_const thy)
2.26 + fun store ignore f =
2.27 + fold (store_thm_in_table options ignore thy)
2.28 (map (Thm.transfer thy) (f (ProofContext.init thy)))
2.29 val table = Symtab.empty
2.30 - |> store [] Predicate_Compile_Alternative_Defs.get
2.31 - val ignore_consts = Symtab.keys table
2.32 + |> store (K false) Predicate_Compile_Alternative_Defs.get
2.33 + val ignore = Symtab.defined table
2.34 in
2.35 table
2.36 - |> store ignore_consts Predicate_Compile_Preproc_Const_Defs.get
2.37 - |> store ignore_consts Nitpick_Simps.get
2.38 - |> store ignore_consts Nitpick_Intros.get
2.39 + |> store ignore (fn ctxt => maps
2.40 + (fn (roughly, (ts, ths)) => if roughly = Spec_Rules.Equational then ths else [])
2.41 + (Spec_Rules.get ctxt))
2.42 + |> store ignore Nitpick_Simps.get
2.43 + |> store ignore Nitpick_Intros.get
2.44 end
2.45
2.46 fun get_specification table constname =
2.47 case Symtab.lookup table constname of
2.48 - SOME thms => thms
2.49 + SOME thms => thms
2.50 | NONE => error ("get_specification: lookup of constant " ^ quote constname ^ " failed")
2.51
2.52 val logic_operator_names =
3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:54 2009 +0100
3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_quickcheck.ML Thu Nov 19 08:25:57 2009 +0100
3.3 @@ -83,7 +83,7 @@
3.4 val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
3.5 val _ = tracing (Display.string_of_thm ctxt' intro)
3.6 val thy'' = thy'
3.7 - |> Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm intro)
3.8 + |> Context.theory_map (Predicate_Compile_Alternative_Defs.add_thm intro)
3.9 |> Predicate_Compile.preprocess options full_constname
3.10 |> Predicate_Compile_Core.add_equations options [full_constname]
3.11 (* |> Predicate_Compile_Core.add_depth_limited_equations Predicate_Compile_Aux.default_options [full_constname]*)
4.1 --- a/src/Pure/Isar/code.ML Thu Nov 19 08:25:54 2009 +0100
4.2 +++ b/src/Pure/Isar/code.ML Thu Nov 19 08:25:57 2009 +0100
4.3 @@ -775,49 +775,4 @@
4.4
4.5 end;
4.6
4.7 -(** datastructure to log definitions for preprocessing of the predicate compiler **)
4.8 -(* obviously a clone of Named_Thms *)
4.9 -
4.10 -signature PREDICATE_COMPILE_PREPROC_CONST_DEFS =
4.11 -sig
4.12 - val get: Proof.context -> thm list
4.13 - val add_thm: thm -> Context.generic -> Context.generic
4.14 - val del_thm: thm -> Context.generic -> Context.generic
4.15 -
4.16 - val add_attribute : attribute
4.17 - val del_attribute : attribute
4.18 -
4.19 - val add_attrib : Attrib.src
4.20 -
4.21 - val setup: theory -> theory
4.22 -end;
4.23 -
4.24 -structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
4.25 -struct
4.26 -
4.27 -structure Data = Generic_Data
4.28 -(
4.29 - type T = thm list;
4.30 - val empty = [];
4.31 - val extend = I;
4.32 - val merge = Thm.merge_thms;
4.33 -);
4.34 -
4.35 -val get = Data.get o Context.Proof;
4.36 -
4.37 -val add_thm = Data.map o Thm.add_thm;
4.38 -val del_thm = Data.map o Thm.del_thm;
4.39 -
4.40 -val add_attribute = Thm.declaration_attribute add_thm;
4.41 -val del_attribute = Thm.declaration_attribute del_thm;
4.42 -
4.43 -val add_attrib = Attrib.internal (K add_attribute)
4.44 -
4.45 -val setup =
4.46 - Attrib.setup (Binding.name "pred_compile_preproc") (Attrib.add_del add_attribute del_attribute)
4.47 - ("declaration of definition for preprocessing of the predicate compiler") #>
4.48 - PureThy.add_thms_dynamic (Binding.name "pred_compile_preproc", Data.get);
4.49 -
4.50 -end;
4.51 -
4.52 structure Code : CODE = struct open Code; end;
5.1 --- a/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:54 2009 +0100
5.2 +++ b/src/Pure/Isar/constdefs.ML Thu Nov 19 08:25:57 2009 +0100
5.3 @@ -55,8 +55,7 @@
5.4 |> PureThy.add_defs false [((name, def), atts)]
5.5 |-> (fn [thm] => (* FIXME thm vs. atts !? *)
5.6 Spec_Rules.add_global Spec_Rules.Equational ([Logic.varify head], [thm]) #>
5.7 - Code.add_default_eqn thm #>
5.8 - Context.theory_map (Predicate_Compile_Preproc_Const_Defs.add_thm thm));
5.9 + Code.add_default_eqn thm);
5.10 in ((c, T), thy') end;
5.11
5.12 fun gen_constdefs prep_vars prep_prop prep_att (raw_structs, specs) thy =
6.1 --- a/src/Pure/Isar/specification.ML Thu Nov 19 08:25:54 2009 +0100
6.2 +++ b/src/Pure/Isar/specification.ML Thu Nov 19 08:25:57 2009 +0100
6.3 @@ -212,8 +212,7 @@
6.4
6.5 val ([(def_name, [th'])], lthy4) = lthy3
6.6 |> Local_Theory.notes_kind Thm.definitionK
6.7 - [((name, Predicate_Compile_Preproc_Const_Defs.add_attrib ::
6.8 - Code.add_default_eqn_attrib :: atts), [([th], [])])];
6.9 + [((name, Code.add_default_eqn_attrib :: atts), [([th], [])])];
6.10
6.11 val lhs' = Morphism.term (Local_Theory.target_morphism lthy4) lhs;
6.12 val _ =