# HG changeset patch # User blanchet # Date 1291638657 -3600 # Node ID 69d0d445c46af5ecd2bb63b6a302aae266659216 # Parent bcd23ddeecef6fcd0724d1785a7f7eafc878e696 fixed bug in clause handling in monotonicity code, whereby the unsound rule False | x <--> False was used to simplify constraints diff -r bcd23ddeecef -r 69d0d445c46a src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:30:38 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:30:57 2010 +0100 @@ -364,8 +364,9 @@ string_for_annotation_atom aa1 ^ " " ^ string_for_comp_op cmp ^ subscript_string_for_vars " \ " xs ^ " " ^ string_for_annotation_atom aa2 -fun string_for_assign_clause [] = "\" - | string_for_assign_clause asgs = +fun string_for_assign_clause NONE = "\" + | string_for_assign_clause (SOME []) = "\" + | string_for_assign_clause (SOME asgs) = space_implode " \ " (map string_for_assign_literal asgs) fun add_assign_literal (x, (sn, a)) clauses = @@ -380,7 +381,8 @@ fun add_assign_disjunct _ NONE = NONE | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs) -val add_assign_clause = insert (op =) +fun add_assign_clause NONE = I + | add_assign_clause (SOME clause) = insert (op =) clause fun annotation_comp Eq a1 a2 = (a1 = a2) | annotation_comp Neq a1 a2 = (a1 <> a2) @@ -506,22 +508,22 @@ fun prop_for_bool b = if b then PL.True else PL.False fun prop_for_bool_var_equality (v1, v2) = - PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)), - PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2)) + PL.SAnd (PL.SOr (PL.BoolVar v1, PL.SNot (PL.BoolVar v2)), + PL.SOr (PL.SNot (PL.BoolVar v1), PL.BoolVar v2)) fun prop_for_assign (x, a) = let val (b1, b2) = bools_from_annotation a in - PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not, - PL.BoolVar (snd_var x) |> not b2 ? PL.Not) + PL.SAnd (PL.BoolVar (fst_var x) |> not b1 ? PL.SNot, + PL.BoolVar (snd_var x) |> not b2 ? PL.SNot) end fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a) - | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a)) + | prop_for_assign_literal (x, (Minus, a)) = PL.SNot (prop_for_assign (x, a)) fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a') | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a)) fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2) | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1) | prop_for_atom_equality (V x1, V x2) = - PL.And (prop_for_bool_var_equality (pairself fst_var (x1, x2)), - prop_for_bool_var_equality (pairself snd_var (x1, x2))) + PL.SAnd (prop_for_bool_var_equality (pairself fst_var (x1, x2)), + prop_for_bool_var_equality (pairself snd_var (x1, x2))) val prop_for_assign_clause = PL.exists o map prop_for_assign_literal fun prop_for_exists_var_assign_literal xs a = PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs) @@ -529,7 +531,7 @@ PL.SAnd (prop_for_comp (aa1, aa2, Leq, []), prop_for_comp (aa2, aa1, Leq, [])) | prop_for_comp (aa1, aa2, Neq, []) = - PL.Not (prop_for_comp (aa1, aa2, Eq, [])) + PL.SNot (prop_for_comp (aa1, aa2, Eq, [])) | prop_for_comp (aa1, aa2, Leq, []) = PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen)) | prop_for_comp (aa1, aa2, cmp, xs) = @@ -560,7 +562,7 @@ trace_msg (fn () => "*** Problem (calculus M" ^ string_of_int calculus ^ "):\n" ^ cat_lines (map string_for_comp comps @ - map string_for_assign_clause clauses)) + map (string_for_assign_clause o SOME) clauses)) fun print_solution asgs = trace_msg (fn () => "*** Solution:\n" ^ @@ -684,22 +686,24 @@ [(aa1, (Eq, Fls)), (aa2, (Neq, Gen)), (res_aa, (Eq, Gen))], [(aa1, (Eq, Fls)), (aa2, (Neq, New)), (res_aa, (Eq, Gen))]] -fun annotation_literal_from_quasi_literal (aa, (cmp, a)) = - case aa of - A a' => if annotation_comp cmp a' a then NONE - else (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ()) - | V x => SOME (x, (sign_for_comp_op cmp, a)) +fun add_annotation_clause_from_quasi_clause _ NONE = NONE + | add_annotation_clause_from_quasi_clause [] accum = accum + | add_annotation_clause_from_quasi_clause ((aa, (cmp, a)) :: rest) accum = + case aa of + A a' => if annotation_comp cmp a' a then NONE + else add_annotation_clause_from_quasi_clause rest accum + | V x => add_annotation_clause_from_quasi_clause rest accum + |> Option.map (cons (x, (sign_for_comp_op cmp, a))) -val assign_clause_from_quasi_clause = - map_filter annotation_literal_from_quasi_literal -val add_quasi_clause = assign_clause_from_quasi_clause #> add_assign_clause +fun assign_clause_from_quasi_clause clause = + add_annotation_clause_from_quasi_clause clause (SOME []) fun add_connective_var conn mk_quasi_clauses res_aa aa1 aa2 = (trace_msg (fn () => "*** Add " ^ string_for_annotation_atom res_aa ^ " = " ^ string_for_annotation_atom aa1 ^ " " ^ conn ^ " " ^ string_for_annotation_atom aa2); - fold add_quasi_clause (mk_quasi_clauses res_aa aa1 aa2)) - + fold (add_assign_clause o assign_clause_from_quasi_clause) + (mk_quasi_clauses res_aa aa1 aa2)) fun add_connective_frames conn mk_quasi_clauses res_frame frame1 frame2 = fold I (map3 (fn (_, res_aa) => fn (_, aa1) => fn (_, aa2) => add_connective_var conn mk_quasi_clauses res_aa aa1 aa2) @@ -729,11 +733,17 @@ | add_annotation_atom_comp_alt cmp (V x) aa1 aa2 = add_annotation_atom_comp cmp [x] aa1 aa2 -fun add_arg_order1 ((_, aa), (_, prev_aa)) = +fun add_arg_order1 ((_, aa), (_, prev_aa)) = I add_annotation_atom_comp_alt Neq prev_aa (A Gen) aa -fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = - add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa - ##> add_quasi_clause [(arg_aa, (Neq, Gen)), (res_aa, (Eq, Gen))] +fun add_app1 fun_aa ((_, res_aa), (_, arg_aa)) = I + let + val clause = [(arg_aa, (Eq, New)), (res_aa, (Eq, Gen))] + |> assign_clause_from_quasi_clause + in + trace_msg (fn () => "*** Add " ^ string_for_assign_clause clause); + apsnd (add_assign_clause clause) + #> add_annotation_atom_comp_alt Leq arg_aa fun_aa res_aa + end fun add_app _ [] [] = I | add_app fun_aa res_frame arg_frame = add_comp_frame (A New) Leq arg_frame