src/HOL/Tools/Nitpick/nitpick_tests.ML
changeset 33192 08a39a957ed7
child 33232 f93390060bbe
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML	Thu Oct 22 14:51:47 2009 +0200
     1.3 @@ -0,0 +1,334 @@
     1.4 +(*  Title:      HOL/Nitpick/Tools/nitpick_tests.ML
     1.5 +    Author:     Jasmin Blanchette, TU Muenchen
     1.6 +    Copyright   2008, 2009
     1.7 +
     1.8 +Unit tests for Nitpick.
     1.9 +*)
    1.10 +
    1.11 +signature NITPICK_TESTS =
    1.12 +sig
    1.13 +  val run_all_tests : unit -> unit
    1.14 +end
    1.15 +
    1.16 +structure NitpickTests =
    1.17 +struct
    1.18 +
    1.19 +open NitpickUtil
    1.20 +open NitpickPeephole
    1.21 +open NitpickRep
    1.22 +open NitpickNut
    1.23 +open NitpickKodkod
    1.24 +open Nitpick
    1.25 +
    1.26 +val settings =
    1.27 +  [("solver", "\"zChaff\""),
    1.28 +   ("skolem_depth", "-1")]
    1.29 +
    1.30 +fun cast_to_rep R u = Op1 (Cast, type_of u, R, u)
    1.31 +
    1.32 +val unit_T = @{typ unit}
    1.33 +val dummy_T = @{typ 'a}
    1.34 +
    1.35 +val unity = Cst (Unity, unit_T, Unit)
    1.36 +val atom1_v1 = FreeName ("atom1_v1", dummy_T, Atom (1, 0))
    1.37 +val atom2_v1 = FreeName ("atom2_v1", dummy_T, Atom (2, 0))
    1.38 +val atom6_v1 = FreeName ("atom6_v1", dummy_T, Atom (6, 0))
    1.39 +val atom16_v1 = FreeName ("atom16_v1", dummy_T, Atom (16, 0))
    1.40 +val atom24_v1 = FreeName ("atom24_v1", dummy_T, Atom (24, 0))
    1.41 +val atom36_v1 = FreeName ("atom36_v1", dummy_T, Atom (36, 0))
    1.42 +val atom81_v1 = FreeName ("atom81_v1", dummy_T, Atom (81, 0))
    1.43 +val struct_atom1_atom1_v1 =
    1.44 +  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Atom (1, 0)])
    1.45 +val struct_atom1_unit_v1 =
    1.46 +  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Atom (1, 0), Unit])
    1.47 +val struct_unit_atom1_v1 =
    1.48 +  FreeName ("struct_atom1_atom1_v1", dummy_T, Struct [Unit, Atom (1, 0)])
    1.49 +
    1.50 +(*
    1.51 +              Formula    Unit   Atom    Struct    Vect    Func
    1.52 +    Formula      X       N/A     X        X       N/A     N/A
    1.53 +    Unit        N/A      N/A    N/A      N/A      N/A     N/A
    1.54 +    Atom         X       N/A     X        X        X       X
    1.55 +    Struct      N/A      N/A     X        X       N/A     N/A
    1.56 +    Vect        N/A      N/A     X       N/A       X       X
    1.57 +    Func        N/A      N/A     X       N/A       X       X
    1.58 +*)
    1.59 +
    1.60 +val tests =
    1.61 +  [("rep_conversion_formula_formula",
    1.62 +    Op2 (Eq, bool_T, Formula Neut,
    1.63 +         cast_to_rep (Formula Neut)
    1.64 +                     (cast_to_rep (Formula Neut) atom2_v1), atom2_v1)),
    1.65 +   ("rep_conversion_atom_atom",
    1.66 +    Op2 (Eq, bool_T, Formula Neut,
    1.67 +         cast_to_rep (Atom (16, 0)) (cast_to_rep (Atom (16, 0)) atom16_v1),
    1.68 +         atom16_v1)),
    1.69 +   ("rep_conversion_struct_struct_1",
    1.70 +    Op2 (Eq, bool_T, Formula Neut,
    1.71 +         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
    1.72 +             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
    1.73 +         atom24_v1)),
    1.74 +   ("rep_conversion_struct_struct_2",
    1.75 +    Op2 (Eq, bool_T, Formula Neut,
    1.76 +         cast_to_rep (Struct [Atom (4, 0), Struct [Atom (2, 0), Atom (3, 0)]])
    1.77 +             (cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)]) atom24_v1),
    1.78 +         atom24_v1)),
    1.79 +   ("rep_conversion_struct_struct_3",
    1.80 +    Op2 (Eq, bool_T, Formula Neut,
    1.81 +         cast_to_rep (Struct [Atom (4, 0), Atom (6, 0)])
    1.82 +             (cast_to_rep (Struct [Atom (4, 0),
    1.83 +                                   Struct [Atom (2, 0), Atom (3, 0)]])
    1.84 +                          atom24_v1),
    1.85 +         atom24_v1)),
    1.86 +   ("rep_conversion_struct_struct_4",
    1.87 +    Op2 (Eq, bool_T, Formula Neut,
    1.88 +         cast_to_rep (Struct [Atom (24, 0), Unit])
    1.89 +             (cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)]) atom24_v1),
    1.90 +         atom24_v1)),
    1.91 +   ("rep_conversion_struct_struct_5",
    1.92 +    Op2 (Eq, bool_T, Formula Neut,
    1.93 +         cast_to_rep (Struct [Atom (24, 0), Atom (1, 0)])
    1.94 +             (cast_to_rep (Struct [Atom (24, 0), Unit]) atom24_v1),
    1.95 +         atom24_v1)),
    1.96 +   ("rep_conversion_struct_struct_6",
    1.97 +    Op2 (Eq, bool_T, Formula Neut,
    1.98 +         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)])
    1.99 +             (cast_to_rep (Struct [Atom (1, 0), Unit])
   1.100 +                 (cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1)),
   1.101 +         atom1_v1)),
   1.102 +   ("rep_conversion_vect_vect_1",
   1.103 +    Op2 (Eq, bool_T, Formula Neut,
   1.104 +         cast_to_rep (Atom (16, 0))
   1.105 +             (cast_to_rep (Vect (2, Atom (4, 0)))
   1.106 +                  (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
   1.107 +                               atom16_v1)),
   1.108 +         atom16_v1)),
   1.109 +   ("rep_conversion_vect_vect_2",
   1.110 +    Op2 (Eq, bool_T, Formula Neut,
   1.111 +         cast_to_rep (Atom (16, 0))
   1.112 +             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (2, 0)]))
   1.113 +                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
   1.114 +         atom16_v1)),
   1.115 +   ("rep_conversion_vect_vect_3",
   1.116 +    Op2 (Eq, bool_T, Formula Neut,
   1.117 +         cast_to_rep (Atom (16, 0))
   1.118 +             (cast_to_rep (Vect (2, Atom (4, 0)))
   1.119 +                  (cast_to_rep (Vect (2, Vect (2, Atom (2, 0)))) atom16_v1)),
   1.120 +         atom16_v1)),
   1.121 +   ("rep_conversion_vect_vect_4",
   1.122 +    Op2 (Eq, bool_T, Formula Neut,
   1.123 +         cast_to_rep (Atom (16, 0))
   1.124 +             (cast_to_rep (Vect (2, Vect (2, Atom (2, 0))))
   1.125 +                  (cast_to_rep (Vect (2, Atom (4, 0))) atom16_v1)),
   1.126 +         atom16_v1)),
   1.127 +   ("rep_conversion_func_func_1",
   1.128 +    Op2 (Eq, bool_T, Formula Neut,
   1.129 +         cast_to_rep (Atom (36, 0))
   1.130 +             (cast_to_rep (Func (Atom (2, 0),
   1.131 +                                 Struct [Atom (2, 0), Atom (3, 0)]))
   1.132 +                  (cast_to_rep (Func (Atom (2, 0), Atom (6, 0))) atom36_v1)),
   1.133 +         atom36_v1)),
   1.134 +   ("rep_conversion_func_func_2",
   1.135 +    Op2 (Eq, bool_T, Formula Neut,
   1.136 +         cast_to_rep (Atom (36, 0))
   1.137 +             (cast_to_rep (Func (Atom (2, 0), Atom (6, 0)))
   1.138 +                  (cast_to_rep (Func (Atom (2, 0),
   1.139 +                                Struct [Atom (2, 0), Atom (3, 0)]))
   1.140 +                       atom36_v1)),
   1.141 +         atom36_v1)),
   1.142 +   ("rep_conversion_func_func_3",
   1.143 +    Op2 (Eq, bool_T, Formula Neut,
   1.144 +         cast_to_rep (Atom (36, 0))
   1.145 +             (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
   1.146 +                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
   1.147 +         atom36_v1)),
   1.148 +   ("rep_conversion_func_func_4",
   1.149 +    Op2 (Eq, bool_T, Formula Neut,
   1.150 +         cast_to_rep (Atom (36, 0))
   1.151 +             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
   1.152 +                  (cast_to_rep (Func (Unit, Struct [Atom (6, 0), Atom (6, 0)]))
   1.153 +                       atom36_v1)),
   1.154 +         atom36_v1)),
   1.155 +   ("rep_conversion_func_func_5",
   1.156 +    Op2 (Eq, bool_T, Formula Neut,
   1.157 +         cast_to_rep (Atom (36, 0))
   1.158 +             (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
   1.159 +                  (cast_to_rep (Func (Atom (1, 0), Atom (36, 0))) atom36_v1)),
   1.160 +         atom36_v1)),
   1.161 +   ("rep_conversion_func_func_6",
   1.162 +    Op2 (Eq, bool_T, Formula Neut,
   1.163 +         cast_to_rep (Atom (36, 0))
   1.164 +             (cast_to_rep (Func (Atom (1, 0), Atom (36, 0)))
   1.165 +                  (cast_to_rep (Func (Unit, Vect (2, Atom (6, 0))))
   1.166 +                       atom36_v1)),
   1.167 +         atom36_v1)),
   1.168 +   ("rep_conversion_func_func_7",
   1.169 +    Op2 (Eq, bool_T, Formula Neut,
   1.170 +         cast_to_rep (Atom (2, 0))
   1.171 +             (cast_to_rep (Func (Unit, Atom (2, 0)))
   1.172 +                  (cast_to_rep (Func (Atom (1, 0), Formula Neut)) atom2_v1)),
   1.173 +         atom2_v1)),
   1.174 +   ("rep_conversion_func_func_8",
   1.175 +    Op2 (Eq, bool_T, Formula Neut,
   1.176 +         cast_to_rep (Atom (2, 0))
   1.177 +             (cast_to_rep (Func (Atom (1, 0), Formula Neut))
   1.178 +                  (cast_to_rep (Func (Unit, Atom (2, 0))) atom2_v1)),
   1.179 +         atom2_v1)),
   1.180 +   ("rep_conversion_atom_formula_atom",
   1.181 +    Op2 (Eq, bool_T, Formula Neut,
   1.182 +         cast_to_rep (Atom (2, 0)) (cast_to_rep (Formula Neut) atom2_v1),
   1.183 +         atom2_v1)),
   1.184 +   ("rep_conversion_unit_atom",
   1.185 +    Op2 (Eq, bool_T, Formula Neut, cast_to_rep (Atom (1, 0)) unity, unity)),
   1.186 +   ("rep_conversion_atom_struct_atom1",
   1.187 +    Op2 (Eq, bool_T, Formula Neut,
   1.188 +         cast_to_rep (Atom (6, 0))
   1.189 +                     (cast_to_rep (Struct [Atom (3, 0), Atom (2, 0)]) atom6_v1),
   1.190 +         atom6_v1)),
   1.191 +   ("rep_conversion_atom_struct_atom_2",
   1.192 +    Op2 (Eq, bool_T, Formula Neut,
   1.193 +         cast_to_rep (Atom (24, 0))
   1.194 +             (cast_to_rep (Struct [Struct [Atom (3, 0), Atom (4, 0)],
   1.195 +                                   Atom (2, 0)]) atom24_v1),
   1.196 +         atom24_v1)),
   1.197 +   ("rep_conversion_atom_struct_atom_3",
   1.198 +    Op2 (Eq, bool_T, Formula Neut,
   1.199 +         cast_to_rep (Atom (6, 0))
   1.200 +                     (cast_to_rep (Struct [Atom (6, 0), Unit]) atom6_v1),
   1.201 +         atom6_v1)),
   1.202 +   ("rep_conversion_atom_struct_atom_4",
   1.203 +    Op2 (Eq, bool_T, Formula Neut,
   1.204 +         cast_to_rep (Atom (6, 0))
   1.205 +             (cast_to_rep (Struct [Struct [Atom (3, 0), Unit], Atom (2, 0)]) 
   1.206 +             atom6_v1),
   1.207 +         atom6_v1)),
   1.208 +   ("rep_conversion_atom_vect_func_atom_1",
   1.209 +    Op2 (Eq, bool_T, Formula Neut,
   1.210 +         cast_to_rep (Atom (16, 0))
   1.211 +             (cast_to_rep (Vect (4, Atom (2, 0)))
   1.212 +                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
   1.213 +         atom16_v1)),
   1.214 +   ("rep_conversion_atom_vect_func_atom_2",
   1.215 +    Op2 (Eq, bool_T, Formula Neut,
   1.216 +         cast_to_rep (Atom (16, 0))
   1.217 +             (cast_to_rep (Vect (4, Atom (2, 0)))
   1.218 +                  (cast_to_rep (Func (Atom (4, 0), Atom (2, 0))) atom16_v1)),
   1.219 +         atom16_v1)),
   1.220 +   ("rep_conversion_atom_vect_func_atom_3",
   1.221 +    Op2 (Eq, bool_T, Formula Neut,
   1.222 +         cast_to_rep (Atom (16, 0))
   1.223 +             (cast_to_rep (Vect (4, Atom (2, 0)))
   1.224 +                  (cast_to_rep (Func (Atom (4, 0), Formula Neut)) atom16_v1)),
   1.225 +         atom16_v1)),
   1.226 +   ("rep_conversion_atom_vect_func_atom_4",
   1.227 +    Op2 (Eq, bool_T, Formula Neut,
   1.228 +         cast_to_rep (Atom (16, 0))
   1.229 +             (cast_to_rep (Vect (1, Atom (16, 0)))
   1.230 +                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
   1.231 +         atom16_v1)),
   1.232 +   ("rep_conversion_atom_vect_func_atom_5",
   1.233 +    Op2 (Eq, bool_T, Formula Neut,
   1.234 +         cast_to_rep (Atom (16, 0))
   1.235 +             (cast_to_rep (Vect (1, Atom (16, 0)))
   1.236 +                  (cast_to_rep (Func (Unit, Atom (16, 0))) atom16_v1)),
   1.237 +         atom16_v1)),
   1.238 +   ("rep_conversion_atom_func_vect_atom_1",
   1.239 +    Op2 (Eq, bool_T, Formula Neut,
   1.240 +         cast_to_rep (Atom (16, 0))
   1.241 +             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
   1.242 +                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
   1.243 +         atom16_v1)),
   1.244 +   ("rep_conversion_atom_func_vect_atom_2",
   1.245 +    Op2 (Eq, bool_T, Formula Neut,
   1.246 +         cast_to_rep (Atom (16, 0))
   1.247 +             (cast_to_rep (Func (Atom (4, 0), Atom (2, 0)))
   1.248 +                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
   1.249 +         atom16_v1)),
   1.250 +   ("rep_conversion_atom_func_vect_atom_3",
   1.251 +    Op2 (Eq, bool_T, Formula Neut,
   1.252 +         cast_to_rep (Atom (16, 0))
   1.253 +             (cast_to_rep (Func (Atom (4, 0), Formula Neut))
   1.254 +                  (cast_to_rep (Vect (4, Atom (2, 0))) atom16_v1)),
   1.255 +         atom16_v1)),
   1.256 +   ("rep_conversion_atom_func_vect_atom_4",
   1.257 +    Op2 (Eq, bool_T, Formula Neut,
   1.258 +         cast_to_rep (Atom (16, 0))
   1.259 +             (cast_to_rep (Func (Unit, Atom (16, 0)))
   1.260 +                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
   1.261 +         atom16_v1)),
   1.262 +   ("rep_conversion_atom_func_vect_atom_5",
   1.263 +    Op2 (Eq, bool_T, Formula Neut,
   1.264 +         cast_to_rep (Atom (16, 0))
   1.265 +             (cast_to_rep (Func (Atom (1, 0), Atom (16, 0)))
   1.266 +                  (cast_to_rep (Vect (1, Atom (16, 0))) atom16_v1)),
   1.267 +         atom16_v1)),
   1.268 +   ("rep_conversion_atom_vect_atom",
   1.269 +    Op2 (Eq, bool_T, Formula Neut,
   1.270 +         cast_to_rep (Atom (36, 0))
   1.271 +             (cast_to_rep (Vect (2, Struct [Atom (2, 0), Atom (3, 0)]))
   1.272 +                          atom36_v1),
   1.273 +         atom36_v1)),
   1.274 +   ("rep_conversion_atom_func_atom",
   1.275 +    Op2 (Eq, bool_T, Formula Neut,
   1.276 +         cast_to_rep (Atom (36, 0))
   1.277 +             (cast_to_rep (Func (Atom (2, 0),
   1.278 +                           Struct [Atom (2, 0), Atom (3, 0)])) atom36_v1),
   1.279 +         atom36_v1)),
   1.280 +   ("rep_conversion_struct_atom1_1",
   1.281 +    Op2 (Eq, bool_T, Formula Neut,
   1.282 +         cast_to_rep (Struct [Atom (1, 0), Atom (1, 0)]) atom1_v1,
   1.283 +                      struct_atom1_atom1_v1)),
   1.284 +   ("rep_conversion_struct_atom1_2",
   1.285 +    Op2 (Eq, bool_T, Formula Neut,
   1.286 +         cast_to_rep (Struct [Atom (1, 0), Unit]) atom1_v1,
   1.287 +                      struct_atom1_unit_v1)),
   1.288 +   ("rep_conversion_struct_atom1_3",
   1.289 +    Op2 (Eq, bool_T, Formula Neut,
   1.290 +         cast_to_rep (Struct [Unit, Atom (1, 0)]) atom1_v1,
   1.291 +                      struct_unit_atom1_v1))
   1.292 +(*
   1.293 +   ("rep_conversion_struct_formula_struct_1",
   1.294 +    Op2 (Eq, bool_T, Formula Neut,
   1.295 +         cast_to_rep (Struct [Atom (2, 0), Unit])
   1.296 +             (cast_to_rep (Formula Neut) struct_atom_2_unit_v1),
   1.297 +         struct_atom_2_unit_v1))
   1.298 +*)
   1.299 +  ]
   1.300 +
   1.301 +fun problem_for_nut ctxt name u =
   1.302 +  let
   1.303 +    val debug = false
   1.304 +    val peephole_optim = true
   1.305 +    val nat_card = 4
   1.306 +    val int_card = 9
   1.307 +    val j0 = 0
   1.308 +    val constrs = kodkod_constrs peephole_optim nat_card int_card j0
   1.309 +    val (free_rels, pool, table) =
   1.310 +      rename_free_vars (fst (add_free_and_const_names u ([], []))) initial_pool
   1.311 +                       NameTable.empty
   1.312 +    val u = Op1 (Not, type_of u, rep_of u, u)
   1.313 +            |> rename_vars_in_nut pool table
   1.314 +    val formula = kodkod_formula_from_nut Typtab.empty false constrs u
   1.315 +    val bounds = map (bound_for_plain_rel ctxt debug) free_rels
   1.316 +    val univ_card = univ_card nat_card int_card j0 bounds formula
   1.317 +    val declarative_axioms = map (declarative_axiom_for_plain_rel constrs)
   1.318 +                                 free_rels
   1.319 +    val formula = fold_rev s_and declarative_axioms formula
   1.320 +  in
   1.321 +    {comment = name, settings = settings, univ_card = univ_card,
   1.322 +     tuple_assigns = [], bounds = bounds, int_bounds = [], expr_assigns = [],
   1.323 +     formula = formula}
   1.324 +  end
   1.325 +
   1.326 +(* string -> unit *)
   1.327 +fun run_test name =
   1.328 +  case Kodkod.solve_any_problem true NONE 0 1
   1.329 +           [problem_for_nut @{context} name
   1.330 +                            (the (AList.lookup (op =) tests name))] of
   1.331 +    Kodkod.Normal ([], _) => ()
   1.332 +  | _ => warning ("Test " ^ quote name ^ " failed")
   1.333 +
   1.334 +(* unit -> unit *)
   1.335 +fun run_all_tests () = List.app run_test (map fst tests)
   1.336 +
   1.337 +end;