src/HOL/Tools/Nitpick/nitpick_model.ML
changeset 38240 a44d108a8d39
parent 38209 3d1d928dce50
child 38284 9f98107ad8b4
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Aug 06 11:37:33 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Fri Aug 06 17:05:29 2010 +0200
     1.3 @@ -25,8 +25,11 @@
     1.4    val unknown : string
     1.5    val unrep : unit -> string
     1.6    val register_term_postprocessor :
     1.7 +    typ -> term_postprocessor -> Proof.context -> Proof.context
     1.8 +  val register_term_postprocessor_global :
     1.9      typ -> term_postprocessor -> theory -> theory
    1.10 -  val unregister_term_postprocessor : typ -> theory -> theory
    1.11 +  val unregister_term_postprocessor : typ -> Proof.context -> Proof.context
    1.12 +  val unregister_term_postprocessor_global : typ -> theory -> theory
    1.13    val tuple_list_for_name :
    1.14      nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
    1.15    val dest_plain_fun : term -> bool * (term list * term list)
    1.16 @@ -59,7 +62,7 @@
    1.17  type term_postprocessor =
    1.18    Proof.context -> string -> (typ -> term list) -> typ -> term -> term
    1.19  
    1.20 -structure Data = Theory_Data(
    1.21 +structure Data = Generic_Data(
    1.22    type T = (typ * term_postprocessor) list
    1.23    val empty = []
    1.24    val extend = I
    1.25 @@ -155,8 +158,17 @@
    1.26                | ord => ord)
    1.27             | _ => Term_Ord.fast_term_ord tp
    1.28  
    1.29 -fun register_term_postprocessor T p = Data.map (cons (T, p))
    1.30 -fun unregister_term_postprocessor T = Data.map (AList.delete (op =) T)
    1.31 +fun register_term_postprocessor_generic T p = Data.map (cons (T, p))
    1.32 +val register_term_postprocessor =
    1.33 +  Context.proof_map oo register_term_postprocessor_generic
    1.34 +val register_term_postprocessor_global =
    1.35 +  Context.theory_map oo register_term_postprocessor_generic
    1.36 +
    1.37 +fun unregister_term_postprocessor_generic T = Data.map (AList.delete (op =) T)
    1.38 +val unregister_term_postprocessor =
    1.39 +  Context.proof_map o unregister_term_postprocessor_generic
    1.40 +val unregister_term_postprocessor_global =
    1.41 +  Context.theory_map o unregister_term_postprocessor_generic
    1.42  
    1.43  fun tuple_list_for_name rel_table bounds name =
    1.44    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
    1.45 @@ -309,8 +321,10 @@
    1.46    | mk_tuple _ (t :: _) = t
    1.47    | mk_tuple T [] = raise TYPE ("Nitpick_Model.mk_tuple", [T], [])
    1.48  
    1.49 -fun varified_type_match thy (candid_T, pat_T) =
    1.50 -  strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
    1.51 +fun varified_type_match ctxt (candid_T, pat_T) =
    1.52 +  let val thy = ProofContext.theory_of ctxt in
    1.53 +    strict_type_match thy (candid_T, varify_type ctxt pat_T)
    1.54 +  end
    1.55  
    1.56  fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
    1.57                         atomss sel_names rel_table bounds card T =
    1.58 @@ -351,11 +365,12 @@
    1.59                           bounds 0
    1.60      fun postprocess_term (Type (@{type_name fun}, _)) = I
    1.61        | postprocess_term T =
    1.62 -        if null (Data.get thy) then
    1.63 -          I
    1.64 -        else case AList.lookup (varified_type_match thy) (Data.get thy) T of
    1.65 -          SOME postproc => postproc ctxt maybe_name all_values T
    1.66 -        | NONE => I
    1.67 +        case Data.get (Context.Proof ctxt) of
    1.68 +          [] => I
    1.69 +        | postprocs =>
    1.70 +          case AList.lookup (varified_type_match ctxt) postprocs T of
    1.71 +            SOME postproc => postproc ctxt maybe_name all_values T
    1.72 +          | NONE => I
    1.73      fun postprocess_subterms Ts (t1 $ t2) =
    1.74          let val t = postprocess_subterms Ts t1 $ postprocess_subterms Ts t2 in
    1.75            postprocess_term (fastype_of1 (Ts, t)) t