merged
authorblanchet
Tue Nov 17 22:51:00 2009 +0100 (2009-11-17 ago)
changeset 337466c6ce0757bfe
parent 33741 4c414d0835ab
parent 33745 daf236998f82
child 33747 3aa6b9911252
merged
     1.1 --- a/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 18:52:30 2009 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/ROOT.ML	Tue Nov 17 22:51:00 2009 +0100
     1.3 @@ -5,7 +5,6 @@
     1.4  Nitpick examples.
     1.5  *)
     1.6  
     1.7 -Toplevel.debug := true;
     1.8  if getenv "KODKODI" = "" then
     1.9    ()
    1.10  else
     2.1 --- a/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 18:52:30 2009 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/HISTORY	Tue Nov 17 22:51:00 2009 +0100
     2.3 @@ -12,6 +12,8 @@
     2.4    * Added support for codatatype view of datatypes
     2.5    * Fixed soundness bugs related to sets and sets of sets
     2.6    * Fixed monotonicity check
     2.7 +  * Fixed error when processing definitions that resulted in an exception
     2.8 +  * Fixed error in Kodkod encoding of "The" and "Eps"
     2.9    * Fixed error in display of uncurried constants
    2.10    * Speeded up scope enumeration
    2.11  
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 18:52:30 2009 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Nov 17 22:51:00 2009 +0100
     4.3 @@ -1109,13 +1109,13 @@
     4.4      |> map_filter (try (Refute.specialize_type thy x))
     4.5      |> filter (equal (Const x) o term_under_def)
     4.6  
     4.7 -(* term -> term *)
     4.8 +(* theory -> term -> term option *)
     4.9  fun normalized_rhs_of thy t =
    4.10    let
    4.11 -    (* term -> term *)
    4.12 -    fun aux (v as Var _) t = lambda v t
    4.13 -      | aux (c as Const (@{const_name TYPE}, T)) t = lambda c t
    4.14 -      | aux _ _ = raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    4.15 +    (* term option -> term option *)
    4.16 +    fun aux (v as Var _) (SOME t) = SOME (lambda v t)
    4.17 +      | aux (c as Const (@{const_name TYPE}, T)) (SOME t) = SOME (lambda c t)
    4.18 +      | aux _ _ = NONE
    4.19      val (lhs, rhs) =
    4.20        case t of
    4.21          Const (@{const_name "=="}, _) $ t1 $ t2 => (t1, t2)
    4.22 @@ -1123,7 +1123,7 @@
    4.23          (t1, t2)
    4.24        | _ => raise TERM ("Nitpick_HOL.normalized_rhs_of", [t])
    4.25      val args = strip_comb lhs |> snd
    4.26 -  in fold_rev aux args rhs end
    4.27 +  in fold_rev aux args (SOME rhs) end
    4.28  
    4.29  (* theory -> const_table -> styp -> term option *)
    4.30  fun def_of_const thy table (x as (s, _)) =
    4.31 @@ -1131,7 +1131,7 @@
    4.32      NONE
    4.33    else
    4.34      x |> def_props_for_const thy false table |> List.last
    4.35 -      |> normalized_rhs_of thy |> prefix_abs_vars s |> SOME
    4.36 +      |> normalized_rhs_of thy |> Option.map (prefix_abs_vars s)
    4.37      handle List.Empty => NONE
    4.38  
    4.39  datatype fixpoint_kind = Lfp | Gfp | NoFp
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 18:52:30 2009 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Nov 17 22:51:00 2009 +0100
     5.3 @@ -1092,6 +1092,12 @@
     5.4                    else
     5.5                      kk_rel_eq r1 r2
     5.6                  end)
     5.7 +         | Op2 (The, T, _, u1, u2) =>
     5.8 +           to_f_with_polarity polar
     5.9 +                              (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
    5.10 +         | Op2 (Eps, T, _, u1, u2) =>
    5.11 +           to_f_with_polarity polar
    5.12 +                              (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
    5.13           | Op2 (Apply, T, _, u1, u2) =>
    5.14             (case (polar, rep_of u1) of
    5.15                (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 18:52:30 2009 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Nov 17 22:51:00 2009 +0100
     6.3 @@ -1158,8 +1158,10 @@
     6.4              let
     6.5                val u1' = sub u1
     6.6                val opt1 = is_opt_rep (rep_of u1')
     6.7 +              val opt = (oper = Eps orelse opt1)
     6.8                val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
     6.9 -              val R = unopt_R |> (oper = Eps orelse opt1) ? opt_rep ofs T
    6.10 +              val R = if is_boolean_type T then bool_rep polar opt
    6.11 +                      else unopt_R |> opt ? opt_rep ofs T
    6.12                val u = Op2 (oper, T, R, u1', sub u2)
    6.13              in
    6.14                if is_precise_type datatypes T orelse not opt1 then