# HG changeset patch
# User blanchet
# Date 1281350415 -7200
# Node ID 9f98107ad8b438ed172bf292f93a8f93ec970fbf
# Parent  1dac99cc8dbd11b929a09e65520753c38b20103a
use "declaration" instead of "setup" to register Nitpick extensions

diff -r 1dac99cc8dbd -r 9f98107ad8b4 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Aug 09 12:07:59 2010 +0200
+++ b/doc-src/Nitpick/nitpick.tex	Mon Aug 09 12:40:15 2010 +0200
@@ -719,9 +719,9 @@
 & \phantom{fun\,~\textit{HOLogic.mk\_number}~T~(}{-}~\textit{snd}~(\textit{HOLogic.dest\_number~t2\/})) \\[-2pt]
 & \phantom{fun}\!{\mid}\,~\textit{my\_int\_postproc}~\_~\_~\_~\_~t = t \\[-2pt]
 {*}\}\end{aligned}$ \\[2\smallskipamount]
-$\textbf{setup}~\,\{{*} \\
+$\textbf{declaration}~\,\{{*} \\
 \!\begin{aligned}[t]
-& \textit{Nitpick\_Model.register\_term\_postprocessor\_global\/}~\!\begin{aligned}[t]
+& \textit{Nitpick\_Model.register\_term\_postprocessor}~\!\begin{aligned}[t]
   & @\{\textrm{typ}~\textit{my\_int}\} \\[-2pt]
   & \textit{my\_int\_postproc}\end{aligned} \\[-2pt]
 {*}\}\end{aligned}$
@@ -2790,10 +2790,11 @@
 \textit{Nitpick\_HOL} structure:
 
 \prew
-$\textbf{val}\,~\textit{register\_codatatype\_global\/} : {}$ \\
-$\hbox{}\quad\textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
-$\textbf{val}\,~\textit{unregister\_codatatype\_global\/} :\,
-\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
+$\textbf{val}\,~\textit{register\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{string} \rightarrow (\textit{string} \times \textit{typ})\;\textit{list} \rightarrow \textit{Context.generic} {}$ \\
+$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
+$\textbf{val}\,~\textit{unregister\_codatatype\/} : {}$ \\
+$\hbox{}\quad\textit{morphism} \rightarrow \textit{typ} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic} {}$
 \postw
 
 The type $'a~\textit{llist}$ of lazy lists is already registered; had it
@@ -2801,24 +2802,25 @@
 to your theory file:
 
 \prew
-$\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.register\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
 $\hbox{}\qquad\quad @\{\antiq{const\_name}~ \textit{llist\_case}\}$ \\
 $\hbox{}\qquad\quad (\textit{map}~\textit{dest\_Const}~[@\{\antiq{term}~\textit{LNil}\},\, @\{\antiq{term}~\textit{LCons}\}])$ \\
 ${*}\}$
 \postw
 
-The \textit{register\_codatatype\_global\/} function takes a coinductive type, its
-case function, and the list of its constructors. The case function must take its
-arguments in the order that the constructors are listed. If no case function
-with the correct signature is available, simply pass the empty string.
+The \textit{register\_codatatype} function takes a coinductive datatype, its
+case function, and the list of its constructors (in addition to the current
+morphism and generic proof context). The case function must take its arguments
+in the order that the constructors are listed. If no case function with the
+correct signature is available, simply pass the empty string.
 
 On the other hand, if your goal is to cripple Nitpick, add the following line to
 your theory file and try to check a few conjectures about lazy lists:
 
 \prew
-$\textbf{setup}~\,\{{*}$ \\
-$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype\_global\/}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
+$\textbf{declaration}~\,\{{*}$ \\
+$\hbox{}\quad\textit{Nitpick\_HOL.unregister\_codatatype}~@\{\antiq{typ}~``\kern1pt'a~\textit{llist\/}\textrm{''}\}$ \\
 ${*}\}$
 \postw
 
@@ -2838,10 +2840,11 @@
 \prew
 $\textbf{type}\,~\textit{term\_postprocessor}\,~{=} {}$ \\
 $\hbox{}\quad\textit{Proof.context} \rightarrow \textit{string} \rightarrow (\textit{typ} \rightarrow \textit{term~list\/}) \rightarrow \textit{typ} \rightarrow \textit{term} \rightarrow \textit{term}$ \\
-$\textbf{val}\,~\textit{register\_term\_postprocessor\_global\/} : {}$ \\
-$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{theory} \rightarrow \textit{theory}$ \\
-$\textbf{val}\,~\textit{unregister\_term\_postprocessor\_global\/} :\,
-\textit{typ} \rightarrow \textit{theory} \rightarrow \textit{theory}$
+$\textbf{val}\,~\textit{register\_term\_postprocessor} : {}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{term\_postprocessor} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic}$ \\
+$\hbox{}\quad{\rightarrow}\; \textit{Context.generic}$ \\
+$\textbf{val}\,~\textit{unregister\_term\_postprocessor} : {}$ \\
+$\hbox{}\quad\textit{typ} \rightarrow \textit{morphism} \rightarrow \textit{Context.generic} \rightarrow \textit{Context.generic}$
 \postw
 
 \S\ref{typedefs-quotient-types-records-rationals-and-reals} and
diff -r 1dac99cc8dbd -r 9f98107ad8b4 src/HOL/Nitpick_Examples/Manual_Nits.thy
--- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 12:07:59 2010 +0200
+++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Mon Aug 09 12:40:15 2010 +0200
@@ -128,9 +128,8 @@
   | my_int_postproc _ _ _ _ t = t
 *}
 
