fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
authorblanchet
Mon Nov 23 13:45:16 2009 +0100 (2009-11-23)
changeset 3385426a4cb3a7eae
parent 33853 348c3ea03e58
child 33855 cd8acf137c9c
child 33863 fb13147a3050
fixed a Kodkod generation exception in Nitpick, reported by a Karlsruhe user
src/HOL/Tools/Nitpick/nitpick_kodkod.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 23 13:24:32 2009 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML	Mon Nov 23 13:45:16 2009 +0100
     1.3 @@ -956,7 +956,8 @@
     1.4          (case u of
     1.5             Cst (False, _, _) => Kodkod.False
     1.6           | Cst (True, _, _) => Kodkod.True
     1.7 -         | Op1 (Not, _, _, u1) => kk_not (to_f u1)
     1.8 +         | Op1 (Not, _, _, u1) =>
     1.9 +           kk_not (to_f_with_polarity (flip_polarity polar) u1)
    1.10           | Op1 (Finite, _, _, u1) =>
    1.11             let val opt1 = is_opt_rep (rep_of u1) in
    1.12               case polar of
    1.13 @@ -968,10 +969,14 @@
    1.14               | Neg => Kodkod.True
    1.15             end
    1.16           | Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
    1.17 -         | Op2 (All, _, _, u1, u2) => kk_all (untuple to_decl u1) (to_f u2)
    1.18 -         | Op2 (Exist, _, _, u1, u2) => kk_exist (untuple to_decl u1) (to_f u2)
    1.19 -         | Op2 (Or, _, _, u1, u2) => kk_or (to_f u1) (to_f u2)
    1.20 -         | Op2 (And, _, _, u1, u2) => kk_and (to_f u1) (to_f u2)
    1.21 +         | Op2 (All, _, _, u1, u2) =>
    1.22 +           kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
    1.23 +         | Op2 (Exist, _, _, u1, u2) =>
    1.24 +           kk_exist (untuple to_decl u1) (to_f_with_polarity polar u2)
    1.25 +         | Op2 (Or, _, _, u1, u2) =>
    1.26 +           kk_or (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
    1.27 +         | Op2 (And, _, _, u1, u2) =>
    1.28 +           kk_and (to_f_with_polarity polar u1) (to_f_with_polarity polar u2)
    1.29           | Op2 (Less, T, Formula polar, u1, u2) =>
    1.30             formula_from_opt_atom polar bool_j0
    1.31                 (to_r (Op2 (Less, T, Opt bool_atom_R, u1, u2)))
    1.32 @@ -1105,9 +1110,10 @@
    1.33                to_f_with_polarity polar
    1.34                   (Op2 (Apply, T, Opt (Atom (2, offset_of_type ofs T)), u1, u2)))
    1.35           | Op3 (Let, _, _, u1, u2, u3) =>
    1.36 -           kk_formula_let [to_expr_assign u1 u2] (to_f u3)
    1.37 +           kk_formula_let [to_expr_assign u1 u2] (to_f_with_polarity polar u3)
    1.38           | Op3 (If, _, _, u1, u2, u3) =>
    1.39 -           kk_formula_if (to_f u1) (to_f u2) (to_f u3)
    1.40 +           kk_formula_if (to_f u1) (to_f_with_polarity polar u2)
    1.41 +                         (to_f_with_polarity polar u3)
    1.42           | FormulaReg (j, _, _) => Kodkod.FormulaReg j
    1.43           | _ => raise NUT ("Nitpick_Kodkod.to_f", [u]))
    1.44        | Atom (2, j0) => formula_from_atom j0 (to_r u)