fixed a few more bugs in \Nitpick's new "set" support
authorblanchet
Tue Jan 03 18:33:17 2012 +0100 (2012-01-03)
changeset 46085447cda88adfe
parent 46084 dd7fb9e651ad
child 46086 096697aec8a7
fixed a few more bugs in \Nitpick's new "set" support
src/HOL/Nitpick_Examples/Core_Nits.thy
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_rep.ML
     1.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy	Tue Jan 03 18:33:17 2012 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  by auto
     1.5  
     1.6  lemma "(a\<Colon>'a\<Rightarrow>'b, a) \<in> Id\<^sup>*"
     1.7 -nitpick [card = 1\<emdash>3, expect = none]
     1.8 +nitpick [card = 1\<emdash>2, expect = none]
     1.9  by auto
    1.10  
    1.11  lemma "(a\<Colon>'a\<times>'a, a) \<in> Id\<^sup>* \<union> {(a, b)}\<^sup>*"
    1.12 @@ -147,7 +147,7 @@
    1.13  nitpick [card = 15, expect = none]
    1.14  by auto
    1.15  
    1.16 -lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow> 
    1.17 +lemma "(A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R) \<Longrightarrow>
    1.18         A = B \<or> (A, B) \<in> R \<or> (\<exists>C. (A, C) \<in> R \<and> (C, B) \<in> R)"
    1.19  nitpick [card = 1\<emdash>25, expect = none]
    1.20  by auto
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Jan 03 18:33:17 2012 +0100
     2.3 @@ -1423,8 +1423,9 @@
     2.4          | Atom (k, _) =>
     2.5            let
     2.6              val dom_card = card_of_rep (rep_of arg_u)
     2.7 -            val ran_R = Atom (exact_root dom_card k,
     2.8 -                              offset_of_type ofs (range_type (type_of func_u)))
     2.9 +            val ran_R =
    2.10 +              Atom (exact_root dom_card k,
    2.11 +                    offset_of_type ofs (pseudo_range_type (type_of func_u)))
    2.12            in
    2.13              to_apply_vect dom_card ran_R res_R (to_vect dom_card ran_R func_u)
    2.14                            arg_u
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     3.3 @@ -845,7 +845,7 @@
     3.4              | @{const_name fst} => do_nth_pair_sel 0 T accum
     3.5              | @{const_name snd} => do_nth_pair_sel 1 T accum
     3.6              | @{const_name Id} =>
     3.7 -              (MFun (mtype_for (domain_type T), A Gen, bool_M), accum)
     3.8 +              (MFun (mtype_for (elem_type T), A Gen, bool_M), accum)
     3.9              | @{const_name converse} =>
    3.10                let
    3.11                  val x = Unsynchronized.inc max_fresh
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Jan 03 18:33:17 2012 +0100
     4.3 @@ -562,11 +562,11 @@
     4.4              do_apply t0 ts
     4.5          | (t0 as Const (x as (@{const_name ord_class.less_eq}, T)),
     4.6             ts as [t1, t2]) =>
     4.7 -          if is_built_in_const thy stds x then
     4.8 +          if is_set_like_type (domain_type T) then
     4.9 +            Op2 (Subset, bool_T, Any, sub t1, sub t2)
    4.10 +          else if is_built_in_const thy stds x then
    4.11              (* FIXME: find out if this case is necessary *)
    4.12              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
    4.13 -          else if is_set_like_type (domain_type T) then
    4.14 -            Op2 (Subset, bool_T, Any, sub t1, sub t2)
    4.15            else
    4.16              do_apply t0 ts
    4.17          | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
    4.18 @@ -968,7 +968,7 @@
    4.19                 val u2' = aux table' false Neut u2
    4.20                 val R =
    4.21                   if is_opt_rep (rep_of u2') orelse
    4.22 -                    (range_type T = bool_T andalso
    4.23 +                    (pseudo_range_type T = bool_T andalso
    4.24                       not (is_Cst False (unrepify_nut_in_nut table false Neut
    4.25                                                              u1 u2))) then
    4.26                     opt_rep ofs T R
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Jan 03 18:33:17 2012 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML	Tue Jan 03 18:33:17 2012 +0100
     5.3 @@ -234,7 +234,8 @@
     5.4  fun rep_to_binary_rel_rep ofs T R =
     5.5    let
     5.6      val k = exact_root 2 (card_of_domain_from_rep 2 R)
     5.7 -    val j0 = offset_of_type ofs (fst (HOLogic.dest_prodT (domain_type T)))
     5.8 +    val j0 =
     5.9 +      offset_of_type ofs (fst (HOLogic.dest_prodT (pseudo_domain_type T)))
    5.10    in Func (Struct [Atom (k, j0), Atom (k, j0)], Formula Neut) end
    5.11  
    5.12  fun best_one_rep_for_type (scope as {card_assigns, ...} : scope)