# HG changeset patch # User blanchet # Date 1268326087 -3600 # Node ID eee1a5e0d33464e8f27d1d9d4f6829fc1a017fd3 # Parent 428284ee1465909ea95630049b0c6fa34a5ec22b moved some Nitpick code around diff -r 428284ee1465 -r eee1a5e0d334 src/HOL/Nitpick_Examples/Manual_Nits.thy --- a/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 16:56:22 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Manual_Nits.thy Thu Mar 11 17:48:07 2010 +0100 @@ -280,19 +280,19 @@ "n \ reach \ n + 2 \ reach" lemma "n \ reach \ 2 dvd n" -nitpick [unary_ints, expect = none] +nitpick [card = 1\5, bits = 1\5, expect = none] apply (induct set: reach) apply auto - nitpick [expect = none] + nitpick [card = 1\5, bits = 1\5, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops lemma "n \ reach \ 2 dvd n \ n \ 0" -nitpick [unary_ints, expect = none] +nitpick [card = 1\5, bits = 1\5, expect = none] apply (induct set: reach) apply auto - nitpick [expect = none] + nitpick [card = 1\5, bits = 1\5, expect = none] apply (thin_tac "n \ reach") nitpick [expect = genuine] oops diff -r 428284ee1465 -r eee1a5e0d334 src/HOL/Tools/Nitpick/kodkod.ML --- a/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 16:56:22 2010 +0100 +++ b/src/HOL/Tools/Nitpick/kodkod.ML Thu Mar 11 17:48:07 2010 +0100 @@ -319,6 +319,8 @@ int_expr_func: int_expr -> 'a -> 'a } +(** Auxiliary functions on ML representation of Kodkod problems **) + (* 'a fold_expr_funcs -> formula -> 'a -> 'a *) fun fold_formula (F : 'a fold_expr_funcs) formula = case formula of @@ -512,18 +514,7 @@ filter (is_relevant_setting o fst) (#settings p1) = filter (is_relevant_setting o fst) (#settings p2) -val created_temp_dir = Unsynchronized.ref false - -(* bool -> string * string *) -fun serial_string_and_temporary_dir_for_overlord overlord = - if overlord then - ("", getenv "ISABELLE_HOME_USER") - else - let - val dir = getenv "ISABELLE_TMP" - val _ = if !created_temp_dir then () - else (created_temp_dir := true; File.mkdir (Path.explode dir)) - in (serial_string (), dir) end +(** Serialization of problem **) (* int -> string *) fun base_name j = @@ -901,6 +892,8 @@ map out_problem problems end +(** Parsing of solution **) + (* string -> bool *) fun is_ident_char s = Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse @@ -1016,6 +1009,21 @@ is partly due to the JVM and partly due to the ML "bash" function. *) val fudge_ms = 250 +(** Main Kodkod entry point **) + +val created_temp_dir = Unsynchronized.ref false + +(* bool -> string * string *) +fun serial_string_and_temporary_dir_for_overlord overlord = + if overlord then + ("", getenv "ISABELLE_HOME_USER") + else + let + val dir = getenv "ISABELLE_TMP" + val _ = if !created_temp_dir then () + else (created_temp_dir := true; File.mkdir (Path.explode dir)) + in (serial_string (), dir) end + (* bool -> Time.time option -> int -> int -> problem list -> outcome *) fun solve_any_problem overlord deadline max_threads max_solutions problems = let diff -r 428284ee1465 -r eee1a5e0d334 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 11 16:56:22 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Thu Mar 11 17:48:07 2010 +0100 @@ -52,6 +52,9 @@ val name_sep : string val numeral_prefix : string + val base_prefix : string + val step_prefix : string + val unrolled_prefix : string val ubfp_prefix : string val lbfp_prefix : string val quot_normal_prefix : string @@ -59,6 +62,8 @@ val special_prefix : string val uncurry_prefix : string val eval_prefix : string + val iter_var_prefix : string + val strip_first_name_sep : string -> string * string val original_name : string -> string val s_conj : term * term -> term val s_disj : term * term -> term @@ -169,6 +174,7 @@ val term_under_def : term -> term val case_const_names : theory -> (typ option * bool) list -> (string * int) list + val unfold_defs_in_term : hol_context -> term -> term val const_def_table : Proof.context -> (term * term) list -> term list -> const_table val const_nondef_table : term list -> const_table @@ -184,13 +190,13 @@ val optimized_quot_type_axioms : Proof.context -> (typ option * bool) list -> string * typ list -> term list val def_of_const : theory -> const_table -> styp -> term option + val fixpoint_kind_of_rhs : term -> fixpoint_kind val fixpoint_kind_of_const : theory -> const_table -> string * typ -> fixpoint_kind val is_inductive_pred : hol_context -> styp -> bool val is_equational_fun : hol_context -> styp -> bool val is_constr_pattern_lhs : theory -> term -> bool val is_constr_pattern_formula : theory -> term -> bool - val unfold_defs_in_term : hol_context -> term -> term val codatatype_bisim_axioms : hol_context -> typ -> term list val is_well_founded_inductive_pred : hol_context -> styp -> bool val unrolled_inductive_pred_const : hol_context -> bool -> styp -> term @@ -199,13 +205,6 @@ val merge_type_vars_in_terms : term list -> term list val ground_types_in_type : hol_context -> bool -> typ -> typ list val ground_types_in_terms : hol_context -> bool -> term list -> typ list - val format_type : int list -> int list -> typ -> typ - val format_term_type : - theory -> const_table -> (term option * int list) list -> term -> typ - val user_friendly_const : - hol_context -> string * string -> (term option * int list) list - -> styp -> term * typ - val assign_operator_for_const : styp -> string end; structure Nitpick_HOL : NITPICK_HOL = @@ -283,7 +282,8 @@ val uncurry_prefix = nitpick_prefix ^ "unc" val eval_prefix = nitpick_prefix ^ "eval" val iter_var_prefix = "i" -val arg_var_prefix = "x" + +(** Constant/type information and term/type manipulation **) (* int -> string *) fun sel_prefix_for j = sel_prefix ^ string_of_int j ^ name_sep @@ -301,7 +301,13 @@ case strip_first_name_sep s of (s1, "") => s1 | (_, s2) => original_name s2 else s -val after_name_sep = snd o strip_first_name_sep + +(* term * term -> term *) +fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t + | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t + | s_betapply p = betapply p +(* term * term list -> term *) +val s_betapplys = Library.foldl s_betapply (* term * term -> term *) fun s_conj (t1, @{const True}) = t1 @@ -505,7 +511,8 @@ Type ((if gfp then gfp_iterator_prefix else lfp_iterator_prefix) ^ s, binder_types T) (* typ -> styp *) -fun const_for_iterator_type (Type (s, Ts)) = (after_name_sep s, Ts ---> bool_T) +fun const_for_iterator_type (Type (s, Ts)) = + (strip_first_name_sep s |> snd, Ts ---> bool_T) | const_for_iterator_type T = raise TYPE ("Nitpick_HOL.const_for_iterator_type", [T], []) @@ -540,13 +547,6 @@ fun dest_n_tuple 1 t = [t] | dest_n_tuple n t = HOLogic.dest_prod t ||> dest_n_tuple (n - 1) |> op :: -(* int -> typ -> typ list *) -fun dest_n_tuple_type 1 T = [T] - | dest_n_tuple_type n (Type (_, [T1, T2])) = - T1 :: dest_n_tuple_type (n - 1) T2 - | dest_n_tuple_type _ T = - raise TYPE ("Nitpick_HOL.dest_n_tuple_type", [T], []) - type typedef_info = {rep_type: typ, abs_type: typ, Rep_name: string, Abs_name: string, set_def: thm option, prop_of_Rep: thm, set_name: string, @@ -1463,106 +1463,57 @@ (Datatype.get_all thy) [] @ map (apsnd length o snd) (#codatatypes (Data.get thy)) -(* Proof.context -> (term * term) list -> term list -> const_table *) -fun const_def_table ctxt subst ts = - table_for (map prop_of o Nitpick_Defs.get) ctxt subst - |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) - (map pair_for_prop ts) -(* term list -> const_table *) -fun const_nondef_table ts = - fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] - |> AList.group (op =) |> Symtab.make -(* Proof.context -> (term * term) list -> const_table *) -val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) -val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) -(* Proof.context -> (term * term) list -> const_table -> const_table *) -fun inductive_intro_table ctxt subst def_table = - table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) - def_table o prop_of) - o Nitpick_Intros.get) ctxt subst -(* theory -> term list Inttab.table *) -fun ground_theorem_table thy = - fold ((fn @{const Trueprop} $ t1 => - is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) - | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty +(* theory -> const_table -> string * typ -> fixpoint_kind *) +fun fixpoint_kind_of_const thy table x = + if is_built_in_const thy [(NONE, false)] false x then + NoFp + else + fixpoint_kind_of_rhs (the (def_of_const thy table x)) + handle Option.Option => NoFp -val basic_ersatz_table = - [(@{const_name prod_case}, @{const_name split}), - (@{const_name card}, @{const_name card'}), - (@{const_name setsum}, @{const_name setsum'}), - (@{const_name fold_graph}, @{const_name fold_graph'}), - (@{const_name wf}, @{const_name wf'}), - (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), - (@{const_name wfrec}, @{const_name wfrec'})] - -(* theory -> (string * string) list *) -fun ersatz_table thy = - fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table - -(* const_table Unsynchronized.ref -> string -> term list -> unit *) -fun add_simps simp_table s eqs = - Unsynchronized.change simp_table - (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) +(* hol_context -> styp -> bool *) +fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table, + ...} : hol_context) x = + fixpoint_kind_of_const thy def_table x <> NoFp andalso + not (null (def_props_for_const thy stds fast_descrs intro_table x)) +fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table, + ...} : hol_context) x = + exists (fn table => not (null (def_props_for_const thy stds fast_descrs table + x))) + [!simp_table, psimp_table] +fun is_inductive_pred hol_ctxt = + is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt) +fun is_equational_fun hol_ctxt = + (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf + (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) -(* theory -> styp -> term list *) -fun inverse_axioms_for_rep_fun thy (x as (_, T)) = - let val abs_T = domain_type T in - typedef_info thy (fst (dest_Type abs_T)) |> the - |> pairf #Abs_inverse #Rep_inverse - |> pairself (Refute.specialize_type thy x o prop_of o the) - ||> single |> op :: - end -(* theory -> string * typ list -> term list *) -fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) = - let val abs_T = Type abs_z in - if is_univ_typedef thy abs_T then - [] - else case typedef_info thy abs_s of - SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} => - let - val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type - val rep_t = Const (Rep_name, abs_T --> rep_T) - val set_t = Const (set_name, rep_T --> bool_T) - val set_t' = - prop_of_Rep |> HOLogic.dest_Trueprop - |> Refute.specialize_type thy (dest_Const rep_t) - |> HOLogic.dest_mem |> snd - in - [HOLogic.all_const abs_T - $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))] - |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t')) - |> map HOLogic.mk_Trueprop - end - | NONE => [] - end -(* Proof.context -> string * typ list -> term list *) -fun optimized_quot_type_axioms ctxt stds abs_z = - let - val thy = ProofContext.theory_of ctxt - val abs_T = Type abs_z - val rep_T = rep_type_for_quot_type thy abs_T - val equiv_rel = equiv_relation_for_quot_type thy abs_T - val a_var = Var (("a", 0), abs_T) - val x_var = Var (("x", 0), rep_T) - val y_var = Var (("y", 0), rep_T) - val x = (@{const_name Quot}, rep_T --> abs_T) - val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T - val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) - val normal_x = normal_t $ x_var - val normal_y = normal_t $ y_var - val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T) - in - [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t), - Logic.list_implies - ([@{const Not} $ (is_unknown_t $ normal_x), - @{const Not} $ (is_unknown_t $ normal_y), - equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop, - Logic.mk_equals (normal_x, normal_y)), - Logic.list_implies - ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)), - HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))], - HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] - end +(* term -> term *) +fun lhs_of_equation t = + case t of + Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 + | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1 + | @{const "==>"} $ _ $ t2 => lhs_of_equation t2 + | @{const Trueprop} $ t1 => lhs_of_equation t1 + | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1 + | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1 + | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2 + | _ => NONE +(* theory -> term -> bool *) +fun is_constr_pattern _ (Bound _) = true + | is_constr_pattern _ (Var _) = true + | is_constr_pattern thy t = + case strip_comb t of + (Const x, args) => + is_constr_like thy x andalso forall (is_constr_pattern thy) args + | _ => false +fun is_constr_pattern_lhs thy t = + forall (is_constr_pattern thy) (snd (strip_comb t)) +fun is_constr_pattern_formula thy t = + case lhs_of_equation t of + SOME t' => is_constr_pattern_lhs thy t' + | NONE => false + +(** Constant unfolding **) (* theory -> (typ option * bool) list -> int * styp -> term *) fun constr_case_body thy stds (j, (x as (_, T))) = @@ -1586,7 +1537,6 @@ |> fold_rev (add_constr_case hol_ctxt res_T) (length xs downto 2 ~~ xs') |> fold_rev (curry absdummy) (func_Ts @ [dataT]) end - (* hol_context -> string -> typ -> typ -> term -> term *) fun optimized_record_get (hol_ctxt as {thy, stds, ...}) s rec_T res_T t = let val constr_x = hd (datatype_constrs hol_ctxt rec_T) in @@ -1624,63 +1574,6 @@ end) (index_seq 0 n) Ts in list_comb (Const constr_x, ts) end -(* theory -> const_table -> string * typ -> fixpoint_kind *) -fun fixpoint_kind_of_const thy table x = - if is_built_in_const thy [(NONE, false)] false x then - NoFp - else - fixpoint_kind_of_rhs (the (def_of_const thy table x)) - handle Option.Option => NoFp - -(* hol_context -> styp -> bool *) -fun is_real_inductive_pred ({thy, stds, fast_descrs, def_table, intro_table, - ...} : hol_context) x = - fixpoint_kind_of_const thy def_table x <> NoFp andalso - not (null (def_props_for_const thy stds fast_descrs intro_table x)) -fun is_real_equational_fun ({thy, stds, fast_descrs, simp_table, psimp_table, - ...} : hol_context) x = - exists (fn table => not (null (def_props_for_const thy stds fast_descrs table - x))) - [!simp_table, psimp_table] -fun is_inductive_pred hol_ctxt = - is_real_inductive_pred hol_ctxt andf (not o is_real_equational_fun hol_ctxt) -fun is_equational_fun hol_ctxt = - (is_real_equational_fun hol_ctxt orf is_real_inductive_pred hol_ctxt orf - (String.isPrefix ubfp_prefix orf String.isPrefix lbfp_prefix) o fst) - -(* term * term -> term *) -fun s_betapply (Const (@{const_name If}, _) $ @{const True} $ t, _) = t - | s_betapply (Const (@{const_name If}, _) $ @{const False} $ _, t) = t - | s_betapply p = betapply p -(* term * term list -> term *) -val s_betapplys = Library.foldl s_betapply - -(* term -> term *) -fun lhs_of_equation t = - case t of - Const (@{const_name all}, _) $ Abs (_, _, t1) => lhs_of_equation t1 - | Const (@{const_name "=="}, _) $ t1 $ _ => SOME t1 - | @{const "==>"} $ _ $ t2 => lhs_of_equation t2 - | @{const Trueprop} $ t1 => lhs_of_equation t1 - | Const (@{const_name All}, _) $ Abs (_, _, t1) => lhs_of_equation t1 - | Const (@{const_name "op ="}, _) $ t1 $ _ => SOME t1 - | @{const "op -->"} $ _ $ t2 => lhs_of_equation t2 - | _ => NONE -(* theory -> term -> bool *) -fun is_constr_pattern _ (Bound _) = true - | is_constr_pattern _ (Var _) = true - | is_constr_pattern thy t = - case strip_comb t of - (Const x, args) => - is_constr_like thy x andalso forall (is_constr_pattern thy) args - | _ => false -fun is_constr_pattern_lhs thy t = - forall (is_constr_pattern thy) (snd (strip_comb t)) -fun is_constr_pattern_formula thy t = - case lhs_of_equation t of - SOME t' => is_constr_pattern_lhs thy t' - | NONE => false - (* Prevents divergence in case of cyclic or infinite definition dependencies. *) val unfold_max_depth = 255 @@ -1823,6 +1716,109 @@ in s_betapplys (const, map (do_term depth Ts) ts) |> Envir.beta_norm end in do_term 0 [] end +(** Axiom extraction/generation **) + +(* Proof.context -> (term * term) list -> term list -> const_table *) +fun const_def_table ctxt subst ts = + table_for (map prop_of o Nitpick_Defs.get) ctxt subst + |> fold (fn (s, t) => Symtab.map_default (s, []) (cons t)) + (map pair_for_prop ts) +(* term list -> const_table *) +fun const_nondef_table ts = + fold (fn t => append (map (fn s => (s, t)) (Term.add_const_names t []))) ts [] + |> AList.group (op =) |> Symtab.make +(* Proof.context -> (term * term) list -> const_table *) +val const_simp_table = table_for (map prop_of o Nitpick_Simps.get) +val const_psimp_table = table_for (map prop_of o Nitpick_Psimps.get) +(* Proof.context -> (term * term) list -> const_table -> const_table *) +fun inductive_intro_table ctxt subst def_table = + table_for (map (unfold_mutually_inductive_preds (ProofContext.theory_of ctxt) + def_table o prop_of) + o Nitpick_Intros.get) ctxt subst +(* theory -> term list Inttab.table *) +fun ground_theorem_table thy = + fold ((fn @{const Trueprop} $ t1 => + is_ground_term t1 ? Inttab.map_default (hash_term t1, []) (cons t1) + | _ => I) o prop_of o snd) (PureThy.all_thms_of thy) Inttab.empty + +val basic_ersatz_table = + [(@{const_name prod_case}, @{const_name split}), + (@{const_name card}, @{const_name card'}), + (@{const_name setsum}, @{const_name setsum'}), + (@{const_name fold_graph}, @{const_name fold_graph'}), + (@{const_name wf}, @{const_name wf'}), + (@{const_name wf_wfrec}, @{const_name wf_wfrec'}), + (@{const_name wfrec}, @{const_name wfrec'})] + +(* theory -> (string * string) list *) +fun ersatz_table thy = + fold (append o snd) (#frac_types (Data.get thy)) basic_ersatz_table + +(* const_table Unsynchronized.ref -> string -> term list -> unit *) +fun add_simps simp_table s eqs = + Unsynchronized.change simp_table + (Symtab.update (s, eqs @ these (Symtab.lookup (!simp_table) s))) + +(* theory -> styp -> term list *) +fun inverse_axioms_for_rep_fun thy (x as (_, T)) = + let val abs_T = domain_type T in + typedef_info thy (fst (dest_Type abs_T)) |> the + |> pairf #Abs_inverse #Rep_inverse + |> pairself (Refute.specialize_type thy x o prop_of o the) + ||> single |> op :: + end +(* theory -> string * typ list -> term list *) +fun optimized_typedef_axioms thy (abs_z as (abs_s, _)) = + let val abs_T = Type abs_z in + if is_univ_typedef thy abs_T then + [] + else case typedef_info thy abs_s of + SOME {abs_type, rep_type, Rep_name, prop_of_Rep, set_name, ...} => + let + val rep_T = varify_and_instantiate_type thy abs_type abs_T rep_type + val rep_t = Const (Rep_name, abs_T --> rep_T) + val set_t = Const (set_name, rep_T --> bool_T) + val set_t' = + prop_of_Rep |> HOLogic.dest_Trueprop + |> Refute.specialize_type thy (dest_Const rep_t) + |> HOLogic.dest_mem |> snd + in + [HOLogic.all_const abs_T + $ Abs (Name.uu, abs_T, set_t $ (rep_t $ Bound 0))] + |> set_t <> set_t' ? cons (HOLogic.mk_eq (set_t, set_t')) + |> map HOLogic.mk_Trueprop + end + | NONE => [] + end +(* Proof.context -> string * typ list -> term list *) +fun optimized_quot_type_axioms ctxt stds abs_z = + let + val thy = ProofContext.theory_of ctxt + val abs_T = Type abs_z + val rep_T = rep_type_for_quot_type thy abs_T + val equiv_rel = equiv_relation_for_quot_type thy abs_T + val a_var = Var (("a", 0), abs_T) + val x_var = Var (("x", 0), rep_T) + val y_var = Var (("y", 0), rep_T) + val x = (@{const_name Quot}, rep_T --> abs_T) + val sel_a_t = select_nth_constr_arg thy stds x a_var 0 rep_T + val normal_t = Const (quot_normal_name_for_type ctxt abs_T, rep_T --> rep_T) + val normal_x = normal_t $ x_var + val normal_y = normal_t $ y_var + val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T) + in + [Logic.mk_equals (normal_t $ sel_a_t, sel_a_t), + Logic.list_implies + ([@{const Not} $ (is_unknown_t $ normal_x), + @{const Not} $ (is_unknown_t $ normal_y), + equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop, + Logic.mk_equals (normal_x, normal_y)), + Logic.list_implies + ([HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)), + HOLogic.mk_Trueprop (@{const Not} $ HOLogic.mk_eq (normal_x, x_var))], + HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))] + end + (* hol_context -> typ -> term list *) fun codatatype_bisim_axioms (hol_ctxt as {thy, stds, ...}) T = let @@ -2155,7 +2151,7 @@ end fun inductive_pred_axiom hol_ctxt (x as (s, T)) = if String.isPrefix ubfp_prefix s orelse String.isPrefix lbfp_prefix s then - let val x' = (after_name_sep s, T) in + let val x' = (strip_first_name_sep s |> snd, T) in raw_inductive_pred_axiom hol_ctxt x' |> subst_atomic [(Const x', Const x)] end else @@ -2177,6 +2173,8 @@ strip_comb t1 |> snd |> forall is_Var | _ => false +(** Type preprocessing **) + (* term list -> term list *) fun merge_type_vars_in_terms ts = let @@ -2222,198 +2220,4 @@ fun ground_types_in_terms hol_ctxt binarize ts = fold (fold_types (add_ground_types hol_ctxt binarize)) ts [] -(* theory -> const_table -> styp -> int list *) -fun const_format thy def_table (x as (s, T)) = - if String.isPrefix unrolled_prefix s then - const_format thy def_table (original_name s, range_type T) - else if String.isPrefix skolem_prefix s then - let - val k = unprefix skolem_prefix s - |> strip_first_name_sep |> fst |> space_explode "@" - |> hd |> Int.fromString |> the - in [k, num_binder_types T - k] end - else if original_name s <> s then - [num_binder_types T] - else case def_of_const thy def_table x of - SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then - let val k = length (strip_abs_vars t') in - [k, num_binder_types T - k] - end - else - [num_binder_types T] - | NONE => [num_binder_types T] -(* int list -> int list -> int list *) -fun intersect_formats _ [] = [] - | intersect_formats [] _ = [] - | intersect_formats ks1 ks2 = - let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in - intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else [])) - (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @ - [Int.min (k1, k2)] - end - -(* theory -> const_table -> (term option * int list) list -> term -> int list *) -fun lookup_format thy def_table formats t = - case AList.lookup (fn (SOME x, SOME y) => - (term_match thy) (x, y) | _ => false) - formats (SOME t) of - SOME format => format - | NONE => let val format = the (AList.lookup (op =) formats NONE) in - case t of - Const x => intersect_formats format - (const_format thy def_table x) - | _ => format - end - -(* int list -> int list -> typ -> typ *) -fun format_type default_format format T = - let - val T = uniterize_unarize_unbox_etc_type T - val format = format |> filter (curry (op <) 0) - in - if forall (curry (op =) 1) format then - T - else - let - val (binder_Ts, body_T) = strip_type T - val batched = - binder_Ts - |> map (format_type default_format default_format) - |> rev |> chunk_list_unevenly (rev format) - |> map (HOLogic.mk_tupleT o rev) - in List.foldl (op -->) body_T batched end - end -(* theory -> const_table -> (term option * int list) list -> term -> typ *) -fun format_term_type thy def_table formats t = - format_type (the (AList.lookup (op =) formats NONE)) - (lookup_format thy def_table formats t) (fastype_of t) - -(* int list -> int -> int list -> int list *) -fun repair_special_format js m format = - m - 1 downto 0 |> chunk_list_unevenly (rev format) - |> map (rev o filter_out (member (op =) js)) - |> filter_out null |> map length |> rev - -(* hol_context -> string * string -> (term option * int list) list - -> styp -> term * typ *) -fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...} - : hol_context) (base_name, step_name) formats = - let - val default_format = the (AList.lookup (op =) formats NONE) - (* styp -> term * typ *) - fun do_const (x as (s, T)) = - (if String.isPrefix special_prefix s then - let - (* term -> term *) - val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t') - val (x' as (_, T'), js, ts) = - AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T) - |> the_single - val max_j = List.last js - val Ts = List.take (binder_types T', max_j + 1) - val missing_js = filter_out (member (op =) js) (0 upto max_j) - val missing_Ts = filter_indices missing_js Ts - (* int -> indexname *) - fun nth_missing_var n = - ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n) - val missing_vars = map nth_missing_var (0 upto length missing_js - 1) - val vars = special_bounds ts @ missing_vars - val ts' = - map (fn j => - case AList.lookup (op =) (js ~~ ts) j of - SOME t => do_term t - | NONE => - Var (nth missing_vars - (find_index (curry (op =) j) missing_js))) - (0 upto max_j) - val t = do_const x' |> fst - val format = - case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2) - | _ => false) formats (SOME t) of - SOME format => - repair_special_format js (num_binder_types T') format - | NONE => - const_format thy def_table x' - |> repair_special_format js (num_binder_types T') - |> intersect_formats default_format - in - (list_comb (t, ts') |> fold_rev abs_var vars, - format_type default_format format T) - end - else if String.isPrefix uncurry_prefix s then - let - val (ss, s') = unprefix uncurry_prefix s - |> strip_first_name_sep |>> space_explode "@" - in - if String.isPrefix step_prefix s' then - do_const (s', T) - else - let - val k = the (Int.fromString (hd ss)) - val j = the (Int.fromString (List.last ss)) - val (before_Ts, (tuple_T, rest_T)) = - strip_n_binders j T ||> (strip_n_binders 1 #>> hd) - val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T - in do_const (s', T') end - end - else if String.isPrefix unrolled_prefix s then - let val t = Const (original_name s, range_type T) in - (lambda (Free (iter_var_prefix, nat_T)) t, - format_type default_format - (lookup_format thy def_table formats t) T) - end - else if String.isPrefix base_prefix s then - (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T), - format_type default_format default_format T) - else if String.isPrefix step_prefix s then - (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T), - format_type default_format default_format T) - else if String.isPrefix quot_normal_prefix s then - let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in - (t, format_term_type thy def_table formats t) - end - else if String.isPrefix skolem_prefix s then - let - val ss = the (AList.lookup (op =) (!skolems) s) - val (Ts, Ts') = chop (length ss) (binder_types T) - val frees = map Free (ss ~~ Ts) - val s' = original_name s - in - (fold lambda frees (Const (s', Ts' ---> T)), - format_type default_format - (lookup_format thy def_table formats (Const x)) T) - end - else if String.isPrefix eval_prefix s then - let - val t = nth evals (the (Int.fromString (unprefix eval_prefix s))) - in (t, format_term_type thy def_table formats t) end - else if s = @{const_name undefined_fast_The} then - (Const (nitpick_prefix ^ "The fallback", T), - format_type default_format - (lookup_format thy def_table formats - (Const (@{const_name The}, (T --> bool_T) --> T))) T) - else if s = @{const_name undefined_fast_Eps} then - (Const (nitpick_prefix ^ "Eps fallback", T), - format_type default_format - (lookup_format thy def_table formats - (Const (@{const_name Eps}, (T --> bool_T) --> T))) T) - else - let val t = Const (original_name s, T) in - (t, format_term_type thy def_table formats t) - end) - |>> map_types uniterize_unarize_unbox_etc_type - |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name - in do_const end - -(* styp -> string *) -fun assign_operator_for_const (s, T) = - if String.isPrefix ubfp_prefix s then - if is_fun_type T then "\" else "\" - else if String.isPrefix lbfp_prefix s then - if is_fun_type T then "\" else "\" - else if original_name s <> s then - assign_operator_for_const (after_name_sep s, T) - else - "=" - end; diff -r 428284ee1465 -r eee1a5e0d334 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 11 16:56:22 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Thu Mar 11 17:48:07 2010 +0100 @@ -72,6 +72,7 @@ val base_mixfix = "_\<^bsub>base\<^esub>" val step_mixfix = "_\<^bsub>step\<^esub>" val abs_mixfix = "\_\" +val arg_var_prefix = "x" val cyclic_co_val_name = "\" val cyclic_const_prefix = "\" val cyclic_type_name = nitpick_prefix ^ cyclic_const_prefix @@ -80,6 +81,31 @@ type atom_pool = ((string * int) * int list) list +(* Proof.context -> ((string * string) * (string * string)) * Proof.context *) +fun add_wacky_syntax ctxt = + let + (* term -> string *) + val name_of = fst o dest_Const + val thy = ProofContext.theory_of ctxt |> Context.reject_draft + val (maybe_t, thy) = + Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), + Mixfix (maybe_mixfix, [1000], 1000)) thy + val (abs_t, thy) = + Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), + Mixfix (abs_mixfix, [40], 40)) thy + val (base_t, thy) = + Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), + Mixfix (base_mixfix, [1000], 1000)) thy + val (step_t, thy) = + Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), + Mixfix (step_mixfix, [1000], 1000)) thy + in + (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), + ProofContext.transfer_syntax thy ctxt) + end + +(** Term reconstruction **) + (* atom_pool Unsynchronized.ref -> string -> int -> int -> string *) fun nth_atom_suffix pool s j k = (case AList.lookup (op =) (!pool) (s, k) of @@ -646,6 +672,211 @@ oooo term_for_rep true [] end +(** Constant postprocessing **) + +(* int -> typ -> typ list *) +fun dest_n_tuple_type 1 T = [T] + | dest_n_tuple_type n (Type (_, [T1, T2])) = + T1 :: dest_n_tuple_type (n - 1) T2 + | dest_n_tuple_type _ T = + raise TYPE ("Nitpick_Model.dest_n_tuple_type", [T], []) + +(* theory -> const_table -> styp -> int list *) +fun const_format thy def_table (x as (s, T)) = + if String.isPrefix unrolled_prefix s then + const_format thy def_table (original_name s, range_type T) + else if String.isPrefix skolem_prefix s then + let + val k = unprefix skolem_prefix s + |> strip_first_name_sep |> fst |> space_explode "@" + |> hd |> Int.fromString |> the + in [k, num_binder_types T - k] end + else if original_name s <> s then + [num_binder_types T] + else case def_of_const thy def_table x of + SOME t' => if fixpoint_kind_of_rhs t' <> NoFp then + let val k = length (strip_abs_vars t') in + [k, num_binder_types T - k] + end + else + [num_binder_types T] + | NONE => [num_binder_types T] +(* int list -> int list -> int list *) +fun intersect_formats _ [] = [] + | intersect_formats [] _ = [] + | intersect_formats ks1 ks2 = + let val ((ks1', k1), (ks2', k2)) = pairself split_last (ks1, ks2) in + intersect_formats (ks1' @ (if k1 > k2 then [k1 - k2] else [])) + (ks2' @ (if k2 > k1 then [k2 - k1] else [])) @ + [Int.min (k1, k2)] + end + +(* theory -> const_table -> (term option * int list) list -> term -> int list *) +fun lookup_format thy def_table formats t = + case AList.lookup (fn (SOME x, SOME y) => + (term_match thy) (x, y) | _ => false) + formats (SOME t) of + SOME format => format + | NONE => let val format = the (AList.lookup (op =) formats NONE) in + case t of + Const x => intersect_formats format + (const_format thy def_table x) + | _ => format + end + +(* int list -> int list -> typ -> typ *) +fun format_type default_format format T = + let + val T = uniterize_unarize_unbox_etc_type T + val format = format |> filter (curry (op <) 0) + in + if forall (curry (op =) 1) format then + T + else + let + val (binder_Ts, body_T) = strip_type T + val batched = + binder_Ts + |> map (format_type default_format default_format) + |> rev |> chunk_list_unevenly (rev format) + |> map (HOLogic.mk_tupleT o rev) + in List.foldl (op -->) body_T batched end + end +(* theory -> const_table -> (term option * int list) list -> term -> typ *) +fun format_term_type thy def_table formats t = + format_type (the (AList.lookup (op =) formats NONE)) + (lookup_format thy def_table formats t) (fastype_of t) + +(* int list -> int -> int list -> int list *) +fun repair_special_format js m format = + m - 1 downto 0 |> chunk_list_unevenly (rev format) + |> map (rev o filter_out (member (op =) js)) + |> filter_out null |> map length |> rev + +(* hol_context -> string * string -> (term option * int list) list + -> styp -> term * typ *) +fun user_friendly_const ({thy, evals, def_table, skolems, special_funs, ...} + : hol_context) (base_name, step_name) formats = + let + val default_format = the (AList.lookup (op =) formats NONE) + (* styp -> term * typ *) + fun do_const (x as (s, T)) = + (if String.isPrefix special_prefix s then + let + (* term -> term *) + val do_term = map_aterms (fn Const x => fst (do_const x) | t' => t') + val (x' as (_, T'), js, ts) = + AList.find (op =) (!special_funs) (s, unarize_unbox_etc_type T) + |> the_single + val max_j = List.last js + val Ts = List.take (binder_types T', max_j + 1) + val missing_js = filter_out (member (op =) js) (0 upto max_j) + val missing_Ts = filter_indices missing_js Ts + (* int -> indexname *) + fun nth_missing_var n = + ((arg_var_prefix ^ nat_subscript (n + 1), 0), nth missing_Ts n) + val missing_vars = map nth_missing_var (0 upto length missing_js - 1) + val vars = special_bounds ts @ missing_vars + val ts' = + map (fn j => + case AList.lookup (op =) (js ~~ ts) j of + SOME t => do_term t + | NONE => + Var (nth missing_vars + (find_index (curry (op =) j) missing_js))) + (0 upto max_j) + val t = do_const x' |> fst + val format = + case AList.lookup (fn (SOME t1, SOME t2) => term_match thy (t1, t2) + | _ => false) formats (SOME t) of + SOME format => + repair_special_format js (num_binder_types T') format + | NONE => + const_format thy def_table x' + |> repair_special_format js (num_binder_types T') + |> intersect_formats default_format + in + (list_comb (t, ts') |> fold_rev abs_var vars, + format_type default_format format T) + end + else if String.isPrefix uncurry_prefix s then + let + val (ss, s') = unprefix uncurry_prefix s + |> strip_first_name_sep |>> space_explode "@" + in + if String.isPrefix step_prefix s' then + do_const (s', T) + else + let + val k = the (Int.fromString (hd ss)) + val j = the (Int.fromString (List.last ss)) + val (before_Ts, (tuple_T, rest_T)) = + strip_n_binders j T ||> (strip_n_binders 1 #>> hd) + val T' = before_Ts ---> dest_n_tuple_type k tuple_T ---> rest_T + in do_const (s', T') end + end + else if String.isPrefix unrolled_prefix s then + let val t = Const (original_name s, range_type T) in + (lambda (Free (iter_var_prefix, nat_T)) t, + format_type default_format + (lookup_format thy def_table formats t) T) + end + else if String.isPrefix base_prefix s then + (Const (base_name, T --> T) $ Const (unprefix base_prefix s, T), + format_type default_format default_format T) + else if String.isPrefix step_prefix s then + (Const (step_name, T --> T) $ Const (unprefix step_prefix s, T), + format_type default_format default_format T) + else if String.isPrefix quot_normal_prefix s then + let val t = Const (nitpick_prefix ^ "normalize quotient type", T) in + (t, format_term_type thy def_table formats t) + end + else if String.isPrefix skolem_prefix s then + let + val ss = the (AList.lookup (op =) (!skolems) s) + val (Ts, Ts') = chop (length ss) (binder_types T) + val frees = map Free (ss ~~ Ts) + val s' = original_name s + in + (fold lambda frees (Const (s', Ts' ---> T)), + format_type default_format + (lookup_format thy def_table formats (Const x)) T) + end + else if String.isPrefix eval_prefix s then + let + val t = nth evals (the (Int.fromString (unprefix eval_prefix s))) + in (t, format_term_type thy def_table formats t) end + else if s = @{const_name undefined_fast_The} then + (Const (nitpick_prefix ^ "The fallback", T), + format_type default_format + (lookup_format thy def_table formats + (Const (@{const_name The}, (T --> bool_T) --> T))) T) + else if s = @{const_name undefined_fast_Eps} then + (Const (nitpick_prefix ^ "Eps fallback", T), + format_type default_format + (lookup_format thy def_table formats + (Const (@{const_name Eps}, (T --> bool_T) --> T))) T) + else + let val t = Const (original_name s, T) in + (t, format_term_type thy def_table formats t) + end) + |>> map_types uniterize_unarize_unbox_etc_type + |>> shorten_names_in_term |>> Term.map_abs_vars shortest_name + in do_const end + +(* styp -> string *) +fun assign_operator_for_const (s, T) = + if String.isPrefix ubfp_prefix s then + if is_fun_type T then "\" else "\" + else if String.isPrefix lbfp_prefix s then + if is_fun_type T then "\" else "\" + else if original_name s <> s then + assign_operator_for_const (strip_first_name_sep s |> snd, T) + else + "=" + +(** Model reconstruction **) + (* atom_pool -> scope -> nut list -> nut NameTable.table -> KK.raw_bound list -> nut -> term *) fun term_for_name pool scope sel_names rel_table bounds name = @@ -655,29 +886,6 @@ rel_table bounds T T (rep_of name) end -(* Proof.context -> ((string * string) * (string * string)) * Proof.context *) -fun add_wacky_syntax ctxt = - let - (* term -> string *) - val name_of = fst o dest_Const - val thy = ProofContext.theory_of ctxt |> Context.reject_draft - val (maybe_t, thy) = - Sign.declare_const ((@{binding nitpick_maybe}, @{typ "'a => 'a"}), - Mixfix (maybe_mixfix, [1000], 1000)) thy - val (abs_t, thy) = - Sign.declare_const ((@{binding nitpick_abs}, @{typ "'a => 'b"}), - Mixfix (abs_mixfix, [40], 40)) thy - val (base_t, thy) = - Sign.declare_const ((@{binding nitpick_base}, @{typ "'a => 'a"}), - Mixfix (base_mixfix, [1000], 1000)) thy - val (step_t, thy) = - Sign.declare_const ((@{binding nitpick_step}, @{typ "'a => 'a"}), - Mixfix (step_mixfix, [1000], 1000)) thy - in - (pairself (pairself name_of) ((maybe_t, abs_t), (base_t, step_t)), - ProofContext.transfer_syntax thy ctxt) - end - (* term -> term *) fun unfold_outer_the_binders (t as Const (@{const_name The}, _) $ Abs (s, T, Const (@{const_name "op ="}, _) diff -r 428284ee1465 -r eee1a5e0d334 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 11 16:56:22 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Mar 11 17:48:07 2010 +0100 @@ -33,27 +33,40 @@ binary coding. *) val binary_int_threshold = 3 +(* bool -> term -> bool *) +val may_use_binary_ints = + let + (* bool -> term -> bool *) + fun aux def (Const (@{const_name "=="}, _) $ t1 $ t2) = + aux def t1 andalso aux false t2 + | aux def (@{const "==>"} $ t1 $ t2) = aux false t1 andalso aux def t2 + | aux def (Const (@{const_name "op ="}, _) $ t1 $ t2) = + aux def t1 andalso aux false t2 + | aux def (@{const "op -->"} $ t1 $ t2) = aux false t1 andalso aux def t2 + | aux def (t1 $ t2) = aux def t1 andalso aux def t2 + | aux def (t as Const (s, _)) = + (not def orelse t <> @{const Suc}) andalso + not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, + @{const_name nat_gcd}, @{const_name nat_lcm}, + @{const_name Frac}, @{const_name norm_frac}] s) + | aux def (Abs (_, _, t')) = aux def t' + | aux _ _ = true + in aux end (* term -> bool *) -fun may_use_binary_ints (t1 $ t2) = - may_use_binary_ints t1 andalso may_use_binary_ints t2 - | may_use_binary_ints (t as Const (s, _)) = - t <> @{const Suc} andalso - not (member (op =) [@{const_name Abs_Frac}, @{const_name Rep_Frac}, - @{const_name nat_gcd}, @{const_name nat_lcm}, - @{const_name Frac}, @{const_name norm_frac}] s) - | may_use_binary_ints (Abs (_, _, t')) = may_use_binary_ints t' - | may_use_binary_ints _ = true -fun should_use_binary_ints (t1 $ t2) = - should_use_binary_ints t1 orelse should_use_binary_ints t2 - | should_use_binary_ints (Const (s, T)) = - ((s = @{const_name times} orelse s = @{const_name div}) andalso - is_integer_type (body_type T)) orelse - (String.isPrefix numeral_prefix s andalso - let val n = the (Int.fromString (unprefix numeral_prefix s)) in - n < ~ binary_int_threshold orelse n > binary_int_threshold - end) - | should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t' - | should_use_binary_ints _ = false +val should_use_binary_ints = + let + (* term -> bool *) + fun aux (t1 $ t2) = aux t1 orelse aux t2 + | aux (Const (s, T)) = + ((s = @{const_name times} orelse s = @{const_name div}) andalso + is_integer_type (body_type T)) orelse + (String.isPrefix numeral_prefix s andalso + let val n = the (Int.fromString (unprefix numeral_prefix s)) in + n < ~ binary_int_threshold orelse n > binary_int_threshold + end) + | aux (Abs (_, _, t')) = aux t' + | aux _ = false + in aux end (** Uncurrying **) @@ -1369,7 +1382,8 @@ is_standard_datatype thy stds nat_T andalso case binary_ints of SOME false => false - | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso + | _ => forall (may_use_binary_ints false) nondef_ts andalso + forall (may_use_binary_ints true) def_ts andalso (binary_ints = SOME true orelse exists should_use_binary_ints (nondef_ts @ def_ts)) val box = exists (not_equal (SOME false) o snd) boxes