tweaked Nitpick based on C++ memory model example
authorblanchet
Mon Feb 21 11:50:31 2011 +0100 (2011-02-21)
changeset 41793c7a2669ae75d
parent 41792 ff3cb0c418b7
child 41794 03bf23a265b6
tweaked Nitpick based on C++ memory model example
doc-src/Nitpick/nitpick.tex
src/HOL/Tools/Nitpick/kodkod.ML
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_tests.ML
     1.1 --- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 10:44:19 2011 +0100
     1.2 +++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:31 2011 +0100
     1.3 @@ -2108,26 +2108,18 @@
     1.4  per-type basis using the \textit{box}~\qty{type} option described above.
     1.5  
     1.6  \opargboolorsmart{finitize}{type}{dont\_finitize}
     1.7 -Specifies whether Nitpick should attempt to finitize an infinite ``shallow
     1.8 -datatype'' (an infinite datatype whose constructors don't appear in the
     1.9 -problem). The option can then take the following values:
    1.10 -
    1.11 -\begin{enum}
    1.12 -\item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the type.
    1.13 -\item[$\bullet$] \textbf{\textit{true}} or \textbf{\textit{smart}:} Finitize the
    1.14 -type wherever possible.
    1.15 -\end{enum}
    1.16 -
    1.17 -The semantics of the option is somewhat different for infinite shallow
    1.18 -datatypes:
    1.19 +Specifies whether Nitpick should attempt to finitize an infinite datatype. The
    1.20 +option can then take the following values:
    1.21  
    1.22  \begin{enum}
    1.23  \item[$\bullet$] \textbf{\textit{true}:} Finitize the datatype. Since this is
    1.24  unsound, counterexamples generated under these conditions are tagged as ``quasi
    1.25  genuine.''
    1.26  \item[$\bullet$] \textbf{\textit{false}:} Don't attempt to finitize the datatype.
    1.27 -\item[$\bullet$] \textbf{\textit{smart}:} Perform a monotonicity analysis to
    1.28 -detect whether the datatype can be soundly finitized before finitizing it.
    1.29 +\item[$\bullet$] \textbf{\textit{smart}:}
    1.30 +If the datatype's constructors don't appear in the problem, perform a
    1.31 +monotonicity analysis to detect whether the datatype can be soundly finitized;
    1.32 +otherwise, don't finitize it.
    1.33  \end{enum}
    1.34  
    1.35  \nopagebreak
     2.1 --- a/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 21 10:44:19 2011 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/kodkod.ML	Mon Feb 21 11:50:31 2011 +0100
     2.3 @@ -169,7 +169,7 @@
     2.4    val is_problem_trivially_false : problem -> bool
     2.5    val problems_equivalent : problem * problem -> bool
     2.6    val solve_any_problem :
     2.7 -    bool -> Time.time option -> int -> int -> problem list -> outcome
     2.8 +    bool -> bool -> Time.time option -> int -> int -> problem list -> outcome
     2.9  end;
    2.10  
    2.11  structure Kodkod : KODKOD =
    2.12 @@ -1090,13 +1090,14 @@
    2.13    Synchronized.var "Kodkod.cached_outcome"
    2.14                     (NONE : ((int * problem list) * outcome) option)
    2.15  
    2.16 -fun solve_any_problem overlord deadline max_threads max_solutions problems =
    2.17 +fun solve_any_problem debug overlord deadline max_threads max_solutions
    2.18 +                      problems =
    2.19    let
    2.20      fun do_solve () =
    2.21        uncached_solve_any_problem overlord deadline max_threads max_solutions
    2.22                                   problems
    2.23    in
    2.24 -    if overlord then
    2.25 +    if debug orelse overlord then
    2.26        do_solve ()
    2.27      else
    2.28        case AList.lookup (fn ((max1, ps1), (max2, ps2)) =>
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 10:44:19 2011 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Mon Feb 21 11:50:31 2011 +0100
     3.3 @@ -363,6 +363,8 @@
     3.4          SOME (SOME b) => b
     3.5        | _ => is_type_fundamentally_monotonic T orelse
     3.6               is_type_actually_monotonic T
     3.7 +    fun is_deep_datatype_finitizable T =
     3.8 +      triple_lookup (type_match thy) finitizes T = SOME (SOME true)
     3.9      fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    3.10          is_type_kind_of_monotonic T
    3.11        | is_shallow_datatype_finitizable T =
    3.12 @@ -407,8 +409,10 @@
    3.13        all_Ts |> filter (is_datatype ctxt stds)
    3.14               |> List.partition is_datatype_deep
    3.15      val finitizable_dataTs =
    3.16 -      shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    3.17 -                     |> filter is_shallow_datatype_finitizable
    3.18 +      (deep_dataTs |> filter_out (is_finite_type hol_ctxt)
    3.19 +                   |> filter is_deep_datatype_finitizable) @
    3.20 +      (shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
    3.21 +                      |> filter is_shallow_datatype_finitizable)
    3.22      val _ =
    3.23        if verbose andalso not (null finitizable_dataTs) then
    3.24          pprint_v (K (monotonicity_message finitizable_dataTs
    3.25 @@ -735,8 +739,8 @@
    3.26          if max_solutions <= 0 then
    3.27            (found_really_genuine, 0, 0, donno)
    3.28          else
    3.29 -          case KK.solve_any_problem overlord deadline max_threads max_solutions
    3.30 -                                    (map fst problems) of
    3.31 +          case KK.solve_any_problem debug overlord deadline max_threads
    3.32 +                                    max_solutions (map fst problems) of
    3.33              KK.JavaNotInstalled =>
    3.34              (print_m install_java_message;
    3.35               (found_really_genuine, max_potential, max_genuine, donno + 1))
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 10:44:19 2011 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Feb 21 11:50:31 2011 +0100
     4.3 @@ -66,7 +66,9 @@
     4.4    val original_name : string -> string
     4.5    val abs_var : indexname * typ -> term -> term
     4.6    val is_higher_order_type : typ -> bool
     4.7 -  val s_let : string -> int -> typ -> typ -> (term -> term) -> term -> term
     4.8 +  val is_special_eligible_arg : bool -> typ list -> term -> bool
     4.9 +  val s_let :
    4.10 +    typ list -> string -> int -> typ -> typ -> (term -> term) -> term -> term
    4.11    val s_betapply : typ list -> term * term -> term
    4.12    val s_betapplys : typ list -> term * term list -> term
    4.13    val s_conj : term * term -> term
    4.14 @@ -327,14 +329,23 @@
    4.15    | is_higher_order_type (Type (_, Ts)) = exists is_higher_order_type Ts
    4.16    | is_higher_order_type _ = false
    4.17  
    4.18 +fun is_special_eligible_arg strict Ts t =
    4.19 +  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
    4.20 +    null bad_Ts orelse
    4.21 +    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
    4.22 +     not strict orelse forall (not o is_higher_order_type) bad_Ts)
    4.23 +  end
    4.24 +
    4.25  fun abs_var ((s, j), T) body = Abs (s, T, abstract_over (Var ((s, j), T), body))
    4.26  
    4.27  fun let_var s = (nitpick_prefix ^ s, 999)
    4.28  val let_inline_threshold = 20
    4.29  
    4.30 -fun s_let s n abs_T body_T f t =
    4.31 +fun s_let Ts s n abs_T body_T f t =
    4.32    if (n - 1) * (size_of_term t - 1) <= let_inline_threshold orelse
    4.33 -     is_higher_order_type abs_T then
    4.34 +     is_special_eligible_arg true Ts t then
    4.35 +     (* TODO: the "true" argument to "is_special_eligible_arg" should perhaps be
    4.36 +        "false" instead to account for potential future specializations. *)
    4.37      f t
    4.38    else
    4.39      let val z = (let_var s, abs_T) in
    4.40 @@ -358,7 +369,7 @@
    4.41        $ t12 $ Abs (s, T, s_betapply (T :: Ts) (t13', incr_boundvars 1 t2))
    4.42      end
    4.43    | s_betapply Ts (t1 as Abs (s1, T1, t1'), t2) =
    4.44 -    (s_let s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
    4.45 +    (s_let Ts s1 (loose_bvar1_count (t1', 0)) T1 (fastype_of1 (T1 :: Ts, t1'))
    4.46                (curry betapply t1) t2
    4.47       handle TERM _ => betapply (t1, t2)) (* FIXME: fix all uses *)
    4.48    | s_betapply _ (t1, t2) = t1 $ t2
    4.49 @@ -1617,7 +1628,7 @@
    4.50  
    4.51  (* Inline definitions or define as an equational constant? Booleans tend to
    4.52     benefit more from inlining, due to the polarity analysis. *)
    4.53 -val def_inline_threshold_for_booleans = 50
    4.54 +val def_inline_threshold_for_booleans = 60
    4.55  val def_inline_threshold_for_non_booleans = 20
    4.56  
    4.57  fun unfold_defs_in_term
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 10:44:19 2011 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Feb 21 11:50:31 2011 +0100
     5.3 @@ -392,18 +392,18 @@
     5.4      val num_occs_of_var =
     5.5        fold_aterms (fn Var z => (fn f => fn z' => f z' |> z = z' ? Integer.add 1)
     5.6                      | _ => I) t (K 0)
     5.7 -    fun aux careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
     5.8 -        aux_eq careful true t0 t1 t2
     5.9 -      | aux careful ((t0 as @{const "==>"}) $ t1 $ t2) =
    5.10 -        t0 $ aux false t1 $ aux careful t2
    5.11 -      | aux careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
    5.12 -        aux_eq careful true t0 t1 t2
    5.13 -      | aux careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
    5.14 -        t0 $ aux false t1 $ aux careful t2
    5.15 -      | aux careful (Abs (s, T, t')) = Abs (s, T, aux careful t')
    5.16 -      | aux careful (t1 $ t2) = aux careful t1 $ aux careful t2
    5.17 -      | aux _ t = t
    5.18 -    and aux_eq careful pass1 t0 t1 t2 =
    5.19 +    fun aux Ts careful ((t0 as Const (@{const_name "=="}, _)) $ t1 $ t2) =
    5.20 +        aux_eq Ts careful true t0 t1 t2
    5.21 +      | aux Ts careful ((t0 as @{const "==>"}) $ t1 $ t2) =
    5.22 +        t0 $ aux Ts false t1 $ aux Ts careful t2
    5.23 +      | aux Ts careful ((t0 as Const (@{const_name HOL.eq}, _)) $ t1 $ t2) =
    5.24 +        aux_eq Ts careful true t0 t1 t2
    5.25 +      | aux Ts careful ((t0 as @{const HOL.implies}) $ t1 $ t2) =
    5.26 +        t0 $ aux Ts false t1 $ aux Ts careful t2
    5.27 +      | aux Ts careful (Abs (s, T, t')) = Abs (s, T, aux (T :: Ts) careful t')
    5.28 +      | aux Ts careful (t1 $ t2) = aux Ts careful t1 $ aux Ts careful t2
    5.29 +      | aux _ _ t = t
    5.30 +    and aux_eq Ts careful pass1 t0 t1 t2 =
    5.31        ((if careful then
    5.32            raise SAME ()
    5.33          else if axiom andalso is_Var t2 andalso
    5.34 @@ -426,22 +426,23 @@
    5.35                  x = (@{const_name Suc}, nat_T --> nat_T)) andalso
    5.36                 (not careful orelse not (is_Var t1) orelse
    5.37                  String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
    5.38 -                s_let "l" (n + 1) dataT bool_T
    5.39 -                      (fn t1 => discriminate_value hol_ctxt x t1 ::
    5.40 -                                map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
    5.41 -                                |> foldr1 s_conj) t1
    5.42 +                s_let Ts "l" (n + 1) dataT bool_T
    5.43 +                      (fn t1 =>
    5.44 +                          discriminate_value hol_ctxt x t1 ::
    5.45 +                          map3 (sel_eq Ts x t1) (index_seq 0 n) arg_Ts args
    5.46 +                          |> foldr1 s_conj) t1
    5.47              else
    5.48                raise SAME ()
    5.49            end
    5.50          | _ => raise SAME ())
    5.51         |> body_type (type_of t0) = prop_T ? HOLogic.mk_Trueprop)
    5.52 -      handle SAME () => if pass1 then aux_eq careful false t0 t2 t1
    5.53 -                        else t0 $ aux false t2 $ aux false t1
    5.54 -    and sel_eq x t n nth_T nth_t =
    5.55 +      handle SAME () => if pass1 then aux_eq Ts careful false t0 t2 t1
    5.56 +                        else t0 $ aux Ts false t2 $ aux Ts false t1
    5.57 +    and sel_eq Ts x t n nth_T nth_t =
    5.58        HOLogic.eq_const nth_T $ nth_t
    5.59                               $ select_nth_constr_arg ctxt stds x t n nth_T
    5.60 -      |> aux false
    5.61 -  in aux axiom t end
    5.62 +      |> aux Ts false
    5.63 +  in aux [] axiom t end
    5.64  
    5.65  (** Destruction of universal and existential equalities **)
    5.66  
    5.67 @@ -709,13 +710,6 @@
    5.68      else if j1 > j2 then overlapping_indices ps1 ps2'
    5.69      else overlapping_indices ps1' ps2' |> the_default t2 t1 = t2 ? cons j1
    5.70  
    5.71 -fun is_eligible_arg Ts t =
    5.72 -  let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
    5.73 -    null bad_Ts orelse
    5.74 -    (is_higher_order_type (fastype_of1 (Ts, t)) andalso
    5.75 -     forall (not o is_higher_order_type) bad_Ts)
    5.76 -  end
    5.77 -
    5.78  fun special_prefix_for j = special_prefix ^ string_of_int j ^ name_sep
    5.79  
    5.80  (* If a constant's definition is picked up deeper than this threshold, we
    5.81 @@ -747,8 +741,9 @@
    5.82                   not (is_constr ctxt stds x) andalso
    5.83                   not (is_choice_spec_fun hol_ctxt x))) then
    5.84                let
    5.85 -                val eligible_args = filter (is_eligible_arg Ts o snd)
    5.86 -                                           (index_seq 0 (length args) ~~ args)
    5.87 +                val eligible_args =
    5.88 +                  filter (is_special_eligible_arg true Ts o snd)
    5.89 +                         (index_seq 0 (length args) ~~ args)
    5.90                  val _ = not (null eligible_args) orelse raise SAME ()
    5.91                  val old_axs = equational_fun_axioms hol_ctxt x
    5.92                                |> map (destroy_existential_equalities hol_ctxt)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 21 10:44:19 2011 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Mon Feb 21 11:50:31 2011 +0100
     6.3 @@ -211,11 +211,11 @@
     6.4  
     6.5  fun run_all_tests () =
     6.6    let
     6.7 -    val {overlord, ...} = Nitpick_Isar.default_params @{theory} []
     6.8 +    val {debug, overlord, ...} = Nitpick_Isar.default_params @{theory} []
     6.9      val max_threads = 1
    6.10      val max_solutions = 1
    6.11    in
    6.12 -    case Kodkod.solve_any_problem overlord NONE max_threads max_solutions
    6.13 +    case Kodkod.solve_any_problem debug overlord NONE max_threads max_solutions
    6.14                                    (map (problem_for_nut @{context}) tests) of
    6.15        Kodkod.Normal ([], _, _) => ()
    6.16      | _ => error "Tests failed."