avoid unsound simplification of (C (s x)) when s is a selector but not C's
authorblanchet
Mon Oct 05 15:57:25 2015 +0200 (2015-10-05)
changeset 61324d4ec7594f558
parent 61323 99b3a17a7eab
child 61325 1cfc476198c9
avoid unsound simplification of (C (s x)) when s is a selector but not C's
NEWS
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_nut.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
     1.1 --- a/NEWS	Mon Oct 05 13:26:25 2015 +0200
     1.2 +++ b/NEWS	Mon Oct 05 15:57:25 2015 +0200
     1.3 @@ -253,6 +253,7 @@
     1.4    - Eliminated obsolete "blocking" option and related subcommands.
     1.5  
     1.6  * Nitpick:
     1.7 +  - Fixed soundness bug in "destroy_constrs" optimization.
     1.8    - Removed "check_potential" and "check_genuine" options.
     1.9    - Eliminated obsolete "blocking" option.
    1.10  
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 05 13:26:25 2015 +0200
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Mon Oct 05 15:57:25 2015 +0200
     2.3 @@ -390,12 +390,12 @@
     2.4     (@{const_name unknown}, 0),
     2.5     (@{const_name is_unknown}, 1),
     2.6     (@{const_name safe_The}, 1),
     2.7 -   (@{const_name Nitpick.Frac}, 0),
     2.8 -   (@{const_name Nitpick.norm_frac}, 0),
     2.9 +   (@{const_name Frac}, 0),
    2.10 +   (@{const_name norm_frac}, 0),
    2.11     (@{const_name Suc}, 0),
    2.12     (@{const_name nat}, 0),
    2.13 -   (@{const_name Nitpick.nat_gcd}, 0),
    2.14 -   (@{const_name Nitpick.nat_lcm}, 0)]
    2.15 +   (@{const_name nat_gcd}, 0),
    2.16 +   (@{const_name nat_lcm}, 0)]
    2.17  val built_in_typed_consts =
    2.18    [((@{const_name zero_class.zero}, nat_T), 0),
    2.19     ((@{const_name one_class.one}, nat_T), 0),
    2.20 @@ -583,9 +583,9 @@
    2.21  fun typedef_info ctxt s =
    2.22    if is_frac_type ctxt (Type (s, [])) then
    2.23      SOME {abs_type = Type (s, []), rep_type = @{typ "int * int"},
    2.24 -          Abs_name = @{const_name Nitpick.Abs_Frac},
    2.25 -          Rep_name = @{const_name Nitpick.Rep_Frac},
    2.26 -          prop_of_Rep = @{prop "Nitpick.Rep_Frac x \<in> Collect Nitpick.Frac"}
    2.27 +          Abs_name = @{const_name Abs_Frac},
    2.28 +          Rep_name = @{const_name Rep_Frac},
    2.29 +          prop_of_Rep = @{prop "Rep_Frac x \<in> Collect Frac"}
    2.30                          |> Logic.varify_global,
    2.31            Abs_inverse = NONE, Rep_inverse = NONE}
    2.32    else case Typedef.get_info ctxt s of
    2.33 @@ -859,7 +859,7 @@
    2.34  
    2.35  fun is_stale_constr ctxt (x as (s, T)) =
    2.36    is_registered_type ctxt (body_type T) andalso is_nonfree_constr ctxt x andalso
    2.37 -  not (s = @{const_name Nitpick.Abs_Frac} orelse is_registered_coconstr ctxt x)
    2.38 +  not (s = @{const_name Abs_Frac} orelse is_registered_coconstr ctxt x)
    2.39  
    2.40  fun is_constr ctxt (x as (_, T)) =
    2.41    is_nonfree_constr ctxt x andalso
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 05 13:26:25 2015 +0200
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Mon Oct 05 15:57:25 2015 +0200
     3.3 @@ -579,7 +579,7 @@
     3.4                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
     3.5                      |> dest_n_tuple (length uncur_arg_Ts)
     3.6                  val t =
     3.7 -                  if constr_s = @{const_name Nitpick.Abs_Frac} then
     3.8 +                  if constr_s = @{const_name Abs_Frac} then
     3.9                      case ts of
    3.10                        [Const (@{const_name Pair}, _) $ t1 $ t2] =>
    3.11                        frac_from_term_pair (body_type T) t1 t2
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Oct 05 13:26:25 2015 +0200
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML	Mon Oct 05 15:57:25 2015 +0200
     4.3 @@ -569,8 +569,8 @@
     4.4              Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
     4.5            else
     4.6              do_apply t0 ts
     4.7 -        | (Const (@{const_name Nitpick.nat_gcd}, T), []) => Cst (Gcd, T, Any)
     4.8 -        | (Const (@{const_name Nitpick.nat_lcm}, T), []) => Cst (Lcm, T, Any)
     4.9 +        | (Const (@{const_name nat_gcd}, T), []) => Cst (Gcd, T, Any)
    4.10 +        | (Const (@{const_name nat_lcm}, T), []) => Cst (Lcm, T, Any)
    4.11          | (Const (x as (s as @{const_name uminus_class.uminus}, T)), []) =>
    4.12            if is_built_in_const x then
    4.13              let val num_T = domain_type T in
    4.14 @@ -586,8 +586,8 @@
    4.15          | (Const (@{const_name safe_The},
    4.16                    Type (@{type_name fun}, [_, T2])), [t1]) =>
    4.17            Op1 (SafeThe, T2, Any, sub t1)
    4.18 -        | (Const (@{const_name Nitpick.Frac}, T), []) => Cst (Fracs, T, Any)
    4.19 -        | (Const (@{const_name Nitpick.norm_frac}, T), []) =>
    4.20 +        | (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
    4.21 +        | (Const (@{const_name norm_frac}, T), []) =>
    4.22            Cst (NormFrac, T, Any)
    4.23          | (Const (@{const_name of_nat}, T as @{typ "nat => int"}), []) =>
    4.24            Cst (NatToInt, T, Any)
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Oct 05 13:26:25 2015 +0200
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Mon Oct 05 15:57:25 2015 +0200
     5.3 @@ -46,9 +46,9 @@
     5.4        | aux def (t as Const (s, _)) =
     5.5          (not def orelse t <> @{const Suc}) andalso
     5.6          not (member (op =)
     5.7 -               [@{const_name Nitpick.Abs_Frac}, @{const_name Nitpick.Rep_Frac},
     5.8 -                @{const_name Nitpick.nat_gcd}, @{const_name Nitpick.nat_lcm},
     5.9 -                @{const_name Nitpick.Frac}, @{const_name Nitpick.norm_frac}] s)
    5.10 +               [@{const_name Abs_Frac}, @{const_name Rep_Frac},
    5.11 +                @{const_name nat_gcd}, @{const_name nat_lcm},
    5.12 +                @{const_name Frac}, @{const_name norm_frac}] s)
    5.13        | aux def (Abs (_, _, t')) = aux def t'
    5.14        | aux _ _ = true
    5.15    in aux end
    5.16 @@ -1055,15 +1055,15 @@
    5.17  
    5.18  fun simplify_constrs_and_sels ctxt t =
    5.19    let
    5.20 -    fun is_nth_sel_on t' n (Const (s, _) $ t) =
    5.21 +    fun is_nth_sel_on constr_s t' n (Const (s, _) $ t) =
    5.22          (t = t' andalso is_sel_like_and_no_discr s andalso
    5.23 -         sel_no_from_name s = n)
    5.24 -      | is_nth_sel_on _ _ _ = false
    5.25 -    fun do_term (Const (@{const_name Nitpick.Rep_Frac}, _)
    5.26 -                 $ (Const (@{const_name Nitpick.Abs_Frac}, _) $ t1)) [] =
    5.27 +         constr_name_for_sel_like s = constr_s andalso sel_no_from_name s = n)
    5.28 +      | is_nth_sel_on _ _ _ _ = false
    5.29 +    fun do_term (Const (@{const_name Rep_Frac}, _)
    5.30 +                 $ (Const (@{const_name Abs_Frac}, _) $ t1)) [] =
    5.31          do_term t1 []
    5.32 -      | do_term (Const (@{const_name Nitpick.Abs_Frac}, _)
    5.33 -                 $ (Const (@{const_name Nitpick.Rep_Frac}, _) $ t1)) [] =
    5.34 +      | do_term (Const (@{const_name Abs_Frac}, _)
    5.35 +                 $ (Const (@{const_name Rep_Frac}, _) $ t1)) [] =
    5.36          do_term t1 []
    5.37        | do_term (t1 $ t2) args = do_term t1 (do_term t2 [] :: args)
    5.38        | do_term (t as Const (x as (s, T))) (args as _ :: _) =
    5.39 @@ -1072,7 +1072,7 @@
    5.40                case hd args of
    5.41                  Const (_, T') $ t' =>
    5.42                  if domain_type T' = body_type T andalso
    5.43 -                   forall (uncurry (is_nth_sel_on t'))
    5.44 +                   forall (uncurry (is_nth_sel_on s t'))
    5.45                            (index_seq 0 (length args) ~~ args) then
    5.46                    t'
    5.47                  else