author blanchet Mon, 06 Dec 2010 13:33:09 +0100 changeset 41009 91495051c2ec parent 41008 298226ba5606 child 41010 1e5f382c48cc
improve precision of finite functions in monotonicity calculus
```--- 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)) =>```