--- 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
(*
--- 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
--- 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
--- 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
--- 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)
--- 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 = {
--- 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;