added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
--- a/NEWS Tue Jun 01 11:58:50 2010 +0200
+++ b/NEWS Tue Jun 01 12:20:08 2010 +0200
@@ -427,6 +427,7 @@
record getters.
- Fixed soundness bug related to higher-order constructors
- Improved precision of set constructs.
+ - Added "atoms" option.
- Added cache to speed up repeated Kodkod invocations on the same
problems.
- Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and
--- a/src/HOL/Tools/Nitpick/HISTORY Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/HISTORY Tue Jun 01 12:20:08 2010 +0200
@@ -16,6 +16,7 @@
* Fixed soundness bug related to higher-order constructors
* Improved precision of set constructs
* Added cache to speed up repeated Kodkod invocations on the same problems
+ * Added "atoms" option
* Renamed "MiniSatJNI", "zChaffJNI", "BerkMinAlloy", and "SAT4JLight" to
"MiniSat_JNI", "zChaff_JNI", "BerkMin_Alloy", and "SAT4J_Light"
* Removed "skolemize", "uncurry", "sym_break", "flatten_prop",
--- a/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Tue Jun 01 12:20:08 2010 +0200
@@ -42,6 +42,7 @@
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
+ atomss: (typ option * string list) list,
max_potential: int,
max_genuine: int,
check_potential: bool,
@@ -112,6 +113,7 @@
show_consts: bool,
evals: term list,
formats: (term option * int list) list,
+ atomss: (typ option * string list) list,
max_potential: int,
max_genuine: int,
check_potential: bool,
@@ -190,7 +192,7 @@
verbose, overlord, user_axioms, assms, merge_type_vars, binary_ints,
destroy_constrs, specialize, star_linear_preds, fast_descrs,
peephole_optim, tac_timeout, max_threads, show_datatypes, show_consts,
- evals, formats, max_potential, max_genuine, check_potential,
+ evals, formats, atomss, max_potential, max_genuine, check_potential,
check_genuine, batch_size, ...} = params
val state_ref = Unsynchronized.ref state
val pprint =
@@ -575,8 +577,8 @@
val (reconstructed_model, codatatypes_ok) =
reconstruct_hol_model {show_datatypes = show_datatypes,
show_consts = show_consts}
- scope formats frees free_names sel_names nonsel_names rel_table
- bounds
+ scope formats atomss frees free_names sel_names nonsel_names
+ rel_table bounds
val genuine_means_genuine =
got_all_user_axioms andalso none_true wfs andalso
sound_finitizes andalso codatatypes_ok
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Tue Jun 01 12:20:08 2010 +0200
@@ -715,7 +715,7 @@
val thy = ProofContext.theory_of ctxt
val (x as (_, T)) = (s, unarize_unbox_etc_type T)
in
- Refute.is_IDT_constructor thy x orelse is_record_constr x orelse
+ is_real_constr thy x orelse is_record_constr x orelse
(is_abs_fun ctxt x andalso is_pure_typedef ctxt (range_type T)) orelse
is_coconstr thy x
end
@@ -861,9 +861,9 @@
let
val (_, dtyps, constrs) = AList.lookup (op =) descr index |> the
in
- map (fn (s', Us) =>
- (s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
- ---> T)) constrs
+ map (apsnd (fn Us =>
+ map (typ_of_dtyp descr (dtyps ~~ Ts)) Us ---> T))
+ constrs
end
| NONE =>
if is_record_type T then
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Tue Jun 01 12:20:08 2010 +0200
@@ -65,6 +65,7 @@
("show_datatypes", "false"),
("show_consts", "false"),
("format", "1"),
+ ("atoms", ""),
("max_potential", "1"),
("max_genuine", "1"),
("check_potential", "false"),
@@ -98,10 +99,11 @@
fun is_known_raw_param s =
AList.defined (op =) default_default_params s orelse
AList.defined (op =) negated_params s orelse
- s = "max" orelse s = "show_all" orelse s = "eval" orelse s = "expect" orelse
+ member (op =) ["max", "show_all", "eval", "expect"] s orelse
exists (fn p => String.isPrefix (p ^ " ") s)
["card", "max", "iter", "box", "dont_box", "finitize", "dont_finitize",
- "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format"]
+ "mono", "non_mono", "std", "non_std", "wf", "non_wf", "format",
+ "atoms"]
fun check_raw_param (s, _) =
if is_known_raw_param s then ()
@@ -149,8 +151,8 @@
let
val override_params = maps normalize_raw_param override_params
val raw_params = rev override_params @ rev default_params
- val lookup =
- Option.map stringify_raw_param_value o AList.lookup (op =) raw_params
+ val raw_lookup = AList.lookup (op =) raw_params
+ val lookup = Option.map stringify_raw_param_value o raw_lookup
val lookup_string = the_default "" o lookup
fun general_lookup_bool option default_value name =
case lookup name of
@@ -191,27 +193,21 @@
[] => [min_int]
| value => value)
| NONE => [min_int]
- fun lookup_ints_assigns read prefix min_int =
- (NONE, lookup_int_seq prefix min_int)
- :: map (fn (name, value) =>
- (SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> int_seq_from_string name min_int))
- (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
- fun lookup_bool_assigns read prefix =
- (NONE, lookup_bool prefix)
+ fun lookup_assigns read prefix default convert =
+ (NONE, convert (the_default default (lookup prefix)))
:: map (fn (name, value) =>
(SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> parse_bool_option false name |> the))
+ convert (stringify_raw_param_value value)))
(filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
+ fun lookup_ints_assigns read prefix min_int =
+ lookup_assigns read prefix (signed_string_of_int min_int)
+ (int_seq_from_string prefix min_int)
+ fun lookup_bool_assigns read prefix =
+ lookup_assigns read prefix "" (the o parse_bool_option false prefix)
fun lookup_bool_option_assigns read prefix =
- (NONE, lookup_bool_option prefix)
- :: map (fn (name, value) =>
- (SOME (read (String.extract (name, size prefix + 1, NONE))),
- value |> stringify_raw_param_value
- |> parse_bool_option true name))
- (filter (String.isPrefix (prefix ^ " ") o fst) raw_params)
+ lookup_assigns read prefix "" (parse_bool_option true prefix)
+ fun lookup_strings_assigns read prefix =
+ lookup_assigns read prefix "" (space_explode " ")
fun lookup_time name =
case lookup name of
NONE => NONE
@@ -255,6 +251,7 @@
val show_datatypes = debug orelse lookup_bool "show_datatypes"
val show_consts = debug orelse lookup_bool "show_consts"
val formats = lookup_ints_assigns read_term_polymorphic "format" 0
+ val atomss = lookup_strings_assigns read_type_polymorphic "atoms"
val evals = lookup_term_list "eval"
val max_potential =
if auto then 0 else Int.max (0, lookup_int "max_potential")
@@ -279,9 +276,10 @@
peephole_optim = peephole_optim, timeout = timeout,
tac_timeout = tac_timeout, max_threads = max_threads,
show_datatypes = show_datatypes, show_consts = show_consts,
- formats = formats, evals = evals, max_potential = max_potential,
- max_genuine = max_genuine, check_potential = check_potential,
- check_genuine = check_genuine, batch_size = batch_size, expect = expect}
+ formats = formats, atomss = atomss, evals = evals,
+ max_potential = max_potential, max_genuine = max_genuine,
+ check_potential = check_potential, check_genuine = check_genuine,
+ batch_size = batch_size, expect = expect}
end
fun default_params thy =
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Tue Jun 01 12:20:08 2010 +0200
@@ -31,8 +31,9 @@
nut NameTable.table -> Kodkod.raw_bound list -> nut -> int list list
val dest_plain_fun : term -> bool * (term list * term list)
val reconstruct_hol_model :
- params -> scope -> (term option * int list) list -> styp list -> nut list
- -> nut list -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
+ params -> scope -> (term option * int list) list
+ -> (typ option * string list) list -> styp list -> nut list -> nut list
+ -> nut list -> nut NameTable.table -> Kodkod.raw_bound list
-> Pretty.T * bool
val prove_hol_model :
scope -> Time.time option -> nut list -> nut list -> nut NameTable.table
@@ -103,31 +104,41 @@
(** Term reconstruction **)
-fun nth_atom_suffix pool s j k =
- (case AList.lookup (op =) (!pool) (s, k) of
- SOME js =>
- (case find_index (curry (op =) j) js of
- ~1 => (Unsynchronized.change pool (cons ((s, k), j :: js));
- length js + 1)
- | n => length js - n)
- | NONE => (Unsynchronized.change pool (cons ((s, k), [j])); 1))
- |> nat_subscript
- |> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
+fun nth_atom_number pool T j =
+ case AList.lookup (op =) (!pool) T of
+ SOME js =>
+ (case find_index (curry (op =) j) js of
+ ~1 => (Unsynchronized.change pool (cons (T, j :: js));
+ length js + 1)
+ | n => length js - n)
+ | NONE => (Unsynchronized.change pool (cons (T, [j])); 1)
+fun atom_suffix s =
+ nat_subscript
+ #> (s <> "" andalso Symbol.is_ascii_digit (List.last (explode s)))
? prefix "\<^isub>,"
-fun nth_atom_name pool prefix (Type (s, _)) j k =
- let val s' = shortest_name s in
- prefix ^ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
- nth_atom_suffix pool s j k
- end
- | nth_atom_name pool prefix (TFree (s, _)) j k =
- prefix ^ perhaps (try (unprefix "'")) s ^ nth_atom_suffix pool s j k
- | nth_atom_name _ _ T _ _ =
- raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
-fun nth_atom pool for_auto T j k =
+fun nth_atom_name thy atomss pool prefix T j =
+ let
+ val ss = these (triple_lookup (type_match thy) atomss T)
+ val m = nth_atom_number pool T j
+ in
+ if m <= length ss then
+ nth ss (m - 1)
+ else case T of
+ Type (s, _) =>
+ let val s' = shortest_name s in
+ prefix ^
+ (if String.isPrefix "\\" s' then s' else substring (s', 0, 1)) ^
+ atom_suffix s m
+ end
+ | TFree (s, _) => prefix ^ perhaps (try (unprefix "'")) s ^ atom_suffix s m
+ | _ => raise TYPE ("Nitpick_Model.nth_atom_name", [T], [])
+ end
+fun nth_atom thy atomss pool for_auto T j =
if for_auto then
- Free (nth_atom_name pool (hd (space_explode "." nitpick_prefix)) T j k, T)
+ Free (nth_atom_name thy atomss pool (hd (space_explode "." nitpick_prefix))
+ T j, T)
else
- Const (nth_atom_name pool "" T j k, T)
+ Const (nth_atom_name thy atomss pool "" T j, T)
fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
@@ -300,14 +311,14 @@
strict_type_match thy (candid_T, Logic.varifyT_global pat_T)
fun all_values_of_type pool wacky_names (scope as {card_assigns, ...} : scope)
- sel_names rel_table bounds card T =
+ atomss sel_names rel_table bounds card T =
let
val card = if card = 0 then card_of_type card_assigns T else card
fun nth_value_of_type n =
let
fun term unfold =
- reconstruct_term unfold pool wacky_names scope sel_names rel_table
- bounds T T (Atom (card, 0)) [[n]]
+ reconstruct_term unfold pool wacky_names scope atomss sel_names
+ rel_table bounds T T (Atom (card, 0)) [[n]]
in
case term false of
t as Const (s, _) =>
@@ -320,7 +331,8 @@
in index_seq 0 card |> map nth_value_of_type |> sort nice_term_ord end
and reconstruct_term unfold pool (wacky_names as ((maybe_name, abs_name), _))
(scope as {hol_ctxt as {thy, ctxt, stds, ...}, binarize, card_assigns,
- bits, datatypes, ofs, ...}) sel_names rel_table bounds =
+ bits, datatypes, ofs, ...})
+ atomss sel_names rel_table bounds =
let
val for_auto = (maybe_name = "")
fun value_of_bits jss =
@@ -332,7 +344,8 @@
js 0
end
val all_values =
- all_values_of_type pool wacky_names scope sel_names rel_table bounds 0
+ all_values_of_type pool wacky_names scope atomss sel_names rel_table
+ bounds 0
fun postprocess_term (Type (@{type_name fun}, _)) = I
| postprocess_term T =
if null (Data.get thy) then
@@ -471,16 +484,16 @@
else if T = @{typ bisim_iterator} then
HOLogic.mk_number nat_T j
else case datatype_spec datatypes T of
- NONE => nth_atom pool for_auto T j k
- | SOME {deep = false, ...} => nth_atom pool for_auto T j k
+ NONE => nth_atom thy atomss pool for_auto T j
+ | SOME {deep = false, ...} => nth_atom thy atomss pool for_auto T j
| SOME {co, standard, constrs, ...} =>
let
fun tuples_for_const (s, T) =
tuple_list_for_name rel_table bounds (ConstName (s, T, Any))
fun cyclic_atom () =
- nth_atom pool for_auto (Type (cyclic_type_name, [])) j k
- fun cyclic_var () = Var ((nth_atom_name pool "" T j k, 0), T)
-
+ nth_atom thy atomss pool for_auto (Type (cyclic_type_name, [])) j
+ fun cyclic_var () =
+ Var ((nth_atom_name thy atomss pool "" T j, 0), T)
val discr_jsss = map (tuples_for_const o discr_for_constr o #const)
constrs
val real_j = j + offset_of_type ofs T
@@ -612,7 +625,7 @@
else term_for_rep true seen T T' R jss
| term_for_rep _ _ T _ R jss =
raise ARG ("Nitpick_Model.reconstruct_term.term_for_rep",
- Refute.string_of_typ T ^ " " ^ string_for_rep R ^ " " ^
+ Syntax.string_of_typ ctxt T ^ " " ^ string_for_rep R ^ " " ^
string_of_int (length jss))
in
postprocess_subterms [] o polish_funs [] o unarize_unbox_etc_term
@@ -811,10 +824,10 @@
(** Model reconstruction **)
-fun term_for_name pool scope sel_names rel_table bounds name =
+fun term_for_name pool scope atomss sel_names rel_table bounds name =
let val T = type_of name in
tuple_list_for_name rel_table bounds name
- |> reconstruct_term false pool (("", ""), ("", "")) scope sel_names
+ |> reconstruct_term false pool (("", ""), ("", "")) scope atomss sel_names
rel_table bounds T T (rep_of name)
end
@@ -848,7 +861,8 @@
ground_thm_table, ersatz_table, skolems, special_funs,
unrolled_preds, wf_cache, constr_cache},
binarize, card_assigns, bits, bisim_depth, datatypes, ofs} : scope)
- formats all_frees free_names sel_names nonsel_names rel_table bounds =
+ formats atomss all_frees free_names sel_names nonsel_names rel_table
+ bounds =
let
val pool = Unsynchronized.ref []
val (wacky_names as (_, base_step_names), ctxt) =
@@ -871,11 +885,10 @@
{hol_ctxt = hol_ctxt, binarize = binarize, card_assigns = card_assigns,
bits = bits, bisim_depth = bisim_depth, datatypes = datatypes, ofs = ofs}
fun term_for_rep unfold =
- reconstruct_term unfold pool wacky_names scope sel_names rel_table bounds
+ reconstruct_term unfold pool wacky_names scope atomss sel_names rel_table
+ bounds
fun nth_value_of_type card T n =
- let
- fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]]
- in
+ let fun aux unfold = term_for_rep unfold T T (Atom (card, 0)) [[n]] in
case aux false of
t as Const (s, _) =>
if String.isPrefix cyclic_const_prefix s then
@@ -885,7 +898,8 @@
| t => t
end
val all_values =
- all_values_of_type pool wacky_names scope sel_names rel_table bounds
+ all_values_of_type pool wacky_names scope atomss sel_names rel_table
+ bounds
fun is_codatatype_wellformed (cos : dtype_spec list)
({typ, card, ...} : dtype_spec) =
let
@@ -996,9 +1010,10 @@
auto_timeout free_names sel_names rel_table bounds prop =
let
val pool = Unsynchronized.ref []
+ val atomss = [(NONE, [])]
fun free_type_assm (T, k) =
let
- fun atom j = nth_atom pool true T j k
+ fun atom j = nth_atom thy atomss pool true T j
fun equation_for_atom j = HOLogic.eq_const T $ Bound 0 $ atom j
val eqs = map equation_for_atom (index_seq 0 k)
val compreh_assm =
@@ -1008,7 +1023,8 @@
in s_conj (compreh_assm, distinct_assm) end
fun free_name_assm name =
HOLogic.mk_eq (Free (nickname_of name, type_of name),
- term_for_name pool scope sel_names rel_table bounds name)
+ term_for_name pool scope atomss sel_names rel_table bounds
+ name)
val freeT_assms = map free_type_assm (filter (is_TFree o fst) card_assigns)
val model_assms = map free_name_assm free_names
val assm = foldr1 s_conj (freeT_assms @ model_assms)
--- a/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_mono.ML Tue Jun 01 12:20:08 2010 +0200
@@ -290,7 +290,7 @@
end
else
MType (s, [])
- | _ => MType (Refute.string_of_typ T, [])
+ | _ => MType (simple_string_of_typ T, [])
in do_type end
fun prodM_factors (MPair (M1, M2)) = maps prodM_factors [M1, M2]
--- a/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_preproc.ML Tue Jun 01 12:20:08 2010 +0200
@@ -910,14 +910,14 @@
\add_axioms_for_term",
"too many nested axioms (" ^
string_of_int depth ^ ")")
- else if Refute.is_const_of_class thy x then
+ else if is_of_class_const thy x then
let
val class = Logic.class_of_const s
val of_class = Logic.mk_of_class (TVar (("'a", 0), [class]),
class)
val ax1 = try (specialize_type thy x) of_class
val ax2 = Option.map (specialize_type thy x o snd)
- (Refute.get_classdef thy class)
+ (get_class_def thy class)
in
fold (add_maybe_def_axiom depth) (map_filter I [ax1, ax2])
accum
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 11:58:50 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Tue Jun 01 12:20:08 2010 +0200
@@ -57,8 +57,15 @@
val bool_T : typ
val nat_T : typ
val int_T : typ
+ val simple_string_of_typ : typ -> string
+ val is_real_constr : theory -> string * typ -> bool
+ val typ_of_dtyp :
+ Datatype_Aux.descr -> (Datatype_Aux.dtyp * typ) list -> Datatype_Aux.dtyp
+ -> typ
+ val is_of_class_const : theory -> string * typ -> bool
+ val get_class_def : theory -> string -> (string * term) option
val monomorphic_term : Type.tyenv -> term -> term
- val specialize_type : theory -> (string * typ) -> term -> term
+ val specialize_type : theory -> string * typ -> term -> term
val nat_subscript : int -> string
val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b
val DETERM_TIMEOUT : Time.time option -> tactic -> tactic
@@ -229,6 +236,11 @@
val nat_T = @{typ nat}
val int_T = @{typ int}
+val simple_string_of_typ = Refute.string_of_typ
+val is_real_constr = Refute.is_IDT_constructor
+val typ_of_dtyp = Refute.typ_of_dtyp
+val is_of_class_const = Refute.is_const_of_class
+val get_class_def = Refute.get_classdef
val monomorphic_term = Sledgehammer_Util.monomorphic_term
val specialize_type = Sledgehammer_Util.specialize_type