src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 40996 63112be4a469
parent 40995 3cae30b60577
child 40997 67e11a73532a
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:26:27 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:29:23 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  datatype annotation = Gen | New | Fls | Tru
     1.5  datatype annotation_atom = A of annotation | V of var
     1.6  
     1.7 -type assign_literal = var * annotation
     1.8 +type assign_literal = var * (sign * annotation)
     1.9  
    1.10  datatype mtyp =
    1.11    MAlpha |
    1.12 @@ -82,8 +82,9 @@
    1.13  fun string_for_annotation_atom (A a) = string_for_annotation a
    1.14    | string_for_annotation_atom (V x) = string_for_var x
    1.15  
    1.16 -fun string_for_assign_literal (x, a) =
    1.17 -  string_for_var x ^ " = " ^ string_for_annotation a
    1.18 +fun string_for_assign_literal (x, (sn, a)) =
    1.19 +  string_for_var x ^ (case sn of Plus => " = " | Minus => " \<noteq> ") ^
    1.20 +  string_for_annotation a
    1.21  
    1.22  val bool_M = MType (@{type_name bool}, [])
    1.23  val dummy_M = MType (nitpick_prefix ^ "dummy", [])
    1.24 @@ -346,7 +347,7 @@
    1.25        | aux (MRec z) = MRec z
    1.26    in aux end
    1.27  
    1.28 -datatype comp_op = Eq | Leq
    1.29 +datatype comp_op = Eq | Neq | Leq
    1.30  
    1.31  type comp = annotation_atom * annotation_atom * comp_op * var list
    1.32  type assign_clause = assign_literal list
    1.33 @@ -354,6 +355,7 @@
    1.34  type constraint_set = comp list * assign_clause list
    1.35  
    1.36  fun string_for_comp_op Eq = "="
    1.37 +  | string_for_comp_op Neq = "\<noteq>"
    1.38    | string_for_comp_op Leq = "\<le>"
    1.39  
    1.40  fun string_for_comp (aa1, aa2, cmp, xs) =
    1.41 @@ -364,28 +366,39 @@
    1.42    | string_for_assign_clause asgs =
    1.43      space_implode " \<or> " (map string_for_assign_literal asgs)
    1.44  
    1.45 -fun add_assign_literal (x, a) clauses =
    1.46 -  if exists (fn [(x', a')] => x = x' andalso a <> a' | _ => false) clauses then
    1.47 +fun add_assign_literal (x, (sn, a)) clauses =
    1.48 +  if exists (fn [(x', (sn', a'))] =>
    1.49 +                x = x' andalso ((sn = sn' andalso a <> a') orelse
    1.50 +                                (sn <> sn' andalso a = a'))
    1.51 +              | _ => false) clauses then
    1.52      NONE
    1.53    else
    1.54 -    SOME ([(x, a)] :: clauses)fun add_assign_conjunct _ NONE = NONE
    1.55 +    SOME ([(x, a)] :: clauses)
    1.56  
    1.57  fun add_assign_disjunct _ NONE = NONE
    1.58    | add_assign_disjunct asg (SOME asgs) = SOME (insert (op =) asg asgs)
    1.59  
    1.60 -fun do_annotation_atom_comp Eq [] aa1 aa2 (cset as (comps, clauses)) =
    1.61 +fun annotation_comp Eq a1 a2 = (a1 = a2)
    1.62 +  | annotation_comp Neq a1 a2 = (a1 <> a2)
    1.63 +  | annotation_comp Leq a1 a2 = (a1 = a2 orelse a2 = Gen)
    1.64 +
    1.65 +fun comp_op_sign Eq = Plus
    1.66 +  | comp_op_sign Neq = Minus
    1.67 +  | comp_op_sign Leq =
    1.68 +    raise BAD ("Nitpick_Mono.comp_op_sign", "unexpected \"Leq\"")
    1.69 +
    1.70 +fun do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
    1.71      (case (aa1, aa2) of
    1.72 -       (A a1, A a2) => if a1 = a2 then SOME cset else NONE
    1.73 +       (A a1, A a2) => if annotation_comp Leq a1 a2 then SOME cset else NONE
    1.74 +     | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses))
    1.75 +  | do_annotation_atom_comp cmp [] aa1 aa2 (cset as (comps, clauses)) =
    1.76 +    (case (aa1, aa2) of
    1.77 +       (A a1, A a2) => if annotation_comp cmp a1 a2 then SOME cset else NONE
    1.78       | (V x1, A a2) =>
    1.79 -       clauses |> add_assign_literal (x1, a2) |> Option.map (pair comps)
    1.80 -     | (V _, V _) => SOME (insert (op =) (aa1, aa2, Eq, []) comps, clauses)
    1.81 -     | _ => do_annotation_atom_comp Eq [] aa2 aa1 cset)
    1.82 -  | do_annotation_atom_comp Leq [] aa1 aa2 (cset as (comps, clauses)) =
    1.83 -    (case (aa1, aa2) of
    1.84 -       (_, A Gen) => SOME cset
    1.85 -     | (A Gen, A _) => NONE
    1.86 -     | (A a1, A a2) => if a1 = a2 then SOME cset else NONE
    1.87 -     | _ => SOME (insert (op =) (aa1, aa2, Leq, []) comps, clauses))
    1.88 +       clauses |> add_assign_literal (x1, (comp_op_sign cmp, a2))
    1.89 +               |> Option.map (pair comps)
    1.90 +     | (A _, V _) => do_annotation_atom_comp cmp [] aa2 aa1 cset
    1.91 +     | (V _, V _) => SOME (insert (op =) (aa1, aa2, cmp, []) comps, clauses))
    1.92    | do_annotation_atom_comp cmp xs aa1 aa2 (comps, clauses) =
    1.93      SOME (insert (op =) (aa1, aa2, cmp, xs) comps, clauses)
    1.94  
    1.95 @@ -440,8 +453,8 @@
    1.96  fun do_notin_mtype_fv _ _ _ NONE = NONE
    1.97    | do_notin_mtype_fv Minus _ MAlpha cset = cset
    1.98    | do_notin_mtype_fv Plus [] MAlpha _ = NONE
    1.99 -  | do_notin_mtype_fv Plus [(x, a)] MAlpha (SOME clauses) =
   1.100 -    clauses |> add_assign_literal (x, a)
   1.101 +  | do_notin_mtype_fv Plus [asg] MAlpha (SOME clauses) =
   1.102 +    clauses |> add_assign_literal asg
   1.103    | do_notin_mtype_fv Plus clause MAlpha (SOME clauses) =
   1.104      SOME (insert (op =) clause clauses)
   1.105    | do_notin_mtype_fv sn clause (MFun (M1, A a, M2)) cset =
   1.106 @@ -451,13 +464,13 @@
   1.107               else I)
   1.108           |> do_notin_mtype_fv sn clause M2
   1.109    | do_notin_mtype_fv Plus clause (MFun (M1, V x, M2)) cset =
   1.110 -    cset |> (case add_assign_disjunct (x, Gen) (SOME clause) of
   1.111 +    cset |> (case add_assign_disjunct (x, (Plus, Gen)) (SOME clause) of
   1.112                 NONE => I
   1.113               | SOME clause' => do_notin_mtype_fv Plus clause' M1)
   1.114           |> do_notin_mtype_fv Minus clause M1
   1.115           |> do_notin_mtype_fv Plus clause M2
   1.116    | do_notin_mtype_fv Minus clause (MFun (M1, V x, M2)) cset =
   1.117 -    cset |> (case fold (fn a => add_assign_disjunct (x, a)) [Fls, Tru]
   1.118 +    cset |> (case fold (fn a => add_assign_disjunct (x, (Plus, a))) [Fls, Tru]
   1.119                         (SOME clause) of
   1.120                 NONE => I
   1.121               | SOME clause' => do_notin_mtype_fv Plus clause' M1)
   1.122 @@ -495,13 +508,15 @@
   1.123  fun prop_for_bool_var_equality (v1, v2) =
   1.124    PL.And (PL.Or (PL.BoolVar v1, PL.Not (PL.BoolVar v2)),
   1.125            PL.Or (PL.Not (PL.BoolVar v1), PL.BoolVar v2))
   1.126 -fun prop_for_assign_literal (x, a) =
   1.127 +fun prop_for_assign (x, a) =
   1.128    let val (b1, b2) = bools_from_annotation a in
   1.129      PL.And (PL.BoolVar (fst_var x) |> not b1 ? PL.Not,
   1.130              PL.BoolVar (snd_var x) |> not b2 ? PL.Not)
   1.131    end
   1.132 +fun prop_for_assign_literal (x, (Plus, a)) = prop_for_assign (x, a)
   1.133 +  | prop_for_assign_literal (x, (Minus, a)) = PL.Not (prop_for_assign (x, a))
   1.134  fun prop_for_atom_assign (A a', a) = prop_for_bool (a = a')
   1.135 -  | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, a)
   1.136 +  | prop_for_atom_assign (V x, a) = prop_for_assign_literal (x, (Plus, a))
   1.137  fun prop_for_atom_equality (aa1, A a2) = prop_for_atom_assign (aa1, a2)
   1.138    | prop_for_atom_equality (A a1, aa2) = prop_for_atom_assign (aa2, a1)
   1.139    | prop_for_atom_equality (V x1, V x2) =
   1.140 @@ -509,10 +524,12 @@
   1.141              prop_for_bool_var_equality (pairself snd_var (x1, x2)))
   1.142  val prop_for_assign_clause = PL.exists o map prop_for_assign_literal
   1.143  fun prop_for_exists_var_assign_literal xs a =
   1.144 -  PL.exists (map (fn x => prop_for_assign_literal (x, a)) xs)
   1.145 +  PL.exists (map (fn x => prop_for_assign_literal (x, (Plus, a))) xs)
   1.146  fun prop_for_comp (aa1, aa2, Eq, []) =
   1.147      PL.SAnd (prop_for_comp (aa1, aa2, Leq, []),
   1.148               prop_for_comp (aa2, aa1, Leq, []))
   1.149 +  | prop_for_comp (aa1, aa2, Neq, []) =
   1.150 +    PL.Not (prop_for_comp (aa1, aa2, Eq, []))
   1.151    | prop_for_comp (aa1, aa2, Leq, []) =
   1.152      PL.SOr (prop_for_atom_equality (aa1, aa2), prop_for_atom_assign (aa2, Gen))
   1.153    | prop_for_comp (aa1, aa2, cmp, xs) =
   1.154 @@ -526,7 +543,8 @@
   1.155    @ (if calculus > 2 then [New, Tru] else [])
   1.156  
   1.157  fun prop_for_variable_domain calculus x =
   1.158 -  PL.exists (map (curry prop_for_assign_literal x) (variable_domain calculus))
   1.159 +  PL.exists (map (fn a => prop_for_assign_literal (x, (Plus, a)))
   1.160 +                 (variable_domain calculus))
   1.161  
   1.162  fun extract_assigns max_var assigns asgs =
   1.163    fold (fn x => fn accum =>
   1.164 @@ -555,7 +573,7 @@
   1.165  
   1.166  fun solve calculus max_var (comps, clauses) =
   1.167    let
   1.168 -    val asgs = map_filter (fn [asg] => SOME asg | _ => NONE) clauses
   1.169 +    val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
   1.170      fun do_assigns assigns =
   1.171        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
   1.172      val _ = print_problem calculus comps clauses