# HG changeset patch
# User blanchet
# Date 1291637905 -3600
# Node ID 902ad76994d54a7860e60079c0c847567f3098ea
# Parent  a36d4d869439410d5900285382da916e8ef5bfcd
proper handling of assignment disjunctions vs. conjunctions

diff -r a36d4d869439 -r 902ad76994d5 src/HOL/Tools/Nitpick/nitpick_mono.ML
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
@@ -364,38 +364,41 @@
   | string_for_assign_clause asgs =
     space_implode " \<or> " (map string_for_assign asgs)
 
-fun do_assign _ NONE = NONE
-  | do_assign (x, a) (SOME asgs) =
+fun add_assign_conjunct _ NONE = NONE
+  | add_assign_conjunct (x, a) (SOME asgs) =
     case AList.lookup (op =) asgs x of
       SOME a' => if a = a' then SOME asgs else NONE
     | NONE => SOME ((x, a) :: asgs)
 
-fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
+fun add_assign_disjunct _ NONE = NONE
+  | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
+
+fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
     (case (aa1, aa2) of
        (A a1, A a2) => if a1 = a2 then SOME accum else NONE
      | (V x1, A a2) =>
-       SOME asgs |> do_assign (x1, a2) |> Option.map (rpair comps)
+       SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
      | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
-     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
-  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
+     | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum)
+  | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
     (case (aa1, aa2) of
        (_, A Gen) => SOME accum
      | (A Gen, A _) => NONE
      | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
      | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
-  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
+  | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
     SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
 
 fun do_mtype_comp _ _ _ _ NONE = NONE
   | do_mtype_comp _ _ MAlpha MAlpha accum = accum
   | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
                   (SOME accum) =
-     accum |> do_annotation_atom_comp Eq xs aa1 aa2
+     accum |> add_annotation_atom_comp Eq xs aa1 aa2
            |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
   | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
                   (SOME accum) =
     (if exists_alpha_sub_mtype M11 then
-       accum |> do_annotation_atom_comp Leq xs aa1 aa2
+       accum |> add_annotation_atom_comp Leq xs aa1 aa2
              |> do_mtype_comp Leq xs M21 M11
              |> (case aa2 of
                    A Gen => I
@@ -416,11 +419,11 @@
                  [M1, M2], [])
 
 fun add_mtype_comp cmp M1 M2 ((asgs, comps, clauses) : constraint_set) =
-    (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
-                         string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
-     case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
-       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
-     | SOME (asgs, comps) => (asgs, comps, clauses))
+  (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
+                       string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
+   case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
+     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
+   | SOME (asgs, comps) => (asgs, comps, clauses))
 
 val add_mtypes_equal = add_mtype_comp Eq
 val add_is_sub_mtype = add_mtype_comp Leq
@@ -429,7 +432,7 @@
   | do_notin_mtype_fv Minus _ MAlpha accum = accum
   | do_notin_mtype_fv Plus [] MAlpha _ = NONE
   | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, clauses)) =
-    SOME asgs |> do_assign (x, a) |> Option.map (rpair clauses)
+    SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
   | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
     SOME (asgs, insert (op =) clause clauses)
   | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum =
@@ -443,13 +446,13 @@
                 I)
           |> do_notin_mtype_fv sn clause M2
   | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) accum =
-    accum |> (case do_assign (x, Gen) (SOME clause) of
+    accum |> (case add_assign_disjunct (x, Gen) (SOME clause) of
                 NONE => I
               | SOME clause' => do_notin_mtype_fv Plus clause' M1)
           |> do_notin_mtype_fv Minus clause M1
           |> do_notin_mtype_fv Plus clause M2
   | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
-    accum |> (case fold (fn a => do_assign (x, a)) (* [New, Fls, Tru] FIXME *) [Fls]
+    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru]
                         (SOME clause) of
                 NONE => I
               | SOME clause' => do_notin_mtype_fv Plus clause' M1)