1.1 --- a/doc-src/Nitpick/nitpick.tex Fri Feb 26 13:29:43 2010 +0100
1.2 +++ b/doc-src/Nitpick/nitpick.tex Fri Feb 26 16:50:09 2010 +0100
1.3 @@ -472,7 +472,7 @@
1.4 \prew
1.5 \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\
1.6 \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount]
1.7 -\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported
1.8 +\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported
1.9 fragment. Only potential counterexamples may be found. \\[2\smallskipamount]
1.10 Nitpick found a potential counterexample: \\[2\smallskipamount]
1.11 \hbox{}\qquad Free variable: \nopagebreak \\
1.12 @@ -2743,8 +2743,8 @@
1.13 \item[$\bullet$] Although this has never been observed, arbitrary theorem
1.14 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples.
1.15
1.16 -%\item[$\bullet$] All constants and types whose names start with
1.17 -%\textit{Nitpick}{.} are reserved for internal use.
1.18 +\item[$\bullet$] All constants, types, free variables, and schematic variables
1.19 +whose names start with \textit{Nitpick}{.} are reserved for internal use.
1.20 \end{enum}
1.21
1.22 \let\em=\sl
2.1 --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Feb 26 13:29:43 2010 +0100
2.2 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Feb 26 16:50:09 2010 +0100
2.3 @@ -1000,7 +1000,7 @@
2.4 oops
2.5
2.6 lemma "(Q\<Colon>nat set) (Eps Q)"
2.7 -nitpick [expect = none]
2.8 +nitpick [expect = none] (* unfortunate *)
2.9 oops
2.10
2.11 lemma "\<not> Q (Eps Q)"
2.12 @@ -1053,11 +1053,11 @@
2.13
2.14 lemma "Q = {x\<Colon>'a} \<Longrightarrow> (Q\<Colon>'a set) (The Q)"
2.15 nitpick [expect = none]
2.16 -oops
2.17 +sorry
2.18
2.19 lemma "Q = {x\<Colon>nat} \<Longrightarrow> (Q\<Colon>nat set) (The Q)"
2.20 nitpick [expect = none]
2.21 -oops
2.22 +sorry
2.23
2.24 subsection {* Destructors and Recursors *}
2.25
3.1 --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Feb 26 13:29:43 2010 +0100
3.2 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Feb 26 16:50:09 2010 +0100
3.3 @@ -69,7 +69,7 @@
3.4 oops
3.5
3.6 lemma "fs (Pd ((a, b), (c, d))) = (a, b)"
3.7 -nitpick [card = 1\<midarrow>10, expect = none]
3.8 +nitpick [card = 1\<midarrow>9, expect = none]
3.9 sorry
3.10
3.11 lemma "fs (Pd ((a, b), (c, d))) = (c, d)"
4.1 --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 13:29:43 2010 +0100
4.2 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 16:50:09 2010 +0100
4.3 @@ -30,8 +30,7 @@
4.4 special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [],
4.5 wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []}
4.6 (* term -> bool *)
4.7 -val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a}
4.8 - Nitpick_Mono.Plus [] []
4.9 +fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], [])
4.10 fun is_const t =
4.11 let val T = fastype_of t in
4.12 is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t),
4.13 @@ -47,26 +46,26 @@
4.14 ML {* const @{term "(A::'a set) = A"} *}
4.15 ML {* const @{term "(A::'a set set) = A"} *}
4.16 ML {* const @{term "(\<lambda>x::'a set. x a)"} *}
4.17 -ML {* const @{term "{{a}} = C"} *}
4.18 +ML {* const @{term "{{a::'a}} = C"} *}
4.19 ML {* const @{term "{f::'a\<Rightarrow>nat} = {g::'a\<Rightarrow>nat}"} *}
4.20 -ML {* const @{term "A \<union> B"} *}
4.21 +ML {* const @{term "A \<union> (B::'a set)"} *}
4.22 ML {* const @{term "P (a::'a)"} *}
4.23 ML {* const @{term "\<lambda>a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *}
4.24 ML {* const @{term "\<forall>A::'a set. A a"} *}
4.25 ML {* const @{term "\<forall>A::'a set. P A"} *}
4.26 ML {* const @{term "P \<or> Q"} *}
4.27 -ML {* const @{term "A \<union> B = C"} *}
4.28 +ML {* const @{term "A \<union> B = (C::'a set)"} *}
4.29 ML {* const @{term "(if P then (A::'a set) else B) = C"} *}
4.30 -ML {* const @{term "let A = C in A \<union> B"} *}
4.31 +ML {* const @{term "let A = (C::'a set) in A \<union> B"} *}
4.32 ML {* const @{term "THE x::'b. P x"} *}
4.33 -ML {* const @{term "{}::'a set"} *}
4.34 +ML {* const @{term "(\<lambda>x::'a. False)"} *}
4.35 ML {* const @{term "(\<lambda>x::'a. True)"} *}
4.36 -ML {* const @{term "Let a A"} *}
4.37 +ML {* const @{term "Let (a::'a) A"} *}
4.38 ML {* const @{term "A (a::'a)"} *}
4.39 -ML {* const @{term "insert a A = B"} *}
4.40 +ML {* const @{term "insert (a::'a) A = B"} *}
4.41 ML {* const @{term "- (A::'a set)"} *}
4.42 -ML {* const @{term "finite A"} *}
4.43 -ML {* const @{term "\<not> finite A"} *}
4.44 +ML {* const @{term "finite (A::'a set)"} *}
4.45 +ML {* const @{term "\<not> finite (A::'a set)"} *}
4.46 ML {* const @{term "finite (A::'a set set)"} *}
4.47 ML {* const @{term "\<lambda>a::'a. A a \<and> \<not> B a"} *}
4.48 ML {* const @{term "A < (B::'a set)"} *}
4.49 @@ -75,27 +74,25 @@
4.50 ML {* const @{term "[a::'a set]"} *}
4.51 ML {* const @{term "[A \<union> (B::'a set)]"} *}
4.52 ML {* const @{term "[A \<union> (B::'a set)] = [C]"} *}
4.53 -ML {* const @{term "\<forall>P. P a"} *}
4.54
4.55 -ML {* nonconst @{term "{%x. True}"} *}
4.56 -ML {* nonconst @{term "{(%x. x = a)} = C"} *}
4.57 +ML {* nonconst @{term "{(\<lambda>x::'a. x = a)} = C"} *}
4.58 ML {* nonconst @{term "\<forall>P (a::'a). P a"} *}
4.59 ML {* nonconst @{term "\<forall>a::'a. P a"} *}
4.60 ML {* nonconst @{term "(\<lambda>a::'a. \<not> A a) = B"} *}
4.61 -ML {* nonconst @{term "THE x. P x"} *}
4.62 -ML {* nonconst @{term "SOME x. P x"} *}
4.63 +ML {* nonconst @{term "THE x::'a. P x"} *}
4.64 +ML {* nonconst @{term "SOME x::'a. P x"} *}
4.65
4.66 ML {* mono @{prop "Q (\<forall>x::'a set. P x)"} *}
4.67 ML {* mono @{prop "P (a::'a)"} *}
4.68 -ML {* mono @{prop "{a} = {b}"} *}
4.69 +ML {* mono @{prop "{a} = {b::'a}"} *}
4.70 ML {* mono @{prop "P (a::'a) \<and> P \<union> P = P"} *}
4.71 ML {* mono @{prop "\<forall>F::'a set set. P"} *}
4.72 ML {* mono @{prop "\<not> (\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h)"} *}
4.73 ML {* mono @{prop "\<not> Q (\<forall>x::'a set. P x)"} *}
4.74 -ML {* mono @{prop "\<not> (\<forall>x. P x)"} *}
4.75 +ML {* mono @{prop "\<not> (\<forall>x::'a. P x)"} *}
4.76
4.77 -ML {* nonmono @{prop "\<forall>x. P x"} *}
4.78 +ML {* nonmono @{prop "\<forall>x::'a. P x"} *}
4.79 +ML {* nonmono @{prop "myall P = (P = (\<lambda>x::'a. True))"} *}
4.80 ML {* nonmono @{prop "\<forall>F f g (h::'a set). F f \<and> F g \<and> \<not> f a \<and> g a \<longrightarrow> F h"} *}
4.81 -ML {* nonmono @{prop "myall P = (P = (\<lambda>x. True))"} *}
4.82
4.83 end
5.1 --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 13:29:43 2010 +0100
5.2 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 16:50:09 2010 +0100
5.3 @@ -64,7 +64,7 @@
5.4 oops
5.5
5.6 lemma "x \<noteq> (y\<Colon>bool bounded) \<Longrightarrow> z = x \<or> z = y"
5.7 -nitpick [expect = none]
5.8 +nitpick [fast_descrs (* ### FIXME *), expect = none]
5.9 sorry
5.10
5.11 lemma "x \<noteq> (y\<Colon>(bool \<times> bool) bounded) \<Longrightarrow> z = x \<or> z = y"
6.1 --- a/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 13:29:43 2010 +0100
6.2 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 16:50:09 2010 +0100
6.3 @@ -4,7 +4,11 @@
6.4 * Added "std" option and implemented support for nonstandard models
6.5 * Added support for quotient types
6.6 * Added support for local definitions
6.7 - * Optimized "Multiset.multiset"
6.8 + * Disabled "fast_descrs" option by default
6.9 + * Optimized "Multiset.multiset" and "FinFun.finfun"
6.10 + * Improved efficiency of "destroy_constrs" optimization
6.11 + * Improved precision of infinite datatypes whose constructors don't appear
6.12 + in the formula to falsify based on a monotonicity analysis
6.13 * Fixed soundness bugs related to "destroy_constrs" optimization and record
6.14 getters
6.15 * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
7.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 13:29:43 2010 +0100
7.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 16:50:09 2010 +0100
7.3 @@ -131,9 +131,7 @@
7.4 nonsel_names: nut list,
7.5 rel_table: nut NameTable.table,
7.6 unsound: bool,
7.7 - scope: scope,
7.8 - core: KK.formula,
7.9 - defs: KK.formula list}
7.10 + scope: scope}
7.11
7.12 type rich_problem = KK.problem * problem_extension
7.13
7.14 @@ -195,7 +193,8 @@
7.15 val timer = Timer.startRealTimer ()
7.16 val thy = Proof.theory_of state
7.17 val ctxt = Proof.context_of state
7.18 -(* FIXME: reintroduce code before new release
7.19 +(* FIXME: reintroduce code before new release:
7.20 +
7.21 val nitpick_thy = ThyInfo.get_theory "Nitpick"
7.22 val _ = Theory.subthy (nitpick_thy, thy) orelse
7.23 error "You must import the theory \"Nitpick\" to use Nitpick"
7.24 @@ -289,8 +288,8 @@
7.25 val frees = Term.add_frees assms_t []
7.26 val _ = null (Term.add_tvars assms_t []) orelse
7.27 raise NOT_SUPPORTED "schematic type variables"
7.28 - val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
7.29 - core_t, binarize) = preprocess_term hol_ctxt assms_t
7.30 + val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
7.31 + binarize) = preprocess_term hol_ctxt assms_t
7.32 val got_all_user_axioms =
7.33 got_all_mono_user_axioms andalso no_poly_user_axioms
7.34
7.35 @@ -307,54 +306,66 @@
7.36 \unroll it.")))
7.37 val _ = if verbose then List.app print_wf (!wf_cache) else ()
7.38 val _ =
7.39 - pprint_d (fn () =>
7.40 - Pretty.chunks
7.41 - (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
7.42 - pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
7.43 - pretties_for_formulas ctxt "Relevant nondefinitional axiom"
7.44 - nondef_ts))
7.45 - val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
7.46 + pprint_d (fn () => Pretty.chunks
7.47 + (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
7.48 + pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
7.49 + pretties_for_formulas ctxt "Relevant nondefinitional axiom"
7.50 + (tl nondef_ts)))
7.51 + val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
7.52 handle TYPE (_, Ts, ts) =>
7.53 raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
7.54
7.55 - val core_u = nut_from_term hol_ctxt Eq core_t
7.56 + val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
7.57 val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
7.58 - val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
7.59 val (free_names, const_names) =
7.60 - fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
7.61 + fold add_free_and_const_names (nondef_us @ def_us) ([], [])
7.62 val (sel_names, nonsel_names) =
7.63 List.partition (is_sel o nickname_of) const_names
7.64 val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
7.65 val standard = forall snd stds
7.66 (*
7.67 - val _ = List.app (priority o string_for_nut ctxt)
7.68 - (core_u :: def_us @ nondef_us)
7.69 + val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
7.70 *)
7.71
7.72 val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
7.73 + (* typ list -> string -> string *)
7.74 + fun monotonicity_message Ts extra =
7.75 + let val ss = map (quote o string_for_type ctxt) Ts in
7.76 + "The type" ^ plural_s_for_list ss ^ " " ^
7.77 + space_implode " " (serial_commas "and" ss) ^ " " ^
7.78 + (if none_true monos then
7.79 + "passed the monotonicity test"
7.80 + else
7.81 + (if length ss = 1 then "is" else "are") ^ " considered monotonic") ^
7.82 + ". " ^ extra
7.83 + end
7.84 (* typ -> bool *)
7.85 fun is_type_always_monotonic T =
7.86 (is_datatype thy stds T andalso not (is_quot_type thy T) andalso
7.87 (not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
7.88 is_number_type thy T orelse is_bit_type T
7.89 + fun is_type_actually_monotonic T =
7.90 + formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
7.91 fun is_type_monotonic T =
7.92 unique_scope orelse
7.93 case triple_lookup (type_match thy) monos T of
7.94 SOME (SOME b) => b
7.95 - | _ => is_type_always_monotonic T orelse
7.96 - formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t
7.97 - fun is_deep_datatype T =
7.98 - is_datatype thy stds T andalso
7.99 - (not standard orelse T = nat_T orelse is_word_type T orelse
7.100 - exists (curry (op =) T o domain_type o type_of) sel_names)
7.101 - val all_Ts = ground_types_in_terms hol_ctxt binarize
7.102 - (core_t :: def_ts @ nondef_ts)
7.103 + | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T
7.104 + fun is_type_finitizable T =
7.105 + case triple_lookup (type_match thy) monos T of
7.106 + SOME (SOME false) => false
7.107 + | _ => is_type_actually_monotonic T
7.108 + fun is_datatype_deep T =
7.109 + not standard orelse T = nat_T orelse is_word_type T orelse
7.110 + exists (curry (op =) T o domain_type o type_of) sel_names
7.111 + val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
7.112 |> sort TermOrd.typ_ord
7.113 val _ = if verbose andalso binary_ints = SOME true andalso
7.114 exists (member (op =) [nat_T, int_T]) all_Ts then
7.115 print_v (K "The option \"binary_ints\" will be ignored because \
7.116 \of the presence of rationals, reals, \"Suc\", \
7.117 - \\"gcd\", or \"lcm\" in the problem.")
7.118 + \\"gcd\", or \"lcm\" in the problem or because of the \
7.119 + \\"non_std\" option.")
7.120 else
7.121 ()
7.122 val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
7.123 @@ -363,23 +374,21 @@
7.124 case filter_out is_type_always_monotonic mono_Ts of
7.125 [] => ()
7.126 | interesting_mono_Ts =>
7.127 - print_v (fn () =>
7.128 - let
7.129 - val ss = map (quote o string_for_type ctxt)
7.130 - interesting_mono_Ts
7.131 - in
7.132 - "The type" ^ plural_s_for_list ss ^ " " ^
7.133 - space_implode " " (serial_commas "and" ss) ^ " " ^
7.134 - (if none_true monos then
7.135 - "passed the monotonicity test"
7.136 - else
7.137 - (if length ss = 1 then "is" else "are") ^
7.138 - " considered monotonic") ^
7.139 - ". Nitpick might be able to skip some scopes."
7.140 - end)
7.141 + print_v (K (monotonicity_message interesting_mono_Ts
7.142 + "Nitpick might be able to skip some scopes."))
7.143 else
7.144 ()
7.145 - val deep_dataTs = filter is_deep_datatype all_Ts
7.146 + val (deep_dataTs, shallow_dataTs) =
7.147 + all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep
7.148 + val finitizable_dataTs =
7.149 + shallow_dataTs |> filter_out (is_finite_type hol_ctxt)
7.150 + |> filter is_type_finitizable
7.151 + val _ =
7.152 + if verbose andalso not (null finitizable_dataTs) then
7.153 + print_v (K (monotonicity_message finitizable_dataTs
7.154 + "Nitpick can use a more precise finite encoding."))
7.155 + else
7.156 + ()
7.157 (* This detection code is an ugly hack. Fortunately, it is used only to
7.158 provide a hint to the user. *)
7.159 (* string * (Rule_Cases.T * bool) -> bool *)
7.160 @@ -446,7 +455,7 @@
7.161 string_of_int j0))
7.162 (Typtab.dest ofs)
7.163 *)
7.164 - val all_exact = forall (is_exact_type datatypes) all_Ts
7.165 + val all_exact = forall (is_exact_type datatypes true) all_Ts
7.166 (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *)
7.167 val repify_consts = choose_reps_for_consts scope all_exact
7.168 val main_j0 = offset_of_type ofs bool_T
7.169 @@ -467,7 +476,6 @@
7.170 (univ_card nat_card int_card main_j0 [] KK.True)
7.171 val _ = check_arity min_univ_card min_highest_arity
7.172
7.173 - val core_u = choose_reps_in_nut scope unsound rep_table false core_u
7.174 val def_us = map (choose_reps_in_nut scope unsound rep_table true)
7.175 def_us
7.176 val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
7.177 @@ -475,7 +483,7 @@
7.178 (*
7.179 val _ = List.app (priority o string_for_nut ctxt)
7.180 (free_names @ sel_names @ nonsel_names @
7.181 - core_u :: def_us @ nondef_us)
7.182 + nondef_us @ def_us)
7.183 *)
7.184 val (free_rels, pool, rel_table) =
7.185 rename_free_vars free_names initial_pool NameTable.empty
7.186 @@ -483,13 +491,11 @@
7.187 rename_free_vars sel_names pool rel_table
7.188 val (other_rels, pool, rel_table) =
7.189 rename_free_vars nonsel_names pool rel_table
7.190 - val core_u = rename_vars_in_nut pool rel_table core_u
7.191 + val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
7.192 val def_us = map (rename_vars_in_nut pool rel_table) def_us
7.193 - val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
7.194 - val core_f = kodkod_formula_from_nut ofs kk core_u
7.195 + val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
7.196 val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
7.197 - val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
7.198 - val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
7.199 + val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
7.200 val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
7.201 PrintMode.setmp [] multiline_string_for_scope scope
7.202 val kodkod_sat_solver =
7.203 @@ -537,8 +543,7 @@
7.204 expr_assigns = [], formula = formula},
7.205 {free_names = free_names, sel_names = sel_names,
7.206 nonsel_names = nonsel_names, rel_table = rel_table,
7.207 - unsound = unsound, scope = scope, core = core_f,
7.208 - defs = nondef_fs @ def_fs @ declarative_axioms})
7.209 + unsound = unsound, scope = scope})
7.210 end
7.211 handle TOO_LARGE (loc, msg) =>
7.212 if loc = "Nitpick_Kodkod.check_arity" andalso
7.213 @@ -834,8 +839,8 @@
7.214 sound_problems then
7.215 print_m (fn () =>
7.216 "Warning: The conjecture either trivially holds for the \
7.217 - \given scopes or (more likely) lies outside Nitpick's \
7.218 - \supported fragment." ^
7.219 + \given scopes or lies outside Nitpick's supported \
7.220 + \fragment." ^
7.221 (if exists (not o KK.is_problem_trivially_false o fst)
7.222 unsound_problems then
7.223 " Only potential counterexamples may be found."
7.224 @@ -907,6 +912,7 @@
7.225 val (skipped, the_scopes) =
7.226 all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns
7.227 iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs
7.228 + finitizable_dataTs
7.229 val _ = if skipped > 0 then
7.230 print_m (fn () => "Too many scopes. Skipping " ^
7.231 string_of_int skipped ^ " scope" ^
8.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 13:29:43 2010 +0100
8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 16:50:09 2010 +0100
8.3 @@ -151,9 +151,10 @@
8.4 val card_of_type : (typ * int) list -> typ -> int
8.5 val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int
8.6 val bounded_exact_card_of_type :
8.7 - hol_context -> int -> int -> (typ * int) list -> typ -> int
8.8 + hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int
8.9 val is_finite_type : hol_context -> typ -> bool
8.10 val special_bounds : term list -> (indexname * typ) list
8.11 + val abs_var : indexname * typ -> term -> term
8.12 val is_funky_typedef : theory -> typ -> bool
8.13 val all_axioms_of :
8.14 theory -> (term * term) list -> term list * term list * term list
8.15 @@ -631,8 +632,13 @@
8.16 in
8.17 case t_opt of
8.18 SOME (Const (@{const_name top}, _)) => true
8.19 + (* "Multiset.multiset" *)
8.20 | SOME (Const (@{const_name Collect}, _)
8.21 $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true
8.22 + (* "FinFun.finfun" *)
8.23 + | SOME (Const (@{const_name Collect}, _) $ Abs (_, _,
8.24 + Const (@{const_name Ex}, _) $ Abs (_, _,
8.25 + Const (@{const_name finite}, _) $ _))) => true
8.26 | _ => false
8.27 end
8.28 | NONE => false)
8.29 @@ -1047,13 +1053,16 @@
8.30 card_of_type assigns T
8.31 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
8.32 default_card)
8.33 -(* hol_context -> int -> (typ * int) list -> typ -> int *)
8.34 -fun bounded_exact_card_of_type hol_ctxt max default_card assigns T =
8.35 +(* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *)
8.36 +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card
8.37 + assigns T =
8.38 let
8.39 (* typ list -> typ -> int *)
8.40 fun aux avoid T =
8.41 (if member (op =) avoid T then
8.42 0
8.43 + else if member (op =) finitizable_dataTs T then
8.44 + raise SAME ()
8.45 else case T of
8.46 Type ("fun", [T1, T2]) =>
8.47 let
8.48 @@ -1096,8 +1105,8 @@
8.49 in Int.min (max, aux [] T) end
8.50
8.51 (* hol_context -> typ -> bool *)
8.52 -fun is_finite_type hol_ctxt =
8.53 - not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 []
8.54 +fun is_finite_type hol_ctxt T =
8.55 + bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0
8.56
8.57 (* term -> bool *)
8.58 fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2
9.1 --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 26 13:29:43 2010 +0100
9.2 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 26 16:50:09 2010 +0100
9.3 @@ -255,10 +255,10 @@
9.4 ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div)
9.5 else if x = nat_less_rel then
9.6 ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0)
9.7 - (int_for_bool o op <))
9.8 + (int_from_bool o op <))
9.9 else if x = int_less_rel then
9.10 ("int_less", tabulate_int_op2 debug univ_card (int_card, j0)
9.11 - (int_for_bool o op <))
9.12 + (int_from_bool o op <))
9.13 else if x = gcd_rel then
9.14 ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd)
9.15 else if x = lcm_rel then
9.16 @@ -444,7 +444,7 @@
9.17 single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1
9.18 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr)
9.19 -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *)
9.20 -fun tripl_rel_rel_let kk f r1 r2 r3 =
9.21 +fun triple_rel_rel_let kk f r1 r2 r3 =
9.22 double_rel_rel_let kk
9.23 (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2
9.24
9.25 @@ -1615,7 +1615,7 @@
9.26 kk_rel_let [to_expr_assign u1 u2] (to_rep R u3)
9.27 | Op3 (If, _, R, u1, u2, u3) =>
9.28 if is_opt_rep (rep_of u1) then
9.29 - tripl_rel_rel_let kk
9.30 + triple_rel_rel_let kk
9.31 (fn r1 => fn r2 => fn r3 =>
9.32 let val empty_r = empty_rel_for_rep R in
9.33 fold1 kk_union
10.1 --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 26 13:29:43 2010 +0100
10.2 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 26 16:50:09 2010 +0100
10.3 @@ -288,7 +288,7 @@
10.4 T1 --> (T1 --> T2) --> T1 --> T2)
10.5 (* (term * term) list -> term *)
10.6 fun aux [] =
10.7 - if maybe_opt andalso not (is_complete_type datatypes T1) then
10.8 + if maybe_opt andalso not (is_complete_type datatypes false T1) then
10.9 insert_const $ Const (unrep, T1) $ empty_const
10.10 else
10.11 empty_const
10.12 @@ -312,7 +312,7 @@
10.13 Const (@{const_name None}, _) => aux' ps
10.14 | _ => update_const $ aux' ps $ t1 $ t2)
10.15 fun aux ps =
10.16 - if not (is_complete_type datatypes T1) then
10.17 + if not (is_complete_type datatypes false T1) then
10.18 update_const $ aux' ps $ Const (unrep, T1)
10.19 $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2'))
10.20 else
10.21 @@ -537,7 +537,7 @@
10.22 val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1
10.23 val ts2 =
10.24 map (fn js => term_for_rep seen T2 T2 (Atom (2, 0))
10.25 - [[int_for_bool (member (op =) jss js)]])
10.26 + [[int_from_bool (member (op =) jss js)]])
10.27 jss1
10.28 in make_fun false T1 T2 T' ts1 ts2 end
10.29 | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss =
10.30 @@ -707,12 +707,13 @@
10.31 Pretty.str "=",
10.32 Pretty.enum "," "{" "}"
10.33 (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @
10.34 - (if complete then [] else [Pretty.str unrep]))])
10.35 + (if fun_from_pair complete false then []
10.36 + else [Pretty.str unrep]))])
10.37 (* typ -> dtype_spec list *)
10.38 fun integer_datatype T =
10.39 [{typ = T, card = card_of_type card_assigns T, co = false,
10.40 - standard = true, complete = false, concrete = true, deep = true,
10.41 - constrs = []}]
10.42 + standard = true, complete = (false, false), concrete = (true, true),
10.43 + deep = true, constrs = []}]
10.44 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => []
10.45 val (codatatypes, datatypes) =
10.46 datatypes |> filter #deep |> List.partition #co
11.1 --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 13:29:43 2010 +0100
11.2 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 16:50:09 2010 +0100
11.3 @@ -2,16 +2,15 @@
11.4 Author: Jasmin Blanchette, TU Muenchen
11.5 Copyright 2009, 2010
11.6
11.7 -Monotonicity predicate for higher-order logic.
11.8 +Monotonicity inference for higher-order logic.
11.9 *)
11.10
11.11 signature NITPICK_MONO =
11.12 sig
11.13 - datatype sign = Plus | Minus
11.14 type hol_context = Nitpick_HOL.hol_context
11.15
11.16 val formulas_monotonic :
11.17 - hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool
11.18 + hol_context -> bool -> typ -> term list * term list -> bool
11.19 end;
11.20
11.21 structure Nitpick_Mono : NITPICK_MONO =
11.22 @@ -27,22 +26,27 @@
11.23
11.24 type literal = var * sign
11.25
11.26 -datatype ctype =
11.27 - CAlpha |
11.28 - CFun of ctype * sign_atom * ctype |
11.29 - CPair of ctype * ctype |
11.30 - CType of string * ctype list |
11.31 - CRec of string * typ list
11.32 +datatype mtyp =
11.33 + MAlpha |
11.34 + MFun of mtyp * sign_atom * mtyp |
11.35 + MPair of mtyp * mtyp |
11.36 + MType of string * mtyp list |
11.37 + MRec of string * typ list
11.38
11.39 -type cdata =
11.40 +datatype mterm =
11.41 + MRaw of term * mtyp |
11.42 + MAbs of string * typ * mtyp * sign_atom * mterm |
11.43 + MApp of mterm * mterm
11.44 +
11.45 +type mdata =
11.46 {hol_ctxt: hol_context,
11.47 binarize: bool,
11.48 alpha_T: typ,
11.49 max_fresh: int Unsynchronized.ref,
11.50 - datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref,
11.51 - constr_cache: (styp * ctype) list Unsynchronized.ref}
11.52 + datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref,
11.53 + constr_cache: (styp * mtyp) list Unsynchronized.ref}
11.54
11.55 -exception CTYPE of string * ctype list
11.56 +exception MTYPE of string * mtyp list
11.57
11.58 (* string -> unit *)
11.59 fun print_g (_ : string) = ()
11.60 @@ -71,55 +75,95 @@
11.61 (* literal -> string *)
11.62 fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
11.63
11.64 -val bool_C = CType (@{type_name bool}, [])
11.65 +val bool_M = MType (@{type_name bool}, [])
11.66 +val dummy_M = MType (nitpick_prefix ^ "dummy", [])
11.67
11.68 -(* ctype -> bool *)
11.69 -fun is_CRec (CRec _) = true
11.70 - | is_CRec _ = false
11.71 +(* mtyp -> bool *)
11.72 +fun is_MRec (MRec _) = true
11.73 + | is_MRec _ = false
11.74 +(* mtyp -> mtyp * sign_atom * mtyp *)
11.75 +fun dest_MFun (MFun z) = z
11.76 + | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M])
11.77
11.78 val no_prec = 100
11.79 -val prec_CFun = 1
11.80 -val prec_CPair = 2
11.81
11.82 -(* tuple_set -> int *)
11.83 -fun precedence_of_ctype (CFun _) = prec_CFun
11.84 - | precedence_of_ctype (CPair _) = prec_CPair
11.85 - | precedence_of_ctype _ = no_prec
11.86 +(* mtyp -> int *)
11.87 +fun precedence_of_mtype (MFun _) = 1
11.88 + | precedence_of_mtype (MPair _) = 2
11.89 + | precedence_of_mtype _ = no_prec
11.90
11.91 -(* ctype -> string *)
11.92 -val string_for_ctype =
11.93 +(* mtyp -> string *)
11.94 +val string_for_mtype =
11.95 let
11.96 - (* int -> ctype -> string *)
11.97 - fun aux outer_prec C =
11.98 + (* int -> mtyp -> string *)
11.99 + fun aux outer_prec M =
11.100 let
11.101 - val prec = precedence_of_ctype C
11.102 + val prec = precedence_of_mtype M
11.103 val need_parens = (prec < outer_prec)
11.104 in
11.105 (if need_parens then "(" else "") ^
11.106 - (case C of
11.107 - CAlpha => "\<alpha>"
11.108 - | CFun (C1, a, C2) =>
11.109 - aux (prec + 1) C1 ^ " \<Rightarrow>\<^bsup>" ^
11.110 - string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2
11.111 - | CPair (C1, C2) => aux (prec + 1) C1 ^ " \<times> " ^ aux prec C2
11.112 - | CType (s, []) =>
11.113 - if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
11.114 - | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s
11.115 - | CRec (s, _) => "[" ^ s ^ "]") ^
11.116 + (if M = dummy_M then
11.117 + "_"
11.118 + else case M of
11.119 + MAlpha => "\<alpha>"
11.120 + | MFun (M1, a, M2) =>
11.121 + aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
11.122 + string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
11.123 + | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
11.124 + | MType (s, []) =>
11.125 + if s = @{type_name prop} orelse s = @{type_name bool} then "o"
11.126 + else s
11.127 + | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
11.128 + | MRec (s, _) => "[" ^ s ^ "]") ^
11.129 (if need_parens then ")" else "")
11.130 end
11.131 in aux 0 end
11.132
11.133 -(* ctype -> ctype list *)
11.134 -fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2]
11.135 - | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs
11.136 - | flatten_ctype C = [C]
11.137 +(* mtyp -> mtyp list *)
11.138 +fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2]
11.139 + | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms
11.140 + | flatten_mtype M = [M]
11.141
11.142 -(* hol_context -> bool -> typ -> cdata *)
11.143 -fun initial_cdata hol_ctxt binarize alpha_T =
11.144 +(* mterm -> bool *)
11.145 +fun precedence_of_mterm (MRaw _) = no_prec
11.146 + | precedence_of_mterm (MAbs _) = 1
11.147 + | precedence_of_mterm (MApp _) = 2
11.148 +
11.149 +(* Proof.context -> mterm -> string *)
11.150 +fun string_for_mterm ctxt =
11.151 + let
11.152 + (* mtype -> string *)
11.153 + fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>"
11.154 + (* int -> mterm -> string *)
11.155 + fun aux outer_prec m =
11.156 + let
11.157 + val prec = precedence_of_mterm m
11.158 + val need_parens = (prec < outer_prec)
11.159 + in
11.160 + (if need_parens then "(" else "") ^
11.161 + (case m of
11.162 + MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
11.163 + | MAbs (s, _, M, a, m) =>
11.164 + "\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
11.165 + string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
11.166 + | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^
11.167 + (if need_parens then ")" else "")
11.168 + end
11.169 + in aux 0 end
11.170 +
11.171 +(* mterm -> mtyp *)
11.172 +fun mtype_of_mterm (MRaw (_, M)) = M
11.173 + | mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
11.174 + | mtype_of_mterm (MApp (m1, _)) =
11.175 + case mtype_of_mterm m1 of
11.176 + MFun (_, _, M12) => M12
11.177 + | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1])
11.178 +
11.179 +(* hol_context -> bool -> typ -> mdata *)
11.180 +fun initial_mdata hol_ctxt binarize alpha_T =
11.181 ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T,
11.182 max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [],
11.183 - constr_cache = Unsynchronized.ref []} : cdata)
11.184 + constr_cache = Unsynchronized.ref []} : mdata)
11.185
11.186 (* typ -> typ -> bool *)
11.187 fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
11.188 @@ -127,172 +171,179 @@
11.189 exists (could_exist_alpha_subtype alpha_T) Ts)
11.190 | could_exist_alpha_subtype alpha_T T = (T = alpha_T)
11.191 (* theory -> typ -> typ -> bool *)
11.192 -fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
11.193 +fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T =
11.194 could_exist_alpha_subtype alpha_T T
11.195 - | could_exist_alpha_sub_ctype thy alpha_T T =
11.196 + | could_exist_alpha_sub_mtype thy alpha_T T =
11.197 (T = alpha_T orelse is_datatype thy [(NONE, true)] T)
11.198
11.199 -(* ctype -> bool *)
11.200 -fun exists_alpha_sub_ctype CAlpha = true
11.201 - | exists_alpha_sub_ctype (CFun (C1, _, C2)) =
11.202 - exists exists_alpha_sub_ctype [C1, C2]
11.203 - | exists_alpha_sub_ctype (CPair (C1, C2)) =
11.204 - exists exists_alpha_sub_ctype [C1, C2]
11.205 - | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs
11.206 - | exists_alpha_sub_ctype (CRec _) = true
11.207 +(* mtyp -> bool *)
11.208 +fun exists_alpha_sub_mtype MAlpha = true
11.209 + | exists_alpha_sub_mtype (MFun (M1, _, M2)) =
11.210 + exists exists_alpha_sub_mtype [M1, M2]
11.211 + | exists_alpha_sub_mtype (MPair (M1, M2)) =
11.212 + exists exists_alpha_sub_mtype [M1, M2]
11.213 + | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms
11.214 + | exists_alpha_sub_mtype (MRec _) = true
11.215
11.216 -(* ctype -> bool *)
11.217 -fun exists_alpha_sub_ctype_fresh CAlpha = true
11.218 - | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true
11.219 - | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) =
11.220 - exists_alpha_sub_ctype_fresh C2
11.221 - | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) =
11.222 - exists exists_alpha_sub_ctype_fresh [C1, C2]
11.223 - | exists_alpha_sub_ctype_fresh (CType (_, Cs)) =
11.224 - exists exists_alpha_sub_ctype_fresh Cs
11.225 - | exists_alpha_sub_ctype_fresh (CRec _) = true
11.226 +(* mtyp -> bool *)
11.227 +fun exists_alpha_sub_mtype_fresh MAlpha = true
11.228 + | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true
11.229 + | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) =
11.230 + exists_alpha_sub_mtype_fresh M2
11.231 + | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) =
11.232 + exists exists_alpha_sub_mtype_fresh [M1, M2]
11.233 + | exists_alpha_sub_mtype_fresh (MType (_, Ms)) =
11.234 + exists exists_alpha_sub_mtype_fresh Ms
11.235 + | exists_alpha_sub_mtype_fresh (MRec _) = true
11.236
11.237 -(* string * typ list -> ctype list -> ctype *)
11.238 -fun constr_ctype_for_binders z Cs =
11.239 - fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z)
11.240 +(* string * typ list -> mtyp list -> mtyp *)
11.241 +fun constr_mtype_for_binders z Ms =
11.242 + fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z)
11.243
11.244 -(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *)
11.245 -fun repair_ctype _ _ CAlpha = CAlpha
11.246 - | repair_ctype cache seen (CFun (C1, a, C2)) =
11.247 - CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2)
11.248 - | repair_ctype cache seen (CPair Cp) =
11.249 - CPair (pairself (repair_ctype cache seen) Cp)
11.250 - | repair_ctype cache seen (CType (s, Cs)) =
11.251 - CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs)
11.252 - | repair_ctype cache seen (CRec (z as (s, _))) =
11.253 +(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *)
11.254 +fun repair_mtype _ _ MAlpha = MAlpha
11.255 + | repair_mtype cache seen (MFun (M1, a, M2)) =
11.256 + MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2)
11.257 + | repair_mtype cache seen (MPair Mp) =
11.258 + MPair (pairself (repair_mtype cache seen) Mp)
11.259 + | repair_mtype cache seen (MType (s, Ms)) =
11.260 + MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms)
11.261 + | repair_mtype cache seen (MRec (z as (s, _))) =
11.262 case AList.lookup (op =) cache z |> the of
11.263 - CRec _ => CType (s, [])
11.264 - | C => if member (op =) seen C then CType (s, [])
11.265 - else repair_ctype cache (C :: seen) C
11.266 + MRec _ => MType (s, [])
11.267 + | M => if member (op =) seen M then MType (s, [])
11.268 + else repair_mtype cache (M :: seen) M
11.269
11.270 -(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *)
11.271 +(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *)
11.272 fun repair_datatype_cache cache =
11.273 let
11.274 - (* (string * typ list) * ctype -> unit *)
11.275 - fun repair_one (z, C) =
11.276 + (* (string * typ list) * mtyp -> unit *)
11.277 + fun repair_one (z, M) =
11.278 Unsynchronized.change cache
11.279 - (AList.update (op =) (z, repair_ctype (!cache) [] C))
11.280 + (AList.update (op =) (z, repair_mtype (!cache) [] M))
11.281 in List.app repair_one (rev (!cache)) end
11.282
11.283 -(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *)
11.284 +(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *)
11.285 fun repair_constr_cache dtype_cache constr_cache =
11.286 let
11.287 - (* styp * ctype -> unit *)
11.288 - fun repair_one (x, C) =
11.289 + (* styp * mtyp -> unit *)
11.290 + fun repair_one (x, M) =
11.291 Unsynchronized.change constr_cache
11.292 - (AList.update (op =) (x, repair_ctype dtype_cache [] C))
11.293 + (AList.update (op =) (x, repair_mtype dtype_cache [] M))
11.294 in List.app repair_one (!constr_cache) end
11.295
11.296 -(* cdata -> typ -> ctype *)
11.297 -fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh,
11.298 - datatype_cache, constr_cache, ...} : cdata) =
11.299 +(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *)
11.300 +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 =
11.301 let
11.302 - (* typ -> typ -> ctype *)
11.303 - fun do_fun T1 T2 =
11.304 - let
11.305 - val C1 = do_type T1
11.306 - val C2 = do_type T2
11.307 - val a = if is_boolean_type (body_type T2) andalso
11.308 - exists_alpha_sub_ctype_fresh C1 then
11.309 - V (Unsynchronized.inc max_fresh)
11.310 - else
11.311 - S Minus
11.312 - in CFun (C1, a, C2) end
11.313 - (* typ -> ctype *)
11.314 - and do_type T =
11.315 + val M1 = fresh_mtype_for_type mdata T1
11.316 + val M2 = fresh_mtype_for_type mdata T2
11.317 + val a = if is_boolean_type (body_type T2) andalso
11.318 + exists_alpha_sub_mtype_fresh M1 then
11.319 + V (Unsynchronized.inc max_fresh)
11.320 + else
11.321 + S Minus
11.322 + in (M1, a, M2) end
11.323 +(* mdata -> typ -> mtyp *)
11.324 +and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T,
11.325 + datatype_cache, constr_cache, ...}) =
11.326 + let
11.327 + (* typ -> typ -> mtyp *)
11.328 + val do_fun = MFun oo fresh_mfun_for_fun_type mdata
11.329 + (* typ -> mtyp *)
11.330 + fun do_type T =
11.331 if T = alpha_T then
11.332 - CAlpha
11.333 + MAlpha
11.334 else case T of
11.335 Type ("fun", [T1, T2]) => do_fun T1 T2
11.336 | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2
11.337 - | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2))
11.338 + | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2))
11.339 | Type (z as (s, _)) =>
11.340 - if could_exist_alpha_sub_ctype thy alpha_T T then
11.341 + if could_exist_alpha_sub_mtype thy alpha_T T then
11.342 case AList.lookup (op =) (!datatype_cache) z of
11.343 - SOME C => C
11.344 + SOME M => M
11.345 | NONE =>
11.346 let
11.347 - val _ = Unsynchronized.change datatype_cache (cons (z, CRec z))
11.348 + val _ = Unsynchronized.change datatype_cache (cons (z, MRec z))
11.349 val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T
11.350 - val (all_Cs, constr_Cs) =
11.351 - fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) =>
11.352 + val (all_Ms, constr_Ms) =
11.353 + fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) =>
11.354 let
11.355 - val binder_Cs = map do_type (binder_types T')
11.356 - val new_Cs = filter exists_alpha_sub_ctype_fresh
11.357 - binder_Cs
11.358 - val constr_C = constr_ctype_for_binders z
11.359 - binder_Cs
11.360 + val binder_Ms = map do_type (binder_types T')
11.361 + val new_Ms = filter exists_alpha_sub_mtype_fresh
11.362 + binder_Ms
11.363 + val constr_M = constr_mtype_for_binders z
11.364 + binder_Ms
11.365 in
11.366 - (union (op =) new_Cs all_Cs,
11.367 - constr_C :: constr_Cs)
11.368 + (union (op =) new_Ms all_Ms,
11.369 + constr_M :: constr_Ms)
11.370 end)
11.371 xs ([], [])
11.372 - val C = CType (s, all_Cs)
11.373 + val M = MType (s, all_Ms)
11.374 val _ = Unsynchronized.change datatype_cache
11.375 - (AList.update (op =) (z, C))
11.376 + (AList.update (op =) (z, M))
11.377 val _ = Unsynchronized.change constr_cache
11.378 - (append (xs ~~ constr_Cs))
11.379 + (append (xs ~~ constr_Ms))
11.380 in
11.381 - if forall (not o is_CRec o snd) (!datatype_cache) then
11.382 + if forall (not o is_MRec o snd) (!datatype_cache) then
11.383 (repair_datatype_cache datatype_cache;
11.384 repair_constr_cache (!datatype_cache) constr_cache;
11.385 AList.lookup (op =) (!datatype_cache) z |> the)
11.386 else
11.387 - C
11.388 + M
11.389 end
11.390 else
11.391 - CType (s, [])
11.392 - | _ => CType (Refute.string_of_typ T, [])
11.393 + MType (s, [])
11.394 + | _ => MType (Refute.string_of_typ T, [])
11.395 in do_type end
11.396
11.397 -(* ctype -> ctype list *)
11.398 -fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2]
11.399 - | prodC_factors C = [C]
11.400 -(* ctype -> ctype list * ctype *)
11.401 -fun curried_strip_ctype (CFun (C1, S Minus, C2)) =
11.402 - curried_strip_ctype C2 |>> append (prodC_factors C1)
11.403 - | curried_strip_ctype C = ([], C)
11.404 -(* string -> ctype -> ctype *)
11.405 -fun sel_ctype_from_constr_ctype s C =
11.406 - let val (arg_Cs, dataC) = curried_strip_ctype C in
11.407 - CFun (dataC, S Minus,
11.408 - case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n)
11.409 +(* mtyp -> mtyp list *)
11.410 +fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
11.411 + | prodM_factors M = [M]
11.412 +(* mtyp -> mtyp list * mtyp *)
11.413 +fun curried_strip_mtype (MFun (M1, S Minus, M2)) =
11.414 + curried_strip_mtype M2 |>> append (prodM_factors M1)
11.415 + | curried_strip_mtype M = ([], M)
11.416 +(* string -> mtyp -> mtyp *)
11.417 +fun sel_mtype_from_constr_mtype s M =
11.418 + let val (arg_Ms, dataM) = curried_strip_mtype M in
11.419 + MFun (dataM, S Minus,
11.420 + case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n)
11.421 end
11.422
11.423 -(* cdata -> styp -> ctype *)
11.424 -fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
11.425 +(* mdata -> styp -> mtyp *)
11.426 +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache,
11.427 ...}) (x as (_, T)) =
11.428 - if could_exist_alpha_sub_ctype thy alpha_T T then
11.429 + if could_exist_alpha_sub_mtype thy alpha_T T then
11.430 case AList.lookup (op =) (!constr_cache) x of
11.431 - SOME C => C
11.432 - | NONE => (fresh_ctype_for_type cdata (body_type T);
11.433 - AList.lookup (op =) (!constr_cache) x |> the)
11.434 + SOME M => M
11.435 + | NONE => if T = alpha_T then
11.436 + let val M = fresh_mtype_for_type mdata T in
11.437 + (Unsynchronized.change constr_cache (cons (x, M)); M)
11.438 + end
11.439 + else
11.440 + (fresh_mtype_for_type mdata (body_type T);
11.441 + AList.lookup (op =) (!constr_cache) x |> the)
11.442 else
11.443 - fresh_ctype_for_type cdata T
11.444 -fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
11.445 + fresh_mtype_for_type mdata T
11.446 +fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) =
11.447 x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize
11.448 - |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s
11.449 + |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s
11.450
11.451 -(* literal list -> ctype -> ctype *)
11.452 -fun instantiate_ctype lits =
11.453 +(* literal list -> mtyp -> mtyp *)
11.454 +fun instantiate_mtype lits =
11.455 let
11.456 - (* ctype -> ctype *)
11.457 - fun aux CAlpha = CAlpha
11.458 - | aux (CFun (C1, V x, C2)) =
11.459 + (* mtyp -> mtyp *)
11.460 + fun aux MAlpha = MAlpha
11.461 + | aux (MFun (M1, V x, M2)) =
11.462 let
11.463 val a = case AList.lookup (op =) lits x of
11.464 SOME sn => S sn
11.465 | NONE => V x
11.466 - in CFun (aux C1, a, aux C2) end
11.467 - | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2)
11.468 - | aux (CPair Cp) = CPair (pairself aux Cp)
11.469 - | aux (CType (s, Cs)) = CType (s, map aux Cs)
11.470 - | aux (CRec z) = CRec z
11.471 + in MFun (aux M1, a, aux M2) end
11.472 + | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2)
11.473 + | aux (MPair Mp) = MPair (pairself aux Mp)
11.474 + | aux (MType (s, Ms)) = MType (s, map aux Ms)
11.475 + | aux (MRec z) = MRec z
11.476 in aux end
11.477
11.478 datatype comp_op = Eq | Leq
11.479 @@ -342,105 +393,106 @@
11.480 | do_sign_atom_comp cmp xs a1 a2 (lits, comps) =
11.481 SOME (lits, insert (op =) (a1, a2, cmp, xs) comps)
11.482
11.483 -(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option
11.484 +(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option
11.485 -> (literal list * comp list) option *)
11.486 -fun do_ctype_comp _ _ _ _ NONE = NONE
11.487 - | do_ctype_comp _ _ CAlpha CAlpha accum = accum
11.488 - | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
11.489 +fun do_mtype_comp _ _ _ _ NONE = NONE
11.490 + | do_mtype_comp _ _ MAlpha MAlpha accum = accum
11.491 + | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
11.492 (SOME accum) =
11.493 - accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21
11.494 - |> do_ctype_comp Eq xs C12 C22
11.495 - | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22))
11.496 + accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21
11.497 + |> do_mtype_comp Eq xs M12 M22
11.498 + | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22))
11.499 (SOME accum) =
11.500 - (if exists_alpha_sub_ctype C11 then
11.501 + (if exists_alpha_sub_mtype M11 then
11.502 accum |> do_sign_atom_comp Leq xs a1 a2
11.503 - |> do_ctype_comp Leq xs C21 C11
11.504 + |> do_mtype_comp Leq xs M21 M11
11.505 |> (case a2 of
11.506 S Minus => I
11.507 - | S Plus => do_ctype_comp Leq xs C11 C21
11.508 - | V x => do_ctype_comp Leq (x :: xs) C11 C21)
11.509 + | S Plus => do_mtype_comp Leq xs M11 M21
11.510 + | V x => do_mtype_comp Leq (x :: xs) M11 M21)
11.511 else
11.512 SOME accum)
11.513 - |> do_ctype_comp Leq xs C12 C22
11.514 - | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22))
11.515 + |> do_mtype_comp Leq xs M12 M22
11.516 + | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22))
11.517 accum =
11.518 - (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)]
11.519 + (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)]
11.520 handle Library.UnequalLengths =>
11.521 - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]))
11.522 - | do_ctype_comp _ _ (CType _) (CType _) accum =
11.523 + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]))
11.524 + | do_mtype_comp _ _ (MType _) (MType _) accum =
11.525 accum (* no need to compare them thanks to the cache *)
11.526 - | do_ctype_comp _ _ C1 C2 _ =
11.527 - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])
11.528 + | do_mtype_comp _ _ M1 M2 _ =
11.529 + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])
11.530
11.531 -(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *)
11.532 -fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
11.533 - | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) =
11.534 - (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^
11.535 - " " ^ string_for_ctype C2);
11.536 - case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of
11.537 +(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *)
11.538 +fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet
11.539 + | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) =
11.540 + (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^
11.541 + " " ^ string_for_mtype M2);
11.542 + case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of
11.543 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
11.544 | SOME (lits, comps) => CSet (lits, comps, sexps))
11.545
11.546 -(* ctype -> ctype -> constraint_set -> constraint_set *)
11.547 -val add_ctypes_equal = add_ctype_comp Eq
11.548 -val add_is_sub_ctype = add_ctype_comp Leq
11.549 +(* mtyp -> mtyp -> constraint_set -> constraint_set *)
11.550 +val add_mtypes_equal = add_mtype_comp Eq
11.551 +val add_is_sub_mtype = add_mtype_comp Leq
11.552
11.553 -(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option
11.554 +(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option
11.555 -> (literal list * sign_expr list) option *)
11.556 -fun do_notin_ctype_fv _ _ _ NONE = NONE
11.557 - | do_notin_ctype_fv Minus _ CAlpha accum = accum
11.558 - | do_notin_ctype_fv Plus [] CAlpha _ = NONE
11.559 - | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) =
11.560 +fun do_notin_mtype_fv _ _ _ NONE = NONE
11.561 + | do_notin_mtype_fv Minus _ MAlpha accum = accum
11.562 + | do_notin_mtype_fv Plus [] MAlpha _ = NONE
11.563 + | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) =
11.564 SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps)
11.565 - | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) =
11.566 + | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) =
11.567 SOME (lits, insert (op =) sexp sexps)
11.568 - | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum =
11.569 + | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum =
11.570 accum |> (if sn' = Plus andalso sn = Plus then
11.571 - do_notin_ctype_fv Plus sexp C1
11.572 + do_notin_mtype_fv Plus sexp M1
11.573 else
11.574 I)
11.575 |> (if sn' = Minus orelse sn = Plus then
11.576 - do_notin_ctype_fv Minus sexp C1
11.577 + do_notin_mtype_fv Minus sexp M1
11.578 else
11.579 I)
11.580 - |> do_notin_ctype_fv sn sexp C2
11.581 - | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum =
11.582 + |> do_notin_mtype_fv sn sexp M2
11.583 + | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum =
11.584 accum |> (case do_literal (x, Minus) (SOME sexp) of
11.585 NONE => I
11.586 - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
11.587 - |> do_notin_ctype_fv Minus sexp C1
11.588 - |> do_notin_ctype_fv Plus sexp C2
11.589 - | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum =
11.590 + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
11.591 + |> do_notin_mtype_fv Minus sexp M1
11.592 + |> do_notin_mtype_fv Plus sexp M2
11.593 + | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum =
11.594 accum |> (case do_literal (x, Plus) (SOME sexp) of
11.595 NONE => I
11.596 - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1)
11.597 - |> do_notin_ctype_fv Minus sexp C2
11.598 - | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum =
11.599 - accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2]
11.600 - | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum =
11.601 - accum |> fold (do_notin_ctype_fv sn sexp) Cs
11.602 - | do_notin_ctype_fv _ _ C _ =
11.603 - raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C])
11.604 + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1)
11.605 + |> do_notin_mtype_fv Minus sexp M2
11.606 + | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum =
11.607 + accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2]
11.608 + | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum =
11.609 + accum |> fold (do_notin_mtype_fv sn sexp) Ms
11.610 + | do_notin_mtype_fv _ _ M _ =
11.611 + raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M])
11.612
11.613 -(* sign -> ctype -> constraint_set -> constraint_set *)
11.614 -fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet
11.615 - | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) =
11.616 - (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^
11.617 +(* sign -> mtyp -> constraint_set -> constraint_set *)
11.618 +fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet
11.619 + | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) =
11.620 + (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^
11.621 (case sn of Minus => "unique" | Plus => "total") ^ ".");
11.622 - case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of
11.623 + case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of
11.624 NONE => (print_g "**** Unsolvable"; UnsolvableCSet)
11.625 | SOME (lits, sexps) => CSet (lits, comps, sexps))
11.626
11.627 -(* ctype -> constraint_set -> constraint_set *)
11.628 -val add_ctype_is_right_unique = add_notin_ctype_fv Minus
11.629 -val add_ctype_is_right_total = add_notin_ctype_fv Plus
11.630 +(* mtyp -> constraint_set -> constraint_set *)
11.631 +val add_mtype_is_right_unique = add_notin_mtype_fv Minus
11.632 +val add_mtype_is_right_total = add_notin_mtype_fv Plus
11.633 +
11.634 +val bool_from_minus = true
11.635
11.636 (* sign -> bool *)
11.637 -fun bool_from_sign Plus = false
11.638 - | bool_from_sign Minus = true
11.639 +fun bool_from_sign Plus = not bool_from_minus
11.640 + | bool_from_sign Minus = bool_from_minus
11.641 (* bool -> sign *)
11.642 -fun sign_from_bool false = Plus
11.643 - | sign_from_bool true = Minus
11.644 +fun sign_from_bool b = if b = bool_from_minus then Minus else Plus
11.645
11.646 (* literal -> PropLogic.prop_formula *)
11.647 fun prop_for_literal (x, sn) =
11.648 @@ -492,228 +544,264 @@
11.649 "-: " ^ commas (map (string_for_var o fst) neg))
11.650 end
11.651
11.652 -(* var -> constraint_set -> literal list list option *)
11.653 +(* var -> constraint_set -> literal list option *)
11.654 fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
11.655 | solve max_var (CSet (lits, comps, sexps)) =
11.656 let
11.657 + (* (int -> bool option) -> literal list option *)
11.658 + fun do_assigns assigns =
11.659 + SOME (literals_from_assignments max_var assigns lits
11.660 + |> tap print_solution)
11.661 val _ = print_problem lits comps sexps
11.662 val prop = PropLogic.all (map prop_for_literal lits @
11.663 map prop_for_comp comps @
11.664 map prop_for_sign_expr sexps)
11.665 - (* use the first ML solver (to avoid startup overhead) *)
11.666 - val solvers = !SatSolver.solvers
11.667 - |> filter (member (op =) ["dptsat", "dpll"] o fst)
11.668 + val default_val = bool_from_sign Minus
11.669 in
11.670 - case snd (hd solvers) prop of
11.671 - SatSolver.SATISFIABLE assigns =>
11.672 - SOME (literals_from_assignments max_var assigns lits
11.673 - |> tap print_solution)
11.674 - | _ => NONE
11.675 + if PropLogic.eval (K default_val) prop then
11.676 + do_assigns (K (SOME default_val))
11.677 + else
11.678 + let
11.679 + (* use the first ML solver (to avoid startup overhead) *)
11.680 + val solvers = !SatSolver.solvers
11.681 + |> filter (member (op =) ["dptsat", "dpll"] o fst)
11.682 + in
11.683 + case snd (hd solvers) prop of
11.684 + SatSolver.SATISFIABLE assigns => do_assigns assigns
11.685 + | _ => NONE
11.686 + end
11.687 end
11.688
11.689 -type ctype_schema = ctype * constraint_set
11.690 -type ctype_context =
11.691 - {bounds: ctype list,
11.692 - frees: (styp * ctype) list,
11.693 - consts: (styp * ctype) list}
11.694 +type mtype_schema = mtyp * constraint_set
11.695 +type mtype_context =
11.696 + {bounds: mtyp list,
11.697 + frees: (styp * mtyp) list,
11.698 + consts: (styp * mtyp) list}
11.699
11.700 -type accumulator = ctype_context * constraint_set
11.701 +type accumulator = mtype_context * constraint_set
11.702
11.703 val initial_gamma = {bounds = [], frees = [], consts = []}
11.704 val unsolvable_accum = (initial_gamma, UnsolvableCSet)
11.705
11.706 -(* ctype -> ctype_context -> ctype_context *)
11.707 -fun push_bound C {bounds, frees, consts} =
11.708 - {bounds = C :: bounds, frees = frees, consts = consts}
11.709 -(* ctype_context -> ctype_context *)
11.710 +(* mtyp -> mtype_context -> mtype_context *)
11.711 +fun push_bound M {bounds, frees, consts} =
11.712 + {bounds = M :: bounds, frees = frees, consts = consts}
11.713 +(* mtype_context -> mtype_context *)
11.714 fun pop_bound {bounds, frees, consts} =
11.715 {bounds = tl bounds, frees = frees, consts = consts}
11.716 handle List.Empty => initial_gamma
11.717
11.718 -(* cdata -> term -> accumulator -> ctype * accumulator *)
11.719 -fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
11.720 +(* mdata -> term -> accumulator -> mterm * accumulator *)
11.721 +fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
11.722 def_table, ...},
11.723 alpha_T, max_fresh, ...}) =
11.724 let
11.725 - (* typ -> ctype *)
11.726 - val ctype_for = fresh_ctype_for_type cdata
11.727 - (* ctype -> ctype *)
11.728 - fun pos_set_ctype_for_dom C =
11.729 - CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C)
11.730 - (* typ -> accumulator -> ctype * accumulator *)
11.731 - fun do_quantifier T (gamma, cset) =
11.732 + (* typ -> typ -> mtyp * sign_atom * mtyp *)
11.733 + val mfun_for = fresh_mfun_for_fun_type mdata
11.734 + (* typ -> mtyp *)
11.735 + val mtype_for = fresh_mtype_for_type mdata
11.736 + (* mtyp -> mtyp *)
11.737 + fun pos_set_mtype_for_dom M =
11.738 + MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M)
11.739 + (* typ -> accumulator -> mterm * accumulator *)
11.740 + fun do_all T (gamma, cset) =
11.741 let
11.742 - val abs_C = ctype_for (domain_type (domain_type T))
11.743 - val body_C = ctype_for (range_type T)
11.744 + val abs_M = mtype_for (domain_type (domain_type T))
11.745 + val body_M = mtype_for (body_type T)
11.746 in
11.747 - (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C),
11.748 - (gamma, cset |> add_ctype_is_right_total abs_C))
11.749 + (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
11.750 + (gamma, cset |> add_mtype_is_right_total abs_M))
11.751 end
11.752 fun do_equals T (gamma, cset) =
11.753 - let val C = ctype_for (domain_type T) in
11.754 - (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh),
11.755 - ctype_for (nth_range_type 2 T))),
11.756 - (gamma, cset |> add_ctype_is_right_unique C))
11.757 + let val M = mtype_for (domain_type T) in
11.758 + (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh),
11.759 + mtype_for (nth_range_type 2 T))),
11.760 + (gamma, cset |> add_mtype_is_right_unique M))
11.761 end
11.762 fun do_robust_set_operation T (gamma, cset) =
11.763 let
11.764 val set_T = domain_type T
11.765 - val C1 = ctype_for set_T
11.766 - val C2 = ctype_for set_T
11.767 - val C3 = ctype_for set_T
11.768 + val M1 = mtype_for set_T
11.769 + val M2 = mtype_for set_T
11.770 + val M3 = mtype_for set_T
11.771 in
11.772 - (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
11.773 - (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3))
11.774 + (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
11.775 + (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3))
11.776 end
11.777 fun do_fragile_set_operation T (gamma, cset) =
11.778 let
11.779 val set_T = domain_type T
11.780 - val set_C = ctype_for set_T
11.781 - (* typ -> ctype *)
11.782 - fun custom_ctype_for (T as Type ("fun", [T1, T2])) =
11.783 - if T = set_T then set_C
11.784 - else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2)
11.785 - | custom_ctype_for T = ctype_for T
11.786 + val set_M = mtype_for set_T
11.787 + (* typ -> mtyp *)
11.788 + fun custom_mtype_for (T as Type ("fun", [T1, T2])) =
11.789 + if T = set_T then set_M
11.790 + else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2)
11.791 + | custom_mtype_for T = mtype_for T
11.792 in
11.793 - (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C))
11.794 + (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M))
11.795 end
11.796 - (* typ -> accumulator -> ctype * accumulator *)
11.797 + (* typ -> accumulator -> mtyp * accumulator *)
11.798 fun do_pair_constr T accum =
11.799 - case ctype_for (nth_range_type 2 T) of
11.800 - C as CPair (a_C, b_C) =>
11.801 - (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum)
11.802 - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C])
11.803 - (* int -> typ -> accumulator -> ctype * accumulator *)
11.804 + case mtype_for (nth_range_type 2 T) of
11.805 + M as MPair (a_M, b_M) =>
11.806 + (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum)
11.807 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M])
11.808 + (* int -> typ -> accumulator -> mtyp * accumulator *)
11.809 fun do_nth_pair_sel n T =
11.810 - case ctype_for (domain_type T) of
11.811 - C as CPair (a_C, b_C) =>
11.812 - pair (CFun (C, S Minus, if n = 0 then a_C else b_C))
11.813 - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C])
11.814 - val unsolvable = (CType ("unsolvable", []), unsolvable_accum)
11.815 - (* typ -> term -> accumulator -> ctype * accumulator *)
11.816 - fun do_bounded_quantifier abs_T bound_t body_t accum =
11.817 + case mtype_for (domain_type T) of
11.818 + M as MPair (a_M, b_M) =>
11.819 + pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
11.820 + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
11.821 + (* mtyp * accumulator *)
11.822 + val mtype_unsolvable = (dummy_M, unsolvable_accum)
11.823 + (* term -> mterm * accumulator *)
11.824 + fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
11.825 + (* term -> string -> typ -> term -> term -> term -> accumulator
11.826 + -> mterm * accumulator *)
11.827 + fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
11.828 let
11.829 - val abs_C = ctype_for abs_T
11.830 - val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t
11.831 - val expected_bound_C = pos_set_ctype_for_dom abs_C
11.832 + val abs_M = mtype_for abs_T
11.833 + val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t
11.834 + val expected_bound_M = pos_set_mtype_for_dom abs_M
11.835 + val (body_m, accum) =
11.836 + accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m)
11.837 + |> do_term body_t ||> apfst pop_bound
11.838 + val bound_M = mtype_of_mterm bound_m
11.839 + val (M1, a, M2) = dest_MFun bound_M
11.840 in
11.841 - accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t
11.842 - ||> apfst pop_bound
11.843 + (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
11.844 + MAbs (abs_s, abs_T, M1, a,
11.845 + MApp (MApp (MRaw (connective_t,
11.846 + mtype_for (fastype_of connective_t)),
11.847 + MApp (bound_m, MRaw (Bound 0, M1))),
11.848 + body_m))), accum)
11.849 end
11.850 - (* term -> accumulator -> ctype * accumulator *)
11.851 - and do_term _ (_, UnsolvableCSet) = unsolvable
11.852 + (* term -> accumulator -> mterm * accumulator *)
11.853 + and do_term t (_, UnsolvableCSet) = mterm_unsolvable t
11.854 | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) =
11.855 (case t of
11.856 Const (x as (s, T)) =>
11.857 (case AList.lookup (op =) consts x of
11.858 - SOME C => (C, accum)
11.859 + SOME M => (M, accum)
11.860 | NONE =>
11.861 if not (could_exist_alpha_subtype alpha_T T) then
11.862 - (ctype_for T, accum)
11.863 + (mtype_for T, accum)
11.864 else case s of
11.865 - @{const_name all} => do_quantifier T accum
11.866 + @{const_name all} => do_all T accum
11.867 | @{const_name "=="} => do_equals T accum
11.868 - | @{const_name All} => do_quantifier T accum
11.869 - | @{const_name Ex} => do_quantifier T accum
11.870 + | @{const_name All} => do_all T accum
11.871 + | @{const_name Ex} =>
11.872 + let val set_T = domain_type T in
11.873 + do_term (Abs (Name.uu, set_T,
11.874 + @{const Not} $ (HOLogic.mk_eq
11.875 + (Abs (Name.uu, domain_type set_T,
11.876 + @{const False}),
11.877 + Bound 0)))) accum
11.878 + |>> mtype_of_mterm
11.879 + end
11.880 | @{const_name "op ="} => do_equals T accum
11.881 - | @{const_name The} => (print_g "*** The"; unsolvable)
11.882 - | @{const_name Eps} => (print_g "*** Eps"; unsolvable)
11.883 + | @{const_name The} => (print_g "*** The"; mtype_unsolvable)
11.884 + | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
11.885 | @{const_name If} =>
11.886 do_robust_set_operation (range_type T) accum
11.887 - |>> curry3 CFun bool_C (S Minus)
11.888 + |>> curry3 MFun bool_M (S Minus)
11.889 | @{const_name Pair} => do_pair_constr T accum
11.890 | @{const_name fst} => do_nth_pair_sel 0 T accum
11.891 | @{const_name snd} => do_nth_pair_sel 1 T accum
11.892 | @{const_name Id} =>
11.893 - (CFun (ctype_for (domain_type T), S Minus, bool_C), accum)
11.894 + (MFun (mtype_for (domain_type T), S Minus, bool_M), accum)
11.895 | @{const_name insert} =>
11.896 let
11.897 val set_T = domain_type (range_type T)
11.898 - val C1 = ctype_for (domain_type set_T)
11.899 - val C1' = pos_set_ctype_for_dom C1
11.900 - val C2 = ctype_for set_T
11.901 - val C3 = ctype_for set_T
11.902 + val M1 = mtype_for (domain_type set_T)
11.903 + val M1' = pos_set_mtype_for_dom M1
11.904 + val M2 = mtype_for set_T
11.905 + val M3 = mtype_for set_T
11.906 in
11.907 - (CFun (C1, S Minus, CFun (C2, S Minus, C3)),
11.908 - (gamma, cset |> add_ctype_is_right_unique C1
11.909 - |> add_is_sub_ctype C1' C3
11.910 - |> add_is_sub_ctype C2 C3))
11.911 + (MFun (M1, S Minus, MFun (M2, S Minus, M3)),
11.912 + (gamma, cset |> add_mtype_is_right_unique M1
11.913 + |> add_is_sub_mtype M1' M3
11.914 + |> add_is_sub_mtype M2 M3))
11.915 end
11.916 | @{const_name converse} =>
11.917 let
11.918 val x = Unsynchronized.inc max_fresh
11.919 - (* typ -> ctype *)
11.920 - fun ctype_for_set T =
11.921 - CFun (ctype_for (domain_type T), V x, bool_C)
11.922 - val ab_set_C = domain_type T |> ctype_for_set
11.923 - val ba_set_C = range_type T |> ctype_for_set
11.924 - in (CFun (ab_set_C, S Minus, ba_set_C), accum) end
11.925 + (* typ -> mtyp *)
11.926 + fun mtype_for_set T =
11.927 + MFun (mtype_for (domain_type T), V x, bool_M)
11.928 + val ab_set_M = domain_type T |> mtype_for_set
11.929 + val ba_set_M = range_type T |> mtype_for_set
11.930 + in (MFun (ab_set_M, S Minus, ba_set_M), accum) end
11.931 | @{const_name trancl} => do_fragile_set_operation T accum
11.932 - | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable)
11.933 + | @{const_name rtrancl} =>
11.934 + (print_g "*** rtrancl"; mtype_unsolvable)
11.935 | @{const_name finite} =>
11.936 - let val C1 = ctype_for (domain_type (domain_type T)) in
11.937 - (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), accum)
11.938 - end
11.939 + if is_finite_type hol_ctxt T then
11.940 + let val M1 = mtype_for (domain_type (domain_type T)) in
11.941 + (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
11.942 + end
11.943 + else
11.944 + (print_g "*** finite"; mtype_unsolvable)
11.945 | @{const_name rel_comp} =>
11.946 let
11.947 val x = Unsynchronized.inc max_fresh
11.948 - (* typ -> ctype *)
11.949 - fun ctype_for_set T =
11.950 - CFun (ctype_for (domain_type T), V x, bool_C)
11.951 - val bc_set_C = domain_type T |> ctype_for_set
11.952 - val ab_set_C = domain_type (range_type T) |> ctype_for_set
11.953 - val ac_set_C = nth_range_type 2 T |> ctype_for_set
11.954 + (* typ -> mtyp *)
11.955 + fun mtype_for_set T =
11.956 + MFun (mtype_for (domain_type T), V x, bool_M)
11.957 + val bc_set_M = domain_type T |> mtype_for_set
11.958 + val ab_set_M = domain_type (range_type T) |> mtype_for_set
11.959 + val ac_set_M = nth_range_type 2 T |> mtype_for_set
11.960 in
11.961 - (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)),
11.962 + (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)),
11.963 accum)
11.964 end
11.965 | @{const_name image} =>
11.966 let
11.967 - val a_C = ctype_for (domain_type (domain_type T))
11.968 - val b_C = ctype_for (range_type (domain_type T))
11.969 + val a_M = mtype_for (domain_type (domain_type T))
11.970 + val b_M = mtype_for (range_type (domain_type T))
11.971 in
11.972 - (CFun (CFun (a_C, S Minus, b_C), S Minus,
11.973 - CFun (pos_set_ctype_for_dom a_C, S Minus,
11.974 - pos_set_ctype_for_dom b_C)), accum)
11.975 + (MFun (MFun (a_M, S Minus, b_M), S Minus,
11.976 + MFun (pos_set_mtype_for_dom a_M, S Minus,
11.977 + pos_set_mtype_for_dom b_M)), accum)
11.978 end
11.979 | @{const_name Sigma} =>
11.980 let
11.981 val x = Unsynchronized.inc max_fresh
11.982 - (* typ -> ctype *)
11.983 - fun ctype_for_set T =
11.984 - CFun (ctype_for (domain_type T), V x, bool_C)
11.985 + (* typ -> mtyp *)
11.986 + fun mtype_for_set T =
11.987 + MFun (mtype_for (domain_type T), V x, bool_M)
11.988 val a_set_T = domain_type T
11.989 - val a_C = ctype_for (domain_type a_set_T)
11.990 - val b_set_C = ctype_for_set (range_type (domain_type
11.991 + val a_M = mtype_for (domain_type a_set_T)
11.992 + val b_set_M = mtype_for_set (range_type (domain_type
11.993 (range_type T)))
11.994 - val a_set_C = ctype_for_set a_set_T
11.995 - val a_to_b_set_C = CFun (a_C, S Minus, b_set_C)
11.996 - val ab_set_C = ctype_for_set (nth_range_type 2 T)
11.997 + val a_set_M = mtype_for_set a_set_T
11.998 + val a_to_b_set_M = MFun (a_M, S Minus, b_set_M)
11.999 + val ab_set_M = mtype_for_set (nth_range_type 2 T)
11.1000 in
11.1001 - (CFun (a_set_C, S Minus,
11.1002 - CFun (a_to_b_set_C, S Minus, ab_set_C)), accum)
11.1003 + (MFun (a_set_M, S Minus,
11.1004 + MFun (a_to_b_set_M, S Minus, ab_set_M)), accum)
11.1005 end
11.1006 | @{const_name Tha} =>
11.1007 let
11.1008 - val a_C = ctype_for (domain_type (domain_type T))
11.1009 - val a_set_C = pos_set_ctype_for_dom a_C
11.1010 - in (CFun (a_set_C, S Minus, a_C), accum) end
11.1011 + val a_M = mtype_for (domain_type (domain_type T))
11.1012 + val a_set_M = pos_set_mtype_for_dom a_M
11.1013 + in (MFun (a_set_M, S Minus, a_M), accum) end
11.1014 | @{const_name FunBox} =>
11.1015 - let val dom_C = ctype_for (domain_type T) in
11.1016 - (CFun (dom_C, S Minus, dom_C), accum)
11.1017 + let val dom_M = mtype_for (domain_type T) in
11.1018 + (MFun (dom_M, S Minus, dom_M), accum)
11.1019 end
11.1020 | _ =>
11.1021 if s = @{const_name minus_class.minus} andalso
11.1022 is_set_type (domain_type T) then
11.1023 let
11.1024 val set_T = domain_type T
11.1025 - val left_set_C = ctype_for set_T
11.1026 - val right_set_C = ctype_for set_T
11.1027 + val left_set_M = mtype_for set_T
11.1028 + val right_set_M = mtype_for set_T
11.1029 in
11.1030 - (CFun (left_set_C, S Minus,
11.1031 - CFun (right_set_C, S Minus, left_set_C)),
11.1032 - (gamma, cset |> add_ctype_is_right_unique right_set_C
11.1033 - |> add_is_sub_ctype right_set_C left_set_C))
11.1034 + (MFun (left_set_M, S Minus,
11.1035 + MFun (right_set_M, S Minus, left_set_M)),
11.1036 + (gamma, cset |> add_mtype_is_right_unique right_set_M
11.1037 + |> add_is_sub_mtype right_set_M left_set_M))
11.1038 end
11.1039 else if s = @{const_name ord_class.less_eq} andalso
11.1040 is_set_type (domain_type T) then
11.1041 @@ -724,34 +812,37 @@
11.1042 do_robust_set_operation T accum
11.1043 else if is_sel s then
11.1044 if constr_name_for_sel_like s = @{const_name FunBox} then
11.1045 - let val dom_C = ctype_for (domain_type T) in
11.1046 - (CFun (dom_C, S Minus, dom_C), accum)
11.1047 + let val dom_M = mtype_for (domain_type T) in
11.1048 + (MFun (dom_M, S Minus, dom_M), accum)
11.1049 end
11.1050 else
11.1051 - (ctype_for_sel cdata x, accum)
11.1052 + (mtype_for_sel mdata x, accum)
11.1053 else if is_constr thy stds x then
11.1054 - (ctype_for_constr cdata x, accum)
11.1055 + (mtype_for_constr mdata x, accum)
11.1056 else if is_built_in_const thy stds fast_descrs x then
11.1057 case def_of_const thy def_table x of
11.1058 - SOME t' => do_term t' accum
11.1059 - | NONE => (print_g ("*** built-in " ^ s); unsolvable)
11.1060 + SOME t' => do_term t' accum |>> mtype_of_mterm
11.1061 + | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable)
11.1062 else
11.1063 - let val C = ctype_for T in
11.1064 - (C, ({bounds = bounds, frees = frees,
11.1065 - consts = (x, C) :: consts}, cset))
11.1066 - end)
11.1067 + let val M = mtype_for T in
11.1068 + (M, ({bounds = bounds, frees = frees,
11.1069 + consts = (x, M) :: consts}, cset))
11.1070 + end) |>> curry MRaw t
11.1071 | Free (x as (_, T)) =>
11.1072 (case AList.lookup (op =) frees x of
11.1073 - SOME C => (C, accum)
11.1074 + SOME M => (M, accum)
11.1075 | NONE =>
11.1076 - let val C = ctype_for T in
11.1077 - (C, ({bounds = bounds, frees = (x, C) :: frees,
11.1078 + let val M = mtype_for T in
11.1079 + (M, ({bounds = bounds, frees = (x, M) :: frees,
11.1080 consts = consts}, cset))
11.1081 - end)
11.1082 - | Var _ => (print_g "*** Var"; unsolvable)
11.1083 - | Bound j => (nth bounds j, accum)
11.1084 - | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum)
11.1085 - | Abs (_, T, t') =>
11.1086 + end) |>> curry MRaw t
11.1087 + | Var _ => (print_g "*** Var"; mterm_unsolvable t)
11.1088 + | Bound j => (MRaw (t, nth bounds j), accum)
11.1089 + | Abs (s, T, t' as @{const False}) =>
11.1090 + let val (M1, a, M2) = mfun_for T bool_T in
11.1091 + (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
11.1092 + end
11.1093 + | Abs (s, T, t') =>
11.1094 ((case t' of
11.1095 t1' $ Bound 0 =>
11.1096 if not (loose_bvar1 (t1', 0)) then
11.1097 @@ -761,107 +852,127 @@
11.1098 | _ => raise SAME ())
11.1099 handle SAME () =>
11.1100 let
11.1101 - val C = ctype_for T
11.1102 - val (C', accum) = do_term t' (accum |>> push_bound C)
11.1103 - in (CFun (C, S Minus, C'), accum |>> pop_bound) end)
11.1104 - | Const (@{const_name All}, _)
11.1105 - $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) =>
11.1106 - do_bounded_quantifier T' t1 t2 accum
11.1107 - | Const (@{const_name Ex}, _)
11.1108 - $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) =>
11.1109 - do_bounded_quantifier T' t1 t2 accum
11.1110 + val M = mtype_for T
11.1111 + val (m', accum) = do_term t' (accum |>> push_bound M)
11.1112 + in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end)
11.1113 + | (t0 as Const (@{const_name All}, _))
11.1114 + $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) =>
11.1115 + do_bounded_quantifier t0 s' T' t10 t11 t12 accum
11.1116 + | (t0 as Const (@{const_name Ex}, _))
11.1117 + $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) =>
11.1118 + do_bounded_quantifier t0 s' T' t10 t11 t12 accum
11.1119 | Const (@{const_name Let}, _) $ t1 $ t2 =>
11.1120 do_term (betapply (t2, t1)) accum
11.1121 | t1 $ t2 =>
11.1122 let
11.1123 - val (C1, accum) = do_term t1 accum
11.1124 - val (C2, accum) = do_term t2 accum
11.1125 + val (m1, accum) = do_term t1 accum
11.1126 + val (m2, accum) = do_term t2 accum
11.1127 in
11.1128 case accum of
11.1129 - (_, UnsolvableCSet) => unsolvable
11.1130 - | _ => case C1 of
11.1131 - CFun (C11, _, C12) =>
11.1132 - (C12, accum ||> add_is_sub_ctype C2 C11)
11.1133 - | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \
11.1134 - \(op $)", [C1])
11.1135 + (_, UnsolvableCSet) => mterm_unsolvable t
11.1136 + | _ =>
11.1137 + let
11.1138 + val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
11.1139 + val M2 = mtype_of_mterm m2
11.1140 + in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
11.1141 end)
11.1142 - |> tap (fn (C, _) =>
11.1143 - print_g (" \<Gamma> \<turnstile> " ^
11.1144 - Syntax.string_of_term ctxt t ^ " : " ^
11.1145 - string_for_ctype C))
11.1146 + |> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^
11.1147 + string_for_mterm ctxt m))
11.1148 in do_term end
11.1149
11.1150 -(* cdata -> sign -> term -> accumulator -> accumulator *)
11.1151 -fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) =
11.1152 +(* mdata -> styp -> term -> term -> mterm * accumulator *)
11.1153 +fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
11.1154 let
11.1155 - (* typ -> ctype *)
11.1156 - val ctype_for = fresh_ctype_for_type cdata
11.1157 - (* term -> accumulator -> ctype * accumulator *)
11.1158 - val do_term = consider_term cdata
11.1159 - (* sign -> term -> accumulator -> accumulator *)
11.1160 - fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
11.1161 - | do_formula sn t (accum as (gamma, cset)) =
11.1162 + val (m1, accum) = consider_term mdata t1 accum
11.1163 + val (m2, accum) = consider_term mdata t2 accum
11.1164 + val M1 = mtype_of_mterm m1
11.1165 + val M2 = mtype_of_mterm m2
11.1166 + val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
11.1167 + in
11.1168 + (MApp (MApp (MRaw (Const x,
11.1169 + MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
11.1170 + accum ||> add_mtypes_equal M1 M2)
11.1171 + end
11.1172 +
11.1173 +(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
11.1174 +fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
11.1175 + let
11.1176 + (* typ -> mtyp *)
11.1177 + val mtype_for = fresh_mtype_for_type mdata
11.1178 + (* term -> accumulator -> mterm * accumulator *)
11.1179 + val do_term = consider_term mdata
11.1180 + (* sign -> term -> accumulator -> mterm * accumulator *)
11.1181 + fun do_formula _ t (_, UnsolvableCSet) =
11.1182 + (MRaw (t, dummy_M), unsolvable_accum)
11.1183 + | do_formula sn t accum =
11.1184 let
11.1185 - (* term -> accumulator -> accumulator *)
11.1186 - val do_co_formula = do_formula sn
11.1187 - val do_contra_formula = do_formula (negate sn)
11.1188 - (* string -> typ -> term -> accumulator *)
11.1189 - fun do_quantifier quant_s abs_T body_t =
11.1190 + (* styp -> string -> typ -> term -> mterm * accumulator *)
11.1191 + fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
11.1192 let
11.1193 - val abs_C = ctype_for abs_T
11.1194 + val abs_M = mtype_for abs_T
11.1195 val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
11.1196 - val cset = cset |> side_cond ? add_ctype_is_right_total abs_C
11.1197 + val (body_m, accum) =
11.1198 + accum ||> side_cond ? add_mtype_is_right_total abs_M
11.1199 + |>> push_bound abs_M |> do_formula sn body_t
11.1200 + val body_M = mtype_of_mterm body_m
11.1201 in
11.1202 - (gamma |> push_bound abs_C, cset) |> do_co_formula body_t
11.1203 - |>> pop_bound
11.1204 + (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
11.1205 + MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
11.1206 + accum |>> pop_bound)
11.1207 end
11.1208 - (* typ -> term -> accumulator *)
11.1209 - fun do_bounded_quantifier abs_T body_t =
11.1210 - accum |>> push_bound (ctype_for abs_T) |> do_co_formula body_t
11.1211 - |>> pop_bound
11.1212 - (* term -> term -> accumulator *)
11.1213 - fun do_equals t1 t2 =
11.1214 + (* styp -> term -> term -> mterm * accumulator *)
11.1215 + fun do_equals x t1 t2 =
11.1216 case sn of
11.1217 - Plus => do_term t accum |> snd
11.1218 - | Minus => let
11.1219 - val (C1, accum) = do_term t1 accum
11.1220 - val (C2, accum) = do_term t2 accum
11.1221 - in accum ||> add_ctypes_equal C1 C2 end
11.1222 + Plus => do_term t accum
11.1223 + | Minus => consider_general_equals mdata x t1 t2 accum
11.1224 in
11.1225 case t of
11.1226 - Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
11.1227 - do_quantifier s0 T1 t1
11.1228 - | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
11.1229 - | @{const "==>"} $ t1 $ t2 =>
11.1230 - accum |> do_contra_formula t1 |> do_co_formula t2
11.1231 - | @{const Trueprop} $ t1 => do_co_formula t1 accum
11.1232 - | @{const Not} $ t1 => do_contra_formula t1 accum
11.1233 - | Const (@{const_name All}, _)
11.1234 - $ Abs (_, T1, t1 as @{const "op -->"} $ (_ $ Bound 0) $ _) =>
11.1235 - do_bounded_quantifier T1 t1
11.1236 - | Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>
11.1237 - do_quantifier s0 T1 t1
11.1238 - | Const (@{const_name Ex}, _)
11.1239 - $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
11.1240 - do_bounded_quantifier T1 t1
11.1241 - | Const (s0 as @{const_name Ex}, _) $ Abs (_, T1, t1) =>
11.1242 - do_quantifier s0 T1 t1
11.1243 - | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
11.1244 - | @{const "op &"} $ t1 $ t2 =>
11.1245 - accum |> do_co_formula t1 |> do_co_formula t2
11.1246 - | @{const "op |"} $ t1 $ t2 =>
11.1247 - accum |> do_co_formula t1 |> do_co_formula t2
11.1248 - | @{const "op -->"} $ t1 $ t2 =>
11.1249 - accum |> do_contra_formula t1 |> do_co_formula t2
11.1250 - | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
11.1251 - accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
11.1252 - | Const (@{const_name Let}, _) $ t1 $ t2 =>
11.1253 - do_co_formula (betapply (t2, t1)) accum
11.1254 - | _ => do_term t accum |> snd
11.1255 + Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
11.1256 + do_quantifier x s1 T1 t1
11.1257 + | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
11.1258 + | @{const Trueprop} $ t1 =>
11.1259 + let val (m1, accum) = do_formula sn t1 accum in
11.1260 + (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
11.1261 + m1), accum)
11.1262 + end
11.1263 + | @{const Not} $ t1 =>
11.1264 + let val (m1, accum) = do_formula (negate sn) t1 accum in
11.1265 + (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
11.1266 + accum)
11.1267 + end
11.1268 + | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
11.1269 + do_quantifier x s1 T1 t1
11.1270 + | Const (x0 as (s0 as @{const_name Ex}, T0))
11.1271 + $ (t1 as Abs (s1, T1, t1')) =>
11.1272 + (case sn of
11.1273 + Plus => do_quantifier x0 s1 T1 t1'
11.1274 + | Minus =>
11.1275 + (* ### do elsewhere *)
11.1276 + do_term (@{const Not}
11.1277 + $ (HOLogic.eq_const (domain_type T0) $ t1
11.1278 + $ Abs (Name.uu, T1, @{const False}))) accum)
11.1279 + | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
11.1280 + do_equals x t1 t2
11.1281 + | (t0 as Const (s0, _)) $ t1 $ t2 =>
11.1282 + if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
11.1283 + s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
11.1284 + let
11.1285 + val impl = (s0 = @{const_name "==>"} orelse
11.1286 + s0 = @{const_name "op -->"})
11.1287 + val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
11.1288 + val (m2, accum) = do_formula sn t2 accum
11.1289 + in
11.1290 + (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
11.1291 + accum)
11.1292 + end
11.1293 + else
11.1294 + do_term t accum
11.1295 + | _ => do_term t accum
11.1296 end
11.1297 - |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
11.1298 - Syntax.string_of_term ctxt t ^
11.1299 - " : o\<^sup>" ^ string_for_sign sn))
11.1300 + |> tap (fn (m, _) =>
11.1301 + print_g ("\<Gamma> \<turnstile> " ^
11.1302 + string_for_mterm ctxt m ^ " : o\<^sup>" ^
11.1303 + string_for_sign sn))
11.1304 in do_formula end
11.1305
11.1306 (* The harmless axiom optimization below is somewhat too aggressive in the face
11.1307 @@ -877,79 +988,110 @@
11.1308 |> (forall (member (op =) harmless_consts o original_name o fst)
11.1309 orf exists (member (op =) bounteous_consts o fst))
11.1310
11.1311 -(* cdata -> sign -> term -> accumulator -> accumulator *)
11.1312 -fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t =
11.1313 - not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata sn t
11.1314 +(* mdata -> term -> accumulator -> mterm * accumulator *)
11.1315 +fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
11.1316 + if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
11.1317 + else consider_general_formula mdata Plus t
11.1318
11.1319 -(* cdata -> term -> accumulator -> accumulator *)
11.1320 -fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t =
11.1321 +(* mdata -> term -> accumulator -> mterm * accumulator *)
11.1322 +fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
11.1323 if not (is_constr_pattern_formula thy t) then
11.1324 - consider_nondefinitional_axiom cdata Plus t
11.1325 + consider_nondefinitional_axiom mdata t
11.1326 else if is_harmless_axiom hol_ctxt t then
11.1327 - I
11.1328 + pair (MRaw (t, dummy_M))
11.1329 else
11.1330 let
11.1331 - (* term -> accumulator -> ctype * accumulator *)
11.1332 - val do_term = consider_term cdata
11.1333 - (* typ -> term -> accumulator -> accumulator *)
11.1334 - fun do_all abs_T body_t accum =
11.1335 - let val abs_C = fresh_ctype_for_type cdata abs_T in
11.1336 - accum |>> push_bound abs_C |> do_formula body_t |>> pop_bound
11.1337 + (* typ -> mtyp *)
11.1338 + val mtype_for = fresh_mtype_for_type mdata
11.1339 + (* term -> accumulator -> mterm * accumulator *)
11.1340 + val do_term = consider_term mdata
11.1341 + (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
11.1342 + fun do_all quant_t abs_s abs_T body_t accum =
11.1343 + let
11.1344 + val abs_M = mtype_for abs_T
11.1345 + val (body_m, accum) =
11.1346 + accum |>> push_bound abs_M |> do_formula body_t
11.1347 + val body_M = mtype_of_mterm body_m
11.1348 + in
11.1349 + (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
11.1350 + MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
11.1351 + accum |>> pop_bound)
11.1352 end
11.1353 - (* term -> term -> accumulator -> accumulator *)
11.1354 - and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
11.1355 - and do_equals t1 t2 accum =
11.1356 + (* term -> term -> term -> accumulator -> mterm * accumulator *)
11.1357 + and do_conjunction t0 t1 t2 accum =
11.1358 let
11.1359 - val (C1, accum) = do_term t1 accum
11.1360 - val (C2, accum) = do_term t2 accum
11.1361 - in accum ||> add_ctypes_equal C1 C2 end
11.1362 + val (m1, accum) = do_formula t1 accum
11.1363 + val (m2, accum) = do_formula t2 accum
11.1364 + in
11.1365 + (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
11.1366 + end
11.1367 + and do_implies t0 t1 t2 accum =
11.1368 + let
11.1369 + val (m1, accum) = do_term t1 accum
11.1370 + val (m2, accum) = do_formula t2 accum
11.1371 + in
11.1372 + (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
11.1373 + end
11.1374 (* term -> accumulator -> accumulator *)
11.1375 - and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
11.1376 + and do_formula t (_, UnsolvableCSet) =
11.1377 + (MRaw (t, dummy_M), unsolvable_accum)
11.1378 | do_formula t accum =
11.1379 case t of
11.1380 - Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
11.1381 + (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
11.1382 + do_all t0 s1 T1 t1 accum
11.1383 | @{const Trueprop} $ t1 => do_formula t1 accum
11.1384 - | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum
11.1385 - | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
11.1386 - | @{const Pure.conjunction} $ t1 $ t2 =>
11.1387 - accum |> do_formula t1 |> do_formula t2
11.1388 - | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
11.1389 - | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
11.1390 - | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
11.1391 - | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
11.1392 + | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
11.1393 + consider_general_equals mdata x t1 t2 accum
11.1394 + | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
11.1395 + | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
11.1396 + do_conjunction t0 t1 t2 accum
11.1397 + | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
11.1398 + do_all t0 s0 T1 t1 accum
11.1399 + | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
11.1400 + consider_general_equals mdata x t1 t2 accum
11.1401 + | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
11.1402 + | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
11.1403 | _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
11.1404 \do_formula", [t])
11.1405 in do_formula t end
11.1406
11.1407 -(* Proof.context -> literal list -> term -> ctype -> string *)
11.1408 -fun string_for_ctype_of_term ctxt lits t C =
11.1409 +(* Proof.context -> literal list -> term -> mtyp -> string *)
11.1410 +fun string_for_mtype_of_term ctxt lits t M =
11.1411 Syntax.string_of_term ctxt t ^ " : " ^
11.1412 - string_for_ctype (instantiate_ctype lits C)
11.1413 + string_for_mtype (instantiate_mtype lits M)
11.1414
11.1415 -(* theory -> literal list -> ctype_context -> unit *)
11.1416 -fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) =
11.1417 - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @
11.1418 - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts
11.1419 +(* theory -> literal list -> mtype_context -> unit *)
11.1420 +fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) =
11.1421 + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @
11.1422 + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
11.1423 |> cat_lines |> print_g
11.1424
11.1425 -(* hol_context -> bool -> typ -> sign -> term list -> term list -> term
11.1426 - -> bool *)
11.1427 -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts
11.1428 - nondef_ts core_t =
11.1429 +(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
11.1430 +fun gather f t (ms, accum) =
11.1431 + let val (m, accum) = f t accum in (m :: ms, accum) end
11.1432 +
11.1433 +(* hol_context -> bool -> typ -> term list * term list -> bool *)
11.1434 +fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
11.1435 + (nondef_ts, def_ts) =
11.1436 let
11.1437 - val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^
11.1438 + val _ = print_g ("****** Monotonicity analysis: " ^
11.1439 + string_for_mtype MAlpha ^ " is " ^
11.1440 Syntax.string_of_typ ctxt alpha_T)
11.1441 - val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T
11.1442 - val (gamma, cset) =
11.1443 - (initial_gamma, slack)
11.1444 - |> fold (consider_definitional_axiom cdata) def_ts
11.1445 - |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts
11.1446 - |> consider_general_formula cdata sn core_t
11.1447 + val mdata as {max_fresh, constr_cache, ...} =
11.1448 + initial_mdata hol_ctxt binarize alpha_T
11.1449 +
11.1450 + val accum = (initial_gamma, slack)
11.1451 + val (nondef_ms, accum) =
11.1452 + ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
11.1453 + |> fold (gather (consider_nondefinitional_axiom mdata))
11.1454 + (tl nondef_ts)
11.1455 + val (def_ms, (gamma, cset)) =
11.1456 + ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
11.1457 in
11.1458 case solve (!max_fresh) cset of
11.1459 - SOME lits => (print_ctype_context ctxt lits gamma; true)
11.1460 + SOME lits => (print_mtype_context ctxt lits gamma; true)
11.1461 | _ => false
11.1462 end
11.1463 - handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs))
11.1464 + handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms))
11.1465
11.1466 end;
12.1 --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 26 13:29:43 2010 +0100
12.2 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 26 16:50:09 2010 +0100
12.3 @@ -1031,7 +1031,7 @@
12.4 if is_opt_rep R then
12.5 triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2)
12.6 else if opt andalso polar = Pos andalso
12.7 - not (is_concrete_type datatypes (type_of u1)) then
12.8 + not (is_concrete_type datatypes true (type_of u1)) then
12.9 Cst (False, T, Formula Pos)
12.10 else
12.11 s_op2 Subset T R u1 u2
12.12 @@ -1057,7 +1057,7 @@
12.13 else opt_opt_case ()
12.14 in
12.15 if unsound orelse polar = Neg orelse
12.16 - is_concrete_type datatypes (type_of u1) then
12.17 + is_concrete_type datatypes true (type_of u1) then
12.18 case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
12.19 (true, true) => opt_opt_case ()
12.20 | (true, false) => hybrid_case u1'
12.21 @@ -1159,7 +1159,7 @@
12.22 let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
12.23 if def orelse
12.24 (unsound andalso (polar = Pos) = (oper = All)) orelse
12.25 - is_complete_type datatypes (type_of u1) then
12.26 + is_complete_type datatypes true (type_of u1) then
12.27 quant_u
12.28 else
12.29 let
12.30 @@ -1202,7 +1202,7 @@
12.31 else unopt_R |> opt ? opt_rep ofs T
12.32 val u = Op2 (oper, T, R, u1', sub u2)
12.33 in
12.34 - if is_complete_type datatypes T orelse not opt1 then
12.35 + if is_complete_type datatypes true T orelse not opt1 then
12.36 u
12.37 else
12.38 let
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Feb 26 13:29:43 2010 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Feb 26 16:50:09 2010 +0100
13.3 @@ -126,7 +126,7 @@
13.4 val norm_frac_rel = (4, 0)
13.5
13.6 (* int -> bool -> rel_expr *)
13.7 -fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool
13.8 +fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool
13.9 (* bool -> formula *)
13.10 fun formula_for_bool b = if b then True else False
13.11
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 13:29:43 2010 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 16:50:09 2010 +0100
14.3 @@ -9,8 +9,7 @@
14.4 sig
14.5 type hol_context = Nitpick_HOL.hol_context
14.6 val preprocess_term :
14.7 - hol_context -> term
14.8 - -> ((term list * term list) * (bool * bool)) * term * bool
14.9 + hol_context -> term -> term list * term list * bool * bool * bool
14.10 end
14.11
14.12 structure Nitpick_Preproc : NITPICK_PREPROC =
14.13 @@ -136,6 +135,59 @@
14.14 (index_seq 0 (length arg_Ts)) arg_Ts)
14.15 end
14.16
14.17 +(* (term -> term) -> int -> term -> term *)
14.18 +fun coerce_bound_no f j t =
14.19 + case t of
14.20 + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
14.21 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
14.22 + | Bound j' => if j' = j then f t else t
14.23 + | _ => t
14.24 +(* hol_context -> typ -> typ -> term -> term *)
14.25 +fun coerce_bound_0_in_term hol_ctxt new_T old_T =
14.26 + old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0
14.27 +(* hol_context -> typ list -> typ -> typ -> term -> term *)
14.28 +and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t =
14.29 + if old_T = new_T then
14.30 + t
14.31 + else
14.32 + case (new_T, old_T) of
14.33 + (Type (new_s, new_Ts as [new_T1, new_T2]),
14.34 + Type ("fun", [old_T1, old_T2])) =>
14.35 + (case eta_expand Ts t 1 of
14.36 + Abs (s, _, t') =>
14.37 + Abs (s, new_T1,
14.38 + t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1
14.39 + |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2)
14.40 + |> Envir.eta_contract
14.41 + |> new_s <> "fun"
14.42 + ? construct_value thy stds
14.43 + (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
14.44 + o single
14.45 + | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']))
14.46 + | (Type (new_s, new_Ts as [new_T1, new_T2]),
14.47 + Type (old_s, old_Ts as [old_T1, old_T2])) =>
14.48 + if old_s = @{type_name fun_box} orelse
14.49 + old_s = @{type_name pair_box} orelse old_s = "*" then
14.50 + case constr_expand hol_ctxt old_T t of
14.51 + Const (old_s, _) $ t1 =>
14.52 + if new_s = "fun" then
14.53 + coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1
14.54 + else
14.55 + construct_value thy stds
14.56 + (old_s, Type ("fun", new_Ts) --> new_T)
14.57 + [coerce_term hol_ctxt Ts (Type ("fun", new_Ts))
14.58 + (Type ("fun", old_Ts)) t1]
14.59 + | Const _ $ t1 $ t2 =>
14.60 + construct_value thy stds
14.61 + (if new_s = "*" then @{const_name Pair}
14.62 + else @{const_name PairBox}, new_Ts ---> new_T)
14.63 + [coerce_term hol_ctxt Ts new_T1 old_T1 t1,
14.64 + coerce_term hol_ctxt Ts new_T2 old_T2 t2]
14.65 + | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t'])
14.66 + else
14.67 + raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
14.68 + | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t])
14.69 +
14.70 (* hol_context -> bool -> term -> term *)
14.71 fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def
14.72 orig_t =
14.73 @@ -146,60 +198,6 @@
14.74 | box_relational_operator_type (Type ("*", Ts)) =
14.75 Type ("*", map (box_type hol_ctxt InPair) Ts)
14.76 | box_relational_operator_type T = T
14.77 - (* (term -> term) -> int -> term -> term *)
14.78 - fun coerce_bound_no f j t =
14.79 - case t of
14.80 - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2
14.81 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t')
14.82 - | Bound j' => if j' = j then f t else t
14.83 - | _ => t
14.84 - (* typ -> typ -> term -> term *)
14.85 - fun coerce_bound_0_in_term new_T old_T =
14.86 - old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0
14.87 - (* typ list -> typ -> term -> term *)
14.88 - and coerce_term Ts new_T old_T t =
14.89 - if old_T = new_T then
14.90 - t
14.91 - else
14.92 - case (new_T, old_T) of
14.93 - (Type (new_s, new_Ts as [new_T1, new_T2]),
14.94 - Type ("fun", [old_T1, old_T2])) =>
14.95 - (case eta_expand Ts t 1 of
14.96 - Abs (s, _, t') =>
14.97 - Abs (s, new_T1,
14.98 - t' |> coerce_bound_0_in_term new_T1 old_T1
14.99 - |> coerce_term (new_T1 :: Ts) new_T2 old_T2)
14.100 - |> Envir.eta_contract
14.101 - |> new_s <> "fun"
14.102 - ? construct_value thy stds
14.103 - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
14.104 - o single
14.105 - | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
14.106 - \coerce_term", [t']))
14.107 - | (Type (new_s, new_Ts as [new_T1, new_T2]),
14.108 - Type (old_s, old_Ts as [old_T1, old_T2])) =>
14.109 - if old_s = @{type_name fun_box} orelse
14.110 - old_s = @{type_name pair_box} orelse old_s = "*" then
14.111 - case constr_expand hol_ctxt old_T t of
14.112 - Const (@{const_name FunBox}, _) $ t1 =>
14.113 - if new_s = "fun" then
14.114 - coerce_term Ts new_T (Type ("fun", old_Ts)) t1
14.115 - else
14.116 - construct_value thy stds
14.117 - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T)
14.118 - [coerce_term Ts (Type ("fun", new_Ts))
14.119 - (Type ("fun", old_Ts)) t1]
14.120 - | Const _ $ t1 $ t2 =>
14.121 - construct_value thy stds
14.122 - (if new_s = "*" then @{const_name Pair}
14.123 - else @{const_name PairBox}, new_Ts ---> new_T)
14.124 - [coerce_term Ts new_T1 old_T1 t1,
14.125 - coerce_term Ts new_T2 old_T2 t2]
14.126 - | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\
14.127 - \coerce_term", [t'])
14.128 - else
14.129 - raise TYPE ("coerce_term", [new_T, old_T], [t])
14.130 - | _ => raise TYPE ("coerce_term", [new_T, old_T], [t])
14.131 (* indexname * typ -> typ * term -> typ option list -> typ option list *)
14.132 fun add_boxed_types_for_var (z as (_, T)) (T', t') =
14.133 case t' of
14.134 @@ -252,7 +250,7 @@
14.135 val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last
14.136 in
14.137 list_comb (Const (s0, T --> T --> body_type T0),
14.138 - map2 (coerce_term new_Ts T) [T1, T2] [t1, t2])
14.139 + map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2])
14.140 end
14.141 (* string -> typ -> term *)
14.142 and do_description_operator s T =
14.143 @@ -320,7 +318,7 @@
14.144 val T' = hd (snd (dest_Type (hd Ts1)))
14.145 val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2')
14.146 val T2 = fastype_of1 (new_Ts, t2)
14.147 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
14.148 + val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
14.149 in
14.150 betapply (if s1 = "fun" then
14.151 t1
14.152 @@ -336,7 +334,7 @@
14.153 val (s1, Ts1) = dest_Type T1
14.154 val t2 = do_term new_Ts old_Ts Neut t2
14.155 val T2 = fastype_of1 (new_Ts, t2)
14.156 - val t2 = coerce_term new_Ts (hd Ts1) T2 t2
14.157 + val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2
14.158 in
14.159 betapply (if s1 = "fun" then
14.160 t1
14.161 @@ -474,6 +472,19 @@
14.162 (list_comb (t, args), seen)
14.163 in aux [] 0 t [] [] |> fst end
14.164
14.165 +val let_var_prefix = nitpick_prefix ^ "l"
14.166 +val let_inline_threshold = 32
14.167 +
14.168 +(* int -> typ -> term -> (term -> term) -> term *)
14.169 +fun hol_let n abs_T body_T f t =
14.170 + if n * size_of_term t <= let_inline_threshold then
14.171 + f t
14.172 + else
14.173 + let val z = ((let_var_prefix, 0), abs_T) in
14.174 + Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
14.175 + $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
14.176 + end
14.177 +
14.178 (* hol_context -> bool -> term -> term *)
14.179 fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
14.180 let
14.181 @@ -508,14 +519,19 @@
14.182 if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
14.183 else raise SAME ()
14.184 | (Const (x as (s, T)), args) =>
14.185 - let val arg_Ts = binder_types T in
14.186 - if length arg_Ts = length args andalso
14.187 - (is_constr thy stds x orelse s = @{const_name Pair}) andalso
14.188 + let
14.189 + val (arg_Ts, dataT) = strip_type T
14.190 + val n = length arg_Ts
14.191 + in
14.192 + if length args = n andalso
14.193 + (is_constr thy stds x orelse s = @{const_name Pair} orelse
14.194 + x = (@{const_name Suc}, nat_T --> nat_T)) andalso
14.195 (not careful orelse not (is_Var t1) orelse
14.196 String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
14.197 - discriminate_value hol_ctxt x t1 ::
14.198 - map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
14.199 - |> foldr1 s_conj
14.200 + hol_let (n + 1) dataT bool_T
14.201 + (fn t1 => discriminate_value hol_ctxt x t1 ::
14.202 + map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
14.203 + |> foldr1 s_conj) t1
14.204 else
14.205 raise SAME ()
14.206 end
14.207 @@ -1020,7 +1036,7 @@
14.208 (* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
14.209 val axioms_max_depth = 255
14.210
14.211 -(* hol_context -> term -> (term list * term list) * (bool * bool) *)
14.212 +(* hol_context -> term -> term list * term list * bool * bool *)
14.213 fun axioms_for_term
14.214 (hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
14.215 fast_descrs, evals, def_table, nondef_table, user_nondefs,
14.216 @@ -1170,10 +1186,9 @@
14.217 |> user_axioms = SOME true
14.218 ? fold (add_nondef_axiom 1) mono_user_nondefs
14.219 val defs = defs @ special_congruence_axioms hol_ctxt xs
14.220 - in
14.221 - ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
14.222 - null poly_user_nondefs))
14.223 - end
14.224 + val got_all_mono_user_axioms =
14.225 + (user_axioms = SOME true orelse null mono_user_nondefs)
14.226 + in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
14.227
14.228 (** Simplification of constructor/selector terms **)
14.229
14.230 @@ -1275,7 +1290,7 @@
14.231
14.232 (* Maximum number of quantifiers in a cluster for which the exponential
14.233 algorithm is used. Larger clusters use a heuristic inspired by Claessen &
14.234 - Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
14.235 + Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
14.236 paper). *)
14.237 val quantifier_cluster_threshold = 7
14.238
14.239 @@ -1386,29 +1401,29 @@
14.240
14.241 (** Preprocessor entry point **)
14.242
14.243 -(* hol_context -> term
14.244 - -> ((term list * term list) * (bool * bool)) * term * bool *)
14.245 +(* hol_context -> term -> term list * term list * bool * bool * bool *)
14.246 fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
14.247 boxes, skolemize, uncurry, ...}) t =
14.248 let
14.249 val skolem_depth = if skolemize then 4 else ~1
14.250 - val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
14.251 - core_t) = t |> unfold_defs_in_term hol_ctxt
14.252 - |> close_form
14.253 - |> skolemize_term_and_more hol_ctxt skolem_depth
14.254 - |> specialize_consts_in_term hol_ctxt 0
14.255 - |> `(axioms_for_term hol_ctxt)
14.256 + val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
14.257 + t |> unfold_defs_in_term hol_ctxt
14.258 + |> close_form
14.259 + |> skolemize_term_and_more hol_ctxt skolem_depth
14.260 + |> specialize_consts_in_term hol_ctxt 0
14.261 + |> axioms_for_term hol_ctxt
14.262 val binarize =
14.263 is_standard_datatype thy stds nat_T andalso
14.264 case binary_ints of
14.265 SOME false => false
14.266 - | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
14.267 + | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso
14.268 (binary_ints = SOME true orelse
14.269 - exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
14.270 + exists should_use_binary_ints (nondef_ts @ def_ts))
14.271 val box = exists (not_equal (SOME false) o snd) boxes
14.272 + val uncurry = uncurry andalso box
14.273 val table =
14.274 - Termtab.empty |> uncurry
14.275 - ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
14.276 + Termtab.empty
14.277 + |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
14.278 (* bool -> term -> term *)
14.279 fun do_rest def =
14.280 binarize ? binarize_nat_and_int_in_term
14.281 @@ -1425,10 +1440,10 @@
14.282 #> push_quantifiers_inward
14.283 #> close_form
14.284 #> Term.map_abs_vars shortest_name
14.285 + val nondef_ts = map (do_rest false) nondef_ts
14.286 + val def_ts = map (do_rest true) def_ts
14.287 in
14.288 - (((map (do_rest true) def_ts, map (do_rest false) nondef_ts),
14.289 - (got_all_mono_user_axioms, no_poly_user_axioms)),
14.290 - do_rest false core_t, binarize)
14.291 + (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
14.292 end
14.293
14.294 end;
15.1 --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Feb 26 13:29:43 2010 +0100
15.2 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Feb 26 16:50:09 2010 +0100
15.3 @@ -299,7 +299,7 @@
15.4 | z => Func z)
15.5 | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T
15.6 fun best_set_rep_for_type (scope as {datatypes, ...}) T =
15.7 - (if is_exact_type datatypes T then best_non_opt_set_rep_for_type
15.8 + (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type
15.9 else best_opt_set_rep_for_type) scope T
15.10 fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...})
15.11 (Type ("fun", [T1, T2])) =
16.1 --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 26 13:29:43 2010 +0100
16.2 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 26 16:50:09 2010 +0100
16.3 @@ -23,8 +23,8 @@
16.4 card: int,
16.5 co: bool,
16.6 standard: bool,
16.7 - complete: bool,
16.8 - concrete: bool,
16.9 + complete: bool * bool,
16.10 + concrete: bool * bool,
16.11 deep: bool,
16.12 constrs: constr_spec list}
16.13
16.14 @@ -39,9 +39,9 @@
16.15
16.16 val datatype_spec : dtype_spec list -> typ -> dtype_spec option
16.17 val constr_spec : dtype_spec list -> styp -> constr_spec
16.18 - val is_complete_type : dtype_spec list -> typ -> bool
16.19 - val is_concrete_type : dtype_spec list -> typ -> bool
16.20 - val is_exact_type : dtype_spec list -> typ -> bool
16.21 + val is_complete_type : dtype_spec list -> bool -> typ -> bool
16.22 + val is_concrete_type : dtype_spec list -> bool -> typ -> bool
16.23 + val is_exact_type : dtype_spec list -> bool -> typ -> bool
16.24 val offset_of_type : int Typtab.table -> typ -> int
16.25 val spec_of_type : scope -> typ -> int * int
16.26 val pretties_for_scope : scope -> bool -> Pretty.T list
16.27 @@ -51,7 +51,7 @@
16.28 val all_scopes :
16.29 hol_context -> bool -> int -> (typ option * int list) list
16.30 -> (styp option * int list) list -> (styp option * int list) list
16.31 - -> int list -> int list -> typ list -> typ list -> typ list
16.32 + -> int list -> int list -> typ list -> typ list -> typ list -> typ list
16.33 -> int * scope list
16.34 end;
16.35
16.36 @@ -74,8 +74,8 @@
16.37 card: int,
16.38 co: bool,
16.39 standard: bool,
16.40 - complete: bool,
16.41 - concrete: bool,
16.42 + complete: bool * bool,
16.43 + concrete: bool * bool,
16.44 deep: bool,
16.45 constrs: constr_spec list}
16.46
16.47 @@ -105,22 +105,24 @@
16.48 SOME c => c
16.49 | NONE => constr_spec dtypes x
16.50
16.51 -(* dtype_spec list -> typ -> bool *)
16.52 -fun is_complete_type dtypes (Type ("fun", [T1, T2])) =
16.53 - is_concrete_type dtypes T1 andalso is_complete_type dtypes T2
16.54 - | is_complete_type dtypes (Type ("*", Ts)) =
16.55 - forall (is_complete_type dtypes) Ts
16.56 - | is_complete_type dtypes T =
16.57 +(* dtype_spec list -> bool -> typ -> bool *)
16.58 +fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) =
16.59 + is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2
16.60 + | is_complete_type dtypes facto (Type ("*", Ts)) =
16.61 + forall (is_complete_type dtypes facto) Ts
16.62 + | is_complete_type dtypes facto T =
16.63 not (is_integer_like_type T) andalso not (is_bit_type T) andalso
16.64 - #complete (the (datatype_spec dtypes T))
16.65 + fun_from_pair (#complete (the (datatype_spec dtypes T))) facto
16.66 handle Option.Option => true
16.67 -and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
16.68 - is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
16.69 - | is_concrete_type dtypes (Type ("*", Ts)) =
16.70 - forall (is_concrete_type dtypes) Ts
16.71 - | is_concrete_type dtypes T =
16.72 - #concrete (the (datatype_spec dtypes T)) handle Option.Option => true
16.73 -fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes
16.74 +and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) =
16.75 + is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2
16.76 + | is_concrete_type dtypes facto (Type ("*", Ts)) =
16.77 + forall (is_concrete_type dtypes facto) Ts
16.78 + | is_concrete_type dtypes facto T =
16.79 + fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto
16.80 + handle Option.Option => true
16.81 +fun is_exact_type dtypes facto =
16.82 + is_complete_type dtypes facto andf is_concrete_type dtypes facto
16.83
16.84 (* int Typtab.table -> typ -> int *)
16.85 fun offset_of_type ofs T =
16.86 @@ -461,15 +463,18 @@
16.87 explicit_max = max, total = total} :: constrs
16.88 end
16.89
16.90 -(* hol_context -> (typ * int) list -> typ -> bool *)
16.91 -fun has_exact_card hol_ctxt card_assigns T =
16.92 +(* hol_context -> bool -> typ list -> (typ * int) list -> typ -> bool *)
16.93 +fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T =
16.94 let val card = card_of_type card_assigns T in
16.95 - card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T
16.96 + card = bounded_exact_card_of_type hol_ctxt
16.97 + (if facto then finitizable_dataTs else []) (card + 1) 0
16.98 + card_assigns T
16.99 end
16.100
16.101 -(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *)
16.102 +(* hol_context -> bool -> typ list -> typ list -> scope_desc -> typ * int
16.103 + -> dtype_spec *)
16.104 fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize
16.105 - deep_dataTs (desc as (card_assigns, _)) (T, card) =
16.106 + deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) =
16.107 let
16.108 val deep = member (op =) deep_dataTs T
16.109 val co = is_codatatype thy T
16.110 @@ -478,10 +483,16 @@
16.111 val self_recs = map (is_self_recursive_constr_type o snd) xs
16.112 val (num_self_recs, num_non_self_recs) =
16.113 List.partition I self_recs |> pairself length
16.114 - val complete = has_exact_card hol_ctxt card_assigns T
16.115 - val concrete = is_word_type T orelse
16.116 - (xs |> maps (binder_types o snd) |> maps binder_types
16.117 - |> forall (has_exact_card hol_ctxt card_assigns))
16.118 + (* bool -> bool *)
16.119 + fun is_complete facto =
16.120 + has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T
16.121 + fun is_concrete facto =
16.122 + is_word_type T orelse
16.123 + xs |> maps (binder_types o snd) |> maps binder_types
16.124 + |> forall (has_exact_card hol_ctxt facto finitizable_dataTs
16.125 + card_assigns)
16.126 + val complete = pair_from_fun is_complete
16.127 + val concrete = pair_from_fun is_concrete
16.128 (* int -> int *)
16.129 fun sum_dom_cards max =
16.130 map (domain_card max card_assigns o snd) xs |> Integer.sum
16.131 @@ -494,13 +505,15 @@
16.132 concrete = concrete, deep = deep, constrs = constrs}
16.133 end
16.134
16.135 -(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *)
16.136 +(* hol_context -> bool -> int -> typ list -> typ list -> scope_desc -> scope *)
16.137 fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break
16.138 - deep_dataTs (desc as (card_assigns, _)) =
16.139 + deep_dataTs finitizable_dataTs
16.140 + (desc as (card_assigns, _)) =
16.141 let
16.142 val datatypes =
16.143 map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs
16.144 - desc) (filter (is_datatype thy stds o fst) card_assigns)
16.145 + finitizable_dataTs desc)
16.146 + (filter (is_datatype thy stds o fst) card_assigns)
16.147 val bits = card_of_type card_assigns @{typ signed_bit} - 1
16.148 handle TYPE ("Nitpick_HOL.card_of_type", _, _) =>
16.149 card_of_type card_assigns @{typ unsigned_bit}
16.150 @@ -530,10 +543,10 @@
16.151
16.152 (* hol_context -> bool -> int -> (typ option * int list) list
16.153 -> (styp option * int list) list -> (styp option * int list) list -> int list
16.154 - -> typ list -> typ list -> typ list -> int * scope list *)
16.155 + -> typ list -> typ list -> typ list ->typ list -> int * scope list *)
16.156 fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns
16.157 maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts
16.158 - deep_dataTs =
16.159 + deep_dataTs finitizable_dataTs =
16.160 let
16.161 val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts
16.162 cards_assigns
16.163 @@ -550,7 +563,7 @@
16.164 (length all - length head,
16.165 descs |> length descs <= distinct_threshold ? distinct (op =)
16.166 |> map (scope_from_descriptor hol_ctxt binarize sym_break
16.167 - deep_dataTs))
16.168 + deep_dataTs finitizable_dataTs))
16.169 end
16.170
16.171 end;
17.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Feb 26 13:29:43 2010 +0100
17.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Feb 26 16:50:09 2010 +0100
17.3 @@ -20,7 +20,9 @@
17.4 val nitpick_prefix : string
17.5 val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd
17.6 val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c
17.7 - val int_for_bool : bool -> int
17.8 + val pair_from_fun : (bool -> 'a) -> 'a * 'a
17.9 + val fun_from_pair : 'a * 'a -> bool -> 'a
17.10 + val int_from_bool : bool -> int
17.11 val nat_minus : int -> int -> int
17.12 val reasonable_power : int -> int -> int
17.13 val exact_log : int -> int -> int
17.14 @@ -84,8 +86,13 @@
17.15 (* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *)
17.16 fun pairf f g x = (f x, g x)
17.17
17.18 +(* (bool -> 'a) -> 'a * 'a *)
17.19 +fun pair_from_fun f = (f false, f true)
17.20 +(* 'a * 'a -> bool -> 'a *)
17.21 +fun fun_from_pair (f, t) b = if b then t else f
17.22 +
17.23 (* bool -> int *)
17.24 -fun int_for_bool b = if b then 1 else 0
17.25 +fun int_from_bool b = if b then 1 else 0
17.26 (* int -> int -> int *)
17.27 fun nat_minus i j = if i > j then i - j else 0
17.28