# HG changeset patch # User blanchet # Date 1291719413 -3600 # Node ID 3db267a01c1d59adfdf406a304955fb338ef04e7 # Parent 2ed1b971fc20659429b6705737843682a3bfa29c remove the "fin_fun" optimization in Nitpick -- it was always a hack and didn't help much diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Nitpick.thy Tue Dec 07 11:56:53 2010 +0100 @@ -35,7 +35,6 @@ and Quot :: "'a \ 'b" and safe_The :: "('a \ bool) \ 'a" -datatype ('a, 'b) fin_fun = FinFun "('a \ 'b)" datatype ('a, 'b) fun_box = FunBox "('a \ 'b)" datatype ('a, 'b) pair_box = PairBox 'a 'b @@ -240,12 +239,11 @@ setup {* Nitpick_Isar.setup *} hide_const (open) unknown is_unknown bisim bisim_iterator_max Quot safe_The - FinFun FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' - setsum' fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac - zero_frac one_frac num denom norm_frac frac plus_frac times_frac uminus_frac + FunBox PairBox Word prod refl' wf' wf_wfrec wf_wfrec' wfrec' card' setsum' + fold_graph' nat_gcd nat_lcm int_gcd int_lcm Frac Abs_Frac Rep_Frac zero_frac + one_frac num denom norm_frac frac plus_frac times_frac uminus_frac number_of_frac inverse_frac less_frac less_eq_frac of_frac -hide_type (open) bisim_iterator fin_fun fun_box pair_box unsigned_bit signed_bit - word +hide_type (open) bisim_iterator fun_box pair_box unsigned_bit signed_bit word hide_fact (open) If_def Ex1_def rtrancl_def rtranclp_def tranclp_def prod_def refl'_def wf'_def wf_wfrec'_def wfrec'_def card'_def setsum'_def fold_graph'_def The_psimp Eps_psimp unit_case_def nat_case_def diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Dec 07 11:56:53 2010 +0100 @@ -292,7 +292,7 @@ val _ = null (fold Term.add_tvars (neg_t :: assm_ts) []) orelse raise NOT_SUPPORTED "schematic type variables" val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, - binarize) = preprocess_formulas hol_ctxt finitizes monos assm_ts neg_t + binarize) = preprocess_formulas hol_ctxt assm_ts neg_t val got_all_user_axioms = got_all_mono_user_axioms andalso no_poly_user_axioms @@ -361,9 +361,7 @@ SOME (SOME b) => b | _ => is_type_fundamentally_monotonic T orelse is_type_actually_monotonic T - fun is_shallow_datatype_finitizable (T as Type (@{type_name fin_fun}, _)) = - is_type_kind_of_monotonic T - | is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) = + fun is_shallow_datatype_finitizable (T as Type (@{type_name fun_box}, _)) = is_type_kind_of_monotonic T | is_shallow_datatype_finitizable T = case triple_lookup (type_match thy) finitizes T of diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Dec 07 11:56:53 2010 +0100 @@ -462,9 +462,7 @@ | unarize_type @{typ "signed_bit word"} = int_T | unarize_type (Type (s, Ts as _ :: _)) = Type (s, map unarize_type Ts) | unarize_type T = T -fun unarize_unbox_etc_type (Type (@{type_name fin_fun}, Ts)) = - unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) - | unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = +fun unarize_unbox_etc_type (Type (@{type_name fun_box}, Ts)) = unarize_unbox_etc_type (Type (@{type_name fun}, Ts)) | unarize_unbox_etc_type (Type (@{type_name pair_box}, Ts)) = Type (@{type_name prod}, map unarize_unbox_etc_type Ts) @@ -804,9 +802,9 @@ end | _ => false fun is_constr_like ctxt (s, T) = - member (op =) [@{const_name FinFun}, @{const_name FunBox}, - @{const_name PairBox}, @{const_name Quot}, - @{const_name Zero_Rep}, @{const_name Suc_Rep}] s orelse + member (op =) [@{const_name FunBox}, @{const_name PairBox}, + @{const_name Quot}, @{const_name Zero_Rep}, + @{const_name Suc_Rep}] s orelse let val thy = ProofContext.theory_of ctxt val (x as (_, T)) = (s, unarize_unbox_etc_type T) @@ -1095,14 +1093,13 @@ |> Envir.eta_contract |> new_s <> @{type_name fun} ? construct_value ctxt stds - (if new_s = @{type_name fin_fun} then @{const_name FinFun} - else @{const_name FunBox}, + (@{const_name FunBox}, Type (@{type_name fun}, new_Ts) --> new_T) o single | t' => raise TERM ("Nitpick_HOL.coerce_term", [t'])) | (Type (new_s, new_Ts as [new_T1, new_T2]), Type (old_s, old_Ts as [old_T1, old_T2])) => - if old_s = @{type_name fin_fun} orelse old_s = @{type_name fun_box} orelse + if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box} orelse old_s = @{type_name prod} then case constr_expand hol_ctxt old_T t of Const (old_s, _) $ t1 => diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Dec 07 11:56:53 2010 +0100 @@ -178,9 +178,7 @@ fun tuple_list_for_name rel_table bounds name = the (AList.lookup (op =) bounds (the_rel rel_table name)) handle NUT _ => [[]] -fun unarize_unbox_etc_term (Const (@{const_name FinFun}, _) $ t1) = - unarize_unbox_etc_term t1 - | unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) = +fun unarize_unbox_etc_term (Const (@{const_name FunBox}, _) $ t1) = unarize_unbox_etc_term t1 | unarize_unbox_etc_term (Const (@{const_name PairBox}, @@ -559,9 +557,8 @@ if length arg_Ts = 0 then [] else - map3 (fn Ts => - term_for_rep (constr_s <> @{const_name FinFun}) - seen Ts Ts) arg_Ts arg_Rs arg_jsss + map3 (fn Ts => term_for_rep true seen Ts Ts) arg_Ts arg_Rs + arg_jsss |> mk_tuple (HOLogic.mk_tupleT uncur_arg_Ts) |> dest_n_tuple (length uncur_arg_Ts) val t = @@ -935,8 +932,7 @@ Pretty.block (Pretty.breaks (pretty_for_type ctxt typ :: (case typ of - Type (@{type_name fin_fun}, _) => [Pretty.str "[finite]"] - | Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"] + Type (@{type_name fun_box}, _) => [Pretty.str "[boxed]"] | Type (@{type_name pair_box}, _) => [Pretty.str "[boxed]"] | _ => []) @ [Pretty.str "=", diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Dec 07 11:56:53 2010 +0100 @@ -12,9 +12,6 @@ val trace : bool Unsynchronized.ref val formulas_monotonic : hol_context -> bool -> typ -> term list * term list -> bool - val finitize_funs : - hol_context -> bool -> (typ option * bool option) list -> typ - -> term list * term list -> term list * term list end; structure Nitpick_Mono : NITPICK_MONO = @@ -1249,110 +1246,4 @@ val formulas_monotonic = is_some oooo infer "Monotonicity" false -fun fin_fun_constr T1 T2 = - (@{const_name FinFun}, (T1 --> T2) --> Type (@{type_name fin_fun}, [T1, T2])) - -fun finitize_funs (hol_ctxt as {thy, ctxt, stds, constr_cache, ...}) binarize - finitizes alpha_T tsp = - case infer "Finiteness" true hol_ctxt binarize alpha_T tsp of - SOME (asgs, msp, constr_mtypes) => - if forall (curry (op =) Gen o snd) asgs then - tsp - else - let - fun should_finitize T aa = - case triple_lookup (type_match thy) finitizes T of - SOME (SOME false) => false - | _ => resolve_annotation_atom asgs aa = A Fls - fun type_from_mtype T M = - case (M, T) of - (MAlpha, _) => T - | (MFun (M1, aa, M2), Type (@{type_name fun}, Ts)) => - Type (if should_finitize T aa then @{type_name fin_fun} - else @{type_name fun}, map2 type_from_mtype Ts [M1, M2]) - | (MPair (M1, M2), Type (@{type_name prod}, Ts)) => - Type (@{type_name prod}, map2 type_from_mtype Ts [M1, M2]) - | (MType _, _) => T - | _ => raise MTYPE ("Nitpick_Mono.finitize_funs.type_from_mtype", - [M], [T]) - fun finitize_constr (x as (s, T)) = - (s, case AList.lookup (op =) constr_mtypes x of - SOME M => type_from_mtype T M - | NONE => T) - fun term_from_mterm new_Ts old_Ts m = - case m of - MRaw (t, M) => - let - val T = fastype_of1 (old_Ts, t) - val T' = type_from_mtype T M - in - case t of - Const (x as (s, _)) => - if s = @{const_name finite} then - case domain_type T' of - set_T' as Type (@{type_name fin_fun}, _) => - Abs (Name.uu, set_T', @{const True}) - | _ => Const (s, T') - else if s = @{const_name "=="} orelse - s = @{const_name HOL.eq} then - let - val T = - case T' of - Type (_, [T1, Type (_, [T2, T3])]) => - T1 --> T2 --> T3 - | _ => raise TYPE ("Nitpick_Mono.finitize_funs.\ - \term_from_mterm", [T, T'], []) - in coerce_term hol_ctxt new_Ts T' T (Const (s, T)) end - else if is_built_in_const thy stds x then - coerce_term hol_ctxt new_Ts T' T t - else if is_constr ctxt stds x then - Const (finitize_constr x) - else if is_sel s then - let - val n = sel_no_from_name s - val x' = - x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize - |> finitize_constr - val x'' = - binarized_and_boxed_nth_sel_for_constr hol_ctxt binarize - x' n - in Const x'' end - else - Const (s, T') - | Free (s, T) => Free (s, type_from_mtype T M) - | Bound _ => t - | _ => raise MTERM ("Nitpick_Mono.finitize_funs.term_from_mterm", - [m]) - end - | MApp (m1, m2) => - let - val (t1, t2) = pairself (term_from_mterm new_Ts old_Ts) (m1, m2) - val (T1, T2) = pairself (curry fastype_of1 new_Ts) (t1, t2) - val (t1', T2') = - case T1 of - Type (s, [T11, T12]) => - (if s = @{type_name fin_fun} then - select_nth_constr_arg ctxt stds (fin_fun_constr T11 T12) t1 - 0 (T11 --> T12) - else - t1, T11) - | _ => raise TYPE ("Nitpick_Mono.finitize_funs.term_from_mterm", - [T1], []) - in betapply (t1', coerce_term hol_ctxt new_Ts T2' T2 t2) end - | MAbs (s, old_T, M, aa, m') => - let - val new_T = type_from_mtype old_T M - val t' = term_from_mterm (new_T :: new_Ts) (old_T :: old_Ts) m' - val T' = fastype_of1 (new_T :: new_Ts, t') - in - Abs (s, new_T, t') - |> should_finitize (new_T --> T') aa - ? construct_value ctxt stds (fin_fun_constr new_T T') o single - end - in - Unsynchronized.change constr_cache (map (apsnd (map finitize_constr))); - pairself (map (term_from_mterm [] [])) msp - end - | NONE => tsp - end; diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Dec 07 11:56:53 2010 +0100 @@ -9,8 +9,7 @@ sig type hol_context = Nitpick_HOL.hol_context val preprocess_formulas : - hol_context -> (typ option * bool option) list - -> (typ option * bool option) list -> term list -> term + hol_context -> term list -> term -> term list * term list * bool * bool * bool end; @@ -1245,32 +1244,13 @@ | _ => t in aux "" [] [] end -(** Inference of finite functions **) - -fun finitize_all_types_of_funs (hol_ctxt as {thy, ...}) binarize finitizes monos - (nondef_ts, def_ts) = - if forall (curry (op =) (SOME false) o snd) finitizes then - (nondef_ts, def_ts) - else - let - val Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts) - |> filter_out (fn Type (@{type_name fun_box}, _) => true - | @{typ signed_bit} => true - | @{typ unsigned_bit} => true - | T => is_small_finite_type hol_ctxt T orelse - triple_lookup (type_match thy) monos T - = SOME (SOME false)) - in - fold (finitize_funs hol_ctxt binarize finitizes) Ts (nondef_ts, def_ts) - end - (** Preprocessor entry point **) val max_skolem_depth = 3 fun preprocess_formulas (hol_ctxt as {thy, ctxt, stds, binary_ints, destroy_constrs, boxes, - ...}) finitizes monos assm_ts neg_t = + ...}) assm_ts neg_t = let val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) = neg_t |> unfold_defs_in_term hol_ctxt @@ -1307,9 +1287,6 @@ #> Term.map_abs_vars shortest_name val nondef_ts = map (do_rest false) nondef_ts val def_ts = map (do_rest true) def_ts - val (nondef_ts, def_ts) = - finitize_all_types_of_funs hol_ctxt binarize finitizes monos - (nondef_ts, def_ts) in (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) end diff -r 2ed1b971fc20 -r 3db267a01c1d src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Dec 07 11:56:01 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Dec 07 11:56:53 2010 +0100 @@ -112,8 +112,6 @@ fun is_complete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 - | is_complete_type dtypes facto (Type (@{type_name fin_fun}, [T1, T2])) = - is_exact_type dtypes facto T1 andalso is_complete_type dtypes facto T2 | is_complete_type dtypes facto (Type (@{type_name prod}, Ts)) = forall (is_complete_type dtypes facto) Ts | is_complete_type dtypes facto T = @@ -122,8 +120,6 @@ handle Option.Option => true and is_concrete_type dtypes facto (Type (@{type_name fun}, [T1, T2])) = is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 - | is_concrete_type dtypes facto (Type (@{type_name fin_fun}, [_, T2])) = - is_concrete_type dtypes facto T2 | is_concrete_type dtypes facto (Type (@{type_name prod}, Ts)) = forall (is_concrete_type dtypes facto) Ts | is_concrete_type dtypes facto T =