proper handling of assignment disjunctions vs. conjunctions
authorblanchet
Mon Dec 06 13:18:25 2010 +0100 (2010-12-06)
changeset 40991902ad76994d5
parent 40990 a36d4d869439
child 40992 8cacefe9851c
proper handling of assignment disjunctions vs. conjunctions
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:18:25 2010 +0100
     1.3 @@ -364,38 +364,41 @@
     1.4    | string_for_assign_clause asgs =
     1.5      space_implode " \<or> " (map string_for_assign asgs)
     1.6  
     1.7 -fun do_assign _ NONE = NONE
     1.8 -  | do_assign (x, a) (SOME asgs) =
     1.9 +fun add_assign_conjunct _ NONE = NONE
    1.10 +  | add_assign_conjunct (x, a) (SOME asgs) =
    1.11      case AList.lookup (op =) asgs x of
    1.12        SOME a' => if a = a' then SOME asgs else NONE
    1.13      | NONE => SOME ((x, a) :: asgs)
    1.14  
    1.15 -fun do_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    1.16 +fun add_assign_disjunct _ NONE = NONE
    1.17 +  | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
    1.18 +
    1.19 +fun add_annotation_atom_comp Eq [] aa1 aa2 (accum as (asgs, comps)) =
    1.20      (case (aa1, aa2) of
    1.21         (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.22       | (V x1, A a2) =>
    1.23 -       SOME asgs |> do_assign (x1, a2) |> Option.map (rpair comps)
    1.24 +       SOME asgs |> add_assign_conjunct (x1, a2) |> Option.map (rpair comps)
    1.25       | (V _, V _) => SOME (asgs, insert (op =) (aa1, aa2, Eq, []) comps)
    1.26 -     | _ => do_annotation_atom_comp Eq [] aa2 aa1 accum)
    1.27 -  | do_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    1.28 +     | _ => add_annotation_atom_comp Eq [] aa2 aa1 accum)
    1.29 +  | add_annotation_atom_comp Leq [] aa1 aa2 (accum as (asgs, comps)) =
    1.30      (case (aa1, aa2) of
    1.31         (_, A Gen) => SOME accum
    1.32       | (A Gen, A _) => NONE
    1.33       | (A a1, A a2) => if a1 = a2 then SOME accum else NONE
    1.34       | _ => SOME (asgs, insert (op =) (aa1, aa2, Leq, []) comps))
    1.35 -  | do_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    1.36 +  | add_annotation_atom_comp cmp xs aa1 aa2 (asgs, comps) =
    1.37      SOME (asgs, insert (op =) (aa1, aa2, cmp, xs) comps)
    1.38  
    1.39  fun do_mtype_comp _ _ _ _ NONE = NONE
    1.40    | do_mtype_comp _ _ MAlpha MAlpha accum = accum
    1.41    | do_mtype_comp Eq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    1.42                    (SOME accum) =
    1.43 -     accum |> do_annotation_atom_comp Eq xs aa1 aa2
    1.44 +     accum |> add_annotation_atom_comp Eq xs aa1 aa2
    1.45             |> do_mtype_comp Eq xs M11 M21 |> do_mtype_comp Eq xs M12 M22
    1.46    | do_mtype_comp Leq xs (MFun (M11, aa1, M12)) (MFun (M21, aa2, M22))
    1.47                    (SOME accum) =
    1.48      (if exists_alpha_sub_mtype M11 then
    1.49 -       accum |> do_annotation_atom_comp Leq xs aa1 aa2
    1.50 +       accum |> add_annotation_atom_comp Leq xs aa1 aa2
    1.51               |> do_mtype_comp Leq xs M21 M11
    1.52               |> (case aa2 of
    1.53                     A Gen => I
    1.54 @@ -416,11 +419,11 @@
    1.55                   [M1, M2], [])
    1.56  
    1.57  fun add_mtype_comp cmp M1 M2 ((asgs, comps, clauses) : constraint_set) =
    1.58 -    (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    1.59 -                         string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    1.60 -     case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
    1.61 -       NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.62 -     | SOME (asgs, comps) => (asgs, comps, clauses))
    1.63 +  (trace_msg (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    1.64 +                       string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    1.65 +   case do_mtype_comp cmp [] M1 M2 (SOME (asgs, comps)) of
    1.66 +     NONE => (trace_msg (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.67 +   | SOME (asgs, comps) => (asgs, comps, clauses))
    1.68  
    1.69  val add_mtypes_equal = add_mtype_comp Eq
    1.70  val add_is_sub_mtype = add_mtype_comp Leq
    1.71 @@ -429,7 +432,7 @@
    1.72    | do_notin_mtype_fv Minus _ MAlpha accum = accum
    1.73    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
    1.74    | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME (asgs, clauses)) =
    1.75 -    SOME asgs |> do_assign (x, a) |> Option.map (rpair clauses)
    1.76 +    SOME asgs |> add_assign_conjunct (x, a) |> Option.map (rpair clauses)
    1.77    | do_notin_mtype_fv Plus clause MAlpha (SOME (asgs, clauses)) =
    1.78      SOME (asgs, insert (op =) clause clauses)
    1.79    | do_notin_mtype_fv sn clause (MFun (M1, A aa, M2)) accum =
    1.80 @@ -443,13 +446,13 @@
    1.81                  I)
    1.82            |> do_notin_mtype_fv sn clause M2
    1.83    | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) accum =
    1.84 -    accum |> (case do_assign (x, Gen) (SOME clause) of
    1.85 +    accum |> (case add_assign_disjunct (x, Gen) (SOME clause) of
    1.86                  NONE => I
    1.87                | SOME clause' => do_notin_mtype_fv Plus clause' M1)
    1.88            |> do_notin_mtype_fv Minus clause M1
    1.89            |> do_notin_mtype_fv Plus clause M2
    1.90    | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) accum =
    1.91 -    accum |> (case fold (fn a => do_assign (x, a)) (* [New, Fls, Tru] FIXME *) [Fls]
    1.92 +    accum |> (case fold (fn a => add_assign_disjunct (x, a)) [New, Fls, Tru]
    1.93                          (SOME clause) of
    1.94                  NONE => I
    1.95                | SOME clause' => do_notin_mtype_fv Plus clause' M1)