--- a/src/HOL/Tools/Nitpick/kodkod.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod.ML Wed Jan 20 10:38:19 2010 +0100
@@ -496,14 +496,14 @@
(* problem -> problem -> bool *)
fun problems_equivalent (p1 : problem) (p2 : problem) =
- #univ_card p1 = #univ_card p2
- andalso #formula p1 = #formula p2
- andalso #bounds p1 = #bounds p2
- andalso #expr_assigns p1 = #expr_assigns p2
- andalso #tuple_assigns p1 = #tuple_assigns p2
- andalso #int_bounds p1 = #int_bounds p2
- andalso filter (is_relevant_setting o fst) (#settings p1)
- = filter (is_relevant_setting o fst) (#settings p2)
+ #univ_card p1 = #univ_card p2 andalso
+ #formula p1 = #formula p2 andalso
+ #bounds p1 = #bounds p2 andalso
+ #expr_assigns p1 = #expr_assigns p2 andalso
+ #tuple_assigns p1 = #tuple_assigns p2 andalso
+ #int_bounds p1 = #int_bounds p2 andalso
+ filter (is_relevant_setting o fst) (#settings p1)
+ = filter (is_relevant_setting o fst) (#settings p2)
(* int -> string *)
fun base_name j =
@@ -883,8 +883,8 @@
(* string -> bool *)
fun is_ident_char s =
- Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s
- orelse s = "_" orelse s = "'" orelse s = "$"
+ Symbol.is_ascii_letter s orelse Symbol.is_ascii_digit s orelse
+ s = "_" orelse s = "'" orelse s = "$"
(* string list -> string list *)
fun strip_blanks [] = []
@@ -950,9 +950,9 @@
-> substring * (int * raw_bound list) list * int list *)
fun read_next_outcomes j (s, ps, js) =
let val (s1, s2) = Substring.position outcome_marker s in
- if Substring.isEmpty s2
- orelse not (Substring.isEmpty (Substring.position problem_marker s1
- |> snd)) then
+ if Substring.isEmpty s2 orelse
+ not (Substring.isEmpty (Substring.position problem_marker s1
+ |> snd)) then
(s, ps, js)
else
let
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Wed Jan 20 10:38:19 2010 +0100
@@ -188,17 +188,11 @@
orig_t =
let
val timer = Timer.startRealTimer ()
- val user_thy = Proof.theory_of state
+ val thy = Proof.theory_of state
+ val ctxt = Proof.context_of state
val nitpick_thy = ThyInfo.get_theory "Nitpick"
- val nitpick_thy_missing = not (Theory.subthy (nitpick_thy, user_thy))
- val thy = if nitpick_thy_missing then
- Theory.begin_theory "Nitpick_Internal_Name_Do_Not_Use_XYZZY"
- [nitpick_thy, user_thy]
- |> Theory.checkpoint
- else
- user_thy
- val ctxt = Proof.context_of state
- |> nitpick_thy_missing ? Context.raw_transfer thy
+ val _ = Theory.subthy (nitpick_thy, thy) orelse
+ error "You must import the theory \"Nitpick\" to use Nitpick"
val {cards_assigns, maxes_assigns, iters_assigns, bitss, bisim_depths,
boxes, monos, wfs, sat_solver, blocking, falsify, debug, verbose,
overlord, user_axioms, assms, merge_type_vars, binary_ints,
@@ -280,8 +274,8 @@
unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [],
constr_cache = Unsynchronized.ref []}
val frees = Term.add_frees assms_t []
- val _ = null (Term.add_tvars assms_t [])
- orelse raise NOT_SUPPORTED "schematic type variables"
+ 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) = preprocess_term ext_ctxt assms_t
val got_all_user_axioms =
@@ -325,77 +319,65 @@
val unique_scope = forall (curry (op =) 1 o length o snd) cards_assigns
(* typ -> bool *)
- fun is_free_type_monotonic T =
- unique_scope orelse
- case triple_lookup (type_match thy) monos T of
- SOME (SOME b) => b
- | _ => is_bit_type T
- orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
- fun is_datatype_monotonic T =
+ fun is_type_always_monotonic T =
+ ((not (is_pure_typedef thy T) orelse is_univ_typedef thy T) andalso
+ not (is_quot_type thy T)) orelse
+ is_number_type thy T orelse is_bit_type T
+ fun is_type_monotonic T =
unique_scope orelse
case triple_lookup (type_match thy) monos T of
SOME (SOME b) => b
- | _ => not (is_pure_typedef thy T) orelse is_univ_typedef thy T
- orelse is_number_type thy T
- orelse formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
- fun is_datatype_deep T =
- is_word_type T
- orelse exists (curry (op =) T o domain_type o type_of) sel_names
+ | _ => is_type_always_monotonic T orelse
+ formulas_monotonic ext_ctxt T def_ts nondef_ts core_t
+ fun is_deep_datatype T =
+ is_datatype thy T andalso
+ (is_word_type T orelse
+ exists (curry (op =) T o domain_type o type_of) sel_names)
val Ts = ground_types_in_terms ext_ctxt (core_t :: def_ts @ nondef_ts)
|> sort TermOrd.typ_ord
- val _ = if verbose andalso binary_ints = SOME true
- andalso exists (member (op =) [nat_T, int_T]) Ts then
+ val _ = if verbose andalso binary_ints = SOME true andalso
+ exists (member (op =) [nat_T, int_T]) 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.")
else
()
- val (all_dataTs, all_free_Ts) =
- List.partition (is_integer_type orf is_datatype thy) Ts
- val (mono_dataTs, nonmono_dataTs) =
- List.partition is_datatype_monotonic all_dataTs
- val (mono_free_Ts, nonmono_free_Ts) =
- List.partition is_free_type_monotonic all_free_Ts
-
- val interesting_mono_free_Ts = filter_out is_bit_type mono_free_Ts
+ val (mono_Ts, nonmono_Ts) = List.partition is_type_monotonic Ts
val _ =
- if not unique_scope andalso not (null interesting_mono_free_Ts) then
- print_v (fn () =>
- let
- val ss = map (quote o string_for_type ctxt)
- interesting_mono_free_Ts
- in
- "The type" ^ plural_s_for_list ss ^ " " ^
- space_implode " " (serial_commas "and" ss) ^ " " ^
- (if none_true monos then
- "passed the monotonicity test"
- else
- (if length ss = 1 then "is" else "are") ^
- " considered monotonic") ^
- ". Nitpick might be able to skip some scopes."
- end)
+ if verbose andalso not unique_scope then
+ case filter_out is_type_always_monotonic mono_Ts of
+ [] => ()
+ | interesting_mono_Ts =>
+ print_v (fn () =>
+ let
+ val ss = map (quote o string_for_type ctxt)
+ interesting_mono_Ts
+ in
+ "The type" ^ plural_s_for_list ss ^ " " ^
+ space_implode " " (serial_commas "and" ss) ^ " " ^
+ (if none_true monos then
+ "passed the monotonicity test"
+ else
+ (if length ss = 1 then "is" else "are") ^
+ " considered monotonic") ^
+ ". Nitpick might be able to skip some scopes."
+ end)
else
()
- val mono_Ts = mono_dataTs @ mono_free_Ts
- val nonmono_Ts = nonmono_dataTs @ nonmono_free_Ts
- val shallow_dataTs = filter_out is_datatype_deep mono_dataTs
+ val shallow_dataTs = filter_out is_deep_datatype Ts
(*
- val _ = priority "Monotonic datatypes:"
- val _ = List.app (priority o string_for_type ctxt) mono_dataTs
- val _ = priority "Nonmonotonic datatypes:"
- val _ = List.app (priority o string_for_type ctxt) nonmono_dataTs
- val _ = priority "Monotonic free types:"
- val _ = List.app (priority o string_for_type ctxt) mono_free_Ts
- val _ = priority "Nonmonotonic free types:"
- val _ = List.app (priority o string_for_type ctxt) nonmono_free_Ts
+ val _ = priority "Monotonic types:"
+ val _ = List.app (priority o string_for_type ctxt) mono_Ts
+ val _ = priority "Nonmonotonic types:"
+ val _ = List.app (priority o string_for_type ctxt) nonmono_Ts
*)
val need_incremental = Int.max (max_potential, max_genuine) >= 2
val effective_sat_solver =
if sat_solver <> "smart" then
- if need_incremental
- andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
- sat_solver) then
+ if need_incremental andalso
+ not (member (op =) (Kodkod_SAT.configured_sat_solvers true)
+ sat_solver) then
(print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \
\be used instead of " ^ quote sat_solver ^ "."));
"SAT4J")
@@ -421,9 +403,9 @@
(scope as {card_assigns, bits, bisim_depth, datatypes, ofs, ...}) =
let
val _ = not (exists (fn other => scope_less_eq other scope)
- (!too_big_scopes))
- orelse raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
- \problem_for_scope", "too large scope")
+ (!too_big_scopes)) orelse
+ raise TOO_LARGE ("Nitpick.pick_them_nits_in_term.\
+ \problem_for_scope", "too large scope")
(*
val _ = priority "Offsets:"
val _ = List.app (fn (T, j0) =>
@@ -437,9 +419,9 @@
val main_j0 = offset_of_type ofs bool_T
val (nat_card, nat_j0) = spec_of_type scope nat_T
val (int_card, int_j0) = spec_of_type scope int_T
- val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0)
- orelse raise BAD ("Nitpick.pick_them_nits_in_term.\
- \problem_for_scope", "bad offsets")
+ val _ = (nat_j0 = main_j0 andalso int_j0 = main_j0) orelse
+ raise BAD ("Nitpick.pick_them_nits_in_term.problem_for_scope",
+ "bad offsets")
val kk = kodkod_constrs peephole_optim nat_card int_card main_j0
val (free_names, rep_table) =
choose_reps_for_free_vars scope free_names NameTable.empty
@@ -527,8 +509,8 @@
defs = nondef_fs @ def_fs @ declarative_axioms})
end
handle TOO_LARGE (loc, msg) =>
- if loc = "Nitpick_KK.check_arity"
- andalso not (Typtab.is_empty ofs) then
+ if loc = "Nitpick_Kodkod.check_arity" andalso
+ not (Typtab.is_empty ofs) then
problem_for_scope liberal
{ext_ctxt = ext_ctxt, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth,
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Jan 20 10:38:19 2010 +0100
@@ -82,6 +82,7 @@
val dest_n_tuple : int -> term -> term list
val instantiate_type : theory -> typ -> typ -> typ -> typ
val is_real_datatype : theory -> string -> bool
+ val is_quot_type : theory -> typ -> bool
val is_codatatype : theory -> typ -> bool
val is_pure_typedef : theory -> typ -> bool
val is_univ_typedef : theory -> typ -> bool
@@ -91,6 +92,8 @@
val is_record_update : theory -> styp -> bool
val is_abs_fun : theory -> styp -> bool
val is_rep_fun : theory -> styp -> bool
+ val is_quot_abs_fun : Proof.context -> styp -> bool
+ val is_quot_rep_fun : Proof.context -> styp -> bool
val is_constr : theory -> styp -> bool
val is_stale_constr : theory -> styp -> bool
val is_sel : string -> bool
@@ -325,6 +328,8 @@
(@{const_name uminus_int_inst.uminus_int}, 0),
(@{const_name ord_int_inst.less_int}, 2),
(@{const_name ord_int_inst.less_eq_int}, 2),
+ (@{const_name unknown}, 0),
+ (@{const_name is_unknown}, 1),
(@{const_name Tha}, 1),
(@{const_name Frac}, 0),
(@{const_name norm_frac}, 0)]
@@ -506,8 +511,8 @@
val constr_xs = map (apsnd (repair_constr_type thy co_T)) constr_xs
val (co_s, co_Ts) = dest_Type co_T
val _ =
- if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts)
- andalso co_s <> "fun" andalso not (is_basic_datatype co_s) then
+ if forall is_TFree co_Ts andalso not (has_duplicates (op =) co_Ts) andalso
+ co_s <> "fun" andalso not (is_basic_datatype co_s) then
()
else
raise TYPE ("Nitpick_HOL.register_codatatype", [co_T], [])
@@ -543,14 +548,16 @@
val is_typedef = is_some oo typedef_info
val is_real_datatype = is_some oo Datatype.get_info
(* theory -> typ -> bool *)
+fun is_quot_type _ (Type ("IntEx.my_int", _)) = true (* ### *)
+ | is_quot_type _ _ = false
fun is_codatatype thy (T as Type (s, _)) =
not (null (AList.lookup (op =) (#codatatypes (Data.get thy)) s
|> Option.map snd |> these))
| is_codatatype _ _ = false
fun is_pure_typedef thy (T as Type (s, _)) =
is_typedef thy s andalso
- not (is_real_datatype thy s orelse is_codatatype thy T
- orelse is_record_type T orelse is_integer_type T)
+ not (is_real_datatype thy s orelse is_quot_type thy T orelse
+ is_codatatype thy T orelse is_record_type T orelse is_integer_type T)
| is_pure_typedef _ _ = false
fun is_univ_typedef thy (Type (s, _)) =
(case typedef_info thy s of
@@ -564,8 +571,9 @@
| NONE => false)
| is_univ_typedef _ _ = false
fun is_datatype thy (T as Type (s, _)) =
- (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind})
- andalso not (is_basic_datatype s)
+ (is_typedef thy s orelse is_codatatype thy T orelse T = @{typ ind} orelse
+ is_quot_type thy T) andalso
+ not (is_basic_datatype s)
| is_datatype _ _ = false
(* theory -> typ -> (string * typ) list * (string * typ) *)
@@ -606,6 +614,11 @@
SOME {Rep_name, ...} => s = Rep_name
| NONE => false)
| is_rep_fun _ _ = false
+(* Proof.context -> styp -> bool *)
+fun is_quot_abs_fun _ ("IntEx.abs_my_int", _) = true (* ### *)
+ | is_quot_abs_fun _ _ = false
+fun is_quot_rep_fun _ ("IntEx.rep_my_int", _) = true (* ### *)
+ | is_quot_rep_fun _ _ = false
(* theory -> styp -> styp *)
fun mate_of_rep_fun thy (x as (_, Type ("fun", [T1 as Type (s', _), T2]))) =
@@ -613,6 +626,15 @@
SOME {Abs_name, ...} => (Abs_name, Type ("fun", [T2, T1]))
| NONE => raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x]))
| mate_of_rep_fun _ x = raise TERM ("Nitpick_HOL.mate_of_rep_fun", [Const x])
+(* theory -> typ -> typ *)
+fun rep_type_for_quot_type _ (Type ("IntEx.my_int", [])) = @{typ "nat * nat"}
+ | rep_type_for_quot_type _ T =
+ raise TYPE ("Nitpick_HOL.rep_type_for_quot_type", [T], [])
+(* theory -> typ -> term *)
+fun equiv_relation_for_quot_type _ (Type ("IntEx.my_int", [])) =
+ Const ("IntEx.intrel", @{typ "(nat * nat) => (nat * nat) => bool"})
+ | equiv_relation_for_quot_type _ T =
+ raise TYPE ("Nitpick_HOL.equiv_relation_for_quot_type", [T], [])
(* theory -> styp -> bool *)
fun is_coconstr thy (s, T) =
@@ -628,19 +650,20 @@
fun is_constr_like thy (s, T) =
s = @{const_name FunBox} orelse s = @{const_name PairBox} orelse
let val (x as (s, T)) = (s, unbit_and_unbox_type T) in
- Refute.is_IDT_constructor thy x orelse is_record_constr x
- orelse (is_abs_fun thy x andalso is_pure_typedef thy (range_type T))
- orelse s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep}
- orelse x = (@{const_name zero_nat_inst.zero_nat}, nat_T)
- orelse is_coconstr thy x
+ Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
+ (is_abs_fun thy x andalso is_pure_typedef thy (range_type T)) orelse
+ s = @{const_name Quot} orelse
+ s = @{const_name Zero_Rep} orelse s = @{const_name Suc_Rep} orelse
+ x = (@{const_name zero_nat_inst.zero_nat}, nat_T) orelse
+ is_coconstr thy x
end
fun is_stale_constr thy (x as (_, T)) =
- is_codatatype thy (body_type T) andalso is_constr_like thy x
- andalso not (is_coconstr thy x)
+ is_codatatype thy (body_type T) andalso is_constr_like thy x andalso
+ not (is_coconstr thy x)
fun is_constr thy (x as (_, T)) =
- is_constr_like thy x
- andalso not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T)))))
- andalso not (is_stale_constr thy x)
+ is_constr_like thy x andalso
+ not (is_basic_datatype (fst (dest_Type (unbit_type (body_type T))))) andalso
+ not (is_stale_constr thy x)
(* string -> bool *)
val is_sel = String.isPrefix discr_prefix orf String.isPrefix sel_prefix
val is_sel_like_and_no_discr =
@@ -662,13 +685,13 @@
fun is_boxing_worth_it (ext_ctxt : extended_context) boxy T =
case T of
Type ("fun", _) =>
- (boxy = InPair orelse boxy = InFunLHS)
- andalso not (is_boolean_type (body_type T))
+ (boxy = InPair orelse boxy = InFunLHS) andalso
+ not (is_boolean_type (body_type T))
| Type ("*", Ts) =>
- boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2
- orelse ((boxy = InExpr orelse boxy = InFunLHS)
- andalso exists (is_boxing_worth_it ext_ctxt InPair)
- (map (box_type ext_ctxt InPair) Ts))
+ boxy = InPair orelse boxy = InFunRHS1 orelse boxy = InFunRHS2 orelse
+ ((boxy = InExpr orelse boxy = InFunLHS) andalso
+ exists (is_boxing_worth_it ext_ctxt InPair)
+ (map (box_type ext_ctxt InPair) Ts))
| _ => false
(* extended_context -> boxability -> string * typ list -> string *)
and should_box_type (ext_ctxt as {thy, boxes, ...}) boxy (z as (s, Ts)) =
@@ -679,8 +702,8 @@
and box_type ext_ctxt boxy T =
case T of
Type (z as ("fun", [T1, T2])) =>
- if boxy <> InConstr andalso boxy <> InSel
- andalso should_box_type ext_ctxt boxy z then
+ if boxy <> InConstr andalso boxy <> InSel andalso
+ should_box_type ext_ctxt boxy z then
Type (@{type_name fun_box},
[box_type ext_ctxt InFunLHS T1, box_type ext_ctxt InFunRHS1 T2])
else
@@ -778,6 +801,8 @@
val T' = (Record.get_extT_fields thy T
|> apsnd single |> uncurry append |> map snd) ---> T
in [(s', T')] end
+ else if is_quot_type thy T then
+ [(@{const_name Quot}, rep_type_for_quot_type thy T --> T)]
else case typedef_info thy s of
SOME {abs_type, rep_type, Abs_name, ...} =>
[(Abs_name, instantiate_type thy abs_type T rep_type --> T)]
@@ -871,10 +896,10 @@
let val args = map Envir.eta_contract args in
case hd args of
Const (x' as (s', _)) $ t =>
- if is_sel_like_and_no_discr s' andalso constr_name_for_sel_like s' = s
- andalso forall (fn (n, t') =>
- select_nth_constr_arg thy x t n dummyT = t')
- (index_seq 0 (length args) ~~ args) then
+ if is_sel_like_and_no_discr s' andalso
+ constr_name_for_sel_like s' = s andalso
+ forall (fn (n, t') => select_nth_constr_arg thy x t n dummyT = t')
+ (index_seq 0 (length args) ~~ args) then
t
else
list_comb (Const x, args)
@@ -1011,8 +1036,8 @@
(* theory -> string -> bool *)
fun is_funky_typedef_name thy s =
member (op =) [@{type_name unit}, @{type_name "*"}, @{type_name "+"},
- @{type_name int}] s
- orelse is_frac_type thy (Type (s, []))
+ @{type_name int}] s orelse
+ is_frac_type thy (Type (s, []))
(* theory -> term -> bool *)
fun is_funky_typedef thy (Type (s, _)) = is_funky_typedef_name thy s
| is_funky_typedef _ _ = false
@@ -1055,8 +1080,8 @@
(* term -> bool *)
fun do_lhs t1 =
case strip_comb t1 of
- (Const _, args) => forall is_Var args
- andalso not (has_duplicates (op =) args)
+ (Const _, args) =>
+ forall is_Var args andalso not (has_duplicates (op =) args)
| _ => false
fun do_eq (Const (@{const_name "=="}, _) $ t1 $ _) = do_lhs t1
| do_eq (@{const Trueprop} $ (Const (@{const_name "op ="}, _) $ t1 $ _)) =
@@ -1174,8 +1199,8 @@
(* term -> bool *)
fun is_good_arg (Bound _) = true
| is_good_arg (Const (s, _)) =
- s = @{const_name True} orelse s = @{const_name False}
- orelse s = @{const_name undefined}
+ s = @{const_name True} orelse s = @{const_name False} orelse
+ s = @{const_name undefined}
| is_good_arg _ = false
in
case t |> strip_abs_body |> strip_comb of
@@ -1289,9 +1314,17 @@
fun nondef_props_for_const thy slack table (x as (s, _)) =
these (Symtab.lookup table s) |> maps (multi_specialize_type thy slack x)
+(* theory -> styp -> term list *)
+fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
+ let val abs_T = domain_type T in
+ typedef_info thy (fst (dest_Type abs_T)) |> the
+ |> pairf #Abs_inverse #Rep_inverse
+ |> pairself (Refute.specialize_type thy x o prop_of o the)
+ ||> single |> op ::
+ end
(* theory -> styp list -> term list *)
-fun optimized_typedef_axioms thy (abs_s, abs_Ts) =
- let val abs_T = Type (abs_s, abs_Ts) in
+fun optimized_typedef_axioms thy (abs_z as (abs_s, abs_Ts)) =
+ let val abs_T = Type abs_z in
if is_univ_typedef thy abs_T then
[]
else case typedef_info thy abs_s of
@@ -1313,13 +1346,31 @@
end
| NONE => []
end
-(* theory -> styp -> term list *)
-fun inverse_axioms_for_rep_fun thy (x as (_, T)) =
- let val abs_T = domain_type T in
- typedef_info thy (fst (dest_Type abs_T)) |> the
- |> pairf #Abs_inverse #Rep_inverse
- |> pairself (Refute.specialize_type thy x o prop_of o the)
- ||> single |> op ::
+fun optimized_quot_type_axioms thy abs_z =
+ let
+ val abs_T = Type abs_z
+ val rep_T = rep_type_for_quot_type thy abs_T
+ val equiv_rel = equiv_relation_for_quot_type thy abs_T
+ val a_var = Var (("a", 0), abs_T)
+ val x_var = Var (("x", 0), rep_T)
+ val y_var = Var (("y", 0), rep_T)
+ val x = (@{const_name Quot}, rep_T --> abs_T)
+ val sel_a_t = select_nth_constr_arg thy x a_var 0 rep_T
+ val normal_t = Const (@{const_name quot_normal}, rep_T --> rep_T)
+ val normal_x = normal_t $ x_var
+ val normal_y = normal_t $ y_var
+ val is_unknown_t = Const (@{const_name is_unknown}, rep_T --> bool_T)
+ in
+ [Logic.mk_equals (sel_a_t, normal_t $ sel_a_t),
+ Logic.list_implies
+ ([@{const Not} $ (HOLogic.mk_eq (x_var, y_var)),
+ @{const Not} $ (is_unknown_t $ normal_x),
+ @{const Not} $ (is_unknown_t $ normal_y),
+ equiv_rel $ x_var $ y_var] |> map HOLogic.mk_Trueprop,
+ Logic.mk_equals (normal_x, normal_y)),
+ @{const "==>"}
+ $ (HOLogic.mk_Trueprop (@{const Not} $ (is_unknown_t $ normal_x)))
+ $ (HOLogic.mk_Trueprop (equiv_rel $ x_var $ normal_x))]
end
(* theory -> int * styp -> term *)
@@ -1402,8 +1453,8 @@
(* extended_context -> styp -> bool *)
fun is_real_inductive_pred ({thy, fast_descrs, def_table, intro_table, ...}
: extended_context) x =
- not (null (def_props_for_const thy fast_descrs intro_table x))
- andalso fixpoint_kind_of_const thy def_table x <> NoFp
+ not (null (def_props_for_const thy fast_descrs intro_table x)) andalso
+ fixpoint_kind_of_const thy def_table x <> NoFp
fun is_real_equational_fun ({thy, fast_descrs, simp_table, psimp_table, ...}
: extended_context) x =
exists (fn table => not (null (def_props_for_const thy fast_descrs table x)))
@@ -1489,10 +1540,9 @@
(t1 |> HOLogic.dest_list |> distinctness_formula T'
handle TERM _ => do_const depth Ts t x [t1])
| (t0 as Const (x as (@{const_name If}, _))) $ t1 $ t2 $ t3 =>
- if is_ground_term t1
- andalso exists (Pattern.matches thy o rpair t1)
- (Inttab.lookup_list ground_thm_table
- (hash_term t1)) then
+ if is_ground_term t1 andalso
+ exists (Pattern.matches thy o rpair t1)
+ (Inttab.lookup_list ground_thm_table (hash_term t1)) then
do_term depth Ts t2
else
do_const depth Ts t x [t1, t2, t3]
@@ -1534,8 +1584,24 @@
if is_constr thy x then
(Const x, ts)
else if is_stale_constr thy x then
- raise NOT_SUPPORTED ("(non-co-)constructors of codatatypes \
+ raise NOT_SUPPORTED ("(non-co)constructors of codatatypes \
\(\"" ^ s ^ "\")")
+ else if is_quot_abs_fun thy x then
+ let
+ val rep_T = domain_type T
+ val abs_T = range_type T
+ in
+ (Abs (Name.uu, rep_T,
+ Const (@{const_name Quot}, rep_T --> abs_T)
+ $ (Const (@{const_name quot_normal},
+ rep_T --> rep_T) $ Bound 0)), ts)
+ end
+ else if is_quot_rep_fun thy x then
+ let
+ val abs_T = domain_type T
+ val rep_T = range_type T
+ val x' = (@{const_name Quot}, rep_T --> abs_T)
+ in select_nth_constr_arg_with_args depth Ts x' ts 0 rep_T end
else if is_record_get thy x then
case length ts of
0 => (do_term depth Ts (eta_expand Ts t 1), [])
@@ -1691,8 +1757,8 @@
else
()
in
- if tac_timeout = (!cached_timeout)
- andalso length (!cached_wf_props) < max_cached_wfs then
+ if tac_timeout = (!cached_timeout) andalso
+ length (!cached_wf_props) < max_cached_wfs then
()
else
(cached_wf_props := []; cached_timeout := tac_timeout);
@@ -1716,8 +1782,8 @@
(x as (s, _)) =
case triple_lookup (const_match thy) wfs x of
SOME (SOME b) => b
- | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'}
- orelse case AList.lookup (op =) (!wf_cache) x of
+ | _ => s = @{const_name Nats} orelse s = @{const_name fold_graph'} orelse
+ case AList.lookup (op =) (!wf_cache) x of
SOME (_, wf) => wf
| NONE =>
let
@@ -1859,8 +1925,8 @@
in
if is_equational_fun ext_ctxt x' then
unrolled_const (* already done *)
- else if not gfp andalso is_linear_inductive_pred_def def
- andalso star_linear_preds then
+ else if not gfp andalso is_linear_inductive_pred_def def andalso
+ star_linear_preds then
starred_linear_pred_const ext_ctxt x def
else
let
@@ -1980,10 +2046,10 @@
let val t_comb = list_comb (t, args) in
case t of
Const x =>
- if not relax andalso is_constr thy x
- andalso not (is_fun_type (fastype_of1 (Ts, t_comb)))
- andalso has_heavy_bounds_or_vars Ts level t_comb
- andalso not (loose_bvar (t_comb, level)) then
+ if not relax andalso is_constr thy x andalso
+ not (is_fun_type (fastype_of1 (Ts, t_comb))) andalso
+ has_heavy_bounds_or_vars Ts level t_comb andalso
+ not (loose_bvar (t_comb, level)) then
let
val (j, seen) = case find_index (curry (op =) t_comb) seen of
~1 => (0, t_comb :: seen)
@@ -2062,18 +2128,17 @@
and aux_eq careful pass1 t0 t1 t2 =
(if careful then
raise SAME ()
- else if axiom andalso is_Var t2
- andalso num_occs_of_var (dest_Var t2) = 1 then
+ else if axiom andalso is_Var t2 andalso
+ num_occs_of_var (dest_Var t2) = 1 then
@{const True}
else case strip_comb t2 of
(Const (x as (s, T)), args) =>
let val arg_Ts = binder_types T in
- if length arg_Ts = length args
- andalso (is_constr thy 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
+ if length arg_Ts = length args andalso
+ (is_constr thy 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 ext_ctxt x t1 ::
map3 (sel_eq x t1) (index_seq 0 (length args)) arg_Ts args
|> foldr1 s_conj
@@ -2095,8 +2160,8 @@
let
(* term -> int -> term *)
fun is_nth_sel_on t' n (Const (s, _) $ t) =
- (t = t' andalso is_sel_like_and_no_discr s
- andalso sel_no_from_name s = n)
+ (t = t' andalso is_sel_like_and_no_discr s andalso
+ sel_no_from_name s = n)
| is_nth_sel_on _ _ _ = false
(* term -> term list -> term *)
fun do_term (Const (@{const_name Rep_Frac}, _)
@@ -2109,9 +2174,9 @@
if length args = num_binder_types T then
case hd args of
Const (x' as (_, T')) $ t' =>
- if domain_type T' = body_type T
- andalso forall (uncurry (is_nth_sel_on t'))
- (index_seq 0 (length args) ~~ args) then
+ if domain_type T' = body_type T andalso
+ forall (uncurry (is_nth_sel_on t'))
+ (index_seq 0 (length args) ~~ args) then
t'
else
raise SAME ()
@@ -2121,9 +2186,9 @@
else if is_sel_like_and_no_discr s then
case strip_comb (hd args) of
(Const (x' as (s', T')), ts') =>
- if is_constr_like thy x'
- andalso constr_name_for_sel_like s = s'
- andalso not (exists is_pair_type (binder_types T')) then
+ if is_constr_like thy x' andalso
+ constr_name_for_sel_like s = s' andalso
+ not (exists is_pair_type (binder_types T')) then
list_comb (nth ts' (sel_no_from_name s), tl args)
else
raise SAME ()
@@ -2164,8 +2229,8 @@
(* term list -> (indexname * typ) list -> indexname * typ -> term -> term
-> term -> term *)
and aux_eq prems zs z t' t1 t2 =
- if not (member (op =) zs z)
- andalso not (exists_subterm (curry (op =) (Var z)) t') then
+ if not (member (op =) zs z) andalso
+ not (exists_subterm (curry (op =) (Var z)) t') then
aux prems zs (subst_free [(Var z, t')] t2)
else
aux (t1 :: prems) (Term.add_vars t1 zs) t2
@@ -2323,8 +2388,8 @@
(t0 as Const (s0, _)) $ Abs (s1, T1, t1 as _ $ _) =>
if s0 = quant_s andalso length Ts < quantifier_cluster_max_size then
aux s0 (s1 :: ss) (T1 :: Ts) t1
- else if quant_s = "" andalso (s0 = @{const_name All}
- orelse s0 = @{const_name Ex}) then
+ else if quant_s = "" andalso
+ (s0 = @{const_name All} orelse s0 = @{const_name Ex}) then
aux s0 [s1] [T1] t1
else
raise SAME ()
@@ -2402,8 +2467,8 @@
(* polarity -> string -> bool *)
fun is_positive_existential polar quant_s =
- (polar = Pos andalso quant_s = @{const_name Ex})
- orelse (polar = Neg andalso quant_s <> @{const_name Ex})
+ (polar = Pos andalso quant_s = @{const_name Ex}) orelse
+ (polar = Neg andalso quant_s <> @{const_name Ex})
(* extended_context -> int -> term -> term *)
fun skolemize_term_and_more (ext_ctxt as {thy, def_table, skolems, ...})
@@ -2418,8 +2483,8 @@
fun do_quantifier quant_s quant_T abs_s abs_T t =
if not (loose_bvar1 (t, 0)) then
aux ss Ts js depth polar (incr_boundvars ~1 t)
- else if depth <= skolem_depth
- andalso is_positive_existential polar quant_s then
+ else if depth <= skolem_depth andalso
+ is_positive_existential polar quant_s then
let
val j = length (!skolems) + 1
val sko_s = skolem_prefix_for (length js) j ^ abs_s
@@ -2469,8 +2534,8 @@
| (t0 as Const (@{const_name Let}, T0)) $ t1 $ t2 =>
t0 $ t1 $ aux ss Ts js depth polar t2
| Const (x as (s, T)) =>
- if is_inductive_pred ext_ctxt x
- andalso not (is_well_founded_inductive_pred ext_ctxt x) then
+ if is_inductive_pred ext_ctxt x andalso
+ not (is_well_founded_inductive_pred ext_ctxt x) then
let
val gfp = (fixpoint_kind_of_const thy def_table x = Gfp)
val (pref, connective, set_oper) =
@@ -2582,9 +2647,9 @@
(* typ list -> term -> bool *)
fun is_eligible_arg Ts t =
let val bad_Ts = map snd (Term.add_vars t []) @ map (nth Ts) (loose_bnos t) in
- null bad_Ts
- orelse (is_higher_order_type (fastype_of1 (Ts, t))
- andalso forall (not o is_higher_order_type) bad_Ts)
+ null bad_Ts orelse
+ (is_higher_order_type (fastype_of1 (Ts, t)) andalso
+ forall (not o is_higher_order_type) bad_Ts)
end
(* (int * term option) list -> (int * term) list -> int list *)
@@ -2608,9 +2673,9 @@
else case term_under_def t of Const x => [x] | _ => []
(* term list -> typ list -> term -> term *)
fun aux args Ts (Const (x as (s, T))) =
- ((if not (member (op =) blacklist x) andalso not (null args)
- andalso not (String.isPrefix special_prefix s)
- andalso is_equational_fun ext_ctxt x then
+ ((if not (member (op =) blacklist x) andalso not (null args) andalso
+ not (String.isPrefix special_prefix s) andalso
+ is_equational_fun ext_ctxt x then
let
val eligible_args = filter (is_eligible_arg Ts o snd)
(index_seq 0 (length args) ~~ args)
@@ -2678,8 +2743,8 @@
let val table = aux t2 [] table in aux t1 (t2 :: args) table end
| aux (Abs (_, _, t')) _ table = aux t' [] table
| aux (t as Const (x as (s, _))) args table =
- if is_built_in_const true x orelse is_constr_like thy x orelse is_sel s
- orelse s = @{const_name Sigma} then
+ if is_built_in_const true x orelse is_constr_like thy x orelse
+ is_sel s orelse s = @{const_name Sigma} then
table
else
Termtab.map_default (t, 65536) (curry Int.min (length args)) table
@@ -2699,8 +2764,8 @@
let
val (arg_Ts, rest_T) = strip_n_binders n T
val j =
- if hd arg_Ts = @{typ bisim_iterator}
- orelse is_fp_iterator_type (hd arg_Ts) then
+ if hd arg_Ts = @{typ bisim_iterator} orelse
+ is_fp_iterator_type (hd arg_Ts) then
1
else case find_index (not_equal bool_T) arg_Ts of
~1 => n
@@ -2766,8 +2831,8 @@
\coerce_term", [t']))
| (Type (new_s, new_Ts as [new_T1, new_T2]),
Type (old_s, old_Ts as [old_T1, old_T2])) =>
- if old_s = @{type_name fun_box} orelse old_s = @{type_name pair_box}
- orelse old_s = "*" then
+ if old_s = @{type_name fun_box} orelse
+ old_s = @{type_name pair_box} orelse old_s = "*" then
case constr_expand ext_ctxt old_T t of
Const (@{const_name FunBox}, _) $ t1 =>
if new_s = "fun" then
@@ -2881,13 +2946,17 @@
$ do_term new_Ts old_Ts polar t2
| Const (s as @{const_name The}, T) => do_description_operator s T
| Const (s as @{const_name Eps}, T) => do_description_operator s T
+ | Const (@{const_name quot_normal}, Type ("fun", [_, T2])) =>
+ let val T' = box_type ext_ctxt InFunRHS1 T2 in
+ Const (@{const_name quot_normal}, T' --> T')
+ end
| Const (s as @{const_name Tha}, T) => do_description_operator s T
| Const (x as (s, T)) =>
- Const (s, if s = @{const_name converse}
- orelse s = @{const_name trancl} then
+ Const (s, if s = @{const_name converse} orelse
+ s = @{const_name trancl} then
box_relational_operator_type T
- else if is_built_in_const fast_descrs x
- orelse s = @{const_name Sigma} then
+ else if is_built_in_const fast_descrs x orelse
+ s = @{const_name Sigma} then
T
else if is_constr_like thy x then
box_type ext_ctxt InConstr T
@@ -2972,7 +3041,7 @@
|> map Logic.mk_equals,
Logic.mk_equals (list_comb (Const x1, bounds1 @ args1),
list_comb (Const x2, bounds2 @ args2)))
- |> Refute.close_form
+ |> Refute.close_form (* TODO: needed? *)
end
(* extended_context -> styp list -> term list *)
@@ -3078,23 +3147,29 @@
fold (add_eq_axiom depth) (equational_fun_axioms ext_ctxt x)
accum
else if is_abs_fun thy x then
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
+ if is_quot_type thy (range_type T) then
+ raise NOT_SUPPORTED "\"Abs_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
(extra_table def_table s) x)
else if is_rep_fun thy x then
- accum |> fold (add_nondef_axiom depth)
- (nondef_props_for_const thy false nondef_table x)
- |> is_funky_typedef thy (range_type T)
- ? fold (add_maybe_def_axiom depth)
- (nondef_props_for_const thy true
+ if is_quot_type thy (domain_type T) then
+ raise NOT_SUPPORTED "\"Rep_\" function of quotient type"
+ else
+ accum |> fold (add_nondef_axiom depth)
+ (nondef_props_for_const thy false nondef_table x)
+ |> is_funky_typedef thy (range_type T)
+ ? fold (add_maybe_def_axiom depth)
+ (nondef_props_for_const thy true
(extra_table def_table s) x)
- |> add_axioms_for_term depth
- (Const (mate_of_rep_fun thy x))
- |> fold (add_def_axiom depth)
- (inverse_axioms_for_rep_fun thy x)
+ |> add_axioms_for_term depth
+ (Const (mate_of_rep_fun thy x))
+ |> fold (add_def_axiom depth)
+ (inverse_axioms_for_rep_fun thy x)
else
accum |> user_axioms <> SOME false
? fold (add_nondef_axiom depth)
@@ -3116,10 +3191,12 @@
| @{typ unit} => I
| TFree (_, S) => add_axioms_for_sort depth T S
| TVar (_, S) => add_axioms_for_sort depth T S
- | Type (z as (_, Ts)) =>
+ | Type (z as (s, Ts)) =>
fold (add_axioms_for_type depth) Ts
#> (if is_pure_typedef thy T then
fold (add_maybe_def_axiom depth) (optimized_typedef_axioms thy z)
+ else if is_quot_type thy T then
+ fold (add_def_axiom depth) (optimized_quot_type_axioms thy z)
else if max_bisim_depth >= 0 andalso is_codatatype thy T then
fold (add_maybe_def_axiom depth)
(codatatype_bisim_axioms ext_ctxt T)
@@ -3364,11 +3441,11 @@
member (op =) [@{const_name times_nat_inst.times_nat},
@{const_name div_nat_inst.div_nat},
@{const_name times_int_inst.times_int},
- @{const_name div_int_inst.div_int}] s
- orelse (String.isPrefix numeral_prefix s andalso
- let val n = the (Int.fromString (unprefix numeral_prefix s)) in
- n <= ~ binary_int_threshold orelse n >= binary_int_threshold
- end)
+ @{const_name div_int_inst.div_int}] s orelse
+ (String.isPrefix numeral_prefix s andalso
+ let val n = the (Int.fromString (unprefix numeral_prefix s)) in
+ n <= ~ binary_int_threshold orelse n >= binary_int_threshold
+ end)
| should_use_binary_ints (Abs (_, _, t')) = should_use_binary_ints t'
| should_use_binary_ints _ = false
@@ -3398,8 +3475,8 @@
SOME false => false
| _ =>
forall may_use_binary_ints (core_t :: def_ts @ nondef_ts) andalso
- (binary_ints = SOME true
- orelse exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
+ (binary_ints = SOME true orelse
+ exists should_use_binary_ints (core_t :: def_ts @ nondef_ts))
val box = exists (not_equal (SOME false) o snd) boxes
val table =
Termtab.empty |> uncurry
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Wed Jan 20 10:38:19 2010 +0100
@@ -106,12 +106,12 @@
(* string -> bool *)
fun is_known_raw_param s =
- AList.defined (op =) default_default_params s
- orelse AList.defined (op =) negated_params s
- orelse s = "max" orelse s = "eval" orelse s = "expect"
- orelse exists (fn p => String.isPrefix (p ^ " ") s)
- ["card", "max", "iter", "box", "dont_box", "mono", "non_mono",
- "wf", "non_wf", "format"]
+ AList.defined (op =) default_default_params s orelse
+ AList.defined (op =) negated_params s orelse
+ s = "max" orelse s = "eval" orelse s = "expect" orelse
+ exists (fn p => String.isPrefix (p ^ " ") s)
+ ["card", "max", "iter", "box", "dont_box", "mono", "non_mono", "wf",
+ "non_wf", "format"]
(* string * 'a -> unit *)
fun check_raw_param (s, _) =
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Jan 20 10:38:19 2010 +0100
@@ -380,8 +380,8 @@
val one = is_one_rep body_R
val opt_x = case r of KK.Rel x => SOME x | _ => NONE
in
- if opt_x <> NONE andalso length binder_schema = 1
- andalso length body_schema = 1 then
+ if opt_x <> NONE andalso length binder_schema = 1 andalso
+ length body_schema = 1 then
(if one then KK.Function else KK.Functional)
(the opt_x, KK.AtomSeq (hd binder_schema),
KK.AtomSeq (hd body_schema))
@@ -490,8 +490,8 @@
r
else
let val card = card_of_rep old_R in
- if is_lone_rep old_R andalso is_lone_rep new_R
- andalso card = card_of_rep new_R then
+ if is_lone_rep old_R andalso is_lone_rep new_R andalso
+ card = card_of_rep new_R then
if card >= lone_rep_fallback_max_card then
raise TOO_LARGE ("Nitpick_Kodkod.lone_rep_fallback",
"too high cardinality (" ^ string_of_int card ^ ")")
@@ -1005,13 +1005,13 @@
| Op1 (Finite, _, _, u1) =>
let val opt1 = is_opt_rep (rep_of u1) in
case polar of
- Neut => if opt1 then
- raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
- else
- KK.True
+ Neut =>
+ if opt1 then raise NUT ("Nitpick_Kodkod.to_f (Finite)", [u])
+ else KK.True
| Pos => formula_for_bool (not opt1)
| Neg => KK.True
end
+ | Op1 (IsUnknown, _, _, u1) => kk_no (to_r u1)
| Op1 (Cast, _, _, u1) => to_f_with_polarity polar u1
| Op2 (All, _, _, u1, u2) =>
kk_all (untuple to_decl u1) (to_f_with_polarity polar u2)
@@ -1070,8 +1070,8 @@
| args _ = []
val opt_arg_us = filter (is_opt_rep o rep_of) (args u1)
in
- if null opt_arg_us orelse not (is_Opt min_R)
- orelse is_eval_name u1 then
+ if null opt_arg_us orelse not (is_Opt min_R) orelse
+ is_eval_name u1 then
fold (kk_or o (kk_no o to_r)) opt_arg_us
(kk_rel_eq (to_rep min_R u1) (to_rep min_R u2))
else
@@ -1100,8 +1100,8 @@
(if polar = Pos then
if not both_opt then
kk_rel_eq r1 r2
- else if is_lone_rep min_R
- andalso arity_of_rep min_R = 1 then
+ else if is_lone_rep min_R andalso
+ arity_of_rep min_R = 1 then
kk_some (kk_intersect r1 r2)
else
raise SAME ()
@@ -1132,9 +1132,9 @@
val rs1 = unpack_products r1
val rs2 = unpack_products r2
in
- if length rs1 = length rs2
- andalso map KK.arity_of_rel_expr rs1
- = map KK.arity_of_rel_expr rs2 then
+ if length rs1 = length rs2 andalso
+ map KK.arity_of_rel_expr rs1
+ = map KK.arity_of_rel_expr rs2 then
fold1 kk_and (map2 kk_subset rs1 rs2)
else
kk_subset r1 r2
@@ -1582,8 +1582,8 @@
else
fold kk_join (map to_integer [u1, u2]) (KK.Rel nat_subtract_rel)
| Op2 (Apply, _, R, u1, u2) =>
- if is_Cst Unrep u2 andalso is_set_type (type_of u1)
- andalso is_FreeName u1 then
+ if is_Cst Unrep u2 andalso is_set_type (type_of u1) andalso
+ is_FreeName u1 then
false_atom
else
to_apply R u1 u2
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Jan 20 10:38:19 2010 +0100
@@ -440,7 +440,9 @@
| _ => raise TERM ("Nitpick_Model.reconstruct_term.term_\
\for_atom (Abs_Frac)", ts)
end
- else if not for_auto andalso is_abs_fun thy constr_x then
+ else if not for_auto andalso
+ (is_abs_fun thy constr_x orelse
+ constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
else
list_comb (Const constr_x, ts)
@@ -560,8 +562,8 @@
pairself (strip_comb o unfold_outer_the_binders) (t1, t2)
val max_depth = max_depth - (if member (op =) coTs T then 1 else 0)
in
- head1 = head2
- andalso forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
+ head1 = head2 andalso
+ forall (bisimilar_values coTs max_depth) (args1 ~~ args2)
end
else
t1 = t2
@@ -704,8 +706,8 @@
in
(Pretty.chunks (if null chunks then [Pretty.str "Empty assignment"]
else chunks),
- bisim_depth >= 0
- orelse forall (is_codatatype_wellformed codatatypes) codatatypes)
+ bisim_depth >= 0 orelse
+ forall (is_codatatype_wellformed codatatypes) codatatypes)
end
(* scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Wed Jan 20 10:38:19 2010 +0100
@@ -121,8 +121,8 @@
(* typ -> typ -> bool *)
fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) =
- T = alpha_T orelse (not (is_fp_iterator_type T)
- andalso exists (could_exist_alpha_subtype alpha_T) Ts)
+ T = alpha_T orelse (not (is_fp_iterator_type T) andalso
+ exists (could_exist_alpha_subtype alpha_T) Ts)
| could_exist_alpha_subtype alpha_T T = (T = alpha_T)
(* theory -> typ -> typ -> bool *)
fun could_exist_alpha_sub_ctype _ (alpha_T as TFree _) T =
@@ -195,8 +195,8 @@
let
val C1 = do_type T1
val C2 = do_type T2
- val a = if is_boolean_type (body_type T2)
- andalso exists_alpha_sub_ctype_fresh C1 then
+ val a = if is_boolean_type (body_type T2) andalso
+ exists_alpha_sub_ctype_fresh C1 then
V (Unsynchronized.inc max_fresh)
else
S Neg
--- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Wed Jan 20 10:38:19 2010 +0100
@@ -39,6 +39,7 @@
Converse |
Closure |
SingletonSet |
+ IsUnknown |
Tha |
First |
Second |
@@ -158,6 +159,7 @@
Converse |
Closure |
SingletonSet |
+ IsUnknown |
Tha |
First |
Second |
@@ -231,6 +233,7 @@
| string_for_op1 Converse = "Converse"
| string_for_op1 Closure = "Closure"
| string_for_op1 SingletonSet = "SingletonSet"
+ | string_for_op1 IsUnknown = "IsUnknown"
| string_for_op1 Tha = "Tha"
| string_for_op1 First = "First"
| string_for_op1 Second = "Second"
@@ -567,7 +570,6 @@
sub t1, sub_abs s T' t2)
| (t0 as Const (@{const_name Let}, T), [t1, t2]) =>
sub (t0 $ t1 $ eta_expand Ts t2 1)
- | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
| (@{const Unity}, []) => Cst (Unity, @{typ unit}, Any)
| (Const (@{const_name Pair}, T), [t1, t2]) =>
Tuple (nth_range_type 2 T, Any, map sub [t1, t2])
@@ -641,6 +643,9 @@
Op2 (Less, bool_T, Any, sub t1, sub t2)
| (Const (@{const_name ord_int_inst.less_eq_int}, T), [t1, t2]) =>
Op1 (Not, bool_T, Any, Op2 (Less, bool_T, Any, sub t2, sub t1))
+ | (Const (@{const_name unknown}, T), []) => Cst (Unknown, T, Any)
+ | (Const (@{const_name is_unknown}, T), [t1]) =>
+ Op1 (IsUnknown, bool_T, Any, sub t1)
| (Const (@{const_name Tha}, Type ("fun", [_, T2])), [t1]) =>
Op1 (Tha, T2, Any, sub t1)
| (Const (@{const_name Frac}, T), []) => Cst (Fracs, T, Any)
@@ -715,12 +720,12 @@
rep_for_abs_fun
else if is_rep_fun thy x then
Func oo best_non_opt_symmetric_reps_for_fun_type
- else if all_exact orelse is_skolem_name v
- orelse member (op =) [@{const_name undefined_fast_The},
- @{const_name undefined_fast_Eps},
- @{const_name bisim},
- @{const_name bisim_iterator_max}]
- (original_name s) then
+ else if all_exact orelse is_skolem_name v orelse
+ member (op =) [@{const_name undefined_fast_The},
+ @{const_name undefined_fast_Eps},
+ @{const_name bisim},
+ @{const_name bisim_iterator_max}]
+ (original_name s) then
best_non_opt_set_rep_for_type
else if member (op =) [@{const_name set}, @{const_name distinct},
@{const_name ord_class.less},
@@ -746,9 +751,9 @@
(vs, table) =
let
val (s', T') = boxed_nth_sel_for_constr ext_ctxt x n
- val R' = if n = ~1 orelse is_word_type (body_type T)
- orelse (is_fun_type (range_type T')
- andalso is_boolean_type (body_type T')) then
+ val R' = if n = ~1 orelse is_word_type (body_type T) orelse
+ (is_fun_type (range_type T') andalso
+ is_boolean_type (body_type T')) then
best_non_opt_set_rep_for_type scope T'
else
best_opt_set_rep_for_type scope T' |> unopt_rep
@@ -798,10 +803,8 @@
if rep_of u = Unit then Cst (Unity, type_of u, Unit) else u
(* typ -> rep -> nut *)
fun unknown_boolean T R =
- Cst (case R of
- Formula Pos => False
- | Formula Neg => True
- | _ => Unknown, T, R)
+ Cst (case R of Formula Pos => False | Formula Neg => True | _ => Unknown,
+ T, R)
(* op1 -> typ -> rep -> nut -> nut *)
fun s_op1 oper T R u1 =
@@ -954,19 +957,18 @@
let
val T1 = domain_type T
val R1 = Atom (spec_of_type scope T1)
- val total = T1 = nat_T
- andalso (cst = Subtract orelse cst = Divide
- orelse cst = Gcd)
+ val total = T1 = nat_T andalso
+ (cst = Subtract orelse cst = Divide orelse cst = Gcd)
in Cst (cst, T, Func (R1, Func (R1, (not total ? Opt) R1))) end
else if cst = NatToInt orelse cst = IntToNat then
let
val (dom_card, dom_j0) = spec_of_type scope (domain_type T)
val (ran_card, ran_j0) = spec_of_type scope (range_type T)
- val total = not (is_word_type (domain_type T))
- andalso (if cst = NatToInt then
- max_int_for_card ran_card >= dom_card + 1
- else
- max_int_for_card dom_card < ran_card)
+ val total = not (is_word_type (domain_type T)) andalso
+ (if cst = NatToInt then
+ max_int_for_card ran_card >= dom_card + 1
+ else
+ max_int_for_card dom_card < ran_card)
in
Cst (cst, T, Func (Atom (dom_card, dom_j0),
Atom (ran_card, ran_j0) |> not total ? Opt))
@@ -979,6 +981,11 @@
triad (s_op1 Not T (Formula Pos) u12)
(s_op1 Not T (Formula Neg) u11)
| u1' => s_op1 Not T (flip_rep_polarity (rep_of u1')) u1')
+ | Op1 (IsUnknown, T, _, u1) =>
+ let val u1 = sub u1 in
+ if is_opt_rep (rep_of u1) then Op1 (IsUnknown, T, Formula Neut, u1)
+ else Cst (False, T, Formula Neut)
+ end
| Op1 (oper, T, _, u1) =>
let
val u1 = sub u1
@@ -1029,8 +1036,8 @@
if is_constructive u then s_op2 Eq T (Formula Neut) u1' u2'
else opt_opt_case ()
in
- if liberal orelse polar = Neg
- orelse is_concrete_type datatypes (type_of u1) then
+ if liberal orelse polar = Neg orelse
+ is_concrete_type datatypes (type_of u1) then
case (is_opt_rep (rep_of u1'), is_opt_rep (rep_of u2')) of
(true, true) => opt_opt_case ()
| (true, false) => hybrid_case u1'
@@ -1108,12 +1115,11 @@
val u1' = aux table' false Neut u1
val u2' = aux table' false Neut u2
val R =
- if is_opt_rep (rep_of u2')
- orelse (range_type T = bool_T andalso
- not (is_Cst False
- (unrepify_nut_in_nut table false Neut
- u1 u2
- |> optimize_nut))) then
+ if is_opt_rep (rep_of u2') orelse
+ (range_type T = bool_T andalso
+ not (is_Cst False (unrepify_nut_in_nut table false Neut
+ u1 u2
+ |> optimize_nut))) then
opt_rep ofs T R
else
unopt_rep R
@@ -1131,9 +1137,9 @@
triad_fn (fn polar => gsub def polar u)
else
let val quant_u = s_op2 oper T (Formula polar) u1' u2' in
- if def
- orelse (liberal andalso (polar = Pos) = (oper = All))
- orelse is_complete_type datatypes (type_of u1) then
+ if def orelse
+ (liberal andalso (polar = Pos) = (oper = All)) orelse
+ is_complete_type datatypes (type_of u1) then
quant_u
else
let
@@ -1231,8 +1237,8 @@
in Construct (map sub us', T, R |> opt ? Opt, us) end
| _ =>
let val u = modify_name_rep u (the_name table u) in
- if polar = Neut orelse not (is_boolean_type (type_of u))
- orelse not (is_opt_rep (rep_of u)) then
+ if polar = Neut orelse not (is_boolean_type (type_of u)) orelse
+ not (is_opt_rep (rep_of u)) then
u
else
s_op1 Cast (type_of u) (Formula polar) u
--- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Wed Jan 20 10:38:19 2010 +0100
@@ -421,8 +421,8 @@
if is_one_rel_expr r1 then
s_or (s_subset r1 r21) (s_subset r1 r22)
else
- if s_subset r1 r21 = True orelse s_subset r1 r22 = True
- orelse r1 = r2 then
+ if s_subset r1 r21 = True orelse s_subset r1 r22 = True orelse
+ r1 = r2 then
True
else
Subset (r1, r2)
--- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Wed Jan 20 10:38:19 2010 +0100
@@ -274,8 +274,8 @@
| (R1, R2) => Struct [R1, R2])
| best_one_rep_for_type (scope as {card_assigns, datatypes, ofs, ...}) T =
(case card_of_type card_assigns T of
- 1 => if is_some (datatype_spec datatypes T)
- orelse is_fp_iterator_type T then
+ 1 => if is_some (datatype_spec datatypes T) orelse
+ is_fp_iterator_type T then
Atom (1, offset_of_type ofs T)
else
Unit
--- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Wed Jan 20 10:38:19 2010 +0100
@@ -107,8 +107,8 @@
| is_complete_type dtypes (Type ("*", Ts)) =
forall (is_complete_type dtypes) Ts
| is_complete_type dtypes T =
- not (is_integer_type T) andalso not (is_bit_type T)
- andalso #complete (the (datatype_spec dtypes T))
+ not (is_integer_type T) andalso not (is_bit_type T) andalso
+ #complete (the (datatype_spec dtypes T))
handle Option.Option => true
and is_concrete_type dtypes (Type ("fun", [T1, T2])) =
is_complete_type dtypes T1 andalso is_concrete_type dtypes T2
@@ -427,8 +427,8 @@
{delta = delta, epsilon = delta, exclusive = true, total = false}
end
else if not co andalso num_self_recs > 0 then
- if not self_rec andalso num_non_self_recs = 1
- andalso domain_card 2 card_assigns T = 1 then
+ if not self_rec andalso num_non_self_recs = 1 andalso
+ domain_card 2 card_assigns T = 1 then
{delta = 0, epsilon = 1, exclusive = (s = @{const_name Nil}),
total = true}
else if s = @{const_name Cons} then
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jan 19 17:53:11 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Wed Jan 20 10:38:19 2010 +0100
@@ -285,8 +285,8 @@
(* string -> string *)
fun maybe_quote y =
let val s = plain_string_from_yxml y in
- y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s))
- orelse OuterKeyword.is_keyword s) ? quote
+ y |> (not (is_long_identifier (perhaps (try (unprefix "'")) s)) orelse
+ OuterKeyword.is_keyword s) ? quote
end
end;