fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
authorblanchet
Tue Nov 17 19:47:27 2009 +0100 (2009-11-17 ago)
changeset 33744e82531ebf5f3
parent 33743 a58893035742
child 33745 daf236998f82
fixed bug in Nitpick's handling of "The" and "Eps" when the return type is a "bool"
src/HOL/Tools/Nitpick/HISTORY
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
     1.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 19:12:10 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 19:47:27 2009 +0100
     1.3 @@ -12,6 +12,8 @@
     1.4    * Added support for codatatype view of datatypes
     1.5    * Fixed soundness bugs related to sets and sets of sets
     1.6    * Fixed monotonicity check
     1.7 +  * Fixed error when processing definitions that resulted in an exception
     1.8 +  * Fixed error in Kodkod encoding of "The" and "Eps"
     1.9    * Fixed error in display of uncurried constants
    1.10    * Speeded up scope enumeration
    1.11  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 17 19:12:10 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Nov 17 19:47:27 2009 +0100
     2.3 @@ -434,11 +434,11 @@
     2.4                           def_us
     2.5          val nondef_us = map (choose_reps_in_nut scope liberal rep_table false)
     2.6                              nondef_us
     2.7 -(*
     2.8 +(*###
     2.9 +*)
    2.10          val _ = List.app (priority o string_for_nut ctxt)
    2.11                           (free_names @ sel_names @ nonsel_names @
    2.12                            core_u :: def_us @ nondef_us)
    2.13 -*)
    2.14          val (free_rels, pool, rel_table) =
    2.15            rename_free_vars free_names initial_pool NameTable.empty
    2.16          val (sel_rels, pool, rel_table) =
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 19:12:10 2009 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 19:47:27 2009 +0100
     3.3 @@ -1092,6 +1092,12 @@
     3.4                    else
     3.5                      kk_rel_eq r1 r2
     3.6                  end)
     3.7 +         | Op2 (The, T, _, u1, u2) =>
     3.8 +           to_f_with_polarity polar
     3.9 +                              (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
    3.10 +         | Op2 (Eps, T, _, u1, u2) =>
    3.11 +           to_f_with_polarity polar
    3.12 +                              (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
    3.13           | Op2 (Apply, T, _, u1, u2) =>
    3.14             (case (polar, rep_of u1) of
    3.15                (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 19:12:10 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 19:47:27 2009 +0100
     4.3 @@ -1158,8 +1158,10 @@
     4.4              let
     4.5                val u1' = sub u1
     4.6                val opt1 = is_opt_rep (rep_of u1')
     4.7 +              val opt = (oper = Eps orelse opt1)
     4.8                val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
     4.9 -              val R = unopt_R |> (oper = Eps orelse opt1) ? opt_rep ofs T
    4.10 +              val R = if is_boolean_type T then bool_rep polar opt
    4.11 +                      else unopt_R |> opt ? opt_rep ofs T
    4.12                val u = Op2 (oper, T, R, u1', sub u2)
    4.13              in
    4.14                if is_precise_type datatypes T orelse not opt1 then