cosmetics
authorblanchet
Thu Feb 25 10:08:44 2010 +0100 (2010-02-25)
changeset 3538488dbcfe75c45
parent 35358 63fb71d29eba
child 35385 29f81babefd7
cosmetics
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 09:16:16 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 10:08:44 2010 +0100
     1.3 @@ -342,7 +342,7 @@
     1.4        case triple_lookup (type_match thy) monos T of
     1.5          SOME (SOME b) => b
     1.6        | _ => is_type_always_monotonic T orelse
     1.7 -             formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
     1.8 +             formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
     1.9      fun is_deep_datatype T =
    1.10        is_datatype thy stds T andalso
    1.11        (not standard orelse T = nat_T orelse is_word_type T orelse
    1.12 @@ -834,8 +834,8 @@
    1.13                          sound_problems then
    1.14                  print_m (fn () =>
    1.15                      "Warning: The conjecture either trivially holds for the \
    1.16 -                    \given scopes or (more likely) lies outside Nitpick's \
    1.17 -                    \supported fragment." ^
    1.18 +                    \given scopes or lies outside Nitpick's supported \
    1.19 +                    \fragment." ^
    1.20                      (if exists (not o KK.is_problem_trivially_false o fst)
    1.21                                 unsound_problems then
    1.22                         " Only potential counterexamples may be found."
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 09:16:16 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 10:08:44 2010 +0100
     2.3 @@ -1096,8 +1096,8 @@
     2.4    in Int.min (max, aux [] T) end
     2.5  
     2.6  (* hol_context -> typ -> bool *)
     2.7 -fun is_finite_type hol_ctxt =
     2.8 -  not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
     2.9 +fun is_finite_type hol_ctxt T =
    2.10 +  bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
    2.11  
    2.12  (* term -> bool *)
    2.13  fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 09:16:16 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 10:08:44 2010 +0100
     3.3 @@ -2,16 +2,15 @@
     3.4      Author:     Jasmin Blanchette, TU Muenchen
     3.5      Copyright   2009, 2010
     3.6  
     3.7 -Monotonicity predicate for higher-order logic.
     3.8 +Monotonicity inference for higher-order logic.
     3.9  *)
    3.10  
    3.11  signature NITPICK_MONO =
    3.12  sig
    3.13 -  datatype sign = Plus | Minus
    3.14    type hol_context = Nitpick_HOL.hol_context
    3.15  
    3.16    val formulas_monotonic :
    3.17 -    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
    3.18 +    hol_context -> bool -> typ -> term list * term list * term -> bool
    3.19  end;
    3.20  
    3.21  structure Nitpick_Mono : NITPICK_MONO =
    3.22 @@ -270,8 +269,13 @@
    3.23    if could_exist_alpha_sub_ctype thy alpha_T T then
    3.24      case AList.lookup (op =) (!constr_cache) x of
    3.25        SOME C => C
    3.26 -    | NONE => (fresh_ctype_for_type cdata (body_type T);
    3.27 -               AList.lookup (op =) (!constr_cache) x |> the)
    3.28 +    | NONE => if T = alpha_T then
    3.29 +                let val C = fresh_ctype_for_type cdata T in
    3.30 +                  (Unsynchronized.change constr_cache (cons (x, C)); C)
    3.31 +                end
    3.32 +              else
    3.33 +                (fresh_ctype_for_type cdata (body_type T);
    3.34 +                 AList.lookup (op =) (!constr_cache) x |> the)
    3.35    else
    3.36      fresh_ctype_for_type cdata T
    3.37  fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
    3.38 @@ -435,12 +439,13 @@
    3.39  val add_ctype_is_right_unique = add_notin_ctype_fv Minus
    3.40  val add_ctype_is_right_total = add_notin_ctype_fv Plus
    3.41  
    3.42 +val bool_from_minus = true
    3.43 +
    3.44  (* sign -> bool *)
    3.45 -fun bool_from_sign Plus = false
    3.46 -  | bool_from_sign Minus = true
    3.47 +fun bool_from_sign Plus = not bool_from_minus
    3.48 +  | bool_from_sign Minus = bool_from_minus
    3.49  (* bool -> sign *)
    3.50 -fun sign_from_bool false = Plus
    3.51 -  | sign_from_bool true = Minus
    3.52 +fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
    3.53  
    3.54  (* literal -> PropLogic.prop_formula *)
    3.55  fun prop_for_literal (x, sn) =
    3.56 @@ -492,7 +497,7 @@
    3.57               "-: " ^ commas (map (string_for_var o fst) neg))
    3.58    end
    3.59  
    3.60 -(* var -> constraint_set -> literal list list option *)
    3.61 +(* var -> constraint_set -> literal list option *)
    3.62  fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
    3.63    | solve max_var (CSet (lits, comps, sexps)) =
    3.64      let
    3.65 @@ -812,8 +817,8 @@
    3.66                val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
    3.67                val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
    3.68              in
    3.69 -              (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
    3.70 -                                                |>> pop_bound
    3.71 +              (gamma |> push_bound abs_C, cset)
    3.72 +              |> do_co_formula body_t |>> pop_bound
    3.73              end
    3.74            (* typ -> term -> accumulator *)
    3.75            fun do_bounded_quantifier abs_T body_t =
    3.76 @@ -932,19 +937,20 @@
    3.77    map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
    3.78    |> cat_lines |> print_g
    3.79  
    3.80 -(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
    3.81 -   -> bool *)
    3.82 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
    3.83 -                       nondef_ts core_t =
    3.84 +(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
    3.85 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
    3.86 +                       (def_ts, nondef_ts, core_t) =
    3.87    let
    3.88 -    val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
    3.89 +    val _ = print_g ("****** Monotonicity analysis: " ^
    3.90 +                     string_for_ctype CAlpha ^ " is " ^
    3.91                       Syntax.string_of_typ ctxt alpha_T)
    3.92 -    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
    3.93 -    val (gamma, cset) =
    3.94 +    val cdata as {max_fresh, constr_cache, ...} =
    3.95 +      initial_cdata hol_ctxt binarize alpha_T
    3.96 +    val (gamma as {frees, consts, ...}, cset) =
    3.97        (initial_gamma, slack)
    3.98        |> fold (consider_definitional_axiom cdata) def_ts
    3.99        |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
   3.100 -      |> consider_general_formula cdata sn core_t
   3.101 +      |> consider_general_formula cdata Plus core_t
   3.102    in
   3.103      case solve (!max_fresh) cset of
   3.104        SOME lits => (print_ctype_context ctxt lits gamma; true)
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 09:16:16 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 10:08:44 2010 +0100
     4.3 @@ -136,6 +136,60 @@
     4.4                                       (index_seq 0 (length arg_Ts)) arg_Ts)
     4.5           end
     4.6  
     4.7 +(* (term -> term) -> int -> term -> term *)
     4.8 +fun coerce_bound_no f j t =
     4.9 +  case t of
    4.10 +    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
    4.11 +  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
    4.12 +  | Bound j' => if j' = j then f t else t
    4.13 +  | _ => t
    4.14 +(* hol_context -> typ -> typ -> term -> term *)
    4.15 +fun coerce_bound_0_in_term hol_ctxt new_T old_T =
    4.16 +  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
    4.17 +(* hol_context -> typ list -> typ -> typ -> term -> term *)
    4.18 +and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
    4.19 +  if old_T = new_T then
    4.20 +    t
    4.21 +  else
    4.22 +    case (new_T, old_T) of
    4.23 +      (Type (new_s, new_Ts as [new_T1, new_T2]),
    4.24 +       Type ("fun", [old_T1, old_T2])) =>
    4.25 +      (case eta_expand Ts t 1 of
    4.26 +         Abs (s, _, t') =>
    4.27 +         Abs (s, new_T1,
    4.28 +              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
    4.29 +                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
    4.30 +         |> Envir.eta_contract
    4.31 +         |> new_s <> "fun"
    4.32 +            ? construct_value thy stds
    4.33 +                  (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
    4.34 +                  o single
    4.35 +       | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
    4.36 +    | (Type (new_s, new_Ts as [new_T1, new_T2]),
    4.37 +       Type (old_s, old_Ts as [old_T1, old_T2])) =>
    4.38 +      if old_s = @{type_name fun_box} orelse
    4.39 +         old_s = @{type_name fin_fun} orelse
    4.40 +         old_s = @{type_name pair_box} orelse old_s = "*" then
    4.41 +        case constr_expand hol_ctxt old_T t of
    4.42 +          Const (old_s, _) $ t1 =>
    4.43 +          if new_s = "fun" then
    4.44 +            coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
    4.45 +          else
    4.46 +            construct_value thy stds
    4.47 +                (old_s, Type ("fun", new_Ts) --> new_T)
    4.48 +                [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
    4.49 +                             (Type ("fun", old_Ts)) t1]
    4.50 +        | Const _ $ t1 $ t2 =>
    4.51 +          construct_value thy stds
    4.52 +              (if new_s = "*" then @{const_name Pair}
    4.53 +               else @{const_name PairBox}, new_Ts ---> new_T)
    4.54 +              [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
    4.55 +               coerce_term hol_ctxt Ts new_T2 old_T2 t2]
    4.56 +        | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
    4.57 +      else
    4.58 +        raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
    4.59 +    | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
    4.60 +
    4.61  (* hol_context -> bool -> term -> term *)
    4.62  fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
    4.63                               orig_t =
    4.64 @@ -146,60 +200,6 @@
    4.65        | box_relational_operator_type (Type ("*", Ts)) =
    4.66          Type ("*", map (box_type hol_ctxt InPair) Ts)
    4.67        | box_relational_operator_type T = T
    4.68 -    (* (term -> term) -> int -> term -> term *)
    4.69 -    fun coerce_bound_no f j t =
    4.70 -      case t of
    4.71 -        t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
    4.72 -      | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
    4.73 -      | Bound j' => if j' = j then f t else t
    4.74 -      | _ => t
    4.75 -    (* typ -> typ -> term -> term *)
    4.76 -    fun coerce_bound_0_in_term new_T old_T =
    4.77 -      old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
    4.78 -    (* typ list -> typ -> term -> term *)
    4.79 -    and coerce_term Ts new_T old_T t =
    4.80 -      if old_T = new_T then
    4.81 -        t
    4.82 -      else
    4.83 -        case (new_T, old_T) of
    4.84 -          (Type (new_s, new_Ts as [new_T1, new_T2]),
    4.85 -           Type ("fun", [old_T1, old_T2])) =>
    4.86 -          (case eta_expand Ts t 1 of
    4.87 -             Abs (s, _, t') =>
    4.88 -             Abs (s, new_T1,
    4.89 -                  t' |> coerce_bound_0_in_term new_T1 old_T1
    4.90 -                     |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
    4.91 -             |> Envir.eta_contract
    4.92 -             |> new_s <> "fun"
    4.93 -                ? construct_value thy stds
    4.94 -                      (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
    4.95 -                      o single
    4.96 -           | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
    4.97 -                               \coerce_term", [t']))
    4.98 -        | (Type (new_s, new_Ts as [new_T1, new_T2]),
    4.99 -           Type (old_s, old_Ts as [old_T1, old_T2])) =>
   4.100 -          if old_s = @{type_name fun_box} orelse
   4.101 -             old_s = @{type_name pair_box} orelse old_s = "*" then
   4.102 -            case constr_expand hol_ctxt old_T t of
   4.103 -              Const (@{const_name FunBox}, _) $ t1 =>
   4.104 -              if new_s = "fun" then
   4.105 -                coerce_term Ts new_T (Type ("fun", old_Ts)) t1
   4.106 -              else
   4.107 -                construct_value thy stds
   4.108 -                    (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
   4.109 -                    [coerce_term Ts (Type ("fun", new_Ts))
   4.110 -                                 (Type ("fun", old_Ts)) t1]
   4.111 -            | Const _ $ t1 $ t2 =>
   4.112 -              construct_value thy stds
   4.113 -                  (if new_s = "*" then @{const_name Pair}
   4.114 -                   else @{const_name PairBox}, new_Ts ---> new_T)
   4.115 -                  [coerce_term Ts new_T1 old_T1 t1,
   4.116 -                   coerce_term Ts new_T2 old_T2 t2]
   4.117 -            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
   4.118 -                                \coerce_term", [t'])
   4.119 -          else
   4.120 -            raise TYPE ("coerce_term", [new_T, old_T], [t])
   4.121 -        | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
   4.122      (* indexname * typ -> typ * term -> typ option list -> typ option list *)
   4.123      fun add_boxed_types_for_var (z as (_, T)) (T', t') =
   4.124        case t' of
   4.125 @@ -252,7 +252,7 @@
   4.126          val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
   4.127        in
   4.128          list_comb (Const (s0, T --> T --> body_type T0),
   4.129 -                   map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
   4.130 +                   map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
   4.131        end
   4.132      (* string -> typ -> term *)
   4.133      and do_description_operator s T =
   4.134 @@ -320,7 +320,7 @@
   4.135            val T' = hd (snd (dest_Type (hd Ts1)))
   4.136            val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
   4.137            val T2 = fastype_of1 (new_Ts, t2)
   4.138 -          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
   4.139 +          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
   4.140          in
   4.141            betapply (if s1 = "fun" then
   4.142                        t1
   4.143 @@ -336,7 +336,7 @@
   4.144            val (s1, Ts1) = dest_Type T1
   4.145            val t2 = do_term new_Ts old_Ts Neut t2
   4.146            val T2 = fastype_of1 (new_Ts, t2)
   4.147 -          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
   4.148 +          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
   4.149          in
   4.150            betapply (if s1 = "fun" then
   4.151                        t1
   4.152 @@ -1425,10 +1425,12 @@
   4.153        #> push_quantifiers_inward
   4.154        #> close_form
   4.155        #> Term.map_abs_vars shortest_name
   4.156 +    val def_ts = map (do_rest true) def_ts
   4.157 +    val nondef_ts = map (do_rest false) nondef_ts
   4.158 +    val core_t = do_rest false core_t
   4.159    in
   4.160 -    (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
   4.161 -      (got_all_mono_user_axioms, no_poly_user_axioms)),
   4.162 -     do_rest false core_t, binarize)
   4.163 +    (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
   4.164 +     core_t, binarize)
   4.165    end
   4.166  
   4.167  end;