fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
authorblanchet
Mon Dec 06 13:33:09 2010 +0100 (2010-12-06)
changeset 41013117345744f44
parent 41012 e5a23ffb5524
child 41014 e538a4f9dd86
fixed bug in monotonicity solution display, whereby the polarity of literals was ignored
src/HOL/Tools/Nitpick/nitpick_mono.ML
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Dec 06 13:33:09 2010 +0100
     1.3 @@ -309,7 +309,7 @@
     1.4        | _ => MType (simple_string_of_typ T, [])
     1.5    in do_type end
     1.6  
     1.7 -val ground_and_sole_base_constrs = [@{const_name Nil}, @{const_name None}]
     1.8 +val ground_and_sole_base_constrs = [] (* FIXME: [@{const_name Nil}, @{const_name None}], cf. lists_empty *)
     1.9  
    1.10  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
    1.11    | prodM_factors M = [M]
    1.12 @@ -579,7 +579,8 @@
    1.13  
    1.14  fun solve tac_timeout max_var (comps, clauses) =
    1.15    let
    1.16 -    val asgs = map_filter (fn [(x, (_, a))] => SOME (x, a) | _ => NONE) clauses
    1.17 +    val asgs =
    1.18 +      map_filter (fn [(x, (Plus, a))] => SOME (x, a) | _ => NONE) clauses
    1.19      fun do_assigns assigns =
    1.20        SOME (extract_assigns max_var assigns asgs |> tap print_solution)
    1.21      val _ = print_problem comps clauses