src/HOL/Tools/Nitpick/nitpick_mono.ML
changeset 41052 3db267a01c1d
parent 41050 effbaa323cf0
child 41054 e58d1cdda832
     1.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -12,9 +12,6 @@
     1.4    val trace : bool Unsynchronized.ref
     1.5    val formulas_monotonic :
     1.6      hol_context -> bool -> typ -> term list * term list -> bool
     1.7 -  val finitize_funs :
     1.8 -    hol_context -> bool -> (typ option * bool option) list -> typ
     1.9 -    -> term list * term list -> term list * term list
    1.10  end;
    1.11  
    1.12  structure Nitpick_Mono : NITPICK_MONO =
    1.13 @@ -1249,110 +1246,4 @@
    1.14  
    1.15  val formulas_monotonic = is_some oooo infer "Monotonicity" false
    1.16  
    1.17 -fun fin_fun_constr T1 T2 =
    1.18 -  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
    1.19 -
    1.20 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
    1.21 -                  finitizes alpha_T tsp =
    1.22 -  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
    1.23 -    SOME (asgs, msp, constr_mtypes) =>
    1.24 -    if forall (curry (op =) Gen o snd) asgs then
    1.25 -      tsp
    1.26 -    else
    1.27 -      let
    1.28 -        fun should_finitize T aa =
    1.29 -          case triple_lookup (type_match thy) finitizes T of
    1.30 -            SOME (SOME false) => false
    1.31 -          | _ => resolve_annotation_atom asgs aa = A Fls
    1.32 -        fun type_from_mtype T M =
    1.33 -          case (M, T) of
    1.34 -            (MAlpha, _) => T
    1.35 -          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
    1.36 -            Type (if should_finitize T aa then @{type_name fin_fun}
    1.37 -                  else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
    1.38 -          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
    1.39 -            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
    1.40 -          | (MType _, _) => T
    1.41 -          | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
    1.42 -                              [M], [T])
    1.43 -        fun finitize_constr (x as (s, T)) =
    1.44 -          (s, case AList.lookup (op =) constr_mtypes x of
    1.45 -                SOME M => type_from_mtype T M
    1.46 -              | NONE => T)
    1.47 -        fun term_from_mterm new_Ts old_Ts m =
    1.48 -          case m of
    1.49 -            MRaw (t, M) =>
    1.50 -            let
    1.51 -              val T = fastype_of1 (old_Ts, t)
    1.52 -              val T' = type_from_mtype T M
    1.53 -            in
    1.54 -              case t of
    1.55 -                Const (x as (s, _)) =>
    1.56 -                if s = @{const_name finite} then
    1.57 -                  case domain_type T' of
    1.58 -                    set_T' as Type (@{type_name fin_fun}, _) =>
    1.59 -                    Abs (Name.uu, set_T', @{const True})
    1.60 -                  | _ => Const (s, T')
    1.61 -                else if s = @{const_name "=="} orelse
    1.62 -                        s = @{const_name HOL.eq} then
    1.63 -                  let
    1.64 -                    val T =
    1.65 -                      case T' of
    1.66 -                        Type (_, [T1, Type (_, [T2, T3])]) =>
    1.67 -                        T1 --> T2 --> T3
    1.68 -                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
    1.69 -                                         \term_from_mterm", [T, T'], [])
    1.70 -                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
    1.71 -                else if is_built_in_const thy stds x then
    1.72 -                  coerce_term hol_ctxt new_Ts T' T t
    1.73 -                else if is_constr ctxt stds x then
    1.74 -                  Const (finitize_constr x)
    1.75 -                else if is_sel s then
    1.76 -                  let
    1.77 -                    val n = sel_no_from_name s
    1.78 -                    val x' =
    1.79 -                      x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    1.80 -                        |> finitize_constr
    1.81 -                    val x'' =
    1.82 -                      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
    1.83 -                                                             x' n
    1.84 -                  in Const x'' end
    1.85 -                else
    1.86 -                  Const (s, T')
    1.87 -              | Free (s, T) => Free (s, type_from_mtype T M)
    1.88 -              | Bound _ => t
    1.89 -              | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
    1.90 -                                  [m])
    1.91 -            end
    1.92 -          | MApp (m1, m2) =>
    1.93 -            let
    1.94 -              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
    1.95 -              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    1.96 -              val (t1', T2') =
    1.97 -                case T1 of
    1.98 -                  Type (s, [T11, T12]) =>
    1.99 -                  (if s = @{type_name fin_fun} then
   1.100 -                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
   1.101 -                                           0 (T11 --> T12)
   1.102 -                   else
   1.103 -                     t1, T11)
   1.104 -                | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
   1.105 -                                   [T1], [])
   1.106 -            in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
   1.107 -          | MAbs (s, old_T, M, aa, m') =>
   1.108 -            let
   1.109 -              val new_T = type_from_mtype old_T M
   1.110 -              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
   1.111 -              val T' = fastype_of1 (new_T :: new_Ts, t')
   1.112 -            in
   1.113 -              Abs (s, new_T, t')
   1.114 -              |> should_finitize (new_T --> T') aa
   1.115 -                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
   1.116 -            end
   1.117 -      in
   1.118 -        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
   1.119 -        pairself (map (term_from_mterm [] [])) msp
   1.120 -      end
   1.121 -  | NONE => tsp
   1.122 -
   1.123  end;