# HG changeset patch # User blanchet # Date 1272118650 -7200 # Node ID 76d5fd5a45fbfa0acc54ef261076fadadfefb29f # Parent 6adf1068ac0f8b8f24679807e0089471d6df3be8 cosmetics diff -r 6adf1068ac0f -r 76d5fd5a45fb src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:05:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Apr 24 16:17:30 2010 +0200 @@ -439,10 +439,10 @@ val _ = List.app (print_g o string_for_type ctxt) nonmono_Ts *) - val need_incremental = Int.max (max_potential, max_genuine) >= 2 - val effective_sat_solver = + val incremental = Int.max (max_potential, max_genuine) >= 2 + val actual_sat_solver = if sat_solver <> "smart" then - if need_incremental andalso + if incremental andalso not (member (op =) (Kodkod_SAT.configured_sat_solvers true) sat_solver) then (print_m (K ("An incremental SAT solver is required: \"SAT4J\" will \ @@ -451,15 +451,14 @@ else sat_solver else - Kodkod_SAT.smart_sat_solver_name need_incremental + Kodkod_SAT.smart_sat_solver_name incremental val _ = if sat_solver = "smart" then - print_v (fn () => "Using SAT solver " ^ quote effective_sat_solver ^ - ". The following" ^ - (if need_incremental then " incremental " else " ") ^ - "solvers are configured: " ^ - commas (map quote (Kodkod_SAT.configured_sat_solvers - need_incremental)) ^ ".") + print_v (fn () => + "Using SAT solver " ^ quote actual_sat_solver ^ ". The following" ^ + (if incremental then " incremental " else " ") ^ + "solvers are configured: " ^ + commas_quote (Kodkod_SAT.configured_sat_solvers incremental) ^ ".") else () @@ -495,9 +494,9 @@ val (sel_names, rep_table) = choose_reps_for_all_sels scope rep_table val (nonsel_names, rep_table) = repify_consts nonsel_names rep_table val min_highest_arity = - NameTable.fold (curry Int.max o arity_of_rep o snd) rep_table 1 + NameTable.fold (Integer.max o arity_of_rep o snd) rep_table 1 val min_univ_card = - NameTable.fold (curry Int.max o min_univ_card_of_rep o snd) rep_table + NameTable.fold (Integer.max o min_univ_card_of_rep o snd) rep_table (univ_card nat_card int_card main_j0 [] KK.True) val _ = check_arity min_univ_card min_highest_arity @@ -524,15 +523,15 @@ val comment = (if unsound then "unsound" else "sound") ^ "\n" ^ PrintMode.setmp [] multiline_string_for_scope scope val kodkod_sat_solver = - Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd + Kodkod_SAT.sat_solver_spec actual_sat_solver |> snd val bit_width = if bits = 0 then 16 else bits + 1 - val delay = if unsound then - Option.map (fn time => Time.- (time, Time.now ())) - deadline - |> unsound_delay_for_timeout - else - 0 - val settings = [("solver", commas (map quote kodkod_sat_solver)), + val delay = + if unsound then + Option.map (fn time => Time.- (time, Time.now ())) deadline + |> unsound_delay_for_timeout + else + 0 + val settings = [("solver", commas_quote kodkod_sat_solver), ("skolem_depth", "-1"), ("bit_width", string_of_int bit_width), ("symmetry_breaking", signed_string_of_int sym_break), @@ -731,7 +730,7 @@ fun print_and_check genuine (j, bounds) = print_and_check_model genuine bounds (snd (nth problems j)) val max_solutions = max_potential + max_genuine - |> not need_incremental ? curry Int.min 1 + |> not incremental ? Integer.min 1 in if max_solutions <= 0 then (found_really_genuine, 0, 0, donno) diff -r 6adf1068ac0f -r 76d5fd5a45fb src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:05:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Sat Apr 24 16:17:30 2010 +0200 @@ -16,6 +16,7 @@ show_skolems: bool, show_datatypes: bool, show_consts: bool} + type term_postprocessor = Proof.context -> string -> (typ -> term list) -> typ -> term -> term diff -r 6adf1068ac0f -r 76d5fd5a45fb src/HOL/Tools/Nitpick/nitpick_preproc.ML --- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:05:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Sat Apr 24 16:17:30 2010 +0200 @@ -83,7 +83,7 @@ is_sel s orelse s = @{const_name Sigma} then table else - Termtab.map_default (t, 65536) (curry Int.min (length args)) table + Termtab.map_default (t, 65536) (Integer.min (length args)) table | aux _ _ table = table in aux t [] end diff -r 6adf1068ac0f -r 76d5fd5a45fb src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:05:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Sat Apr 24 16:17:30 2010 +0200 @@ -235,7 +235,7 @@ | NONE => raise ARG ("Nitpick_Scope.lookup_ints_assign", "") (* theory -> (typ option * int list) list -> typ -> int list *) fun lookup_type_ints_assign thy assigns T = - map (curry Int.max 1) (lookup_ints_assign (type_match thy) assigns T) + map (Integer.max 1) (lookup_ints_assign (type_match thy) assigns T) handle ARG ("Nitpick_Scope.lookup_ints_assign", _) => raise TYPE ("Nitpick_Scope.lookup_type_ints_assign", [T], []) (* theory -> (styp option * int list) list -> styp -> int list *) diff -r 6adf1068ac0f -r 76d5fd5a45fb src/HOL/Tools/Nitpick/nitpick_tests.ML --- a/src/HOL/Tools/Nitpick/nitpick_tests.ML Sat Apr 24 16:05:42 2010 +0200 +++ b/src/HOL/Tools/Nitpick/nitpick_tests.ML Sat Apr 24 16:17:30 2010 +0200 @@ -324,6 +324,6 @@ case Kodkod.solve_any_problem false NONE 0 1 (map (problem_for_nut @{context}) tests) of Kodkod.Normal ([], _, _) => () - | _ => error "Tests failed" + | _ => error "Tests failed." end;