# HG changeset patch
# User blanchet
# Date 1267088924 -3600
# Node ID 88dbcfe75c459a78cb81dd64829004fdca54639f
# Parent  63fb71d29eba7e791cbbde8fa1603b66d35e6649
cosmetics

diff -r 63fb71d29eba -r 88dbcfe75c45 src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Thu Feb 25 10:08:44 2010 +0100
@@ -342,7 +342,7 @@
       case triple_lookup (type_match thy) monos T of
         SOME (SOME b) => b
       | _ => is_type_always_monotonic T orelse
-             formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
+             formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
     fun is_deep_datatype T =
       is_datatype thy stds T andalso
       (not standard orelse T = nat_T orelse is_word_type T orelse
@@ -834,8 +834,8 @@
                         sound_problems then
                 print_m (fn () =>
                     "Warning: The conjecture either trivially holds for the \
-                    \given scopes or (more likely) lies outside Nitpick's \
-                    \supported fragment." ^
+                    \given scopes or lies outside Nitpick's supported \
+                    \fragment." ^
                     (if exists (not o KK.is_problem_trivially_false o fst)
                                unsound_problems then
                        " Only potential counterexamples may be found."
diff -r 63fb71d29eba -r 88dbcfe75c45 src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Thu Feb 25 10:08:44 2010 +0100
@@ -1096,8 +1096,8 @@
   in Int.min (max, aux [] T) end
 
 (* hol_context -> typ -> bool *)
-fun is_finite_type hol_ctxt =
-  not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
+fun is_finite_type hol_ctxt T =
+  bounded_exact_card_of_type hol_ctxt 1 2 [] T <> 0
 
 (* term -> bool *)
 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
diff -r 63fb71d29eba -r 88dbcfe75c45 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Thu Feb 25 10:08:44 2010 +0100
@@ -2,16 +2,15 @@
     Author:     Jasmin Blanchette, TU Muenchen
     Copyright   2009, 2010
 
-Monotonicity predicate for higher-order logic.
+Monotonicity inference for higher-order logic.
 *)
 
 signature NITPICK_MONO =
 sig
-  datatype sign = Plus | Minus
   type hol_context = Nitpick_HOL.hol_context
 
   val formulas_monotonic :
-    hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
+    hol_context -> bool -> typ -> term list * term list * term -> bool
 end;
 
 structure Nitpick_Mono : NITPICK_MONO =
@@ -270,8 +269,13 @@
   if could_exist_alpha_sub_ctype thy alpha_T T then
     case AList.lookup (op =) (!constr_cache) x of
       SOME C => C
-    | NONE => (fresh_ctype_for_type cdata (body_type T);
-               AList.lookup (op =) (!constr_cache) x |> the)
+    | NONE => if T = alpha_T then
+                let val C = fresh_ctype_for_type cdata T in
+                  (Unsynchronized.change constr_cache (cons (x, C)); C)
+                end
+              else
+                (fresh_ctype_for_type cdata (body_type T);
+                 AList.lookup (op =) (!constr_cache) x |> the)
   else
     fresh_ctype_for_type cdata T
 fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
@@ -435,12 +439,13 @@
 val add_ctype_is_right_unique = add_notin_ctype_fv Minus
 val add_ctype_is_right_total = add_notin_ctype_fv Plus
 
+val bool_from_minus = true
+
 (* sign -> bool *)
-fun bool_from_sign Plus = false
-  | bool_from_sign Minus = true
+fun bool_from_sign Plus = not bool_from_minus
+  | bool_from_sign Minus = bool_from_minus
 (* bool -> sign *)
-fun sign_from_bool false = Plus
-  | sign_from_bool true = Minus
+fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
 
 (* literal -> PropLogic.prop_formula *)
 fun prop_for_literal (x, sn) =
@@ -492,7 +497,7 @@
              "-: " ^ commas (map (string_for_var o fst) neg))
   end
 
-(* var -> constraint_set -> literal list list option *)
+(* var -> constraint_set -> literal list option *)
 fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
   | solve max_var (CSet (lits, comps, sexps)) =
     let
@@ -812,8 +817,8 @@
               val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
               val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
             in
-              (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
-                                                |>> pop_bound
+              (gamma |> push_bound abs_C, cset)
+              |> do_co_formula body_t |>> pop_bound
             end
           (* typ -> term -> accumulator *)
           fun do_bounded_quantifier abs_T body_t =
@@ -932,19 +937,20 @@
   map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
   |> cat_lines |> print_g
 
-(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
-   -> bool *)
-fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
-                       nondef_ts core_t =
+(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
+fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
+                       (def_ts, nondef_ts, core_t) =
   let
-    val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
+    val _ = print_g ("****** Monotonicity analysis: " ^
+                     string_for_ctype CAlpha ^ " is " ^
                      Syntax.string_of_typ ctxt alpha_T)
-    val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
-    val (gamma, cset) =
+    val cdata as {max_fresh, constr_cache, ...} =
+      initial_cdata hol_ctxt binarize alpha_T
+    val (gamma as {frees, consts, ...}, cset) =
       (initial_gamma, slack)
       |> fold (consider_definitional_axiom cdata) def_ts
       |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
-      |> consider_general_formula cdata sn core_t
+      |> consider_general_formula cdata Plus core_t
   in
     case solve (!max_fresh) cset of
       SOME lits => (print_ctype_context ctxt lits gamma; true)
diff -r 63fb71d29eba -r 88dbcfe75c45 src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 09:16:16 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Thu Feb 25 10:08:44 2010 +0100
@@ -136,6 +136,60 @@
                                      (index_seq 0 (length arg_Ts)) arg_Ts)
          end
 
+(* (term -> term) -> int -> term -> term *)
+fun coerce_bound_no f j t =
+  case t of
+    t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
+  | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
+  | Bound j' => if j' = j then f t else t
+  | _ => t
+(* hol_context -> typ -> typ -> term -> term *)
+fun coerce_bound_0_in_term hol_ctxt new_T old_T =
+  old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
+(* hol_context -> typ list -> typ -> typ -> term -> term *)
+and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
+  if old_T = new_T then
+    t
+  else
+    case (new_T, old_T) of
+      (Type (new_s, new_Ts as [new_T1, new_T2]),
+       Type ("fun", [old_T1, old_T2])) =>
+      (case eta_expand Ts t 1 of
+         Abs (s, _, t') =>
+         Abs (s, new_T1,
+              t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
+                 |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
+         |> Envir.eta_contract
+         |> new_s <> "fun"
+            ? construct_value thy stds
+                  (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
+                  o single
+       | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
+    | (Type (new_s, new_Ts as [new_T1, new_T2]),
+       Type (old_s, old_Ts as [old_T1, old_T2])) =>
+      if old_s = @{type_name fun_box} orelse
+         old_s = @{type_name fin_fun} orelse
+         old_s = @{type_name pair_box} orelse old_s = "*" then
+        case constr_expand hol_ctxt old_T t of
+          Const (old_s, _) $ t1 =>
+          if new_s = "fun" then
+            coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
+          else
+            construct_value thy stds
+                (old_s, Type ("fun", new_Ts) --> new_T)
+                [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
+                             (Type ("fun", old_Ts)) t1]
+        | Const _ $ t1 $ t2 =>
+          construct_value thy stds
+              (if new_s = "*" then @{const_name Pair}
+               else @{const_name PairBox}, new_Ts ---> new_T)
+              [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
+               coerce_term hol_ctxt Ts new_T2 old_T2 t2]
+        | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
+      else
+        raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
+    | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
+
 (* hol_context -> bool -> term -> term *)
 fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
                              orig_t =
@@ -146,60 +200,6 @@
       | box_relational_operator_type (Type ("*", Ts)) =
         Type ("*", map (box_type hol_ctxt InPair) Ts)
       | box_relational_operator_type T = T
-    (* (term -> term) -> int -> term -> term *)
-    fun coerce_bound_no f j t =
-      case t of
-        t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
-      | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
-      | Bound j' => if j' = j then f t else t
-      | _ => t
-    (* typ -> typ -> term -> term *)
-    fun coerce_bound_0_in_term new_T old_T =
-      old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
-    (* typ list -> typ -> term -> term *)
-    and coerce_term Ts new_T old_T t =
-      if old_T = new_T then
-        t
-      else
-        case (new_T, old_T) of
-          (Type (new_s, new_Ts as [new_T1, new_T2]),
-           Type ("fun", [old_T1, old_T2])) =>
-          (case eta_expand Ts t 1 of
-             Abs (s, _, t') =>
-             Abs (s, new_T1,
-                  t' |> coerce_bound_0_in_term new_T1 old_T1
-                     |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
-             |> Envir.eta_contract
-             |> new_s <> "fun"
-                ? construct_value thy stds
-                      (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
-                      o single
-           | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
-                               \coerce_term", [t']))
-        | (Type (new_s, new_Ts as [new_T1, new_T2]),
-           Type (old_s, old_Ts as [old_T1, old_T2])) =>
-          if old_s = @{type_name fun_box} orelse
-             old_s = @{type_name pair_box} orelse old_s = "*" then
-            case constr_expand hol_ctxt old_T t of
-              Const (@{const_name FunBox}, _) $ t1 =>
-              if new_s = "fun" then
-                coerce_term Ts new_T (Type ("fun", old_Ts)) t1
-              else
-                construct_value thy stds
-                    (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
-                    [coerce_term Ts (Type ("fun", new_Ts))
-                                 (Type ("fun", old_Ts)) t1]
-            | Const _ $ t1 $ t2 =>
-              construct_value thy stds
-                  (if new_s = "*" then @{const_name Pair}
-                   else @{const_name PairBox}, new_Ts ---> new_T)
-                  [coerce_term Ts new_T1 old_T1 t1,
-                   coerce_term Ts new_T2 old_T2 t2]
-            | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
-                                \coerce_term", [t'])
-          else
-            raise TYPE ("coerce_term", [new_T, old_T], [t])
-        | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
     (* indexname * typ -> typ * term -> typ option list -> typ option list *)
     fun add_boxed_types_for_var (z as (_, T)) (T', t') =
       case t' of
@@ -252,7 +252,7 @@
         val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
       in
         list_comb (Const (s0, T --> T --> body_type T0),
-                   map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
+                   map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
       end
     (* string -> typ -> term *)
     and do_description_operator s T =
@@ -320,7 +320,7 @@
           val T' = hd (snd (dest_Type (hd Ts1)))
           val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
           val T2 = fastype_of1 (new_Ts, t2)
-          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
         in
           betapply (if s1 = "fun" then
                       t1
@@ -336,7 +336,7 @@
           val (s1, Ts1) = dest_Type T1
           val t2 = do_term new_Ts old_Ts Neut t2
           val T2 = fastype_of1 (new_Ts, t2)
-          val t2 = coerce_term new_Ts (hd Ts1) T2 t2
+          val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
         in
           betapply (if s1 = "fun" then
                       t1
@@ -1425,10 +1425,12 @@
       #> push_quantifiers_inward
       #> close_form
       #> Term.map_abs_vars shortest_name
+    val def_ts = map (do_rest true) def_ts
+    val nondef_ts = map (do_rest false) nondef_ts
+    val core_t = do_rest false core_t
   in
-    (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
-      (got_all_mono_user_axioms, no_poly_user_axioms)),
-     do_rest false core_t, binarize)
+    (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
+     core_t, binarize)
   end
 
 end;