# HG changeset patch
# User krauss
# Date 1312272194 -7200
# Node ID 8c1dfd6c226215328a09e4fdc783049f4af50e42
# Parent  f67c93f52d137c58ccaef6e27c4abec89c42523c
added dynamic ersatz_table to Nitpick's data slot

diff -r f67c93f52d13 -r 8c1dfd6c2262 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:03:12 2011 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Aug 02 10:03:14 2011 +0200
@@ -148,6 +148,9 @@
   val unregister_frac_type :
     string -> morphism -> Context.generic -> Context.generic
   val unregister_frac_type_global : string -> theory -> theory
+  val register_ersatz :
+    (string * string) list -> morphism -> Context.generic -> Context.generic
+  val register_ersatz_global : (string * string) list -> theory -> theory
   val register_codatatype :
     typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
   val register_codatatype_global :
@@ -287,12 +290,14 @@
 structure Data = Generic_Data
 (
   type T = {frac_types: (string * (string * string) list) list,
+            ersatz_table: (string * string) list,
             codatatypes: (string * (string * styp list)) list}
-  val empty = {frac_types = [], codatatypes = []}
+  val empty = {frac_types = [], ersatz_table = [], codatatypes = []}
   val extend = I
-  fun merge ({frac_types = fs1, codatatypes = cs1},
-             {frac_types = fs2, codatatypes = cs2}) : T =
+  fun merge ({frac_types = fs1, ersatz_table = et1, codatatypes = cs1},
+             {frac_types = fs2, ersatz_table = et2, codatatypes = cs2}) : T =
     {frac_types = AList.merge (op =) (K true) (fs1, fs2),
+     ersatz_table = AList.merge (op =) (K true) (et1, et2),
      codatatypes = AList.merge (op =) (K true) (cs1, cs2)}
 )
 
@@ -491,8 +496,7 @@
 val is_integer_like_type = is_iterator_type orf is_integer_type orf is_word_type
 val is_record_type = not o null o Record.dest_recTs
 fun is_frac_type ctxt (Type (s, [])) =
-    s |> AList.lookup (op =) (#frac_types (Data.get (Context.Proof ctxt)))
-      |> these |> null |> not
+    s |> AList.defined (op =) (#frac_types (Data.get (Context.Proof ctxt)))
   | is_frac_type _ _ = false
 fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
 fun is_higher_order_type (Type (@{type_name fun}, _)) = true
@@ -575,9 +579,10 @@
 
 fun register_frac_type_generic frac_s ersaetze generic =
   let
-    val {frac_types, codatatypes} = Data.get generic
+    val {frac_types, ersatz_table, codatatypes} = Data.get generic
     val frac_types = AList.update (op =) (frac_s, ersaetze) frac_types
-  in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
+  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
+               codatatypes = codatatypes} generic end
 (* TODO: Consider morphism. *)
 fun register_frac_type frac_s ersaetze (_ : morphism) =
   register_frac_type_generic frac_s ersaetze
@@ -590,11 +595,22 @@
 val unregister_frac_type_global =
   Context.theory_map o unregister_frac_type_generic
 
+fun register_ersatz_generic ersatz generic =
+  let
+    val {frac_types, ersatz_table, codatatypes} = Data.get generic
+    val ersatz_table = AList.merge (op =) (K true) (ersatz_table, ersatz)
+  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
+               codatatypes = codatatypes} generic end
+(* TODO: Consider morphism. *)
+fun register_ersatz ersatz (_ : morphism) =
+  register_ersatz_generic ersatz
+val register_ersatz_global = Context.theory_map o register_ersatz_generic
+
 fun register_codatatype_generic co_T case_name constr_xs generic =
   let
     val ctxt = Context.proof_of generic
     val thy = Context.theory_of generic
-    val {frac_types, codatatypes} = Data.get generic
+    val {frac_types, ersatz_table, codatatypes} = Data.get generic
     val constr_xs = map (apsnd (repair_constr_type ctxt co_T)) constr_xs
     val (co_s, co_Ts) = dest_Type co_T
     val _ =
@@ -606,7 +622,8 @@
         raise TYPE ("Nitpick_HOL.register_codatatype_generic", [co_T], [])
     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
                                    codatatypes
-  in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
+  in Data.put {frac_types = frac_types, ersatz_table = ersatz_table,
+               codatatypes = codatatypes} generic end
 (* TODO: Consider morphism. *)
 fun register_codatatype co_T case_name constr_xs (_ : morphism) =
   register_codatatype_generic co_T case_name constr_xs
@@ -1861,7 +1878,7 @@
    (@{const_name wfrec}, @{const_name wfrec'})]
 
 fun ersatz_table ctxt =
- basic_ersatz_table
+ (basic_ersatz_table @ #ersatz_table (Data.get (Context.Proof ctxt)))
  |> fold (append o snd) (#frac_types (Data.get (Context.Proof ctxt)))
 
 fun add_simps simp_table s eqs =