use boolean pair to encode annotation, which may now take four values
authorblanchet
Mon Dec 06 13:18:25 2010 +0100 (2010-12-06)
changeset 40986cfd91aa80701
parent 40985 8b870370c26f
child 40987 7d52af07bff1
use boolean pair to encode annotation, which may now take four values
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 @@ -461,14 +461,23 @@
     1.4  val add_mtype_is_concrete = add_notin_mtype_fv Minus
     1.5  val add_mtype_is_complete = add_notin_mtype_fv Plus
     1.6  
     1.7 -val bool_from_minus = true
     1.8 +fun fst_var n = 2 * n
     1.9 +fun snd_var n = 2 * n + 1
    1.10  
    1.11 -fun bool_from_annotation Fls = not bool_from_minus
    1.12 -  | bool_from_annotation Gen = bool_from_minus
    1.13 -fun sign_from_bool b = if b = bool_from_minus then Gen else Fls
    1.14 +val bool_table =
    1.15 +  [(Gen, (false, false)),
    1.16 +   (New, (false, true)),
    1.17 +   (Fls, (true, false)),
    1.18 +   (Tru, (true, true))]
    1.19 +
    1.20 +val bools_from_annotation = AList.lookup (op =) bool_table #> the
    1.21 +val annotation_from_bools = AList.find (op =) bool_table #> the_single
    1.22  
    1.23  fun prop_for_literal (x, a) =
    1.24 -  PropLogic.BoolVar x |> not (bool_from_annotation a) ? PropLogic.Not
    1.25 +  let val (b1, b2) = bools_from_annotation a in
    1.26 +    PropLogic.SAnd (PropLogic.BoolVar (fst_var x) |> not b1 ? PropLogic.Not,
    1.27 +                    PropLogic.BoolVar (snd_var x) |> not b2 ? PropLogic.Not)
    1.28 +  end
    1.29  fun prop_for_annotation_atom_eq (A a', a) =
    1.30      if a = a' then PropLogic.True else PropLogic.False
    1.31    | prop_for_annotation_atom_eq (V x, a) = prop_for_literal (x, a)
    1.32 @@ -484,13 +493,19 @@
    1.33    | prop_for_comp (a1, a2, cmp, xs) =
    1.34      PropLogic.SOr (prop_for_exists_eq xs Gen, prop_for_comp (a1, a2, cmp, []))
    1.35  
    1.36 +fun fix_bool_options (NONE, NONE) = (false, false)
    1.37 +  | fix_bool_options (NONE, SOME b) = (b, b)
    1.38 +  | fix_bool_options (SOME b, NONE) = (b, b)
    1.39 +  | fix_bool_options (SOME b1, SOME b2) = (b1, b2)
    1.40 +
    1.41  fun literals_from_assignments max_var assigns lits =
    1.42    fold (fn x => fn accum =>
    1.43             if AList.defined (op =) lits x then
    1.44               accum
    1.45 -           else case assigns x of
    1.46 -             SOME b => (x, sign_from_bool b) :: accum
    1.47 -           | NONE => accum) (max_var downto 1) lits
    1.48 +           else case (fst_var x, snd_var x) |> pairself assigns of
    1.49 +             (NONE, NONE) => accum
    1.50 +           | bp => (x, annotation_from_bools (fix_bool_options bp)) :: accum)
    1.51 +       (max_var downto 1) lits
    1.52  
    1.53  fun string_for_comp (a1, a2, cmp, xs) =
    1.54    string_for_annotation_atom a1 ^ " " ^ string_for_comp_op cmp ^
    1.55 @@ -518,7 +533,7 @@
    1.56      val prop = PropLogic.all (map prop_for_literal lits @
    1.57                                map prop_for_comp comps @
    1.58                                map prop_for_annotation_expr sexps)
    1.59 -    val default_val = bool_from_annotation Gen
    1.60 +    val default_val = fst (bools_from_annotation Gen)
    1.61    in
    1.62      if PropLogic.eval (K default_val) prop then
    1.63        do_assigns (K (SOME default_val))