# HG changeset patch
# User blanchet
# Date 1298285431 -3600
# Node ID c7a2669ae75dc14f4a2574c0a7a1d4be98746d7a
# Parent  ff3cb0c418b7d45552a7c734e140edf2db8a4f3c
tweaked Nitpick based on C++ memory model example

diff -r ff3cb0c418b7 -r c7a2669ae75d doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 10:44:19 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:31 2011 +0100
@@ -2108,26 +2108,18 @@
 per-type basis using the \textit{box}~\qty{type} option described above.
 
 \opargboolorsmart{finitize}{type}{dont\_finitize}
-Specifies whether Nitpick should attempt to finitize an infinite ``shallow
-datatype'' (an infinite datatype whose constructors don't appear in the
-problem). The option can then take the following values:
-
-\begin{enum}
-\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
-\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
-type wherever possible.
-\end{enum}
-
-The semantics of the option is somewhat different for infinite shallow
-datatypes:
+Specifies whether Nitpick should attempt to finitize an infinite datatype. The
+option can then take the following values:
 
 \begin{enum}
 \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
 unsound, counterexamples generated under these conditions are tagged as ``quasi
 genuine.''
 \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
-\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
-detect whether the datatype can be soundly finitized before finitizing it.
+\item[$\bullet$] \textbf{\textit{smart}:}
+If the datatype's constructors don't appear in the problem, perform a
+monotonicity analysis to detect whether the datatype can be soundly finitized;
+otherwise, don't finitize it.
 \end{enum}
 
 \nopagebreak
diff -r ff3cb0c418b7 -r c7a2669ae75d src/HOL/Tools/Nitpick/kodkod.ML
--- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 21 11:50:31 2011 +0100
@@ -169,7 +169,7 @@
   val is_problem_trivially_false : problem -> bool
   val problems_equivalent : problem * problem -> bool
   val solve_any_problem :
-    bool -> Time.time option -> int -> int -> problem list -> outcome
+    bool -> bool -> Time.time option -> int -> int -> problem list -> outcome
 end;
 
 structure Kodkod : KODKOD =
@@ -1090,13 +1090,14 @@
   Synchronized.var "Kodkod.cached_outcome"
                    (NONE : ((int * problem list) * outcome) option)
 
-fun solve_any_problem overlord deadline max_threads max_solutions problems =
+fun solve_any_problem debug overlord deadline max_threads max_solutions
+                      problems =
   let
     fun do_solve () =
       uncached_solve_any_problem overlord deadline max_threads max_solutions
                                  problems
   in
-    if overlord then
+    if debug orelse overlord then
       do_solve ()
     else
       case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
diff -r ff3cb0c418b7 -r c7a2669ae75d src/HOL/Tools/Nitpick/nitpick.ML
--- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 11:50:31 2011 +0100
@@ -363,6 +363,8 @@
         SOME (SOME b) => b
       | _ => is_type_fundamentally_monotonic T orelse
              is_type_actually_monotonic T
+    fun is_deep_datatype_finitizable T =
+      triple_lookup (type_match thy) finitizes T = SOME (SOME true)
     fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
         is_type_kind_of_monotonic T
       | is_shallow_datatype_finitizable T =
@@ -407,8 +409,10 @@
       all_Ts |> filter (is_datatype ctxt stds)
              |> List.partition is_datatype_deep
     val finitizable_dataTs =
