# HG changeset patch # User blanchet # Date 1291638789 -3600 # Node ID 91495051c2ec0d44cbae42bbb92209fcee852912 # Parent 298226ba5606dd60342b882d3a1235ecc2942a3c improve precision of finite functions in monotonicity calculus diff -r 298226ba5606 -r 91495051c2ec src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:09 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Mon Dec 06 13:33:09 2010 +0100 @@ -229,6 +229,8 @@ | is_fin_fun_supported_type @{typ bool} = true | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true | is_fin_fun_supported_type _ = false + +(* TODO: clean this up *) fun fin_fun_body _ _ (t as @{term False}) = SOME t | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t | fin_fun_body dom_T ran_T @@ -307,14 +309,23 @@ | _ => MType (simple_string_of_typ T, []) in do_type end +val ground_and_sole_base_constrs = [@{const_name Nil}, @{const_name None}] + fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2] | prodM_factors M = [M] fun curried_strip_mtype (MFun (M1, _, M2)) = curried_strip_mtype M2 |>> append (prodM_factors M1) | curried_strip_mtype M = ([], M) fun sel_mtype_from_constr_mtype s M = - let val (arg_Ms, dataM) = curried_strip_mtype M in - MFun (dataM, A Gen, + let + val (arg_Ms, dataM) = curried_strip_mtype M + val a = if member (op =) ground_and_sole_base_constrs + (constr_name_for_sel_like s) then + Fls + else + Gen + in + MFun (dataM, A a, case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) end @@ -837,6 +848,8 @@ case t of @{const False} => (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame) + | Const (@{const_name None}, _) => + (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame) | @{const True} => (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame) | Const (x as (s, T)) =>