remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
authorblanchet
Tue Dec 07 11:56:53 2010 +0100 (2010-12-07)
changeset 410523db267a01c1d
parent 41051 2ed1b971fc20
child 41053 8e2f2398aae7
remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much
src/HOL/Nitpick.thy
src/HOL/Tools/Nitpick/nitpick.ML
src/HOL/Tools/Nitpick/nitpick_hol.ML
src/HOL/Tools/Nitpick/nitpick_model.ML
src/HOL/Tools/Nitpick/nitpick_mono.ML
src/HOL/Tools/Nitpick/nitpick_preproc.ML
src/HOL/Tools/Nitpick/nitpick_scope.ML
     1.1 --- a/src/HOL/Nitpick.thy	Tue Dec 07 11:56:01 2010 +0100
     1.2 +++ b/src/HOL/Nitpick.thy	Tue Dec 07 11:56:53 2010 +0100
     1.3 @@ -35,7 +35,6 @@
     1.4             and Quot :: "'a \<Rightarrow> 'b"
     1.5             and safe_The :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
     1.6  
     1.7 -datatype ('a, 'b) fin_fun = FinFun "('a \<Rightarrow> 'b)"
     1.8  datatype ('a, 'b) fun_box = FunBox "('a \<Rightarrow> 'b)"
     1.9  datatype ('a, 'b) pair_box = PairBox 'a 'b
    1.10  
    1.11 @@ -240,12 +239,11 @@
    1.12  setup {* Nitpick_Isar.setup *}
    1.13  
    1.14  hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The
    1.15 -    FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card'
    1.16 -    setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac
    1.17 -    zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.18 +    FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum'
    1.19 +    fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac
    1.20 +    one_frac num denom norm_frac frac plus_frac times_frac uminus_frac
    1.21      number_of_frac inverse_frac less_frac less_eq_frac of_frac
    1.22 -hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit
    1.23 -    word
    1.24 +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word
    1.25  hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def
    1.26      refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def
    1.27      fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def
     2.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:01 2010 +0100
     2.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML	Tue Dec 07 11:56:53 2010 +0100
     2.3 @@ -292,7 +292,7 @@
     2.4      val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse
     2.5              raise NOT_SUPPORTED "schematic type variables"
     2.6      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
     2.7 -         binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t
     2.8 +         binarize) = preprocess_formulas hol_ctxt assm_ts neg_t
     2.9      val got_all_user_axioms =
    2.10        got_all_mono_user_axioms andalso no_poly_user_axioms
    2.11  
    2.12 @@ -361,9 +361,7 @@
    2.13          SOME (SOME b) => b
    2.14        | _ => is_type_fundamentally_monotonic T orelse
    2.15               is_type_actually_monotonic T
    2.16 -    fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) =
    2.17 -        is_type_kind_of_monotonic T
    2.18 -      | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    2.19 +    fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) =
    2.20          is_type_kind_of_monotonic T
    2.21        | is_shallow_datatype_finitizable T =
    2.22          case triple_lookup (type_match thy) finitizes T of
     3.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:01 2010 +0100
     3.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML	Tue Dec 07 11:56:53 2010 +0100
     3.3 @@ -462,9 +462,7 @@
     3.4    | unarize_type @{typ "signed_bit word"} = int_T
     3.5    | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts)
     3.6    | unarize_type T = T
     3.7 -fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) =
     3.8 -    unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
     3.9 -  | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    3.10 +fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) =
    3.11      unarize_unbox_etc_type (Type (@{type_name fun}, Ts))
    3.12    | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) =
    3.13      Type (@{type_name prod}, map unarize_unbox_etc_type Ts)
    3.14 @@ -804,9 +802,9 @@
    3.15      end
    3.16    | _ => false
    3.17  fun is_constr_like ctxt (s, T) =
    3.18 -  member (op =) [@{const_name FinFun}, @{const_name FunBox},
    3.19 -                 @{const_name PairBox}, @{const_name Quot},
    3.20 -                 @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse
    3.21 +  member (op =) [@{const_name FunBox}, @{const_name PairBox},
    3.22 +                 @{const_name Quot}, @{const_name Zero_Rep},
    3.23 +                 @{const_name Suc_Rep}] s orelse
    3.24    let
    3.25      val thy = ProofContext.theory_of ctxt
    3.26      val (x as (_, T)) = (s, unarize_unbox_etc_type T)
    3.27 @@ -1095,14 +1093,13 @@
    3.28           |> Envir.eta_contract
    3.29           |> new_s <> @{type_name fun}
    3.30              ? construct_value ctxt stds
    3.31 -                  (if new_s = @{type_name fin_fun} then @{const_name FinFun}
    3.32 -                   else @{const_name FunBox},
    3.33 +                  (@{const_name FunBox},
    3.34                     Type (@{type_name fun}, new_Ts) --> new_T)
    3.35                o single
    3.36         | t' => raise TERM ("Nitpick_HOL.coerce_term", [t']))
    3.37      | (Type (new_s, new_Ts as [new_T1, new_T2]),
    3.38         Type (old_s, old_Ts as [old_T1, old_T2])) =>
    3.39 -      if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse
    3.40 +      if old_s = @{type_name fun_box} orelse
    3.41           old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then
    3.42          case constr_expand hol_ctxt old_T t of
    3.43            Const (old_s, _) $ t1 =>
     4.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:01 2010 +0100
     4.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML	Tue Dec 07 11:56:53 2010 +0100
     4.3 @@ -178,9 +178,7 @@
     4.4  fun tuple_list_for_name rel_table bounds name =
     4.5    the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]]
     4.6  
     4.7 -fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) =
     4.8 -    unarize_unbox_etc_term t1
     4.9 -  | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    4.10 +fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) =
    4.11      unarize_unbox_etc_term t1
    4.12    | unarize_unbox_etc_term
    4.13          (Const (@{const_name PairBox},
    4.14 @@ -559,9 +557,8 @@
    4.15                    if length arg_Ts = 0 then
    4.16                      []
    4.17                    else
    4.18 -                    map3 (fn Ts =>
    4.19 -                             term_for_rep (constr_s <> @{const_name FinFun})
    4.20 -                                          seen Ts Ts) arg_Ts arg_Rs arg_jsss
    4.21 +                    map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs
    4.22 +                         arg_jsss
    4.23                      |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts)
    4.24                      |> dest_n_tuple (length uncur_arg_Ts)
    4.25                  val t =
    4.26 @@ -935,8 +932,7 @@
    4.27        Pretty.block (Pretty.breaks
    4.28            (pretty_for_type ctxt typ ::
    4.29             (case typ of
    4.30 -              Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"]
    4.31 -            | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    4.32 +              Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"]
    4.33              | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"]
    4.34              | _ => []) @
    4.35             [Pretty.str "=",
     5.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:01 2010 +0100
     5.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML	Tue Dec 07 11:56:53 2010 +0100
     5.3 @@ -12,9 +12,6 @@
     5.4    val trace : bool Unsynchronized.ref
     5.5    val formulas_monotonic :
     5.6      hol_context -> bool -> typ -> term list * term list -> bool
     5.7 -  val finitize_funs :
     5.8 -    hol_context -> bool -> (typ option * bool option) list -> typ
     5.9 -    -> term list * term list -> term list * term list
    5.10  end;
    5.11  
    5.12  structure Nitpick_Mono : NITPICK_MONO =
    5.13 @@ -1249,110 +1246,4 @@
    5.14  
    5.15  val formulas_monotonic = is_some oooo infer "Monotonicity" false
    5.16  
    5.17 -fun fin_fun_constr T1 T2 =
    5.18 -  (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2]))
    5.19 -
    5.20 -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize
    5.21 -                  finitizes alpha_T tsp =
    5.22 -  case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of
    5.23 -    SOME (asgs, msp, constr_mtypes) =>
    5.24 -    if forall (curry (op =) Gen o snd) asgs then
    5.25 -      tsp
    5.26 -    else
    5.27 -      let
    5.28 -        fun should_finitize T aa =
    5.29 -          case triple_lookup (type_match thy) finitizes T of
    5.30 -            SOME (SOME false) => false
    5.31 -          | _ => resolve_annotation_atom asgs aa = A Fls
    5.32 -        fun type_from_mtype T M =
    5.33 -          case (M, T) of
    5.34 -            (MAlpha, _) => T
    5.35 -          | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) =>
    5.36 -            Type (if should_finitize T aa then @{type_name fin_fun}
    5.37 -                  else @{type_name fun}, map2 type_from_mtype Ts [M1, M2])
    5.38 -          | (MPair (M1, M2), Type (@{type_name prod}, Ts)) =>
    5.39 -            Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2])
    5.40 -          | (MType _, _) => T
    5.41 -          | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype",
    5.42 -                              [M], [T])
    5.43 -        fun finitize_constr (x as (s, T)) =
    5.44 -          (s, case AList.lookup (op =) constr_mtypes x of
    5.45 -                SOME M => type_from_mtype T M
    5.46 -              | NONE => T)
    5.47 -        fun term_from_mterm new_Ts old_Ts m =
    5.48 -          case m of
    5.49 -            MRaw (t, M) =>
    5.50 -            let
    5.51 -              val T = fastype_of1 (old_Ts, t)
    5.52 -              val T' = type_from_mtype T M
    5.53 -            in
    5.54 -              case t of
    5.55 -                Const (x as (s, _)) =>
    5.56 -                if s = @{const_name finite} then
    5.57 -                  case domain_type T' of
    5.58 -                    set_T' as Type (@{type_name fin_fun}, _) =>
    5.59 -                    Abs (Name.uu, set_T', @{const True})
    5.60 -                  | _ => Const (s, T')
    5.61 -                else if s = @{const_name "=="} orelse
    5.62 -                        s = @{const_name HOL.eq} then
    5.63 -                  let
    5.64 -                    val T =
    5.65 -                      case T' of
    5.66 -                        Type (_, [T1, Type (_, [T2, T3])]) =>
    5.67 -                        T1 --> T2 --> T3
    5.68 -                      | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\
    5.69 -                                         \term_from_mterm", [T, T'], [])
    5.70 -                  in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end
    5.71 -                else if is_built_in_const thy stds x then
    5.72 -                  coerce_term hol_ctxt new_Ts T' T t
    5.73 -                else if is_constr ctxt stds x then
    5.74 -                  Const (finitize_constr x)
    5.75 -                else if is_sel s then
    5.76 -                  let
    5.77 -                    val n = sel_no_from_name s
    5.78 -                    val x' =
    5.79 -                      x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
    5.80 -                        |> finitize_constr
    5.81 -                    val x'' =
    5.82 -                      binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize
    5.83 -                                                             x' n
    5.84 -                  in Const x'' end
    5.85 -                else
    5.86 -                  Const (s, T')
    5.87 -              | Free (s, T) => Free (s, type_from_mtype T M)
    5.88 -              | Bound _ => t
    5.89 -              | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm",
    5.90 -                                  [m])
    5.91 -            end
    5.92 -          | MApp (m1, m2) =>
    5.93 -            let
    5.94 -              val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2)
    5.95 -              val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2)
    5.96 -              val (t1', T2') =
    5.97 -                case T1 of
    5.98 -                  Type (s, [T11, T12]) =>
    5.99 -                  (if s = @{type_name fin_fun} then
   5.100 -                     select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1
   5.101 -                                           0 (T11 --> T12)
   5.102 -                   else
   5.103 -                     t1, T11)
   5.104 -                | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm",
   5.105 -                                   [T1], [])
   5.106 -            in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end
   5.107 -          | MAbs (s, old_T, M, aa, m') =>
   5.108 -            let
   5.109 -              val new_T = type_from_mtype old_T M
   5.110 -              val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m'
   5.111 -              val T' = fastype_of1 (new_T :: new_Ts, t')
   5.112 -            in
   5.113 -              Abs (s, new_T, t')
   5.114 -              |> should_finitize (new_T --> T') aa
   5.115 -                 ? construct_value ctxt stds (fin_fun_constr new_T T') o single
   5.116 -            end
   5.117 -      in
   5.118 -        Unsynchronized.change constr_cache (map (apsnd (map finitize_constr)));
   5.119 -        pairself (map (term_from_mterm [] [])) msp
   5.120 -      end
   5.121 -  | NONE => tsp
   5.122 -
   5.123  end;
     6.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:01 2010 +0100
     6.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML	Tue Dec 07 11:56:53 2010 +0100
     6.3 @@ -9,8 +9,7 @@
     6.4  sig
     6.5    type hol_context = Nitpick_HOL.hol_context
     6.6    val preprocess_formulas :
     6.7 -    hol_context -> (typ option * bool option) list
     6.8 -    -> (typ option * bool option) list -> term list -> term
     6.9 +    hol_context -> term list -> term
    6.10      -> term list * term list * bool * bool * bool
    6.11  end;
    6.12  
    6.13 @@ -1245,32 +1244,13 @@
    6.14               | _ => t
    6.15    in aux "" [] [] end
    6.16  
    6.17 -(** Inference of finite functions **)
    6.18 -
    6.19 -fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos
    6.20 -                               (nondef_ts, def_ts) =
    6.21 -  if forall (curry (op =) (SOME false) o snd) finitizes then
    6.22 -    (nondef_ts, def_ts)
    6.23 -  else
    6.24 -    let
    6.25 -      val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
    6.26 -               |> filter_out (fn Type (@{type_name fun_box}, _) => true
    6.27 -                               | @{typ signed_bit} => true
    6.28 -                               | @{typ unsigned_bit} => true
    6.29 -                               | T => is_small_finite_type hol_ctxt T orelse
    6.30 -                                      triple_lookup (type_match thy) monos T
    6.31 -                                      = SOME (SOME false))
    6.32 -    in
    6.33 -      fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts)
    6.34 -    end
    6.35 -
    6.36  (** Preprocessor entry point **)
    6.37  
    6.38  val max_skolem_depth = 3
    6.39  
    6.40  fun preprocess_formulas
    6.41          (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes,
    6.42 -                      ...}) finitizes monos assm_ts neg_t =
    6.43 +                      ...}) assm_ts neg_t =
    6.44    let
    6.45      val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
    6.46        neg_t |> unfold_defs_in_term hol_ctxt
    6.47 @@ -1307,9 +1287,6 @@
    6.48        #> Term.map_abs_vars shortest_name
    6.49      val nondef_ts = map (do_rest false) nondef_ts
    6.50      val def_ts = map (do_rest true) def_ts
    6.51 -    val (nondef_ts, def_ts) =
    6.52 -      finitize_all_types_of_funs hol_ctxt binarize finitizes monos
    6.53 -                                 (nondef_ts, def_ts)
    6.54    in
    6.55      (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
    6.56    end
     7.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:01 2010 +0100
     7.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML	Tue Dec 07 11:56:53 2010 +0100
     7.3 @@ -112,8 +112,6 @@
     7.4  
     7.5  fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
     7.6      is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     7.7 -  | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) =
     7.8 -    is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2
     7.9    | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) =
    7.10      forall (is_complete_type dtypes facto) Ts
    7.11    | is_complete_type dtypes facto T =
    7.12 @@ -122,8 +120,6 @@
    7.13      handle Option.Option => true
    7.14  and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) =
    7.15      is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
    7.16 -  | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) =
    7.17 -    is_concrete_type dtypes facto T2
    7.18    | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) =
    7.19      forall (is_concrete_type dtypes facto) Ts
    7.20    | is_concrete_type dtypes facto T =