-      shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
-                     |> filter is_shallow_datatype_finitizable
+      (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
+                   |> filter is_deep_datatype_finitizable) @
+      (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
+                      |> filter is_shallow_datatype_finitizable)
     val _ =
       if verbose andalso not (null finitizable_dataTs) then
         pprint_v (K (monotonicity_message finitizable_dataTs
@@ -735,8 +739,8 @@
         if max_solutions <= 0 then
           (found_really_genuine, 0, 0, donno)
         else
-          case KK.solve_any_problem overlord deadline max_threads max_solutions
-                                    (map fst problems) of
+          case KK.solve_any_problem debug overlord deadline max_threads
+                                    max_solutions (map fst problems) of
             KK.JavaNotInstalled =>
             (print_m install_java_message;
              (found_really_genuine, max_potential, max_genuine, donno + 1))
diff -r ff3cb0c418b7 -r c7a2669ae75d src/HOL/Tools/Nitpick/nitpick_hol.ML
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:31 2011 +0100
@@ -66,7 +66,9 @@
   val original_name : string -> string
   val abs_var : indexname * typ -> term -> term
   val is_higher_order_type : typ -> bool
-  val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
+  val is_special_eligible_arg : bool -> typ list -> term -> bool
+  val s_let :
+    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
   val s_betapply : typ list -> term * term -> term
   val s_betapplys : typ list -> term * term list -> term
   val s_conj : term * term -> term
@@ -327,14 +329,23 @@
   | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
   | is_higher_order_type _ = false
 
+fun is_special_eligible_arg strict Ts t =
+  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
+    null bad_Ts orelse
+    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+     not strict orelse forall (not o is_higher_order_type) bad_Ts)
+  end
+
 fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
 
 fun let_var s = (nitpick_prefix ^ s, 999)
 val let_inline_threshold = 20
 
-fun s_let s n abs_T body_T f t =
+fun s_let Ts s n abs_T body_T f t =
   if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
-     is_higher_order_type abs_T then
+     is_special_eligible_arg true Ts t then
+     (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
+        "false" instead to account for potential future specializations. *)
     f t
   else
     let val z = (let_var s, abs_T) in
@@ -358,7 +369,7 @@
       $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
     end
   | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
-    (s_let s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
+    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
               (curry betapply t1) t2
      handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
   | s_betapply _ (t1, t2) = t1 $ t2
@@ -1617,7 +1628,7 @@
 
 (* Inline definitions or define as an equational constant? Booleans tend to
    benefit more from inlining, due to the polarity analysis. *)
-val def_inline_threshold_for_booleans = 50
+val def_inline_threshold_for_booleans = 60
 val def_inline_threshold_for_non_booleans = 20
 
 fun unfold_defs_in_term
diff -r ff3cb0c418b7 -r c7a2669ae75d src/HOL/Tools/Nitpick/nitpick_preproc.ML
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 11:50:31 2011 +0100
@@ -392,18 +392,18 @@
     val num_occs_of_var =
       fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
                     | _ => I) t (K 0)
-    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
-        aux_eq careful true t0 t1 t2
-      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
-        t0 $ aux false t1 $ aux careful t2
-      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
-        aux_eq careful true t0 t1 t2
-      | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
-        t0 $ aux false t1 $ aux careful t2
-      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
-      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
-      | aux _ t = t
-    and aux_eq careful pass1 t0 t1 t2 =
+    fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
+        aux_eq Ts careful true t0 t1 t2
+      | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
+        t0 $ aux Ts false t1 $ aux Ts careful t2
+      | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
+        aux_eq Ts careful true t0 t1 t2
+      | aux Ts careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
+        t0 $ aux Ts false t1 $ aux Ts careful t2
+      | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
+      | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
+      | aux _ _ t = t
+    and aux_eq Ts careful pass1 t0 t1 t2 =
       ((if careful then
           raise SAME ()
         else if axiom andalso is_Var t2 andalso
@@ -426,22 +426,23 @@
                 x = (@{const_name Suc}, nat_T --> nat_T)) andalso
                (not careful orelse not (is_Var t1) orelse
                 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
-                s_let "l" (n + 1) dataT bool_T
-                      (fn t1 => discriminate_value hol_ctxt x t1 ::
-                                map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
-                                |> foldr1 s_conj) t1
+                s_let Ts "l" (n + 1) dataT bool_T
+                      (fn t1 =>
+                          discriminate_value hol_ctxt x t1 ::
+                          map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
+                          |> foldr1 s_conj) t1
             else
               raise SAME ()
           end
         | _ => raise SAME ())
        |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
-      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
-                        else t0 $ aux false t2 $ aux false t1
-    and sel_eq x t n nth_T nth_t =
+      handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
+                        else t0 $ aux Ts false t2 $ aux Ts false t1
+    and sel_eq Ts x t n nth_T nth_t =
       HOLogic.eq_const nth_T $ nth_t
                              $ select_nth_constr_arg ctxt stds x t n nth_T
-      |> aux false
-  in aux axiom t end
+      |> aux Ts false
+  in aux [] axiom t end
 
 (** Destruction of universal and existential equalities **)
 
@@ -709,13 +710,6 @@
     else if j1 > j2 then overlapping_indices ps1 ps2'
     else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
 
-fun is_eligible_arg Ts t =
-  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
-    null bad_Ts orelse
-    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
-     forall (not o is_higher_order_type) bad_Ts)
-  end
-
 fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
 
 (* If a constant's definition is picked up deeper than this threshold, we
@@ -747,8 +741,9 @@
                  not (is_constr ctxt stds x) andalso
                  not (is_choice_spec_fun hol_ctxt x))) then
               let
-                val eligible_args = filter (is_eligible_arg Ts o snd)
-                                           (index_seq 0 (length args) ~~ args)
+                val eligible_args =
+                  filter (is_special_eligible_arg true Ts o snd)
+                         (index_seq 0 (length args) ~~ args)
                 val _ = not (null eligible_args) orelse raise SAME ()
                 val old_axs = equational_fun_axioms hol_ctxt x
                               |> map (destroy_existential_equalities hol_ctxt)
diff -r ff3cb0c418b7 -r c7a2669ae75d src/HOL/Tools/Nitpick/nitpick_tests.ML
--- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 21 10:44:19 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 21 11:50:31 2011 +0100
@@ -211,11 +211,11 @@
 
 fun run_all_tests () =
   let
-    val {overlord, ...} = Nitpick_Isar.default_params @{theory} []
+    val {debug, overlord, ...} = Nitpick_Isar.default_params @{theory} []
     val max_threads = 1
     val max_solutions = 1
   in
-    case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
+    case Kodkod.solve_any_problem debug overlord NONE max_threads max_solutions
                                   (map (problem_for_nut @{context}) tests) of
       Kodkod.Normal ([], _, _) => ()
     | _ => error "Tests failed."