--- a/src/HOL/Nitpick.thy Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Nitpick.thy Fri Feb 12 19:44:37 2010 +0100
@@ -37,7 +37,7 @@
and bisim_iterator_max :: bisim_iterator
and Quot :: "'a \<Rightarrow> 'b"
and quot_normal :: "'a \<Rightarrow> 'a"
- and NonStd :: "'a \<Rightarrow> 'b"
+ and Silly :: "'a \<Rightarrow> 'b"
and Tha :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
datatype ('a, 'b) pair_box = PairBox 'a 'b
@@ -254,7 +254,7 @@
setup {* Nitpick_Isar.setup *}
hide (open) const unknown is_unknown undefined_fast_The undefined_fast_Eps bisim
- bisim_iterator_max Quot quot_normal NonStd Tha PairBox FunBox Word refl' wf'
+ bisim_iterator_max Quot quot_normal Silly Tha PairBox FunBox Word refl' wf'
wf_wfrec wf_wfrec' wfrec' card' setsum' fold_graph' nat_gcd nat_lcm int_gcd
int_lcm Frac Abs_Frac Rep_Frac zero_frac one_frac num denom norm_frac frac
plus_frac times_frac uminus_frac number_of_frac inverse_frac less_eq_frac
--- a/src/HOL/Tools/Nitpick/kodkod_sat.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/kodkod_sat.ML Fri Feb 12 19:44:37 2010 +0100
@@ -9,7 +9,7 @@
sig
val configured_sat_solvers : bool -> string list
val smart_sat_solver_name : bool -> string
- val sat_solver_spec : bool -> string -> string * string list
+ val sat_solver_spec : string -> string * string list
end;
structure Kodkod_SAT : KODKOD_SAT =
@@ -51,15 +51,15 @@
("HaifaSat", ExternalV2 (ToStdout, "HAIFASAT_HOME", "HaifaSat", ["-p", "1"],
"s SATISFIABLE", "v ", "s UNSATISFIABLE"))]
-(* bool -> string -> sink -> string -> string -> string list -> string list
+(* string -> sink -> string -> string -> string list -> string list
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_external overlord name dev home exec args markers =
+fun dynamic_entry_for_external name dev home exec args markers =
case getenv home of
"" => NONE
| dir =>
SOME (name, fn () =>
let
- val serial_str = if overlord then "" else serial_string ()
+ val serial_str = serial_string ()
val base = name ^ serial_str
val out_file = base ^ ".out"
val dir_sep =
@@ -76,9 +76,9 @@
end)
(* bool -> bool -> string * sat_solver_info
-> (string * (unit -> string list)) option *)
-fun dynamic_entry_for_info _ incremental (name, Internal (Java, mode, ss)) =
+fun dynamic_entry_for_info incremental (name, Internal (Java, mode, ss)) =
if incremental andalso mode = Batch then NONE else SOME (name, K ss)
- | dynamic_entry_for_info _ incremental (name, Internal (JNI, mode, ss)) =
+ | dynamic_entry_for_info incremental (name, Internal (JNI, mode, ss)) =
if incremental andalso mode = Batch then
NONE
else
@@ -92,26 +92,25 @@
else
NONE
end
- | dynamic_entry_for_info overlord false
- (name, External (dev, home, exec, args)) =
- dynamic_entry_for_external overlord name dev home exec args []
- | dynamic_entry_for_info overlord false
+ | dynamic_entry_for_info false (name, External (dev, home, exec, args)) =
+ dynamic_entry_for_external name dev home exec args []
+ | dynamic_entry_for_info false
(name, ExternalV2 (dev, home, exec, args, m1, m2, m3)) =
- dynamic_entry_for_external overlord name dev home exec args [m1, m2, m3]
- | dynamic_entry_for_info _ true _ = NONE
-(* bool -> bool -> (string * (unit -> string list)) list *)
-fun dynamic_list overlord incremental =
- map_filter (dynamic_entry_for_info overlord incremental) static_list
+ dynamic_entry_for_external name dev home exec args [m1, m2, m3]
+ | dynamic_entry_for_info true _ = NONE
+(* bool -> (string * (unit -> string list)) list *)
+fun dynamic_list incremental =
+ map_filter (dynamic_entry_for_info incremental) static_list
(* bool -> string list *)
-val configured_sat_solvers = map fst o dynamic_list false
+val configured_sat_solvers = map fst o dynamic_list
(* bool -> string *)
-val smart_sat_solver_name = fst o hd o dynamic_list false
+val smart_sat_solver_name = fst o hd o dynamic_list
-(* bool -> string -> string * string list *)
-fun sat_solver_spec overlord name =
+(* string -> string * string list *)
+fun sat_solver_spec name =
let
- val dyn_list = dynamic_list overlord false
+ val dyn_list = dynamic_list false
(* (string * 'a) list -> string *)
fun enum_solvers solvers =
commas (distinct (op =) (map (quote o fst) solvers))
--- a/src/HOL/Tools/Nitpick/nitpick.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Fri Feb 12 19:44:37 2010 +0100
@@ -398,7 +398,7 @@
val _ = if standard andalso not (null induct_dataTs) then
pprint_m (fn () => Pretty.blk (0,
pstrs "Hint: To check that the induction hypothesis is \
- \general enough, try the following command: " @
+ \general enough, try this command: " @
[Pretty.mark Markup.sendback (Pretty.blk (0,
pstrs ("nitpick [" ^
commas (map (prefix "non_std " o maybe_quote
@@ -504,7 +504,7 @@
val comment = (if liberal then "liberal" else "conservative") ^ "\n" ^
PrintMode.setmp [] multiline_string_for_scope scope
val kodkod_sat_solver =
- Kodkod_SAT.sat_solver_spec overlord effective_sat_solver |> snd
+ Kodkod_SAT.sat_solver_spec effective_sat_solver |> snd
val bit_width = if bits = 0 then 16 else bits + 1
val delay = if liberal then
Option.map (fn time => Time.- (time, Time.now ()))
--- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Fri Feb 12 19:44:37 2010 +0100
@@ -844,7 +844,7 @@
(s', map (Refute.typ_of_dtyp descr (dtyps ~~ Ts)) Us
---> T)) constrs
|> (triple_lookup (type_match thy) stds T |> the |> not) ?
- cons (@{const_name NonStd}, @{typ \<xi>} --> T)
+ cons (@{const_name Silly}, @{typ \<xi>} --> T)
end
| NONE =>
if is_record_type T then
@@ -1393,7 +1393,7 @@
fun optimized_case_def (hol_ctxt as {thy, ...}) dataT res_T =
let
val xs = datatype_constrs hol_ctxt dataT
- val xs' = filter_out (fn (s, _) => s = @{const_name NonStd}) xs
+ val xs' = filter_out (curry (op =) @{const_name Silly} o fst) xs
val func_Ts = map ((fn T => binder_types T ---> res_T) o snd) xs'
in
(if length xs = length xs' then
--- a/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_kodkod.ML Fri Feb 12 19:44:37 2010 +0100
@@ -317,7 +317,7 @@
[ts] |> not exclusive ? cons (KK.TupleSet [])
else
[KK.TupleSet [],
- if (* ### exclusive andalso*) T1 = T2 andalso epsilon > delta then
+ if T1 = T2 andalso epsilon > delta then
index_seq delta (epsilon - delta)
|> map (fn j =>
KK.TupleProduct (KK.TupleSet [Kodkod.Tuple [j + j0]],
@@ -770,45 +770,47 @@
val empty_rel = KK.Product (KK.None, KK.None)
(* nfa_table -> typ -> typ -> KK.rel_expr list *)
-fun direct_path_rel_exprs nfa start final =
- case AList.lookup (op =) nfa final of
- SOME trans => map fst (filter (curry (op =) start o snd) trans)
+fun direct_path_rel_exprs nfa start_T final_T =
+ case AList.lookup (op =) nfa final_T of
+ SOME trans => map fst (filter (curry (op =) start_T o snd) trans)
| NONE => []
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> KK.rel_expr *)
-and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start final =
- fold kk_union (direct_path_rel_exprs nfa start final)
- (if start = final then KK.Iden else empty_rel)
- | any_path_rel_expr (kk as {kk_union, ...}) nfa (q :: qs) start final =
- kk_union (any_path_rel_expr kk nfa qs start final)
- (knot_path_rel_expr kk nfa qs start q final)
+and any_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T
+ final_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T final_T)
+ (if start_T = final_T then KK.Iden else empty_rel)
+ | any_path_rel_expr (kk as {kk_union, ...}) nfa (T :: Ts) start_T final_T =
+ kk_union (any_path_rel_expr kk nfa Ts start_T final_T)
+ (knot_path_rel_expr kk nfa Ts start_T T final_T)
(* kodkod_constrs -> nfa_table -> typ list -> typ -> typ -> typ
-> KK.rel_expr *)
-and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa qs start
- knot final =
- kk_join (kk_join (any_path_rel_expr kk nfa qs knot final)
- (kk_reflexive_closure (loop_path_rel_expr kk nfa qs knot)))
- (any_path_rel_expr kk nfa qs start knot)
+and knot_path_rel_expr (kk as {kk_join, kk_reflexive_closure, ...}) nfa Ts
+ start_T knot_T final_T =
+ kk_join (kk_join (any_path_rel_expr kk nfa Ts knot_T final_T)
+ (kk_reflexive_closure (loop_path_rel_expr kk nfa Ts knot_T)))
+ (any_path_rel_expr kk nfa Ts start_T knot_T)
(* kodkod_constrs -> nfa_table -> typ list -> typ -> KK.rel_expr *)
-and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start =
- fold kk_union (direct_path_rel_exprs nfa start start) empty_rel
- | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (q :: qs) start =
- if start = q then
- kk_closure (loop_path_rel_expr kk nfa qs start)
+and loop_path_rel_expr ({kk_union, ...} : kodkod_constrs) nfa [] start_T =
+ fold kk_union (direct_path_rel_exprs nfa start_T start_T) empty_rel
+ | loop_path_rel_expr (kk as {kk_union, kk_closure, ...}) nfa (T :: Ts)
+ start_T =
+ if start_T = T then
+ kk_closure (loop_path_rel_expr kk nfa Ts start_T)
else
- kk_union (loop_path_rel_expr kk nfa qs start)
- (knot_path_rel_expr kk nfa qs start q start)
+ kk_union (loop_path_rel_expr kk nfa Ts start_T)
+ (knot_path_rel_expr kk nfa Ts start_T T start_T)
(* nfa_table -> unit NfaGraph.T *)
fun graph_for_nfa nfa =
let
(* typ -> unit NfaGraph.T -> unit NfaGraph.T *)
- fun new_node q = perhaps (try (NfaGraph.new_node (q, ())))
+ fun new_node T = perhaps (try (NfaGraph.new_node (T, ())))
(* nfa_table -> unit NfaGraph.T -> unit NfaGraph.T *)
fun add_nfa [] = I
| add_nfa ((_, []) :: nfa) = add_nfa nfa
- | add_nfa ((q, ((_, q') :: transitions)) :: nfa) =
- add_nfa ((q, transitions) :: nfa) o NfaGraph.add_edge (q, q') o
- new_node q' o new_node q
+ | add_nfa ((T, ((_, T') :: transitions)) :: nfa) =
+ add_nfa ((T, transitions) :: nfa) o NfaGraph.add_edge (T, T') o
+ new_node T' o new_node T
in add_nfa nfa NfaGraph.empty end
(* nfa_table -> nfa_table list *)
@@ -816,17 +818,17 @@
nfa |> graph_for_nfa |> NfaGraph.strong_conn
|> map (fn keys => filter (member (op =) keys o fst) nfa)
-(* dtype_spec list -> kodkod_constrs -> nfa_table -> typ -> KK.formula *)
-fun acyclicity_axiom_for_datatype dtypes kk nfa start =
+(* kodkod_constrs -> dtype_spec list -> nfa_table -> typ -> KK.formula *)
+fun acyclicity_axiom_for_datatype kk dtypes nfa start_T =
#kk_no kk (#kk_intersect kk
- (loop_path_rel_expr kk nfa (map fst nfa) start) KK.Iden)
+ (loop_path_rel_expr kk nfa (map fst nfa) start_T) KK.Iden)
(* hol_context -> kodkod_constrs -> nut NameTable.table -> dtype_spec list
-> KK.formula list *)
fun acyclicity_axioms_for_datatypes hol_ctxt kk rel_table dtypes =
map_filter (nfa_entry_for_datatype hol_ctxt kk rel_table dtypes) dtypes
|> strongly_connected_sub_nfas
- |> maps (fn nfa => map (acyclicity_axiom_for_datatype dtypes kk nfa o fst)
- nfa)
+ |> maps (fn nfa =>
+ map (acyclicity_axiom_for_datatype kk dtypes nfa o fst) nfa)
(* hol_context -> int -> kodkod_constrs -> nut NameTable.table -> KK.rel_expr
-> constr_spec -> int -> KK.formula *)
--- a/src/HOL/Tools/Nitpick/nitpick_model.ML Wed Feb 10 11:47:33 2010 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick_model.ML Fri Feb 12 19:44:37 2010 +0100
@@ -88,7 +88,7 @@
Const (nth_atom_name pool "" T j k, T)
(* term -> real *)
-fun extract_real_number (Const (@{const_name Rings.divide}, _) $ t1 $ t2) =
+fun extract_real_number (Const (@{const_name divide}, _) $ t1 $ t2) =
real (snd (HOLogic.dest_number t1)) / real (snd (HOLogic.dest_number t2))
| extract_real_number t = real (snd (HOLogic.dest_number t))
(* term * term -> order *)
@@ -459,7 +459,7 @@
0 => mk_num 0
| n1 => case HOLogic.dest_number t2 |> snd of
1 => mk_num n1
- | n2 => Const (@{const_name Rings.divide},
+ | n2 => Const (@{const_name divide},
num_T --> num_T --> num_T)
$ mk_num n1 $ mk_num n2)
| _ => raise TERM ("Nitpick_Model.reconstruct_term.\
@@ -470,7 +470,7 @@
constr_s = @{const_name Quot}) then
Const (abs_name, constr_T) $ the_single ts
else if not for_auto andalso
- constr_s = @{const_name NonStd} then
+ constr_s = @{const_name Silly} then
Const (fst (dest_Const (the_single ts)), T)
else
list_comb (Const constr_x, ts)