removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
authorblanchet
Tue Dec 07 11:56:01 2010 +0100 (2010-12-07)
changeset 410490edd245892ed
parent 41048 d5ebe94248ad
child 41050 effbaa323cf0
removed needless optimization for image -- there might be cases that benefit from it but there are others where it is clearly evil
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     1.3 @@ -424,7 +424,6 @@
     1.4     (@{const_name converse}, 1),
     1.5     (@{const_name trancl}, 1),
     1.6     (@{const_name rel_comp}, 2),
     1.7 -   (@{const_name image}, 2),
     1.8     (@{const_name finite}, 1),
     1.9     (@{const_name unknown}, 0),
    1.10     (@{const_name is_unknown}, 1),
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Tue Dec 07 11:56:01 2010 +0100
     2.3 @@ -1510,33 +1510,6 @@
     2.4             | _ => raise NUT ("Nitpick_Kodkod.to_r (Composition)", [u]))
     2.5            |> rel_expr_from_rel_expr kk R (Func (Struct [a_R, c_R], body_R))
     2.6          end
     2.7 -      | Op2 (Image, T, R, u1, u2) =>
     2.8 -        (case (rep_of u1, rep_of u2) of
     2.9 -           (Func (R11, R12), Func (R21, Formula Neut)) =>
    2.10 -           if R21 = R11 andalso is_lone_rep R12 then
    2.11 -             let
    2.12 -               fun big_join r = kk_n_fold_join kk false R21 R12 r (to_r u1)
    2.13 -               val core_r = big_join (to_r u2)
    2.14 -               val core_R = Func (R12, Formula Neut)
    2.15 -             in
    2.16 -               if is_opt_rep R12 then
    2.17 -                 let
    2.18 -                   val schema = atom_schema_of_rep R21
    2.19 -                   val decls = decls_for_atom_schema ~1 schema
    2.20 -                   val vars = unary_var_seq ~1 (length decls)
    2.21 -                   val f = kk_some (big_join (fold1 kk_product vars))
    2.22 -                 in
    2.23 -                   kk_rel_if (kk_all decls f)
    2.24 -                             (rel_expr_from_rel_expr kk R core_R core_r)
    2.25 -                             (rel_expr_from_rel_expr kk R (opt_rep ofs T core_R)
    2.26 -                                              (kk_product core_r true_atom))
    2.27 -                 end
    2.28 -               else
    2.29 -                 rel_expr_from_rel_expr kk R core_R core_r
    2.30 -             end
    2.31 -           else
    2.32 -             raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2])
    2.33 -         | _ => raise NUT ("Nitpick_Kodkod.to_r (Image)", [u1, u2]))
    2.34        | Op2 (Apply, @{typ nat}, _,
    2.35               Op2 (Apply, _, _, Cst (Subtract, _, _), u1), u2) =>
    2.36          if is_Cst Unrep u2 andalso not (is_opt_rep (rep_of u1)) then
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     3.3 @@ -912,17 +912,6 @@
     3.4                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
     3.5                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
     3.6                end
     3.7 -            | @{const_name image} =>
     3.8 -              let
     3.9 -                val x = Unsynchronized.inc max_fresh
    3.10 -                val a_M = mtype_for (domain_type (domain_type T))
    3.11 -                val b_M = mtype_for (range_type (domain_type T))
    3.12 -              in
    3.13 -                (MFun (MFun (a_M, A Gen, b_M), A Gen,
    3.14 -                       MFun (MFun (a_M, V x, bool_M), A Gen,
    3.15 -                             MFun (b_M, V x, bool_M))),
    3.16 -                 accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    3.17 -              end
    3.18              | @{const_name finite} =>
    3.19                let
    3.20                  val M1 = mtype_for (domain_type (domain_type T))
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Tue Dec 07 11:56:01 2010 +0100
     4.3 @@ -55,7 +55,6 @@
     4.4      Eq |
     4.5      Triad |
     4.6      Composition |
     4.7 -    Image |
     4.8      Apply |
     4.9      Lambda
    4.10  
    4.11 @@ -169,7 +168,6 @@
    4.12    Eq |
    4.13    Triad |
    4.14    Composition |
    4.15 -  Image |
    4.16    Apply |
    4.17    Lambda
    4.18  
    4.19 @@ -233,7 +231,6 @@
    4.20    | string_for_op2 Eq = "Eq"
    4.21    | string_for_op2 Triad = "Triad"
    4.22    | string_for_op2 Composition = "Composition"
    4.23 -  | string_for_op2 Image = "Image"
    4.24    | string_for_op2 Apply = "Apply"
    4.25    | string_for_op2 Lambda = "Lambda"
    4.26  
    4.27 @@ -525,8 +522,6 @@
    4.28            Op1 (Closure, range_type T, Any, sub t1)
    4.29          | (Const (@{const_name rel_comp}, T), [t1, t2]) =>
    4.30            Op2 (Composition, nth_range_type 2 T, Any, sub t1, sub t2)
    4.31 -        | (Const (@{const_name image}, T), [t1, t2]) =>
    4.32 -          Op2 (Image, nth_range_type 2 T, Any, sub t1, sub t2)
    4.33          | (Const (x as (s as @{const_name Suc}, T)), []) =>
    4.34            if is_built_in_const thy stds x then Cst (Suc, T, Any)
    4.35            else if is_constr ctxt stds x then do_construct x []
    4.36 @@ -936,46 +931,6 @@
    4.37                Cst (False, T, Formula Pos)
    4.38                |> polar = Neut ? (fn pos_u => triad pos_u (gsub def Neg u))
    4.39            end
    4.40 -        | Op2 (Image, T, _, u1, u2) =>
    4.41 -          let
    4.42 -            val u1' = sub u1
    4.43 -            val u2' = sub u2
    4.44 -          in
    4.45 -            (case (rep_of u1', rep_of u2') of
    4.46 -               (Func (R11, R12), Func (R21, Formula Neut)) =>
    4.47 -               if R21 = R11 andalso is_lone_rep R12 then
    4.48 -                 let
    4.49 -                   val R =
    4.50 -                     best_non_opt_set_rep_for_type scope T
    4.51 -                     |> exists (is_opt_rep o rep_of) [u1', u2'] ? opt_rep ofs T
    4.52 -                 in s_op2 Image T R u1' u2' end
    4.53 -               else
    4.54 -                 raise SAME ()
    4.55 -             | _ => raise SAME ())
    4.56 -            handle SAME () =>
    4.57 -                   let
    4.58 -                     val T1 = type_of u1
    4.59 -                     val dom_T = domain_type T1
    4.60 -                     val ran_T = range_type T1
    4.61 -                     val x_u = BoundName (~1, dom_T, Any, "image.x")
    4.62 -                     val y_u = BoundName (~2, ran_T, Any, "image.y")
    4.63 -                   in
    4.64 -                     Op2 (Lambda, T, Any, y_u,
    4.65 -                          Op2 (Exist, bool_T, Any, x_u,
    4.66 -                               Op2 (And, bool_T, Any,
    4.67 -                                    case u2 of
    4.68 -                                      Op2 (Lambda, _, _, u21, u22) =>
    4.69 -                                      if num_occurrences_in_nut u21 u22 = 0 then
    4.70 -                                        u22
    4.71 -                                      else
    4.72 -                                        Op2 (Apply, bool_T, Any, u2, x_u)
    4.73 -                                    | _ => Op2 (Apply, bool_T, Any, u2, x_u),
    4.74 -
    4.75 -                                    Op2 (Eq, bool_T, Any, y_u,
    4.76 -                                         Op2 (Apply, ran_T, Any, u1, x_u)))))
    4.77 -                     |> sub
    4.78 -                   end
    4.79 -          end
    4.80          | Op2 (Apply, T, _, u1, u2) =>
    4.81            let
    4.82              val u1 = sub u1