# HG changeset patch # User blanchet # Date 1275387608 -7200 # Node ID dde817e6dfb1b779689409d428140e730a314197 # Parent a66851c4c5f832986015d79b4b38c130cfe50c4e added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML" diff -r a66851c4c5f8 -r dde817e6dfb1 NEWS --- 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 diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/HISTORY --- 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", diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick.ML --- 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 diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_hol.ML --- 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 diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_isar.ML --- 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 = diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_model.ML --- 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) diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_mono.ML --- 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] diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_preproc.ML --- 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 diff -r a66851c4c5f8 -r dde817e6dfb1 src/HOL/Tools/Nitpick/nitpick_util.ML --- 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