# HG changeset patch # User blanchet # Date 1267199409 -3600 # Node ID 4356263e0bdd794d6a89bacf830567e952515e66 # Parent f5fa7c72937edbf0f4dc85861f096120b70d4229# Parent 45a4e19d3ebde35eae0e1d25929db2cccf08ad87 merged diff -r f5fa7c72937e -r 4356263e0bdd doc-src/Nitpick/nitpick.tex --- a/doc-src/Nitpick/nitpick.tex Fri Feb 26 13:29:43 2010 +0100 +++ b/doc-src/Nitpick/nitpick.tex Fri Feb 26 16:50:09 2010 +0100 @@ -472,7 +472,7 @@ \prew \textbf{lemma} ``$\forall n.\; \textit{Suc}~n \mathbin{\not=} n \,\Longrightarrow\, P$'' \\ \textbf{nitpick} [\textit{card~nat}~= 100, \textit{check\_potential}] \\[2\smallskipamount] -\slshape Warning: The conjecture either trivially holds for the given scopes or (more likely) lies outside Nitpick's supported +\slshape Warning: The conjecture either trivially holds for the given scopes or lies outside Nitpick's supported fragment. Only potential counterexamples may be found. \\[2\smallskipamount] Nitpick found a potential counterexample: \\[2\smallskipamount] \hbox{}\qquad Free variable: \nopagebreak \\ @@ -2743,8 +2743,8 @@ \item[$\bullet$] Although this has never been observed, arbitrary theorem morphisms could possibly confuse Nitpick, resulting in spurious counterexamples. -%\item[$\bullet$] All constants and types whose names start with -%\textit{Nitpick}{.} are reserved for internal use. +\item[$\bullet$] All constants, types, free variables, and schematic variables +whose names start with \textit{Nitpick}{.} are reserved for internal use. \end{enum} \let\em=\sl diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Nitpick_Examples/Core_Nits.thy --- a/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Core_Nits.thy Fri Feb 26 16:50:09 2010 +0100 @@ -1000,7 +1000,7 @@ oops lemma "(Q\nat set) (Eps Q)" -nitpick [expect = none] +nitpick [expect = none] (* unfortunate *) oops lemma "\ Q (Eps Q)" @@ -1053,11 +1053,11 @@ lemma "Q = {x\'a} \ (Q\'a set) (The Q)" nitpick [expect = none] -oops +sorry lemma "Q = {x\nat} \ (Q\nat set) (The Q)" nitpick [expect = none] -oops +sorry subsection {* Destructors and Recursors *} diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Nitpick_Examples/Datatype_Nits.thy --- a/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Datatype_Nits.thy Fri Feb 26 16:50:09 2010 +0100 @@ -69,7 +69,7 @@ oops lemma "fs (Pd ((a, b), (c, d))) = (a, b)" -nitpick [card = 1\10, expect = none] +nitpick [card = 1\9, expect = none] sorry lemma "fs (Pd ((a, b), (c, d))) = (c, d)" diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Nitpick_Examples/Mono_Nits.thy --- a/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Mono_Nits.thy Fri Feb 26 16:50:09 2010 +0100 @@ -30,8 +30,7 @@ special_funs = Unsynchronized.ref [], unrolled_preds = Unsynchronized.ref [], wf_cache = Unsynchronized.ref [], constr_cache = Unsynchronized.ref []} (* term -> bool *) -val is_mono = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} - Nitpick_Mono.Plus [] [] +fun is_mono t = Nitpick_Mono.formulas_monotonic hol_ctxt false @{typ 'a} ([t], []) fun is_const t = let val T = fastype_of t in is_mono (Logic.mk_implies (Logic.mk_equals (Free ("dummyP", T), t), @@ -47,26 +46,26 @@ ML {* const @{term "(A::'a set) = A"} *} ML {* const @{term "(A::'a set set) = A"} *} ML {* const @{term "(\x::'a set. x a)"} *} -ML {* const @{term "{{a}} = C"} *} +ML {* const @{term "{{a::'a}} = C"} *} ML {* const @{term "{f::'a\nat} = {g::'a\nat}"} *} -ML {* const @{term "A \ B"} *} +ML {* const @{term "A \ (B::'a set)"} *} ML {* const @{term "P (a::'a)"} *} ML {* const @{term "\a::'a. b (c (d::'a)) (e::'a) (f::'a)"} *} ML {* const @{term "\A::'a set. A a"} *} ML {* const @{term "\A::'a set. P A"} *} ML {* const @{term "P \ Q"} *} -ML {* const @{term "A \ B = C"} *} +ML {* const @{term "A \ B = (C::'a set)"} *} ML {* const @{term "(if P then (A::'a set) else B) = C"} *} -ML {* const @{term "let A = C in A \ B"} *} +ML {* const @{term "let A = (C::'a set) in A \ B"} *} ML {* const @{term "THE x::'b. P x"} *} -ML {* const @{term "{}::'a set"} *} +ML {* const @{term "(\x::'a. False)"} *} ML {* const @{term "(\x::'a. True)"} *} -ML {* const @{term "Let a A"} *} +ML {* const @{term "Let (a::'a) A"} *} ML {* const @{term "A (a::'a)"} *} -ML {* const @{term "insert a A = B"} *} +ML {* const @{term "insert (a::'a) A = B"} *} ML {* const @{term "- (A::'a set)"} *} -ML {* const @{term "finite A"} *} -ML {* const @{term "\ finite A"} *} +ML {* const @{term "finite (A::'a set)"} *} +ML {* const @{term "\ finite (A::'a set)"} *} ML {* const @{term "finite (A::'a set set)"} *} ML {* const @{term "\a::'a. A a \ \ B a"} *} ML {* const @{term "A < (B::'a set)"} *} @@ -75,27 +74,25 @@ ML {* const @{term "[a::'a set]"} *} ML {* const @{term "[A \ (B::'a set)]"} *} ML {* const @{term "[A \ (B::'a set)] = [C]"} *} -ML {* const @{term "\P. P a"} *} -ML {* nonconst @{term "{%x. True}"} *} -ML {* nonconst @{term "{(%x. x = a)} = C"} *} +ML {* nonconst @{term "{(\x::'a. x = a)} = C"} *} ML {* nonconst @{term "\P (a::'a). P a"} *} ML {* nonconst @{term "\a::'a. P a"} *} ML {* nonconst @{term "(\a::'a. \ A a) = B"} *} -ML {* nonconst @{term "THE x. P x"} *} -ML {* nonconst @{term "SOME x. P x"} *} +ML {* nonconst @{term "THE x::'a. P x"} *} +ML {* nonconst @{term "SOME x::'a. P x"} *} ML {* mono @{prop "Q (\x::'a set. P x)"} *} ML {* mono @{prop "P (a::'a)"} *} -ML {* mono @{prop "{a} = {b}"} *} +ML {* mono @{prop "{a} = {b::'a}"} *} ML {* mono @{prop "P (a::'a) \ P \ P = P"} *} ML {* mono @{prop "\F::'a set set. P"} *} ML {* mono @{prop "\ (\F f g (h::'a set). F f \ F g \ \ f a \ g a \ F h)"} *} ML {* mono @{prop "\ Q (\x::'a set. P x)"} *} -ML {* mono @{prop "\ (\x. P x)"} *} +ML {* mono @{prop "\ (\x::'a. P x)"} *} -ML {* nonmono @{prop "\x. P x"} *} +ML {* nonmono @{prop "\x::'a. P x"} *} +ML {* nonmono @{prop "myall P = (P = (\x::'a. True))"} *} ML {* nonmono @{prop "\F f g (h::'a set). F f \ F g \ \ f a \ g a \ F h"} *} -ML {* nonmono @{prop "myall P = (P = (\x. True))"} *} end diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Nitpick_Examples/Typedef_Nits.thy --- a/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Nitpick_Examples/Typedef_Nits.thy Fri Feb 26 16:50:09 2010 +0100 @@ -64,7 +64,7 @@ oops lemma "x \ (y\bool bounded) \ z = x \ z = y" -nitpick [expect = none] +nitpick [fast_descrs (* ### FIXME *), expect = none] sorry lemma "x \ (y\(bool \ bool) bounded) \ z = x \ z = y" diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/HISTORY --- a/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/HISTORY Fri Feb 26 16:50:09 2010 +0100 @@ -4,7 +4,11 @@ * Added "std" option and implemented support for nonstandard models * Added support for quotient types * Added support for local definitions - * Optimized "Multiset.multiset" + * Disabled "fast_descrs" option by default + * Optimized "Multiset.multiset" and "FinFun.finfun" + * Improved efficiency of "destroy_constrs" optimization + * Improved precision of infinite datatypes whose constructors don't appear + in the formula to falsify based on a monotonicity analysis * Fixed soundness bugs related to "destroy_constrs" optimization and record getters * Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 26 16:50:09 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,54 +306,66 @@ \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 + (* typ list -> string -> string *) + fun monotonicity_message Ts extra = + let val ss = map (quote o string_for_type ctxt) 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") ^ + ". " ^ extra + end (* typ -> bool *) fun is_type_always_monotonic T = (is_datatype thy stds T andalso not (is_quot_type thy T) andalso (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 (nondef_ts, def_ts) fun is_type_monotonic T = unique_scope orelse case triple_lookup (type_match thy) monos T of SOME (SOME b) => b - | _ => is_type_always_monotonic T orelse - formulas_monotonic hol_ctxt binarize T Plus def_ts nondef_ts core_t - fun is_deep_datatype T = - is_datatype thy stds T andalso - (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) + | _ => is_type_always_monotonic T orelse is_type_actually_monotonic T + fun is_type_finitizable T = + case triple_lookup (type_match thy) monos T of + SOME (SOME false) => false + | _ => is_type_actually_monotonic T + 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 (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 @@ -363,23 +374,21 @@ 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) + print_v (K (monotonicity_message interesting_mono_Ts + "Nitpick might be able to skip some scopes.")) else () - val deep_dataTs = filter is_deep_datatype all_Ts + val (deep_dataTs, shallow_dataTs) = + all_Ts |> filter (is_datatype thy stds) |> List.partition is_datatype_deep + val finitizable_dataTs = + shallow_dataTs |> filter_out (is_finite_type hol_ctxt) + |> filter is_type_finitizable + val _ = + if verbose andalso not (null finitizable_dataTs) then + print_v (K (monotonicity_message finitizable_dataTs + "Nitpick can use a more precise finite encoding.")) + else + () (* This detection code is an ugly hack. Fortunately, it is used only to provide a hint to the user. *) (* string * (Rule_Cases.T * bool) -> bool *) @@ -446,7 +455,7 @@ string_of_int j0)) (Typtab.dest ofs) *) - val all_exact = forall (is_exact_type datatypes) all_Ts + val all_exact = forall (is_exact_type datatypes true) all_Ts (* nut list -> rep NameTable.table -> nut list * rep NameTable.table *) val repify_consts = choose_reps_for_consts scope all_exact val main_j0 = offset_of_type ofs bool_T @@ -467,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) @@ -475,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 @@ -483,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 = @@ -537,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 @@ -834,8 +839,8 @@ sound_problems then print_m (fn () => "Warning: The conjecture either trivially holds for the \ - \given scopes or (more likely) lies outside Nitpick's \ - \supported fragment." ^ + \given scopes or lies outside Nitpick's supported \ + \fragment." ^ (if exists (not o KK.is_problem_trivially_false o fst) unsound_problems then " Only potential counterexamples may be found." @@ -907,6 +912,7 @@ val (skipped, the_scopes) = all_scopes hol_ctxt binarize sym_break cards_assigns maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts deep_dataTs + finitizable_dataTs val _ = if skipped > 0 then print_m (fn () => "Too many scopes. Skipping " ^ string_of_int skipped ^ " scope" ^ diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 26 16:50:09 2010 +0100 @@ -151,9 +151,10 @@ val card_of_type : (typ * int) list -> typ -> int val bounded_card_of_type : int -> int -> (typ * int) list -> typ -> int val bounded_exact_card_of_type : - hol_context -> int -> int -> (typ * int) list -> typ -> int + hol_context -> typ list -> int -> int -> (typ * int) list -> typ -> int val is_finite_type : hol_context -> typ -> bool val special_bounds : term list -> (indexname * typ) list + val abs_var : indexname * typ -> term -> term val is_funky_typedef : theory -> typ -> bool val all_axioms_of : theory -> (term * term) list -> term list * term list * term list @@ -631,8 +632,13 @@ in case t_opt of SOME (Const (@{const_name top}, _)) => true + (* "Multiset.multiset" *) | SOME (Const (@{const_name Collect}, _) $ Abs (_, _, Const (@{const_name finite}, _) $ _)) => true + (* "FinFun.finfun" *) + | SOME (Const (@{const_name Collect}, _) $ Abs (_, _, + Const (@{const_name Ex}, _) $ Abs (_, _, + Const (@{const_name finite}, _) $ _))) => true | _ => false end | NONE => false) @@ -1047,13 +1053,16 @@ card_of_type assigns T handle TYPE ("Nitpick_HOL.card_of_type", _, _) => default_card) -(* hol_context -> int -> (typ * int) list -> typ -> int *) -fun bounded_exact_card_of_type hol_ctxt max default_card assigns T = +(* hol_context -> typ list -> int -> (typ * int) list -> typ -> int *) +fun bounded_exact_card_of_type hol_ctxt finitizable_dataTs max default_card + assigns T = let (* typ list -> typ -> int *) fun aux avoid T = (if member (op =) avoid T then 0 + else if member (op =) finitizable_dataTs T then + raise SAME () else case T of Type ("fun", [T1, T2]) => let @@ -1096,8 +1105,8 @@ in Int.min (max, aux [] T) end (* hol_context -> typ -> bool *) -fun is_finite_type hol_ctxt = - not_equal 0 o bounded_exact_card_of_type hol_ctxt 1 2 [] +fun is_finite_type hol_ctxt T = + bounded_exact_card_of_type hol_ctxt [] 1 2 [] T <> 0 (* term -> bool *) fun is_ground_term (t1 $ t2) = is_ground_term t1 andalso is_ground_term t2 diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 26 16:50:09 2010 +0100 @@ -255,10 +255,10 @@ ("int_divide", tabulate_int_op2 debug univ_card (int_card, j0) isa_div) else if x = nat_less_rel then ("nat_less", tabulate_nat_op2 debug univ_card (nat_card, j0) - (int_for_bool o op <)) + (int_from_bool o op <)) else if x = int_less_rel then ("int_less", tabulate_int_op2 debug univ_card (int_card, j0) - (int_for_bool o op <)) + (int_from_bool o op <)) else if x = gcd_rel then ("gcd", tabulate_nat_op2 debug univ_card (nat_card, j0) isa_gcd) else if x = lcm_rel then @@ -444,7 +444,7 @@ single_rel_rel_let kk (fn r1 => basic_rel_rel_let 1 kk (f r1) r2) r1 (* kodkod_constrs -> (KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr) -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr -> KK.rel_expr *) -fun tripl_rel_rel_let kk f r1 r2 r3 = +fun triple_rel_rel_let kk f r1 r2 r3 = double_rel_rel_let kk (fn r1 => fn r2 => basic_rel_rel_let 2 kk (f r1 r2) r3) r1 r2 @@ -1615,7 +1615,7 @@ kk_rel_let [to_expr_assign u1 u2] (to_rep R u3) | Op3 (If, _, R, u1, u2, u3) => if is_opt_rep (rep_of u1) then - tripl_rel_rel_let kk + triple_rel_rel_let kk (fn r1 => fn r2 => fn r3 => let val empty_r = empty_rel_for_rep R in fold1 kk_union diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 26 16:50:09 2010 +0100 @@ -288,7 +288,7 @@ T1 --> (T1 --> T2) --> T1 --> T2) (* (term * term) list -> term *) fun aux [] = - if maybe_opt andalso not (is_complete_type datatypes T1) then + if maybe_opt andalso not (is_complete_type datatypes false T1) then insert_const $ Const (unrep, T1) $ empty_const else empty_const @@ -312,7 +312,7 @@ Const (@{const_name None}, _) => aux' ps | _ => update_const $ aux' ps $ t1 $ t2) fun aux ps = - if not (is_complete_type datatypes T1) then + if not (is_complete_type datatypes false T1) then update_const $ aux' ps $ Const (unrep, T1) $ (Const (@{const_name Some}, T2' --> T2) $ Const (unknown, T2')) else @@ -537,7 +537,7 @@ val ts1 = map (term_for_rep seen T1 T1 R1 o single) jss1 val ts2 = map (fn js => term_for_rep seen T2 T2 (Atom (2, 0)) - [[int_for_bool (member (op =) jss js)]]) + [[int_from_bool (member (op =) jss js)]]) jss1 in make_fun false T1 T2 T' ts1 ts2 end | term_for_rep seen (Type ("fun", [T1, T2])) T' (Func (R1, R2)) jss = @@ -707,12 +707,13 @@ Pretty.str "=", Pretty.enum "," "{" "}" (map (Syntax.pretty_term ctxt) (all_values_of_type card typ) @ - (if complete then [] else [Pretty.str unrep]))]) + (if fun_from_pair complete false then [] + else [Pretty.str unrep]))]) (* typ -> dtype_spec list *) fun integer_datatype T = [{typ = T, card = card_of_type card_assigns T, co = false, - standard = true, complete = false, concrete = true, deep = true, - constrs = []}] + standard = true, complete = (false, false), concrete = (true, true), + deep = true, constrs = []}] handle TYPE ("Nitpick_HOL.card_of_type", _, _) => [] val (codatatypes, datatypes) = datatypes |> filter #deep |> List.partition #co diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_mono.ML --- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Fri Feb 26 16:50:09 2010 +0100 @@ -2,16 +2,15 @@ Author: Jasmin Blanchette, TU Muenchen Copyright 2009, 2010 -Monotonicity predicate for higher-order logic. +Monotonicity inference for higher-order logic. *) signature NITPICK_MONO = sig - datatype sign = Plus | Minus type hol_context = Nitpick_HOL.hol_context val formulas_monotonic : - hol_context -> bool -> typ -> sign -> term list -> term list -> term -> bool + hol_context -> bool -> typ -> term list * term list -> bool end; structure Nitpick_Mono : NITPICK_MONO = @@ -27,22 +26,27 @@ type literal = var * sign -datatype ctype = - CAlpha | - CFun of ctype * sign_atom * ctype | - CPair of ctype * ctype | - CType of string * ctype list | - CRec of string * typ list +datatype mtyp = + MAlpha | + MFun of mtyp * sign_atom * mtyp | + MPair of mtyp * mtyp | + MType of string * mtyp list | + MRec of string * typ list -type cdata = +datatype mterm = + MRaw of term * mtyp | + MAbs of string * typ * mtyp * sign_atom * mterm | + MApp of mterm * mterm + +type mdata = {hol_ctxt: hol_context, binarize: bool, alpha_T: typ, max_fresh: int Unsynchronized.ref, - datatype_cache: ((string * typ list) * ctype) list Unsynchronized.ref, - constr_cache: (styp * ctype) list Unsynchronized.ref} + datatype_cache: ((string * typ list) * mtyp) list Unsynchronized.ref, + constr_cache: (styp * mtyp) list Unsynchronized.ref} -exception CTYPE of string * ctype list +exception MTYPE of string * mtyp list (* string -> unit *) fun print_g (_ : string) = () @@ -71,55 +75,95 @@ (* literal -> string *) fun string_for_literal (x, sn) = string_for_var x ^ " = " ^ string_for_sign sn -val bool_C = CType (@{type_name bool}, []) +val bool_M = MType (@{type_name bool}, []) +val dummy_M = MType (nitpick_prefix ^ "dummy", []) -(* ctype -> bool *) -fun is_CRec (CRec _) = true - | is_CRec _ = false +(* mtyp -> bool *) +fun is_MRec (MRec _) = true + | is_MRec _ = false +(* mtyp -> mtyp * sign_atom * mtyp *) +fun dest_MFun (MFun z) = z + | dest_MFun M = raise MTYPE ("Nitpick_Mono.dest_MFun", [M]) val no_prec = 100 -val prec_CFun = 1 -val prec_CPair = 2 -(* tuple_set -> int *) -fun precedence_of_ctype (CFun _) = prec_CFun - | precedence_of_ctype (CPair _) = prec_CPair - | precedence_of_ctype _ = no_prec +(* mtyp -> int *) +fun precedence_of_mtype (MFun _) = 1 + | precedence_of_mtype (MPair _) = 2 + | precedence_of_mtype _ = no_prec -(* ctype -> string *) -val string_for_ctype = +(* mtyp -> string *) +val string_for_mtype = let - (* int -> ctype -> string *) - fun aux outer_prec C = + (* int -> mtyp -> string *) + fun aux outer_prec M = let - val prec = precedence_of_ctype C + val prec = precedence_of_mtype M val need_parens = (prec < outer_prec) in (if need_parens then "(" else "") ^ - (case C of - CAlpha => "\" - | CFun (C1, a, C2) => - aux (prec + 1) C1 ^ " \\<^bsup>" ^ - string_for_sign_atom a ^ "\<^esup> " ^ aux prec C2 - | CPair (C1, C2) => aux (prec + 1) C1 ^ " \ " ^ aux prec C2 - | CType (s, []) => - if s = @{type_name prop} orelse s = @{type_name bool} then "o" else s - | CType (s, Cs) => "(" ^ commas (map (aux 0) Cs) ^ ") " ^ s - | CRec (s, _) => "[" ^ s ^ "]") ^ + (if M = dummy_M then + "_" + else case M of + MAlpha => "\" + | MFun (M1, a, M2) => + aux (prec + 1) M1 ^ " \\<^bsup>" ^ + string_for_sign_atom a ^ "\<^esup> " ^ aux prec M2 + | MPair (M1, M2) => aux (prec + 1) M1 ^ " \ " ^ 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 -(* ctype -> ctype list *) -fun flatten_ctype (CPair (C1, C2)) = maps flatten_ctype [C1, C2] - | flatten_ctype (CType (_, Cs)) = maps flatten_ctype Cs - | flatten_ctype C = [C] +(* mtyp -> mtyp list *) +fun flatten_mtype (MPair (M1, M2)) = maps flatten_mtype [M1, M2] + | flatten_mtype (MType (_, Ms)) = maps flatten_mtype Ms + | flatten_mtype M = [M] + +(* mterm -> bool *) +fun precedence_of_mterm (MRaw _) = no_prec + | precedence_of_mterm (MAbs _) = 1 + | precedence_of_mterm (MApp _) = 2 -(* hol_context -> bool -> typ -> cdata *) -fun initial_cdata hol_ctxt binarize alpha_T = +(* Proof.context -> mterm -> string *) +fun string_for_mterm ctxt = + let + (* mtype -> string *) + fun mtype_annotation M = "\<^bsup>" ^ string_for_mtype M ^ "\<^esup>" + (* int -> mterm -> string *) + fun aux outer_prec m = + let + val prec = precedence_of_mterm m + val need_parens = (prec < outer_prec) + in + (if need_parens then "(" else "") ^ + (case m of + MRaw (t, M) => Syntax.string_of_term ctxt t ^ mtype_annotation M + | MAbs (s, _, M, a, m) => + "\" ^ s ^ mtype_annotation M ^ ".\<^bsup>" ^ + string_for_sign_atom a ^ "\<^esup> " ^ aux prec m + | MApp (m1, m2) => aux prec m1 ^ " " ^ aux (prec + 1) m2) ^ + (if need_parens then ")" else "") + end + in aux 0 end + +(* mterm -> mtyp *) +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 + MFun (_, _, M12) => M12 + | M1 => raise MTYPE ("Nitpick_Mono.mtype_of_mterm", [M1]) + +(* hol_context -> bool -> typ -> mdata *) +fun initial_mdata hol_ctxt binarize alpha_T = ({hol_ctxt = hol_ctxt, binarize = binarize, alpha_T = alpha_T, max_fresh = Unsynchronized.ref 0, datatype_cache = Unsynchronized.ref [], - constr_cache = Unsynchronized.ref []} : cdata) + constr_cache = Unsynchronized.ref []} : mdata) (* typ -> typ -> bool *) fun could_exist_alpha_subtype alpha_T (T as Type (_, Ts)) = @@ -127,172 +171,179 @@ 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 = +fun could_exist_alpha_sub_mtype _ (alpha_T as TFree _) T = could_exist_alpha_subtype alpha_T T - | could_exist_alpha_sub_ctype thy alpha_T T = + | could_exist_alpha_sub_mtype thy alpha_T T = (T = alpha_T orelse is_datatype thy [(NONE, true)] T) -(* ctype -> bool *) -fun exists_alpha_sub_ctype CAlpha = true - | exists_alpha_sub_ctype (CFun (C1, _, C2)) = - exists exists_alpha_sub_ctype [C1, C2] - | exists_alpha_sub_ctype (CPair (C1, C2)) = - exists exists_alpha_sub_ctype [C1, C2] - | exists_alpha_sub_ctype (CType (_, Cs)) = exists exists_alpha_sub_ctype Cs - | exists_alpha_sub_ctype (CRec _) = true +(* mtyp -> bool *) +fun exists_alpha_sub_mtype MAlpha = true + | exists_alpha_sub_mtype (MFun (M1, _, M2)) = + exists exists_alpha_sub_mtype [M1, M2] + | exists_alpha_sub_mtype (MPair (M1, M2)) = + exists exists_alpha_sub_mtype [M1, M2] + | exists_alpha_sub_mtype (MType (_, Ms)) = exists exists_alpha_sub_mtype Ms + | exists_alpha_sub_mtype (MRec _) = true -(* ctype -> bool *) -fun exists_alpha_sub_ctype_fresh CAlpha = true - | exists_alpha_sub_ctype_fresh (CFun (_, V _, _)) = true - | exists_alpha_sub_ctype_fresh (CFun (_, _, C2)) = - exists_alpha_sub_ctype_fresh C2 - | exists_alpha_sub_ctype_fresh (CPair (C1, C2)) = - exists exists_alpha_sub_ctype_fresh [C1, C2] - | exists_alpha_sub_ctype_fresh (CType (_, Cs)) = - exists exists_alpha_sub_ctype_fresh Cs - | exists_alpha_sub_ctype_fresh (CRec _) = true +(* mtyp -> bool *) +fun exists_alpha_sub_mtype_fresh MAlpha = true + | exists_alpha_sub_mtype_fresh (MFun (_, V _, _)) = true + | exists_alpha_sub_mtype_fresh (MFun (_, _, M2)) = + exists_alpha_sub_mtype_fresh M2 + | exists_alpha_sub_mtype_fresh (MPair (M1, M2)) = + exists exists_alpha_sub_mtype_fresh [M1, M2] + | exists_alpha_sub_mtype_fresh (MType (_, Ms)) = + exists exists_alpha_sub_mtype_fresh Ms + | exists_alpha_sub_mtype_fresh (MRec _) = true -(* string * typ list -> ctype list -> ctype *) -fun constr_ctype_for_binders z Cs = - fold_rev (fn C => curry3 CFun C (S Minus)) Cs (CRec z) +(* string * typ list -> mtyp list -> mtyp *) +fun constr_mtype_for_binders z Ms = + fold_rev (fn M => curry3 MFun M (S Minus)) Ms (MRec z) -(* ((string * typ list) * ctype) list -> ctype list -> ctype -> ctype *) -fun repair_ctype _ _ CAlpha = CAlpha - | repair_ctype cache seen (CFun (C1, a, C2)) = - CFun (repair_ctype cache seen C1, a, repair_ctype cache seen C2) - | repair_ctype cache seen (CPair Cp) = - CPair (pairself (repair_ctype cache seen) Cp) - | repair_ctype cache seen (CType (s, Cs)) = - CType (s, maps (flatten_ctype o repair_ctype cache seen) Cs) - | repair_ctype cache seen (CRec (z as (s, _))) = +(* ((string * typ list) * mtyp) list -> mtyp list -> mtyp -> mtyp *) +fun repair_mtype _ _ MAlpha = MAlpha + | repair_mtype cache seen (MFun (M1, a, M2)) = + MFun (repair_mtype cache seen M1, a, repair_mtype cache seen M2) + | repair_mtype cache seen (MPair Mp) = + MPair (pairself (repair_mtype cache seen) Mp) + | repair_mtype cache seen (MType (s, Ms)) = + MType (s, maps (flatten_mtype o repair_mtype cache seen) Ms) + | repair_mtype cache seen (MRec (z as (s, _))) = case AList.lookup (op =) cache z |> the of - CRec _ => CType (s, []) - | C => if member (op =) seen C then CType (s, []) - else repair_ctype cache (C :: seen) C + MRec _ => MType (s, []) + | M => if member (op =) seen M then MType (s, []) + else repair_mtype cache (M :: seen) M -(* ((string * typ list) * ctype) list Unsynchronized.ref -> unit *) +(* ((string * typ list) * mtyp) list Unsynchronized.ref -> unit *) fun repair_datatype_cache cache = let - (* (string * typ list) * ctype -> unit *) - fun repair_one (z, C) = + (* (string * typ list) * mtyp -> unit *) + fun repair_one (z, M) = Unsynchronized.change cache - (AList.update (op =) (z, repair_ctype (!cache) [] C)) + (AList.update (op =) (z, repair_mtype (!cache) [] M)) in List.app repair_one (rev (!cache)) end -(* (typ * ctype) list -> (styp * ctype) list Unsynchronized.ref -> unit *) +(* (typ * mtyp) list -> (styp * mtyp) list Unsynchronized.ref -> unit *) fun repair_constr_cache dtype_cache constr_cache = let - (* styp * ctype -> unit *) - fun repair_one (x, C) = + (* styp * mtyp -> unit *) + fun repair_one (x, M) = Unsynchronized.change constr_cache - (AList.update (op =) (x, repair_ctype dtype_cache [] C)) + (AList.update (op =) (x, repair_mtype dtype_cache [] M)) in List.app repair_one (!constr_cache) end -(* cdata -> typ -> ctype *) -fun fresh_ctype_for_type ({hol_ctxt as {thy, ...}, binarize, alpha_T, max_fresh, - datatype_cache, constr_cache, ...} : cdata) = +(* mdata -> typ -> typ -> mtyp * sign_atom * mtyp *) +fun fresh_mfun_for_fun_type (mdata as {max_fresh, ...} : mdata) T1 T2 = let - (* typ -> typ -> ctype *) - fun do_fun T1 T2 = - 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 - V (Unsynchronized.inc max_fresh) - else - S Minus - in CFun (C1, a, C2) end - (* typ -> ctype *) - and do_type T = + val M1 = fresh_mtype_for_type mdata T1 + val M2 = fresh_mtype_for_type mdata T2 + val a = if is_boolean_type (body_type T2) andalso + exists_alpha_sub_mtype_fresh M1 then + V (Unsynchronized.inc max_fresh) + else + S Minus + in (M1, a, M2) end +(* mdata -> typ -> mtyp *) +and fresh_mtype_for_type (mdata as {hol_ctxt as {thy, ...}, binarize, alpha_T, + datatype_cache, constr_cache, ...}) = + let + (* typ -> typ -> mtyp *) + val do_fun = MFun oo fresh_mfun_for_fun_type mdata + (* typ -> mtyp *) + fun do_type T = if T = alpha_T then - CAlpha + MAlpha else case T of Type ("fun", [T1, T2]) => do_fun T1 T2 | Type (@{type_name fun_box}, [T1, T2]) => do_fun T1 T2 - | Type ("*", [T1, T2]) => CPair (pairself do_type (T1, T2)) + | Type ("*", [T1, T2]) => MPair (pairself do_type (T1, T2)) | Type (z as (s, _)) => - if could_exist_alpha_sub_ctype thy alpha_T T then + if could_exist_alpha_sub_mtype thy alpha_T T then case AList.lookup (op =) (!datatype_cache) z of - SOME C => C + SOME M => M | NONE => let - val _ = Unsynchronized.change datatype_cache (cons (z, CRec z)) + val _ = Unsynchronized.change datatype_cache (cons (z, MRec z)) val xs = binarized_and_boxed_datatype_constrs hol_ctxt binarize T - val (all_Cs, constr_Cs) = - fold_rev (fn (_, T') => fn (all_Cs, constr_Cs) => + val (all_Ms, constr_Ms) = + fold_rev (fn (_, T') => fn (all_Ms, constr_Ms) => let - val binder_Cs = map do_type (binder_types T') - val new_Cs = filter exists_alpha_sub_ctype_fresh - binder_Cs - val constr_C = constr_ctype_for_binders z - binder_Cs + val binder_Ms = map do_type (binder_types T') + val new_Ms = filter exists_alpha_sub_mtype_fresh + binder_Ms + val constr_M = constr_mtype_for_binders z + binder_Ms in - (union (op =) new_Cs all_Cs, - constr_C :: constr_Cs) + (union (op =) new_Ms all_Ms, + constr_M :: constr_Ms) end) xs ([], []) - val C = CType (s, all_Cs) + val M = MType (s, all_Ms) val _ = Unsynchronized.change datatype_cache - (AList.update (op =) (z, C)) + (AList.update (op =) (z, M)) val _ = Unsynchronized.change constr_cache - (append (xs ~~ constr_Cs)) + (append (xs ~~ constr_Ms)) in - if forall (not o is_CRec o snd) (!datatype_cache) then + if forall (not o is_MRec o snd) (!datatype_cache) then (repair_datatype_cache datatype_cache; repair_constr_cache (!datatype_cache) constr_cache; AList.lookup (op =) (!datatype_cache) z |> the) else - C + M end else - CType (s, []) - | _ => CType (Refute.string_of_typ T, []) + MType (s, []) + | _ => MType (Refute.string_of_typ T, []) in do_type end -(* ctype -> ctype list *) -fun prodC_factors (CPair (C1, C2)) = maps prodC_factors [C1, C2] - | prodC_factors C = [C] -(* ctype -> ctype list * ctype *) -fun curried_strip_ctype (CFun (C1, S Minus, C2)) = - curried_strip_ctype C2 |>> append (prodC_factors C1) - | curried_strip_ctype C = ([], C) -(* string -> ctype -> ctype *) -fun sel_ctype_from_constr_ctype s C = - let val (arg_Cs, dataC) = curried_strip_ctype C in - CFun (dataC, S Minus, - case sel_no_from_name s of ~1 => bool_C | n => nth arg_Cs n) +(* mtyp -> mtyp list *) +fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2] + | prodM_factors M = [M] +(* mtyp -> mtyp list * mtyp *) +fun curried_strip_mtype (MFun (M1, S Minus, M2)) = + curried_strip_mtype M2 |>> append (prodM_factors M1) + | curried_strip_mtype M = ([], M) +(* string -> mtyp -> mtyp *) +fun sel_mtype_from_constr_mtype s M = + let val (arg_Ms, dataM) = curried_strip_mtype M in + MFun (dataM, S Minus, + case sel_no_from_name s of ~1 => bool_M | n => nth arg_Ms n) end -(* cdata -> styp -> ctype *) -fun ctype_for_constr (cdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, +(* mdata -> styp -> mtyp *) +fun mtype_for_constr (mdata as {hol_ctxt = {thy, ...}, alpha_T, constr_cache, ...}) (x as (_, T)) = - if could_exist_alpha_sub_ctype thy alpha_T T then + if could_exist_alpha_sub_mtype thy alpha_T T then case AList.lookup (op =) (!constr_cache) x of - SOME C => C - | NONE => (fresh_ctype_for_type cdata (body_type T); - AList.lookup (op =) (!constr_cache) x |> the) + SOME M => M + | NONE => if T = alpha_T then + let val M = fresh_mtype_for_type mdata T in + (Unsynchronized.change constr_cache (cons (x, M)); M) + end + else + (fresh_mtype_for_type mdata (body_type T); + AList.lookup (op =) (!constr_cache) x |> the) else - fresh_ctype_for_type cdata T -fun ctype_for_sel (cdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = + fresh_mtype_for_type mdata T +fun mtype_for_sel (mdata as {hol_ctxt, binarize, ...}) (x as (s, _)) = x |> binarized_and_boxed_constr_for_sel hol_ctxt binarize - |> ctype_for_constr cdata |> sel_ctype_from_constr_ctype s + |> mtype_for_constr mdata |> sel_mtype_from_constr_mtype s -(* literal list -> ctype -> ctype *) -fun instantiate_ctype lits = +(* literal list -> mtyp -> mtyp *) +fun instantiate_mtype lits = let - (* ctype -> ctype *) - fun aux CAlpha = CAlpha - | aux (CFun (C1, V x, C2)) = + (* mtyp -> mtyp *) + fun aux MAlpha = MAlpha + | aux (MFun (M1, V x, M2)) = let val a = case AList.lookup (op =) lits x of SOME sn => S sn | NONE => V x - in CFun (aux C1, a, aux C2) end - | aux (CFun (C1, a, C2)) = CFun (aux C1, a, aux C2) - | aux (CPair Cp) = CPair (pairself aux Cp) - | aux (CType (s, Cs)) = CType (s, map aux Cs) - | aux (CRec z) = CRec z + in MFun (aux M1, a, aux M2) end + | aux (MFun (M1, a, M2)) = MFun (aux M1, a, aux M2) + | aux (MPair Mp) = MPair (pairself aux Mp) + | aux (MType (s, Ms)) = MType (s, map aux Ms) + | aux (MRec z) = MRec z in aux end datatype comp_op = Eq | Leq @@ -342,105 +393,106 @@ | do_sign_atom_comp cmp xs a1 a2 (lits, comps) = SOME (lits, insert (op =) (a1, a2, cmp, xs) comps) -(* comp -> var list -> ctype -> ctype -> (literal list * comp list) option +(* comp -> var list -> mtyp -> mtyp -> (literal list * comp list) option -> (literal list * comp list) option *) -fun do_ctype_comp _ _ _ _ NONE = NONE - | do_ctype_comp _ _ CAlpha CAlpha accum = accum - | do_ctype_comp Eq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) +fun do_mtype_comp _ _ _ _ NONE = NONE + | do_mtype_comp _ _ MAlpha MAlpha accum = accum + | do_mtype_comp Eq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) (SOME accum) = - accum |> do_sign_atom_comp Eq xs a1 a2 |> do_ctype_comp Eq xs C11 C21 - |> do_ctype_comp Eq xs C12 C22 - | do_ctype_comp Leq xs (CFun (C11, a1, C12)) (CFun (C21, a2, C22)) + accum |> do_sign_atom_comp Eq xs a1 a2 |> do_mtype_comp Eq xs M11 M21 + |> do_mtype_comp Eq xs M12 M22 + | do_mtype_comp Leq xs (MFun (M11, a1, M12)) (MFun (M21, a2, M22)) (SOME accum) = - (if exists_alpha_sub_ctype C11 then + (if exists_alpha_sub_mtype M11 then accum |> do_sign_atom_comp Leq xs a1 a2 - |> do_ctype_comp Leq xs C21 C11 + |> do_mtype_comp Leq xs M21 M11 |> (case a2 of S Minus => I - | S Plus => do_ctype_comp Leq xs C11 C21 - | V x => do_ctype_comp Leq (x :: xs) C11 C21) + | S Plus => do_mtype_comp Leq xs M11 M21 + | V x => do_mtype_comp Leq (x :: xs) M11 M21) else SOME accum) - |> do_ctype_comp Leq xs C12 C22 - | do_ctype_comp cmp xs (C1 as CPair (C11, C12)) (C2 as CPair (C21, C22)) + |> do_mtype_comp Leq xs M12 M22 + | do_mtype_comp cmp xs (M1 as MPair (M11, M12)) (M2 as MPair (M21, M22)) accum = - (accum |> fold (uncurry (do_ctype_comp cmp xs)) [(C11, C21), (C12, C22)] + (accum |> fold (uncurry (do_mtype_comp cmp xs)) [(M11, M21), (M12, M22)] handle Library.UnequalLengths => - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2])) - | do_ctype_comp _ _ (CType _) (CType _) accum = + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2])) + | do_mtype_comp _ _ (MType _) (MType _) accum = accum (* no need to compare them thanks to the cache *) - | do_ctype_comp _ _ C1 C2 _ = - raise CTYPE ("Nitpick_Mono.do_ctype_comp", [C1, C2]) + | do_mtype_comp _ _ M1 M2 _ = + raise MTYPE ("Nitpick_Mono.do_mtype_comp", [M1, M2]) -(* comp_op -> ctype -> ctype -> constraint_set -> constraint_set *) -fun add_ctype_comp _ _ _ UnsolvableCSet = UnsolvableCSet - | add_ctype_comp cmp C1 C2 (CSet (lits, comps, sexps)) = - (print_g ("*** Add " ^ string_for_ctype C1 ^ " " ^ string_for_comp_op cmp ^ - " " ^ string_for_ctype C2); - case do_ctype_comp cmp [] C1 C2 (SOME (lits, comps)) of +(* comp_op -> mtyp -> mtyp -> constraint_set -> constraint_set *) +fun add_mtype_comp _ _ _ UnsolvableCSet = UnsolvableCSet + | add_mtype_comp cmp M1 M2 (CSet (lits, comps, sexps)) = + (print_g ("*** Add " ^ string_for_mtype M1 ^ " " ^ string_for_comp_op cmp ^ + " " ^ string_for_mtype M2); + case do_mtype_comp cmp [] M1 M2 (SOME (lits, comps)) of NONE => (print_g "**** Unsolvable"; UnsolvableCSet) | SOME (lits, comps) => CSet (lits, comps, sexps)) -(* ctype -> ctype -> constraint_set -> constraint_set *) -val add_ctypes_equal = add_ctype_comp Eq -val add_is_sub_ctype = add_ctype_comp Leq +(* mtyp -> mtyp -> constraint_set -> constraint_set *) +val add_mtypes_equal = add_mtype_comp Eq +val add_is_sub_mtype = add_mtype_comp Leq -(* sign -> sign_expr -> ctype -> (literal list * sign_expr list) option +(* sign -> sign_expr -> mtyp -> (literal list * sign_expr list) option -> (literal list * sign_expr list) option *) -fun do_notin_ctype_fv _ _ _ NONE = NONE - | do_notin_ctype_fv Minus _ CAlpha accum = accum - | do_notin_ctype_fv Plus [] CAlpha _ = NONE - | do_notin_ctype_fv Plus [(x, sn)] CAlpha (SOME (lits, sexps)) = +fun do_notin_mtype_fv _ _ _ NONE = NONE + | do_notin_mtype_fv Minus _ MAlpha accum = accum + | do_notin_mtype_fv Plus [] MAlpha _ = NONE + | do_notin_mtype_fv Plus [(x, sn)] MAlpha (SOME (lits, sexps)) = SOME lits |> do_literal (x, sn) |> Option.map (rpair sexps) - | do_notin_ctype_fv Plus sexp CAlpha (SOME (lits, sexps)) = + | do_notin_mtype_fv Plus sexp MAlpha (SOME (lits, sexps)) = SOME (lits, insert (op =) sexp sexps) - | do_notin_ctype_fv sn sexp (CFun (C1, S sn', C2)) accum = + | do_notin_mtype_fv sn sexp (MFun (M1, S sn', M2)) accum = accum |> (if sn' = Plus andalso sn = Plus then - do_notin_ctype_fv Plus sexp C1 + do_notin_mtype_fv Plus sexp M1 else I) |> (if sn' = Minus orelse sn = Plus then - do_notin_ctype_fv Minus sexp C1 + do_notin_mtype_fv Minus sexp M1 else I) - |> do_notin_ctype_fv sn sexp C2 - | do_notin_ctype_fv Plus sexp (CFun (C1, V x, C2)) accum = + |> do_notin_mtype_fv sn sexp M2 + | do_notin_mtype_fv Plus sexp (MFun (M1, V x, M2)) accum = accum |> (case do_literal (x, Minus) (SOME sexp) of NONE => I - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1) - |> do_notin_ctype_fv Minus sexp C1 - |> do_notin_ctype_fv Plus sexp C2 - | do_notin_ctype_fv Minus sexp (CFun (C1, V x, C2)) accum = + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1) + |> do_notin_mtype_fv Minus sexp M1 + |> do_notin_mtype_fv Plus sexp M2 + | do_notin_mtype_fv Minus sexp (MFun (M1, V x, M2)) accum = accum |> (case do_literal (x, Plus) (SOME sexp) of NONE => I - | SOME sexp' => do_notin_ctype_fv Plus sexp' C1) - |> do_notin_ctype_fv Minus sexp C2 - | do_notin_ctype_fv sn sexp (CPair (C1, C2)) accum = - accum |> fold (do_notin_ctype_fv sn sexp) [C1, C2] - | do_notin_ctype_fv sn sexp (CType (_, Cs)) accum = - accum |> fold (do_notin_ctype_fv sn sexp) Cs - | do_notin_ctype_fv _ _ C _ = - raise CTYPE ("Nitpick_Mono.do_notin_ctype_fv", [C]) + | SOME sexp' => do_notin_mtype_fv Plus sexp' M1) + |> do_notin_mtype_fv Minus sexp M2 + | do_notin_mtype_fv sn sexp (MPair (M1, M2)) accum = + accum |> fold (do_notin_mtype_fv sn sexp) [M1, M2] + | do_notin_mtype_fv sn sexp (MType (_, Ms)) accum = + accum |> fold (do_notin_mtype_fv sn sexp) Ms + | do_notin_mtype_fv _ _ M _ = + raise MTYPE ("Nitpick_Mono.do_notin_mtype_fv", [M]) -(* sign -> ctype -> constraint_set -> constraint_set *) -fun add_notin_ctype_fv _ _ UnsolvableCSet = UnsolvableCSet - | add_notin_ctype_fv sn C (CSet (lits, comps, sexps)) = - (print_g ("*** Add " ^ string_for_ctype C ^ " is right-" ^ +(* sign -> mtyp -> constraint_set -> constraint_set *) +fun add_notin_mtype_fv _ _ UnsolvableCSet = UnsolvableCSet + | add_notin_mtype_fv sn M (CSet (lits, comps, sexps)) = + (print_g ("*** Add " ^ string_for_mtype M ^ " is right-" ^ (case sn of Minus => "unique" | Plus => "total") ^ "."); - case do_notin_ctype_fv sn [] C (SOME (lits, sexps)) of + case do_notin_mtype_fv sn [] M (SOME (lits, sexps)) of NONE => (print_g "**** Unsolvable"; UnsolvableCSet) | SOME (lits, sexps) => CSet (lits, comps, sexps)) -(* ctype -> constraint_set -> constraint_set *) -val add_ctype_is_right_unique = add_notin_ctype_fv Minus -val add_ctype_is_right_total = add_notin_ctype_fv Plus +(* mtyp -> constraint_set -> constraint_set *) +val add_mtype_is_right_unique = add_notin_mtype_fv Minus +val add_mtype_is_right_total = add_notin_mtype_fv Plus + +val bool_from_minus = true (* sign -> bool *) -fun bool_from_sign Plus = false - | bool_from_sign Minus = true +fun bool_from_sign Plus = not bool_from_minus + | bool_from_sign Minus = bool_from_minus (* bool -> sign *) -fun sign_from_bool false = Plus - | sign_from_bool true = Minus +fun sign_from_bool b = if b = bool_from_minus then Minus else Plus (* literal -> PropLogic.prop_formula *) fun prop_for_literal (x, sn) = @@ -492,228 +544,264 @@ "-: " ^ commas (map (string_for_var o fst) neg)) end -(* var -> constraint_set -> literal list list option *) +(* var -> constraint_set -> literal list option *) 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 ctype_schema = ctype * constraint_set -type ctype_context = - {bounds: ctype list, - frees: (styp * ctype) list, - consts: (styp * ctype) list} +type mtype_schema = mtyp * constraint_set +type mtype_context = + {bounds: mtyp list, + frees: (styp * mtyp) list, + consts: (styp * mtyp) list} -type accumulator = ctype_context * constraint_set +type accumulator = mtype_context * constraint_set val initial_gamma = {bounds = [], frees = [], consts = []} val unsolvable_accum = (initial_gamma, UnsolvableCSet) -(* ctype -> ctype_context -> ctype_context *) -fun push_bound C {bounds, frees, consts} = - {bounds = C :: bounds, frees = frees, consts = consts} -(* ctype_context -> ctype_context *) +(* mtyp -> mtype_context -> mtype_context *) +fun push_bound M {bounds, frees, consts} = + {bounds = M :: bounds, frees = frees, consts = consts} +(* mtype_context -> mtype_context *) fun pop_bound {bounds, frees, consts} = {bounds = tl bounds, frees = frees, consts = consts} handle List.Empty => initial_gamma -(* cdata -> term -> accumulator -> ctype * accumulator *) -fun consider_term (cdata as {hol_ctxt = {thy, ctxt, stds, fast_descrs, +(* mdata -> term -> accumulator -> mterm * accumulator *) +fun consider_term (mdata as {hol_ctxt as {thy, ctxt, stds, fast_descrs, def_table, ...}, alpha_T, max_fresh, ...}) = let - (* typ -> ctype *) - val ctype_for = fresh_ctype_for_type cdata - (* ctype -> ctype *) - fun pos_set_ctype_for_dom C = - CFun (C, S (if exists_alpha_sub_ctype C then Plus else Minus), bool_C) - (* typ -> accumulator -> ctype * accumulator *) - fun do_quantifier T (gamma, cset) = + (* typ -> typ -> mtyp * sign_atom * mtyp *) + val mfun_for = fresh_mfun_for_fun_type mdata + (* typ -> mtyp *) + val mtype_for = fresh_mtype_for_type mdata + (* mtyp -> mtyp *) + fun pos_set_mtype_for_dom M = + MFun (M, S (if exists_alpha_sub_mtype M then Plus else Minus), bool_M) + (* typ -> accumulator -> mterm * accumulator *) + fun do_all T (gamma, cset) = let - val abs_C = ctype_for (domain_type (domain_type T)) - val body_C = ctype_for (range_type T) + val abs_M = mtype_for (domain_type (domain_type T)) + val body_M = mtype_for (body_type T) in - (CFun (CFun (abs_C, S Minus, body_C), S Minus, body_C), - (gamma, cset |> add_ctype_is_right_total abs_C)) + (MFun (MFun (abs_M, S Minus, body_M), S Minus, body_M), + (gamma, cset |> add_mtype_is_right_total abs_M)) end fun do_equals T (gamma, cset) = - let val C = ctype_for (domain_type T) in - (CFun (C, S Minus, CFun (C, V (Unsynchronized.inc max_fresh), - ctype_for (nth_range_type 2 T))), - (gamma, cset |> add_ctype_is_right_unique C)) + let val M = mtype_for (domain_type T) in + (MFun (M, S Minus, MFun (M, V (Unsynchronized.inc max_fresh), + mtype_for (nth_range_type 2 T))), + (gamma, cset |> add_mtype_is_right_unique M)) end fun do_robust_set_operation T (gamma, cset) = let val set_T = domain_type T - val C1 = ctype_for set_T - val C2 = ctype_for set_T - val C3 = ctype_for set_T + val M1 = mtype_for set_T + val M2 = mtype_for set_T + val M3 = mtype_for set_T in - (CFun (C1, S Minus, CFun (C2, S Minus, C3)), - (gamma, cset |> add_is_sub_ctype C1 C3 |> add_is_sub_ctype C2 C3)) + (MFun (M1, S Minus, MFun (M2, S Minus, M3)), + (gamma, cset |> add_is_sub_mtype M1 M3 |> add_is_sub_mtype M2 M3)) end fun do_fragile_set_operation T (gamma, cset) = let val set_T = domain_type T - val set_C = ctype_for set_T - (* typ -> ctype *) - fun custom_ctype_for (T as Type ("fun", [T1, T2])) = - if T = set_T then set_C - else CFun (custom_ctype_for T1, S Minus, custom_ctype_for T2) - | custom_ctype_for T = ctype_for T + val set_M = mtype_for set_T + (* typ -> mtyp *) + fun custom_mtype_for (T as Type ("fun", [T1, T2])) = + if T = set_T then set_M + else MFun (custom_mtype_for T1, S Minus, custom_mtype_for T2) + | custom_mtype_for T = mtype_for T in - (custom_ctype_for T, (gamma, cset |> add_ctype_is_right_unique set_C)) + (custom_mtype_for T, (gamma, cset |> add_mtype_is_right_unique set_M)) end - (* typ -> accumulator -> ctype * accumulator *) + (* typ -> accumulator -> mtyp * accumulator *) fun do_pair_constr T accum = - case ctype_for (nth_range_type 2 T) of - C as CPair (a_C, b_C) => - (CFun (a_C, S Minus, CFun (b_C, S Minus, C)), accum) - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [C]) - (* int -> typ -> accumulator -> ctype * accumulator *) + case mtype_for (nth_range_type 2 T) of + M as MPair (a_M, b_M) => + (MFun (a_M, S Minus, MFun (b_M, S Minus, M)), accum) + | M => raise MTYPE ("Nitpick_Mono.consider_term.do_pair_constr", [M]) + (* int -> typ -> accumulator -> mtyp * accumulator *) fun do_nth_pair_sel n T = - case ctype_for (domain_type T) of - C as CPair (a_C, b_C) => - pair (CFun (C, S Minus, if n = 0 then a_C else b_C)) - | C => raise CTYPE ("Nitpick_Mono.consider_term.do_nth_pair_sel", [C]) - val unsolvable = (CType ("unsolvable", []), unsolvable_accum) - (* typ -> term -> accumulator -> ctype * accumulator *) - fun do_bounded_quantifier abs_T bound_t body_t accum = + case mtype_for (domain_type T) of + M as MPair (a_M, b_M) => + 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 = (dummy_M, unsolvable_accum) + (* term -> mterm * accumulator *) + 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 = let - val abs_C = ctype_for abs_T - val (bound_C, accum) = accum |>> push_bound abs_C |> do_term bound_t - val expected_bound_C = pos_set_ctype_for_dom abs_C + val abs_M = mtype_for abs_T + val (bound_m, accum) = accum |>> push_bound abs_M |> do_term bound_t + val expected_bound_M = pos_set_mtype_for_dom abs_M + val (body_m, accum) = + accum ||> add_mtypes_equal expected_bound_M (mtype_of_mterm bound_m) + |> do_term body_t ||> apfst pop_bound + val bound_M = mtype_of_mterm bound_m + val (M1, a, M2) = dest_MFun bound_M in - accum ||> add_ctypes_equal expected_bound_C bound_C |> do_term body_t - ||> apfst pop_bound + (MApp (MRaw (t0, MFun (bound_M, S Minus, bool_M)), + MAbs (abs_s, abs_T, M1, a, + MApp (MApp (MRaw (connective_t, + mtype_for (fastype_of connective_t)), + MApp (bound_m, MRaw (Bound 0, M1))), + body_m))), accum) end - (* term -> accumulator -> ctype * accumulator *) - and do_term _ (_, UnsolvableCSet) = unsolvable + (* term -> accumulator -> mterm * accumulator *) + and do_term t (_, UnsolvableCSet) = mterm_unsolvable t | do_term t (accum as (gamma as {bounds, frees, consts}, cset)) = (case t of Const (x as (s, T)) => (case AList.lookup (op =) consts x of - SOME C => (C, accum) + SOME M => (M, accum) | NONE => if not (could_exist_alpha_subtype alpha_T T) then - (ctype_for T, accum) + (mtype_for T, accum) else case s of - @{const_name all} => do_quantifier T accum + @{const_name all} => do_all T accum | @{const_name "=="} => do_equals T accum - | @{const_name All} => do_quantifier T accum - | @{const_name Ex} => do_quantifier T accum + | @{const_name All} => do_all T accum + | @{const_name Ex} => + 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"; unsolvable) - | @{const_name Eps} => (print_g "*** Eps"; unsolvable) + | @{const_name The} => (print_g "*** The"; mtype_unsolvable) + | @{const_name Eps} => (print_g "*** Eps"; mtype_unsolvable) | @{const_name If} => do_robust_set_operation (range_type T) accum - |>> curry3 CFun bool_C (S Minus) + |>> curry3 MFun bool_M (S Minus) | @{const_name Pair} => do_pair_constr T accum | @{const_name fst} => do_nth_pair_sel 0 T accum | @{const_name snd} => do_nth_pair_sel 1 T accum | @{const_name Id} => - (CFun (ctype_for (domain_type T), S Minus, bool_C), accum) + (MFun (mtype_for (domain_type T), S Minus, bool_M), accum) | @{const_name insert} => let val set_T = domain_type (range_type T) - val C1 = ctype_for (domain_type set_T) - val C1' = pos_set_ctype_for_dom C1 - val C2 = ctype_for set_T - val C3 = ctype_for set_T + val M1 = mtype_for (domain_type set_T) + val M1' = pos_set_mtype_for_dom M1 + val M2 = mtype_for set_T + val M3 = mtype_for set_T in - (CFun (C1, S Minus, CFun (C2, S Minus, C3)), - (gamma, cset |> add_ctype_is_right_unique C1 - |> add_is_sub_ctype C1' C3 - |> add_is_sub_ctype C2 C3)) + (MFun (M1, S Minus, MFun (M2, S Minus, M3)), + (gamma, cset |> add_mtype_is_right_unique M1 + |> add_is_sub_mtype M1' M3 + |> add_is_sub_mtype M2 M3)) end | @{const_name converse} => let val x = Unsynchronized.inc max_fresh - (* typ -> ctype *) - fun ctype_for_set T = - CFun (ctype_for (domain_type T), V x, bool_C) - val ab_set_C = domain_type T |> ctype_for_set - val ba_set_C = range_type T |> ctype_for_set - in (CFun (ab_set_C, S Minus, ba_set_C), accum) end + (* typ -> mtyp *) + fun mtype_for_set T = + MFun (mtype_for (domain_type T), V x, bool_M) + val ab_set_M = domain_type T |> mtype_for_set + val ba_set_M = range_type T |> mtype_for_set + in (MFun (ab_set_M, S Minus, ba_set_M), accum) end | @{const_name trancl} => do_fragile_set_operation T accum - | @{const_name rtrancl} => (print_g "*** rtrancl"; unsolvable) + | @{const_name rtrancl} => + (print_g "*** rtrancl"; mtype_unsolvable) | @{const_name finite} => - let val C1 = ctype_for (domain_type (domain_type T)) in - (CFun (pos_set_ctype_for_dom C1, S Minus, bool_C), 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 - (* typ -> ctype *) - fun ctype_for_set T = - CFun (ctype_for (domain_type T), V x, bool_C) - val bc_set_C = domain_type T |> ctype_for_set - val ab_set_C = domain_type (range_type T) |> ctype_for_set - val ac_set_C = nth_range_type 2 T |> ctype_for_set + (* typ -> mtyp *) + fun mtype_for_set T = + MFun (mtype_for (domain_type T), V x, bool_M) + val bc_set_M = domain_type T |> mtype_for_set + val ab_set_M = domain_type (range_type T) |> mtype_for_set + val ac_set_M = nth_range_type 2 T |> mtype_for_set in - (CFun (bc_set_C, S Minus, CFun (ab_set_C, S Minus, ac_set_C)), + (MFun (bc_set_M, S Minus, MFun (ab_set_M, S Minus, ac_set_M)), accum) end | @{const_name image} => let - val a_C = ctype_for (domain_type (domain_type T)) - val b_C = ctype_for (range_type (domain_type T)) + val a_M = mtype_for (domain_type (domain_type T)) + val b_M = mtype_for (range_type (domain_type T)) in - (CFun (CFun (a_C, S Minus, b_C), S Minus, - CFun (pos_set_ctype_for_dom a_C, S Minus, - pos_set_ctype_for_dom b_C)), accum) + (MFun (MFun (a_M, S Minus, b_M), S Minus, + MFun (pos_set_mtype_for_dom a_M, S Minus, + pos_set_mtype_for_dom b_M)), accum) end | @{const_name Sigma} => let val x = Unsynchronized.inc max_fresh - (* typ -> ctype *) - fun ctype_for_set T = - CFun (ctype_for (domain_type T), V x, bool_C) + (* typ -> mtyp *) + fun mtype_for_set T = + MFun (mtype_for (domain_type T), V x, bool_M) val a_set_T = domain_type T - val a_C = ctype_for (domain_type a_set_T) - val b_set_C = ctype_for_set (range_type (domain_type + val a_M = mtype_for (domain_type a_set_T) + val b_set_M = mtype_for_set (range_type (domain_type (range_type T))) - val a_set_C = ctype_for_set a_set_T - val a_to_b_set_C = CFun (a_C, S Minus, b_set_C) - val ab_set_C = ctype_for_set (nth_range_type 2 T) + val a_set_M = mtype_for_set a_set_T + val a_to_b_set_M = MFun (a_M, S Minus, b_set_M) + val ab_set_M = mtype_for_set (nth_range_type 2 T) in - (CFun (a_set_C, S Minus, - CFun (a_to_b_set_C, S Minus, ab_set_C)), accum) + (MFun (a_set_M, S Minus, + MFun (a_to_b_set_M, S Minus, ab_set_M)), accum) end | @{const_name Tha} => let - val a_C = ctype_for (domain_type (domain_type T)) - val a_set_C = pos_set_ctype_for_dom a_C - in (CFun (a_set_C, S Minus, a_C), accum) end + val a_M = mtype_for (domain_type (domain_type T)) + val a_set_M = pos_set_mtype_for_dom a_M + in (MFun (a_set_M, S Minus, a_M), accum) end | @{const_name FunBox} => - let val dom_C = ctype_for (domain_type T) in - (CFun (dom_C, S Minus, dom_C), accum) + let val dom_M = mtype_for (domain_type T) in + (MFun (dom_M, S Minus, dom_M), accum) end | _ => if s = @{const_name minus_class.minus} andalso is_set_type (domain_type T) then let val set_T = domain_type T - val left_set_C = ctype_for set_T - val right_set_C = ctype_for set_T + val left_set_M = mtype_for set_T + val right_set_M = mtype_for set_T in - (CFun (left_set_C, S Minus, - CFun (right_set_C, S Minus, left_set_C)), - (gamma, cset |> add_ctype_is_right_unique right_set_C - |> add_is_sub_ctype right_set_C left_set_C)) + (MFun (left_set_M, S Minus, + MFun (right_set_M, S Minus, left_set_M)), + (gamma, cset |> add_mtype_is_right_unique right_set_M + |> add_is_sub_mtype right_set_M left_set_M)) end else if s = @{const_name ord_class.less_eq} andalso is_set_type (domain_type T) then @@ -724,34 +812,37 @@ do_robust_set_operation T accum else if is_sel s then if constr_name_for_sel_like s = @{const_name FunBox} then - let val dom_C = ctype_for (domain_type T) in - (CFun (dom_C, S Minus, dom_C), accum) + let val dom_M = mtype_for (domain_type T) in + (MFun (dom_M, S Minus, dom_M), accum) end else - (ctype_for_sel cdata x, accum) + (mtype_for_sel mdata x, accum) else if is_constr thy stds x then - (ctype_for_constr cdata x, accum) + (mtype_for_constr mdata x, accum) else if is_built_in_const thy stds fast_descrs x then case def_of_const thy def_table x of - SOME t' => do_term t' accum - | NONE => (print_g ("*** built-in " ^ s); unsolvable) + SOME t' => do_term t' accum |>> mtype_of_mterm + | NONE => (print_g ("*** built-in " ^ s); mtype_unsolvable) else - let val C = ctype_for T in - (C, ({bounds = bounds, frees = frees, - consts = (x, C) :: consts}, cset)) - end) + let val M = mtype_for T in + (M, ({bounds = bounds, frees = frees, + consts = (x, M) :: consts}, cset)) + end) |>> curry MRaw t | Free (x as (_, T)) => (case AList.lookup (op =) frees x of - SOME C => (C, accum) + SOME M => (M, accum) | NONE => - let val C = ctype_for T in - (C, ({bounds = bounds, frees = (x, C) :: frees, + let val M = mtype_for T in + (M, ({bounds = bounds, frees = (x, M) :: frees, consts = consts}, cset)) - end) - | Var _ => (print_g "*** Var"; unsolvable) - | Bound j => (nth bounds j, accum) - | Abs (_, T, @{const False}) => (ctype_for (T --> bool_T), accum) - | Abs (_, T, t') => + end) |>> curry MRaw t + | Var _ => (print_g "*** Var"; mterm_unsolvable t) + | 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, MRaw (t', M2)), accum) + end + | Abs (s, T, t') => ((case t' of t1' $ Bound 0 => if not (loose_bvar1 (t1', 0)) then @@ -761,107 +852,127 @@ | _ => raise SAME ()) handle SAME () => let - val C = ctype_for T - val (C', accum) = do_term t' (accum |>> push_bound C) - in (CFun (C, S Minus, C'), accum |>> pop_bound) end) - | Const (@{const_name All}, _) - $ Abs (_, T', @{const "op -->"} $ (t1 $ Bound 0) $ t2) => - do_bounded_quantifier T' t1 t2 accum - | Const (@{const_name Ex}, _) - $ Abs (_, T', @{const "op &"} $ (t1 $ Bound 0) $ t2) => - do_bounded_quantifier T' t1 t2 accum + val M = mtype_for T + val (m', accum) = do_term t' (accum |>> push_bound M) + in (MAbs (s, T, M, S Minus, m'), accum |>> pop_bound) end) + | (t0 as Const (@{const_name All}, _)) + $ Abs (s', T', (t10 as @{const "op -->"}) $ (t11 $ Bound 0) $ t12) => + do_bounded_quantifier t0 s' T' t10 t11 t12 accum + | (t0 as Const (@{const_name Ex}, _)) + $ Abs (s', T', (t10 as @{const "op &"}) $ (t11 $ Bound 0) $ t12) => + do_bounded_quantifier t0 s' T' t10 t11 t12 accum | Const (@{const_name Let}, _) $ t1 $ t2 => do_term (betapply (t2, t1)) accum | t1 $ t2 => let - val (C1, accum) = do_term t1 accum - val (C2, accum) = do_term t2 accum + val (m1, accum) = do_term t1 accum + val (m2, accum) = do_term t2 accum in case accum of - (_, UnsolvableCSet) => unsolvable - | _ => case C1 of - CFun (C11, _, C12) => - (C12, accum ||> add_is_sub_ctype C2 C11) - | _ => raise CTYPE ("Nitpick_Mono.consider_term.do_term \ - \(op $)", [C1]) + (_, UnsolvableCSet) => mterm_unsolvable t + | _ => + 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 (C, _) => - print_g (" \ \ " ^ - Syntax.string_of_term ctxt t ^ " : " ^ - string_for_ctype C)) + |> tap (fn (m, _) => print_g (" \ \ " ^ + string_for_mterm ctxt m)) in do_term end -(* cdata -> sign -> term -> accumulator -> accumulator *) -fun consider_general_formula (cdata as {hol_ctxt = {ctxt, ...}, ...}) = +(* mdata -> styp -> term -> term -> mterm * accumulator *) +fun consider_general_equals mdata (x as (_, T)) t1 t2 accum = let - (* typ -> ctype *) - val ctype_for = fresh_ctype_for_type cdata - (* term -> accumulator -> ctype * accumulator *) - val do_term = consider_term cdata - (* sign -> term -> accumulator -> accumulator *) - fun do_formula _ _ (_, UnsolvableCSet) = unsolvable_accum - | do_formula sn t (accum as (gamma, cset)) = + 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 -> 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_C = ctype_for abs_T + val abs_M = mtype_for abs_T val side_cond = ((sn = Minus) = (quant_s = @{const_name Ex})) - val cset = cset |> side_cond ? add_ctype_is_right_total abs_C + 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_C, 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 (ctype_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 (C1, accum) = do_term t1 accum - val (C2, accum) = do_term t2 accum - in accum ||> add_ctypes_equal C1 C2 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}, _) $ Abs (_, T1, t1) => - do_quantifier s0 T1 t1 - | 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 + 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 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) + | 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 ("\ \ " ^ - Syntax.string_of_term ctxt t ^ - " : o\<^sup>" ^ string_for_sign sn)) + |> tap (fn (m, _) => + print_g ("\ \ " ^ + 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 @@ -877,79 +988,110 @@ |> (forall (member (op =) harmless_consts o original_name o fst) orf exists (member (op =) bounteous_consts o fst)) -(* cdata -> sign -> term -> accumulator -> accumulator *) -fun consider_nondefinitional_axiom (cdata as {hol_ctxt, ...}) sn t = - not (is_harmless_axiom hol_ctxt t) ? consider_general_formula cdata 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 -(* cdata -> term -> accumulator -> accumulator *) -fun consider_definitional_axiom (cdata as {hol_ctxt as {thy, ...}, ...}) t = +(* 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 cdata 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 -> ctype * accumulator *) - val do_term = consider_term cdata - (* typ -> term -> accumulator -> accumulator *) - fun do_all abs_T body_t accum = - let val abs_C = fresh_ctype_for_type cdata abs_T in - accum |>> push_bound abs_C |> 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 (C1, accum) = do_term t1 accum - val (C2, accum) = do_term t2 accum - in accum ||> add_ctypes_equal C1 C2 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 -(* Proof.context -> literal list -> term -> ctype -> string *) -fun string_for_ctype_of_term ctxt lits t C = +(* Proof.context -> literal list -> term -> mtyp -> string *) +fun string_for_mtype_of_term ctxt lits t M = Syntax.string_of_term ctxt t ^ " : " ^ - string_for_ctype (instantiate_ctype lits C) + string_for_mtype (instantiate_mtype lits M) -(* theory -> literal list -> ctype_context -> unit *) -fun print_ctype_context ctxt lits ({frees, consts, ...} : ctype_context) = - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Free x) C) frees @ - map (fn (x, C) => string_for_ctype_of_term ctxt lits (Const x) C) consts +(* theory -> literal list -> mtype_context -> unit *) +fun print_mtype_context ctxt lits ({frees, consts, ...} : mtype_context) = + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Free x) M) frees @ + map (fn (x, M) => string_for_mtype_of_term ctxt lits (Const x) M) consts |> cat_lines |> print_g -(* hol_context -> bool -> typ -> sign -> term list -> term list -> term - -> bool *) -fun formulas_monotonic (hol_ctxt as {ctxt, ...}) binarize alpha_T sn def_ts - nondef_ts core_t = +(* ('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 + (nondef_ts, def_ts) = let - val _ = print_g ("****** " ^ string_for_ctype CAlpha ^ " is " ^ + val _ = print_g ("****** Monotonicity analysis: " ^ + string_for_mtype MAlpha ^ " is " ^ Syntax.string_of_typ ctxt alpha_T) - val cdata as {max_fresh, ...} = initial_cdata hol_ctxt binarize alpha_T - val (gamma, cset) = - (initial_gamma, slack) - |> fold (consider_definitional_axiom cdata) def_ts - |> fold (consider_nondefinitional_axiom cdata Plus) nondef_ts - |> consider_general_formula cdata sn core_t + val mdata as {max_fresh, constr_cache, ...} = + initial_mdata hol_ctxt binarize alpha_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_ctype_context ctxt lits gamma; true) + SOME lits => (print_mtype_context ctxt lits gamma; true) | _ => false end - handle CTYPE (loc, Cs) => raise BAD (loc, commas (map string_for_ctype Cs)) + handle MTYPE (loc, Ms) => raise BAD (loc, commas (map string_for_mtype Ms)) end; diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_nut.ML --- a/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_nut.ML Fri Feb 26 16:50:09 2010 +0100 @@ -1031,7 +1031,7 @@ if is_opt_rep R then triad_fn (fn polar => s_op2 Subset T (Formula polar) u1 u2) else if opt andalso polar = Pos andalso - not (is_concrete_type datatypes (type_of u1)) then + not (is_concrete_type datatypes true (type_of u1)) then Cst (False, T, Formula Pos) else s_op2 Subset T R u1 u2 @@ -1057,7 +1057,7 @@ else opt_opt_case () in if unsound orelse polar = Neg orelse - is_concrete_type datatypes (type_of u1) then + is_concrete_type datatypes true (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' @@ -1159,7 +1159,7 @@ let val quant_u = s_op2 oper T (Formula polar) u1' u2' in if def orelse (unsound andalso (polar = Pos) = (oper = All)) orelse - is_complete_type datatypes (type_of u1) then + is_complete_type datatypes true (type_of u1) then quant_u else let @@ -1202,7 +1202,7 @@ else unopt_R |> opt ? opt_rep ofs T val u = Op2 (oper, T, R, u1', sub u2) in - if is_complete_type datatypes T orelse not opt1 then + if is_complete_type datatypes true T orelse not opt1 then u else let diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Feb 26 16:50:09 2010 +0100 @@ -126,7 +126,7 @@ val norm_frac_rel = (4, 0) (* int -> bool -> rel_expr *) -fun atom_for_bool j0 = Atom o Integer.add j0 o int_for_bool +fun atom_for_bool j0 = Atom o Integer.add j0 o int_from_bool (* bool -> formula *) fun formula_for_bool b = if b then True else False diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Fri Feb 26 16:50:09 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 = @@ -136,6 +135,59 @@ (index_seq 0 (length arg_Ts)) arg_Ts) end +(* (term -> term) -> int -> term -> term *) +fun coerce_bound_no f j t = + case t of + t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 + | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') + | Bound j' => if j' = j then f t else t + | _ => t +(* hol_context -> typ -> typ -> term -> term *) +fun coerce_bound_0_in_term hol_ctxt new_T old_T = + old_T <> new_T ? coerce_bound_no (coerce_term hol_ctxt [new_T] old_T new_T) 0 +(* hol_context -> typ list -> typ -> typ -> term -> term *) +and coerce_term (hol_ctxt as {thy, stds, fast_descrs, ...}) Ts new_T old_T t = + if old_T = new_T then + t + else + case (new_T, old_T) of + (Type (new_s, new_Ts as [new_T1, new_T2]), + Type ("fun", [old_T1, old_T2])) => + (case eta_expand Ts t 1 of + Abs (s, _, t') => + Abs (s, new_T1, + t' |> coerce_bound_0_in_term hol_ctxt new_T1 old_T1 + |> coerce_term hol_ctxt (new_T1 :: Ts) new_T2 old_T2) + |> Envir.eta_contract + |> new_s <> "fun" + ? construct_value thy stds + (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) + o single + | t' => raise TERM ("Nitpick_Preproc.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 + case constr_expand hol_ctxt old_T t of + Const (old_s, _) $ t1 => + if new_s = "fun" then + coerce_term hol_ctxt Ts new_T (Type ("fun", old_Ts)) t1 + else + construct_value thy stds + (old_s, Type ("fun", new_Ts) --> new_T) + [coerce_term hol_ctxt Ts (Type ("fun", new_Ts)) + (Type ("fun", old_Ts)) t1] + | Const _ $ t1 $ t2 => + construct_value thy stds + (if new_s = "*" then @{const_name Pair} + else @{const_name PairBox}, new_Ts ---> new_T) + [coerce_term hol_ctxt Ts new_T1 old_T1 t1, + coerce_term hol_ctxt Ts new_T2 old_T2 t2] + | t' => raise TERM ("Nitpick_Preproc.coerce_term", [t']) + else + raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t]) + | _ => raise TYPE ("Nitpick_Preproc.coerce_term", [new_T, old_T], [t]) + (* hol_context -> bool -> term -> term *) fun box_fun_and_pair_in_term (hol_ctxt as {thy, stds, fast_descrs, ...}) def orig_t = @@ -146,60 +198,6 @@ | box_relational_operator_type (Type ("*", Ts)) = Type ("*", map (box_type hol_ctxt InPair) Ts) | box_relational_operator_type T = T - (* (term -> term) -> int -> term -> term *) - fun coerce_bound_no f j t = - case t of - t1 $ t2 => coerce_bound_no f j t1 $ coerce_bound_no f j t2 - | Abs (s, T, t') => Abs (s, T, coerce_bound_no f (j + 1) t') - | Bound j' => if j' = j then f t else t - | _ => t - (* typ -> typ -> term -> term *) - fun coerce_bound_0_in_term new_T old_T = - old_T <> new_T ? coerce_bound_no (coerce_term [new_T] old_T new_T) 0 - (* typ list -> typ -> term -> term *) - and coerce_term Ts new_T old_T t = - if old_T = new_T then - t - else - case (new_T, old_T) of - (Type (new_s, new_Ts as [new_T1, new_T2]), - Type ("fun", [old_T1, old_T2])) => - (case eta_expand Ts t 1 of - Abs (s, _, t') => - Abs (s, new_T1, - t' |> coerce_bound_0_in_term new_T1 old_T1 - |> coerce_term (new_T1 :: Ts) new_T2 old_T2) - |> Envir.eta_contract - |> new_s <> "fun" - ? construct_value thy stds - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) - o single - | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ - \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 - case constr_expand hol_ctxt old_T t of - Const (@{const_name FunBox}, _) $ t1 => - if new_s = "fun" then - coerce_term Ts new_T (Type ("fun", old_Ts)) t1 - else - construct_value thy stds - (@{const_name FunBox}, Type ("fun", new_Ts) --> new_T) - [coerce_term Ts (Type ("fun", new_Ts)) - (Type ("fun", old_Ts)) t1] - | Const _ $ t1 $ t2 => - construct_value thy stds - (if new_s = "*" then @{const_name Pair} - else @{const_name PairBox}, new_Ts ---> new_T) - [coerce_term Ts new_T1 old_T1 t1, - coerce_term Ts new_T2 old_T2 t2] - | t' => raise TERM ("Nitpick_Preproc.box_fun_and_pair_in_term.\ - \coerce_term", [t']) - else - raise TYPE ("coerce_term", [new_T, old_T], [t]) - | _ => raise TYPE ("coerce_term", [new_T, old_T], [t]) (* indexname * typ -> typ * term -> typ option list -> typ option list *) fun add_boxed_types_for_var (z as (_, T)) (T', t') = case t' of @@ -252,7 +250,7 @@ val T = [T1, T2] |> sort TermOrd.typ_ord |> List.last in list_comb (Const (s0, T --> T --> body_type T0), - map2 (coerce_term new_Ts T) [T1, T2] [t1, t2]) + map2 (coerce_term hol_ctxt new_Ts T) [T1, T2] [t1, t2]) end (* string -> typ -> term *) and do_description_operator s T = @@ -320,7 +318,7 @@ val T' = hd (snd (dest_Type (hd Ts1))) val t2 = Abs (s, T', do_term (T' :: new_Ts) (T :: old_Ts) Neut t2') val T2 = fastype_of1 (new_Ts, t2) - val t2 = coerce_term new_Ts (hd Ts1) T2 t2 + val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 in betapply (if s1 = "fun" then t1 @@ -336,7 +334,7 @@ val (s1, Ts1) = dest_Type T1 val t2 = do_term new_Ts old_Ts Neut t2 val T2 = fastype_of1 (new_Ts, t2) - val t2 = coerce_term new_Ts (hd Ts1) T2 t2 + val t2 = coerce_term hol_ctxt new_Ts (hd Ts1) T2 t2 in betapply (if s1 = "fun" then t1 @@ -474,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 @@ -508,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 @@ -1020,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, @@ -1170,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 **) @@ -1275,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 @@ -1386,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 @@ -1425,10 +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 in - (((map (do_rest true) def_ts, map (do_rest false) nondef_ts), - (got_all_mono_user_axioms, no_poly_user_axioms)), - do_rest false core_t, binarize) + (nondef_ts, def_ts, got_all_mono_user_axioms, no_poly_user_axioms, binarize) end end; diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_rep.ML --- a/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_rep.ML Fri Feb 26 16:50:09 2010 +0100 @@ -299,7 +299,7 @@ | z => Func z) | best_non_opt_set_rep_for_type scope T = best_one_rep_for_type scope T fun best_set_rep_for_type (scope as {datatypes, ...}) T = - (if is_exact_type datatypes T then best_non_opt_set_rep_for_type + (if is_exact_type datatypes true T then best_non_opt_set_rep_for_type else best_opt_set_rep_for_type) scope T fun best_non_opt_symmetric_reps_for_fun_type (scope as {ofs, ...}) (Type ("fun", [T1, T2])) = diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Feb 26 16:50:09 2010 +0100 @@ -23,8 +23,8 @@ card: int, co: bool, standard: bool, - complete: bool, - concrete: bool, + complete: bool * bool, + concrete: bool * bool, deep: bool, constrs: constr_spec list} @@ -39,9 +39,9 @@ val datatype_spec : dtype_spec list -> typ -> dtype_spec option val constr_spec : dtype_spec list -> styp -> constr_spec - val is_complete_type : dtype_spec list -> typ -> bool - val is_concrete_type : dtype_spec list -> typ -> bool - val is_exact_type : dtype_spec list -> typ -> bool + val is_complete_type : dtype_spec list -> bool -> typ -> bool + val is_concrete_type : dtype_spec list -> bool -> typ -> bool + val is_exact_type : dtype_spec list -> bool -> typ -> bool val offset_of_type : int Typtab.table -> typ -> int val spec_of_type : scope -> typ -> int * int val pretties_for_scope : scope -> bool -> Pretty.T list @@ -51,7 +51,7 @@ val all_scopes : hol_context -> bool -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list - -> int list -> int list -> typ list -> typ list -> typ list + -> int list -> int list -> typ list -> typ list -> typ list -> typ list -> int * scope list end; @@ -74,8 +74,8 @@ card: int, co: bool, standard: bool, - complete: bool, - concrete: bool, + complete: bool * bool, + concrete: bool * bool, deep: bool, constrs: constr_spec list} @@ -105,22 +105,24 @@ SOME c => c | NONE => constr_spec dtypes x -(* dtype_spec list -> typ -> bool *) -fun is_complete_type dtypes (Type ("fun", [T1, T2])) = - is_concrete_type dtypes T1 andalso is_complete_type dtypes T2 - | is_complete_type dtypes (Type ("*", Ts)) = - forall (is_complete_type dtypes) Ts - | is_complete_type dtypes T = +(* dtype_spec list -> bool -> typ -> bool *) +fun is_complete_type dtypes facto (Type ("fun", [T1, T2])) = + is_concrete_type dtypes facto T1 andalso is_complete_type dtypes facto T2 + | is_complete_type dtypes facto (Type ("*", Ts)) = + forall (is_complete_type dtypes facto) Ts + | is_complete_type dtypes facto T = not (is_integer_like_type T) andalso not (is_bit_type T) andalso - #complete (the (datatype_spec dtypes T)) + fun_from_pair (#complete (the (datatype_spec dtypes T))) facto handle Option.Option => true -and is_concrete_type dtypes (Type ("fun", [T1, T2])) = - is_complete_type dtypes T1 andalso is_concrete_type dtypes T2 - | is_concrete_type dtypes (Type ("*", Ts)) = - forall (is_concrete_type dtypes) Ts - | is_concrete_type dtypes T = - #concrete (the (datatype_spec dtypes T)) handle Option.Option => true -fun is_exact_type dtypes = is_complete_type dtypes andf is_concrete_type dtypes +and is_concrete_type dtypes facto (Type ("fun", [T1, T2])) = + is_complete_type dtypes facto T1 andalso is_concrete_type dtypes facto T2 + | is_concrete_type dtypes facto (Type ("*", Ts)) = + forall (is_concrete_type dtypes facto) Ts + | is_concrete_type dtypes facto T = + fun_from_pair (#concrete (the (datatype_spec dtypes T))) facto + handle Option.Option => true +fun is_exact_type dtypes facto = + is_complete_type dtypes facto andf is_concrete_type dtypes facto (* int Typtab.table -> typ -> int *) fun offset_of_type ofs T = @@ -461,15 +463,18 @@ explicit_max = max, total = total} :: constrs end -(* hol_context -> (typ * int) list -> typ -> bool *) -fun has_exact_card hol_ctxt card_assigns T = +(* hol_context -> bool -> typ list -> (typ * int) list -> typ -> bool *) +fun has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T = let val card = card_of_type card_assigns T in - card = bounded_exact_card_of_type hol_ctxt (card + 1) 0 card_assigns T + card = bounded_exact_card_of_type hol_ctxt + (if facto then finitizable_dataTs else []) (card + 1) 0 + card_assigns T end -(* hol_context -> bool -> typ list -> scope_desc -> typ * int -> dtype_spec *) +(* hol_context -> bool -> typ list -> typ list -> scope_desc -> typ * int + -> dtype_spec *) fun datatype_spec_from_scope_descriptor (hol_ctxt as {thy, stds, ...}) binarize - deep_dataTs (desc as (card_assigns, _)) (T, card) = + deep_dataTs finitizable_dataTs (desc as (card_assigns, _)) (T, card) = let val deep = member (op =) deep_dataTs T val co = is_codatatype thy T @@ -478,10 +483,16 @@ val self_recs = map (is_self_recursive_constr_type o snd) xs val (num_self_recs, num_non_self_recs) = List.partition I self_recs |> pairself length - val complete = has_exact_card hol_ctxt card_assigns T - val concrete = is_word_type T orelse - (xs |> maps (binder_types o snd) |> maps binder_types - |> forall (has_exact_card hol_ctxt card_assigns)) + (* bool -> bool *) + fun is_complete facto = + has_exact_card hol_ctxt facto finitizable_dataTs card_assigns T + fun is_concrete facto = + is_word_type T orelse + xs |> maps (binder_types o snd) |> maps binder_types + |> forall (has_exact_card hol_ctxt facto finitizable_dataTs + card_assigns) + val complete = pair_from_fun is_complete + val concrete = pair_from_fun is_concrete (* int -> int *) fun sum_dom_cards max = map (domain_card max card_assigns o snd) xs |> Integer.sum @@ -494,13 +505,15 @@ concrete = concrete, deep = deep, constrs = constrs} end -(* hol_context -> bool -> int -> typ list -> scope_desc -> scope *) +(* hol_context -> bool -> int -> typ list -> typ list -> scope_desc -> scope *) fun scope_from_descriptor (hol_ctxt as {thy, stds, ...}) binarize sym_break - deep_dataTs (desc as (card_assigns, _)) = + deep_dataTs finitizable_dataTs + (desc as (card_assigns, _)) = let val datatypes = map (datatype_spec_from_scope_descriptor hol_ctxt binarize deep_dataTs - desc) (filter (is_datatype thy stds o fst) card_assigns) + finitizable_dataTs desc) + (filter (is_datatype thy stds o fst) card_assigns) val bits = card_of_type card_assigns @{typ signed_bit} - 1 handle TYPE ("Nitpick_HOL.card_of_type", _, _) => card_of_type card_assigns @{typ unsigned_bit} @@ -530,10 +543,10 @@ (* hol_context -> bool -> int -> (typ option * int list) list -> (styp option * int list) list -> (styp option * int list) list -> int list - -> typ list -> typ list -> typ list -> int * scope list *) + -> typ list -> typ list -> typ list ->typ list -> int * scope list *) fun all_scopes (hol_ctxt as {thy, ...}) binarize sym_break cards_assigns maxes_assigns iters_assigns bitss bisim_depths mono_Ts nonmono_Ts - deep_dataTs = + deep_dataTs finitizable_dataTs = let val cards_assigns = repair_cards_assigns_wrt_boxing thy mono_Ts cards_assigns @@ -550,7 +563,7 @@ (length all - length head, descs |> length descs <= distinct_threshold ? distinct (op =) |> map (scope_from_descriptor hol_ctxt binarize sym_break - deep_dataTs)) + deep_dataTs finitizable_dataTs)) end end; diff -r f5fa7c72937e -r 4356263e0bdd src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Feb 26 13:29:43 2010 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Feb 26 16:50:09 2010 +0100 @@ -20,7 +20,9 @@ val nitpick_prefix : string val curry3 : ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd val pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c - val int_for_bool : bool -> int + val pair_from_fun : (bool -> 'a) -> 'a * 'a + val fun_from_pair : 'a * 'a -> bool -> 'a + val int_from_bool : bool -> int val nat_minus : int -> int -> int val reasonable_power : int -> int -> int val exact_log : int -> int -> int @@ -84,8 +86,13 @@ (* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *) fun pairf f g x = (f x, g x) +(* (bool -> 'a) -> 'a * 'a *) +fun pair_from_fun f = (f false, f true) +(* 'a * 'a -> bool -> 'a *) +fun fun_from_pair (f, t) b = if b then t else f + (* bool -> int *) -fun int_for_bool b = if b then 1 else 0 +fun int_from_bool b = if b then 1 else 0 (* int -> int -> int *) fun nat_minus i j = if i > j then i - j else 0