--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 16:49:46 2010 +0100
@@ -131,9 +131,7 @@
nonsel_names: nut list,
rel_table: nut NameTable.table,
unsound: bool,
- scope: scope,
- core: KK.formula,
- defs: KK.formula list}
+ scope: scope}
type rich_problem = KK.problem * problem_extension
@@ -195,7 +193,8 @@
val timer = Timer.startRealTimer ()
val thy = Proof.theory_of state
val ctxt = Proof.context_of state
-(* FIXME: reintroduce code before new release
+(* FIXME: reintroduce code before new release:
+
val nitpick_thy = ThyInfo.get_theory "Nitpick"
val _ = Theory.subthy (nitpick_thy, thy) orelse
error "You must import the theory \"Nitpick\" to use Nitpick"
@@ -289,8 +288,8 @@
val frees = Term.add_frees assms_t []
val _ = null (Term.add_tvars assms_t []) orelse
raise NOT_SUPPORTED "schematic type variables"
- val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t, binarize) = preprocess_term hol_ctxt assms_t
+ val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms,
+ binarize) = preprocess_term hol_ctxt assms_t
val got_all_user_axioms =
got_all_mono_user_axioms andalso no_poly_user_axioms
@@ -307,28 +306,25 @@
\unroll it.")))
val _ = if verbose then List.app print_wf (!wf_cache) else ()
val _ =
- pprint_d (fn () =>
- Pretty.chunks
- (pretties_for_formulas ctxt "Preprocessed formula" [core_t] @
- pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
- pretties_for_formulas ctxt "Relevant nondefinitional axiom"
- nondef_ts))
- val _ = List.app (ignore o Term.type_of) (core_t :: def_ts @ nondef_ts)
+ pprint_d (fn () => Pretty.chunks
+ (pretties_for_formulas ctxt "Preprocessed formula" [hd nondef_ts] @
+ pretties_for_formulas ctxt "Relevant definitional axiom" def_ts @
+ pretties_for_formulas ctxt "Relevant nondefinitional axiom"
+ (tl nondef_ts)))
+ val _ = List.app (ignore o Term.type_of) (nondef_ts @ def_ts)
handle TYPE (_, Ts, ts) =>
raise TYPE ("Nitpick.pick_them_nits_in_term", Ts, ts)
- val core_u = nut_from_term hol_ctxt Eq core_t
+ val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
val def_us = map (nut_from_term hol_ctxt DefEq) def_ts
- val nondef_us = map (nut_from_term hol_ctxt Eq) nondef_ts
val (free_names, const_names) =
- fold add_free_and_const_names (core_u :: def_us @ nondef_us) ([], [])
+ fold add_free_and_const_names (nondef_us @ def_us) ([], [])
val (sel_names, nonsel_names) =
List.partition (is_sel o nickname_of) const_names
val genuine_means_genuine = got_all_user_axioms andalso none_true wfs
val standard = forall snd stds
(*
- val _ = List.app (priority o string_for_nut ctxt)
- (core_u :: def_us @ nondef_us)
+ val _ = List.app (priority o string_for_nut ctxt) (nondef_us @ def_us)
*)
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
@@ -349,7 +345,7 @@
(not (is_pure_typedef thy T) orelse is_univ_typedef thy T)) orelse
is_number_type thy T orelse is_bit_type T
fun is_type_actually_monotonic T =
- formulas_monotonic hol_ctxt binarize T (def_ts, nondef_ts, core_t)
+ formulas_monotonic hol_ctxt binarize T (nondef_ts, def_ts)
fun is_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
@@ -362,14 +358,14 @@
fun is_datatype_deep T =
not standard orelse T = nat_T orelse is_word_type T orelse
exists (curry (op =) T o domain_type o type_of) sel_names
- val all_Ts = ground_types_in_terms hol_ctxt binarize
- (core_t :: def_ts @ nondef_ts)
+ val all_Ts = ground_types_in_terms hol_ctxt binarize (nondef_ts @ def_ts)
|> sort TermOrd.typ_ord
val _ = if verbose andalso binary_ints = SOME true andalso
exists (member (op =) [nat_T, int_T]) all_Ts then
print_v (K "The option \"binary_ints\" will be ignored because \
\of the presence of rationals, reals, \"Suc\", \
- \\"gcd\", or \"lcm\" in the problem.")
+ \\"gcd\", or \"lcm\" in the problem or because of the \
+ \\"non_std\" option.")
else
()
val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic all_Ts
@@ -480,7 +476,6 @@
(univ_card nat_card int_card main_j0 [] KK.True)
val _ = check_arity min_univ_card min_highest_arity
- val core_u = choose_reps_in_nut scope unsound rep_table false core_u
val def_us = map (choose_reps_in_nut scope unsound rep_table true)
def_us
val nondef_us = map (choose_reps_in_nut scope unsound rep_table false)
@@ -488,7 +483,7 @@
(*
val _ = List.app (priority o string_for_nut ctxt)
(free_names @ sel_names @ nonsel_names @
- core_u :: def_us @ nondef_us)
+ nondef_us @ def_us)
*)
val (free_rels, pool, rel_table) =
rename_free_vars free_names initial_pool NameTable.empty
@@ -496,13 +491,11 @@
rename_free_vars sel_names pool rel_table
val (other_rels, pool, rel_table) =
rename_free_vars nonsel_names pool rel_table
- val core_u = rename_vars_in_nut pool rel_table core_u
+ val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
val def_us = map (rename_vars_in_nut pool rel_table) def_us
- val nondef_us = map (rename_vars_in_nut pool rel_table) nondef_us
- val core_f = kodkod_formula_from_nut ofs kk core_u
+ val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
val def_fs = map (kodkod_formula_from_nut ofs kk) def_us
- val nondef_fs = map (kodkod_formula_from_nut ofs kk) nondef_us
- val formula = fold (fold s_and) [def_fs, nondef_fs] core_f
+ val formula = fold (fold s_and) [def_fs, nondef_fs] KK.True
val comment = (if unsound then "unsound" else "sound") ^ "\n" ^
PrintMode.setmp [] multiline_string_for_scope scope
val kodkod_sat_solver =
@@ -550,8 +543,7 @@
expr_assigns = [], formula = formula},
{free_names = free_names, sel_names = sel_names,
nonsel_names = nonsel_names, rel_table = rel_table,
- unsound = unsound, scope = scope, core = core_f,
- defs = nondef_fs @ def_fs @ declarative_axioms})
+ unsound = unsound, scope = scope})
end
handle TOO_LARGE (loc, msg) =>
if loc = "Nitpick_Kodkod.check_arity" andalso
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 16:49:46 2010 +0100
@@ -10,7 +10,7 @@
type hol_context = Nitpick_HOL.hol_context
val formulas_monotonic :
- hol_context -> bool -> typ -> term list * term list * term -> bool
+ hol_context -> bool -> typ -> term list * term list -> bool
end;
structure Nitpick_Mono : NITPICK_MONO =
@@ -34,7 +34,7 @@
MRec of string * typ list
datatype mterm =
- MAtom of term * mtyp |
+ MRaw of term * mtyp |
MAbs of string * typ * mtyp * sign_atom * mterm |
MApp of mterm * mterm
@@ -76,7 +76,7 @@
fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn
val bool_M = MType (@{type_name bool}, [])
-val irrelevant_M = MType (nitpick_prefix ^ "irrelevant", [])
+val dummy_M = MType (nitpick_prefix ^ "dummy", [])
(* mtyp -> bool *)
fun is_MRec (MRec _) = true
@@ -102,16 +102,19 @@
val need_parens = (prec < outer_prec)
in
(if need_parens then "(" else "") ^
- (case M of
- MAlpha => "\<alpha>"
- | MFun (M1, a, M2) =>
- aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
- string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
- | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
- | MType (s, []) =>
- if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s
- | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
- | MRec (s, _) => "[" ^ s ^ "]") ^
+ (if M = dummy_M then
+ "_"
+ else case M of
+ MAlpha => "\<alpha>"
+ | MFun (M1, a, M2) =>
+ aux (prec + 1) M1 ^ " \<Rightarrow>\<^bsup>" ^
+ string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2
+ | MPair (M1, M2) => aux (prec + 1) M1 ^ " \<times> " ^ aux prec M2
+ | MType (s, []) =>
+ if s = @{type_name prop} orelse s = @{type_name bool} then "o"
+ else s
+ | MType (s, Ms) => "(" ^ commas (map (aux 0) Ms) ^ ") " ^ s
+ | MRec (s, _) => "[" ^ s ^ "]") ^
(if need_parens then ")" else "")
end
in aux 0 end
@@ -122,7 +125,7 @@
| flatten_mtype M = [M]
(* mterm -> bool *)
-fun precedence_of_mterm (MAtom _) = no_prec
+fun precedence_of_mterm (MRaw _) = no_prec
| precedence_of_mterm (MAbs _) = 1
| precedence_of_mterm (MApp _) = 2
@@ -139,7 +142,7 @@
in
(if need_parens then "(" else "") ^
(case m of
- MAtom (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
+ MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M
| MAbs (s, _, M, a, m) =>
"\<lambda>" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^
string_for_sign_atom a ^ "\<^esup> " ^ aux prec m
@@ -149,7 +152,7 @@
in aux 0 end
(* mterm -> mtyp *)
-fun mtype_of_mterm (MAtom (_, M)) = M
+fun mtype_of_mterm (MRaw (_, M)) = M
| mtype_of_mterm (MAbs (_, _, M, a, m)) = MFun (M, a, mtype_of_mterm m)
| mtype_of_mterm (MApp (m1, _)) =
case mtype_of_mterm m1 of
@@ -545,19 +548,28 @@
fun solve _ UnsolvableCSet = (print_g "*** Problem: Unsolvable"; NONE)
| solve max_var (CSet (lits, comps, sexps)) =
let
+ (* (int -> bool option) -> literal list option *)
+ fun do_assigns assigns =
+ SOME (literals_from_assignments max_var assigns lits
+ |> tap print_solution)
val _ = print_problem lits comps sexps
val prop = PropLogic.all (map prop_for_literal lits @
map prop_for_comp comps @
map prop_for_sign_expr sexps)
- (* use the first ML solver (to avoid startup overhead) *)
- val solvers = !SatSolver.solvers
- |> filter (member (op =) ["dptsat", "dpll"] o fst)
+ val default_val = bool_from_sign Minus
in
- case snd (hd solvers) prop of
- SatSolver.SATISFIABLE assigns =>
- SOME (literals_from_assignments max_var assigns lits
- |> tap print_solution)
- | _ => NONE
+ if PropLogic.eval (K default_val) prop then
+ do_assigns (K (SOME default_val))
+ else
+ let
+ (* use the first ML solver (to avoid startup overhead) *)
+ val solvers = !SatSolver.solvers
+ |> filter (member (op =) ["dptsat", "dpll"] o fst)
+ in
+ case snd (hd solvers) prop of
+ SatSolver.SATISFIABLE assigns => do_assigns assigns
+ | _ => NONE
+ end
end
type mtype_schema = mtyp * constraint_set
@@ -580,7 +592,7 @@
handle List.Empty => initial_gamma
(* mdata -> term -> accumulator -> mterm * accumulator *)
-fun consider_term (mdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs,
+fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs,
def_table, ...},
alpha_T, max_fresh, ...}) =
let
@@ -595,7 +607,7 @@
fun do_all T (gamma, cset) =
let
val abs_M = mtype_for (domain_type (domain_type T))
- val body_M = mtype_for (range_type T)
+ val body_M = mtype_for (body_type T)
in
(MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M),
(gamma, cset |> add_mtype_is_right_total abs_M))
@@ -641,9 +653,9 @@
pair (MFun (M, S Minus, if n = 0 then a_M else b_M))
| M => raise MTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [M])
(* mtyp * accumulator *)
- val mtype_unsolvable = (irrelevant_M, unsolvable_accum)
+ val mtype_unsolvable = (dummy_M, unsolvable_accum)
(* term -> mterm * accumulator *)
- fun mterm_unsolvable t = (MAtom (t, irrelevant_M), unsolvable_accum)
+ fun mterm_unsolvable t = (MRaw (t, dummy_M), unsolvable_accum)
(* term -> string -> typ -> term -> term -> term -> accumulator
-> mterm * accumulator *)
fun do_bounded_quantifier t0 abs_s abs_T connective_t bound_t body_t accum =
@@ -657,10 +669,11 @@
val bound_M = mtype_of_mterm bound_m
val (M1, a, M2) = dest_MFun bound_M
in
- (MApp (MAtom (t0, MFun (bound_M, S Minus, bool_M)),
+ (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)),
MAbs (abs_s, abs_T, M1, a,
- MApp (MApp (MAtom (connective_t, irrelevant_M),
- MApp (bound_m, MAtom (Bound 0, M1))),
+ MApp (MApp (MRaw (connective_t,
+ mtype_for (fastype_of connective_t)),
+ MApp (bound_m, MRaw (Bound 0, M1))),
body_m))), accum)
end
(* term -> accumulator -> mterm * accumulator *)
@@ -678,10 +691,14 @@
| @{const_name "=="} => do_equals T accum
| @{const_name All} => do_all T accum
| @{const_name Ex} =>
- do_term (@{const Not}
- $ (HOLogic.eq_const (domain_type T)
- $ Abs (Name.uu, T, @{const False}))) accum
- |>> mtype_of_mterm
+ let val set_T = domain_type T in
+ do_term (Abs (Name.uu, set_T,
+ @{const Not} $ (HOLogic.mk_eq
+ (Abs (Name.uu, domain_type set_T,
+ @{const False}),
+ Bound 0)))) accum
+ |>> mtype_of_mterm
+ end
| @{const_name "op ="} => do_equals T accum
| @{const_name The} => (print_g "*** The"; mtype_unsolvable)
| @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable)
@@ -719,9 +736,12 @@
| @{const_name rtrancl} =>
(print_g "*** rtrancl"; mtype_unsolvable)
| @{const_name finite} =>
- let val M1 = mtype_for (domain_type (domain_type T)) in
- (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
- end
+ if is_finite_type hol_ctxt T then
+ let val M1 = mtype_for (domain_type (domain_type T)) in
+ (MFun (pos_set_mtype_for_dom M1, S Minus, bool_M), accum)
+ end
+ else
+ (print_g "*** finite"; mtype_unsolvable)
| @{const_name rel_comp} =>
let
val x = Unsynchronized.inc max_fresh
@@ -807,7 +827,7 @@
let val M = mtype_for T in
(M, ({bounds = bounds, frees = frees,
consts = (x, M) :: consts}, cset))
- end) |>> curry MAtom t
+ end) |>> curry MRaw t
| Free (x as (_, T)) =>
(case AList.lookup (op =) frees x of
SOME M => (M, accum)
@@ -815,12 +835,12 @@
let val M = mtype_for T in
(M, ({bounds = bounds, frees = (x, M) :: frees,
consts = consts}, cset))
- end) |>> curry MAtom t
+ end) |>> curry MRaw t
| Var _ => (print_g "*** Var"; mterm_unsolvable t)
- | Bound j => (MAtom (t, nth bounds j), accum)
+ | Bound j => (MRaw (t, nth bounds j), accum)
| Abs (s, T, t' as @{const False}) =>
let val (M1, a, M2) = mfun_for T bool_T in
- (MAbs (s, T, M1, a, MAtom (t', M2)), accum)
+ (MAbs (s, T, M1, a, MRaw (t', M2)), accum)
end
| Abs (s, T, t') =>
((case t' of
@@ -850,88 +870,109 @@
in
case accum of
(_, UnsolvableCSet) => mterm_unsolvable t
- | _ => (MApp (m1, m2), accum)
+ | _ =>
+ let
+ val M11 = mtype_of_mterm m1 |> dest_MFun |> #1
+ val M2 = mtype_of_mterm m2
+ in (MApp (m1, m2), accum ||> add_is_sub_mtype M2 M11) end
end)
|> tap (fn (m, _) => print_g (" \<Gamma> \<turnstile> " ^
string_for_mterm ctxt m))
in do_term end
-(* mdata -> sign -> term -> accumulator -> accumulator *)
+(* mdata -> styp -> term -> term -> mterm * accumulator *)
+fun consider_general_equals mdata (x as (_, T)) t1 t2 accum =
+ let
+ val (m1, accum) = consider_term mdata t1 accum
+ val (m2, accum) = consider_term mdata t2 accum
+ val M1 = mtype_of_mterm m1
+ val M2 = mtype_of_mterm m2
+ val body_M = fresh_mtype_for_type mdata (nth_range_type 2 T)
+ in
+ (MApp (MApp (MRaw (Const x,
+ MFun (M1, S Minus, MFun (M2, S Minus, body_M))), m1), m2),
+ accum ||> add_mtypes_equal M1 M2)
+ end
+
+(* mdata -> sign -> term -> accumulator -> mterm * accumulator *)
fun consider_general_formula (mdata as {hol_ctxt = {ctxt, ...}, ...}) =
let
(* typ -> mtyp *)
val mtype_for = fresh_mtype_for_type mdata
- (* term -> accumulator -> mtyp * accumulator *)
- val do_term = apfst mtype_of_mterm oo consider_term mdata
- (* sign -> term -> accumulator -> accumulator *)
- fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum
- | do_formula sn t (accum as (gamma, cset)) =
+ (* term -> accumulator -> mterm * accumulator *)
+ val do_term = consider_term mdata
+ (* sign -> term -> accumulator -> mterm * accumulator *)
+ fun do_formula _ t (_, UnsolvableCSet) =
+ (MRaw (t, dummy_M), unsolvable_accum)
+ | do_formula sn t accum =
let
- (* term -> accumulator -> accumulator *)
- val do_co_formula = do_formula sn
- val do_contra_formula = do_formula (negate sn)
- (* string -> typ -> term -> accumulator *)
- fun do_quantifier quant_s abs_T body_t =
+ (* styp -> string -> typ -> term -> mterm * accumulator *)
+ fun do_quantifier (quant_x as (quant_s, _)) abs_s abs_T body_t =
let
val abs_M = mtype_for abs_T
val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex}))
- val cset = cset |> side_cond ? add_mtype_is_right_total abs_M
+ val (body_m, accum) =
+ accum ||> side_cond ? add_mtype_is_right_total abs_M
+ |>> push_bound abs_M |> do_formula sn body_t
+ val body_M = mtype_of_mterm body_m
in
- (gamma |> push_bound abs_M, cset)
- |> do_co_formula body_t |>> pop_bound
+ (MApp (MRaw (Const quant_x, MFun (abs_M, S Minus, body_M)),
+ MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+ accum |>> pop_bound)
end
- (* typ -> term -> accumulator *)
- fun do_bounded_quantifier abs_T body_t =
- accum |>> push_bound (mtype_for abs_T) |> do_co_formula body_t
- |>> pop_bound
- (* term -> term -> accumulator *)
- fun do_equals t1 t2 =
+ (* styp -> term -> term -> mterm * accumulator *)
+ fun do_equals x t1 t2 =
case sn of
- Plus => do_term t accum |> snd
- | Minus => let
- val (M1, accum) = do_term t1 accum
- val (M2, accum) = do_term t2 accum
- in accum ||> add_mtypes_equal M1 M2 end
+ Plus => do_term t accum
+ | Minus => consider_general_equals mdata x t1 t2 accum
in
case t of
- Const (s0 as @{const_name all}, _) $ Abs (_, T1, t1) =>
- do_quantifier s0 T1 t1
- | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2
- | @{const "==>"} $ t1 $ t2 =>
- accum |> do_contra_formula t1 |> do_co_formula t2
- | @{const Trueprop} $ t1 => do_co_formula t1 accum
- | @{const Not} $ t1 => do_contra_formula t1 accum
- | Const (@{const_name All}, _)
- $ Abs (_, T1, t1 as @{const "op -->"} $ (_ $ Bound 0) $ _) =>
- do_bounded_quantifier T1 t1
- | Const (s0 as @{const_name All}, _) $ Abs (_, T1, t1) =>
- do_quantifier s0 T1 t1
- | Const (@{const_name Ex}, _)
- $ Abs (_, T1, t1 as @{const "op &"} $ (_ $ Bound 0) $ _) =>
- do_bounded_quantifier T1 t1
- | Const (s0 as @{const_name Ex}, T0) $ (t1 as Abs (_, T1, t1')) =>
+ Const (x as (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 => do_equals x t1 t2
+ | @{const Trueprop} $ t1 =>
+ let val (m1, accum) = do_formula sn t1 accum in
+ (MApp (MRaw (@{const Trueprop}, mtype_for (bool_T --> prop_T)),
+ m1), accum)
+ end
+ | @{const Not} $ t1 =>
+ let val (m1, accum) = do_formula (negate sn) t1 accum in
+ (MApp (MRaw (@{const Not}, mtype_for (bool_T --> bool_T)), m1),
+ accum)
+ end
+ | Const (x as (@{const_name All}, _)) $ Abs (s1, T1, t1) =>
+ do_quantifier x s1 T1 t1
+ | Const (x0 as (s0 as @{const_name Ex}, T0))
+ $ (t1 as Abs (s1, T1, t1')) =>
(case sn of
- Plus => do_quantifier s0 T1 t1'
+ Plus => do_quantifier x0 s1 T1 t1'
| Minus =>
+ (* ### do elsewhere *)
do_term (@{const Not}
$ (HOLogic.eq_const (domain_type T0) $ t1
- $ Abs (Name.uu, T1, @{const False}))) accum |> snd)
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2
- | @{const "op &"} $ t1 $ t2 =>
- accum |> do_co_formula t1 |> do_co_formula t2
- | @{const "op |"} $ t1 $ t2 =>
- accum |> do_co_formula t1 |> do_co_formula t2
- | @{const "op -->"} $ t1 $ t2 =>
- accum |> do_contra_formula t1 |> do_co_formula t2
- | Const (@{const_name If}, _) $ t1 $ t2 $ t3 =>
- accum |> do_term t1 |> snd |> fold do_co_formula [t2, t3]
- | Const (@{const_name Let}, _) $ t1 $ t2 =>
- do_co_formula (betapply (t2, t1)) accum
- | _ => do_term t accum |> snd
+ $ Abs (Name.uu, T1, @{const False}))) accum)
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ do_equals x t1 t2
+ | (t0 as Const (s0, _)) $ t1 $ t2 =>
+ if s0 = @{const_name "==>"} orelse s0 = @{const_name "op &"} orelse
+ s0 = @{const_name "op |"} orelse s0 = @{const_name "op -->"} then
+ let
+ val impl = (s0 = @{const_name "==>"} orelse
+ s0 = @{const_name "op -->"})
+ val (m1, accum) = do_formula (sn |> impl ? negate) t1 accum
+ val (m2, accum) = do_formula sn t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2),
+ accum)
+ end
+ else
+ do_term t accum
+ | _ => do_term t accum
end
- |> tap (fn _ => print_g ("\<Gamma> \<turnstile> " ^
- Syntax.string_of_term ctxt t ^
- " : o\<^sup>" ^ string_for_sign sn))
+ |> tap (fn (m, _) =>
+ print_g ("\<Gamma> \<turnstile> " ^
+ string_for_mterm ctxt m ^ " : o\<^sup>" ^
+ string_for_sign sn))
in do_formula end
(* The harmless axiom optimization below is somewhat too aggressive in the face
@@ -947,46 +988,69 @@
|> (forall (member (op =) harmless_consts o original_name o fst)
orf exists (member (op =) bounteous_consts o fst))
-(* mdata -> sign -> term -> accumulator -> accumulator *)
-fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) sn t =
- not (is_harmless_axiom hol_ctxt t) ? consider_general_formula mdata sn t
+(* mdata -> term -> accumulator -> mterm * accumulator *)
+fun consider_nondefinitional_axiom (mdata as {hol_ctxt, ...}) t =
+ if is_harmless_axiom hol_ctxt t then pair (MRaw (t, dummy_M))
+ else consider_general_formula mdata Plus t
-(* mdata -> term -> accumulator -> accumulator *)
+(* mdata -> term -> accumulator -> mterm * accumulator *)
fun consider_definitional_axiom (mdata as {hol_ctxt as {thy, ...}, ...}) t =
if not (is_constr_pattern_formula thy t) then
- consider_nondefinitional_axiom mdata Plus t
+ consider_nondefinitional_axiom mdata t
else if is_harmless_axiom hol_ctxt t then
- I
+ pair (MRaw (t, dummy_M))
else
let
- (* term -> accumulator -> mtyp * accumulator *)
- val do_term = apfst mtype_of_mterm oo consider_term mdata
- (* typ -> term -> accumulator -> accumulator *)
- fun do_all abs_T body_t accum =
- let val abs_M = fresh_mtype_for_type mdata abs_T in
- accum |>> push_bound abs_M |> do_formula body_t |>> pop_bound
+ (* typ -> mtyp *)
+ val mtype_for = fresh_mtype_for_type mdata
+ (* term -> accumulator -> mterm * accumulator *)
+ val do_term = consider_term mdata
+ (* term -> string -> typ -> term -> accumulator -> mterm * accumulator *)
+ fun do_all quant_t abs_s abs_T body_t accum =
+ let
+ val abs_M = mtype_for abs_T
+ val (body_m, accum) =
+ accum |>> push_bound abs_M |> do_formula body_t
+ val body_M = mtype_of_mterm body_m
+ in
+ (MApp (MRaw (quant_t, MFun (abs_M, S Minus, body_M)),
+ MAbs (abs_s, abs_T, abs_M, S Minus, body_m)),
+ accum |>> pop_bound)
end
- (* term -> term -> accumulator -> accumulator *)
- and do_implies t1 t2 = do_term t1 #> snd #> do_formula t2
- and do_equals t1 t2 accum =
+ (* term -> term -> term -> accumulator -> mterm * accumulator *)
+ and do_conjunction t0 t1 t2 accum =
let
- val (M1, accum) = do_term t1 accum
- val (M2, accum) = do_term t2 accum
- in accum ||> add_mtypes_equal M1 M2 end
+ val (m1, accum) = do_formula t1 accum
+ val (m2, accum) = do_formula t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+ end
+ and do_implies t0 t1 t2 accum =
+ let
+ val (m1, accum) = do_term t1 accum
+ val (m2, accum) = do_formula t2 accum
+ in
+ (MApp (MApp (MRaw (t0, mtype_for (fastype_of t0)), m1), m2), accum)
+ end
(* term -> accumulator -> accumulator *)
- and do_formula _ (_, UnsolvableCSet) = unsolvable_accum
+ and do_formula t (_, UnsolvableCSet) =
+ (MRaw (t, dummy_M), unsolvable_accum)
| do_formula t accum =
case t of
- Const (@{const_name all}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
+ (t0 as Const (@{const_name all}, _)) $ Abs (s1, T1, t1) =>
+ do_all t0 s1 T1 t1 accum
| @{const Trueprop} $ t1 => do_formula t1 accum
- | Const (@{const_name "=="}, _) $ t1 $ t2 => do_equals t1 t2 accum
- | @{const "==>"} $ t1 $ t2 => do_implies t1 t2 accum
- | @{const Pure.conjunction} $ t1 $ t2 =>
- accum |> do_formula t1 |> do_formula t2
- | Const (@{const_name All}, _) $ Abs (_, T1, t1) => do_all T1 t1 accum
- | Const (@{const_name "op ="}, _) $ t1 $ t2 => do_equals t1 t2 accum
- | @{const "op &"} $ t1 $ t2 => accum |> do_formula t1 |> do_formula t2
- | @{const "op -->"} $ t1 $ t2 => do_implies t1 t2 accum
+ | Const (x as (@{const_name "=="}, _)) $ t1 $ t2 =>
+ consider_general_equals mdata x t1 t2 accum
+ | (t0 as @{const "==>"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
+ | (t0 as @{const Pure.conjunction}) $ t1 $ t2 =>
+ do_conjunction t0 t1 t2 accum
+ | (t0 as Const (@{const_name All}, _)) $ Abs (s0, T1, t1) =>
+ do_all t0 s0 T1 t1 accum
+ | Const (x as (@{const_name "op ="}, _)) $ t1 $ t2 =>
+ consider_general_equals mdata x t1 t2 accum
+ | (t0 as @{const "op &"}) $ t1 $ t2 => do_conjunction t0 t1 t2 accum
+ | (t0 as @{const "op -->"}) $ t1 $ t2 => do_implies t0 t1 t2 accum
| _ => raise TERM ("Nitpick_Mono.consider_definitional_axiom.\
\do_formula", [t])
in do_formula t end
@@ -1002,20 +1066,27 @@
map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts
|> cat_lines |> print_g
-(* hol_context -> bool -> typ -> term list * term list * term -> bool *)
+(* ('a -> 'b -> 'c * 'd) -> 'a -> 'c list * 'b -> 'c list * 'd *)
+fun gather f t (ms, accum) =
+ let val (m, accum) = f t accum in (m :: ms, accum) end
+
+(* hol_context -> bool -> typ -> term list * term list -> bool *)
fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T
- (def_ts, nondef_ts, core_t) =
+ (nondef_ts, def_ts) =
let
val _ = print_g ("****** Monotonicity analysis: " ^
string_for_mtype MAlpha ^ " is " ^
Syntax.string_of_typ ctxt alpha_T)
val mdata as {max_fresh, constr_cache, ...} =
initial_mdata hol_ctxt binarize alpha_T
- val (gamma as {frees, consts, ...}, cset) =
- (initial_gamma, slack)
- |> fold (consider_definitional_axiom mdata) def_ts
- |> fold (consider_nondefinitional_axiom mdata Plus) nondef_ts
- |> consider_general_formula mdata Plus core_t
+
+ val accum = (initial_gamma, slack)
+ val (nondef_ms, accum) =
+ ([], accum) |> gather (consider_general_formula mdata Plus) (hd nondef_ts)
+ |> fold (gather (consider_nondefinitional_axiom mdata))
+ (tl nondef_ts)
+ val (def_ms, (gamma, cset)) =
+ ([], accum) |> fold (gather (consider_definitional_axiom mdata)) def_ts
in
case solve (!max_fresh) cset of
SOME lits => (print_mtype_context ctxt lits gamma; true)
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Thu Feb 25 16:33:39 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 16:49:46 2010 +0100
@@ -9,8 +9,7 @@
sig
type hol_context = Nitpick_HOL.hol_context
val preprocess_term :
- hol_context -> term
- -> ((term list * term list) * (bool * bool)) * term * bool
+ hol_context -> term -> term list * term list * bool * bool * bool
end
structure Nitpick_Preproc : NITPICK_PREPROC =
@@ -473,6 +472,19 @@
(list_comb (t, args), seen)
in aux [] 0 t [] [] |> fst end
+val let_var_prefix = nitpick_prefix ^ "l"
+val let_inline_threshold = 32
+
+(* int -> typ -> term -> (term -> term) -> term *)
+fun hol_let n abs_T body_T f t =
+ if n * size_of_term t <= let_inline_threshold then
+ f t
+ else
+ let val z = ((let_var_prefix, 0), abs_T) in
+ Const (@{const_name Let}, abs_T --> (abs_T --> body_T) --> body_T)
+ $ t $ abs_var z (incr_boundvars 1 (f (Var z)))
+ end
+
(* hol_context -> bool -> term -> term *)
fun destroy_pulled_out_constrs (hol_ctxt as {thy, stds, ...}) axiom t =
let
@@ -507,14 +519,19 @@
if z1 = z2 andalso num_occs_of_var z1 = 2 then @{const True}
else raise SAME ()
| (Const (x as (s, T)), args) =>
- let val arg_Ts = binder_types T in
- if length arg_Ts = length args andalso
- (is_constr thy stds x orelse s = @{const_name Pair}) andalso
+ let
+ val (arg_Ts, dataT) = strip_type T
+ val n = length arg_Ts
+ in
+ if length args = n andalso
+ (is_constr thy stds x orelse s = @{const_name Pair} orelse
+ x = (@{const_name Suc}, nat_T --> nat_T)) andalso
(not careful orelse not (is_Var t1) orelse
String.isPrefix val_var_prefix (fst (fst (dest_Var t1)))) then
- discriminate_value hol_ctxt x t1 ::
- map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
- |> foldr1 s_conj
+ hol_let (n + 1) dataT bool_T
+ (fn t1 => discriminate_value hol_ctxt x t1 ::
+ map3 (sel_eq x t1) (index_seq 0 n) arg_Ts args
+ |> foldr1 s_conj) t1
else
raise SAME ()
end
@@ -1019,7 +1036,7 @@
(* Prevents divergence in case of cyclic or infinite axiom dependencies. *)
val axioms_max_depth = 255
-(* hol_context -> term -> (term list * term list) * (bool * bool) *)
+(* hol_context -> term -> term list * term list * bool * bool *)
fun axioms_for_term
(hol_ctxt as {thy, ctxt, max_bisim_depth, stds, user_axioms,
fast_descrs, evals, def_table, nondef_table, user_nondefs,
@@ -1169,10 +1186,9 @@
|> user_axioms = SOME true
? fold (add_nondef_axiom 1) mono_user_nondefs
val defs = defs @ special_congruence_axioms hol_ctxt xs
- in
- ((defs, nondefs), (user_axioms = SOME true orelse null mono_user_nondefs,
- null poly_user_nondefs))
- end
+ val got_all_mono_user_axioms =
+ (user_axioms = SOME true orelse null mono_user_nondefs)
+ in (t :: nondefs, defs, got_all_mono_user_axioms, null poly_user_nondefs) end
(** Simplification of constructor/selector terms **)
@@ -1274,7 +1290,7 @@
(* Maximum number of quantifiers in a cluster for which the exponential
algorithm is used. Larger clusters use a heuristic inspired by Claessen &
- Sörensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
+ Soerensson's polynomial binary splitting procedure (p. 5 of their MODEL 2003
paper). *)
val quantifier_cluster_threshold = 7
@@ -1385,29 +1401,29 @@
(** Preprocessor entry point **)
-(* hol_context -> term
- -> ((term list * term list) * (bool * bool)) * term * bool *)
+(* hol_context -> term -> term list * term list * bool * bool * bool *)
fun preprocess_term (hol_ctxt as {thy, stds, binary_ints, destroy_constrs,
boxes, skolemize, uncurry, ...}) t =
let
val skolem_depth = if skolemize then 4 else ~1
- val (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t) = t |> unfold_defs_in_term hol_ctxt
- |> close_form
- |> skolemize_term_and_more hol_ctxt skolem_depth
- |> specialize_consts_in_term hol_ctxt 0
- |> `(axioms_for_term hol_ctxt)
+ val (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms) =
+ t |> unfold_defs_in_term hol_ctxt
+ |> close_form
+ |> skolemize_term_and_more hol_ctxt skolem_depth
+ |> specialize_consts_in_term hol_ctxt 0
+ |> axioms_for_term hol_ctxt
val binarize =
is_standard_datatype thy stds nat_T andalso
case binary_ints of
SOME false => false
- | _ => forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
+ | _ => forall may_use_binary_ints (nondef_ts @ def_ts) andalso
(binary_ints = SOME true orelse
- exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ exists should_use_binary_ints (nondef_ts @ def_ts))
val box = exists (not_equal (SOME false) o snd) boxes
+ val uncurry = uncurry andalso box
val table =
- Termtab.empty |> uncurry
- ? fold (add_to_uncurry_table thy) (core_t :: def_ts @ nondef_ts)
+ Termtab.empty
+ |> uncurry ? fold (add_to_uncurry_table thy) (nondef_ts @ def_ts)
(* bool -> term -> term *)
fun do_rest def =
binarize ? binarize_nat_and_int_in_term
@@ -1424,12 +1440,10 @@
#> push_quantifiers_inward
#> close_form
#> Term.map_abs_vars shortest_name
+ val nondef_ts = map (do_rest false) nondef_ts
val def_ts = map (do_rest true) def_ts
- val nondef_ts = map (do_rest false) nondef_ts
- val core_t = do_rest false core_t
in
- (((def_ts, nondef_ts), (got_all_mono_user_axioms, no_poly_user_axioms)),
- core_t, binarize)
+ (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize)
end
end;