-setup {*
-Nitpick_Model.register_term_postprocessor_global @{typ my_int}
-                                                 my_int_postproc
+declare {*
+Nitpick_Model.register_term_postprocessor @{typ my_int} my_int_postproc
 *}
 
 lemma "add x y = add x x"
@@ -213,8 +212,8 @@
 "iterates f a = LCons a (iterates f (f a))"
 sorry
 
-setup {*
-Nitpick_HOL.register_codatatype_global @{typ "'a llist"} ""
+declare {*
+Nitpick_HOL.register_codatatype @{typ "'a llist"} ""
     (map dest_Const [@{term LNil}, @{term LCons}])
 *}
 
diff -r 1dac99cc8dbd -r 9f98107ad8b4 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 09 12:07:59 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Aug 09 12:40:15 2010 +0200
@@ -144,18 +144,19 @@
   val eta_expand : typ list -> term -> int -> term
   val distinctness_formula : typ -> term list -> term
   val register_frac_type :
-    string -> (string * string) list -> Proof.context -> Proof.context
+    string -> (string * string) list -> morphism -> Context.generic
+    -> Context.generic
   val register_frac_type_global :
     string -> (string * string) list -> theory -> theory
-  val unregister_frac_type : string -> Proof.context -> Proof.context
+  val unregister_frac_type :
+    string -> morphism -> Context.generic -> Context.generic
   val unregister_frac_type_global : string -> theory -> theory
-  val register_codatatype_generic :
-    typ -> string -> styp list -> Context.generic -> Context.generic
   val register_codatatype :
-    typ -> string -> styp list -> Proof.context -> Proof.context
+    typ -> string -> styp list -> morphism -> Context.generic -> Context.generic
   val register_codatatype_global :
     typ -> string -> styp list -> theory -> theory
-  val unregister_codatatype : typ -> Proof.context -> Proof.context
+  val unregister_codatatype :
+    typ -> morphism -> Context.generic -> Context.generic
   val unregister_codatatype_global : typ -> theory -> theory
   val datatype_constrs : hol_context -> typ -> styp list
   val binarized_and_boxed_datatype_constrs :
@@ -633,11 +634,15 @@
     val {frac_types, 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
-val register_frac_type = Context.proof_map oo register_frac_type_generic
+(* TODO: Consider morphism. *)
+fun register_frac_type frac_s ersaetze (_ : morphism) =
+  register_frac_type_generic frac_s ersaetze
 val register_frac_type_global = Context.theory_map oo register_frac_type_generic
 
 fun unregister_frac_type_generic frac_s = register_frac_type_generic frac_s []
-val unregister_frac_type = Context.proof_map o unregister_frac_type_generic
+(* TODO: Consider morphism. *)
+fun unregister_frac_type frac_s (_ : morphism) =
+  unregister_frac_type_generic frac_s
 val unregister_frac_type_global =
   Context.theory_map o unregister_frac_type_generic
 
@@ -658,12 +663,16 @@
     val codatatypes = AList.update (op =) (co_s, (case_name, constr_xs))
                                    codatatypes
   in Data.put {frac_types = frac_types, codatatypes = codatatypes} generic end
-val register_codatatype = Context.proof_map ooo register_codatatype_generic
+(* TODO: Consider morphism. *)
+fun register_codatatype co_T case_name constr_xs (_ : morphism) =
+  register_codatatype_generic co_T case_name constr_xs
 val register_codatatype_global =
   Context.theory_map ooo register_codatatype_generic
 
 fun unregister_codatatype_generic co_T = register_codatatype_generic co_T "" []
-val unregister_codatatype = Context.proof_map o unregister_codatatype_generic
+(* TODO: Consider morphism. *)
+fun unregister_codatatype co_T (_ : morphism) =
+  unregister_codatatype_generic co_T
 val unregister_codatatype_global =
   Context.theory_map o unregister_codatatype_generic
 
diff -r 1dac99cc8dbd -r 9f98107ad8b4 src/HOL/Tools/Nitpick/nitpick_model.ML
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 09 12:07:59 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Aug 09 12:40:15 2010 +0200
@@ -25,10 +25,11 @@
   val unknown : string
   val unrep : unit -> string
   val register_term_postprocessor :
-    typ -> term_postprocessor -> Proof.context -> Proof.context
+    typ -> term_postprocessor -> morphism -> Context.generic -> Context.generic
   val register_term_postprocessor_global :
     typ -> term_postprocessor -> theory -> theory
-  val unregister_term_postprocessor : typ -> Proof.context -> Proof.context
+  val unregister_term_postprocessor :
+    typ -> morphism -> Context.generic -> Context.generic
   val unregister_term_postprocessor_global : typ -> theory -> theory
   val tuple_list_for_name :
     nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
@@ -158,15 +159,18 @@
               | ord => ord)
            | _ => Term_Ord.fast_term_ord tp
 
-fun register_term_postprocessor_generic T p = Data.map (cons (T, p))
-val register_term_postprocessor =
-  Context.proof_map oo register_term_postprocessor_generic
+fun register_term_postprocessor_generic T postproc =
+  Data.map (cons (T, postproc))
+(* TODO: Consider morphism. *)
+fun register_term_postprocessor T postproc (_ : morphism) =
+  register_term_postprocessor_generic T postproc
 val register_term_postprocessor_global =
   Context.theory_map oo register_term_postprocessor_generic
 
 fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
-val unregister_term_postprocessor =
-  Context.proof_map o unregister_term_postprocessor_generic
+(* TODO: Consider morphism. *)
+fun unregister_term_postprocessor T (_ : morphism) =
+  unregister_term_postprocessor_generic T
 val unregister_term_postprocessor_global =
   Context.theory_map o unregister_term_postprocessor_generic