eliminate more clutter related to "fast_descrs" optimization
authorblanchet
Tue Sep 14 13:44:43 2010 +0200 (2010-09-14)
changeset 39360cdf2c3341422
parent 39359 6f49c7fbb1b1
child 39361 520ea38711e4
eliminate more clutter related to "fast_descrs" optimization
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 14 13:24:18 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Sep 14 13:44:43 2010 +0200
     1.3 @@ -424,7 +424,6 @@
     1.4     (@{const_name unknown}, 0),
     1.5     (@{const_name is_unknown}, 1),
     1.6     (@{const_name safe_The}, 1),
     1.7 -   (@{const_name safe_Eps}, 1),
     1.8     (@{const_name Frac}, 0),
     1.9     (@{const_name norm_frac}, 0)]
    1.10  val built_in_nat_consts =
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Sep 14 13:24:18 2010 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Sep 14 13:44:43 2010 +0200
     2.3 @@ -1039,10 +1039,6 @@
     2.4      fun kk_vect_set_bool_op connective k r1 r2 =
     2.5        fold1 kk_and (map2 connective (unpack_formulas k r1)
     2.6                           (unpack_formulas k r2))
     2.7 -    fun is_surely_singleton R r =
     2.8 -      kk_and (kk_subset (full_rel_for_rep R)
     2.9 -                        (kk_join r (full_rel_for_rep bool_atom_R)))
    2.10 -             (kk_one (kk_join r true_atom))
    2.11      fun to_f u =
    2.12        case rep_of u of
    2.13          Formula polar =>
    2.14 @@ -1185,12 +1181,6 @@
    2.15                    else
    2.16                      kk_rel_eq r1 r2
    2.17                  end)
    2.18 -         | Op2 (The, T, _, u1, u2) =>
    2.19 -           to_f_with_polarity polar
    2.20 -                              (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2))
    2.21 -         | Op2 (Eps, T, _, u1, u2) =>
    2.22 -           to_f_with_polarity polar
    2.23 -                              (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2))
    2.24           | Op2 (Apply, T, _, u1, u2) =>
    2.25             (case (polar, rep_of u1) of
    2.26                (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1)
    2.27 @@ -1473,41 +1463,6 @@
    2.28                           KK.None)
    2.29                   (to_rep R1 u1) (to_rep R1 u2)
    2.30              end)
    2.31 -      | Op2 (The, _, R, u1, u2) =>
    2.32 -        if is_opt_rep R then
    2.33 -          let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in
    2.34 -            kk_rel_if (is_surely_singleton R r1) (kk_join r1 true_atom)
    2.35 -                      (kk_rel_if (kk_or (kk_some (kk_join r1 true_atom))
    2.36 -                                        (kk_subset (full_rel_for_rep R)
    2.37 -                                                   (kk_join r1 false_atom)))
    2.38 -                                 (to_rep R u2) (empty_rel_for_rep R))
    2.39 -          end
    2.40 -        else
    2.41 -          let val r1 = to_rep (Func (R, Formula Neut)) u1 in
    2.42 -            kk_rel_if (kk_one r1) r1 (to_rep R u2)
    2.43 -          end
    2.44 -      | Op2 (Eps, _, R, u1, u2) =>
    2.45 -        if is_opt_rep (rep_of u1) then
    2.46 -          let
    2.47 -            val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1
    2.48 -            val r2 = to_rep R u2
    2.49 -          in
    2.50 -            kk_union (kk_rel_if (is_surely_singleton R r1)
    2.51 -                                (kk_join r1 true_atom) (empty_rel_for_rep R))
    2.52 -                     (kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom))
    2.53 -                                       (kk_subset (full_rel_for_rep R)
    2.54 -                                                  (kk_join r1 false_atom)))
    2.55 -                                r2 (empty_rel_for_rep R))
    2.56 -          end
    2.57 -        else
    2.58 -          let
    2.59 -            val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1
    2.60 -            val r2 = to_rep R u2
    2.61 -          in
    2.62 -            kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R))
    2.63 -                     (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1))
    2.64 -                                r2 (empty_rel_for_rep R))
    2.65 -          end
    2.66        | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) =>
    2.67          let
    2.68            val f1 = to_f u1
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 13:24:18 2010 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Sep 14 13:44:43 2010 +0200
     3.3 @@ -816,16 +816,6 @@
     3.4           let
     3.5             val t = nth evals (the (Int.fromString (unprefix eval_prefix s)))
     3.6           in (t, format_term_type thy def_table formats t) end
     3.7 -       else if s = @{const_name undefined_fast_The} then
     3.8 -         (Const (nitpick_prefix ^ "The fallback", T),
     3.9 -          format_type default_format
    3.10 -                      (lookup_format thy def_table formats
    3.11 -                           (Const (@{const_name The}, (T --> bool_T) --> T))) T)
    3.12 -       else if s = @{const_name undefined_fast_Eps} then
    3.13 -         (Const (nitpick_prefix ^ "Eps fallback", T),
    3.14 -          format_type default_format
    3.15 -                      (lookup_format thy def_table formats
    3.16 -                           (Const (@{const_name Eps}, (T --> bool_T) --> T))) T)
    3.17         else
    3.18           let val t = Const (original_name s, T) in
    3.19             (t, format_term_type thy def_table formats t)
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:24:18 2010 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Sep 14 13:44:43 2010 +0200
     4.3 @@ -711,8 +711,7 @@
     4.4                           MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
     4.5                  end
     4.6                | _ =>
     4.7 -                if s = @{const_name safe_The} orelse
     4.8 -                   s = @{const_name safe_Eps} then
     4.9 +                if s = @{const_name safe_The} then
    4.10                    let
    4.11                      val a_set_M = mtype_for (domain_type T)
    4.12                      val a_M = dest_MFun a_set_M |> #1
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Sep 14 13:24:18 2010 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Sep 14 13:44:43 2010 +0200
     5.3 @@ -53,8 +53,6 @@
     5.4      Subset |
     5.5      DefEq |
     5.6      Eq |
     5.7 -    The |
     5.8 -    Eps |
     5.9      Triad |
    5.10      Composition |
    5.11      Product |
    5.12 @@ -170,8 +168,6 @@
    5.13    Subset |
    5.14    DefEq |
    5.15    Eq |
    5.16 -  The |
    5.17 -  Eps |
    5.18    Triad |
    5.19    Composition |
    5.20    Product |
    5.21 @@ -237,8 +233,6 @@
    5.22    | string_for_op2 Subset = "Subset"
    5.23    | string_for_op2 DefEq = "DefEq"
    5.24    | string_for_op2 Eq = "Eq"
    5.25 -  | string_for_op2 The = "The"
    5.26 -  | string_for_op2 Eps = "Eps"
    5.27    | string_for_op2 Triad = "Triad"
    5.28    | string_for_op2 Composition = "Composition"
    5.29    | string_for_op2 Product = "Product"
    5.30 @@ -674,16 +668,14 @@
    5.31               else if is_rep_fun ctxt x then
    5.32                 Func oo best_non_opt_symmetric_reps_for_fun_type
    5.33               else if all_exact orelse is_skolem_name v orelse
    5.34 -                    member (op =) [@{const_name undefined_fast_The},
    5.35 -                                   @{const_name undefined_fast_Eps},
    5.36 -                                   @{const_name bisim},
    5.37 -                                   @{const_name bisim_iterator_max}]
    5.38 -                           (original_name s) then
    5.39 +                     member (op =) [@{const_name bisim},
    5.40 +                                    @{const_name bisim_iterator_max}]
    5.41 +                            (original_name s) then
    5.42                 best_non_opt_set_rep_for_type
    5.43               else if member (op =) [@{const_name set}, @{const_name distinct},
    5.44                                      @{const_name ord_class.less},
    5.45                                      @{const_name ord_class.less_eq}]
    5.46 -                                   (original_name s) then
    5.47 +                            (original_name s) then
    5.48                 best_set_rep_for_type
    5.49               else
    5.50                 best_opt_set_rep_for_type) scope T
    5.51 @@ -1072,29 +1064,6 @@
    5.52                   raise SAME ())
    5.53                handle SAME () => s_op2 oper T (Formula polar) u1' u2'
    5.54              end
    5.55 -          else if oper = The orelse oper = Eps then
    5.56 -            let
    5.57 -              val u1' = sub u1
    5.58 -              val opt1 = is_opt_rep (rep_of u1')
    5.59 -              val opt = (oper = Eps orelse opt1)
    5.60 -              val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T
    5.61 -              val R = if is_boolean_type T then bool_rep polar opt
    5.62 -                      else unopt_R |> opt ? opt_rep ofs T
    5.63 -              val u = Op2 (oper, T, R, u1', sub u2)
    5.64 -            in
    5.65 -              if is_complete_type datatypes true T orelse not opt1 then
    5.66 -                u
    5.67 -              else
    5.68 -                let
    5.69 -                  val x_u = BoundName (~1, T, unopt_R, "descr.x")
    5.70 -                  val R = R |> opt_rep ofs T
    5.71 -                in
    5.72 -                  Op3 (If, T, R,
    5.73 -                       Op2 (Exist, bool_T, Formula Pos, x_u,
    5.74 -                            s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1)
    5.75 -                                  x_u), u, Cst (Unknown, T, R))
    5.76 -                end
    5.77 -            end
    5.78            else
    5.79              let
    5.80                val u1 = sub u1
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 14 13:24:18 2010 +0200
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Sep 14 13:44:43 2010 +0200
     6.3 @@ -26,8 +26,7 @@
     6.4    (polar = Neg andalso quant_s <> @{const_name Ex})
     6.5  
     6.6  val is_descr =
     6.7 -  member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The},
     6.8 -                 @{const_name safe_Eps}]
     6.9 +  member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}]
    6.10  
    6.11  (** Binary coding of integers **)
    6.12