# HG changeset patch # User blanchet # Date 1258124393 -3600 # Node ID 947184dc75c9895a78e07d6e12ed80c7c552e082 # Parent feaf3627a844096d59508fbf71cbe009e5a15fa3 removed a few global names in Nitpick (styp, nat_less, pairf) diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick.ML --- a/src/HOL/Tools/Nitpick/nitpick.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Nov 13 15:59:53 2009 +0100 @@ -7,6 +7,7 @@ signature NITPICK = sig + type styp = Nitpick_Util.styp type params = { cards_assigns: (typ option * int list) list, maxes_assigns: (styp option * int list) list, @@ -231,9 +232,8 @@ else neg_t val (assms_t, evals) = - assms_t :: evals - |> merge_type_vars ? merge_type_vars_in_terms - |> hd pairf tl + assms_t :: evals |> merge_type_vars ? merge_type_vars_in_terms + |> pairf hd tl val original_max_potential = max_potential val original_max_genuine = max_genuine (* diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_hol.ML --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Nov 13 15:59:53 2009 +0100 @@ -7,6 +7,7 @@ signature NITPICK_HOL = sig + type styp = Nitpick_Util.styp type const_table = term list Symtab.table type special_fun = (styp * int list * term list) * styp type unrolled = styp * styp @@ -1499,7 +1500,7 @@ SOME n => let val (dataT, res_T) = nth_range_type n T - |> domain_type pairf range_type + |> pairf domain_type range_type in (optimized_case_def ext_ctxt dataT res_T |> do_term (depth + 1) Ts, ts) @@ -1675,8 +1676,8 @@ | NONE => let val goal = prop |> cterm_of thy |> Goal.init - val wf = silence (exists (terminates_by ctxt tac_timeout goal)) - termination_tacs + val wf = exists (terminates_by ctxt tac_timeout goal) + termination_tacs in Unsynchronized.change cached_wf_props (cons (prop, wf)); wf end end) handle List.Empty => false diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_kodkod.ML --- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Nov 13 15:59:53 2009 +0100 @@ -216,7 +216,7 @@ ("int_add", tabulate_int_op2 debug univ_card (int_card, j0) (op +)) else if Kodkod.Rel x = nat_subtract_rel then ("nat_subtract", - tabulate_op2 debug univ_card (nat_card, j0) j0 (op nat_minus)) + tabulate_op2 debug univ_card (nat_card, j0) j0 (uncurry nat_minus)) else if Kodkod.Rel x = int_subtract_rel then ("int_subtract", tabulate_int_op2 debug univ_card (int_card, j0) (op -)) else if Kodkod.Rel x = nat_multiply_rel then diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_model.ML --- a/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Nov 13 15:59:53 2009 +0100 @@ -7,6 +7,7 @@ signature NITPICK_MODEL = sig + type styp = Nitpick_Util.styp type scope = Nitpick_Scope.scope type rep = Nitpick_Rep.rep type nut = Nitpick_Nut.nut @@ -636,7 +637,7 @@ ||> filter_out (equal @{const_name bisim_iterator_max} o nickname_of) val free_names = map (fn x as (s, T) => - case filter (equal x o nickname_of pairf (unbox_type o type_of)) + case filter (equal x o pairf nickname_of (unbox_type o type_of)) free_names of [name] => name | [] => FreeName (s, T, Any) @@ -698,8 +699,8 @@ | TimeLimit.TimeOut => false end in - if silence try_out false then SOME true - else if silence try_out true then SOME false + if try_out false then SOME true + else if try_out true then SOME false else NONE end diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_peephole.ML --- a/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_peephole.ML Fri Nov 13 15:59:53 2009 +0100 @@ -531,7 +531,7 @@ | _ => raise SAME () else if r22 = nat_subtract_rel then case (r21, r1) of - (Atom j1, Atom j2) => from_nat (to_nat j1 nat_minus to_nat j2) + (Atom j1, Atom j2) => from_nat (nat_minus (to_nat j1) (to_nat j2)) | _ => raise SAME () else if r22 = nat_multiply_rel then case (r21, r1) of @@ -581,11 +581,11 @@ let val arity2 = arity_of_rel_expr r2 val arity1 = arity - arity2 - val n1 = Int.min (arity1 nat_minus j0, n) + val n1 = Int.min (nat_minus arity1 j0, n) val n2 = n - n1 (* unit -> rel_expr *) fun one () = aux arity1 r1 j0 n1 - fun two () = aux arity2 r2 (j0 nat_minus arity1) n2 + fun two () = aux arity2 r2 (nat_minus j0 arity1) n2 in case (n1, n2) of (0, _) => s_rel_if (s_some r1) (two ()) (empty_n_ary_rel n2) diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_scope.ML --- a/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_scope.ML Fri Nov 13 15:59:53 2009 +0100 @@ -7,6 +7,7 @@ signature NITPICK_SCOPE = sig + type styp = Nitpick_Util.styp type extended_context = Nitpick_HOL.extended_context type constr_spec = { diff -r feaf3627a844 -r 947184dc75c9 src/HOL/Tools/Nitpick/nitpick_util.ML --- a/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 13 06:24:31 2009 +0100 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Fri Nov 13 15:59:53 2009 +0100 @@ -5,18 +5,9 @@ General-purpose functions used by the Nitpick modules. *) -infix 6 nat_minus -infix 7 pairf - -signature BASIC_NITPICK_UTIL = +signature NITPICK_UTIL = sig type styp = string * typ -end; - -signature NITPICK_UTIL = -sig - include BASIC_NITPICK_UTIL - datatype polarity = Pos | Neg | Neut exception ARG of string * string @@ -27,9 +18,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 pairf : ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c val int_for_bool : bool -> int - val nat_minus : int * int -> int + val nat_minus : int -> int -> int val reasonable_power : int -> int -> int val exact_log : int -> int -> int val exact_root : int -> int -> int @@ -63,7 +54,6 @@ val subscript : string -> string val nat_subscript : int -> string val time_limit : Time.time option -> ('a -> 'b) -> 'a -> 'b - val silence : ('a -> 'b) -> 'a -> 'b val DETERM_TIMEOUT : Time.time option -> tactic -> tactic val setmp_show_all_types : ('a -> 'b) -> 'a -> 'b val indent_size : int @@ -90,13 +80,13 @@ (* ('a * 'b * 'c -> 'd) -> 'a -> 'b -> 'c -> 'd *) fun curry3 f = fn x => fn y => fn z => f (x, y, z) -(* ('a -> 'b) * ('a -> 'c) -> 'a -> 'b * 'c *) -fun (f pairf g) = fn x => (f x, g x) +(* ('a -> 'b) -> ('a -> 'c) -> 'a -> 'b * 'c *) +fun pairf f g x = (f x, g x) (* bool -> int *) fun int_for_bool b = if b then 1 else 0 -(* int * int -> int *) -fun (i nat_minus j) = if i > j then i - j else 0 +(* int -> int -> int *) +fun nat_minus i j = if i > j then i - j else 0 val max_exponent = 16384 @@ -263,15 +253,6 @@ fun time_limit NONE f = f | time_limit (SOME delay) f = TimeLimit.timeLimit delay f -(* (string -> unit) Unsynchronized.ref -> ('a -> 'b) -> 'a -> 'b *) -fun silence_one out_fn = setmp_CRITICAL out_fn (K ()) - -(* ('a -> 'b) -> 'a -> 'b *) -fun silence f = - fold silence_one - [Output.writeln_fn, Output.priority_fn, Output.tracing_fn, - Output.warning_fn, Output.error_fn, Output.debug_fn] f - (* Time.time option -> tactic -> tactic *) fun DETERM_TIMEOUT delay tac st = Seq.of_list (the_list (time_limit delay (fn () => SINGLE tac st) ())) @@ -302,6 +283,3 @@ end end; - -structure Basic_Nitpick_Util : BASIC_NITPICK_UTIL = Nitpick_Util; -open Basic_Nitpick_Util;