fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type
authorblanchet
Mon Nov 23 13:24:32 2009 +0100 (2009-11-23)
changeset 33853348c3ea03e58
parent 33852 3a586209151e
child 33854 26a4cb3a7eae
fixed soundness bug in Nitpick that occurred because unrolled predicate iterators were considered to be a "precise" type
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 13:23:39 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Mon Nov 23 13:24:32 2009 +0100
     1.3 @@ -10,9 +10,11 @@
     1.4    * Optimized Kodkod encoding of datatypes whose constructors don't appear in
     1.5      the formula to falsify
     1.6    * Added support for codatatype view of datatypes
     1.7 -  * Fixed soundness bugs related to sets and sets of sets
     1.8 +  * Fixed soundness bugs related to sets, sets of sets, and (co)inductive
     1.9 +    predicates
    1.10    * Fixed monotonicity check
    1.11 -  * Fixed error when processing definitions that resulted in an exception
    1.12 +  * Fixed error when processing definitions
    1.13 +  * Fixed error in "star_linear_preds" optimization
    1.14    * Fixed error in Kodkod encoding of "The" and "Eps"
    1.15    * Fixed error in display of uncurried constants
    1.16    * Speeded up scope enumeration
    1.17 @@ -70,7 +72,7 @@
    1.18    * Improved precision of "trancl" and "rtrancl"
    1.19    * Optimized Kodkod encoding of "tranclp" and "rtranclp"
    1.20    * Made detection of inconsistent scope specifications more robust
    1.21 -  * Fixed a few Kodkod generation bugs that resulted in exceptions
    1.22 +  * Fixed a few Kodkod generation bugs
    1.23  
    1.24  Version 1.1.1 (24 Jun 2009)
    1.25  
    1.26 @@ -79,8 +81,7 @@
    1.27    * Improved precision of some set constructs
    1.28    * Fiddled with the automatic monotonicity check
    1.29    * Fixed performance issues related to scope enumeration
    1.30 -  * Fixed a few Kodkod generation bugs that resulted in exceptions or stack
    1.31 -    overflows
    1.32 +  * Fixed a few Kodkod generation bugs
    1.33  
    1.34  Version 1.1.0 (16 Jun 2009)
    1.35  
    1.36 @@ -117,7 +118,7 @@
    1.37    * Fixed soundness issue in handling of non-definitional axioms
    1.38    * Fixed soundness issue in handling of "Abs_" and "Rep_" functions for "unit",
    1.39      "nat", "int", and "*"
    1.40 -  * Fixed a few Kodkod generation bugs that resulted in exceptions
    1.41 +  * Fixed a few Kodkod generation bugs
    1.42    * Optimized "div", "mod", and "dvd" on "nat" and "int"
    1.43  
    1.44  Version 1.0.2 (12 Mar 2009)
    1.45 @@ -152,7 +153,7 @@
    1.46      infinite loop for "Nominal.perm"
    1.47    * Added support for multiple instantiations of non-well-founded inductive
    1.48      predicates, which previously raised an exception
    1.49 -  * Fixed a Kodkod generation bug that resulted in an exception
    1.50 +  * Fixed a Kodkod generation bug
    1.51    * Altered order of scope enumeration and automatic SAT solver selection
    1.52    * Optimized "Eps", "nat_case", and "list_case"
    1.53    * Improved output formatting
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 13:23:39 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Nov 23 13:24:32 2009 +0100
     2.3 @@ -712,15 +712,16 @@
     2.4               else if is_rep_fun thy x then
     2.5                 Func oo best_non_opt_symmetric_reps_for_fun_type
     2.6               else if all_precise orelse is_skolem_name v
     2.7 -                     orelse s mem [@{const_name undefined_fast_The},
     2.8 -                                   @{const_name undefined_fast_Eps},
     2.9 -                                   @{const_name bisim}] then
    2.10 +                     orelse original_name s
    2.11 +                            mem [@{const_name undefined_fast_The},
    2.12 +                                 @{const_name undefined_fast_Eps},
    2.13 +                                 @{const_name bisim},
    2.14 +                                 @{const_name bisim_iterator_max}] then
    2.15                 best_non_opt_set_rep_for_type
    2.16               else if original_name s
    2.17                       mem [@{const_name set}, @{const_name distinct},
    2.18                            @{const_name ord_class.less},
    2.19 -                          @{const_name ord_class.less_eq},
    2.20 -                          @{const_name bisim_iterator_max}] then
    2.21 +                          @{const_name ord_class.less_eq}] then
    2.22                 best_set_rep_for_type
    2.23               else
    2.24                 best_opt_set_rep_for_type) scope T
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 23 13:23:39 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Mon Nov 23 13:24:32 2009 +0100
     3.3 @@ -100,8 +100,7 @@
     3.4      forall (is_precise_type dtypes) Ts
     3.5    | is_precise_type dtypes (Type ("*", Ts)) = forall (is_precise_type dtypes) Ts
     3.6    | is_precise_type dtypes T =
     3.7 -    T <> nat_T andalso T <> int_T
     3.8 -    andalso #precise (the (datatype_spec dtypes T))
     3.9 +    not (is_integer_type T) andalso #precise (the (datatype_spec dtypes T))
    3.10      handle Option.Option => true
    3.11  fun is_fully_comparable_type dtypes (Type ("fun", [T1, T2])) =
    3.12      is_precise_type dtypes T1 andalso is_fully_comparable_type dtypes T2