src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 46081 8f6465f7021b
parent 41471 54a58904a598
child 46083 efeaa79f021b
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Jan 03 18:33:17 2012 +0100
     1.3 @@ -224,6 +224,7 @@
     1.4          Type (@{type_name fun}, [T1, T2]) =>
     1.5          MFun (fresh_mfun_for_fun_type mdata all_minus T1 T2)
     1.6        | Type (@{type_name prod}, [T1, T2]) => MPair (pairself do_type (T1, T2))
     1.7 +      | Type (@{type_name set}, [T']) => do_type (T' --> bool_T)
     1.8        | Type (z as (s, _)) =>
     1.9          if could_exist_alpha_sub_mtype ctxt alpha_T T then
    1.10            case AList.lookup (op =) (!datatype_mcache) z of
    1.11 @@ -474,15 +475,18 @@
    1.12  
    1.13  fun prop_for_bool b = if b then Prop_Logic.True else Prop_Logic.False
    1.14  fun prop_for_bool_var_equality (v1, v2) =
    1.15 -  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1, Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
    1.16 -           Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1), Prop_Logic.BoolVar v2))
    1.17 +  Prop_Logic.SAnd (Prop_Logic.SOr (Prop_Logic.BoolVar v1,
    1.18 +                                   Prop_Logic.SNot (Prop_Logic.BoolVar v2)),
    1.19 +                   Prop_Logic.SOr (Prop_Logic.SNot (Prop_Logic.BoolVar v1),
    1.20 +                                   Prop_Logic.BoolVar v2))
    1.21  fun prop_for_assign (x, a) =
    1.22    let val (b1, b2) = bools_from_annotation a in
    1.23      Prop_Logic.SAnd (Prop_Logic.BoolVar (fst_var x) |> not b1 ? Prop_Logic.SNot,
    1.24 -             Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
    1.25 +                     Prop_Logic.BoolVar (snd_var x) |> not b2 ? Prop_Logic.SNot)
    1.26    end
    1.27  fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
    1.28 -  | prop_for_assign_literal (x, (Minus, a)) = Prop_Logic.SNot (prop_for_assign (x, a))
    1.29 +  | prop_for_assign_literal (x, (Minus, a)) =
    1.30 +    Prop_Logic.SNot (prop_for_assign (x, a))
    1.31  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
    1.32    | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
    1.33  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
    1.34 @@ -499,7 +503,8 @@
    1.35    | prop_for_comp (aa1, aa2, Neq, []) =
    1.36      Prop_Logic.SNot (prop_for_comp (aa1, aa2, Eq, []))
    1.37    | prop_for_comp (aa1, aa2, Leq, []) =
    1.38 -    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
    1.39 +    Prop_Logic.SOr (prop_for_atom_equality (aa1, aa2),
    1.40 +                    prop_for_atom_assign (aa2, Gen))
    1.41    | prop_for_comp (aa1, aa2, cmp, xs) =
    1.42      Prop_Logic.SOr (prop_for_exists_var_assign_literal xs Gen,
    1.43              prop_for_comp (aa1, aa2, cmp, []))
    1.44 @@ -540,7 +545,8 @@
    1.45        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
    1.46      val _ = print_problem comps clauses
    1.47      val prop =
    1.48 -      Prop_Logic.all (map prop_for_comp comps @ map prop_for_assign_clause clauses)
    1.49 +      Prop_Logic.all (map prop_for_comp comps @
    1.50 +                      map prop_for_assign_clause clauses)
    1.51    in
    1.52      if Prop_Logic.eval (K false) prop then
    1.53        do_assigns (K (SOME false))
    1.54 @@ -739,6 +745,7 @@
    1.55          <= length ts
    1.56        | _ => true
    1.57      val mtype_for = fresh_mtype_for_type mdata false
    1.58 +    fun mtype_for_set x T = MFun (mtype_for (elem_type T), V x, bool_M)
    1.59      fun do_all T (gamma, cset) =
    1.60        let
    1.61          val abs_M = mtype_for (domain_type (domain_type T))
    1.62 @@ -774,6 +781,8 @@
    1.63          fun custom_mtype_for (T as Type (@{type_name fun}, [T1, T2])) =
    1.64              if T = set_T then set_M
    1.65              else MFun (custom_mtype_for T1, A Gen, custom_mtype_for T2)
    1.66 +          | custom_mtype_for (Type (@{type_name set}, [T'])) =
    1.67 +            custom_mtype_for (T' --> bool_T)
    1.68            | custom_mtype_for T = mtype_for T
    1.69        in
    1.70          (custom_mtype_for T, (gamma, cset |> add_mtype_is_concrete [] set_M))
    1.71 @@ -840,10 +849,8 @@
    1.72              | @{const_name converse} =>
    1.73                let
    1.74                  val x = Unsynchronized.inc max_fresh
    1.75 -                fun mtype_for_set T =
    1.76 -                  MFun (mtype_for (domain_type T), V x, bool_M)
    1.77 -                val ab_set_M = domain_type T |> mtype_for_set
    1.78 -                val ba_set_M = range_type T |> mtype_for_set
    1.79 +                val ab_set_M = domain_type T |> mtype_for_set x
    1.80 +                val ba_set_M = range_type T |> mtype_for_set x
    1.81                in
    1.82                  (MFun (ab_set_M, A Gen, ba_set_M),
    1.83                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.84 @@ -852,29 +859,25 @@
    1.85              | @{const_name rel_comp} =>
    1.86                let
    1.87                  val x = Unsynchronized.inc max_fresh
    1.88 -                fun mtype_for_set T =
    1.89 -                  MFun (mtype_for (domain_type T), V x, bool_M)
    1.90 -                val bc_set_M = domain_type T |> mtype_for_set
    1.91 -                val ab_set_M = domain_type (range_type T) |> mtype_for_set
    1.92 -                val ac_set_M = nth_range_type 2 T |> mtype_for_set
    1.93 +                val bc_set_M = domain_type T |> mtype_for_set x
    1.94 +                val ab_set_M = domain_type (range_type T) |> mtype_for_set x
    1.95 +                val ac_set_M = nth_range_type 2 T |> mtype_for_set x
    1.96                in
    1.97                  (MFun (bc_set_M, A Gen, MFun (ab_set_M, A Gen, ac_set_M)),
    1.98                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
    1.99                end
   1.100              | @{const_name finite} =>
   1.101                let
   1.102 -                val M1 = mtype_for (domain_type (domain_type T))
   1.103 +                val M1 = mtype_for (elem_type (domain_type T))
   1.104                  val a = if exists_alpha_sub_mtype M1 then Fls else Gen
   1.105                in (MFun (MFun (M1, A a, bool_M), A Gen, bool_M), accum) end
   1.106              | @{const_name prod} =>
   1.107                let
   1.108                  val x = Unsynchronized.inc max_fresh
   1.109 -                fun mtype_for_set T =
   1.110 -                  MFun (mtype_for (domain_type T), V x, bool_M)
   1.111 -                val a_set_M = mtype_for_set (domain_type T)
   1.112 +                val a_set_M = domain_type T |> mtype_for_set x
   1.113                  val b_set_M =
   1.114 -                  mtype_for_set (range_type (domain_type (range_type T)))
   1.115 -                val ab_set_M = mtype_for_set (nth_range_type 2 T)
   1.116 +                  range_type (domain_type (range_type T)) |> mtype_for_set x
   1.117 +                val ab_set_M = nth_range_type 2 T |> mtype_for_set x
   1.118                in
   1.119                  (MFun (a_set_M, A Gen, MFun (b_set_M, A Gen, ab_set_M)),
   1.120                   accum ||> add_annotation_atom_comp Neq [] (V x) (A New))
   1.121 @@ -886,7 +889,7 @@
   1.122                    val a_M = dest_MFun a_set_M |> #1
   1.123                  in (MFun (a_set_M, A Gen, a_M), accum) end
   1.124                else if s = @{const_name ord_class.less_eq} andalso
   1.125 -                      is_set_type (domain_type T) then
   1.126 +                      is_set_like_type (domain_type T) then
   1.127                  do_fragile_set_operation T accum
   1.128                else if is_sel s then
   1.129                  (mtype_for_sel mdata x, accum)