src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 37476 0681e46b4022
parent 37267 5c47d633c84d
child 37678 0040bafffdef
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Jun 21 09:38:20 2010 +0200
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Mon Jun 21 11:15:21 2010 +0200
     1.3 @@ -54,8 +54,9 @@
     1.4  exception MTYPE of string * mtyp list * typ list
     1.5  exception MTERM of string * mterm list
     1.6  
     1.7 -fun print_g (_ : string) = ()
     1.8 -(* val print_g = tracing *)
     1.9 +val debug_mono = false
    1.10 +
    1.11 +fun print_g f = () |> debug_mono ? tracing o f
    1.12  
    1.13  val string_for_var = signed_string_of_int
    1.14  fun string_for_vars sep [] = "0\<^bsub>" ^ sep ^ "\<^esub>"
    1.15 @@ -401,10 +402,10 @@
    1.16                   [M1, M2], [])
    1.17  
    1.18  fun add_mtype_comp cmp M1 M2 ((lits, comps, sexps) : constraint_set) =
    1.19 -    (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
    1.20 -              " " ^ string_for_mtype M2);
    1.21 +    (print_g (fn () => "*** Add " ^ string_for_mtype M1 ^ " " ^
    1.22 +                       string_for_comp_op cmp ^ " " ^ string_for_mtype M2);
    1.23       case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
    1.24 -       NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
    1.25 +       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.26       | SOME (lits, comps) => (lits, comps, sexps))
    1.27  
    1.28  val add_mtypes_equal = add_mtype_comp Eq
    1.29 @@ -446,10 +447,11 @@
    1.30      raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M], [])
    1.31  
    1.32  fun add_notin_mtype_fv sn M ((lits, comps, sexps) : constraint_set) =
    1.33 -    (print_g ("*** Add " ^ string_for_mtype M ^ " is " ^
    1.34 -              (case sn of Minus => "concrete" | Plus => "complete") ^ ".");
    1.35 +    (print_g (fn () => "*** Add " ^ string_for_mtype M ^ " is " ^
    1.36 +                       (case sn of Minus => "concrete" | Plus => "complete") ^
    1.37 +                       ".");
    1.38       case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
    1.39 -       NONE => (print_g "**** Unsolvable"; raise UNSOLVABLE ())
    1.40 +       NONE => (print_g (K "**** Unsolvable"); raise UNSOLVABLE ())
    1.41       | SOME (lits, sexps) => (lits, comps, sexps))
    1.42  
    1.43  val add_mtype_is_concrete = add_notin_mtype_fv Minus
    1.44 @@ -491,15 +493,16 @@
    1.45    subscript_string_for_vars " \<and> " xs ^ " " ^ string_for_sign_atom a2
    1.46  
    1.47  fun print_problem lits comps sexps =
    1.48 -  print_g ("*** Problem:\n" ^ cat_lines (map string_for_literal lits @
    1.49 -                                         map string_for_comp comps @
    1.50 -                                         map string_for_sign_expr sexps))
    1.51 +  print_g (fn () => "*** Problem:\n" ^
    1.52 +                    cat_lines (map string_for_literal lits @
    1.53 +                               map string_for_comp comps @
    1.54 +                               map string_for_sign_expr sexps))
    1.55  
    1.56  fun print_solution lits =
    1.57    let val (pos, neg) = List.partition (curry (op =) Plus o snd) lits in
    1.58 -    print_g ("*** Solution:\n" ^
    1.59 -             "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    1.60 -             "-: " ^ commas (map (string_for_var o fst) neg))
    1.61 +    print_g (fn () => "*** Solution:\n" ^
    1.62 +                      "+: " ^ commas (map (string_for_var o fst) pos) ^ "\n" ^
    1.63 +                      "-: " ^ commas (map (string_for_var o fst) neg))
    1.64    end
    1.65  
    1.66  fun solve max_var (lits, comps, sexps) =
    1.67 @@ -550,6 +553,12 @@
    1.68                                            def_table, ...},
    1.69                               alpha_T, max_fresh, ...}) =
    1.70    let
    1.71 +    fun is_enough_eta_expanded t =
    1.72 +      case strip_comb t of
    1.73 +        (Const x, ts) =>
    1.74 +        the_default 0 (arity_of_built_in_const thy stds fast_descrs x)
    1.75 +        <= length ts
    1.76 +      | _ => true
    1.77      val mtype_for = fresh_mtype_for_type mdata false
    1.78      fun plus_set_mtype_for_dom M =
    1.79        MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
    1.80 @@ -640,8 +649,10 @@
    1.81                    |>> mtype_of_mterm
    1.82                  end
    1.83                | @{const_name "op ="} => do_equals T accum
    1.84 -              | @{const_name The} => (print_g "*** The"; raise UNSOLVABLE ())
    1.85 -              | @{const_name Eps} => (print_g "*** Eps"; raise UNSOLVABLE ())
    1.86 +              | @{const_name The} =>
    1.87 +                (print_g (K "*** The"); raise UNSOLVABLE ())
    1.88 +              | @{const_name Eps} =>
    1.89 +                (print_g (K "*** Eps"); raise UNSOLVABLE ())
    1.90                | @{const_name If} =>
    1.91                  do_robust_set_operation (range_type T) accum
    1.92                  |>> curry3 MFun bool_M (S Minus)
    1.93 @@ -650,19 +661,6 @@
    1.94                | @{const_name snd} => do_nth_pair_sel 1 T accum 
    1.95                | @{const_name Id} =>
    1.96                  (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
    1.97 -              | @{const_name insert} =>
    1.98 -                let
    1.99 -                  val set_T = domain_type (range_type T)
   1.100 -                  val M1 = mtype_for (domain_type set_T)
   1.101 -                  val M1' = plus_set_mtype_for_dom M1
   1.102 -                  val M2 = mtype_for set_T
   1.103 -                  val M3 = mtype_for set_T
   1.104 -                in
   1.105 -                  (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
   1.106 -                   (gamma, cset |> add_mtype_is_concrete M1
   1.107 -                                |> add_is_sub_mtype M1' M3
   1.108 -                                |> add_is_sub_mtype M2 M3))
   1.109 -                end
   1.110                | @{const_name converse} =>
   1.111                  let
   1.112                    val x = Unsynchronized.inc max_fresh
   1.113 @@ -720,25 +718,9 @@
   1.114                      val a_set_M = mtype_for (domain_type T)
   1.115                      val a_M = dest_MFun a_set_M |> #1
   1.116                    in (MFun (a_set_M, S Minus, a_M), accum) end
   1.117 -                else if s = @{const_name minus_class.minus} andalso
   1.118 -                        is_set_type (domain_type T) then
   1.119 -                  let
   1.120 -                    val set_T = domain_type T
   1.121 -                    val left_set_M = mtype_for set_T
   1.122 -                    val right_set_M = mtype_for set_T
   1.123 -                  in
   1.124 -                    (MFun (left_set_M, S Minus,
   1.125 -                           MFun (right_set_M, S Minus, left_set_M)),
   1.126 -                     (gamma, cset |> add_mtype_is_concrete right_set_M
   1.127 -                                  |> add_is_sub_mtype right_set_M left_set_M))
   1.128 -                  end
   1.129                  else if s = @{const_name ord_class.less_eq} andalso
   1.130                          is_set_type (domain_type T) then
   1.131                    do_fragile_set_operation T accum
   1.132 -                else if (s = @{const_name semilattice_inf_class.inf} orelse
   1.133 -                         s = @{const_name semilattice_sup_class.sup}) andalso
   1.134 -                        is_set_type (domain_type T) then
   1.135 -                  do_robust_set_operation T accum
   1.136                  else if is_sel s then
   1.137                    (mtype_for_sel mdata x, accum)
   1.138                  else if is_constr ctxt stds x then
   1.139 @@ -758,7 +740,7 @@
   1.140                  (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   1.141                        frees = (x, M) :: frees, consts = consts}, cset))
   1.142                end) |>> curry MRaw t
   1.143 -         | Var _ => (print_g "*** Var"; raise UNSOLVABLE ())
   1.144 +         | Var _ => (print_g (K "*** Var"); raise UNSOLVABLE ())
   1.145           | Bound j => (MRaw (t, nth bound_Ms j), accum)
   1.146           | Abs (s, T, t') =>
   1.147             (case fin_fun_body T (fastype_of1 (T :: bound_Ts, t')) t' of
   1.148 @@ -771,10 +753,16 @@
   1.149              | NONE =>
   1.150                ((case t' of
   1.151                    t1' $ Bound 0 =>
   1.152 -                  if not (loose_bvar1 (t1', 0)) then
   1.153 +                  if not (loose_bvar1 (t1', 0)) andalso
   1.154 +                     is_enough_eta_expanded t1' then
   1.155                      do_term (incr_boundvars ~1 t1') accum
   1.156                    else
   1.157                      raise SAME ()
   1.158 +                | (t11 as Const (@{const_name "op ="}, _)) $ Bound 0 $ t13 =>
   1.159 +                  if not (loose_bvar1 (t13, 0)) then
   1.160 +                    do_term (incr_boundvars ~1 (t11 $ t13)) accum
   1.161 +                  else
   1.162 +                    raise SAME ()
   1.163                  | _ => raise SAME ())
   1.164                 handle SAME () =>
   1.165                        let
   1.166 @@ -803,8 +791,8 @@
   1.167                 val M2 = mtype_of_mterm m2
   1.168               in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
   1.169             end)
   1.170 -        |> tap (fn (m, _) => print_g ("  \<Gamma> \<turnstile> " ^
   1.171 -                                      string_for_mterm ctxt m))
   1.172 +        |> tap (fn (m, _) => print_g (fn () => "  \<Gamma> \<turnstile> " ^
   1.173 +                                               string_for_mterm ctxt m))
   1.174    in do_term end
   1.175  
   1.176  fun force_minus_funs 0 _ = I
   1.177 @@ -902,9 +890,9 @@
   1.178            | _ => do_term t accum
   1.179          end
   1.180          |> tap (fn (m, _) =>
   1.181 -                   print_g ("\<Gamma> \<turnstile> " ^
   1.182 -                            string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.183 -                            string_for_sign sn))
   1.184 +                   print_g (fn () => "\<Gamma> \<turnstile> " ^
   1.185 +                                     string_for_mterm ctxt m ^ " : o\<^sup>" ^
   1.186 +                                     string_for_sign sn))
   1.187    in do_formula end
   1.188  
   1.189  (* The harmless axiom optimization below is somewhat too aggressive in the face
   1.190 @@ -987,9 +975,10 @@
   1.191    Syntax.string_of_term ctxt t ^ " : " ^ string_for_mtype (resolve_mtype lits M)
   1.192  
   1.193  fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
   1.194 -  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   1.195 -  map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   1.196 -  |> cat_lines |> print_g
   1.197 +  print_g (fn () =>
   1.198 +      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
   1.199 +      map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
   1.200 +      |> cat_lines)
   1.201  
   1.202  fun amass f t (ms, accum) =
   1.203    let val (m, accum) = f t accum in (m :: ms, accum) end
   1.204 @@ -997,9 +986,9 @@
   1.205  fun infer which no_harmless (hol_ctxt as {ctxt, ...}) binarize alpha_T
   1.206            (nondef_ts, def_ts) =
   1.207    let
   1.208 -    val _ = print_g ("****** " ^ which ^ " analysis: " ^
   1.209 -                     string_for_mtype MAlpha ^ " is " ^
   1.210 -                     Syntax.string_of_typ ctxt alpha_T)
   1.211 +    val _ = print_g (fn () => "****** " ^ which ^ " analysis: " ^
   1.212 +                              string_for_mtype MAlpha ^ " is " ^
   1.213 +                              Syntax.string_of_typ ctxt alpha_T)
   1.214      val mdata as {max_fresh, constr_mcache, ...} =
   1.215        initial_mdata hol_ctxt binarize no_harmless alpha_T
   1.216      val accum = (initial_gamma, ([], [], []))
   1.217 @@ -1064,26 +1053,21 @@
   1.218              in
   1.219                case t of
   1.220                  Const (x as (s, _)) =>
   1.221 -                if s = @{const_name insert} then
   1.222 -                  case nth_range_type 2 T' of
   1.223 -                    set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
   1.224 -                      Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
   1.225 -                          Const (@{const_name If},
   1.226 -                                 bool_T --> set_T' --> set_T' --> set_T')
   1.227 -                          $ (Const (@{const_name is_unknown},
   1.228 -                                    elem_T' --> bool_T) $ Bound 1)
   1.229 -                          $ (Const (@{const_name unknown}, set_T'))
   1.230 -                          $ (coerce_term hol_ctxt new_Ts T' T (Const x)
   1.231 -                             $ Bound 1 $ Bound 0)))
   1.232 -                  | _ => Const (s, T')
   1.233 -                else if s = @{const_name finite} then
   1.234 +                if s = @{const_name finite} then
   1.235                    case domain_type T' of
   1.236                      set_T' as Type (@{type_name fin_fun}, _) =>
   1.237                      Abs (Name.uu, set_T', @{const True})
   1.238                    | _ => Const (s, T')
   1.239                  else if s = @{const_name "=="} orelse
   1.240                          s = @{const_name "op ="} then
   1.241 -                  Const (s, T')
   1.242 +                  let
   1.243 +                    val T =
   1.244 +                      case T' of
   1.245 +                        Type (_, [T1, Type (_, [T2, T3])]) =>
   1.246 +                        T1 --> T2 --> T3
   1.247 +                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
   1.248 +                                         \term_from_mterm", [T, T'], [])
   1.249 +                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
   1.250                  else if is_built_in_const thy stds fast_descrs x then
   1.251                    coerce_term hol_ctxt new_Ts T' T t
   1.252                  else if is_constr ctxt stds x then