1.1 --- a/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
1.2 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Mon Mar 03 22:33:22 2014 +0100
1.3 @@ -7,21 +7,20 @@
1.4
1.5 signature NITPICK =
1.6 sig
1.7 - type styp = Nitpick_Util.styp
1.8 type term_postprocessor = Nitpick_Model.term_postprocessor
1.9
1.10 datatype mode = Auto_Try | Try | Normal | TPTP
1.11
1.12 type params =
1.13 {cards_assigns: (typ option * int list) list,
1.14 - maxes_assigns: (styp option * int list) list,
1.15 - iters_assigns: (styp option * int list) list,
1.16 + maxes_assigns: ((string * typ) option * int list) list,
1.17 + iters_assigns: ((string * typ) option * int list) list,
1.18 bitss: int list,
1.19 bisim_depths: int list,
1.20 boxes: (typ option * bool option) list,
1.21 finitizes: (typ option * bool option) list,
1.22 monos: (typ option * bool option) list,
1.23 - wfs: (styp option * bool option) list,
1.24 + wfs: ((string * typ) option * bool option) list,
1.25 sat_solver: string,
1.26 blocking: bool,
1.27 falsify: bool,
1.28 @@ -45,7 +44,7 @@
1.29 timeout: Time.time,
1.30 tac_timeout: Time.time,
1.31 max_threads: int,
1.32 - show_datatypes: bool,
1.33 + show_types: bool,
1.34 show_skolems: bool,
1.35 show_consts: bool,
1.36 evals: term list,
1.37 @@ -65,7 +64,8 @@
1.38 val unknownN : string
1.39 val register_frac_type : string -> (string * string) list -> theory -> theory
1.40 val unregister_frac_type : string -> theory -> theory
1.41 - val register_codatatype : typ -> string -> styp list -> theory -> theory
1.42 + val register_codatatype : typ -> string -> (string * typ) list -> theory ->
1.43 + theory
1.44 val unregister_codatatype : typ -> theory -> theory
1.45 val register_term_postprocessor :
1.46 typ -> term_postprocessor -> theory -> theory
1.47 @@ -99,14 +99,14 @@
1.48
1.49 type params =
1.50 {cards_assigns: (typ option * int list) list,
1.51 - maxes_assigns: (styp option * int list) list,
1.52 - iters_assigns: (styp option * int list) list,
1.53 + maxes_assigns: ((string * typ) option * int list) list,
1.54 + iters_assigns: ((string * typ) option * int list) list,
1.55 bitss: int list,
1.56 bisim_depths: int list,
1.57 boxes: (typ option * bool option) list,
1.58 finitizes: (typ option * bool option) list,
1.59 monos: (typ option * bool option) list,
1.60 - wfs: (styp option * bool option) list,
1.61 + wfs: ((string * typ) option * bool option) list,
1.62 sat_solver: string,
1.63 blocking: bool,
1.64 falsify: bool,
1.65 @@ -130,7 +130,7 @@
1.66 timeout: Time.time,
1.67 tac_timeout: Time.time,
1.68 max_threads: int,
1.69 - show_datatypes: bool,
1.70 + show_types: bool,
1.71 show_skolems: bool,
1.72 show_consts: bool,
1.73 evals: term list,
1.74 @@ -181,13 +181,14 @@
1.75
1.76 val isabelle_wrong_message =
1.77 "Something appears to be wrong with your Isabelle installation."
1.78 -fun java_not_found_message () =
1.79 +val java_not_found_message =
1.80 "Java could not be launched. " ^ isabelle_wrong_message
1.81 -fun java_too_old_message () =
1.82 +val java_too_old_message =
1.83 "The Java version is too old. " ^ isabelle_wrong_message
1.84 -fun kodkodi_not_installed_message () =
1.85 +val kodkodi_not_installed_message =
1.86 "Nitpick requires the external Java program Kodkodi."
1.87 -fun kodkodi_too_old_message () = "The installed Kodkodi version is too old."
1.88 +val kodkodi_too_old_message = "The installed Kodkodi version is too old."
1.89 +
1.90 val max_unsound_delay_ms = 200
1.91 val max_unsound_delay_percent = 2
1.92
1.93 @@ -205,6 +206,7 @@
1.94 val syntactic_sorts =
1.95 @{sort "{default,zero,one,plus,minus,uminus,times,inverse,abs,sgn,ord,equal}"} @
1.96 @{sort numeral}
1.97 +
1.98 fun has_tfree_syntactic_sort (TFree (_, S as _ :: _)) =
1.99 subset (op =) (S, syntactic_sorts)
1.100 | has_tfree_syntactic_sort _ = false
1.101 @@ -229,9 +231,9 @@
1.102 overlord, spy, user_axioms, assms, whacks, merge_type_vars,
1.103 binary_ints, destroy_constrs, specialize, star_linear_preds,
1.104 total_consts, needs, peephole_optim, datatype_sym_break,
1.105 - kodkod_sym_break, tac_timeout, max_threads, show_datatypes,
1.106 - show_skolems, show_consts, evals, formats, atomss, max_potential,
1.107 - max_genuine, check_potential, check_genuine, batch_size, ...} = params
1.108 + kodkod_sym_break, tac_timeout, max_threads, show_types, show_skolems,
1.109 + show_consts, evals, formats, atomss, max_potential, max_genuine,
1.110 + check_potential, check_genuine, batch_size, ...} = params
1.111 val state_ref = Unsynchronized.ref state
1.112 fun pprint print =
1.113 if mode = Auto_Try then
1.114 @@ -652,7 +654,7 @@
1.115 "% SZS output start FiniteModel")
1.116 val (reconstructed_model, codatatypes_ok) =
1.117 reconstruct_hol_model
1.118 - {show_datatypes = show_datatypes, show_skolems = show_skolems,
1.119 + {show_types = show_types, show_skolems = show_skolems,
1.120 show_consts = show_consts}
1.121 scope formats atomss real_frees pseudo_frees free_names sel_names
1.122 nonsel_names rel_table bounds
1.123 @@ -771,16 +773,16 @@
1.124 case KK.solve_any_problem debug overlord deadline max_threads
1.125 max_solutions (map fst problems) of
1.126 KK.JavaNotFound =>
1.127 - (print_nt java_not_found_message;
1.128 + (print_nt (K java_not_found_message);
1.129 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.130 | KK.JavaTooOld =>
1.131 - (print_nt java_too_old_message;
1.132 + (print_nt (K java_too_old_message);
1.133 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.134 | KK.KodkodiNotInstalled =>
1.135 - (print_nt kodkodi_not_installed_message;
1.136 + (print_nt (K kodkodi_not_installed_message);
1.137 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.138 | KK.KodkodiTooOld =>
1.139 - (print_nt kodkodi_too_old_message;
1.140 + (print_nt (K kodkodi_too_old_message);
1.141 (found_really_genuine, max_potential, max_genuine, donno + 1))
1.142 | KK.Normal ([], unsat_js, s) =>
1.143 (update_checked_problems problems unsat_js; show_kodkod_warning s;
1.144 @@ -1029,7 +1031,7 @@
1.145 if getenv "KODKODI" = "" then
1.146 (* The "expect" argument is deliberately ignored if Kodkodi is missing so
1.147 that the "Nitpick_Examples" can be processed on any machine. *)
1.148 - (print_nt (Pretty.string_of (plazy kodkodi_not_installed_message));
1.149 + (print_nt (Pretty.string_of (plazy (K kodkodi_not_installed_message)));
1.150 ("no_kodkodi", state))
1.151 else
1.152 let
1.153 @@ -1062,6 +1064,7 @@
1.154 (Const (@{const_name "=="}, _) $ Free (s, _) $ Const _) =
1.155 Variable.is_fixed ctxt s
1.156 | is_fixed_equation _ _ = false
1.157 +
1.158 fun extract_fixed_frees ctxt (assms, t) =
1.159 let
1.160 val (subst, other_assms) =