src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41009 91495051c2ec
parent 41007 75275c796b46
child 41011 5c2f16eae066
     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 @@ -229,6 +229,8 @@
     1.4    | is_fin_fun_supported_type @{typ bool} = true
     1.5    | is_fin_fun_supported_type (Type (@{type_name option}, _)) = true
     1.6    | is_fin_fun_supported_type _ = false
     1.7 +
     1.8 +(* TODO: clean this up *)
     1.9  fun fin_fun_body _ _ (t as @{term False}) = SOME t
    1.10    | fin_fun_body _ _ (t as Const (@{const_name None}, _)) = SOME t
    1.11    | fin_fun_body dom_T ran_T
    1.12 @@ -307,14 +309,23 @@
    1.13        | _ => MType (simple_string_of_typ T, [])
    1.14    in do_type end
    1.15  
    1.16 +val ground_and_sole_base_constrs = [@{const_name Nil}, @{const_name None}]
    1.17 +
    1.18  fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
    1.19    | prodM_factors M = [M]
    1.20  fun curried_strip_mtype (MFun (M1, _, M2)) =
    1.21      curried_strip_mtype M2 |>> append (prodM_factors M1)
    1.22    | curried_strip_mtype M = ([], M)
    1.23  fun sel_mtype_from_constr_mtype s M =
    1.24 -  let val (arg_Ms, dataM) = curried_strip_mtype M in
    1.25 -    MFun (dataM, A Gen,
    1.26 +  let
    1.27 +    val (arg_Ms, dataM) = curried_strip_mtype M
    1.28 +    val a = if member (op =) ground_and_sole_base_constrs
    1.29 +                             (constr_name_for_sel_like s) then
    1.30 +              Fls
    1.31 +            else
    1.32 +              Gen
    1.33 +  in
    1.34 +    MFun (dataM, A a,
    1.35            case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
    1.36    end
    1.37  
    1.38 @@ -837,6 +848,8 @@
    1.39         case t of
    1.40           @{const False} =>
    1.41           (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
    1.42 +       | Const (@{const_name None}, _) =>
    1.43 +         (MRaw (t, bool_M), accum ||> add_comp_frame (A Fls) Leq frame)
    1.44         | @{const True} =>
    1.45           (MRaw (t, bool_M), accum ||> add_comp_frame (A Tru) Leq frame)
    1.46         | Const (x as (s, T)) =>