# HG changeset patch # User blanchet # Date 1284464683 -7200 # Node ID cdf2c33414228de6c161ae38f35228cc3fcde415 # Parent 6f49c7fbb1b1abdbc3b5256d657fafd300ad5f5d eliminate more clutter related to "fast_descrs" optimization diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Sep 14 13:44:43 2010 +0200 @@ -424,7 +424,6 @@ (@{const_name unknown}, 0), (@{const_name is_unknown}, 1), (@{const_name safe_The}, 1), - (@{const_name safe_Eps}, 1), (@{const_name Frac}, 0), (@{const_name norm_frac}, 0)] val built_in_nat_consts = diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Sep 14 13:44:43 2010 +0200 @@ -1039,10 +1039,6 @@ fun kk_vect_set_bool_op connective k r1 r2 = fold1 kk_and (map2 connective (unpack_formulas k r1) (unpack_formulas k r2)) - fun is_surely_singleton R r = - kk_and (kk_subset (full_rel_for_rep R) - (kk_join r (full_rel_for_rep bool_atom_R))) - (kk_one (kk_join r true_atom)) fun to_f u = case rep_of u of Formula polar => @@ -1185,12 +1181,6 @@ else kk_rel_eq r1 r2 end) - | Op2 (The, T, _, u1, u2) => - to_f_with_polarity polar - (Op2 (The, T, Opt (Atom (2, bool_j0)), u1, u2)) - | Op2 (Eps, T, _, u1, u2) => - to_f_with_polarity polar - (Op2 (Eps, T, Opt (Atom (2, bool_j0)), u1, u2)) | Op2 (Apply, T, _, u1, u2) => (case (polar, rep_of u1) of (Neg, Func (R, Formula Neut)) => kk_subset (to_opt R u2) (to_r u1) @@ -1473,41 +1463,6 @@ KK.None) (to_rep R1 u1) (to_rep R1 u2) end) - | Op2 (The, _, R, u1, u2) => - if is_opt_rep R then - let val r1 = to_opt (Func (unopt_rep R, bool_atom_R)) u1 in - kk_rel_if (is_surely_singleton R r1) (kk_join r1 true_atom) - (kk_rel_if (kk_or (kk_some (kk_join r1 true_atom)) - (kk_subset (full_rel_for_rep R) - (kk_join r1 false_atom))) - (to_rep R u2) (empty_rel_for_rep R)) - end - else - let val r1 = to_rep (Func (R, Formula Neut)) u1 in - kk_rel_if (kk_one r1) r1 (to_rep R u2) - end - | Op2 (Eps, _, R, u1, u2) => - if is_opt_rep (rep_of u1) then - let - val r1 = to_rep (Func (unopt_rep R, Opt bool_atom_R)) u1 - val r2 = to_rep R u2 - in - kk_union (kk_rel_if (is_surely_singleton R r1) - (kk_join r1 true_atom) (empty_rel_for_rep R)) - (kk_rel_if (kk_or (kk_subset r2 (kk_join r1 true_atom)) - (kk_subset (full_rel_for_rep R) - (kk_join r1 false_atom))) - r2 (empty_rel_for_rep R)) - end - else - let - val r1 = to_rep (Func (unopt_rep R, Formula Neut)) u1 - val r2 = to_rep R u2 - in - kk_union (kk_rel_if (kk_one r1) r1 (empty_rel_for_rep R)) - (kk_rel_if (kk_or (kk_no r1) (kk_subset r2 r1)) - r2 (empty_rel_for_rep R)) - end | Op2 (Triad, _, Opt (Atom (2, j0)), u1, u2) => let val f1 = to_f u1 diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Sep 14 13:44:43 2010 +0200 @@ -816,16 +816,6 @@ let val t = nth evals (the (Int.fromString (unprefix eval_prefix s))) in (t, format_term_type thy def_table formats t) end - else if s = @{const_name undefined_fast_The} then - (Const (nitpick_prefix ^ "The fallback", T), - format_type default_format - (lookup_format thy def_table formats - (Const (@{const_name The}, (T --> bool_T) --> T))) T) - else if s = @{const_name undefined_fast_Eps} then - (Const (nitpick_prefix ^ "Eps fallback", T), - format_type default_format - (lookup_format thy def_table formats - (Const (@{const_name Eps}, (T --> bool_T) --> T))) T) else let val t = Const (original_name s, T) in (t, format_term_type thy def_table formats t) diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Sep 14 13:44:43 2010 +0200 @@ -711,8 +711,7 @@ MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) end | _ => - if s = @{const_name safe_The} orelse - s = @{const_name safe_Eps} then + if s = @{const_name safe_The} then let val a_set_M = mtype_for (domain_type T) val a_M = dest_MFun a_set_M |> #1 diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Sep 14 13:44:43 2010 +0200 @@ -53,8 +53,6 @@ Subset | DefEq | Eq | - The | - Eps | Triad | Composition | Product | @@ -170,8 +168,6 @@ Subset | DefEq | Eq | - The | - Eps | Triad | Composition | Product | @@ -237,8 +233,6 @@ | string_for_op2 Subset = "Subset" | string_for_op2 DefEq = "DefEq" | string_for_op2 Eq = "Eq" - | string_for_op2 The = "The" - | string_for_op2 Eps = "Eps" | string_for_op2 Triad = "Triad" | string_for_op2 Composition = "Composition" | string_for_op2 Product = "Product" @@ -674,16 +668,14 @@ else if is_rep_fun ctxt x then Func oo best_non_opt_symmetric_reps_for_fun_type else if all_exact orelse is_skolem_name v orelse - member (op =) [@{const_name undefined_fast_The}, - @{const_name undefined_fast_Eps}, - @{const_name bisim}, - @{const_name bisim_iterator_max}] - (original_name s) then + member (op =) [@{const_name bisim}, + @{const_name bisim_iterator_max}] + (original_name s) then best_non_opt_set_rep_for_type else if member (op =) [@{const_name set}, @{const_name distinct}, @{const_name ord_class.less}, @{const_name ord_class.less_eq}] - (original_name s) then + (original_name s) then best_set_rep_for_type else best_opt_set_rep_for_type) scope T @@ -1072,29 +1064,6 @@ raise SAME ()) handle SAME () => s_op2 oper T (Formula polar) u1' u2' end - else if oper = The orelse oper = Eps then - let - val u1' = sub u1 - val opt1 = is_opt_rep (rep_of u1') - val opt = (oper = Eps orelse opt1) - val unopt_R = best_one_rep_for_type scope T |> optable_rep ofs T - val R = if is_boolean_type T then bool_rep polar opt - else unopt_R |> opt ? opt_rep ofs T - val u = Op2 (oper, T, R, u1', sub u2) - in - if is_complete_type datatypes true T orelse not opt1 then - u - else - let - val x_u = BoundName (~1, T, unopt_R, "descr.x") - val R = R |> opt_rep ofs T - in - Op3 (If, T, R, - Op2 (Exist, bool_T, Formula Pos, x_u, - s_op2 Apply bool_T (Formula Pos) (gsub false Pos u1) - x_u), u, Cst (Unknown, T, R)) - end - end else let val u1 = sub u1 diff -r 6f49c7fbb1b1 -r cdf2c3341422 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:24:18 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Sep 14 13:44:43 2010 +0200 @@ -26,8 +26,7 @@ (polar = Neg andalso quant_s <> @{const_name Ex}) val is_descr = - member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}, - @{const_name safe_Eps}] + member (op =) [@{const_name The}, @{const_name Eps}, @{const_name safe_The}] (** Binary coding of integers **)