src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 35672 ff484d4f2e14
parent 35671 ed2c3830d881
child 35812 394fe2b064cd
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 14:18:21 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Mar 09 16:40:31 2010 +0100
     1.3 @@ -264,20 +264,22 @@
     1.4                  $ (Const (@{const_name unknown}, ran_T)) $ (t0 $ t1 $ t2 $ t3)))
     1.5    | fin_fun_body _ _ _ = NONE
     1.6  
     1.7 -(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
     1.8 -fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
     1.9 +(* mdata -> bool -> typ -> typ -> mtyp * sign_atom * mtyp *)
    1.10 +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) all_minus
    1.11 +                            T1 T2 =
    1.12    let
    1.13 -    val M1 = fresh_mtype_for_type mdata T1
    1.14 -    val M2 = fresh_mtype_for_type mdata T2
    1.15 -    val a = if is_fin_fun_supported_type (body_type T2) andalso
    1.16 -               exists_alpha_sub_mtype_fresh M1 then
    1.17 +    val M1 = fresh_mtype_for_type mdata all_minus T1
    1.18 +    val M2 = fresh_mtype_for_type mdata all_minus T2
    1.19 +    val a = if not all_minus andalso exists_alpha_sub_mtype_fresh M1 andalso
    1.20 +               is_fin_fun_supported_type (body_type T2) then
    1.21                V (Unsynchronized.inc max_fresh)
    1.22              else
    1.23                S Minus
    1.24    in (M1, a, M2) end
    1.25 -(* mdata -> typ -> mtyp *)
    1.26 +(* mdata -> bool -> typ -> mtyp *)
    1.27  and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
    1.28 -                                    datatype_mcache, constr_mcache, ...}) =
    1.29 +                                    datatype_mcache, constr_mcache, ...})
    1.30 +                         all_minus =
    1.31    let
    1.32      (* typ -> mtyp *)
    1.33      fun do_type T =
    1.34 @@ -285,7 +287,7 @@
    1.35          MAlpha
    1.36        else case T of
    1.37          Type (@{type_name fun}, [T1, T2]) =>
    1.38 -        MFun (fresh_mfun_for_fun_type mdata T1 T2)
    1.39 +        MFun (fresh_mfun_for_fun_type mdata false T1 T2)
    1.40        | Type (@{type_name "*"}, [T1, T2]) => MPair (pairself do_type (T1, T2))
    1.41        | Type (z as (s, _)) =>
    1.42          if could_exist_alpha_sub_mtype thy alpha_T T then
    1.43 @@ -347,14 +349,14 @@
    1.44      case AList.lookup (op =) (!constr_mcache) x of
    1.45        SOME M => M
    1.46      | NONE => if T = alpha_T then
    1.47 -                let val M = fresh_mtype_for_type mdata T in
    1.48 +                let val M = fresh_mtype_for_type mdata false T in
    1.49                    (Unsynchronized.change constr_mcache (cons (x, M)); M)
    1.50                  end
    1.51                else
    1.52 -                (fresh_mtype_for_type mdata (body_type T);
    1.53 +                (fresh_mtype_for_type mdata false (body_type T);
    1.54                   AList.lookup (op =) (!constr_mcache) x |> the)
    1.55    else
    1.56 -    fresh_mtype_for_type mdata T
    1.57 +    fresh_mtype_for_type mdata false T
    1.58  fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
    1.59    x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    1.60      |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
    1.61 @@ -629,7 +631,7 @@
    1.62                               alpha_T, max_fresh, ...}) =
    1.63    let
    1.64      (* typ -> mtyp *)
    1.65 -    val mtype_for = fresh_mtype_for_type mdata
    1.66 +    val mtype_for = fresh_mtype_for_type mdata false
    1.67      (* mtyp -> mtyp *)
    1.68      fun plus_set_mtype_for_dom M =
    1.69        MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
    1.70 @@ -765,12 +767,6 @@
    1.71                    val ba_set_M = range_type T |> mtype_for_set
    1.72                  in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
    1.73                | @{const_name trancl} => do_fragile_set_operation T accum
    1.74 -              | @{const_name rtrancl} =>
    1.75 -                (print_g "*** rtrancl"; mtype_unsolvable)
    1.76 -              | @{const_name finite} =>
    1.77 -                let val M1 = mtype_for (domain_type (domain_type T)) in
    1.78 -                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
    1.79 -                end
    1.80                | @{const_name rel_comp} =>
    1.81                  let
    1.82                    val x = Unsynchronized.inc max_fresh
    1.83 @@ -793,6 +789,10 @@
    1.84                           MFun (plus_set_mtype_for_dom a_M, S Minus,
    1.85                                 plus_set_mtype_for_dom b_M)), accum)
    1.86                  end
    1.87 +              | @{const_name finite} =>
    1.88 +                let val M1 = mtype_for (domain_type (domain_type T)) in
    1.89 +                  (MFun (plus_set_mtype_for_dom M1, S Minus, bool_M), accum)
    1.90 +                end
    1.91                | @{const_name Sigma} =>
    1.92                  let
    1.93                    val x = Unsynchronized.inc max_fresh
    1.94 @@ -840,13 +840,8 @@
    1.95                    (mtype_for_sel mdata x, accum)
    1.96                  else if is_constr thy stds x then
    1.97                    (mtype_for_constr mdata x, accum)
    1.98 -                else if is_built_in_const thy stds fast_descrs x andalso
    1.99 -                        s <> @{const_name is_unknown} andalso
   1.100 -                        s <> @{const_name unknown} then
   1.101 -                  (* the "unknown" part is a hack *)
   1.102 -                  case def_of_const thy def_table x of
   1.103 -                    SOME t' => do_term t' accum |>> mtype_of_mterm
   1.104 -                  | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
   1.105 +                else if is_built_in_const thy stds fast_descrs x then
   1.106 +                  (fresh_mtype_for_type mdata true T, accum)
   1.107                  else
   1.108                    let val M = mtype_for T in
   1.109                      (M, ({bound_Ts = bound_Ts, bound_Ms = bound_Ms,
   1.110 @@ -934,7 +929,7 @@
   1.111      val M1 = mtype_of_mterm m1
   1.112      val M2 = mtype_of_mterm m2
   1.113      val accum = accum ||> add_mtypes_equal M1 M2
   1.114 -    val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
   1.115 +    val body_M = fresh_mtype_for_type mdata false (nth_range_type 2 T)
   1.116      val m = MApp (MApp (MRaw (Const x,
   1.117                  MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2)
   1.118    in
   1.119 @@ -950,7 +945,7 @@
   1.120  fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
   1.121    let
   1.122      (* typ -> mtyp *)
   1.123 -    val mtype_for = fresh_mtype_for_type mdata
   1.124 +    val mtype_for = fresh_mtype_for_type mdata false
   1.125      (* term -> accumulator -> mterm * accumulator *)
   1.126      val do_term = consider_term mdata
   1.127      (* sign -> term -> accumulator -> mterm * accumulator *)
   1.128 @@ -1057,7 +1052,7 @@
   1.129    else
   1.130      let
   1.131        (* typ -> mtyp *)
   1.132 -      val mtype_for = fresh_mtype_for_type mdata
   1.133 +      val mtype_for = fresh_mtype_for_type mdata false
   1.134        (* term -> accumulator -> mterm * accumulator *)
   1.135        val do_term = consider_term mdata
   1.136        (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
   1.137 @@ -1203,11 +1198,23 @@
   1.138              val T' = type_from_mtype T M
   1.139            in
   1.140              case t of
   1.141 -              Const (x as (s, T)) =>
   1.142 -              if s = @{const_name finite} then
   1.143 +              Const (x as (s, _)) =>
   1.144 +              if s = @{const_name insert} then
   1.145 +                case nth_range_type 2 T' of
   1.146 +                  set_T' as Type (@{type_name fin_fun}, [elem_T', _]) =>
   1.147 +                    Abs (Name.uu, elem_T', Abs (Name.uu, set_T',
   1.148 +                        Const (@{const_name If},
   1.149 +                               bool_T --> set_T' --> set_T' --> set_T')
   1.150 +                        $ (Const (@{const_name is_unknown}, elem_T' --> bool_T)
   1.151 +                           $ Bound 1)
   1.152 +                        $ (Const (@{const_name unknown}, set_T'))
   1.153 +                        $ (coerce_term hol_ctxt Ts T' T (Const x)
   1.154 +                           $ Bound 1 $ Bound 0)))
   1.155 +                | _ => Const (s, T')
   1.156 +              else if s = @{const_name finite} then
   1.157                  case domain_type T' of
   1.158 -                  T1' as Type (@{type_name fin_fun}, _) =>
   1.159 -                  Abs (Name.uu, T1', @{const True})
   1.160 +                  set_T' as Type (@{type_name fin_fun}, _) =>
   1.161 +                  Abs (Name.uu, set_T', @{const True})
   1.162                  | _ => Const (s, T')
   1.163                else if s = @{const_name "=="} orelse
   1.164                        s = @{const_name "op ="} then
   1.165 @@ -1232,16 +1239,6 @@
   1.166              | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
   1.167                                  [m])
   1.168            end
   1.169 -        | MAbs (s, T, M, a, m') =>
   1.170 -          let
   1.171 -            val T = type_from_mtype T M
   1.172 -            val t' = term_from_mterm (T :: Ts) m'
   1.173 -            val T' = fastype_of1 (T :: Ts, t')
   1.174 -          in
   1.175 -            Abs (s, T, t')
   1.176 -            |> should_finitize (T --> T') a
   1.177 -               ? construct_value thy stds (fin_fun_constr T T') o single
   1.178 -          end
   1.179          | MApp (m1, m2) =>
   1.180            let
   1.181              val (t1, t2) = pairself (term_from_mterm Ts) (m1, m2)
   1.182 @@ -1257,6 +1254,16 @@
   1.183                | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
   1.184                                   [T1], [])
   1.185            in betapply (t1', coerce_term hol_ctxt Ts T2' T2 t2) end
   1.186 +        | MAbs (s, T, M, a, m') =>
   1.187 +          let
   1.188 +            val T = type_from_mtype T M
   1.189 +            val t' = term_from_mterm (T :: Ts) m'
   1.190 +            val T' = fastype_of1 (T :: Ts, t')
   1.191 +          in
   1.192 +            Abs (s, T, t')
   1.193 +            |> should_finitize (T --> T') a
   1.194 +               ? construct_value thy stds (fin_fun_constr T T') o single
   1.195 +          end
   1.196      in
   1.197        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
   1.198        pairself (map (term_from_mterm [])) msp