improved "set" support by code inspection
authorblanchet
Wed Jan 04 12:09:53 2012 +0100 (2012-01-04)
changeset 46115ecab67f5a5c2
parent 46114 e6d33b200f42
child 46116 b903d272c37d
improved "set" support by code inspection
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Wed Jan 04 12:09:53 2012 +0100
     1.3 @@ -87,6 +87,8 @@
     1.4    val frac_from_term_pair : typ -> term -> term -> term
     1.5    val is_TFree : typ -> bool
     1.6    val is_fun_type : typ -> bool
     1.7 +  val is_set_type : typ -> bool
     1.8 +  val is_fun_or_set_type : typ -> bool
     1.9    val is_set_like_type : typ -> bool
    1.10    val is_pair_type : typ -> bool
    1.11    val is_lfp_iterator_type : typ -> bool
    1.12 @@ -482,7 +484,11 @@
    1.13    | is_TFree _ = false
    1.14  fun is_fun_type (Type (@{type_name fun}, _)) = true
    1.15    | is_fun_type _ = false
    1.16 -fun is_set_like_type (Type (@{type_name fun}, [_, @{typ bool}])) = true
    1.17 +fun is_set_type (Type (@{type_name set}, _)) = true
    1.18 +  | is_set_type _ = false
    1.19 +val is_fun_or_set_type = is_fun_type orf is_set_type
    1.20 +fun is_set_like_type (Type (@{type_name fun}, [_, T'])) =
    1.21 +    (body_type T' = bool_T)
    1.22    | is_set_like_type (Type (@{type_name set}, _)) = true
    1.23    | is_set_like_type _ = false
    1.24  fun is_pair_type (Type (@{type_name prod}, _)) = true
    1.25 @@ -506,6 +512,7 @@
    1.26    | is_frac_type _ _ = false
    1.27  fun is_number_type ctxt = is_integer_like_type orf is_frac_type ctxt
    1.28  fun is_higher_order_type (Type (@{type_name fun}, _)) = true
    1.29 +  | is_higher_order_type (Type (@{type_name set}, _)) = true
    1.30    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    1.31    | is_higher_order_type _ = false
    1.32  
    1.33 @@ -1816,7 +1823,7 @@
    1.34  (** Axiom extraction/generation **)
    1.35  
    1.36  fun extensional_equal j T t1 t2 =
    1.37 -  if is_fun_type T orelse is_set_like_type T then
    1.38 +  if is_fun_or_set_type T then
    1.39      let
    1.40        val dom_T = pseudo_domain_type T
    1.41        val ran_T = pseudo_range_type T
    1.42 @@ -2233,7 +2240,7 @@
    1.43    end
    1.44  
    1.45  fun is_good_starred_linear_pred_type (Type (@{type_name fun}, Ts)) =
    1.46 -    forall (not o (is_fun_type orf is_pair_type)) Ts
    1.47 +    forall (not o (is_fun_or_set_type orf is_pair_type)) Ts
    1.48    | is_good_starred_linear_pred_type _ = false
    1.49  
    1.50  fun unrolled_inductive_pred_const (hol_ctxt as {thy, star_linear_preds,
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jan 04 12:09:53 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Wed Jan 04 12:09:53 2012 +0100
     2.3 @@ -682,7 +682,8 @@
     2.4      val (s', T') = binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize x n
     2.5      val R' = if n = ~1 orelse is_word_type (body_type T) orelse
     2.6                  (is_fun_type (range_type T') andalso
     2.7 -                 is_boolean_type (body_type T')) then
     2.8 +                 is_boolean_type (body_type T')) orelse
     2.9 +                (is_set_type (body_type T')) then
    2.10                 best_non_opt_set_rep_for_type scope T'
    2.11               else
    2.12                 best_opt_set_rep_for_type scope T' |> unopt_rep
    2.13 @@ -718,7 +719,8 @@
    2.14     is representable or "Unrep", because unknown implies "Unrep". *)
    2.15  fun is_constructive u =
    2.16    is_Cst Unrep u orelse
    2.17 -  (not (is_fun_type (type_of u)) andalso not (is_opt_rep (rep_of u))) orelse
    2.18 +  (not (is_fun_or_set_type (type_of u)) andalso
    2.19 +   not (is_opt_rep (rep_of u))) orelse
    2.20    case u of
    2.21      Cst (Num _, _, _) => true
    2.22    | Cst (cst, T, _) => body_type T = nat_T andalso (cst = Suc orelse cst = Add)
    2.23 @@ -807,8 +809,9 @@
    2.24      fun triad_fn f = triad (f Pos) (f Neg)
    2.25      fun unrepify_nut_in_nut table def polar needle_u =
    2.26        let val needle_T = type_of needle_u in
    2.27 -        substitute_in_nut needle_u (Cst (if is_fun_type needle_T then Unknown
    2.28 -                                         else Unrep, needle_T, Any))
    2.29 +        substitute_in_nut needle_u
    2.30 +            (Cst (if is_fun_or_set_type needle_T then Unknown
    2.31 +                  else Unrep, needle_T, Any))
    2.32          #> aux table def polar
    2.33        end
    2.34      and aux table def polar u =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Jan 04 12:09:53 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Wed Jan 04 12:09:53 2012 +0100
     3.3 @@ -301,7 +301,7 @@
     3.4  fun has_heavy_bounds_or_vars Ts t =
     3.5    let
     3.6      fun aux [] = false
     3.7 -      | aux [T] = is_fun_type T orelse is_pair_type T
     3.8 +      | aux [T] = is_fun_or_set_type T orelse is_pair_type T
     3.9        | aux _ = true
    3.10    in aux (map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t)) end
    3.11  
    3.12 @@ -311,7 +311,7 @@
    3.13      case t of
    3.14        Const x =>
    3.15        if not relax andalso is_constr ctxt stds x andalso
    3.16 -         not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
    3.17 +         not (is_fun_or_set_type (fastype_of1 (Ts, t_comb))) andalso
    3.18           has_heavy_bounds_or_vars Ts t_comb andalso
    3.19           not (loose_bvar (t_comb, level)) then
    3.20          let
    3.21 @@ -1009,6 +1009,7 @@
    3.22        case T of
    3.23          Type (@{type_name fun}, Ts) => fold (add_axioms_for_type depth) Ts
    3.24        | Type (@{type_name prod}, Ts) => fold (add_axioms_for_type depth) Ts
    3.25 +      | Type (@{type_name set}, Ts) => fold (add_axioms_for_type depth) Ts
    3.26        | @{typ prop} => I
    3.27        | @{typ bool} => I
    3.28        | TFree (_, S) => add_axioms_for_sort depth T S