src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 35711 548d3f16404b
parent 35665 ff2bf50505ab
child 35712 77aa29bf14ee
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 10:13:24 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Thu Mar 11 12:22:11 2010 +0100
     1.3 @@ -16,9 +16,13 @@
     1.4      show_skolems: bool,
     1.5      show_datatypes: bool,
     1.6      show_consts: bool}
     1.7 +  type term_postprocessor = Proof.context -> typ -> term -> term
     1.8  
     1.9    structure NameTable : TABLE
    1.10  
    1.11 +  val register_term_postprocessor :
    1.12 +    typ -> term_postprocessor -> theory -> theory
    1.13 +  val unregister_term_postprocessor : typ -> theory -> theory
    1.14    val tuple_list_for_name :
    1.15      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
    1.16    val reconstruct_hol_model :
    1.17 @@ -47,6 +51,14 @@
    1.18    show_datatypes: bool,
    1.19    show_consts: bool}
    1.20  
    1.21 +type term_postprocessor = Proof.context -> typ -> term -> term
    1.22 +
    1.23 +structure Data = Theory_Data(
    1.24 +  type T = (typ * term_postprocessor) list
    1.25 +  val empty = []
    1.26 +  val extend = I
    1.27 +  fun merge (ps1, ps2) = AList.merge (op =) (K true) (ps1, ps2))
    1.28 +
    1.29  val unknown = "?"
    1.30  val unrep = "\<dots>"
    1.31  val maybe_mixfix = "_\<^sup>?"
    1.32 @@ -105,6 +117,11 @@
    1.33                | ord => ord)
    1.34             | _ => Term_Ord.fast_term_ord tp
    1.35  
    1.36 +(* typ -> term_postprocessor -> theory -> theory *)
    1.37 +fun register_term_postprocessor T p = Data.map (cons (T, p))
    1.38 +(* typ -> theory -> theory *)
    1.39 +fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
    1.40 +
    1.41  (* nut NameTable.table -> KK.raw_bound list -> nut -> int list list *)
    1.42  fun tuple_list_for_name rel_table bounds name =
    1.43    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
    1.44 @@ -271,12 +288,25 @@
    1.45    | mk_tuple _ (t :: _) = t
    1.46    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.47  
    1.48 +(* theory -> typ * typ -> bool *)
    1.49 +fun varified_type_match thy (candid_T, pat_T) =
    1.50 +  strict_type_match thy (candid_T, Logic.varifyT pat_T)
    1.51 +(* Proof.context -> typ -> term -> term *)
    1.52 +fun postprocess_term ctxt T =
    1.53 +  let val thy = ProofContext.theory_of ctxt in
    1.54 +    if null (Data.get thy) then
    1.55 +      I
    1.56 +    else
    1.57 +      (T |> AList.lookup (varified_type_match thy) (Data.get thy)
    1.58 +         |> the_default (K (K I))) ctxt T
    1.59 +  end
    1.60 +
    1.61  (* bool -> atom_pool -> (string * string) * (string * string) -> scope
    1.62     -> nut list -> nut list -> nut list -> nut NameTable.table
    1.63     -> KK.raw_bound list -> typ -> typ -> rep -> int list list -> term *)
    1.64  fun reconstruct_term unfold pool ((maybe_name, abs_name), _)
    1.65 -        ({hol_ctxt as {thy, stds, ...}, binarize, card_assigns, bits, datatypes,
    1.66 -          ofs, ...} : scope) sel_names rel_table bounds =
    1.67 +        ({hol_ctxt as {ctxt, thy, stds, ...}, binarize, card_assigns, bits,
    1.68 +          datatypes, ofs, ...} : scope) sel_names rel_table bounds =
    1.69    let
    1.70      val for_auto = (maybe_name = "")
    1.71      (* int list list -> int *)
    1.72 @@ -476,23 +506,11 @@
    1.73                      |> dest_n_tuple (length uncur_arg_Ts)
    1.74                  val t =
    1.75                    if constr_s = @{const_name Abs_Frac} then
    1.76 -                    let
    1.77 -                      val num_T = body_type T
    1.78 -                      (* int -> term *)
    1.79 -                      val mk_num = HOLogic.mk_number num_T
    1.80 -                    in
    1.81 -                      case ts of
    1.82 -                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    1.83 -                        (case snd (HOLogic.dest_number t1) of
    1.84 -                           0 => mk_num 0
    1.85 -                         | n1 => case HOLogic.dest_number t2 |> snd of
    1.86 -                                   1 => mk_num n1
    1.87 -                                 | n2 => Const (@{const_name divide},
    1.88 -                                                num_T --> num_T --> num_T)
    1.89 -                                         $ mk_num n1 $ mk_num n2)
    1.90 -                      | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
    1.91 -                                         \term_for_atom (Abs_Frac)", ts)
    1.92 -                    end
    1.93 +                    case ts of
    1.94 +                      [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    1.95 +                      frac_from_term_pair (body_type T) t1 t2
    1.96 +                    | _ => raise TERM ("Nitpick_Model.reconstruct_term.\
    1.97 +                                       \term_for_atom (Abs_Frac)", ts)
    1.98                    else if not for_auto andalso
    1.99                            (is_abs_fun thy constr_x orelse
   1.100                             constr_s = @{const_name Quot}) then
   1.101 @@ -523,6 +541,7 @@
   1.102                    t
   1.103                end
   1.104            end
   1.105 +          |> postprocess_term ctxt T
   1.106      (* (typ * int) list -> int -> rep -> typ -> typ -> typ -> int list
   1.107         -> term *)
   1.108      and term_for_vect seen k R T1 T2 T' js =