# HG changeset patch
# User bulwahn
# Date 1257240246 -3600
# Node ID 66746e4b4531565577d7655a31e4f1bca38ba237
# Parent  a9b6497391b05969bcb42069f3900654fb599f34
adapted the inlining in the predicate compiler

diff -r a9b6497391b0 -r 66746e4b4531 src/HOL/Tools/Predicate_Compile/predicate_compile.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Nov 03 10:24:05 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML	Tue Nov 03 10:24:06 2009 +0100
@@ -37,6 +37,9 @@
   map (fn (c, thms) => "Constant " ^ c ^ " has specification:\n"
     ^ (space_implode "\n" (map (Display.string_of_thm_global thy) thms)) ^ "\n") specs
 
+(* TODO: *)
+fun overload_const thy s = s
+
 fun map_specs f specs =
   map (fn (s, ths) => (s, f ths)) specs
 
@@ -59,15 +62,14 @@
     val (intross3, (new_defs, thy''')) = Predicate_Compile_Pred.flat_higher_order_arguments (intross2, thy'')
     val (new_intross, thy'''')  =
       if not (null new_defs) then
-      let
-        val _ = print_step options "Recursively obtaining introduction rules for new definitions..."
-      in process_specification options new_defs thy''' end
-    else ([], thy''')
+        let
+          val _ = print_step options "Recursively obtaining introduction rules for new definitions..."
+        in process_specification options new_defs thy''' end
+      else ([], thy''')
   in
     (intross3 @ new_intross, thy'''')
   end
 
-
 fun preprocess_strong_conn_constnames options gr constnames thy =
   let
     val get_specs = map (fn k => (k, Graph.get_node gr k))
@@ -85,7 +87,7 @@
     val _ = print_intross options thy''' "Introduction rules with new constants: " intross3
     val intross4 = map_specs (maps remove_pointless_clauses) intross3
     val _ = print_intross options thy''' "After removing pointless clauses: " intross4
-      (*val intross5 = map (fn s, ths) => ( s, map (AxClass.overload thy''') ths)) intross4*)
+    val intross5 = (*map (fn (s, ths) => (overload_const s, map (AxClass.overload thy''') ths))*) intross4
     val intross6 = map_specs (map (expand_tuples thy''')) intross4
     val _ = print_intross options thy''' "introduction rules before registering: " intross6
     val _ = print_step options "Registering introduction rules..."
@@ -97,7 +99,7 @@
 fun preprocess options const thy =
   let
     val _ = print_step options "Fetching definitions from theory..."
-    val table = Predicate_Compile_Data.make_const_spec_table thy
+    val table = Predicate_Compile_Data.make_const_spec_table options thy
     val gr = Predicate_Compile_Data.obtain_specification_graph options thy table const
     val gr = Graph.subgraph (member (op =) (Graph.all_succs gr [const])) gr
   in fold_rev (preprocess_strong_conn_constnames options gr)
diff -r a9b6497391b0 -r 66746e4b4531 src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Nov 03 10:24:05 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Tue Nov 03 10:24:06 2009 +0100
@@ -7,7 +7,7 @@
 signature PREDICATE_COMPILE_DATA =
 sig
   type specification_table;
-  val make_const_spec_table : theory -> specification_table
+  val make_const_spec_table : Predicate_Compile_Aux.options -> theory -> specification_table
   val get_specification :  specification_table -> string -> thm list
   val obtain_specification_graph : Predicate_Compile_Aux.options -> theory ->
     specification_table -> string -> thm list Graph.T
@@ -126,14 +126,22 @@
   |> 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 options thy th =
+  let
+    val inline_defs = Predicate_Compile_Inline_Defs.get (ProofContext.init thy)
+    val th' = (Simplifier.full_simplify (HOL_basic_ss addsimps inline_defs)) th
+    (*val _ = print_step options 
+      ("Inlining " ^ (Syntax.string_of_term_global thy (prop_of th))
+       ^ "with " ^ (commas (map ((Syntax.string_of_term_global thy) o prop_of) inline_defs))
+       ^" to " ^ (Syntax.string_of_term_global thy (prop_of th')))*)
+  in
+    th'
+  end
 
-fun store_thm_in_table ignore_consts thy th=
+fun store_thm_in_table options ignore_consts thy th=
   let
     val th = th
-      |> inline_equations thy
+      |> inline_equations options thy
       |> Predicate_Compile_Set.unfold_set_notation
       |> AxClass.unoverload thy
     val (const, th) =
@@ -151,9 +159,9 @@
     else I
   end
 
-fun make_const_spec_table thy =
+fun make_const_spec_table options thy =
   let
-    fun store ignore_const f = fold (store_thm_in_table ignore_const thy) (map (Thm.transfer thy) (f (ProofContext.init thy)))
+    fun store ignore_const f = fold (store_thm_in_table options ignore_const 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