1.1 --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 10:13:24 2010 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy	Thu Mar 11 12:22:11 2010 +0100
     1.3 @@ -117,6 +117,19 @@
     1.4  nitpick [show_datatypes, expect = genuine]
     1.5  oops
     1.6  
     1.7 +ML {*
     1.8 +(* Proof.context -> typ -> term -> term *)
     1.9 +fun my_int_postproc _ T (Const _ $ (Const _ $ t1 $ t2)) =
    1.10 +    HOLogic.mk_number T (snd (HOLogic.dest_number t1) - snd (HOLogic.dest_number t2))
    1.11 +  | my_int_postproc _ _ t = t
    1.12 +*}
    1.13 +
    1.14 +setup {* Nitpick.register_term_postprocessor @{typ my_int} my_int_postproc *}
    1.15 +
    1.16 +lemma "add x y = add x x"
    1.17 +nitpick [show_datatypes]
    1.18 +oops
    1.19 +
    1.20  record point =
    1.21    Xcoord :: int
    1.22    Ycoord :: int

     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 11 10:13:24 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Mar 11 12:22:11 2010 +0100
     2.3 @@ -8,6 +8,7 @@
     2.4  signature NITPICK =
     2.5  sig
     2.6    type styp = Nitpick_Util.styp
     2.7 +  type term_postprocessor = Nitpick_Model.term_postprocessor
     2.8    type params = {
     2.9      cards_assigns: (typ option * int list) list,
    2.10      maxes_assigns: (styp option * int list) list,
    2.11 @@ -58,6 +59,9 @@
    2.12    val unregister_frac_type : string -> theory -> theory
    2.13    val register_codatatype : typ -> string -> styp list -> theory -> theory
    2.14    val unregister_codatatype : typ -> theory -> theory
    2.15 +  val register_term_postprocessor :
    2.16 +    typ -> term_postprocessor -> theory -> theory
    2.17 +  val unregister_term_postprocessor : typ -> theory -> theory
    2.18    val pick_nits_in_term :
    2.19      Proof.state -> params -> bool -> int -> int -> int -> (term * term) list
    2.20      -> term list -> term -> string * Proof.state

     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 11 10:13:24 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Mar 11 12:22:11 2010 +0100
     3.3 @@ -72,9 +72,11 @@
     3.4    val shortest_name : string -> string
     3.5    val short_name : string -> string
     3.6    val shorten_names_in_term : term -> term
     3.7 +  val strict_type_match : theory -> typ * typ -> bool
     3.8    val type_match : theory -> typ * typ -> bool
     3.9    val const_match : theory -> styp * styp -> bool
    3.10    val term_match : theory -> term * term -> bool
    3.11 +  val frac_from_term_pair : typ -> term -> term -> term
    3.12    val is_TFree : typ -> bool
    3.13    val is_higher_order_type : typ -> bool
    3.14    val is_fun_type : typ -> bool
    3.15 @@ -457,6 +459,15 @@
    3.16      const_match thy ((shortest_name s1, T1), (shortest_name s2, T2))
    3.17    | term_match _ (t1, t2) = t1 aconv t2
    3.18  
    3.19 +(* typ -> term -> term -> term *)
    3.20 +fun frac_from_term_pair T t1 t2 =
    3.21 +  case snd (HOLogic.dest_number t1) of
    3.22 +    0 => HOLogic.mk_number T 0
    3.23 +  | n1 => case snd (HOLogic.dest_number t2) of
    3.24 +            1 => HOLogic.mk_number T n1
    3.25 +          | n2 => Const (@{const_name divide}, T --> T --> T)
    3.26 +                  $ HOLogic.mk_number T n1 $ HOLogic.mk_number T n2
    3.27 +
    3.28  (* typ -> bool *)
    3.29  fun is_TFree (TFree _) = true
    3.30    | is_TFree _ = false

     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 10:13:24 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 12:22:11 2010 +0100
     4.3 @@ -16,9 +16,13 @@
     4.4      show_skolems: bool,
     4.5      show_datatypes: bool,
     4.6      show_consts: bool}
     4.7 +  type term_postprocessor = Proof.context -> typ -> term -> term
     4.8  
     4.9    structure NameTable : TABLE
    4.10  
    4.11 +  val register_term_postprocessor :
    4.12 +    typ -> term_postprocessor -> theory -> theory
    4.13 +  val unregister_term_postprocessor : typ -> theory -> theory
    4.14    val tuple_list_for_name :
    4.15      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
    4.16    val reconstruct_hol_model :
    4.17 @@ -47,6 +51,14 @@
    4.18    show_datatypes: bool,
    4.19    show_consts: bool}
    4.20  
    4.21 +type term_postprocessor = Proof.context -> typ -> term -> term
    4.22 +
    4.23 +structure Data = Theory_Data(
    4.24 +  type T = (typ * term_postprocessor) list
    4.25 +  val empty = []
    4.26 +  val extend = I
    4.27 +  fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
    4.28 +
    4.29  val unknown = "?"
    4.30  val unrep = "\<dots>"
    4.31  val maybe_mixfix = "_\<^sup>?"
    4.32 @@ -105,6 +117,11 @@
    4.33                | ord => ord)
    4.34             | _ => Term_Ord.fast_term_ord tp
    4.35  
    4.36 +(* typ -> term_postprocessor -> theory -> theory *)
    4.37 +fun register_term_postprocessor T p = Data.map (cons (T, p))
    4.38 +(* typ -> theory -> theory *)
    4.39 +fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
    4.40 +
    4.41  (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
    4.42  fun tuple_list_for_name rel_table bounds name =
    4.43    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
    4.44 @@ -271,12 +288,25 @@
    4.45    | mk_tuple _ (t :: _) = t
    4.46    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    4.47  
    4.48 +(* theory -> typ * typ -> bool *)
    4.49 +fun varified_type_match thy (candid_T, pat_T) =
    4.50 +  strict_type_match thy (candid_T, Logic.varifyT pat_T)
    4.51 +(* Proof.context -> typ -> term -> term *)
    4.52 +fun postprocess_term ctxt T =
    4.53 +  let val thy = ProofContext.theory_of ctxt in
    4.54 +    if null (Data.get thy) then
    4.55 +      I
    4.56 +    else
    4.57 +      (T |> AList.lookup (varified_type_match thy) (Data.get thy)
    4.58 +         |> the_default (K (K I))) ctxt T
    4.59 +  end
    4.60 +
    4.61  (* bool -> atom_pool -> (string * string) * (string * string) -> scope
    4.62     -> nut list -> nut list -> nut list -> nut NameTable.table
    4.63     -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
    4.64  fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
    4.65 -        ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
    4.66 -          ofs, ...} : scope) sel_names rel_table bounds =
    4.67 +        ({hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns, bits,
    4.68 +          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
    4.69    let
    4.70      val for_auto = (maybe_name = "")
    4.71      (* int list list -> int *)
    4.72 @@ -476,23 +506,11 @@
    4.73                      |> dest_n_tuple (length uncur_arg_Ts)
    4.74                  val t =
    4.75                    if constr_s = @{const_name Abs_Frac} then
    4.76 -                    let
    4.77 -                      val num_T = body_type T
    4.78 -                      (* int -> term *)
    4.79 -                      val mk_num = HOLogic.mk_number num_T
    4.80 -                    in
    4.81 -                      case ts of
    4.82 -                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    4.83 -                        (case snd (HOLogic.dest_number t1) of
    4.84 -                           0 => mk_num 0
    4.85 -                         | n1 => case HOLogic.dest_number t2 |> snd of
    4.86 -                                   1 => mk_num n1
    4.87 -                                 | n2 => Const (@{const_name divide},
    4.88 -                                                num_T --> num_T --> num_T)
    4.89 -                                         $ mk_num n1 $ mk_num n2)
    4.90 -                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
    4.91 -                                         \term_for_atom (Abs_Frac)", ts)
    4.92 -                    end
    4.93 +                    case ts of
    4.94 +                      [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    4.95 +                      frac_from_term_pair (body_type T) t1 t2
    4.96 +                    | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
    4.97 +                                       \term_for_atom (Abs_Frac)", ts)
    4.98                    else if not for_auto andalso
    4.99                            (is_abs_fun thy constr_x orelse
   4.100                             constr_s = @{const_name Quot}) then
   4.101 @@ -523,6 +541,7 @@
   4.102                    t
   4.103                end
   4.104            end
   4.105 +          |> postprocess_term ctxt T
   4.106      (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
   4.107         -> term *)
   4.108      and term_for_vect seen k R T1 T2 T' js =